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 : Type

• noEntailment (target : Expr) : SolveResult

  target was not of the form H ⊢ₛ T.

• noProgramFoundInTarget (T : Expr) : SolveResult

  The T in H ⊢ₛ T was not of the form wp⟦e⟧ Q s₁ ... sₙ.

• noStrategyForProgram (e : Expr) : SolveResult

  Don't know how to handle e in H ⊢ₛ wp⟦e⟧ Q s₁ ... sₙ.

• noSpecFoundForProgram (e monad : Expr) (thms : Array SpecAttr.SpecTheoremNew) : SolveResult

  Did not find a spec for the e in H ⊢ₛ wp⟦e⟧ Q s₁ ... sₙ. Candidates were thms, but none of them matched the monad.

• goals (subgoals : List MVarId) : SolveResult

  Successfully decomposed the goal. These are the subgoals.

def Lean.Elab.Tactic.Do.Internal.VCGen.solve (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, .noProgramFoundInTarget, etc.) when no further decomposition is possible.

The function performs the following steps in order:

1. Forall introduction: If the target is a ∀, introduce binders via Sym.intros.
2. Triple unfolding: If the target is ⦃P⦄ x ⦃Q⦄, unfold into P ⊢ₛ wp⟦x⟧ Q.
3. PostCond.entails decomposition: Split PostCond.entails into its components.
4. Lambda introduction: If the RHS T in H ⊢ₛ T is a lambda, introduce an extra state variable via SPred.entails_cons_intro.
5. Proj/beta reduction: Reduce Prod.fst/Prod.snd projections and beta redexes in both H and T (e.g., (fun _ => T, Q.snd).fst s → T).
6. Syntactic rfl: If T is not a PredTrans.apply, try closing by SPred.entails.refl.
7. Let-hoisting: Hoist let-expressions from the program head to the goal target. 7a. Let-zeta/intro: If the target starts with let, zeta immediately if duplicable, else introduce into the local context via introsSimp. 7b. Fvar zeta: Unfold local let-bound fvars on demand when they appear as the program head.
8. Iota reduction: Reduce matchers/recursors with concrete discriminants.
9. ite/dite/match splitting: Apply the appropriate split backward rule.
10. Spec application: Look up a registered @[spec] theorem (triple or simp) and apply its cached backward rule.

Equations

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