From 7034310a3b44bb2cb129d72df2fb89986a3a1ce4 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Sun, 27 Jul 2025 16:49:10 +0200
Subject: [PATCH] fix: disequality proof construction in `grind` (#9578)

This PR fixes an issue in `grind`'s disequality proof construction. The
issue occurs when an equality is merged with the `False` equivalence
class, but it is not the root of its congruence class, and its
congruence root has not yet been merged into the `False` equivalence
class yet.

closes #9562
---
 src/Lean/Meta/Tactic/Grind/Core.lean | 21 +++++++++++++++++++--
 tests/lean/run/grind_9562.lean       | 12 ++++++++++++
 2 files changed, 31 insertions(+), 2 deletions(-)
 create mode 100644 tests/lean/run/grind_9562.lean

diff --git a/src/Lean/Meta/Tactic/Grind/Core.lean b/src/Lean/Meta/Tactic/Grind/Core.lean
index f27814adf4..a4ed1258de 100644
--- a/src/Lean/Meta/Tactic/Grind/Core.lean
+++ b/src/Lean/Meta/Tactic/Grind/Core.lean
@@ -335,8 +335,25 @@ where
       propagateCommRing ringTodo
       propagateLinarith linarithTodo
   updateRoots (lhs : Expr) (rootNew : Expr) : GoalM Unit := do
-    traverseEqc lhs fun n =>
-      setENode n.self { n with root := rootNew }
+    let isFalseRoot ← isFalseExpr rootNew
+    traverseEqc lhs fun n => do
+      let n := { n with root := rootNew }
+      setENode n.self n
+      /-
+      If `n` is an equality being inserted into the `False` equivalence class,
+      we must ensure it is root `m` of its congruence class if the root is not already
+      in the `False` equivalence class.
+      This can happen when the equality `n = m` is still has to be processed. That is,
+      it is in the `newFacts` todo array.
+      A similar swap is performed at `addCongrTable`.
+      -/
+      if isFalseRoot && n.self.isAppOfArity ``Eq 3 && !n.isCongrRoot then
+        if let some { e } := (← get).congrTable.find? { e := n.self } then
+        -- If the current congruence root is already `False`, we don't need to swap
+        unless (← isFalseExpr e) do
+          -- We must swap the congruence root to ensure `isDiseq` and `getDiseqFor?` work properly
+          modify fun s => { s with congrTable := s.congrTable.insert { e := n.self } }
+          setENode n.self { n with congr := n.self }
 
 /-- Ensures collection of equations to be processed is empty. -/
 private def resetNewFacts : GoalM Unit :=
diff --git a/tests/lean/run/grind_9562.lean b/tests/lean/run/grind_9562.lean
new file mode 100644
index 0000000000..e608833ec2
--- /dev/null
+++ b/tests/lean/run/grind_9562.lean
@@ -0,0 +1,12 @@
+axiom A : Type
+axiom angle (x y z : A) : Int
+axiom pi : Int
+axiom Collinear (x y z : A) : Prop
+axiom collinear_iff_eq_or_eq_or_angle_eq_zero_or_angle_eq_pi {p₁ p₂ p₃ : A} :
+  Collinear p₁ p₂ p₃ ↔ p₁ = p₂ ∨ p₃ = p₂ ∨ angle p₁ p₂ p₃ = 0 ∨ angle p₁ p₂ p₃ = pi
+
+example {a b c a' b' c' : A} (h : ¬Collinear a b c)
+    (ha₁ : angle a b c = angle a' b' c')
+    (h' : angle a' b' c' = 0 ∨ angle a' b' c' = pi) :
+    False := by
+  grind only [collinear_iff_eq_or_eq_or_angle_eq_zero_or_angle_eq_pi]