doc:

We should have APIs for this

src/Lean/Meta/Sym.lean

@@ -23,6 +23,7 @@ public import Lean.Meta.Sym.Apply
 public import Lean.Meta.Sym.InferType
 public import Lean.Meta.Sym.Simp
 public import Lean.Meta.Sym.Util
+public import Lean.Meta.Sym.Grind
 
 /-!
 # Symbolic simulation support.

src/Lean/Meta/Sym/Apply.lean

@@ -100,8 +100,8 @@ def mkValue (expr : Expr) (pattern : Pattern) (result : MatchUnifyResult) : Expr
     mkAppN (expr.instantiateLevelParams pattern.levelParams result.us) result.args
 
 public inductive ApplyResult where
-  | notApplicable
-  | goals (mvarId : List MVarId)
+  | failed
+  | goals (mvarIds : List MVarId)
 
 /--
 Applies a backward rule to a goal, returning new subgoals.
@@ -119,7 +119,7 @@ public def BackwardRule.apply (mvarId : MVarId) (rule : BackwardRule) : SymM App
     return .goals <| rule.resultPos.map fun i =>
       result.args[i]!.mvarId!
   else
-    return .notApplicable
+    return .failed
 
 /--
 Similar to `BackwardRule.apply', but throws an error if unification fails.

src/Lean/Meta/Sym/Grind.lean

@@ -0,0 +1,129 @@
+/-
+Copyright (c) 2026 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
+-/
+module
+prelude
+public import Lean.Meta.Tactic.Grind.Types
+public import Lean.Meta.Sym.Simp.SimpM
+public import Lean.Meta.Sym.Apply
+import Lean.Meta.Tactic.Grind.Main
+import Lean.Meta.Sym.Simp.Goal
+import Lean.Meta.Sym.Intro
+import Lean.Meta.Sym.Util
+import Lean.Meta.Tactic.Grind.Solve
+import Lean.Meta.Tactic.Assumption
+namespace Lean.Meta.Grind
+
+/-!
+# Grind Goal API for Symbolic Simulation
+
+This module provides an API for building symbolic simulation engines and
+verification condition generators on top of `grind`. It wraps `Sym` operations
+to work with `grind`'s `Goal` type, enabling users to carry `grind` state
+through symbolic execution while using lightweight `Sym` operations for
+the main loop.
+
+## Typical usage pattern
+```
+let goal ← mkGoal mvarId
+let .goal xs goal ← goal.introN 2 | failure
+let .goal goal ← goal.simp methods | failure
+let goal ← goal.internalizeAll
+-- ... symbolic execution loop using goal.apply ...
+let .closed ← goal.grind | failure
+```
+
+## Design
+
+Operations like `introN`, `apply`, and `simp` run in `SymM` for performance.
+`internalize` and `grind` run in `GrindM` to access the E-graph.
+-/
+
+
+/--
+Creates a `Goal` from an `MVarId`, applying `Sym` preprocessing.
+Preprocessing ensures the goal is compatible with `Sym` operations.
+-/
+public def mkGoal (mvarId : MVarId) : GrindM Goal := do
+  let mvarId ← Sym.preprocessMVar mvarId
+  mkGoalCore mvarId
+
+open Sym (SymM)
+
+public inductive IntrosResult where
+  | failed
+  | goal (newDecls : Array FVarId) (goal : Goal)
+
+/-- Introduces `num` binders from the goal's target. -/
+public def Goal.introN (goal : Goal) (num : Nat) : SymM IntrosResult := do
+  let .goal xs mvarId ← Sym.introN goal.mvarId num | return .failed
+  return .goal xs { goal with mvarId }
+
+/-- Introduces binders with the specified names. -/
+public def Goal.intros (goal : Goal) (names : Array Name) : SymM IntrosResult := do
+  let .goal xs mvarId ← Sym.intros goal.mvarId names | return .failed
+  return .goal xs { goal with mvarId }
+
+public inductive ApplyResult where
+  | failed
+  | goals (subgoals : List Goal)
+
+/-- Applies a backward rule, returning subgoals on success. -/
+public def Goal.apply (goal : Goal) (rule : Sym.BackwardRule) : SymM ApplyResult := do
+  let .goals mvarIds ← rule.apply goal.mvarId | return .failed
+  return .goals <| mvarIds.map fun mvarId => { goal with mvarId }
+
+public inductive SimpGoalResult where
+  | noProgress
+  | closed
+  | goal (goal : Goal)
+
+/-- Simplifies the goal using the given methods. -/
+public def Goal.simp (goal : Goal) (methods : Sym.Simp.Methods := {}) (config : Sym.Simp.Config := {}) : SymM SimpGoalResult := do
+  match (← Sym.simpGoal goal.mvarId methods config) with
+  | .goal mvarId => return .goal { goal with mvarId }
+  | .noProgress  => return .noProgress
+  | .closed => return .closed
+
+/-- Like `simp`, but returns the original goal unchanged when no progress is made. -/
+public def Goal.simpIgnoringNoProgress (goal : Goal) (methods : Sym.Simp.Methods := {}) (config : Sym.Simp.Config := {}) : SymM SimpGoalResult := do
+  match (← Sym.simpGoal goal.mvarId methods config) with
+  | .goal mvarId => return .goal { goal with mvarId }
+  | .noProgress  => return .goal goal
+  | .closed => return .closed
+
+/--
+Internalizes the next `num` hypotheses from the local context into the `grind` state (e.g., its E-graph).
+-/
+public def Goal.internalize (goal : Goal) (num : Nat) : GrindM Goal := do
+  Grind.processHypotheses goal (some num)
+
+/-- Internalizes all (un-internalized) hypotheses from the local context into the `grind` state. -/
+public def Goal.internalizeAll (goal : Goal) : GrindM Goal := do
+  Grind.processHypotheses goal none
+
+public inductive GrindResult where
+  | failed (goal : Goal)
+  | closed
+
+/--
+Attempts to close the goal using `grind`.
+Returns `.closed` on success, or `.failed` with the first subgoal that failed to be closed.
+-/
+public def Goal.grind (goal : Goal) : GrindM GrindResult := do
+  if let some failure ← solve goal then
+    return .failed failure
+  else
+    return .closed
+
+/--
+Closes the goal if its target matches a hypothesis.
+Returns `true` on success.
+-/
+public def Goal.assumption (goal : Goal) : MetaM Bool := do
+  -- **TODO**: add indexing
+  goal.mvarId.assumptionCore
+
+end Lean.Meta.Grind

src/Lean/Meta/Sym/Intro.lean

@@ -96,48 +96,39 @@ def introCore (mvarId : MVarId) (max : Nat) (names : Array Name) : SymM (Array F
 
 def hugeNat := 1000000
 
+public inductive IntrosResult where
+  | failed
+  | goal (newDecls : Array FVarId) (mvarId : MVarId)
+
 /--
 Introduces leading binders (universal quantifiers and let-expressions) from the goal's target type.
 
 If `names` is non-empty, introduces (at most) `names.size` binders using the provided names.
 If `names` is empty, introduces all leading binders using inaccessible names.
 
-Returns the introduced free variable Ids and the updated goal.
-
-Throws an error if the target type does not have a leading binder.
+Returns `.goal newDecls mvarId` with new introduced free variable Ids and the updated goal.
+Returns `.failed` if no new declaration was introduced.
 -/
-public def intros (mvarId : MVarId) (names : Array Name := #[]) : SymM (Array FVarId × MVarId) := do
+public def intros (mvarId : MVarId) (names : Array Name := #[]) : SymM IntrosResult := do
   let result ← if names.isEmpty then
     introCore mvarId hugeNat #[]
   else
     introCore mvarId  names.size names
   if result.1.isEmpty then
-    throwError "`intros` failed, binder expected"
-  return result
-
-/--
-Introduces a single binder from the goal's target type with the given name.
-
-Returns the introduced free variable ID and the updated goal.
-Throws an error if the target type does not have a leading binder.
--/
-public def intro (mvarId : MVarId) (name : Name) : SymM (FVarId × MVarId) := do
-  let (fvarIds, goal') ← introCore mvarId 1 #[name]
-  if h : 0 < fvarIds.size then
-    return (fvarIds[0], goal')
-  else
-    throwError "`intro` failed, binder expected"
+    return .failed
+  return .goal result.1 result.2
 
 /--
 Introduces exactly `num` binders from the goal's target type.
 
-Returns the introduced free variable IDs and the updated goal.
-Throws an error if the target type has fewer than `num` leading binders.
+Returns `.goal newDecls mvarId` if successful where `newDecls` are the introduced free variable IDs,
+`mvarId` the updated goal.
+Returns `.failed` if it was not possible to introduce `num` new local declarations.
 -/
-public def introN (mvarId : MVarId) (num : Nat) : SymM (Array FVarId × MVarId) := do
+public def introN (mvarId : MVarId) (num : Nat) : SymM IntrosResult := do
   let result ← introCore mvarId num #[]
   unless result.1.size == num do
-    throwError "`introN` failed, insufficient number of binders"
-  return result
+    return .failed
+  return .goal result.1 result.2
 
 end Lean.Meta.Sym

src/Lean/Meta/Sym/Simp/Goal.lean

@@ -72,7 +72,7 @@ public def simpGoal (mvarId : MVarId) (methods :  Simp.Methods := {}) (config :
 /--
 Similar to `simpGoal`, but returns `.goal mvarId` if no progress was made.
 -/
-public def trySimpGoal (mvarId : MVarId) (methods :  Simp.Methods := {}) (config : Simp.Config := {})
+public def simpGoalIgnoringNoProgress (mvarId : MVarId) (methods :  Simp.Methods := {}) (config : Simp.Config := {})
     : SymM SimpGoalResult := do
   match (← simpGoal mvarId methods config) with
   | .noProgress => return .goal mvarId

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

@@ -155,7 +155,7 @@ private def initENodeCore (e : Expr) (interpreted ctor : Bool) : GoalM Unit := d
   mkENodeCore e interpreted ctor (generation := 0) (funCC := false)
 
 /-- Returns a new goal for the given metavariable. -/
-public def mkGoal (mvarId : MVarId) : GrindM Goal := do
+public def mkGoalCore (mvarId : MVarId) : GrindM Goal := do
   let config ← getConfig
   let mvarId ← if config.clean then mvarId.exposeNames else pure mvarId
   let trueExpr ← getTrueExpr
@@ -288,7 +288,7 @@ private def initCore (mvarId : MVarId) : GrindM Goal := do
   let mvarId ← mvarId.unfoldReducible
   let mvarId ← mvarId.betaReduce
   appendTagSuffix mvarId `grind
-  let goal ← mkGoal mvarId
+  let goal ← mkGoalCore mvarId
   if config.revert then
     return goal
   else

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.lean

@@ -188,6 +188,12 @@ def applyEqLemma (e : Expr → EqResult) (lemmaName : Name) (args : Array Expr)
   return .some (e (mkAppN (mkConst lemmaName) args))
 
 def reduceNatEqExpr (x y : Expr) : SimpM (Option EqResult):= do
+  /-
+  **TODO**: These proofs rely too much on definitional equality.
+  Example:
+  `x + 1 + 1 + ... + 1 = x + 1 + ... + 1`
+  It will treat both sides as `x + n = x + n`.
+  -/
   let some xno ← NatOffset.fromExpr? x | return none
   let some yno ← NatOffset.fromExpr? y | return none
   match xno, yno with

tests/bench/sym/add_sub_cancel.lean

@@ -299,7 +299,7 @@ partial def solve (mvarId : MVarId) (simpEagerly : Bool) : SymM Unit := do
   -- `processMVar` ensures the input goal becomes a `Sym` compatible goal.
   let mvarId ← preprocessMVar mvarId
   -- `intro m l`
-  let (_, mvarId) ← Sym.introN mvarId 2
+  let .goal _ mvarId ← Sym.introN mvarId 2 | failure
   -- `simp only [generated_cmd, repeated_cmds]`
   let .goal mvarId ← Sym.simpGoal mvarId unfoldMethods | failure
   -- `apply Exec.seq_cps`
@@ -307,7 +307,7 @@ partial def solve (mvarId : MVarId) (simpEagerly : Bool) : SymM Unit := do
   -- `apply Exec.input`
   let .goals [mvarId] ← inputRule.apply mvarId | failure
   -- `intro v`
-  let (_, mvarId) ← Sym.introN mvarId 1
+  let .goal _ mvarId ← Sym.introN mvarId 1 | failure
   -- ## Loop
   -- We simulate the `repeat` block using a tail-recursive function `loop`
   let rec loop (mvarId : MVarId) : SymM MVarId := do
@@ -326,7 +326,7 @@ partial def solve (mvarId : MVarId) (simpEagerly : Bool) : SymM Unit := do
     if simpEagerly then
       -- The following step is not in the `MetaM` version, but it helps performance
       -- `simp only [PartialMap.get_put_diff, PartialMap.get_put, PartialMap.put_put, Binop.interp_add, Binop.interp_sub, Word.add_sub_cancel, Option.some.injEq, not_false_eq_true, String.reduceEq, ne_eq]`
-      let .goal mvarId ← Sym.trySimpGoal mvarId simpMethods | failure
+      let .goal mvarId ← Sym.simpGoalIgnoringNoProgress mvarId simpMethods | failure
       loop mvarId
     else
       loop mvarId
@@ -383,11 +383,11 @@ partial def solveReusingCache (mvarId : MVarId) : SymM Unit := do
     ``and_self, ``exists_eq_True, ``Word.add_sub_cancel]
   -- ## Initialize
   let mvarId ← preprocessMVar mvarId
-  let (_, mvarId) ← Sym.introN mvarId 2
+  let .goal _ mvarId ← Sym.introN mvarId 2 | failure
   let .goal mvarId ← Sym.simpGoal mvarId unfoldMethods | failure
   let .goals [mvarId] ← exec_cpsRule.apply mvarId | failure
   let .goals [mvarId] ← inputRule.apply mvarId | failure
-  let (_, mvarId) ← Sym.introN mvarId 1
+  let .goal _ mvarId ← Sym.introN mvarId 1 | failure
   -- ## Loop
   let rec loop (mvarId : MVarId) (simpState : Sym.Simp.State) : SymM MVarId := do
     let .goals [mvarId] ← exec_cpsRule.apply mvarId | return mvarId

tests/bench/sym/shallow_add_sub_cancel.lean

@@ -40,6 +40,12 @@ theorem Exec.ite_false {_ : Decidable c} (t e : StateM S α) :
     ¬ c → Exec s e post → Exec s (if c then t else e) post := by
   intro h; simp [*]
 
+theorem Exec.ite {_ : Decidable c} (t e : StateM S α) :
+    (c → Exec s t post) → (¬ c → Exec s e post) → Exec s (if c then t else e) post := by
+  intro h₁ h₂; split
+  next h => exact h₁ h
+  next h => exact h₂ h
+
 theorem modify_eq : (modify f : StateM S Unit) s = ((), f s) := by
   simp [modify, modifyGet, MonadStateOf.modifyGet, StateT.modifyGet, pure]
 
@@ -140,7 +146,7 @@ partial def solve (mvarId : MVarId) : SymM Unit := do
   -- `processMVar` ensures the input goal becomes a `Sym` compatible goal.
   let mvarId ← preprocessMVar mvarId
   -- `intro s post n`
-  let (_, mvarId) ← Sym.introN mvarId 3
+  let .goal _ mvarId ← Sym.introN mvarId 3 | failure
   let .goal mvarId ← Sym.simpGoal mvarId preMethods | failure
   -- ## Loop
   -- We simulate the `repeat` block using a tail-recursive function `loop`

tests/bench/sym/shallow_add_sub_cancel_grind.lean

@@ -0,0 +1,159 @@
+import Lean
+
+/-!
+Benchmark similar to `add_sub_cancel` but using a shallow embedding into monadic `do` notation.
+-/
+
+def Exec (s : S) (k : StateM S α) (post : α → S → Prop) : Prop :=
+  post (k s).1 (k s).2
+
+theorem Exec.pure (a : α) :
+    post a s → Exec s (pure a) post := by
+  simp [Exec, Pure.pure, StateT.pure]
+
+theorem Exec.bind (k₁ : StateM S α) (k₂ : α → StateM S β) (post : β → S → Prop) :
+    Exec s k₁ (fun a s₁ => Exec s₁ (k₂ a) post)
+    → Exec s (k₁ >>= k₂) post := by
+  simp [Exec, Bind.bind, StateT.bind]
+  cases k₁ s; simp
+
+theorem Exec.andThen (k₁ : StateM S α) (k₂ : StateM S β) (post : β → S → Prop) :
+    Exec s k₁ (fun _ s₁ => Exec s₁ k₂ post)
+    → Exec s (k₁ *> k₂) post := by
+  simp [Exec, SeqRight.seqRight, StateT.bind, Bind.bind]
+  cases k₁ s; simp
+
+theorem Exec.get : post s s → Exec s get post := by
+  simp [Exec, MonadState.get, getThe, MonadStateOf.get, StateT.get, Pure.pure]
+
+theorem Exec.set : post () s' → Exec s (set s') post := by
+  simp [Exec, MonadStateOf.set, StateT.set, Pure.pure]
+
+theorem Exec.modify : post () (f s) → Exec s (modify f) post := by
+  simp [Exec, _root_.modify, modifyGet, MonadStateOf.modifyGet, StateT.modifyGet, Pure.pure]
+
+theorem Exec.ite_true {_ : Decidable c} (t e : StateM S α) :
+    c → Exec s t post → Exec s (if c then t else e) post := by
+  intro h; simp [*]
+
+theorem Exec.ite_false {_ : Decidable c} (t e : StateM S α) :
+    ¬ c → Exec s e post → Exec s (if c then t else e) post := by
+  intro h; simp [*]
+
+theorem Exec.ite {_ : Decidable c} (t e : StateM S α) :
+    (c → Exec s t post) → (¬ c → Exec s e post) → Exec s (if c then t else e) post := by
+  intro h₁ h₂; split
+  next h => exact h₁ h
+  next h => exact h₂ h
+
+theorem modify_eq : (modify f : StateM S Unit) s = ((), f s) := by
+  simp [modify, modifyGet, MonadStateOf.modifyGet, StateT.modifyGet, pure]
+
+def step (v : Nat) : StateM Nat Unit := do
+  let s ← get
+  set (v + s)
+  let s' ← get
+  if s' = s then
+    set (s' - v)
+
+def loop (n : Nat) : StateM Nat Unit := do
+  match n with
+  | 0 => pure ()
+  | n+1 => step n; loop n
+
+def Goal (n : Nat) : Prop := ∀ s, Exec s (loop n) fun _ s' => s' > s
+
+set_option maxRecDepth 100_000
+
+open Lean Meta Elab
+
+/-- Helper function for executing a tactic `k` for solving `Goal n`. -/
+def driver (n : Nat) (check := true) (k : MVarId → MetaM Unit) : MetaM Unit := do
+  let some goal ← unfoldDefinition? (mkApp (mkConst ``Goal) (mkNatLit n)) | throwError "UNFOLD FAILED!"
+  let mvar ← mkFreshExprMVar goal
+  let startTime ← IO.monoNanosNow
+  k mvar.mvarId!
+  let endTime ← IO.monoNanosNow
+  let ms := (endTime - startTime).toFloat / 1000000.0
+  if check then
+    let startTime ← IO.monoNanosNow
+    checkWithKernel (← instantiateExprMVars mvar)
+    let endTime ← IO.monoNanosNow
+    let kernelMs := (endTime - startTime).toFloat / 1000000.0
+    IO.println s!"goal_{n}: {ms} ms, kernel: {kernelMs} ms"
+  else
+    IO.println s!"goal_{n}: {ms} ms"
+
+/-!
+`SymM` + `GrindM` Solution
+-/
+
+open Sym Grind
+
+theorem unit_map : (fun _ : Unit => PUnit.unit) <$> (k : StateM Nat Unit) = k := by
+ simp
+
+def mkSimpMethods (declNames : Array Name) : MetaM Sym.Simp.Methods := do
+  let rewrite ← Sym.mkSimprocFor declNames Sym.Simp.dischargeSimpSelf
+  return {
+    post := Sym.Simp.evalGround.andThen rewrite
+  }
+
+def isBind (goal : Goal) : MetaM Bool := do
+  let target ← goal.mvarId.getType
+  let_expr Exec _ _ _ k _ := target | return false
+  return k.isAppOf ``Bind.bind
+
+partial def solve (mvarId : MVarId) : GrindM Unit := do
+  /-
+  Creates an `BackwardRule` for each theorem `T` we want to use `apply T`.
+  -/
+  let execBindRule ← mkBackwardRuleFromDecl ``Exec.bind
+  let execGetRule ← mkBackwardRuleFromDecl ``Exec.get
+  let execSetRule ← mkBackwardRuleFromDecl ``Exec.set
+  let execPureRule ← mkBackwardRuleFromDecl ``Exec.pure
+  let execIteTrueRule ← mkBackwardRuleFromDecl ``Exec.ite_true
+  let execIteFalseRule ← mkBackwardRuleFromDecl ``Exec.ite_false
+  /-
+  Creates simplification methods for each collection of rewriting rules we want to apply.
+  Recall Lean creates equational lemmas of the form `_eq_<idx>` for definitions.
+  -/
+  let preMethods ← mkSimpMethods #[``step.eq_1, ``loop.eq_1, ``loop.eq_2,
+    ``Nat.add_zero, ``Nat.sub_zero, ``bind_pure_comp, ``map_bind, ``id_map', ``unit_map, ``bind_assoc]
+  -- ## Initialize
+  let goal ← mkGoal mvarId
+  let .goal _ goal ← goal.introN 1 | failure
+  let .goal goal ← goal.simp preMethods | failure
+  let goal ← goal.internalizeAll -- Internalize all hypotheses
+  -- ## Loop
+  -- We simulate the `repeat` block using a tail-recursive function `loop`
+  let rec loop (goal₀ : Goal) : GrindM Goal := do
+    -- logInfo goal₀.mvarId
+    let .goals [goal] ← goal₀.apply execBindRule | return goal₀
+    let .goals [goal] ← goal.apply execGetRule | failure
+    let .goals [goal] ← goal.apply execBindRule | failure
+    let .goals [goal] ← goal.apply execSetRule | failure
+    let .goals [goal] ← goal.apply execBindRule | failure
+    let .goals [goal] ← goal.apply execGetRule | failure
+    if (← isBind goal) then
+      let .goals [goal] ← goal.apply execBindRule | failure
+      let .goals [goalCond, goal] ← goal.apply execIteFalseRule | failure
+      let .closed ← goalCond.grind | failure
+      let .goals [goal] ← goal.apply execPureRule | failure
+      loop goal
+    else
+      let .goals [goalCond, goal] ← goal.apply execIteTrueRule | failure
+      let .closed ← goalCond.grind | failure
+      return goal
+  let goal ← loop goal
+  let .goals [goal] ← goal.apply execSetRule | failure
+  let .closed ← goal.grind | failure
+  return
+
+def solveUsingGrind (n : Nat) (check := true) : MetaM Unit := do
+  let params ← mkDefaultParams {}
+  driver n check fun mvarId => SymM.run <| GrindM.run (params := params) do
+    solve mvarId
+
+-- **TODO**: the proof term grows quadratically because we are not simplifying the state
+#eval solveUsingGrind 50

tests/lean/run/sym_intro.lean

@@ -10,7 +10,7 @@ open Lean Meta Sym Elab Tactic
 
 def test (mvarId : MVarId) : MetaM MVarId := do
   SymM.run do
-    let (_, mvarId) ← intros mvarId
+    let .goal _ mvarId ← intros mvarId | failure
     return mvarId
 
 /--

tests/lean/run/sym_intro_have.lean

@@ -23,6 +23,6 @@ run_meta SymM.run do
   let mvarId ← unfoldTarget mvarId ``f
   let mvarId ← mvarId.liftLets
   logInfo mvarId
-  let (_, mvarId) ← intro mvarId `y
+  let .goal _ mvarId ← intros mvarId #[`y] | failure
   logInfo mvarId
   return ()

tests/lean/sym/perf_sym_apply.lean

@@ -26,7 +26,7 @@ set_option maxRecDepth 10000000
 def tryIntros? (goals : List MVarId) : SymM (Option (List MVarId)) := do
   try
     let goal :: goals := goals | return none
-    let (_, goal') ← intros goal
+    let .goal _ goal' ← intros goal | failure
     return some (goal' :: goals)
   catch _ =>
     return none