Quantitative WP carrier for OracleComp (Loom2 default) #
This file is the home of the quantitative algebra structure on
OracleComp spec valued in ℝ≥0∞, plus its registration as the
default Std.Do'.WP (OracleComp spec) ℝ≥0∞ EPost.nil instance.
It provides three layers:
- Expectation algebra —
μ : OracleComp spec ℝ≥0∞ → ℝ≥0∞and the legacyMAlgOrdered (OracleComp spec) ℝ≥0∞instance. These remain the structural root forOracleComp.ProgramLogic.wp/.Tripleand the relational eRHL stack until the irreversible Commit 8 prunesMAlgOrdered. Lean.Orderadapters forℝ≥0∞— bridges Mathlib's≤andsSupto Lean core'sLean.Order.{PartialOrder, CompleteLattice}, which Loom2 builds on.Propships with its own adapters inLoom/LatticeExt.lean.Std.Do'.WPinstance — the canonical entry point for new program-logic developments. ItswpTranswraps the existingMAlgOrdered.wp, so the keystone alignment lemmawp_eq_mAlgOrdered_wpholds byrfl.
Layout #
This is one of three WP carriers we register on OracleComp. Because
Std.Do'.WP's Pred and EPred are outParams, only one carrier can
be visible to instance synthesis at a time. We register them
asymmetrically:
- This file (
Loom/Quantitative.lean) — theℝ≥0∞carrier as a normalinstance, always live once the file is imported. This is the default. Loom/Qualitative.lean— thePropcarrier as ascoped instanceundernamespace OracleComp.Qualitative, opt-in viaopen OracleComp.Qualitative.Loom/Probabilistic.lean— theProbcarrier as ascoped instanceundernamespace OracleComp.Probabilistic, opt-in viaopen OracleComp.Probabilistic.
There is no umbrella Unary/Loom.lean re-export. Consumers import the
specific carrier they need. This makes the carrier choice explicit at
every import site.
Loom2 vs. Mathlib lattice plumbing #
Loom2 builds on Lean.Order.{PartialOrder, CompleteLattice, CCPO} from
Init.Internal.Order, a class hierarchy distinct from Mathlib's
Order.{PartialOrder, CompleteLattice}. We provide the narrow ℝ≥0∞
adapters here.
When Volo's PR #12965 lands upstream and the Std.Do.{WP,…} API
stabilizes, this bridge collapses to a re-export and the lattice
adapters can move to a shared ToMathlib/Order/LeanOrderAdapter.lean.
Expectation algebra and the MAlgOrdered instance #
Expectation-style algebra for oracle computations returning ℝ≥0∞.
Instances For
Lean.Order adapters for ℝ≥0∞ #
Loom2's Std.Do'.WP m Pred EPred requires Assertion Pred (a class
abbrev for Lean.Order.CompleteLattice). We bridge Mathlib's order
structure on ℝ≥0∞ to Lean core's lattice hierarchy here.
Bridge Mathlib's ≤ on ℝ≥0∞ to Lean.Order.PartialOrder.
Bridge Mathlib's sSup on ℝ≥0∞ to Lean.Order.CompleteLattice.
Lean.Order.CompleteLattice.has_sup c requires a least upper bound for
the predicate-encoded set {x | c x}. We discharge it with Mathlib's
sSup specialization.
Lean.Order.CCPO instance for Std.Do'.EPost.nil #
Loom2's Hoare-triple notation ⦃ pre ⦄ x ⦃ post ⦄ (defined in
Loom.Triple.Basic) expands to Std.Do'.Triple pre x post ⊥ where
⊥ is the Lean.Order.CCPO-bottom (Lean.Order.bot). For monads
with no exception layer, the EPred is Std.Do'.EPost.nil, which
Loom2 ships only with a Lean.Order.CompleteLattice instance, not a
CCPO one. (CCPO and CompleteLattice are independent sibling
classes in Lean core's Init.Internal.Order.)
We provide the missing CCPO instance here. EPost.nil is a
single-element type, so the chain-supremum is trivial: every chain has
the unique element EPost.nil.mk as its least upper bound.
Std.Do'.WP instance for OracleComp #
Quantitative Std.Do'.WP interpretation of OracleComp spec valued in ℝ≥0∞.
The wpTrans is the existing MAlgOrdered.wp (i.e. expectation of
post under evalDist); the EPost.nil argument is ignored since
OracleComp has no first-class exception slot. The three WP axioms
reduce to the existing MAlgOrdered.{wp_pure, wp_bind, wp_mono}
equalities.
Definitional alignment with MAlgOrdered.wp #
The keystone lemma confirms Std.Do'.wp agrees with MAlgOrdered.wp
on the nose, so every existing quantitative wp_* theorem in
HoareTriple.lean transports for free when the user rewrites
Std.Do'.wp _ _ _ ↦ MAlgOrdered.wp _ _.
The epost argument is ⊥ to match Loom2's ⦃ _ ⦄ _ ⦃ _ ⦄ notation in
Loom.Triple.Basic. The WP instance for OracleComp ignores the
epost argument entirely, so any element of EPost.nil would yield the
same value.
Std.Do'.Triple agrees with MAlgOrdered.Triple propositionally.
Use as a forward iff: triple_iff_mAlgOrdered_triple.mp extracts
pre ≤ MAlgOrdered.wp … from a Std.Do'.Triple, and .mpr packages
it back. The two are not definitionally equal because Std.Do'.Triple
is an inductive wrapper rather than a def over ≤.