feat: lemmas about list iterators (#8384)

This PR provides lemmas about the behavior of `step`, `toArray`,
`toList` and `toListRev` on list iterators created with `List.iter` and
`List.iterM`.

Author: datokrat

src/Std/Data/Iterators/Basic.lean

@@ -183,6 +183,21 @@ def IterStep.mapIterator {α' : Type u'} (f : α → α') : IterStep α β → I
   | .skip it => .skip (f it)
   | .done => .done
 
+@[simp]
+theorem IterStep.mapIterator_yield {α' : Type u'} {f : α → α'} {it : α} {out : β} :
+    (IterStep.yield it out).mapIterator f = IterStep.yield (f it) out :=
+  rfl
+
+@[simp]
+theorem IterStep.mapIterator_skip {α' : Type u'} {f : α → α'} {it : α} :
+    (IterStep.skip it (β := β)).mapIterator f = IterStep.skip (f it) :=
+  rfl
+
+@[simp]
+theorem IterStep.mapIterator_done {α' : Type u'} {f : α → α'} :
+    (IterStep.done (α := α) (β := β)).mapIterator f = IterStep.done :=
+  rfl
+
 @[simp]
 theorem IterStep.mapIterator_mapIterator {α' : Type u'} {α'' : Type u''}
     {f : α → α'} {g : α' → α''} {step : IterStep α β} :

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

@@ -35,6 +35,10 @@ They can, however, assume that consumers that require an instance will work for
 provided by the standard library.
 -/
 class IteratorCollect (α : Type w) (m : Type w → Type w') {β : Type w} [Iterator α m β] where
+  /--
+  Maps the emitted values of an iterator using the given function and collects the results in an
+  `Array`. This is an internal implementation detail. Consider using `it.map f |>.toArray` instead.
+  -/
   toArrayMapped [Finite α m] : ∀ {γ : Type w}, (β → m γ) → IterM (α := α) m β → m (Array γ)
 
 /--
@@ -46,8 +50,13 @@ They can, however, assume that consumers that require an instance will work for
 provided by the standard library.
 -/
 class IteratorCollectPartial
-  (α : Type w) (m : Type w → Type w') {β : Type w} [Iterator α m β] where
-    toArrayMappedPartial : ∀ {γ : Type w}, (β → m γ) → IterM (α := α) m β → m (Array γ)
+    (α : Type w) (m : Type w → Type w') {β : Type w} [Iterator α m β] where
+  /--
+  Maps the emitted values of an iterator using the given function and collects the results in an
+  `Array`. This is an internal implementation detail.
+  Consider using `it.map f |>.allowNontermination.toArray` instead.
+  -/
+  toArrayMappedPartial : ∀ {γ : Type w}, (β → m γ) → IterM (α := α) m β → m (Array γ)
 
 end Typeclasses
 

src/Std/Data/Iterators/Lemmas.lean

@@ -7,3 +7,4 @@ prelude
 import Std.Data.Iterators.Lemmas.Basic
 import Std.Data.Iterators.Lemmas.Monadic
 import Std.Data.Iterators.Lemmas.Consumers
+import Std.Data.Iterators.Lemmas.Producers

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

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

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

@@ -0,0 +1,47 @@
+/-
+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
+import Std.Data.Iterators.Lemmas.Consumers.Collect
+import Std.Data.Iterators.Lemmas.Producers.Monadic.List
+
+/-!
+# Lemmas about list iterators
+
+This module provides lemmas about the interactions of `List.iter` with `Iter.step` and various
+collectors.
+-/
+
+namespace Std.Iterators
+
+variable {β : Type w}
+
+@[simp]
+theorem _root_.List.step_iter_nil :
+    (([] : List β).iter).step = ⟨.done, rfl⟩ := by
+  simp only [Iter.step, IterM.step, Iterator.step]; rfl
+
+@[simp]
+theorem _root_.List.step_iter_cons {x : β} {xs : List β} :
+    ((x :: xs).iter).step = ⟨.yield xs.iter x, rfl⟩ := by
+  simp only [List.iter, List.iterM, IterM.step, Iterator.step]; rfl
+
+@[simp]
+theorem _root_.List.toArray_iter {m : Type w → Type w'} [Monad m] [LawfulMonad m] {l : List β} :
+    l.iter.toArray = l.toArray := by
+  simp [List.iter, List.toArray_iterM, Iter.toArray_eq_toArray_toIterM]
+
+@[simp]
+theorem _root_.List.toList_iter {m : Type w → Type w'} [Monad m] [LawfulMonad m] {l : List β} :
+    l.iter.toList = l := by
+  simp [List.iter, List.toList_iterM]
+
+@[simp]
+theorem _root_.List.toListRev_iter {m : Type w → Type w'} [Monad m] [LawfulMonad m] {l : List β} :
+    l.iter.toListRev = l.reverse := by
+  simp [List.iter, Iter.toListRev_eq_toListRev_toIterM, List.toListRev_iterM]
+
+end Std.Iterators

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

@@ -0,0 +1,7 @@
+/-
+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.Lemmas.Producers.Monadic.List

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

@@ -0,0 +1,60 @@
+/-
+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.Producers.Monadic.List
+import Std.Data.Iterators.Consumers
+import Std.Data.Iterators.Lemmas.Consumers.Monadic
+
+/-!
+# Lemmas about list iterators
+
+This module provides lemmas about the interactions of `List.iterM` with `IterM.step` and various
+collectors.
+-/
+
+namespace Std.Iterators
+
+variable {m : Type w → Type w'} [Monad m] {β : Type w}
+
+@[simp]
+theorem _root_.List.step_iterM_nil :
+    (([] : List β).iterM m).step = pure ⟨.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 ⟨.yield (xs.iterM m) x, rfl⟩ := by
+  simp only [List.iterM, IterM.step, Iterator.step]; rfl
+
+theorem ListIterator.toArrayMapped_toIterM [LawfulMonad m]
+    {β : Type w} {γ : Type w} {f : β → m γ} {l : List β} :
+    IteratorCollect.toArrayMapped f (l.iterM 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]
+  | cons x xs ih =>
+    rw [IterM.DefaultConsumers.toArrayMapped_eq_match_step]
+    simp [List.step_iterM_cons, List.mapM_cons, pure_bind, ih]
+
+@[simp]
+theorem _root_.List.toArray_iterM [LawfulMonad m] {l : List β} :
+    (l.iterM m).toArray = pure l.toArray := by
+  simp only [IterM.toArray, ListIterator.toArrayMapped_toIterM]
+  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