feat: LawfulBEq must be reflexive

src/Init/Core.lean

@@ -178,21 +178,22 @@ infix:50 " != " => bne
 
 class LawfulBEq (α : Type u) [BEq α] : Prop where
   eq_of_beq : (a b : α) → (a == b) = true → a = b
+  rfl : (a : α) → (a == a) = true
 
 theorem eq_of_beq [BEq α] [LawfulBEq α] {a b : α} (h : (a == b) = true) : a = b :=
   LawfulBEq.eq_of_beq a b h
 
 instance : LawfulBEq Bool where
   eq_of_beq a b h := by cases a <;> cases b <;> first | rfl | contradiction
-
-instance : LawfulBEq Nat where
-  eq_of_beq _ _ h := of_decide_eq_true h
+  rfl a := by cases a <;> decide
 
 instance : LawfulBEq Char where
   eq_of_beq _ _  h := of_decide_eq_true h
+  rfl a := of_decide_eq_self_eq_true a
 
 instance : LawfulBEq String where
   eq_of_beq _ _  h := of_decide_eq_true h
+  rfl a := of_decide_eq_self_eq_true a
 
 /- Logical connectives an equality -/
 

src/Init/Data/List/Basic.lean

@@ -483,5 +483,9 @@ instance [BEq α] [LawfulBEq α] : LawfulBEq (List α) where
         simp [BEq.beq, List.beq]
         intro ⟨h₁, h₂⟩
         exact ⟨eq_of_beq h₁, ih _ h₂⟩
+  rfl as := by
+    induction as with
+    | nil => rfl
+    | cons a as ih => simp [BEq.beq, List.beq, LawfulBEq.rfl]; exact ih
 
 end List

src/Init/Data/Nat/Basic.lean

@@ -60,6 +60,10 @@ def blt (a b : Nat) : Bool :=
 @[simp] theorem ble_eq : (Nat.ble x y = true) = (x ≤ y) := propext <| Iff.intro Nat.le_of_ble_eq_true Nat.ble_eq_true_of_le
 @[simp] theorem blt_eq : (Nat.blt x y = true) = (x < y) := propext <| Iff.intro Nat.le_of_ble_eq_true Nat.ble_eq_true_of_le
 
+instance : LawfulBEq Nat where
+  eq_of_beq _ _ h := of_decide_eq_true h
+  rfl a := by simp [BEq.beq]
+
 /- Nat.add theorems -/
 
 @[simp] protected theorem zero_add : ∀ (n : Nat), 0 + n = n

src/Init/Data/Nat/Linear.lean

@@ -179,6 +179,10 @@ instance : LawfulBEq PolyCnstr where
     simp at h
     have ⟨⟨h₁, h₂⟩, h₃⟩ := h
     rw [h₁, eq_of_beq h₂, eq_of_beq h₃]
+  rfl a := by
+    cases a; rename_i eq lhs rhs
+    show (eq == eq && lhs == lhs && rhs == rhs) = true
+    simp [LawfulBEq.rfl]
 
 def PolyCnstr.mul (k : Nat) (c : PolyCnstr) : PolyCnstr :=
   { c with lhs := c.lhs.mul k, rhs := c.rhs.mul k }

src/Init/Data/Prod.lean

@@ -8,3 +8,4 @@ import Init.SimpLemmas
 
 instance [BEq α] [BEq β] [LawfulBEq α] [LawfulBEq β] : LawfulBEq (α × β) where
   eq_of_beq a b h := by cases a; cases b; simp [BEq.beq] at h; have ⟨h₁, h₂⟩ := h; rw [eq_of_beq h₁, eq_of_beq h₂]
+  rfl a := by cases a; simp [BEq.beq, LawfulBEq.rfl]

src/Init/Prelude.lean

@@ -300,6 +300,11 @@ theorem of_decide_eq_false [s : Decidable p] : Eq (decide p) false → Not p :=
   | isTrue  h₁ => absurd h (ne_false_of_eq_true (decide_eq_true h₁))
   | isFalse h₁ => h₁
 
+theorem of_decide_eq_self_eq_true [s : DecidableEq α] (a : α) : Eq (decide (Eq a a)) true :=
+  match (generalizing := false) s a a with
+  | isTrue  h₁ => rfl
+  | isFalse h₁ => absurd rfl h₁
+
 @[inline] instance : DecidableEq Bool :=
   fun a b => match a, b with
    | false, false => isTrue rfl

src/Init/SimpLemmas.lean

@@ -157,3 +157,5 @@ theorem Bool.of_not_eq_false {b : Bool} : ¬ (b = false) → b = true := by case
 
 @[simp] theorem cond_true (a b : α) : cond true a b = a := rfl
 @[simp] theorem cond_false (a b : α) : cond false a b = b := rfl
+
+@[simp] theorem beq_self_eq_true [BEq α] [LawfulBEq α] (a : α) : (a == a) = true := LawfulBEq.rfl a