Quantitative Hoare triples for OracleComp

The user-facing wp_* and triple_* lemma library for the quantitative (ℝ≥0∞) program logic on OracleComp spec. After the Loom2 cutover the canonical heads are Std.Do'.wp and Std.Do'.Triple, both with the exception postcondition fixed to Lean.Order.bot on the empty Std.Do'.EPost.nil carrier (which we equip with a Lean.Order.CCPO instance in Loom/Quantitative.lean). All lemmas are stated against those canonical heads, exactly the shape that:

• the user-facing notation wp⟦c⟧ post (in NotationCore.lean) elaborates to,
• Loom2's ⦃ pre ⦄ c ⦃ post ⦄ notation (in Loom.Triple.Basic) elaborates to,
• the vcgen / vcstep tactic infrastructure recognises after the cutover.

The keystone definitional alignment lives in Loom/Quantitative.lean: wp _ _ = MAlgOrdered.wp _ _ is rfl for OracleComp, so existing MAlgOrdered.wp_* machinery transports directly into the Std.Do' shape. The Std.Do'.Triple analogue is inductive (not definitional) and bridged via Std.Do'.Triple.iff (pre ⊑ wp …) and triple_ofLE.

API contract

• This unary quantitative interface is instantiated for OracleComp spec.
• Probability/evaluation assumptions are [spec.Fintype] and [spec.Inhabited].
• The quantitative codomain is fixed to ℝ≥0∞.
• Every wp_* lemma is stated as wp oa post = …, every triple_* lemma as Triple pre oa post.
• For ergonomic call-site syntax, the abbreviations wp and Triple reduce to the canonical heads with epost :=. They are pure notation: every theorem is stated against the canonical forms, and tactics (vcgen, vcstep, @[wpStep], …) match on the canonical heads after abbrev unfolding.

@[reducible, inline]

noncomputable abbrev OracleComp.ProgramLogic.wp {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α : Type} (oa : OracleComp spec α) (post : α → ENNReal) : ENNReal

Quantitative weakest-precondition for OracleComp spec, fixing the exception postcondition to Lean.Order.bot. Definitionally equal to Std.Do'.wp oa post Lean.Order.bot; see the API contract for details.

@[reducible, inline]

noncomputable abbrev OracleComp.ProgramLogic.Triple {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α : Type} (pre : ENNReal) (oa : OracleComp spec α) (post : α → ENNReal) : Prop

Quantitative Hoare triple for OracleComp spec, fixing the exception postcondition to Lean.Order.bot. Definitionally equal to Std.Do'.Triple pre oa post Lean.Order.bot; see the API contract for details.

Internal alias

MAlgOrdered.wp is rfl-equal to wp _ _ on OracleComp via the Loom.instWP instance. The bridge wp_eq_mAlgOrdered_wp re-exposes this so existing MAlgOrdered.wp_* lemmas can be applied with a single rewrite.

theorem OracleComp.ProgramLogic.wp_eq_mAlgOrdered_wp {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α : Type} (oa : OracleComp spec α) (post : α → ENNReal) : wp oa post = MAlgOrdered.wp oa post

theorem OracleComp.ProgramLogic.triple_iff_le_wp {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α : Type} (pre : ENNReal) (oa : OracleComp spec α) (post : α → ENNReal) : Triple pre oa post ↔ pre ≤ wp oa post

Bridge between Loom2's inductive Std.Do'.Triple and Mathlib's ≤ on ℝ≥0∞. Loom2 defines Std.Do'.Triple.iff against Lean.Order.PartialOrder.rel; on ℝ≥0∞ our Lean.Order.PartialOrder instance defines rel as Mathlib's ≤, so the two coincide. The explicit Iff.rfl re-exposes the equivalence in ≤-form, which is what all the downstream triple_* proofs are stated against.

theorem OracleComp.ProgramLogic.triple_ofLE {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α : Type} {pre : ENNReal} {oa : OracleComp spec α} {post : α → ENNReal} (h : pre ≤ wp oa post) : Triple pre oa post

Construct a Triple … from a ≤-form proof pre ≤ wp oa post. Companion to triple_iff_le_wp.mpr; preferred as the constructor in concrete proofs because it avoids Lean's typeclass-projection unification failures that arise when calling Std.Do'.Triple.intro directly with a ≤ proof.

theorem OracleComp.ProgramLogic.triple_toLE {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α : Type} {pre : ENNReal} {oa : OracleComp spec α} {post : α → ENNReal} (h : Triple pre oa post) : pre ≤ wp oa post

Extract the ≤-form pre ≤ wp oa post from a Triple …. Companion to triple_iff_le_wp.mp.

wp lemmas (against wp _ _)

@[simp]

theorem OracleComp.ProgramLogic.wp_pure {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α : Type} (x : α) (post : α → ENNReal) : wp (pure x) post = post x

@[simp]

theorem OracleComp.ProgramLogic.wp_ite {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α : Type} (c : Prop) [Decidable c] (oa ob : OracleComp spec α) (post : α → ENNReal) : wp (if c then oa else ob) post = if c then wp oa post else wp ob post

@[simp]

theorem OracleComp.ProgramLogic.wp_dite {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α : Type} (c : Prop) [Decidable c] (oa : c → OracleComp spec α) (ob : ¬c → OracleComp spec α) (post : α → ENNReal) : wp (dite c oa ob) post = if h : c then wp (oa h) post else wp (ob h) post

theorem OracleComp.ProgramLogic.wp_bind {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α β : Type} (oa : OracleComp spec α) (ob : α → OracleComp spec β) (post : β → ENNReal) : wp (oa >>= ob) post = wp oa fun (x : α) => wp (ob x) post

theorem OracleComp.ProgramLogic.wp_replicate_zero {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α : Type} (oa : OracleComp spec α) (post : List α → ENNReal) : wp (replicate 0 oa) post = post []

theorem OracleComp.ProgramLogic.wp_replicate_succ {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α : Type} (oa : OracleComp spec α) (n : ℕ) (post : List α → ENNReal) : wp (replicate (n + 1) oa) post = wp oa fun (x : α) => wp (replicate n oa) fun (xs : List α) => post (x :: xs)

theorem OracleComp.ProgramLogic.wp_list_mapM_nil {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α β : Type} (f : α → OracleComp spec β) (post : List β → ENNReal) : wp (List.mapM f []) post = post []

theorem OracleComp.ProgramLogic.wp_list_mapM_cons {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α β : Type} (x : α) (xs : List α) (f : α → OracleComp spec β) (post : List β → ENNReal) : wp (List.mapM f (x :: xs)) post = wp (f x) fun (y : β) => wp (List.mapM f xs) fun (ys : List β) => post (y :: ys)

theorem OracleComp.ProgramLogic.wp_list_foldlM_nil {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α σ : Type} (f : σ → α → OracleComp spec σ) (init : σ) (post : σ → ENNReal) : wp (List.foldlM f init []) post = post init

theorem OracleComp.ProgramLogic.wp_list_foldlM_cons {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α σ : Type} (x : α) (xs : List α) (f : σ → α → OracleComp spec σ) (init : σ) (post : σ → ENNReal) : wp (List.foldlM f init (x :: xs)) post = wp (f init x) fun (s : σ) => wp (List.foldlM f s xs) post

theorem OracleComp.ProgramLogic.wp_mono {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α : Type} (oa : OracleComp spec α) {post post' : α → ENNReal} (hpost : ∀ (x : α), post x ≤ post' x) : wp oa post ≤ wp oa post'

theorem OracleComp.ProgramLogic.wp_map {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α β : Type} (f : α → β) (oa : OracleComp spec α) (post : β → ENNReal) : wp (f <$> oa) post = wp oa (post ∘ f)

theorem OracleComp.ProgramLogic.wp_eq_tsum {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α : Type} (oa : OracleComp spec α) (post : α → ENNReal) : wp oa post = ∑' (x : α), Pr[= x | oa] * post x

General unfolding: wp as weighted sum over output probabilities.

@[simp]

theorem OracleComp.ProgramLogic.wp_const {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α : Type} (oa : OracleComp spec α) (c : ENNReal) : (wp oa fun (x : α) => c) = c

theorem OracleComp.ProgramLogic.wp_add {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α : Type} (oa : OracleComp spec α) (f g : α → ENNReal) : (wp oa fun (x : α) => f x + g x) = wp oa f + wp oa g

theorem OracleComp.ProgramLogic.wp_mul_const {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α : Type} (oa : OracleComp spec α) (c : ENNReal) (f : α → ENNReal) : (wp oa fun (x : α) => c * f x) = c * wp oa f

theorem OracleComp.ProgramLogic.wp_const_mul {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α : Type} (oa : OracleComp spec α) (f : α → ENNReal) (c : ENNReal) : (wp oa fun (x : α) => f x * c) = wp oa f * c

Triple lemmas (against Triple _ _ _)

Std.Do'.Triple is an inductive wrapper around pre ⊑ wp …. The accessor Std.Do'.Triple.iff exchanges between the inductive form and the ≤-form; triple_ofLE packages a ≤-proof into the constructor; pattern matching match h with | .intro h => h extracts the underlying inequality.

theorem OracleComp.ProgramLogic.triple_conseq {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α : Type} {pre pre' : ENNReal} {oa : OracleComp spec α} {post post' : α → ENNReal} (hpre : pre' ≤ pre) (hpost : ∀ (x : α), post x ≤ post' x) : Triple pre oa post → Triple pre' oa post'

theorem OracleComp.ProgramLogic.triple_bind {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α β : Type} {pre : ENNReal} {oa : OracleComp spec α} {cut : α → ENNReal} {ob : α → OracleComp spec β} {post : β → ENNReal} (hoa : Triple pre oa cut) (hob : ∀ (x : α), Triple (cut x) (ob x) post) : Triple pre (oa >>= ob) post

theorem OracleComp.ProgramLogic.triple_bind_wp {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α β : Type} {pre : ENNReal} {oa : OracleComp spec α} {ob : α → OracleComp spec β} {post : β → ENNReal} (h : Triple pre oa fun (x : α) => wp (ob x) post) : Triple pre (oa >>= ob) post

theorem OracleComp.ProgramLogic.triple_pure {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α : Type} (x : α) (post : α → ENNReal) : Triple (post x) (pure x) post

theorem OracleComp.ProgramLogic.triple_zero {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α : Type} (oa : OracleComp spec α) (post : α → ENNReal) : Triple 0 oa post

A quantitative triple with precondition 0 is always true.

theorem OracleComp.ProgramLogic.triple_ite {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α : Type} {c : Prop} [Decidable c] {pre : ENNReal} {oa ob : OracleComp spec α} {post : α → ENNReal} (ht : c → Triple pre oa post) (hf : ¬c → Triple pre ob post) : Triple pre (if c then oa else ob) post

theorem OracleComp.ProgramLogic.triple_dite {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α : Type} {c : Prop} [Decidable c] {pre : ENNReal} {oa : c → OracleComp spec α} {ob : ¬c → OracleComp spec α} {post : α → ENNReal} (ht : ∀ (h : c), Triple pre (oa h) post) (hf : ∀ (h : ¬c), Triple pre (ob h) post) : Triple pre (dite c oa ob) post

theorem OracleComp.ProgramLogic.probEvent_eq_wp_indicator {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α : Type} (oa : OracleComp spec α) (p : α → Prop) [DecidablePred p] : probEvent oa p = wp oa fun (x : α) => if p x then 1 else 0

probEvent as a WP of an indicator postcondition.

theorem OracleComp.ProgramLogic.probOutput_eq_wp_indicator {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α : Type} (oa : OracleComp spec α) [DecidableEq α] (x : α) : Pr[= x | oa] = wp oa fun (y : α) => if y = x then 1 else 0

probOutput as a WP of a singleton-indicator postcondition.

theorem OracleComp.ProgramLogic.wp_liftM_query {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] (t : spec.Domain) (post : spec.Range t → ENNReal) : wp (liftM (OracleSpec.query t)) post = ∑' (u : spec.Range t), 1 / ↑(Fintype.card (spec.Range t)) * post u

liftM query form of wp_query.

theorem OracleComp.ProgramLogic.wp_query {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] (t : spec.Domain) (post : spec.Range t → ENNReal) : wp (liftM (OracleSpec.query t)) post = ∑' (u : spec.Range t), 1 / ↑(Fintype.card (spec.Range t)) * post u

Quantitative WP rule for a uniform oracle query.

theorem OracleComp.ProgramLogic.wp_HasQuery_query {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] (t : spec.Domain) (post : spec.Range t → ENNReal) : wp (query t) post = ∑' (u : spec.Range t), 1 / ↑(Fintype.card (spec.Range t)) * post u

HasQuery.query form of wp_query: after the HasQuery ergonomic cutover, the bare query t : OracleComp spec _ in user code elaborates to HasQuery.query t. This restates the rule with that head so the @[game_rule] registry can dispatch on user-facing goals without unfolding.

theorem OracleComp.ProgramLogic.wp_uniformSample {α : Type} [SampleableType α] (post : α → ENNReal) : wp ($ᵗ α) post = ∑' (x : α), Pr[= x | $ᵗ α] * post x

theorem OracleComp.ProgramLogic.triple_probEvent_indicator {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α : Type} (oa : OracleComp spec α) (p : α → Prop) [DecidablePred p] : Triple (probEvent oa p) oa fun (x : α) => if p x then 1 else 0

Indicator-event probability as an exact quantitative triple.

theorem OracleComp.ProgramLogic.triple_probOutput_indicator {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α : Type} (oa : OracleComp spec α) [DecidableEq α] (x : α) : Triple Pr[= x | oa] oa fun (y : α) => if y = x then 1 else 0

Singleton-output probability as an exact quantitative triple.

theorem OracleComp.ProgramLogic.le_probEvent_iff_triple_indicator {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α : Type} (oa : OracleComp spec α) (p : α → Prop) [DecidablePred p] (r : ENNReal) : r ≤ probEvent oa p ↔ Triple r oa fun (x : α) => if p x then 1 else 0

Lower bounds on probEvent are exactly indicator-postcondition triples.

theorem OracleComp.ProgramLogic.le_probOutput_iff_triple_indicator {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α : Type} (oa : OracleComp spec α) [DecidableEq α] (x : α) (r : ENNReal) : r ≤ Pr[= x | oa] ↔ Triple r oa fun (y : α) => if y = x then 1 else 0

Lower bounds on probOutput are exactly singleton-indicator triples.

@[simp]

theorem OracleComp.ProgramLogic.probEvent_mem_support {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α : Type} (oa : OracleComp spec α) : (probEvent oa fun (x : α) => x ∈ support oa) = 1

The support event of an OracleComp occurs almost surely.

theorem OracleComp.ProgramLogic.triple_probEvent_eq_one {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α : Type} (oa : OracleComp spec α) (p : α → Prop) [DecidablePred p] (h : probEvent oa p = 1) : Triple 1 oa fun (x : α) => if p x then 1 else 0

Exact probability-1 events are exact quantitative triples.

theorem OracleComp.ProgramLogic.triple_probOutput_eq_one {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α : Type} (oa : OracleComp spec α) [DecidableEq α] (x : α) (h : Pr[= x | oa] = 1) : Triple 1 oa fun (y : α) => if y = x then 1 else 0

Exact probability-1 singleton outputs are exact quantitative triples.

theorem OracleComp.ProgramLogic.probOutput_eq_one_iff_triple {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α : Type} (oa : OracleComp spec α) [DecidableEq α] (x : α) : Pr[= x | oa] = 1 ↔ Triple 1 oa fun (y : α) => if y = x then 1 else 0

Pr[= x | oa] = 1 ↔ Triple 1 oa (indicator). Bridge for vcgen probability lowering.

theorem OracleComp.ProgramLogic.triple_support {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α : Type} (oa : OracleComp spec α) [DecidablePred fun (x : α) => x ∈ support oa] : Triple 1 oa fun (x : α) => if x ∈ support oa then 1 else 0

Support membership is a useful default cut function for support-sensitive bind proofs.

Loop stepping rules (Triple-level)

theorem OracleComp.ProgramLogic.triple_replicate_succ {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α : Type} {pre : ENNReal} {oa : OracleComp spec α} {n : ℕ} {post : List α → ENNReal} (h : Triple pre oa fun (x : α) => wp (replicate n oa) fun (xs : List α) => post (x :: xs)) : Triple pre (replicate (n + 1) oa) post

theorem OracleComp.ProgramLogic.triple_list_mapM_cons {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α β : Type} {pre : ENNReal} {x : α} {xs : List α} {f : α → OracleComp spec β} {post : List β → ENNReal} (h : Triple pre (f x) fun (y : β) => wp (List.mapM f xs) fun (ys : List β) => post (y :: ys)) : Triple pre (List.mapM f (x :: xs)) post

theorem OracleComp.ProgramLogic.triple_list_foldlM_cons {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α σ : Type} {pre : ENNReal} {x : α} {xs : List α} {f : σ → α → OracleComp spec σ} {init : σ} {post : σ → ENNReal} (h : Triple pre (f init x) fun (s : σ) => wp (List.foldlM f s xs) post) : Triple pre (List.foldlM f init (x :: xs)) post

Loop invariant rules

theorem OracleComp.ProgramLogic.triple_replicate_inv {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α : Type} {I : ENNReal} {oa : OracleComp spec α} {n : ℕ} (hstep : Triple I oa fun (x : α) => I) : Triple I (replicate n oa) fun (x : List α) => I

Constant invariant through bounded iteration via replicate.

theorem OracleComp.ProgramLogic.triple_list_foldlM_inv {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α σ : Type} {I : σ → ENNReal} {f : σ → α → OracleComp spec σ} {l : List α} {s₀ : σ} (hstep : ∀ (s : σ), ∀ x ∈ l, Triple (I s) (f s x) I) : Triple (I s₀) (List.foldlM f s₀ l) I

Indexed invariant through List.foldlM.

theorem OracleComp.ProgramLogic.triple_list_mapM_inv {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α β : Type} {I : ENNReal} {f : α → OracleComp spec β} {l : List α} (hstep : ∀ x ∈ l, Triple I (f x) fun (x : β) => I) : Triple I (List.mapM f l) fun (x : List β) => I

Constant invariant through List.mapM.

theorem OracleComp.ProgramLogic.triple_replicate {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α : Type} {I pre : ENNReal} {oa : OracleComp spec α} {n : ℕ} {post : List α → ENNReal} (hpre : pre ≤ I) (hpost : ∀ (xs : List α), I ≤ post xs) (hstep : Triple I oa fun (x : α) => I) : Triple pre (replicate n oa) post

replicate invariant with consequence: bridges arbitrary pre/post to the invariant.

theorem OracleComp.ProgramLogic.triple_list_foldlM {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α σ : Type} {I : σ → ENNReal} {f : σ → α → OracleComp spec σ} {l : List α} {s₀ : σ} {pre : ENNReal} {post : σ → ENNReal} (hpre : pre ≤ I s₀) (hpost : ∀ (s : σ), I s ≤ post s) (hstep : ∀ (s : σ), ∀ x ∈ l, Triple (I s) (f s x) I) : Triple pre (List.foldlM f s₀ l) post

List.foldlM invariant with consequence.

theorem OracleComp.ProgramLogic.triple_list_mapM {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α β : Type} {I : ENNReal} {f : α → OracleComp spec β} {l : List α} {pre : ENNReal} {post : List β → ENNReal} (hpre : pre ≤ I) (hpost : ∀ (ys : List β), I ≤ post ys) (hstep : ∀ x ∈ l, Triple I (f x) fun (x : β) => I) : Triple pre (List.mapM f l) post

List.mapM invariant with consequence.

Congruence under evalDist equality

theorem OracleComp.ProgramLogic.probOutput_congr_evalDist {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α : Type} {oa ob : OracleComp spec α} (h : 𝒟[oa] = 𝒟[ob]) (x : α) : Pr[= x | oa] = Pr[= x | ob]

theorem OracleComp.ProgramLogic.μ_congr_evalDist {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {oa ob : OracleComp spec ENNReal} (h : 𝒟[oa] = 𝒟[ob]) : μ oa = μ ob

theorem OracleComp.ProgramLogic.wp_congr_evalDist {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α : Type} {oa ob : OracleComp spec α} (h : 𝒟[oa] = 𝒟[ob]) (post : α → ENNReal) : wp oa post = wp ob post

theorem OracleComp.ProgramLogic.μ_cross_congr_evalDist {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {ι' : Type u_1} {spec' : OracleSpec ι'} [spec'.Fintype] [spec'.Inhabited] {oa : OracleComp spec' ENNReal} {ob : OracleComp spec ENNReal} (h : 𝒟[oa] = 𝒟[ob]) : μ oa = μ ob