Quantitative RelWP carrier for OracleComp (Loom2-style default)

This file is the home of the default quantitative Std.Do'.RelWP instance for pairs of OracleComp programs valued in ℝ≥0∞. The rwpTrans field wraps the existing eRelWP (VCVio/ProgramLogic/Relational/QuantitativeDefs.lean:31); the three RelWP axioms are discharged by the existing eRelWP_pure, eRelWP_bind_le, eRelWP_mono lemmas (VCVio/ProgramLogic/Relational/Quantitative.lean).

Layout

This is one of three relational carriers we register on OracleComp. Because Std.Do'.RelWP's Pred is an outParam, only one carrier can be visible to instance synthesis at a time. We register them asymmetrically, matching the unary tier in VCVio/ProgramLogic/Unary/Loom/:

• This file (Loom/Quantitative.lean) — the ℝ≥0∞ carrier as a normal instance, always live once the file is imported. This is the default.
• Loom/Qualitative.lean — the Prop carrier as a scoped instance under namespace OracleComp.Rel.Qualitative, opt-in via open OracleComp.Rel.Qualitative.
• Loom/Probabilistic.lean — the Prob carrier as a scoped instance under namespace OracleComp.Rel.Probabilistic, opt-in via open OracleComp.Rel.Probabilistic.

There is no umbrella Relational/Loom.lean re-export. Consumers import the specific carrier they need.

Lattice plumbing

The Lean.Order.{PartialOrder, CompleteLattice} adapters for ℝ≥0∞ are shipped by VCVio/ProgramLogic/Unary/Loom/Quantitative.lean and re-used here unchanged. We do not redefine them.

@[implicit_reducible]

noncomputable instance OracleComp.ProgramLogic.Relational.Loom.instRelWP {ι₁ ι₂ : Type u} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} [spec₁.Fintype] [spec₁.Inhabited] [spec₂.Fintype] [spec₂.Inhabited] : Std.Do'.RelWP (OracleComp spec₁) (OracleComp spec₂) ENNReal EPost⟨⟩ EPost⟨⟩

Quantitative Std.Do'.RelWP interpretation of pairs of OracleComp programs valued in ℝ≥0∞.

The rwpTrans is the existing eRelWP (the supremum over couplings of expected values); the two EPost.nil arguments are ignored since neither side of an OracleComp pair has a first-class exception slot. The three RelWP axioms reduce to the existing eRelWP_pure, eRelWP_bind_le, eRelWP_mono lemmas.

Definitional alignment with eRelWP

The keystone lemma confirms Std.Do'.rwp agrees with eRelWP on the nose, so every existing eRHL theorem in VCVio/ProgramLogic/Relational/Quantitative.lean transports for free when the user rewrites Std.Do'.rwp _ _ _ _ _ ↦ eRelWP _ _ _.

theorem OracleComp.ProgramLogic.Relational.Loom.rwp_eq_eRelWP {ι₁ ι₂ : Type u} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} [spec₁.Fintype] [spec₁.Inhabited] [spec₂.Fintype] [spec₂.Inhabited] {α β : Type} (oa : OracleComp spec₁ α) (ob : OracleComp spec₂ β) (post : α → β → ENNReal) : Std.Do'.rwp oa ob post Lean.Order.bot Lean.Order.bot = eRelWP oa ob post

theorem OracleComp.ProgramLogic.Relational.Loom.relTriple_iff_eRelWP_le {ι₁ ι₂ : 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) : Std.Do'.RelTriple pre oa ob post Lean.Order.bot Lean.Order.bot ↔ pre ≤ eRelWP oa ob post

Std.Do'.RelTriple agrees with the raw quantitative lower-bound form.

Quantitative RelTriple rules

theorem OracleComp.ProgramLogic.Relational.Loom.relTriple_pure {ι₁ ι₂ : Type u} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} [spec₁.Fintype] [spec₁.Inhabited] [spec₂.Fintype] [spec₂.Inhabited] {α β : Type} (a : α) (b : β) (post : α → β → ENNReal) : Std.Do'.RelTriple (post a b) (pure a) (pure b) post Lean.Order.bot Lean.Order.bot

Pure rule for the default quantitative Std.Do'.RelTriple carrier.

theorem OracleComp.ProgramLogic.Relational.Loom.relTriple_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 : Std.Do'.RelTriple pre oa ob post Lean.Order.bot Lean.Order.bot) : Std.Do'.RelTriple pre' oa ob post' Lean.Order.bot Lean.Order.bot

Consequence rule for the default quantitative Std.Do'.RelTriple carrier.

theorem OracleComp.ProgramLogic.Relational.Loom.relTriple_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 : Std.Do'.RelTriple pre oa ob cut Lean.Order.bot Lean.Order.bot) (hfg : ∀ (a : α) (b : β), Std.Do'.RelTriple (cut a b) (fa a) (fb b) post Lean.Order.bot Lean.Order.bot) : Std.Do'.RelTriple pre (oa >>= fa) (ob >>= fb) post Lean.Order.bot Lean.Order.bot

Bind rule for the default quantitative Std.Do'.RelTriple carrier.

theorem OracleComp.ProgramLogic.Relational.Loom.relTriple_uniformSample_bij {α : Type} [SampleableType α] {f : α → α} (hf : Function.Bijective f) (post : α → α → ENNReal) {pre : ENNReal} (hpre : pre ≤ ∑' (a : α), Pr[= a | $ᵗ α] * post a (f a)) : Std.Do'.RelTriple pre ($ᵗ α) ($ᵗ α) post Lean.Order.bot Lean.Order.bot

Uniform sampling under a bijection for the default quantitative Std.Do'.RelTriple carrier.

theorem OracleComp.ProgramLogic.Relational.Loom.relTriple_uniformSample_refl {α : Type} [SampleableType α] (post : α → α → ENNReal) : Std.Do'.RelTriple (∑' (a : α), Pr[= a | $ᵗ α] * post a a) ($ᵗ α) ($ᵗ α) post Lean.Order.bot Lean.Order.bot

Identity coupling for uniform sampling under the default quantitative Std.Do'.RelTriple carrier.

theorem OracleComp.ProgramLogic.Relational.Loom.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) (post : spec₁.Range t → spec₁.Range t → ENNReal) {pre : ENNReal} (hpre : pre ≤ ∑' (a : spec₁.Range t), Pr[= a | liftM (query t)] * post a (f a)) : Std.Do'.RelTriple pre (liftM (query t)) (liftM (query t)) post Lean.Order.bot Lean.Order.bot

Oracle query under a bijection for the default quantitative Std.Do'.RelTriple carrier.

theorem OracleComp.ProgramLogic.Relational.Loom.relTriple_query_refl {ι₁ : Type u} {spec₁ : OracleSpec ι₁} [spec₁.Fintype] [spec₁.Inhabited] (t : spec₁.Domain) (post : spec₁.Range t → spec₁.Range t → ENNReal) : Std.Do'.RelTriple (∑' (a : spec₁.Range t), Pr[= a | liftM (query t)] * post a a) (liftM (query t)) (liftM (query t)) post Lean.Order.bot Lean.Order.bot

Identity coupling for oracle queries under the default quantitative Std.Do'.RelTriple carrier.