leanprover · sgraf812 · May 26, 2026 · May 7, 2026
@@ -123,9 +123,10 @@ public structure VCGen.State where
   -/
   invariants : Array MVarId := #[]
   /--
-  The verification conditions that have been generated so far.
+  The verification conditions that have been generated so far. Each entry
+  shares the parent `Grind.Goal`'s state.
   -/
-  vcs : Array MVarId := #[]
+  vcs : Array Grind.Goal := #[]
   /--
   Persistent cache for the `Sym.Simp` simplifier used to pre-simplify hypotheses
   before grind internalization. Threading this cache across VCGen iterations avoids

@@ -58,15 +58,18 @@ succeeded. Numbering is 1-based; out-of-order labelled forms (e.g. `| inv2 =>
 before `| inv1 => …`) are supported because the map is keyed by parsed number,
 not position.
 -/
-private def tryInlineInvariant (n : Nat) (mv : MVarId) : VCGenM Bool := do
-  let some alt := (← read).invariantAlts[n]? | return false
+public def elabInvariant (invariantAlts : Std.HashMap Nat Syntax) (n : Nat) (mv : MVarId) : SymM Bool := do
   try
+    let some alt := invariantAlts[n]? | return false
     let tac ← match alt with
       | `(Lean.Parser.Tactic.invariantDotAlt| · $rhs) => `(tactic| exact $rhs)
       | `(Lean.Parser.Tactic.invariantCaseAlt| | $_tag $args* => $rhs) =>
           `(tactic| (rename_i $args*; exact $rhs))
       | _ => return false
-    let _ ← Lean.Elab.runTactic mv tac {} {}
+    -- `withDefault`: the surrounding grind context forces reducible transparency,
+    -- under which the invariant's binder type (e.g. `List.Cursor _`) isn't
+    -- resolved enough for term elaboration of `xs.suffix.length` to succeed.
+    withRef alt <| discard <| Meta.withDefault <| Lean.Elab.runTactic mv tac {} {}
     -- The tactic runs without throwing even when it fails to close the goal;
     -- check explicitly that the MVar got assigned.
     if ← mv.isAssigned then
@@ -78,8 +81,7 @@ private def tryInlineInvariant (n : Nat) (mv : MVarId) : VCGenM Bool := do
       return true
     else
       return false
-  catch _ =>
-    return false
+  catch _ => return false
 
 /-- Pull invariant subgoals out of `subgoals` and handle them eagerly: register
 each in `State.invariants` (1-based stable index) and try to inline-elaborate
@@ -93,7 +95,7 @@ private def handleInvariantSubgoals (subgoals : List MVarId) : VCGenM (Array MVa
     if isSpecInvariantType env (← sg.getType) then
       let n := (← get).invariants.size + 1
       modify fun s => { s with invariants := s.invariants.push sg }
-      if ← tryInlineInvariant n sg then
+      if ← elabInvariant (← read).invariantAlts n sg then
         modify fun s => { s with inlineHandledInvariants := s.inlineHandledInvariants.insert n }
       else
         sg.setKind .syntheticOpaque
@@ -108,7 +110,7 @@ so they never reach this path.
 -/
 public def emitVC (goal : Grind.Goal) : VCGenM Unit := do
   let goal ← (← read).preTac.processHypotheses goal
-  let mut vcs := #[]
+  let mut vcs : Array Grind.Goal := #[]
   -- `trivial`: when false, skip `repeatAndRfl` (which collapses And-chains via rfl);
   -- emit the goal as-is.
   let mvarId ←
@@ -120,7 +122,7 @@ public def emitVC (goal : Grind.Goal) : VCGenM Unit := do
   let goal := { goal with mvarId := mvarId }
   for mvarId in (← (← read).preTac.run goal) do
     mvarId.setKind .syntheticOpaque
-    vcs := vcs.push mvarId
+    vcs := vcs.push { goal with mvarId }
   modify fun s => { s with vcs := s.vcs ++ vcs }
 
 public def work (goal : Grind.Goal) : VCGenM Unit := do
@@ -166,8 +168,8 @@ public structure Result where
   invariant number. Some entries may already be assigned (inline-elaborated by
   `Driver.emitVC`); the caller is responsible for filtering before discharging. -/
   invariants : Array MVarId
-  /-- Unassigned VCs. -/
-  vcs : Array MVarId
+  /-- Unassigned VCs. Each shares the parent `Grind.Goal`'s state. -/
+  vcs : Array Grind.Goal
   /-- Invariant numbers handled inline by `Driver.emitVC`. Used by `Frontend` to
   avoid spurious "alt does not match any invariant" warnings for inline-consumed
   alts. -/
@@ -182,16 +184,15 @@ Return the VCs and invariant goals.
 
 `stepLimit?`, when `some n`, seeds the fuel counter to `n`; when `none`, fuel is unlimited.
 -/
-public partial def main (goal : MVarId) (ctx : Context) (stepLimit? : Option Nat := none) :
+public partial def run (goal : Grind.Goal) (ctx : Context) (stepLimit? : Option Nat := none) :
     Grind.GrindM Result := do
-  let grindGoal ← Grind.mkGoalCore goal
   let initState : State := { fuel := match stepLimit? with | some n => .limited n | none => .unlimited }
-  let ((), state) ← StateRefT'.run (ReaderT.run (work grindGoal) ctx) initState
+  let ((), state) ← StateRefT'.run (ReaderT.run (work goal) ctx) initState
   _ ← state.invariants.mapIdxM fun idx mv => do
     mv.setTag (Name.mkSimple ("inv" ++ toString (idx + 1)))
-  _ ← state.vcs.mapIdxM fun idx mv => do
-    mv.setTag (Name.mkSimple ("vc" ++ toString (idx + 1)) ++ (← mv.getTag).eraseMacroScopes)
-  let vcs ← state.vcs.filterM (not <$> ·.isAssigned)
+  _ ← state.vcs.mapIdxM fun idx g => do
+    g.mvarId.setTag (Name.mkSimple ("vc" ++ toString (idx + 1)) ++ (← g.mvarId.getTag).eraseMacroScopes)
+  let vcs ← state.vcs.filterM (not <$> ·.mvarId.isAssigned)
   return {
     invariants := state.invariants,
     vcs,

@@ -16,7 +16,8 @@ public import Lean.Meta.Sym.Simp.EvalGround
 public import Lean.Meta.Sym.Simp.Forall
 public import Lean.Meta.Sym.Simp.Rewrite
 public import Lean.Meta.Sym.Simp.Simproc
-import Lean.Elab.Tactic.Grind.Main
+public import Lean.Elab.Tactic.Grind.Main
+public import Lean.Elab.Tactic.Grind.Basic
 
 open Lean Parser Meta Elab Tactic Sym
 open Lean.Elab.Tactic.Do Lean.Elab.Tactic.Do.SpecAttr
@@ -26,10 +27,14 @@ namespace Lean.Elab.Tactic.Do.Internal
 
 /-!
 `mvcgen'` tactic frontend: parse the user-facing argument syntax into a
-`VCGen.Context`, run `VCGen.main`, and replace the main goal with the
+`VCGen.Context`, run `VCGen.run`, and replace the main goal with the
 resulting invariants and VCs.
 -/
 
+/-- A local helper for running config elaborators in TermElabM. -/
+private def runTacticM (x : TacticM α) (goals : List MVarId := [])  : TermElabM α :=
+  x.run { elaborator := `mvcgen } |>.run' { goals }
+
 namespace VCGen
 
 /--
@@ -38,7 +43,7 @@ spec theorems and simp lemmas. Follows the same approach as
 `Lean.Elab.Tactic.Do.VCGen.mkSpecContext`: each entry is first tried as a spec theorem,
 and on failure falls back to a simp/unfold lemma processed via `mkSimpContext`.
 -/
-public def mkSpecContext (lemmas : Syntax) (ignoreStarArg := false) : TacticM VCGen.Context := do
+public def mkSpecContext (lemmas : Syntax) (goal : MVarId) (ignoreStarArg := false) : TermElabM VCGen.Context := do
   let mut specThms ← getSpecTheorems
   let mut simpStuff := #[]
   let mut starArg := false
@@ -87,7 +92,7 @@ public def mkSpecContext (lemmas : Syntax) (ignoreStarArg := false) : TacticM VC
   -- spec simp theorems database (which contains `@[spec]`-registered simp equations
   -- and definitions to unfold).
   let stx ← `(tactic| simp +unfoldPartialApp -zeta [$(Syntax.TSepArray.ofElems simpStuff),*])
-  let res ← mkSimpContext stx.raw
+  let res ← runTacticM (goals := [goal]) <| mkSimpContext stx.raw
     (eraseLocal := false)
     (simpTheorems := getSpecSimpTheorems)
     (ignoreStarArg := ignoreStarArg)
@@ -144,17 +149,17 @@ end VCGen
 ignored at runtime. As more options gain implementation support, drop their checks
 here. Options with implemented semantics (`trivial`, `elimLets`, `stepLimit`,
 `invariants?`) are silently accepted. -/
-private def warnIgnoredConfig (config : VCGen.Config) : TacticM Unit := do
+private def warnIgnoredConfig (config : VCGen.Config) : MetaM Unit := do
   let default : VCGen.Config := {}
   if config.leave != default.leave then
     logWarning "mvcgen': the `leave` config option is currently ignored."
 
 /-- Parse grind configuration from the `with grind ...` clause and build `Grind.Params`.
 Overrides the internal simp step limit to accommodate large unrolled goals. -/
-private def elabGrindParams (grindStx : Syntax) (goal : MVarId) : TacticM Grind.Params := do
+private def elabGrindParams (grindStx : Syntax) (goal : MVarId) : TermElabM Grind.Params := do
   let `(tactic| grind $config:optConfig $[only%$only]? $[ [$grindParams:grindParam,*] ]? $[=> $_:grindSeq]?) := grindStx
     | throwUnsupportedSyntax
-  let grindConfig ← elabGrindConfig config
+  let grindConfig ← runTacticM <| elabGrindConfig config
   mkGrindParams grindConfig only.isSome (grindParams.getD {}).getElems goal
 
 /--
@@ -165,7 +170,7 @@ Supports the anonymous (default) variant. Named variants require a public
 private def elabSymSimpParts
     (variantId? : Option (TSyntax `ident))
     (extraIds? : Option (Array (TSyntax `ident)))
-    : TacticM Sym.Simp.Methods := do
+    : MetaM Sym.Simp.Methods := do
   let variantName := variantId?.map (·.getId) |>.getD .anonymous
   if !variantName.isAnonymous then
     -- TODO: `resolveExtraTheorems`, `elabVariant`, and `elabSymSimproc` in
@@ -196,14 +201,15 @@ private def elabSymSimpParts
     post := post >> thms.rewrite
   return { pre, post }
 
-private def elabSimplifyingAssumptions (simpClause : Syntax) : TacticM (Option Sym.Simp.Methods) := do
+private def elabSimplifyingAssumptions (simpClause : Syntax) : MetaM (Option Sym.Simp.Methods) := do
   if simpClause.getNumArgs == 0 then return none
   let variantId? := if simpClause[1].getNumArgs != 0 then some ⟨simpClause[1][0]⟩ else none
   let extraIds? := if simpClause[2].getNumArgs != 0
     then some (simpClause[2][1].getSepArgs.map (⟨·⟩)) else none
   pure (some (← elabSymSimpParts variantId? extraIds?))
 
-private def elabPreTac (goal : MVarId) (withPreTac : Syntax) : TacticM (VCGen.PreTac × Grind.Params) := do
+-- The goal is for `elabGrindParams` which uses it for library suggestions.
+private def elabPreTac (goal : MVarId) (withPreTac : Syntax) : TermElabM (VCGen.PreTac × Grind.Params) := do
   let mut params ← Grind.mkDefaultParams {}
   if withPreTac.getNumArgs == 0 then return (.none, params)
   let preTac := withPreTac[1]
@@ -231,7 +237,7 @@ forms (one or the other is enforced by the `dotOrCase` flag in the upstream
 elaborator; we replicate that check here).
 -/
 private def parseInvariantMap (stx : Syntax) :
-    TacticM (Option (Std.HashMap Nat Syntax)) := do
+    TermElabM (Option (Std.HashMap Nat Syntax)) := do
   let some altsStx := stx.getOptional? | return none
   -- The `invariants?` (suggest) form is handled separately by upstream's `elabInvariants`.
   match altsStx with
@@ -269,43 +275,45 @@ private def parseInvariantMap (stx : Syntax) :
 
 /--
 Run after VC generation: iterate the (unfiltered) `invariants` array returned by
-`Driver.main`, look up each entry in the pre-parsed `alts` map by its 1-based
-position (which equals the `inv<n>` tag the entry carries — `Driver.main` assigns
+`VCGen.run`, look up each entry in the pre-parsed `alts` map by its 1-based
+position (which equals the `inv<n>` tag the entry carries — `VCGen.run` assigns
 tags consecutively), and elaborate the matching alt. Invariants that were already
 elaborated inline by `Driver.emitVC` (tracked in `inlineHandled`) are skipped, so
 we don't warn about alts that were already consumed there. -/
 private def elabRemainingInvariants (alts : Std.HashMap Nat Syntax)
-    (invariants : Array MVarId) (inlineHandled : Std.HashSet Nat) : TacticM Unit := do
+    (invariants : Array MVarId) (inlineHandled : Std.HashSet Nat) : SymM Unit := do
   let mut handled := inlineHandled
   for h : i in 0...invariants.size do
     let n := i + 1
     if handled.contains n then continue
     let some alt := alts[n]? | continue
     handled := handled.insert n
-    let tac ← match alt with
-      | `(invariantDotAlt| · $rhs) => `(tactic| exact $rhs)
-      | `(invariantCaseAlt| | $_tag $args* => $rhs) => `(tactic| (rename_i $args*; exact $rhs))
-      | _ => continue
-    withRef alt <| discard <| evalTacticAt tac invariants[i]
+    discard <| VCGen.elabInvariant alts n invariants[i]
   -- Warn on user-provided alts that matched no invariant goal (neither inline nor post-hoc).
   for (n, alt) in alts.toArray do
     unless handled.contains n do
       logWarningAt alt s!"Invariant alternative `inv{n}` does not match any invariant goal."
 
-@[builtin_tactic Lean.Parser.Tactic.mvcgen']
-public def elabMVCGen' : Tactic := fun stx => withMainContext do
+/-- Parsed `mvcgen'` arguments shared by the two entry points. -/
+private structure ParsedArgs where
+  config : VCGen.Config
+  ctx : VCGen.Context
+  params : Grind.Params
+  invariantAlts? : Option (Std.HashMap Nat Syntax)
+
+/-- Parse `mvcgen'` arguments. -/
+private def parseArgs (stx : Syntax) (goal : MVarId) : TermElabM ParsedArgs := goal.withContext do
   if mvcgen.warning.get (← getOptions) then
     logWarningAt stx "The `mvcgen'` tactic is an experimental drop-in replacement for `mvcgen` \
       that will eventually replace it. Avoid using it in production projects."
-  let config ← elabConfig stx[1]
+  let config ← runTacticM <| elabConfig stx[1]
   warnIgnoredConfig config
-  let goal ← getMainGoal
   -- `elimLets` defaults to `false` in `mvcgen'` (vs. `true` in upstream `mvcgen`):
   -- existing tests rely on let-bindings being preserved in VC local contexts so that
   -- `case vcN bs* =>` patterns line up. Re-enabling on opt-in would require detecting
   -- explicit `(elimLets := true)` at the syntax level (upstream `Config` can't
   -- distinguish "default true" from "user-set true"); not yet wired.
-  let ctx ← VCGen.mkSpecContext stx[2]
+  let ctx ← VCGen.mkSpecContext stx[2] goal
   let hypSimpMethods ← elabSimplifyingAssumptions stx[4]
   let (preTac, params) ← elabPreTac goal stx[5]
   let invariantAlts? ← parseInvariantMap stx[3]
@@ -316,15 +324,49 @@ public def elabMVCGen' : Tactic := fun stx => withMainContext do
     errorOnMissingSpec := config.errorOnMissingSpec,
     debug := config.debug,
     invariantAlts := invariantAlts?.getD {} }
-  let result ← Grind.GrindM.run (VCGen.main goal ctx config.stepLimit) params
-  -- For `invariants?` (suggest), defer entirely to the upstream elaborator.
-  -- Otherwise, dispatch any still-unassigned invariants via the pre-parsed map.
-  if let some alts := invariantAlts? then
-    elabRemainingInvariants alts result.invariants result.inlineHandledInvariants
-  else
-    elabInvariants stx[3] result.invariants (suggestInvariant result.vcs)
+  return { config, ctx, params, invariantAlts? }
+
+/-- `mvcgen'` step inside `sym => …` blocks. -/
+@[builtin_grind_tactic Lean.Parser.Tactic.Grind.mvcgen']
+def evalSymMVCGen' : Lean.Elab.Tactic.Grind.GrindTactic := fun stx => do
+  let goal ← Lean.Elab.Tactic.Grind.getMainGoal
+  let args ← parseArgs stx goal.mvarId
+  if args.invariantAlts?.isNone && !stx[3].isNone then
+    throwError "`mvcgen' invariants?` (suggest mode) is not supported inside `sym => …` blocks"
+  let result ← Lean.Elab.Tactic.Grind.liftGrindM do
+    let result ← VCGen.run goal args.ctx args.config.stepLimit
+    if let some alts := args.invariantAlts? then
+      elabRemainingInvariants alts result.invariants result.inlineHandledInvariants
+    return result
+  let invariants ← result.invariants.filterM (not <$> ·.isAssigned)
+  let newGoals ← Lean.Elab.Tactic.Grind.liftGrindM do
+    let invGoals ← invariants.toList.mapM Grind.mkGoalCore
+    -- Need to internalize all remaining hypotheses in the goal. As of May 26, it is still unclear
+    -- whether it is the job of downstream tactics such as `finish` in `sym => mvcgen'; finish`
+    -- to internalize.
+    let vcGoals ← result.vcs.toList.mapM Grind.processHypotheses
+    return invGoals ++ vcGoals
+  Lean.Elab.Tactic.Grind.replaceMainGoal newGoals
+  if result.preTacFailed then
+    throwError "pre-tactic failed on at least one VC; see errors above"
+
+/-- Tactic-level `mvcgen'`. -/
+-- Cannot wrap `evalSymMVCGen'` because routing through `runAtGoal`/`withProtectedMCtx` wraps the
+-- proof in an aux theorem, which rejects unsolved leftover VCs.
+@[builtin_tactic Lean.Parser.Tactic.mvcgen']
+public def elabMVCGen' : Tactic := fun stx => withMainContext do
+  let goal ← getMainGoal
+  let args ← parseArgs stx goal
+  let result ← Grind.GrindM.run (params := args.params) do
+    let result ← VCGen.run (← Grind.mkGoalCore goal) args.ctx args.config.stepLimit
+    if let some alts := args.invariantAlts? then
+      elabRemainingInvariants alts result.invariants result.inlineHandledInvariants
+    return result
+  if args.invariantAlts?.isNone then
+    -- handle `mvcgen invariants?` suggestions. TODO: re-implement
+    elabInvariants stx[3] result.invariants (suggestInvariant (result.vcs.map (·.mvarId)))
   let invariants ← result.invariants.filterM (not <$> ·.isAssigned)
-  replaceMainGoal (invariants ++ result.vcs).toList
+  replaceMainGoal (invariants.toList ++ result.vcs.toList.map (·.mvarId))
   if result.preTacFailed then
     throwError "pre-tactic failed on at least one VC; see errors above"
 

@@ -133,11 +133,13 @@ public def mkBackwardRuleFromSpec (specThm : SpecTheoremNew) (m σs ps instWP :
   let_expr f@Triple m' ps' instWP' α prog P Q := specTy
     | liftMetaM <| throwError "target not a Triple application {specTy}"
   -- Reject the spec and try the next if the monad doesn't match.
-  unless ← isDefEqGuarded m m' do -- TODO: Try isDefEqS?
+  -- `withDefault`: spec/goal instance projections (e.g. `WPMonad.toWP`)
+  -- needs default to unfold; the ambient grind transparency is `reducible`.
+  unless ← Meta.withDefault <| isDefEqGuarded m m' do
     throwError "Post program defeq Monad mismatch: {m} ≠ {m'}"
-  unless ← isDefEqGuarded ps ps' do
+  unless ← Meta.withDefault <| isDefEqGuarded ps ps' do
     throwError "Post program defeq Postshape mismatch: {ps} ≠ {ps'}"
-  unless ← isDefEqGuarded instWP instWP' do
+  unless ← Meta.withDefault <| isDefEqGuarded instWP instWP' do
     throwError "Post program defeq WP instance mismatch: {instWP} ≠ {instWP'}"
 
   -- We must ensure that P and Q are pattern variables so that the spec matches for every potential

@@ -9,6 +9,7 @@ prelude
 public import Std.Do
 public import Std.Tactic.Do.ProofMode -- For (meta) importing `mgoalStx`; otherwise users might experience
 public import Init.Data.Array.GetLit
+public import Init.Grind.Interactive
                                       -- a broken goal view due to the builtin delaborator for `MGoalEntails`
 
 @[expose] public section
@@ -434,3 +435,14 @@ syntax (name := mvcgen') "mvcgen'" optConfig
   (invariantAlts)?
   (&" simplifying_assumptions" (ppSpace colGt ident)? (" [" ident,* "]")?)?
   (&" with " tactic)? : tactic
+
+namespace Grind
+
+/-- `mvcgen'` step for `sym => …` blocks; same surface as the tactic form. -/
+syntax (name := mvcgen') "mvcgen'" optConfig
+  (" [" withoutPosition((simpStar <|> simpErase <|> simpLemma),*,?) "] ")?
+  (invariantAlts)?
+  (&" simplifying_assumptions" (ppSpace colGt ident)? (" [" ident,* "]")?)?
+  (&" with " tactic)? : grind
+
+end Grind