Unary VC Tactics

User-facing unary VCGen tactics and finish passes.

Unary VC tactics

def OracleComp.ProgramLogic.tacticVcstepUsing_ : Lean.ParserDescr

vcstep applies one quantitative VCGen step to a Triple, raw wp, or probability goal.

For Triple goals: decomposes a bind via triple_bind and automatically tries to close the spec subgoal using hypotheses in the local context, with backward WP fallback. Also handles ite/dite splitting, match case analysis, loop invariant auto-detection from context, and WP-rule unfolding, including simulateQ ... run'. After the built-in leaf rules, it may also use user-authored @[vcspec] lemmas whose registered head symbol matches the current computation.

For Pr[ ...] = 1 and lower-bound goals such as r ≤ Pr[ p | oa]: automatically lowers the goal into a Triple form.

For Pr[ ...] = Pr[ ...] goals: tries bind-swap (probEvent_bind_bind_swap), bind congruence (probOutput_bind_congr / probEvent_bind_congr), swap-then-congr, or an exact-probOutput bridge into relational VCGen. Handles up to 2 layers of tsum peeling for nested swaps.

For other general Pr[ ...] goals: rewrites to raw wp form and keeps stepping structurally when a wp rule applies, rather than immediately exiting the VCGen pipeline.

Variants:

• vcstep using cut for an explicit intermediate postcondition.
• vcstep with thm to force a specific unary theorem/assumption step.
• vcstep inv I to apply a loop invariant I to a replicate/foldlM/mapM goal.
• vcstep rw to perform one explicit top-level probability-equality rewrite step.
• vcstep rw under n to rewrite one bind-swap under n shared bind prefixes.
• vcstep rw congr to expose one shared bind plus its support hypothesis.
• vcstep rw congr' to expose one shared bind without a support hypothesis.

Use @[vcspec] on unary Triple or raw wp theorems to opt them into bounded lookup.

def OracleComp.ProgramLogic.tacticVcstepWith_ : Lean.ParserDescr

def OracleComp.ProgramLogic.«tacticVcstepAs⟨_⟩» : Lean.ParserDescr

def OracleComp.ProgramLogic.«tacticVcstepUsing_As⟨_⟩» : Lean.ParserDescr

def OracleComp.ProgramLogic.«tacticVcstepWith_As⟨_⟩» : Lean.ParserDescr

def OracleComp.ProgramLogic.tacticVcstep? : Lean.ParserDescr

def OracleComp.ProgramLogic.tacticVcstepRw : Lean.ParserDescr

def OracleComp.ProgramLogic.tacticVcstepRwUnder_ : Lean.ParserDescr

def OracleComp.ProgramLogic.tacticVcstepRwCongr : Lean.ParserDescr

def OracleComp.ProgramLogic.tacticVcstepRwCongr' : Lean.ParserDescr

def OracleComp.ProgramLogic.«tacticVcstepRwAs⟨_⟩» : Lean.ParserDescr

def OracleComp.ProgramLogic.«tacticVcstepRwUnder_As⟨_⟩» : Lean.ParserDescr

def OracleComp.ProgramLogic.«tacticVcstepRwCongrAs⟨_⟩» : Lean.ParserDescr

def OracleComp.ProgramLogic.«tacticVcstepRwCongr'As⟨_⟩» : Lean.ParserDescr

def OracleComp.ProgramLogic.tacticVcstepInv_ : Lean.ParserDescr

def OracleComp.ProgramLogic.«tacticVcstepInv_As⟨_⟩» : Lean.ParserDescr

def OracleComp.ProgramLogic.tacticVcgenUsing_ : Lean.ParserDescr

vcgen exhaustively decomposes a Triple, raw wp, or probability goal with spec-aware stepping.

Accepts Triple goals, raw wp goals, lower-bound / exact probability goals, and Pr[ ...] = Pr[ ...] equality goals. Probability goals are automatically lowered or dispatched (swap/congr) before structural decomposition continues.

Enhancements over simple structural decomposition:

• Lowers Pr[ ...] goals into Triple or raw wp form before decomposition
• Bridges exact Pr[= x | oa] = Pr[= x | ob] goals into relational VCGen when helpful
• After bind decomposition, tries to close spec subgoals from local context
• Falls back to backward WP (triple_bind_wp) when no spec is available
• Splits ite/dite conditionals into branch goals with hypotheses
• Case-splits match expressions on their discriminants
• Auto-detects loop invariants from context for replicate/foldlM/mapM
• Keeps decomposing across all open goals after branch splits
• Understands simulateQ and simulateQ ... run' through the unary WP rules
• Normalizes remaining wp terms and indicator arithmetic via simp
• Finishes with bounded local consequence search on closed goals

Typical usage: bring specs into context with have or as function parameters, then call vcgen to automatically decompose and apply them.

Variants:

• vcgen using cut performs one explicit bind step with intermediate postcondition cut, then continues with exhaustive decomposition on all resulting goals.
• vcgen inv I applies an explicit loop invariant I to the first replicate/foldlM/mapM goal, then continues with exhaustive decomposition.

def OracleComp.ProgramLogic.tacticVcgenInv_ : Lean.ParserDescr

def OracleComp.ProgramLogic.tacticVcgen? : Lean.ParserDescr

def OracleComp.ProgramLogic.tacticExp_norm : Lean.ParserDescr

exp_norm normalizes expectation / indicator arithmetic in the current goal.

Rewrites using linearity of expectation (wp_add, wp_mul_const), indicator algebra (propInd_true, propInd_false, propInd_and), and standard WP step rules.

def OracleComp.ProgramLogic.tacticBy_hoare : Lean.ParserDescr

by_hoare transforms a probability goal into a quantitative WP goal.