From a4931661a3007e1b790c0db81a2053cbc604db39 Mon Sep 17 00:00:00 2001 From: Sebastian Graf Date: Thu, 7 May 2026 18:03:27 +0000 Subject: [PATCH] =?UTF-8?q?feat:=20support=20`mvcgen'`=20inside=20`sym=20?= =?UTF-8?q?=3D>=20=E2=80=A6`=20blocks?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This PR registers `mvcgen'` as a step in the `grind` syntax category, so it can be used inside `sym => …` blocks. Each leftover VC becomes a fresh `Grind.Goal` built in the surrounding block's `Grind.GrindM`, with its local hypotheses internalized (`processHypotheses`) and the block's user-supplied e-match theorems activated (`assertExtra`), so subsequent grind steps see them without explicit `internalize_all` or having to re-pass the lemmas. Spec lookup (`mkBackwardRuleFromSpec`) wraps its three triple-defeq checks in `Meta.withDefault`. The ambient grind transparency is `reducible` (set by `Grind.withGTransparency` because `Grind.Config.reducible := true`), under which instance projections like `WPMonad.toWP` don't unfold and so don't compare equal to a direct `WP` instance. Standalone `mvcgen'` happens to inherit default transparency from `MetaM`, so the issue only surfaces when called from inside an outer `Grind.GrindM`. `Driver.runFromGoal` is renamed to `Driver.run`; callers seed the `Grind.Goal` themselves (via `Grind.mkGoalCore` from `TacticM`, or `getMainGoal` from `Grind.GrindTacticM`). --- .../Tactic/Do/Internal/VCGen/Context.lean | 5 +- .../Elab/Tactic/Do/Internal/VCGen/Driver.lean | 19 +++-- .../Tactic/Do/Internal/VCGen/Frontend.lean | 75 +++++++++++++++--- .../Do/Internal/VCGen/RuleConstruction.lean | 8 +- src/Std/Tactic/Do/Syntax.lean | 12 +++ tests/elab/mvcgenSymBlock.lean | 76 +++++++++++++++++++ 6 files changed, 168 insertions(+), 27 deletions(-) create mode 100644 tests/elab/mvcgenSymBlock.lean diff --git a/src/Lean/Elab/Tactic/Do/Internal/VCGen/Context.lean b/src/Lean/Elab/Tactic/Do/Internal/VCGen/Context.lean index 13ce4f25d46e..eb77218b88a3 100644 --- a/src/Lean/Elab/Tactic/Do/Internal/VCGen/Context.lean +++ b/src/Lean/Elab/Tactic/Do/Internal/VCGen/Context.lean @@ -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 diff --git a/src/Lean/Elab/Tactic/Do/Internal/VCGen/Driver.lean b/src/Lean/Elab/Tactic/Do/Internal/VCGen/Driver.lean index 1f11003a5ecf..89fad0f256dd 100644 --- a/src/Lean/Elab/Tactic/Do/Internal/VCGen/Driver.lean +++ b/src/Lean/Elab/Tactic/Do/Internal/VCGen/Driver.lean @@ -108,7 +108,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 +120,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 +166,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 +182,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, diff --git a/src/Lean/Elab/Tactic/Do/Internal/VCGen/Frontend.lean b/src/Lean/Elab/Tactic/Do/Internal/VCGen/Frontend.lean index af095e778160..198c0400fe1a 100644 --- a/src/Lean/Elab/Tactic/Do/Internal/VCGen/Frontend.lean +++ b/src/Lean/Elab/Tactic/Do/Internal/VCGen/Frontend.lean @@ -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,7 +27,7 @@ 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. -/ @@ -269,8 +270,8 @@ 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` 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` 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. -/ @@ -292,8 +293,17 @@ private def elabRemainingInvariants (alts : Std.HashMap Nat Syntax) 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. Lives in `TacticM` because the elaboration +helpers it calls do; `evalMVCGen'Grind` reaches it via a `Tactic.run` +excursion. -/ +private def parseArgs (stx : Syntax) : TacticM ParsedArgs := withMainContext 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." @@ -316,15 +326,56 @@ 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 + return { config, ctx, params, invariantAlts? } + +/-- `mvcgen'` step inside `sym => …` blocks; the `invariants?` suggester +form is unsupported here. -/ +@[builtin_grind_tactic Lean.Parser.Tactic.Grind.mvcgen'] +def evalMVCGen'Grind : Lean.Elab.Tactic.Grind.GrindTactic := fun stx => do + let goal ← Lean.Elab.Tactic.Grind.getMainGoal + -- `TacticM` excursion to parse args; capture via `IO.Ref` since `Tactic.run` + -- only propagates leftover `MVarId`s. + let argsRef : IO.Ref (Option ParsedArgs) ← IO.mkRef none + let _ ← Lean.Elab.Tactic.run goal.mvarId do + argsRef.set (some (← parseArgs stx)) + let some args ← argsRef.get + | throwError "internal error: `mvcgen'` parsing produced no args" + let result ← Lean.Elab.Tactic.Grind.liftGrindM <| + VCGen.run goal args.ctx args.config.stepLimit + match args.invariantAlts? with + | some alts => + let _ ← Lean.Elab.Tactic.run goal.mvarId <| + elabRemainingInvariants alts result.invariants result.inlineHandledInvariants + | none => + if !stx[3].isNone then + throwError "`mvcgen' invariants?` (suggest mode) is not supported inside `sym => …` blocks" + let invariants ← result.invariants.filterM (not <$> ·.isAssigned) + let newGoals ← Lean.Elab.Tactic.Grind.liftGrindM do + -- VCs inherit the parent's E-graph; `processHypotheses` internalizes + -- fvars introduced during VC generation. Invariants are discharged via + -- term values, so a fresh `mkGoalCore` is enough. + let invGoals ← invariants.toList.mapM Grind.mkGoalCore + 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 `evalMVCGen'Grind` 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 args ← parseArgs stx + let mvarId ← getMainGoal + let result ← Grind.GrindM.run (do + VCGen.run (← Grind.mkGoalCore mvarId) args.ctx args.config.stepLimit) args.params + if let some alts := args.invariantAlts? then elabRemainingInvariants alts result.invariants result.inlineHandledInvariants else - elabInvariants stx[3] result.invariants (suggestInvariant result.vcs) + 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" diff --git a/src/Lean/Elab/Tactic/Do/Internal/VCGen/RuleConstruction.lean b/src/Lean/Elab/Tactic/Do/Internal/VCGen/RuleConstruction.lean index 84365a9f6dea..9236a51cc141 100644 --- a/src/Lean/Elab/Tactic/Do/Internal/VCGen/RuleConstruction.lean +++ b/src/Lean/Elab/Tactic/Do/Internal/VCGen/RuleConstruction.lean @@ -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`) + -- need defaults 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 diff --git a/src/Std/Tactic/Do/Syntax.lean b/src/Std/Tactic/Do/Syntax.lean index baf8407e4908..508007d9c81d 100644 --- a/src/Std/Tactic/Do/Syntax.lean +++ b/src/Std/Tactic/Do/Syntax.lean @@ -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 diff --git a/tests/elab/mvcgenSymBlock.lean b/tests/elab/mvcgenSymBlock.lean new file mode 100644 index 000000000000..679df548ad6f --- /dev/null +++ b/tests/elab/mvcgenSymBlock.lean @@ -0,0 +1,76 @@ +import Std.Tactic.Do + +/-! Tests that `mvcgen'` is usable as a step inside `sym => …` blocks. -/ + +open Std.Do + +set_option mvcgen.warning false + +/-! ## Trivial postcondition: `mvcgen'` closes the goal -/ + +axiom G : StateM Nat Unit +axiom H : StateM Nat Unit + +noncomputable def F : StateM Nat Unit := do + G + H + +@[spec] +axiom G_spec : ⦃⌜True⌝⦄ G ⦃⇓ _ n => ⌜n = n⌝⦄ + +@[spec] +axiom H_spec : ⦃⌜True⌝⦄ H ⦃⇓ _ n => ⌜n = n⌝⦄ + +example : ⦃⌜True⌝⦄ F ⦃⇓ _ n => ⌜n = n⌝⦄ := by + sym => + mvcgen' [F] + +/-! ## Pre-tactic dispatches the leftover VC -/ + +axiom G2 : StateM Nat Unit +axiom H2 : StateM Nat Unit + +noncomputable def F2 : StateM Nat Unit := do + G2 + H2 + +axiom P : Nat → Prop + +@[spec] +axiom G2_spec : ⦃⌜True⌝⦄ G2 ⦃⇓ _ n => ⌜P n⌝⦄ + +@[spec] +axiom H2_spec : ⦃fun n => ⌜P n⌝⦄ H2 ⦃⇓ _ n => ⌜True⌝⦄ + +example : ⦃⌜True⌝⦄ F2 ⦃⇓ _ n => ⌜True⌝⦄ := by + sym => + mvcgen' [F2] with grind + +/-! ## VC leftover; closed by a subsequent grind step -/ + +axiom G3 : StateM Nat Unit +axiom H3 : StateM Nat Unit + +noncomputable def F3 : StateM Nat Unit := do + G3 + H3 + +axiom Q : Nat → Prop +axiom hPQ : ∀ n, P n → Q n + +@[spec] +axiom G3_spec : ⦃⌜True⌝⦄ G3 ⦃⇓ _ n => ⌜P n⌝⦄ + +@[spec] +axiom H3_spec : ⦃fun n => ⌜Q n⌝⦄ H3 ⦃⇓ _ n => ⌜True⌝⦄ + +example : ⦃⌜True⌝⦄ F3 ⦃⇓ _ n => ⌜True⌝⦄ := by + sym => + mvcgen' [F3] + finish [hPQ] + +-- `sym [hPQ]` propagates to the new VC `Grind.Goal`s; no need to re-pass it. +example : ⦃⌜True⌝⦄ F3 ⦃⇓ _ n => ⌜True⌝⦄ := by + sym [hPQ] => + mvcgen' [F3] + finish