feat: add a proper BEq instance for Nat

src/Init/Data/Nat/Basic.lean

@@ -61,9 +61,17 @@ def blt (a b : Nat) : Bool :=
 @[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
+  eq_of_beq _ _ h := Nat.eq_of_beq_eq_true h
   rfl a := by simp [BEq.beq]
 
+@[simp] theorem beq_eq_true_eq (a b : Nat) : ((a == b) = true) = (a = b) := propext <| Iff.intro eq_of_beq (fun h => by subst h; apply LawfulBEq.rfl)
+@[simp] theorem not_beq_eq_true_eq (a b : Nat) : ((!(a == b)) = true) = ¬(a = b) :=
+  propext <| Iff.intro
+    (fun h₁ h₂ => by subst h₂; rw [LawfulBEq.rfl] at h₁; contradiction)
+    (fun h =>
+      have : ¬ ((a == b) = true) := fun h' => absurd (eq_of_beq h') h
+      by simp [this])
+
 /- Nat.add theorems -/
 
 @[simp] protected theorem zero_add : ∀ (n : Nat), 0 + n = n

src/Init/Prelude.lean

@@ -605,6 +605,9 @@ def Nat.beq : (@& Nat) → (@& Nat) → Bool
   | succ n, zero   => false
   | succ n, succ m => beq n m
 
+instance : BEq Nat where
+  beq := Nat.beq
+
 theorem Nat.eq_of_beq_eq_true : {n m : Nat} → Eq (beq n m) true → Eq n m
   | zero,   zero,   h => rfl
   | zero,   succ m, h => Bool.noConfusion h

src/Init/SimpLemmas.lean

@@ -150,9 +150,6 @@ theorem Bool.of_not_eq_false {b : Bool} : ¬ (b = false) → b = true := by case
 @[simp] theorem decide_not [h : Decidable p] : decide (¬ p) = !decide p := by cases h <;> rfl
 @[simp] theorem not_decide_eq_true [h : Decidable p] : ((!decide p) = true) = ¬ p := by cases h <;> simp [decide, *]
 
-@[simp] theorem Nat.beq_to_eq (a b : Nat) : ((a == b) = true) = (a = b) := by simp [BEq.beq]
-@[simp] theorem Nat.not_beq_to_not_eq (a b : Nat) : ((!(a == b)) = true) = ¬(a = b) := by simp [BEq.beq]
-
 @[simp] theorem heq_eq_eq {α : Sort u} (a b : α) : HEq a b = (a = b) := propext <| Iff.intro eq_of_heq heq_of_eq
 
 @[simp] theorem cond_true (a b : α) : cond true a b = a := rfl

tests/lean/603.lean.expected.out

@@ -2,7 +2,7 @@
 [result]
 def even (x_1 : obj) : obj :=
   let x_2 : obj := 0;
-  let x_3 : u8 := Nat.decEq x_1 x_2;
+  let x_3 : u8 := Nat.beq x_1 x_2;
   case x_3 : u8 of
   Bool.false →
     let x_4 : obj := 1;
@@ -16,7 +16,7 @@ def even (x_1 : obj) : obj :=
     ret x_7
 def odd (x_1 : obj) : obj :=
   let x_2 : obj := 0;
-  let x_3 : u8 := Nat.decEq x_1 x_2;
+  let x_3 : u8 := Nat.beq x_1 x_2;
   case x_3 : u8 of
   Bool.false →
     let x_4 : obj := 1;

tests/lean/eagerCoeExpansion.lean.expected.out

@@ -4,22 +4,9 @@ def r : Nat → Prop :=
 fun a => if (a == 0) = true then (a != 1) = true else (a != 2) = true
 def r : Nat → Prop :=
 fun (a : Nat) =>
-  @ite.{1} Prop
-    (@Eq.{1} Bool
-      (@BEq.beq.{0} Nat (@instBEq.{0} Nat fun (a b : Nat) => instDecidableEqNat a b) a
-        (@OfNat.ofNat.{0} Nat 0 (instOfNatNat 0)))
-      Bool.true)
-    (instDecidableEqBool
-      (@BEq.beq.{0} Nat (@instBEq.{0} Nat fun (a b : Nat) => instDecidableEqNat a b) a
-        (@OfNat.ofNat.{0} Nat 0 (instOfNatNat 0)))
-      Bool.true)
-    (@Eq.{1} Bool
-      (@bne.{0} Nat (@instBEq.{0} Nat fun (a b : Nat) => instDecidableEqNat a b) a
-        (@OfNat.ofNat.{0} Nat 1 (instOfNatNat 1)))
-      Bool.true)
-    (@Eq.{1} Bool
-      (@bne.{0} Nat (@instBEq.{0} Nat fun (a b : Nat) => instDecidableEqNat a b) a
-        (@OfNat.ofNat.{0} Nat 2 (instOfNatNat 2)))
-      Bool.true)
+  @ite.{1} Prop (@Eq.{1} Bool (@BEq.beq.{0} Nat instBEqNat a (@OfNat.ofNat.{0} Nat 0 (instOfNatNat 0))) Bool.true)
+    (instDecidableEqBool (@BEq.beq.{0} Nat instBEqNat a (@OfNat.ofNat.{0} Nat 0 (instOfNatNat 0))) Bool.true)
+    (@Eq.{1} Bool (@bne.{0} Nat instBEqNat a (@OfNat.ofNat.{0} Nat 1 (instOfNatNat 1))) Bool.true)
+    (@Eq.{1} Bool (@bne.{0} Nat instBEqNat a (@OfNat.ofNat.{0} Nat 2 (instOfNatNat 2))) Bool.true)
 def s : Option Nat :=
 HOrElse.hOrElse (ConstantFunction.f myFun 3) fun x => ConstantFunction.f myFun 4

tests/lean/phashmap_inst_coherence.lean.expected.out

@@ -3,6 +3,6 @@ phashmap_inst_coherence.lean:12:6-12:56: error: application type mismatch
 argument
   m
 has type
-  @PersistentHashMap Nat Nat instBEq instHashableNat : Type
+  @PersistentHashMap Nat Nat instBEqNat instHashableNat : Type
 but is expected to have type
-  @PersistentHashMap Nat Nat instBEq natDiffHash : Type
+  @PersistentHashMap Nat Nat instBEqNat natDiffHash : Type