Relational program-logic baseline

This file defines RelTriple via the generic two-monad algebra interface MAlgRelOrdered, instantiated for OracleComp using coupling semantics.

HasCoupling and coupling lemmas remain as semantic bridge lemmas.

@[reducible, inline]

abbrev OracleComp.ProgramLogic.Relational.RelPost (α : Sort w) (β : Sort x) : Sort (max (max 1 w) x)

Relational postconditions over two output spaces.

def OracleComp.ProgramLogic.Relational.EqRel (α : Sort w) : RelPost α α

Equality relation helper for same-type outputs.

def OracleComp.ProgramLogic.Relational.CouplingPost {ι₁ : Type u} {ι₂ : Type v} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} [spec₁.Fintype] [spec₁.Inhabited] [spec₂.Fintype] [spec₂.Inhabited] {α β : Type} (oa : OracleComp spec₁ α) (ob : OracleComp spec₂ β) (R : RelPost α β) : Prop

Coupling-based semantic relational WP for OracleComp.

@[implicit_reducible]

noncomputable instance OracleComp.ProgramLogic.Relational.instMAlgRelOrdered {ι₁ : Type u} {ι₂ : Type v} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} [spec₁.Fintype] [spec₁.Inhabited] [spec₂.Fintype] [spec₂.Inhabited] : MAlgRelOrdered (OracleComp spec₁) (OracleComp spec₂) Prop

Relational algebra instance for OracleComp, based on coupling semantics.

instance OracleComp.ProgramLogic.Relational.instAnchored {ι₁ : Type u} {ι₂ : Type v} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} [spec₁.Fintype] [spec₁.Inhabited] [spec₂.Fintype] [spec₂.Inhabited] : MAlgRelOrdered.Anchored (OracleComp spec₁) (OracleComp spec₂) Prop

Anchoring instance for the qualitative Prop-valued relational logic on OracleComp.

When one of the two computations is pure, the relational coupling logic collapses to the unary support-based logic of the other side. This is the relational analogue of the Dirac coupling identity c (a, b) = (evalDist y) b whenever c couples pure a with y.

Together with the unary Prop algebra in VCVio/ProgramLogic/Unary/HoarePropTriple.lean, this lets wpExc / rwpExc-style honest exception combinators (in ToMathlib/Control/Monad/RelationalAlgebraAnchored.lean) be derived uniformly.

@[reducible, inline]

abbrev OracleComp.ProgramLogic.Relational.RelWP {ι₁ : Type u} {ι₂ : Type v} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} [spec₁.Fintype] [spec₁.Inhabited] [spec₂.Fintype] [spec₂.Inhabited] {α β : Type} (oa : OracleComp spec₁ α) (ob : OracleComp spec₂ β) (R : RelPost α β) : Prop

Relational weakest precondition induced by MAlgRelOrdered for OracleComp.

@[reducible, inline]

abbrev OracleComp.ProgramLogic.Relational.RelTriple {ι₁ : Type u} {ι₂ : Type v} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} [spec₁.Fintype] [spec₁.Inhabited] [spec₂.Fintype] [spec₂.Inhabited] {α β : Type} (oa : OracleComp spec₁ α) (ob : OracleComp spec₂ β) (R : RelPost α β) : Prop

Relational Hoare-style triple with implicit precondition True.

@[simp]

theorem OracleComp.ProgramLogic.Relational.relTriple_iff_relWP {ι₁ : Type u} {ι₂ : Type v} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} [spec₁.Fintype] [spec₁.Inhabited] [spec₂.Fintype] [spec₂.Inhabited] {α β : Type} {oa : OracleComp spec₁ α} {ob : OracleComp spec₂ β} {R : RelPost α β} : RelTriple oa ob R ↔ RelWP oa ob R

@[simp]

theorem OracleComp.ProgramLogic.Relational.relWP_iff_couplingPost {ι₁ : Type u} {ι₂ : Type v} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} [spec₁.Fintype] [spec₁.Inhabited] [spec₂.Fintype] [spec₂.Inhabited] {α β : Type} {oa : OracleComp spec₁ α} {ob : OracleComp spec₂ β} {R : RelPost α β} : RelWP oa ob R ↔ CouplingPost oa ob R

def OracleComp.ProgramLogic.Relational.HasCoupling {ι₁ : Type u} {ι₂ : Type v} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} [spec₁.Fintype] [spec₁.Inhabited] [spec₂.Fintype] [spec₂.Inhabited] {α β : Type} (oa : OracleComp spec₁ α) (ob : OracleComp spec₂ β) : Prop

Existence of an SPMF coupling witness between two computations.

theorem OracleComp.ProgramLogic.Relational.hasCoupling_of_relTriple {ι₁ : Type u} {ι₂ : Type v} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} [spec₁.Fintype] [spec₁.Inhabited] [spec₂.Fintype] [spec₂.Inhabited] {α β : Type} {oa : OracleComp spec₁ α} {ob : OracleComp spec₂ β} {R : RelPost α β} (h : RelTriple oa ob R) : HasCoupling oa ob

Any relational triple yields a coupling witness.

theorem OracleComp.ProgramLogic.Relational.relTriple_pure_pure {ι₁ : Type u} {ι₂ : Type v} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} [spec₁.Fintype] [spec₁.Inhabited] [spec₂.Fintype] [spec₂.Inhabited] {α β : Type} {a : α} {b : β} {R : RelPost α β} (h : R a b) : RelTriple (pure a) (pure b) R

Pure values on both sides: R a b implies the coupling.

theorem OracleComp.ProgramLogic.Relational.relTriple_refl {ι₁ : Type u} {spec₁ : OracleSpec ι₁} [spec₁.Fintype] [spec₁.Inhabited] {α : Type} (oa : OracleComp spec₁ α) : RelTriple oa oa (EqRel α)

Reflexivity rule for relational triples on equality.

theorem OracleComp.ProgramLogic.Relational.relTriple_post_mono {ι₁ : Type u} {ι₂ : Type v} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} [spec₁.Fintype] [spec₁.Inhabited] [spec₂.Fintype] [spec₂.Inhabited] {α β : Type} {oa : OracleComp spec₁ α} {ob : OracleComp spec₂ β} {R R' : RelPost α β} (h : RelTriple oa ob R) (hpost : ∀ ⦃x : α⦄ ⦃y : β⦄, R x y → R' x y) : RelTriple oa ob R'

Postcondition monotonicity for relational triples.

theorem OracleComp.ProgramLogic.Relational.relTriple_true {ι₁ : Type u} {ι₂ : Type v} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} [spec₁.Fintype] [spec₁.Inhabited] [spec₂.Fintype] [spec₂.Inhabited] {α β : Type} (oa : OracleComp spec₁ α) (ob : OracleComp spec₂ β) : RelTriple oa ob fun (x : α) (x_1 : β) => True

The trivial product coupling always exists for OracleComp, so any pair of computations satisfies the constantly-true postcondition.

The witness is the product coupling evalDist oa ⊗ evalDist ob, which is well-defined because OracleComp computations have no failure mass. This discharges any RelTriple goal whose postcondition is structurally fun _ _ => True and is the foundation of the trivial-leaf closer in tryCloseRelGoalImmediate.

theorem OracleComp.ProgramLogic.Relational.relTriple_post_const {ι₁ : Type u} {ι₂ : Type v} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} [spec₁.Fintype] [spec₁.Inhabited] [spec₂.Fintype] [spec₂.Inhabited] {α β : Type} {oa : OracleComp spec₁ α} {ob : OracleComp spec₂ β} {R : RelPost α β} (h : ∀ (a : α) (b : β), R a b) : RelTriple oa ob R

Any postcondition that is unconditionally true gives a valid relational triple, via the product coupling. Useful as a closing rule for vacuous postconditions.

theorem OracleComp.ProgramLogic.Relational.relTriple_symm {ι₁ : Type u} {ι₂ : Type v} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} [spec₁.Fintype] [spec₁.Inhabited] [spec₂.Fintype] [spec₂.Inhabited] {α β : Type} {oa : OracleComp spec₁ α} {ob : OracleComp spec₂ β} {R : RelPost α β} (h : RelTriple oa ob R) : RelTriple ob oa fun (b : β) (a : α) => R a b

Symmetry for relational triples, swapping the two computations and the postcondition.

theorem OracleComp.ProgramLogic.Relational.relTriple_of_evalDist_eq_left {ι₁ : Type u} {ι₂ : Type v} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} [spec₁.Fintype] [spec₁.Inhabited] [spec₂.Fintype] [spec₂.Inhabited] {α β : Type} {ι₃ : Type w} {spec₃ : OracleSpec ι₃} [spec₃.Fintype] [spec₃.Inhabited] {oa : OracleComp spec₁ α} {oa' : OracleComp spec₂ α} {ob : OracleComp spec₃ β} {R : RelPost α β} (heq : 𝒟[oa] = 𝒟[oa']) (h : RelTriple oa' ob R) : RelTriple oa ob R

Transport a relational triple across equality of the left output distribution.

theorem OracleComp.ProgramLogic.Relational.relTriple_of_evalDist_eq_right {ι₁ : Type u} {ι₂ : Type v} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} [spec₁.Fintype] [spec₁.Inhabited] [spec₂.Fintype] [spec₂.Inhabited] {α β : Type} {ι₃ : Type w} {spec₃ : OracleSpec ι₃} [spec₃.Fintype] [spec₃.Inhabited] {oa : OracleComp spec₁ α} {ob : OracleComp spec₂ β} {ob' : OracleComp spec₃ β} {R : RelPost α β} (heq : 𝒟[ob] = 𝒟[ob']) (h : RelTriple oa ob R) : RelTriple oa ob' R

Transport a relational triple across equality of the right output distribution.

theorem OracleComp.ProgramLogic.Relational.relTriple_bind {ι₁ : Type u} {ι₂ : Type v} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} [spec₁.Fintype] [spec₁.Inhabited] [spec₂.Fintype] [spec₂.Inhabited] {α β γ δ : Type} {oa : OracleComp spec₁ α} {ob : OracleComp spec₂ β} {fa : α → OracleComp spec₁ γ} {fb : β → OracleComp spec₂ δ} {R : RelPost α β} {S : RelPost γ δ} (hxy : RelTriple oa ob R) (hfg : ∀ (a : α) (b : β), R a b → RelTriple (fa a) (fb b) S) : RelTriple (oa >>= fa) (ob >>= fb) S

Bind composition rule for relational triples.

theorem OracleComp.ProgramLogic.Relational.relTriple_eqRel_of_eq {ι₁ : Type u} {spec₁ : OracleSpec ι₁} [spec₁.Fintype] [spec₁.Inhabited] {α : Type} {oa ob : OracleComp spec₁ α} (h : oa = ob) : RelTriple oa ob (EqRel α)

Equality of programs gives an equality-relation relational triple.

theorem OracleComp.ProgramLogic.Relational.relTriple_eqRel_of_evalDist_eq {ι₁ : Type u} {ι₂ : Type v} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} [spec₁.Fintype] [spec₁.Inhabited] [spec₂.Fintype] [spec₂.Inhabited] {α : Type} {oa : OracleComp spec₁ α} {ob : OracleComp spec₂ α} (h : 𝒟[oa] = 𝒟[ob]) : RelTriple oa ob (EqRel α)

Equality of evaluation distributions gives an equality-relation relational triple.

theorem OracleComp.ProgramLogic.Relational.relTriple_of_evalDist_eq {ι₁ : Type u} {ι₂ : Type v} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} [spec₁.Fintype] [spec₁.Inhabited] [spec₂.Fintype] [spec₂.Inhabited] {α : Type} {oa : OracleComp spec₁ α} {ob : OracleComp spec₂ α} {R : RelPost α α} (h : 𝒟[oa] = 𝒟[ob]) (hR : ∀ (x : α), R x x) : RelTriple oa ob R

If two computations have equal output distributions, any reflexive postcondition holds.

theorem OracleComp.ProgramLogic.Relational.relTriple_eqRel_of_probOutput_eq {ι₁ : Type u} {ι₂ : Type v} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} [spec₁.Fintype] [spec₁.Inhabited] [spec₂.Fintype] [spec₂.Inhabited] {α : Type} {oa : OracleComp spec₁ α} {ob : OracleComp spec₂ α} (h : ∀ (x : α), Pr[= x | oa] = Pr[= x | ob]) : RelTriple oa ob (EqRel α)

Pointwise output-probability equality gives an equality-relation relational triple.

theorem OracleComp.ProgramLogic.Relational.relTriple_bind_bind_swap_eqRel {ι₁ : Type u} {spec₁ : OracleSpec ι₁} [spec₁.Fintype] [spec₁.Inhabited] {α β γ : Type} {oa : OracleComp spec₁ α} {ob : OracleComp spec₁ β} {f : α → β → OracleComp spec₁ γ} : RelTriple (do let a ← oa let b ← ob f a b) (do let b ← ob let a ← oa f a b) (EqRel γ)

Swapping two adjacent independent binds preserves the output distribution.

theorem OracleComp.ProgramLogic.Relational.probOutput_eq_of_relTriple_eqRel {ι₁ : Type u} {ι₂ : Type v} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} [spec₁.Fintype] [spec₁.Inhabited] [spec₂.Fintype] [spec₂.Inhabited] {α : Type} {oa : OracleComp spec₁ α} {ob : OracleComp spec₂ α} (h : RelTriple oa ob (EqRel α)) (x : α) : Pr[= x | oa] = Pr[= x | ob]

Equality-relation relational triples imply equality of point output probabilities.

theorem OracleComp.ProgramLogic.Relational.evalDist_eq_of_relTriple_eqRel {ι₁ : Type u} {ι₂ : Type v} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} [spec₁.Fintype] [spec₁.Inhabited] [spec₂.Fintype] [spec₂.Inhabited] {α : Type} {oa : OracleComp spec₁ α} {ob : OracleComp spec₂ α} (h : RelTriple oa ob (EqRel α)) : 𝒟[oa] = 𝒟[ob]

Equality-relation relational triples imply equality of evaluation distributions.

theorem OracleComp.ProgramLogic.Relational.relTriple_trans_eqRel_left {ι₁ : Type u} {ι₂ : Type v} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} [spec₁.Fintype] [spec₁.Inhabited] [spec₂.Fintype] [spec₂.Inhabited] {α β : Type} {ι₃ : Type w} {spec₃ : OracleSpec ι₃} [spec₃.Fintype] [spec₃.Inhabited] {oa : OracleComp spec₁ α} {mid : OracleComp spec₂ α} {ob : OracleComp spec₃ β} {R : RelPost α β} (hleft : RelTriple oa mid (EqRel α)) (hright : RelTriple mid ob R) : RelTriple oa ob R

Transitivity through an intermediate computation related to the left side by EqRel.

theorem OracleComp.ProgramLogic.Relational.relTriple_trans_eqRel_right {ι₁ : Type u} {ι₂ : Type v} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} [spec₁.Fintype] [spec₁.Inhabited] [spec₂.Fintype] [spec₂.Inhabited] {α β : Type} {ι₃ : Type w} {spec₃ : OracleSpec ι₃} [spec₃.Fintype] [spec₃.Inhabited] {oa : OracleComp spec₁ α} {mid : OracleComp spec₂ β} {ob : OracleComp spec₃ β} {R : RelPost α β} (hleft : RelTriple oa mid R) (hright : RelTriple mid ob (EqRel β)) : RelTriple oa ob R

Transitivity through an intermediate computation related to the right side by EqRel.

theorem OracleComp.ProgramLogic.Relational.relTriple_trans_eqRel {ι₁ : Type u} {ι₂ : Type v} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} [spec₁.Fintype] [spec₁.Inhabited] [spec₂.Fintype] [spec₂.Inhabited] {α : Type} {ι₃ : Type w} {spec₃ : OracleSpec ι₃} [spec₃.Fintype] [spec₃.Inhabited] {oa : OracleComp spec₁ α} {mid : OracleComp spec₂ α} {ob : OracleComp spec₃ α} (hleft : RelTriple oa mid (EqRel α)) (hright : RelTriple mid ob (EqRel α)) : RelTriple oa ob (EqRel α)

Transitivity of equality-relation relational triples through an intermediate computation.

theorem OracleComp.ProgramLogic.Relational.probOutput_true_eq_of_relTriple_eqRel {ι₁ : Type u} {ι₂ : Type v} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} [spec₁.Fintype] [spec₁.Inhabited] [spec₂.Fintype] [spec₂.Inhabited] {oa : OracleComp spec₁ Bool} {ob : OracleComp spec₂ Bool} (h : RelTriple oa ob (EqRel Bool)) : Pr[= true | oa] = Pr[= true | ob]

Bool-specialized bridge from relational triples to game success equality.

Oracle query coupling rules (pRHL level)

theorem OracleComp.ProgramLogic.Relational.relTriple_query {ι₁ : Type u} {spec₁ : OracleSpec ι₁} [spec₁.Fintype] [spec₁.Inhabited] (t : spec₁.Domain) : RelTriple (liftM (OracleSpec.query t)) (liftM (OracleSpec.query t)) (EqRel (spec₁.Range t))

Same-type identity coupling: querying the same oracle on both sides yields equal outputs.

theorem OracleComp.ProgramLogic.Relational.relTriple_query_bij {ι₁ : Type u} {spec₁ : OracleSpec ι₁} [spec₁.Fintype] [spec₁.Inhabited] (t : spec₁.Domain) {f : spec₁.Range t → spec₁.Range t} (hf : Function.Bijective f) : RelTriple (liftM (OracleSpec.query t)) (liftM (OracleSpec.query t)) fun (a b : spec₁.Range t) => f a = b

Bijection coupling (the "rnd" rule from EasyCrypt): querying the same oracle on both sides, related by a bijection f.

theorem OracleComp.ProgramLogic.Relational.relTriple_bind_query_bij {ι₁ : Type u} {spec₁ : OracleSpec ι₁} [spec₁.Fintype] [spec₁.Inhabited] {γ δ : Type} (t : spec₁.Domain) {f : spec₁.Range t → spec₁.Range t} {fa : spec₁.Range t → OracleComp spec₁ γ} {fb : spec₁.Range t → OracleComp spec₁ δ} {S : RelPost γ δ} (hfg : ∀ (a : spec₁.Range t), RelTriple (fa a) (fb (f a)) S) (hf : Function.Bijective f) : RelTriple (liftM (OracleSpec.query t) >>= fa) (liftM (OracleSpec.query t) >>= fb) S

Bind rule specialized to two equal oracle queries coupled by a bijection.

The continuation is stated over the left sample only, with the right sample already rewritten to f a. This is the stable continuation shape used by the relational tactic for unary bijection hints.

theorem OracleComp.ProgramLogic.Relational.relTriple_map {ι₁ : Type u} {ι₂ : Type v} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} [spec₁.Fintype] [spec₁.Inhabited] [spec₂.Fintype] [spec₂.Inhabited] {α β γ δ : Type} {R : RelPost γ δ} {f : α → γ} {g : β → δ} {oa : OracleComp spec₁ α} {ob : OracleComp spec₂ β} (h : RelTriple oa ob fun (a : α) (b : β) => R (f a) (g b)) : RelTriple (f <$> oa) (g <$> ob) R

theorem OracleComp.ProgramLogic.Relational.evalDist_map_eq_of_relTriple {ι₁ : Type u} {ι₂ : Type v} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} [spec₁.Fintype] [spec₁.Inhabited] [spec₂.Fintype] [spec₂.Inhabited] {α β σ : Type} {f : α → σ} {g : β → σ} {oa : OracleComp spec₁ α} {ob : OracleComp spec₂ β} (h : RelTriple oa ob fun (a : α) (b : β) => f a = g b) : 𝒟[f <$> oa] = 𝒟[g <$> ob]

If a relational triple holds for fun a b => f a = g b, then mapping by f and g produces equal distributions. Generalizes evalDist_eq_of_relTriple_eqRel.

theorem OracleComp.ProgramLogic.Relational.relTriple_replicate {ι₁ : Type u} {ι₂ : Type v} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} [spec₁.Fintype] [spec₁.Inhabited] [spec₂.Fintype] [spec₂.Inhabited] {α β : Type} {oa : OracleComp spec₁ α} {ob : OracleComp spec₂ β} {R : RelPost α β} (n : ℕ) (hstep : RelTriple oa ob R) : RelTriple (replicate n oa) (replicate n ob) (List.Forall₂ R)

Lift a one-step coupling through bounded iteration.

theorem OracleComp.ProgramLogic.Relational.relTriple_replicate_eqRel {ι₁ : Type u} {spec₁ : OracleSpec ι₁} [spec₁.Fintype] [spec₁.Inhabited] {α : Type} {oa ob : OracleComp spec₁ α} (n : ℕ) (hstep : RelTriple oa ob (EqRel α)) : RelTriple (replicate n oa) (replicate n ob) (EqRel (List α))

Equality coupling version of relTriple_replicate.

theorem OracleComp.ProgramLogic.Relational.relTriple_list_mapM {ι₁ : Type u} {ι₂ : Type v} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} [spec₁.Fintype] [spec₁.Inhabited] [spec₂.Fintype] [spec₂.Inhabited] {α β γ δ : Type} {xs : List α} {ys : List β} {f : α → OracleComp spec₁ γ} {g : β → OracleComp spec₂ δ} {Rin : α → β → Prop} {Rout : γ → δ → Prop} (hxy : List.Forall₂ Rin xs ys) (hfg : ∀ (a : α) (b : β), Rin a b → RelTriple (f a) (g b) Rout) : RelTriple (List.mapM f xs) (List.mapM g ys) (List.Forall₂ Rout)

Lift pointwise relational reasoning through finite list traversals.

theorem OracleComp.ProgramLogic.Relational.relTriple_list_mapM_eqRel {ι₁ : Type u} {ι₂ : Type v} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} [spec₁.Fintype] [spec₁.Inhabited] [spec₂.Fintype] [spec₂.Inhabited] {α β : Type} {xs : List α} {f : α → OracleComp spec₁ β} {g : α → OracleComp spec₂ β} (hfg : ∀ (a : α), RelTriple (f a) (g a) (EqRel β)) : RelTriple (List.mapM f xs) (List.mapM g xs) (EqRel (List β))

Same-input equality-coupling specialization of relTriple_list_mapM.

theorem OracleComp.ProgramLogic.Relational.relTriple_list_foldlM {ι₁ : Type u} {ι₂ : Type v} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} [spec₁.Fintype] [spec₁.Inhabited] [spec₂.Fintype] [spec₂.Inhabited] {α β σ₁ σ₂ : Type} {xs : List α} {ys : List β} {f : σ₁ → α → OracleComp spec₁ σ₁} {g : σ₂ → β → OracleComp spec₂ σ₂} {Rin : α → β → Prop} {S : σ₁ → σ₂ → Prop} {s₁ : σ₁} {s₂ : σ₂} (hs : S s₁ s₂) (hxy : List.Forall₂ Rin xs ys) (hfg : ∀ (a : α) (b : β), Rin a b → ∀ (t₁ : σ₁) (t₂ : σ₂), S t₁ t₂ → RelTriple (f t₁ a) (g t₂ b) S) : RelTriple (List.foldlM f s₁ xs) (List.foldlM g s₂ ys) S

Loop-invariant rule for bounded left folds over related input lists.

theorem OracleComp.ProgramLogic.Relational.relTriple_list_foldlM_same {ι₁ : Type u} {ι₂ : Type v} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} [spec₁.Fintype] [spec₁.Inhabited] [spec₂.Fintype] [spec₂.Inhabited] {α σ₁ σ₂ : Type} {xs : List α} {f : σ₁ → α → OracleComp spec₁ σ₁} {g : σ₂ → α → OracleComp spec₂ σ₂} {S : σ₁ → σ₂ → Prop} {s₁ : σ₁} {s₂ : σ₂} (hs : S s₁ s₂) (hfg : ∀ (a : α) (t₁ : σ₁) (t₂ : σ₂), S t₁ t₂ → RelTriple (f t₁ a) (g t₂ a) S) : RelTriple (List.foldlM f s₁ xs) (List.foldlM g s₂ xs) S

Same-input specialization of relTriple_list_foldlM.

Synchronized branching rule

theorem OracleComp.ProgramLogic.Relational.relTriple_if {ι₁ : Type u} {ι₂ : Type v} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} [spec₁.Fintype] [spec₁.Inhabited] [spec₂.Fintype] [spec₂.Inhabited] {α β : Type} {c : Prop} [Decidable c] {oa₁ oa₂ : OracleComp spec₁ α} {ob₁ ob₂ : OracleComp spec₂ β} {R : RelPost α β} (htrue : c → RelTriple oa₁ ob₁ R) (hfalse : ¬c → RelTriple oa₂ ob₂ R) : RelTriple (if c then oa₁ else oa₂) (if c then ob₁ else ob₂) R

Synchronized conditional: if both sides branch on the same condition, the relational triple holds if it holds on both branches.

theorem OracleComp.ProgramLogic.Relational.relTriple_pure_left {ι₁ : Type u} {ι₂ : Type v} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} [spec₁.Fintype] [spec₁.Inhabited] [spec₂.Fintype] [spec₂.Inhabited] {α β : Type} {a : α} {ob : OracleComp spec₂ β} {R : RelPost α β} (h : RelTriple (pure a) ob fun (x : α) (y : β) => x = a ∧ R x y) : RelTriple (pure a) ob R

Pure-left rule: the left side is a pure value, applied via bind decomposition.

theorem OracleComp.ProgramLogic.Relational.relTriple_pure_right {ι₁ : Type u} {ι₂ : Type v} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} [spec₁.Fintype] [spec₁.Inhabited] [spec₂.Fintype] [spec₂.Inhabited] {α β : Type} {oa : OracleComp spec₁ α} {b : β} {R : RelPost α β} (h : RelTriple oa (pure b) fun (x : α) (y : β) => y = b ∧ R x y) : RelTriple oa (pure b) R

Pure-right rule: the right side is a pure value, applied via bind decomposition.

theorem OracleComp.ProgramLogic.Relational.relTriple_uniformSample_bij {α : Type} [SampleableType α] {f : α → α} (hf : Function.Bijective f) (R : RelPost α α) (hR : ∀ (x : α), R x (f x)) : RelTriple ($ᵗ α) ($ᵗ α) R

Relational coupling for uniform sampling via bijection. Given a bijection f : α → α such that R x (f x) for all x, the two uniform samples are related by R.

theorem OracleComp.ProgramLogic.Relational.relTriple_bind_uniformSample_bij {α γ δ : Type} [SampleableType α] {f : α → α} {fa : α → ProbComp γ} {fb : α → ProbComp δ} {S : RelPost γ δ} (hfg : ∀ (a : α), RelTriple (fa a) (fb (f a)) S) (hf : Function.Bijective f) : RelTriple ($ᵗ α >>= fa) ($ᵗ α >>= fb) S

Bind rule specialized to two uniform samples coupled by a bijection.

The continuation is stated over the left sample only, with the right sample already rewritten to f a. This avoids exposing an auxiliary equality witness to proof scripts after rvcstep using f.

theorem OracleComp.ProgramLogic.Relational.relTriple_uniformSample_refl {α : Type} [SampleableType α] : RelTriple ($ᵗ α) ($ᵗ α) (EqRel α)

Identity coupling for uniform sampling.