cleanups

Author: datokrat

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

@@ -107,8 +107,10 @@ theorem Iter.forIn'_eq_match_step {α β : Type w} [Iterator α Id β]
             fun out h' acc => f out (.indirect ⟨_, rfl, h⟩ h') acc
       | .done _ => return init) := by
   simp only [forIn'_eq]
-  rw [IterM.DefaultConsumers.forIn'_eq_match_step (fun _ _ _ => True) IteratorLoop.wellFounded_of_finite
-    (f' := fun a b c => (⟨·, trivial⟩) <$> f a (Iter.isPlausibleIndirectOutput_iff_isPlausibleIndirectOutput_toIterM.mpr b) c)
+  rw [IterM.DefaultConsumers.forIn'_eq_match_step (fun _ _ _ => True)
+    IteratorLoop.wellFounded_of_finite
+    (f' := fun a b c => (⟨·, trivial⟩) <$>
+        f a (Iter.isPlausibleIndirectOutput_iff_isPlausibleIndirectOutput_toIterM.mpr b) c)
     (hf := by simp)]
   simp only [Iter.step]
   cases it.toIterM.step.run.inflate using PlausibleIterStep.casesOn
@@ -120,16 +122,20 @@ theorem Iter.forIn'_eq_match_step {α β : Type w} [Iterator α Id β]
     · simp only
       apply IterM.DefaultConsumers.forIn'_eq_forIn' (fun _ _ _ => True)
         IteratorLoop.wellFounded_of_finite
-        (f' := fun a b c => (⟨·, trivial⟩) <$> f a (Iter.isPlausibleIndirectOutput_iff_isPlausibleIndirectOutput_toIterM.mpr b) c)
-        (g' := fun a b c => (⟨·, trivial⟩) <$> f a (Iter.isPlausibleIndirectOutput_iff_isPlausibleIndirectOutput_toIterM.mpr (.indirect ⟨_, rfl, ‹_›⟩ b)) c)
+        (f' := fun a b c => (⟨·, trivial⟩) <$>
+            f a (Iter.isPlausibleIndirectOutput_iff_isPlausibleIndirectOutput_toIterM.mpr b) c)
+        (g' := fun a b c => (⟨·, trivial⟩) <$>
+            f a (Iter.isPlausibleIndirectOutput_iff_isPlausibleIndirectOutput_toIterM.mpr (.indirect ⟨_, rfl, ‹_›⟩ b)) c)
       · simp
       · simp
       · simp
   · simp only
     apply IterM.DefaultConsumers.forIn'_eq_forIn' (fun _ _ _ => True)
       IteratorLoop.wellFounded_of_finite
-      (f' := fun a b c => (⟨·, trivial⟩) <$> f a (Iter.isPlausibleIndirectOutput_iff_isPlausibleIndirectOutput_toIterM.mpr b) c)
-      (g' := fun a b c => (⟨·, trivial⟩) <$> f a (Iter.isPlausibleIndirectOutput_iff_isPlausibleIndirectOutput_toIterM.mpr (.indirect ⟨_, rfl, ‹_›⟩ b)) c)
+      (f' := fun a b c => (⟨·, trivial⟩) <$>
+          f a (Iter.isPlausibleIndirectOutput_iff_isPlausibleIndirectOutput_toIterM.mpr b) c)
+      (g' := fun a b c => (⟨·, trivial⟩) <$>
+          f a (Iter.isPlausibleIndirectOutput_iff_isPlausibleIndirectOutput_toIterM.mpr (.indirect ⟨_, rfl, ‹_›⟩ b)) c)
     · simp
     · simp
     · simp

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

@@ -15,8 +15,7 @@ public section
 namespace Std.Iterators
 
 theorem IterM.DefaultConsumers.forIn'_eq_match_step {α β : Type w} {m : Type w → Type w'}
-    [Iterator α m β]
-    {n : Type x → Type x'} [Monad n] [LawfulMonad n]
+    [Iterator α m β] {n : Type x → Type x'} [Monad n] [LawfulMonad n]
     {lift : ∀ γ δ, (γ → n δ) → m γ → n δ} {γ : Type x}
     {it : IterM (α := α) m β} {init : γ}
     {P hP} {f : (b : β) → P b → (c : γ) → n (ForInStep γ)}

src/Init/Data/Range/Polymorphic/RangeIterator.lean

@@ -512,7 +512,7 @@ where finally
     refine ⟨1, ?_⟩
     simpa [succMany?_one] using hs
 
-private theorem Iterator.instIteratorLoop.loop_eq_loopWf [UpwardEnumerable α] [LE α] [DecidableLE α]
+private theorem Iterator.instIteratorLoop.loop_eq_wf [UpwardEnumerable α] [LE α] [DecidableLE α]
     [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] [Monad n] [LawfulMonad n]
     {γ LargeEnough hl upperBound} {next hn} {acc} (Pl wf f) :
     loop γ LargeEnough hl upperBound acc next hn (fun out h₁ h₂ acc => Subtype.val <$> f out h₁ h₂ acc) =
@@ -620,7 +620,7 @@ instance Iterator.instLawfulIteratorLoop [UpwardEnumerable α] [LE α] [Decidabl
     split; rotate_left
     · simp [Monadic.step_eq_step, Monadic.step, Internal.LawfulMonadLiftBindFunction.liftBind_pure]
     rename_i next _
-    rw [instIteratorLoop.loop_eq_loopWf Pl wf, instIteratorLoop.loopWf_eq (lift := lift)]
+    rw [instIteratorLoop.loop_eq_wf Pl wf, instIteratorLoop.loopWf_eq (lift := lift)]
     simp only [Monadic.step_eq_step, Monadic.step, instLawfulMonadLiftFunction.liftBind_pure,
       Shrink.inflate_deflate]
     split
@@ -1110,7 +1110,7 @@ where finally
     refine ⟨1, ?_⟩
     simpa [succMany?_one] using hs
 
-private theorem Iterator.instIteratorLoop.loop_eq_loopWf [UpwardEnumerable α] [LT α] [DecidableLT α]
+private theorem Iterator.instIteratorLoop.loop_eq_wf [UpwardEnumerable α] [LT α] [DecidableLT α]
     [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α] [Monad n] [LawfulMonad n]
     {γ LargeEnough hl upperBound} {next hn} {acc} (Pl wf f) :
     loop γ LargeEnough hl upperBound acc next hn (fun out h₁ h₂ acc => Subtype.val <$> f out h₁ h₂ acc) =
@@ -1218,7 +1218,7 @@ instance Iterator.instLawfulIteratorLoop [UpwardEnumerable α] [LT α] [Decidabl
     split; rotate_left
     · simp [Monadic.step_eq_step, Monadic.step, Internal.LawfulMonadLiftBindFunction.liftBind_pure]
     rename_i next _
-    rw [instIteratorLoop.loop_eq_loopWf Pl wf, instIteratorLoop.loopWf_eq (lift := lift)]
+    rw [instIteratorLoop.loop_eq_wf Pl wf, instIteratorLoop.loopWf_eq (lift := lift)]
     simp only [Monadic.step_eq_step, Monadic.step, instLawfulMonadLiftFunction.liftBind_pure,
       Shrink.inflate_deflate]
     split
@@ -1614,7 +1614,7 @@ where finally
     refine ⟨1, ?_⟩
     simpa [succMany?_one] using hs
 
-private theorem Iterator.instIteratorLoop.loop_eq_loopWf [UpwardEnumerable α]
+private theorem Iterator.instIteratorLoop.loop_eq_wf [UpwardEnumerable α]
     [LawfulUpwardEnumerable α] [Monad n] [LawfulMonad n]
     {γ LargeEnough hl} {next hn} {acc} (Pl wf f) :
     loop γ LargeEnough hl acc next hn (fun out h acc => Subtype.val <$> f out h acc) =
@@ -1707,7 +1707,7 @@ instance Iterator.instLawfulIteratorLoop [UpwardEnumerable α]
     split; rotate_left
     · simp [Monadic.step_eq_step, Monadic.step, Internal.LawfulMonadLiftBindFunction.liftBind_pure]
     rename_i next _
-    rw [instIteratorLoop.loop_eq_loopWf Pl wf, instIteratorLoop.loopWf_eq (lift := lift)]
+    rw [instIteratorLoop.loop_eq_wf Pl wf, instIteratorLoop.loopWf_eq (lift := lift)]
     simp only [Monadic.step_eq_step, Monadic.step, instLawfulMonadLiftFunction.liftBind_pure,
       Shrink.inflate_deflate]
     apply bind_congr; intro forInStep

src/Init/Internal/ExtrinsicTermination.lean

@@ -205,8 +205,8 @@ public def TerminatesTotally₃
 /-
 SAFE assuming that the code generated by iteration over `F` is compatible
 with the kernel semantics of iteration over
-`F' : (a : α) → (b : β a) → ((a' : α) → (b' : β a') → C₂ a' b') → C₂ a b`
-for all `F'` as in `TerminatesTotally₂`.
+`F' : ∀ a b c, (∀ a' b' c', C₃ a' b' c') → C₃ a b c`
+for all `F'` as in `TerminatesTotally₃`.
 -/
 @[implemented_by opaqueFix₃]
 public def extrinsicFix₃ [∀ a b c, Nonempty (C₃ a b c)]

src/Lean/Elab/Tactic/BVDecide/LRAT/Trim.lean

@@ -192,7 +192,6 @@ where
           | .del .. => go worklist
         | none => go worklist
 
-set_option trace.compiler.ir.result true in
 /--
 Map the set of used proof steps to a new LRAT proof that has no holes in the sequence of proof
 identifiers.