corrections

Author: datokrat

src/Init/Data/Iterators/Basic.lean

@@ -222,36 +222,6 @@ theorem IterStep.mapIterator_id {step : IterStep α β} :
     step.mapIterator id = step := by
   cases step <;> rfl
 
-/--
-A variant of `mapIterator` where the mapping function takes a proof that the
-given iterator has been obtained with `IterStep.successor`.
-
-If present, applies `f` to the iterator of an `IterStep` and replaces the iterator
-with the result of the application of `f`.
--/
-@[always_inline, inline, expose]
-def IterStep.pmapIterator {α' : Type u'} (step : IterStep α β)
-    (f : (it : α) → step.successor = some it → α') : IterStep α' β :=
-  match step with
-  | .yield it out => .yield (f it rfl) out
-  | .skip it => .skip (f it rfl)
-  | .done => .done
-
-@[simp]
-theorem IterStep.pmapIterator_yield {α' : Type u'} {it : α} {out : β} {f : (it : α) → _ → α'} :
-    (IterStep.yield it out).pmapIterator f = IterStep.yield (f it rfl) out :=
-  rfl
-
-@[simp]
-theorem IterStep.pmapIterator_skip {α' : Type u'} {it : α} {f : (it : α) → _ → α'} :
-    (IterStep.skip it (β := β)).pmapIterator f = IterStep.skip (f it rfl) :=
-  rfl
-
-@[simp]
-theorem IterStep.pmapIterator_done {α' : Type u'} {f : (it : α) → _ → α'} :
-    (IterStep.done (α := α) (β := β)).pmapIterator f = IterStep.done :=
-  rfl
-
 /--
 A variant of `IterStep` that bundles the step together with a proof that it is "plausible".
 The plausibility predicate will later be chosen to assert that a state is a plausible successor
@@ -370,45 +340,6 @@ def IterM.IsPlausibleSuccessorOf {α : Type w} {m : Type w → Type w'} {β : Ty
     (it' it : IterM (α := α) m β) : Prop :=
   ∃ step, step.successor = some it' ∧ it.IsPlausibleStep step
 
-inductive IterM.IsPlausibleIndirectOutput {α β : Type w} {m : Type w → Type w'} [Iterator α m β]
-    : IterM (α := α) m β → β → Prop where
-  | direct {it : IterM (α := α) m β} {out : β} : it.IsPlausibleOutput out →
-      it.IsPlausibleIndirectOutput out
-  | indirect {it it' : IterM (α := α) m β} {out : β} : it'.IsPlausibleSuccessorOf it →
-      it'.IsPlausibleIndirectOutput out → it.IsPlausibleIndirectOutput out
-
--- TODO: remove if unused
-def IterM.IsInLineageOf {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β]
-    (it' it : IterM (α := α) m β) : Prop :=
-  it' = it ∨ Relation.TransGen IterM.IsPlausibleSuccessorOf it' it
-
-protected theorem IterM.IsInLineageOf.rfl {α : Type w} {m : Type w → Type w'} {β : Type w}
-    [Iterator α m β] {it : IterM (α := α) m β} :
-    it.IsInLineageOf it :=
-  .inl rfl
-
-protected theorem IterM.IsInLineageOf.single {α : Type w} {m : Type w → Type w'} {β : Type w}
-    [Iterator α m β] {it' it : IterM (α := α) m β}
-    (h : it'.IsPlausibleSuccessorOf it) :
-    it'.IsInLineageOf it :=
-  .inr <| .single h
-
-protected theorem IterM.IsInLineageOf.trans {α : Type w} {m : Type w → Type w'} {β : Type w}
-    [Iterator α m β] {it'' it' it : IterM (α := α) m β}
-    (h' : it''.IsInLineageOf it') (h : it'.IsInLineageOf it) :
-    it''.IsInLineageOf it := by
-  cases h
-  · rename_i h
-    cases h
-    exact h'
-  · rename_i h
-    cases h'
-    · rename_i h'
-      cases h'
-      exact .inr h
-    · rename_i h'
-      exact .inr <| .trans h' h
-
 /--
 Asserts that a certain iterator `it'` could plausibly be the directly succeeding iterator of another
 given iterator `it` while no value is emitted (see `IterStep.skip`).
@@ -498,34 +429,6 @@ def Iter.IsPlausibleSuccessorOf {α : Type w} {β : Type w} [Iterator α Id β]
     (it' it : Iter (α := α) β) : Prop :=
   it'.toIterM.IsPlausibleSuccessorOf it.toIterM
 
-inductive Iter.IsPlausibleIndirectOutput {α β : Type w} [Iterator α Id β] :
-    Iter (α := α) β → β → Prop where
-  | direct {it : Iter (α := α) β} {out : β} : it.IsPlausibleOutput out →
-      it.IsPlausibleIndirectOutput out
-  | indirect {it it' : Iter (α := α) β} {out : β} : it'.IsPlausibleSuccessorOf it →
-      it'.IsPlausibleIndirectOutput out → it.IsPlausibleIndirectOutput out
-
-theorem Iter.isPlausibleIndirectOutput_iff_isPlausibleIndirectOutput_toIterM {α β : Type w}
-    [Iterator α Id β] {it : Iter (α := α) β} {out : β} :
-    it.IsPlausibleIndirectOutput out ↔ it.toIterM.IsPlausibleIndirectOutput out := by
-  constructor
-  · intro h
-    induction h with
-    | direct h =>
-      exact .direct h
-    | indirect h _ ih =>
-      exact .indirect h ih
-  · intro h
-    rw [← Iter.toIter_toIterM (it := it)]
-    generalize it.toIterM = it at ⊢ h
-    induction h with
-    | direct h =>
-      exact .direct h
-    | indirect h h' ih =>
-      rename_i it it' out
-      replace h : it'.toIter.IsPlausibleSuccessorOf it.toIter := h
-      exact .indirect (α := α) h ih
-
 /--
 Asserts that a certain iterator `it'` could plausibly be the directly succeeding iterator of another
 given iterator `it` while no value is emitted (see `IterStep.skip`).

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

@@ -26,11 +26,9 @@ namespace Std.Iterators
 
 instance (α : Type w) (β : Type w) (n : Type w → Type w') [Monad n]
     [Iterator α Id β] [Finite α Id] [IteratorLoop α Id n] :
-    ForIn' n (Iter (α := α) β) β ⟨fun it out => it.IsPlausibleIndirectOutput out⟩ where
-  forIn' it init f :=
-    IteratorLoop.finiteForIn' (fun δ (c : Id δ) => pure c.run) |>.forIn' it.toIterM init
-        fun out h acc =>
-          f out (Iter.isPlausibleIndirectOutput_iff_isPlausibleIndirectOutput_toIterM.mpr h) acc
+    ForIn n (Iter (α := α) β) β where
+  forIn it init f :=
+    IteratorLoop.finiteForIn (fun δ (c : Id δ) => pure c.run) |>.forIn it.toIterM init f
 
 instance (α : Type w) (β : Type w) (n : Type w → Type w') [Monad n]
     [Iterator α Id β] [IteratorLoopPartial α Id n] :
@@ -115,14 +113,4 @@ def Iter.Partial.fold {α : Type w} {β : Type w} {γ : Type w} [Iterator α Id
     (init : γ) (it : Iter.Partial (α := α) β) : γ :=
   ForIn.forIn (m := Id) it init (fun x acc => ForInStep.yield (f acc x))
 
-@[always_inline, inline, inherit_doc IterM.size]
-def Iter.size {α : Type w} {β : Type w} [Iterator α Id β] [IteratorSize α Id]
-    (it : Iter (α := α) β) : Nat :=
-  (IteratorSize.size it.toIterM).run.down
-
-@[always_inline, inline, inherit_doc IterM.Partial.size]
-def Iter.Partial.size {α : Type w} {β : Type w} [Iterator α Id β] [IteratorSizePartial α Id]
-    (it : Iter (α := α) β) : Nat :=
-  (IteratorSizePartial.size it.toIterM).run.down
-
 end Std.Iterators

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

@@ -65,7 +65,7 @@ class IteratorLoop (α : Type w) (m : Type w → Type w') {β : Type w} [Iterato
       (plausible_forInStep : β → γ → ForInStep γ → Prop) →
       IteratorLoop.WellFounded α m plausible_forInStep →
       (it : IterM (α := α) m β) → γ →
-      ((b : β) → it.IsPlausibleIndirectOutput b → (c : γ) → n (Subtype (plausible_forInStep b c))) →
+      ((b : β) → (c : γ) → n (Subtype (plausible_forInStep b c))) →
       n γ
 
 /--
@@ -80,13 +80,7 @@ class IteratorLoopPartial (α : Type w) (m : Type w → Type w') {β : Type w} [
     (n : Type w → Type w'') where
   forInPartial : ∀ (_lift : (γ : Type w) → m γ → n γ) {γ : Type w},
       (it : IterM (α := α) m β) → γ →
-      ((b : β) → it.IsPlausibleIndirectOutput b → (c : γ) → n (ForInStep γ)) → n γ
-
-class IteratorSize (α : Type w) (m : Type w → Type w') {β : Type w} [Iterator α m β] where
-  size : IterM (α := α) m β → m (ULift Nat)
-
-class IteratorSizePartial (α : Type w) (m : Type w → Type w') {β : Type w} [Iterator α m β] where
-  size : IterM (α := α) m β → m (ULift Nat)
+      ((b : β) → (c : γ) → n (ForInStep γ)) → n γ
 
 end Typeclasses
 
@@ -119,20 +113,20 @@ def IterM.DefaultConsumers.forIn {m : Type w → Type w'} {α : Type w} {β : Ty
     (plausible_forInStep : β → γ → ForInStep γ → Prop)
     (wf : IteratorLoop.WellFounded α m plausible_forInStep)
     (it : IterM (α := α) m β) (init : γ)
-    (f : (b : β) → it.IsPlausibleIndirectOutput b → (c : γ) → n (Subtype (plausible_forInStep b c))) : n γ :=
+    (f : (b : β) → (c : γ) → n (Subtype (plausible_forInStep b c))) : n γ :=
   haveI : WellFounded _ := wf
   letI : MonadLift m n := ⟨fun {γ} => lift γ⟩
   do
     match ← it.step with
-    | .yield it' out h =>
-      match ← f out (.direct ⟨_, h⟩) init with
+    | .yield it' out _ =>
+      match ← f out init with
       | ⟨.yield c, _⟩ =>
         IterM.DefaultConsumers.forIn lift _ plausible_forInStep wf it' c
-          (fun out h' acc => f out (.indirect ⟨_, rfl, h⟩ h') acc)
+          (fun out acc => f out acc)
       | ⟨.done c, _⟩ => return c
-    | .skip it' h =>
+    | .skip it' _ =>
       IterM.DefaultConsumers.forIn lift _ plausible_forInStep wf it' init
-        (fun out h' acc => f out (.indirect ⟨_, rfl, h⟩ h') acc)
+        (fun out acc => f out acc)
     | .done _ => return init
 termination_by IteratorLoop.WFRel.mk wf it init
 decreasing_by
@@ -167,19 +161,19 @@ partial def IterM.DefaultConsumers.forInPartial {m : Type w → Type w'} {α : T
     {n : Type w → Type w''} [Monad n]
     (lift : ∀ γ, m γ → n γ) (γ : Type w)
     (it : IterM (α := α) m β) (init : γ)
-    (f : (b : β) → it.IsPlausibleIndirectOutput b → (c : γ) → n (ForInStep γ)) : n γ :=
+    (f : (b : β) → (c : γ) → n (ForInStep γ)) : n γ :=
   letI : MonadLift m n := ⟨fun {γ} => lift γ⟩
   do
     match ← it.step with
-    | .yield it' out h =>
-      match ← f out (.direct ⟨_, h⟩) init with
+    | .yield it' out _ =>
+      match ← f out init with
       | .yield c =>
         IterM.DefaultConsumers.forInPartial lift _ it' c
-          fun out h' acc => f out (.indirect ⟨_, rfl, h⟩ h') acc
+          fun out acc => f out acc
       | .done c => return c
-    | .skip it' h =>
+    | .skip it' _ =>
       IterM.DefaultConsumers.forInPartial lift _ it' init
-        fun out h' acc => f out (.indirect ⟨_, rfl, h⟩ h') acc
+        fun out acc => f out acc
     | .done _ => return init
 
 /--
@@ -214,28 +208,28 @@ theorem IteratorLoop.wellFounded_of_finite {m : Type w → Type w'}
     exact WellFoundedRelation.wf
 
 /--
-This `ForIn'`-style loop construct traverses a finite iterator using an `IteratorLoop` instance.
+This `ForIn`-style loop construct traverses a finite iterator using an `IteratorLoop` instance.
 -/
 @[always_inline, inline]
-def IteratorLoop.finiteForIn' {m : Type w → Type w'} {n : Type w → Type w''}
+def IteratorLoop.finiteForIn {m : Type w → Type w'} {n : Type w → Type w''}
     {α : Type w} {β : Type w} [Iterator α m β] [Finite α m] [IteratorLoop α m n]
     (lift : ∀ γ, m γ → n γ) :
-    ForIn' n (IterM (α := α) m β) β ⟨fun it out => it.IsPlausibleIndirectOutput out⟩ where
-  forIn' {γ} [Monad n] it init f :=
+    ForIn n (IterM (α := α) m β) β where
+  forIn {γ} [Monad n] it init f :=
     IteratorLoop.forIn (α := α) (m := m) lift γ (fun _ _ _ => True)
       wellFounded_of_finite
-      it init (fun out h acc => (⟨·, .intro⟩) <$> f out h acc)
+      it init (fun out acc => (⟨·, .intro⟩) <$> f out acc)
 
 instance {m : Type w → Type w'} {n : Type w → Type w''}
     {α : Type w} {β : Type w} [Iterator α m β] [Finite α m] [IteratorLoop α m n]
     [MonadLiftT m n] :
-    ForIn' n (IterM (α := α) m β) β ⟨fun it out => it.IsPlausibleIndirectOutput out⟩ :=
-  IteratorLoop.finiteForIn' (fun _ => monadLift)
+    ForIn n (IterM (α := α) m β) β :=
+  IteratorLoop.finiteForIn (fun _ => monadLift)
 
 instance {m : Type w → Type w'} {n : Type w → Type w''}
     {α : Type w} {β : Type w} [Iterator α m β] [IteratorLoopPartial α m n] [MonadLiftT m n] :
-    ForIn' n (IterM.Partial (α := α) m β) β ⟨fun it out => it.it.IsPlausibleIndirectOutput out⟩ where
-  forIn' it init f :=
+    ForIn n (IterM.Partial (α := α) m β) β where
+  forIn it init f :=
     IteratorLoopPartial.forInPartial (α := α) (m := m) (fun _ => monadLift) it.it init f
 
 instance {m : Type w → Type w'} {n : Type w → Type w''}
@@ -346,42 +340,4 @@ def IterM.Partial.drain {α : Type w} {m : Type w → Type w'} [Monad m] {β : T
     m PUnit :=
   it.fold (γ := PUnit) (fun _ _ => .unit) .unit
 
-section Size
-
-@[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)
-
-@[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)
-
-@[always_inline, inline]
-instance 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
-
-@[always_inline, inline]
-instance IteratorSize.Partial.defaultImplementation {α β : Type w} {m : Type w → Type w'} [Monad m]
-    [Iterator α m β] [Finite α m] [IteratorLoopPartial α m m] :
-    IteratorSizePartial α m where
-  size := IterM.DefaultConsumers.sizePartial
-
-@[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
-
-@[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
-
-end Size
-
 end Std.Iterators

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

@@ -6,10 +6,10 @@ Authors: Paul Reichert
 module
 
 prelude
-import all Init.Data.Iterators.Consumers.Access
-import all Init.Data.Iterators.Consumers.Collect
 import Init.Data.Iterators.Lemmas.Basic
 import Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect
+import all Init.Data.Iterators.Consumers.Access
+import all Init.Data.Iterators.Consumers.Collect
 
 namespace Std.Iterators
 

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

@@ -4,33 +4,21 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Paul Reichert
 -/
 prelude
-import Init.Data.List.Control
-import Init.Data.Iterators.Lemmas.Basic
 import Init.Data.Iterators.Lemmas.Consumers.Collect
 import Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
-import Init.Data.Iterators.Consumers.Collect
 import Init.Data.Iterators.Consumers.Loop
 
 namespace Std.Iterators
 
-theorem Iter.forIn'_eq {α β : Type w} [Iterator α Id β] [Finite α Id]
-    {m : Type w → Type w''} [Monad m] [IteratorLoop α Id m] [hl : LawfulIteratorLoop α Id m]
-    {γ : Type w} {it : Iter (α := α) β} {init : γ}
-    {f : (b : β) → it.IsPlausibleIndirectOutput b → γ → m (ForInStep γ)} :
-    ForIn'.forIn' it init f =
-      IterM.DefaultConsumers.forIn (fun _ c => pure c.run) γ (fun _ _ _ => True)
-        IteratorLoop.wellFounded_of_finite it.toIterM init
-          (fun out h acc => (⟨·, .intro⟩) <$>
-            f out (Iter.isPlausibleIndirectOutput_iff_isPlausibleIndirectOutput_toIterM.mpr h) acc) := by
-  cases hl.lawful; rfl
-
 theorem Iter.forIn_eq {α β : Type w} [Iterator α Id β] [Finite α Id]
     {m : Type w → Type w''} [Monad m] [IteratorLoop α Id m] [hl : LawfulIteratorLoop α Id m]
     {γ : Type w} {it : Iter (α := α) β} {init : γ}
-    {f : β → γ → m (ForInStep γ)} :
+    {f : (b : β) → γ → m (ForInStep γ)} :
     ForIn.forIn it init f =
       IterM.DefaultConsumers.forIn (fun _ c => pure c.run) γ (fun _ _ _ => True)
-        IteratorLoop.wellFounded_of_finite it.toIterM init (fun out _ acc => (⟨·, .intro⟩) <$> f out acc) := by
+        IteratorLoop.wellFounded_of_finite it.toIterM init
+          (fun out acc => (⟨·, .intro⟩) <$>
+            f out acc) := by
   cases hl.lawful; rfl
 
 theorem Iter.forIn_eq_forIn_toIterM {α β : Type w} [Iterator α Id β]

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

@@ -7,8 +7,8 @@ module
 
 prelude
 import Init.Data.Array.Lemmas
-import all Init.Data.Iterators.Consumers.Monadic.Collect
 import Init.Data.Iterators.Lemmas.Monadic.Basic
+import all Init.Data.Iterators.Consumers.Monadic.Collect
 
 namespace Std.Iterators