From a4a2bfa426bad159bacd99d9928107a288dda008 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Wed, 10 Sep 2025 19:54:36 -0700
Subject: [PATCH] fix: minor issues in `grind` (#10339)

This PR fixes a few minor issues and applies a few cleanups.
---
 src/Lean/Meta/Tactic/Grind/AC/Eq.lean         |  2 --
 src/Lean/Meta/Tactic/Grind/Core.lean          |  4 ++--
 src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean |  6 ------
 src/Lean/Meta/Tactic/Grind/Types.lean         | 12 +++++++++++-
 4 files changed, 13 insertions(+), 11 deletions(-)

diff --git a/src/Lean/Meta/Tactic/Grind/AC/Eq.lean b/src/Lean/Meta/Tactic/Grind/AC/Eq.lean
index 4eb6058c1f..d938bdc50c 100644
--- a/src/Lean/Meta/Tactic/Grind/AC/Eq.lean
+++ b/src/Lean/Meta/Tactic/Grind/AC/Eq.lean
@@ -497,8 +497,6 @@ def check : GoalM Bool := do profileitM Exception "grind ac" (← getOptions) do
       let r ← ACM.run opId checkStruct
       progress := progress || r
       if (← isInconsistent) then return true
-    if progress then
-      processNewFacts
     return progress
   finally
     checkInvariants
diff --git a/src/Lean/Meta/Tactic/Grind/Core.lean b/src/Lean/Meta/Tactic/Grind/Core.lean
index 8f9b49a895..0aa048356c 100644
--- a/src/Lean/Meta/Tactic/Grind/Core.lean
+++ b/src/Lean/Meta/Tactic/Grind/Core.lean
@@ -229,7 +229,7 @@ where
     }
     propagateBeta lams₁ fns₁
     propagateBeta lams₂ fns₂
-    let todo ← Solvers.mergeTerms rhsRoot lhsRoot
+    let toPropagateSolvers ← Solvers.mergeTerms rhsRoot lhsRoot
     resetParentsOf lhsRoot.self
     copyParentsTo parents rhsNode.root
     unless (← isInconsistent) do
@@ -240,7 +240,7 @@ where
       for e in toPropagateDown do
         propagateDown e
       propagateUnitConstFuns lams₁ lams₂
-      todo.propagate
+      toPropagateSolvers.propagate
   updateRoots (lhs : Expr) (rootNew : Expr) : GoalM Unit := do
     let isFalseRoot ← isFalseExpr rootNew
     traverseEqc lhs fun n => do
diff --git a/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean b/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean
index 74783fef5d..6773e8eb31 100644
--- a/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean
+++ b/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean
@@ -585,17 +585,11 @@ private structure Context where
 
 private abbrev M := ReaderT Context StateRefT State MetaM
 
-/-- Helper declaration for finding bootstrapping issues. See `isCandidateSymbol`. -/
-private abbrev badForPatterns := [``Eq, ``HEq, ``Iff, ``And, ``Or, ``Not]
-
 private def isCandidateSymbol (declName : Name) (root : Bool) : M Bool := do
   let ctx ← read
   let prio := ctx.symPrios.getPrio declName
   -- Priority 0 are never considered, they are treated as forbidden
   if prio == 0 then return false
-  -- Remark: uncomment the following code to fix bootstrapping issues
-  -- if declName ∈ badForPatterns then
-  --  throwError "INSERT `import Init.Grind.Tactics`, otherwise a pattern containing `{.ofConstName declName}` will be used, prio: {prio}"
   -- If it is the root symbol, then we check whether `prio ≥ minPrio`
   if root then
     return prio ≥ ctx.minPrio
diff --git a/src/Lean/Meta/Tactic/Grind/Types.lean b/src/Lean/Meta/Tactic/Grind/Types.lean
index b24dc34888..3a0ca0f4de 100644
--- a/src/Lean/Meta/Tactic/Grind/Types.lean
+++ b/src/Lean/Meta/Tactic/Grind/Types.lean
@@ -1085,7 +1085,15 @@ For each equality `b = c` in `parents`, executes `k b c` IF
   for parent in parents do
     let_expr Eq _ b c := parent | continue
     if (← isEqFalse parent) then
-      k b c
+      if (← isEqv b c) then
+        /-
+        Remark: if `b` and `c` are already in the same equivalence class,
+        there is an inconsistency in the TODO queue already, and we can interrupt
+        propagation
+        -/
+        return ()
+      else
+        k b c
 
 /-- Returns `true` is `e` is the root of its congruence class. -/
 def isCongrRoot (e : Expr) : GoalM Bool := do
@@ -1485,6 +1493,8 @@ def Solvers.checkInvariants : GoalM Unit := do
 def Solvers.check : GoalM Bool := do
   let mut result := false
   for ext in (← solverExtensionsRef.get) do
+    if (← isInconsistent) then
+      return true
     if (← ext.check) then
       result := true
   if result then