feat: introduce empty iterator (#8615)

This PR provides a special empty iterator type. Although its behavior
can be emulated with a list iterator (for example), having a special
type has the advantage of being easier to optimize for the compiler.

src/Std/Data/Iterators/Combinators/Monadic/Drop.lean

@@ -51,6 +51,7 @@ it.drop 3   ------⊥
 Currently, this combinator incurs an additional O(1) cost with each output of `it`, even when the iterator
 does not drop any elements anymore.
 -/
+@[always_inline, inline]
 def IterM.drop (n : Nat) (it : IterM (α := α) m β) :=
   toIterM (Drop.mk n it) m β
 

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

@@ -175,7 +175,7 @@ def IteratorLoopPartial.defaultImplementation {α : Type w} {m : Type w → Type
     IteratorLoopPartial α m n where
   forInPartial lift := IterM.DefaultConsumers.forInPartial lift _
 
-instance (α : Type w) (m : Type w → Type w') (n : Type w → Type w')
+instance (α : Type w) (m : Type w → Type w') (n : Type w → Type w'')
     [Monad m] [Monad n] [Iterator α m β] [Finite α m] :
     letI : IteratorLoop α m n := .defaultImplementation
     LawfulIteratorLoop α m n :=

src/Std/Data/Iterators/Lemmas/Consumers/Loop.lean

@@ -87,6 +87,13 @@ theorem Iter.foldM_eq_forIn {α β γ : Type w} [Iterator α Id β] [Finite α I
     it.foldM (init := init) f = ForIn.forIn it init (fun x acc => ForInStep.yield <$> f acc x) :=
   rfl
 
+theorem Iter.foldM_eq_foldM_toIterM {α β : Type w} [Iterator α Id β]
+    [Finite α Id] {m : Type w → Type w''} [Monad m] [LawfulMonad m]
+    [IteratorLoop α Id m] [LawfulIteratorLoop α Id m]
+    {γ : Type w} {it : Iter (α := α) β} {init : γ} {f : γ → β → m γ} :
+    it.foldM (init := init) f = letI : MonadLift Id m := ⟨pure⟩; it.toIterM.foldM (init := init) f :=
+  rfl
+
 theorem Iter.forIn_yield_eq_foldM {α β γ δ : Type w} [Iterator α Id β]
     [Finite α Id] {m : Type w → Type w''} [Monad m] [LawfulMonad m] [IteratorLoop α Id m]
     [LawfulIteratorLoop α Id m] {f : β → γ → m δ} {g : β → γ → δ → γ} {init : γ}

src/Std/Data/Iterators/Lemmas/Consumers/Monadic.lean

@@ -5,3 +5,4 @@ Authors: Paul Reichert
 -/
 prelude
 import Std.Data.Iterators.Lemmas.Consumers.Monadic.Collect
+import Std.Data.Iterators.Lemmas.Consumers.Monadic.Loop

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

@@ -6,5 +6,6 @@ Authors: Paul Reichert
 prelude
 import Std.Data.Iterators.Lemmas.Producers.Monadic
 import Std.Data.Iterators.Lemmas.Producers.Array
+import Std.Data.Iterators.Lemmas.Producers.Empty
 import Std.Data.Iterators.Lemmas.Producers.List
 import Std.Data.Iterators.Lemmas.Producers.Repeat

src/Std/Data/Iterators/Lemmas/Producers/Empty.lean

@@ -0,0 +1,60 @@
+/-
+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.Lemmas.Producers.Monadic.Empty
+import Std.Data.Iterators.Lemmas.Consumers
+import Std.Data.Iterators.Producers.Empty
+
+namespace Std.Iterators
+
+@[simp]
+theorem Iter.toIterM_empty {β} :
+    (Iter.empty β).toIterM = IterM.empty Id β :=
+  rfl
+
+@[simp]
+theorem Iter.step_empty {β} :
+    (Iter.empty β).step = ⟨.done, rfl⟩ := by
+  simp [Iter.step]
+
+@[simp]
+theorem Iter.toList_empty {β} :
+    (Iter.empty β).toList = [] := by
+  simp [Iter.toList_eq_toList_toIterM]
+
+@[simp]
+theorem Iter.toListRev_empty {β} :
+    (Iter.empty β).toListRev = [] := by
+  simp [Iter.toListRev_eq_toListRev_toIterM]
+
+@[simp]
+theorem Iter.toArray_empty {β} :
+    (Iter.empty β).toArray = #[] := by
+  simp [Iter.toArray_eq_toArray_toIterM]
+
+@[simp]
+theorem Iter.forIn_empty {m β γ} [Monad m] [LawfulMonad m]
+    {init : γ} {f} :
+    ForIn.forIn (m := m) (Iter.empty β) init f = pure init := by
+  simp [Iter.forIn_eq_forIn_toIterM]
+  letI : MonadLift Id m := ⟨Internal.idToMonad (α := _)⟩
+  letI := Internal.LawfulMonadLiftFunction.idToMonad (m := m)
+  haveI : LawfulMonadLiftT Id m := inferInstance
+  rw [IterM.forIn_empty]
+
+
+@[simp]
+theorem Iter.foldM_empty {m β γ} [Monad m] [LawfulMonad m]
+    {init : γ} {f} :
+    (Iter.empty β).foldM (m := m) (init := init) f = pure init := by
+  simp [Iter.foldM_eq_forIn]
+
+@[simp]
+theorem Iter.fold_empty {β γ} {init : γ} {f} :
+    (Iter.empty β).fold (init := init) f = init := by
+  simp [Iter.fold_eq_foldM]
+
+end Std.Iterators

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

@@ -5,4 +5,5 @@ Authors: Paul Reichert
 -/
 prelude
 import Std.Data.Iterators.Lemmas.Producers.Monadic.Array
+import Std.Data.Iterators.Lemmas.Producers.Monadic.Empty
 import Std.Data.Iterators.Lemmas.Producers.Monadic.List

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

@@ -0,0 +1,62 @@
+/-
+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.Empty
+import Std.Data.Iterators.Lemmas.Consumers.Monadic
+import Std.Data.Iterators.Lemmas.Consumers.Monadic.Loop
+
+namespace Std.Iterators
+
+@[simp]
+theorem IterM.step_empty {m β} [Monad m] :
+    (IterM.empty m β).step = pure ⟨.done, rfl⟩ :=
+  rfl
+
+@[simp]
+theorem IterM.toList_empty {m β} [Monad m] [LawfulMonad m] :
+    (IterM.empty m β).toList = pure [] := by
+  rw [toList_eq_match_step]
+  simp
+
+@[simp]
+theorem IterM.toListRev_empty {m β} [Monad m] [LawfulMonad m] :
+    (IterM.empty m β).toListRev = pure [] := by
+  rw [toListRev_eq_match_step]
+  simp
+
+@[simp]
+theorem IterM.toArray_empty {m β} [Monad m] [LawfulMonad m] :
+    (IterM.empty m β).toArray = pure #[] := by
+  rw [toArray_eq_match_step]
+  simp
+
+@[simp]
+theorem IterM.forIn_empty {m n β γ} [Monad m] [LawfulMonad m]
+    [Monad n] [LawfulMonad n] [MonadLiftT m n] [LawfulMonadLiftT m n]
+    {init : γ} {f} :
+    ForIn.forIn (m := n) (IterM.empty m β) init f = pure init := by
+  rw [IterM.forIn_eq_match_step]
+  simp
+
+@[simp]
+theorem IterM.foldM_empty {m n β γ} [Monad m] [LawfulMonad m]
+    [Monad n] [LawfulMonad n] [MonadLiftT m n] [LawfulMonadLiftT m n]
+    {init : γ} {f} :
+    (IterM.empty m β).foldM (n := n) (init := init) f = pure init := by
+  simp [IterM.foldM_eq_forIn]
+
+@[simp]
+theorem IterM.fold_empty {m β γ} [Monad m] [LawfulMonad m]
+    {init : γ} {f} :
+    (IterM.empty m β).fold (init := init) f = pure init := by
+  simp [IterM.fold_eq_foldM]
+
+@[simp]
+theorem IterM.drain_empty {m β} [Monad m] [LawfulMonad m] :
+    (IterM.empty m β).drain = pure .unit := by
+  simp [IterM.drain_eq_fold]
+
+end Std.Iterators

src/Std/Data/Iterators/Producers.lean

@@ -6,5 +6,6 @@ Authors: Paul Reichert
 prelude
 import Std.Data.Iterators.Producers.Monadic
 import Std.Data.Iterators.Producers.Array
+import Std.Data.Iterators.Producers.Empty
 import Std.Data.Iterators.Producers.List
 import Std.Data.Iterators.Producers.Repeat

src/Std/Data/Iterators/Producers/Empty.lean

@@ -0,0 +1,23 @@
+/-
+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.Empty
+
+namespace Std.Iterators
+
+/--
+Returns an iterator that terminates immediately.
+
+**Termination properties:**
+
+* `Finite` instance: always
+* `Productive` instance: always
+-/
+@[always_inline, inline]
+def Iter.empty (β : Type w) :=
+  ((IterM.empty Id β).toIter : Iter β)
+
+end Std.Iterators

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

@@ -5,4 +5,5 @@ Authors: Paul Reichert
 -/
 prelude
 import Std.Data.Iterators.Producers.Monadic.Array
+import Std.Data.Iterators.Producers.Monadic.Empty
 import Std.Data.Iterators.Producers.Monadic.List

src/Std/Data/Iterators/Producers/Monadic/Empty.lean

@@ -0,0 +1,73 @@
+/-
+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.Collect
+import Std.Data.Iterators.Consumers.Loop
+import Std.Data.Iterators.Internal.Termination
+
+/-!
+This file provides an empty iterator.
+-/
+
+namespace Std.Iterators
+
+variable {m : Type w → Type w'} {β : Type w}
+
+/--
+The internal state of the `IterM.empty` iterator.
+-/
+structure Empty (m : Type w → Type w') (β : Type w) : Type w where
+
+/--
+Returns an iterator that terminates immediately.
+
+**Termination properties:**
+
+* `Finite` instance: always
+* `Productive` instance: always
+
+-/
+@[always_inline, inline]
+def IterM.empty (m : Type w → Type w') (β : Type w) :=
+  toIterM (Empty.mk (m := m) (β := β)) m β
+
+def Empty.PlausibleStep (_ : IterM (α := Empty m β) m β)
+    (step : IterStep (IterM (α := Empty m β) m β) β) : Prop :=
+  step = .done
+
+instance Empty.instIterator [Monad m] : Iterator (Empty m β) m β where
+  IsPlausibleStep := Empty.PlausibleStep
+  step _ := return .done rfl
+
+private def Empty.instFinitenessRelation [Monad m] :
+    FinitenessRelation (Empty m β) m where
+  rel := emptyRelation
+  wf := emptyWf.wf
+  subrelation {it it'} h := by
+    obtain ⟨step, h, h'⟩ := h
+    cases h'
+    cases h
+
+instance Empty.instFinite [Monad m] : Finite (Empty m β) m :=
+  Finite.of_finitenessRelation instFinitenessRelation
+
+instance Empty.instIteratorCollect {n : Type w → Type w''} [Monad m] [Monad n] :
+    IteratorCollect (Empty m β) m n :=
+  .defaultImplementation
+
+instance Empty.instIteratorCollectPartial {n : Type w → Type w''} [Monad m] [Monad n] :
+    IteratorCollectPartial (Empty m β) m n :=
+  .defaultImplementation
+
+instance Empty.instIteratorLoop {n : Type w → Type w''} [Monad m] [Monad n] :
+    IteratorLoop (Empty m β) m n :=
+  .defaultImplementation
+
+instance Empty.instIteratorLoopPartial {n : Type w → Type w''} [Monad m] [Monad n] :
+    IteratorLoopPartial (Empty m β) m n :=
+  .defaultImplementation
+
+end Std.Iterators

tests/lean/run/iterators.lean

@@ -1,4 +1,5 @@
 import Std.Data.Iterators
+import Std.Data.Iterators.Producers.Empty
 
 section ListIteratorBasic
 
@@ -296,3 +297,14 @@ example : isPrime 5 := by
   simp
 
 end Repeat
+
+section Empty
+
+/-- info: [] -/
+#guard_msgs in
+#eval (Std.Iterators.Iter.empty Nat).toList
+
+example : (Std.Iterators.Iter.empty Nat).toList = [] := by
+  simp
+
+end Empty