From 3b817db307e440abead97169f74a71cc7f571b2e Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sat, 29 Aug 2026 09:13:46 +0200 Subject: [PATCH 1/6] fix for loop over several collections --- RandomDo/Monad/Examples.lean | 122 +++++++++++++++++++++++++++++ RandomDo/Monad/ForInInstances.lean | 7 ++ RandomDo/Monad/Notation.lean | 2 +- 3 files changed, 130 insertions(+), 1 deletion(-) diff --git a/RandomDo/Monad/Examples.lean b/RandomDo/Monad/Examples.lean index 952cf91..1690fda 100644 --- a/RandomDo/Monad/Examples.lean +++ b/RandomDo/Monad/Examples.lean @@ -2,6 +2,7 @@ module public import RandomDo.Monad.ForInInstances public import RandomDo.Monad.Instances +public import RandomDo.Measurable public import Mathlib.Algebra.Ring.BooleanRing public import Mathlib.Probability.Distributions.Bernoulli @@ -56,4 +57,125 @@ def sampleBitsArray [HasBit m] (n : ℕ) : m (Array Bool) := rdo xs := xs.push b return xs +/- # `for` over several collections + +A `for` loop over several collections is expanded into a loop over the first one whose body reads +the remaining ones off a `Std.Stream` held in a mutable variable. That body has to stay part of the +surrounding `rdo` block: expanding it into a fresh `rdo` block instead puts the mutable variables +declared before the loop out of scope, and reassigning one of them is then rejected. + +The loops below are run in a deterministic monad so that the tests can pin the value the loop +computes, not merely that it elaborates. -/ + +section MultiCollectionFor + +/-- A deterministic `MeasurableSpaceMonad`, so that `rdo` programs reduce to a value. -/ +abbrev IdM := Monad.toMeasurableSpaceMonad Id + +/-- Read the value out of a deterministic `rdo` program. `IdM α` is definitionally `α`, but it is +not reducibly so, so the tests below go through this to state the value a loop computes. -/ +def IdM.run {α : Type u} [MeasurableSpace α] (x : IdM α) : α := x + +def zipDot (xs ys : List ℕ) : IdM ℕ := rdo + let mut s := 0 + for x in xs, y in ys rdo + s := s + x * y + return s + +example : IdM.run (zipDot [1, 2, 3] [10, 20, 30]) = 140 := rfl + +/-- Iteration stops with the shorter collection, whichever one that is. -/ +example : IdM.run (zipDot [1, 2, 3] [10, 20]) = 50 := rfl + +example : IdM.run (zipDot [1, 2] [10, 20, 30]) = 50 := rfl + +example : IdM.run (zipDot [] [10, 20]) = 0 := rfl + +def zipTriple (xs ys zs : List ℕ) : IdM ℕ := rdo + let mut s := 0 + for x in xs, y in ys, z in zs rdo + s := s + x * y * z + return s + +example : IdM.run (zipTriple [1, 2] [3, 4] [5, 6]) = 63 := rfl + +/-- `break` in the body of a loop over several collections. -/ +def zipUntilZero (xs ys : List ℕ) : IdM ℕ := rdo + let mut s := 0 + for x in xs, y in ys rdo + if x = 0 then + break + s := s + y + return s + +example : IdM.run (zipUntilZero [1, 0, 1] [10, 20, 30]) = 10 := rfl + +/-- `continue` in the body of a loop over several collections. -/ +def zipSkipZero (xs ys : List ℕ) : IdM ℕ := rdo + let mut s := 0 + for x in xs, y in ys rdo + if x = 0 then + continue + s := s + y + return s + +example : IdM.run (zipSkipZero [1, 0, 1] [10, 20, 30]) = 40 := rfl + +/-- Early `return` out of a loop over several collections. -/ +def firstAgreement (xs ys : List ℕ) : IdM (Option ℕ) := rdo + for x in xs, y in ys rdo + if x = y then + return some x + return none + +example : IdM.run (firstAgreement [1, 2, 3] [3, 2, 1]) = some 2 := rfl + +example : IdM.run (firstAgreement [1, 2] [3, 4]) = none := rfl + +/-- The collections a loop ranges over need not have the same type, nor need an `Array` be the +leading one: the collections past the first are iterated through `Std.toStream`, and an `Array` +streams as a `Subarray`, which is measurable. + +The two definitions here are checked by elaborating: without `MeasurableSpace (Subarray _)` they +are rejected. Their value is not pinned the way the loops above are, because `Std.Slice`, which +`Subarray` is built from, does not reduce inside a `module` file. -/ +def zipMixed (xs : List ℕ) (ys : Array Bool) : IdM ℕ := rdo + let mut s := 0 + for x in xs, y in ys rdo + s := s + (if y then x else 0) + return s + +def zipArrays (xs ys : Array ℕ) : IdM ℕ := rdo + let mut s := 0 + for x in xs, y in ys rdo + s := s + x * y + return s + +/-- A `Vector` leading a loop over several collections, where it is consumed by +`MeasurableSpaceForIn'`. -/ +def zipVectorFirst (xs : Vector ℕ 3) (ys : List ℕ) : IdM ℕ := rdo + let mut s := 0 + for x in xs, y in ys rdo + s := s + x * y + return s + +example : IdM.run (zipVectorFirst #v[1, 2, 3] [10, 20, 30]) = 140 := rfl + +/-- A `Vector` following one, where it streams as a `Subarray` just as an `Array` does. -/ +def zipVectorSecond (xs : List ℕ) (ys : Vector ℕ 3) : IdM ℕ := rdo + let mut s := 0 + for x in xs, y in ys rdo + s := s + x * y + return s + +/-- The same loop shape, in a genuinely probabilistic monad. -/ +noncomputable def zipBernoulli (xs ys : List Bool) : Measure Bool := rdo + let mut acc := false + for x in xs, y in ys rdo + let b ← bernoulliMeasure true false ⟨(1 : ℝ) / 2, by norm_num⟩ + acc := acc || (b && x && y) + return acc + +end MultiCollectionFor + end diff --git a/RandomDo/Monad/ForInInstances.lean b/RandomDo/Monad/ForInInstances.lean index 40bf67d..929a76d 100644 --- a/RandomDo/Monad/ForInInstances.lean +++ b/RandomDo/Monad/ForInInstances.lean @@ -29,10 +29,17 @@ instance : MeasurableSpace (Array α) := instance {n : ℕ} : MeasurableSpace (Vector α n) := MeasurableSpace.comap Vector.toArray inferInstance +instance : MeasurableSpace (Subarray α) := + MeasurableSpace.comap (fun s : Subarray α ↦ s.toList) inferInstance + @[fun_prop] lemma measurable_toList : Measurable (Array.toList : Array α → List α) := Measurable.of_comap_le fun _ a ↦ a +@[fun_prop] +lemma measurable_subarray_toList : Measurable (fun s : Subarray α ↦ s.toList) := + Measurable.of_comap_le fun _ a ↦ a + @[fun_prop] lemma measurable_toArray {n : ℕ} : Measurable (Vector.toArray : Vector α n → Array α) := Measurable.of_comap_le fun _ a ↦ a diff --git a/RandomDo/Monad/Notation.lean b/RandomDo/Monad/Notation.lean index 1943765..21cec4d 100644 --- a/RandomDo/Monad/Notation.lean +++ b/RandomDo/Monad/Notation.lean @@ -138,7 +138,7 @@ def rdoForDecl := leading_parser | none => break | some ($y, s') => $s:ident := s' - rdo $body) + do $body) doElems := doElems.push (← `(doSeqItem| for%$tk $[$h? : ]? $x:ident in $xs rdo $body)) `(doElem| do $doElems*) | _ => Macro.throwUnsupported From 525832097d76484620ffb6a61b3f545de6ed6a31 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sat, 29 Aug 2026 09:17:37 +0200 Subject: [PATCH 2/6] minor --- RandomDo/Monad/Examples.lean | 10 +--------- 1 file changed, 1 insertion(+), 9 deletions(-) diff --git a/RandomDo/Monad/Examples.lean b/RandomDo/Monad/Examples.lean index 1690fda..fb09d5e 100644 --- a/RandomDo/Monad/Examples.lean +++ b/RandomDo/Monad/Examples.lean @@ -57,15 +57,7 @@ def sampleBitsArray [HasBit m] (n : ℕ) : m (Array Bool) := rdo xs := xs.push b return xs -/- # `for` over several collections - -A `for` loop over several collections is expanded into a loop over the first one whose body reads -the remaining ones off a `Std.Stream` held in a mutable variable. That body has to stay part of the -surrounding `rdo` block: expanding it into a fresh `rdo` block instead puts the mutable variables -declared before the loop out of scope, and reassigning one of them is then rejected. - -The loops below are run in a deterministic monad so that the tests can pin the value the loop -computes, not merely that it elaborates. -/ +/- # `for` over several collections -/ section MultiCollectionFor From 3690c4883baded5bff11aeefba2b21a024d9f0a3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Serr=C3=A9?= Date: Mon, 31 Aug 2026 16:06:02 +0200 Subject: [PATCH 3/6] Remove examples --- RandomDo/Monad/Examples.lean | 173 ----------------------------------- 1 file changed, 173 deletions(-) delete mode 100644 RandomDo/Monad/Examples.lean diff --git a/RandomDo/Monad/Examples.lean b/RandomDo/Monad/Examples.lean deleted file mode 100644 index fb09d5e..0000000 --- a/RandomDo/Monad/Examples.lean +++ /dev/null @@ -1,173 +0,0 @@ -module - -public import RandomDo.Monad.ForInInstances -public import RandomDo.Monad.Instances -public import RandomDo.Measurable -public import Mathlib.Algebra.Ring.BooleanRing -public import Mathlib.Probability.Distributions.Bernoulli - -set_option linter.style.header false - -@[expose] public section - -open MeasureTheory ProbabilityTheory Measure - -/- # Nonpolymorphic examples -/ - -universe u v - -noncomputable def measureSample : Measure Bool := rdo - let x ← bernoulliMeasure true false ⟨(1 : ℝ) / 2, by norm_num⟩ - let y ← bernoulliMeasure true false ⟨(1 : ℝ) / 2, by norm_num⟩ - return x + y - -def pseudoSample : Rand Bool := do - let x ← Random.randBool - let y ← Random.randBool - return x + y - -/- # Polymorphic examples -/ - -variable {m : (α : Type) → [MeasurableSpace α] → Type v} [MeasurableSpaceMonad m] - -class HasBit (m : (α : Type) → MeasurableSpace α → Type v) where - bit : m Bool (by infer_instance) - -noncomputable instance : HasBit Measure where - bit := bernoulliMeasure true false ⟨(1 : ℝ) / 2, by norm_num⟩ - -instance : HasBit PseudoRandomM where - bit := Random.randBool - -def indepAnd [HasBit m] : m Bool := rdo - let x ← HasBit.bit - let y ← HasBit.bit - return x && y - -noncomputable def indepAndMeasure : Measure Bool := indepAnd (m := Measure) - -def indepAndGen : PseudoRandomM Bool := indepAnd (m := PseudoRandomM) - -variable {α : Type*} [MeasurableSpace α] - -def sampleBitsArray [HasBit m] (n : ℕ) : m (Array Bool) := rdo - let mut xs : Array Bool := #[] - for _ in List.range n rdo - let b ← HasBit.bit (m := m) - xs := xs.push b - return xs - -/- # `for` over several collections -/ - -section MultiCollectionFor - -/-- A deterministic `MeasurableSpaceMonad`, so that `rdo` programs reduce to a value. -/ -abbrev IdM := Monad.toMeasurableSpaceMonad Id - -/-- Read the value out of a deterministic `rdo` program. `IdM α` is definitionally `α`, but it is -not reducibly so, so the tests below go through this to state the value a loop computes. -/ -def IdM.run {α : Type u} [MeasurableSpace α] (x : IdM α) : α := x - -def zipDot (xs ys : List ℕ) : IdM ℕ := rdo - let mut s := 0 - for x in xs, y in ys rdo - s := s + x * y - return s - -example : IdM.run (zipDot [1, 2, 3] [10, 20, 30]) = 140 := rfl - -/-- Iteration stops with the shorter collection, whichever one that is. -/ -example : IdM.run (zipDot [1, 2, 3] [10, 20]) = 50 := rfl - -example : IdM.run (zipDot [1, 2] [10, 20, 30]) = 50 := rfl - -example : IdM.run (zipDot [] [10, 20]) = 0 := rfl - -def zipTriple (xs ys zs : List ℕ) : IdM ℕ := rdo - let mut s := 0 - for x in xs, y in ys, z in zs rdo - s := s + x * y * z - return s - -example : IdM.run (zipTriple [1, 2] [3, 4] [5, 6]) = 63 := rfl - -/-- `break` in the body of a loop over several collections. -/ -def zipUntilZero (xs ys : List ℕ) : IdM ℕ := rdo - let mut s := 0 - for x in xs, y in ys rdo - if x = 0 then - break - s := s + y - return s - -example : IdM.run (zipUntilZero [1, 0, 1] [10, 20, 30]) = 10 := rfl - -/-- `continue` in the body of a loop over several collections. -/ -def zipSkipZero (xs ys : List ℕ) : IdM ℕ := rdo - let mut s := 0 - for x in xs, y in ys rdo - if x = 0 then - continue - s := s + y - return s - -example : IdM.run (zipSkipZero [1, 0, 1] [10, 20, 30]) = 40 := rfl - -/-- Early `return` out of a loop over several collections. -/ -def firstAgreement (xs ys : List ℕ) : IdM (Option ℕ) := rdo - for x in xs, y in ys rdo - if x = y then - return some x - return none - -example : IdM.run (firstAgreement [1, 2, 3] [3, 2, 1]) = some 2 := rfl - -example : IdM.run (firstAgreement [1, 2] [3, 4]) = none := rfl - -/-- The collections a loop ranges over need not have the same type, nor need an `Array` be the -leading one: the collections past the first are iterated through `Std.toStream`, and an `Array` -streams as a `Subarray`, which is measurable. - -The two definitions here are checked by elaborating: without `MeasurableSpace (Subarray _)` they -are rejected. Their value is not pinned the way the loops above are, because `Std.Slice`, which -`Subarray` is built from, does not reduce inside a `module` file. -/ -def zipMixed (xs : List ℕ) (ys : Array Bool) : IdM ℕ := rdo - let mut s := 0 - for x in xs, y in ys rdo - s := s + (if y then x else 0) - return s - -def zipArrays (xs ys : Array ℕ) : IdM ℕ := rdo - let mut s := 0 - for x in xs, y in ys rdo - s := s + x * y - return s - -/-- A `Vector` leading a loop over several collections, where it is consumed by -`MeasurableSpaceForIn'`. -/ -def zipVectorFirst (xs : Vector ℕ 3) (ys : List ℕ) : IdM ℕ := rdo - let mut s := 0 - for x in xs, y in ys rdo - s := s + x * y - return s - -example : IdM.run (zipVectorFirst #v[1, 2, 3] [10, 20, 30]) = 140 := rfl - -/-- A `Vector` following one, where it streams as a `Subarray` just as an `Array` does. -/ -def zipVectorSecond (xs : List ℕ) (ys : Vector ℕ 3) : IdM ℕ := rdo - let mut s := 0 - for x in xs, y in ys rdo - s := s + x * y - return s - -/-- The same loop shape, in a genuinely probabilistic monad. -/ -noncomputable def zipBernoulli (xs ys : List Bool) : Measure Bool := rdo - let mut acc := false - for x in xs, y in ys rdo - let b ← bernoulliMeasure true false ⟨(1 : ℝ) / 2, by norm_num⟩ - acc := acc || (b && x && y) - return acc - -end MultiCollectionFor - -end From c8a36c58da2b042a5749604afb7b04f32dca971e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Serr=C3=A9?= Date: Mon, 31 Aug 2026 16:06:07 +0200 Subject: [PATCH 4/6] Fix instance name --- RandomDo/Monad/ForInInstances.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/RandomDo/Monad/ForInInstances.lean b/RandomDo/Monad/ForInInstances.lean index 929a76d..728f2b2 100644 --- a/RandomDo/Monad/ForInInstances.lean +++ b/RandomDo/Monad/ForInInstances.lean @@ -29,7 +29,7 @@ instance : MeasurableSpace (Array α) := instance {n : ℕ} : MeasurableSpace (Vector α n) := MeasurableSpace.comap Vector.toArray inferInstance -instance : MeasurableSpace (Subarray α) := +instance instMeasurableSpaceSubarray : MeasurableSpace (Subarray α) := MeasurableSpace.comap (fun s : Subarray α ↦ s.toList) inferInstance @[fun_prop] From 5cd0bc2e9c5a183a8599c99ac550d24f493d1a76 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Serr=C3=A9?= Date: Mon, 31 Aug 2026 16:09:45 +0200 Subject: [PATCH 5/6] Update RandomDo.lean --- RandomDo.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/RandomDo.lean b/RandomDo.lean index eb84dc7..3460f37 100644 --- a/RandomDo.lean +++ b/RandomDo.lean @@ -2,7 +2,6 @@ module -- shake: keep-all --deprecated_module: ignore public import RandomDo.ForMathlib.MeasureTheory.MeasurableSpace.Embedding public import RandomDo.Measurable -public import RandomDo.Monad.Examples public import RandomDo.Monad.ForInInstances public import RandomDo.Monad.Instances public import RandomDo.Monad.MeasurableSpace From f2a4e1e33768ae3c870619b5d4bf97db2b5955e0 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Serr=C3=A9?= Date: Mon, 31 Aug 2026 16:36:00 +0200 Subject: [PATCH 6/6] Remove gaps that now work --- Test/Gaps.lean | 41 ----------------------------------------- 1 file changed, 41 deletions(-) diff --git a/Test/Gaps.lean b/Test/Gaps.lean index 09b1b72..39aeb1c 100644 --- a/Test/Gaps.lean +++ b/Test/Gaps.lean @@ -18,47 +18,6 @@ open MeasureTheory ProbabilityTheory namespace Test.Gaps -/-! ## `for` over several collections - -TODO: the expander at `RandomDo/Monad/Notation.lean:141` wraps the loop body in a fresh term-level -`rdo` block, which severs it from the block around it. Emitting `do $body` instead — a nested -`doElem`, which is what core's otherwise identical expander does — fixes all three tests below. --/ - -/-- -error: Variable `s` cannot be mutated. Only variables declared using `let mut` can be mutated. - If you did not intend to mutate but define `s`, consider using `let s` instead --/ -#guard_msgs in -def zipMut (xs ys : List ℕ) : IdM ℕ := rdo - let mut s := 0 - for x in xs, y in ys rdo - s := s + x * y - return s - -/-- -error: Type mismatch - some x -has type - Option ℕ -but is expected to have type - Unit --/ -#guard_msgs in -def zipReturn (xs ys : List ℕ) : IdM (Option ℕ) := rdo - for x in xs, y in ys rdo - if x = y then - return some x - return none - -/-- error: `break` must be nested inside a loop -/ -#guard_msgs in -def zipThree (xs ys zs : List ℕ) : IdM Bool := rdo - for x in xs, y in ys, z in zs rdo - if x + y = z then - return true - return false - /-! ## Nested loops TODO: register a `ControlInfo` inference handler for `RDo.rdoFor`, mirroring the rule core states