From 8165ecc1db80dd7c8d6909c734eec69bfe1bc7e9 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Tue, 3 Jun 2025 20:34:47 -0400
Subject: [PATCH] fix: bug in the equality resolution procedure in `grind`
 (#8621)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This PR fixes a bug in the equality-resolution procedure used by
`grind`.
The procedure now performs a topological sort so that every simplified
theorem declaration is emitted **before** any place where it is
referenced.
Previously, applying equality resolution to
```lean
h : ∀ x, p x a → ∀ y, p y b → x ≠ y
```
in the example
```lean
example
  (p : Nat → Nat → Prop)
  (a b c : Nat)
  (h  : ∀ x, p x a → ∀ y, p y b → x ≠ y)
  (h₁ : p c a)
  (h₂ : p c b) :
  False := by
  grind
```
caused `grind` to produce the incorrect term
```lean
p ?y a → ∀ y, p y b → False
```
The patch eliminates this error, and the following correct simplified
theorem is generated
```lean
∀ y, p y a → p y b → False
```
---
 src/Lean/Meta/Tactic/Grind/EqResolution.lean | 63 ++++++++++++++++++++
 tests/lean/grind/lrat_mvar.lean              |  4 +-
 tests/lean/run/grind_eqres_bug.lean          | 17 ++++++
 3 files changed, 82 insertions(+), 2 deletions(-)
 create mode 100644 tests/lean/run/grind_eqres_bug.lean

diff --git a/src/Lean/Meta/Tactic/Grind/EqResolution.lean b/src/Lean/Meta/Tactic/Grind/EqResolution.lean
index b7a4c07064..fe954f3025 100644
--- a/src/Lean/Meta/Tactic/Grind/EqResolution.lean
+++ b/src/Lean/Meta/Tactic/Grind/EqResolution.lean
@@ -6,6 +6,7 @@ Authors: Leonardo de Moura
 prelude
 import Lean.Meta.AppBuilder
 import Lean.Meta.MatchUtil
+import Lean.Util.ForEachExpr
 
 namespace Lean.Meta.Grind
 /-! A basic "equality resolution" procedure. -/
@@ -21,6 +22,67 @@ private def forallMetaTelescopeReducingAndUnfoldingNot (prop : Expr) : MetaM (Ar
     return (ms.push m, mkConst ``False)
   return (ms, type)
 
+structure TopSort.State where
+  tempMark  : Std.HashSet Expr := {}
+  permMark  : Std.HashSet Expr := {}
+  result : Array Expr := #[]
+
+abbrev TopSortM := OptionT $ StateT TopSort.State MetaM
+
+/--
+Sorts metavariables `ms` using topological sort.
+There is an "edge" from `m₁` to `m₂` if type of `m₁` contains `m₂`.
+We use this function to ensure that after applying equality resolution to
+```
+∀ x : Nat, p x a → ∀ y : Nat, p y b → x = y → False
+```
+we produce
+```
+∀ y, p y a → p y b → False
+```
+instead of
+```
+p ?y a → ∀ y, p y b → False
+```
+Recall that in equality resolution we create a meta-variable for each hypothesis.
+Thus, we initially have
+```
+?x : Nat, ?h₁ : p ?x a, ?y : Nat, ?h₂ : p ?y b, ?h₃ : ?x = ?y
+```
+Then, we resolve `?h₃ : ?x = ?y` as `?y := ?x` and `?h₃ := Eq.refl ?y`.
+But `?h₁` occurs before `?y`. We use topological sort to address this situation.
+If a cycle is detected, it returns `none`.
+-/
+private partial def topsortMVars? (ms : Array Expr) : MetaM (Option (Array Expr)) := do
+  let (some _, s) ← go.run.run {} | return none
+  return some s.result
+where
+  go : TopSortM Unit := do
+    for m in ms do
+      visit m
+
+  visit (m : Expr) : TopSortM Unit := do
+    if (← get).permMark.contains m then
+      return ()
+    if (← get).tempMark.contains m then
+      failure
+    modify fun s => { s with tempMark := s.tempMark.insert m }
+    visitTypeOf m
+    modify fun s => { s with
+      result := s.result.push m
+      permMark := s.permMark.insert m
+    }
+
+  visitTypeOf (m : Expr) : TopSortM Unit := do
+    let type ← instantiateMVars (← inferType m)
+    type.forEach' fun e => do
+      if e.hasExprMVar then
+        if e.isMVar && ms.contains e then
+          visit e
+        return true
+      else
+        return false
+
 private def eqResCore (prop proof : Expr) : MetaM (Option (Expr × Expr)) := withNewMCtxDepth do
   /-
   We use `forallMetaTelescopeReducingAndUnfoldingNot` because we want to treat
@@ -51,6 +113,7 @@ private def eqResCore (prop proof : Expr) : MetaM (Option (Expr × Expr)) := wit
   let prop' ← instantiateMVars type
   let proof' ← instantiateMVars (mkAppN proof ms)
   let ms ← ms.filterM fun m => return !(← m.mvarId!.isAssigned)
+  let some ms ← topsortMVars? ms | return none
   let prop' ← mkForallFVars ms prop' (binderInfoForMVars := .default)
   let proof' ← mkLambdaFVars ms proof'
   return some (prop', proof')
diff --git a/tests/lean/grind/lrat_mvar.lean b/tests/lean/grind/lrat_mvar.lean
index d4ec43ffce..6568ae8937 100644
--- a/tests/lean/grind/lrat_mvar.lean
+++ b/tests/lean/grind/lrat_mvar.lean
@@ -21,6 +21,6 @@ example (ls : Array Unit) : Option Clause :=
 
 example (ls : Array Unit) : Option Clause :=
   ls.foldl folder (some ∅) |>.map fun map =>
-    -- FIXME: Commenting this out gives an unknown metavariable error in `grind`!
-    -- have mapnodup := map.distinct_keys
+    -- The following example is still failing, but
+    -- we don't get the unknown metavar bug anymore
     ⟨map.toList, by grind⟩
diff --git a/tests/lean/run/grind_eqres_bug.lean b/tests/lean/run/grind_eqres_bug.lean
new file mode 100644
index 0000000000..bf04f2972f
--- /dev/null
+++ b/tests/lean/run/grind_eqres_bug.lean
@@ -0,0 +1,17 @@
+set_option grind.warning false
+
+/--
+trace: [grind.eqResolution] ∀ (x : Nat), p x a → ∀ (y : Nat), p y b → ¬x = y, ∀ (y : Nat), p y a → p y b → False
+[grind.ematch.instance] local_0: p c a → ¬p c b
+-/
+#guard_msgs (trace) in
+example
+    (p : Nat → Nat → Prop)
+    (a b c : Nat)
+    (h : ∀ x, p x a → ∀ y, p y b → x ≠ y)
+    (h₁ : p c a)
+    (h₂ : p c b)
+    : False := by
+  set_option trace.grind.eqResolution true in
+  set_option trace.grind.ematch.instance true in
+  grind