feat: grind simple strategy (#6503)

This PR adds a simple strategy to the (WIP) `grind` tactic. It just
keeps internalizing new theorem instances found by E-matching. The
simple strategy can solve examples such as:

```lean
grind_pattern Array.size_set => Array.set a i v h
grind_pattern Array.get_set_eq  => a.set i v h
grind_pattern Array.get_set_ne => (a.set i v hi)[j]

example (as bs : Array α) (v : α)
        (i : Nat)
        (h₁ : i < as.size)
        (h₂ : bs = as.set i v)
        : as.size = bs.size := by
  grind

example (as bs cs : Array α) (v : α)
        (i : Nat)
        (h₁ : i < as.size)
        (h₂ : bs = as.set i v)
        (h₃ : cs = bs)
        (h₄ : i ≠ j)
        (h₅ : j < cs.size)
        (h₆ : j < as.size)
        : cs[j] = as[j] := by
  grind


opaque R : Nat → Nat → Prop
theorem Rtrans (a b c : Nat) : R a b → R b c → R a c := sorry

grind_pattern Rtrans => R a b, R b c

example : R a b → R b c → R c d → R d e → R a d := by
  grind
```

src/Lean/Meta/Tactic/Grind.lean

@@ -7,7 +7,6 @@ prelude
 import Lean.Meta.Tactic.Grind.Attr
 import Lean.Meta.Tactic.Grind.RevertAll
 import Lean.Meta.Tactic.Grind.Types
-import Lean.Meta.Tactic.Grind.Preprocessor
 import Lean.Meta.Tactic.Grind.Util
 import Lean.Meta.Tactic.Grind.Cases
 import Lean.Meta.Tactic.Grind.Injection
@@ -22,6 +21,9 @@ import Lean.Meta.Tactic.Grind.Simp
 import Lean.Meta.Tactic.Grind.Ctor
 import Lean.Meta.Tactic.Grind.Parser
 import Lean.Meta.Tactic.Grind.EMatchTheorem
+import Lean.Meta.Tactic.Grind.EMatch
+import Lean.Meta.Tactic.Grind.Main
+
 
 namespace Lean
 
@@ -41,8 +43,8 @@ builtin_initialize registerTraceClass `grind.simp
 builtin_initialize registerTraceClass `grind.debug
 builtin_initialize registerTraceClass `grind.debug.proofs
 builtin_initialize registerTraceClass `grind.debug.congr
-builtin_initialize registerTraceClass `grind.debug.pre
 builtin_initialize registerTraceClass `grind.debug.proof
 builtin_initialize registerTraceClass `grind.debug.proj
+builtin_initialize registerTraceClass `grind.debug.parent
 
 end Lean

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

@@ -41,6 +41,7 @@ This is an auxiliary function performed while merging equivalence classes.
 private def removeParents (root : Expr) : GoalM ParentSet := do
   let parents ← getParentsAndReset root
   for parent in parents do
+    trace[grind.debug.parent] "remove: {parent}"
     modify fun s => { s with congrTable := s.congrTable.erase { e := parent } }
   return parents
 
@@ -50,6 +51,7 @@ This is an auxiliary function performed while merging equivalence classes.
 -/
 private def reinsertParents (parents : ParentSet) : GoalM Unit := do
   for parent in parents do
+    trace[grind.debug.parent] "reinsert: {parent}"
     addCongrTable parent
 
 /-- Closes the goal when `True` and `False` are in the same equivalence class. -/
@@ -223,10 +225,8 @@ where
       internalize rhs generation
       addEqCore lhs rhs proof isHEq
 
-/--
-Adds a new hypothesis.
--/
-def addHyp (fvarId : FVarId) (generation := 0) : GoalM Unit := do
+/-- Adds a new hypothesis. -/
+def addHypothesis (fvarId : FVarId) (generation := 0) : GoalM Unit := do
   add (← fvarId.getType) (mkFVar fvarId) generation
 
 end Lean.Meta.Grind

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

@@ -5,7 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Lean.Meta.Tactic.Grind.Types
-import Lean.Meta.Tactic.Grind.Internalize
+import Lean.Meta.Tactic.Grind.Intro
 
 namespace Lean.Meta.Grind
 namespace EMatch
@@ -278,4 +278,15 @@ def ematch : GoalM Unit := do
       gmt          := s.gmt + 1
     }
 
+/-- Performs one round of E-matching, and assert new instances. -/
+def ematchAndAssert? (goal : Goal) : GrindM (Option (List Goal)) := do
+  let numInstances := goal.numInstances
+  let goal ← GoalM.run' goal ematch
+  if goal.numInstances == numInstances then
+    return none
+  assertAll goal
+
+def ematchStar (goal : Goal) : GrindM (List Goal) := do
+  iterate goal ematchAndAssert?
+
 end Lean.Meta.Grind

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

@@ -20,7 +20,7 @@ def propagateForallProp (parent : Expr) : GoalM Unit := do
   unless (← isEqTrue p) do return ()
   let h₁ ← mkEqTrueProof p
   let qh₁ := q.instantiate1 (mkApp2 (mkConst ``of_eq_true) p h₁)
-  let r ← pre qh₁
+  let r ← simp qh₁
   let q := mkLambda n bi p q
   let q' := r.expr
   internalize q' (← getGeneration parent)

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

@@ -0,0 +1,139 @@
+/-
+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 Init.Grind.Lemmas
+import Lean.Meta.Tactic.Assert
+import Lean.Meta.Tactic.Grind.Simp
+import Lean.Meta.Tactic.Grind.Types
+import Lean.Meta.Tactic.Grind.Cases
+import Lean.Meta.Tactic.Grind.Injection
+import Lean.Meta.Tactic.Grind.Core
+
+namespace Lean.Meta.Grind
+
+private inductive IntroResult where
+  | done
+  | newHyp (fvarId : FVarId) (goal : Goal)
+  | newDepHyp (goal : Goal)
+  | newLocal (fvarId : FVarId) (goal : Goal)
+  deriving Inhabited
+
+private def introNext (goal : Goal) : GrindM IntroResult := do
+  let target ← goal.mvarId.getType
+  if target.isArrow then
+    goal.mvarId.withContext do
+      let p := target.bindingDomain!
+      if !(← isProp p) then
+        let (fvarId, mvarId) ← goal.mvarId.intro1P
+        return .newLocal fvarId { goal with mvarId }
+      else
+        let tag ← goal.mvarId.getTag
+        let q := target.bindingBody!
+        -- TODO: keep applying simp/eraseIrrelevantMData/canon/shareCommon until no progress
+        let r ← simp p
+        let fvarId ← mkFreshFVarId
+        let lctx := (← getLCtx).mkLocalDecl fvarId target.bindingName! r.expr target.bindingInfo!
+        let mvarNew ← mkFreshExprMVarAt lctx (← getLocalInstances) q .syntheticOpaque tag
+        let mvarIdNew := mvarNew.mvarId!
+        mvarIdNew.withContext do
+          let h ← mkLambdaFVars #[mkFVar fvarId] mvarNew
+          match r.proof? with
+          | some he =>
+            let hNew := mkAppN (mkConst ``Lean.Grind.intro_with_eq) #[p, r.expr, q, he, h]
+            goal.mvarId.assign hNew
+            return .newHyp fvarId { goal with mvarId := mvarIdNew }
+          | none =>
+            -- `p` and `p'` are definitionally equal
+            goal.mvarId.assign h
+            return .newHyp fvarId { goal with mvarId := mvarIdNew }
+  else if target.isLet || target.isForall then
+    let (fvarId, mvarId) ← goal.mvarId.intro1P
+    mvarId.withContext do
+      let localDecl ← fvarId.getDecl
+      if (← isProp localDecl.type) then
+        -- Add a non-dependent copy
+        let mvarId ← mvarId.assert (← mkFreshUserName localDecl.userName) localDecl.type (mkFVar fvarId)
+        return .newDepHyp { goal with mvarId }
+      else
+        return .newLocal fvarId { goal with mvarId }
+  else
+    return .done
+
+private def isCasesCandidate (fvarId : FVarId) : MetaM Bool := do
+  let .const declName _ := (← fvarId.getType).getAppFn | return false
+  isGrindCasesTarget declName
+
+private def applyCases? (goal : Goal) (fvarId : FVarId) : MetaM (Option (List Goal)) := goal.mvarId.withContext do
+  if (← isCasesCandidate fvarId) then
+    let mvarIds ← cases goal.mvarId fvarId
+    return mvarIds.map fun mvarId => { goal with mvarId }
+  else
+    return none
+
+private def applyInjection? (goal : Goal) (fvarId : FVarId) : MetaM (Option Goal) := do
+  if let some mvarId ← injection? goal.mvarId fvarId then
+    return some { goal with mvarId }
+  else
+    return none
+
+/-- Introduce new hypotheses (and apply `by_contra`) until goal is of the form `... ⊢ False` -/
+partial def intros (goal : Goal) (generation : Nat) : GrindM (List Goal) := do
+  let rec go (goal : Goal) : StateRefT (Array Goal) GrindM Unit := do
+    if goal.inconsistent then
+      return ()
+    match (← introNext goal) with
+    | .done =>
+      if let some mvarId ← goal.mvarId.byContra? then
+        go { goal with mvarId }
+      else
+        modify fun s => s.push goal
+    | .newHyp fvarId goal =>
+      if let some goals ← applyCases? goal fvarId then
+        goals.forM go
+      else if let some goal ← applyInjection? goal fvarId then
+        go goal
+      else
+        go (← GoalM.run' goal <| addHypothesis fvarId generation)
+    | .newDepHyp goal =>
+      go goal
+    | .newLocal fvarId goal =>
+      if let some goals ← applyCases? goal fvarId then
+        goals.forM go
+      else
+        go goal
+  let (_, goals) ← (go goal).run #[]
+  return goals.toList
+
+/-- Asserts a new fact `prop` with proof `proof` to the given `goal`. -/
+def assertAt (goal : Goal) (proof : Expr) (prop : Expr) (generation : Nat) : GrindM (List Goal) := do
+  -- TODO: check whether `prop` may benefit from `intros` or not. If not, we should avoid the `assert`+`intros` step and use `Grind.add`
+  let mvarId ← goal.mvarId.assert (← mkFreshUserName `h) prop proof
+  let goal := { goal with mvarId }
+  intros goal generation
+
+/-- Asserts next fact in the `goal` fact queue. -/
+def assertNext? (goal : Goal) : GrindM (Option (List Goal)) := do
+  let some (fact, newFacts) := goal.newFacts.dequeue?
+    | return none
+  assertAt { goal with newFacts } fact.proof fact.prop fact.generation
+
+partial def iterate (goal : Goal) (f : Goal → GrindM (Option (List Goal))) : GrindM (List Goal) := do
+  go [goal] []
+where
+  go (todo : List Goal) (result : List Goal) : GrindM (List Goal) := do
+    match todo with
+    | [] => return result
+    | goal :: todo =>
+      if let some goalsNew ← f goal then
+        go (goalsNew ++ todo) result
+      else
+        go todo (goal :: result)
+
+/-- Asserts all facts in the `goal` fact queue. -/
+partial def assertAll (goal : Goal) : GrindM (List Goal) := do
+  iterate goal assertNext?
+
+end Lean.Meta.Grind

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

@@ -99,4 +99,7 @@ def checkInvariants (expensive := false) : GoalM Unit := do
   if expensive && grind.debug.proofs.get (← getOptions) then
     checkProofs
 
+def Goal.checkInvariants (goal : Goal) (expensive := false) : GrindM Unit :=
+  discard <| GoalM.run' goal <| Grind.checkInvariants expensive
+
 end Lean.Meta.Grind

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

@@ -0,0 +1,93 @@
+/-
+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 Init.Grind.Lemmas
+import Lean.Meta.Tactic.Util
+import Lean.Meta.Tactic.Grind.RevertAll
+import Lean.Meta.Tactic.Grind.PropagatorAttr
+import Lean.Meta.Tactic.Grind.Proj
+import Lean.Meta.Tactic.Grind.ForallProp
+import Lean.Meta.Tactic.Grind.Util
+import Lean.Meta.Tactic.Grind.Inv
+import Lean.Meta.Tactic.Grind.Intro
+import Lean.Meta.Tactic.Grind.EMatch
+
+namespace Lean.Meta.Grind
+
+def mkMethods : CoreM Methods := do
+  let builtinPropagators ← builtinPropagatorsRef.get
+  return {
+    propagateUp := fun e => do
+     propagateForallProp e
+     let .const declName _ := e.getAppFn | return ()
+     propagateProjEq e
+     if let some prop := builtinPropagators.up[declName]? then
+       prop e
+    propagateDown := fun e => do
+     let .const declName _ := e.getAppFn | return ()
+     if let some prop := builtinPropagators.down[declName]? then
+       prop e
+  }
+
+def GrindM.run (x : GrindM α) (mainDeclName : Name) (config : Grind.Config) : MetaM α := do
+  let scState := ShareCommon.State.mk _
+  let (falseExpr, scState) := ShareCommon.State.shareCommon scState (mkConst ``False)
+  let (trueExpr, scState)  := ShareCommon.State.shareCommon scState (mkConst ``True)
+  let thms ← grindNormExt.getTheorems
+  let simprocs := #[(← grindNormSimprocExt.getSimprocs)]
+  let simp ← Simp.mkContext
+    (config := { arith := true })
+    (simpTheorems := #[thms])
+    (congrTheorems := (← getSimpCongrTheorems))
+  x (← mkMethods).toMethodsRef { mainDeclName, config, simprocs, simp } |>.run' { scState, trueExpr, falseExpr }
+
+private def mkGoal (mvarId : MVarId) : GrindM Goal := do
+  let trueExpr ← getTrueExpr
+  let falseExpr ← getFalseExpr
+  let thmMap ← getEMatchTheorems
+  GoalM.run' { mvarId, thmMap } do
+    mkENodeCore falseExpr (interpreted := true) (ctor := false) (generation := 0)
+    mkENodeCore trueExpr (interpreted := true) (ctor := false) (generation := 0)
+
+private def initCore (mvarId : MVarId) : GrindM (List Goal) := do
+  mvarId.ensureProp
+  -- TODO: abstract metavars
+  mvarId.ensureNoMVar
+  let mvarId ← mvarId.clearAuxDecls
+  let mvarId ← mvarId.revertAll
+  let mvarId ← mvarId.unfoldReducible
+  let mvarId ← mvarId.betaReduce
+  let goals ← intros (← mkGoal mvarId) (generation := 0)
+  goals.forM (·.checkInvariants (expensive := true))
+  return goals.filter fun goal => !goal.inconsistent
+
+def all (goals : List Goal) (f : Goal → GrindM (List Goal)) : GrindM (List Goal) := do
+  goals.foldlM (init := []) fun acc goal => return acc ++ (← f goal)
+
+/-- A very simple strategy -/
+private def simple (goals : List Goal) : GrindM (List Goal) := do
+  all goals ematchStar
+
+def main (mvarId : MVarId) (config : Grind.Config) (mainDeclName : Name) : MetaM (List MVarId) := do
+  let go : GrindM (List MVarId) := do
+    let goals ← initCore mvarId
+    let goals ← simple goals
+    trace[grind.debug.final] "{← ppGoals goals}"
+    return goals.map (·.mvarId)
+  go.run mainDeclName config
+
+/-- Helper function for debugging purposes -/
+def preprocessAndProbe (mvarId : MVarId) (mainDeclName : Name) (p : GoalM Unit) : MetaM Unit :=
+  let go : GrindM Unit := do
+    let goals ← initCore mvarId
+    trace[grind.debug.final] "{← ppGoals goals}"
+    goals.forM fun goal =>
+      discard <| GoalM.run' goal p
+    return ()
+  withoutModifyingMCtx do
+    go.run mainDeclName {}
+
+end Lean.Meta.Grind

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

@@ -56,4 +56,11 @@ def ppState : GoalM Format := do
       r := r ++ "\n" ++ "{" ++ (Format.joinSep (← eqc.mapM ppENodeRef) ", ") ++  "}"
   return r
 
+def ppGoals (goals : List Goal) : GrindM Format := do
+  let mut r := f!""
+  for goal in goals do
+    let (f, _) ← GoalM.run goal ppState
+    r := r ++ Format.line ++ f
+  return r
+
 end Lean.Meta.Grind