address remarks

Author: datokrat

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

@@ -34,19 +34,19 @@ theorem Iter.toListRev_eq_toListRev_toIterM {α β} [Iterator α Id β] [Finite
   (rfl)
 
 @[simp]
-theorem Iter.ensureTerminationToArray_eq_toArray {α β} [Iterator α Id β] [Finite α Id] [IteratorCollect α Id Id]
+theorem Iter.toArray_ensureTermination {α β} [Iterator α Id β] [Finite α Id] [IteratorCollect α Id Id]
     [LawfulIteratorCollect α Id Id] {it : Iter (α := α) β} :
     it.ensureTermination.toArray = it.toArray :=
   (rfl)
 
 @[simp]
-theorem Iter.ensureTerminationToList_eq_toList {α β} [Iterator α Id β] [Finite α Id] [IteratorCollect α Id Id]
+theorem Iter.toList_ensureTermination {α β} [Iterator α Id β] [Finite α Id] [IteratorCollect α Id Id]
     [LawfulIteratorCollect α Id Id] {it : Iter (α := α) β} :
     it.ensureTermination.toList = it.toList :=
   (rfl)
 
 @[simp]
-theorem Iter.ensureTerminationToListRev_eq_toListRev {α β} [Iterator α Id β] [Finite α Id]
+theorem Iter.toListRev_ensureTermination_eq_toListRev {α β} [Iterator α Id β] [Finite α Id]
     {it : Iter (α := α) β} : it.ensureTermination.toListRev = it.toListRev :=
   (rfl)
 
@@ -68,23 +68,21 @@ theorem Iter.toList_toArray {α β} [Iterator α Id β] [Finite α Id] [Iterator
     it.toArray.toList = it.toList := by
   simp [toArray_eq_toArray_toIterM, toList_eq_toList_toIterM, ← IterM.toList_toArray]
 
-@[simp]
-theorem Iter.toList_ensureTerminationToArray {α β} [Iterator α Id β] [Finite α Id]
+theorem Iter.toList_toArray_ensureTermination {α β} [Iterator α Id β] [Finite α Id]
     [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id] {it : Iter (α := α) β} :
     it.ensureTermination.toArray.toList = it.toList := by
-  rw [ensureTerminationToArray_eq_toArray, toList_toArray]
+  simp
 
 @[simp]
 theorem Iter.toArray_toList {α β} [Iterator α Id β] [Finite α Id] [IteratorCollect α Id Id]
     [LawfulIteratorCollect α Id Id] {it : Iter (α := α) β} :
     it.toList.toArray = it.toArray := by
   simp [toArray_eq_toArray_toIterM, toList_eq_toList_toIterM, ← IterM.toArray_toList]
 
-@[simp]
-theorem Iter.toArray_ensureTerminationToList {α β} [Iterator α Id β] [Finite α Id]
+theorem Iter.toArray_toList_ensureTermination {α β} [Iterator α Id β] [Finite α Id]
     [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id] {it : Iter (α := α) β} :
     it.ensureTermination.toList.toArray = it.toArray := by
-  rw [ensureTerminationToList_eq_toList, toArray_toList]
+  simp
 
 @[simp]
 theorem Iter.reverse_toListRev [Iterator α Id β] [Finite α Id]
@@ -93,21 +91,20 @@ theorem Iter.reverse_toListRev [Iterator α Id β] [Finite α Id]
     it.toListRev.reverse = it.toList := by
   simp [toListRev_eq_toListRev_toIterM, toList_eq_toList_toIterM, ← IterM.reverse_toListRev]
 
-@[simp]
-theorem Iter.reverse_ensureTerminationToListRev [Iterator α Id β] [Finite α Id]
+theorem Iter.reverse_toListRev_ensureTermination [Iterator α Id β] [Finite α Id]
     [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id] {it : Iter (α := α) β} :
     it.ensureTermination.toListRev.reverse = it.toList := by
-  rw [ensureTerminationToListRev_eq_toListRev, reverse_toListRev]
+  simp
 
 theorem Iter.toListRev_eq {α β} [Iterator α Id β] [Finite α Id] [IteratorCollect α Id Id]
     [LawfulIteratorCollect α Id Id] {it : Iter (α := α) β} :
     it.toListRev = it.toList.reverse := by
   simp [Iter.toListRev_eq_toListRev_toIterM, Iter.toList_eq_toList_toIterM, IterM.toListRev_eq]
 
-theorem Iter.ensureTerminationToListRev_eq {α β} [Iterator α Id β] [Finite α Id]
+theorem Iter.toListRev_ensureTermination {α β} [Iterator α Id β] [Finite α Id]
     [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id] {it : Iter (α := α) β} :
     it.ensureTermination.toListRev = it.toList.reverse := by
-  rw [ensureTerminationToListRev_eq_toListRev, toListRev_eq]
+  simp [toListRev_eq]
 
 theorem Iter.toArray_eq_match_step {α β} [Iterator α Id β] [Finite α Id] [IteratorCollect α Id Id]
     [LawfulIteratorCollect α Id Id] {it : Iter (α := α) β} :
@@ -120,13 +117,13 @@ theorem Iter.toArray_eq_match_step {α β} [Iterator α Id β] [Finite α Id] [I
   generalize it.toIterM.step.run = step
   cases step.inflate using PlausibleIterStep.casesOn <;> simp
 
-theorem Iter.ensureTerminationToArray_eq_match_step {α β} [Iterator α Id β] [Finite α Id] [IteratorCollect α Id Id]
+theorem Iter.toArray_ensureTermination_eq_match_step {α β} [Iterator α Id β] [Finite α Id] [IteratorCollect α Id Id]
     [LawfulIteratorCollect α Id Id] {it : Iter (α := α) β} :
     it.ensureTermination.toArray = match it.step.val with
       | .yield it' out => #[out] ++ it'.toArray
       | .skip it' => it'.toArray
       | .done => #[] := by
-  rw [ensureTerminationToArray_eq_toArray, toArray_eq_match_step]
+  rw [toArray_ensureTermination, toArray_eq_match_step]
 
 theorem Iter.toList_eq_match_step {α β} [Iterator α Id β] [Finite α Id] [IteratorCollect α Id Id]
     [LawfulIteratorCollect α Id Id] {it : Iter (α := α) β} :
@@ -137,13 +134,13 @@ theorem Iter.toList_eq_match_step {α β} [Iterator α Id β] [Finite α Id] [It
   rw [← Iter.toList_toArray, Iter.toArray_eq_match_step]
   split <;> simp [Iter.toList_toArray]
 
-theorem Iter.ensureTerminationToList_eq_match_step {α β} [Iterator α Id β] [Finite α Id] [IteratorCollect α Id Id]
+theorem Iter.toList_ensureTermination_eq_match_step {α β} [Iterator α Id β] [Finite α Id] [IteratorCollect α Id Id]
     [LawfulIteratorCollect α Id Id] {it : Iter (α := α) β} :
     it.ensureTermination.toList = match it.step.val with
       | .yield it' out => out :: it'.toList
       | .skip it' => it'.toList
       | .done => [] := by
-  rw [ensureTerminationToList_eq_toList, toList_eq_match_step]
+  rw [toList_ensureTermination, toList_eq_match_step]
 
 theorem Iter.toListRev_eq_match_step {α β} [Iterator α Id β] [Finite α Id] {it : Iter (α := α) β} :
     it.toListRev = match it.step.val with
@@ -154,12 +151,12 @@ theorem Iter.toListRev_eq_match_step {α β} [Iterator α Id β] [Finite α Id]
   generalize it.toIterM.step.run = step
   cases step.inflate using PlausibleIterStep.casesOn <;> simp
 
-theorem Iter.ensureTerminationToListRev_eq_match_step {α β} [Iterator α Id β] [Finite α Id] {it : Iter (α := α) β} :
+theorem Iter.toListRev_ensureTermination_eq_match_step {α β} [Iterator α Id β] [Finite α Id] {it : Iter (α := α) β} :
     it.ensureTermination.toListRev = match it.step.val with
       | .yield it' out => it'.toListRev ++ [out]
       | .skip it' => it'.toListRev
       | .done => [] := by
-  rw [ensureTerminationToListRev_eq_toListRev, toListRev_eq_match_step]
+  rw [toListRev_ensureTermination_eq_toListRev, toListRev_eq_match_step]
 
 theorem Iter.getElem?_toList_eq_atIdxSlow? {α β}
     [Iterator α Id β] [Finite α Id] [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id]

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

@@ -88,7 +88,7 @@ theorem IterM.DefaultConsumers.toArrayMapped_eq_match_step [Monad n] [LawfulMona
     simp [IterM.DefaultConsumers.toArrayMapped.go.aux₂]
 
 @[simp]
-theorem IterM.ensureTerminationToArray_eq_toArray [Monad m] [Iterator α m β] [Finite α m]
+theorem IterM.toArray_ensureTermination [Monad m] [Iterator α m β] [Finite α m]
     [IteratorCollect α m m] {it : IterM (α := α) m β} :
     it.ensureTermination.toArray = it.toArray :=
   (rfl)
@@ -104,17 +104,17 @@ theorem IterM.toArray_eq_match_step [Monad m] [LawfulMonad m] [Iterator α m β]
   rw [IterM.DefaultConsumers.toArrayMapped_eq_match_step]
   simp [bind_pure_comp, pure_bind]
 
-theorem IterM.ensureTerminationToArray_eq_match_step [Monad m] [LawfulMonad m] [Iterator α m β]
+theorem IterM.toArray_ensureTermination_eq_match_step [Monad m] [LawfulMonad m] [Iterator α m β]
     [Finite α m] [IteratorCollect α m m] [LawfulIteratorCollect α m m] :
     it.ensureTermination.toArray = (do
       match (← it.step).inflate.val with
       | .yield it' out => return #[out] ++ (← it'.toArray)
       | .skip it' => it'.toArray
       | .done => return #[]) := by
-  rw [ensureTerminationToArray_eq_toArray, toArray_eq_match_step]
+  rw [toArray_ensureTermination, toArray_eq_match_step]
 
 @[simp]
-theorem IterM.ensureTerminationToList_eq_toList [Monad m] [Iterator α m β] [Finite α m]
+theorem IterM.toList_ensureTermination [Monad m] [Iterator α m β] [Finite α m]
     [IteratorCollect α m m] {it : IterM (α := α) m β} :
     it.ensureTermination.toList = it.toList :=
   (rfl)
@@ -125,23 +125,21 @@ theorem IterM.toList_toArray [Monad m] [Iterator α m β] [Finite α m] [Iterato
     Array.toList <$> it.toArray = it.toList := by
   simp [IterM.toList]
 
-@[simp]
-theorem IterM.toList_ensureTerminationToArray [Monad m] [Iterator α m β] [Finite α m]
+theorem IterM.toList_toArray_ensureTermination [Monad m] [Iterator α m β] [Finite α m]
     [IteratorCollect α m m] {it : IterM (α := α) m β} :
     Array.toList <$> it.ensureTermination.toArray = it.toList := by
-  rw [ensureTerminationToArray_eq_toArray, toList_toArray]
+  simp
 
 @[simp]
 theorem IterM.toArray_toList [Monad m] [LawfulMonad m] [Iterator α m β] [Finite α m]
     [IteratorCollect α m m] {it : IterM (α := α) m β} :
     List.toArray <$> it.toList = it.toArray := by
   simp [IterM.toList, -toList_toArray]
 
-@[simp]
-theorem IterM.toArray_ensureTerminationToList [Monad m] [LawfulMonad m] [Iterator α m β] [Finite α m]
+theorem IterM.toArray_toList_ensureTermination [Monad m] [LawfulMonad m] [Iterator α m β] [Finite α m]
     [IteratorCollect α m m] {it : IterM (α := α) m β} :
     List.toArray <$> it.ensureTermination.toList = it.toArray := by
-  rw [ensureTerminationToList_eq_toList, toArray_toList]
+  rw [toList_ensureTermination, toArray_toList]
 
 theorem IterM.toList_eq_match_step [Monad m] [LawfulMonad m] [Iterator α m β] [Finite α m]
     [IteratorCollect α m m] [LawfulIteratorCollect α m m] {it : IterM (α := α) m β} :
@@ -156,17 +154,17 @@ theorem IterM.toList_eq_match_step [Monad m] [LawfulMonad m] [Iterator α m β]
   intro step
   split <;> simp
 
-theorem IterM.ensureTerminationToList_eq_match_step [Monad m] [LawfulMonad m] [Iterator α m β]
+theorem IterM.toList_ensureTermination_eq_match_step [Monad m] [LawfulMonad m] [Iterator α m β]
     [Finite α m] [IteratorCollect α m m] [LawfulIteratorCollect α m m] {it : IterM (α := α) m β} :
     it.ensureTermination.toList = (do
       match (← it.step).inflate.val with
       | .yield it' out => return out :: (← it'.toList)
       | .skip it' => it'.toList
       | .done => return []) := by
-  rw [ensureTerminationToList_eq_toList, toList_eq_match_step]
+  rw [toList_ensureTermination, toList_eq_match_step]
 
 @[simp]
-theorem IterM.ensureTerminationToListRev_eq_toListRev [Monad m] [Iterator α m β] [Finite α m]
+theorem IterM.toListRev_ensureTermination_eq_toListRev [Monad m] [Iterator α m β] [Finite α m]
     {it : IterM (α := α) m β} :
     it.ensureTermination.toListRev = it.toListRev :=
   (rfl)
@@ -230,14 +228,14 @@ theorem IterM.toListRev_eq_match_step [Monad m] [LawfulMonad m] [Iterator α m 
   intro step
   cases step.inflate using PlausibleIterStep.casesOn <;> simp [IterM.toListRev.go.aux₂]
 
-theorem IterM.ensureTerminationToListRev_eq_match_step [Monad m] [LawfulMonad m] [Iterator α m β]
+theorem IterM.toListRev_ensureTermination_eq_match_step [Monad m] [LawfulMonad m] [Iterator α m β]
     [Finite α m] {it : IterM (α := α) m β} :
     it.ensureTermination.toListRev = (do
       match (← it.step).inflate.val with
       | .yield it' out => return (← it'.toListRev) ++ [out]
       | .skip it' => it'.toListRev
       | .done => return []) := by
-  rw [ensureTerminationToListRev_eq_toListRev, toListRev_eq_match_step]
+  rw [toListRev_ensureTermination_eq_toListRev, toListRev_eq_match_step]
 
 @[simp]
 theorem IterM.reverse_toListRev [Monad m] [LawfulMonad m] [Iterator α m β] [Finite α m]
@@ -253,19 +251,19 @@ theorem IterM.reverse_toListRev [Monad m] [LawfulMonad m] [Iterator α m β] [Fi
   cases step.inflate using PlausibleIterStep.casesOn <;> simp (discharger := assumption) [ihy, ihs]
 
 @[simp]
-theorem IterM.reverse_ensureTerminationToListRev [Monad m] [LawfulMonad m] [Iterator α m β]
+theorem IterM.reverse_toListRev_ensureTermination [Monad m] [LawfulMonad m] [Iterator α m β]
     [Finite α m] [IteratorCollect α m m] [LawfulIteratorCollect α m m]
     {it : IterM (α := α) m β} :
     List.reverse <$> it.ensureTermination.toListRev = it.toList := by
-  rw [ensureTerminationToListRev_eq_toListRev, reverse_toListRev]
+  rw [toListRev_ensureTermination_eq_toListRev, reverse_toListRev]
 
 theorem IterM.toListRev_eq [Monad m] [LawfulMonad m] [Iterator α m β] [Finite α m]
     [IteratorCollect α m m] [LawfulIteratorCollect α m m]
     {it : IterM (α := α) m β} :
     it.toListRev = List.reverse <$> it.toList := by
   simp [← IterM.reverse_toListRev]
 
-theorem IterM.ensureTerminationToListRev_eq [Monad m] [LawfulMonad m] [Iterator α m β] [Finite α m]
+theorem IterM.toListRev_ensureTermination [Monad m] [LawfulMonad m] [Iterator α m β] [Finite α m]
     [IteratorCollect α m m] [LawfulIteratorCollect α m m]
     {it : IterM (α := α) m β} :
     it.ensureTermination.toListRev = List.reverse <$> it.toList := by

src/Init/Internal/ExtrinsicTermination.lean

@@ -71,7 +71,7 @@ public def extrinsicFix [∀ a, Nonempty (C a)] (F : ∀ a, (∀ a', C a') → C
     -- In effect, `extrinsicFix` is opaque if `TerminatesTotally F` is false.
     opaqueFix F a
 
-public def extrinsicFix_eq [∀ a, Nonempty (C a)] {F : ∀ a, (∀ a', C a') → C a}
+public theorem extrinsicFix_eq [∀ a, Nonempty (C a)] {F : ∀ a, (∀ a', C a') → C a}
     (h : TerminatesTotally F) {a : α} :
     extrinsicFix F a = F a (extrinsicFix F) := by
   simp only [extrinsicFix, dif_pos h]
@@ -128,7 +128,7 @@ public def extrinsicFix₂ [∀ a b, Nonempty (C₂ a b)]
     F x.1 x.2 (fun a b => G ⟨a, b⟩)
   extrinsicFix (C := fun x : PSigma β => C₂ x.1 x.2) F' ⟨a, b⟩
 
-public def extrinsicFix₂_eq [∀ a b, Nonempty (C₂ a b)]
+public theorem extrinsicFix₂_eq [∀ a b, Nonempty (C₂ a b)]
     {F : (a : α) → (b : β a) → ((a' : α) → (b' : β a') → C₂ a' b') → C₂ a b}
     (h : TerminatesTotally₂ F) {a : α} {b : β a} :
     extrinsicFix₂ F a b = F a b (extrinsicFix₂ F) := by