lemmas about list iterators

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/Lemmas/Producers/List.lean

@@ -0,0 +1,42 @@
+/-
+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.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}
+
+theorem _root_.List.step_iter_nil :
+    (([] : List β).iter).step = ⟨.done, rfl⟩ := by
+  simp only [Iter.step, IterM.step, Iterator.step]; rfl
+
+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
+
+theorem _root_.List.toArray_iter {m : Type w → Type w'} [Monad m] [LawfulMonad m] {l : List β} :
+    (l.iterM m).toArray = pure l.toArray := by
+  simp only [IterM.toArray, ListIterator.toArrayMapped_eq]
+  rw [List.mapM_pure, map_pure, List.map_id']
+
+theorem _root_.List.toList_iter {m : Type w → Type w'} [Monad m] [LawfulMonad m] {l : List β} :
+    (l.iterM m).toList = pure l := by
+  rw [← IterM.toList_toArray, List.toArray_iterM, map_pure, List.toList_toArray]
+
+theorem _root_.List.toListRev_iter {m : Type w → Type w'} [Monad m] [LawfulMonad m] {l : List β} :
+    (l.iterM m).toListRev = pure l.reverse := by
+  simp [IterM.toListRev_eq, List.toList_iterM]
+
+end Std.Iterators

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

@@ -0,0 +1,55 @@
+/-
+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}
+
+theorem _root_.List.step_iterM_nil :
+    (([] : List β).iterM m).step = pure ⟨.done, rfl⟩ := by
+  simp only [IterM.step, Iterator.step]; rfl
+
+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_eq [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_of_step]
+    simp [List.step_iterM_nil]
+  | cons x xs ih =>
+    rw [IterM.DefaultConsumers.toArrayMapped_of_step]
+    simp [List.step_iterM_cons, List.mapM_cons, pure_bind, ih]
+
+theorem _root_.List.toArray_iterM [LawfulMonad m] {l : List β} :
+    (l.iterM m).toArray = pure l.toArray := by
+  simp only [IterM.toArray, ListIterator.toArrayMapped_eq]
+  rw [List.mapM_pure, map_pure, List.map_id']
+
+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]
+
+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