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 (fp : FrameProc) (info : WPApp) : MetaM FrameBackwardRule

The frame backward rule for a frame operator op : R → Pred → Pred, built from the frame rule WP.Frames.op_wp_upperAdjoint_le_wp.

The rule concludes pre ⊑ wp prog Q E s⃗ from the split VC pre ⊑ (op F W) s⃗ and the frame condition WP.Frames op prog F, with the frame F left schematic and the weakest footprint W = wp prog (fun a => upperAdjoint (op F) (Q a)) E baked in, so a single rule serves every inferred frame. analyzeFrameRule records the positions of the schematic slots.

Equations

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