wip: move consumer lemmas to Init

src/Init/Data.lean

@@ -46,3 +46,4 @@ import Init.Data.NeZero
 import Init.Data.Function
 import Init.Data.RArray
 import Init.Data.Vector
+import Init.Data.Iterators

src/Init/Data/Array/Lex/Basic.lean

@@ -8,7 +8,7 @@ module
 prelude
 import Init.Data.Array.Basic
 import Init.Data.Nat.Lemmas
-import Init.Data.Range
+import Init.Data.Range.New.Nat
 
 set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
 set_option linter.indexVariables true -- Enforce naming conventions for index variables.
@@ -24,9 +24,9 @@ Specifically, `Array.lex as bs lt` is true if
 * there is an index `i` such that `lt as[i] bs[i]`, and for all `j < i`, `as[j] == bs[j]`.
 -/
 def lex [BEq α] (as bs : Array α) (lt : α → α → Bool := by exact (· < ·)) : Bool := Id.run do
-  for h : i in [0 : min as.size bs.size] do
+  for h : i in 0,,<(min as.size bs.size) do
     -- TODO: `omega` should be able to find this itself.
-    have : i < min as.size bs.size := Membership.get_elem_helper h rfl
+    have : i < min as.size bs.size := Range.get_elem_helper h rfl
     if lt as[i] bs[i] then
       return true
     else if as[i] != bs[i] then

src/Init/Data/Iterators.lean

@@ -3,7 +3,10 @@ Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Paul Reichert
 -/
+module
+
 prelude
-import Std.Data.Iterators.Consumers.Monadic.Collect
-import Std.Data.Iterators.Consumers.Monadic.Loop
-import Std.Data.Iterators.Consumers.Monadic.Partial
+import Init.Data.Iterators.Basic
+import Init.Data.Iterators.PostconditionMonad
+import Init.Data.Iterators.Consumers
+import Init.Data.Iterators.Lemmas

src/Init/Data/Iterators/Basic.lean

@@ -3,6 +3,8 @@ Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Paul Reichert
 -/
+module
+
 prelude
 import Init.Core
 import Init.Classical
@@ -31,7 +33,7 @@ See `Std.Data.Iterators.Producers` for ways to iterate over common data structur
 By convention, the monadic iterator associated with an object can be obtained via dot notation.
 For example, `List.iterM IO` creates an iterator over a list in the monad `IO`.
 
-See `Std.Data.Iterators.Consumers` for ways to use an iterator. For example, `it.toList` will
+See `Init.Data.Iterators.Consumers` for ways to use an iterator. For example, `it.toList` will
 convert a provably finite iterator `it` into a list and `it.allowNontermination.toList` will
 do so even if finiteness cannot be proved. It is also always possible to manually iterate using
 `it.step`, relying on the termination measures `it.finitelyManySteps` and `it.finitelyManySkips`.
@@ -75,7 +77,7 @@ See `Std.Data.Iterators.Producers` for ways to iterate over common data structur
 By convention, the monadic iterator associated with an object can be obtained via dot notation.
 For example, `List.iterM IO` creates an iterator over a list in the monad `IO`.
 
-See `Std.Data.Iterators.Consumers` for ways to use an iterator. For example, `it.toList` will
+See `Init.Data.Iterators.Consumers` for ways to use an iterator. For example, `it.toList` will
 convert a provably finite iterator `it` into a list and `it.allowNontermination.toList` will
 do so even if finiteness cannot be proved. It is also always possible to manually iterate using
 `it.step`, relying on the termination measures `it.finitelyManySteps` and `it.finitelyManySkips`.
@@ -111,12 +113,14 @@ structure Iter {α : Type w} (β : Type w) where
 Converts a pure iterator (`Iter β`) into a monadic iterator (`IterM Id β`) in the
 identity monad `Id`.
 -/
+@[expose]
 def Iter.toIterM {α : Type w} {β : Type w} (it : Iter (α := α) β) : IterM (α := α) Id β :=
   ⟨it.internalState⟩
 
 /--
 Converts a monadic iterator (`IterM Id β`) over `Id` into a pure iterator (`Iter β`).
 -/
+@[expose]
 def IterM.toIter {α : Type w} {β : Type w} (it : IterM (α := α) Id β) : Iter (α := α) β :=
   ⟨it.internalState⟩
 
@@ -170,6 +174,7 @@ inductive IterStep (α β) where
 Returns the succeeding iterator stored in an iterator step or `none` if the step is `.done`
 and the iterator has finished.
 -/
+@[expose]
 def IterStep.successor : IterStep α β → Option α
   | .yield it _ => some it
   | .skip it => some it
@@ -179,7 +184,7 @@ def IterStep.successor : IterStep α β → Option α
 If present, applies `f` to the iterator of an `IterStep` and replaces the iterator
 with the result of the application of `f`.
 -/
-@[always_inline, inline]
+@[always_inline, inline, expose]
 def IterStep.mapIterator {α' : Type u'} (f : α → α') : IterStep α β → IterStep α' β
   | .yield it out => .yield (f it) out
   | .skip it => .skip (f it)
@@ -217,6 +222,36 @@ theorem IterStep.mapIterator_id {step : IterStep α β} :
     step.mapIterator id = step := by
   cases step <;> rfl
 
+/--
+A variant of `mapIterator` where the mapping function takes a proof that the
+given iterator has been obtained with `IterStep.successor`.
+
+If present, applies `f` to the iterator of an `IterStep` and replaces the iterator
+with the result of the application of `f`.
+-/
+@[always_inline, inline, expose]
+def IterStep.pmapIterator {α' : Type u'} (step : IterStep α β)
+    (f : (it : α) → step.successor = some it → α') : IterStep α' β :=
+  match step with
+  | .yield it out => .yield (f it rfl) out
+  | .skip it => .skip (f it rfl)
+  | .done => .done
+
+@[simp]
+theorem IterStep.pmapIterator_yield {α' : Type u'} {it : α} {out : β} {f : (it : α) → _ → α'} :
+    (IterStep.yield it out).pmapIterator f = IterStep.yield (f it rfl) out :=
+  rfl
+
+@[simp]
+theorem IterStep.pmapIterator_skip {α' : Type u'} {it : α} {f : (it : α) → _ → α'} :
+    (IterStep.skip it (β := β)).pmapIterator f = IterStep.skip (f it rfl) :=
+  rfl
+
+@[simp]
+theorem IterStep.pmapIterator_done {α' : Type u'} {f : (it : α) → _ → α'} :
+    (IterStep.done (α := α) (β := β)).pmapIterator f = IterStep.done :=
+  rfl
+
 /--
 A variant of `IterStep` that bundles the step together with a proof that it is "plausible".
 The plausibility predicate will later be chosen to assert that a state is a plausible successor
@@ -224,12 +259,13 @@ of another state. Having this proof bundled up with the step is important for te
 
 See `IterM.Step` and `Iter.Step` for the concrete choice of the plausibility predicate.
 -/
+@[expose]
 def PlausibleIterStep (IsPlausibleStep : IterStep α β → Prop) := Subtype IsPlausibleStep
 
 /--
 Match pattern for the `yield` case. See also `IterStep.yield`.
 -/
-@[match_pattern, simp]
+@[match_pattern, simp, expose]
 def PlausibleIterStep.yield {IsPlausibleStep : IterStep α β → Prop}
     (it' : α) (out : β) (h : IsPlausibleStep (.yield it' out)) :
     PlausibleIterStep IsPlausibleStep :=
@@ -238,7 +274,7 @@ def PlausibleIterStep.yield {IsPlausibleStep : IterStep α β → Prop}
 /--
 Match pattern for the `skip` case. See also `IterStep.skip`.
 -/
-@[match_pattern, simp]
+@[match_pattern, simp, expose]
 def PlausibleIterStep.skip {IsPlausibleStep : IterStep α β → Prop}
     (it' : α) (h : IsPlausibleStep (.skip it')) : PlausibleIterStep IsPlausibleStep :=
   ⟨.skip it', h⟩
@@ -246,7 +282,7 @@ def PlausibleIterStep.skip {IsPlausibleStep : IterStep α β → Prop}
 /--
 Match pattern for the `done` case. See also `IterStep.done`.
 -/
-@[match_pattern, simp]
+@[match_pattern, simp, expose]
 def PlausibleIterStep.done {IsPlausibleStep : IterStep α β → Prop}
     (h : IsPlausibleStep .done) : PlausibleIterStep IsPlausibleStep :=
   ⟨.done, h⟩
@@ -283,7 +319,7 @@ section Monadic
 /--
 Converts wraps the state of an iterator into an `IterM` object.
 -/
-@[always_inline, inline]
+@[always_inline, inline, expose]
 def toIterM {α : Type w} (it : α) (m : Type w → Type w') (β : Type w) :
     IterM (α := α) m β :=
   ⟨it⟩
@@ -302,6 +338,7 @@ theorem internalState_toIterM {α m β} (it : α) :
 Asserts that certain step is plausibly the successor of a given iterator. What "plausible" means
 is up to the `Iterator` instance but it should be strong enough to allow termination proofs.
 -/
+@[expose]
 abbrev IterM.IsPlausibleStep {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β] :
     IterM (α := α) m β → IterStep (IterM (α := α) m β) β → Prop :=
   Iterator.IsPlausibleStep (α := α) (m := m)
@@ -310,6 +347,7 @@ abbrev IterM.IsPlausibleStep {α : Type w} {m : Type w → Type w'} {β : Type w
 The type of the step object returned by `IterM.step`, containing an `IterStep`
 and a proof that this is a plausible step for the given iterator.
 -/
+@[expose]
 abbrev IterM.Step {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β]
     (it : IterM (α := α) m β) :=
   PlausibleIterStep it.IsPlausibleStep
@@ -318,6 +356,7 @@ abbrev IterM.Step {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator
 Asserts that a certain output value could plausibly be emitted by the given iterator in its next
 step.
 -/
+@[expose]
 def IterM.IsPlausibleOutput {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β]
     (it : IterM (α := α) m β) (out : β) : Prop :=
   ∃ it', it.IsPlausibleStep (.yield it' out)
@@ -326,14 +365,55 @@ def IterM.IsPlausibleOutput {α : Type w} {m : Type w → Type w'} {β : Type w}
 Asserts that a certain iterator `it'` could plausibly be the directly succeeding iterator of another
 given iterator `it`.
 -/
+@[expose]
 def IterM.IsPlausibleSuccessorOf {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β]
     (it' it : IterM (α := α) m β) : Prop :=
   ∃ step, step.successor = some it' ∧ it.IsPlausibleStep step
 
+inductive IterM.IsPlausibleIndirectOutput {α β : Type w} {m : Type w → Type w'} [Iterator α m β]
+    : IterM (α := α) m β → β → Prop where
+  | direct {it : IterM (α := α) m β} {out : β} : it.IsPlausibleOutput out →
+      it.IsPlausibleIndirectOutput out
+  | indirect {it it' : IterM (α := α) m β} {out : β} : it'.IsPlausibleSuccessorOf it →
+      it'.IsPlausibleIndirectOutput out → it.IsPlausibleIndirectOutput out
+
+-- TODO: remove if unused
+def IterM.IsInLineageOf {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β]
+    (it' it : IterM (α := α) m β) : Prop :=
+  it' = it ∨ Relation.TransGen IterM.IsPlausibleSuccessorOf it' it
+
+protected theorem IterM.IsInLineageOf.rfl {α : Type w} {m : Type w → Type w'} {β : Type w}
+    [Iterator α m β] {it : IterM (α := α) m β} :
+    it.IsInLineageOf it :=
+  .inl rfl
+
+protected theorem IterM.IsInLineageOf.single {α : Type w} {m : Type w → Type w'} {β : Type w}
+    [Iterator α m β] {it' it : IterM (α := α) m β}
+    (h : it'.IsPlausibleSuccessorOf it) :
+    it'.IsInLineageOf it :=
+  .inr <| .single h
+
+protected theorem IterM.IsInLineageOf.trans {α : Type w} {m : Type w → Type w'} {β : Type w}
+    [Iterator α m β] {it'' it' it : IterM (α := α) m β}
+    (h' : it''.IsInLineageOf it') (h : it'.IsInLineageOf it) :
+    it''.IsInLineageOf it := by
+  cases h
+  · rename_i h
+    cases h
+    exact h'
+  · rename_i h
+    cases h'
+    · rename_i h'
+      cases h'
+      exact .inr h
+    · rename_i h'
+      exact .inr <| .trans h' h
+
 /--
 Asserts that a certain iterator `it'` could plausibly be the directly succeeding iterator of another
 given iterator `it` while no value is emitted (see `IterStep.skip`).
 -/
+@[expose]
 def IterM.IsPlausibleSkipSuccessorOf {α : Type w} {m : Type w → Type w'} {β : Type w}
     [Iterator α m β] (it' it : IterM (α := α) m β) : Prop :=
   it.IsPlausibleStep (.skip it')
@@ -356,6 +436,7 @@ section Pure
 Asserts that certain step is plausibly the successor of a given iterator. What "plausible" means
 is up to the `Iterator` instance but it should be strong enough to allow termination proofs.
 -/
+@[expose]
 def Iter.IsPlausibleStep {α : Type w} {β : Type w} [Iterator α Id β]
     (it : Iter (α := α) β) (step : IterStep (Iter (α := α) β) β) : Prop :=
   it.toIterM.IsPlausibleStep (step.mapIterator Iter.toIterM)
@@ -364,6 +445,7 @@ def Iter.IsPlausibleStep {α : Type w} {β : Type w} [Iterator α Id β]
 The type of the step object returned by `Iter.step`, containing an `IterStep`
 and a proof that this is a plausible step for the given iterator.
 -/
+@[expose]
 def Iter.Step {α : Type w} {β : Type w} [Iterator α Id β] (it : Iter (α := α) β) :=
   PlausibleIterStep (Iter.IsPlausibleStep it)
 
@@ -378,7 +460,7 @@ def Iter.Step.toMonadic {α : Type w} {β : Type w} [Iterator α Id β] {it : It
 /--
 Converts an `IterM.Step` into an `Iter.Step`.
 -/
-@[always_inline, inline]
+@[always_inline, inline, expose]
 def IterM.Step.toPure {α : Type w} {β : Type w} [Iterator α Id β] {it : IterM (α := α) Id β}
     (step : it.Step) : it.toIter.Step :=
   ⟨step.val.mapIterator IterM.toIter, (by simp [Iter.IsPlausibleStep, step.property])⟩
@@ -402,6 +484,7 @@ theorem IterM.Step.toPure_done {α β : Type w} [Iterator α Id β] {it : IterM
 Asserts that a certain output value could plausibly be emitted by the given iterator in its next
 step.
 -/
+@[expose]
 def Iter.IsPlausibleOutput {α : Type w} {β : Type w} [Iterator α Id β]
     (it : Iter (α := α) β) (out : β) : Prop :=
   it.toIterM.IsPlausibleOutput out
@@ -410,10 +493,39 @@ def Iter.IsPlausibleOutput {α : Type w} {β : Type w} [Iterator α Id β]
 Asserts that a certain iterator `it'` could plausibly be the directly succeeding iterator of another
 given iterator `it`.
 -/
+@[expose]
 def Iter.IsPlausibleSuccessorOf {α : Type w} {β : Type w} [Iterator α Id β]
     (it' it : Iter (α := α) β) : Prop :=
   it'.toIterM.IsPlausibleSuccessorOf it.toIterM
 
+inductive Iter.IsPlausibleIndirectOutput {α β : Type w} [Iterator α Id β] :
+    Iter (α := α) β → β → Prop where
+  | direct {it : Iter (α := α) β} {out : β} : it.IsPlausibleOutput out →
+      it.IsPlausibleIndirectOutput out
+  | indirect {it it' : Iter (α := α) β} {out : β} : it'.IsPlausibleSuccessorOf it →
+      it'.IsPlausibleIndirectOutput out → it.IsPlausibleIndirectOutput out
+
+theorem Iter.isPlausibleIndirectOutput_iff_isPlausibleIndirectOutput_toIterM {α β : Type w}
+    [Iterator α Id β] {it : Iter (α := α) β} {out : β} :
+    it.IsPlausibleIndirectOutput out ↔ it.toIterM.IsPlausibleIndirectOutput out := by
+  constructor
+  · intro h
+    induction h with
+    | direct h =>
+      exact .direct h
+    | indirect h _ ih =>
+      exact .indirect h ih
+  · intro h
+    rw [← Iter.toIter_toIterM (it := it)]
+    generalize it.toIterM = it at ⊢ h
+    induction h with
+    | direct h =>
+      exact .direct h
+    | indirect h h' ih =>
+      rename_i it it' out
+      replace h : it'.toIter.IsPlausibleSuccessorOf it.toIter := h
+      exact .indirect (α := α) h ih
+
 /--
 Asserts that a certain iterator `it'` could plausibly be the directly succeeding iterator of another
 given iterator `it` while no value is emitted (see `IterStep.skip`).
@@ -456,6 +568,7 @@ structure IterM.TerminationMeasures.Finite
 The relation of plausible successors on `IterM.TerminationMeasures.Finite`. It is well-founded
 if there is a `Finite` instance.
 -/
+@[expose]
 def IterM.TerminationMeasures.Finite.Rel
     {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β] :
     TerminationMeasures.Finite α m → TerminationMeasures.Finite α m → Prop :=
@@ -464,12 +577,14 @@ def IterM.TerminationMeasures.Finite.Rel
 instance {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β]
     [Finite α m] : WellFoundedRelation (IterM.TerminationMeasures.Finite α m) where
   rel := IterM.TerminationMeasures.Finite.Rel
-  wf := (InvImage.wf _ Finite.wf).transGen
+  -- TODO: workaround for module system issue?
+  wf := by exact (InvImage.wf _ Finite.wf).transGen
 
 /--
 Termination measure to be used in well-founded recursive functions recursing over a finite iterator
 (see also `Finite`).
 -/
+@[expose]
 def IterM.finitelyManySteps {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β]
     [Finite α m] (it : IterM (α := α) m β) : IterM.TerminationMeasures.Finite α m :=
   ⟨it⟩
@@ -496,7 +611,7 @@ macro_rules | `(tactic| decreasing_trivial) => `(tactic|
   | exact IterM.TerminationMeasures.Finite.rel_of_yield ‹_›
   | exact IterM.TerminationMeasures.Finite.rel_of_skip ‹_›)
 
-@[inherit_doc IterM.finitelyManySteps]
+@[inherit_doc IterM.finitelyManySteps, expose]
 def Iter.finitelyManySteps {α : Type w} {β : Type w} [Iterator α Id β] [Finite α Id]
     (it : Iter (α := α) β) : IterM.TerminationMeasures.Finite α Id :=
   it.toIterM.finitelyManySteps
@@ -561,6 +676,7 @@ structure IterM.TerminationMeasures.Productive
 The relation of plausible successors while skipping on `IterM.TerminationMeasures.Productive`.
 It is well-founded if there is a `Productive` instance.
 -/
+@[expose]
 def IterM.TerminationMeasures.Productive.Rel
     {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β] :
     TerminationMeasures.Productive α m → TerminationMeasures.Productive α m → Prop :=
@@ -569,12 +685,14 @@ def IterM.TerminationMeasures.Productive.Rel
 instance {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β]
     [Productive α m] : WellFoundedRelation (IterM.TerminationMeasures.Productive α m) where
   rel := IterM.TerminationMeasures.Productive.Rel
-  wf := (InvImage.wf _ Productive.wf).transGen
+  -- TODO: workaround for module system issue?
+  wf := by exact (InvImage.wf _ Productive.wf).transGen
 
 /--
 Termination measure to be used in well-founded recursive functions recursing over a productive
 iterator (see also `Productive`).
 -/
+@[expose]
 def IterM.finitelyManySkips {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β]
     [Productive α m] (it : IterM (α := α) m β) : IterM.TerminationMeasures.Productive α m :=
   ⟨it⟩
@@ -592,7 +710,7 @@ theorem IterM.TerminationMeasures.Productive.rel_of_skip
 macro_rules | `(tactic| decreasing_trivial) => `(tactic|
   exact IterM.TerminationMeasures.Productive.rel_of_skip ‹_›)
 
-@[inherit_doc IterM.finitelyManySkips]
+@[inherit_doc IterM.finitelyManySkips, expose]
 def Iter.finitelyManySkips {α : Type w} {β : Type w} [Iterator α Id β] [Productive α Id]
     (it : Iter (α := α) β) : IterM.TerminationMeasures.Productive α Id :=
   it.toIterM.finitelyManySkips

src/Init/Data/Iterators/Consumers.lean

@@ -0,0 +1,13 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Paul Reichert
+-/
+module
+
+prelude
+import Init.Data.Iterators.Consumers.Monadic
+import Init.Data.Iterators.Consumers.Access
+import Init.Data.Iterators.Consumers.Collect
+import Init.Data.Iterators.Consumers.Loop
+import Init.Data.Iterators.Consumers.Partial

src/Init/Data/Iterators/Consumers/Access.lean

@@ -3,8 +3,10 @@ Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Paul Reichert
 -/
+module
+
 prelude
-import Std.Data.Iterators.Consumers.Partial
+import Init.Data.Iterators.Consumers.Partial
 
 namespace Std.Iterators
 

src/Init/Data/Iterators/Consumers/Collect.lean

@@ -3,10 +3,12 @@ Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Paul Reichert
 -/
+module
+
 prelude
-import Std.Data.Iterators.Basic
-import Std.Data.Iterators.Consumers.Partial
-import Std.Data.Iterators.Consumers.Monadic.Collect
+import Init.Data.Iterators.Basic
+import Init.Data.Iterators.Consumers.Partial
+import Init.Data.Iterators.Consumers.Monadic.Collect
 
 /-!
 # Collectors

src/Init/Data/Iterators/Consumers/Loop.lean

@@ -3,9 +3,11 @@ Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Paul Reichert
 -/
+module
+
 prelude
-import Std.Data.Iterators.Consumers.Monadic.Loop
-import Std.Data.Iterators.Consumers.Partial
+import Init.Data.Iterators.Consumers.Monadic.Loop
+import Init.Data.Iterators.Consumers.Partial
 
 /-!
 # Loop consumers
@@ -24,9 +26,11 @@ namespace Std.Iterators
 
 instance (α : Type w) (β : Type w) (n : Type w → Type w') [Monad n]
     [Iterator α Id β] [Finite α Id] [IteratorLoop α Id n] :
-    ForIn n (Iter (α := α) β) β where
-  forIn it init f :=
-    IteratorLoop.finiteForIn (fun δ (c : Id δ) => pure c.run) |>.forIn it.toIterM init f
+    ForIn' n (Iter (α := α) β) β ⟨fun it out => it.IsPlausibleIndirectOutput out⟩ where
+  forIn' it init f :=
+    IteratorLoop.finiteForIn' (fun δ (c : Id δ) => pure c.run) |>.forIn' it.toIterM init
+        fun out h acc =>
+          f out (Iter.isPlausibleIndirectOutput_iff_isPlausibleIndirectOutput_toIterM.mpr h) acc
 
 instance (α : Type w) (β : Type w) (n : Type w → Type w') [Monad n]
     [Iterator α Id β] [IteratorLoopPartial α Id n] :
@@ -111,4 +115,14 @@ def Iter.Partial.fold {α : Type w} {β : Type w} {γ : Type w} [Iterator α Id
     (init : γ) (it : Iter.Partial (α := α) β) : γ :=
   ForIn.forIn (m := Id) it init (fun x acc => ForInStep.yield (f acc x))
 
+@[always_inline, inline, inherit_doc IterM.size]
+def Iter.size {α : Type w} {β : Type w} [Iterator α Id β] [IteratorSize α Id]
+    (it : Iter (α := α) β) : Nat :=
+  (IteratorSize.size it.toIterM).run.down
+
+@[always_inline, inline, inherit_doc IterM.Partial.size]
+def Iter.Partial.size {α : Type w} {β : Type w} [Iterator α Id β] [IteratorSizePartial α Id]
+    (it : Iter (α := α) β) : Nat :=
+  (IteratorSizePartial.size it.toIterM).run.down
+
 end Std.Iterators

src/Init/Data/Iterators/Consumers/Monadic.lean

@@ -0,0 +1,11 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Paul Reichert
+-/
+module
+
+prelude
+import Init.Data.Iterators.Consumers.Monadic.Collect
+import Init.Data.Iterators.Consumers.Monadic.Loop
+import Init.Data.Iterators.Consumers.Monadic.Partial

src/Init/Data/Iterators/Consumers/Monadic/Collect.lean

@@ -3,9 +3,11 @@ Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Paul Reichert
 -/
+module
+
 prelude
-import Std.Data.Iterators.Consumers.Monadic.Partial
-import Std.Data.Internal.LawfulMonadLiftFunction
+import Init.Data.Iterators.Consumers.Monadic.Partial
+import Init.Data.Iterators.Internal.LawfulMonadLiftFunction
 
 /-!
 # Collectors

src/Init/Data/Iterators/Consumers/Monadic/Loop.lean

@@ -3,10 +3,12 @@ Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Paul Reichert
 -/
+module
+
 prelude
 import Init.RCases
-import Std.Data.Iterators.Basic
-import Std.Data.Iterators.Consumers.Monadic.Partial
+import Init.Data.Iterators.Basic
+import Init.Data.Iterators.Consumers.Monadic.Partial
 
 /-!
 # Loop-based consumers
@@ -62,8 +64,9 @@ class IteratorLoop (α : Type w) (m : Type w → Type w') {β : Type w} [Iterato
   forIn : ∀ (_lift : (γ : Type w) → m γ → n γ) (γ : Type w),
       (plausible_forInStep : β → γ → ForInStep γ → Prop) →
       IteratorLoop.WellFounded α m plausible_forInStep →
-      IterM (α := α) m β → γ →
-      ((b : β) → (c : γ) → n (Subtype (plausible_forInStep b c))) → n γ
+      (it : IterM (α := α) m β) → γ →
+      ((b : β) → it.IsPlausibleIndirectOutput b → (c : γ) → n (Subtype (plausible_forInStep b c))) →
+      n γ
 
 /--
 `IteratorLoopPartial α m` provides efficient implementations of loop-based consumers for `α`-based
@@ -76,7 +79,14 @@ provided by the standard library.
 class IteratorLoopPartial (α : Type w) (m : Type w → Type w') {β : Type w} [Iterator α m β]
     (n : Type w → Type w'') where
   forInPartial : ∀ (_lift : (γ : Type w) → m γ → n γ) {γ : Type w},
-      IterM (α := α) m β → γ → ((b : β) → (c : γ) → n (ForInStep γ)) → n γ
+      (it : IterM (α := α) m β) → γ →
+      ((b : β) → it.IsPlausibleIndirectOutput b → (c : γ) → n (ForInStep γ)) → n γ
+
+class IteratorSize (α : Type w) (m : Type w → Type w') {β : Type w} [Iterator α m β] where
+  size : IterM (α := α) m β → m (ULift Nat)
+
+class IteratorSizePartial (α : Type w) (m : Type w → Type w') {β : Type w} [Iterator α m β] where
+  size : IterM (α := α) m β → m (ULift Nat)
 
 end Typeclasses
 
@@ -91,7 +101,7 @@ private def IteratorLoop.WFRel.mk {α : Type w} {m : Type w → Type w'} {β : T
     IteratorLoop.WFRel wf :=
   (it, c)
 
-instance {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β]
+private instance {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β]
     {γ : Type x} {plausible_forInStep : β → γ → ForInStep γ → Prop}
     (wf : IteratorLoop.WellFounded α m plausible_forInStep) :
     WellFoundedRelation (IteratorLoop.WFRel wf) where
@@ -109,16 +119,20 @@ def IterM.DefaultConsumers.forIn {m : Type w → Type w'} {α : Type w} {β : Ty
     (plausible_forInStep : β → γ → ForInStep γ → Prop)
     (wf : IteratorLoop.WellFounded α m plausible_forInStep)
     (it : IterM (α := α) m β) (init : γ)
-    (f : (b : β) → (c : γ) → n (Subtype (plausible_forInStep b c))) : n γ :=
+    (f : (b : β) → it.IsPlausibleIndirectOutput b → (c : γ) → n (Subtype (plausible_forInStep b c))) : n γ :=
   haveI : WellFounded _ := wf
   letI : MonadLift m n := ⟨fun {γ} => lift γ⟩
   do
     match ← it.step with
-    | .yield it' out _ =>
-      match ← f out init with
-      | ⟨.yield c, _⟩ => IterM.DefaultConsumers.forIn lift _ plausible_forInStep wf it' c f
+    | .yield it' out h =>
+      match ← f out (.direct ⟨_, h⟩) init with
+      | ⟨.yield c, _⟩ =>
+        IterM.DefaultConsumers.forIn lift _ plausible_forInStep wf it' c
+          (fun out h' acc => f out (.indirect ⟨_, rfl, h⟩ h') acc)
       | ⟨.done c, _⟩ => return c
-    | .skip it' _ => IterM.DefaultConsumers.forIn lift _ plausible_forInStep wf it' init f
+    | .skip it' h =>
+      IterM.DefaultConsumers.forIn lift _ plausible_forInStep wf it' init
+        (fun out h' acc => f out (.indirect ⟨_, rfl, h⟩ h') acc)
     | .done _ => return init
 termination_by IteratorLoop.WFRel.mk wf it init
 decreasing_by
@@ -153,15 +167,19 @@ partial def IterM.DefaultConsumers.forInPartial {m : Type w → Type w'} {α : T
     {n : Type w → Type w''} [Monad n]
     (lift : ∀ γ, m γ → n γ) (γ : Type w)
     (it : IterM (α := α) m β) (init : γ)
-    (f : (b : β) → (c : γ) → n (ForInStep γ)) : n γ :=
+    (f : (b : β) → it.IsPlausibleIndirectOutput b → (c : γ) → n (ForInStep γ)) : n γ :=
   letI : MonadLift m n := ⟨fun {γ} => lift γ⟩
   do
     match ← it.step with
-    | .yield it' out _ =>
-      match ← f out init with
-      | .yield c => IterM.DefaultConsumers.forInPartial lift _ it' c f
+    | .yield it' out h =>
+      match ← f out (.direct ⟨_, h⟩) init with
+      | .yield c =>
+        IterM.DefaultConsumers.forInPartial lift _ it' c
+          fun out h' acc => f out (.indirect ⟨_, rfl, h⟩ h') acc
       | .done c => return c
-    | .skip it' _ => IterM.DefaultConsumers.forInPartial lift _ it' init f
+    | .skip it' h =>
+      IterM.DefaultConsumers.forInPartial lift _ it' init
+        fun out h' acc => f out (.indirect ⟨_, rfl, h⟩ h') acc
     | .done _ => return init
 
 /--
@@ -196,27 +214,28 @@ theorem IteratorLoop.wellFounded_of_finite {m : Type w → Type w'}
     exact WellFoundedRelation.wf
 
 /--
-This `ForIn`-style loop construct traverses a finite iterator using an `IteratorLoop` instance.
+This `ForIn'`-style loop construct traverses a finite iterator using an `IteratorLoop` instance.
 -/
 @[always_inline, inline]
-def IteratorLoop.finiteForIn {m : Type w → Type w'} {n : Type w → Type w''}
+def IteratorLoop.finiteForIn' {m : Type w → Type w'} {n : Type w → Type w''}
     {α : Type w} {β : Type w} [Iterator α m β] [Finite α m] [IteratorLoop α m n]
     (lift : ∀ γ, m γ → n γ) :
-    ForIn n (IterM (α := α) m β) β where
-  forIn {γ} [Monad n] it init f :=
+    ForIn' n (IterM (α := α) m β) β ⟨fun it out => it.IsPlausibleIndirectOutput out⟩ where
+  forIn' {γ} [Monad n] it init f :=
     IteratorLoop.forIn (α := α) (m := m) lift γ (fun _ _ _ => True)
       wellFounded_of_finite
-      it init ((⟨·, .intro⟩) <$> f · ·)
+      it init (fun out h acc => (⟨·, .intro⟩) <$> f out h acc)
 
 instance {m : Type w → Type w'} {n : Type w → Type w''}
     {α : Type w} {β : Type w} [Iterator α m β] [Finite α m] [IteratorLoop α m n]
     [MonadLiftT m n] :
-    ForIn n (IterM (α := α) m β) β := IteratorLoop.finiteForIn (fun _ => monadLift)
+    ForIn' n (IterM (α := α) m β) β ⟨fun it out => it.IsPlausibleIndirectOutput out⟩ :=
+  IteratorLoop.finiteForIn' (fun _ => monadLift)
 
 instance {m : Type w → Type w'} {n : Type w → Type w''}
     {α : Type w} {β : Type w} [Iterator α m β] [IteratorLoopPartial α m n] [MonadLiftT m n] :
-    ForIn n (IterM.Partial (α := α) m β) β where
-  forIn it init f :=
+    ForIn' n (IterM.Partial (α := α) m β) β ⟨fun it out => it.it.IsPlausibleIndirectOutput out⟩ where
+  forIn' it init f :=
     IteratorLoopPartial.forInPartial (α := α) (m := m) (fun _ => monadLift) it.it init f
 
 instance {m : Type w → Type w'} {n : Type w → Type w''}
@@ -327,4 +346,42 @@ def IterM.Partial.drain {α : Type w} {m : Type w → Type w'} [Monad m] {β : T
     m PUnit :=
   it.fold (γ := PUnit) (fun _ _ => .unit) .unit
 
+section Size
+
+@[always_inline, inline]
+def IterM.DefaultConsumers.size {α : Type w} {m : Type w → Type w'} [Monad m] {β : Type w}
+    [Iterator α m β] [IteratorLoop α m m] [Finite α m] (it : IterM (α := α) m β) :
+    m (ULift Nat) :=
+  it.fold (init := .up 0) fun acc _ => .up (acc.down + 1)
+
+@[always_inline, inline]
+def IterM.DefaultConsumers.sizePartial {α : Type w} {m : Type w → Type w'} [Monad m] {β : Type w}
+    [Iterator α m β] [IteratorLoopPartial α m m] (it : IterM (α := α) m β) :
+    m (ULift Nat) :=
+  it.allowNontermination.fold (init := .up 0) fun acc _ => .up (acc.down + 1)
+
+@[always_inline, inline]
+instance IteratorSize.defaultImplementation {α β : Type w} {m : Type w → Type w'} [Monad m]
+    [Iterator α m β] [Finite α m] [IteratorLoop α m m] :
+    IteratorSize α m where
+  size := IterM.DefaultConsumers.size
+
+@[always_inline, inline]
+instance IteratorSize.Partial.defaultImplementation {α β : Type w} {m : Type w → Type w'} [Monad m]
+    [Iterator α m β] [Finite α m] [IteratorLoopPartial α m m] :
+    IteratorSizePartial α m where
+  size := IterM.DefaultConsumers.sizePartial
+
+@[always_inline, inline]
+def IterM.size {α : Type} {m : Type → Type w'} {β : Type} [Iterator α m β] [Monad m]
+    (it : IterM (α := α) m β) [IteratorSize α m] : m Nat :=
+  ULift.down <$> IteratorSize.size it
+
+@[always_inline, inline]
+def IterM.Partial.size {α : Type} {m : Type → Type w'} {β : Type} [Iterator α m β] [Monad m]
+    (it : IterM.Partial (α := α) m β) [IteratorSizePartial α m] : m Nat :=
+  ULift.down <$> IteratorSizePartial.size it.it
+
+end Size
+
 end Std.Iterators

src/Init/Data/Iterators/Consumers/Monadic/Partial.lean

@@ -3,8 +3,10 @@ Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Paul Reichert
 -/
+module
+
 prelude
-import Std.Data.Iterators.Basic
+import Init.Data.Iterators.Basic
 
 namespace Std.Iterators
 

src/Init/Data/Iterators/Consumers/Partial.lean

@@ -3,8 +3,10 @@ Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Paul Reichert
 -/
+module
+
 prelude
-import Std.Data.Iterators.Basic
+import Init.Data.Iterators.Basic
 
 namespace Std.Iterators
 

src/Init/Data/Iterators/Internal.lean

@@ -3,5 +3,8 @@ Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Paul Reichert
 -/
+module
+
 prelude
-import Std.Data.Iterators.Internal.Termination
+import Init.Data.Iterators.Internal.LawfulMonadLiftFunction
+import Init.Data.Iterators.Internal.Termination

src/Init/Data/Iterators/Internal/LawfulMonadLiftFunction.lean

@@ -3,6 +3,8 @@ Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Paul Reichert
 -/
+module
+
 prelude
 import Init.Control.Basic
 import Init.Control.Lawful.Basic

src/Init/Data/Iterators/Internal/Termination.lean

@@ -3,8 +3,10 @@ Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Paul Reichert
 -/
+module
+
 prelude
-import Std.Data.Iterators.Basic
+import Init.Data.Iterators.Basic
 
 /-!
 This is an internal module used by iterator implementations.

src/Init/Data/Iterators/Lemmas.lean

@@ -0,0 +1,4 @@
+module
+
+prelude
+import Init.Data.Iterators.Lemmas.Consumers

src/Init/Data/Iterators/Lemmas/Consumers.lean

@@ -0,0 +1,6 @@
+module
+
+prelude
+import Init.Data.Iterators.Lemmas.Consumers.Monadic
+import Init.Data.Iterators.Lemmas.Consumers.Collect
+import Init.Data.Iterators.Lemmas.Consumers.Loop

src/Init/Data/Iterators/Lemmas/Consumers/Collect.lean

@@ -4,10 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Paul Reichert
 -/
 prelude
-import Std.Data.Iterators.Consumers.Access
-import Std.Data.Iterators.Consumers.Collect
+import Init.Data.Iterators.Consumers.Access
+import Init.Data.Iterators.Consumers.Collect
 import Std.Data.Iterators.Lemmas.Basic
-import Std.Data.Iterators.Lemmas.Consumers.Monadic.Collect
+import Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect
 
 namespace Std.Iterators
 

src/Init/Data/Iterators/Lemmas/Consumers/Loop.lean

@@ -6,20 +6,31 @@ Authors: Paul Reichert
 prelude
 import Init.Data.List.Control
 import Std.Data.Iterators.Lemmas.Basic
-import Std.Data.Iterators.Lemmas.Consumers.Collect
-import Std.Data.Iterators.Lemmas.Consumers.Monadic.Loop
-import Std.Data.Iterators.Consumers.Collect
-import Std.Data.Iterators.Consumers.Loop
+import Init.Data.Iterators.Lemmas.Consumers.Collect
+import Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
+import Init.Data.Iterators.Consumers.Collect
+import Init.Data.Iterators.Consumers.Loop
 
 namespace Std.Iterators
 
+theorem Iter.forIn'_eq {α β : Type w} [Iterator α Id β] [Finite α Id]
+    {m : Type w → Type w''} [Monad m] [IteratorLoop α Id m] [hl : LawfulIteratorLoop α Id m]
+    {γ : Type w} {it : Iter (α := α) β} {init : γ}
+    {f : (b : β) → it.IsPlausibleIndirectOutput b → γ → m (ForInStep γ)} :
+    ForIn'.forIn' it init f =
+      IterM.DefaultConsumers.forIn (fun _ c => pure c.run) γ (fun _ _ _ => True)
+        IteratorLoop.wellFounded_of_finite it.toIterM init
+          (fun out h acc => (⟨·, .intro⟩) <$>
+            f out (Iter.isPlausibleIndirectOutput_iff_isPlausibleIndirectOutput_toIterM.mpr h) acc) := by
+  cases hl.lawful; rfl
+
 theorem Iter.forIn_eq {α β : Type w} [Iterator α Id β] [Finite α Id]
     {m : Type w → Type w''} [Monad m] [IteratorLoop α Id m] [hl : LawfulIteratorLoop α Id m]
     {γ : Type w} {it : Iter (α := α) β} {init : γ}
     {f : β → γ → m (ForInStep γ)} :
     ForIn.forIn it init f =
       IterM.DefaultConsumers.forIn (fun _ c => pure c.run) γ (fun _ _ _ => True)
-        IteratorLoop.wellFounded_of_finite it.toIterM init ((⟨·, .intro⟩) <$> f · ·) := by
+        IteratorLoop.wellFounded_of_finite it.toIterM init (fun out _ acc => (⟨·, .intro⟩) <$> f out acc) := by
   cases hl.lawful; rfl
 
 theorem Iter.forIn_eq_forIn_toIterM {α β : Type w} [Iterator α Id β]

src/Init/Data/Iterators/Lemmas/Consumers/Monadic.lean

@@ -4,5 +4,5 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Paul Reichert
 -/
 prelude
-import Std.Data.Iterators.Lemmas.Consumers.Monadic.Collect
-import Std.Data.Iterators.Lemmas.Consumers.Monadic.Loop
+import Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect
+import Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop

src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Collect.lean

@@ -5,7 +5,7 @@ Authors: Paul Reichert
 -/
 prelude
 import Init.Data.Array.Lemmas
-import Std.Data.Iterators.Consumers.Monadic.Collect
+import Init.Data.Iterators.Consumers.Monadic.Collect
 import Std.Data.Iterators.Lemmas.Monadic.Basic
 import Std.Data.Iterators.Producers
 import Std.Data.Iterators.Lemmas.Equivalence.StepCongr

src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Loop.lean

@@ -5,41 +5,53 @@ Authors: Paul Reichert
 -/
 prelude
 import Init.Control.Lawful.Basic
-import Std.Data.Iterators.Consumers.Monadic.Collect
-import Std.Data.Iterators.Consumers.Monadic.Loop
+import Init.Data.Iterators.Consumers.Monadic.Collect
+import Init.Data.Iterators.Consumers.Monadic.Loop
 import Std.Data.Iterators.Lemmas.Monadic.Basic
-import Std.Data.Iterators.Lemmas.Consumers.Monadic.Collect
+import Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect
 import Std.Data.Iterators.Lemmas.Equivalence.StepCongr
 
 namespace Std.Iterators
 
-theorem IterM.DefaultConsumers.forIn_eq_match_step {α β : Type w} {m : Type w → Type w'}
+theorem IterM.DefaultConsumers.forIn'_eq_match_step {α β : Type w} {m : Type w → Type w'}
     [Iterator α m β]
     {n : Type w → Type w''} [Monad n]
     {lift : ∀ γ, m γ → n γ} {γ : Type w}
     {plausible_forInStep : β → γ → ForInStep γ → Prop}
     {wf : IteratorLoop.WellFounded α m plausible_forInStep}
     {it : IterM (α := α) m β} {init : γ}
-    {f : (b : β) → (c : γ) → n (Subtype (plausible_forInStep b c))} :
+    {f : (b : β) → it.IsPlausibleIndirectOutput b → (c : γ) → n (Subtype (plausible_forInStep b c))} :
     IterM.DefaultConsumers.forIn lift γ plausible_forInStep wf it init f = (do
       match ← lift _ it.step with
-      | .yield it' out _ =>
-        match ← f out init with
-        | ⟨.yield c, _⟩ => IterM.DefaultConsumers.forIn lift _ plausible_forInStep wf it' c f
+      | .yield it' out h =>
+        match ← f out (.direct ⟨_, h⟩) init with
+        | ⟨.yield c, _⟩ =>
+          IterM.DefaultConsumers.forIn lift _ plausible_forInStep wf it' c
+            fun out h'' acc => f out (.indirect ⟨_, rfl, h⟩ h'') acc
         | ⟨.done c, _⟩ => return c
-      | .skip it' _ => IterM.DefaultConsumers.forIn lift _ plausible_forInStep wf it' init f
+      | .skip it' h =>
+        IterM.DefaultConsumers.forIn lift _ plausible_forInStep wf it' init
+          fun out h' acc => f out (.indirect ⟨_, rfl, h⟩ h') acc
       | .done _ => return init) := by
   rw [forIn]
   apply bind_congr
   intro step
   cases step using PlausibleIterStep.casesOn <;> rfl
 
+theorem IterM.forIn'_eq {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [Finite α m]
+    {n : Type w → Type w''} [Monad n] [IteratorLoop α m n] [hl : LawfulIteratorLoop α m n]
+    [MonadLiftT m n] {γ : Type w} {it : IterM (α := α) m β} {init : γ}
+    {f : (b : β) → it.IsPlausibleIndirectOutput b → γ → n (ForInStep γ)} :
+    ForIn'.forIn' it init f = IterM.DefaultConsumers.forIn (fun _ => monadLift) γ (fun _ _ _ => True)
+        IteratorLoop.wellFounded_of_finite it init ((⟨·, .intro⟩) <$> f · · ·) := by
+  cases hl.lawful; rfl
+
 theorem IterM.forIn_eq {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [Finite α m]
     {n : Type w → Type w''} [Monad n] [IteratorLoop α m n] [hl : LawfulIteratorLoop α m n]
     [MonadLiftT m n] {γ : Type w} {it : IterM (α := α) m β} {init : γ}
     {f : β → γ → n (ForInStep γ)} :
     ForIn.forIn it init f = IterM.DefaultConsumers.forIn (fun _ => monadLift) γ (fun _ _ _ => True)
-        IteratorLoop.wellFounded_of_finite it init ((⟨·, .intro⟩) <$> f · ·) := by
+        IteratorLoop.wellFounded_of_finite it init (fun out _ acc => (⟨·, .intro⟩) <$> f out acc) := by
   cases hl.lawful; rfl
 
 theorem IterM.forIn_eq_match_step {α β : Type w} {m : Type w → Type w'} [Iterator α m β]
@@ -55,7 +67,7 @@ theorem IterM.forIn_eq_match_step {α β : Type w} {m : Type w → Type w'} [Ite
         | .done c => return c
       | .skip it' _ => ForIn.forIn it' init f
       | .done _ => return init) := by
-  rw [IterM.forIn_eq, DefaultConsumers.forIn_eq_match_step]
+  rw [IterM.forIn_eq, DefaultConsumers.forIn'_eq_match_step]
   apply bind_congr
   intro step
   cases step using PlausibleIterStep.casesOn

src/Init/Data/Iterators/PostconditionMonad.lean

@@ -3,6 +3,8 @@ Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Paul Reichert
 -/
+module
+
 prelude
 import Init.Control.Lawful.Basic
 import Init.Data.Subtype
@@ -48,6 +50,7 @@ def PostconditionT.lift {α : Type w} {m : Type w → Type w'} [Functor m] (x :
     PostconditionT m α :=
   ⟨fun _ => True, (⟨·, .intro⟩) <$> x⟩
 
+@[always_inline, inline]
 protected def PostconditionT.pure {m : Type w → Type w'} [Pure m] {α : Type w}
     (a : α) : PostconditionT m α :=
   ⟨fun y => a = y, pure <| ⟨a, rfl⟩⟩
@@ -117,16 +120,20 @@ instance {m : Type w → Type w'} [Monad m] : Monad (PostconditionT m) where
   pure := PostconditionT.pure
   bind := PostconditionT.bind
 
-@[simp]
-theorem PostconditionT.computation_pure {m : Type w → Type w'} [Monad m] {α : Type w}
-    {x : α} :
-    (pure x : PostconditionT m α).operation = pure ⟨x, rfl⟩ :=
+theorem PostconditionT.pure_eq_pure {m : Type w → Type w'} [Monad m] {α} {a : α} :
+    pure a = PostconditionT.pure (m := m) a :=
   rfl
 
 @[simp]
 theorem PostconditionT.property_pure {m : Type w → Type w'} [Monad m] {α : Type w}
     {x : α} :
-    (pure x : PostconditionT m α).Property = (x = ·) :=
+    (pure x : PostconditionT m α).Property = (x = ·) := by
+  rfl
+
+@[simp]
+theorem PostconditionT.operation_pure {m : Type w → Type w'} [Monad m] {α : Type w}
+    {x : α} :
+    (pure x : PostconditionT m α).operation = pure ⟨x, property_pure (m := m) ▸ rfl⟩ := by
   rfl
 
 theorem PostconditionT.ext {m : Type w → Type w'} [Monad m] [LawfulMonad m]
@@ -209,12 +216,19 @@ theorem PostconditionT.property_map {m : Type w → Type w'} [Functor m] {α : T
 @[simp]
 theorem PostconditionT.operation_map {m : Type w → Type w'} [Functor m] {α : Type w} {β : Type w}
     {x : PostconditionT m α} {f : α → β} :
-    (x.map f).operation = (fun a => ⟨_, a, rfl⟩) <$> x.operation :=
+    (x.map f).operation =
+      (fun a => ⟨_, (property_map (m := m)).mpr ⟨a.1, rfl, a.2⟩⟩) <$> x.operation := by
   rfl
 
 @[simp]
-theorem PostconditionT.operation_lift {m : Type w →Type w'} [Functor m] {α : Type w}
-    {x : m α} : (lift x : PostconditionT m α).operation = (⟨·, True.intro⟩) <$> x :=
+theorem PostconditionT.property_lift {m : Type w → Type w'} [Functor m] {α : Type w}
+    {x : m α} : (lift x : PostconditionT m α).Property = (fun _ => True) := by
+  rfl
+
+@[simp]
+theorem PostconditionT.operation_lift {m : Type w → Type w'} [Functor m] {α : Type w}
+    {x : m α} : (lift x : PostconditionT m α).operation =
+      (⟨·, property_lift (m := m) ▸ True.intro⟩) <$> x := by
   rfl
 
 end Std.Iterators

src/Init/Data/List/Range.lean

@@ -8,6 +8,7 @@ module
 prelude
 import Init.Data.List.Pairwise
 import Init.Data.List.Zip
+import Init.Data.Range.Classes
 
 /-!
 # Lemmas about `List.range` and `List.zipIdx`

src/Init/Data/Range/Classes.lean

@@ -0,0 +1,49 @@
+module
+
+prelude
+import Init.Core
+import Init.Data.Nat.Basic
+import Init.Data.Option.Basic
+
+class Succ? (α : Type u) where
+  succ? : α → Option α
+  succAtIdx? (n : Nat) (a : α) : Option α := Nat.repeat (· >>= succ?) n (some a)
+
+class LawfulSucc? (α : Type u) [Succ? α] where
+  succAtIdx?_zero {a : α} : Succ?.succAtIdx? 0 a = some a
+  succAtIdx?_succ {a : α} : Succ?.succAtIdx? (n + 1) a = Succ?.succAtIdx? n a >>= Succ?.succ?
+
+class LawfulLESucc? (α : Type u) [LE α] [Succ? α] where
+  le_rfl : {a : α} → a ≤ a
+  le_succ? : {a b : α} → Succ?.succ? a = some b → a ≤ b
+  le_succ?_of_le : {a b c : α} → a ≤ b → (h : Succ?.succ? b = some c) → a ≤ c
+  le_succAtIdx?_of_le : {a b c : α} → {n : Nat} → a ≤ b → (h : Succ?.succAtIdx? n b = some c) → a ≤ c
+
+class LawfulLTSucc? [LT α] [Succ? α] where
+  lt_succ? : {a b : α} → (h : Succ?.succ? a = some b) → a < b
+  lt_succ?_of_lt : {a b c : α} → a < b → (h : Succ?.succ? b = some c) → a < c
+
+class HasDownwardUnboundedRanges (α : Type u) where
+  min : α
+
+instance : Succ? Nat where
+  succ? n := some (n + 1)
+  succAtIdx? k n := some (n + k)
+
+instance : LawfulSucc? Nat where
+  succAtIdx?_zero := by simp [Succ?.succAtIdx?]
+  succAtIdx?_succ := by simp [Succ?.succAtIdx?, Succ?.succ?, Bind.bind, Nat.add_assoc]
+
+instance : LawfulLESucc? Nat where
+  le_rfl := Nat.le_refl _
+  le_succ? := sorry
+  le_succ?_of_le hle h := by
+    simp only [Succ?.succ?, Option.some.injEq] at h
+    rw [← h]
+    exact Nat.le_trans hle (Nat.le_succ _)
+  le_succAtIdx?_of_le {a b c n} hle h := by
+    simp only [Succ?.succAtIdx?, Option.some.injEq] at h
+    rw [← h]
+    exact Nat.le_trans hle (Nat.le_add_right _ _)
+
+#print instLawfulLESucc?Nat._proof_2

src/Init/Data/Range/New/Basic.lean

@@ -0,0 +1,329 @@
+module
+
+prelude
+import Init.Core
+import Init.NotationExtra
+import Init.Data.Range.Classes
+
+import Init.Data.Range.New.RangeIterator
+
+open Std.Iterators
+
+inductive BoundShape where
+  | «open» : BoundShape
+  | closed : BoundShape
+  | none : BoundShape
+
+structure RangeShape where
+  lower : BoundShape
+  upper : BoundShape
+
+abbrev Bound (shape : BoundShape) (α : Type u) : Type u :=
+  match shape with
+  | .open | .closed => α
+  | .none => PUnit
+
+structure PRange (shape : RangeShape) (α : Type u) where
+  lower : Bound shape.lower α
+  upper : Bound shape.upper α
+
+syntax:max (term ",," term) : term
+syntax:max (",," term) : term
+syntax:max (term ",,") : term
+syntax:max (",,") : term
+syntax:max (term "<,," term) : term
+syntax:max (term "<,,") : term
+syntax:max (term ",,<" term) : term
+syntax:max (",,<" term) : term
+syntax:max (term "<,,<" term) : term
+
+macro_rules
+  | `($a,,$b) => ``(PRange.mk (shape := RangeShape.mk BoundShape.closed BoundShape.closed) $a $b)
+  | `(,,$b) => ``(PRange.mk (shape := RangeShape.mk BoundShape.none BoundShape.closed) PUnit.unit $b)
+  | `($a,,) => ``(PRange.mk (shape := RangeShape.mk BoundShape.closed BoundShape.none) $a PUnit.unit)
+  | `(,,) => ``(PRange.mk (shape := RangeShape.mk BoundShape.none BoundShape.none) PUnit.unit PUnit.unit)
+  | `($a<,,$b) => ``(PRange.mk (shape := RangeShape.mk BoundShape.open BoundShape.closed) $a $b)
+  | `($a<,,) => ``(PRange.mk (shape := RangeShape.mk BoundShape.open BoundShape.none) $a PUnit.unit)
+  | `($a,,<$b) => ``(PRange.mk (shape := RangeShape.mk BoundShape.closed BoundShape.open) $a $b)
+  | `(,,<$b) => ``(PRange.mk (shape := RangeShape.mk BoundShape.none BoundShape.open) PUnit.unit $b)
+  | `($a<,,<$b) => ``(PRange.mk (shape := RangeShape.mk BoundShape.open BoundShape.open) $a $b)
+
+class RangeIter (shape : RangeShape) (α : Type u) where
+  State : PRange shape α → Type u
+  iter : (r : PRange shape α) → Iter (α := State r) α
+
+@[always_inline, inline, expose]
+def RangeIter.of {State : PRange shape α → Type u}
+    (iter : (r : PRange shape α) → Iter (α := State r) α) :
+    RangeIter shape α where
+  State := State
+  iter := iter
+
+instance {State : PRange shape α → Type u}
+    {r : PRange shape α} [Iterator (State r) Id α]
+    {iter : (r : PRange shape α) → Iter (α := State r) α} :
+    letI : RangeIter shape α := RangeIter.of iter
+    Iterator (RangeIter.State (shape := shape) (α := α) r) Id α :=
+  inferInstanceAs <| Iterator (State r) Id α
+
+instance {State : PRange shape α → Type u} {r : PRange shape α}
+    [Iterator (State r) Id α]
+    [Finite (State r) Id]
+    {iter : (r : PRange shape α) → Iter (α := State r) α} :
+    letI : RangeIter shape α := RangeIter.of iter
+    Finite (RangeIter.State (shape := shape) (α := α) r) Id :=
+  inferInstanceAs <| Finite (State r) Id
+
+instance {State : PRange shape α → Type u} {r : PRange shape α}
+    [Iterator (State r) Id α] [IteratorCollect (State r) Id m]
+    {iter : (r : PRange shape α) → Iter (α := State r) α} :
+    letI : RangeIter shape α := RangeIter.of iter
+    IteratorCollect (RangeIter.State r) Id m :=
+  inferInstanceAs <| IteratorCollect (State r) Id m
+
+instance {State : PRange shape α → Type u} {r : PRange shape α}
+    [Iterator (State r) Id α] [IteratorCollectPartial (State r) Id m]
+    {iter : (r : PRange shape α) → Iter (α := State r) α} :
+    letI : RangeIter shape α := RangeIter.of iter
+    IteratorCollectPartial (RangeIter.State r) Id m :=
+  inferInstanceAs <| IteratorCollectPartial (State r) Id m
+
+instance {State : PRange shape α → Type u} {r : PRange shape α}
+    [Iterator (State r) Id α] [IteratorLoop (State r) Id m]
+    {iter : (r : PRange shape α) → Iter (α := State r) α} :
+    letI : RangeIter shape α := RangeIter.of iter
+    IteratorLoop (RangeIter.State r) Id m :=
+  inferInstanceAs <| IteratorLoop (State r) Id m
+
+instance {State : PRange shape α → Type u} {r : PRange shape α}
+    [Iterator (State r) Id α] [IteratorLoopPartial (State r) Id m]
+    {iter : (r : PRange shape α) → Iter (α := State r) α} :
+    letI : RangeIter shape α := RangeIter.of iter
+    IteratorLoopPartial (RangeIter.State r) Id m :=
+  inferInstanceAs <| IteratorLoopPartial (State r) Id m
+
+@[always_inline, inline]
+def PRange.iter [RangeIter shape α] (r : PRange shape α) :=
+  (RangeIter.iter r : Iter α)
+
+@[always_inline, inline]
+def PRange.size [RangeIter shape α] (r : PRange shape α)
+    [Iterator (RangeIter.State r) Id α] [IteratorSize (RangeIter.State r) Id] :
+    Nat :=
+  r.iter.size
+
+@[always_inline, inline]
+def PRange.toList [RangeIter shape α] (r : PRange shape α)
+    [Iterator (RangeIter.State r) Id α] [IteratorCollect (RangeIter.State r) Id Id]
+    [Finite (RangeIter.State r) Id] :
+    List α :=
+  r.iter.toList
+
+instance [i : RangeIter shape α] [∀ r, ForIn m (Iter (α := i.State r) α) α] :
+    ForIn m (PRange shape α) α where
+  forIn r := forIn r.iter
+
+instance : Membership α (PRange ⟨.none, .none⟩ α) where
+  mem _ _ := True
+
+instance (r : PRange ⟨.none, .none⟩ α) : Decidable (a ∈ r) :=
+  inferInstanceAs <| Decidable True
+
+instance [LT α] : Membership α (PRange ⟨.none, .open⟩ α) where
+  mem r a := a < r.upper
+
+instance [LT α] [DecidableLT α] (r : PRange ⟨.none, .open⟩ α) : Decidable (a ∈ r) :=
+  inferInstanceAs <| Decidable (a < r.upper)
+
+instance [LE α] : Membership α (PRange ⟨.none, .closed⟩ α) where
+  mem r a := a ≤ r.upper
+
+instance [LE α] [DecidableLE α] (r : PRange ⟨.none, .closed⟩ α) : Decidable (a ∈ r) :=
+  inferInstanceAs <| Decidable (a ≤ r.upper)
+
+instance [LT α] : Membership α (PRange ⟨.open, .none⟩ α) where
+  mem r a := r.lower < a
+
+instance [LT α] [DecidableLT α] (r : PRange ⟨.open, .none⟩ α) : Decidable (a ∈ r) :=
+  inferInstanceAs <| Decidable (r.lower < a)
+
+instance [LT α] : Membership α (PRange ⟨.open, .open⟩ α) where
+  mem r a := r.lower < a ∧ a < r.upper
+
+instance [LT α] [DecidableLT α] (r : PRange ⟨.open, .open⟩ α) : Decidable (a ∈ r) :=
+  inferInstanceAs <| Decidable (r.lower < a ∧ _)
+
+instance [LT α] [LE α] : Membership α (PRange ⟨.open, .closed⟩ α) where
+  mem r a := r.lower < a ∧ a ≤ r.upper
+
+instance [LT α] [DecidableLT α] [LE α] [DecidableLE α] (r : PRange ⟨.open, .closed⟩ α) :
+    Decidable (a ∈ r) :=
+  inferInstanceAs <| Decidable (_ ∧ _)
+
+instance [LE α] : Membership α (PRange ⟨.closed, .none⟩ α) where
+  mem r a := r.lower ≤ a
+
+instance [LE α] [DecidableLE α] (r : PRange ⟨.closed, .none⟩ α) : Decidable (a ∈ r) :=
+  inferInstanceAs <| Decidable (r.lower ≤ a)
+
+instance [LE α] [LT α] : Membership α (PRange ⟨.closed, .open⟩ α) where
+  mem r a := r.lower ≤ a ∧ a < r.upper
+
+instance [LT α] [DecidableLT α] [LE α] [DecidableLE α] (r : PRange ⟨.closed, .open⟩ α) :
+    Decidable (a ∈ r) :=
+  inferInstanceAs <| Decidable (_ ∧ _)
+
+instance [LE α] : Membership α (PRange ⟨.closed, .closed⟩ α) where
+  mem r a := r.lower ≤ a ∧ a ≤ r.upper
+
+instance [LE α] [DecidableLE α] (r : PRange ⟨.closed, .closed⟩ α) : Decidable (a ∈ r) :=
+  inferInstanceAs <| Decidable (_ ∧ _)
+
+
+section Iterator
+
+@[always_inline, inline]
+def Range.succIterator [Succ? α] (init : Option α) (Predicate : α → Bool) :
+    (Iter (α := Types.RangeIterator α inferInstance Predicate) α) :=
+  ⟨⟨init⟩⟩
+
+-- @[always_inline, inline]
+-- def Range.SuccIterator.next [Succ? α] (stepSize : Nat) (Predicate : α → Bool)
+--     {h : stepSize > 0} (it : SuccIterator stepSize Predicate h) : α :=
+--   it.inner.internalState.next
+
+-- @[no_expose]
+-- instance [Succ? α] (stepSize : Nat) (Predicate : α → Bool) (h) :
+--     Iterator (Range.SuccIterator stepSize Predicate h) Id α := by
+--   unfold Range.SuccIterator
+--   infer_instance
+
+-- @[no_expose]
+-- instance [Monad m] [Succ? α] (stepSize : Nat) (Predicate : α → Bool) (h) :
+--     IteratorCollect (Range.SuccIterator stepSize Predicate h) Id m := by
+--   unfold Range.SuccIterator
+--   infer_instance
+
+-- @[no_expose]
+-- instance [Monad m] [Succ? α] (stepSize : Nat) (Predicate : α → Bool) (h) :
+--     IteratorCollectPartial (Range.SuccIterator stepSize Predicate h) Id m := by
+--   unfold Range.SuccIterator
+--   infer_instance
+
+-- @[no_expose]
+-- instance [Monad m] [MonadLiftT Id m] [Succ? α] (stepSize : Nat) (Predicate : α → Bool) (h) :
+--     IteratorLoop (Range.SuccIterator stepSize Predicate h) Id m := by
+--   unfold Range.SuccIterator
+--   infer_instance
+
+-- @[no_expose]
+-- instance [Monad m] [MonadLiftT Id m] [Succ? α] (stepSize : Nat) (Predicate : α → Bool) (h) :
+--     IteratorLoopPartial (Range.SuccIterator stepSize Predicate h) Id m := by
+--   unfold Range.SuccIterator
+--   infer_instance
+
+-- TODO: Should we hide the ≤ or < predicates behind some identifier to avoid accidental rewriting?
+@[expose]
+instance [Succ? α] [LE α] [DecidableLE α] : RangeIter ⟨.closed, .closed⟩ α :=
+  .of fun r => Range.succIterator (some r.lower) (fun a => a ≤ r.upper)
+
+instance [Succ? α] [LT α] [DecidableLT α] : RangeIter ⟨.closed, .open⟩ α :=
+  .of fun r => Range.succIterator (some r.lower) (fun a => a < r.upper)
+
+instance [Succ? α] [LT α] [DecidableLT α] : RangeIter ⟨.closed, .none⟩ α :=
+  .of fun r => Range.succIterator (some r.lower) (fun _ => True)
+
+instance [Succ? α] [LE α] [DecidableLE α] : RangeIter ⟨.open, .closed⟩ α :=
+  .of fun r => Range.succIterator (Succ?.succ? r.lower) (fun a => a ≤ r.upper)
+
+instance [Succ? α] [LT α] [DecidableLT α] : RangeIter ⟨.open, .open⟩ α :=
+  .of fun r => Range.succIterator (Succ?.succ? r.lower) (fun a => a < r.upper)
+
+instance [Succ? α] [LT α] [DecidableLT α] : RangeIter ⟨.open, .none⟩ α :=
+  .of fun r => Range.succIterator (Succ?.succ? r.lower) (fun _ => True)
+
+instance [Succ? α] [LE α] [DecidableLE α] [HasDownwardUnboundedRanges α] :
+    RangeIter ⟨.none, .closed⟩ α :=
+  .of fun r => Range.succIterator (some HasDownwardUnboundedRanges.min) (· ≤ r.upper)
+
+-- TODO: iterators for ranges that are unbounded downwards
+
+-- theorem Range.SuccIterator.succ?_eq_some_of_isPlausibleSuccessorOf [Succ? α] [LE α] [DecidableLE α]
+--     {it' it : Iter (α := Types.RangeIterator α inferInstance P) α}
+--     [Finite (Types.RangeIterator α inferInstance P) Id]
+--     (h' : it'.IsPlausibleSuccessorOf it) :
+--     Succ?.succ? 1 it.internalState.next = some it'.internalState.next :=
+--   h' |>
+--     TakeWhile.isPlausibleSuccessorOf_inner_of_isPlausibleSuccessorOf |>
+--     RepeatIterator.Monadic.next_eq_some_of_isPlausibleSuccessorOf
+
+@[no_expose]
+instance [Succ? α] [LE α] [DecidableLE α] [LawfulLESucc? α] [Monad m]
+    [∀ a, Finite (Types.RangeIterator α inferInstance (· ≤ a)) Id] :
+    ForIn' m (PRange ⟨.closed, .closed⟩ α) α inferInstance where
+  forIn' r init f := by
+    haveI : MonadLift Id m := ⟨Std.Internal.idToMonad (α := _)⟩
+    refine ForIn'.forIn' (α := α) r.iter init (fun a ha acc => f a ?_ acc)
+    sorry
+    -- have hle : r.lower ≤ r.iter.internalState.next := by exact LawfulLESucc?.le_rfl (α := α)
+    -- generalize r.iter = it at ha hle
+    -- induction ha with
+    -- | direct =>
+    --   rename_i it out h
+    --   rcases h with ⟨it', h, h'⟩
+    --   refine ⟨?_, ?_⟩
+    --   · rcases h with ⟨rfl, _⟩
+    --     exact hle
+    --   · simpa [← PostconditionT.pure_eq_pure] using h'
+    -- | indirect =>
+    --   rename_i it it' it'' out h h' ih
+    --   apply ih
+    --   replace h := Range.SuccIterator.succ?_eq_some_of_isPlausibleSuccessorOf h
+    --   exact LawfulLESucc?.le_succAtIdx?_of_le (α := α) hle h
+
+@[no_expose]
+instance [Succ? α] [LT α] [DecidableLT α] [LE α] [DecidableLE α] [LawfulLESucc? α] [Monad m]
+    [∀ a, Finite (Types.RangeIterator α inferInstance (· < a)) Id] :
+    ForIn' m (PRange ⟨.closed, .open⟩ α) α inferInstance where
+  forIn' r init f := by
+    haveI : MonadLift Id m := ⟨Std.Internal.idToMonad (α := _)⟩
+    refine ForIn'.forIn' (α := α) r.iter init (fun a ha acc => f a ?_ acc)
+    sorry
+    -- have hle : r.lower ≤ r.iter.internalState.next := by exact LawfulLESucc?.le_rfl (α := α)
+    -- generalize r.iter = it at ha hle
+    -- induction ha with
+    -- | direct =>
+    --   rename_i it out h
+    --   rcases h with ⟨it', h, h'⟩
+    --   refine ⟨?_, ?_⟩
+    --   · rcases h with ⟨rfl, _⟩
+    --     exact hle
+    --   · simpa [← PostconditionT.pure_eq_pure] using h'
+    -- | indirect =>
+    --   rename_i it it' it'' out h h' ih
+    --   apply ih
+    --   replace h := Range.SuccIterator.succ?_eq_some_of_isPlausibleSuccessorOf h
+    --   exact LawfulLESucc?.le_succAtIdx?_of_le (α := α) hle h
+
+-- instance [Succ? α] [LE α] [DecidableLE α] [LawfulLESucc? α]
+--     [HasDownwardUnboundedRanges α] [Monad m]
+--     [∀ a h, Finite (Range.SuccIterator (α := α) 1  (· ≤ a) h) Id] :
+--     ForIn' m (PRange ⟨.none, .closed⟩ α) α inferInstance where
+--   forIn' r init f :=
+--     ForIn'.forIn' (HasDownwardUnboundedRanges.min,,r.upper) init
+--       fun out h acc => f out (by exact h.2) acc
+
+end Iterator
+
+theorem Range.mem.upper [LE α] {i : α} {r : PRange ⟨.none, .closed⟩ α} (h : i ∈ r) : i ≤ r.upper :=
+  h
+
+-- theorem Range.mem.lower [LE α] {i : α} {r : PRange ⟨.none, .closed⟩ α} (h : i ∈ r) : r.lower ≤ i := h.1
+
+-- theorem Range.mem.step {i : Nat} {r : PRange shape α} (h : i ∈ r) : (i - r.start) % r.step = 0 := h.2.2
+
+theorem Range.get_elem_helper {i n : Nat} {r : PRange ⟨.closed, .open⟩ Nat} (h₁ : i ∈ r) (h₂ : r.upper = n) :
+    i < n := h₂ ▸ h₁.2
+
+macro_rules
+  | `(tactic| get_elem_tactic_extensible) => `(tactic| apply Range.get_elem_helper; assumption; rfl)

src/Init/Data/Range/New/Lemmas.lean

@@ -0,0 +1,118 @@
+module
+
+prelude
+import all Init.Data.Range.New.Nat
+import Init.Data.List.Range
+
+namespace Std.PRange
+
+-- /-- Generalization of `mem_of_mem_range'` used in `forIn'_loop_eq_forIn'_range'` below. -/
+-- private theorem mem_of_mem_range'_aux [LE α] {r : PRange ⟨.closed, .closed⟩ α} {a : α}
+--     -- (w₁ : (i - r.lower) % r.step = 0)
+--     (w₂ : r.lower ≤ i)
+--     (h : a ∈ List.polymorphicRange i ((r.upper - i + r.step - 1) / r.step) r.step) : a ∈ r := by
+--   obtain ⟨j, h', rfl⟩ := List.mem_range'.1 h
+--   refine ⟨by omega, ?_⟩
+--   rw [Nat.lt_div_iff_mul_lt r.step_pos, Nat.mul_comm] at h'
+--   constructor
+--   · omega
+--   · rwa [Nat.add_comm, Nat.add_sub_assoc w₂, Nat.mul_add_mod_self_left]
+
+-- theorem mem_of_mem_range' [Succ? α] [LE α] [DecidableLE α] {r : PRange ⟨.closed, .closed⟩ α}
+--     [LawfulSucc? α]
+--     (h : x ∈ List.polymorphicRange r.lower r.size 1) : x ∈ r := by
+--   refine ⟨?_, ?_⟩
+--   ·
+--   unfold PRange.size at h
+--   apply mem_of_mem_range'_aux (by simp) (by simp) h
+
+@[simp] theorem mem_of_mem_toList [Succ? α] [LE α] [DecidableLE α]
+    [LawfulLESucc? α] [Monad m]
+    (r : PRange ⟨.closed, .closed⟩ α)
+    (h : a ∈ r.toList) :
+    a ∈ r := by
+  refine ⟨?_, ?_⟩
+  · sorry -- a is an indirect output
+    -- hence, a has been obtained from a chain of `succ?`
+    -- hence, a is large enough
+  · sorry -- a is an indirect output, hence small enough
+
+-- @[simp] theorem forIn'_eq_forIn'_toList [Succ? α] [LE α] [DecidableLE α]
+--     [LawfulLESucc? α] [Monad m]
+--     (r : PRange ⟨.closed, .closed⟩ α)
+--     (init : β) (f : (a : α) → a ∈ r → β → m (ForInStep β)) :
+--     forIn' r init f =
+--       forIn' r.toList init (fun a h => f a sorry) := by
+--   conv => lhs; simp only [forIn', Range.forIn']
+--   simp only [size]
+--   rw [forIn'_loop_eq_forIn'_range']
+
+-- private theorem size_eq (r : Std.Range) (h : i < r.stop) :
+--     (r.stop - i + r.step - 1) / r.step =
+--       (r.stop - (i + r.step) + r.step - 1) / r.step + 1 := by
+--   have w := r.step_pos
+--   if i + r.step < r.stop then -- Not sure this case split is strictly necessary.
+--     rw [Nat.div_eq_iff w, Nat.add_one_mul]
+--     have : (r.stop - (i + r.step) + r.step - 1) / r.step * r.step ≤
+--         (r.stop - (i + r.step) + r.step - 1) := Nat.div_mul_le_self _ _
+--     have : r.stop - (i + r.step) + r.step - 1 - r.step <
+--         (r.stop - (i + r.step) + r.step - 1) / r.step * r.step :=
+--       Nat.lt_div_mul_self w (by omega)
+--     omega
+--   else
+--     have : (r.stop - i + r.step - 1) / r.step = 1 := by
+--       rw [Nat.div_eq_iff w, Nat.one_mul]
+--       omega
+--     have : (r.stop - (i + r.step) + r.step - 1) / r.step = 0 := by
+--       rw [Nat.div_eq_iff] <;> omega
+--     omega
+
+-- private theorem forIn'_loop_eq_forIn'_range' [Monad m] (r : Std.Range)
+--     (init : β) (f : (a : Nat) → a ∈ r → β → m (ForInStep β)) (i) (w₁) (w₂) :
+--     forIn'.loop r f init i w₁ w₂ =
+--       forIn' (List.range' i ((r.stop - i + r.step - 1) / r.step) r.step) init
+--         fun a h => f a (mem_of_mem_range'_aux w₁ w₂ h) := by
+--   have w := r.step_pos
+--   rw [forIn'.loop]
+--   split <;> rename_i h
+--   · simp only [size_eq r h, List.range'_succ, List.forIn'_cons]
+--     congr 1
+--     funext step
+--     split
+--     · simp
+--     · rw [forIn'_loop_eq_forIn'_range']
+--   · have : (r.stop - i + r.step - 1) / r.step = 0 := by
+--       rw [Nat.div_eq_iff] <;> omega
+--     simp [this]
+
+-- @[simp] theorem forIn'_eq_forIn'_range' [Monad m] (r : Std.Range)
+--     (init : β) (f : (a : Nat) → a ∈ r → β → m (ForInStep β)) :
+--     forIn' r init f =
+--       forIn' (List.range' r.start r.size r.step) init (fun a h => f a (mem_of_mem_range' h)) := by
+--   conv => lhs; simp only [forIn', Range.forIn']
+--   simp only [size]
+--   rw [forIn'_loop_eq_forIn'_range']
+
+-- @[simp] theorem forIn_eq_forIn_range' [Monad m] (r : Std.Range)
+--     (init : β) (f : Nat → β → m (ForInStep β)) :
+--     forIn r init f = forIn (List.range' r.start r.size r.step) init f := by
+--   simp only [forIn, forIn'_eq_forIn'_range']
+
+-- private theorem forM_loop_eq_forM_range' [Monad m] (r : Std.Range) (f : Nat → m PUnit) :
+--     forM.loop r f i = forM (List.range' i ((r.stop - i + r.step - 1) / r.step) r.step) f := by
+--   have w := r.step_pos
+--   rw [forM.loop]
+--   split <;> rename_i h
+--   · simp [size_eq r h, List.range'_succ, List.forM_cons]
+--     congr 1
+--     funext
+--     rw [forM_loop_eq_forM_range']
+--   · have : (r.stop - i + r.step - 1) / r.step = 0 := by
+--       rw [Nat.div_eq_iff] <;> omega
+--     simp [this]
+
+-- @[simp] theorem forM_eq_forM_range' [Monad m] (r : Std.Range) (f : Nat → m PUnit) :
+--     forM r f = forM (List.range' r.start r.size r.step) f := by
+--   simp only [forM, Range.forM, forM_loop_eq_forM_range', size]
+
+-- end Std.Range

src/Init/Data/Range/New/Nat.lean

@@ -0,0 +1,55 @@
+module
+
+prelude
+import all Init.Data.Range.New.Basic
+
+open Std.Iterators
+
+-- instance : Succ? Nat where
+--   succ? n := some (n + 1)
+--   succAtIdx? k n := some (n + k)
+
+-- instance : LawfulLESucc? Nat where
+--   le_rfl := Nat.le_refl _
+--   le_succ? := sorry
+--   le_succ?_of_le hle h := by
+--     simp only [Succ?.succ?, Option.some.injEq] at h
+--     sorry
+--   le_succAtIdx?_of_le {a b c n} hle h := by
+--     simp only [Succ?.succAtIdx?, Option.some.injEq] at h
+--     sorry
+--     -- simp only [Succ?.succAtIdx?, Option.bind_eq_bind] at h
+--     -- induction n generalizing b c with
+--     -- | zero => simp_all [Nat.repeat]
+--     -- | succ n ih =>
+--     --   simp only [Nat.repeat, Option.bind_eq_some_iff] at h ih
+--     --   rcases h with ⟨c', hc', h⟩
+--     --   cases h
+--     --   specialize ih hle hc'
+--     --   omega
+
+-- instance (stepSize : Nat) (h) :
+--     Finite (Range.SuccIterator (α := Nat) stepSize (· ≤ n) h) Id := by
+--   unfold Range.SuccIterator
+--   sorry
+
+-- instance (stepSize : Nat) (h) :
+--     Finite (Range.SuccIterator (α := Nat) stepSize (· < n) h) Id := by
+--   unfold Range.SuccIterator
+--   sorry
+
+-- instance (stepSize : Nat) (h) :
+--     IteratorSize (Range.SuccIterator (α := Nat) stepSize (· ≤ n) h) Id where
+--   size it := pure <| .up <| (n + stepSize - it.internalState.next) / stepSize
+
+-- instance (stepSize : Nat) (h) :
+--     IteratorSizePartial (Range.SuccIterator (α := Nat) stepSize (· ≤ n) h) Id where
+--   size it := pure <| .up <| (n + stepSize - it.internalState.next) / stepSize
+
+-- instance (stepSize : Nat) (h) :
+--     IteratorSize (Range.SuccIterator (α := Nat) stepSize (· < n) h) Id where
+--   size it := pure <| .up <| (n + stepSize - it.internalState.next - 1) / stepSize
+
+-- instance (stepSize : Nat) (h) :
+--     IteratorSizePartial (Range.SuccIterator (α := Nat) stepSize (· < n) h) Id where
+--   size it := pure <| .up <| (n + stepSize - it.internalState.next - 1) / stepSize

src/Init/Data/Range/New/RangeIterator.lean

@@ -0,0 +1,94 @@
+module
+
+prelude
+import Init.Data.Iterators.Internal.Termination
+import Init.Data.Iterators.Consumers.Loop
+import Init.Data.Iterators.Consumers.Collect
+import Init.Data.Range.Classes
+
+open Std.Iterators
+
+namespace Std.Iterators.Types
+
+@[unbox]
+structure RangeIterator (α : Type u) (instSucc? : Succ? α) (P : α → Bool) where
+  next : Option α
+
+variable {α : Type u} {instSucc? : Succ? α} {P : α → Bool}
+
+@[always_inline, inline]
+def RangeIterator.step (it : IterM (α := RangeIterator α instSucc? P) Id α) :
+    IterStep (IterM (α := RangeIterator α instSucc? P) Id α) α :=
+  match it.internalState.next with
+  | none => .done
+  | some a => if P a then .yield ⟨⟨instSucc?.succ? a⟩⟩ a else .done
+
+@[always_inline, inline]
+instance : Iterator (RangeIterator α instSucc? P) Id α where
+  IsPlausibleStep it step := step = RangeIterator.step it
+  step it := pure ⟨RangeIterator.step it, rfl⟩
+
+@[always_inline, inline]
+instance RepeatIterator.instIteratorLoop {n : Type u → Type w} [Monad n] :
+    IteratorLoop (RangeIterator α instSucc? P) Id n :=
+  .defaultImplementation
+  -- forIn lift γ plausible_forInStep wf it init f :=
+  --   let rec @[specialize] loop (a : α) (c : γ) : n γ := do
+  --     if P a then
+  --       match ← f a sorry c with
+  --       | ⟨.yield c', _⟩ => match (instSucc? a) with
+  --         | none => pure c'
+  --         | some a' => loop a' c'
+  --       | ⟨.done c', _⟩ => pure c'
+  --     else
+  --       return init
+  --   termination_by a
+  --   decreasing_by all_goals sorry
+  --   match it.internalState.next with
+  --   | none => pure init
+  --   | some a => loop a init
+
+instance RepeatIterator.instIteratorLoopPartial {n : Type u → Type w}
+    [Monad n] : IteratorLoopPartial (RangeIterator α instSucc? P) Id n :=
+  .defaultImplementation
+
+instance RepeatIterator.instIteratorCollect {n : Type u → Type w}
+    [Monad n] : IteratorCollect (RangeIterator α instSucc? P) Id n :=
+  .defaultImplementation
+
+instance RepeatIterator.instIteratorCollectPartial {n : Type u → Type w}
+    [Monad n] : IteratorCollectPartial (RangeIterator α instSucc? P) Id n :=
+  .defaultImplementation
+
+instance RepeatIterator.instFinite : Finite (RangeIterator α instSucc? P) Id := sorry
+
+abbrev test : ForIn Id (Iter (α := RangeIterator α instSucc? p) α) α :=
+  inferInstance
+
+@[always_inline, inline]
+def test' : ForIn Id.{u} (Iter (α := RangeIterator α instSucc? P) α) α where
+  forIn {γ _} it init f :=
+    let rec @[specialize] loop (a : α) (c : γ) : Id γ := do
+      if P a then
+        match ← f a c with
+        | .yield c' => match instSucc?.succ? a with
+          | none => pure c'
+          | some a' => loop a' c'
+        | .done c' => pure c'
+      else
+        pure c
+    termination_by a
+    decreasing_by all_goals sorry
+    match it.internalState.next with
+    | none => pure init
+    | some a => loop a init
+
+@[csimp]
+theorem aaa : @test = @test' := sorry
+
+@[always_inline, inline]
+instance test'' :
+    ForIn Id.{u} (Iter (α := RangeIterator α instSucc? p) α) α :=
+  test
+
+end Std.Iterators.Types

src/Init/Data/Vector/Basic.lean

@@ -11,9 +11,11 @@ import Init.Data.Array.Lemmas
 import Init.Data.Array.MapIdx
 import Init.Data.Array.InsertIdx
 import Init.Data.Array.Range
-import Init.Data.Range
+import Init.Data.Range.New.Nat
 import Init.Data.Stream
 
+import Init.GetElem
+
 /-!
 # Vectors
 
@@ -557,7 +559,7 @@ Lexicographic comparator for vectors.
 - there is an index `i` such that `lt v[i] w[i]`, and for all `j < i`, `v[j] == w[j]`.
 -/
 def lex [BEq α] (xs ys : Vector α n) (lt : α → α → Bool := by exact (· < ·)) : Bool := Id.run do
-  for h : i in [0 : n] do
+  for h : i in 0,,<n do
     if lt xs[i] ys[i] then
       return true
     else if xs[i] != ys[i] then

src/Std/Data.lean

@@ -25,3 +25,4 @@ import Std.Data.TreeMap.Raw
 import Std.Data.TreeSet.Raw
 
 import Std.Data.Iterators
+import Std.Data.Ranges

src/Std/Data/Iterators.lean

@@ -4,13 +4,13 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Paul Reichert
 -/
 prelude
-import Std.Data.Iterators.Basic
+import Init.Data.Iterators.Basic
+import Init.Data.Iterators.Consumers
+import Init.Data.Iterators.PostconditionMonad
+import Init.Data.Iterators.Internal
 import Std.Data.Iterators.Producers
-import Std.Data.Iterators.Consumers
 import Std.Data.Iterators.Combinators
 import Std.Data.Iterators.Lemmas
-import Std.Data.Iterators.PostConditionMonad
-import Std.Data.Iterators.Internal
 
 /-!
 # Iterators

src/Std/Data/Iterators/Combinators/Monadic/Drop.lean

@@ -4,10 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Paul Reichert
 -/
 prelude
-import Std.Data.Iterators.Basic
-import Std.Data.Iterators.Consumers.Collect
-import Std.Data.Iterators.Consumers.Loop
-import Std.Data.Iterators.Internal.Termination
+import Init.Data.Iterators.Basic
+import Init.Data.Iterators.Consumers.Collect
+import Init.Data.Iterators.Consumers.Loop
+import Init.Data.Iterators.Internal.Termination
 
 /-!
 This file provides the iterator combinator `IterM.drop`.

src/Std/Data/Iterators/Combinators/Monadic/DropWhile.lean

@@ -6,11 +6,11 @@ Authors: Paul Reichert
 prelude
 import Init.Data.Nat.Lemmas
 import Init.RCases
-import Std.Data.Iterators.Basic
-import Std.Data.Iterators.Consumers.Monadic.Collect
-import Std.Data.Iterators.Consumers.Monadic.Loop
-import Std.Data.Iterators.Internal.Termination
-import Std.Data.Iterators.PostConditionMonad
+import Init.Data.Iterators.Basic
+import Init.Data.Iterators.Consumers.Monadic.Collect
+import Init.Data.Iterators.Consumers.Monadic.Loop
+import Init.Data.Iterators.Internal.Termination
+import Init.Data.Iterators.PostconditionMonad
 
 /-!
 # Monadic `dropWhile` iterator combinator
@@ -278,7 +278,7 @@ instance DropWhile.instIteratorCollectPartial [Monad m] [Monad n] [Iterator α m
   .defaultImplementation
 
 instance DropWhile.instIteratorLoop [Monad m] [Monad n] [Iterator α m β] :
-    IteratorLoop α m n :=
+    IteratorLoop (DropWhile α m β P) m n :=
   .defaultImplementation
 
 instance DropWhile.instIteratorForPartial [Monad m] [Monad n] [Iterator α m β]

src/Std/Data/Iterators/Combinators/Monadic/FilterMap.lean

@@ -4,11 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Paul Reichert
 -/
 prelude
-import Std.Data.Iterators.Basic
-import Std.Data.Iterators.Consumers.Collect
-import Std.Data.Iterators.Consumers.Loop
-import Std.Data.Iterators.PostConditionMonad
-import Std.Data.Iterators.Internal.Termination
+import Init.Data.Iterators.Basic
+import Init.Data.Iterators.Consumers.Collect
+import Init.Data.Iterators.Consumers.Loop
+import Init.Data.Iterators.PostconditionMonad
+import Init.Data.Iterators.Internal.Termination
 
 /-!
 

src/Std/Data/Iterators/Combinators/Monadic/Lineage.lean

@@ -0,0 +1,111 @@
+prelude
+import Init.RCases
+import Init.Data.Iterators.Basic
+import Std.Data.Iterators.Producers.Monadic.List
+
+/-!
+This file provides a way to restrict the type of an iterator to the iterator itself and its
+plausible successors. The resulting type is called the iterator's lineage iterator type.
+
+The main application of this type is that if the original iterator is finite (in a suitable sense),
+then its lineage iterator type can be proved to have a `Finite` instance, enabling well-founded
+recursion.
+-/
+
+namespace Std.Iterators
+
+structure Lineage {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β]
+    (it : IterM (α := α) m β) where
+  inner : IterM (α := α) m β
+  is_transitive_successor : IterM.IsInLineageOf inner it
+
+instance [Iterator α m β] [Monad m] (it : IterM (α := α) m β) :
+    Iterator (Lineage it) m β where
+  IsPlausibleStep it' step := it'.internalState.inner.IsPlausibleStep (step.mapIterator (·.internalState.inner))
+  step it' := by
+    refine (fun step => ⟨step.1.pmapIterator (fun it'' h => ⟨it'', ?_⟩), ?_⟩) <$> it'.internalState.inner.step
+    · rcases step with ⟨step, hs⟩
+      cases step <;> simp [hs]
+    · refine IterM.IsInLineageOf.trans (it' := ?_) ?fst ?snd
+      case snd => exact it'.internalState.is_transitive_successor
+      case fst =>
+      · apply IterM.IsInLineageOf.single
+        exact ⟨step.1, h, step.2⟩
+
+instance Lineage.instFiniteOfFinite [Iterator α m β] [h : Finite α m] [Monad m] (it : IterM (α := α) m β) :
+    Finite (Lineage it) m := sorry
+
+def IterM.IsFinite [Iterator α m β] [Monad m] (it : IterM (α := α) m β) :=
+  Finite (Lineage it) m
+
+def FiniteIterator [Iterator α m β] [Monad m] (it : IterM (α := α) m β)
+    (_ : it.IsFinite) :=
+  Lineage it
+
+instance [Iterator α m β] [Monad m] (it : IterM (α := α) m β) (h : it.IsFinite) :
+    Iterator (FiniteIterator it h) m β :=
+  inferInstanceAs <| Iterator (Lineage it) m β
+
+instance [Iterator α m β] [Monad m] (it : IterM (α := α) m β) (h : it.IsFinite) :
+    Finite (FiniteIterator it h) m :=
+  h
+
+@[always_inline, inline]
+def IterM.Advanced.lineage [Iterator α m β] (it : IterM (α := α) m β) :
+    IterM (α := Lineage it) m β :=
+  ⟨it, .rfl⟩
+
+/--
+`finite_iterator_tactic_trivial` is an extensible tactic automatically called
+by the notation `arr[i]` to prove any side conditions that arise when
+constructing the term (e.g. the index is in bounds of the array).
+The default behavior is to just try `trivial` (which handles the case
+where `i < arr.size` is in the context) and `simp +arith` and `omega`
+(for doing linear arithmetic in the index).
+-/
+syntax "finite_iterator_tactic_trivial" : tactic
+
+macro_rules | `(tactic| finite_iterator_tactic_trivial) => `(tactic| exact inferInstanceAs (Finite _ _))
+-- macro_rules | `(tactic| finite_iterator_tactic_trivial) => `(tactic| simp +arith; done)
+-- macro_rules | `(tactic| finite_iterator_tactic_trivial) => `(tactic| trivial)
+
+/--
+`finite_iterator_tactic` is the tactic automatically called by the notation `arr[i]`
+to prove any side conditions that arise when constructing the term
+(e.g. the index is in bounds of the array). It just delegates to
+`finite_iterator_tactic_trivial` and gives a diagnostic error message otherwise;
+users are encouraged to extend `finite_iterator_tactic_trivial` instead of this tactic.
+-/
+macro "finite_iterator_tactic" : tactic =>
+  `(tactic| first
+      /-
+      Recall that `macro_rules` (namely, for `finite_iterator_tactic_trivial`) are tried in reverse order.
+      We first, however, try `done`, since the necessary proof may already have been
+      found during unification, in which case there is no goal to solve (see #6999).
+      If a goal is present, we want `assumption` to be tried first.
+      This is important for theorems such as
+      ```
+      [simp] theorem getElem_pop (a : Array α) (i : Nat) (hi : i < a.pop.size) :
+      a.pop[i] = a[i]'(Nat.lt_of_lt_of_le (a.size_pop ▸ hi) (Nat.sub_le _ _)) :=
+      ```
+      There is a proof embedded in the right-hand-side, and we want it to be just `hi`.
+      If `omega` is used to "fill" this proof, we will have a more complex proof term that
+      cannot be inferred by unification.
+      We hardcoded `assumption` here to ensure users cannot accidentally break this IF
+      they add new `macro_rules` for `finite_iterator_tactic_trivial`.
+      -/
+    | done
+    | assumption
+    | finite_iterator_tactic_trivial
+    | fail "failed to prove that the iterator is finite, possible solutions:
+  - Use `have`-expressions to prove that the iterator is finite
+  - Instead of `it.toList`, try `it.allowNontermination.toList`, which is partial and does not require a termination proof
+  - Extend `finite_iterator_tactic_trivial` using `macro_rules`"
+   )
+
+@[always_inline, inline]
+def IterM.showFinite [Iterator α m β] [Monad m] (it : IterM (α := α) m β) (h : it.IsFinite := by finite_iterator_tactic) :
+    IterM (α := FiniteIterator it h) m β :=
+  IterM.Advanced.lineage it
+
+end Std.Iterators

src/Std/Data/Iterators/Combinators/Monadic/Take.lean

@@ -6,10 +6,10 @@ Authors: Paul Reichert
 prelude
 import Init.Data.Nat.Lemmas
 import Init.RCases
-import Std.Data.Iterators.Basic
-import Std.Data.Iterators.Consumers.Monadic.Collect
-import Std.Data.Iterators.Consumers.Monadic.Loop
-import Std.Data.Iterators.Internal.Termination
+import Init.Data.Iterators.Basic
+import Init.Data.Iterators.Consumers.Monadic.Collect
+import Init.Data.Iterators.Consumers.Monadic.Loop
+import Init.Data.Iterators.Internal.Termination
 
 /-!
 This module provides the iterator combinator `IterM.take`.
@@ -145,13 +145,7 @@ instance Take.instIteratorLoop [Monad m] [Monad n] [Iterator α m β]
 
 instance Take.instIteratorForPartial [Monad m] [Monad n] [Iterator α m β]
     [IteratorLoopPartial α m n] [MonadLiftT m n] :
-    IteratorLoopPartial (Take α m β) m n where
-  forInPartial lift {γ} it init f := do
-    Prod.fst <$> IteratorLoopPartial.forInPartial lift it.internalState.inner (γ := γ × Nat)
-        (init, it.internalState.remaining)
-        fun out acc =>
-          match acc.snd with
-          | 0 => pure <| .done acc
-          | n + 1 => (fun | .yield x => .yield ⟨x, n⟩ | .done x => .done ⟨x, n⟩) <$> f out acc.fst
+    IteratorLoopPartial (Take α m β) m n :=
+  .defaultImplementation
 
 end Std.Iterators

src/Std/Data/Iterators/Combinators/Monadic/TakeWhile.lean

@@ -6,11 +6,11 @@ Authors: Paul Reichert
 prelude
 import Init.Data.Nat.Lemmas
 import Init.RCases
-import Std.Data.Iterators.Basic
-import Std.Data.Iterators.Consumers.Monadic.Collect
-import Std.Data.Iterators.Consumers.Monadic.Loop
-import Std.Data.Iterators.Internal.Termination
-import Std.Data.Iterators.PostConditionMonad
+import Init.Data.Iterators.Basic
+import Init.Data.Iterators.Consumers.Monadic.Collect
+import Init.Data.Iterators.Consumers.Monadic.Loop
+import Init.Data.Iterators.Internal.Termination
+import Init.Data.Iterators.PostconditionMonad
 
 /-!
 # Monadic `takeWhile` iterator combinator
@@ -155,7 +155,7 @@ it terminates.
 -/
 @[always_inline, inline]
 def IterM.takeWhile [Monad m] (P : β → Bool) (it : IterM (α := α) m β) :=
-  (it.takeWhileM (pure ∘ ULift.up ∘ P) : IterM m β)
+  (it.takeWhileWithPostcondition (fun x => PostconditionT.pure (.up <| P x)) : IterM m β)
 
 /--
 `it.PlausibleStep step` is the proposition that `step` is a possible next step from the
@@ -237,16 +237,9 @@ instance TakeWhile.instIteratorLoop [Monad m] [Monad n] [Iterator α m β]
     IteratorLoop (TakeWhile α m β P) m n :=
   .defaultImplementation
 
-instance TakeWhile.instIteratorForPartial [Monad m] [Monad n] [Iterator α m β]
+instance TakeWhile.instIteratorLoopPartial [Monad m] [Monad n] [Iterator α m β]
     [IteratorLoopPartial α m n] [MonadLiftT m n] {P} :
-    IteratorLoopPartial (TakeWhile α m β P) m n where
-  forInPartial lift {γ} it init f := do
-    IteratorLoopPartial.forInPartial lift it.internalState.inner (γ := γ)
-        init
-        fun out acc => do match ← (P out).operation with
-          | ⟨.up true, _⟩ => match ← f out acc with
-            | .yield c => pure (.yield c)
-            | .done c => pure (.done c)
-          | ⟨.up false, _⟩ => pure (.done acc)
+    IteratorLoopPartial (TakeWhile α m β P) m n :=
+  .defaultImplementation
 
 end Std.Iterators

src/Std/Data/Iterators/Combinators/Monadic/Zip.lean

@@ -5,10 +5,10 @@ Authors: Paul Reichert
 -/
 prelude
 import Init.Data.Option.Lemmas
-import Std.Data.Iterators.Basic
-import Std.Data.Iterators.Consumers.Collect
-import Std.Data.Iterators.Consumers.Loop
-import Std.Data.Iterators.Internal.Termination
+import Init.Data.Iterators.Basic
+import Init.Data.Iterators.Consumers.Collect
+import Init.Data.Iterators.Consumers.Loop
+import Init.Data.Iterators.Internal.Termination
 
 /-!
 

src/Std/Data/Iterators/Consumers.lean

@@ -1,11 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Paul Reichert
--/
-prelude
-import Std.Data.Iterators.Consumers.Monadic
-import Std.Data.Iterators.Consumers.Access
-import Std.Data.Iterators.Consumers.Collect
-import Std.Data.Iterators.Consumers.Loop
-import Std.Data.Iterators.Consumers.Partial

src/Std/Data/Iterators/Lemmas.lean

@@ -6,7 +6,7 @@ Authors: Paul Reichert
 prelude
 import Std.Data.Iterators.Lemmas.Basic
 import Std.Data.Iterators.Lemmas.Monadic
-import Std.Data.Iterators.Lemmas.Consumers
+import Init.Data.Iterators.Lemmas.Consumers
 import Std.Data.Iterators.Lemmas.Combinators
 import Std.Data.Iterators.Lemmas.Producers
 import Std.Data.Iterators.Lemmas.Equivalence

src/Std/Data/Iterators/Lemmas/Basic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Paul Reichert
 -/
 prelude
-import Std.Data.Iterators.Basic
+import Init.Data.Iterators.Basic
 
 namespace Std.Iterators
 

src/Std/Data/Iterators/Lemmas/Combinators/Drop.lean

@@ -7,7 +7,7 @@ prelude
 import Std.Data.Iterators.Combinators.Drop
 import Std.Data.Iterators.Lemmas.Combinators.Monadic.Drop
 import Std.Data.Iterators.Lemmas.Combinators.Take
-import Std.Data.Iterators.Lemmas.Consumers
+import Init.Data.Iterators.Lemmas.Consumers
 
 namespace Std.Iterators
 

src/Std/Data/Iterators/Lemmas/Combinators/DropWhile.lean

@@ -6,7 +6,7 @@ Authors: Paul Reichert
 prelude
 import Std.Data.Iterators.Combinators.DropWhile
 import Std.Data.Iterators.Lemmas.Combinators.Monadic.DropWhile
-import Std.Data.Iterators.Lemmas.Consumers
+import Init.Data.Iterators.Lemmas.Consumers
 
 namespace Std.Iterators
 

src/Std/Data/Iterators/Lemmas/Combinators/FilterMap.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Paul Reichert
 -/
 prelude
-import Std.Data.Iterators.Lemmas.Consumers
+import Init.Data.Iterators.Lemmas.Consumers
 import Std.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
 import Std.Data.Iterators.Combinators.FilterMap
 

src/Std/Data/Iterators/Lemmas/Combinators/Monadic/Drop.lean

@@ -5,7 +5,7 @@ Authors: Paul Reichert
 -/
 prelude
 import Std.Data.Iterators.Combinators.Monadic.Drop
-import Std.Data.Iterators.Lemmas.Consumers.Monadic
+import Init.Data.Iterators.Lemmas.Consumers.Monadic
 
 namespace Std.Iterators
 

src/Std/Data/Iterators/Lemmas/Combinators/Monadic/DropWhile.lean

@@ -5,7 +5,7 @@ Authors: Paul Reichert
 -/
 prelude
 import Std.Data.Iterators.Combinators.Monadic.DropWhile
-import Std.Data.Iterators.Lemmas.Consumers.Monadic
+import Init.Data.Iterators.Lemmas.Consumers.Monadic
 
 namespace Std.Iterators
 

src/Std/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.lean

@@ -4,9 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Paul Reichert
 -/
 prelude
-import Std.Data.Internal.LawfulMonadLiftFunction
+import Init.Data.Iterators.Internal.LawfulMonadLiftFunction
 import Std.Data.Iterators.Combinators.Monadic.FilterMap
-import Std.Data.Iterators.Lemmas.Consumers.Monadic
+import Init.Data.Iterators.Lemmas.Consumers.Monadic
 import Std.Data.Iterators.Lemmas.Equivalence.StepCongr
 
 namespace Std.Iterators

src/Std/Data/Iterators/Lemmas/Combinators/Monadic/Take.lean

@@ -5,7 +5,7 @@ Authors: Paul Reichert
 -/
 prelude
 import Std.Data.Iterators.Combinators.Monadic.Take
-import Std.Data.Iterators.Lemmas.Consumers.Monadic
+import Init.Data.Iterators.Lemmas.Consumers.Monadic
 
 namespace Std.Iterators
 

src/Std/Data/Iterators/Lemmas/Combinators/Monadic/TakeWhile.lean

@@ -5,7 +5,7 @@ Authors: Paul Reichert
 -/
 prelude
 import Std.Data.Iterators.Combinators.Monadic.TakeWhile
-import Std.Data.Iterators.Lemmas.Consumers.Monadic
+import Init.Data.Iterators.Lemmas.Consumers.Monadic
 
 namespace Std.Iterators
 
@@ -48,18 +48,35 @@ theorem IterM.step_takeWhile {α m β} [Monad m] [LawfulMonad m] [Iterator α m
     {it : IterM (α := α) m β} {P} :
     (it.takeWhile P).step = (do
       match ← it.step with
-      | .yield it' out h => match P out with
-        | true => pure <| .yield (it'.takeWhile P) out (.yield h True.intro)
-        | false => pure <| .done (.rejected h True.intro)
+      | .yield it' out h => match h' : P out with
+        | true => pure <| .yield (it'.takeWhile P) out (.yield h (congrArg ULift.up h'))
+        | false => pure <| .done (.rejected h (congrArg ULift.up h'))
       | .skip it' h => pure <| .skip (it'.takeWhile P) (.skip h)
       | .done h => pure <| .done (.done h)) := by
-  simp only [takeWhile, step_takeWhileM]
+  simp only [takeWhile, step_takeWhileWithPostcondition]
   apply bind_congr
   intro step
   cases step using PlausibleIterStep.casesOn
   · simp only [Function.comp_apply, PlausibleIterStep.yield, PlausibleIterStep.done, pure_bind]
-    cases P _ <;> rfl
+    simp only [PostconditionT.pure, pure_bind]
+    split <;> split <;> simp_all
   · simp
   · simp
 
+theorem TakeWhile.Monadic.isPlausibleSuccessorOf_inner_of_isPlausibleSuccessorOf {α m β P} [Monad m] [Iterator α m β]
+    {it' it : IterM (α := TakeWhile α m β P) m β} (h : it'.IsPlausibleSuccessorOf it) :
+    it'.internalState.inner.IsPlausibleSuccessorOf it.internalState.inner := by
+  rcases h with ⟨step, h, h'⟩
+  cases step
+  · rename_i out
+    cases h
+    cases h'
+    rename_i it' h' h''
+    exact ⟨.yield it' out, rfl, h'⟩
+  · cases h
+    cases h'
+    rename_i it' h'
+    exact ⟨.skip it', rfl, h'⟩
+  · cases h
+
 end Std.Iterators

src/Std/Data/Iterators/Lemmas/Combinators/Monadic/Zip.lean

@@ -5,7 +5,7 @@ Authors: Paul Reichert
 -/
 prelude
 import Std.Data.Iterators.Combinators.Monadic.Zip
-import Std.Data.Iterators.Lemmas.Consumers.Monadic
+import Init.Data.Iterators.Lemmas.Consumers.Monadic
 
 namespace Std.Iterators
 

src/Std/Data/Iterators/Lemmas/Combinators/Take.lean

@@ -5,9 +5,9 @@ Authors: Paul Reichert
 -/
 prelude
 import Std.Data.Iterators.Combinators.Take
-import Std.Data.Iterators.Consumers.Access
+import Init.Data.Iterators.Consumers.Access
 import Std.Data.Iterators.Lemmas.Combinators.Monadic.Take
-import Std.Data.Iterators.Lemmas.Consumers
+import Init.Data.Iterators.Lemmas.Consumers
 
 namespace Std.Iterators
 

src/Std/Data/Iterators/Lemmas/Combinators/TakeWhile.lean

@@ -6,7 +6,7 @@ Authors: Paul Reichert
 prelude
 import Std.Data.Iterators.Combinators.TakeWhile
 import Std.Data.Iterators.Lemmas.Combinators.Monadic.TakeWhile
-import Std.Data.Iterators.Lemmas.Consumers
+import Init.Data.Iterators.Lemmas.Consumers
 
 namespace Std.Iterators
 
@@ -18,16 +18,16 @@ theorem Iter.takeWhile_eq {α β} [Iterator α Id β] {P}
 theorem Iter.step_takeWhile {α β} [Iterator α Id β] {P}
     {it : Iter (α := α) β} :
     (it.takeWhile P).step = (match it.step with
-      | .yield it' out h => match P out with
-        | true => .yield (it'.takeWhile P) out (.yield h True.intro)
-        | false => .done (.rejected h True.intro)
+      | .yield it' out h => match h' : P out with
+        | true => .yield (it'.takeWhile P) out (.yield h (congrArg _ h'))
+        | false => .done (.rejected h (congrArg _ h'))
       | .skip it' h => .skip (it'.takeWhile P) (.skip h)
       | .done h => .done (.done h)) := by
   simp [Iter.takeWhile_eq, Iter.step, toIterM_toIter, IterM.step_takeWhile]
   generalize it.toIterM.step.run = step
   cases step using PlausibleIterStep.casesOn
   · simp only [IterM.Step.toPure_yield, PlausibleIterStep.yield, toIter_toIterM, toIterM_toIter]
-    cases P _ <;> rfl
+    split <;> split <;> (try exfalso; simp_all; done) <;> simp_all
   · simp
   · simp
 
@@ -43,29 +43,29 @@ theorem Iter.atIdxSlow?_takeWhile {α β}
     simp only [Option.any_some]
     apply Eq.symm
     split
-    · cases h' : P out
-      · exfalso; simp_all
-      · simp
-    · cases h' : P out
+    · -- Ugh, this is so ugly
+      have : (match h' : P out with | true => Unit.unit | false => Unit.unit) = .unit := rfl
+      split at this
       · simp
       · exfalso; simp_all
+    · have : (match h' : P out with | true => Unit.unit | false => Unit.unit) = .unit := rfl
+      split at this
+      · exfalso; simp_all
+      · simp
   case case2 it it' out h h' l ih =>
     simp only [Nat.succ_eq_add_one, atIdxSlow?.eq_def (it := it.takeWhile P), step_takeWhile, h']
     simp only [atIdxSlow?.eq_def (it := it), h']
-    cases hP : P out
-    · simp
-      intro h
-      specialize h 0 (Nat.zero_le _)
-      simp at h
-      exfalso; simp_all
-    · simp [ih]
+    have : (match h' : P out with | true => Unit.unit | false => Unit.unit) = .unit := rfl
+    split at this
+    · rename_i hP
+      simp only [ih]
       split
       · rename_i h
         rw [if_pos]
         intro k hk
         split
         · exact hP
-        · simp at hk
+        · simp only [Nat.succ_eq_add_one, Nat.add_le_add_iff_right] at hk
           exact h _ hk
       · rename_i hl
         rw [if_neg]
@@ -73,6 +73,11 @@ theorem Iter.atIdxSlow?_takeWhile {α β}
         apply hl
         intro k hk
         exact hl' (k + 1) (Nat.succ_le_succ hk)
+    · simp only [right_eq_ite_iff]
+      intro h
+      specialize h 0 (Nat.zero_le _)
+      simp only at h
+      exfalso; simp_all
   case case3 l it it' h h' ih =>
     simp only [atIdxSlow?.eq_def (it := it.takeWhile P), step_takeWhile, h', ih]
     simp only [atIdxSlow?.eq_def (it := it), h']
@@ -131,4 +136,10 @@ theorem Iter.toArray_takeWhile_of_finite {α β} [Iterator α Id β] {P}
     (it.takeWhile P).toArray = it.toArray.takeWhile P := by
   rw [← toArray_toList, ← toArray_toList, List.takeWhile_toArray, toList_takeWhile_of_finite]
 
+theorem TakeWhile.isPlausibleSuccessorOf_inner_of_isPlausibleSuccessorOf {α β P}
+    [Iterator α Id β]
+    {it' it : Iter (α := TakeWhile α Id β P) β} (h : it'.IsPlausibleSuccessorOf it) :
+    it'.internalState.inner.IsPlausibleSuccessorOf it.internalState.inner :=
+  TakeWhile.Monadic.isPlausibleSuccessorOf_inner_of_isPlausibleSuccessorOf h
+
 end Std.Iterators

src/Std/Data/Iterators/Lemmas/Combinators/Zip.lean

@@ -6,10 +6,10 @@ Authors: Paul Reichert
 prelude
 import Std.Data.Iterators.Combinators.Take
 import Std.Data.Iterators.Combinators.Zip
-import Std.Data.Iterators.Consumers.Access
+import Init.Data.Iterators.Consumers.Access
 import Std.Data.Iterators.Lemmas.Combinators.Monadic.Zip
 import Std.Data.Iterators.Lemmas.Combinators.Take
-import Std.Data.Iterators.Lemmas.Consumers
+import Init.Data.Iterators.Lemmas.Consumers
 
 namespace Std.Iterators
 

src/Std/Data/Iterators/Lemmas/Consumers.lean

@@ -4,6 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Paul Reichert
 -/
 prelude
-import Std.Data.Iterators.Lemmas.Consumers.Monadic
-import Std.Data.Iterators.Lemmas.Consumers.Collect
-import Std.Data.Iterators.Lemmas.Consumers.Loop
+import Init.Data.Iterators.Lemmas.Consumers.Monadic
+import Init.Data.Iterators.Lemmas.Consumers.Collect
+import Init.Data.Iterators.Lemmas.Consumers.Loop

src/Std/Data/Iterators/Lemmas/Equivalence/Basic.lean

@@ -8,8 +8,8 @@ import Init.Control.Lawful.Basic
 import Init.Ext
 import Init.Internal.Order
 import Init.Core
-import Std.Data.Iterators.Basic
-import Std.Data.Iterators.PostConditionMonad
+import Init.Data.Iterators.Basic
+import Init.Data.Iterators.PostconditionMonad
 import Std.Data.Iterators.Lemmas.Equivalence.HetT
 
 namespace Std.Iterators

src/Std/Data/Iterators/Lemmas/Equivalence/HetT.lean

@@ -8,8 +8,8 @@ import Init.Control.Lawful.Basic
 import Init.Data.Subtype
 import Init.PropLemmas
 import Init.Classical
-import Std.Data.Internal.LawfulMonadLiftFunction
-import Std.Data.Iterators.PostConditionMonad
+import Init.Data.Iterators.Internal.LawfulMonadLiftFunction
+import Init.Data.Iterators.PostconditionMonad
 
 namespace Std.Internal
 

src/Std/Data/Iterators/Lemmas/Monadic/Basic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Paul Reichert
 -/
 prelude
-import Std.Data.Iterators.Basic
+import Init.Data.Iterators.Basic
 
 namespace Std.Iterators
 

src/Std/Data/Iterators/Lemmas/Producers/Array.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Paul Reichert
 -/
 prelude
-import Std.Data.Iterators.Lemmas.Consumers.Collect
+import Init.Data.Iterators.Lemmas.Consumers.Collect
 import Std.Data.Iterators.Lemmas.Producers.Monadic.Array
 
 /-!

src/Std/Data/Iterators/Lemmas/Producers/Empty.lean

@@ -5,7 +5,7 @@ Authors: Paul Reichert
 -/
 prelude
 import Std.Data.Iterators.Lemmas.Producers.Monadic.Empty
-import Std.Data.Iterators.Lemmas.Consumers
+import Init.Data.Iterators.Lemmas.Consumers
 import Std.Data.Iterators.Producers.Empty
 
 namespace Std.Iterators

src/Std/Data/Iterators/Lemmas/Producers/List.lean

@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Paul Reichert
 -/
 prelude
-import Std.Data.Iterators.Consumers
-import Std.Data.Iterators.Lemmas.Consumers.Collect
+import Init.Data.Iterators.Consumers
+import Init.Data.Iterators.Lemmas.Consumers.Collect
 import Std.Data.Iterators.Lemmas.Producers.Monadic.List
 
 /-!

src/Std/Data/Iterators/Lemmas/Producers/Monadic/Array.lean

@@ -4,10 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Paul Reichert
 -/
 prelude
-import Std.Data.Internal.LawfulMonadLiftFunction
+import Init.Data.Iterators.Internal.LawfulMonadLiftFunction
 import Std.Data.Iterators.Producers.Monadic.Array
-import Std.Data.Iterators.Consumers
-import Std.Data.Iterators.Lemmas.Consumers.Monadic
+import Init.Data.Iterators.Consumers
+import Init.Data.Iterators.Lemmas.Consumers.Monadic
 import Std.Data.Iterators.Lemmas.Producers.Monadic.List
 import Std.Data.Iterators.Lemmas.Equivalence.Basic
 

src/Std/Data/Iterators/Lemmas/Producers/Monadic/Empty.lean

@@ -5,8 +5,8 @@ Authors: Paul Reichert
 -/
 prelude
 import Std.Data.Iterators.Producers.Monadic.Empty
-import Std.Data.Iterators.Lemmas.Consumers.Monadic
-import Std.Data.Iterators.Lemmas.Consumers.Monadic.Loop
+import Init.Data.Iterators.Lemmas.Consumers.Monadic
+import Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
 
 namespace Std.Iterators
 

src/Std/Data/Iterators/Lemmas/Producers/Monadic/List.lean

@@ -5,9 +5,9 @@ Authors: Paul Reichert
 -/
 prelude
 import Std.Data.Iterators.Producers.Monadic.List
-import Std.Data.Iterators.Consumers
-import Std.Data.Iterators.Lemmas.Consumers.Monadic
-import Std.Data.Internal.LawfulMonadLiftFunction
+import Init.Data.Iterators.Consumers
+import Init.Data.Iterators.Lemmas.Consumers.Monadic
+import Init.Data.Iterators.Internal.LawfulMonadLiftFunction
 
 /-!
 # Lemmas about list iterators

src/Std/Data/Iterators/Lemmas/Producers/Repeat.lean

@@ -6,8 +6,8 @@ Authors: Paul Reichert
 prelude
 import Init.Data.Option.Lemmas
 import Std.Data.Iterators.Producers.Repeat
-import Std.Data.Iterators.Consumers.Access
-import Std.Data.Iterators.Consumers.Collect
+import Init.Data.Iterators.Consumers.Access
+import Init.Data.Iterators.Consumers.Collect
 import Std.Data.Iterators.Combinators.Take
 import Std.Data.Iterators.Lemmas.Combinators.Take
 
@@ -16,7 +16,7 @@ namespace Std.Iterators
 variable {α : Type w} {f : α → α} {init : α}
 
 theorem Iter.step_repeat :
-    (Iter.repeat f init).step = .yield (Iter.repeat f (f init)) init ⟨rfl, rfl⟩ := by
+    (Iter.repeat f init).step = .yield (Iter.repeat f (f init)) init ⟨rfl, f init, rfl, rfl⟩ := by
   rfl
 
 theorem Iter.atIdxSlow?_zero_repeat :
@@ -52,4 +52,20 @@ theorem Iter.toList_take_repeat_succ {k : Nat} :
     ((Iter.repeat f init).take (k + 1)).toList = init :: ((Iter.repeat f (f init)).take k).toList := by
   rw [toList_eq_match_step, step_take, step_repeat]
 
+theorem RepeatIterator.Monadic.next_eq_some_of_isPlausibleSuccessorOf {f : α → Option α}
+    {it' it : IterM (α := RepeatIterator α f) Id α} (h : it'.IsPlausibleSuccessorOf it) :
+    f it.internalState.next = some it'.internalState.next := by
+  rcases h with ⟨step, h, h'⟩
+  cases step
+  · cases h
+    rcases h' with ⟨rfl, a, ha, h'⟩
+    simp_all [Iter.toIterM]
+  · cases h'
+  · cases h
+
+theorem RepeatIterator.next_eq_some_of_isPlausibleSuccessorOf {f : α → Option α}
+    {it' it : Iter (α := RepeatIterator α f) α} (h : it'.IsPlausibleSuccessorOf it) :
+    f it.internalState.next = some it'.internalState.next :=
+  RepeatIterator.Monadic.next_eq_some_of_isPlausibleSuccessorOf h
+
 end Std.Iterators

src/Std/Data/Iterators/Producers/Monadic/Array.lean

@@ -6,8 +6,8 @@ Authors: Paul Reichert
 prelude
 import Init.Data.Nat.Lemmas
 import Init.RCases
-import Std.Data.Iterators.Consumers
-import Std.Data.Iterators.Internal.Termination
+import Init.Data.Iterators.Consumers
+import Init.Data.Iterators.Internal.Termination
 
 /-!
 # Array iterator

src/Std/Data/Iterators/Producers/Monadic/Empty.lean

@@ -4,9 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Paul Reichert
 -/
 prelude
-import Std.Data.Iterators.Consumers.Collect
-import Std.Data.Iterators.Consumers.Loop
-import Std.Data.Iterators.Internal.Termination
+import Init.Data.Iterators.Consumers.Collect
+import Init.Data.Iterators.Consumers.Loop
+import Init.Data.Iterators.Internal.Termination
 
 /-!
 This file provides an empty iterator.

src/Std/Data/Iterators/Producers/Monadic/List.lean

@@ -6,8 +6,8 @@ Authors: Paul Reichert
 prelude
 import Init.Data.Nat.Lemmas
 import Init.RCases
-import Std.Data.Iterators.Consumers
-import Std.Data.Iterators.Internal.Termination
+import Init.Data.Iterators.Consumers
+import Init.Data.Iterators.Internal.Termination
 
 /-!
 # List iterator

src/Std/Data/Iterators/Producers/Repeat.lean

@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Paul Reichert
 -/
 prelude
-import Std.Data.Iterators.Consumers.Monadic
-import Std.Data.Iterators.Internal.Termination
+import Init.Data.Iterators.Consumers.Monadic
+import Init.Data.Iterators.Internal.Termination
 
 /-!
 # Function-unfolding iterator
@@ -18,23 +18,39 @@ namespace Std.Iterators
 
 universe u v
 
-variable {α : Type w} {m : Type w → Type w'} {f : α → α}
+variable {α : Type w} {m : Type w → Type w'} {f : α → Option α}
 
 /--
 Internal state of the `repeat` combinator. Do not depend on its internals.
 -/
 @[unbox]
-structure RepeatIterator (α : Type u) (f : α → α) where
+structure RepeatIterator (α : Type u) (f : α → Option α) where
   /-- Internal implementation detail of the iterator library. -/
   next : α
 
 @[always_inline, inline]
 instance : Iterator (RepeatIterator α f) Id α where
   IsPlausibleStep it
-    | .yield it' out => out = it.internalState.next ∧ it' = ⟨⟨f it.internalState.next⟩⟩
+    | .yield it' out => out = it.internalState.next ∧ ∃ a, f it.internalState.next = some a ∧ it' = ⟨⟨a⟩⟩
     | .skip _ => False
-    | .done => False
-  step it := pure <| .yield ⟨⟨f it.internalState.next⟩⟩ it.internalState.next (by simp)
+    | .done => f it.internalState.next = none
+  step it := match f it.internalState.next with
+    | none => pure <| .done rfl
+    | some a => pure <| .yield ⟨⟨a⟩⟩ it.internalState.next (by simp)
+
+/--
+Creates an iterator from an initial value `init` and a function `f : α → Option α`.
+First it yields `init`, and in each successive step, the iterator applies `f` to the previous value.
+If `f` returns `some a`, the iterator emits `a`, and otherwise terminates.
+
+**Termination properties:**
+
+* `Finite` instance: not available but provable in some cases
+* `Productive` instance: always
+-/
+@[always_inline, inline]
+def Iter.repeatUntilNone {α : Type w} (f : α → Option α) (init : α) :=
+  (⟨RepeatIterator.mk (f := f) init⟩ : Iter α)
 
 /--
 Creates an infinite iterator from an initial value `init` and a function `f : α → α`.
@@ -52,7 +68,7 @@ order.
 -/
 @[always_inline, inline]
 def Iter.repeat {α : Type w} (f : α → α) (init : α) :=
-  (⟨RepeatIterator.mk (f := f) init⟩ : Iter α)
+  Iter.repeatUntilNone (fun a => some (f a)) init
 
 private def RepeatIterator.instProductivenessRelation :
     ProductivenessRelation (RepeatIterator α f) Id where
@@ -64,19 +80,19 @@ instance RepeatIterator.instProductive :
     Productive (RepeatIterator α f) Id :=
   Productive.of_productivenessRelation instProductivenessRelation
 
-instance RepeatIterator.instIteratorLoop {α : Type w} {f : α → α} {n : Type w → Type w'} [Monad n] :
+instance RepeatIterator.instIteratorLoop {α : Type w} {f : α → Option α} {n : Type w → Type w'} [Monad n] :
     IteratorLoop (RepeatIterator α f) Id n :=
   .defaultImplementation
 
-instance RepeatIterator.instIteratorLoopPartial {α : Type w} {f : α → α} {n : Type w → Type w'}
+instance RepeatIterator.instIteratorLoopPartial {α : Type w} {f : α → Option α} {n : Type w → Type w'}
     [Monad n] : IteratorLoopPartial (RepeatIterator α f) Id n :=
   .defaultImplementation
 
-instance RepeatIterator.instIteratorCollect {α : Type w} {f : α → α} {n : Type w → Type w'}
+instance RepeatIterator.instIteratorCollect {α : Type w} {f : α → Option α} {n : Type w → Type w'}
     [Monad n] : IteratorCollect (RepeatIterator α f) Id n :=
   .defaultImplementation
 
-instance RepeatIterator.instIteratorCollectPartial {α : Type w} {f : α → α} {n : Type w → Type w'}
+instance RepeatIterator.instIteratorCollectPartial {α : Type w} {f : α → Option α} {n : Type w → Type w'}
     [Monad n] : IteratorCollectPartial (RepeatIterator α f) Id n :=
   .defaultImplementation
 

src/Std/Data/Ranges.lean

@@ -0,0 +1 @@
+prelude

src/Std/Data/Ranges/Array.lean

@@ -0,0 +1,31 @@
+prelude
+-- import Std.Data.Ranges.Slice
+
+-- instance : Sliceable shape (Array α) Nat α where
+
+-- instance : SliceIter ⟨.none, .none⟩ (Array α) Nat :=
+--   .of (·.collection.iter)
+
+-- instance : SliceIter ⟨.closed, .none⟩ (Array α) Nat :=
+--   .of (fun s => s.collection.iter.drop s.range.lower)
+
+-- instance : SliceIter ⟨.open, .none⟩ (Array α) Nat :=
+--   .of (fun s => s.collection.iter.drop (s.range.lower + 1))
+
+-- instance : SliceIter ⟨.none, .closed⟩ (Array α) Nat :=
+--   .of (fun s => s.collection.iter.take (s.range.upper + 1))
+
+-- instance : SliceIter ⟨.closed, .closed⟩ (Array α) Nat :=
+--   .of (fun s => s.collection.iter.take (s.range.upper + 1) |>.drop s.range.lower)
+
+-- instance : SliceIter ⟨.open, .closed⟩ (Array α) Nat :=
+--   .of (fun s => s.collection.iter.take (s.range.upper + 1) |>.drop (s.range.lower + 1))
+
+-- instance : SliceIter ⟨.none, .open⟩ (Array α) Nat :=
+--   .of (fun s => s.collection.iter.take s.range.upper)
+
+-- instance : SliceIter ⟨.closed, .open⟩ (Array α) Nat :=
+--   .of (fun s => s.collection.iter.take s.range.upper |>.drop s.range.lower)
+
+-- instance : SliceIter ⟨.open, .open⟩ (Array α) Nat :=
+--   .of (fun s => s.collection.iter.take s.range.upper |>.drop (s.range.lower + 1))

src/Std/Data/Ranges/Basic.lean

@@ -0,0 +1,148 @@
+prelude
+-- import Init.Core
+-- import Init.NotationExtra
+-- import Std.Data.Iterators
+-- import Init.System.IO -- just for testing
+
+-- open Std.Iterators
+
+-- inductive BoundShape where
+--   | «open» : BoundShape
+--   | closed : BoundShape
+--   | none : BoundShape
+
+-- structure RangeShape where
+--   lower : BoundShape
+--   upper : BoundShape
+
+-- abbrev Bound (shape : BoundShape) (α : Type u) : Type u :=
+--   match shape with
+--   | .open | .closed => α
+--   | .none => PUnit
+
+-- structure PRange (shape : RangeShape) (α : Type u) where
+--   lower : Bound shape.lower α
+--   upper : Bound shape.upper α
+
+-- syntax:max (term ",," term) : term
+-- syntax:max (",," term) : term
+-- syntax:max (term ",,") : term
+-- syntax:max (",,") : term
+-- syntax:max (term "<,," term) : term
+-- syntax:max (term "<,,") : term
+-- syntax:max (term ",,<" term) : term
+-- syntax:max (",,<" term) : term
+-- syntax:max (term "<,,<" term) : term
+
+-- macro_rules
+--   | `($a,,$b) => ``(PRange.mk (shape := RangeShape.mk BoundShape.closed BoundShape.closed) $a $b)
+--   | `(,,$b) => ``(PRange.mk (shape := RangeShape.mk BoundShape.none BoundShape.closed) PUnit.unit $b)
+--   | `($a,,) => ``(PRange.mk (shape := RangeShape.mk BoundShape.closed BoundShape.none) $a PUnit.unit)
+--   | `(,,) => ``(PRange.mk (shape := RangeShape.mk BoundShape.none BoundShape.none) PUnit.unit PUnit.unit)
+--   | `($a<,,$b) => ``(PRange.mk (shape := RangeShape.mk BoundShape.open BoundShape.closed) $a $b)
+--   | `($a<,,) => ``(PRange.mk (shape := RangeShape.mk BoundShape.open BoundShape.none) $a PUnit.unit)
+--   | `($a,,<$b) => ``(PRange.mk (shape := RangeShape.mk BoundShape.closed BoundShape.open) $a $b)
+--   | `(,,<$b) => ``(PRange.mk (shape := RangeShape.mk BoundShape.none BoundShape.open) PUnit.unit $b)
+--   | `($a<,,<$b) => ``(PRange.mk (shape := RangeShape.mk BoundShape.open BoundShape.open) $a $b)
+
+-- class RangeIter (shape : RangeShape) (α : Type u) where
+--   State : PRange shape α → Type u
+--   iter : (r : PRange shape α) → Iter (α := State r) α
+
+-- @[always_inline, inline]
+-- def RangeIter.of {State : PRange shape α → Type u}
+--     (iter : (r : PRange shape α) → Iter (α := State r) α) :
+--     RangeIter shape α where
+--   State := State
+--   iter := iter
+
+-- instance {State : PRange shape α → Type u}
+--     {r : PRange shape α} [Iterator (State r) Id α]
+--     {iter : (r : PRange shape α) → Iter (α := State r) α} :
+--     letI : RangeIter shape α := RangeIter.of iter
+--     Iterator (RangeIter.State (shape := shape) (α := α) r) Id α :=
+--   inferInstanceAs <| Iterator (State r) Id α
+
+-- instance {State : PRange shape α → Type u} {r : PRange shape α}
+--     [Iterator (State r) Id α]
+--     [Finite (State r) Id]
+--     {iter : (r : PRange shape α) → Iter (α := State r) α} :
+--     letI : RangeIter shape α := RangeIter.of iter
+--     Finite (RangeIter.State (shape := shape) (α := α) r) Id :=
+--   inferInstanceAs <| Finite (State r) Id
+
+-- instance {State : PRange shape α → Type u} {r : PRange shape α}
+--     [Iterator (State r) Id α] [IteratorCollect (State r) Id m]
+--     {iter : (r : PRange shape α) → Iter (α := State r) α} :
+--     letI : RangeIter shape α := RangeIter.of iter
+--     IteratorCollect (RangeIter.State r) Id m :=
+--   inferInstanceAs <| IteratorCollect (State r) Id m
+
+-- instance {State : PRange shape α → Type u} {r : PRange shape α}
+--     [Iterator (State r) Id α] [IteratorCollectPartial (State r) Id m]
+--     {iter : (r : PRange shape α) → Iter (α := State r) α} :
+--     letI : RangeIter shape α := RangeIter.of iter
+--     IteratorCollectPartial (RangeIter.State r) Id m :=
+--   inferInstanceAs <| IteratorCollectPartial (State r) Id m
+
+-- instance {State : PRange shape α → Type u} {r : PRange shape α}
+--     [Iterator (State r) Id α] [IteratorLoop (State r) Id m]
+--     {iter : (r : PRange shape α) → Iter (α := State r) α} :
+--     letI : RangeIter shape α := RangeIter.of iter
+--     IteratorLoop (RangeIter.State r) Id m :=
+--   inferInstanceAs <| IteratorLoop (State r) Id m
+
+-- instance {State : PRange shape α → Type u} {r : PRange shape α}
+--     [Iterator (State r) Id α] [IteratorLoopPartial (State r) Id m]
+--     {iter : (r : PRange shape α) → Iter (α := State r) α} :
+--     letI : RangeIter shape α := RangeIter.of iter
+--     IteratorLoopPartial (RangeIter.State r) Id m :=
+--   inferInstanceAs <| IteratorLoopPartial (State r) Id m
+
+-- @[always_inline, inline]
+-- def PRange.iter [RangeIter shape α] (r : PRange shape α) :=
+--   (RangeIter.iter r : Iter α)
+
+-- @[always_inline, inline]
+-- def PRange.size [RangeIter shape α] (r : PRange shape α)
+--     [Iterator (RangeIter.State r) Id α] [IteratorSize (RangeIter.State r) Id] :
+--     Nat :=
+--   r.iter.size
+
+-- instance [i : RangeIter shape α] [∀ r, ForIn m (Iter (α := i.State r) α) α] :
+--     ForIn m (PRange shape α) α where
+--   forIn r := forIn r.iter
+
+/-!
+
+Ranges don't have a concept of orientation or steps.
+
+They can support:
+
+* size
+* Membership
+* toIter (possibly with an orientation/step size)
+* getElem
+* ForIn (via toIter? How to ensure termination? -> by encoding the bound shapes in the iterator type)
+
+Slices: similar contexts but separate framework for performance reasons?
+
+Actually, slices seem like the more fundamental concept.
+
+Should slices always be allowed, possibly truncating, or not?
+* List/Array: requiring proof seems sensible
+* HashMap/TreeMap: any slices should be possible
+
+# Use cases
+
+`0..10` (`Nat`, `Int`, `Fin`, `ℝ`)
+
+`0..10 (step := 3)`
+
+`0.2..0.6 (step := 0.1)`
+
+`xs[(0..1), (4..5)]` or `xs[(0, 4)..(1, 5)]`
+
+`xs [10..0 (step := -2)]`
+
+-/

src/Std/Data/Ranges/General.lean

@@ -0,0 +1,196 @@
+prelude
+-- import Std.Data.Ranges.Basic
+-- import Std.Data.Ranges.Slice
+-- open Std.Iterators
+
+-- class Succ? (α : Type u) where
+--   succ? : α → Option α
+--   succAtIdx? (n : Nat) (a : α) : Option α := Nat.repeat (· >>= succ?) n (some a)
+
+-- class LawfulLESucc? (α : Type u) [LE α] [Succ? α] where
+--   le_rfl : {a : α} → a ≤ a
+--   le_succ?_of_le : {a b c : α} → a ≤ b → (h : Succ?.succ? b = some c) → a ≤ c
+--   le_succAtIdx?_of_le : {a b c : α} → {n : Nat} → a ≤ b → (h : Succ?.succAtIdx? n b = some c) → a ≤ c
+
+-- class LawfulLTSucc? [LT α] [Succ? α] where
+--   lt_succ? : {a b : α} → (h : Succ?.succ? a = some b) → a < b
+--   lt_succ?_of_lt : {a b c : α} → a < b → (h : Succ?.succ? b = some c) → a < c
+
+-- class HasDownwardUnboundedRanges (α : Type u) where
+--   min : α
+
+-- instance : Membership α (PRange ⟨.none, .none⟩ α) where
+--   mem _ _ := True
+
+-- instance (r : PRange ⟨.none, .none⟩ α) : Decidable (a ∈ r) :=
+--   inferInstanceAs <| Decidable True
+
+-- instance [LT α] : Membership α (PRange ⟨.none, .open⟩ α) where
+--   mem r a := a < r.upper
+
+-- instance [LT α] [DecidableLT α] (r : PRange ⟨.none, .open⟩ α) : Decidable (a ∈ r) :=
+--   inferInstanceAs <| Decidable (a < r.upper)
+
+-- instance [LE α] : Membership α (PRange ⟨.none, .closed⟩ α) where
+--   mem r a := a ≤ r.upper
+
+-- instance [LE α] [DecidableLE α] (r : PRange ⟨.none, .closed⟩ α) : Decidable (a ∈ r) :=
+--   inferInstanceAs <| Decidable (a ≤ r.upper)
+
+-- instance [LT α] : Membership α (PRange ⟨.open, .none⟩ α) where
+--   mem r a := r.lower < a
+
+-- instance [LT α] [DecidableLT α] (r : PRange ⟨.open, .none⟩ α) : Decidable (a ∈ r) :=
+--   inferInstanceAs <| Decidable (r.lower < a)
+
+-- instance [LT α] : Membership α (PRange ⟨.open, .open⟩ α) where
+--   mem r a := r.lower < a ∧ a < r.upper
+
+-- instance [LT α] [DecidableLT α] (r : PRange ⟨.open, .open⟩ α) : Decidable (a ∈ r) :=
+--   inferInstanceAs <| Decidable (r.lower < a ∧ _)
+
+-- instance [LT α] [LE α] : Membership α (PRange ⟨.open, .closed⟩ α) where
+--   mem r a := r.lower < a ∧ a ≤ r.upper
+
+-- instance [LT α] [DecidableLT α] [LE α] [DecidableLE α] (r : PRange ⟨.open, .closed⟩ α) :
+--     Decidable (a ∈ r) :=
+--   inferInstanceAs <| Decidable (_ ∧ _)
+
+-- instance [LE α] : Membership α (PRange ⟨.closed, .none⟩ α) where
+--   mem r a := r.lower ≤ a
+
+-- instance [LE α] [DecidableLE α] (r : PRange ⟨.closed, .none⟩ α) : Decidable (a ∈ r) :=
+--   inferInstanceAs <| Decidable (r.lower ≤ a)
+
+-- instance [LE α] [LT α] : Membership α (PRange ⟨.closed, .open⟩ α) where
+--   mem r a := r.lower ≤ a ∧ a < r.upper
+
+-- instance [LT α] [DecidableLT α] [LE α] [DecidableLE α] (r : PRange ⟨.closed, .open⟩ α) :
+--     Decidable (a ∈ r) :=
+--   inferInstanceAs <| Decidable (_ ∧ _)
+
+-- instance [LE α] : Membership α (PRange ⟨.closed, .closed⟩ α) where
+--   mem r a := r.lower ≤ a ∧ a ≤ r.upper
+
+-- instance [LE α] [DecidableLE α] (r : PRange ⟨.closed, .closed⟩ α) : Decidable (a ∈ r) :=
+--   inferInstanceAs <| Decidable (_ ∧ _)
+
+
+-- section Iterator
+
+-- def Range.succIteratorInternal [Succ? α] (init : α) (stepSize : Nat) (Predicate : α → Bool) :=
+--   Iter.repeatUntilNone (init := init) (Succ?.succAtIdx? stepSize) |>.takeWhile Predicate
+
+-- def Range.SuccIterator [Succ? α] (stepSize : Nat) (Predicate : α → Bool)
+--     (_ : stepSize > 0) :=
+--   type_of% (succIteratorInternal (_ : α) stepSize Predicate).internalState
+
+-- def Range.succIterator [Succ? α] (init : α) (stepSize : Nat) (Predicate : α → Bool) (h) :
+--     (Iter (α := SuccIterator stepSize Predicate h) α) :=
+--   Iter.repeatUntilNone (init := init) (Succ?.succAtIdx? stepSize) |>.takeWhile Predicate
+
+-- @[always_inline, inline]
+-- def Range.SuccIterator.next [Succ? α] (stepSize : Nat) (Predicate : α → Bool)
+--     {h : stepSize > 0} (it : SuccIterator stepSize Predicate h) : α :=
+--   it.inner.internalState.next
+
+-- instance [Succ? α] (stepSize : Nat) (Predicate : α → Bool) (h) :
+--     Iterator (Range.SuccIterator stepSize Predicate h) Id α := by
+--   unfold Range.SuccIterator
+--   infer_instance
+
+-- instance [Monad m] [Succ? α] (stepSize : Nat) (Predicate : α → Bool) (h) :
+--     IteratorCollect (Range.SuccIterator stepSize Predicate h) Id m := by
+--   unfold Range.SuccIterator
+--   infer_instance
+
+-- instance [Monad m] [Succ? α] (stepSize : Nat) (Predicate : α → Bool) (h) :
+--     IteratorCollectPartial (Range.SuccIterator stepSize Predicate h) Id m := by
+--   unfold Range.SuccIterator
+--   infer_instance
+
+-- instance [Monad m] [MonadLiftT Id m] [Succ? α] (stepSize : Nat) (Predicate : α → Bool) (h) :
+--     IteratorLoop (Range.SuccIterator stepSize Predicate h) Id m := by
+--   unfold Range.SuccIterator
+--   infer_instance
+
+-- instance [Monad m] [MonadLiftT Id m] [Succ? α] (stepSize : Nat) (Predicate : α → Bool) (h) :
+--     IteratorLoopPartial (Range.SuccIterator stepSize Predicate h) Id m := by
+--   unfold Range.SuccIterator
+--   infer_instance
+
+-- -- TODO: Should we hide the ≤ or < predicates behind some identifier to avoid accidental rewriting?
+-- instance [Succ? α] [LE α] [DecidableLE α] : RangeIter ⟨.closed, .closed⟩ α :=
+--   .of fun r => Range.succIterator r.lower 1 (fun a => a ≤ r.upper) (by omega)
+
+-- instance [Succ? α] [LT α] [DecidableLT α] : RangeIter ⟨.closed, .open⟩ α :=
+--   .of fun r => Range.succIterator r.lower 1 (fun a => a < r.upper) (by omega)
+
+-- instance [Succ? α] [LT α] [DecidableLT α] : RangeIter ⟨.closed, .none⟩ α :=
+--   .of fun r => Range.succIterator r.lower 1 (fun _ => True) (by omega)
+
+-- instance [Succ? α] [LE α] [DecidableLE α] : RangeIter ⟨.open, .closed⟩ α :=
+--   .of fun r => Range.succIterator r.lower 1 (fun a => a ≤ r.upper) (by omega) |>.drop 1
+
+-- instance [Succ? α] [LT α] [DecidableLT α] : RangeIter ⟨.open, .open⟩ α :=
+--   .of fun r => Range.succIterator r.lower 1 (fun a => a < r.upper) (by omega) |>.drop 1
+
+-- instance [Succ? α] [LT α] [DecidableLT α] : RangeIter ⟨.open, .none⟩ α :=
+--   .of fun r => Range.succIterator r.lower 1 (fun _ => True) (by omega) |>.drop 1
+
+-- instance [Succ? α] [LE α] [DecidableLE α] [HasDownwardUnboundedRanges α] :
+--     RangeIter ⟨.none, .closed⟩ α :=
+--   .of fun r => Range.succIterator HasDownwardUnboundedRanges.min 1 (· ≤ r.upper) (by omega)
+
+-- -- TODO: iterators for ranges that are unbounded downwards
+
+-- theorem Range.SuccIterator.succ?_eq_some_of_isPlausibleSuccessorOf [Succ? α] [LE α] [DecidableLE α]
+--     [∀ a h, Finite (Range.SuccIterator (α := α) 1 (· ≤ a) h) Id]
+--     {it' it : Iter (α := Range.SuccIterator (α := α) 1 (· ≤ a) h) α}
+--     (h' : it'.IsPlausibleSuccessorOf it) :
+--     Succ?.succAtIdx? 1 it.internalState.next = some it'.internalState.next :=
+--   h' |>
+--     TakeWhile.isPlausibleSuccessorOf_inner_of_isPlausibleSuccessorOf |>
+--     RepeatIterator.Monadic.next_eq_some_of_isPlausibleSuccessorOf
+
+-- instance [Succ? α] [LE α] [DecidableLE α] [LawfulLESucc? α] [Monad m]
+--     [∀ a h, Finite (Range.SuccIterator (α := α) 1  (· ≤ a) h) Id] :
+--     ForIn' m (PRange ⟨.closed, .closed⟩ α) α inferInstance where
+--   forIn' r init f := by
+--     haveI : MonadLift Id m := ⟨Std.Internal.idToMonad (α := _)⟩
+--     refine ForIn'.forIn' (α := α) r.iter init (fun a ha acc => f a ?_ acc)
+--     have hle : r.lower ≤ r.iter.internalState.next := LawfulLESucc?.le_rfl
+--     generalize r.iter = it at ha hle
+--     induction ha with
+--     | direct =>
+--       rename_i it out h
+--       rcases h with ⟨it', h, h'⟩
+--       refine ⟨?_, ?_⟩
+--       · rcases h with ⟨rfl, _⟩
+--         exact hle
+--       · simpa [PostconditionT.pure] using h'
+--     | indirect =>
+--       rename_i it it' it'' out h h' ih
+--       apply ih
+--       replace h := Range.SuccIterator.succ?_eq_some_of_isPlausibleSuccessorOf h
+--       exact LawfulLESucc?.le_succAtIdx?_of_le (α := α) hle h
+
+-- instance [Succ? α] [LE α] [DecidableLE α] [LawfulLESucc? α]
+--     [HasDownwardUnboundedRanges α] [Monad m]
+--     [∀ a h, Finite (Range.SuccIterator (α := α) 1  (· ≤ a) h) Id] :
+--     ForIn' m (PRange ⟨.none, .closed⟩ α) α inferInstance where
+--   forIn' r init f := by
+--     haveI : MonadLift Id m := ⟨Std.Internal.idToMonad (α := _)⟩
+--     refine ForIn'.forIn' (α := α) r.iter init (fun a ha acc => f a ?_ acc)
+--     generalize r.iter = it at ha
+--     induction ha with
+--     | direct =>
+--       sorry
+--     | indirect =>
+--       sorry
+
+-- end Iterator
+
+-- section Examples
+
+-- end Examples

src/Std/Data/Ranges/Nat.lean

@@ -0,0 +1,52 @@
+prelude
+-- import Std.Data.Ranges.Basic
+-- import Std.Data.Ranges.General
+-- import Std.Data.Ranges.Slice
+-- import Std.Data.Iterators.Combinators.Monadic.Lineage
+
+-- open Std.Iterators
+
+-- instance : Succ? Nat where
+--   succ? n := some (n + 1)
+
+-- instance : LawfulLESucc? Nat where
+--   le_rfl := Nat.le_refl _
+--   le_succ?_of_le hle h := by
+--     simp only [Succ?.succ?, Option.some.injEq] at h
+--     omega
+--   le_succAtIdx?_of_le {a b c n} hle h := by
+--     simp only [Succ?.succAtIdx?, Option.bind_eq_bind] at h
+--     induction n generalizing b c with
+--     | zero => simp_all [Nat.repeat]
+--     | succ n ih =>
+--       simp only [Nat.repeat, Option.bind_eq_some_iff] at h ih
+--       rcases h with ⟨c', hc', h⟩
+--       cases h
+--       specialize ih hle hc'
+--       omega
+
+-- instance (stepSize : Nat) (h) :
+--     Finite (Range.SuccIterator (α := Nat) stepSize (· ≤ n) h) Id := by
+--   unfold Range.SuccIterator
+--   sorry
+
+-- instance (stepSize : Nat) (h) :
+--     Finite (Range.SuccIterator (α := Nat) stepSize (· < n) h) Id := by
+--   unfold Range.SuccIterator
+--   sorry
+
+-- instance (stepSize : Nat) (h) :
+--     IteratorSize (Range.SuccIterator (α := Nat) stepSize (· ≤ n) h) Id where
+--   size it := pure <| .up <| (n + stepSize - it.internalState.next) / stepSize
+
+-- instance (stepSize : Nat) (h) :
+--     IteratorSizePartial (Range.SuccIterator (α := Nat) stepSize (· ≤ n) h) Id where
+--   size it := pure <| .up <| (n + stepSize - it.internalState.next) / stepSize
+
+-- instance (stepSize : Nat) (h) :
+--     IteratorSize (Range.SuccIterator (α := Nat) stepSize (· < n) h) Id where
+--   size it := pure <| .up <| (n + stepSize - it.internalState.next - 1) / stepSize
+
+-- instance (stepSize : Nat) (h) :
+--     IteratorSizePartial (Range.SuccIterator (α := Nat) stepSize (· < n) h) Id where
+--   size it := pure <| .up <| (n + stepSize - it.internalState.next - 1) / stepSize

src/Std/Data/Ranges/Slice.lean

@@ -0,0 +1,55 @@
+prelude
+-- import Std.Data.Ranges.Basic
+
+-- open Std.Iterators
+
+-- class Sliceable (shape : RangeShape) (ρ : Type v) (α : Type u) (β : outParam (Type w)) where
+
+-- structure Slice (shape : RangeShape) (ρ : Type v) (α : Type u) where
+--   collection : ρ
+--   range : PRange shape α
+
+-- def makeSlice [Sliceable shape ρ α β] (x : ρ) (r : PRange shape α) : Slice shape ρ α :=
+--   ⟨x, r⟩
+
+-- syntax:max term noWs "[[" term "]]" : term
+
+-- macro_rules
+--   | `($x[[$r]]) => `(makeSlice $x $r)
+
+-- class SliceIter (shape : RangeShape) (ρ α) {β} [Sliceable shape ρ α β] where
+--   State : Slice shape ρ α → Type u
+--   iter : (s : Slice shape ρ α) → Iter (α := State s) β
+
+-- @[always_inline, inline]
+-- def SliceIter.of [Sliceable shape ρ α β] {State : Slice shape ρ α → _}
+--     (iter : (s : Slice shape ρ α) → Iter (α := State s) β) : SliceIter shape ρ α where
+--   State := State
+--   iter := iter
+
+-- @[always_inline, inline]
+-- def Slice.iter [Sliceable shape ρ α β] [SliceIter shape ρ α]
+--     (s : Slice shape ρ α) :
+--     Iter (α := SliceIter.State (shape := shape) (ρ := ρ) (α := α) (β := β) s) β :=
+--   SliceIter.iter s
+
+-- instance {State : Slice shape ρ α → _} [Iterator (State s) Id α] [Sliceable shape ρ α β]
+--     {iter : (s : Slice shape ρ α) → Iter (α := State s) β} :
+--     letI : SliceIter shape ρ α := SliceIter.of iter
+--     Iterator (SliceIter.State (shape := shape) (ρ := ρ) (α := α) β s) Id α :=
+--   inferInstanceAs <| Iterator (State s) Id α
+
+-- instance {State : Slice shape ρ α → _} [Iterator (State s) Id α]
+--     [Sliceable shape ρ α β]
+--     [Finite (State s) Id]
+--     {iter : (s : Slice shape ρ α) → Iter (α := State s) β} :
+--     letI : SliceIter shape ρ α := SliceIter.of iter
+--     Finite (SliceIter.State (shape := shape) (ρ := ρ) (α := α) β s) Id :=
+--   inferInstanceAs <| Finite (State s) Id
+
+-- instance {State : Slice shape ρ α → _} [Iterator (State s) Id α] [Sliceable shape ρ α β]
+--     [IteratorCollect (State s) Id m]
+--     {iter : (s : Slice shape ρ α) → Iter (α := State s) β} :
+--     letI : SliceIter shape ρ α := SliceIter.of iter
+--     IteratorCollect (SliceIter.State (shape := shape) (ρ := ρ) (α := α) β s) Id m :=
+--   inferInstanceAs <| IteratorCollect (State s) Id m

tests/lean/run/rangesSlices.lean

@@ -0,0 +1,47 @@
+prelude
+import Init.Data.Range.New.RangeIterator
+--import Init.Data.Range.New.Nat
+import Init.System.IO
+import Init.Data.Iterators
+
+open Std.Iterators Types
+
+def it := (⟨⟨some 0⟩⟩ : Iter (α := RangeIterator Nat inferInstance (· < 5)) Nat)
+
+set_option trace.compiler.ir true in
+set_option compiler.small 1000 in
+def f (it : Iter (α := RangeIterator Nat (some <| · + 1) (· < 5)) Nat) : Nat := Id.run do
+  let mut acc := 0
+  for x in it do
+    acc := acc + x
+  return acc
+
+#eval! f it
+
+#eval! it.toList
+
+#eval "b" ∈ ("a",,"c")
+
+#eval "a"
+
+#eval! (1<,,<4).iter.toList
+
+#eval! (2<,,<5).size
+
+-- #eval (,,<5).iter.toList
+
+#eval 1 ∈ (1,,5)
+
+-- TODO:
+instance [Pure m] : MonadLiftT Id m where
+  monadLift := pure
+
+def f : IO Unit := do
+  for h : x in ((2 : Nat),,8) do -- ugly: For some reason, we need a type hint here
+    IO.println x
+
+#synth ForIn IO (type_of% (2,,8)) _ -- Note that we don't need the type hint this time
+
+def testArray : Array Nat := #[0, 1, 2, 3, 4, 5, 6]
+
+-- #eval testArray[[2<,,]].iter.toList