Probabilistic WP carrier for OracleComp (Prob, scoped)

Installs the probabilistic Std.Do'.WP (OracleComp spec) Prob EPost.nil instance, where Prob = { x : ℝ≥0∞ // x ≤ 1 } is the unit interval as a subtype of ℝ≥0∞. Sitting between the qualitative Prop carrier and the quantitative ℝ≥0∞ carrier, this tier is the natural home for probability-bounded reasoning: union bound, complement (1 - p involution), Bayes, independence, advantage / negligibility.

The carrier is a noncomputable scoped instance under namespace OracleComp.Probabilistic. Consumers open the namespace to enable it.

Why a separate tier (rather than ℝ≥0∞ with side conditions)?

In pure ℝ≥0∞:

• 1 - (1 - p) = p only when p ≤ 1; the side condition is implicit at every step.
• Union bound Pr[A ∪ B] ≤ Pr[A] + Pr[B] requires threading (· : Prop → ℝ≥0∞) indicator coercions through every step.
• Game-hopping uses signed differences |Pr[A] - Pr[B]|; in ℝ≥0∞ you build |·| out of max - min.
• Negligibility lives in [0,1] morally; our Negligible machinery in Asymptotics/ already silently assumes ≤ 1.

Prob makes all of these direct, and lets tactic registries (@[wpStep], @[vcspec]) be partitioned by tier so that wp_prob goals never invoke Markov / KL_div lemmas.

See .ignore/wp-cutover-plan.md §"Three-tier carrier design" for the broader story (Galois connections, coherence lemmas).

The Prob carrier

Prob is the closed unit interval [0, 1] ⊆ ℝ≥0∞. It is a complete bounded lattice under the inherited ≤ from ℝ≥0∞, with sup of any predicate-encoded subset given by sSup (clamped at 1, but the bound follows for free since every element is already ≤ 1).

def Prob : Type

The closed unit interval [0, 1] as a subtype of ℝ≥0∞.

Used as the carrier for the probabilistic Std.Do'.WP interpretation of OracleComp (see OracleComp.Probabilistic.instWP_prob). The Subtype.val coercion to ℝ≥0∞ is free, so probabilistic statements re-export to the quantitative carrier without duplication.

def Prob.val (p : Prob) : ENNReal

Underlying ℝ≥0∞ value.

@[implicit_reducible]

instance Prob.instCoeENNReal : Coe Prob ENNReal

theorem Prob.ext {p q : Prob} (h : ↑p = ↑q) : p = q

theorem Prob.ext_iff {p q : Prob} : p = q ↔ ↑p = ↑q

theorem Prob.val_le_one (p : Prob) : ↑p ≤ 1

The ≤ 1 witness for any Prob.

@[implicit_reducible]

instance Prob.instZero : Zero Prob

@[implicit_reducible]

instance Prob.instOne : One Prob

@[simp]

theorem Prob.val_zero : ↑0 = 0

@[simp]

theorem Prob.val_one : ↑1 = 1

def Prob.indicator (p : Prop) [Decidable p] : Prob

Indicator coercion from a decidable proposition to Prob: 1 if p holds, 0 otherwise. Used to lift a qualitative post α → Prop into a probabilistic post α → Prob, as in OracleComp.Loom.Coherence.wp_qual_iff_wp_prob_indicator_eq_one.

@[simp]

theorem Prob.val_indicator (p : Prop) [Decidable p] : ↑(indicator p) = if p then 1 else 0

Lean.Order instances

Loom2 builds on Lean.Order.{PartialOrder, CompleteLattice} from Lean core's Init.Internal.Order. We provide the bridges for Prob here; the pattern mirrors …/Loom/Quantitative.lean for ℝ≥0∞.

@[implicit_reducible]

instance Prob.instPartialOrder : Lean.Order.PartialOrder Prob

Bridge Subtype ordering on Prob to Lean.Order.PartialOrder.

Definitionally, a ⊑ b ↔ a.val ≤ b.val, so change a.val ≤ b.val unfolds the Lean.Order.PartialOrder.rel projection at proof sites.

noncomputable def Prob.probSup (c : Prob → Prop) : Prob

Supremum on Prob of a predicate-encoded subset.

The supremum on ℝ≥0∞ of any subset of [0,1] is itself in [0,1], since sSup is monotone and bounded above by 1.

theorem Prob.probSup_is_sup (c : Prob → Prop) : Lean.Order.is_sup c (probSup c)

@[implicit_reducible]

noncomputable instance Prob.instCompleteLattice : Lean.Order.CompleteLattice Prob

Bridge sSup on Prob to Lean.Order.CompleteLattice.

The least upper bound of any predicate-encoded subset of Prob exists (it is the sSup in ℝ≥0∞ of the underlying values, which lands in [0,1] because every member already does).

WP instance for OracleComp

The probabilistic WP wraps the existing quantitative MAlgOrdered.wp post-composed with the Prob constructor. The ≤ 1 bound is witnessed by monotonicity of MAlgOrdered.wp against the constant-1 post, which evaluates to 1 on OracleComp (since OracleComp has HasEvalPMF, a true probability monad).

@[implicit_reducible]

noncomputable def OracleComp.Probabilistic.instWP_prob {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] : Std.Do'.WP (OracleComp spec) Prob EPost⟨⟩

Probabilistic Std.Do'.WP interpretation of OracleComp spec valued in Prob = [0, 1] ⊆ ℝ≥0∞.

The wpTrans is the existing quantitative MAlgOrdered.wp evaluated on Prob-valued postconditions and packaged into Prob via the ≤ 1 bound. The EPost.nil argument is ignored since OracleComp has no first-class exception slot.

This is a scoped instance rather than a normal instance: only one Std.Do'.WP (OracleComp spec) _ _ instance can be visible at a time (Pred is an outParam), and the default is the quantitative ℝ≥0∞ carrier. Open OracleComp.Probabilistic to switch into the probabilistic carrier.

Definitional alignment with MAlgOrdered.wp (Prob)

The keystone lemma confirms that the underlying ℝ≥0∞ value of Std.Do'.wp agrees with the quantitative MAlgOrdered.wp on the nose, so quantitative theorems still apply after coercing through .val.

theorem OracleComp.Probabilistic.wp_val_eq_mAlgOrdered_wp {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α : Type} (oa : OracleComp spec α) (post : α → Prob) : ↑(Std.Do'.wp oa post Lean.Order.bot) = MAlgOrdered.wp oa fun (a : α) => ↑(post a)