docstring

Author: datokrat

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

@@ -21,41 +21,39 @@ Concretely, the following operations are provided:
 * `Iter.toListRev`, collecting the values in a list in reverse order but more efficiently
 * `Iter.toArray`, collecting the values in an array
 
-Some operations are implemented using the `IteratorCollect` and `IteratorCollectPartial`
-typeclasses.
+Some operations are implemented using the `IteratorCollect` type class.
 -/
 
 namespace Std.Iterators
 
-@[always_inline, inline, inherit_doc IterM.toArray]
+@[always_inline, inherit_doc IterM.toArray]
 def Iter.toArray {α : Type w} {β : Type w}
     [Iterator α Id β] [IteratorCollect α Id Id] (it : Iter (α := α) β) : Array β :=
   it.toIterM.toArray.run
 
-@[always_inline, inline, inherit_doc IterM.Partial.toArray, deprecated Iter.toArray (since := "2025-10-15")]
+@[always_inline, inherit_doc IterM.Partial.toArray, deprecated Iter.toArray (since := "2025-10-15")]
 def Iter.Partial.toArray {α : Type w} {β : Type w}
     [Iterator α Id β] [IteratorCollect α Id Id] (it : Iter.Partial (α := α) β) : Array β :=
-  it.it.toIterM.toArray.run
+  it.it.toArray
 
--- TODO:
-@[always_inline, inline, inherit_doc IterM.toListRev]
+@[always_inline, inherit_doc IterM.toListRev]
 def Iter.toListRev {α : Type w} {β : Type w}
-    [Iterator α Id β] [Finite α Id] (it : Iter (α := α) β) : List β :=
+    [Iterator α Id β] (it : Iter (α := α) β) : List β :=
   it.toIterM.toListRev.run
 
-@[always_inline, inline, inherit_doc IterM.Partial.toListRev]
+@[always_inline, inherit_doc IterM.Partial.toListRev, deprecated Iter.toListRev (since := "2025-10-16")]
 def Iter.Partial.toListRev {α : Type w} {β : Type w}
     [Iterator α Id β] (it : Iter.Partial (α := α) β) : List β :=
-  it.it.toIterM.allowNontermination.toListRev.run
+  it.it.toListRev
 
-@[always_inline, inline, inherit_doc IterM.toList]
+@[always_inline, inherit_doc IterM.toList]
 def Iter.toList {α : Type w} {β : Type w}
     [Iterator α Id β] [IteratorCollect α Id Id] (it : Iter (α := α) β) : List β :=
   it.toIterM.toList.run
 
-@[always_inline, inline, inherit_doc IterM.Partial.toList, deprecated Iter.toList (since := "2025-10-15")]
+@[always_inline, inherit_doc IterM.Partial.toList, deprecated Iter.toList (since := "2025-10-15")]
 def Iter.Partial.toList {α : Type w} {β : Type w}
     [Iterator α Id β] [IteratorCollect α Id Id] (it : Iter.Partial (α := α) β) : List β :=
-  it.it.toIterM.toList.run
+  it.it.toList
 
 end Std.Iterators

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

@@ -23,9 +23,9 @@ Concretely, the following operations are provided:
 * `IterM.toArray`, collecting the values in an array
 
 Some producers and combinators provide specialized implementations. These are captured by the
-`IteratorCollect` and `IteratorCollectPartial` typeclasses. They should be implemented by all
-types of iterators. A default implementation is provided. The typeclass `LawfulIteratorCollect`
-asserts that an `IteratorCollect` instance equals the default implementation.
+`IteratorCollect` type class. They should be implemented by all types of iterators. A default
+implementation is provided. The typeclass `LawfulIteratorCollect` asserts that an `IteratorCollect`
+instance equals the default implementation.
 -/
 
 namespace Std.Iterators
@@ -65,7 +65,7 @@ This is an internal function used in `IteratorCollect.defaultImplementation`.
 It iterates over an iterator and applies `f` whenever a value is emitted before inserting the result
 of `f` into an array.
 -/
-@[always_inline, inline, no_expose]
+@[always_inline, no_expose]
 def IterM.DefaultConsumers.toArrayMapped {α β : Type w} {m : Type w → Type w'}
     {n : Type w → Type w''} [Monad n] [Iterator α m β]
     (lift : ⦃α : Type w⦄ → m α → n α) {γ : Type w} (f : β → n γ)
@@ -88,7 +88,7 @@ It simply iterates through the iterator using `IterM.step`, incrementally buildi
 data structure. For certain iterators, more efficient implementations are possible and should be
 used instead.
 -/
-@[always_inline, inline]
+@[always_inline]
 def IteratorCollect.defaultImplementation {α β : Type w} {m : Type w → Type w'}
     {n : Type w → Type w''} [Monad n] [Iterator α m β] :
     IteratorCollect α m n where
@@ -124,7 +124,7 @@ instance (α β : Type w) (m : Type w → Type w') (n : Type w → Type w'') [Mo
 /--
 Traverses the given iterator and stores the emitted values in an array.
 -/
-@[always_inline, inline]
+@[always_inline]
 def IterM.toArray {α β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β]
     [IteratorCollect α m m] (it : IterM (α := α) m β) : m (Array β) :=
   IteratorCollect.toArrayMapped (fun ⦃_⦄ => id) pure it
@@ -134,59 +134,46 @@ Traverses the given iterator and stores the emitted values in an array.
 
 This function is deprecated. Instead of `it.allowNontermination.toArray`, use `it.toArray`.
 -/
-@[always_inline, inline, deprecated IterM.toArray (since := "2025-10-15")]
+@[always_inline, deprecated IterM.toArray (since := "2025-10-15")]
 def IterM.Partial.toArray {α : Type w} {m : Type w → Type w'} {β : Type w} [Monad m]
     [Iterator α m β] (it : IterM.Partial (α := α) m β) [IteratorCollect α m m] : m (Array β) :=
   it.it.toArray
 
 end ToArray
 
--- TODO:
 /--
 Traverses the given iterator and stores the emitted values in reverse order in a list. Because
 lists are prepend-only, this `toListRev` is usually more efficient that `toList`.
-
-This function requires a `Finite` instance proving that the iterator will finish after a finite
-number of steps. If the iterator is not finite or such an instance is not available, consider using
-`it.allowNontermination.toListRev` instead of `it.toListRev`. However, it is not possible to
-formally verify the behavior of the partial variant.
 -/
-@[inline]
+@[always_inline]
 def IterM.toListRev {α : Type w} {m : Type w → Type w'} [Monad m] {β : Type w}
-    [Iterator α m β] [Finite α m] (it : IterM (α := α) m β) : m (List β) :=
+    [Iterator α m β] (it : IterM (α := α) m β) : m (List β) :=
   go it []
 where
-  go [Finite α m] it bs := do
-    match (← it.step).inflate with
-    | .yield it' b _ => go it' (b :: bs)
-    | .skip it' _ => go it' bs
-    | .done _ => return bs
-  termination_by it.finitelyManySteps
+  @[always_inline]
+  go (it : IterM m β) acc :=
+    extrinsicFix₂ (fun it acc recur => do
+      match (← it.step).inflate with
+      | .yield it' out _ => recur it' (out :: acc)
+      | .skip it' _ => recur it' acc
+      | .done _ => return acc) it acc
 
 /--
 Traverses the given iterator and stores the emitted values in reverse order in a list. Because
 lists are prepend-only, this `toListRev` is usually more efficient that `toList`.
 
-This is a partial, potentially nonterminating, function. It is not possible to formally verify
-its behavior. If the iterator has a `Finite` instance, consider using `IterM.toListRev` instead.
+This function is deprecated. Instead of `it.allowNontermination.toListRev`, use `it.toListRev`.
 -/
-@[always_inline, inline]
+@[always_inline, deprecated IterM.toListRev (since := "2025-10-16")]
 partial def IterM.Partial.toListRev {α : Type w} {m : Type w → Type w'} [Monad m] {β : Type w}
     [Iterator α m β] (it : IterM.Partial (α := α) m β) : m (List β) :=
-  go it.it []
-where
-  @[specialize]
-  go it bs := do
-    match (← it.step).inflate with
-    | .yield it' b _ => go it' (b :: bs)
-    | .skip it' _ => go it' bs
-    | .done _ => return bs
+  it.it.toListRev
 
 /--
 Traverses the given iterator and stores the emitted values in a list. Because
 lists are prepend-only, `toListRev` is usually more efficient that `toList`.
 -/
-@[always_inline, inline]
+@[always_inline]
 def IterM.toList {α : Type w} {m : Type w → Type w'} [Monad m] {β : Type w}
     [Iterator α m β] [IteratorCollect α m m] (it : IterM (α := α) m β) : m (List β) :=
   Array.toList <$> IterM.toArray it
@@ -197,7 +184,7 @@ lists are prepend-only, `toListRev` is usually more efficient that `toList`.
 
 This function is deprecated. Instead of `it.allowNontermination.toList`, use `it.toList`.
 -/
-@[always_inline, inline, deprecated IterM.toList (since := "2025-10-15")]
+@[always_inline, deprecated IterM.toList (since := "2025-10-15")]
 def IterM.Partial.toList {α : Type w} {m : Type w → Type w'} [Monad m] {β : Type w}
     [Iterator α m β] (it : IterM.Partial (α := α) m β) [IteratorCollect α m m] :
     m (List β) :=

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

@@ -121,15 +121,42 @@ theorem IterM.toList_eq_match_step [Monad m] [LawfulMonad m] [Iterator α m β]
   intro step
   split <;> simp
 
+theorem IterM.toListRev.go_eq [Monad m] [LawfulMonad m] [Iterator α m β] [Finite α m]
+    {it : IterM (α := α) m β} {bs : List β} :
+    go it bs = (do
+      match (← it.step).inflate.val with
+      | .yield it' out => go it' (out :: bs)
+      | .skip it' => go it' bs
+      | .done => return bs) := by
+  rw [go, extrinsicFix₂_eq]
+  · apply bind_congr; intro step
+    cases step.inflate using PlausibleIterStep.casesOn <;> simp [go]
+  · refine ⟨?r, ?F, ?wf, ?_⟩
+    · exact InvImage WellFoundedRelation.rel (fun x => x.1.finitelyManySteps)
+    · exact fun it acc G => (do
+        match (← it.step).inflate with
+        | .yield it' out h => G it' (out :: acc) (TerminationMeasures.Finite.rel_of_yield h)
+        | .skip it' h => G it' acc (TerminationMeasures.Finite.rel_of_skip h)
+        | .done _ => return acc)
+    · apply InvImage.wf
+      exact WellFoundedRelation.wf
+    · intro it acc G
+      simp only
+      apply bind_congr; intro step
+      cases step.inflate using PlausibleIterStep.casesOn <;> simp
+
 theorem IterM.toListRev.go.aux₁ [Monad m] [LawfulMonad m] [Iterator α m β] [Finite α m]
     {it : IterM (α := α) m β} {b : β} {bs : List β} :
     IterM.toListRev.go it (bs ++ [b]) = (· ++ [b]) <$> IterM.toListRev.go it bs:= by
-  induction it, bs using IterM.toListRev.go.induct with | _ it bs ih₁ ih₂
-  rw [go, go, map_eq_pure_bind, bind_assoc]
+  induction it using IterM.inductSteps generalizing bs with | step it ihy ihs
+  rw [go_eq, go_eq, map_eq_pure_bind, bind_assoc]
   apply bind_congr
   intro step
-  simp only [List.cons_append] at ih₁
-  split <;> simp [*]
+  cases step.inflate using PlausibleIterStep.casesOn
+  · simpa using ihy ‹_› (bs := _ :: bs)
+  · simpa using ihs ‹_›
+  · simp
+
 
 theorem IterM.toListRev.go.aux₂ [Monad m] [LawfulMonad m] [Iterator α m β] [Finite α m]
     {it : IterM (α := α) m β} {acc : List β} :
@@ -148,7 +175,7 @@ theorem IterM.toListRev_eq_match_step [Monad m] [LawfulMonad m] [Iterator α m 
       | .skip it' => it'.toListRev
       | .done => return []) := by
   simp [IterM.toListRev]
-  rw [toListRev.go]
+  rw [toListRev.go_eq]
   apply bind_congr
   intro step
   cases step.inflate using PlausibleIterStep.casesOn <;> simp [IterM.toListRev.go.aux₂]