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.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 eposts, 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 WP instance of the goal's wp application
• 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.VCGen.mkBackwardRuleForSplit (splitInfo : Do.SplitInfo) (info : WPApp) : MetaM Meta.Sym.BackwardRule

Creates a reusable backward rule for splitting ite, dite, cond, 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.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 meet_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 G, with the frame F left schematic, the guard G the frame of pre for the excess state arguments fun u⃗ => ⌜u⃗ = s⃗⌝ ⊓ pre, and the weakest footprint W = wp prog (fun a => upperAdjoint (op F) (Q a)) (upperAdjoint (opE F) 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.