From 165d24c7215cc60380034d81fea9546e47db50fa Mon Sep 17 00:00:00 2001 From: David Ledvinka Date: Mon, 26 Oct 2026 17:37:35 +0000 Subject: [PATCH 01/13] Start the polymorphic measurable-space monad rebuild --- .github/workflows/build.yml | 4 + RandomDoNext.lean | 10 + RandomDoNext/MeasurableSpaceMonad.lean | 20 ++ RandomDoNext/MeasurableSpaceMonad/Core.lean | 17 ++ .../MeasurableSpaceMonad/Core/Basic.lean | 105 ++++++++ .../MeasurableSpaceMonad/Core/ForIn.lean | 73 ++++++ .../MeasurableSpaceMonad/Core/Lawful.lean | 142 +++++++++++ .../MeasurableSpaceMonad/Notation.lean | 16 ++ .../MeasurableSpaceMonad/Notation/Basic.lean | 81 +++++++ .../MeasurableSpaceMonad/Notation/ForIn.lean | 228 ++++++++++++++++++ TestNext.lean | 6 + TestNext/MeasurableSpaceMonad/Core.lean | 44 ++++ .../MeasurableSpaceMonad/ImportBoundary.lean | 17 ++ TestNext/MeasurableSpaceMonad/Notation.lean | 90 +++++++ .../MeasurableSpaceMonad/NotationBasic.lean | 36 +++ lakefile.toml | 8 +- 16 files changed, 896 insertions(+), 1 deletion(-) create mode 100644 RandomDoNext.lean create mode 100644 RandomDoNext/MeasurableSpaceMonad.lean create mode 100644 RandomDoNext/MeasurableSpaceMonad/Core.lean create mode 100644 RandomDoNext/MeasurableSpaceMonad/Core/Basic.lean create mode 100644 RandomDoNext/MeasurableSpaceMonad/Core/ForIn.lean create mode 100644 RandomDoNext/MeasurableSpaceMonad/Core/Lawful.lean create mode 100644 RandomDoNext/MeasurableSpaceMonad/Notation.lean create mode 100644 RandomDoNext/MeasurableSpaceMonad/Notation/Basic.lean create mode 100644 RandomDoNext/MeasurableSpaceMonad/Notation/ForIn.lean create mode 100644 TestNext.lean create mode 100644 TestNext/MeasurableSpaceMonad/Core.lean create mode 100644 TestNext/MeasurableSpaceMonad/ImportBoundary.lean create mode 100644 TestNext/MeasurableSpaceMonad/Notation.lean create mode 100644 TestNext/MeasurableSpaceMonad/NotationBasic.lean diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index 550a3a1..11b98c2 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -7,6 +7,7 @@ on: pull_request: branches: - main + - 'codex/rebuild-*' workflow_dispatch: # Allow manual triggering of the workflow from the GitHub Actions interface # Cancel previous runs if a new commit is pushed to the same PR or branch @@ -54,3 +55,6 @@ jobs: build-args: "--wfail" lint: true mk_all-check: true + + - name: Build rebuilt library tests + run: lake build --wfail TestNext diff --git a/RandomDoNext.lean b/RandomDoNext.lean new file mode 100644 index 0000000..996b532 --- /dev/null +++ b/RandomDoNext.lean @@ -0,0 +1,10 @@ +module -- shake: keep-all --deprecated_module: ignore + +public import RandomDoNext.MeasurableSpaceMonad +public import RandomDoNext.MeasurableSpaceMonad.Core +public import RandomDoNext.MeasurableSpaceMonad.Core.Basic +public import RandomDoNext.MeasurableSpaceMonad.Core.ForIn +public import RandomDoNext.MeasurableSpaceMonad.Core.Lawful +public import RandomDoNext.MeasurableSpaceMonad.Notation +public import RandomDoNext.MeasurableSpaceMonad.Notation.Basic +public import RandomDoNext.MeasurableSpaceMonad.Notation.ForIn diff --git a/RandomDoNext/MeasurableSpaceMonad.lean b/RandomDoNext/MeasurableSpaceMonad.lean new file mode 100644 index 0000000..5eb6dac --- /dev/null +++ b/RandomDoNext/MeasurableSpaceMonad.lean @@ -0,0 +1,20 @@ +/- +Copyright (c) 2026 David Ledvinka. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: David Ledvinka +-/ +module + +public import RandomDoNext.MeasurableSpaceMonad.Core +public import RandomDoNext.MeasurableSpaceMonad.Notation + +/-! +# Measurable-space monads + +The polymorphic foundation of the rebuilt library. `Core` contains operations, laws, and +iteration interfaces; `Notation` contains their `rdo` elaborators. Concrete interpretations +and sampling implementations belong outside this subtree. + +`RandomDoNext` is the staging module root. Declaration namespaces already use `RandomDo`, so +promoting the library will change module paths without renaming its mathematical API. +-/ diff --git a/RandomDoNext/MeasurableSpaceMonad/Core.lean b/RandomDoNext/MeasurableSpaceMonad/Core.lean new file mode 100644 index 0000000..a21d7b8 --- /dev/null +++ b/RandomDoNext/MeasurableSpaceMonad/Core.lean @@ -0,0 +1,17 @@ +/- +Copyright (c) 2026 David Ledvinka. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: David Ledvinka +-/ +module + +public import RandomDoNext.MeasurableSpaceMonad.Core.Basic +public import RandomDoNext.MeasurableSpaceMonad.Core.ForIn +public import RandomDoNext.MeasurableSpaceMonad.Core.Lawful + +/-! +# Polymorphic measurable-space monad theory + +Operations, conditional laws, and iteration interfaces, independent of any concrete monad. +Import `RandomDoNext.MeasurableSpaceMonad.Notation` as well to write programs using `rdo`. +-/ diff --git a/RandomDoNext/MeasurableSpaceMonad/Core/Basic.lean b/RandomDoNext/MeasurableSpaceMonad/Core/Basic.lean new file mode 100644 index 0000000..18b112d --- /dev/null +++ b/RandomDoNext/MeasurableSpaceMonad/Core/Basic.lean @@ -0,0 +1,105 @@ +/- +Copyright (c) 2026 David Ledvinka. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: David Ledvinka +-/ +module + +public import Mathlib.MeasureTheory.MeasurableSpace.Defs + +/-! +# Operations on measurable-space monads + +A measurable-space monad takes a result type together with its measurable-space instance: +`m : (α : Type u) → [MeasurableSpace α] → Type v`. The classes in this file follow the separation +of `Functor`, `Pure`, `Bind`, and `Monad` in `Init/Core.lean`. + +The operations accept ordinary functions. Measurability assumptions belong to the laws in +`RandomDoNext.MeasurableSpaceMonad.Core.Lawful`, so constructing a program does not require +proving its measurability. The operational classes alone assert no laws. + +Declarations live in `RandomDo`. Opening this namespace also enables the scoped mapping +notation `<$>ₘ` and sequencing notation `>>=ₘ`. + +Adapted from `RandomDo/Monad/MeasurableSpace.lean` at main commit `150ecab`. +-/ + +@[expose] public section + +namespace RandomDo + +open Function + +universe u v + +/-- A functor on types with a `MeasurableSpace` instance. The `mMap` operator `<$>ₘ` is overloaded +via instances of this class. This class does not require proofs of the `MeasurableSpaceFunctor` +axioms. Proofs may be provided or required via the `LawfulMeasurableSpaceFunctor` class. -/ +class MeasurableSpaceFunctor (f : (α : Type u) → [MeasurableSpace α] → Type v) : + Type (max (u+1) v) where + /-- + Applies a function inside a functor on measurable spaces. This is used to overload the + `<$>ₘ` operator. + + When mapping a constant function (if one cares about executing the code), use + `MeasurableSpaceFunctor.mMapConst` instead, because it may be more efficient. + -/ + mMap {α β : Type u} [MeasurableSpace α] [MeasurableSpace β] : (α → β) → f α → f β + /-- + Mapping a constant function. + + Given `a : α` and `v : f β`, `mMapConst a v` is equivalent to `(fun _ => a) <$>ₘ v`. For some + functors, this can be implemented more efficiently; for all other functors, the default + implementation may be used. + -/ + mMapConst {α β : Type u} [MeasurableSpace α] [MeasurableSpace β] : α → f β → f α := + mMap ∘ (const _) + +@[inherit_doc] scoped infixr:100 " <$>ₘ " => MeasurableSpaceFunctor.mMap + +/-- +The `mPure` function is overloaded via `MeasurableSpacePure` instances. + +`MeasurableSpacePure` is typically accessed via `MeasurableSpaceMonad` instances, which extend it. +-/ +class MeasurableSpacePure (f : (α : Type u) → [MeasurableSpace α] → Type v) where + /-- Given `a : α` where `α` has a `MeasurableSpace` instance, `mPure a : f α` represents an + action that does nothing and returns `a`. -/ + mPure {α : Type u} [MeasurableSpace α] : α → f α + +/-- +The `>>=ₘ` operator is overloaded via instances of `MeasurableSpaceBind`. + +`MeasurableSpaceBind` is typically used via `MeasurableSpaceMonad`, which extends it. +-/ +class MeasurableSpaceBind (m : (α : Type u) → [MeasurableSpace α] → Type v) where + /-- + Sequences two computations, allowing the second to depend on the value computed by the first. + + If `x : m α` and `f : α → m β`, then `x >>=ₘ f : m β` represents the result of executing `x` + to get a value of type `α` and then passing it to `f`. + -/ + mBind {α β : Type u} [MeasurableSpace α] [MeasurableSpace β] : m α → (α → m β) → m β + +@[inherit_doc] scoped infixl:55 " >>=ₘ " => MeasurableSpaceBind.mBind + +/-- Return, sequencing, and mapping for computations indexed by measurable result types. +By default, mapping sequences a computation with return. The operations accept ordinary functions; +measurability assumptions and laws are supplied separately by `LawfulMeasurableSpaceMonad`. -/ +class MeasurableSpaceMonad (m : (α : Type u) → [MeasurableSpace α] → Type v) : + Type (max (u+1) v) + extends MeasurableSpaceFunctor m, MeasurableSpacePure m, MeasurableSpaceBind m where + mMap f μ := mBind μ (Function.comp mPure f) + +variable {m : (α : Type u) → [MeasurableSpace α] → Type v} {α β : Type u} + [MeasurableSpace α] [MeasurableSpace β] + +theorem MeasurableSpaceBind.bind_congr [MeasurableSpaceBind m] {x : m α} {f g : α → m β} + (h : ∀ a, f a = g a) : x >>=ₘ f = x >>=ₘ g := by + simp [funext h] + +theorem MeasurableSpaceFunctor.map_congr [MeasurableSpaceFunctor m] {x : m α} {f g : α → β} + (h : ∀ a, f a = g a) : (f <$>ₘ x : m β) = g <$>ₘ x := by + simp [funext h] + +end RandomDo diff --git a/RandomDoNext/MeasurableSpaceMonad/Core/ForIn.lean b/RandomDoNext/MeasurableSpaceMonad/Core/ForIn.lean new file mode 100644 index 0000000..d47be09 --- /dev/null +++ b/RandomDoNext/MeasurableSpaceMonad/Core/ForIn.lean @@ -0,0 +1,73 @@ +/- +Copyright (c) 2026 David Ledvinka. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: David Ledvinka, Gaëtan Serré +-/ +module + +public import RandomDoNext.MeasurableSpaceMonad.Core.Basic +public import Mathlib.MeasureTheory.MeasurableSpace.Basic + +/-! +# Polymorphic iteration interfaces + +`MeasurableSpaceForIn` and `MeasurableSpaceForIn'` are the measurable-space counterparts of +Lean's iteration classes. The accumulator has a measurable space, and each step either yields +an updated accumulator or stops the loop. + +The measurable spaces on `ForInStep` and `Option`, and the adapter from membership-aware +iteration, are generic in the monad. Implementations for particular collections or monads belong +in separate modules. +No unbounded-loop operation or semantics is chosen here. + +Adapted from `RandomDo/Monad/MeasurableSpace.lean` and the optional-value instance in +`RandomDo/Measurable.lean` at main commit `150ecab`. +-/ + +@[expose] public section + +namespace RandomDo + +universe uρ uα u v + +variable {α : Type u} [mα : MeasurableSpace α] (m : (α : Type u) → [MeasurableSpace α] → Type v) + +/-- The measurable space on optional results used to carry an early return. +A set of optional values is measurable exactly when its `some` preimage is measurable. -/ +instance instMeasurableSpaceOption : MeasurableSpace (Option α) := mα.map some + +/-- The disjoint-union measurable space on the two possible loop-step outcomes. -/ +instance instMeasurableSpaceForInStep {β : Type u} [mβ : MeasurableSpace β] : + MeasurableSpace (ForInStep β) := mβ.map ForInStep.yield ⊓ mβ.map ForInStep.done + +/-- +Monadic iteration in `rdo`-blocks, using the `for x in xs` notation. +-/ +class MeasurableSpaceForIn (ρ : Type uρ) (α : outParam (Type uα)) where + /-- + Monadically iterates over the contents of a collection `xs`, with a local state `b` and the + possibility of early termination. + -/ + forIn {β : Type u} [MeasurableSpace β] (xs : ρ) (b : β) + (f : α → β → m (ForInStep β)) : m β + +/-- +Monadic iteration in `rdo`-blocks with a membership proof, using the `for h : x in xs` notation. +-/ +class MeasurableSpaceForIn' (ρ : Type uρ) (α : outParam (Type uα)) + (d : outParam (Membership α ρ)) where + /-- + Monadically iterates over the contents of a collection `xs`, with a local state `b` and the + possibility of early termination. At each iteration, the body of the loop is provided with a proof + that the current element is in the collection. + -/ + forIn' {β : Type u} [MeasurableSpace β] (xs : ρ) (b : β) + (f : (a : α) → a ∈ xs → β → m (ForInStep β)) : m β + +@[simps] +instance (priority := 500) instMeasurableSpaceForInOfForIn' + {ρ : Type uρ} {α : Type uα} {d : Membership α ρ} [MeasurableSpaceForIn' m ρ α d] : + MeasurableSpaceForIn m ρ α where + forIn x b f := MeasurableSpaceForIn'.forIn' x b fun a _ s => f a s + +end RandomDo diff --git a/RandomDoNext/MeasurableSpaceMonad/Core/Lawful.lean b/RandomDoNext/MeasurableSpaceMonad/Core/Lawful.lean new file mode 100644 index 0000000..7f8f231 --- /dev/null +++ b/RandomDoNext/MeasurableSpaceMonad/Core/Lawful.lean @@ -0,0 +1,142 @@ +/- +Copyright (c) 2026 David Ledvinka. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: David Ledvinka +-/ +module + +public import RandomDoNext.MeasurableSpaceMonad.Core.Basic +public import Mathlib.MeasureTheory.MeasurableSpace.Constructions +public import Mathlib.Tactic.FunProp + +/-! +# Laws of measurable-space functors and monads + +The lawfulness classes require a measurable space on each computation type `m α`. They state +functor and monad laws for measurable maps and continuations, together with measurability of +mapping, return, and sequencing. Composition and sequencing laws carry explicit measurability +hypotheses. + +The type constructor and its operations remain abstract throughout this file. In particular, +there are no assumptions about probability, sampling, or a choice of interpretation. + +These are the laws from `RandomDo/Monad/MeasurableSpace.lean` at main commit `150ecab`, following +`Init/Control/Lawful/Basic.lean`. The simplifier attributes apply to the measurable-space laws +rather than similarly named laws for ordinary monads. +-/ + +@[expose] public section + +namespace RandomDo + +open Function + +universe u v + +open MeasurableSpaceFunctor + +/-- A `MeasurableSpaceFunctor` satisfies the measurable space functor laws. -/ +class LawfulMeasurableSpaceFunctor + (f : (α : Type u) → [MeasurableSpace α] → Type v) [MeasurableSpaceFunctor f] + [∀ α, [MeasurableSpace α] → MeasurableSpace (f α)] : Prop where + /-- `mMap` of a measurable function is a measurable function. -/ + measurable_mMap {α β : Type u} [MeasurableSpace α] [MeasurableSpace β] + {g : α → β} (hg : Measurable g) : Measurable ((g <$>ₘ ·) : f α → f β) + /-- The `mMapConst` implementation is equivalent to the default implementation. -/ + mMap_const {α β : Type u} [MeasurableSpace α] [MeasurableSpace β] : + (mMapConst : α → f β → f α) = mMap ∘ const β + /-- `mMap` preserves identity. -/ + id_mMap {α : Type u} [MeasurableSpace α] (x : f α) : id <$>ₘ x = x + /-- `mMap` preserves function composition of measurable functions. -/ + comp_mMap {α β γ : Type u} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] + {g₀ : α → β} {g₁ : β → γ} (x : f α) (hg₀ : Measurable g₀) (hg₁ : Measurable g₁) : + (g₁ ∘ g₀) <$>ₘ x = g₁ <$>ₘ g₀ <$>ₘ x + +open LawfulMeasurableSpaceFunctor + +attribute [fun_prop] measurable_mMap +attribute [simp] id_mMap + +variable {f : (α : Type u) → [MeasurableSpace α] → Type v} [MeasurableSpaceFunctor f] + [∀ α, [MeasurableSpace α] → MeasurableSpace (f α)] [LawfulMeasurableSpaceFunctor f] + {α β γ : Type u} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] + +@[simp] theorem id_mMap' (x : f α) : (fun a => a) <$>ₘ x = x := id_mMap x + +@[simp] theorem mMap_mMap {g₀ : α → β} {g₁ : β → γ} (x : f α) + (hg₀ : Measurable g₀) (hg₁ : Measurable g₁) : + g₁ <$>ₘ g₀ <$>ₘ x = (fun a => g₁ (g₀ a)) <$>ₘ x := + (comp_mMap x hg₀ hg₁).symm + +open MeasurableSpaceBind MeasurableSpacePure MeasurableSpaceFunctor + +/-- A `MeasurableSpaceMonad` satisfies the measurable space monad laws. -/ +class LawfulMeasurableSpaceMonad + (m : (α : Type u) → [MeasurableSpace α] → Type v) [MeasurableSpaceMonad m] + [∀ α, [MeasurableSpace α] → MeasurableSpace (m α)] : Prop + extends LawfulMeasurableSpaceFunctor m where + /-- `mPure` is a measurable function. -/ + measurable_mPure {α : Type u} [MeasurableSpace α] : Measurable (mPure : α → m α) + /-- `mBind` of a measurable function is a measurable function. -/ + measurable_mBind {α β : Type u} [MeasurableSpace α] [MeasurableSpace β] + {f : α → m β} (hf : Measurable f) : Measurable (fun x : m α => x >>=ₘ f) + /-- A `mBind` followed by `mPure` composed with a measurable function is equivalent to a + functorial map. -/ + mBind_mPure_comp {α β : Type u} [MeasurableSpace α] [MeasurableSpace β] + {f : α → β} (hf : Measurable f) (x : m α) : + x >>=ₘ (fun a => mPure (f a)) = f <$>ₘ x + /-- `mPure` followed by `mBind` of a function application is equivalent to function + application. -/ + mPure_mBind {α β : Type u} [MeasurableSpace α] [MeasurableSpace β] + (x : α) {f : α → m β} (hf : Measurable f) : + mPure x >>=ₘ f = f x + /-- `mBind` is associative on measurable functions. -/ + mBind_assoc {α β γ : Type u} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] + (x : m α) {f : α → m β} {g : β → m γ} (hf : Measurable f) (hg : Measurable g) : + x >>=ₘ f >>=ₘ g = x >>=ₘ fun x => f x >>=ₘ g + measurable_mMap hg := (by + convert measurable_mBind (measurable_mPure.comp hg) + exact (mBind_mPure_comp hg _).symm) + comp_mMap x g_meas h_meas := (by + rw [← mBind_mPure_comp (by fun_prop), ← mBind_mPure_comp h_meas, + ← mBind_mPure_comp g_meas, mBind_assoc _ (by fun_prop) (by fun_prop)] + congr with _ + exact (mPure_mBind _ (measurable_mPure.comp h_meas)).symm) + +open LawfulMeasurableSpaceMonad + +attribute [fun_prop] measurable_mPure measurable_mBind +attribute [simp] mPure_mBind mBind_assoc mBind_mPure_comp +attribute [grind <=] mPure_mBind + +variable {m : (α : Type u) → [MeasurableSpace α] → Type v} [MeasurableSpaceMonad m] + [∀ α, [MeasurableSpace α] → MeasurableSpace (m α)] [LawfulMeasurableSpaceMonad m] + {α β γ : Type u} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] + +@[simp] theorem mMap_mPure {f : α → β} (hf : Measurable f) (x : α) : + f <$>ₘ (mPure x : m α) = mPure (f x) := by + rw [← mBind_mPure_comp hf, mPure_mBind _ (by fun_prop)] + +@[simp] theorem mBind_mPure (x : m α) : x >>=ₘ mPure = x := by + change x >>=ₘ (fun a => (mPure (id a))) = x + rw [mBind_mPure_comp (by fun_prop), id_mMap] + +theorem mMap_eq_mPure_mBind {f : α → β} (hf : Measurable f) (x : m α) : + f <$>ₘ x = x >>=ₘ fun a => mPure (f a) := by + rw [← mBind_mPure_comp hf x] + +theorem mBind_mPure_unit {x : m PUnit} : (x >>=ₘ fun _ => mPure ⟨⟩) = x := by rw [mBind_mPure] + +@[simp] theorem mMap_mBind {f : β → γ} (hf : Measurable f) (x : m α) + {g : α → m β} (hg : Measurable g) : + f <$>ₘ (x >>=ₘ g) = x >>=ₘ fun a => f <$>ₘ g a := by + rw [← mBind_mPure_comp hf, mBind_assoc _ hg (by fun_prop)] + simp (disch := fun_prop) [mBind_mPure_comp] + +@[simp] theorem mBind_mMap_left {f : α → β} (hf : Measurable f) (x : m α) + {g : β → m γ} (hg : Measurable g) : + ((f <$>ₘ x) >>=ₘ fun b => g b) = (x >>=ₘ fun a => g (f a)) := by + rw [← mBind_mPure_comp hf] + simp (disch := fun_prop) only [mBind_assoc, mPure_mBind] + +end RandomDo diff --git a/RandomDoNext/MeasurableSpaceMonad/Notation.lean b/RandomDoNext/MeasurableSpaceMonad/Notation.lean new file mode 100644 index 0000000..4680585 --- /dev/null +++ b/RandomDoNext/MeasurableSpaceMonad/Notation.lean @@ -0,0 +1,16 @@ +/- +Copyright (c) 2026 David Ledvinka. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: David Ledvinka +-/ +module + +public import RandomDoNext.MeasurableSpaceMonad.Notation.Basic +public import RandomDoNext.MeasurableSpaceMonad.Notation.ForIn + +/-! +# Syntax for polymorphic measurable-space monad programs + +Provides `rdo` and collection iteration. The operations and iteration instances are supplied +by the caller; importing this module does not select a concrete interpretation. +-/ diff --git a/RandomDoNext/MeasurableSpaceMonad/Notation/Basic.lean b/RandomDoNext/MeasurableSpaceMonad/Notation/Basic.lean new file mode 100644 index 0000000..41a7dd7 --- /dev/null +++ b/RandomDoNext/MeasurableSpaceMonad/Notation/Basic.lean @@ -0,0 +1,81 @@ +/- +Copyright (c) 2026 David Ledvinka. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: David Ledvinka +-/ +module + +public import RandomDoNext.MeasurableSpaceMonad.Core.Basic +public import Mathlib.MeasureTheory.MeasurableSpace.Prod +public meta import Lean.Elab.BuiltinDo + +/-! +# `rdo` notation + +`rdo` elaborates a program using the measurable-space operations `mPure` and `mBind`. +It reuses Lean's `do` elaborators for binding, branching, mutation, and early return, supplying +the additional measurable-space argument when constructing a computation type or operation. + +`randOps` adapts `DoOps.default` from `Lean/Elab/Do/Basic.lean`. Collection iteration is provided +separately by `RandomDoNext.MeasurableSpaceMonad.Notation.ForIn`. + +Adapted from `RandomDo/Monad/Notation.lean` at main commit `150ecab`. No concrete monad instance +is needed to elaborate a polymorphic program. +-/ + +open Lean Lean.Parser Lean.Parser.Term Lean.Meta Lean.Elab Lean.Elab.Do Lean.Elab.Term Std Meta +open RandomDo MeasurableSpacePure MeasurableSpaceBind + +public meta section + +namespace RandomDo.RDo + +/-- Define `DoOp`s for `rdo` notation. -/ +def randOps : DoOps := { DoOps.default with + mkPureApp α e := do + let ⟨m, u, v, _, _⟩ := (← read).monadInfo + let α ← Term.ensureHasType (mkSort (mkLevelSucc u)) α + let e ← Term.ensureHasType α e + let instPure ← mkInstMVar (.app (mkConst ``MeasurableSpacePure [u,v]) m) + let instPure ← instantiateMVars instPure + let σ ← mkInstMVar (.app (mkConst ``MeasurableSpace [u]) α) + let σ ← instantiateMVars σ + return mkAppN (mkConst ``mPure [u, v]) #[m, instPure, α, σ, e] + mkBindApp α β e k := do + let ⟨m, u, v, _, _⟩ := (← read).monadInfo + let α ← Term.ensureHasType (mkSort (mkLevelSucc u)) α + let σα ← mkInstMVar (.app (mkConst ``MeasurableSpace [u]) α) + let σβ ← mkInstMVar (.app (mkConst ``MeasurableSpace [u]) β) + let mα := mkApp2 m α σα + let mβ := mkApp2 m β σβ + let e ← Term.ensureHasType mα e + let k ← Term.ensureHasType (← mkArrow α mβ) k + let σα ← instantiateMVars σα + let σβ ← instantiateMVars σβ + let instBind ← mkInstMVar (.app (mkConst ``MeasurableSpaceBind [u, v]) m) + let instBind ← instantiateMVars instBind + return mkAppN (mkConst ``mBind [u, v]) #[m, instBind, α, β, σα, σβ, e, k] + isPureApp? e := + if e.isAppOfArity ``mPure 5 then some (e.getArg! 4) else none + splitMonadApp? type := do + let .app m _ := type.consumeMData | return none + let .app m resultType := m.consumeMData | return none + unless ← isType resultType do return none + let u ← getDecLevel resultType + let v ← getDecLevel type + return some ({ m := m, u := u.normalize, v := v.normalize }, resultType) + mkMonadApp α := do + let ⟨m, u, _, _, _⟩ := (← read).monadInfo + let σ ← mkInstMVar (mkApp (mkConst ``MeasurableSpace [u]) α) + return mkApp2 m α σ + } + +/-- The `do` notation for writing monadic programs depending on a `MeasurableSpace` instance. -/ +syntax (name := randKind) "rdo" doSeq : term + +/-- Define `rdo` notation elaborator. -/ +@[term_elab randKind] def elabRand : Term.TermElab := fun stx et? => do + let `(rdo $doSeq) := stx | throwUnsupportedSyntax + elabDoWith randOps doSeq et? + +end RandomDo.RDo diff --git a/RandomDoNext/MeasurableSpaceMonad/Notation/ForIn.lean b/RandomDoNext/MeasurableSpaceMonad/Notation/ForIn.lean new file mode 100644 index 0000000..1548c44 --- /dev/null +++ b/RandomDoNext/MeasurableSpaceMonad/Notation/ForIn.lean @@ -0,0 +1,228 @@ +/- +Copyright (c) 2026 David Ledvinka. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: David Ledvinka +-/ +module + +public import RandomDoNext.MeasurableSpaceMonad.Core.ForIn +public import RandomDoNext.MeasurableSpaceMonad.Notation.Basic +public meta import Lean.Meta.ProdN + +/-! +# Collection iteration in `rdo` + +`for x in xs rdo body` uses `MeasurableSpaceForIn`; `for h : x in xs rdo body` uses +`MeasurableSpaceForIn'` and supplies a membership proof. The elaborator carries mutable state, +`break`, `continue`, and early returns through the loop accumulator. + +The parser and elaborator are adapted from `RandomDo/Monad/Notation.lean` at main commit +`150ecab`, which mirrors `Lean/Parser/Do.lean` and `Lean/Elab/BuiltinDo/For.lean`. The control-info +handler from the `loops` branch at `c0f8f5b` also supports nested loops. While-loop syntax and +interpretations are left to a later change. + +There are no collection or monad implementations here: a polymorphic caller supplies the +appropriate iteration instance. +-/ + +open Lean Lean.Parser Lean.Parser.Term Lean.Meta Lean.Elab Lean.Elab.Do Lean.Elab.Term Std Meta +open RandomDo MeasurableSpacePure MeasurableSpaceBind + +public meta section + +namespace RandomDo.RDo + +/-- parses `_ : _ in` for `rdo` for loops -/ +def rdoForDecl := leading_parser + Lean.Parser.optional (atomic (Term.ident >> " : ")) >> termParser >> " in " >> + withForbidden "rdo" termParser + +/-- parser for `rdo` for loops -/ +@[doElem_parser] def rdoFor := leading_parser + "for " >> sepBy1 rdoForDecl ", " >> "rdo " >> doSeq + +/-- Define expander for loops in `rdo` notation. Note this code mirrors core's implementation for +`do` notation as much as possible. -/ +@[macro rdoFor] def expandRDoFor : Macro := fun stx => do + match stx with + | `(rdoFor| for $[$_ : ]? $_:ident in $_ rdo $_) => + -- This is the target form of the expander, handled by `elabRDoFor` below. + Macro.throwUnsupported + | `(rdoFor| for%$tk $decls:rdoForDecl,* rdo $body) => + let decls := decls.getElems + let `(rdoForDecl| $[$h? : ]? $pattern in $xs) := decls[0]! | Macro.throwUnsupported + let mut doElems := #[] + let mut body := body + -- Expand `pattern` into an `Ident` `x`: + let x ← + if pattern.raw.isIdent then + pure ⟨pattern⟩ + else if pattern.raw.isOfKind ``Lean.Parser.Term.hole then + Term.mkFreshIdent pattern + else + -- This case is a last resort, because it introduces a `match` and that will cause eager + -- defaulting. In practice this means that `mut` vars default to `Nat` too often. + -- Hence we try to only generate a `match` if we absolutely must. + let x ← Term.mkFreshIdent pattern + body ← `(doSeq| match $x:term with | $pattern => $body) + pure x + -- Expand the remaining `rdoForDecl`s: + for rdoForDecl in decls[1...*] do + /- + Expand + ``` + for x in xs, y in ys rdo + body + ``` + into + ``` + let mut s := Std.toStream ys + for x in xs rdo + match Std.Stream.next? s with + | none => break + | some (y, s') => + s := s' + body + ``` + -/ + let `(rdoForDecl| $[$h? : ]? $y in $ys) := rdoForDecl | Macro.throwUnsupported + if let some h := h? then + Macro.throwErrorAt h "The proof annotation here has not been implemented yet." + /- Recall that `@` (explicit) disables `coeAtOutParam`. + We used `@` at `Stream` functions to make sure `resultIsOutParamSupport` is not used. -/ + let toStreamApp ← withRef ys `(@Std.toStream _ _ _ $ys) + let s := mkIdentFrom ys (← withFreshMacroScope <| MonadQuotation.addMacroScope `__s) + doElems := doElems.push (← `(doSeqItem| let mut $s := $toStreamApp:term)) + body ← `(doSeq| + match @Std.Stream.next? _ _ _ $s with + | none => break + | some ($y, s') => + $s:ident := s' + do $body) + doElems := doElems.push (← `(doSeqItem| for%$tk $[$h? : ]? $x:ident in $xs rdo $body)) + `(doElem| do $doElems*) + | _ => Macro.throwUnsupported + +/-- Define loop elaborator for `rdo` notation. Note this code mirrors core's implementation for +`do` notation as much as possible. -/ +@[doElem_elab rdoFor] def elabRDoFor : DoElab := fun stx dec => do + let `(rdoFor| for%$tk $[$h? : ]? $x:ident in $xs rdo $body) := stx | throwUnsupportedSyntax + let dec ← dec.ensureUnitAt tk + checkMutVarsForShadowing #[x] + let uα ← mkFreshLevelMVar + let uρ ← mkFreshLevelMVar + let α ← mkFreshExprMVar (mkSort (uα.succ)) (userName := `α) -- assigned by outParam + let ρ ← mkFreshExprMVar (mkSort (uρ.succ)) (userName := `ρ) -- assigned in the next line + let xs ← Term.elabTermEnsuringType xs ρ + let mi := (← read).monadInfo + let mutVars := (← read).mutVars + let info ← inferControlInfoSeq body + let oldReturnCont ← getReturnCont + let returnVarName ← mkFreshUserName `__r + let loopMutVars := mutVars.filter fun x => info.reassigns.contains x.getId + let loopMutVarNames := + if info.returnsEarly then + returnVarName :: (loopMutVars.map (·.getId)).toList + else + (loopMutVars.map (·.getId)).toList + let useLoopMutVars (e : Option Expr) : TermElabM (Array Expr) := do + let mut defs := #[] + unless e.isNone || info.returnsEarly do + throwError "Early returning {e} but the info said there is no early return" + if info.returnsEarly then + let returnVar ← + match e with + | none => mkNone oldReturnCont.resultType + | some e => mkSome oldReturnCont.resultType e + defs := defs.push returnVar + for x in loopMutVars do + let defn ← getLocalDeclFromUserName x.getId + Term.addTermInfo' x.ident defn.toExpr + -- ForIn forces the mut tuple into the universe mi.u: that of the do block result type. + -- If we don't do this, then we are stuck on solving constraints such as + -- `max ?u.46 ?u.47 =?= max (max ?u.22 ?u.46) ?u.47` + -- It's important we do this as a separate isLevelDefEq check on the decremented level because + -- otherwise (`ensureHasType (mkSort mi.u.succ)`) we are stuck on constraints like + -- `max (?u+1) (?v+1) =?= ?u+1` + let u ← getDecLevel defn.type + discard <| isLevelDefEq u mi.u + defs := defs.push defn.toExpr + if info.returnsEarly && loopMutVars.isEmpty then + defs := defs.push (mkConst ``Unit.unit) + return defs + let (preS, σ) ← mkProdMkN (← useLoopMutVars none) mi.u + let mσ ← Term.mkInstMVar <| mkApp (mkConst ``MeasurableSpace [mi.u]) σ + let (app, p?) ← match h? with + | none => + let instForIn ← Term.mkInstMVar <| + mkApp3 (mkConst ``MeasurableSpaceForIn [uρ, uα, mi.u, mi.v]) mi.m ρ α + let app := Lean.mkConst ``MeasurableSpaceForIn.forIn [uρ, uα, mi.u, mi.v] + let app := mkApp8 app mi.m ρ α instForIn σ mσ xs preS + pure (app, none) + | some _ => + let d ← mkFreshExprMVar (mkApp2 (mkConst ``Membership [uα, uρ]) α ρ) (userName := `d) + let instForIn ← Term.mkInstMVar <| + mkApp4 (mkConst ``MeasurableSpaceForIn' [uρ, uα, mi.u, mi.v]) mi.m ρ α d + let app := Lean.mkConst ``MeasurableSpaceForIn'.forIn' [uρ, uα, mi.u, mi.v] + let app := mkApp9 app mi.m ρ α d instForIn σ mσ xs preS + pure (app, some d) + let s ← mkFreshUserName `__s + let xh : Array (Name × (Array Expr → DoElabM Expr)) := match h?, p? with + | some h, some d => + #[(x.getId, fun _ => pure α), + (h.getId, fun x => pure (mkApp5 (mkConst ``Membership.mem [uα, uρ]) α ρ d xs x[0]!))] + | _, _ => + #[(x.getId, fun _ => pure α)] + let body ← + withLocalDeclsD xh fun xh => do + Term.addLocalVarInfo x xh[0]! + if let some h := h? then + Term.addLocalVarInfo h xh[1]! + withLocalDecl s .default σ (kind := .implDetail) fun loopS => do + mkLambdaFVars (xh.push loopS) <| ← do + bindMutVarsFromTuple loopMutVarNames loopS.fvarId! do + let newDoBlockResultType := mkApp (mkConst ``ForInStep [mi.u]) σ + withDoBlockResultType newDoBlockResultType do + let continueCont := do + let (tuple, _tupleTy) ← mkProdMkN (← useLoopMutVars none) mi.u + let yield := mkApp2 (mkConst ``ForInStep.yield [mi.u]) σ tuple + mkPureApp newDoBlockResultType yield + let breakCont := do + let (tuple, _tupleTy) ← mkProdMkN (← useLoopMutVars none) mi.u + let done := mkApp2 (mkConst ``ForInStep.done [mi.u]) σ tuple + mkPureApp newDoBlockResultType done + let returnCont := { oldReturnCont with k := fun e => do + let (tuple, _tupleTy) ← mkProdMkN (← useLoopMutVars (some e)) mi.u + let done := mkApp2 (mkConst ``ForInStep.done [mi.u]) σ tuple + mkPureApp newDoBlockResultType done + } + enterLoopBody breakCont continueCont returnCont do + -- Elaborate the loop body, which must have result type `PUnit`, just like the whole `for` loop. + elabDoSeq body { dec with k := continueCont, kind := .duplicable } + let forIn := mkApp app body + let γ := (← read).doBlockResultType + let rest ← + withLocalDeclD s σ fun postS => do mkLambdaFVars #[postS] <| ← do + bindMutVarsFromTuple loopMutVarNames postS.fvarId! do + if info.returnsEarly then + let ret ← getFVarFromUserName returnVarName + let ret ← if loopMutVars.isEmpty then mkAppM ``Prod.fst #[ret] else pure ret + /- Both branches produce an `m γ`, so the motive is constant and the matcher generated + for `Break.runK` is not needed: `Break.runK` itself is that case analysis. Note that it + takes the `none` branch first, the other way round from the matcher. -/ + let none := mkSimpleThunk (← dec.continueWithUnit) + let some ← withLocalDeclD (← mkFreshUserName `r) oldReturnCont.resultType fun r => do + mkLambdaFVars #[r] (← oldReturnCont.k r) + return mkAppN (mkConst ``Break.runK [mi.u, mi.v]) + #[oldReturnCont.resultType, ← mkMonadApp γ, ret, none, some] + else + dec.continueWithUnit + mkBindApp σ γ forIn rest + + +/-- Infer nested-loop control flow using Lean's ordinary `for` handler. -/ +@[doElem_control_info rdoFor] def controlInfoRDoFor : ControlInfoHandler := fun stx => do + let `(rdoFor| for $_:rdoForDecl,* rdo $body) := stx | throwUnsupportedSyntax + inferControlInfoElem (← `(doElem| for _ in #[()] do $body)) + +end RandomDo.RDo diff --git a/TestNext.lean b/TestNext.lean new file mode 100644 index 0000000..6c1e48c --- /dev/null +++ b/TestNext.lean @@ -0,0 +1,6 @@ +module -- shake: keep-all --deprecated_module: ignore + +public import TestNext.MeasurableSpaceMonad.Core +public import TestNext.MeasurableSpaceMonad.ImportBoundary +public import TestNext.MeasurableSpaceMonad.Notation +public import TestNext.MeasurableSpaceMonad.NotationBasic diff --git a/TestNext/MeasurableSpaceMonad/Core.lean b/TestNext/MeasurableSpaceMonad/Core.lean new file mode 100644 index 0000000..22cec99 --- /dev/null +++ b/TestNext/MeasurableSpaceMonad/Core.lean @@ -0,0 +1,44 @@ +/- +Copyright (c) 2026 David Ledvinka. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: David Ledvinka +-/ +module + +import RandomDoNext.MeasurableSpaceMonad.Core + +/-! +# Polymorphic reasoning checks + +Exercise the public simplifier and measurability interfaces with an abstract monad and +independent result/computation universes. No concrete interpretation is installed. +-/ + +open RandomDo MeasurableSpacePure MeasurableSpaceBind MeasurableSpaceFunctor + +universe u v + +variable {m : (α : Type u) → [MeasurableSpace α] → Type v} [MeasurableSpaceMonad m] + [∀ α, [MeasurableSpace α] → MeasurableSpace (m α)] [LawfulMeasurableSpaceMonad m] + {α β γ : Type u} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] + +-- This uses the registered measurable-space simp rules, not ordinary monad laws. +example (a : α) {f : α → m β} {g : β → m γ} + (hf : Measurable f) : + ((mPure a : m α) >>=ₘ f) >>=ₘ g = f a >>=ₘ g := by + simp [hf] + +example (x : m α) : x >>=ₘ mPure = x := by simp + +example (x : m α) {f : α → β} {g : β → γ} + (hf : Measurable f) (hg : Measurable g) : + x >>=ₘ (fun a => mPure (g (f a))) = g <$>ₘ (f <$>ₘ x) := by + simp (disch := fun_prop) only [LawfulMeasurableSpaceMonad.mBind_mPure_comp, mMap_mMap] + +example {f : α → m β} {g : β → γ} (hf : Measurable f) (hg : Measurable g) : + Measurable (fun x : m α => g <$>ₘ (x >>=ₘ f)) := by + fun_prop + +example {f : α → β} (hf : Measurable f) : + Measurable (fun a : α => (mPure (f a) : m β)) := by + fun_prop diff --git a/TestNext/MeasurableSpaceMonad/ImportBoundary.lean b/TestNext/MeasurableSpaceMonad/ImportBoundary.lean new file mode 100644 index 0000000..5d07f5c --- /dev/null +++ b/TestNext/MeasurableSpaceMonad/ImportBoundary.lean @@ -0,0 +1,17 @@ +/- +Copyright (c) 2026 David Ledvinka. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: David Ledvinka +-/ +module + +import RandomDoNext + +/-! +# Isolation of the polymorphic foundation + +The complete rebuilt library must not pull in the original monad classes, concrete measure +semantics, or random-number implementations. These checks also catch transitive imports. +-/ + +assert_not_exists MeasurableSpaceMonad MeasureTheory.Measure PseudoRandomM NumLean.RandPCG diff --git a/TestNext/MeasurableSpaceMonad/Notation.lean b/TestNext/MeasurableSpaceMonad/Notation.lean new file mode 100644 index 0000000..a9183dd --- /dev/null +++ b/TestNext/MeasurableSpaceMonad/Notation.lean @@ -0,0 +1,90 @@ +/- +Copyright (c) 2026 David Ledvinka. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: David Ledvinka +-/ +module + +public import RandomDoNext.MeasurableSpaceMonad.Notation + +/-! +# Elaboration without a concrete interpretation + +The programs below use only abstract operation and iteration instances. They check the split +notation imports, mutable state, membership proofs, nested loops, and early control flow. +-/ + +open RandomDo MeasurableSpacePure MeasurableSpaceBind + +@[expose] public section + +namespace TestNext.MeasurableSpaceMonad + +universe u v + +variable {m : (α : Type u) → [MeasurableSpace α] → Type v} [MeasurableSpaceMonad m] + {α β : Type u} [MeasurableSpace α] [MeasurableSpace β] + +example (a : α) : (rdo return a : m α) = mPure a := rfl + +example (x : m α) (f : α → m β) : (rdo + let a ← x + f a : m β) = x >>=ₘ f := rfl + +/-- Branching and mutation only require the abstract monad operations. -/ +def branch (x : m α) (p : α → Bool) (f : α → m α) : m α := rdo + let mut a ← x + if p a then + a ← f a + return a + +/-- An abstract collection loop can update its accumulator. -/ +def accumulate [MeasurableSpaceForIn m (List α) α] + (xs : List α) (initial : α) (step : α → α → m α) : m α := rdo + let mut acc := initial + for x in xs rdo + acc ← step x acc + return acc + +/-- Nested loops retain mutations of the outer accumulator. -/ +def nested [MeasurableSpaceForIn m (List α) α] + (xs : List α) (initial : α) (step : α → α → α → m α) : m α := rdo + let mut acc := initial + for x in xs rdo + for y in xs rdo + acc ← step x y acc + return acc + +/-- Membership-aware iteration passes the proof to the body. -/ +def withMembership [MeasurableSpaceForIn' m (List α) α inferInstance] + (xs : List α) (initial : α) (step : (x : α) → x ∈ xs → α → m α) : m α := rdo + let mut acc := initial + for h : x in xs rdo + acc ← step x h acc + return acc + +/-- A membership-aware instance also supplies ordinary iteration. -/ +def forgetMembership [MeasurableSpaceForIn' m (List α) α inferInstance] + (xs : List α) (initial : α) (step : α → α → m α) : m α := + accumulate xs initial step + +/-- A nested loop can return from the whole block. -/ +def firstMatch [MeasurableSpaceForIn m (List α) α] + (xs : List α) (fallback : α) (p : α → α → Bool) : m α := rdo + for x in xs rdo + for y in xs rdo + if p x y then + return y + return fallback + +/-- `break` and `continue` preserve the loop's accumulated state. -/ +def control [MeasurableSpaceForIn m (List α) α] + (xs : List α) (initial : α) (skip stop : α → Bool) (step : α → α → m α) : m α := rdo + let mut acc := initial + for x in xs rdo + if stop x then break + if skip x then continue + acc ← step x acc + return acc + +end TestNext.MeasurableSpaceMonad diff --git a/TestNext/MeasurableSpaceMonad/NotationBasic.lean b/TestNext/MeasurableSpaceMonad/NotationBasic.lean new file mode 100644 index 0000000..0ae5256 --- /dev/null +++ b/TestNext/MeasurableSpaceMonad/NotationBasic.lean @@ -0,0 +1,36 @@ +/- +Copyright (c) 2026 David Ledvinka. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: David Ledvinka +-/ +module + +public import RandomDoNext.MeasurableSpaceMonad.Notation.Basic + +/-! +# Basic notation as a standalone import + +Updating two mutable variables across a branch requires a measurable space on their product. +This example must elaborate without importing the collection-loop notation or an interpretation. +-/ + +open RandomDo + +@[expose] public section + +namespace TestNext.MeasurableSpaceMonad + +universe u v + +/-- Branching carries both abstract mutable values. -/ +def branchPair {m : (α : Type u) → [MeasurableSpace α] → Type v} [MeasurableSpaceMonad m] + {α β : Type u} [MeasurableSpace α] [MeasurableSpace β] + (a : α) (b : β) (choose : Bool) (left : α → m α) (right : β → m β) : m (α × β) := rdo + let mut x := a + let mut y := b + if choose then + x ← left x + y ← right y + return (x, y) + +end TestNext.MeasurableSpaceMonad diff --git a/lakefile.toml b/lakefile.toml index 1dd6684..649890d 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -1,5 +1,5 @@ name = "RandomDo" -defaultTargets = ["RandomDo"] +defaultTargets = ["RandomDo", "RandomDoNext"] lintDriver = "batteries/runLinter" testDriver = "Test" @@ -21,6 +21,12 @@ precompileModules = true [[lean_lib]] name = "RandomDo" +[[lean_lib]] +name = "RandomDoNext" + +[[lean_lib]] +name = "TestNext" + [[lean_lib]] name = "Test" From 4b21c60ba3f05d3c28e46b609bc85d8a0b9758ed Mon Sep 17 00:00:00 2001 From: David Ledvinka Date: Mon, 26 Oct 2026 17:55:37 +0000 Subject: [PATCH 02/13] Consolidate measurable-space monad core and notation under RandomDo --- RandomDo.lean | 2 + RandomDo/MeasurableSpaceMonad/Core.lean | 267 ++++++++++++++++++ .../MeasurableSpaceMonad/Notation.lean | 104 ++++++- RandomDoNext.lean | 10 - RandomDoNext/MeasurableSpaceMonad.lean | 20 -- RandomDoNext/MeasurableSpaceMonad/Core.lean | 17 -- .../MeasurableSpaceMonad/Core/Basic.lean | 105 ------- .../MeasurableSpaceMonad/Core/ForIn.lean | 73 ----- .../MeasurableSpaceMonad/Core/Lawful.lean | 142 ---------- .../MeasurableSpaceMonad/Notation.lean | 16 -- .../MeasurableSpaceMonad/Notation/Basic.lean | 81 ------ TestNext.lean | 1 - TestNext/MeasurableSpaceMonad/Core.lean | 2 +- .../MeasurableSpaceMonad/ImportBoundary.lean | 4 +- TestNext/MeasurableSpaceMonad/Notation.lean | 17 +- .../MeasurableSpaceMonad/NotationBasic.lean | 36 --- lakefile.toml | 5 +- 17 files changed, 376 insertions(+), 526 deletions(-) create mode 100644 RandomDo/MeasurableSpaceMonad/Core.lean rename RandomDoNext/MeasurableSpaceMonad/Notation/ForIn.lean => RandomDo/MeasurableSpaceMonad/Notation.lean (71%) delete mode 100644 RandomDoNext.lean delete mode 100644 RandomDoNext/MeasurableSpaceMonad.lean delete mode 100644 RandomDoNext/MeasurableSpaceMonad/Core.lean delete mode 100644 RandomDoNext/MeasurableSpaceMonad/Core/Basic.lean delete mode 100644 RandomDoNext/MeasurableSpaceMonad/Core/ForIn.lean delete mode 100644 RandomDoNext/MeasurableSpaceMonad/Core/Lawful.lean delete mode 100644 RandomDoNext/MeasurableSpaceMonad/Notation.lean delete mode 100644 RandomDoNext/MeasurableSpaceMonad/Notation/Basic.lean delete mode 100644 TestNext/MeasurableSpaceMonad/NotationBasic.lean diff --git a/RandomDo.lean b/RandomDo.lean index b2d4043..76bf7b3 100644 --- a/RandomDo.lean +++ b/RandomDo.lean @@ -2,6 +2,8 @@ module -- shake: keep-all --deprecated_module: ignore public import RandomDo.ForMathlib.MeasureTheory.MeasurableSpace.Embedding public import RandomDo.Measurable +public import RandomDo.MeasurableSpaceMonad.Core +public import RandomDo.MeasurableSpaceMonad.Notation public import RandomDo.Monad.ForInInstances public import RandomDo.Monad.Instances public import RandomDo.Monad.MeasurableSpace diff --git a/RandomDo/MeasurableSpaceMonad/Core.lean b/RandomDo/MeasurableSpaceMonad/Core.lean new file mode 100644 index 0000000..a070899 --- /dev/null +++ b/RandomDo/MeasurableSpaceMonad/Core.lean @@ -0,0 +1,267 @@ +/- +Copyright (c) 2026 David Ledvinka. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: David Ledvinka +-/ +module + +public import Mathlib.MeasureTheory.MeasurableSpace.Basic +public import Mathlib.MeasureTheory.MeasurableSpace.Constructions +public import Mathlib.Tactic.FunProp + +/-! +# Measurable-space monads + +A measurable-space monad takes a result type together with its measurable-space instance: +`m : (α : Type u) → [MeasurableSpace α] → Type v`. This file contains the operations, conditional +functor and monad laws, and generic iteration interfaces from +`RandomDo/Monad/MeasurableSpace.lean` at main commit `150ecab`. + +The operations accept ordinary functions. The lawfulness classes require a measurable space on +each computation type and state laws for measurable maps and continuations. Concrete monad and +collection implementations belong in separate modules. + +Declarations live in `RandomDo`. Opening this namespace also enables the scoped mapping +notation `<$>ₘ` and sequencing notation `>>=ₘ`. Import +`RandomDo.MeasurableSpaceMonad.Notation` to write programs using `rdo`. +-/ + +@[expose] public section + +namespace RandomDo + +open Function + +section + +universe u v + +section MeasurableSpaceMonad + +/-- A functor on types with a `MeasurableSpace` instance. The `mMap` operator `<$>ₘ` is overloaded +via instances of this class. This class does not require proofs of the `MeasurableSpaceFunctor` +axioms. Proofs may be provided or required via the `LawfulMeasurableSpaceFunctor` class. -/ +class MeasurableSpaceFunctor (f : (α : Type u) → [MeasurableSpace α] → Type v) : + Type (max (u+1) v) where + /-- + Applies a function inside a functor on measurable spaces. This is used to overload the + `<$>ₘ` operator. + + When mapping a constant function (if one cares about executing the code), use + `MeasurableSpaceFunctor.mMapConst` instead, because it may be more efficient. + -/ + mMap {α β : Type u} [MeasurableSpace α] [MeasurableSpace β] : (α → β) → f α → f β + /-- + Mapping a constant function. + + Given `a : α` and `v : f β`, `mMapConst a v` is equivalent to `(fun _ => a) <$>ₘ v`. For some + functors, this can be implemented more efficiently; for all other functors, the default + implementation may be used. + -/ + mMapConst {α β : Type u} [MeasurableSpace α] [MeasurableSpace β] : α → f β → f α := + mMap ∘ (const _) + +@[inherit_doc] scoped infixr:100 " <$>ₘ " => MeasurableSpaceFunctor.mMap + +/-- +The `mPure` function is overloaded via `MeasurableSpacePure` instances. + +`MeasurableSpacePure` is typically accessed via `MeasurableSpaceMonad` instances, which extend it. +-/ +class MeasurableSpacePure (f : (α : Type u) → [MeasurableSpace α] → Type v) where + /-- Given `a : α` where `α` has a `MeasurableSpace` instance, `mPure a : f α` represents an + action that does nothing and returns `a`. -/ + mPure {α : Type u} [MeasurableSpace α] : α → f α + +/-- +The `>>=ₘ` operator is overloaded via instances of `MeasurableSpaceBind`. + +`MeasurableSpaceBind` is typically used via `MeasurableSpaceMonad`, which extends it. +-/ +class MeasurableSpaceBind (m : (α : Type u) → [MeasurableSpace α] → Type v) where + /-- + Sequences two computations, allowing the second to depend on the value computed by the first. + + If `x : m α` and `f : α → m β`, then `x >>=ₘ f : m β` represents the result of executing `x` + to get a value of type `α` and then passing it to `f`. + -/ + mBind {α β : Type u} [MeasurableSpace α] [MeasurableSpace β] : m α → (α → m β) → m β + +@[inherit_doc] scoped infixl:55 " >>=ₘ " => MeasurableSpaceBind.mBind + +/-- Return, sequencing, and mapping for computations indexed by measurable result types. +By default, mapping sequences a computation with return. The operations accept ordinary functions; +measurability assumptions and laws are supplied separately by `LawfulMeasurableSpaceMonad`. -/ +class MeasurableSpaceMonad (m : (α : Type u) → [MeasurableSpace α] → Type v) : + Type (max (u+1) v) + extends MeasurableSpaceFunctor m, MeasurableSpacePure m, MeasurableSpaceBind m where + mMap f μ := mBind μ (Function.comp mPure f) + +variable {m : (α : Type u) → [MeasurableSpace α] → Type v} {α β : Type u} + [MeasurableSpace α] [MeasurableSpace β] + +theorem MeasurableSpaceBind.bind_congr [MeasurableSpaceBind m] {x : m α} {f g : α → m β} + (h : ∀ a, f a = g a) : x >>=ₘ f = x >>=ₘ g := by + simp [funext h] + +theorem MeasurableSpaceFunctor.map_congr [MeasurableSpaceFunctor m] {x : m α} {f g : α → β} + (h : ∀ a, f a = g a) : (f <$>ₘ x : m β) = g <$>ₘ x := by + simp [funext h] + +end MeasurableSpaceMonad + +section Lawful + +open MeasurableSpaceFunctor + +/-- A `MeasurableSpaceFunctor` satisfies the measurable space functor laws. -/ +class LawfulMeasurableSpaceFunctor + (f : (α : Type u) → [MeasurableSpace α] → Type v) [MeasurableSpaceFunctor f] + [∀ α, [MeasurableSpace α] → MeasurableSpace (f α)] : Prop where + /-- `mMap` of a measurable function is a measurable function. -/ + measurable_mMap {α β : Type u} [MeasurableSpace α] [MeasurableSpace β] + {g : α → β} (hg : Measurable g) : Measurable ((g <$>ₘ ·) : f α → f β) + /-- The `mMapConst` implementation is equivalent to the default implementation. -/ + mMap_const {α β : Type u} [MeasurableSpace α] [MeasurableSpace β] : + (mMapConst : α → f β → f α) = mMap ∘ const β + /-- `mMap` preserves identity. -/ + id_mMap {α : Type u} [MeasurableSpace α] (x : f α) : id <$>ₘ x = x + /-- `mMap` preserves function composition of measurable functions. -/ + comp_mMap {α β γ : Type u} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] + {g₀ : α → β} {g₁ : β → γ} (x : f α) (hg₀ : Measurable g₀) (hg₁ : Measurable g₁) : + (g₁ ∘ g₀) <$>ₘ x = g₁ <$>ₘ g₀ <$>ₘ x + +open LawfulMeasurableSpaceFunctor + +attribute [fun_prop] measurable_mMap +attribute [simp] id_mMap + +variable {f : (α : Type u) → [MeasurableSpace α] → Type v} [MeasurableSpaceFunctor f] + [∀ α, [MeasurableSpace α] → MeasurableSpace (f α)] [LawfulMeasurableSpaceFunctor f] + {α β γ : Type u} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] + +@[simp] theorem id_mMap' (x : f α) : (fun a => a) <$>ₘ x = x := id_mMap x + +@[simp] theorem mMap_mMap {g₀ : α → β} {g₁ : β → γ} (x : f α) + (hg₀ : Measurable g₀) (hg₁ : Measurable g₁) : + g₁ <$>ₘ g₀ <$>ₘ x = (fun a => g₁ (g₀ a)) <$>ₘ x := + (comp_mMap x hg₀ hg₁).symm + +open MeasurableSpaceBind MeasurableSpacePure MeasurableSpaceFunctor + +/-- A `MeasurableSpaceMonad` satisfies the measurable space monad laws. -/ +class LawfulMeasurableSpaceMonad + (m : (α : Type u) → [MeasurableSpace α] → Type v) [MeasurableSpaceMonad m] + [∀ α, [MeasurableSpace α] → MeasurableSpace (m α)] : Prop + extends LawfulMeasurableSpaceFunctor m where + /-- `mPure` is a measurable function. -/ + measurable_mPure {α : Type u} [MeasurableSpace α] : Measurable (mPure : α → m α) + /-- `mBind` of a measurable function is a measurable function. -/ + measurable_mBind {α β : Type u} [MeasurableSpace α] [MeasurableSpace β] + {f : α → m β} (hf : Measurable f) : Measurable (fun x : m α => x >>=ₘ f) + /-- A `mBind` followed by `mPure` composed with a measurable function is equivalent to a + functorial map. -/ + mBind_mPure_comp {α β : Type u} [MeasurableSpace α] [MeasurableSpace β] + {f : α → β} (hf : Measurable f) (x : m α) : + x >>=ₘ (fun a => mPure (f a)) = f <$>ₘ x + /-- `mPure` followed by `mBind` of a function application is equivalent to function + application. -/ + mPure_mBind {α β : Type u} [MeasurableSpace α] [MeasurableSpace β] + (x : α) {f : α → m β} (hf : Measurable f) : + mPure x >>=ₘ f = f x + /-- `mBind` is associative on measurable functions. -/ + mBind_assoc {α β γ : Type u} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] + (x : m α) {f : α → m β} {g : β → m γ} (hf : Measurable f) (hg : Measurable g) : + x >>=ₘ f >>=ₘ g = x >>=ₘ fun x => f x >>=ₘ g + measurable_mMap hg := (by + convert measurable_mBind (measurable_mPure.comp hg) + exact (mBind_mPure_comp hg _).symm) + comp_mMap x g_meas h_meas := (by + rw [← mBind_mPure_comp (by fun_prop), ← mBind_mPure_comp h_meas, + ← mBind_mPure_comp g_meas, mBind_assoc _ (by fun_prop) (by fun_prop)] + congr with _ + exact (mPure_mBind _ (measurable_mPure.comp h_meas)).symm) + +open LawfulMeasurableSpaceMonad + +attribute [fun_prop] measurable_mPure measurable_mBind +attribute [simp] mPure_mBind mBind_assoc mBind_mPure_comp +attribute [grind <=] mPure_mBind + +variable {m : (α : Type u) → [MeasurableSpace α] → Type v} [MeasurableSpaceMonad m] + [∀ α, [MeasurableSpace α] → MeasurableSpace (m α)] [LawfulMeasurableSpaceMonad m] + {α β γ : Type u} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] + +@[simp] theorem mMap_mPure {f : α → β} (hf : Measurable f) (x : α) : + f <$>ₘ (mPure x : m α) = mPure (f x) := by + rw [← mBind_mPure_comp hf, mPure_mBind _ (by fun_prop)] + +@[simp] theorem mBind_mPure (x : m α) : x >>=ₘ mPure = x := by + change x >>=ₘ (fun a => (mPure (id a))) = x + rw [mBind_mPure_comp (by fun_prop), id_mMap] + +theorem mMap_eq_mPure_mBind {f : α → β} (hf : Measurable f) (x : m α) : + f <$>ₘ x = x >>=ₘ fun a => mPure (f a) := by + rw [← mBind_mPure_comp hf x] + +theorem mBind_mPure_unit {x : m PUnit} : (x >>=ₘ fun _ => mPure ⟨⟩) = x := by rw [mBind_mPure] + +@[simp] theorem mMap_mBind {f : β → γ} (hf : Measurable f) (x : m α) + {g : α → m β} (hg : Measurable g) : + f <$>ₘ (x >>=ₘ g) = x >>=ₘ fun a => f <$>ₘ g a := by + rw [← mBind_mPure_comp hf, mBind_assoc _ hg (by fun_prop)] + simp (disch := fun_prop) [mBind_mPure_comp] + +@[simp] theorem mBind_mMap_left {f : α → β} (hf : Measurable f) (x : m α) + {g : β → m γ} (hg : Measurable g) : + ((f <$>ₘ x) >>=ₘ fun b => g b) = (x >>=ₘ fun a => g (f a)) := by + rw [← mBind_mPure_comp hf] + simp (disch := fun_prop) only [mBind_assoc, mPure_mBind] + +end Lawful + +end + +section MeasurableSpaceFor + +universe uρ uα u v + +variable {α : Type u} [mα : MeasurableSpace α] (m : (α : Type u) → [MeasurableSpace α] → Type v) + +/-- The disjoint-union measurable space on the two possible loop-step outcomes. -/ +instance instMeasurableSpaceForInStep {β : Type u} [mβ : MeasurableSpace β] : + MeasurableSpace (ForInStep β) := mβ.map ForInStep.yield ⊓ mβ.map ForInStep.done + +/-- +Monadic iteration in `rdo`-blocks, using the `for x in xs` notation. +-/ +class MeasurableSpaceForIn (ρ : Type uρ) (α : outParam (Type uα)) where + /-- + Monadically iterates over the contents of a collection `xs`, with a local state `b` and the + possibility of early termination. + -/ + forIn {β : Type u} [MeasurableSpace β] (xs : ρ) (b : β) + (f : α → β → m (ForInStep β)) : m β + +/-- +Monadic iteration in `rdo`-blocks with a membership proof, using the `for h : x in xs` notation. +-/ +class MeasurableSpaceForIn' (ρ : Type uρ) (α : outParam (Type uα)) + (d : outParam (Membership α ρ)) where + /-- + Monadically iterates over the contents of a collection `xs`, with a local state `b` and the + possibility of early termination. At each iteration, the body of the loop is provided with a proof + that the current element is in the collection. + -/ + forIn' {β : Type u} [MeasurableSpace β] (xs : ρ) (b : β) + (f : (a : α) → a ∈ xs → β → m (ForInStep β)) : m β + +@[simps] +instance (priority := 500) instMeasurableSpaceForInOfForIn' + {ρ : Type uρ} {α : Type uα} {d : Membership α ρ} [MeasurableSpaceForIn' m ρ α d] : + MeasurableSpaceForIn m ρ α where + forIn x b f := MeasurableSpaceForIn'.forIn' x b fun a _ s => f a s + +end MeasurableSpaceFor + +end RandomDo diff --git a/RandomDoNext/MeasurableSpaceMonad/Notation/ForIn.lean b/RandomDo/MeasurableSpaceMonad/Notation.lean similarity index 71% rename from RandomDoNext/MeasurableSpaceMonad/Notation/ForIn.lean rename to RandomDo/MeasurableSpaceMonad/Notation.lean index 1548c44..ce5bdeb 100644 --- a/RandomDoNext/MeasurableSpaceMonad/Notation/ForIn.lean +++ b/RandomDo/MeasurableSpaceMonad/Notation.lean @@ -1,36 +1,101 @@ /- Copyright (c) 2026 David Ledvinka. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: David Ledvinka +Authors: David Ledvinka, Gaëtan Serré -/ module -public import RandomDoNext.MeasurableSpaceMonad.Core.ForIn -public import RandomDoNext.MeasurableSpaceMonad.Notation.Basic +public import RandomDo.MeasurableSpaceMonad.Core +public import Mathlib.MeasureTheory.MeasurableSpace.Prod +public meta import Lean.Elab.BuiltinDo public meta import Lean.Meta.ProdN /-! -# Collection iteration in `rdo` +# `rdo` notation + +`rdo` elaborates programs using the measurable-space operations `mPure` and `mBind`. It reuses +Lean's `do` elaborators for binding, branching, mutation, and early return, supplying the +additional measurable-space argument when constructing a computation type or operation. +Use `open RandomDo` (or `open scoped RandomDo`) to enable the notation. `for x in xs rdo body` uses `MeasurableSpaceForIn`; `for h : x in xs rdo body` uses `MeasurableSpaceForIn'` and supplies a membership proof. The elaborator carries mutable state, -`break`, `continue`, and early returns through the loop accumulator. - -The parser and elaborator are adapted from `RandomDo/Monad/Notation.lean` at main commit -`150ecab`, which mirrors `Lean/Parser/Do.lean` and `Lean/Elab/BuiltinDo/For.lean`. The control-info -handler from the `loops` branch at `c0f8f5b` also supports nested loops. While-loop syntax and -interpretations are left to a later change. +`break`, `continue`, and early returns through the loop accumulator. The measurable space on +`Option` below supports early returns. Callers supply the monad and collection instances. -There are no collection or monad implementations here: a polymorphic caller supplies the -appropriate iteration instance. +Adapted from `RandomDo/Monad/Notation.lean` at main commit `150ecab`, which mirrors Lean's +`DoOps`, parser, and `for` elaborator. The optional-value instance comes from +`RandomDo/Measurable.lean` at that commit. The control-info handler from the `loops` branch at +`c0f8f5b` supports nested loops. While-loop syntax and semantics are left to a later change. -/ +namespace RandomDo + +universe u + +/-- The measurable space on optional results used to carry an early return. +A set of optional values is measurable exactly when its `some` preimage is measurable. -/ +public instance instMeasurableSpaceOption {α : Type u} [mα : MeasurableSpace α] : + MeasurableSpace (Option α) := mα.map some + +end RandomDo + open Lean Lean.Parser Lean.Parser.Term Lean.Meta Lean.Elab Lean.Elab.Do Lean.Elab.Term Std Meta open RandomDo MeasurableSpacePure MeasurableSpaceBind public meta section -namespace RandomDo.RDo +namespace RandomDo + +/-- The `do` notation for writing monadic programs depending on a `MeasurableSpace` instance. -/ +scoped syntax (name := randKind) (priority := high) "rdo" doSeq : term + +namespace RDo + +/-- Define `DoOp`s for `rdo` notation. -/ +def randOps : DoOps := { DoOps.default with + mkPureApp α e := do + let ⟨m, u, v, _, _⟩ := (← read).monadInfo + let α ← Term.ensureHasType (mkSort (mkLevelSucc u)) α + let e ← Term.ensureHasType α e + let instPure ← mkInstMVar (.app (mkConst ``MeasurableSpacePure [u,v]) m) + let instPure ← instantiateMVars instPure + let σ ← mkInstMVar (.app (mkConst ``MeasurableSpace [u]) α) + let σ ← instantiateMVars σ + return mkAppN (mkConst ``mPure [u, v]) #[m, instPure, α, σ, e] + mkBindApp α β e k := do + let ⟨m, u, v, _, _⟩ := (← read).monadInfo + let α ← Term.ensureHasType (mkSort (mkLevelSucc u)) α + let σα ← mkInstMVar (.app (mkConst ``MeasurableSpace [u]) α) + let σβ ← mkInstMVar (.app (mkConst ``MeasurableSpace [u]) β) + let mα := mkApp2 m α σα + let mβ := mkApp2 m β σβ + let e ← Term.ensureHasType mα e + let k ← Term.ensureHasType (← mkArrow α mβ) k + let σα ← instantiateMVars σα + let σβ ← instantiateMVars σβ + let instBind ← mkInstMVar (.app (mkConst ``MeasurableSpaceBind [u, v]) m) + let instBind ← instantiateMVars instBind + return mkAppN (mkConst ``mBind [u, v]) #[m, instBind, α, β, σα, σβ, e, k] + isPureApp? e := + if e.isAppOfArity ``mPure 5 then some (e.getArg! 4) else none + splitMonadApp? type := do + let .app m _ := type.consumeMData | return none + let .app m resultType := m.consumeMData | return none + unless ← isType resultType do return none + let u ← getDecLevel resultType + let v ← getDecLevel type + return some ({ m := m, u := u.normalize, v := v.normalize }, resultType) + mkMonadApp α := do + let ⟨m, u, _, _, _⟩ := (← read).monadInfo + let σ ← mkInstMVar (mkApp (mkConst ``MeasurableSpace [u]) α) + return mkApp2 m α σ + } + +/-- Define `rdo` notation elaborator. -/ +@[term_elab randKind] def elabRand : Term.TermElab := fun stx et? => do + let `(rdo $doSeq) := stx | throwUnsupportedSyntax + elabDoWith randOps doSeq et? /-- parses `_ : _ in` for `rdo` for loops -/ def rdoForDecl := leading_parser @@ -38,9 +103,16 @@ def rdoForDecl := leading_parser withForbidden "rdo" termParser /-- parser for `rdo` for loops -/ -@[doElem_parser] def rdoFor := leading_parser +def rdoFor := leading_parser "for " >> sepBy1 rdoForDecl ", " >> "rdo " >> doSeq +end RDo + +-- Prefer the new parser when its scope is open, including alongside the legacy notation. +attribute [scoped doElem_parser high] RDo.rdoFor + +namespace RDo + /-- Define expander for loops in `rdo` notation. Note this code mirrors core's implementation for `do` notation as much as possible. -/ @[macro rdoFor] def expandRDoFor : Macro := fun stx => do @@ -225,4 +297,6 @@ def rdoForDecl := leading_parser let `(rdoFor| for $_:rdoForDecl,* rdo $body) := stx | throwUnsupportedSyntax inferControlInfoElem (← `(doElem| for _ in #[()] do $body)) -end RandomDo.RDo +end RDo + +end RandomDo diff --git a/RandomDoNext.lean b/RandomDoNext.lean deleted file mode 100644 index 996b532..0000000 --- a/RandomDoNext.lean +++ /dev/null @@ -1,10 +0,0 @@ -module -- shake: keep-all --deprecated_module: ignore - -public import RandomDoNext.MeasurableSpaceMonad -public import RandomDoNext.MeasurableSpaceMonad.Core -public import RandomDoNext.MeasurableSpaceMonad.Core.Basic -public import RandomDoNext.MeasurableSpaceMonad.Core.ForIn -public import RandomDoNext.MeasurableSpaceMonad.Core.Lawful -public import RandomDoNext.MeasurableSpaceMonad.Notation -public import RandomDoNext.MeasurableSpaceMonad.Notation.Basic -public import RandomDoNext.MeasurableSpaceMonad.Notation.ForIn diff --git a/RandomDoNext/MeasurableSpaceMonad.lean b/RandomDoNext/MeasurableSpaceMonad.lean deleted file mode 100644 index 5eb6dac..0000000 --- a/RandomDoNext/MeasurableSpaceMonad.lean +++ /dev/null @@ -1,20 +0,0 @@ -/- -Copyright (c) 2026 David Ledvinka. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: David Ledvinka --/ -module - -public import RandomDoNext.MeasurableSpaceMonad.Core -public import RandomDoNext.MeasurableSpaceMonad.Notation - -/-! -# Measurable-space monads - -The polymorphic foundation of the rebuilt library. `Core` contains operations, laws, and -iteration interfaces; `Notation` contains their `rdo` elaborators. Concrete interpretations -and sampling implementations belong outside this subtree. - -`RandomDoNext` is the staging module root. Declaration namespaces already use `RandomDo`, so -promoting the library will change module paths without renaming its mathematical API. --/ diff --git a/RandomDoNext/MeasurableSpaceMonad/Core.lean b/RandomDoNext/MeasurableSpaceMonad/Core.lean deleted file mode 100644 index a21d7b8..0000000 --- a/RandomDoNext/MeasurableSpaceMonad/Core.lean +++ /dev/null @@ -1,17 +0,0 @@ -/- -Copyright (c) 2026 David Ledvinka. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: David Ledvinka --/ -module - -public import RandomDoNext.MeasurableSpaceMonad.Core.Basic -public import RandomDoNext.MeasurableSpaceMonad.Core.ForIn -public import RandomDoNext.MeasurableSpaceMonad.Core.Lawful - -/-! -# Polymorphic measurable-space monad theory - -Operations, conditional laws, and iteration interfaces, independent of any concrete monad. -Import `RandomDoNext.MeasurableSpaceMonad.Notation` as well to write programs using `rdo`. --/ diff --git a/RandomDoNext/MeasurableSpaceMonad/Core/Basic.lean b/RandomDoNext/MeasurableSpaceMonad/Core/Basic.lean deleted file mode 100644 index 18b112d..0000000 --- a/RandomDoNext/MeasurableSpaceMonad/Core/Basic.lean +++ /dev/null @@ -1,105 +0,0 @@ -/- -Copyright (c) 2026 David Ledvinka. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: David Ledvinka --/ -module - -public import Mathlib.MeasureTheory.MeasurableSpace.Defs - -/-! -# Operations on measurable-space monads - -A measurable-space monad takes a result type together with its measurable-space instance: -`m : (α : Type u) → [MeasurableSpace α] → Type v`. The classes in this file follow the separation -of `Functor`, `Pure`, `Bind`, and `Monad` in `Init/Core.lean`. - -The operations accept ordinary functions. Measurability assumptions belong to the laws in -`RandomDoNext.MeasurableSpaceMonad.Core.Lawful`, so constructing a program does not require -proving its measurability. The operational classes alone assert no laws. - -Declarations live in `RandomDo`. Opening this namespace also enables the scoped mapping -notation `<$>ₘ` and sequencing notation `>>=ₘ`. - -Adapted from `RandomDo/Monad/MeasurableSpace.lean` at main commit `150ecab`. --/ - -@[expose] public section - -namespace RandomDo - -open Function - -universe u v - -/-- A functor on types with a `MeasurableSpace` instance. The `mMap` operator `<$>ₘ` is overloaded -via instances of this class. This class does not require proofs of the `MeasurableSpaceFunctor` -axioms. Proofs may be provided or required via the `LawfulMeasurableSpaceFunctor` class. -/ -class MeasurableSpaceFunctor (f : (α : Type u) → [MeasurableSpace α] → Type v) : - Type (max (u+1) v) where - /-- - Applies a function inside a functor on measurable spaces. This is used to overload the - `<$>ₘ` operator. - - When mapping a constant function (if one cares about executing the code), use - `MeasurableSpaceFunctor.mMapConst` instead, because it may be more efficient. - -/ - mMap {α β : Type u} [MeasurableSpace α] [MeasurableSpace β] : (α → β) → f α → f β - /-- - Mapping a constant function. - - Given `a : α` and `v : f β`, `mMapConst a v` is equivalent to `(fun _ => a) <$>ₘ v`. For some - functors, this can be implemented more efficiently; for all other functors, the default - implementation may be used. - -/ - mMapConst {α β : Type u} [MeasurableSpace α] [MeasurableSpace β] : α → f β → f α := - mMap ∘ (const _) - -@[inherit_doc] scoped infixr:100 " <$>ₘ " => MeasurableSpaceFunctor.mMap - -/-- -The `mPure` function is overloaded via `MeasurableSpacePure` instances. - -`MeasurableSpacePure` is typically accessed via `MeasurableSpaceMonad` instances, which extend it. --/ -class MeasurableSpacePure (f : (α : Type u) → [MeasurableSpace α] → Type v) where - /-- Given `a : α` where `α` has a `MeasurableSpace` instance, `mPure a : f α` represents an - action that does nothing and returns `a`. -/ - mPure {α : Type u} [MeasurableSpace α] : α → f α - -/-- -The `>>=ₘ` operator is overloaded via instances of `MeasurableSpaceBind`. - -`MeasurableSpaceBind` is typically used via `MeasurableSpaceMonad`, which extends it. --/ -class MeasurableSpaceBind (m : (α : Type u) → [MeasurableSpace α] → Type v) where - /-- - Sequences two computations, allowing the second to depend on the value computed by the first. - - If `x : m α` and `f : α → m β`, then `x >>=ₘ f : m β` represents the result of executing `x` - to get a value of type `α` and then passing it to `f`. - -/ - mBind {α β : Type u} [MeasurableSpace α] [MeasurableSpace β] : m α → (α → m β) → m β - -@[inherit_doc] scoped infixl:55 " >>=ₘ " => MeasurableSpaceBind.mBind - -/-- Return, sequencing, and mapping for computations indexed by measurable result types. -By default, mapping sequences a computation with return. The operations accept ordinary functions; -measurability assumptions and laws are supplied separately by `LawfulMeasurableSpaceMonad`. -/ -class MeasurableSpaceMonad (m : (α : Type u) → [MeasurableSpace α] → Type v) : - Type (max (u+1) v) - extends MeasurableSpaceFunctor m, MeasurableSpacePure m, MeasurableSpaceBind m where - mMap f μ := mBind μ (Function.comp mPure f) - -variable {m : (α : Type u) → [MeasurableSpace α] → Type v} {α β : Type u} - [MeasurableSpace α] [MeasurableSpace β] - -theorem MeasurableSpaceBind.bind_congr [MeasurableSpaceBind m] {x : m α} {f g : α → m β} - (h : ∀ a, f a = g a) : x >>=ₘ f = x >>=ₘ g := by - simp [funext h] - -theorem MeasurableSpaceFunctor.map_congr [MeasurableSpaceFunctor m] {x : m α} {f g : α → β} - (h : ∀ a, f a = g a) : (f <$>ₘ x : m β) = g <$>ₘ x := by - simp [funext h] - -end RandomDo diff --git a/RandomDoNext/MeasurableSpaceMonad/Core/ForIn.lean b/RandomDoNext/MeasurableSpaceMonad/Core/ForIn.lean deleted file mode 100644 index d47be09..0000000 --- a/RandomDoNext/MeasurableSpaceMonad/Core/ForIn.lean +++ /dev/null @@ -1,73 +0,0 @@ -/- -Copyright (c) 2026 David Ledvinka. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: David Ledvinka, Gaëtan Serré --/ -module - -public import RandomDoNext.MeasurableSpaceMonad.Core.Basic -public import Mathlib.MeasureTheory.MeasurableSpace.Basic - -/-! -# Polymorphic iteration interfaces - -`MeasurableSpaceForIn` and `MeasurableSpaceForIn'` are the measurable-space counterparts of -Lean's iteration classes. The accumulator has a measurable space, and each step either yields -an updated accumulator or stops the loop. - -The measurable spaces on `ForInStep` and `Option`, and the adapter from membership-aware -iteration, are generic in the monad. Implementations for particular collections or monads belong -in separate modules. -No unbounded-loop operation or semantics is chosen here. - -Adapted from `RandomDo/Monad/MeasurableSpace.lean` and the optional-value instance in -`RandomDo/Measurable.lean` at main commit `150ecab`. --/ - -@[expose] public section - -namespace RandomDo - -universe uρ uα u v - -variable {α : Type u} [mα : MeasurableSpace α] (m : (α : Type u) → [MeasurableSpace α] → Type v) - -/-- The measurable space on optional results used to carry an early return. -A set of optional values is measurable exactly when its `some` preimage is measurable. -/ -instance instMeasurableSpaceOption : MeasurableSpace (Option α) := mα.map some - -/-- The disjoint-union measurable space on the two possible loop-step outcomes. -/ -instance instMeasurableSpaceForInStep {β : Type u} [mβ : MeasurableSpace β] : - MeasurableSpace (ForInStep β) := mβ.map ForInStep.yield ⊓ mβ.map ForInStep.done - -/-- -Monadic iteration in `rdo`-blocks, using the `for x in xs` notation. --/ -class MeasurableSpaceForIn (ρ : Type uρ) (α : outParam (Type uα)) where - /-- - Monadically iterates over the contents of a collection `xs`, with a local state `b` and the - possibility of early termination. - -/ - forIn {β : Type u} [MeasurableSpace β] (xs : ρ) (b : β) - (f : α → β → m (ForInStep β)) : m β - -/-- -Monadic iteration in `rdo`-blocks with a membership proof, using the `for h : x in xs` notation. --/ -class MeasurableSpaceForIn' (ρ : Type uρ) (α : outParam (Type uα)) - (d : outParam (Membership α ρ)) where - /-- - Monadically iterates over the contents of a collection `xs`, with a local state `b` and the - possibility of early termination. At each iteration, the body of the loop is provided with a proof - that the current element is in the collection. - -/ - forIn' {β : Type u} [MeasurableSpace β] (xs : ρ) (b : β) - (f : (a : α) → a ∈ xs → β → m (ForInStep β)) : m β - -@[simps] -instance (priority := 500) instMeasurableSpaceForInOfForIn' - {ρ : Type uρ} {α : Type uα} {d : Membership α ρ} [MeasurableSpaceForIn' m ρ α d] : - MeasurableSpaceForIn m ρ α where - forIn x b f := MeasurableSpaceForIn'.forIn' x b fun a _ s => f a s - -end RandomDo diff --git a/RandomDoNext/MeasurableSpaceMonad/Core/Lawful.lean b/RandomDoNext/MeasurableSpaceMonad/Core/Lawful.lean deleted file mode 100644 index 7f8f231..0000000 --- a/RandomDoNext/MeasurableSpaceMonad/Core/Lawful.lean +++ /dev/null @@ -1,142 +0,0 @@ -/- -Copyright (c) 2026 David Ledvinka. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: David Ledvinka --/ -module - -public import RandomDoNext.MeasurableSpaceMonad.Core.Basic -public import Mathlib.MeasureTheory.MeasurableSpace.Constructions -public import Mathlib.Tactic.FunProp - -/-! -# Laws of measurable-space functors and monads - -The lawfulness classes require a measurable space on each computation type `m α`. They state -functor and monad laws for measurable maps and continuations, together with measurability of -mapping, return, and sequencing. Composition and sequencing laws carry explicit measurability -hypotheses. - -The type constructor and its operations remain abstract throughout this file. In particular, -there are no assumptions about probability, sampling, or a choice of interpretation. - -These are the laws from `RandomDo/Monad/MeasurableSpace.lean` at main commit `150ecab`, following -`Init/Control/Lawful/Basic.lean`. The simplifier attributes apply to the measurable-space laws -rather than similarly named laws for ordinary monads. --/ - -@[expose] public section - -namespace RandomDo - -open Function - -universe u v - -open MeasurableSpaceFunctor - -/-- A `MeasurableSpaceFunctor` satisfies the measurable space functor laws. -/ -class LawfulMeasurableSpaceFunctor - (f : (α : Type u) → [MeasurableSpace α] → Type v) [MeasurableSpaceFunctor f] - [∀ α, [MeasurableSpace α] → MeasurableSpace (f α)] : Prop where - /-- `mMap` of a measurable function is a measurable function. -/ - measurable_mMap {α β : Type u} [MeasurableSpace α] [MeasurableSpace β] - {g : α → β} (hg : Measurable g) : Measurable ((g <$>ₘ ·) : f α → f β) - /-- The `mMapConst` implementation is equivalent to the default implementation. -/ - mMap_const {α β : Type u} [MeasurableSpace α] [MeasurableSpace β] : - (mMapConst : α → f β → f α) = mMap ∘ const β - /-- `mMap` preserves identity. -/ - id_mMap {α : Type u} [MeasurableSpace α] (x : f α) : id <$>ₘ x = x - /-- `mMap` preserves function composition of measurable functions. -/ - comp_mMap {α β γ : Type u} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] - {g₀ : α → β} {g₁ : β → γ} (x : f α) (hg₀ : Measurable g₀) (hg₁ : Measurable g₁) : - (g₁ ∘ g₀) <$>ₘ x = g₁ <$>ₘ g₀ <$>ₘ x - -open LawfulMeasurableSpaceFunctor - -attribute [fun_prop] measurable_mMap -attribute [simp] id_mMap - -variable {f : (α : Type u) → [MeasurableSpace α] → Type v} [MeasurableSpaceFunctor f] - [∀ α, [MeasurableSpace α] → MeasurableSpace (f α)] [LawfulMeasurableSpaceFunctor f] - {α β γ : Type u} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] - -@[simp] theorem id_mMap' (x : f α) : (fun a => a) <$>ₘ x = x := id_mMap x - -@[simp] theorem mMap_mMap {g₀ : α → β} {g₁ : β → γ} (x : f α) - (hg₀ : Measurable g₀) (hg₁ : Measurable g₁) : - g₁ <$>ₘ g₀ <$>ₘ x = (fun a => g₁ (g₀ a)) <$>ₘ x := - (comp_mMap x hg₀ hg₁).symm - -open MeasurableSpaceBind MeasurableSpacePure MeasurableSpaceFunctor - -/-- A `MeasurableSpaceMonad` satisfies the measurable space monad laws. -/ -class LawfulMeasurableSpaceMonad - (m : (α : Type u) → [MeasurableSpace α] → Type v) [MeasurableSpaceMonad m] - [∀ α, [MeasurableSpace α] → MeasurableSpace (m α)] : Prop - extends LawfulMeasurableSpaceFunctor m where - /-- `mPure` is a measurable function. -/ - measurable_mPure {α : Type u} [MeasurableSpace α] : Measurable (mPure : α → m α) - /-- `mBind` of a measurable function is a measurable function. -/ - measurable_mBind {α β : Type u} [MeasurableSpace α] [MeasurableSpace β] - {f : α → m β} (hf : Measurable f) : Measurable (fun x : m α => x >>=ₘ f) - /-- A `mBind` followed by `mPure` composed with a measurable function is equivalent to a - functorial map. -/ - mBind_mPure_comp {α β : Type u} [MeasurableSpace α] [MeasurableSpace β] - {f : α → β} (hf : Measurable f) (x : m α) : - x >>=ₘ (fun a => mPure (f a)) = f <$>ₘ x - /-- `mPure` followed by `mBind` of a function application is equivalent to function - application. -/ - mPure_mBind {α β : Type u} [MeasurableSpace α] [MeasurableSpace β] - (x : α) {f : α → m β} (hf : Measurable f) : - mPure x >>=ₘ f = f x - /-- `mBind` is associative on measurable functions. -/ - mBind_assoc {α β γ : Type u} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] - (x : m α) {f : α → m β} {g : β → m γ} (hf : Measurable f) (hg : Measurable g) : - x >>=ₘ f >>=ₘ g = x >>=ₘ fun x => f x >>=ₘ g - measurable_mMap hg := (by - convert measurable_mBind (measurable_mPure.comp hg) - exact (mBind_mPure_comp hg _).symm) - comp_mMap x g_meas h_meas := (by - rw [← mBind_mPure_comp (by fun_prop), ← mBind_mPure_comp h_meas, - ← mBind_mPure_comp g_meas, mBind_assoc _ (by fun_prop) (by fun_prop)] - congr with _ - exact (mPure_mBind _ (measurable_mPure.comp h_meas)).symm) - -open LawfulMeasurableSpaceMonad - -attribute [fun_prop] measurable_mPure measurable_mBind -attribute [simp] mPure_mBind mBind_assoc mBind_mPure_comp -attribute [grind <=] mPure_mBind - -variable {m : (α : Type u) → [MeasurableSpace α] → Type v} [MeasurableSpaceMonad m] - [∀ α, [MeasurableSpace α] → MeasurableSpace (m α)] [LawfulMeasurableSpaceMonad m] - {α β γ : Type u} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] - -@[simp] theorem mMap_mPure {f : α → β} (hf : Measurable f) (x : α) : - f <$>ₘ (mPure x : m α) = mPure (f x) := by - rw [← mBind_mPure_comp hf, mPure_mBind _ (by fun_prop)] - -@[simp] theorem mBind_mPure (x : m α) : x >>=ₘ mPure = x := by - change x >>=ₘ (fun a => (mPure (id a))) = x - rw [mBind_mPure_comp (by fun_prop), id_mMap] - -theorem mMap_eq_mPure_mBind {f : α → β} (hf : Measurable f) (x : m α) : - f <$>ₘ x = x >>=ₘ fun a => mPure (f a) := by - rw [← mBind_mPure_comp hf x] - -theorem mBind_mPure_unit {x : m PUnit} : (x >>=ₘ fun _ => mPure ⟨⟩) = x := by rw [mBind_mPure] - -@[simp] theorem mMap_mBind {f : β → γ} (hf : Measurable f) (x : m α) - {g : α → m β} (hg : Measurable g) : - f <$>ₘ (x >>=ₘ g) = x >>=ₘ fun a => f <$>ₘ g a := by - rw [← mBind_mPure_comp hf, mBind_assoc _ hg (by fun_prop)] - simp (disch := fun_prop) [mBind_mPure_comp] - -@[simp] theorem mBind_mMap_left {f : α → β} (hf : Measurable f) (x : m α) - {g : β → m γ} (hg : Measurable g) : - ((f <$>ₘ x) >>=ₘ fun b => g b) = (x >>=ₘ fun a => g (f a)) := by - rw [← mBind_mPure_comp hf] - simp (disch := fun_prop) only [mBind_assoc, mPure_mBind] - -end RandomDo diff --git a/RandomDoNext/MeasurableSpaceMonad/Notation.lean b/RandomDoNext/MeasurableSpaceMonad/Notation.lean deleted file mode 100644 index 4680585..0000000 --- a/RandomDoNext/MeasurableSpaceMonad/Notation.lean +++ /dev/null @@ -1,16 +0,0 @@ -/- -Copyright (c) 2026 David Ledvinka. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: David Ledvinka --/ -module - -public import RandomDoNext.MeasurableSpaceMonad.Notation.Basic -public import RandomDoNext.MeasurableSpaceMonad.Notation.ForIn - -/-! -# Syntax for polymorphic measurable-space monad programs - -Provides `rdo` and collection iteration. The operations and iteration instances are supplied -by the caller; importing this module does not select a concrete interpretation. --/ diff --git a/RandomDoNext/MeasurableSpaceMonad/Notation/Basic.lean b/RandomDoNext/MeasurableSpaceMonad/Notation/Basic.lean deleted file mode 100644 index 41a7dd7..0000000 --- a/RandomDoNext/MeasurableSpaceMonad/Notation/Basic.lean +++ /dev/null @@ -1,81 +0,0 @@ -/- -Copyright (c) 2026 David Ledvinka. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: David Ledvinka --/ -module - -public import RandomDoNext.MeasurableSpaceMonad.Core.Basic -public import Mathlib.MeasureTheory.MeasurableSpace.Prod -public meta import Lean.Elab.BuiltinDo - -/-! -# `rdo` notation - -`rdo` elaborates a program using the measurable-space operations `mPure` and `mBind`. -It reuses Lean's `do` elaborators for binding, branching, mutation, and early return, supplying -the additional measurable-space argument when constructing a computation type or operation. - -`randOps` adapts `DoOps.default` from `Lean/Elab/Do/Basic.lean`. Collection iteration is provided -separately by `RandomDoNext.MeasurableSpaceMonad.Notation.ForIn`. - -Adapted from `RandomDo/Monad/Notation.lean` at main commit `150ecab`. No concrete monad instance -is needed to elaborate a polymorphic program. --/ - -open Lean Lean.Parser Lean.Parser.Term Lean.Meta Lean.Elab Lean.Elab.Do Lean.Elab.Term Std Meta -open RandomDo MeasurableSpacePure MeasurableSpaceBind - -public meta section - -namespace RandomDo.RDo - -/-- Define `DoOp`s for `rdo` notation. -/ -def randOps : DoOps := { DoOps.default with - mkPureApp α e := do - let ⟨m, u, v, _, _⟩ := (← read).monadInfo - let α ← Term.ensureHasType (mkSort (mkLevelSucc u)) α - let e ← Term.ensureHasType α e - let instPure ← mkInstMVar (.app (mkConst ``MeasurableSpacePure [u,v]) m) - let instPure ← instantiateMVars instPure - let σ ← mkInstMVar (.app (mkConst ``MeasurableSpace [u]) α) - let σ ← instantiateMVars σ - return mkAppN (mkConst ``mPure [u, v]) #[m, instPure, α, σ, e] - mkBindApp α β e k := do - let ⟨m, u, v, _, _⟩ := (← read).monadInfo - let α ← Term.ensureHasType (mkSort (mkLevelSucc u)) α - let σα ← mkInstMVar (.app (mkConst ``MeasurableSpace [u]) α) - let σβ ← mkInstMVar (.app (mkConst ``MeasurableSpace [u]) β) - let mα := mkApp2 m α σα - let mβ := mkApp2 m β σβ - let e ← Term.ensureHasType mα e - let k ← Term.ensureHasType (← mkArrow α mβ) k - let σα ← instantiateMVars σα - let σβ ← instantiateMVars σβ - let instBind ← mkInstMVar (.app (mkConst ``MeasurableSpaceBind [u, v]) m) - let instBind ← instantiateMVars instBind - return mkAppN (mkConst ``mBind [u, v]) #[m, instBind, α, β, σα, σβ, e, k] - isPureApp? e := - if e.isAppOfArity ``mPure 5 then some (e.getArg! 4) else none - splitMonadApp? type := do - let .app m _ := type.consumeMData | return none - let .app m resultType := m.consumeMData | return none - unless ← isType resultType do return none - let u ← getDecLevel resultType - let v ← getDecLevel type - return some ({ m := m, u := u.normalize, v := v.normalize }, resultType) - mkMonadApp α := do - let ⟨m, u, _, _, _⟩ := (← read).monadInfo - let σ ← mkInstMVar (mkApp (mkConst ``MeasurableSpace [u]) α) - return mkApp2 m α σ - } - -/-- The `do` notation for writing monadic programs depending on a `MeasurableSpace` instance. -/ -syntax (name := randKind) "rdo" doSeq : term - -/-- Define `rdo` notation elaborator. -/ -@[term_elab randKind] def elabRand : Term.TermElab := fun stx et? => do - let `(rdo $doSeq) := stx | throwUnsupportedSyntax - elabDoWith randOps doSeq et? - -end RandomDo.RDo diff --git a/TestNext.lean b/TestNext.lean index 6c1e48c..96afc04 100644 --- a/TestNext.lean +++ b/TestNext.lean @@ -3,4 +3,3 @@ module -- shake: keep-all --deprecated_module: ignore public import TestNext.MeasurableSpaceMonad.Core public import TestNext.MeasurableSpaceMonad.ImportBoundary public import TestNext.MeasurableSpaceMonad.Notation -public import TestNext.MeasurableSpaceMonad.NotationBasic diff --git a/TestNext/MeasurableSpaceMonad/Core.lean b/TestNext/MeasurableSpaceMonad/Core.lean index 22cec99..ee6f838 100644 --- a/TestNext/MeasurableSpaceMonad/Core.lean +++ b/TestNext/MeasurableSpaceMonad/Core.lean @@ -5,7 +5,7 @@ Authors: David Ledvinka -/ module -import RandomDoNext.MeasurableSpaceMonad.Core +import RandomDo.MeasurableSpaceMonad.Core /-! # Polymorphic reasoning checks diff --git a/TestNext/MeasurableSpaceMonad/ImportBoundary.lean b/TestNext/MeasurableSpaceMonad/ImportBoundary.lean index 5d07f5c..8dc21b7 100644 --- a/TestNext/MeasurableSpaceMonad/ImportBoundary.lean +++ b/TestNext/MeasurableSpaceMonad/ImportBoundary.lean @@ -5,12 +5,12 @@ Authors: David Ledvinka -/ module -import RandomDoNext +import RandomDo.MeasurableSpaceMonad.Notation /-! # Isolation of the polymorphic foundation -The complete rebuilt library must not pull in the original monad classes, concrete measure +The new notation import must not pull in the original monad classes, concrete measure semantics, or random-number implementations. These checks also catch transitive imports. -/ diff --git a/TestNext/MeasurableSpaceMonad/Notation.lean b/TestNext/MeasurableSpaceMonad/Notation.lean index a9183dd..780b5fe 100644 --- a/TestNext/MeasurableSpaceMonad/Notation.lean +++ b/TestNext/MeasurableSpaceMonad/Notation.lean @@ -5,13 +5,13 @@ Authors: David Ledvinka -/ module -public import RandomDoNext.MeasurableSpaceMonad.Notation +public import RandomDo.MeasurableSpaceMonad.Notation /-! # Elaboration without a concrete interpretation -The programs below use only abstract operation and iteration instances. They check the split -notation imports, mutable state, membership proofs, nested loops, and early control flow. +The programs below use only abstract operation and iteration instances. They check the +notation import, mutable state, membership proofs, nested loops, and early control flow. -/ open RandomDo MeasurableSpacePure MeasurableSpaceBind @@ -87,4 +87,15 @@ def control [MeasurableSpaceForIn m (List α) α] acc ← step x acc return acc +/-- Branching carries both abstract mutable values. -/ +def branchPair {m : (α : Type u) → [MeasurableSpace α] → Type v} [MeasurableSpaceMonad m] + {α β : Type u} [MeasurableSpace α] [MeasurableSpace β] + (a : α) (b : β) (choose : Bool) (left : α → m α) (right : β → m β) : m (α × β) := rdo + let mut x := a + let mut y := b + if choose then + x ← left x + y ← right y + return (x, y) + end TestNext.MeasurableSpaceMonad diff --git a/TestNext/MeasurableSpaceMonad/NotationBasic.lean b/TestNext/MeasurableSpaceMonad/NotationBasic.lean deleted file mode 100644 index 0ae5256..0000000 --- a/TestNext/MeasurableSpaceMonad/NotationBasic.lean +++ /dev/null @@ -1,36 +0,0 @@ -/- -Copyright (c) 2026 David Ledvinka. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: David Ledvinka --/ -module - -public import RandomDoNext.MeasurableSpaceMonad.Notation.Basic - -/-! -# Basic notation as a standalone import - -Updating two mutable variables across a branch requires a measurable space on their product. -This example must elaborate without importing the collection-loop notation or an interpretation. --/ - -open RandomDo - -@[expose] public section - -namespace TestNext.MeasurableSpaceMonad - -universe u v - -/-- Branching carries both abstract mutable values. -/ -def branchPair {m : (α : Type u) → [MeasurableSpace α] → Type v} [MeasurableSpaceMonad m] - {α β : Type u} [MeasurableSpace α] [MeasurableSpace β] - (a : α) (b : β) (choose : Bool) (left : α → m α) (right : β → m β) : m (α × β) := rdo - let mut x := a - let mut y := b - if choose then - x ← left x - y ← right y - return (x, y) - -end TestNext.MeasurableSpaceMonad diff --git a/lakefile.toml b/lakefile.toml index 649890d..ea66cf7 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -1,5 +1,5 @@ name = "RandomDo" -defaultTargets = ["RandomDo", "RandomDoNext"] +defaultTargets = ["RandomDo"] lintDriver = "batteries/runLinter" testDriver = "Test" @@ -21,9 +21,6 @@ precompileModules = true [[lean_lib]] name = "RandomDo" -[[lean_lib]] -name = "RandomDoNext" - [[lean_lib]] name = "TestNext" From af55bde661c7ecacd20c146eb48f81ccc5f1ec2a Mon Sep 17 00:00:00 2001 From: David Ledvinka Date: Mon, 26 Oct 2026 18:36:24 +0000 Subject: [PATCH 03/13] Defer ForIn support and document the monad foundation --- RandomDo/MeasurableSpaceMonad/Core.lean | 82 ++----- RandomDo/MeasurableSpaceMonad/Notation.lean | 235 +------------------- TestNext/MeasurableSpaceMonad/Notation.lean | 53 +---- 3 files changed, 38 insertions(+), 332 deletions(-) diff --git a/RandomDo/MeasurableSpaceMonad/Core.lean b/RandomDo/MeasurableSpaceMonad/Core.lean index a070899..30056f1 100644 --- a/RandomDo/MeasurableSpaceMonad/Core.lean +++ b/RandomDo/MeasurableSpaceMonad/Core.lean @@ -5,25 +5,37 @@ Authors: David Ledvinka -/ module -public import Mathlib.MeasureTheory.MeasurableSpace.Basic public import Mathlib.MeasureTheory.MeasurableSpace.Constructions public import Mathlib.Tactic.FunProp /-! -# Measurable-space monads +# Measurable space monads -A measurable-space monad takes a result type together with its measurable-space instance: -`m : (α : Type u) → [MeasurableSpace α] → Type v`. This file contains the operations, conditional -functor and monad laws, and generic iteration interfaces from -`RandomDo/Monad/MeasurableSpace.lean` at main commit `150ecab`. +This file defines functor and monad interfaces for type constructors of the form +`m : (α : Type u) → [MeasurableSpace α] → Type v`. The operations accept arbitrary functions. +The corresponding laws require measurability of maps and continuations, and a measurable space +on each computation type `m α`. -The operations accept ordinary functions. The lawfulness classes require a measurable space on -each computation type and state laws for measurable maps and continuations. Concrete monad and -collection implementations belong in separate modules. +## Main definitions -Declarations live in `RandomDo`. Opening this namespace also enables the scoped mapping -notation `<$>ₘ` and sequencing notation `>>=ₘ`. Import -`RandomDo.MeasurableSpaceMonad.Notation` to write programs using `rdo`. +* `RandomDo.MeasurableSpaceFunctor`: mapping functions over computations on measurable types. +* `RandomDo.MeasurableSpacePure`: embedding a value into a computation. +* `RandomDo.MeasurableSpaceBind`: sequencing computations with a continuation. +* `RandomDo.MeasurableSpaceMonad`: combines mapping, pure, and bind, with mapping defined by + pure and bind by default. +* `RandomDo.LawfulMeasurableSpaceFunctor`: functor laws for measurable maps, together with + measurability of mapping. +* `RandomDo.LawfulMeasurableSpaceMonad`: monad laws for measurable continuations, together with + measurability of pure and bind. + +## Notation + +The following notation is available in the `RandomDo` scope: + +* `f <$>ₘ x`: `RandomDo.MeasurableSpaceFunctor.mMap f x`. +* `x >>=ₘ f`: `RandomDo.MeasurableSpaceBind.mBind x f`. + +Import `RandomDo.MeasurableSpaceMonad.Notation` for `rdo` notation. -/ @[expose] public section @@ -32,8 +44,6 @@ namespace RandomDo open Function -section - universe u v section MeasurableSpaceMonad @@ -220,48 +230,4 @@ theorem mBind_mPure_unit {x : m PUnit} : (x >>=ₘ fun _ => mPure ⟨⟩) = x := end Lawful -end - -section MeasurableSpaceFor - -universe uρ uα u v - -variable {α : Type u} [mα : MeasurableSpace α] (m : (α : Type u) → [MeasurableSpace α] → Type v) - -/-- The disjoint-union measurable space on the two possible loop-step outcomes. -/ -instance instMeasurableSpaceForInStep {β : Type u} [mβ : MeasurableSpace β] : - MeasurableSpace (ForInStep β) := mβ.map ForInStep.yield ⊓ mβ.map ForInStep.done - -/-- -Monadic iteration in `rdo`-blocks, using the `for x in xs` notation. --/ -class MeasurableSpaceForIn (ρ : Type uρ) (α : outParam (Type uα)) where - /-- - Monadically iterates over the contents of a collection `xs`, with a local state `b` and the - possibility of early termination. - -/ - forIn {β : Type u} [MeasurableSpace β] (xs : ρ) (b : β) - (f : α → β → m (ForInStep β)) : m β - -/-- -Monadic iteration in `rdo`-blocks with a membership proof, using the `for h : x in xs` notation. --/ -class MeasurableSpaceForIn' (ρ : Type uρ) (α : outParam (Type uα)) - (d : outParam (Membership α ρ)) where - /-- - Monadically iterates over the contents of a collection `xs`, with a local state `b` and the - possibility of early termination. At each iteration, the body of the loop is provided with a proof - that the current element is in the collection. - -/ - forIn' {β : Type u} [MeasurableSpace β] (xs : ρ) (b : β) - (f : (a : α) → a ∈ xs → β → m (ForInStep β)) : m β - -@[simps] -instance (priority := 500) instMeasurableSpaceForInOfForIn' - {ρ : Type uρ} {α : Type uα} {d : Membership α ρ} [MeasurableSpaceForIn' m ρ α d] : - MeasurableSpaceForIn m ρ α where - forIn x b f := MeasurableSpaceForIn'.forIn' x b fun a _ s => f a s - -end MeasurableSpaceFor - end RandomDo diff --git a/RandomDo/MeasurableSpaceMonad/Notation.lean b/RandomDo/MeasurableSpaceMonad/Notation.lean index ce5bdeb..6c8d0a1 100644 --- a/RandomDo/MeasurableSpaceMonad/Notation.lean +++ b/RandomDo/MeasurableSpaceMonad/Notation.lean @@ -1,44 +1,33 @@ /- Copyright (c) 2026 David Ledvinka. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: David Ledvinka, Gaëtan Serré +Authors: David Ledvinka -/ module public import RandomDo.MeasurableSpaceMonad.Core public import Mathlib.MeasureTheory.MeasurableSpace.Prod public meta import Lean.Elab.BuiltinDo -public meta import Lean.Meta.ProdN /-! # `rdo` notation -`rdo` elaborates programs using the measurable-space operations `mPure` and `mBind`. It reuses -Lean's `do` elaborators for binding, branching, mutation, and early return, supplying the -additional measurable-space argument when constructing a computation type or operation. -Use `open RandomDo` (or `open scoped RandomDo`) to enable the notation. +This file defines `rdo` notation for computations in a measurable space monad. It reuses Lean's +`do` elaborators for binding, branching, mutation, and early return, supplying the additional +measurable-space argument when constructing a computation type or operation. -`for x in xs rdo body` uses `MeasurableSpaceForIn`; `for h : x in xs rdo body` uses -`MeasurableSpaceForIn'` and supplies a membership proof. The elaborator carries mutable state, -`break`, `continue`, and early returns through the loop accumulator. The measurable space on -`Option` below supports early returns. Callers supply the monad and collection instances. +## Main definitions -Adapted from `RandomDo/Monad/Notation.lean` at main commit `150ecab`, which mirrors Lean's -`DoOps`, parser, and `for` elaborator. The optional-value instance comes from -`RandomDo/Measurable.lean` at that commit. The control-info handler from the `loops` branch at -`c0f8f5b` supports nested loops. While-loop syntax and semantics are left to a later change. --/ +* `RandomDo.RDo.randOps`: adapts Lean's `DoOps` to measurable space monad operations. +* `RandomDo.RDo.elabRand`: elaborates an `rdo` block using `randOps`. -namespace RandomDo +## Notation -universe u +* `rdo ...`: a monadic program using `RandomDo.MeasurableSpacePure.mPure` and + `RandomDo.MeasurableSpaceBind.mBind`. -/-- The measurable space on optional results used to carry an early return. -A set of optional values is measurable exactly when its `some` preimage is measurable. -/ -public instance instMeasurableSpaceOption {α : Type u} [mα : MeasurableSpace α] : - MeasurableSpace (Option α) := mα.map some - -end RandomDo +Use `open RandomDo` (or `open scoped RandomDo`) to enable the notation. +-/ open Lean Lean.Parser Lean.Parser.Term Lean.Meta Lean.Elab Lean.Elab.Do Lean.Elab.Term Std Meta open RandomDo MeasurableSpacePure MeasurableSpaceBind @@ -97,206 +86,6 @@ def randOps : DoOps := { DoOps.default with let `(rdo $doSeq) := stx | throwUnsupportedSyntax elabDoWith randOps doSeq et? -/-- parses `_ : _ in` for `rdo` for loops -/ -def rdoForDecl := leading_parser - Lean.Parser.optional (atomic (Term.ident >> " : ")) >> termParser >> " in " >> - withForbidden "rdo" termParser - -/-- parser for `rdo` for loops -/ -def rdoFor := leading_parser - "for " >> sepBy1 rdoForDecl ", " >> "rdo " >> doSeq - -end RDo - --- Prefer the new parser when its scope is open, including alongside the legacy notation. -attribute [scoped doElem_parser high] RDo.rdoFor - -namespace RDo - -/-- Define expander for loops in `rdo` notation. Note this code mirrors core's implementation for -`do` notation as much as possible. -/ -@[macro rdoFor] def expandRDoFor : Macro := fun stx => do - match stx with - | `(rdoFor| for $[$_ : ]? $_:ident in $_ rdo $_) => - -- This is the target form of the expander, handled by `elabRDoFor` below. - Macro.throwUnsupported - | `(rdoFor| for%$tk $decls:rdoForDecl,* rdo $body) => - let decls := decls.getElems - let `(rdoForDecl| $[$h? : ]? $pattern in $xs) := decls[0]! | Macro.throwUnsupported - let mut doElems := #[] - let mut body := body - -- Expand `pattern` into an `Ident` `x`: - let x ← - if pattern.raw.isIdent then - pure ⟨pattern⟩ - else if pattern.raw.isOfKind ``Lean.Parser.Term.hole then - Term.mkFreshIdent pattern - else - -- This case is a last resort, because it introduces a `match` and that will cause eager - -- defaulting. In practice this means that `mut` vars default to `Nat` too often. - -- Hence we try to only generate a `match` if we absolutely must. - let x ← Term.mkFreshIdent pattern - body ← `(doSeq| match $x:term with | $pattern => $body) - pure x - -- Expand the remaining `rdoForDecl`s: - for rdoForDecl in decls[1...*] do - /- - Expand - ``` - for x in xs, y in ys rdo - body - ``` - into - ``` - let mut s := Std.toStream ys - for x in xs rdo - match Std.Stream.next? s with - | none => break - | some (y, s') => - s := s' - body - ``` - -/ - let `(rdoForDecl| $[$h? : ]? $y in $ys) := rdoForDecl | Macro.throwUnsupported - if let some h := h? then - Macro.throwErrorAt h "The proof annotation here has not been implemented yet." - /- Recall that `@` (explicit) disables `coeAtOutParam`. - We used `@` at `Stream` functions to make sure `resultIsOutParamSupport` is not used. -/ - let toStreamApp ← withRef ys `(@Std.toStream _ _ _ $ys) - let s := mkIdentFrom ys (← withFreshMacroScope <| MonadQuotation.addMacroScope `__s) - doElems := doElems.push (← `(doSeqItem| let mut $s := $toStreamApp:term)) - body ← `(doSeq| - match @Std.Stream.next? _ _ _ $s with - | none => break - | some ($y, s') => - $s:ident := s' - do $body) - doElems := doElems.push (← `(doSeqItem| for%$tk $[$h? : ]? $x:ident in $xs rdo $body)) - `(doElem| do $doElems*) - | _ => Macro.throwUnsupported - -/-- Define loop elaborator for `rdo` notation. Note this code mirrors core's implementation for -`do` notation as much as possible. -/ -@[doElem_elab rdoFor] def elabRDoFor : DoElab := fun stx dec => do - let `(rdoFor| for%$tk $[$h? : ]? $x:ident in $xs rdo $body) := stx | throwUnsupportedSyntax - let dec ← dec.ensureUnitAt tk - checkMutVarsForShadowing #[x] - let uα ← mkFreshLevelMVar - let uρ ← mkFreshLevelMVar - let α ← mkFreshExprMVar (mkSort (uα.succ)) (userName := `α) -- assigned by outParam - let ρ ← mkFreshExprMVar (mkSort (uρ.succ)) (userName := `ρ) -- assigned in the next line - let xs ← Term.elabTermEnsuringType xs ρ - let mi := (← read).monadInfo - let mutVars := (← read).mutVars - let info ← inferControlInfoSeq body - let oldReturnCont ← getReturnCont - let returnVarName ← mkFreshUserName `__r - let loopMutVars := mutVars.filter fun x => info.reassigns.contains x.getId - let loopMutVarNames := - if info.returnsEarly then - returnVarName :: (loopMutVars.map (·.getId)).toList - else - (loopMutVars.map (·.getId)).toList - let useLoopMutVars (e : Option Expr) : TermElabM (Array Expr) := do - let mut defs := #[] - unless e.isNone || info.returnsEarly do - throwError "Early returning {e} but the info said there is no early return" - if info.returnsEarly then - let returnVar ← - match e with - | none => mkNone oldReturnCont.resultType - | some e => mkSome oldReturnCont.resultType e - defs := defs.push returnVar - for x in loopMutVars do - let defn ← getLocalDeclFromUserName x.getId - Term.addTermInfo' x.ident defn.toExpr - -- ForIn forces the mut tuple into the universe mi.u: that of the do block result type. - -- If we don't do this, then we are stuck on solving constraints such as - -- `max ?u.46 ?u.47 =?= max (max ?u.22 ?u.46) ?u.47` - -- It's important we do this as a separate isLevelDefEq check on the decremented level because - -- otherwise (`ensureHasType (mkSort mi.u.succ)`) we are stuck on constraints like - -- `max (?u+1) (?v+1) =?= ?u+1` - let u ← getDecLevel defn.type - discard <| isLevelDefEq u mi.u - defs := defs.push defn.toExpr - if info.returnsEarly && loopMutVars.isEmpty then - defs := defs.push (mkConst ``Unit.unit) - return defs - let (preS, σ) ← mkProdMkN (← useLoopMutVars none) mi.u - let mσ ← Term.mkInstMVar <| mkApp (mkConst ``MeasurableSpace [mi.u]) σ - let (app, p?) ← match h? with - | none => - let instForIn ← Term.mkInstMVar <| - mkApp3 (mkConst ``MeasurableSpaceForIn [uρ, uα, mi.u, mi.v]) mi.m ρ α - let app := Lean.mkConst ``MeasurableSpaceForIn.forIn [uρ, uα, mi.u, mi.v] - let app := mkApp8 app mi.m ρ α instForIn σ mσ xs preS - pure (app, none) - | some _ => - let d ← mkFreshExprMVar (mkApp2 (mkConst ``Membership [uα, uρ]) α ρ) (userName := `d) - let instForIn ← Term.mkInstMVar <| - mkApp4 (mkConst ``MeasurableSpaceForIn' [uρ, uα, mi.u, mi.v]) mi.m ρ α d - let app := Lean.mkConst ``MeasurableSpaceForIn'.forIn' [uρ, uα, mi.u, mi.v] - let app := mkApp9 app mi.m ρ α d instForIn σ mσ xs preS - pure (app, some d) - let s ← mkFreshUserName `__s - let xh : Array (Name × (Array Expr → DoElabM Expr)) := match h?, p? with - | some h, some d => - #[(x.getId, fun _ => pure α), - (h.getId, fun x => pure (mkApp5 (mkConst ``Membership.mem [uα, uρ]) α ρ d xs x[0]!))] - | _, _ => - #[(x.getId, fun _ => pure α)] - let body ← - withLocalDeclsD xh fun xh => do - Term.addLocalVarInfo x xh[0]! - if let some h := h? then - Term.addLocalVarInfo h xh[1]! - withLocalDecl s .default σ (kind := .implDetail) fun loopS => do - mkLambdaFVars (xh.push loopS) <| ← do - bindMutVarsFromTuple loopMutVarNames loopS.fvarId! do - let newDoBlockResultType := mkApp (mkConst ``ForInStep [mi.u]) σ - withDoBlockResultType newDoBlockResultType do - let continueCont := do - let (tuple, _tupleTy) ← mkProdMkN (← useLoopMutVars none) mi.u - let yield := mkApp2 (mkConst ``ForInStep.yield [mi.u]) σ tuple - mkPureApp newDoBlockResultType yield - let breakCont := do - let (tuple, _tupleTy) ← mkProdMkN (← useLoopMutVars none) mi.u - let done := mkApp2 (mkConst ``ForInStep.done [mi.u]) σ tuple - mkPureApp newDoBlockResultType done - let returnCont := { oldReturnCont with k := fun e => do - let (tuple, _tupleTy) ← mkProdMkN (← useLoopMutVars (some e)) mi.u - let done := mkApp2 (mkConst ``ForInStep.done [mi.u]) σ tuple - mkPureApp newDoBlockResultType done - } - enterLoopBody breakCont continueCont returnCont do - -- Elaborate the loop body, which must have result type `PUnit`, just like the whole `for` loop. - elabDoSeq body { dec with k := continueCont, kind := .duplicable } - let forIn := mkApp app body - let γ := (← read).doBlockResultType - let rest ← - withLocalDeclD s σ fun postS => do mkLambdaFVars #[postS] <| ← do - bindMutVarsFromTuple loopMutVarNames postS.fvarId! do - if info.returnsEarly then - let ret ← getFVarFromUserName returnVarName - let ret ← if loopMutVars.isEmpty then mkAppM ``Prod.fst #[ret] else pure ret - /- Both branches produce an `m γ`, so the motive is constant and the matcher generated - for `Break.runK` is not needed: `Break.runK` itself is that case analysis. Note that it - takes the `none` branch first, the other way round from the matcher. -/ - let none := mkSimpleThunk (← dec.continueWithUnit) - let some ← withLocalDeclD (← mkFreshUserName `r) oldReturnCont.resultType fun r => do - mkLambdaFVars #[r] (← oldReturnCont.k r) - return mkAppN (mkConst ``Break.runK [mi.u, mi.v]) - #[oldReturnCont.resultType, ← mkMonadApp γ, ret, none, some] - else - dec.continueWithUnit - mkBindApp σ γ forIn rest - - -/-- Infer nested-loop control flow using Lean's ordinary `for` handler. -/ -@[doElem_control_info rdoFor] def controlInfoRDoFor : ControlInfoHandler := fun stx => do - let `(rdoFor| for $_:rdoForDecl,* rdo $body) := stx | throwUnsupportedSyntax - inferControlInfoElem (← `(doElem| for _ in #[()] do $body)) - end RDo end RandomDo diff --git a/TestNext/MeasurableSpaceMonad/Notation.lean b/TestNext/MeasurableSpaceMonad/Notation.lean index 780b5fe..2f089bb 100644 --- a/TestNext/MeasurableSpaceMonad/Notation.lean +++ b/TestNext/MeasurableSpaceMonad/Notation.lean @@ -10,8 +10,8 @@ public import RandomDo.MeasurableSpaceMonad.Notation /-! # Elaboration without a concrete interpretation -The programs below use only abstract operation and iteration instances. They check the -notation import, mutable state, membership proofs, nested loops, and early control flow. +The programs below use only abstract monad operations. They check return, binding, branching, +and mutable state through the notation import. -/ open RandomDo MeasurableSpacePure MeasurableSpaceBind @@ -38,55 +38,6 @@ def branch (x : m α) (p : α → Bool) (f : α → m α) : m α := rdo a ← f a return a -/-- An abstract collection loop can update its accumulator. -/ -def accumulate [MeasurableSpaceForIn m (List α) α] - (xs : List α) (initial : α) (step : α → α → m α) : m α := rdo - let mut acc := initial - for x in xs rdo - acc ← step x acc - return acc - -/-- Nested loops retain mutations of the outer accumulator. -/ -def nested [MeasurableSpaceForIn m (List α) α] - (xs : List α) (initial : α) (step : α → α → α → m α) : m α := rdo - let mut acc := initial - for x in xs rdo - for y in xs rdo - acc ← step x y acc - return acc - -/-- Membership-aware iteration passes the proof to the body. -/ -def withMembership [MeasurableSpaceForIn' m (List α) α inferInstance] - (xs : List α) (initial : α) (step : (x : α) → x ∈ xs → α → m α) : m α := rdo - let mut acc := initial - for h : x in xs rdo - acc ← step x h acc - return acc - -/-- A membership-aware instance also supplies ordinary iteration. -/ -def forgetMembership [MeasurableSpaceForIn' m (List α) α inferInstance] - (xs : List α) (initial : α) (step : α → α → m α) : m α := - accumulate xs initial step - -/-- A nested loop can return from the whole block. -/ -def firstMatch [MeasurableSpaceForIn m (List α) α] - (xs : List α) (fallback : α) (p : α → α → Bool) : m α := rdo - for x in xs rdo - for y in xs rdo - if p x y then - return y - return fallback - -/-- `break` and `continue` preserve the loop's accumulated state. -/ -def control [MeasurableSpaceForIn m (List α) α] - (xs : List α) (initial : α) (skip stop : α → Bool) (step : α → α → m α) : m α := rdo - let mut acc := initial - for x in xs rdo - if stop x then break - if skip x then continue - acc ← step x acc - return acc - /-- Branching carries both abstract mutable values. -/ def branchPair {m : (α : Type u) → [MeasurableSpace α] → Type v} [MeasurableSpaceMonad m] {α β : Type u} [MeasurableSpace α] [MeasurableSpace β] From 953e034343c673effe5b1502f98201d8d4f4ea16 Mon Sep 17 00:00:00 2001 From: David Ledvinka Date: Mon, 26 Oct 2026 19:16:28 +0000 Subject: [PATCH 04/13] Explain the measurable monad hierarchy and Applicative omission --- RandomDo/MeasurableSpaceMonad/Core.lean | 34 ++++++++++++++++++++++--- 1 file changed, 30 insertions(+), 4 deletions(-) diff --git a/RandomDo/MeasurableSpaceMonad/Core.lean b/RandomDo/MeasurableSpaceMonad/Core.lean index 30056f1..f2b59f3 100644 --- a/RandomDo/MeasurableSpaceMonad/Core.lean +++ b/RandomDo/MeasurableSpaceMonad/Core.lean @@ -11,10 +11,11 @@ public import Mathlib.Tactic.FunProp /-! # Measurable space monads -This file defines functor and monad interfaces for type constructors of the form -`m : (α : Type u) → [MeasurableSpace α] → Type v`. The operations accept arbitrary functions. -The corresponding laws require measurability of maps and continuations, and a measurable space -on each computation type `m α`. +This file defines `MeasurableSpaceFunctor` and `MeasurableSpaceMonad` as classes on type +constructors of the form `m : (α : Type u) → [MeasurableSpace α] → Type v`. They play the roles +of Lean's core `Functor` and `Monad` for types equipped with a `MeasurableSpace` instance. +The lawful classes express the corresponding functor and monad laws for measurable maps and +continuations between measurable spaces. ## Main definitions @@ -36,6 +37,31 @@ The following notation is available in the `RandomDo` scope: * `x >>=ₘ f`: `RandomDo.MeasurableSpaceBind.mBind x f`. Import `RandomDo.MeasurableSpaceMonad.Notation` for `rdo` notation. + +## Implementation details + +The development mirrors Lean core's intermediate operation classes (`Functor`, `Pure`, and +`Bind`) and separate `Lawful*` classes in `Init/Prelude.lean` and +`Init/Control/Lawful/Basic.lean`. As in core, the default mapping operation is defined using pure +and bind. Operations accept ordinary functions; measurability hypotheses belong to the laws. + +We omit core's `Applicative` layer. Ignoring its lazy argument, `Seq.seq` has type +`m (α → β) → m α → m β`. A general measurable analogue would require function spaces compatible +with evaluation `(f, x) ↦ f x`. The category of measurable spaces is not cartesian closed, so +such function spaces do not exist in general. In contrast, `mBind` receives its continuation +as an ordinary function; it does not require a measurable space on the type of continuations. + +For a concrete obstruction, let `F` be the set of Borel-measurable functions `ℝ → ℝ`. +Aumann's theorem states that no σ-algebra on `F` makes `ev : F × ℝ → ℝ`, `ev (f, x) = f x`, +measurable for the product σ-algebra, where `ℝ` carries its Borel σ-algebra. See Proposition 6 +of the reference below. Product-based formulations of applicative operations remain possible; +the obstruction concerns a general function-space interface with compatible measurable evaluation. + +## References + +* C. Heunen, O. Kammar, S. Staton, H. Yang, + [A Convenient Category for Higher-Order Probability Theory](https://arxiv.org/abs/1701.02547), + §II.B, Proposition 6 (Aumann's theorem). -/ @[expose] public section From 9d81bb6e6f9d25e8ff4f91ae8c0fe83c7aa0b5ff Mon Sep 17 00:00:00 2001 From: David Ledvinka Date: Mon, 26 Oct 2026 19:57:24 +0000 Subject: [PATCH 05/13] Restore the original user-written module introduction --- RandomDo/MeasurableSpaceMonad/Core.lean | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/RandomDo/MeasurableSpaceMonad/Core.lean b/RandomDo/MeasurableSpaceMonad/Core.lean index f2b59f3..838d9a7 100644 --- a/RandomDo/MeasurableSpaceMonad/Core.lean +++ b/RandomDo/MeasurableSpaceMonad/Core.lean @@ -11,11 +11,10 @@ public import Mathlib.Tactic.FunProp /-! # Measurable space monads -This file defines `MeasurableSpaceFunctor` and `MeasurableSpaceMonad` as classes on type -constructors of the form `m : (α : Type u) → [MeasurableSpace α] → Type v`. They play the roles -of Lean's core `Functor` and `Monad` for types equipped with a `MeasurableSpace` instance. -The lawful classes express the corresponding functor and monad laws for measurable maps and -continuations between measurable spaces. +This file defines `MeasurableSpaceFunctor` and `MeasurableSpaceMonad` as classes on functions of +the form `m : (α : Type u) → [MeasurableSpace α] → Type v`. They play the role of core lean's +`Functor` and `Monad` for types equipped with a `MeasurableSpace` instance. Assuming that instances +are lawful, this corresponds to functors and monads on the category of measure spaces respectfully. ## Main definitions From 07cbf001aba993828f37dca769ec7b6ebbb1ddfe Mon Sep 17 00:00:00 2001 From: David Ledvinka Date: Mon, 26 Oct 2026 20:13:59 +0000 Subject: [PATCH 06/13] Omit redundant namespace prefixes in the core module docs --- RandomDo/MeasurableSpaceMonad/Core.lean | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/RandomDo/MeasurableSpaceMonad/Core.lean b/RandomDo/MeasurableSpaceMonad/Core.lean index 838d9a7..b9205c3 100644 --- a/RandomDo/MeasurableSpaceMonad/Core.lean +++ b/RandomDo/MeasurableSpaceMonad/Core.lean @@ -18,22 +18,22 @@ are lawful, this corresponds to functors and monads on the category of measure s ## Main definitions -* `RandomDo.MeasurableSpaceFunctor`: mapping functions over computations on measurable types. -* `RandomDo.MeasurableSpacePure`: embedding a value into a computation. -* `RandomDo.MeasurableSpaceBind`: sequencing computations with a continuation. -* `RandomDo.MeasurableSpaceMonad`: combines mapping, pure, and bind, with mapping defined by +* `MeasurableSpaceFunctor`: mapping functions over computations on measurable types. +* `MeasurableSpacePure`: embedding a value into a computation. +* `MeasurableSpaceBind`: sequencing computations with a continuation. +* `MeasurableSpaceMonad`: combines mapping, pure, and bind, with mapping defined by pure and bind by default. -* `RandomDo.LawfulMeasurableSpaceFunctor`: functor laws for measurable maps, together with +* `LawfulMeasurableSpaceFunctor`: functor laws for measurable maps, together with measurability of mapping. -* `RandomDo.LawfulMeasurableSpaceMonad`: monad laws for measurable continuations, together with +* `LawfulMeasurableSpaceMonad`: monad laws for measurable continuations, together with measurability of pure and bind. ## Notation The following notation is available in the `RandomDo` scope: -* `f <$>ₘ x`: `RandomDo.MeasurableSpaceFunctor.mMap f x`. -* `x >>=ₘ f`: `RandomDo.MeasurableSpaceBind.mBind x f`. +* `f <$>ₘ x`: `MeasurableSpaceFunctor.mMap f x`. +* `x >>=ₘ f`: `MeasurableSpaceBind.mBind x f`. Import `RandomDo.MeasurableSpaceMonad.Notation` for `rdo` notation. From d8019a7240cd0bee1f3126789047770da1d95f12 Mon Sep 17 00:00:00 2001 From: David Ledvinka Date: Mon, 26 Oct 2026 20:33:37 +0000 Subject: [PATCH 07/13] Move the rebuilt measurable monad API into MeasureTheory --- RandomDo/MeasurableSpaceMonad/Core.lean | 6 +++--- RandomDo/MeasurableSpaceMonad/Notation.lean | 18 +++++++++--------- Test/Common.lean | 3 ++- Test/Computable.lean | 3 ++- Test/Polymorphic.lean | 5 ++++- TestNext/MeasurableSpaceMonad/Core.lean | 2 +- TestNext/MeasurableSpaceMonad/Notation.lean | 2 +- 7 files changed, 22 insertions(+), 17 deletions(-) diff --git a/RandomDo/MeasurableSpaceMonad/Core.lean b/RandomDo/MeasurableSpaceMonad/Core.lean index b9205c3..35a9e4e 100644 --- a/RandomDo/MeasurableSpaceMonad/Core.lean +++ b/RandomDo/MeasurableSpaceMonad/Core.lean @@ -30,7 +30,7 @@ are lawful, this corresponds to functors and monads on the category of measure s ## Notation -The following notation is available in the `RandomDo` scope: +The following notation is available in the `MeasureTheory` scope: * `f <$>ₘ x`: `MeasurableSpaceFunctor.mMap f x`. * `x >>=ₘ f`: `MeasurableSpaceBind.mBind x f`. @@ -65,7 +65,7 @@ the obstruction concerns a general function-space interface with compatible meas @[expose] public section -namespace RandomDo +namespace MeasureTheory open Function @@ -255,4 +255,4 @@ theorem mBind_mPure_unit {x : m PUnit} : (x >>=ₘ fun _ => mPure ⟨⟩) = x := end Lawful -end RandomDo +end MeasureTheory diff --git a/RandomDo/MeasurableSpaceMonad/Notation.lean b/RandomDo/MeasurableSpaceMonad/Notation.lean index 6c8d0a1..a5723fd 100644 --- a/RandomDo/MeasurableSpaceMonad/Notation.lean +++ b/RandomDo/MeasurableSpaceMonad/Notation.lean @@ -18,26 +18,26 @@ measurable-space argument when constructing a computation type or operation. ## Main definitions -* `RandomDo.RDo.randOps`: adapts Lean's `DoOps` to measurable space monad operations. -* `RandomDo.RDo.elabRand`: elaborates an `rdo` block using `randOps`. +* `RDo.randOps`: adapts Lean's `DoOps` to measurable space monad operations. +* `RDo.elabRand`: elaborates an `rdo` block using `randOps`. ## Notation -* `rdo ...`: a monadic program using `RandomDo.MeasurableSpacePure.mPure` and - `RandomDo.MeasurableSpaceBind.mBind`. +* `rdo ...`: a monadic program using `MeasurableSpacePure.mPure` and + `MeasurableSpaceBind.mBind`. -Use `open RandomDo` (or `open scoped RandomDo`) to enable the notation. +Use `open MeasureTheory` (or `open scoped MeasureTheory`) to enable the notation. -/ open Lean Lean.Parser Lean.Parser.Term Lean.Meta Lean.Elab Lean.Elab.Do Lean.Elab.Term Std Meta -open RandomDo MeasurableSpacePure MeasurableSpaceBind +open MeasureTheory MeasurableSpacePure MeasurableSpaceBind public meta section -namespace RandomDo +namespace MeasureTheory /-- The `do` notation for writing monadic programs depending on a `MeasurableSpace` instance. -/ -scoped syntax (name := randKind) (priority := high) "rdo" doSeq : term +scoped syntax (name := randKind) "rdo" doSeq : term namespace RDo @@ -88,4 +88,4 @@ def randOps : DoOps := { DoOps.default with end RDo -end RandomDo +end MeasureTheory diff --git a/Test/Common.lean b/Test/Common.lean index 83934c5..500489e 100644 --- a/Test/Common.lean +++ b/Test/Common.lean @@ -1,6 +1,7 @@ module -public import RandomDo +public import RandomDo.NumLean.Distributions +public import RandomDo.Tactic.IsMarkov.Deriving public import Mathlib.Probability.Distributions.Bernoulli set_option linter.style.header false diff --git a/Test/Computable.lean b/Test/Computable.lean index 0b7752b..a86acd3 100644 --- a/Test/Computable.lean +++ b/Test/Computable.lean @@ -2,7 +2,8 @@ module public import Test.IsMarkov public import Test.Bind -public meta import RandomDo +public import RandomDo.Tactic.Computable.Counterparts +public meta import RandomDo.Tactic.Computable.Deriving import Batteries.Data.Float.Basic set_option linter.style.header false diff --git a/Test/Polymorphic.lean b/Test/Polymorphic.lean index 566bf7d..bd4f39e 100644 --- a/Test/Polymorphic.lean +++ b/Test/Polymorphic.lean @@ -1,7 +1,10 @@ module public import Test.IsMarkov -public meta import RandomDo +public import RandomDo.Tactic.Computable.Polymorphic.Polymorphic +public import RandomDo.Tactic.Computable.Polymorphic.Scalar +public meta import RandomDo.Tactic.Computable.Polymorphic.Polymorphic +public meta import RandomDo.Tactic.Computable.Polymorphic.Scalar import Batteries.Data.Float.Basic set_option linter.style.header false diff --git a/TestNext/MeasurableSpaceMonad/Core.lean b/TestNext/MeasurableSpaceMonad/Core.lean index ee6f838..fe24a5e 100644 --- a/TestNext/MeasurableSpaceMonad/Core.lean +++ b/TestNext/MeasurableSpaceMonad/Core.lean @@ -14,7 +14,7 @@ Exercise the public simplifier and measurability interfaces with an abstract mon independent result/computation universes. No concrete interpretation is installed. -/ -open RandomDo MeasurableSpacePure MeasurableSpaceBind MeasurableSpaceFunctor +open MeasureTheory MeasurableSpacePure MeasurableSpaceBind MeasurableSpaceFunctor universe u v diff --git a/TestNext/MeasurableSpaceMonad/Notation.lean b/TestNext/MeasurableSpaceMonad/Notation.lean index 2f089bb..8c6223a 100644 --- a/TestNext/MeasurableSpaceMonad/Notation.lean +++ b/TestNext/MeasurableSpaceMonad/Notation.lean @@ -14,7 +14,7 @@ The programs below use only abstract monad operations. They check return, bindin and mutable state through the notation import. -/ -open RandomDo MeasurableSpacePure MeasurableSpaceBind +open MeasureTheory MeasurableSpacePure MeasurableSpaceBind @[expose] public section From b1db789394e077efa5e935d5467a87d57b584b74 Mon Sep 17 00:00:00 2001 From: David Ledvinka Date: Mon, 26 Oct 2026 20:33:38 +0000 Subject: [PATCH 08/13] Cite Aumann directly for the function-space obstruction --- RandomDo/MeasurableSpaceMonad/Core.lean | 16 +++++++++------- 1 file changed, 9 insertions(+), 7 deletions(-) diff --git a/RandomDo/MeasurableSpaceMonad/Core.lean b/RandomDo/MeasurableSpaceMonad/Core.lean index 35a9e4e..9375ab6 100644 --- a/RandomDo/MeasurableSpaceMonad/Core.lean +++ b/RandomDo/MeasurableSpaceMonad/Core.lean @@ -50,17 +50,19 @@ with evaluation `(f, x) ↦ f x`. The category of measurable spaces is not carte such function spaces do not exist in general. In contrast, `mBind` receives its continuation as an ordinary function; it does not require a measurable space on the type of continuations. -For a concrete obstruction, let `F` be the set of Borel-measurable functions `ℝ → ℝ`. -Aumann's theorem states that no σ-algebra on `F` makes `ev : F × ℝ → ℝ`, `ev (f, x) = f x`, -measurable for the product σ-algebra, where `ℝ` carries its Borel σ-algebra. See Proposition 6 -of the reference below. Product-based formulations of applicative operations remain possible; +For a concrete obstruction, let `I = [0, 1]` carry its Borel σ-algebra and let `F` be the set +of Borel-measurable functions `I → I`. Aumann shows that no σ-algebra on `F` makes +`ev : F × I → I`, `ev (f, x) = f x`, measurable for the product σ-algebra. See §3 of the +reference below, where this is stated as the inadmissibility of `I^I`. +Product-based formulations of applicative operations remain possible; the obstruction concerns a general function-space interface with compatible measurable evaluation. ## References -* C. Heunen, O. Kammar, S. Staton, H. Yang, - [A Convenient Category for Higher-Order Probability Theory](https://arxiv.org/abs/1701.02547), - §II.B, Proposition 6 (Aumann's theorem). +* R. J. Aumann, + [Borel structures for function spaces](https://doi.org/10.1215/ijm/1255631584), + Illinois Journal of Mathematics 5(4) (1961), 614–630, §3 + ([author's reprint](https://math.huji.ac.il/~raumann/pdf/66.pdf#page=8)). -/ @[expose] public section From afa7d0c67e5cfa080af9be1d5f4642c631c1c016 Mon Sep 17 00:00:00 2001 From: David Ledvinka Date: Mon, 26 Oct 2026 20:49:20 +0000 Subject: [PATCH 09/13] Clarify the measurability distinction between bind and seq --- RandomDo/MeasurableSpaceMonad/Core.lean | 39 ++++++++++--------------- 1 file changed, 15 insertions(+), 24 deletions(-) diff --git a/RandomDo/MeasurableSpaceMonad/Core.lean b/RandomDo/MeasurableSpaceMonad/Core.lean index 9375ab6..5b3a6ef 100644 --- a/RandomDo/MeasurableSpaceMonad/Core.lean +++ b/RandomDo/MeasurableSpaceMonad/Core.lean @@ -39,30 +39,21 @@ Import `RandomDo.MeasurableSpaceMonad.Notation` for `rdo` notation. ## Implementation details -The development mirrors Lean core's intermediate operation classes (`Functor`, `Pure`, and -`Bind`) and separate `Lawful*` classes in `Init/Prelude.lean` and -`Init/Control/Lawful/Basic.lean`. As in core, the default mapping operation is defined using pure -and bind. Operations accept ordinary functions; measurability hypotheses belong to the laws. - -We omit core's `Applicative` layer. Ignoring its lazy argument, `Seq.seq` has type -`m (α → β) → m α → m β`. A general measurable analogue would require function spaces compatible -with evaluation `(f, x) ↦ f x`. The category of measurable spaces is not cartesian closed, so -such function spaces do not exist in general. In contrast, `mBind` receives its continuation -as an ordinary function; it does not require a measurable space on the type of continuations. - -For a concrete obstruction, let `I = [0, 1]` carry its Borel σ-algebra and let `F` be the set -of Borel-measurable functions `I → I`. Aumann shows that no σ-algebra on `F` makes -`ev : F × I → I`, `ev (f, x) = f x`, measurable for the product σ-algebra. See §3 of the -reference below, where this is stated as the inadmissibility of `I^I`. -Product-based formulations of applicative operations remain possible; -the obstruction concerns a general function-space interface with compatible measurable evaluation. - -## References - -* R. J. Aumann, - [Borel structures for function spaces](https://doi.org/10.1215/ijm/1255631584), - Illinois Journal of Mathematics 5(4) (1961), 614–630, §3 - ([author's reprint](https://math.huji.ac.il/~raumann/pdf/66.pdf#page=8)). +The development of `MeasurableSpaceMonad` mirrors Lean core's `Monad`, with intermediate classes +`MeasurableSpaceFunctor`, `MeasurableSpacePure`, and `MeasurableSpaceBind`. It extends these +three classes directly, omitting the `Applicative` layer. + +Ignoring laziness, core's `Seq.seq` has type `m (α → β) → m α → m β`. A function-space analogue +with measurable application would require evaluation `(f, x) ↦ f x` to be jointly measurable. +Even the space of all Borel functions `[0, 1] → [0, 1]` admits no σ-algebra with this property; +see [Aumann's counterexample](https://math.huji.ac.il/~raumann/pdf/66.pdf#page=8), §3, the +unnumbered example before Lemma 3.1. Consequently, measurable spaces are not cartesian closed. + +For `mBind`, the laws fix a measurable continuation `k : α → m β` and require +`μ ↦ mBind μ k` to be measurable. They impose no measurability as `k` varies over a function +space, so no measurable space of continuations is needed. The obstruction concerns jointly +measurable function application; product-based applicative formulations remain possible. + -/ @[expose] public section From bc65172fcf04335e0fb2ba6b0ae967052d6eb576 Mon Sep 17 00:00:00 2001 From: David Ledvinka Date: Mon, 26 Oct 2026 20:56:06 +0000 Subject: [PATCH 10/13] Restore the original wording and continue the implementation note --- RandomDo/MeasurableSpaceMonad/Core.lean | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) diff --git a/RandomDo/MeasurableSpaceMonad/Core.lean b/RandomDo/MeasurableSpaceMonad/Core.lean index 5b3a6ef..fc1985a 100644 --- a/RandomDo/MeasurableSpaceMonad/Core.lean +++ b/RandomDo/MeasurableSpaceMonad/Core.lean @@ -39,12 +39,13 @@ Import `RandomDo.MeasurableSpaceMonad.Notation` for `rdo` notation. ## Implementation details -The development of `MeasurableSpaceMonad` mirrors Lean core's `Monad`, with intermediate classes -`MeasurableSpaceFunctor`, `MeasurableSpacePure`, and `MeasurableSpaceBind`. It extends these -three classes directly, omitting the `Applicative` layer. - -Ignoring laziness, core's `Seq.seq` has type `m (α → β) → m α → m β`. A function-space analogue -with measurable application would require evaluation `(f, x) ↦ f x` to be jointly measurable. +The development of `MeasurableSpaceMonad` mirrors the development of `Monad` in core lean, including +the definition of intermediate classes `MeasurableSpaceFunctor`, `MeasurableSpacePure`, and +`MeasurableSpaceBind` except with the key exception that there is no `MeasurableSpaceApplicative` +and instead `MeasurableSpaceMonad` extends all three of the preceding classes directly. This is +because defining a `MeasurableSpaceApplicative` would require defining a measurable analogue of +`Seq.seq : m (α → β) → m α → m β` but +there is no general function space with jointly measurable evaluation `(f, x) ↦ f x`. Even the space of all Borel functions `[0, 1] → [0, 1]` admits no σ-algebra with this property; see [Aumann's counterexample](https://math.huji.ac.il/~raumann/pdf/66.pdf#page=8), §3, the unnumbered example before Lemma 3.1. Consequently, measurable spaces are not cartesian closed. From 66c83cdbf3cf7cb90e4b016727f8c2fa24706f82 Mon Sep 17 00:00:00 2001 From: David Ledvinka Date: Mon, 26 Oct 2026 21:04:03 +0000 Subject: [PATCH 11/13] Complete the implementation note with the identity monad example --- RandomDo/MeasurableSpaceMonad/Core.lean | 17 +++++++---------- 1 file changed, 7 insertions(+), 10 deletions(-) diff --git a/RandomDo/MeasurableSpaceMonad/Core.lean b/RandomDo/MeasurableSpaceMonad/Core.lean index fc1985a..b584969 100644 --- a/RandomDo/MeasurableSpaceMonad/Core.lean +++ b/RandomDo/MeasurableSpaceMonad/Core.lean @@ -44,16 +44,13 @@ the definition of intermediate classes `MeasurableSpaceFunctor`, `MeasurableSpac `MeasurableSpaceBind` except with the key exception that there is no `MeasurableSpaceApplicative` and instead `MeasurableSpaceMonad` extends all three of the preceding classes directly. This is because defining a `MeasurableSpaceApplicative` would require defining a measurable analogue of -`Seq.seq : m (α → β) → m α → m β` but -there is no general function space with jointly measurable evaluation `(f, x) ↦ f x`. -Even the space of all Borel functions `[0, 1] → [0, 1]` admits no σ-algebra with this property; -see [Aumann's counterexample](https://math.huji.ac.il/~raumann/pdf/66.pdf#page=8), §3, the -unnumbered example before Lemma 3.1. Consequently, measurable spaces are not cartesian closed. - -For `mBind`, the laws fix a measurable continuation `k : α → m β` and require -`μ ↦ mBind μ k` to be measurable. They impose no measurability as `k` varies over a function -space, so no measurable space of continuations is needed. The obstruction concerns jointly -measurable function application; product-based applicative formulations remain possible. +`Seq.seq : m (α → β) → m α → m β`, and we would like such an operation to be measurable, but +requiring this operation to be jointly measurable would already fail for the identity monad: +there, `seq f x = f x`, so `seq` is precisely function evaluation. No σ-algebra on the space of +all measurable functions makes evaluation jointly measurable in general; see +[Aumann's counterexample](https://math.huji.ac.il/~raumann/pdf/66.pdf#page=8), §3, the unnumbered +example before Lemma 3.1. Our bind laws avoid this requirement by fixing a measurable +continuation `k` and requiring measurability only of `μ ↦ mBind μ k`. -/ From ad59547f16db6061d7dd7f68a5a215333fd1a4dc Mon Sep 17 00:00:00 2001 From: David Ledvinka Date: Mon, 26 Oct 2026 23:43:54 +0000 Subject: [PATCH 12/13] Improve MeasurableSpaceMonad Documentation --- RandomDo/MeasurableSpaceMonad/Core.lean | 89 +++++++++++++++---------- 1 file changed, 54 insertions(+), 35 deletions(-) diff --git a/RandomDo/MeasurableSpaceMonad/Core.lean b/RandomDo/MeasurableSpaceMonad/Core.lean index b584969..940bce5 100644 --- a/RandomDo/MeasurableSpaceMonad/Core.lean +++ b/RandomDo/MeasurableSpaceMonad/Core.lean @@ -12,21 +12,20 @@ public import Mathlib.Tactic.FunProp # Measurable space monads This file defines `MeasurableSpaceFunctor` and `MeasurableSpaceMonad` as classes on functions of -the form `m : (α : Type u) → [MeasurableSpace α] → Type v`. They play the role of core lean's +the form `m : (α : Type u) → [MeasurableSpace α] → Type v`. They play the role of Lean core's `Functor` and `Monad` for types equipped with a `MeasurableSpace` instance. Assuming that instances -are lawful, this corresponds to functors and monads on the category of measure spaces respectfully. +are lawful, this corresponds to functors and monads on the category of measurable spaces. ## Main definitions -* `MeasurableSpaceFunctor`: mapping functions over computations on measurable types. -* `MeasurableSpacePure`: embedding a value into a computation. -* `MeasurableSpaceBind`: sequencing computations with a continuation. -* `MeasurableSpaceMonad`: combines mapping, pure, and bind, with mapping defined by - pure and bind by default. -* `LawfulMeasurableSpaceFunctor`: functor laws for measurable maps, together with - measurability of mapping. -* `LawfulMeasurableSpaceMonad`: monad laws for measurable continuations, together with - measurability of pure and bind. +* `MeasurableSpaceFunctor`: A typeclass for functors on types equipped with a `MeasurableSpace` +instance. +* `MeasurableSpaceMonad`: A typeclass for monads on types equipped with a `MeasurableSpace` +instance. +* `LawfulMeasurableSpaceFunctor`: A `Prop`-valued typeclass which states that a given +`MeasurableSpaceFunctor` satisfies the laws of a functor on measurable spaces. +* `LawfulMeasurableSpaceMonad`: A `Prop`-valued typeclass which states that a given +`MeasurableSpaceMonad` satisfies the laws of a monad on measurable spaces. ## Notation @@ -35,22 +34,20 @@ The following notation is available in the `MeasureTheory` scope: * `f <$>ₘ x`: `MeasurableSpaceFunctor.mMap f x`. * `x >>=ₘ f`: `MeasurableSpaceBind.mBind x f`. -Import `RandomDo.MeasurableSpaceMonad.Notation` for `rdo` notation. - ## Implementation details -The development of `MeasurableSpaceMonad` mirrors the development of `Monad` in core lean, including +The development of `MeasurableSpaceMonad` mirrors the development of `Monad` in Lean core, including the definition of intermediate classes `MeasurableSpaceFunctor`, `MeasurableSpacePure`, and -`MeasurableSpaceBind` except with the key exception that there is no `MeasurableSpaceApplicative` -and instead `MeasurableSpaceMonad` extends all three of the preceding classes directly. This is -because defining a `MeasurableSpaceApplicative` would require defining a measurable analogue of -`Seq.seq : m (α → β) → m α → m β`, and we would like such an operation to be measurable, but -requiring this operation to be jointly measurable would already fail for the identity monad: -there, `seq f x = f x`, so `seq` is precisely function evaluation. No σ-algebra on the space of -all measurable functions makes evaluation jointly measurable in general; see -[Aumann's counterexample](https://math.huji.ac.il/~raumann/pdf/66.pdf#page=8), §3, the unnumbered -example before Lemma 3.1. Our bind laws avoid this requirement by fixing a measurable -continuation `k` and requiring measurability only of `μ ↦ mBind μ k`. +`MeasurableSpaceBind` except that there is no `MeasurableSpaceApplicative` and instead +`MeasurableSpaceMonad` extends all three of the preceding classes directly. This is because +defining a `MeasurableSpaceApplicative` would require defining an analogue of +`Seq.seq : m (α → β) → (Unit → m α) → m β`, and we would like such an operation to be jointly +measurable in `m (α → β)` and `Unit → m α`, but requiring this operation to be jointly measurable +would already fail for the identity monad: there, `seq f (fun _ => x) = f x`, so `seq` reduces to +function evaluation. No σ-algebra on the space of all measurable functions makes evaluation +jointly measurable in general; +see R. J. Aumann, [*Borel structures for function spaces*](https://doi.org/10.1215/ijm/1255631584), +*Illinois Journal of Mathematics* **5** (1961), no. 4, 614–630, §3. -/ @@ -64,16 +61,27 @@ universe u v section MeasurableSpaceMonad -/-- A functor on types with a `MeasurableSpace` instance. The `mMap` operator `<$>ₘ` is overloaded -via instances of this class. This class does not require proofs of the `MeasurableSpaceFunctor` -axioms. Proofs may be provided or required via the `LawfulMeasurableSpaceFunctor` class. -/ +/-- +A functor on types with a `MeasurableSpace` instance. This means a function +`f : (α : Type u) → [MeasurableSpace α] → Type v` equipped with an +`mMap [MeasurableSpace α] [MeasurableSpace β] : (α → β) → f α → f β` operator, +which can be written with the notation `<$>ₘ`. + +A lawful instance of this class requires a `MeasurableSpace` instance on each output type `f α`, +and that `mMap` maps measurable functions `α → β` to measurable functions `f α → f β`, maps +identity functions to identity functions, and respects composition of measurable functions. +This class does not require its instances to be lawful. Proofs of lawful instances can be +provided via the `Prop`-valued class `LawfulMeasurableSpaceFunctor`. + +Lawful instances of this class correspond to functors on the category of measurable spaces. +-/ class MeasurableSpaceFunctor (f : (α : Type u) → [MeasurableSpace α] → Type v) : Type (max (u+1) v) where /-- Applies a function inside a functor on measurable spaces. This is used to overload the `<$>ₘ` operator. - When mapping a constant function (if one cares about executing the code), use + When mapping a constant function in executable code, use `MeasurableSpaceFunctor.mMapConst` instead, because it may be more efficient. -/ mMap {α β : Type u} [MeasurableSpace α] [MeasurableSpace β] : (α → β) → f α → f β @@ -81,8 +89,8 @@ class MeasurableSpaceFunctor (f : (α : Type u) → [MeasurableSpace α] → Typ Mapping a constant function. Given `a : α` and `v : f β`, `mMapConst a v` is equivalent to `(fun _ => a) <$>ₘ v`. For some - functors, this can be implemented more efficiently; for all other functors, the default - implementation may be used. + functors where executable code is relevant, this can be implemented more efficiently; for all + other functors, the default implementation may be used. -/ mMapConst {α β : Type u} [MeasurableSpace α] [MeasurableSpace β] : α → f β → f α := mMap ∘ (const _) @@ -115,9 +123,21 @@ class MeasurableSpaceBind (m : (α : Type u) → [MeasurableSpace α] → Type v @[inherit_doc] scoped infixl:55 " >>=ₘ " => MeasurableSpaceBind.mBind -/-- Return, sequencing, and mapping for computations indexed by measurable result types. -By default, mapping sequences a computation with return. The operations accept ordinary functions; -measurability assumptions and laws are supplied separately by `LawfulMeasurableSpaceMonad`. -/ +/-- +A monad on types with a `MeasurableSpace` instance. + +Monads are an abstraction of sequential control flow and side effects in functional programming, +and `MeasurableSpaceMonad`s allow the use of this abstraction on programs taking values in +`MeasurableSpace`s. The canonical example of such a monad is `Measure` where programs +"written" in the `Measure` monad can represent programs with "random" outputs whose output +distribution is given by the output measure. `MeasurableSpaceMonad`s support `rdo` notation, +the measurable-space analogue of `do` notation, for specifying these programs. + +A lawful instance of this class should satisfy various properties so that the instance corresponds +to a monad on the category of measurable spaces. These are specified precisely in the `Prop`-valued +class `LawfulMeasurableSpaceMonad` and proofs of lawfulness can be given by defining an instance +of that class. +-/ class MeasurableSpaceMonad (m : (α : Type u) → [MeasurableSpace α] → Type v) : Type (max (u+1) v) extends MeasurableSpaceFunctor m, MeasurableSpacePure m, MeasurableSpaceBind m where @@ -190,8 +210,7 @@ class LawfulMeasurableSpaceMonad mBind_mPure_comp {α β : Type u} [MeasurableSpace α] [MeasurableSpace β] {f : α → β} (hf : Measurable f) (x : m α) : x >>=ₘ (fun a => mPure (f a)) = f <$>ₘ x - /-- `mPure` followed by `mBind` of a function application is equivalent to function - application. -/ + /-- Binding `mPure x` to a measurable function `f` is equivalent to applying `f` to `x`. -/ mPure_mBind {α β : Type u} [MeasurableSpace α] [MeasurableSpace β] (x : α) {f : α → m β} (hf : Measurable f) : mPure x >>=ₘ f = f x From 0462759e222f3b725a7200d723ce7ebc6b99622a Mon Sep 17 00:00:00 2001 From: David Ledvinka Date: Mon, 26 Oct 2026 23:43:54 +0000 Subject: [PATCH 13/13] Improve MeasurableSpaceMonad Documentation --- RandomDo/Monad/MeasurableSpace.lean | 88 +++++++++++++++++++++++------ 1 file changed, 70 insertions(+), 18 deletions(-) diff --git a/RandomDo/Monad/MeasurableSpace.lean b/RandomDo/Monad/MeasurableSpace.lean index b593969..eb2ebfe 100644 --- a/RandomDo/Monad/MeasurableSpace.lean +++ b/RandomDo/Monad/MeasurableSpace.lean @@ -9,19 +9,48 @@ public import Mathlib.Control.Random public import Mathlib.MeasureTheory.Measure.GiryMonad /-! -# Measurable Space Monad +# Measurable space monads -**TODO** +This file defines `MeasurableSpaceFunctor` and `MeasurableSpaceMonad` as classes on functions of +the form `m : (α : Type u) → [MeasurableSpace α] → Type v`. They play the role of Lean core's +`Functor` and `Monad` for types equipped with a `MeasurableSpace` instance. Assuming that instances +are lawful, this corresponds to functors and monads on the category of measurable spaces. ## Main definitions -* `MeasurableSpaceFunctor f`: **TODO** -* `MeasurableSpaceMonad m`: **TODO** -* `LawfulMeasurableSpaceFunctor f`: **TODO** -* `LawfulMeasurableSpaceMonad m`: **TODO** +* `MeasurableSpaceFunctor`: A typeclass for functors on types equipped with a `MeasurableSpace` +instance. +* `MeasurableSpaceMonad`: A typeclass for monads on types equipped with a `MeasurableSpace` +instance. +* `LawfulMeasurableSpaceFunctor`: A `Prop`-valued typeclass which states that a given +`MeasurableSpaceFunctor` satisfies the laws of a functor on measurable spaces. +* `LawfulMeasurableSpaceMonad`: A `Prop`-valued typeclass which states that a given +`MeasurableSpaceMonad` satisfies the laws of a monad on measurable spaces. * `MeasurableSpaceForIn`: **TODO** * `MeasurableSpaceForIn'`: **TODO** +## Notation + +The following notation is available: + +* `f <$>ₘ x`: `MeasurableSpaceFunctor.mMap f x`. +* `x >>=ₘ f`: `MeasurableSpaceBind.mBind x f`. + +## Implementation details + +The development of `MeasurableSpaceMonad` mirrors the development of `Monad` in Lean core, including +the definition of intermediate classes `MeasurableSpaceFunctor`, `MeasurableSpacePure`, and +`MeasurableSpaceBind` except that there is no `MeasurableSpaceApplicative` and instead +`MeasurableSpaceMonad` extends all three of the preceding classes directly. This is because +defining a `MeasurableSpaceApplicative` would require defining an analogue of +`Seq.seq : m (α → β) → (Unit → m α) → m β`, and we would like such an operation to be jointly +measurable in `m (α → β)` and `Unit → m α`, but requiring this operation to be jointly measurable +would already fail for the identity monad: there, `seq f (fun _ => x) = f x`, so `seq` reduces to +function evaluation. No σ-algebra on the space of all measurable functions makes evaluation +jointly measurable in general; +see R. J. Aumann, [*Borel structures for function spaces*](https://doi.org/10.1215/ijm/1255631584), +*Illinois Journal of Mathematics* **5** (1961), no. 4, 614–630, §3. + -/ @[expose] public section @@ -34,25 +63,36 @@ universe u v section MeasurableSpaceMonad -/-- A functor on types with a `MeasurableSpace` instance. The `mMap` operator `<$>ₘ` is overloaded -via instances of this class. This class does not require proofs of the `MeasurableSpaceFunctor` -axioms. Proofs may be provided or required via the `LawfulMeasurableSpaceFunctor` class. -/ +/-- +A functor on types with a `MeasurableSpace` instance. This means a function +`f : (α : Type u) → [MeasurableSpace α] → Type v` equipped with an +`mMap [MeasurableSpace α] [MeasurableSpace β] : (α → β) → f α → f β` operator, +which can be written with the notation `<$>ₘ`. + +A lawful instance of this class requires a `MeasurableSpace` instance on each output type `f α`, +and that `mMap` maps measurable functions `α → β` to measurable functions `f α → f β`, maps +identity functions to identity functions, and respects composition of measurable functions. +This class does not require its instances to be lawful. Proofs of lawful instances can be +provided via the `Prop`-valued class `LawfulMeasurableSpaceFunctor`. + +Lawful instances of this class correspond to functors on the category of measurable spaces. +-/ class MeasurableSpaceFunctor (f : (α : Type u) → [MeasurableSpace α] → Type v) : Type (max (u+1) v) where /-- Applies a function inside a functor on measurable spaces. This is used to overload the `<$>ₘ` operator. - When mapping a constant function (if one cares about executing the code), use - `Functor.mMapConst` instead, because it may be more efficient. + When mapping a constant function in executable code, use + `MeasurableSpaceFunctor.mMapConst` instead, because it may be more efficient. -/ mMap {α β : Type u} [MeasurableSpace α] [MeasurableSpace β] : (α → β) → f α → f β /-- Mapping a constant function. Given `a : α` and `v : f β`, `mMapConst a v` is equivalent to `(fun _ => a) <$>ₘ v`. For some - functors, this can be implemented more efficiently; for all other functors, the default - implementation may be used. + functors where executable code is relevant, this can be implemented more efficiently; for all + other functors, the default implementation may be used. -/ mMapConst {α β : Type u} [MeasurableSpace α] [MeasurableSpace β] : α → f β → f α := mMap ∘ (const _) @@ -66,7 +106,7 @@ The `mPure` function is overloaded via `MeasurableSpacePure` instances. -/ class MeasurableSpacePure (f : (α : Type u) → [MeasurableSpace α] → Type v) where /-- Given `a : α` where `α` has a `MeasurableSpace` instance, `mPure a : f α` represents an - action that does nothing and returns a -/ + action that does nothing and returns `a`. -/ mPure {α : Type u} [MeasurableSpace α] : α → f α /-- @@ -85,8 +125,21 @@ class MeasurableSpaceBind (m : (α : Type u) → [MeasurableSpace α] → Type v @[inherit_doc] infixl:55 " >>=ₘ " => MeasurableSpaceBind.mBind -/-- A monad on types with a `MeasurableSpace` instance. This abstraction allows the user to write -code that depends on "random" side-effects -/ +/-- +A monad on types with a `MeasurableSpace` instance. + +Monads are an abstraction of sequential control flow and side effects in functional programming, +and `MeasurableSpaceMonad`s allow the use of this abstraction on programs taking values in +`MeasurableSpace`s. The canonical example of such a monad is `Measure` where programs +"written" in the `Measure` monad can represent programs with "random" outputs whose output +distribution is given by the output measure. `MeasurableSpaceMonad`s support `rdo` notation, +the measurable-space analogue of `do` notation, for specifying these programs. + +A lawful instance of this class should satisfy various properties so that the instance corresponds +to a monad on the category of measurable spaces. These are specified precisely in the `Prop`-valued +class `LawfulMeasurableSpaceMonad` and proofs of lawfulness can be given by defining an instance +of that class. +-/ class MeasurableSpaceMonad (m : (α : Type u) → [MeasurableSpace α] → Type v) : Type (max (u+1) v) extends MeasurableSpaceFunctor m, MeasurableSpacePure m, MeasurableSpaceBind m where @@ -159,8 +212,7 @@ class LawfulMeasurableSpaceMonad mBind_mPure_comp {α β : Type u} [MeasurableSpace α] [MeasurableSpace β] {f : α → β} (hf : Measurable f) (x : m α) : x >>=ₘ (fun a => mPure (f a)) = f <$>ₘ x - /-- `mPure` followed by `mBind` of a function application is equivalent to function - application. -/ + /-- Binding `mPure x` to a measurable function `f` is equivalent to applying `f` to `x`. -/ mPure_mBind {α β : Type u} [MeasurableSpace α] [MeasurableSpace β] (x : α) {f : α → m β} (hf : Measurable f) : mPure x >>=ₘ f = f x