Coupling introduction for relE (the symmetric proof principle)

A relE judgment is two rel directions, and for asymmetric coupling relations the two directions are not logically interderivable — proving them separately duplicates the whole case analysis (the "mirror tax" measured in the up-to-bad client).

This module provides the missing symmetric introduction form: an explicit coupling witness — a joint subdistribution over output pairs whose marginals are the two runs and whose support lies in the post — yields both directions at once (ProgramDenotation.relE.of_coupling). This is the CertiCrypt/FCF lifting, deliberately confined to its sweet spot:

• leaves are proved by exhibiting a coupling (Coupling.of_pure for deterministic steps, Coupling.of_uniform for synchronized sampling — the closed wp forms required as inputs are exactly what the wp-style proofs compute anyway, now stated once instead of once per direction);
• composition stays with the wp-lifting rules (relE.bind, relE.loop_n, …), which need no couplings, no measurability, and no choice principles.

structure GaudisCrypt.ProgramDenotation.Coupling {s₁ s₂ α β : Type} (p : ProgramDenotation s₁ α) (q : ProgramDenotation s₂ β) (σ₁ : s₁) (σ₂ : s₂) (Post : α × s₁ → β × s₂ → Prop) : Type

A coupling witness for the runs p from σ₁ and q from σ₂: a joint subdistribution on output pairs with the two runs as marginals and support inside Post (stated in CertiCrypt's range form, which needs no decidability).

• w : SubProbability ((α × s₁) × β × s₂)

  The joint subdistribution.

• marg₁ (F : α × s₁ → ENNReal) : (self.w.expected fun (uv : (α × s₁) × β × s₂) => F uv.1) = p.wp F σ₁

  Left marginal: integrating a left-post recovers p's run.

• marg₂ (G : β × s₂ → ENNReal) : (self.w.expected fun (uv : (α × s₁) × β × s₂) => G uv.2) = q.wp G σ₂

  Right marginal.

• supp (f : (α × s₁) × β × s₂ → ENNReal) : (∀ (uv : (α × s₁) × β × s₂), Post uv.1 uv.2 → f uv = 0) → self.w.expected f = 0

  Support condition: any function vanishing on Post integrates to 0.

Expected-value helpers

theorem GaudisCrypt.SubProbability.expected_mono_pt {γ : Type} (μ : SubProbability γ) {f g : γ → ENNReal} (h : ∀ (x : γ), f x ≤ g x) : μ.expected f ≤ μ.expected g

theorem GaudisCrypt.SubProbability.expected_add {γ : Type} (μ : SubProbability γ) (f g : γ → ENNReal) : (μ.expected fun (x : γ) => f x + g x) = μ.expected f + μ.expected g

theorem GaudisCrypt.SubProbability.expected_zero {γ : Type} (μ : SubProbability γ) : (μ.expected fun (x : γ) => 0) = 0

Expected value of the constant-zero post.

theorem GaudisCrypt.SubProbability.expected_bot {γ : Type} (f : γ → ENNReal) : ⊥.expected f = 0

Expected value over the zero subdistribution.

theorem GaudisCrypt.SubProbability.expected_congr {γ : Type} (μ : SubProbability γ) {f g : γ → ENNReal} (h : ∀ (x : γ), f x = g x) : μ.expected f = μ.expected g

Pointwise congruence for expected.

theorem GaudisCrypt.sum_const_div_card {T : Type} [Fintype T] [Nonempty T] (c : ENNReal) : ∑ _t : T, c / ↑(Fintype.card T) = c

Collapse a constant average.

theorem GaudisCrypt.ProgramDenotation.Coupling.expected_le {s₁ s₂ α β : Type} {p : ProgramDenotation s₁ α} {q : ProgramDenotation s₂ β} {σ₁ : s₁} {σ₂ : s₂} {Post : α × s₁ → β × s₂ → Prop} (c : p.Coupling q σ₁ σ₂ Post) {A B : (α × s₁) × β × s₂ → ENNReal} (hAB : ∀ (uv : (α × s₁) × β × s₂), Post uv.1 uv.2 → A uv ≤ B uv) : c.w.expected A ≤ c.w.expected B

Domination through the witness: a Post-pointwise inequality between pair-posts integrates.

noncomputable def GaudisCrypt.ProgramDenotation.Coupling.of_pure {s₁ s₂ α β : Type} {p : ProgramDenotation s₁ α} {q : ProgramDenotation s₂ β} {σ₁ : s₁} {σ₂ : s₂} {Post : α × s₁ → β × s₂ → Prop} (u₀ : α × s₁) (v₀ : β × s₂) (h₁ : ∀ (F : ProgramDenotation.Post s₁ α), p.wp F σ₁ = F u₀) (h₂ : ∀ (G : ProgramDenotation.Post s₂ β), q.wp G σ₂ = G v₀) (hP : Post u₀ v₀) : p.Coupling q σ₁ σ₂ Post

Deterministic coupling: both runs are point masses on a Post-related pair of outputs.

Equations

• GaudisCrypt.ProgramDenotation.Coupling.of_pure u₀ v₀ h₁ h₂ hP = { w := pure (u₀, v₀), marg₁ := ⋯, marg₂ := ⋯, supp := ⋯ }

noncomputable def GaudisCrypt.ProgramDenotation.Coupling.of_uniform {s₁ s₂ α β : Type} {p : ProgramDenotation s₁ α} {q : ProgramDenotation s₂ β} {σ₁ : s₁} {σ₂ : s₂} {Post : α × s₁ → β × s₂ → Prop} {T : Type} [Fintype T] [Nonempty T] (f₁ : T → α × s₁) (f₂ : T → β × s₂) (h₁ : ∀ (F : ProgramDenotation.Post s₁ α), p.wp F σ₁ = ∑ t : T, F (f₁ t) / ↑(Fintype.card T)) (h₂ : ∀ (G : ProgramDenotation.Post s₂ β), q.wp G σ₂ = ∑ t : T, G (f₂ t) / ↑(Fintype.card T)) (hP : ∀ (t : T), Post (f₁ t) (f₂ t)) : p.Coupling q σ₁ σ₂ Post

Sampling coupling along a shared index (the rnd rule with an explicit branch matching): both runs are uniform averages over T, coupled branch-by-branch.

Equations

• GaudisCrypt.ProgramDenotation.Coupling.of_uniform f₁ f₂ h₁ h₂ hP = { w := do let t ← GaudisCrypt.SubProbability.uniform pure (f₁ t, f₂ t), marg₁ := ⋯, marg₂ := ⋯, supp := ⋯ }

theorem GaudisCrypt.ProgramDenotation.relE.of_coupling {s₁ s₂ α β : Type} {p : ProgramDenotation s₁ α} {q : ProgramDenotation s₂ β} {Pre : s₁ → s₂ → Prop} {Post : α × s₁ → β × s₂ → Prop} (h : (σ₁ : s₁) → (σ₂ : s₂) → Pre σ₁ σ₂ → p.Coupling q σ₁ σ₂ Post) : p.relE q Pre Post

Coupling introduction (the symmetric proof principle): a coupling witness at every Pre-related state pair yields the full two-sided relE judgment — both directions from the same witness.