feat: equality resolution for grind (#6663)

This PR implements a basic equality resolution procedure for the `grind`
tactic.

src/Lean/Meta/Tactic/Grind.lean

@@ -38,6 +38,7 @@ builtin_initialize registerTraceClass `grind.ematch.pattern
 builtin_initialize registerTraceClass `grind.ematch.pattern.search
 builtin_initialize registerTraceClass `grind.ematch.instance
 builtin_initialize registerTraceClass `grind.ematch.instance.assignment
+builtin_initialize registerTraceClass `grind.eqResolution
 builtin_initialize registerTraceClass `grind.issues
 builtin_initialize registerTraceClass `grind.simp
 builtin_initialize registerTraceClass `grind.split

src/Lean/Meta/Tactic/Grind/EqResolution.lean

@@ -0,0 +1,49 @@
+/-
+Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Lean.Meta.AppBuilder
+
+namespace Lean.Meta.Grind
+/-!
+A basic "equality resolution" procedure to make Kim happy.
+-/
+
+private def eqResCore (prop proof : Expr) : MetaM (Option (Expr × Expr)) := withNewMCtxDepth do
+  let (ms, _, type) ← forallMetaTelescopeReducing prop
+  if ms.isEmpty then return none
+  let mut progress := false
+  for m in ms do
+    let type ← inferType m
+    let_expr Eq _ lhs rhs ← type
+      | pure ()
+    if (← isDefEq lhs rhs) then
+      unless (← m.mvarId!.checkedAssign (← mkEqRefl lhs)) do
+        return none
+      progress := true
+  unless progress do
+    return none
+  if (← ms.anyM fun m => m.mvarId!.isDelayedAssigned) then
+    return none
+  let prop' ← instantiateMVars type
+  let proof' ← instantiateMVars (mkAppN proof ms)
+  let ms ← ms.filterM fun m => return !(← m.mvarId!.isAssigned)
+  let prop' ← mkForallFVars ms prop' (binderInfoForMVars := .default)
+  let proof' ← mkLambdaFVars ms proof'
+  return some (prop', proof')
+
+/--
+A basic "equality resolution" procedure: Given a proposition `prop` with a proof `proof`, it attempts to resolve equality hypotheses using `isDefEq`. For example, it reduces `∀ x y, f x = f (g y y) → g x y = y` to `∀ y, g (g y y) y = y`, and `∀ (x : Nat), f x ≠ f a` to `False`.
+If successful, the result is a pair `(prop', proof)`, where `prop'` is the simplified proposition,
+and `proof : prop → prop'`
+-/
+def eqResolution (prop : Expr) : MetaM (Option (Expr × Expr)) :=
+  withLocalDeclD `h prop fun h => do
+    let some (prop', proof') ← eqResCore prop h
+      | return none
+    let proof' ← mkLambdaFVars #[h] proof'
+    return some (prop', proof')
+
+end Lean.Meta.Grind

src/Lean/Meta/Tactic/Grind/ForallProp.lean

@@ -8,6 +8,7 @@ import Init.Grind.Lemmas
 import Lean.Meta.Tactic.Grind.Types
 import Lean.Meta.Tactic.Grind.Internalize
 import Lean.Meta.Tactic.Grind.Simp
+import Lean.Meta.Tactic.Grind.EqResolution
 
 namespace Lean.Meta.Grind
 /--
@@ -96,7 +97,13 @@ def propagateForallPropDown (e : Expr) : GoalM Unit := do
       pushEqTrue a <| mkApp3 (mkConst ``Grind.eq_true_of_imp_eq_false) a b h
       pushEqFalse b <| mkApp3 (mkConst ``Grind.eq_false_of_imp_eq_false) a b h
   else if (← isEqTrue e) then
-    if b.hasLooseBVars then
-      addLocalEMatchTheorems e
+    if let some (e', h') ← eqResolution e then
+      trace[grind.eqResolution] "{e}, {e'}"
+      let h := mkOfEqTrueCore e (← mkEqTrueProof e)
+      let h' := mkApp h' h
+      addNewFact h' e' (← getGeneration e)
+    else
+      if b.hasLooseBVars then
+        addLocalEMatchTheorems e
 
 end Lean.Meta.Grind

tests/lean/run/grind_t1.lean

@@ -290,3 +290,6 @@ example {m n : Nat} : m < n ↔ m ≤ n ∧ ¬ n ≤ m := by
 
 example {α} (f : α → Type) (a : α) (h : ∀ x, Nonempty (f x)) : Nonempty (f a) := by
   grind
+
+example {α β} (f : α → β) (a : α) : ∃ a', f a' = f a := by
+  grind