refactor: replace Iter(M).size with Iter(M).count (#10952)

This PR replaces `Iter(M).size` with the `Iter(M).count`. While the
former used a special `IteratorSize` type class, the latter relies on
`IteratorLoop`. The `IteratorSize` class is deprecated. The PR also
renames lemmas about ranges be replacing `_Rcc` with `_rcc`, `_Rco` with
`_roo` (and so on) in names, in order to be more consistent with the
naming convention.

Author: datokrat

src/Init/Data/Array/Lex/Lemmas.lean

@@ -75,11 +75,11 @@ private theorem cons_lex_cons [BEq α] {lt : α → α → Bool} {a b : α} {xs
     Nat.add_min_add_left, Nat.add_lt_add_iff_left, Std.Rco.forIn'_eq_forIn'_toList]
   conv =>
     lhs; congr; congr
-    rw [cons_lex_cons.forIn'_congr_aux Std.Rco.toList_eq_if rfl (fun _ _ _ => rfl)]
+    rw [cons_lex_cons.forIn'_congr_aux Std.Rco.toList_eq_if_roo rfl (fun _ _ _ => rfl)]
     simp only [bind_pure_comp, map_pure]
     rw [cons_lex_cons.forIn'_congr_aux (if_pos (by omega)) rfl (fun _ _ _ => rfl)]
-  simp only [Std.toList_Roo_eq_toList_Rco_of_isSome_succ? (lo := 0) (h := rfl),
-    Std.PRange.UpwardEnumerable.succ?, Nat.add_comm 1, Std.PRange.Nat.toList_Rco_succ_succ,
+  simp only [Std.toList_roo_eq_toList_rco_of_isSome_succ? (lo := 0) (h := rfl),
+    Std.PRange.UpwardEnumerable.succ?, Nat.add_comm 1, Std.PRange.Nat.toList_rco_succ_succ,
     Option.get_some, List.forIn'_cons, List.size_toArray, List.length_cons, List.length_nil,
     Nat.lt_add_one, getElem_append_left, List.getElem_toArray, List.getElem_cons_zero]
   cases lt a b

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

@@ -106,16 +106,6 @@ instance Attach.instIteratorLoopPartial {α β : Type w} {m : Type w → Type w'
     IteratorLoopPartial (Attach α m P) m n :=
   .defaultImplementation
 
-instance {α β : Type w} {m : Type w → Type w'} [Monad m]
-    {P : β → Prop} [Iterator α m β] [IteratorSize α m] :
-    IteratorSize (Attach α m P) m where
-  size it := IteratorSize.size it.internalState.inner
-
-instance {α β : Type w} {m : Type w → Type w'} [Monad m]
-    {P : β → Prop} [Iterator α m β] [IteratorSizePartial α m] :
-    IteratorSizePartial (Attach α m P) m where
-  size it := IteratorSizePartial.size it.internalState.inner
-
 end Types
 
 /--

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

@@ -604,30 +604,4 @@ def IterM.filter {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [M
     (f : β → Bool) (it : IterM (α := α) m β) :=
   (it.filterMap (fun b => if f b then some b else none) : IterM m β)
 
-instance {α β γ : Type w} {m : Type w → Type w'}
-    {n : Type w → Type w''} [Monad n] [Iterator α m β] {lift : ⦃α : Type w⦄ → m α → n α}
-    {f : β → PostconditionT n (Option γ)} [Finite α m] :
-    IteratorSize (FilterMap α m n lift f) n :=
-  .defaultImplementation
-
-instance {α β γ : Type w} {m : Type w → Type w'}
-    {n : Type w → Type w''} [Monad n] [Iterator α m β] {lift : ⦃α : Type w⦄ → m α → n α}
-    {f : β → PostconditionT n (Option γ)} :
-    IteratorSizePartial (FilterMap α m n lift f) n :=
-  .defaultImplementation
-
-instance {α β γ : Type w} {m : Type w → Type w'}
-    {n : Type w → Type w''} [Monad n] [Iterator α m β]
-    {lift : ⦃α : Type w⦄ → m α → n α}
-    {f : β → PostconditionT n γ} [IteratorSize α m] :
-    IteratorSize (Map α m n lift f) n where
-  size it := lift (IteratorSize.size it.internalState.inner)
-
-instance {α β γ : Type w} {m : Type w → Type w'}
-    {n : Type w → Type w''} [Monad n] [Iterator α m β]
-    {lift : ⦃α : Type w⦄ → m α → n α}
-    {f : β → PostconditionT n γ} [IteratorSizePartial α m] :
-    IteratorSizePartial (Map α m n lift f) n where
-  size it := lift (IteratorSizePartial.size it.internalState.inner)
-
 end Std.Iterators

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

@@ -74,7 +74,7 @@ variable {α : Type u} {m : Type u → Type u'} {n : Type max u v → Type v'}
 /--
 Transforms a step of the base iterator into a step of the `uLift` iterator.
 -/
-@[always_inline, inline]
+@[always_inline, inline, expose]
 def Types.ULiftIterator.Monadic.modifyStep (step : IterStep (IterM (α := α) m β) β) :
     IterStep (IterM (α := ULiftIterator.{v} α m n β lift) n (ULift.{v} β)) (ULift.{v} β) :=
   match step with
@@ -140,15 +140,6 @@ instance Types.ULiftIterator.instIteratorCollectPartial {o} [Monad n] [Monad o]
     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 :=
-  .defaultImplementation
-
-instance Types.ULiftIterator.instIteratorSizePartial [Monad n] [Iterator α m β] [IteratorSize α m] :
-    IteratorSizePartial (ULiftIterator α m n β lift) n :=
-  .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/Loop.lean

@@ -255,28 +255,52 @@ def Iter.Partial.find? {α β : Type w} [Iterator α Id β] [IteratorLoopPartial
     (it : Iter.Partial (α := α) β) (f : β → Bool) : Option β :=
   Id.run (it.findM? (pure <| .up <| f ·))
 
-@[always_inline, inline, expose, inherit_doc IterM.size]
-def Iter.size {α : Type w} {β : Type w} [Iterator α Id β] [IteratorSize α Id]
+/--
+Steps through the whole iterator, counting the number of outputs emitted.
+
+**Performance**:
+
+This function's runtime is linear in the number of steps taken by the iterator.
+-/
+@[always_inline, inline, expose]
+def Iter.count {α : Type w} {β : Type w} [Iterator α Id β] [Finite α Id] [IteratorLoop α Id Id]
     (it : Iter (α := α) β) : Nat :=
-  (IteratorSize.size it.toIterM).run.down
+  it.toIterM.count.run.down
+
+/--
+Steps through the whole iterator, counting the number of outputs emitted.
+
+**Performance**:
 
-@[always_inline, inline, inherit_doc IterM.Partial.size]
-def Iter.Partial.size {α : Type w} {β : Type w} [Iterator α Id β] [IteratorSizePartial α Id]
+This function's runtime is linear in the number of steps taken by the iterator.
+-/
+@[always_inline, inline, expose, deprecated Iter.count (since := "2025-10-29")]
+def Iter.size {α : Type w} {β : Type w} [Iterator α Id β] [Finite α Id] [IteratorLoop α Id Id]
     (it : Iter (α := α) β) : Nat :=
-  (IteratorSizePartial.size it.toIterM).run.down
+   it.count
 
 /--
-`LawfulIteratorSize α m` ensures that the `size` function of an iterator behaves as if it
-iterated over the whole iterator, counting its elements and causing all the monadic side effects
-of the iterations. This is a fairly strong condition for monadic iterators and it will be false
-for many efficient implementations of `size` that compute the size without actually iterating.
+Steps through the whole iterator, counting the number of outputs emitted.
+
+**Performance**:
+
+This function's runtime is linear in the number of steps taken by the iterator.
+-/
+@[always_inline, inline, expose]
+def Iter.Partial.count {α : Type w} {β : Type w} [Iterator α Id β] [IteratorLoopPartial α Id Id]
+    (it : Iter.Partial (α := α) β) : Nat :=
+  it.it.toIterM.allowNontermination.count.run.down
+
+/--
+Steps through the whole iterator, counting the number of outputs emitted.
+
+**Performance**:
 
-This class is experimental and users of the iterator API should not explicitly depend on it.
+This function's runtime is linear in the number of steps taken by the iterator.
 -/
-class LawfulIteratorSize (α : Type w) {β : Type w} [Iterator α Id β] [Finite α Id]
-    [IteratorSize α Id] where
-    size_eq_size_toArray {it : Iter (α := α) β} : it.size =
-      haveI : IteratorCollect α Id Id := .defaultImplementation
-      it.toArray.size
+@[always_inline, inline, expose, deprecated Iter.Partial.count (since := "2025-10-29")]
+def Iter.Partial.size {α : Type w} {β : Type w} [Iterator α Id β] [IteratorLoopPartial α Id Id]
+    (it : Iter.Partial (α := α) β) : Nat :=
+  it.count
 
 end Std.Iterators

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

@@ -88,27 +88,6 @@ class IteratorLoopPartial (α : Type w) (m : Type w → Type w') {β : Type w} [
       (it : IterM (α := α) m β) → γ →
       ((b : β) → it.IsPlausibleIndirectOutput b → (c : γ) → n (ForInStep γ)) → n γ
 
-/--
-`IteratorSize α m` provides an implementation of the `IterM.size` function.
-
-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 IteratorSize (α : Type w) (m : Type w → Type w') {β : Type w} [Iterator α m β] where
-  size : IterM (α := α) m β → m (ULift Nat)
-
-/--
-`IteratorSizePartial α m` provides an implementation of the `IterM.Partial.size` function that
-can be used as `it.allowTermination.size`.
-
-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 IteratorSizePartial (α : Type w) (m : Type w → Type w') {β : Type w} [Iterator α m β] where
-  size : IterM (α := α) m β → m (ULift Nat)
-
 end Typeclasses
 
 /-- Internal implementation detail of the iterator library. -/
@@ -315,7 +294,7 @@ instance {m : Type w → Type w'} {n : Type w → Type w''}
   forM it f := forIn it PUnit.unit (fun out _ => do f out; return .yield .unit)
 
 instance {m : Type w → Type w'} {n : Type w → Type w''}
-    {α : Type w} {β : Type w} [Iterator α m β] [Finite α m] [IteratorLoopPartial α m n]
+    {α : Type w} {β : Type w} [Iterator α m β] [IteratorLoopPartial α m n]
     [MonadLiftT m n] :
     ForM n (IterM.Partial (α := α) m β) β where
   forM it f := forIn it PUnit.unit (fun out _ => do f out; return .yield .unit)
@@ -633,86 +612,58 @@ def IterM.Partial.find? {α β : Type w} {m : Type w → Type w'} [Monad m] [Ite
     m (Option β) :=
   it.findM? (pure <| .up <| f ·)
 
-section Size
+section Count
 
 /--
-This is the implementation of the default instance `IteratorSize.defaultImplementation`.
--/
-@[always_inline, inline]
-def IterM.DefaultConsumers.size {α : Type w} {m : Type w → Type w'} [Monad m] {β : Type w}
-    [Iterator α m β] [IteratorLoop α m m] [Finite α m] (it : IterM (α := α) m β) :
-    m (ULift Nat) :=
-  it.fold (init := .up 0) fun acc _ => .up (acc.down + 1)
+Steps through the whole iterator, counting the number of outputs emitted.
 
-/--
-This is the implementation of the default instance `IteratorSizePartial.defaultImplementation`.
+**Performance**:
+
+This function's runtime is linear in the number of steps taken by the iterator.
 -/
 @[always_inline, inline]
-def IterM.DefaultConsumers.sizePartial {α : Type w} {m : Type w → Type w'} [Monad m] {β : Type w}
-    [Iterator α m β] [IteratorLoopPartial α m m] (it : IterM (α := α) m β) :
-    m (ULift Nat) :=
-  it.allowNontermination.fold (init := .up 0) fun acc _ => .up (acc.down + 1)
+def IterM.count {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β] [Finite α m]
+    [IteratorLoop α m m]
+    [Monad m] (it : IterM (α := α) m β) : m (ULift Nat) :=
+  it.fold (init := .up 0) fun acc _ => .up (acc.down + 1)
 
 /--
-This is the default implementation of the `IteratorSize` class.
-It simply iterates using `IteratorLoop` and counts the elements.
-For certain iterators, more efficient implementations are possible and should be used instead.
--/
-@[always_inline, inline]
-def IteratorSize.defaultImplementation {α β : Type w} {m : Type w → Type w'} [Monad m]
-    [Iterator α m β] [Finite α m] [IteratorLoop α m m] :
-    IteratorSize α m where
-  size := IterM.DefaultConsumers.size
+Steps through the whole iterator, counting the number of outputs emitted.
 
+**Performance**:
 
-/--
-This is the default implementation of the `IteratorSizePartial` class.
-It simply iterates using `IteratorLoopPartial` and counts the elements.
-For certain iterators, more efficient implementations are possible and should be used instead.
+This function's runtime is linear in the number of steps taken by the iterator.
 -/
-@[always_inline, inline]
-instance IteratorSizePartial.defaultImplementation {α β : Type w} {m : Type w → Type w'} [Monad m]
-    [Iterator α m β] [IteratorLoopPartial α m m] :
-    IteratorSizePartial α m where
-  size := IterM.DefaultConsumers.sizePartial
+@[always_inline, inline, deprecated IterM.count (since := "2025-10-29")]
+def IterM.size {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β] [Finite α m]
+    [IteratorLoop α m m]
+    [Monad m] (it : IterM (α := α) m β) : m (ULift Nat) :=
+  it.count
 
 /--
-Computes how many elements the iterator returns. In monadic situations, it is unclear which effects
-are caused by calling `size`, and if the monad is nondeterministic, it is also unclear what the
-returned value should be. The reference implementation, `IteratorSize.defaultImplementation`,
-simply iterates over the whole iterator monadically, counting the number of emitted values.
-An `IteratorSize` instance is considered lawful if it is equal to the reference implementation.
+Steps through the whole iterator, counting the number of outputs emitted.
 
 **Performance**:
 
-Default performance is linear in the number of steps taken by the iterator.
+This function's runtime is linear in the number of steps taken by the iterator.
 -/
 @[always_inline, inline]
-def IterM.size {α : Type} {m : Type → Type w'} {β : Type} [Iterator α m β] [Monad m]
-    (it : IterM (α := α) m β) [IteratorSize α m] : m Nat :=
-  ULift.down <$> IteratorSize.size it
+def IterM.Partial.count {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β]
+    [IteratorLoopPartial α m m] [Monad m] (it : IterM.Partial (α := α) m β) : m (ULift Nat) :=
+  it.fold (init := .up 0) fun acc _ => .up (acc.down + 1)
 
 /--
-Computes how many elements the iterator emits.
-
-With monadic iterators (`IterM`), it is unclear which effects
-are caused by calling `size`, and if the monad is nondeterministic, it is also unclear what the
-returned value should be. The reference implementation, `IteratorSize.defaultImplementation`,
-simply iterates over the whole iterator monadically, counting the number of emitted values.
-An `IteratorSize` instance is considered lawful if it is equal to the reference implementation.
-
-This is the partial version of `size`. It does not require a proof of finiteness and might loop
-forever. It is not possible to verify the behavior in Lean because it uses `partial`.
+Steps through the whole iterator, counting the number of outputs emitted.
 
 **Performance**:
 
-Default performance is linear in the number of steps taken by the iterator.
+This function's runtime is linear in the number of steps taken by the iterator.
 -/
-@[always_inline, inline]
-def IterM.Partial.size {α : Type} {m : Type → Type w'} {β : Type} [Iterator α m β] [Monad m]
-    (it : IterM.Partial (α := α) m β) [IteratorSizePartial α m] : m Nat :=
-  ULift.down <$> IteratorSizePartial.size it.it
+@[always_inline, inline, deprecated IterM.Partial.count (since := "2025-10-29")]
+def IterM.Partial.size {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β]
+    [IteratorLoopPartial α m m] [Monad m] (it : IterM.Partial (α := α) m β) : m (ULift Nat) :=
+  it.count
 
-end Size
+end Count
 
 end Std.Iterators

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

@@ -11,6 +11,7 @@ import all Init.Data.Iterators.Combinators.Attach
 import all Init.Data.Iterators.Combinators.Monadic.Attach
 public import Init.Data.Iterators.Lemmas.Combinators.Monadic.Attach
 public import Init.Data.Iterators.Lemmas.Consumers.Collect
+public import Init.Data.Iterators.Lemmas.Consumers.Loop
 public import Init.Data.Array.Attach
 
 public section
@@ -82,4 +83,14 @@ theorem Iter.toArray_attachWith [Iterator α Id β]
     simpa only [Array.toList_inj]
   simp [Iter.toList_toArray]
 
+@[simp]
+theorem Iter.count_attachWith [Iterator α Id β]
+    {it : Iter (α := α) β} {hP}
+    [Finite α Id] [IteratorLoop α Id Id]
+    [LawfulIteratorLoop α Id Id] :
+    (it.attachWith P hP).count = it.count := by
+  letI : IteratorCollect α Id Id := .defaultImplementation
+  rw [← Iter.length_toList_eq_count, toList_attachWith]
+  simp
+
 end Std.Iterators

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

@@ -467,6 +467,17 @@ theorem Iter.fold_map {α β γ : Type w} {δ : Type x}
 
 end Fold
 
+section Count
+
+@[simp]
+theorem Iter.count_map {α β β' : Type w} [Iterator α Id β]
+    [IteratorLoop α Id Id] [Finite α Id] [LawfulIteratorLoop α Id Id]
+    {it : Iter (α := α) β} {f : β → β'} :
+    (it.map f).count = it.count := by
+  simp [map_eq_toIter_map_toIterM, count_eq_count_toIterM]
+
+end Count
+
 theorem Iter.anyM_filterMapM {α β β' : Type w} {m : Type w → Type w'}
     [Iterator α Id β] [Finite α Id] [Monad m] [LawfulMonad m]
     {it : Iter (α := α) β} {f : β → m (Option β')} {p : β' → m (ULift Bool)} :

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

@@ -9,6 +9,7 @@ prelude
 public import Init.Data.Iterators.Combinators.Monadic.Attach
 import all Init.Data.Iterators.Combinators.Monadic.Attach
 public import Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect
+public import Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
 
 public section
 
@@ -59,4 +60,14 @@ theorem IterM.map_unattach_toArray_attachWith [Iterator α m β] [Monad m] [Mona
   rw [← toArray_toList, ← toArray_toList, ← map_unattach_toList_attachWith (it := it) (hP := hP)]
   simp [-map_unattach_toList_attachWith, -IterM.toArray_toList]
 
+@[simp]
+theorem IterM.count_attachWith [Iterator α m β] [Monad m] [Monad n]
+    {it : IterM (α := α) m β} {hP}
+    [Finite α m] [IteratorLoop α m m] [LawfulMonad m] [LawfulIteratorLoop α m m] :
+    (it.attachWith P hP).count = it.count := by
+  letI : IteratorCollect α m m := .defaultImplementation
+  rw [← up_length_toList_eq_count, ← up_length_toList_eq_count,
+    ← map_unattach_toList_attachWith (it := it) (P := P) (hP := hP)]
+  simp only [Functor.map_map, List.length_unattach]
+
 end Std.Iterators

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

@@ -895,6 +895,23 @@ theorem IterM.fold_map {α β γ δ : Type w} {m : Type w → Type w'}
 
 end Fold
 
+section Count
+
+@[simp]
+theorem IterM.count_map {α β β' : Type w} {m : Type w → Type w'} [Iterator α m β] [Monad m]
+    [IteratorLoop α m m] [Finite α m] [LawfulMonad m] [LawfulIteratorLoop α m m]
+    {it : IterM (α := α) m β} {f : β → β'} :
+    (it.map f).count = it.count := by
+  induction it using IterM.inductSteps with | step it ihy ihs
+  rw [count_eq_match_step, count_eq_match_step, step_map, bind_assoc]
+  apply bind_congr; intro step
+  cases step.inflate using PlausibleIterStep.casesOn
+  · simp [ihy ‹_›]
+  · simp [ihs ‹_›]
+  · simp
+
+end Count
+
 section AnyAll
 
 theorem IterM.anyM_filterMapM {α β β' : Type w} {m : Type w → Type w'} {n : Type w → Type w''}