Relational VC Tactics #
User-facing relational VCGen tactics and syntax.
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 / quantitative
Std.Do'.RelTriple 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, where
t : α → β → Prop - bind bijection coupling, where
t : α → αand both sides start with a uniform sample / query (the cut is inferred asfun a b => b = t a, closing the sample subgoal viarelTriple_uniformSample_bij/relTriple_query_bijand substituting the equality on the continuation) - random/query bijection, where
t : α → α - traversal input relation (
List.mapM/List.foldlM) simulateQstate relation
rvcstep left and rvcstep right expose controlled one-sided bind steps for
raw Std.Do'.rwp and folded Std.Do'.RelTriple goals. They do not run as part
of default relational automation, because choosing an asynchronous split fixes a
coupling frontier.
rvcstep sym swaps the two sides of a qualitative RelTriple goal and swaps
the relational postcondition accordingly.
rvcstep upto R changes the current qualitative postcondition to an explicit
intermediate relation R, leaving the transformed relational goal and the
postcondition implication as subgoals.
rvcstep trans mid introduces an explicit intermediate computation. It first
tries the shape oa ~ mid | EqRel _ followed by mid ~ ob | R, and then the
dual shape oa ~ mid | R followed by mid ~ ob | EqRel _.
rvcstep swap left and rvcstep swap right explicitly commute two adjacent
independent binds on one side through EqRel transport. Add using R to
immediately decompose the aligned residual bind with cut relation R.
rvcstep with thm forces one explicit relational theorem/assumption step.
Instances For
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 using [t₁, t₂, ...] applies explicit cuts in sequence, introducing and
substituting EqRel continuation equalities between cuts when present.
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.
rvcfinish runs the opt-in residual search/consequence closer.
rvcgen! runs ordinary rvcgen and then rvcfinish.
Instances For
rel_conseq weakens or strengthens the postcondition of a RelTriple goal.
Given a goal RelTriple oa ob R', applies relTriple_post_mono to produce:
RelTriple oa ob ?R— the triple with a (possibly easier) postcondition∀ x y, ?R x y → R' x y— the implication between postconditions
Use rel_conseq with R to specify the intermediate postcondition explicitly.
Instances For
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.
Instances For
Proof mode entry tactics #
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.
Instances For
game_trans introduces an intermediate game for transitivity of GameEquiv.
Given a goal g₁ ≡ₚ g₃, game_trans g₂ produces two subgoals:
g₁ ≡ₚ g₂g₂ ≡ₚ g₃
This is the fundamental tactic for multi-step game-hopping chains.
Instances For
by_dist transforms a TV distance or advantage bound goal into a subgoal
suitable for relational or coupling reasoning.
Instances For
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.