From 5963bc8b8a969251d74a80ac5b65ef8e9d91c58c Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Fri, 6 Jun 2025 10:06:59 +0200
Subject: [PATCH] fix: remove `IteratorLoop` instances without associated
 `LawfulIteratorLoop` instances (#8629)

This PR replaces special, more optimized `IteratorLoop` instances, for
which no lawfulness proof has been made, with the verified default
implementation. The specialization of the loop/collect implementations
is low priority, but having lawfulness instances for all iterators is
important for verification.
---
 .../Iterators/Combinators/Monadic/Take.lean   | 30 --------------
 .../Combinators/Monadic/TakeWhile.lean        | 41 +------------------
 2 files changed, 2 insertions(+), 69 deletions(-)

diff --git a/src/Std/Data/Iterators/Combinators/Monadic/Take.lean b/src/Std/Data/Iterators/Combinators/Monadic/Take.lean
index 542bb0115b..19d5675faf 100644
--- a/src/Std/Data/Iterators/Combinators/Monadic/Take.lean
+++ b/src/Std/Data/Iterators/Combinators/Monadic/Take.lean
@@ -138,36 +138,6 @@ instance Take.instIteratorCollectPartial [Monad m] [Monad n] [Iterator α m β]
     IteratorCollectPartial (Take α m β) m n :=
   .defaultImplementation
 
-private def Take.PlausibleForInStep {β : Type u} {γ : Type v}
-    (f : β → γ → ForInStep γ → Prop) :
-    β → γ × Nat → (ForInStep (γ × Nat)) → Prop
-  | out, (c, n), ForInStep.yield (c', n') => n = n' + 1 ∧ f out c (.yield c')
-  | _, _, .done _ => True
-
-private def Take.wellFounded_plausibleForInStep {α β : Type w} {m : Type w → Type w'}
-    [Monad m] [Iterator α m β] {γ : Type x}
-    {f : β → γ → ForInStep γ → Prop} (wf : IteratorLoop.WellFounded (Take α m β) m f) :
-    IteratorLoop.WellFounded α m (PlausibleForInStep f) := by
-      simp only [IteratorLoop.WellFounded] at ⊢ wf
-      letI : WellFoundedRelation _ := ⟨_, wf⟩
-      apply Subrelation.wf
-        (r := InvImage WellFoundedRelation.rel fun p => (p.1.take (p.2.2 + 1), p.2.1))
-        (fun {p q} h => by
-          simp only [InvImage, WellFoundedRelation.rel, this, IteratorLoop.rel,
-            IterM.IsPlausibleStep, Iterator.IsPlausibleStep]
-          obtain ⟨out, h, h'⟩ | ⟨h, h'⟩ := h
-          · apply Or.inl
-            exact ⟨out, .yield h (by simp only [IterM.take, internalState_toIterM,
-                Nat.add_right_cancel_iff, this]; exact h'.1), h'.2⟩
-          · apply Or.inr
-            refine ⟨?_, by rw [h']⟩
-            rw [h']
-            apply PlausibleStep.skip
-            · exact h
-            · rfl)
-      apply InvImage.wf
-      exact WellFoundedRelation.wf
-
 instance Take.instIteratorLoop [Monad m] [Monad n] [Iterator α m β]
     [IteratorLoop α m n] [MonadLiftT m n] :
     IteratorLoop (Take α m β) m n :=
diff --git a/src/Std/Data/Iterators/Combinators/Monadic/TakeWhile.lean b/src/Std/Data/Iterators/Combinators/Monadic/TakeWhile.lean
index f912e66cdc..9b18315e01 100644
--- a/src/Std/Data/Iterators/Combinators/Monadic/TakeWhile.lean
+++ b/src/Std/Data/Iterators/Combinators/Monadic/TakeWhile.lean
@@ -232,47 +232,10 @@ instance TakeWhile.instIteratorCollectPartial [Monad m] [Monad n] [Iterator α m
     IteratorCollectPartial (TakeWhile α m β P) m n :=
   .defaultImplementation
 
-private def TakeWhile.PlausibleForInStep {β : Type u} {γ : Type v}
-    (P : β → PostconditionT m (ULift Bool))
-    (f : β → γ → ForInStep γ → Prop) :
-    β → γ → (ForInStep γ) → Prop
-  | out, c, ForInStep.yield c' => (P out).Property (.up true) ∧ f out c (.yield c')
-  | _, _, .done _ => True
-
-private def TakeWhile.wellFounded_plausibleForInStep {α β : Type w} {m : Type w → Type w'}
-    [Monad m] [Iterator α m β] {γ : Type x} {P}
-    {f : β → γ → ForInStep γ → Prop} (wf : IteratorLoop.WellFounded (TakeWhile α m β P) m f) :
-    IteratorLoop.WellFounded α m (PlausibleForInStep P f) := by
-      simp only [IteratorLoop.WellFounded] at ⊢ wf
-      letI : WellFoundedRelation _ := ⟨_, wf⟩
-      apply Subrelation.wf
-        (r := InvImage WellFoundedRelation.rel fun p => (p.1.takeWhileWithPostcondition P, p.2))
-        (fun {p q} h => by
-          simp only [InvImage, WellFoundedRelation.rel, this, IteratorLoop.rel,
-            IterM.IsPlausibleStep, Iterator.IsPlausibleStep]
-          obtain ⟨out, h, h'⟩ | ⟨h, h'⟩ := h
-          · apply Or.inl
-            exact ⟨out, .yield h h'.1, h'.2⟩
-          · apply Or.inr
-            refine ⟨?_, h'⟩
-            exact PlausibleStep.skip h)
-      apply InvImage.wf
-      exact WellFoundedRelation.wf
-
 instance TakeWhile.instIteratorLoop [Monad m] [Monad n] [Iterator α m β]
     [IteratorLoop α m n] [MonadLiftT m n] :
-    IteratorLoop (TakeWhile α m β P) m n where
-  forIn lift {γ} Plausible wf it init f := by
-    refine IteratorLoop.forIn lift (γ := γ)
-        (PlausibleForInStep P Plausible)
-        (wellFounded_plausibleForInStep wf)
-        it.internalState.inner
-        init
-        fun out acc => do match ← (P out).operation with
-          | ⟨.up true, h⟩ => match ← f out acc with
-            | ⟨.yield c, h'⟩ => pure ⟨.yield c, h, h'⟩
-            | ⟨.done c, h'⟩ => pure ⟨.done c, .intro⟩
-          | ⟨.up false, h⟩ => pure ⟨.done acc, .intro⟩
+    IteratorLoop (TakeWhile α m β P) m n :=
+  .defaultImplementation
 
 instance TakeWhile.instIteratorForPartial [Monad m] [Monad n] [Iterator α m β]
     [IteratorLoopPartial α m n] [MonadLiftT m n] {P} :