From 2fedd7144aff67f65ee95736d6fa8a1f9319ebc4 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Thu, 30 Jan 2025 08:00:18 -0800
Subject: [PATCH] feat: normalize `!=` and `==` in `grind` (#6870)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

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            | 12 ++++++++++--
 tests/lean/run/grind_bool_prop.lean | 14 ++++++++++++++
 2 files changed, 24 insertions(+), 2 deletions(-)

diff --git a/src/Init/Grind/Norm.lean b/src/Init/Grind/Norm.lean
index 92708a7593..c31d2534bf 100644
--- a/src/Init/Grind/Norm.lean
+++ b/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
diff --git a/tests/lean/run/grind_bool_prop.lean b/tests/lean/run/grind_bool_prop.lean
index 275064a4fc..95ffef4820 100644
--- a/tests/lean/run/grind_bool_prop.lean
+++ b/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