From 2979830120f16453f7f7ff1259f22da4818a9f27 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Tue, 1 Apr 2025 15:12:20 -0700
Subject: [PATCH] fix: `Bool` disequality propagation in `grind` (#7781)

This PR adds a new propagation rule for `Bool` disequalities to `grind`.
It now propagates `x = true` (`x = false`) from the disequality `x =
false` (`x = true`). It ensures we don't have to perform case analysis
on `x` to learn this fact. See tests.
---
 src/Init/Grind/Lemmas.lean                |  3 +++
 src/Lean/Meta/Tactic/Grind/Propagate.lean | 15 +++++++++++-
 tests/lean/grind/list_problems.lean       | 28 -----------------------
 tests/lean/run/grind_bool_diseq.lean      | 25 ++++++++++++++++++++
 tests/lean/run/grind_list_issue.lean      |  9 ++++++++
 5 files changed, 51 insertions(+), 29 deletions(-)
 delete mode 100644 tests/lean/grind/list_problems.lean
 create mode 100644 tests/lean/run/grind_bool_diseq.lean
 create mode 100644 tests/lean/run/grind_list_issue.lean

diff --git a/src/Init/Grind/Lemmas.lean b/src/Init/Grind/Lemmas.lean
index fc1eb2149a..d6ad8457e1 100644
--- a/src/Init/Grind/Lemmas.lean
+++ b/src/Init/Grind/Lemmas.lean
@@ -113,6 +113,9 @@ theorem Bool.not_eq_of_eq_false {a : Bool} (h : a = false) : (!a) = true := by s
 theorem Bool.eq_false_of_not_eq_true {a : Bool} (h : (!a) = true) : a = false := by simp_all
 theorem Bool.eq_true_of_not_eq_false {a : Bool} (h : (!a) = false) : a = true := by simp_all
 
+theorem Bool.eq_false_of_not_eq_true' {a : Bool} (h : ¬ a = true) : a = false := by simp_all
+theorem Bool.eq_true_of_not_eq_false' {a : Bool} (h : ¬ a = false) : a = true := by simp_all
+
 theorem Bool.false_of_not_eq_self {a : Bool} (h : (!a) = a) : False := by
   by_cases a <;> simp_all
 
diff --git a/src/Lean/Meta/Tactic/Grind/Propagate.lean b/src/Lean/Meta/Tactic/Grind/Propagate.lean
index 647aa48b93..ccfa6925f4 100644
--- a/src/Lean/Meta/Tactic/Grind/Propagate.lean
+++ b/src/Lean/Meta/Tactic/Grind/Propagate.lean
@@ -119,15 +119,25 @@ builtin_grind_propagator propagateNotDown ↓Not := fun e => do
   else if (← isEqv e a) then
     closeGoal <| mkApp2 (mkConst ``Grind.false_of_not_eq_self) a (← mkEqProof e a)
 
+def propagateBoolDiseq (a : Expr) : GoalM Unit := do
+  if let some h ← mkDiseqProof? a (← getBoolFalseExpr) then
+    pushEqBoolTrue a <| mkApp2 (mkConst ``Grind.Bool.eq_true_of_not_eq_false') a h
+  if let some h ← mkDiseqProof? a (← getBoolTrueExpr) then
+    pushEqBoolFalse a <| mkApp2 (mkConst ``Grind.Bool.eq_false_of_not_eq_true') a h
+
 /-- Propagates `Eq` upwards -/
 builtin_grind_propagator propagateEqUp ↑Eq := fun e => do
-  let_expr Eq _ a b := e | return ()
+  let_expr Eq α a b := e | return ()
   if (← isEqTrue a) then
     pushEq e b <| mkApp3 (mkConst ``Grind.eq_eq_of_eq_true_left) a b (← mkEqTrueProof a)
   else if (← isEqTrue b) then
     pushEq e a <| mkApp3 (mkConst ``Grind.eq_eq_of_eq_true_right) a b (← mkEqTrueProof b)
   else if (← isEqv a b) then
     pushEqTrue e <| mkEqTrueCore e (← mkEqProof a b)
+  if α.isConstOf ``Bool then
+    if (← isEqFalse e) then
+      propagateBoolDiseq a
+      propagateBoolDiseq b
   let aRoot ← getRootENode a
   let bRoot ← getRootENode b
   if aRoot.ctor && bRoot.ctor && aRoot.self.getAppFn != bRoot.self.getAppFn then
@@ -146,6 +156,9 @@ builtin_grind_propagator propagateEqDown ↓Eq := fun e => do
     pushEq a b <| mkOfEqTrueCore e (← mkEqTrueProof e)
   else if (← isEqFalse e) then
     let_expr Eq α lhs rhs := e | return ()
+    if α.isConstOf ``Bool then
+      propagateBoolDiseq lhs
+      propagateBoolDiseq rhs
     propagateCutsatDiseq lhs rhs
     let thms ← getExtTheorems α
     if !thms.isEmpty then
diff --git a/tests/lean/grind/list_problems.lean b/tests/lean/grind/list_problems.lean
deleted file mode 100644
index e1dfae439e..0000000000
--- a/tests/lean/grind/list_problems.lean
+++ /dev/null
@@ -1,28 +0,0 @@
-open List Nat
-
-attribute [grind] List.getElem_cons_zero
-
-attribute [grind] List.filter_nil List.filter_cons
-attribute [grind] List.any_nil List.any_cons
-
-@[simp] theorem any_filter {l : List α} {p q : α → Bool} :
-    (filter p l).any q = l.any fun a => p a && q a := by
-  induction l <;> grind
-  -- Fails at:
-  -- [grind] Goal diagnostics ▼
-  -- [facts] Asserted facts ▼
-  --   [prop] (filter p tail).any q = tail.any fun a => p a && q a
-  --   [prop] ¬(filter p (head :: tail)).any q = (head :: tail).any fun a => p a && q a
-  --   [prop] filter p (head :: tail) = if p head = true then head :: filter p tail else filter p tail
-  --   [prop] ((head :: tail).any fun a => p a && q a) = (p head && q head || tail.any fun a => p a && q a)
-  --   [prop] ¬p head = true
-  -- [eqc] False propositions ▼
-  --   [prop] (filter p (head :: tail)).any q = (head :: tail).any fun a => p a && q a
-  --   [prop] p head = true
-  -- [eqc] Equivalence classes ▼
-  --   [] {(head :: tail).any fun a => p a && q a, p head && q head || tail.any fun a => p a && q a}
-  --   [] {filter p (head :: tail), filter p tail, if p head = true then head :: filter p tail else filter p tail}
-  --   [] {(filter p tail).any q, (filter p (head :: tail)).any q, tail.any fun a => p a && q a}
-  -- Despite knowing that `p head = false`, grind doesn't see that
-  -- `p head && q head || tail.any fun a => p a && q a = tail.any fun a => p a && q a`,
-  -- which should finish the problem.
diff --git a/tests/lean/run/grind_bool_diseq.lean b/tests/lean/run/grind_bool_diseq.lean
new file mode 100644
index 0000000000..e166eecc8b
--- /dev/null
+++ b/tests/lean/run/grind_bool_diseq.lean
@@ -0,0 +1,25 @@
+set_option grind.warning false
+
+example (f : Bool → Nat) : (x = y ↔ q) → ¬ q → y = false → f x = 0 → f true = 0 := by
+  grind (splits := 0)
+
+example (f : Bool → Nat) : (x = false ↔ q) → ¬ q → f x = 0 → f true = 0 := by
+  grind (splits := 0)
+
+example (f : Bool → Nat) : (y = x ↔ q) → ¬ q → y = false → f x = 0 → f true = 0 := by
+  grind (splits := 0)
+
+example (f : Bool → Nat) : (x = true ↔ q) → ¬ q → f x = 0 → f false = 0 := by
+  grind (splits := 0)
+
+example (f : Bool → Nat) : (true = x ↔ q) → ¬ q → f x = 0 → f false = 0 := by
+  grind (splits := 0)
+
+example (f : Bool → Nat) : (false = x ↔ q) → ¬ q → f x = 0 → f true = 0 := by
+  grind (splits := 0)
+
+example (f : Bool → Nat) : (x = false ↔ q) → ¬ q → f x = 0 → f true = 0 := by
+  grind (splits := 0)
+
+example (f : Bool → Nat) : (y = x ↔ q) → ¬ q → y = true → f x = 0 → f false = 0 := by
+  grind (splits := 0)
diff --git a/tests/lean/run/grind_list_issue.lean b/tests/lean/run/grind_list_issue.lean
new file mode 100644
index 0000000000..ae0047dae3
--- /dev/null
+++ b/tests/lean/run/grind_list_issue.lean
@@ -0,0 +1,9 @@
+reset_grind_attrs%
+open List Nat
+
+attribute [grind] List.filter_nil List.filter_cons
+attribute [grind] List.any_nil List.any_cons
+
+@[simp] theorem any_filter {l : List α} {p q : α → Bool} :
+    (filter p l).any q = l.any fun a => p a && q a := by
+  induction l <;> grind