feat: remove Finite conditions from iterator consumers relying on a new fixpoint combinator (#11038)

This PR introduces a new fixpoint combinator,
`WellFounded.extrinsicFix`. A termination proof, if provided at all, can
be given extrinsically, i.e., looking at the term from the outside, and
is only required if one intends to formally verify the behavior of the
fixpoint. The new combinator is then applied to the iterator API.
Consumers such as `toList` or `ForIn` no longer require a proof that the
underlying iterator is finite. If one wants to ensure the termination of
them intrinsically, there are strictly terminating variants available
as, for example, `it.ensureTermination.toList` instead of `it.toList`.

Author: datokrat

src/Init/Data/Iterators/Basic.lean

@@ -393,6 +393,16 @@ abbrev IterM.Step {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator
     (it : IterM (α := α) m β) :=
   PlausibleIterStep it.IsPlausibleStep
 
+/--
+Makes a single step with the given iterator `it`, potentially emitting a value and providing a
+succeeding iterator. If this function is used recursively, termination can sometimes be proved with
+the termination measures `it.finitelyManySteps` and `it.finitelyManySkips`.
+-/
+@[always_inline, inline, expose]
+def IterM.step {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β]
+    (it : IterM (α := α) m β) : m (Shrink it.Step) :=
+  Iterator.step it
+
 /--
 Asserts that a certain output value could plausibly be emitted by the given iterator in its next
 step.
@@ -420,16 +430,6 @@ def IterM.IsPlausibleSkipSuccessorOf {α : Type w} {m : Type w → Type w'} {β
     [Iterator α m β] (it' it : IterM (α := α) m β) : Prop :=
   it.IsPlausibleStep (.skip it')
 
-/--
-Makes a single step with the given iterator `it`, potentially emitting a value and providing a
-succeeding iterator. If this function is used recursively, termination can sometimes be proved with
-the termination measures `it.finitelyManySteps` and `it.finitelyManySkips`.
--/
-@[always_inline, inline, expose]
-def IterM.step {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β]
-    (it : IterM (α := α) m β) : m (Shrink it.Step) :=
-  Iterator.step it
-
 end Monadic
 
 section Pure
@@ -717,6 +717,15 @@ def IterM.finitelyManySteps {α : Type w} {m : Type w → Type w'} {β : Type w}
     [Finite α m] (it : IterM (α := α) m β) : IterM.TerminationMeasures.Finite α m :=
   ⟨it⟩
 
+/--
+Termination measure to be used in well-founded recursive functions recursing over a finite iterator
+(see also `Finite`).
+-/
+@[expose]
+def IterM.finitelyManySteps! {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β]
+    (it : IterM (α := α) m β) : IterM.TerminationMeasures.Finite α m :=
+  ⟨it⟩
+
 /--
 This theorem is used by a `decreasing_trivial` extension. It powers automatic termination proofs
 with `IterM.finitelyManySteps`.

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

@@ -91,21 +91,11 @@ 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 :=
   .defaultImplementation
 
-instance Attach.instIteratorLoopPartial {α β : Type w} {m : Type w → Type w'} [Monad m]
-    {n : Type x → Type x'} [Monad n] {P : β → Prop} [Iterator α m β] :
-    IteratorLoopPartial (Attach α m P) m n :=
-  .defaultImplementation
-
 end Types
 
 /--

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

@@ -221,25 +221,11 @@ 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 α}
-    {f : β → PostconditionT n (Option γ)} [Finite α m] :
-    IteratorLoop (FilterMap α m n lift f) n o :=
-  .defaultImplementation
-
-instance FilterMap.instIteratorLoopPartial {α β γ : 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 α}
     {f : β → PostconditionT n (Option γ)} :
-    IteratorLoopPartial (FilterMap α m n lift f) n o :=
+    IteratorLoop (FilterMap α m n lift f) n o :=
   .defaultImplementation
 
 /--
@@ -249,7 +235,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₁ (α := _)⟩
@@ -259,32 +245,13 @@ 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 α}
     {f : β → PostconditionT n γ} :
     IteratorLoop (Map α m n lift f) n o :=
   .defaultImplementation
 
-instance Map.instIteratorLoopPartial {α β γ : 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 α}
-    {f : β → PostconditionT n γ} :
-    IteratorLoopPartial (Map α m n lift f) n o :=
-  .defaultImplementation
-
 /--
 *Note: This is a very general combinator that requires an advanced understanding of monads, dependent
 types and termination proofs. The variants `map` and `mapM` are easier to use and sufficient

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

@@ -33,7 +33,7 @@ public structure Flatten (α α₂ β : Type w) (m) where
 /--
 Internal iterator combinator that is used to implement all `flatMap` variants
 -/
-@[always_inline]
+@[always_inline, inline]
 def IterM.flattenAfter {α α₂ β : Type w} {m : Type w → Type w'} [Monad m]
     [Iterator α m (IterM (α := α₂) m β)] [Iterator α₂ m β]
     (it₁ : IterM (α := α) m (IterM (α := α₂) m β)) (it₂ : Option (IterM (α := α₂) m β)) :=
@@ -75,7 +75,7 @@ iterator.
 
 For each value emitted by the outer iterator `it₁`, this combinator calls `f`.
 -/
-@[always_inline]
+@[always_inline, inline]
 public def IterM.flatMapAfterM {α : Type w} {β : Type w} {α₂ : Type w}
     {γ : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β] [Iterator α₂ m γ]
     (f : β → m (IterM (α := α₂) m γ)) (it₁ : IterM (α := α) m β) (it₂ : Option (IterM (α := α₂) m γ)) :=
@@ -114,7 +114,7 @@ This combinator incurs an additional O(1) cost with each output of `it` or an in
 
 For each value emitted by the outer iterator `it`, this combinator calls `f`.
 -/
-@[always_inline, expose]
+@[always_inline, inline, expose]
 public def IterM.flatMapM {α : Type w} {β : Type w} {α₂ : Type w}
     {γ : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β] [Iterator α₂ m γ]
     (f : β → m (IterM (α := α₂) m γ)) (it : IterM (α := α) m β) :=
@@ -156,7 +156,7 @@ iterator.
 
 For each value emitted by the outer iterator `it₁`, this combinator calls `f`.
 -/
-@[always_inline]
+@[always_inline, inline]
 public def IterM.flatMapAfter {α : Type w} {β : Type w} {α₂ : Type w}
     {γ : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β] [Iterator α₂ m γ]
     (f : β → IterM (α := α₂) m γ) (it₁ : IterM (α := α) m β) (it₂ : Option (IterM (α := α₂) m γ)) :=
@@ -195,7 +195,7 @@ This combinator incurs an additional O(1) cost with each output of `it` or an in
 
 For each value emitted by the outer iterator `it`, this combinator calls `f`.
 -/
-@[always_inline, expose]
+@[always_inline, inline, expose]
 public def IterM.flatMap {α : Type w} {β : Type w} {α₂ : Type w}
     {γ : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β] [Iterator α₂ m γ]
     (f : β → IterM (α := α₂) m γ) (it : IterM (α := α) m β) :=
@@ -370,16 +370,8 @@ 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
 
-public instance Flatten.instIteratorLoopPartial [Monad m] [Monad n] [Iterator α m (IterM (α := α₂) m β)]
-    [Iterator α₂ m β] : IteratorLoopPartial (Flatten α α₂ β m) m n :=
-  .defaultImplementation
-
 end Std.Iterators

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

@@ -208,16 +208,8 @@ instance Take.instIteratorCollect {n : Type w → Type w'} [Monad m] [Monad n] [
     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/Monadic/ULift.lean

@@ -128,18 +128,10 @@ instance Types.ULiftIterator.instIteratorLoop {o : Type x → Type x'} [Monad n]
     IteratorLoop (ULiftIterator α m n β lift) n o :=
   .defaultImplementation
 
-instance Types.ULiftIterator.instIteratorLoopPartial {o : Type x → Type x'} [Monad n] [Monad o] [Iterator α m β] :
-    IteratorLoopPartial (ULiftIterator α m n β lift) n o :=
-  .defaultImplementation
-
 instance Types.ULiftIterator.instIteratorCollect [Monad n] [Monad o] [Iterator α m β] :
     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
-
 /--
 Transforms an `m`-monadic iterator with values in `β` into an `n`-monadic iterator with
 values in `ULift β`. Requires a `MonadLift m (ULiftT n)` instance.

src/Init/Data/Iterators/Consumers.lean

@@ -11,5 +11,6 @@ public import Init.Data.Iterators.Consumers.Access
 public import Init.Data.Iterators.Consumers.Collect
 public import Init.Data.Iterators.Consumers.Loop
 public import Init.Data.Iterators.Consumers.Partial
+public import Init.Data.Iterators.Consumers.Total
 
 public import Init.Data.Iterators.Consumers.Stream

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

@@ -7,6 +7,7 @@ module
 
 prelude
 public import Init.Data.Iterators.Consumers.Partial
+public import Init.Data.Iterators.Consumers.Total
 public import Init.Data.Iterators.Consumers.Monadic.Collect
 
 @[expose] public section
@@ -21,40 +22,113 @@ 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]
+/--
+Traverses the given iterator and stores the emitted values in an array.
+
+If the iterator is not finite, this function might run forever. The variant
+`it.ensureTermination.toArray` always terminates after finitely many steps.
+-/
+@[always_inline, inline]
 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]
+/--
+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 Iter.toArray (since := "2025-12-04")]
 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.toArray
+
+/--
+Traverses the given iterator and stores the emitted values in an array.
 
-@[always_inline, inline, inherit_doc IterM.toListRev]
+This variant terminates after finitely many steps and requires a proof that the iterator is
+finite. If such a proof is not available, consider using `Iter.toArray`.
+-/
+@[always_inline, inline]
+def Iter.Total.toArray {α : Type w} {β : Type w}
+    [Iterator α Id β] [Finite α Id] [IteratorCollect α Id Id] (it : Iter.Total (α := α) β) :
+    Array β :=
+  it.it.toArray
+
+/--
+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`.
+
+If the iterator is not finite, this function might run forever. The variant
+`it.ensureTermination.toListRev` always terminates after finitely many steps.
+-/
+@[always_inline, inline]
 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]
+/--
+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 is deprecated. Instead of `it.allowNontermination.toListRev`, use `it.toListRev`.
+-/
+@[always_inline, inline, deprecated Iter.toListRev (since := "2025-12-04")]
 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]
+/--
+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 variant terminates after finitely many steps and requires a proof that the iterator is
+finite. If such a proof is not available, consider using `Iter.toListRev`.
+-/
+@[always_inline, inline]
+def Iter.Total.toListRev {α : Type w} {β : Type w}
+    [Iterator α Id β] [Finite α Id] (it : Iter.Total (α := α) β) : List β :=
+  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`.
+
+If the iterator is not finite, this function might run forever. The variant
+`it.ensureTermination.toList` always terminates after finitely many steps.
+-/
+@[always_inline, inline]
 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]
+/--
+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 is deprecated. Instead of `it.allowNontermination.toList`, use `it.toList`.
+-/
+@[always_inline, deprecated Iter.toList (since := "2025-12-04")]
 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.toList
+
+/--
+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 variant terminates after finitely many steps and requires a proof that the iterator is
+finite. If such a proof is not available, consider using `Iter.toList`.
+-/
+@[always_inline, inline]
+def Iter.Total.toList {α : Type w} {β : Type w}
+    [Iterator α Id β] [Finite α Id] [IteratorCollect α Id Id] (it : Iter.Total (α := α) β) :
+    List β :=
+  it.it.toList
 
 end Std.Iterators