From d16c4052c2cfdb8f1801361ca72b2a6a4e783371 Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Fri, 6 Jun 2025 16:26:52 +0200
Subject: [PATCH] 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.
---
 .../Iterators/Combinators/Monadic/Drop.lean   |  1 +
 .../Iterators/Consumers/Monadic/Loop.lean     |  2 +-
 .../Data/Iterators/Lemmas/Consumers/Loop.lean |  7 ++
 .../Iterators/Lemmas/Consumers/Monadic.lean   |  1 +
 src/Std/Data/Iterators/Lemmas/Producers.lean  |  1 +
 .../Iterators/Lemmas/Producers/Empty.lean     | 60 +++++++++++++++
 .../Iterators/Lemmas/Producers/Monadic.lean   |  1 +
 .../Lemmas/Producers/Monadic/Empty.lean       | 62 ++++++++++++++++
 src/Std/Data/Iterators/Producers.lean         |  1 +
 src/Std/Data/Iterators/Producers/Empty.lean   | 23 ++++++
 src/Std/Data/Iterators/Producers/Monadic.lean |  1 +
 .../Iterators/Producers/Monadic/Empty.lean    | 73 +++++++++++++++++++
 tests/lean/run/iterators.lean                 | 12 +++
 13 files changed, 244 insertions(+), 1 deletion(-)
 create mode 100644 src/Std/Data/Iterators/Lemmas/Producers/Empty.lean
 create mode 100644 src/Std/Data/Iterators/Lemmas/Producers/Monadic/Empty.lean
 create mode 100644 src/Std/Data/Iterators/Producers/Empty.lean
 create mode 100644 src/Std/Data/Iterators/Producers/Monadic/Empty.lean

diff --git a/src/Std/Data/Iterators/Combinators/Monadic/Drop.lean b/src/Std/Data/Iterators/Combinators/Monadic/Drop.lean
index 76b2c48c79..3297883175 100644
--- a/src/Std/Data/Iterators/Combinators/Monadic/Drop.lean
+++ b/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 β
 
diff --git a/src/Std/Data/Iterators/Consumers/Monadic/Loop.lean b/src/Std/Data/Iterators/Consumers/Monadic/Loop.lean
index 018db4909a..7aefb897a3 100644
--- a/src/Std/Data/Iterators/Consumers/Monadic/Loop.lean
+++ b/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 :=
diff --git a/src/Std/Data/Iterators/Lemmas/Consumers/Loop.lean b/src/Std/Data/Iterators/Lemmas/Consumers/Loop.lean
index 6263dea687..8ed9231bd8 100644
--- a/src/Std/Data/Iterators/Lemmas/Consumers/Loop.lean
+++ b/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 : γ}
diff --git a/src/Std/Data/Iterators/Lemmas/Consumers/Monadic.lean b/src/Std/Data/Iterators/Lemmas/Consumers/Monadic.lean
index e8c7d3c8ef..e2faca8e96 100644
--- a/src/Std/Data/Iterators/Lemmas/Consumers/Monadic.lean
+++ b/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
diff --git a/src/Std/Data/Iterators/Lemmas/Producers.lean b/src/Std/Data/Iterators/Lemmas/Producers.lean
index baeab5010c..48f7be300a 100644
--- a/src/Std/Data/Iterators/Lemmas/Producers.lean
+++ b/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
diff --git a/src/Std/Data/Iterators/Lemmas/Producers/Empty.lean b/src/Std/Data/Iterators/Lemmas/Producers/Empty.lean
new file mode 100644
index 0000000000..e96a100d40
--- /dev/null
+++ b/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
diff --git a/src/Std/Data/Iterators/Lemmas/Producers/Monadic.lean b/src/Std/Data/Iterators/Lemmas/Producers/Monadic.lean
index 82882a799d..d89cdc3f43 100644
--- a/src/Std/Data/Iterators/Lemmas/Producers/Monadic.lean
+++ b/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
diff --git a/src/Std/Data/Iterators/Lemmas/Producers/Monadic/Empty.lean b/src/Std/Data/Iterators/Lemmas/Producers/Monadic/Empty.lean
new file mode 100644
index 0000000000..9bded4fd6f
--- /dev/null
+++ b/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
diff --git a/src/Std/Data/Iterators/Producers.lean b/src/Std/Data/Iterators/Producers.lean
index 8a8c3598a6..eb9319a6ba 100644
--- a/src/Std/Data/Iterators/Producers.lean
+++ b/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
diff --git a/src/Std/Data/Iterators/Producers/Empty.lean b/src/Std/Data/Iterators/Producers/Empty.lean
new file mode 100644
index 0000000000..4da7c69352
--- /dev/null
+++ b/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
diff --git a/src/Std/Data/Iterators/Producers/Monadic.lean b/src/Std/Data/Iterators/Producers/Monadic.lean
index d7db666229..e9111f8fd3 100644
--- a/src/Std/Data/Iterators/Producers/Monadic.lean
+++ b/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
diff --git a/src/Std/Data/Iterators/Producers/Monadic/Empty.lean b/src/Std/Data/Iterators/Producers/Monadic/Empty.lean
new file mode 100644
index 0000000000..e952845e6c
--- /dev/null
+++ b/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
diff --git a/tests/lean/run/iterators.lean b/tests/lean/run/iterators.lean
index 73f8f6f370..8e843b9332 100644
--- a/tests/lean/run/iterators.lean
+++ b/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