address remarks

Author: datokrat

src/Std/Data/Iterators/Basic.lean

@@ -115,27 +115,27 @@ def Iter.toIterM {α : Type w} {β : Type w} (it : Iter (α := α) β) : IterM (
 /--
 Converts a monadic iterator (`IterM Id β`) over `Id` into a pure iterator (`Iter β`).
 -/
-def IterM.toPureIter {α : Type w} {β : Type w} (it : IterM (α := α) Id β) : Iter (α := α) β :=
+def IterM.toIter {α : Type w} {β : Type w} (it : IterM (α := α) Id β) : Iter (α := α) β :=
   ⟨it.internalState⟩
 
 @[simp]
-theorem Iter.toPureIter_toIterM {α : Type w} {β : Type w} (it : Iter (α := α) β) :
-    it.toIterM.toPureIter = it :=
+theorem Iter.toIter_toIterM {α : Type w} {β : Type w} (it : Iter (α := α) β) :
+    it.toIterM.toIter = it :=
   rfl
 
 @[simp]
-theorem Iter.toPureIter_comp_toIterM {α : Type w} {β : Type w} :
-    IterM.toPureIter ∘ Iter.toIterM (α := α) (β := β) = id :=
+theorem Iter.toIter_comp_toIterM {α : Type w} {β : Type w} :
+    IterM.toIter ∘ Iter.toIterM (α := α) (β := β) = id :=
   rfl
 
 @[simp]
-theorem Iter.toIterM_toPureIter {α : Type w} {β : Type w} (it : IterM (α := α) Id β) :
-    it.toPureIter.toIterM = it :=
+theorem Iter.toIterM_toIter {α : Type w} {β : Type w} (it : IterM (α := α) Id β) :
+    it.toIter.toIterM = it :=
   rfl
 
 @[simp]
-theorem Iter.toIterM_comp_toPureIter {α : Type w} {β : Type w} :
-    Iter.toIterM ∘ IterM.toPureIter (α := α) (β := β) = id :=
+theorem Iter.toIterM_comp_toIter {α : Type w} {β : Type w} :
+    Iter.toIterM ∘ IterM.toIter (α := α) (β := β) = id :=
   rfl
 
 section IterStep
@@ -184,8 +184,8 @@ def IterStep.mapIterator {α' : Type u'} (f : α → α') : IterStep α β → I
   | .done => .done
 
 @[simp]
-theorem IterStep.mapIterator_mapIterator {α' : Type u'} {f : α → α'} {g : α' → α}
-    {step : IterStep α β} :
+theorem IterStep.mapIterator_mapIterator {α' : Type u'} {α'' : Type u''}
+    {f : α → α'} {g : α' → α''} {step : IterStep α β} :
     (step.mapIterator f).mapIterator g = step.mapIterator (g ∘ f) := by
   cases step <;> rfl
 
@@ -229,35 +229,18 @@ def PlausibleIterStep.done {IsPlausibleStep : IterStep α β → Prop}
   ⟨.done, h⟩
 
 /--
-An inductive type that makes it easier to apply the `cases` tactic to a
-`PlausibleIterStep`. See `PlausibleIterStep.casesHelper` for more information.
+A more convenient `cases` eliminator for `PlausibleIterStep`.
 -/
-inductive PlausibleIterStep.CasesHelper {IsPlausibleStep : IterStep α β → Prop} :
-    PlausibleIterStep IsPlausibleStep → Type _ where
-  | yield (it' out h) : CasesHelper ⟨.yield it' out, h⟩
-  | skip (it' h) : CasesHelper ⟨.skip it', h⟩
-  | done (h) : CasesHelper ⟨.done, h⟩
-
-/--
-Because `PlausibleIterStep` is a subtype of `IterStep`, it is tedious to use
-the `cases` tactic:
-
-```lean
-obtain ⟨step, h⟩ := step
-cases step
-```
-
-Using `casesHelper`, the case distinction can be done more ergonomically.
-
-```lean
-cases step.casesHelper
-```
--/
-def PlausibleIterStep.casesHelper {IsPlausibleStep : IterStep α β → Prop} :
-    (step : PlausibleIterStep IsPlausibleStep) → PlausibleIterStep.CasesHelper step
-  | .yield it' out h => .yield it' out h
-  | .skip it' h => .skip it' h
-  | .done h => .done h
+@[elab_as_elim, cases_eliminator]
+abbrev PlausibleIterStep.casesOn {IsPlausibleStep : IterStep α β → Prop}
+    {motive : PlausibleIterStep IsPlausibleStep → Sort x} (s : PlausibleIterStep IsPlausibleStep)
+    (yield : ∀ it' out h, motive ⟨.yield it' out, h⟩)
+    (skip : ∀ it' h, motive ⟨.skip it', h⟩)
+    (done : ∀ h, motive ⟨.done, h⟩) : motive s :=
+  match s with
+  | .yield it' out h => yield it' out h
+  | .skip it' h => skip it' h
+  | .done h => done h
 
 end IterStep
 
@@ -374,17 +357,17 @@ Converts an `IterM.Step` into an `Iter.Step`.
 -/
 @[always_inline, inline]
 def IterM.Step.toPure {α : Type w} {β : Type w} [Iterator α Id β] {it : IterM (α := α) Id β}
-    (step : it.Step) : it.toPureIter.Step :=
-  ⟨step.val.mapIterator IterM.toPureIter, (by simp [Iter.IsPlausibleStep, step.property])⟩
+    (step : it.Step) : it.toIter.Step :=
+  ⟨step.val.mapIterator IterM.toIter, (by simp [Iter.IsPlausibleStep, step.property])⟩
 
 @[simp]
 theorem IterM.Step.toPure_yield {α β : Type w} [Iterator α Id β] {it : IterM (α := α) Id β}
-    {it' out h} : IterM.Step.toPure (⟨.yield it' out, h⟩ : it.Step) = .yield it'.toPureIter out h :=
+    {it' out h} : IterM.Step.toPure (⟨.yield it' out, h⟩ : it.Step) = .yield it'.toIter out h :=
   rfl
 
 @[simp]
 theorem IterM.Step.toPure_skip {α β : Type w} [Iterator α Id β] {it : IterM (α := α) Id β}
-    {it' h} : IterM.Step.toPure (⟨.skip it', h⟩ : it.Step) = .skip it'.toPureIter h :=
+    {it' h} : IterM.Step.toPure (⟨.skip it', h⟩ : it.Step) = .skip it'.toIter h :=
   rfl
 
 @[simp]

src/Std/Data/Iterators/Consumers/Access.lean

@@ -15,7 +15,7 @@ before emitting `n` values.
 
 This function requires a `Productive` instance proving that the iterator will always emit a value
 after a finite number of skips. If the iterator is not productive or such an instance is not
-available, consider using `it.allowNontermination.toArray` instead of `it.toArray`. However, it is
+available, consider using `it.allowNontermination.seekIdx?` instead of `it.seekIdx?`. However, it is
 not possible to formally verify the behavior of the partial variant.
 -/
 @[specialize]

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

@@ -14,17 +14,32 @@ iterator `it` to an element of `motive it` by defining `f it` in terms of the va
 the plausible successors of `it'.
 -/
 @[specialize]
-def Iter.induct {α β} [Iterator α Id β] [Finite α Id]
+def Iter.inductSteps {α β} [Iterator α Id β] [Finite α Id]
   (motive : Iter (α := α) β → Sort x)
   (step : (it : Iter (α := α) β) →
     (ih_yield : ∀ {it' : Iter (α := α) β} {out : β},
       it.IsPlausibleStep (.yield it' out) → motive it') →
-    (ih_skip : ∀ {it' : Iter (α := α) β}, it.IsPlausibleStep (.skip it') → motive it' ) →
+    (ih_skip : ∀ {it' : Iter (α := α) β}, it.IsPlausibleStep (.skip it') → motive it') →
     motive it)
   (it : Iter (α := α) β) : motive it :=
   step it
-    (fun {it' _} _ => Iter.induct motive step it')
-    (fun {it'} _ => Iter.induct motive step it')
+    (fun {it' _} _ => inductSteps motive step it')
+    (fun {it'} _ => inductSteps motive step it')
 termination_by it.finitelyManySteps
 
+/--
+Induction principle for productive iterators: One can define a function `f` that maps every
+iterator `it` to an element of `motive it` by defining `f it` in terms of the values of `f` on
+the plausible skip successors of `it'.
+-/
+@[specialize]
+def Iter.inductSkips {α β} [Iterator α Id β] [Productive α Id]
+  (motive : Iter (α := α) β → Sort x)
+  (step : (it : Iter (α := α) β) →
+    (ih_skip : ∀ {it' : Iter (α := α) β}, it.IsPlausibleStep (.skip it') → motive it') →
+    motive it)
+  (it : Iter (α := α) β) : motive it :=
+  step it (fun {it'} _ => inductSkips motive step it')
+termination_by it.finitelyManySkips
+
 end Std.Iterators

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

@@ -27,15 +27,15 @@ theorem Iter.toListRev_eq_toListRev_toIterM {α β} [Iterator α Id β] [Finite
   rfl
 
 @[simp]
-theorem IterM.toList_toPureIter {α β} [Iterator α Id β] [Finite α Id] [IteratorCollect α Id]
+theorem IterM.toList_toIter {α β} [Iterator α Id β] [Finite α Id] [IteratorCollect α Id]
     {it : IterM (α := α) Id β} :
-    it.toPureIter.toList = it.toList :=
+    it.toIter.toList = it.toList :=
   rfl
 
 @[simp]
-theorem IterM.toListRev_toPureIter {α β} [Iterator α Id β] [Finite α Id]
+theorem IterM.toListRev_toIter {α β} [Iterator α Id β] [Finite α Id]
     {it : IterM (α := α) Id β} :
-    it.toPureIter.toListRev = it.toListRev :=
+    it.toIter.toListRev = it.toListRev :=
   rfl
 
 theorem Iter.toList_toArray {α β} [Iterator α Id β] [Finite α Id] [IteratorCollect α Id]
@@ -55,45 +55,43 @@ theorem Iter.toListRev_eq {α β} [Iterator α Id β] [Finite α Id] [IteratorCo
     it.toListRev = it.toList.reverse := by
   simp [Iter.toListRev_eq_toListRev_toIterM, Iter.toList_eq_toList_toIterM, IterM.toListRev_eq]
 
-theorem Iter.toArray_of_step {α β} [Iterator α Id β] [Finite α Id] [IteratorCollect α Id]
+theorem Iter.toArray_eq_match_step {α β} [Iterator α Id β] [Finite α Id] [IteratorCollect α Id]
     [LawfulIteratorCollect α Id] {it : Iter (α := α) β} :
     it.toArray = match it.step with
       | .yield it' out _ => #[out] ++ it'.toArray
       | .skip it' _ => it'.toArray
       | .done _ => #[] := by
   simp only [Iter.toArray_eq_toArray_toIterM, Iter.step]
-  rw [IterM.toArray_of_step]
+  rw [IterM.toArray_eq_match_step]
   simp only [Id.map_eq, Id.pure_eq, Id.bind_eq, Id.run]
   generalize it.toIterM.step = step
-  cases step.casesHelper <;> simp
+  cases step using PlausibleIterStep.casesOn <;> simp
 
-theorem Iter.toList_of_step {α β} [Iterator α Id β] [Finite α Id] [IteratorCollect α Id]
+theorem Iter.toList_eq_match_step {α β} [Iterator α Id β] [Finite α Id] [IteratorCollect α Id]
     [LawfulIteratorCollect α Id] {it : Iter (α := α) β} :
     it.toList = match it.step with
       | .yield it' out _ => out :: it'.toList
       | .skip it' _ => it'.toList
       | .done _ => [] := by
-  rw [← Iter.toList_toArray, Iter.toArray_of_step]
+  rw [← Iter.toList_toArray, Iter.toArray_eq_match_step]
   split <;> simp [Iter.toList_toArray]
 
-theorem Iter.toListRev_of_step {α β} [Iterator α Id β] [Finite α Id] {it : Iter (α := α) β} :
+theorem Iter.toListRev_eq_match_step {α β} [Iterator α Id β] [Finite α Id] {it : Iter (α := α) β} :
     it.toListRev = match it.step with
       | .yield it' out _ => it'.toListRev ++ [out]
       | .skip it' _ => it'.toListRev
       | .done _ => [] := by
-  rw [Iter.toListRev_eq_toListRev_toIterM, IterM.toListRev_of_step, Iter.step]
+  rw [Iter.toListRev_eq_toListRev_toIterM, IterM.toListRev_eq_match_step, Iter.step]
   simp only [Id.map_eq, Id.pure_eq, Id.bind_eq, Id.run]
   generalize it.toIterM.step = step
-  cases step.run.casesHelper <;> simp
+  cases step using PlausibleIterStep.casesOn <;> simp
 
 theorem Iter.getElem?_toList_eq_seekIdx? {α β}
     [Iterator α Id β] [Finite α Id] [IteratorCollect α Id] [LawfulIteratorCollect α Id]
     {it : Iter (α := α) β} {k : Nat} :
     it.toList[k]? = it.seekIdx? k := by
-  revert k
-  induction it using Iter.induct with | step it ihy ihs =>
-  intro k
-  rw [toList_of_step, seekIdx?]
+  induction it using Iter.inductSteps generalizing k with | step it ihy ihs =>
+  rw [toList_eq_match_step, seekIdx?]
   obtain ⟨step, h⟩ := it.step
   cases step
   · cases k <;> simp [ihy h]

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

@@ -38,7 +38,7 @@ theorem IterM.DefaultConsumers.toArrayMapped.go.aux₂ [Monad m] [LawfulMonad m]
     rw [List.toArray_cons, IterM.DefaultConsumers.toArrayMapped.go.aux₁, ih]
     simp only [Functor.map_map, Array.append_assoc]
 
-theorem IterM.DefaultConsumers.toArrayMapped_of_step [Monad m] [LawfulMonad m]
+theorem IterM.DefaultConsumers.toArrayMapped_eq_match_step [Monad m] [LawfulMonad m]
     [Iterator α m β] [Finite α m] {it : IterM (α := α) m β} {f : β → m γ} :
     IterM.DefaultConsumers.toArrayMapped f it = (do
       match ← it.step with
@@ -50,7 +50,7 @@ theorem IterM.DefaultConsumers.toArrayMapped_of_step [Monad m] [LawfulMonad m]
   intro step
   split <;> simp [IterM.DefaultConsumers.toArrayMapped.go.aux₂]
 
-theorem IterM.toArray_of_step [Monad m] [LawfulMonad m]
+theorem IterM.toArray_eq_match_step [Monad m] [LawfulMonad m]
     [Iterator α m β] [Finite α m] [IteratorCollect α m] [LawfulIteratorCollect α m]
     {it : IterM (α := α) m β} :
     it.toArray = (do
@@ -59,7 +59,7 @@ theorem IterM.toArray_of_step [Monad m] [LawfulMonad m]
       | .skip it' _ => it'.toArray
       | .done _ => return #[]) := by
   simp only [IterM.toArray, LawfulIteratorCollect.toArrayMapped_eq]
-  rw [IterM.DefaultConsumers.toArrayMapped_of_step]
+  rw [IterM.DefaultConsumers.toArrayMapped_eq_match_step]
   simp [bind_pure_comp, pure_bind, toArray]
 
 theorem IterM.toList_toArray [Monad m] [Iterator α m β] [Finite α m] [IteratorCollect α m]
@@ -72,15 +72,15 @@ theorem IterM.toArray_toList [Monad m] [LawfulMonad m] [Iterator α m β] [Finit
     List.toArray <$> it.toList = it.toArray := by
   simp [IterM.toList]
 
-theorem IterM.toList_of_step [Monad m] [LawfulMonad m] [Iterator α m β] [Finite α m]
+theorem IterM.toList_eq_match_step [Monad m] [LawfulMonad m] [Iterator α m β] [Finite α m]
     [IteratorCollect α m] [LawfulIteratorCollect α m] {it : IterM (α := α) m β} :
     it.toList = (do
       match ← it.step with
       | .yield it' out _ => return out :: (← it'.toList)
       | .skip it' _ => it'.toList
       | .done _ => return []) := by
   simp [← IterM.toList_toArray]
-  rw [IterM.toArray_of_step, map_eq_pure_bind, bind_assoc]
+  rw [IterM.toArray_eq_match_step, map_eq_pure_bind, bind_assoc]
   apply bind_congr
   intro step
   split <;> simp
@@ -105,7 +105,7 @@ theorem IterM.toListRev.go.aux₂ [Monad m] [LawfulMonad m] [Iterator α m β] [
   | nil => simp [toListRev]
   | cons x xs ih => simp [IterM.toListRev.go.aux₁, ih]
 
-theorem IterM.toListRev_of_step [Monad m] [LawfulMonad m] [Iterator α m β] [Finite α m]
+theorem IterM.toListRev_eq_match_step [Monad m] [LawfulMonad m] [Iterator α m β] [Finite α m]
     {it : IterM (α := α) m β} :
     it.toListRev = (do
       match ← it.step with
@@ -116,16 +116,16 @@ theorem IterM.toListRev_of_step [Monad m] [LawfulMonad m] [Iterator α m β] [Fi
   rw [toListRev.go]
   apply bind_congr
   intro step
-  cases step.casesHelper <;> simp [IterM.toListRev.go.aux₂]
+  cases step using PlausibleIterStep.casesOn <;> simp [IterM.toListRev.go.aux₂]
 
 theorem IterM.reverse_toListRev [Monad m] [LawfulMonad m] [Iterator α m β] [Finite α m]
     [IteratorCollect α m] [LawfulIteratorCollect α m]
     {it : IterM (α := α) m β} :
     List.reverse <$> it.toListRev = it.toList := by
   apply Eq.symm
-  induction it using IterM.induct
+  induction it using IterM.inductSteps
   rename_i it ihy ihs
-  rw [toListRev_of_step, toList_of_step, map_eq_pure_bind, bind_assoc]
+  rw [toListRev_eq_match_step, toList_eq_match_step, map_eq_pure_bind, bind_assoc]
   apply bind_congr
   intro step
   split <;> simp (discharger := assumption) [ihy, ihs]

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

@@ -14,17 +14,32 @@ iterator `it` to an element of `motive it` by defining `f it` in terms of the va
 the plausible successors of `it'.
 -/
 @[specialize]
-def IterM.induct {α m β} [Iterator α m β] [Finite α m]
+def IterM.inductSteps {α m β} [Iterator α m β] [Finite α m]
   (motive : IterM (α := α) m β → Sort x)
   (step : (it : IterM (α := α) m β) →
     (ih_yield : ∀ {it' : IterM (α := α) m β} {out : β},
       it.IsPlausibleStep (.yield it' out) → motive it') →
-    (ih_skip : ∀ {it' : IterM (α := α) m β}, it.IsPlausibleStep (.skip it') → motive it' ) →
+    (ih_skip : ∀ {it' : IterM (α := α) m β}, it.IsPlausibleStep (.skip it') → motive it') →
     motive it)
   (it : IterM (α := α) m β) : motive it :=
   step it
-    (fun {it' _} _ => IterM.induct motive step it')
-    (fun {it'} _ => IterM.induct motive step it')
+    (fun {it' _} _ => inductSteps motive step it')
+    (fun {it'} _ => inductSteps motive step it')
 termination_by it.finitelyManySteps
 
+/--
+Induction principle for productive monadic iterators: One can define a function `f` that maps every
+iterator `it` to an element of `motive it` by defining `f it` in terms of the values of `f` on
+the plausible skip successors of `it'.
+-/
+@[specialize]
+def IterM.inductSkips {α m β} [Iterator α m β] [Productive α m]
+  (motive : IterM (α := α) m β → Sort x)
+  (step : (it : IterM (α := α) m β) →
+    (ih_skip : ∀ {it' : IterM (α := α) m β}, it.IsPlausibleStep (.skip it') → motive it') →
+    motive it)
+  (it : IterM (α := α) m β) : motive it :=
+  step it (fun {it'} _ => inductSkips motive step it')
+termination_by it.finitelyManySkips
+
 end Std.Iterators

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

@@ -17,6 +17,6 @@ namespace Std.Iterators
 @[always_inline, inline]
 def _root_.List.iter {α : Type w} (l : List α) :
     Iter (α := ListIterator α) α :=
-  ((l.iterM Id).toPureIter : Iter α)
+  ((l.iterM Id).toIter : Iter α)
 
 end Std.Iterators