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.spmf_bind_const_of_no_failure {α' β' : Type w} {p : SPMF α'} (hp : Pr[⊥ | p] = 0) (q : SPMF β') : (do let _ ← p q) = q

theorem OracleComp.ProgramLogic.Relational.spmf_map_const_of_no_failure {α' β' : Type w} {p : SPMF α'} (hp : Pr[⊥ | p] = 0) (b : β') : (fun (x : α') => b) <$> p = pure b

theorem OracleComp.ProgramLogic.Relational.spmf_bind_bind_const_of_no_failure {α' β' γ' : Type w} {p : SPMF α'} (hp : Pr[⊥ | p] = 0) (q : α' → SPMF β') (hq : ∀ (a : α'), Pr[⊥ | q a] = 0) (r : SPMF γ') : (do let a ← p let _ ← q a r) = r

theorem OracleComp.ProgramLogic.Relational.probFailure_evalDist_eq_zero {m : Type u → Type v} [Monad m] [LawfulMonad m] [HasEvalPMF m] {α : Type u} (mx : m α) : Pr[⊥ | 𝒟[mx]] = 0

noncomputable def OracleComp.ProgramLogic.Relational.PMF.condOnMap {α : Type u_1} {β : Type u_2} (p : PMF α) (f : α → β) (b : β) : PMF α

Conditional distribution of a PMF along a deterministic observation map.

For an observation value outside the support of f <$> p, the choice of distribution is irrelevant; we use an arbitrary support point of p.

theorem OracleComp.ProgramLogic.Relational.PMF.condOnMap_apply_of_not_mem_fiber {α : Type u_1} {β : Type u_2} (p : PMF α) (f : α → β) (b : β) {a : α} (ha : a ∉ OracleComp.ProgramLogic.Relational.PMF.fiber✝ f b) (hb : ∃ a ∈ OracleComp.ProgramLogic.Relational.PMF.fiber✝¹ f b, a ∈ p.support) : (condOnMap p f b) a = 0

theorem OracleComp.ProgramLogic.Relational.PMF.condOnMap_apply_of_mem_support {α : Type u_1} {β : Type u_2} (p : PMF α) (f : α → β) {a : α} (ha : a ∈ p.support) : (condOnMap p f (f a)) a = p a * ((PMF.map f p) (f a))⁻¹

theorem OracleComp.ProgramLogic.Relational.PMF.map_bind_condOnMap {α : Type u_1} {β : Type u_2} (p : PMF α) (f : α → β) : (PMF.map f p).bind (condOnMap p f) = p

noncomputable def OracleComp.ProgramLogic.Relational.PMF.mapKernelWithFallback {α : Type u_1} {β : Type u_2} {γ : Type u_3} (p : PMF α) (f : α → β) (out : α → γ) (fallback : β → γ) (b : β) : PMF γ

Conditional output kernel induced by a deterministic observation map.

When the observation value is not in the support of f <$> p, the fallback is used. Since the observation has zero mass there, this does not affect the rebuilt distribution, but it makes pointwise continuation equalities easier to state.

theorem OracleComp.ProgramLogic.Relational.PMF.map_bind_mapKernelWithFallback {α : Type u_1} {β : Type u_2} {γ : Type u_3} (p : PMF α) (f : α → β) (out : α → γ) (fallback : β → γ) : (PMF.map f p).bind (mapKernelWithFallback p f out fallback) = PMF.map out p

theorem OracleComp.ProgramLogic.Relational.PMF.mapKernelWithFallback_eq_pure_of {α : Type u_1} {β : Type u_2} {γ : Type u_3} (p : PMF α) (f : α → β) (out : α → γ) (fallback : β → γ) (bad : β → Prop) (h_eq : ∀ (a : α) (b : β), f a = b → ¬bad b → out a = fallback b) (b : β) (hb : ¬bad b) : mapKernelWithFallback p f out fallback b = pure (fallback b)

theorem OracleComp.ProgramLogic.Relational.ofReal_tvDist_map_private_right_bad_le {m : Type u → Type v} [Monad m] [LawfulMonad m] [HasEvalPMF m] {α β γ : Type u} (oa : m α) (ob : m β) (pub : α → β) (fa : α → γ) (fb : β → γ) (bad : β → Prop) (h_eq : ∀ (a : α) (b : β), pub a = b → ¬bad b → fa a = fb b) : ENNReal.ofReal (tvDist (fa <$> oa) (fb <$> ob)) ≤ ENNReal.ofReal (tvDist (pub <$> oa) ob) + probEvent ob bad

theorem OracleComp.ProgramLogic.Relational.ofReal_tvDist_bind_left_le_const {m : Type u → Type v} [Monad m] [LawfulMonad m] [HasEvalPMF m] {α β : Type u} (mx : m α) (f g : α → m β) (ε : ENNReal) (hfg : ∀ a ∈ support mx, ENNReal.ofReal (tvDist (f a) (g a)) ≤ ε) : ENNReal.ofReal (tvDist (mx >>= f) (mx >>= g)) ≤ ε

theorem OracleComp.ProgramLogic.Relational.ofReal_tvDist_bind_left_le_const' {m : Type u → Type v} [Monad m] [LawfulMonad m] [HasEvalPMF m] {α β : Type u} (mx : m α) (f g : α → m β) (ε : ENNReal) (hfg : ∀ (a : α), ENNReal.ofReal (tvDist (f a) (g a)) ≤ ε) : ENNReal.ofReal (tvDist (mx >>= f) (mx >>= g)) ≤ ε

theorem OracleComp.ProgramLogic.Relational.evalDist_bind_ignore {m : Type u → Type v} [Monad m] [LawfulMonad m] [HasEvalPMF m] {α β γ : Type u} (mx : m α) (noise : α → m β) (f : α → γ) : 𝒟[do let a ← mx let _ ← noise a pure (f a)] = 𝒟[f <$> mx]

theorem OracleComp.ProgramLogic.Relational.evalDist_bind_const_of_no_failure {m : Type u → Type v} [Monad m] [LawfulMonad m] [HasEvalPMF m] {α β : Type u} (mx : m α) (my : m β) : 𝒟[do let _ ← mx my] = 𝒟[my]

theorem OracleComp.ProgramLogic.Relational.SPMF.bind_liftM {α β : Type u} (p : PMF α) (f : α → PMF β) : (do let a ← liftM p liftM (f a)) = liftM (p.bind f)

theorem OracleComp.ProgramLogic.Relational.SPMF.map_const_liftM {α β : Type u} (q : PMF α) (b : β) : (fun (x : α) => b) <$> liftM q = pure b

noncomputable def OracleComp.ProgramLogic.Relational.liftLeftMapCoupling {ι₁ ι₂ : Type u} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} [spec₁.Fintype] [spec₁.Inhabited] [spec₂.Fintype] [spec₂.Inhabited] {α β : Type} {oa : OracleComp spec₁ α} {ob : OracleComp spec₂ β} (f : α → β) (c : 𝒟[f <$> oa].Coupling 𝒟[ob]) : SPMF (α × β)

Lift a coupling of a deterministic observation of the left computation into a coupling of the full left computation with the right one.

theorem OracleComp.ProgramLogic.Relational.liftLeftMapCoupling_isCoupling {ι₁ ι₂ : Type u} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} [spec₁.Fintype] [spec₁.Inhabited] [spec₂.Fintype] [spec₂.Inhabited] {α β : Type} {oa : OracleComp spec₁ α} {ob : OracleComp spec₂ β} (f : α → β) (c : 𝒟[f <$> oa].Coupling 𝒟[ob]) : (liftLeftMapCoupling f c).IsCoupling 𝒟[oa] 𝒟[ob]

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) : 𝒟[f <$> oa] = 𝒟[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.

Quantitative relational WP rules

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

Pure rule for quantitative relational WP.

theorem OracleComp.ProgramLogic.Relational.eRelWP_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 : pre ≤ eRelWP oa ob post) : pre' ≤ eRelWP oa ob post'

Monotonicity/consequence rule for quantitative relational WP.

theorem OracleComp.ProgramLogic.Relational.eRelWP_bind_rule {ι₁ ι₂ : 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 : pre ≤ eRelWP oa ob cut) (hfg : ∀ (a : α) (b : β), cut a b ≤ eRelWP (fa a) (fb b) post) : pre ≤ eRelWP (oa >>= fa) (ob >>= fb) post

Bind/sequential composition rule for quantitative relational WP.

Indicator-postcondition rules (RelTriple')

These are direct quantitative analogues of the pRHL effect-rule block in VCVio.ProgramLogic.Relational.Basic, expressed as quantitative eRelWP lower bounds via the relTriple'_iff_relTriple bridge. They give the eRHL-flavoured statement of every coupling primitive OracleComp already exposes, so downstream proofs can mix exact indicator rules with the genuinely quantitative bounds below without having to re-derive the bridge each time.

Each rule is a one-line wrapper of its RelTriple cousin. The proofs that the underlying couplings exist live in Basic.lean; this section only repackages them at the RelTriple' level.

theorem OracleComp.ProgramLogic.Relational.relTriple'_pure_pure {ι₁ ι₂ : Type u} {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

RelTriple' introduction from a pure-pure pair satisfying the post.

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 RelTriple' on the diagonal equality relation.

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

theorem OracleComp.ProgramLogic.Relational.relTriple'_bind {ι₁ ι₂ : Type u} {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

Sequential composition rule for RelTriple'.

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 lifts to a RelTriple' on EqRel.

theorem OracleComp.ProgramLogic.Relational.relTriple'_eqRel_of_evalDist_eq {ι₁ ι₂ : Type u} {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 lifts to a RelTriple' on EqRel.

theorem OracleComp.ProgramLogic.Relational.relTriple'_eqRel_of_probOutput_eq {ι₁ ι₂ : Type u} {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 lifts to a RelTriple' on EqRel.

Oracle-query coupling rules (eRHL 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 for queries: RelTriple' analogue of relTriple_query.

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 for queries (the eRHL "rnd" rule).

Functorial / structural rules

theorem OracleComp.ProgramLogic.Relational.relTriple'_map {ι₁ ι₂ : Type u} {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

Functor.map rule for RelTriple'.

theorem OracleComp.ProgramLogic.Relational.relTriple'_if {ι₁ ι₂ : Type u} {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 rule for RelTriple'.

theorem OracleComp.ProgramLogic.Relational.relTriple'_pure_left {ι₁ ι₂ : Type u} {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: lift the strengthened post (· = a) ∧ R back to R.

theorem OracleComp.ProgramLogic.Relational.relTriple'_pure_right {ι₁ ι₂ : Type u} {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: lift the strengthened post (· = b) ∧ R back to R.

Iteration / list-traversal rules

theorem OracleComp.ProgramLogic.Relational.relTriple'_replicate {ι₁ ι₂ : Type u} {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)

RelTriple' for OracleComp.replicate.

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-relation specialization of relTriple'_replicate.

theorem OracleComp.ProgramLogic.Relational.relTriple'_list_mapM {ι₁ ι₂ : Type u} {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)

RelTriple' for List.mapM.

theorem OracleComp.ProgramLogic.Relational.relTriple'_list_mapM_eqRel {ι₁ ι₂ : Type u} {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 specialization of relTriple'_list_mapM.

theorem OracleComp.ProgramLogic.Relational.relTriple'_list_foldlM {ι₁ ι₂ : Type u} {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

RelTriple' for List.foldlM.

theorem OracleComp.ProgramLogic.Relational.relTriple'_list_foldlM_same {ι₁ ι₂ : Type u} {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.

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

Bijection coupling for uniform sampling at the RelTriple' level.

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

Identity coupling for uniform sampling at the RelTriple' level.

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₂ α} : 𝒟[oa].tvDist 𝒟[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.approxRelTriple_eqRel_of_ofReal_tvDist_le {ι₁ : Type u} {spec₁ : OracleSpec ι₁} [spec₁.Fintype] [spec₁.Inhabited] {α : Type} {oa ob : OracleComp spec₁ α} {ε : ENNReal} (h : ENNReal.ofReal (tvDist oa ob) ≤ ε) : ApproxRelTriple ε oa ob (EqRel α)

A TV-distance bound induces an approximate equality coupling.

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 α)) : 𝒟[oa] = 𝒟[ob]

Game equivalence from pRHL equality coupling.

Relational algebra instance

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

Pure values characterize the quantitative relational weakest precondition.

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

Quantitative relational weakest precondition is monotone in the postcondition.

theorem OracleComp.ProgramLogic.Relational.eRelWP_bind_le {ι₁ ι₂ : Type u} {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₂ δ) (post : γ → δ → ENNReal) : (eRelWP oa ob fun (a : α) (b : β) => eRelWP (fa a) (fb b) post) ≤ eRelWP (oa >>= fa) (ob >>= fb) post

Quantitative relational weakest preconditions compose through bind.

@[implicit_reducible]

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

Quantitative relational algebra instance for OracleComp, based on eRelWP.

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

Anchoring instance for the quantitative ℝ≥0∞-valued relational logic on OracleComp.

When one of the two computations is pure, the supremum over couplings collapses to the single Dirac coupling (existence: IsCoupling.dirac_left; uniqueness on the supports follows from IsCoupling.apply_pure_left_eq), and the relational expectation reduces to the unary expectation wp y (post a) (resp. wp x (fun a => post a b)). This is the genuinely quantitative analogue of the qualitative Anchored Prop instance in VCVio/ProgramLogic/Relational/Basic.lean.

Specialisations of the generic asynchronous and structural rules

The following examples confirm that the new generic rules in ToMathlib/Control/Monad/RelationalAlgebra.lean (asynchronous one-sided binds and structural pure rules) automatically apply to eRelWP. They are the quantitative counterparts of SSProve's apply_left / apply_right / if_rule style rules.

Quantitative effect-specific rules (eRHL primitives)

These are the genuinely quantitative companions of the indicator wrappers above: they expose witness-based lower bounds for eRelWP on the basic OracleComp effect operations (uniform sampling and oracle queries under a bijection). Together with the existing closed form eRelWP_pure and the core eRelWP_pure_le / _conseq / _bind_rule, they are sufficient to discharge most apRHL-style goals without descending to the underlying coupling supremum.

theorem OracleComp.ProgramLogic.Relational.eRelWP_ge_of_isCoupling {ι₁ ι₂ : Type u} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} [spec₁.Fintype] [spec₁.Inhabited] [spec₂.Fintype] [spec₂.Inhabited] {α β : Type} {oa : OracleComp spec₁ α} {ob : OracleComp spec₂ β} (post : α → β → ENNReal) (c : SPMF (α × β)) (hc : c.IsCoupling 𝒟[oa] 𝒟[ob]) : ∑' (z : α × β), Pr[= z | c] * post z.1 z.2 ≤ eRelWP oa ob post

A witness coupling provides a lower bound on the eRHL weakest precondition.

This is the basic primitive used by every closed-form / lower-bound rule below, and is the right tool whenever a proof can exhibit a specific coupling.

theorem OracleComp.ProgramLogic.Relational.eRelWP_of_isCoupling {ι₁ ι₂ : Type u} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} [spec₁.Fintype] [spec₁.Inhabited] [spec₂.Fintype] [spec₂.Inhabited] {α β : Type} {pre : ENNReal} {oa : OracleComp spec₁ α} {ob : OracleComp spec₂ β} (post : α → β → ENNReal) (c : SPMF (α × β)) (hc : c.IsCoupling 𝒟[oa] 𝒟[ob]) (hpre : pre ≤ ∑' (z : α × β), Pr[= z | c] * post z.1 z.2) : pre ≤ eRelWP oa ob post

A witness coupling whose score dominates the precondition discharges a quantitative relational WP lower-bound obligation.

Uniform sampling under a bijection

theorem OracleComp.ProgramLogic.Relational.eRelWP_uniformSample_bij_ge {α : Type} [SampleableType α] {f : α → α} (hf : Function.Bijective f) (post : α → α → ENNReal) : ∑' (a : α), Pr[= a | $ᵗ α] * post a (f a) ≤ eRelWP ($ᵗ α) ($ᵗ α) post

Quantitative lower bound for two uniform samples coupled by a bijection.

The bijection coupling (fun x => (x, f x)) <$> $ᵗ α realises the sum on the left as a score, providing the sharpest "syntactic" lower bound on the coupling supremum.

theorem OracleComp.ProgramLogic.Relational.eRelWP_uniformSample_bij {α : Type} [SampleableType α] {f : α → α} (hf : Function.Bijective f) (post : α → α → ENNReal) {pre : ENNReal} (hpre : pre ≤ ∑' (a : α), Pr[= a | $ᵗ α] * post a (f a)) : pre ≤ eRelWP ($ᵗ α) ($ᵗ α) post

Any precondition below the bijection average discharges the quantitative relational WP lower-bound for two uniform samples.

Oracle queries under a bijection

theorem OracleComp.ProgramLogic.Relational.eRelWP_query_bij_ge {ι₁ : Type u} {spec₁ : OracleSpec ι₁} [spec₁.Fintype] [spec₁.Inhabited] (t : spec₁.Domain) {f : spec₁.Range t → spec₁.Range t} (hf : Function.Bijective f) (post : spec₁.Range t → spec₁.Range t → ENNReal) : ∑' (a : spec₁.Range t), Pr[= a | liftM (OracleSpec.query t)] * post a (f a) ≤ eRelWP (liftM (OracleSpec.query t)) (liftM (OracleSpec.query t)) post

Quantitative lower bound for two oracle queries coupled by a bijection on the range. This is the eRHL counterpart of relTriple_query_bij.

theorem OracleComp.ProgramLogic.Relational.eRelWP_query_bij {ι₁ : Type u} {spec₁ : OracleSpec ι₁} [spec₁.Fintype] [spec₁.Inhabited] (t : spec₁.Domain) {f : spec₁.Range t → spec₁.Range t} (hf : Function.Bijective f) (post : spec₁.Range t → spec₁.Range t → ENNReal) {pre : ENNReal} (hpre : pre ≤ ∑' (a : spec₁.Range t), Pr[= a | liftM (OracleSpec.query t)] * post a (f a)) : pre ≤ eRelWP (liftM (OracleSpec.query t)) (liftM (OracleSpec.query t)) post

Triple form of eRelWP_query_bij_ge.

Demonstration examples for the indicator wrappers and quantitative primitives

Small examples illustrating how the RelTriple' wrappers and the closed-form / lower-bound eRelWP rules combine in practice.