Couplings

This file defines couplings of sub-distributions and the lifting operation that is fundamental to probabilistic relational Hoare logic.

Main definitions

• Coupling d₁ d₂ - A coupling of two sub-distributions
• Coupling.satisfies - A coupling satisfies a relation
• liftR R d₁ d₂ - Relation R lifts to distributions (there exists a coupling satisfying R)

Main results

• liftR_refl - Equality lifts to any distribution (diagonal coupling)
• liftR_mono - Lifting is monotone in the relation
• liftR_bind - Lifting composes through bind (key for bind rule)

References

• Probabilistic couplings in verification
• SSProve: theories/Crypt/rhl_semantics/only_prob/Couplings.v

Coupling definition

structure CatCrypt.Prob.Coupling {α : Type u_1} {β : Type u_2} (d₁ : SDistr α) (d₂ : SDistr β) : Type (max u_1 u_2)

A coupling of two sub-distributions. The joint distribution has the correct marginals.

• joint : SDistr (α × β)

  The joint distribution

• left_marginal (a : α) : (self.joint.bind fun (p : α × β) => SDistr.pure p.1) (some a) = d₁ (some a)

  Left marginal condition: projecting gives d₁

• right_marginal (b : β) : (self.joint.bind fun (p : α × β) => SDistr.pure p.2) (some b) = d₂ (some b)

  Right marginal condition: projecting gives d₂

def CatCrypt.Prob.Coupling.satisfies {α : Type u_1} {β : Type u_2} {d₁ : SDistr α} {d₂ : SDistr β} (c : Coupling d₁ d₂) (R : α → β → Prop) : Prop

A coupling satisfies relation R if all coupled pairs satisfy R

Equations

• c.satisfies R = ∀ (a : α) (b : β), c.joint (some (a, b)) ≠ 0 → R a b

theorem CatCrypt.Prob.Coupling.in_left_support {α : Type u_1} {β : Type u_2} {d₁ : SDistr α} {d₂ : SDistr β} (c : Coupling d₁ d₂) {a : α} {b : β} (h : c.joint (some (a, b)) ≠ 0) : d₁ (some a) ≠ 0

If (a, b) has nonzero joint mass, then a has nonzero left marginal mass.

Proof: By the left marginal condition, d₁ (some a) = ∑' b', joint (some (a, b')) (modulo encoding). Since joint (some (a, b)) ≠ 0, the sum is nonzero.

theorem CatCrypt.Prob.Coupling.in_right_support {α : Type u_1} {β : Type u_2} {d₁ : SDistr α} {d₂ : SDistr β} (c : Coupling d₁ d₂) {a : α} {b : β} (h : c.joint (some (a, b)) ≠ 0) : d₂ (some b) ≠ 0

If (a, b) has nonzero joint mass, then b has nonzero right marginal mass.

Lifting relation to distributions

def CatCrypt.Prob.liftR {α : Type u_1} {β : Type u_2} (R : α → β → Prop) (d₁ : SDistr α) (d₂ : SDistr β) : Prop

Lifting: relation R lifts from values to distributions if there exists a coupling where all coupled pairs satisfy R.

Equations

• (d₁ ⟨R⟩# d₂) = ∃ (c : CatCrypt.Prob.Coupling d₁ d₂), c.satisfies R

def CatCrypt.Prob.«term_⟨_⟩#_» : Lean.TrailingParserDescr

Notation for lifting

Equations

• One or more equations did not get rendered due to their size.

Standard coupling constructions

noncomputable def CatCrypt.Prob.Coupling.diagonal {α : Type u_1} (d : SDistr α) : Coupling d d

Diagonal/identity coupling: couple each element with itself

Equations

• CatCrypt.Prob.Coupling.diagonal d = { joint := d.bind fun (a : α) => CatCrypt.Prob.SDistr.pure (a, a), left_marginal := ⋯, right_marginal := ⋯ }

noncomputable def CatCrypt.Prob.Coupling.fromBij {α : Type u_1} {β : Type u_2} (d : SDistr α) (f : α ≃ β) : Coupling d (d.bind fun (a : α) => SDistr.pure (f a))

Bijection coupling: couple a with f(a)

Equations

• CatCrypt.Prob.Coupling.fromBij d f = { joint := d.bind fun (a : α) => CatCrypt.Prob.SDistr.pure (a, f a), left_marginal := ⋯, right_marginal := ⋯ }

Key lifting lemmas

theorem CatCrypt.Prob.liftR_refl {α : Type u_1} (d : SDistr α) : d ⟨Eq⟩# d

Reflexivity: equality always lifts (via diagonal coupling)

theorem CatCrypt.Prob.liftR_mono {α : Type u_1} {β : Type u_2} {R S : α → β → Prop} {d₁ : SDistr α} {d₂ : SDistr β} (hRS : ∀ (a : α) (b : β), R a b → S a b) (h : d₁ ⟨R⟩# d₂) : d₁ ⟨S⟩# d₂

Monotonicity: if R ⊆ S and R lifts, then S lifts

theorem CatCrypt.Prob.liftR_symm {α : Type u_1} {β : Type u_2} {R : α → β → Prop} {d₁ : SDistr α} {d₂ : SDistr β} (h : d₁ ⟨R⟩# d₂) : d₂ ⟨fun (b : β) (a : α) => R a b⟩# d₁

Symmetry: if R lifts, then R⁻¹ lifts with swapped distributions

Marginal sum lemmas

theorem CatCrypt.Prob.SDistr.mass_one_implies_none_zero {α : Type u_1} {d : SDistr α} (h : d.mass = 1) : d none = 0

If mass d = 1, then d none = 0

theorem CatCrypt.Prob.SDistr.bind_const_mass_one {α : Type u_1} {β : Type u_2} {d : SDistr α} {e : SDistr β} (h : d.mass = 1) : (d.bind fun (x : α) => e) = e

Binding with a constant (when mass = 1)

noncomputable def CatCrypt.Prob.Coupling.prod {α : Type u_1} {β : Type u_2} (d₁ : SDistr α) (d₂ : SDistr β) (h₁ : d₁.mass = 1) (h₂ : d₂.mass = 1) : Coupling d₁ d₂

Product coupling: independent sampling. Requires both distributions to have mass 1 (i.e., no failure probability). For sub-distributions with mass < 1, the product joint has marginals that are scaled by the other distribution's mass.

Note: This coupling is not used in the main pRHL development, which uses liftR_bind for composition instead.

Equations

• CatCrypt.Prob.Coupling.prod d₁ d₂ h₁ h₂ = { joint := d₁.bind fun (a : α) => d₂.bind fun (b : β) => CatCrypt.Prob.SDistr.pure (a, b), left_marginal := ⋯, right_marginal := ⋯ }

theorem CatCrypt.Prob.Coupling.left_marginal_sum {α : Type u_1} {β : Type u_2} {d₁ : SDistr α} {d₂ : SDistr β} (c : Coupling d₁ d₂) (a₀ : α) : ∑' (b : β), c.joint (some (a₀, b)) = d₁ (some a₀)

The left marginal condition implies a sum identity: ∑' b, joint (some (a, b)) = d₁ (some a)

theorem CatCrypt.Prob.Coupling.right_marginal_sum {α : Type u_1} {β : Type u_2} {d₁ : SDistr α} {d₂ : SDistr β} (c : Coupling d₁ d₂) (b₀ : β) : ∑' (a : α), c.joint (some (a, b₀)) = d₂ (some b₀)

The right marginal condition implies a sum identity: ∑' a, joint (some (a, b)) = d₂ (some b)

theorem CatCrypt.Prob.liftR_eq_implies_eq {α : Type u_1} {d₁ d₂ : SDistr α} (h : d₁ ⟨Eq⟩# d₂) : d₁ = d₂

If d₁ and d₂ are coupled by equality (diagonal coupling only), then they are equal as distributions. Key insight: equality coupling forces all mass to be on the diagonal, and marginal sums on the diagonal give the same values for both.

theorem CatCrypt.Prob.liftR_trans_eq {α : Type u_1} {d₁ d₂ d₃ : SDistr α} (h₁₂ : d₁ ⟨Eq⟩# d₂) (h₂₃ : d₂ ⟨Eq⟩# d₃) : d₁ ⟨Eq⟩# d₃

Transitivity for equality

theorem CatCrypt.Prob.coupling_marginal_proof {α' : Type u_5} {β' : Type u_6} {γ' : Type u_7} {δ' : Type u_8} {ε₁ : Type u_9} {ε₂ : Type u_10} (joint : SDistr (α' × β')) (kd : α' × β' → SDistr (γ' × δ')) (proj : γ' × δ' → ε₁) (sel : α' × β' → ε₂) (fi : ε₂ → SDistr ε₁) (di : SDistr ε₂) (inner : ∀ (a : α') (b : β'), joint (some (a, b)) ≠ 0 → ((kd (a, b)).bind fun (p' : γ' × δ') => SDistr.pure (proj p')) = fi (sel (a, b))) (marginal : ∀ (x : ε₂), (joint.bind fun (p : α' × β') => SDistr.pure (sel p)) (some x) = di (some x)) (x : ε₁) : ((joint.bind kd).bind fun (p' : γ' × δ') => SDistr.pure (proj p')) (some x) = (di.bind fi) (some x)

Helper: given a joint distribution, continuation coupling kd, and a marginal condition, prove that projecting the composed joint gives the expected bound distribution. This abstracts the shared proof structure used for both left and right marginals in liftR_bind.

theorem CatCrypt.Prob.liftR_bind {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {d₁ : SDistr α} {d₂ : SDistr β} {f₁ : α → SDistr γ} {f₂ : β → SDistr δ} {R : α → β → Prop} {S : γ → δ → Prop} (hd : d₁ ⟨R⟩# d₂) (hf : ∀ (a : α) (b : β), R a b → f₁ a ⟨S⟩# f₂ b) : d₁.bind f₁ ⟨S⟩# d₂.bind f₂

Composition through bind (THE KEY LEMMA for pRHL) This is the fundamental lemma that makes probabilistic relational Hoare logic work. The construction composes couplings:

1. Sample (a, b) from the coupling of d₁ and d₂
2. For each sampled pair, use the coupling from hf to get the continuation coupling
3. The result is a coupling of the bound computations

The key challenge in the formal proof is that hf requires R a b, but we only know R a b when c.joint (some (a, b)) ≠ 0. We use Classical.choice to pick couplings for pairs outside the support (any choice works since they have zero measure).

Specialized lifting lemmas

theorem CatCrypt.Prob.liftR_pure {α : Type u_1} {β : Type u_2} {R : α → β → Prop} {a : α} {b : β} (h : R a b) : SDistr.pure a ⟨R⟩# SDistr.pure b

Lifting for pure/return

theorem CatCrypt.Prob.liftR_fail {α : Type u_1} {β : Type u_2} {R : α → β → Prop} : SDistr.fail ⟨R⟩# SDistr.fail

Lifting for fail: fail lifts with fail on any relation. This is the correct formulation for sub-distributions: the coupling joint = fail satisfies both marginal conditions.

theorem CatCrypt.Prob.liftR_fail_l {α : Type u_1} {β : Type u_2} {R : α → β → Prop} : SDistr.fail ⟨R⟩# SDistr.fail

Lifting for fail on left when d₂ = fail. For sub-distributions with joint = fail, the right marginal is 0, so d₂ must also have 0 probability on all some values.

theorem CatCrypt.Prob.liftR_fail_r {α : Type u_1} {β : Type u_2} {R : α → β → Prop} : SDistr.fail ⟨R⟩# SDistr.fail

Lifting for fail on right when d₁ = fail. For sub-distributions with joint = fail, the left marginal is 0, so d₁ must also have 0 probability on all some values.

theorem CatCrypt.Prob.liftR_uniform_bij {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] [Nonempty α] [Nonempty β] (f : α ≃ β) : SDistr.uniform α ⟨fun (a : α) (b : β) => f a = b⟩# SDistr.uniform β

Uniform distributions lift with any bijection

theorem CatCrypt.Prob.liftR_uniform_same {α : Type u_1} [Fintype α] [Nonempty α] : SDistr.uniform α ⟨Eq⟩# SDistr.uniform α

Same uniform distribution lifts with equality