Quantitative Relational Program Logic (eRHL)

This file develops the main theorem layer for the eRHL-style quantitative relational logic for OracleComp, building on the core interfaces in VCVio.ProgramLogic.Relational.QuantitativeDefs.

The core idea (from Avanzini-Barthe-Gregoire-Davoli, POPL 2025) is to make pre/postconditions ℝ≥0∞-valued instead of Prop-valued. This subsumes both pRHL (exact coupling, via indicator postconditions) and apRHL (ε-approximate coupling, via threshold preconditions).

Main results in this file

• coupling-mass lemmas and support facts
• introduction, consequence, and bind rules for eRHL
• bridges to exact and approximate couplings
• total-variation characterizations via EqRel

Design

                eRHL (ℝ≥0∞-valued pre/post)
               /          |           \
              /           |            \
pRHL (exact)    apRHL (ε-approx)   stat-distance
indicator R      1-ε, indicator R    1, indicator(=)

Helpers for coupling mass

theorem OracleComp.ProgramLogic.Relational.relTriple'_iff_couplingPost {ι₁ ι₂ : Type u} {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 ↔ CouplingPost oa ob R

Bridge: the eRHL-based definition agrees with the existing coupling-based one.

Forward direction blocker: RelTriple' → CouplingPost requires extracting a coupling c with f(c) = 1 from 1 ≤ ⨆ c, f(c). Although the coupling polytope is compact and f is linear (so the max IS attained in standard math), formalizing this in Lean requires proving compactness of the coupling space, which needs topology infrastructure not yet available here.

theorem OracleComp.ProgramLogic.Relational.relTriple'_iff_relTriple {ι₁ ι₂ : Type u} {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 ↔ RelTriple oa ob R

Bridge: RelTriple' agrees with the existing RelTriple.

theorem OracleComp.ProgramLogic.Relational.evalDist_map_eq_of_relTriple' {ι₁ ι₂ : Type u} {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) : evalDist (f <$> oa) = evalDist (g <$> ob)

If a RelTriple' holds for fun a b => f a = g b, then mapping by f and g produces equal distributions. This is the eRHL-level version of evalDist_map_eq_of_relTriple.

eRHL rules

theorem OracleComp.ProgramLogic.Relational.eRelTriple_pure {ι₁ ι₂ : Type u} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} [spec₁.Fintype] [spec₁.Inhabited] [spec₂.Fintype] [spec₂.Inhabited] {α β : Type} (a : α) (b : β) (post : α → β → ENNReal) : eRelTriple (post a b) (pure a) (pure b) post

Pure rule for eRHL.

theorem OracleComp.ProgramLogic.Relational.eRelTriple_conseq {ι₁ ι₂ : Type u} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} [spec₁.Fintype] [spec₁.Inhabited] [spec₂.Fintype] [spec₂.Inhabited] {α β : Type} {pre pre' : ENNReal} {oa : OracleComp spec₁ α} {ob : OracleComp spec₂ β} {post post' : α → β → ENNReal} (hpre : pre' ≤ pre) (hpost : ∀ (a : α) (b : β), post a b ≤ post' a b) (h : eRelTriple pre oa ob post) : eRelTriple pre' oa ob post'

Monotonicity/consequence rule for eRHL.

theorem OracleComp.ProgramLogic.Relational.eRelTriple_bind {ι₁ ι₂ : Type u} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} [spec₁.Fintype] [spec₁.Inhabited] [spec₂.Fintype] [spec₂.Inhabited] {α β γ δ : Type} {pre : ENNReal} {oa : OracleComp spec₁ α} {ob : OracleComp spec₂ β} {fa : α → OracleComp spec₁ γ} {fb : β → OracleComp spec₂ δ} {cut : α → β → ENNReal} {post : γ → δ → ENNReal} (hxy : eRelTriple pre oa ob cut) (hfg : ∀ (a : α) (b : β), eRelTriple (cut a b) (fa a) (fb b) post) : eRelTriple pre (oa >>= fa) (ob >>= fb) post

Bind/sequential composition rule for eRHL.

Helpers for statistical distance / coupling characterization

Statistical distance via eRHL

theorem OracleComp.ProgramLogic.Relational.spmf_tvDist_eq_one_sub_eRelWP_eqRel {ι₁ ι₂ : Type u} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} [spec₁.Fintype] [spec₁.Inhabited] [spec₂.Fintype] [spec₂.Inhabited] {α : Type} {oa : OracleComp spec₁ α} {ob : OracleComp spec₂ α} : (evalDist oa).tvDist (evalDist ob) = (1 - eRelWP oa ob (EqRel α).indicator).toReal

Statistical distance as a complement of eRHL value with equality indicator. Uses SPMF.tvDist directly to handle cross-spec comparison.

theorem OracleComp.ProgramLogic.Relational.tvDist_eq_one_sub_eRelWP_eqRel {ι₁ : Type u} {spec₁ : OracleSpec ι₁} [spec₁.Fintype] [spec₁.Inhabited] {α : Type} {oa ob : OracleComp spec₁ α} : tvDist oa ob = (1 - eRelWP oa ob (EqRel α).indicator).toReal

Same-spec version using the tvDist notation.

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

Game equivalence from pRHL equality coupling.