The main solve step. Runs once per worklist iteration and either fully decomposes the current goal into subgoals, or reports why no further progress is possible (SolveResult).

inductive Lean.Elab.Tactic.Do.Internal.VCGen.SolveResult.StopReason : Type

The reason why no further VC generation progress is possible on the current goal.

• outOfFuel : StopReason

  Out of fuel.

• untilPatternMatched (m : Expr) : StopReason

  until <pat> matched.

• noEntailment (target : Expr) : StopReason

  The target was not of the form pre ⊑ rhs.

• noProgress (pre rhs : Expr) : StopReason

  The target was of the form pre ⊑ rhs, but we couldn't make further progress.

• noSpecFound (e monad : Expr) (thms : Array SpecAttr.SpecTheorem) : StopReason

  No spec was found for the program e in pre ⊑ wp e post epost s₁ ... sₙ. Candidates were thms, but none matched the monad. Reached only when errorOnMissingSpec is false.

inductive Lean.Elab.Tactic.Do.Internal.VCGen.SolveResult : Type

The result of one solve step of VC generation.

• goals (scope : Scope) (subgoals : List MVarId) : SolveResult

  Successfully decomposed the goal. These are the subgoals, sharing scope.

• stop (reason : StopReason) : SolveResult

  No further progress possible; emit the current goal as a VC.

def Lean.Elab.Tactic.Do.Internal.VCGen.matchFrame? (resourceTy : Expr) (info : WPApp) : VCGenM (Option Expr)

Find an unretired frames alternative matching the program (earliest source order wins), elaborate its frame at the resource type resourceTy, and retire it so it applies at most once.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Tactic.Do.Internal.VCGen.solve (scope : Scope) (goal : MVarId) : VCGenM SolveResult

The main VC generation step. Operates on a plain MVarId with no knowledge of grind. Returns .goals subgoals when the goal was decomposed, or a classification result (.noEntailment, .noProgramOrLatticeFoundInTarget, etc.) when no further decomposition is possible.

The function performs the following steps in order:

1. Forall introduction: If the target is a ∀, simp it and introduce binders.
2. Target-let handling: zeta-substitute duplicable top-level lets, otherwise introduce them.
3. Triple unfolding: If the target is ⦃P⦄ x ⦃Q; E⦄, unfold into P ⊑ wp x Q E.
4. Syntactic rfl: close pre ⊑ rhs by PartialOrder.rel_refl when both sides unify.
5. Embedded pure precondition introduction: lift a ⌜φ⌝ precondition into the local context, before state-argument introduction would apply it to the introduced arguments.
6. State-argument introduction: If the lattice carrier is a function type σ₁ → ... → σₙ → Base, introduce all excess state arguments.
7. Bare pure precondition introduction: on the Prop lattice, replace a True precondition by ⊤ and lift any other precondition into the local context.
8. EPost projection reduction: reduce an EPost.Cons.head RHS to the projected component.
9. Lattice decomposition: decompose ⊓, ⇨, ⌜p⌝ and ⊤ RHS connectives.
10. Lifted-hypothesis discharge: close a residual pre ⊑ ⌜φ⌝ entailment against the most recently lifted precondition h : φ in the local context, cached in Scope.lastLiftedPre?.
11. WP decomposition: when the RHS is wp e post epost s₁ ... sₙ, in order: hoist/zeta program-head lets, split ite/dite/match, zeta-unfold fvar program heads, reduce projection heads, and finally apply a registered @[spec] theorem.

Equations

• One or more equations did not get rendered due to their size.