Relational VC Tactics

User-facing relational VCGen tactics and syntax.

def OracleComp.ProgramLogic.tacticRvcstepUsing_ : Lean.ParserDescr

rvcstep applies one relational VCGen step.

It first lowers GameEquiv / evalDist equality goals into relational mode, then tries the obvious structural relational rule on RelTriple / RelWP / eRelTriple goals: synchronized conditionals, simulateQ, Functor.map, bounded traversals, bind decomposition, or random/query coupling.

rvcstep using t supplies the explicit witness needed for the current shape:

• bind cut relation
• random/query bijection
• traversal input relation (List.mapM / List.foldlM)
• simulateQ state relation

rvcstep with thm forces one explicit relational theorem/assumption step.

def OracleComp.ProgramLogic.tacticRvcstepWith_ : Lean.ParserDescr

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

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

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

def OracleComp.ProgramLogic.tacticRvcstep? : Lean.ParserDescr

def OracleComp.ProgramLogic.tacticRvcgenUsing_ : Lean.ParserDescr

rvcgen repeatedly applies relational VCGen steps across all current goals until stuck.

rvcgen using t uses the explicit hint t for the first step on the main goal, then continues with ordinary hint-free relational VCGen on all remaining goals.

rvcgen with thm forces one explicit relational theorem step on the main goal, then continues with ordinary hint-free relational VCGen on all remaining goals.

def OracleComp.ProgramLogic.tacticRvcgenWith_ : Lean.ParserDescr

def OracleComp.ProgramLogic.tacticRvcgen? : Lean.ParserDescr

def OracleComp.ProgramLogic.tacticRel_conseqWith_ : Lean.ParserDescr

rel_conseq weakens or strengthens the postcondition of a RelTriple goal.

Given a goal RelTriple oa ob R', applies relTriple_post_mono to produce:

1. RelTriple oa ob ?R — the triple with a (possibly easier) postcondition
2. ∀ x y, ?R x y → R' x y — the implication between postconditions

Use rel_conseq with R to specify the intermediate postcondition explicitly.

def OracleComp.ProgramLogic.tacticRel_inline_ : Lean.ParserDescr

rel_inline unfolds definitions and then tries to close or simplify the relational goal. Use rel_inline foo bar to unfold specific definitions, or just rel_inline to simplify.

Proof mode entry tactics

def OracleComp.ProgramLogic.tacticBy_equiv : Lean.ParserDescr

by_equiv transforms a GameEquiv g₁ g₂ goal into RelTriple g₁ g₂ (EqRel α). Also works for evalDist g₁ = evalDist g₂ goals. Always targets RelTriple (coupling-based), never RelTriple' (eRHL-based), so that rvcstep / rvcgen work on the resulting goal.

def OracleComp.ProgramLogic.tacticRel_dist : Lean.ParserDescr

rel_dist reduces a RelTriple oa ob (EqRel α) goal to evalDist oa = evalDist ob.

This is the reverse direction of by_equiv: while by_equiv enters relational mode from a distributional equality, rel_dist exits relational mode back to distributional reasoning.

Useful when both sides are equal in distribution but not syntactically identical, and the equality is easier to prove at the evalDist level than via stepwise coupling.

def OracleComp.ProgramLogic.tacticGame_trans_ : Lean.ParserDescr

game_trans introduces an intermediate game for transitivity of GameEquiv.

Given a goal g₁ ≡ₚ g₃, game_trans g₂ produces two subgoals:

1. g₁ ≡ₚ g₂
2. g₂ ≡ₚ g₃

This is the fundamental tactic for multi-step game-hopping chains.

def OracleComp.ProgramLogic.tacticBy_dist_ : Lean.ParserDescr

by_dist transforms a TV distance or advantage bound goal into a subgoal suitable for relational or coupling reasoning.

def OracleComp.ProgramLogic.tacticBy_upto_ : Lean.ParserDescr

by_upto bad applies the "identical until bad" TV-distance theorem for simulateQ. It leaves the standard four subgoals: initial non-bad state, agreement off bad, and bad-state monotonicity for each implementation.