feat: add until clause to mvcgen' (#13983)

This PR adds `mvcgen' until $t`, where `$t` is a conv-style pattern
(holes `_` allowed); verification-condition generation stops as soon as
the program matches the pattern, leaving it as a VC instead of applying
a spec, similar to the existing `stepLimit` option.

The pattern is elaborated lazily against the monad of the first program
it is tested against, so overloaded heads resolve correctly and editor
hovers work on the pattern. The out-of-fuel check and the new `until`
check now share a single `SolveResult.stop`.

Author: sgraf812

src/Lean/Elab/Tactic/Do/Internal/VCGen/Context.lean

@@ -25,6 +25,26 @@ The `VCGenM` monad: its read-only `Context` (a fixed bundle of pre-built
 (rule caches, accumulated invariants/VCs, simp cache).
 -/
 
+/-- A lazily elaborated `until` pattern, stored behind an `IO.Ref` so the first `force` caches its
+result. The pattern is elaborated against the monad of the first program encountered in `solve`
+(supplied as the expected type). -/
+public inductive UntilPatternThunk where
+  /-- Not yet elaborated; `elabFn m` elaborates the pattern against the program monad `m`. -/
+  | deferred (elabFn : Expr → MetaM Sym.Pattern)
+  /-- Already elaborated and cached. -/
+  | elaborated (pat : Sym.Pattern)
+
+/-- Force the thunk in `ref` against the program monad `m`, elaborating, tracing, and caching the
+pattern on first use; later calls return the cached pattern. -/
+public def UntilPatternThunk.force (ref : IO.Ref UntilPatternThunk) (m : Expr) : MetaM Sym.Pattern := do
+  match ← ref.get with
+  | .elaborated pat => return pat
+  | .deferred elabFn =>
+    let pat ← elabFn m
+    trace[Elab.Tactic.Do.vcgen] "`until` pattern elaborated to {pat.pattern}"
+    ref.set (.elaborated pat)
+    return pat
+
 public structure VCGen.Context where
   /-- The backward rule for `SPred.entails_cons_intro`. -/
   entailsConsIntroRule : BackwardRule
@@ -93,6 +113,9 @@ public structure VCGen.Context where
   the parsed `inv<n>` numbers (out-of-order labels are supported). Empty when no
   `invariants` clause is provided or in `invariants?` (suggest) mode (handled separately). -/
   invariantAlts : Std.HashMap Nat Syntax := {}
+  /-- The `until` pattern: when `some ref`, VC generation stops and emits the current goal as a VC
+  once the program in `wp⟦e⟧` matches the (lazily elaborated) pattern, before applying a spec. -/
+  untilPat? : Option (IO.Ref UntilPatternThunk) := none
 
 public structure VCGen.Scope where
   /-- Spec database in scope: globals plus locals from in-scope hypotheses. -/

src/Lean/Elab/Tactic/Do/Internal/VCGen/Driver.lean

@@ -108,10 +108,9 @@ public def work (scope : Scope) (goal : Grind.Goal) : VCGenM Unit := do
     worklist := worklist.pop
     let goal := s.goal
     if goal.inconsistent then continue
-    if ← outOfFuel then
-      emitVC goal
-      continue
     match ← solve s.scope goal.mvarId with
+    | .stop =>
+      emitVC goal
     | .noEntailment .. | .noProgramFoundInTarget .. =>
       emitVC goal
     | .noSpecFoundForProgram prog monad thms =>

src/Lean/Elab/Tactic/Do/Internal/VCGen/Frontend.lean

@@ -18,6 +18,7 @@ public import Lean.Meta.Sym.Simp.Rewrite
 public import Lean.Meta.Sym.Simp.Simproc
 public import Lean.Elab.Tactic.Grind.Main
 public import Lean.Elab.Tactic.Grind.Basic
+import Lean.Meta.Sym.ProofInstInfo
 
 open Lean Parser Meta Elab Tactic Sym
 open Lean.Elab.Tactic.Do Lean.Elab.Tactic.Do.SpecAttr
@@ -277,6 +278,38 @@ private structure ParsedArgs where
   scope : VCGen.Scope
   invariantAlts? : Option (Std.HashMap Nat Syntax)
 
+/-- Build a `Sym.Pattern` from `e` by abstracting the metavariables `xs` into pattern variables.
+`checkTypeMask?` is `none` because `until` holes appear as function arguments, whose types the
+enclosing application already constrains. -/
+private def mkUntilPattern (xs : Array Expr) (e : Expr) : MetaM Sym.Pattern := do
+  let pattern := e.abstract xs
+  let mut varTypes := #[]
+  for h : i in [0:xs.size] do
+    varTypes := varTypes.push ((← inferType xs[i]).abstractRange i xs)
+  let mut fnInfos : AssocList Name Sym.ProofInstInfo := {}
+  for declName in pattern.getUsedConstants do
+    if let some info ← Sym.mkProofInstInfo? declName then
+      fnInfos := fnInfos.insertNew declName info
+  let varInfos? ← Sym.mkProofInstArgInfo? xs
+  return { levelParams := [], varTypes, pattern, fnInfos, varInfos?, checkTypeMask? := none }
+
+/-- Build a deferred `until` pattern (holes `_` allowed, as in `conv in $t`). The pattern term is
+elaborated lazily when the first program is seen in `solve`, using that program's monad `m` as the
+expected type (`m _`) so overloaded heads resolve; the result is cached. The holes become pattern
+variables. -/
+private def elabUntilPattern (p : Term) : TermElabM (IO.Ref UntilPatternThunk) := do
+  let lctx ← getLCtx
+  let localInsts ← getLocalInstances
+  IO.mkRef <| UntilPatternThunk.deferred fun m =>
+    withLCtx lctx localInsts <| Term.TermElabM.run' <|
+      -- Restore the metavariable state but keep info trees, so hovers work on the pattern.
+      Term.withoutModifyingElabMetaStateWithInfo <| withRef p <|
+      withTheReader Term.Context ({ · with ignoreTCFailures := true }) <|
+      Term.withoutErrToSorry do
+        let e ← instantiateMVars (← Term.elabTerm p (some (mkApp m (← mkFreshTypeMVar))))
+        let xs := (e.collectMVars {}).result.map Expr.mvar
+        mkUntilPattern xs e
+
 /-- Parse `mvcgen'` arguments. -/
 private def parseArgs (stx : Syntax) (goal : MVarId) : TermElabM ParsedArgs := goal.withContext do
   if mvcgen.warning.get (← getOptions) then
@@ -290,16 +323,18 @@ private def parseArgs (stx : Syntax) (goal : MVarId) : TermElabM ParsedArgs := g
   -- explicit `(elimLets := true)` at the syntax level (upstream `Config` can't
   -- distinguish "default true" from "user-set true"); not yet wired.
   let (ctx, scope) ← VCGen.mkContext stx[2] goal
-  let hypSimpMethods ← elabSimplifyingAssumptions stx[4]
-  let invariantAlts? ← parseInvariantMap stx[3]
+  let untilPat? ← if stx[3].isNone then pure none else some <$> elabUntilPattern ⟨stx[3][1]⟩
+  let hypSimpMethods ← elabSimplifyingAssumptions stx[5]
+  let invariantAlts? ← parseInvariantMap stx[4]
   let ctx := { ctx with
     hypSimpMethods,
     trivial := config.trivial,
     useJP := config.jp,
     errorOnMissingSpec := config.errorOnMissingSpec,
     debug := config.debug,
     internalize := config.internalize,
-    invariantAlts := invariantAlts?.getD {} }
+    invariantAlts := invariantAlts?.getD {},
+    untilPat? }
   return { config, ctx, scope, invariantAlts? }
 
 /-- `mvcgen'` step inside `sym => …` blocks. -/
@@ -314,7 +349,7 @@ def evalSymMVCGen' : Lean.Elab.Tactic.Grind.GrindTactic := fun stx => do
     return result
   if args.invariantAlts?.isNone then
     runTacticM (goals := result.invariants.toList) <|
-      elabInvariants stx[3] result.invariants (suggestInvariant (result.vcs.map (·.mvarId)))
+      elabInvariants stx[4] result.invariants (suggestInvariant (result.vcs.map (·.mvarId)))
   let invariants ← result.invariants.filterM (not <$> ·.isAssigned)
   let newGoals ← Lean.Elab.Tactic.Grind.liftGrindM do
     let invGoals ← invariants.toList.mapM Grind.mkGoalCore
@@ -328,7 +363,7 @@ goals. The optional `with $g:grind` clause runs as `<;> $g` and lets the user-su
 grind step share an internalised E-graph with `mvcgen'`. -/
 @[builtin_tactic Lean.Parser.Tactic.mvcgen']
 public def elabMVCGen' : Tactic := fun stx => withMainContext do
-  let `(tactic| mvcgen'%$tk $cfg:optConfig $[[$lems,*]]? $(invs)?
+  let `(tactic| mvcgen'%$tk $cfg:optConfig $[[$lems,*]]? $[until $u:term]? $(invs)?
         $[simplifying_assumptions $(sa)? $[[$thms,*]]?]? $[with $g:grind]?) := stx
     | throwUnsupportedSyntax
   -- Without `with`, no downstream grind step will read the E-graph, so opt out of
@@ -338,7 +373,7 @@ public def elabMVCGen' : Tactic := fun stx => withMainContext do
     | none   => do
         let off ← `(optConfig| -internalize)
         pure (Lean.Parser.Tactic.appendConfig off cfg)
-  let core ← `(grind| mvcgen'%$tk $cfg:optConfig $[[$lems,*]]? $(invs)?
+  let core ← `(grind| mvcgen'%$tk $cfg:optConfig $[[$lems,*]]? $[until $u:term]? $(invs)?
         $[simplifying_assumptions $(sa)? $[[$thms,*]]?]?)
   let step ← match g with
     | some g => `(grind| $core <;> $g)

src/Lean/Elab/Tactic/Do/Internal/VCGen/Solve.lean

@@ -41,6 +41,8 @@ public inductive SolveResult where
   | noSpecFoundForProgram (e : Expr) (monad : Expr) (thms : Array SpecTheoremNew)
   /-- Successfully decomposed the goal. These are the subgoals, sharing `scope`. -/
   | goals (scope : VCGen.Scope) (subgoals : List MVarId)
+  /-- Stop decomposing and emit the current goal as a VC (out of fuel, or `until` matched). -/
+  | stop
 
 private def isDuplicable (e : Expr) : Bool := match e with
   | .bvar .. | .mvar .. | .fvar .. | .const .. | .lit .. | .sort .. => true
@@ -208,6 +210,7 @@ The function performs the following steps in order:
     its cached backward rule.
 -/
 public def solve (scope : VCGen.Scope) (goal : MVarId) : VCGenM SolveResult := goal.withContext do
+  if ← outOfFuel then return .stop
   let target ← goal.getType
   trace[Elab.Tactic.Do.vcgen] "🎯 Target: {target}"
   -- Phase 1: simplify `target` until it is of the form `H ⊢ₛ T`.
@@ -268,6 +271,16 @@ public def solve (scope : VCGen.Scope) (goal : MVarId) : VCGenM SolveResult := g
     VCGen.burnOne
     return .goals scope [g]
 
+  -- Stop if the program matches the `until` pattern (elaborated lazily against the program monad).
+  let matchesUntilPattern (m : Expr) : VCGenM Bool := do
+    let some ref := (← read).untilPat? | return false
+    let pat ← UntilPatternThunk.force ref m
+    if (← pat.match? e).isSome then
+      trace[Elab.Tactic.Do.vcgen] "`until` pattern matched program {e}; stopping"
+      return true
+    return false
+  if ← matchesUntilPattern m then return .stop
+
   -- Apply registered specifications, or fall through to `.noStrategyForProgram`.
   VCGen.burnOne
   applySpec scope goal e excessArgs m σs ps instWP

src/Std/Tactic/Do/Syntax.lean

@@ -444,6 +444,7 @@ syntax (name := mvcgenHint) "mvcgen?" optConfig
 @[tactic_alt Lean.Parser.Tactic.mvcgen'Macro]
 syntax (name := mvcgen') "mvcgen'" optConfig
   (" [" withoutPosition((simpStar <|> simpErase <|> simpLemma),*,?) "] ")?
+  (&" until " term)?
   (invariantAlts)?
   (&" simplifying_assumptions" (ppSpace colGt ident)? (" [" ident,* "]")?)?
   (&" with " grind)? : tactic
@@ -454,6 +455,7 @@ namespace Grind
 steps using `<;>` instead. -/
 syntax (name := mvcgen') "mvcgen'" optConfig
   (" [" withoutPosition((simpStar <|> simpErase <|> simpLemma),*,?) "] ")?
+  (&" until " term)?
   (invariantAlts)?
   (&" simplifying_assumptions" (ppSpace colGt ident)? (" [" ident,* "]")?)?
   : grind

tests/elab/mvcgenUntil.lean

@@ -0,0 +1,66 @@
+import Lean
+import Std
+import Std.Tactic.Do
+
+set_option mvcgen.warning false
+set_option warn.sorry false
+
+/-! Tests for the `mvcgen' until <pattern>` stop condition. -/
+
+open Std.Do
+
+namespace MVCGenUntil
+
+def tick : StateM Nat Unit := modify (· + 1)
+
+def useTick : StateM Nat Nat := do
+  tick
+  return 0
+
+def step (k : Nat) : StateM Nat Unit := modify (· + k)
+
+def useStep : StateM Nat Nat := do
+  step 1
+  return 0
+
+def getThenTick : StateM Nat Nat := do
+  let x ← get
+  tick
+  return x
+
+-- `until tick` matches the nullary `tick` call and stops; `unfold tick` hits the leftover `wp⟦tick⟧`.
+theorem useTick_until : ⦃⌜True⌝⦄ useTick ⦃⇓ _ => ⌜True⌝⦄ := by
+  mvcgen' [useTick] until tick
+  all_goals unfold tick
+  all_goals admit
+
+-- An explicit hole matches: `until step _` stops at `step 1`, the `_` matching its argument.
+theorem useStep_until_hole : ⦃⌜True⌝⦄ useStep ⦃⇓ _ => ⌜True⌝⦄ := by
+  mvcgen' [useStep] until step _
+  all_goals unfold step
+  all_goals admit
+
+-- A concrete argument discriminates: `until step 1` matches the `step 1` call and stops.
+theorem useStep_until_one : ⦃⌜True⌝⦄ useStep ⦃⇓ _ => ⌜True⌝⦄ := by
+  mvcgen' [useStep] until step 1
+  all_goals unfold step
+  all_goals admit
+
+-- ...but `until step 2` does not match `step 1`, so VC generation reaches the un-specced call.
+/-- error: No spec found for program step 1. -/
+#guard_msgs in
+example : ⦃⌜True⌝⦄ useStep ⦃⇓ _ => ⌜True⌝⦄ := by
+  mvcgen' [useStep] until step 2
+
+-- A non-matching `until` (with a hole) is a no-op: VC generation runs to completion.
+theorem useStep_until_nomatch : ⦃⌜True⌝⦄ useStep ⦃⇓ r => ⌜r = 0⌝⦄ := by
+  mvcgen' [useStep, step] until List.length _
+  all_goals grind
+
+-- The overloaded `get` is resolved against the program's monad and matches the `get` call, so VC
+-- generation stops before the un-specced `tick`. A wrong resolution would proceed to `tick` and error.
+theorem getThenTick_until_get : ⦃⌜True⌝⦄ getThenTick ⦃⇓ _ => ⌜True⌝⦄ := by
+  mvcgen' [getThenTick] until get
+  all_goals admit
+
+end MVCGenUntil