From 0f06fbf64891235d070504474c77a3b20645da78 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 28 Feb 2022 19:15:15 -0800
Subject: [PATCH] feat: `LawfulBEq` must be reflexive

---
 src/Init/Core.lean            | 7 ++++---
 src/Init/Data/List/Basic.lean | 4 ++++
 src/Init/Data/Nat/Basic.lean  | 4 ++++
 src/Init/Data/Nat/Linear.lean | 4 ++++
 src/Init/Data/Prod.lean       | 1 +
 src/Init/Prelude.lean         | 5 +++++
 src/Init/SimpLemmas.lean      | 2 ++
 7 files changed, 24 insertions(+), 3 deletions(-)

diff --git a/src/Init/Core.lean b/src/Init/Core.lean
index 4e8ae36f98..ee209d1f07 100644
--- a/src/Init/Core.lean
+++ b/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 -/
 
diff --git a/src/Init/Data/List/Basic.lean b/src/Init/Data/List/Basic.lean
index a77e0b9926..5e84bff599 100644
--- a/src/Init/Data/List/Basic.lean
+++ b/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
diff --git a/src/Init/Data/Nat/Basic.lean b/src/Init/Data/Nat/Basic.lean
index f29613e388..25a5b96606 100644
--- a/src/Init/Data/Nat/Basic.lean
+++ b/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
diff --git a/src/Init/Data/Nat/Linear.lean b/src/Init/Data/Nat/Linear.lean
index a4417f3eae..db05a780e9 100644
--- a/src/Init/Data/Nat/Linear.lean
+++ b/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 }
diff --git a/src/Init/Data/Prod.lean b/src/Init/Data/Prod.lean
index 6b192a4e3d..f5564dd9dd 100644
--- a/src/Init/Data/Prod.lean
+++ b/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]
diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
index a5b97170c1..6d12bde79f 100644
--- a/src/Init/Prelude.lean
+++ b/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
diff --git a/src/Init/SimpLemmas.lean b/src/Init/SimpLemmas.lean
index 8ff2c6f950..0648058113 100644
--- a/src/Init/SimpLemmas.lean
+++ b/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