Construction of BackwardRules from SpecTheorems and split info, with no knowledge of VCGenM. The VCGenM cache wrappers live in VCGen.RuleCache.

Spec rules

def Lean.Elab.Tactic.Do.Internal.VCGen.tryMkBackwardRuleFromSpec (specThm : SpecAttr.SpecTheorem) (info : WPApp) (stateArgNames : Array Name := #[]) : OptionT MetaM Meta.Sym.BackwardRule

Try to build a backward rule from a single spec theorem.

For a spec already in ⊑ wp form (pre ⊑ wp prog post epost, where the lattice type is info.Pred = σ1 → ... → σn → Prop), produces an auxiliary lemma directly. An equality spec lhs = rhs is first normalized to wp rhs Q E ⊑ wp lhs Q E via eqSpecToWp? and then handled the same way.

• info.Pred: the goal's lattice type (e.g. Nat → Prop)
• info.instWP: the WPMonad instance for the goal monad
• info.excessArgs: free variables representing state args from info.Pred = σ1 → ... → σn → Prop

Equations

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

Split rules

def Lean.Elab.Tactic.Do.Internal.VCGen.mkBackwardRuleForSplit (splitInfo : SplitInfo) (info : WPApp) : MetaM Meta.Sym.BackwardRule

Creates a reusable backward rule for splitting ite, dite, or matchers.

Uses SplitInfo.withAbstract to introduce abstract fvars for the split components, then SplitInfo.splitWith to build the splitting proof. Hypothesis types are discovered via rwIfOrMatcher inside the splitter telescope.

Equations

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

Frame rules

def Lean.Elab.Tactic.Do.Internal.VCGen.mkFrameBackwardRule (op : Expr) (info : WPApp) : MetaM Meta.Sym.BackwardRule

The F-abstract upper-adjoint frame rule for a frame operator op : R → Pred → Pred.

The rule concludes pre ⊑ wp prog Q E s⃗ from the framed precondition pre ⊑ op F (wp prog (fun a => upperAdjoint (op F) (Q a)) E) s⃗ and the frame condition WP.Frames op prog F, with the frame F left schematic so a single rule serves every inferred frame. Its subgoals lead with F, so the caller assigns the inferred frame before decomposing the rest.

Equations

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