From 19d549e07205d335285b037d254860f87479de4b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Serr=C3=A9?= Date: Mon, 31 Aug 2026 16:21:57 +0200 Subject: [PATCH] CI passing --- RandomDo/Measurable.lean | 3 ++- RandomDo/Monad/ForInInstances.lean | 12 ++++++------ RandomDo/Monad/Instances.lean | 2 ++ RandomDo/Monad/MeasurableSpace.lean | 2 -- Test/Common.lean | 1 + lakefile.toml | 3 ++- 6 files changed, 13 insertions(+), 10 deletions(-) diff --git a/RandomDo/Measurable.lean b/RandomDo/Measurable.lean index 7887e6a..262db34 100644 --- a/RandomDo/Measurable.lean +++ b/RandomDo/Measurable.lean @@ -117,7 +117,8 @@ def Vector.measurableEquivTuple {n : ℕ} : Vector α n ≃ᵐ (Fin n → α) wh ext simp -instance : MeasurableSpace (Option α) := MeasurableSpace.map some inferInstance +instance instMeasurableSpaceOption : MeasurableSpace (Option α) := + MeasurableSpace.map some inferInstance theorem measurableSet_option_iff {s : Set (Option α)} : MeasurableSet s ↔ MeasurableSet (some ⁻¹' s) := Iff.rfl diff --git a/RandomDo/Monad/ForInInstances.lean b/RandomDo/Monad/ForInInstances.lean index 40bf67d..99d8103 100644 --- a/RandomDo/Monad/ForInInstances.lean +++ b/RandomDo/Monad/ForInInstances.lean @@ -20,13 +20,13 @@ section MeasurableSpace variable {α : Type*} [MeasurableSpace α] -instance : MeasurableSpace (List α) := +instance instMeasurableSpaceList : MeasurableSpace (List α) := MeasurableSpace.comap List.equivSigmaTuple inferInstance -instance : MeasurableSpace (Array α) := +instance instMeasurableSpaceArray : MeasurableSpace (Array α) := MeasurableSpace.comap Array.toList inferInstance -instance {n : ℕ} : MeasurableSpace (Vector α n) := +instance instMeasurableSpaceVector {n : ℕ} : MeasurableSpace (Vector α n) := MeasurableSpace.comap Vector.toArray inferInstance @[fun_prop] @@ -52,7 +52,7 @@ section Array {β : Type u} [mβ : MeasurableSpace β] (as : Array α) (b : β) (f : (a : α) → a ∈ as → β → m (ForInStep β)) : m β := let sz := as.usize - let rec @[specialize] loop (i : USize) (b : β) : m β := rdo + let rec @[specialize, nolint docBlame] loop (i : USize) (b : β) : m β := rdo if i < sz then let a := as.uget i lcProof match (← f a lcProof b) with @@ -67,7 +67,7 @@ section Array protected def Array.measurableSpaceForIn' [MeasurableSpaceMonad m] {β : Type u} [mβ : MeasurableSpace β] (as : Array α) (b : β) (f : (a : α) → a ∈ as → β → m (ForInStep β)) : m β := - let rec loop (i : Nat) (h : i ≤ as.size) (b : β) : m β := rdo + let rec @[nolint docBlame] loop (i : Nat) (h : i ≤ as.size) (b : β) : m β := rdo match i, h with | 0, _ => mPure b | i+1, h => @@ -97,7 +97,7 @@ variable {α β : Type*} [MeasurableSpace α] [MeasurableSpace β] [Ring α] protected def List.measurableSpaceForIn' [MeasurableSpaceMonad m] {β : Type u} [mβ : MeasurableSpace β] (as : @& List α) (init : β) (f : (a : α) → a ∈ as → β → m (ForInStep β)) : m β := - let rec @[specialize] + let rec @[specialize, nolint docBlame] loop : (as' : @& List α) → (b : β) → Exists (fun bs => bs ++ as' = as) → m β | [], b, _ => mPure b | a::as', b, h => rdo diff --git a/RandomDo/Monad/Instances.lean b/RandomDo/Monad/Instances.lean index 87afea9..fd064d9 100644 --- a/RandomDo/Monad/Instances.lean +++ b/RandomDo/Monad/Instances.lean @@ -57,6 +57,8 @@ open Function /-- A monad for random number generation. -/ structure RandomM (Ω : Type w) [MeasurableSpace Ω] (P : Measure Ω) (α : Type u) [MeasurableSpace α] where + /-- Draws a value from a state of the source of randomness, and hands back the state left for the + next draw. -/ sample : Ω → α × Ω measurePreserving : MeasurePreserving sample P ((Measure.map (Prod.fst ∘ sample) P).prod P) diff --git a/RandomDo/Monad/MeasurableSpace.lean b/RandomDo/Monad/MeasurableSpace.lean index 9b5fa7c..b593969 100644 --- a/RandomDo/Monad/MeasurableSpace.lean +++ b/RandomDo/Monad/MeasurableSpace.lean @@ -142,8 +142,6 @@ variable {f : (α : Type u) → [MeasurableSpace α] → Type v} [MeasurableSpac g₁ <$>ₘ g₀ <$>ₘ x = (fun a => g₁ (g₀ a)) <$>ₘ x := (comp_mMap x hg₀ hg₁).symm -@[simp] theorem mMap_unit {a : f PUnit} : (fun _ => PUnit.unit) <$>ₘ a = a := by simp - open MeasurableSpaceBind MeasurableSpacePure MeasurableSpaceFunctor /-- A `MeasurableSpaceMonad` satisfies the measurable space monad laws. -/ diff --git a/Test/Common.lean b/Test/Common.lean index d3b23f4..83934c5 100644 --- a/Test/Common.lean +++ b/Test/Common.lean @@ -1,6 +1,7 @@ module public import RandomDo +public import Mathlib.Probability.Distributions.Bernoulli set_option linter.style.header false diff --git a/lakefile.toml b/lakefile.toml index 0fdcde8..f51bc95 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -1,6 +1,7 @@ name = "RandomDo" -defaultTargets = ["RandomDo", "Test"] +defaultTargets = ["RandomDo"] lintDriver = "batteries/runLinter" +testDriver = "Test" [leanOptions] pp.unicode.fun = true