feat: normalize != and == in grind (#6870)

This PR adds two new normalization steps in `grind` that reduces `a !=
b` and `a == b` to `decide (¬ a = b)` and `decide (a = b)`,
respectively.

src/Init/Grind/Norm.lean

@@ -61,6 +61,14 @@ theorem Int.lt_eq (a b : Int) : (a < b) = (a + 1 ≤ b) := by
 theorem ge_eq [LE α] (a b : α) : (a ≥ b) = (b ≤ a) := rfl
 theorem gt_eq [LT α] (a b : α) : (a > b) = (b < a) := rfl
 
+theorem beq_eq_decide_eq {_ : BEq α} [LawfulBEq α] [DecidableEq α] (a b : α) : (a == b) = (decide (a = b)) := by
+  by_cases a = b
+  next h => simp [h]
+  next h => simp [beq_eq_false_iff_ne.mpr h, decide_eq_false h]
+
+theorem bne_eq_decide_not_eq {_ : BEq α} [LawfulBEq α] [DecidableEq α] (a b : α) : (a != b) = (decide (¬ a = b)) := by
+  by_cases a = b <;> simp [*]
+
 init_grind_norm
   /- Pre theorems -/
   not_and not_or not_ite not_forall not_exists
@@ -95,9 +103,9 @@ init_grind_norm
   -- Bool not
   Bool.not_not
   -- beq
-  beq_iff_eq
+  beq_iff_eq beq_eq_decide_eq
   -- bne
-  bne_iff_ne
+  bne_iff_ne bne_eq_decide_not_eq
   -- Bool not eq true/false
   Bool.not_eq_true Bool.not_eq_false
   -- decide

tests/lean/run/grind_bool_prop.lean

@@ -17,3 +17,17 @@ example (f : Bool → Nat) : f (!a) = 0 → a = false → f true = 0 := by grind
 example (f : Bool → Nat) : (!a) = c → c = true → f a = 0 → f false = 0 := by grind (splits := 0)
 example (f : Bool → Nat) : (!a) = c → c = false → f a = 0 → f true = 0 := by grind (splits := 0)
 example : (!a) = c → c = a → False := by grind (splits := 0)
+
+example (as bs : List Nat) (f : Prop → Nat) : f (as = bs) = 0 → as = [] → bs = b :: bs' → f False = 0 := by grind (splits := 0)
+example (as bs : List Nat) (f : Bool → Nat) : f (as == bs) = 0 → as = [] → bs = b :: bs' → f false = 0 := by grind (splits := 0)
+example (as bs : List Nat) : (as == bs) = c → c = true → as = bs := by grind (splits := 0)
+example (as bs : List Nat) : (as == bs) = c → c = true → as = cs → bs = cs := by grind (splits := 0)
+example (a b : Nat) : (a == b, c) = d → d = (true, true) → a = b := by grind (splits := 0)
+
+example (as bs : List Nat) (f : Bool → Nat) : f (as != bs) = 0 → as = [] → bs = b :: bs' → f true = 0 := by grind (splits := 0)
+example (as bs : List Nat) : (as != bs) = c → c = true → as ≠ bs := by grind (splits := 0)
+example (a b : Nat) : (a != b, c) = d → d = (false, true) → a = b := by grind (splits := 0)
+example (a b : Bool) : (a ^^ b, c) = d → d = (false, true) → a = b := by grind (splits := 0)
+example (a b : Bool) : (a == b, c) = d → d = (true, true) → a = true → true = b := by grind (splits := 0)
+
+example (h : α = β) (a : α) (b : β) : h ▸ a = b → HEq a b := by grind