Relational VCGen Internals #
Implementation details for the relational VCGen planner and step selection.
Registered VC-spec rules #
Centralized @[vcspec] registrations for the relational planner. Lemmas added here become
candidates for the registered-rule branch of rvcstep/rvcgen (and surface in the
"Registered @[vcspec] candidates" hint when the planner gets stuck), in addition to any
structural rule that runRVCGenCore already tries by goal shape.
Attempt to close the current relational/eRHL leaf goal with the canonical fast paths.
Tries, in order:
assumption(catches a hypothesis matching the relational triple verbatim);- quantitative
Std.Do'.RelTriplepure-pure leaves; relTriple_refl(identical computations, equality coupling);relTriple_eqRel_of_eq rfl(syntactically identical computations);relTriple_pure_pure rfl(pure x ⨯ pure xwith reflexive postcondition);relTriple_pure_puretogether withassumption(pure a ⨯ pure bwithR a bin scope);- a small proof-search variant of
relTriple_pure_pureusingrfl,assumption, or a symmetric assumption for the value-level relation; - the same closers after
subst_vars(resolves goals where the pure values are syntactically distinct but unified via local equality hypotheses); relTriple_true _ _/relTriple_post_constonly when the postcondition has first been classified as vacuous.
The vacuous-postcondition rules are intentionally last and guarded. Applying them blindly to non-vacuous pure leaves can create expensive failed elaboration attempts and obscure the predictable pure/reflexive close path.
Instances For
Normalize the monad structure of both sides of a relational/eRHL goal.
Applies the standard set of monad simplification lemmas (right-association, pure-bind
elimination, bind_pure_comp, Functor.map_map, map_pure) to flatten nested binds
and strip pure-bind layers so that downstream rule selection (especially
relTriple_bind) sees aligned structures on both sides. The pass is best-effort:
try simp only always succeeds and leaves the goal unchanged when no lemma applies.
Instances For
Instances For
Monad-law normalization used as a fallback when a direct relTriple_bind
attempt fails. Flattens nested binds (bind_assoc) and reduces pure_bind so
that commit-style intermediate computations (e.g. do x ← oa; pure (x, x))
align with the corresponding flat form on the other side.
Instances For
After relTriple_bind ?_ ?_ produces [sample, continuation, …pre-existing],
this helper tries to auto-close the sample subgoal (typically RelTriple oa oa (EqRel _) closes via relTriple_refl) and the continuation subgoal in isolation,
then puts any unclosed continuation first for the user's natural intro-style flow.
Pre-existing goals (those already in the goal list before relTriple_bind produced
the two new subgoals at the head) are preserved unchanged at the tail; the helper
never touches or reorders them. This guards against the multi-goal scenario where
rvcstep is invoked on a goal sitting alongside other open goals (for example,
after constructor): a naive close-then-swap would, when the sample closes,
swap the continuation with an unrelated trailing goal, and a follow-up close pass
could fire on it.
Instances For
Bijection-coupling interpretation of an rvcstep using f hint when both sides
of a bind start with a uniform sample / query.
Given a goal RelTriple ((⋯ : OracleComp _ α) >>= fa) ((⋯ : OracleComp _ α) >>= fb) S,
applies a specialized bind-bijection rule when possible. The continuation then
mentions only the left sample, with the right sample already rewritten to f a.
Resulting goal order:
- The continuation
RelTriple (fa a) (fb (f a)) Sfor an arbitrary fresha. - The bijectivity side condition
Function.Bijective f. - Any prior trailing goals.
Returns true iff every step of the recipe fired; otherwise restores state and
returns false so a caller can try a different interpretation of the hint.
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Controlled one-sided relational bind step on the left.
Instances For
Controlled one-sided relational bind step on the right.
Instances For
Instances For
Find the local hypotheses that work as relational using hints.
Instances For
Find the unique local hypothesis that works as a relational using hint.
Returns none if there are 0 or ≥ 2 viable hints (keeping ambiguity explicit).
Instances For
Instances For
Try to close a relational goal by applying postcondition monotonicity and closing both the inner triple and the implication from local hypotheses.
Instances For
Instances For
Apply an explicit relational theorem/assumption step and try to close any easy side goals.
Instances For
Find default-safe registered relational @[vcspec] entries whose bounded
application makes progress on the current goal. This uses direct
discrimination-tree hits only; broad fallback/search tiers are reserved for
rvcfinish / rvcgen!.
Instances For
Structural/default relational VCGen step, excluding explicit using-hint fallbacks.
Instances For
Choose one relational VCGen step and remember how to replay it explicitly.
Instances For
Execute one planned relational VCGen step, returning the chosen step for replay/trace.
Instances For
One step of relational VCGen.