extrinsic toList and toArray

Author: datokrat

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

@@ -93,11 +93,6 @@ instance Attach.instIteratorCollect {α β : Type w} {m : Type w → Type w'} [M
     IteratorCollect (Attach α m P) m n :=
   .defaultImplementation
 
-instance Attach.instIteratorCollectPartial {α β : Type w} {m : Type w → Type w'} [Monad m]
-    [Monad n] {P : β → Prop} [Iterator α m β] :
-    IteratorCollectPartial (Attach α m P) m n :=
-  .defaultImplementation
-
 instance Attach.instIteratorLoop {α β : Type w} {m : Type w → Type w'} [Monad m]
     {n : Type x → Type x'} [Monad n] {P : β → Prop} [Iterator α m β] :
     IteratorLoop (Attach α m P) m n :=

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

@@ -223,13 +223,6 @@ instance {α β γ : Type w} {m : Type w → Type w'}
     IteratorCollect (FilterMap α m n lift f) n o :=
   .defaultImplementation
 
-instance {α β γ : Type w} {m : Type w → Type w'}
-    {n : Type w → Type w''} {o : Type w → Type x} [Monad n] [Monad o] [Iterator α m β]
-    {lift : ⦃α : Type w⦄ → m α → n α}
-    {f : β → PostconditionT n (Option γ)} [Finite α m] :
-    IteratorCollectPartial (FilterMap α m n lift f) n o :=
-  .defaultImplementation
-
 instance FilterMap.instIteratorLoop {α β γ : Type w} {m : Type w → Type w'}
     {n : Type w → Type w''} {o : Type x → Type x'}
     [Monad n] [Monad o] [Iterator α m β] {lift : ⦃α : Type w⦄ → m α → n α}
@@ -251,7 +244,7 @@ instance FilterMap.instIteratorLoopPartial {α β γ : Type w} {m : Type w → T
 instance Map.instIteratorCollect {α β γ : Type w} {m : Type w → Type w'}
     {n : Type w → Type w''} {o : Type w → Type x} [Monad n] [Monad o] [Iterator α m β]
     {lift₁ : ⦃α : Type w⦄ → m α → n α}
-    {f : β → PostconditionT n γ} [IteratorCollect α m o] [Finite α m] :
+    {f : β → PostconditionT n γ} [IteratorCollect α m o] :
     IteratorCollect (Map α m n lift₁ f) n o where
   toArrayMapped lift₂ _ g it :=
     letI : MonadLift m n := ⟨lift₁ (α := _)⟩
@@ -261,18 +254,6 @@ instance Map.instIteratorCollect {α β γ : Type w} {m : Type w → Type w'}
       (fun x => do g (← (f x).operation))
       it.internalState.inner (m := m)
 
-@[no_expose]
-instance Map.instIteratorCollectPartial {α β γ : Type w} {m : Type w → Type w'}
-    {n : Type w → Type w''} {o : Type w → Type x} [Monad n] [Monad o] [Iterator α m β]
-    {lift₁ : ⦃α : Type w⦄ → m α → n α}
-    {f : β → PostconditionT n γ} [IteratorCollectPartial α m o] :
-    IteratorCollectPartial (Map α m n lift₁ f) n o where
-  toArrayMappedPartial lift₂ _ g it :=
-    IteratorCollectPartial.toArrayMappedPartial
-      (lift := fun ⦃_⦄ a => lift₂ (lift₁ a))
-      (fun x => do g (← lift₂ (f x).operation))
-      it.internalState.inner (m := m)
-
 instance Map.instIteratorLoop {α β γ : Type w} {m : Type w → Type w'}
     {n : Type w → Type w''} {o : Type x → Type x'} [Monad n] [Monad o] [Iterator α m β]
     {lift : ⦃α : Type w⦄ → m α → n α}

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

@@ -370,10 +370,6 @@ public instance Flatten.instIteratorCollect [Monad m] [Monad n] [Iterator α m (
     [Iterator α₂ m β] : IteratorCollect (Flatten α α₂ β m) m n :=
   .defaultImplementation
 
-public instance Flatten.instIteratorCollectPartial [Monad m] [Monad n] [Iterator α m (IterM (α := α₂) m β)]
-    [Iterator α₂ m β] : IteratorCollectPartial (Flatten α α₂ β m) m n :=
-  .defaultImplementation
-
 public instance Flatten.instIteratorLoop [Monad m] [Monad n] [Iterator α m (IterM (α := α₂) m β)]
     [Iterator α₂ m β] : IteratorLoop (Flatten α α₂ β m) m n :=
   .defaultImplementation

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

@@ -137,10 +137,6 @@ instance Types.ULiftIterator.instIteratorCollect [Monad n] [Monad o] [Iterator 
     IteratorCollect (ULiftIterator α m n β lift) n o :=
   .defaultImplementation
 
-instance Types.ULiftIterator.instIteratorCollectPartial {o} [Monad n] [Monad o] [Iterator α m β] :
-    IteratorCollectPartial (ULiftIterator α m n β lift) n o :=
-  .defaultImplementation
-
 instance Types.ULiftIterator.instIteratorSize [Monad n] [Iterator α m β] [IteratorSize α m]
     [Finite (ULiftIterator α m n β lift) n] :
     IteratorSize (ULiftIterator α m n β lift) n :=

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

@@ -30,14 +30,15 @@ namespace Std.Iterators
 
 @[always_inline, inline, inherit_doc IterM.toArray]
 def Iter.toArray {α : Type w} {β : Type w}
-    [Iterator α Id β] [Finite α Id] [IteratorCollect α Id Id] (it : Iter (α := α) β) : Array β :=
+    [Iterator α Id β] [IteratorCollect α Id Id] (it : Iter (α := α) β) : Array β :=
   it.toIterM.toArray.run
 
-@[always_inline, inline, inherit_doc IterM.Partial.toArray]
+@[always_inline, inline, inherit_doc IterM.Partial.toArray, deprecated Iter.toArray (since := "2025-10-15")]
 def Iter.Partial.toArray {α : Type w} {β : Type w}
-    [Iterator α Id β] [IteratorCollectPartial α Id Id] (it : Iter.Partial (α := α) β) : Array β :=
-  it.it.toIterM.allowNontermination.toArray.run
+    [Iterator α Id β] [IteratorCollect α Id Id] (it : Iter.Partial (α := α) β) : Array β :=
+  it.it.toIterM.toArray.run
 
+-- TODO:
 @[always_inline, inline, inherit_doc IterM.toListRev]
 def Iter.toListRev {α : Type w} {β : Type w}
     [Iterator α Id β] [Finite α Id] (it : Iter (α := α) β) : List β :=
@@ -50,12 +51,12 @@ def Iter.Partial.toListRev {α : Type w} {β : Type w}
 
 @[always_inline, inline, inherit_doc IterM.toList]
 def Iter.toList {α : Type w} {β : Type w}
-    [Iterator α Id β] [Finite α Id] [IteratorCollect α Id Id] (it : Iter (α := α) β) : List β :=
+    [Iterator α Id β] [IteratorCollect α Id Id] (it : Iter (α := α) β) : List β :=
   it.toIterM.toList.run
 
-@[always_inline, inline, inherit_doc IterM.Partial.toList]
+@[always_inline, inline, inherit_doc IterM.Partial.toList, deprecated Iter.toList (since := "2025-10-15")]
 def Iter.Partial.toList {α : Type w} {β : Type w}
-    [Iterator α Id β] [IteratorCollectPartial α Id Id] (it : Iter.Partial (α := α) β) : List β :=
-  it.it.toIterM.allowNontermination.toList.run
+    [Iterator α Id β] [IteratorCollect α Id Id] (it : Iter.Partial (α := α) β) : List β :=
+  it.it.toIterM.toList.run
 
 end Std.Iterators

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

@@ -8,6 +8,7 @@ module
 prelude
 public import Init.Data.Iterators.Consumers.Monadic.Partial
 public import Init.Data.Iterators.Internal.LawfulMonadLiftFunction
+public import Init.Internal.ExtrinsicTermination
 
 @[expose] public section
 
@@ -51,25 +52,7 @@ class IteratorCollect (α : Type w) (m : Type w → Type w') (n : Type w → Typ
   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] :
-    (lift : ⦃δ : Type w⦄ → m δ → n δ) → {γ : Type w} → (β → n γ) → IterM (α := α) m β → n (Array γ)
-
-/--
-`IteratorCollectPartial α m` provides efficient implementations of collectors for `α`-based
-iterators. Right now, it is limited to a potentially optimized partial `toArray` implementation.
-
-This class is experimental and users of the iterator API should not explicitly depend on it.
-They can, however, assume that consumers that require an instance will work for all iterators
-provided by the standard library.
--/
-class IteratorCollectPartial (α : Type w) (m : Type w → Type w') (n : 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 :
+  toArrayMapped :
     (lift : ⦃δ : Type w⦄ → m δ → n δ) → {γ : Type w} → (β → n γ) → IterM (α := α) m β → n (Array γ)
 
 end Typeclasses
@@ -82,20 +65,21 @@ 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]
+@[always_inline, inline, no_expose]
 def IterM.DefaultConsumers.toArrayMapped {α β : Type w} {m : Type w → Type w'}
-    {n : Type w → Type w''} [Monad n] [Iterator α m β] [Finite α m]
+    {n : Type w → Type w''} [Monad n] [Iterator α m β]
     (lift : ⦃α : Type w⦄ → m α → n α) {γ : Type w} (f : β → n γ)
     (it : IterM (α := α) m β) : n (Array γ) :=
+  letI : MonadLift m n := ⟨lift (α := _)⟩
   go it #[]
 where
-  @[specialize]
-  go [Monad n] [Finite α m] (it : IterM (α := α) m β) a := letI : MonadLift m n := ⟨lift (α := _)⟩; do
-    match (← it.step).inflate with
-    | .yield it' b _ => go it' (a.push (← f b))
-    | .skip it' _ => go it' a
-    | .done _ => return a
-  termination_by it.finitelyManySteps
+  go it (acc : Array γ) : n (Array γ) :=
+    letI : MonadLift m n := ⟨lift (α := _)⟩
+    extrinsicFix₂ (C₂ := fun _ _ => n (Array γ)) (fun it acc recur => do
+      match (← it.step).inflate.val with
+      | .yield it' out => recur it' (acc.push (← f out))
+      | .skip it' => recur it' acc
+      | .done => return acc) it acc
 
 /--
 This is the default implementation of the `IteratorLoop` class.
@@ -110,7 +94,8 @@ def IteratorCollect.defaultImplementation {α β : Type w} {m : Type w → Type
   toArrayMapped := IterM.DefaultConsumers.toArrayMapped
 
 /--
-Asserts that a given `IteratorCollect` instance is equal to `IteratorCollect.defaultImplementation`.
+Asserts that a given `IteratorCollect` instance is equal to `IteratorCollect.defaultImplementation`
+*if the underlying iterator is finite*.
 (Even though equal, the given instance might be vastly more efficient.)
 -/
 class LawfulIteratorCollect (α : Type w) (m : Type w → Type w') (n : Type w → Type w'')
@@ -135,65 +120,27 @@ instance (α β : Type w) (m : Type w → Type w') (n : Type w → Type w'') [Mo
   letI : IteratorCollect α m n := .defaultImplementation
   ⟨fun _ => rfl⟩
 
-/--
-This is an internal function used in `IteratorCollectPartial.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]
-partial def IterM.DefaultConsumers.toArrayMappedPartial {α β : 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 γ)
-    (it : IterM (α := α) m β) : n (Array γ) :=
-  go it #[]
-where
-  @[specialize]
-  go [Monad n] (it : IterM (α := α) m β) a := letI : MonadLift m n := ⟨lift⟩; do
-    match (← it.step).inflate with
-    | .yield it' b _ => go it' (a.push (← f b))
-    | .skip it' _ => go it' a
-    | .done _ => return a
-
-/--
-This is the default implementation of the `IteratorLoopPartial` class.
-It simply iterates through the iterator using `IterM.step`, incrementally building up the desired
-data structure. For certain iterators, more efficient implementations are possible and should be
-used instead.
--/
-@[always_inline, inline]
-def IteratorCollectPartial.defaultImplementation {α β : Type w} {m : Type w → Type w'}
-    {n : Type w → Type w''} [Monad n] [Iterator α m β] :
-    IteratorCollectPartial α m n where
-  toArrayMappedPartial := IterM.DefaultConsumers.toArrayMappedPartial
-
 /--
 Traverses the given iterator and stores the emitted values in an array.
-
-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.toArray` instead of `it.toArray`. However, it is not possible to formally
-verify the behavior of the partial variant.
 -/
 @[always_inline, inline]
-def IterM.toArray {α β : Type w} {m : Type w → Type w'} [Monad m]
-    [Iterator α m β] [Finite α m] [IteratorCollect α m m]
-    (it : IterM (α := α) m β) : m (Array β) :=
+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
 
 /--
 Traverses the given iterator and stores the emitted values in an array.
 
-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.toArray` instead.
+This function is deprecated. Instead of `it.allowNontermination.toArray`, use `it.toArray`.
 -/
-@[always_inline, inline]
+@[always_inline, 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 β) [IteratorCollectPartial α m m] : m (Array β) :=
-  IteratorCollectPartial.toArrayMappedPartial (fun ⦃_⦄ => id) pure it.it
+    [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`.
@@ -237,28 +184,22 @@ where
 /--
 Traverses the given iterator and stores the emitted values in a list. Because
 lists are prepend-only, `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.toList` instead of `it.toList`. However, it is not possible to
-formally verify the behavior of the partial variant.
 -/
 @[always_inline, inline]
 def IterM.toList {α : Type w} {m : Type w → Type w'} [Monad m] {β : Type w}
-    [Iterator α m β] [Finite α m] [IteratorCollect α m m] (it : IterM (α := α) m β) : m (List β) :=
+    [Iterator α m β] [IteratorCollect α m m] (it : IterM (α := α) m β) : m (List β) :=
   Array.toList <$> IterM.toArray it
 
 /--
 Traverses the given iterator and stores the emitted values in a list. Because
 lists are prepend-only, `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.toList` instead.
+This function is deprecated. Instead of `it.allowNontermination.toList`, use `it.toList`.
 -/
-@[always_inline, inline]
+@[always_inline, 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 β) [IteratorCollectPartial α m m] :
+    [Iterator α m β] (it : IterM.Partial (α := α) m β) [IteratorCollect α m m] :
     m (List β) :=
-  Array.toList <$> it.toArray
+  Array.toList <$> it.it.toArray
 
 end Std.Iterators

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

@@ -489,13 +489,8 @@ theorem IterM.toList_map {α β β' : Type w} {m : Type w → Type w'} [Monad m]
   · simp [instIteratorMap, inferInstanceAs]
     congr
     simp
-  · refine heq_of_eqRec_eq ?_ rfl
-    congr
+  · congr
     simp only [Map, PostconditionT.map_pure, Function.comp_apply]
-    simp only [instIteratorMap, inferInstanceAs, Function.comp_apply]
-    congr
-    simp
-  · simp [Map]
   · simp only [instIteratorMap, inferInstanceAs, Function.comp_apply]
     congr
     simp

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

@@ -14,25 +14,53 @@ import all Init.Data.Iterators.Consumers.Monadic.Collect
 public section
 
 namespace Std.Iterators
+open Std.Internal
 
 variable {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''}
   {lift : ⦃δ : Type w⦄ → m δ → n δ} {f : β → n γ} {it : IterM (α := α) m β}
 
-theorem IterM.DefaultConsumers.toArrayMapped.go.aux₁ [Monad n] [LawfulMonad n] [Iterator α m β]
-    [Finite α m] {b : γ} {bs : Array γ} :
+private theorem IterM.DefaultConsumers.toArrayMapped.go_eq [Monad n] [Iterator α m β]
+    [Finite α m] {acc : Array γ} :
+    letI : MonadLift m n := ⟨lift (δ := _)⟩
+    go lift f it acc (m := m) = (do
+      match (← it.step).inflate.val with
+      | .yield it' out => go lift f it' (acc.push (← f out))
+      | .skip it' => go lift f it' acc
+      | .done => return acc) := by
+  letI : MonadLift m n := ⟨lift (δ := _)⟩
+  rw [toArrayMapped.go, extrinsicFix₂_eq]
+  · apply bind_congr; intro step
+    cases step.inflate using PlausibleIterStep.casesOn
+    · simp only
+      apply bind_congr; intro fx
+      simp [go]
+    · simp [go]
+    · simp
+  · refine ⟨?r, ?F, ?wf, ?h⟩
+    · 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' (acc.push (← f out)) (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
+
+private theorem IterM.DefaultConsumers.toArrayMapped.go.aux₁ [Monad n] [LawfulMonad n]
+    [Iterator α m β] [Finite α m] {b : γ} {bs : Array γ} :
     IterM.DefaultConsumers.toArrayMapped.go lift f it (#[b] ++ bs) (m := m) =
       (#[b] ++ ·) <$> IterM.DefaultConsumers.toArrayMapped.go lift f it bs (m := m) := by
-  induction it, bs using IterM.DefaultConsumers.toArrayMapped.go.induct with | _ it bs ih₁ ih₂
-  rw [go, map_eq_pure_bind, go, bind_assoc]
-  apply bind_congr
-  intro step
-  split
-  · simp [ih₁ _ _ ‹_›]
-  · simp [ih₂ _ ‹_›]
-  · simp
+  induction it using IterM.inductSteps generalizing bs with | step it ihy ihs
+  rw [go_eq, map_eq_pure_bind, go_eq, bind_assoc]
+  apply bind_congr; intro step
+  cases step.inflate using PlausibleIterStep.casesOn <;> simp (discharger := assumption) [ihy, ihs]
 
-theorem IterM.DefaultConsumers.toArrayMapped.go.aux₂ [Monad n] [LawfulMonad n] [Iterator α m β]
-    [Finite α m] {acc : Array γ} :
+private theorem IterM.DefaultConsumers.toArrayMapped.go.aux₂ [Monad n] [LawfulMonad n]
+    [Iterator α m β] [Finite α m] {acc : Array γ} :
     IterM.DefaultConsumers.toArrayMapped.go lift f it acc (m := m) =
       (acc ++ ·) <$> IterM.DefaultConsumers.toArrayMapped lift f it (m := m) := by
   rw [← Array.toArray_toList (xs := acc)]
@@ -51,7 +79,7 @@ theorem IterM.DefaultConsumers.toArrayMapped_eq_match_step [Monad n] [LawfulMona
         return #[← f out] ++ (← IterM.DefaultConsumers.toArrayMapped lift f it' (m := m))
       | .skip it' => IterM.DefaultConsumers.toArrayMapped lift f it' (m := m)
       | .done => return #[]) := by
-  rw [IterM.DefaultConsumers.toArrayMapped, IterM.DefaultConsumers.toArrayMapped.go]
+  rw [IterM.DefaultConsumers.toArrayMapped, IterM.DefaultConsumers.toArrayMapped.go_eq]
   apply bind_congr
   intro step
   cases step.inflate using PlausibleIterStep.casesOn <;>

src/Init/Data/Iterators/ToIterator.lean

@@ -90,12 +90,6 @@ instance {x : γ} {State : Type w} {iter}
     IteratorCollect (α := i.State) m n :=
   inferInstanceAs <| IteratorCollect (α := State) m n
 
-instance {x : γ} {State : Type w} {iter}
-    [Iterator (α := State) m β] [IteratorCollectPartial State m n] :
-    letI i : ToIterator x m β := .ofM State iter
-    IteratorCollectPartial (α := i.State) m n :=
-  inferInstanceAs <| IteratorCollectPartial (α := State) m n
-
 instance {x : γ} {State : Type w} {iter}
     [Iterator (α := State) m β] [IteratorLoop State m n] :
     letI i : ToIterator x m β := .ofM State iter