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/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..940bce5 --- /dev/null +++ b/RandomDo/MeasurableSpaceMonad/Core.lean @@ -0,0 +1,268 @@ +/- +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.Constructions +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 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`: 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 + +The following notation is available in the `MeasureTheory` scope: + +* `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 + +namespace MeasureTheory + +open Function + +universe u v + +section MeasurableSpaceMonad + +/-- +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 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 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 _) + +@[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 + +/-- +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 + 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 + /-- 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 + /-- `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 MeasureTheory diff --git a/RandomDo/MeasurableSpaceMonad/Notation.lean b/RandomDo/MeasurableSpaceMonad/Notation.lean new file mode 100644 index 0000000..a5723fd --- /dev/null +++ b/RandomDo/MeasurableSpaceMonad/Notation.lean @@ -0,0 +1,91 @@ +/- +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 RandomDo.MeasurableSpaceMonad.Core +public import Mathlib.MeasureTheory.MeasurableSpace.Prod +public meta import Lean.Elab.BuiltinDo + +/-! +# `rdo` 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. + +## Main definitions + +* `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 `MeasurableSpacePure.mPure` and + `MeasurableSpaceBind.mBind`. + +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 MeasureTheory MeasurableSpacePure MeasurableSpaceBind + +public meta section + +namespace MeasureTheory + +/-- The `do` notation for writing monadic programs depending on a `MeasurableSpace` instance. -/ +scoped syntax (name := randKind) "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? + +end RDo + +end MeasureTheory 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 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.lean b/TestNext.lean new file mode 100644 index 0000000..96afc04 --- /dev/null +++ b/TestNext.lean @@ -0,0 +1,5 @@ +module -- shake: keep-all --deprecated_module: ignore + +public import TestNext.MeasurableSpaceMonad.Core +public import TestNext.MeasurableSpaceMonad.ImportBoundary +public import TestNext.MeasurableSpaceMonad.Notation diff --git a/TestNext/MeasurableSpaceMonad/Core.lean b/TestNext/MeasurableSpaceMonad/Core.lean new file mode 100644 index 0000000..fe24a5e --- /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 RandomDo.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 MeasureTheory 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..8dc21b7 --- /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 RandomDo.MeasurableSpaceMonad.Notation + +/-! +# Isolation of the polymorphic foundation + +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. +-/ + +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..8c6223a --- /dev/null +++ b/TestNext/MeasurableSpaceMonad/Notation.lean @@ -0,0 +1,52 @@ +/- +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 RandomDo.MeasurableSpaceMonad.Notation + +/-! +# Elaboration without a concrete interpretation + +The programs below use only abstract monad operations. They check return, binding, branching, +and mutable state through the notation import. +-/ + +open MeasureTheory 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 + +/-- 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..ea66cf7 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -21,6 +21,9 @@ precompileModules = true [[lean_lib]] name = "RandomDo" +[[lean_lib]] +name = "TestNext" + [[lean_lib]] name = "Test"