feat: List slices (#11019)

This PR introduces slices of lists that are available via slice notation
(e.g., `xs[1...5]`).

* Moved the `take` combinator and the `List` iterator producer to
`Init`.
* Introduced a `toTake` combinator: `it.toTake` behaves like `it`, but
it has the same type as `it.take n`. There is a constant cost per
iteration compared to `it` itself.
* Introduced `List` slices. Their iterators are defined as
`suffixList.iter.take n` for upper-bounded slices and
`suffixList.iter.toTake` for unbounded ones.

Performance characteristics of using the slice `list[a...b]`:

* when creating it: `O(a)`
* every iterator step: `O(1)`
* `toList`: `O(b - a + 1)` (given that a <= b)

Because the slice only stores a suffix of `xs` internally, two slices
can be equal even though the underlying lists differ in an irrelevant
prefix. Because the `stop` field is allowed to be beyond the list's
upper bound, the slices `[1][0...1]` and `[1][0...2]` are not equal,
even though they effectively cover the same range of the same list.
Improving this would require us to call `List.length` when building the
slice, which would iterate through the whole list.

src/Init/Data/Iterators.lean

@@ -9,6 +9,7 @@ prelude
 public import Init.Data.Iterators.Basic
 public import Init.Data.Iterators.PostconditionMonad
 public import Init.Data.Iterators.Consumers
+public import Init.Data.Iterators.Producers
 public import Init.Data.Iterators.Combinators
 public import Init.Data.Iterators.Lemmas
 public import Init.Data.Iterators.ToIterator

src/Init/Data/Iterators/Basic.lean

@@ -817,6 +817,24 @@ def IterM.TerminationMeasures.Productive.Rel
     TerminationMeasures.Productive α m → TerminationMeasures.Productive α m → Prop :=
   Relation.TransGen <| InvImage IterM.IsPlausibleSkipSuccessorOf IterM.TerminationMeasures.Productive.it
 
+theorem IterM.TerminationMeasures.Finite.Rel.of_productive
+    {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β] {a b : Finite α m} :
+    Productive.Rel ⟨a.it⟩ ⟨b.it⟩ → Finite.Rel a b := by
+  generalize ha' : Productive.mk a.it = a'
+  generalize hb' : Productive.mk b.it = b'
+  have ha : a = ⟨a'.it⟩ := by simp [← ha']
+  have hb : b = ⟨b'.it⟩ := by simp [← hb']
+  rw [ha, hb]
+  clear ha hb ha' hb' a b
+  rw [Productive.Rel, Finite.Rel]
+  intro h
+  induction h
+  · rename_i ih
+    exact .single ⟨_, rfl, ih⟩
+  · rename_i hab ih
+    refine .trans ih ?_
+    exact .single ⟨_, rfl, hab⟩
+
 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

src/Init/Data/Iterators/Combinators.lean

@@ -9,4 +9,5 @@ prelude
 public import Init.Data.Iterators.Combinators.Monadic
 public import Init.Data.Iterators.Combinators.FilterMap
 public import Init.Data.Iterators.Combinators.FlatMap
+public import Init.Data.Iterators.Combinators.Take
 public import Init.Data.Iterators.Combinators.ULift

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

@@ -8,4 +8,5 @@ module
 prelude
 public import Init.Data.Iterators.Combinators.Monadic.FilterMap
 public import Init.Data.Iterators.Combinators.Monadic.FlatMap
+public import Init.Data.Iterators.Combinators.Monadic.Take
 public import Init.Data.Iterators.Combinators.Monadic.ULift

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

@@ -0,0 +1,223 @@
+/-
+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
+public import Init.Data.Nat.Lemmas
+public import Init.Data.Iterators.Consumers.Monadic.Collect
+public import Init.Data.Iterators.Consumers.Monadic.Loop
+public import Init.Data.Iterators.Internal.Termination
+
+@[expose] public section
+
+/-!
+This module provides the iterator combinator `IterM.take`.
+-/
+
+namespace Std.Iterators
+
+variable {α : Type w} {m : Type w → Type w'} {β : Type w}
+
+/--
+The internal state of the `IterM.take` iterator combinator.
+-/
+@[unbox]
+structure Take (α : Type w) (m : Type w → Type w') {β : Type w} [Iterator α m β] where
+  /--
+  Internal implementation detail of the iterator library.
+  Caution: For `take n`, `countdown` is `n + 1`.
+  If `countdown` is zero, the combinator only terminates when `inner` terminates.
+  -/
+  countdown : Nat
+  /-- Internal implementation detail of the iterator library -/
+  inner : IterM (α := α) m β
+  /--
+  Internal implementation detail of the iterator library.
+  This proof term ensures that a `take` always produces a finite iterator from a productive one.
+  -/
+  finite : countdown > 0 ∨ Finite α m
+
+/--
+Given an iterator `it` and a natural number `n`, `it.take n` is an iterator that outputs
+up to the first `n` of `it`'s values in order and then terminates.
+
+**Marble diagram:**
+
+```text
+it          ---a----b---c--d-e--⊥
+it.take 3   ---a----b---c⊥
+
+it          ---a--⊥
+it.take 3   ---a--⊥
+```
+
+**Termination properties:**
+
+* `Finite` instance: only if `it` is productive
+* `Productive` instance: only if `it` is productive
+
+**Performance:**
+
+This combinator incurs an additional O(1) cost with each output of `it`.
+-/
+@[always_inline, inline]
+def IterM.take [Iterator α m β] (n : Nat) (it : IterM (α := α) m β) :=
+  toIterM (Take.mk (n + 1) it (Or.inl <| Nat.zero_lt_succ _)) m β
+
+/--
+This combinator is only useful for advanced use cases.
+
+Given a finite iterator `it`, returns an iterator that behaves exactly like `it` but is of the same
+type as `it.take n`.
+
+**Marble diagram:**
+
+```text
+it          ---a----b---c--d-e--⊥
+it.toTake   ---a----b---c--d-e--⊥
+```
+
+**Termination properties:**
+
+* `Finite` instance: always
+* `Productive` instance: always
+
+**Performance:**
+
+This combinator incurs an additional O(1) cost with each output of `it`.
+-/
+@[always_inline, inline]
+def IterM.toTake [Iterator α m β] [Finite α m] (it : IterM (α := α) m β) :=
+  toIterM (Take.mk 0 it (Or.inr inferInstance)) m β
+
+theorem IterM.take.surjective_of_zero_lt {α : Type w} {m : Type w → Type w'} {β : Type w}
+    [Iterator α m β] (it : IterM (α := Take α m) m β) (h : 0 < it.internalState.countdown) :
+    ∃ (it₀ : IterM (α := α) m β) (k : Nat), it = it₀.take k := by
+  refine ⟨it.internalState.inner, it.internalState.countdown - 1, ?_⟩
+  simp only [take, Nat.sub_add_cancel (m := 1) (n := it.internalState.countdown) (by omega)]
+  rfl
+
+inductive Take.PlausibleStep [Iterator α m β] (it : IterM (α := Take α m) m β) :
+    (step : IterStep (IterM (α := Take α m) m β) β) → Prop where
+  | yield : ∀ {it' out}, it.internalState.inner.IsPlausibleStep (.yield it' out) →
+      (h : it.internalState.countdown ≠ 1) → PlausibleStep it (.yield ⟨it.internalState.countdown - 1, it', it.internalState.finite.imp_left (by omega)⟩ out)
+  | skip : ∀ {it'}, it.internalState.inner.IsPlausibleStep (.skip it') →
+      it.internalState.countdown ≠ 1 → PlausibleStep it (.skip ⟨it.internalState.countdown, it', it.internalState.finite⟩)
+  | done : it.internalState.inner.IsPlausibleStep .done → PlausibleStep it .done
+  | depleted : it.internalState.countdown = 1 →
+      PlausibleStep it .done
+
+@[always_inline, inline]
+instance Take.instIterator [Monad m] [Iterator α m β] : Iterator (Take α m) m β where
+  IsPlausibleStep := Take.PlausibleStep
+  step it :=
+    if h : it.internalState.countdown = 1 then
+      pure <| .deflate <| .done (.depleted h)
+    else do
+      match (← it.internalState.inner.step).inflate with
+      | .yield it' out h' =>
+        pure <| .deflate <| .yield ⟨it.internalState.countdown - 1, it', (it.internalState.finite.imp_left (by omega))⟩ out (.yield h' h)
+      | .skip it' h' => pure <| .deflate <| .skip ⟨it.internalState.countdown, it', it.internalState.finite⟩ (.skip h' h)
+      | .done h' => pure <| .deflate <| .done (.done h')
+
+def Take.Rel (m : Type w → Type w') [Monad m] [Iterator α m β] [Productive α m] :
+    IterM (α := Take α m) m β → IterM (α := Take α m) m β → Prop :=
+  open scoped Classical in
+  if _ : Finite α m then
+    InvImage (Prod.Lex Nat.lt_wfRel.rel IterM.TerminationMeasures.Finite.Rel)
+      (fun it => (it.internalState.countdown, it.internalState.inner.finitelyManySteps))
+  else
+    InvImage (Prod.Lex Nat.lt_wfRel.rel IterM.TerminationMeasures.Productive.Rel)
+      (fun it => (it.internalState.countdown, it.internalState.inner.finitelyManySkips))
+
+theorem Take.rel_of_countdown [Monad m] [Iterator α m β] [Productive α m]
+    {it it' : IterM (α := Take α m) m β}
+    (h : it'.internalState.countdown < it.internalState.countdown) : Take.Rel m it' it := by
+  simp only [Rel]
+  split <;> exact Prod.Lex.left _ _ h
+
+theorem Take.rel_of_inner [Monad m] [Iterator α m β] [Productive α m] {remaining : Nat}
+    {it it' : IterM (α := α) m β}
+    (h : it'.finitelyManySkips.Rel it.finitelyManySkips) :
+    Take.Rel m (it'.take remaining) (it.take remaining) := by
+  simp only [Rel]
+  split
+  · exact Prod.Lex.right _ (.of_productive h)
+  · exact Prod.Lex.right _ h
+
+theorem Take.rel_of_zero_of_inner [Monad m] [Iterator α m β]
+    {it it' : IterM (α := Take α m) m β}
+    (h : it.internalState.countdown = 0) (h' : it'.internalState.countdown = 0)
+    (h'' : haveI := it.internalState.finite.resolve_left (by omega); it'.internalState.inner.finitelyManySteps.Rel it.internalState.inner.finitelyManySteps) :
+    haveI := it.internalState.finite.resolve_left (by omega)
+    Take.Rel m it' it := by
+  haveI := it.internalState.finite.resolve_left (by omega)
+  simp only [Rel, this, ↓reduceDIte, InvImage, h, h']
+  exact Prod.Lex.right _ h''
+
+private def Take.instFinitenessRelation [Monad m] [Iterator α m β]
+    [Productive α m] :
+    FinitenessRelation (Take α m) m where
+  rel := Take.Rel m
+  wf := by
+    rw [Rel]
+    split
+    all_goals
+      apply InvImage.wf
+      refine ⟨fun (a, b) => Prod.lexAccessible (WellFounded.apply ?_ a) (WellFounded.apply ?_) b⟩
+      · exact WellFoundedRelation.wf
+      · exact WellFoundedRelation.wf
+  subrelation {it it'} h := by
+    obtain ⟨step, h, h'⟩ := h
+    cases h'
+    case yield it' out k h' h'' =>
+      cases h
+      cases it.internalState.finite
+      · apply rel_of_countdown
+        simp only
+        omega
+      · by_cases h : it.internalState.countdown = 0
+        · simp only [h, Nat.zero_le, Nat.sub_eq_zero_of_le]
+          apply rel_of_zero_of_inner h rfl
+          exact .single ⟨_, rfl, h'⟩
+        · apply rel_of_countdown
+          simp only
+          omega
+    case skip it' out k h' h'' =>
+      cases h
+      by_cases h : it.internalState.countdown = 0
+      · simp only [h]
+        apply Take.rel_of_zero_of_inner h rfl
+        exact .single ⟨_, rfl, h'⟩
+      · obtain ⟨it, k, rfl⟩ := IterM.take.surjective_of_zero_lt it (by omega)
+        apply Take.rel_of_inner
+        exact IterM.TerminationMeasures.Productive.rel_of_skip h'
+    case done _ =>
+      cases h
+    case depleted _ =>
+      cases h
+
+instance Take.instFinite [Monad m] [Iterator α m β] [Productive α m] :
+    Finite (Take α m) m :=
+  by exact Finite.of_finitenessRelation instFinitenessRelation
+
+instance Take.instIteratorCollect {n : Type w → Type w'} [Monad m] [Monad n] [Iterator α m β] :
+    IteratorCollect (Take α m) m n :=
+  .defaultImplementation
+
+instance Take.instIteratorCollectPartial {n : Type w → Type w'} [Monad m] [Monad n] [Iterator α m β] :
+    IteratorCollectPartial (Take α m) m n :=
+  .defaultImplementation
+
+instance Take.instIteratorLoop {n : Type x → Type x'} [Monad m] [Monad n] [Iterator α m β] :
+    IteratorLoop (Take α m) m n :=
+  .defaultImplementation
+
+instance Take.instIteratorLoopPartial [Monad m] [Monad n] [Iterator α m β] :
+    IteratorLoopPartial (Take α m) m n :=
+  .defaultImplementation
+
+end Std.Iterators

src/Init/Data/Iterators/Combinators/Take.lean

@@ -0,0 +1,70 @@
+/-
+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
+public import Init.Data.Iterators.Combinators.Monadic.Take
+
+@[expose] public section
+
+namespace Std.Iterators
+
+/--
+Given an iterator `it` and a natural number `n`, `it.take n` is an iterator that outputs
+up to the first `n` of `it`'s values in order and then terminates.
+
+**Marble diagram:**
+
+```text
+it          ---a----b---c--d-e--⊥
+it.take 3   ---a----b---c⊥
+
+it          ---a--⊥
+it.take 3   ---a--⊥
+```
+
+**Termination properties:**
+
+* `Finite` instance: only if `it` is productive
+* `Productive` instance: only if `it` is productive
+
+**Performance:**
+
+This combinator incurs an additional O(1) cost with each output of `it`.
+-/
+@[always_inline, inline]
+def Iter.take {α : Type w} {β : Type w} [Iterator α Id β] (n : Nat) (it : Iter (α := α) β) :
+    Iter (α := Take α Id) β :=
+  it.toIterM.take n |>.toIter
+
+/--
+This combinator is only useful for advanced use cases.
+
+Given a finite iterator `it`, returns an iterator that behaves exactly like `it` but is of the same
+type as `it.take n`.
+
+**Marble diagram:**
+
+```text
+it          ---a----b---c--d-e--⊥
+it.toTake   ---a----b---c--d-e--⊥
+```
+
+**Termination properties:**
+
+* `Finite` instance: always
+* `Productive` instance: always
+
+**Performance:**
+
+This combinator incurs an additional O(1) cost with each output of `it`.
+-/
+@[always_inline, inline]
+def Iter.toTake {α : Type w} {β : Type w} [Iterator α Id β] [Finite α Id] (it : Iter (α := α) β) :
+    Iter (α := Take α Id) β :=
+  it.toIterM.toTake.toIter
+
+end Std.Iterators

src/Init/Data/Iterators/Lemmas.lean

@@ -8,3 +8,4 @@ module
 prelude
 public import Init.Data.Iterators.Lemmas.Consumers
 public import Init.Data.Iterators.Lemmas.Combinators
+public import Init.Data.Iterators.Lemmas.Producers

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

@@ -10,4 +10,5 @@ public import Init.Data.Iterators.Lemmas.Combinators.Attach
 public import Init.Data.Iterators.Lemmas.Combinators.Monadic
 public import Init.Data.Iterators.Lemmas.Combinators.FilterMap
 public import Init.Data.Iterators.Lemmas.Combinators.FlatMap
+public import Init.Data.Iterators.Lemmas.Combinators.Take
 public import Init.Data.Iterators.Lemmas.Combinators.ULift

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

@@ -9,4 +9,5 @@ prelude
 public import Init.Data.Iterators.Lemmas.Combinators.Monadic.Attach
 public import Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
 public import Init.Data.Iterators.Lemmas.Combinators.Monadic.FlatMap
+public import Init.Data.Iterators.Lemmas.Combinators.Monadic.Take
 public import Init.Data.Iterators.Lemmas.Combinators.Monadic.ULift

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

@@ -0,0 +1,77 @@
+/-
+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
+public import Init.Data.Iterators.Combinators.Monadic.Take
+public import Init.Data.Iterators.Lemmas.Consumers.Monadic
+
+@[expose] public section
+
+namespace Std.Iterators
+
+theorem Take.isPlausibleStep_take_yield [Monad m] [Iterator α m β] {n : Nat}
+    {it : IterM (α := α) m β} (h : it.IsPlausibleStep (.yield it' out)) :
+    (it.take (n + 1)).IsPlausibleStep (.yield (it'.take n) out) :=
+  (.yield h (by simp [IterM.take]))
+
+theorem Take.isPlausibleStep_take_skip [Monad m] [Iterator α m β] {n : Nat}
+    {it : IterM (α := α) m β} (h : it.IsPlausibleStep (.skip it')) :
+    (it.take (n + 1)).IsPlausibleStep (.skip (it'.take (n + 1))) :=
+  (.skip h (by simp [IterM.take]))
+
+theorem IterM.step_take {α m β} [Monad m] [Iterator α m β] {n : Nat}
+    {it : IterM (α := α) m β} :
+    (it.take n).step = (match n with
+      | 0 => pure <| .deflate <| .done (.depleted rfl)
+      | k + 1 => do
+        match (← it.step).inflate with
+        | .yield it' out h => pure <| .deflate <| .yield (it'.take k) out (Take.isPlausibleStep_take_yield h)
+        | .skip it' h => pure <| .deflate <| .skip (it'.take (k + 1)) (Take.isPlausibleStep_take_skip h)
+        | .done h => pure <| .deflate <| .done (.done h)) := by
+  simp only [take, step, Iterator.step, internalState_toIterM]
+  cases n
+  case zero => rfl
+  case succ k =>
+    apply bind_congr
+    intro step
+    cases step.inflate using PlausibleIterStep.casesOn <;> rfl
+
+theorem IterM.toList_take_zero {α m β} [Monad m] [LawfulMonad m] [Iterator α m β]
+    [Finite (Take α m) m]
+    [IteratorCollect (Take α m) m m] [LawfulIteratorCollect (Take α m) m m]
+    {it : IterM (α := α) m β} :
+    (it.take 0).toList = pure [] := by
+  rw [toList_eq_match_step]
+  simp [step_take]
+
+theorem IterM.step_toTake {α m β} [Monad m] [Iterator α m β] [Finite α m]
+    {it : IterM (α := α) m β} :
+    it.toTake.step = (do
+        match (← it.step).inflate with
+        | .yield it' out h => pure <| .deflate <| .yield it'.toTake out (.yield h Nat.zero_ne_one)
+        | .skip it' h => pure <| .deflate <| .skip it'.toTake (.skip h Nat.zero_ne_one)
+        | .done h => pure <| .deflate <| .done (.done h)) := by
+  simp only [toTake, step, Iterator.step, internalState_toIterM]
+  apply bind_congr
+  intro step
+  cases step.inflate using PlausibleIterStep.casesOn <;> rfl
+
+@[simp]
+theorem IterM.toList_toTake {α m β} [Monad m] [LawfulMonad m] [Iterator α m β] [Finite α m]
+    [IteratorCollect α m m] [LawfulIteratorCollect α m m]
+    {it : IterM (α := α) m β} :
+    it.toTake.toList = it.toList := by
+  induction it using IterM.inductSteps with | step it ihy ihs
+  rw [toList_eq_match_step, toList_eq_match_step]
+  simp only [step_toTake, bind_assoc]
+  apply bind_congr; intro step
+  cases step.inflate using PlausibleIterStep.casesOn
+  · simp [ihy ‹_›]
+  · simp [ihs ‹_›]
+  · simp
+
+end Std.Iterators

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

@@ -6,8 +6,8 @@ Authors: Paul Reichert
 module
 
 prelude
-public import Std.Data.Iterators.Combinators.Take
-public import Std.Data.Iterators.Lemmas.Combinators.Monadic.Take
+public import Init.Data.Iterators.Combinators.Take
+public import Init.Data.Iterators.Lemmas.Combinators.Monadic.Take
 public import Init.Data.Iterators.Lemmas.Consumers
 
 @[expose] public section
@@ -19,14 +19,19 @@ theorem Iter.take_eq_toIter_take_toIterM {α β} [Iterator α Id β] {n : Nat}
     it.take n = (it.toIterM.take n).toIter :=
   rfl
 
+theorem Iter.toTake_eq_toIter_toTake_toIterM {α β} [Iterator α Id β] [Finite α Id]
+    {it : Iter (α := α) β} :
+    it.toTake = it.toIterM.toTake.toIter :=
+  rfl
+
 theorem Iter.step_take {α β} [Iterator α Id β] {n : Nat}
     {it : Iter (α := α) β} :
     (it.take n).step = (match n with
       | 0 => .done (.depleted rfl)
       | k + 1 =>
         match it.step with
-        | .yield it' out h => .yield (it'.take k) out (.yield h rfl)
-        | .skip it' h => .skip (it'.take (k + 1)) (.skip h rfl)
+        | .yield it' out h => .yield (it'.take k) out (Take.isPlausibleStep_take_yield h)
+        | .skip it' h => .skip (it'.take (k + 1)) (Take.isPlausibleStep_take_skip h)
         | .done h => .done (.done h)) := by
   simp only [Iter.step, Iter.step, Iter.take_eq_toIter_take_toIterM, IterM.step_take, toIterM_toIter]
   cases n
@@ -88,11 +93,29 @@ theorem Iter.toArray_take_of_finite {α β} [Iterator α Id β] {n : Nat}
 
 @[simp]
 theorem Iter.toList_take_zero {α β} [Iterator α Id β]
-    [Finite (Take α Id β) Id]
-    [IteratorCollect (Take α Id β) Id Id] [LawfulIteratorCollect (Take α Id β) Id Id]
+    [Finite (Take α Id) Id]
+    [IteratorCollect (Take α Id) Id Id] [LawfulIteratorCollect (Take α Id) Id Id]
     {it : Iter (α := α) β} :
     (it.take 0).toList = [] := by
   rw [toList_eq_match_step]
   simp [step_take]
 
+theorem Iter.step_toTake {α β} [Iterator α Id β] [Finite α Id]
+    {it : Iter (α := α) β} :
+    it.toTake.step = (
+        match it.step with
+        | .yield it' out h => .yield it'.toTake out (.yield h Nat.zero_ne_one)
+        | .skip it' h => .skip it'.toTake (.skip h Nat.zero_ne_one)
+        | .done h => .done (.done h)) := by
+  simp only [toTake_eq_toIter_toTake_toIterM, Iter.step, toIterM_toIter, IterM.step_toTake,
+    Id.run_bind]
+  cases it.toIterM.step.run.inflate using PlausibleIterStep.casesOn <;> simp
+
+@[simp]
+theorem Iter.toList_toTake {α β} [Iterator α Id β] [Finite α Id]
+    [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id]
+    {it : Iter (α := α) β} :
+    it.toTake.toList = it.toList := by
+  simp [toTake_eq_toIter_toTake_toIterM, toList_eq_toList_toIterM]
+
 end Std.Iterators

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

@@ -0,0 +1,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
+public import Init.Data.Iterators.Lemmas.Producers.Monadic
+public import Init.Data.Iterators.Lemmas.Producers.List

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

@@ -7,8 +7,8 @@ module
 
 prelude
 public import Init.Data.Iterators.Lemmas.Consumers.Collect
-public import Std.Data.Iterators.Producers.List
-public import Std.Data.Iterators.Lemmas.Producers.Monadic.List
+public import Init.Data.Iterators.Producers.List
+public import Init.Data.Iterators.Lemmas.Producers.Monadic.List
 
 @[expose] public section
 

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

@@ -0,0 +1,9 @@
+/-
+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
+public import Init.Data.Iterators.Lemmas.Producers.Monadic.List

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

@@ -0,0 +1,71 @@
+/-
+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
+public import Init.Data.Iterators.Lemmas.Consumers.Monadic
+public import Init.Data.Iterators.Producers.Monadic.List
+
+@[expose] public section
+
+/-!
+# Lemmas about list iterators
+
+This module provides lemmas about the interactions of `List.iterM` with `IterM.step` and various
+collectors.
+-/
+
+namespace Std.Iterators
+open Std.Internal
+
+variable {m : Type w → Type w'} {n : Type w → Type w''} [Monad m] {β : Type w}
+
+@[simp]
+theorem _root_.List.step_iterM_nil :
+    (([] : List β).iterM m).step = pure (.deflate ⟨.done, rfl⟩) := by
+  simp only [IterM.step, Iterator.step]; rfl
+
+@[simp]
+theorem _root_.List.step_iterM_cons {x : β} {xs : List β} :
+    ((x :: xs).iterM m).step = pure (.deflate ⟨.yield (xs.iterM m) x, rfl⟩) := by
+  simp only [List.iterM, IterM.step, Iterator.step]; rfl
+
+theorem _root_.List.step_iterM {l : List β} :
+    (l.iterM m).step = match l with
+      | [] => pure (.deflate ⟨.done, rfl⟩)
+      | x :: xs => pure (.deflate ⟨.yield (xs.iterM m) x, rfl⟩) := by
+  cases l <;> simp [List.step_iterM_cons, List.step_iterM_nil]
+
+theorem ListIterator.toArrayMapped_iterM [Monad n] [LawfulMonad n]
+    {β : Type w} {γ : Type w} {lift : ⦃δ : Type w⦄ → m δ → n δ}
+    [LawfulMonadLiftFunction lift] {f : β → n γ} {l : List β} :
+    IteratorCollect.toArrayMapped lift f (l.iterM m) (m := m) = List.toArray <$> l.mapM f := by
+  rw [LawfulIteratorCollect.toArrayMapped_eq]
+  induction l with
+  | nil =>
+    rw [IterM.DefaultConsumers.toArrayMapped_eq_match_step]
+    simp [List.step_iterM_nil, LawfulMonadLiftFunction.lift_pure]
+  | cons x xs ih =>
+    rw [IterM.DefaultConsumers.toArrayMapped_eq_match_step]
+    simp [List.step_iterM_cons, List.mapM_cons, pure_bind, ih, LawfulMonadLiftFunction.lift_pure]
+
+@[simp]
+theorem _root_.List.toArray_iterM [LawfulMonad m] {l : List β} :
+    (l.iterM m).toArray = pure l.toArray := by
+  simp only [IterM.toArray, ListIterator.toArrayMapped_iterM]
+  rw [List.mapM_pure, map_pure, List.map_id']
+
+@[simp]
+theorem _root_.List.toList_iterM [LawfulMonad m] {l : List β} :
+    (l.iterM m).toList = pure l := by
+  rw [← IterM.toList_toArray, List.toArray_iterM, map_pure, List.toList_toArray]
+
+@[simp]
+theorem _root_.List.toListRev_iterM [LawfulMonad m] {l : List β} :
+    (l.iterM m).toListRev = pure l.reverse := by
+  simp [IterM.toListRev_eq, List.toList_iterM]
+
+end Std.Iterators

src/Init/Data/Iterators/Producers.lean

@@ -0,0 +1,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
+public import Init.Data.Iterators.Producers.Monadic
+public import Init.Data.Iterators.Producers.List

src/Init/Data/Iterators/Producers/List.lean

@@ -6,7 +6,7 @@ Authors: Paul Reichert
 module
 
 prelude
-public import Std.Data.Iterators.Producers.Monadic.List
+public import Init.Data.Iterators.Producers.Monadic.List
 
 @[expose] public section
 

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

@@ -0,0 +1,9 @@
+/-
+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
+public import Init.Data.Iterators.Producers.Monadic.List

src/Init/Data/Slice.lean

@@ -10,6 +10,7 @@ public import Init.Data.Slice.Basic
 public import Init.Data.Slice.Notation
 public import Init.Data.Slice.Operations
 public import Init.Data.Slice.Array
+public import Init.Data.Slice.List
 public import Init.Data.Slice.Lemmas
 
 public section

src/Init/Data/Slice/Array/Iterator.lean

@@ -17,8 +17,7 @@ import Init.Omega
 public section
 
 /-!
-This module provides slice notation for array slices (a.k.a. `Subarray`) and implements an iterator
-for those slices.
+This module implements an iterator for array slices (`Subarray`).
 -/
 
 open Std Slice PRange Iterators

src/Init/Data/Slice/List.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
+public import Init.Data.Slice.List.Basic
+public import Init.Data.Slice.List.Iterator
+public import Init.Data.Slice.List.Lemmas

src/Init/Data/Slice/List/Basic.lean

@@ -0,0 +1,101 @@
+/-
+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
+public import Init.Data.Slice.Basic
+public import Init.Data.Slice.Notation
+public import Init.Data.Range.Polymorphic.Nat
+
+set_option linter.missingDocs true
+
+/-!
+This module provides slice notation for list slices (a.k.a. `Sublist`) and implements an iterator
+for those slices.
+-/
+
+open Std Std.Slice Std.PRange
+
+/--
+Internal representation of `ListSlice`, which is an abbreviation for `Slice ListSliceData`.
+-/
+public class Std.Slice.Internal.ListSliceData (α : Type u) where
+  /-- The relevant suffix of the underlying list. -/
+  list : List α
+  /-- The maximum length of the slice, starting at the beginning of `list`. -/
+  stop : Option Nat
+
+/--
+A region of some underlying list. List slices can be used to avoid copying or allocating space,
+while being more convenient than tracking the bounds by hand.
+
+A list slice only stores the suffix of the underlying list, starting from the range's lower bound
+so that the cost of operations on the slice does not depend on the start position. However,
+the cost of creating a list slice is linear in the start position.
+-/
+public abbrev ListSlice (α : Type u) := Slice (Internal.ListSliceData α)
+
+variable {α : Type u}
+
+/--
+Returns a slice of a list with the given bounds.
+
+If `start` or `stop` are not valid bounds for a sublist, then they are clamped to the list's length.
+Additionally, the starting index is clamped to the ending index.
+
+This function is linear in `start` because it stores `as.drop start` in the slice.
+-/
+public def List.toSlice (as : List α) (start : Nat) (stop : Nat) : ListSlice α :=
+  if start ≤ stop then
+    ⟨{ list := as.drop start, stop := some (stop - start) }⟩
+  else
+    ⟨{ list := [], stop := some 0 }⟩
+
+/--
+Returns a slice of a list with the given lower bound.
+
+If `start` is not a valid bound for a sublist, then they are clamped to the list's length.
+
+This function is linear in `start` because it stores `as.drop start` in the slice.
+-/
+public def List.toUnboundedSlice (as : List α) (start : Nat) : ListSlice α :=
+  ⟨{ list := as.drop start, stop := none }⟩
+
+public instance : Rcc.Sliceable (List α) Nat (ListSlice α) where
+  mkSlice xs range :=
+    (xs.toSlice range.lower (range.upper + 1))
+
+public instance : Rco.Sliceable (List α) Nat (ListSlice α) where
+  mkSlice xs range :=
+    (xs.toSlice range.lower range.upper)
+
+public instance : Rci.Sliceable (List α) Nat (ListSlice α) where
+  mkSlice xs range :=
+    (xs.toUnboundedSlice range.lower)
+
+public instance : Roc.Sliceable (List α) Nat (ListSlice α) where
+  mkSlice xs range :=
+    (xs.toSlice (range.lower + 1) (range.upper + 1))
+
+public instance : Roo.Sliceable (List α) Nat (ListSlice α) where
+  mkSlice xs range :=
+    (xs.toSlice (range.lower + 1) range.upper)
+
+public instance : Roi.Sliceable (List α) Nat (ListSlice α) where
+  mkSlice xs range :=
+    (xs.toUnboundedSlice (range.lower + 1))
+
+public instance : Ric.Sliceable (List α) Nat (ListSlice α) where
+  mkSlice xs range :=
+    (xs.toSlice 0 (range.upper + 1))
+
+public instance : Rio.Sliceable (List α) Nat (ListSlice α) where
+  mkSlice xs range :=
+    (xs.toSlice 0 range.upper)
+
+public instance : Rii.Sliceable (List α) Nat (ListSlice α) where
+  mkSlice xs _ :=
+    (xs.toUnboundedSlice 0)

src/Init/Data/Slice/List/Iterator.lean

@@ -0,0 +1,79 @@
+/-
+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
+public import Init.Data.Slice.List.Basic
+public import Init.Data.Iterators.Producers.List
+public import Init.Data.Iterators.Combinators.Take
+import all Init.Data.Range.Polymorphic.Basic
+public import Init.Data.Range.Polymorphic.Iterators
+public import Init.Data.Slice.Operations
+import Init.Omega
+
+public section
+
+/-!
+This module implements an iterator for list slices.
+-/
+
+open Std Slice PRange Iterators
+
+variable {shape : RangeShape} {α : Type u}
+
+instance {s : ListSlice α} : ToIterator s Id α :=
+  .of _ (match s.internalRepresentation.stop with
+      | some n => s.internalRepresentation.list.iter.take n
+      | none => s.internalRepresentation.list.iter.toTake)
+
+universe v w
+
+@[no_expose] instance {s : ListSlice α} : Iterator (ToIterator.State s Id) Id α := inferInstance
+@[no_expose] instance {s : ListSlice α} : Finite (ToIterator.State s Id) Id := inferInstance
+@[no_expose] instance {s : ListSlice α} : IteratorCollect (ToIterator.State s Id) Id Id := inferInstance
+@[no_expose] instance {s : ListSlice α} : IteratorCollectPartial (ToIterator.State s Id) Id Id := inferInstance
+@[no_expose] instance {s : ListSlice α} {m : Type v → Type w} [Monad m] :
+    IteratorLoop (ToIterator.State s Id) Id m := inferInstance
+@[no_expose] instance {s : ListSlice α} {m : Type v → Type w} [Monad m] :
+    IteratorLoopPartial (ToIterator.State s Id) Id m := inferInstance
+
+instance : SliceSize (Internal.ListSliceData α) where
+  size s := (Internal.iter s).count
+
+@[no_expose]
+instance {α : Type u} {m : Type v → Type w} :
+    ForIn m (ListSlice α) α where
+  forIn xs init f := forIn (Internal.iter xs) init f
+
+namespace List
+
+/-- Allocates a new list that contains the contents of the slice. -/
+def ofSlice (s : ListSlice α) : List α :=
+  s.toList
+
+docs_to_verso ofSlice
+
+instance : Append (ListSlice α) where
+  append x y :=
+   let a := x.toList ++ y.toList
+   a.toSlice 0 a.length
+
+/-- `ListSlice` representation. -/
+protected def ListSlice.repr [Repr α] (s : ListSlice α) : Std.Format :=
+  let xs := s.toList
+  repr xs ++ ".toSlice 0 " ++ toString xs.length
+
+instance [Repr α] : Repr (ListSlice α) where
+  reprPrec s  _ := ListSlice.repr s
+
+instance [ToString α] : ToString (ListSlice α) where
+  toString s := toString s.toArray
+
+end List
+
+@[inherit_doc List.ofSlice]
+def ListSlice.toList (s : ListSlice α) : List α :=
+  List.ofSlice s

src/Init/Data/Slice/List/Lemmas.lean

@@ -0,0 +1,43 @@
+/-
+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 all Init.Data.Slice.List.Basic
+public import Init.Data.Slice.List.Iterator
+import all Init.Data.Slice.List.Iterator
+import all Init.Data.Slice.Operations
+import all Init.Data.Range.Polymorphic.Iterators
+import all Init.Data.Range.Polymorphic.Lemmas
+public import Init.Data.Slice.Lemmas
+public import Init.Data.Iterators.Lemmas
+
+open Std.Iterators Std.PRange
+
+namespace Std.Slice.List
+
+theorem internalIter_eq {α : Type u} {s : ListSlice α} :
+    Internal.iter s = match s.internalRepresentation.stop with
+        | some stop => s.internalRepresentation.list.iter.take stop
+        | none => s.internalRepresentation.list.iter.toTake := by
+  simp only [Internal.iter, ToIterator.iter_eq]; rfl
+
+theorem toList_internalIter {α : Type u} {s : ListSlice α} :
+    (Internal.iter s).toList = match s.internalRepresentation.stop with
+        | some stop => s.internalRepresentation.list.take stop
+        | none => s.internalRepresentation.list := by
+  simp only [internalIter_eq]
+  split <;> simp
+
+theorem internalIter_eq_toIteratorIter {α : Type u} {s : ListSlice α} :
+    Internal.iter s = ToIterator.iter s :=
+  rfl
+
+public instance : LawfulSliceSize (Internal.ListSliceData α) where
+  lawful s := by
+    simp [← internalIter_eq_toIteratorIter, SliceSize.size]
+
+end Std.Slice.List

src/Std/Data/Iterators/Combinators.lean

@@ -7,7 +7,6 @@ module
 
 prelude
 public import Std.Data.Iterators.Combinators.Monadic
-public import Std.Data.Iterators.Combinators.Take
 public import Std.Data.Iterators.Combinators.TakeWhile
 public import Std.Data.Iterators.Combinators.Drop
 public import Std.Data.Iterators.Combinators.DropWhile

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

@@ -6,7 +6,6 @@ Authors: Paul Reichert
 module
 
 prelude
-public import Std.Data.Iterators.Combinators.Monadic.Take
 public import Std.Data.Iterators.Combinators.Monadic.TakeWhile
 public import Std.Data.Iterators.Combinators.Monadic.Drop
 public import Std.Data.Iterators.Combinators.Monadic.DropWhile

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

@@ -1,152 +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
--/
-module
-
-prelude
-public import Init.Data.Nat.Lemmas
-public import Init.Data.Iterators.Consumers.Monadic.Collect
-public import Init.Data.Iterators.Consumers.Monadic.Loop
-public import Init.Data.Iterators.Internal.Termination
-
-@[expose] public section
-
-/-!
-This module provides the iterator combinator `IterM.take`.
--/
-
-namespace Std.Iterators
-
-variable {α : Type w} {m : Type w → Type w'} {β : Type w}
-
-/--
-The internal state of the `IterM.take` iterator combinator.
--/
-@[unbox]
-structure Take (α : Type w) (m : Type w → Type w') (β : Type w) where
-  /-- Internal implementation detail of the iterator library -/
-  remaining : Nat
-  /-- Internal implementation detail of the iterator library -/
-  inner : IterM (α := α) m β
-
-/--
-Given an iterator `it` and a natural number `n`, `it.take n` is an iterator that outputs
-up to the first `n` of `it`'s values in order and then terminates.
-
-**Marble diagram:**
-
-```text
-it          ---a----b---c--d-e--⊥
-it.take 3   ---a----b---c⊥
-
-it          ---a--⊥
-it.take 3   ---a--⊥
-```
-
-**Termination properties:**
-
-* `Finite` instance: only if `it` is productive
-* `Productive` instance: only if `it` is productive
-
-**Performance:**
-
-This combinator incurs an additional O(1) cost with each output of `it`.
--/
-@[always_inline, inline]
-def IterM.take (n : Nat) (it : IterM (α := α) m β) :=
-  toIterM (Take.mk n it) m β
-
-theorem IterM.take.surjective {α : Type w} {m : Type w → Type w'} {β : Type w}
-    (it : IterM (α := Take α m β) m β) :
-    ∃ (it₀ : IterM (α := α) m β) (k : Nat), it = it₀.take k := by
-  refine ⟨it.internalState.inner, it.internalState.remaining, rfl⟩
-
-inductive Take.PlausibleStep [Iterator α m β] (it : IterM (α := Take α m β) m β) :
-    (step : IterStep (IterM (α := Take α m β) m β) β) → Prop where
-  | yield : ∀ {it' out k}, it.internalState.inner.IsPlausibleStep (.yield it' out) →
-      it.internalState.remaining = k + 1 → PlausibleStep it (.yield (it'.take k) out)
-  | skip : ∀ {it' k}, it.internalState.inner.IsPlausibleStep (.skip it') →
-      it.internalState.remaining = k + 1 → PlausibleStep it (.skip (it'.take (k + 1)))
-  | done : it.internalState.inner.IsPlausibleStep .done → PlausibleStep it .done
-  | depleted : it.internalState.remaining = 0 →
-      PlausibleStep it .done
-
-@[always_inline, inline]
-instance Take.instIterator [Monad m] [Iterator α m β] : Iterator (Take α m β) m β where
-  IsPlausibleStep := Take.PlausibleStep
-  step it :=
-    match h : it.internalState.remaining with
-    | 0 => pure <| .deflate <| .done (.depleted h)
-    | k + 1 => do
-      match (← it.internalState.inner.step).inflate with
-      | .yield it' out h' => pure <| .deflate <| .yield (it'.take k) out (.yield h' h)
-      | .skip it' h' => pure <| .deflate <| .skip (it'.take (k + 1)) (.skip h' h)
-      | .done h' => pure <| .deflate <| .done (.done h')
-
-def Take.Rel (m : Type w → Type w') [Monad m] [Iterator α m β] [Productive α m] :
-    IterM (α := Take α m β) m β → IterM (α := Take α m β) m β → Prop :=
-  InvImage (Prod.Lex Nat.lt_wfRel.rel IterM.TerminationMeasures.Productive.Rel)
-    (fun it => (it.internalState.remaining, it.internalState.inner.finitelyManySkips))
-
-theorem Take.rel_of_remaining [Monad m] [Iterator α m β] [Productive α m]
-    {it it' : IterM (α := Take α m β) m β}
-    (h : it'.internalState.remaining < it.internalState.remaining) : Take.Rel m it' it :=
-  Prod.Lex.left _ _ h
-
-theorem Take.rel_of_inner [Monad m] [Iterator α m β] [Productive α m] {remaining : Nat}
-    {it it' : IterM (α := α) m β}
-    (h : it'.finitelyManySkips.Rel it.finitelyManySkips) :
-    Take.Rel m (it'.take remaining) (it.take remaining) :=
-  Prod.Lex.right _ h
-
-private def Take.instFinitenessRelation [Monad m] [Iterator α m β]
-    [Productive α m] :
-    FinitenessRelation (Take α m β) m where
-  rel := Take.Rel m
-  wf := by
-    apply InvImage.wf
-    refine ⟨fun (a, b) => Prod.lexAccessible (WellFounded.apply ?_ a) (WellFounded.apply ?_) b⟩
-    · exact WellFoundedRelation.wf
-    · exact WellFoundedRelation.wf
-  subrelation {it it'} h := by
-    obtain ⟨step, h, h'⟩ := h
-    cases h'
-    case yield it' out k h' h'' =>
-      cases h
-      apply rel_of_remaining
-      simp_all [IterM.take]
-    case skip it' out k h' h'' =>
-      cases h
-      obtain ⟨it, k, rfl⟩ := IterM.take.surjective it
-      cases h''
-      apply Take.rel_of_inner
-      exact IterM.TerminationMeasures.Productive.rel_of_skip h'
-    case done _ =>
-      cases h
-    case depleted _ =>
-      cases h
-
-instance Take.instFinite [Monad m] [Iterator α m β] [Productive α m] :
-    Finite (Take α m β) m :=
-  by exact Finite.of_finitenessRelation instFinitenessRelation
-
-instance Take.instIteratorCollect {n : Type w → Type w'} [Monad m] [Monad n] [Iterator α m β] :
-    IteratorCollect (Take α m β) m n :=
-  .defaultImplementation
-
-instance Take.instIteratorCollectPartial {n : Type w → Type w'} [Monad m] [Monad n] [Iterator α m β] :
-    IteratorCollectPartial (Take α m β) m n :=
-  .defaultImplementation
-
-instance Take.instIteratorLoop {n : Type x → Type x'} [Monad m] [Monad n] [Iterator α m β] :
-    IteratorLoop (Take α m β) m n :=
-  .defaultImplementation
-
-instance Take.instIteratorLoopPartial [Monad m] [Monad n] [Iterator α m β]
-    [MonadLiftT m n] :
-    IteratorLoopPartial (Take α m β) m n :=
-  .defaultImplementation
-
-end Std.Iterators

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

@@ -1,43 +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
--/
-module
-
-prelude
-public import Std.Data.Iterators.Combinators.Monadic.Take
-
-@[expose] public section
-
-namespace Std.Iterators
-
-/--
-Given an iterator `it` and a natural number `n`, `it.take n` is an iterator that outputs
-up to the first `n` of `it`'s values in order and then terminates.
-
-**Marble diagram:**
-
-```text
-it          ---a----b---c--d-e--⊥
-it.take 3   ---a----b---c⊥
-
-it          ---a--⊥
-it.take 3   ---a--⊥
-```
-
-**Termination properties:**
-
-* `Finite` instance: only if `it` is productive
-* `Productive` instance: only if `it` is productive
-
-**Performance:**
-
-This combinator incurs an additional O(1) cost with each output of `it`.
--/
-@[always_inline, inline]
-def Iter.take {α : Type w} {β : Type w} (n : Nat) (it : Iter (α := α) β) :
-    Iter (α := Take α Id β) β :=
-  it.toIterM.take n |>.toIter
-
-end Std.Iterators

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

@@ -7,7 +7,6 @@ module
 
 prelude
 public import Std.Data.Iterators.Lemmas.Combinators.Monadic
-public import Std.Data.Iterators.Lemmas.Combinators.Take
 public import Std.Data.Iterators.Lemmas.Combinators.TakeWhile
 public import Std.Data.Iterators.Lemmas.Combinators.Drop
 public import Std.Data.Iterators.Lemmas.Combinators.DropWhile

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

@@ -8,7 +8,7 @@ module
 prelude
 public import Std.Data.Iterators.Combinators.Drop
 public import Std.Data.Iterators.Lemmas.Combinators.Monadic.Drop
-public import Std.Data.Iterators.Lemmas.Combinators.Take
+public import Init.Data.Iterators.Lemmas.Combinators.Take
 
 @[expose] public section
 

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

@@ -6,7 +6,6 @@ Authors: Paul Reichert
 module
 
 prelude
-public import Std.Data.Iterators.Lemmas.Combinators.Monadic.Take
 public import Std.Data.Iterators.Lemmas.Combinators.Monadic.TakeWhile
 public import Std.Data.Iterators.Lemmas.Combinators.Monadic.Drop
 public import Std.Data.Iterators.Lemmas.Combinators.Monadic.DropWhile

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

@@ -1,41 +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
--/
-module
-
-prelude
-public import Std.Data.Iterators.Combinators.Monadic.Take
-public import Init.Data.Iterators.Lemmas.Consumers.Monadic
-
-@[expose] public section
-
-namespace Std.Iterators
-
-theorem IterM.step_take {α m β} [Monad m] [Iterator α m β] {n : Nat}
-    {it : IterM (α := α) m β} :
-    (it.take n).step = (match n with
-      | 0 => pure <| .deflate <| .done (.depleted rfl)
-      | k + 1 => do
-        match (← it.step).inflate with
-        | .yield it' out h => pure <| .deflate <| .yield (it'.take k) out (.yield h rfl)
-        | .skip it' h => pure <| .deflate <| .skip (it'.take (k + 1)) (.skip h rfl)
-        | .done h => pure <| .deflate <| .done (.done h)) := by
-  simp only [take, step, Iterator.step, internalState_toIterM, Nat.succ_eq_add_one]
-  cases n
-  case zero => rfl
-  case succ k =>
-    apply bind_congr
-    intro step
-    cases step.inflate using PlausibleIterStep.casesOn <;> rfl
-
-theorem IterM.toList_take_zero {α m β} [Monad m] [LawfulMonad m] [Iterator α m β]
-    [Finite (Take α m β) m]
-    [IteratorCollect (Take α m β) m m] [LawfulIteratorCollect (Take α m β) m m]
-    {it : IterM (α := α) m β} :
-    (it.take 0).toList = pure [] := by
-  rw [toList_eq_match_step]
-  simp [step_take]
-
-end Std.Iterators

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

@@ -8,7 +8,7 @@ module
 prelude
 public import Std.Data.Iterators.Combinators.Zip
 public import Std.Data.Iterators.Lemmas.Combinators.Monadic.Zip
-public import Std.Data.Iterators.Lemmas.Combinators.Take
+public import Init.Data.Iterators.Lemmas.Combinators.Take
 
 @[expose] public section
 

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

@@ -9,7 +9,6 @@ prelude
 public import Std.Data.Iterators.Lemmas.Producers.Monadic
 public import Std.Data.Iterators.Lemmas.Producers.Array
 public import Std.Data.Iterators.Lemmas.Producers.Empty
-public import Std.Data.Iterators.Lemmas.Producers.List
 public import Std.Data.Iterators.Lemmas.Producers.Repeat
 public import Std.Data.Iterators.Lemmas.Producers.Range
 public import Std.Data.Iterators.Lemmas.Producers.Slice

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

@@ -8,7 +8,7 @@ module
 prelude
 public import Std.Data.Iterators.Lemmas.Consumers.Collect
 public import Std.Data.Iterators.Producers.Array
-public import Std.Data.Iterators.Producers.List
+public import Init.Data.Iterators.Producers.List
 public import Std.Data.Iterators.Lemmas.Producers.Monadic.Array
 
 @[expose] public section

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

@@ -6,73 +6,16 @@ Authors: Paul Reichert
 module
 
 prelude
-public import Init.Data.Iterators.Lemmas.Consumers.Monadic
-public import Std.Data.Iterators.Producers.Monadic.List
+public import Init.Data.Iterators.Lemmas.Producers.Monadic.List
 public import Std.Data.Iterators.Lemmas.Equivalence.Basic
 
-@[expose] public section
-
-/-!
-# Lemmas about list iterators
-
-This module provides lemmas about the interactions of `List.iterM` with `IterM.step` and various
-collectors.
--/
-
 namespace Std.Iterators
 open Std.Internal
 
 variable {m : Type w → Type w'} {n : Type w → Type w''} [Monad m] {β : Type w}
 
-@[simp]
-theorem _root_.List.step_iterM_nil :
-    (([] : List β).iterM m).step = pure (.deflate ⟨.done, rfl⟩) := by
-  simp only [IterM.step, Iterator.step]; rfl
-
-@[simp]
-theorem _root_.List.step_iterM_cons {x : β} {xs : List β} :
-    ((x :: xs).iterM m).step = pure (.deflate ⟨.yield (xs.iterM m) x, rfl⟩) := by
-  simp only [List.iterM, IterM.step, Iterator.step]; rfl
-
-theorem _root_.List.step_iterM {l : List β} :
-    (l.iterM m).step = match l with
-      | [] => pure (.deflate ⟨.done, rfl⟩)
-      | x :: xs => pure (.deflate ⟨.yield (xs.iterM m) x, rfl⟩) := by
-  cases l <;> simp [List.step_iterM_cons, List.step_iterM_nil]
-
-theorem ListIterator.toArrayMapped_iterM [Monad n] [LawfulMonad n]
-    {β : Type w} {γ : Type w} {lift : ⦃δ : Type w⦄ → m δ → n δ}
-    [LawfulMonadLiftFunction lift] {f : β → n γ} {l : List β} :
-    IteratorCollect.toArrayMapped lift f (l.iterM m) (m := m) = List.toArray <$> l.mapM f := by
-  rw [LawfulIteratorCollect.toArrayMapped_eq]
-  induction l with
-  | nil =>
-    rw [IterM.DefaultConsumers.toArrayMapped_eq_match_step]
-    simp [List.step_iterM_nil, LawfulMonadLiftFunction.lift_pure]
-  | cons x xs ih =>
-    rw [IterM.DefaultConsumers.toArrayMapped_eq_match_step]
-    simp [List.step_iterM_cons, List.mapM_cons, pure_bind, ih, LawfulMonadLiftFunction.lift_pure]
-
-@[simp]
-theorem _root_.List.toArray_iterM [LawfulMonad m] {l : List β} :
-    (l.iterM m).toArray = pure l.toArray := by
-  simp only [IterM.toArray, ListIterator.toArrayMapped_iterM]
-  rw [List.mapM_pure, map_pure, List.map_id']
-
-@[simp]
-theorem _root_.List.toList_iterM [LawfulMonad m] {l : List β} :
-    (l.iterM m).toList = pure l := by
-  rw [← IterM.toList_toArray, List.toArray_iterM, map_pure, List.toList_toArray]
-
-@[simp]
-theorem _root_.List.toListRev_iterM [LawfulMonad m] {l : List β} :
-    (l.iterM m).toListRev = pure l.reverse := by
-  simp [IterM.toListRev_eq, List.toList_iterM]
-
-section Equivalence
-
 -- We don't want to pollute `List` with this rarely used lemma.
-theorem ListIterator.stepAsHetT_iterM [LawfulMonad m] {l : List β} :
+public theorem ListIterator.stepAsHetT_iterM [LawfulMonad m] {l : List β} :
     (l.iterM m).stepAsHetT = (match l with
       | [] => pure .done
       | x :: xs => pure (.yield (xs.iterM m) x)) := by
@@ -92,6 +35,4 @@ theorem ListIterator.stepAsHetT_iterM [LawfulMonad m] {l : List β} :
     simp only [IterM.step, Iterator.step, pure_bind]
     cases l <;> simp [Pure.pure, toIterM]
 
-end Equivalence
-
 end Std.Iterators

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

@@ -7,7 +7,7 @@ module
 
 prelude
 public import Std.Data.Iterators.Producers.Repeat
-public import Std.Data.Iterators.Lemmas.Combinators.Take
+public import Init.Data.Iterators.Lemmas.Combinators.Take
 
 @[expose] public section
 

src/Std/Data/Iterators/Producers.lean

@@ -9,7 +9,6 @@ prelude
 public import Std.Data.Iterators.Producers.Monadic
 public import Std.Data.Iterators.Producers.Array
 public import Std.Data.Iterators.Producers.Empty
-public import Std.Data.Iterators.Producers.List
 public import Std.Data.Iterators.Producers.Range
 public import Std.Data.Iterators.Producers.Repeat
 public import Std.Data.Iterators.Producers.Slice

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

@@ -8,4 +8,3 @@ module
 prelude
 public import Std.Data.Iterators.Producers.Monadic.Array
 public import Std.Data.Iterators.Producers.Monadic.Empty
-public import Std.Data.Iterators.Producers.Monadic.List

tests/lean/run/slice.lean

@@ -33,3 +33,35 @@ example : #[1, 1, 1][0...2].size = 2 := by native_decide
 -- Verify that subarray iterators are universe polymorphic
 def f (_ : Type) : Nat := 1
 example : #[Nat, Int][*...1].toList.map f = [1] := by native_decide
+
+
+example : [1, 2, 3][*...*].toList = [1, 2, 3] := by native_decide
+
+example : [1, 2, 3][*...2].toList = [1, 2] := by native_decide
+
+example : [1, 2, 3][*...<2].toList = [1, 2] := by native_decide
+
+example : [1, 2, 3][*...=1].toList = [1, 2] := by native_decide
+
+example : [1, 2, 3][0<...*].toList = [2, 3] := by native_decide
+
+example : [1, 2, 3][0<...2].toList = [2] := by native_decide
+
+example : [1, 2, 3][0<...<2].toList = [2] := by native_decide
+
+example : [1, 2, 3][0<...=1].toList = [2] := by native_decide
+
+example : [1, 2, 3][1...*].toList = [2, 3] := by native_decide
+
+example : [1, 2, 3][1...2].toList = [2] := by native_decide
+
+example : [1, 2, 3][1...<2].toList = [2] := by native_decide
+
+example : [1, 2, 3][1...=1].toList = [2] := by native_decide
+
+example : [1, 2, 3][1...<10].size = 2 := by native_decide
+
+example : [1, 1, 1][0...2].size = 2 := by native_decide
+
+-- Verify that list slice iterators are universe polymorphic
+example : [Nat, Int][*...1].toList.map f = [1] := by native_decide