Lifting unary Std.Do triples to relational couplings

Two OracleComp computations that are independently correct (each satisfying a unary Std.Do.Triple) can always be paired via the product coupling, since every OracleComp distribution sums to probability 1 (HasEvalPMF).

This file provides the "unary → relational" bridge:

• relTriple_prod_of_wpProp — two unary wpProp witnesses give a relational triple on the product postcondition.
• relTriple_prod_of_triple — same statement, phrased directly in terms of Std.Do.Triple.
• relTriple_prod — a slightly stronger variant taking support-style postconditions.

These lemmas let proofs established against the stateful Std.Do/mvcgen proof mode be composed into relational arguments (e.g. game-hopping reductions) without redoing the underlying analysis.

theorem OracleComp.ProgramLogic.Relational.relTriple_prod {ι₁ ι₂ : Type u} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} [spec₁.Fintype] [spec₁.Inhabited] [spec₂.Fintype] [spec₂.Inhabited] {α β : Type} {oa : OracleComp spec₁ α} {ob : OracleComp spec₂ β} {P : α → Prop} {Q : β → Prop} (hP : ∀ a ∈ support oa, P a) (hQ : ∀ b ∈ support ob, Q b) : RelTriple oa ob fun (a : α) (b : β) => P a ∧ Q b

Core lift: two support-style unary postconditions combine into a relational coupling. The product coupling evalDist oa ⊗ evalDist ob witnesses the conjunction, using HasEvalPMF to ensure neither side has failure mass.

theorem OracleComp.ProgramLogic.Relational.relTriple_prod_of_wpProp {ι₁ ι₂ : Type u} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} [spec₁.Fintype] [spec₁.Inhabited] [spec₂.Fintype] [spec₂.Inhabited] {α β : Type} {oa : OracleComp spec₁ α} {ob : OracleComp spec₂ β} {P : α → Prop} {Q : β → Prop} (hP : StdDo.wpProp oa P) (hQ : StdDo.wpProp ob Q) : RelTriple oa ob fun (a : α) (b : β) => P a ∧ Q b

wpProp-phrased version of the product lift.

theorem OracleComp.ProgramLogic.Relational.relTriple_prod_of_triple {ι₁ ι₂ : Type u} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} [spec₁.Fintype] [spec₁.Inhabited] [spec₂.Fintype] [spec₂.Inhabited] {α β : Type} {oa : OracleComp spec₁ α} {ob : OracleComp spec₂ β} {P : α → Prop} {Q : β → Prop} (hP : ⦃⌜True⌝⦄ oa ⦃Std.Do.PostCond.noThrow fun (a : α) => ⌜P a⌝⦄) (hQ : ⦃⌜True⌝⦄ ob ⦃Std.Do.PostCond.noThrow fun (b : β) => ⌜Q b⌝⦄) : RelTriple oa ob fun (a : α) (b : β) => P a ∧ Q b

Std.Do.Triple-phrased version of the product lift. Two independent Std.Do triples with pure precondition True combine into a RelTriple over the product postcondition.

theorem OracleComp.ProgramLogic.Relational.relTriple_of_triple_of_imp {ι₁ ι₂ : Type u} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} [spec₁.Fintype] [spec₁.Inhabited] [spec₂.Fintype] [spec₂.Inhabited] {α β : Type} {oa : OracleComp spec₁ α} {ob : OracleComp spec₂ β} {P : α → Prop} {Q : β → Prop} {R : RelPost α β} (hP : ⦃⌜True⌝⦄ oa ⦃Std.Do.PostCond.noThrow fun (a : α) => ⌜P a⌝⦄) (hQ : ⦃⌜True⌝⦄ ob ⦃Std.Do.PostCond.noThrow fun (b : β) => ⌜Q b⌝⦄) (hImp : ∀ (a : α) (b : β), P a → Q b → R a b) : RelTriple oa ob R

Relational triples are monotone in the postcondition, so a product coupling can be weakened to any relation implied by the conjunction of independent postconditions.

Smoke tests