make it compile

Author: datokrat

src/Init/Data/Iterators/Basic.lean

@@ -8,6 +8,7 @@ module
 prelude
 public import Init.Classical
 public import Init.Ext
+public import Init.Internal.MonadAttach
 
 set_option doc.verso true
 
@@ -393,6 +394,31 @@ abbrev IterM.Step {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator
     (it : IterM (α := α) m β) :=
   PlausibleIterStep it.IsPlausibleStep
 
+/--
+Makes a single step with the given iterator `it`, potentially emitting a value and providing a
+succeeding iterator. If this function is used recursively, termination can sometimes be proved with
+the termination measures `it.finitelyManySteps` and `it.finitelyManySkips`.
+-/
+@[always_inline, inline, expose]
+def IterM.step {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β]
+    (it : IterM (α := α) m β) : m (Shrink it.Step) :=
+  Iterator.step it
+
+/--
+Asserts that certain step is plausibly the successor of a given iterator. What "plausible" means
+is up to the `Iterator` instance but it should be strong enough to allow termination proofs.
+-/
+@[expose]
+abbrev IterM.IsPlausibleStepE {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β]
+    [MonadAttach m] (it : IterM (α := α) m β) (step : IterStep (IterM (α := α) m β) β) : Prop :=
+  ∃ h, MonadAttach.CanReturn it.step (.deflate ⟨step, h⟩)
+
+theorem IterM.isPlausibleStep_of_isPlausibleStepE {α : Type w} {m : Type w → Type w'} {β : Type w}
+    [Iterator α m β] [MonadAttach m]
+    {it : IterM (α := α) m β} {step : IterStep (IterM (α := α) m β) β}
+    (h : it.IsPlausibleStepE step) : it.IsPlausibleStep step :=
+  h.choose
+
 /--
 Asserts that a certain output value could plausibly be emitted by the given iterator in its next
 step.
@@ -411,6 +437,21 @@ def IterM.IsPlausibleSuccessorOf {α : Type w} {m : Type w → Type w'} {β : Ty
     (it' it : IterM (α := α) m β) : Prop :=
   ∃ step, step.successor = some it' ∧ it.IsPlausibleStep step
 
+/--
+Asserts that a certain iterator `it'` could plausibly be the directly succeeding iterator of another
+given iterator `it`.
+-/
+@[expose]
+def IterM.IsPlausibleSuccessorOfE {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β]
+    [MonadAttach m] (it' it : IterM (α := α) m β) : Prop :=
+  ∃ step, step.successor = some it' ∧ it.IsPlausibleStepE step
+
+theorem IterM.isPlausibleSuccessorOf_of_isPlausibleSuccessorOfE {α : Type w} {m : Type w → Type w'}
+    {β : Type w} [Iterator α m β] [MonadAttach m] {it' it : IterM (α := α) m β}
+    (h : it'.IsPlausibleSuccessorOfE it) : it'.IsPlausibleSuccessorOf it :=
+  let ⟨step, hs, hp⟩ := h
+  ⟨step, hs, isPlausibleStep_of_isPlausibleStepE hp⟩
+
 /--
 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`).
@@ -420,16 +461,6 @@ def IterM.IsPlausibleSkipSuccessorOf {α : Type w} {m : Type w → Type w'} {β
     [Iterator α m β] (it' it : IterM (α := α) m β) : Prop :=
   it.IsPlausibleStep (.skip it')
 
-/--
-Makes a single step with the given iterator `it`, potentially emitting a value and providing a
-succeeding iterator. If this function is used recursively, termination can sometimes be proved with
-the termination measures `it.finitelyManySteps` and `it.finitelyManySkips`.
--/
-@[always_inline, inline, expose]
-def IterM.step {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β]
-    (it : IterM (α := α) m β) : m (Shrink it.Step) :=
-  Iterator.step it
-
 end Monadic
 
 section Pure
@@ -734,7 +765,7 @@ Termination measure to be used in well-founded recursive functions recursing ove
 (see also `Finite`).
 -/
 @[expose]
-def IterM.finitelyManyStepsExtrinsic {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β]
+def IterM.finitelyManySteps! {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β]
     (it : IterM (α := α) m β) : IterM.TerminationMeasures.Finite α m :=
   ⟨it⟩
 

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

@@ -56,10 +56,8 @@ def Iter.Partial.instForIn' {α : Type w} {β : Type w} {n : Type x → Type x'}
     [Iterator α Id β] [IteratorLoop α Id n] :
     ForIn' n (Iter.Partial (α := α) β) β ⟨fun it out => it.it.IsPlausibleIndirectOutput out⟩ where
   forIn' it init f :=
-    IteratorLoop.forIn (α := α) (m := Id) (n := n) (fun _ _ f c => f c.run) _
-      it.it.toIterM init
-      fun out h acc =>
-        f out (Iter.isPlausibleIndirectOutput_iff_isPlausibleIndirectOutput_toIterM.mpr h) acc
+    haveI := @Iter.instForIn'
+    forIn' it.it init f
 
 instance (α : Type w) (β : Type w) (n : Type x → Type x') [Monad n]
     [Iterator α Id β] [IteratorLoop α Id n] :

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

@@ -10,7 +10,6 @@ public import Init.Data.Iterators.Consumers.Monadic.Partial
 public import Init.Data.Iterators.Consumers.Monadic.Total
 public import Init.Data.Iterators.Internal.LawfulMonadLiftFunction
 public import Init.Internal.ExtrinsicTermination
-public import Init.Internal.MonadAttach
 
 @[expose] public section
 
@@ -61,6 +60,11 @@ end Typeclasses
 
 section ToArray
 
+def IterM.DefaultConsumers.toArrayMapped.RecursionRel {α β : Type w} {m : Type w → Type w'}
+    [Iterator α m β] {γ : Type w} (x' x : (_ : IterM (α := α) m β) ×' Array γ) : Prop :=
+  (∃ out, x.1.IsPlausibleStep (.yield x'.1 out) ∧ ∃ fx, x'.2 = x.2.push fx) ∨
+    (x.1.IsPlausibleStep (.skip x'.1) ∧ x'.2 = x.2)
+
 /--
 This is an internal function used in `IteratorCollect.defaultImplementation`.
 
@@ -69,7 +73,7 @@ of `f` into an array.
 -/
 @[always_inline, no_expose]
 def IterM.DefaultConsumers.toArrayMapped {α β : Type w} {m : Type w → Type w'}
-    {n : Type w → Type w''} [Monad n] [MonadAttach n] [Iterator α m β]
+    {n : Type w → Type w''} [Monad n] [Iterator α m β]
     (lift : ⦃α : Type w⦄ → m α → n α) {γ : Type w} (f : β → n γ)
     (it : IterM (α := α) m β) : n (Array γ) :=
   letI : MonadLift m n := ⟨lift (α := _)⟩
@@ -78,24 +82,43 @@ where
   @[always_inline]
   go it (acc : Array γ) : n (Array γ) :=
     letI : MonadLift m n := ⟨lift (α := _)⟩
-    extrinsicFix₂ (C₂ := fun _ _ => n (Array γ))
-    (fun x' x => (∃ out h, MonadAttach.CanReturn (m := n) x.1.step (.deflate <| .yield x'.1 out h) ∧ ∃ fx, MonadAttach.CanReturn (f out) fx ∧ x'.2 = x.2.push fx) ∨ (∃ h, MonadAttach.CanReturn (m := n) x.1.step (.deflate <| .skip x'.1 h) ∧ x'.2 = x.2))
+    extrinsicFixE₂ (C₂ := fun _ _ => n (Array γ)) (InvImage TerminationMeasures.Finite.Rel (·.1.finitelyManySteps!))
     (fun (it : IterM (α := α) m β) acc recur => do
-      let ⟨step, hs⟩ ← MonadAttach.attach (m := n) it.step
-      match hs' : step.inflate with
+      match (← it.step).inflate with
       | .yield it' out h =>
-        let fx ← MonadAttach.attach (f out)
-        recur it' (acc.push fx.val) (by
-          apply Or.inl
-          have : step = .deflate (.yield it' out h) := by simp [← hs']
-          rw [this] at hs
-          exact ⟨out, h, hs, fx.val, fx.property, rfl⟩)
-      | .skip it' h => recur it' acc (by
-          apply Or.inr
-          have : step = .deflate (.skip it' h) := by simp [← hs']
-          rw [this] at hs
-          exact ⟨h, hs, rfl⟩)
-      | .done h => return acc) it acc
+        recur it' (acc.push (← f out)) (by exact TerminationMeasures.Finite.rel_of_yield ‹_›)
+      | .skip it' h => recur it' acc (by exact TerminationMeasures.Finite.rel_of_skip ‹_›)
+      | .done _ => return acc) it acc
+
+-- @[always_inline, no_expose]
+-- def IterM.DefaultConsumers.toArrayMapped {α β : Type w} {m : Type w → Type w'}
+--     {n : Type w → Type w''} [Monad n] [MonadAttach n] [Iterator α m β]
+--     (lift : ⦃α : Type w⦄ → m α → n α) {γ : Type w} (f : β → n γ)
+--     (it : IterM (α := α) m β) : n (Array γ) :=
+--   letI : MonadLift m n := ⟨lift (α := _)⟩
+--   go it #[]
+-- where
+--   @[always_inline]
+--   go it (acc : Array γ) : n (Array γ) :=
+--     letI : MonadLift m n := ⟨lift (α := _)⟩
+--     extrinsicFixE₂ (C₂ := fun _ _ => n (Array γ))
+--     (fun x' x => (∃ out, x.1.IsPlausibleStepE (.yield x'.1 out) ∧ ∃ fx, MonadAttach.CanReturn (f out) fx ∧ x'.2 = x.2.push fx) ∨ (∃ h, MonadAttach.CanReturn (m := n) x.1.step (.deflate <| .skip x'.1 h) ∧ x'.2 = x.2))
+--     (fun (it : IterM (α := α) m β) acc recur => do
+--       let ⟨step, hs⟩ ← MonadAttach.attach (m := n) it.step
+--       match hs' : step.inflate with
+--       | .yield it' out h =>
+--         let fx ← MonadAttach.attach (f out)
+--         recur it' (acc.push fx.val) (by
+--           apply Or.inl
+--           have : step = .deflate (.yield it' out h) := by simp [← hs']
+--           rw [this] at hs
+--           exact ⟨out, h, hs, fx.val, fx.property, rfl⟩)
+--       | .skip it' h => recur it' acc (by
+--           apply Or.inr
+--           have : step = .deflate (.skip it' h) := by simp [← hs']
+--           rw [this] at hs
+--           exact ⟨h, hs, rfl⟩)
+--       | .done h => return acc) it acc
 
 /--
 This is the default implementation of the `IteratorCollect` class.
@@ -105,7 +128,7 @@ used instead.
 -/
 @[always_inline]
 def IteratorCollect.defaultImplementation {α β : Type w} {m : Type w → Type w'}
-    {n : Type w → Type w''} [Monad n] [MonadAttach n] [Iterator α m β] :
+    {n : Type w → Type w''} [Monad n] [Iterator α m β] :
     IteratorCollect α m n where
   toArrayMapped := IterM.DefaultConsumers.toArrayMapped
 
@@ -115,21 +138,21 @@ Asserts that a given `IteratorCollect` instance is equal to `IteratorCollect.def
 (Even though equal, the given instance might be vastly more efficient.)
 -/
 class LawfulIteratorCollect (α : Type w) (m : Type w → Type w') (n : Type w → Type w'')
-    {β : Type w} [Monad m] [Monad n] [MonadAttach n] [Iterator α m β] [i : IteratorCollect α m n] where
+    {β : Type w} [Monad m] [Monad n] [Iterator α m β] [i : IteratorCollect α m n] where
   lawful_toArrayMapped : ∀ lift [LawfulMonadLiftFunction lift] [Finite α m],
     i.toArrayMapped lift (α := α) (γ := γ)
       = IteratorCollect.defaultImplementation.toArrayMapped lift
 
 theorem LawfulIteratorCollect.toArrayMapped_eq {α β γ : Type w} {m : Type w → Type w'}
-    {n : Type w → Type w''} [Monad m] [Monad n] [MonadAttach n] [Iterator α m β] [Finite α m] [IteratorCollect α m n]
+    {n : Type w → Type w''} [Monad m] [Monad n] [Iterator α m β] [Finite α m] [IteratorCollect α m n]
     [hl : LawfulIteratorCollect α m n] {lift : ⦃δ : Type w⦄ → m δ → n δ}
     [LawfulMonadLiftFunction lift]
     {f : β → n γ} {it : IterM (α := α) m β} :
     IteratorCollect.toArrayMapped lift f it (m := m) =
       IterM.DefaultConsumers.toArrayMapped lift f it (m := m) := by
   rw [lawful_toArrayMapped]; rfl
 
-instance (α β : Type w) (m : Type w → Type w') (n : Type w → Type w'') [Monad n] [MonadAttach n]
+instance (α β : Type w) (m : Type w → Type w') (n : Type w → Type w'') [Monad n]
     [Iterator α m β] [Monad m] [Iterator α m β] [Finite α m] :
     haveI : IteratorCollect α m n := .defaultImplementation
     LawfulIteratorCollect α m n :=
@@ -185,11 +208,12 @@ def IterM.toListRev {α : Type w} {m : Type w → Type w'} [Monad m] {β : Type
 where
   @[always_inline, inline]
   go (it : IterM m β) acc :=
-    extrinsicFix₂ (fun it acc recur => do
-      match (← it.step).inflate with
-      | .yield it' out _ => recur it' (out :: acc)
-      | .skip it' _ => recur it' acc
-      | .done _ => return acc) it acc
+    extrinsicFixE₂ (InvImage TerminationMeasures.Finite.Rel (·.1.finitelyManySteps!))
+      (fun it acc recur => do
+        match (← it.step).inflate with
+        | .yield it' out h => recur it' (out :: acc) (TerminationMeasures.Finite.rel_of_yield h)
+        | .skip it' h => recur it' acc (TerminationMeasures.Finite.rel_of_skip h)
+        | .done _ => return acc) it acc
 
 /--
 Traverses the given iterator and stores the emitted values in reverse order in a list. Because

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

@@ -71,8 +71,10 @@ provided by the standard library.
 class IteratorLoop (α : Type w) (m : Type w → Type w') {β : Type w} [Iterator α m β]
     (n : Type x → Type x') where
   forIn : ∀ (_liftBind : (γ : Type w) → (δ : Type x) → (γ → n δ) → m γ → n δ) (γ : Type x),
+      (plausible_forInStep : β → γ → ForInStep γ → Prop) →
       (it : IterM (α := α) m β) → γ →
-      ((b : β) → it.IsPlausibleIndirectOutput b → (c : γ) → n (ForInStep γ)) → n γ
+      ((b : β) → it.IsPlausibleIndirectOutput b → (c : γ) → n (Subtype (plausible_forInStep b c))) →
+      n γ
 
 end Typeclasses
 
@@ -99,18 +101,19 @@ def IterM.DefaultConsumers.forIn' {m : Type w → Type w'} {α : Type w} {β : T
     [Iterator α m β]
     {n : Type x → Type x'} [Monad n]
     (lift : ∀ γ δ, (γ → n δ) → m γ → n δ) (γ : Type x)
+    (plausible_forInStep : β → γ → ForInStep γ → Prop)
     (it : IterM (α := α) m β) (init : γ)
     (P : β → Prop) (hP : ∀ b, it.IsPlausibleIndirectOutput b → P b)
-    (f : (b : β) → P b → (c : γ) → n (ForInStep γ)) : n γ :=
+    (f : (b : β) → P b → (c : γ) → n (Subtype (plausible_forInStep b c))) : n γ :=
   haveI : Nonempty γ := ⟨init⟩
-  extrinsicFix₃ (C₃ := fun _ _ _ => n γ)
+  extrinsicFixE₃ (C₃ := fun _ _ _ => n γ) (InvImage (IteratorLoop.rel α m plausible_forInStep) (fun x => (x.1, x.2.1)))
     (fun it acc (hP : ∀ b, it.IsPlausibleIndirectOutput b → P b) recur => (lift _ _ · it.step) fun s => do
       match s.inflate with
       | .yield it' out h =>
         match ← f out (hP out <| .direct ⟨_, h⟩) acc with
-        | .yield c => recur it' c (fun _ h' => hP _ <| .indirect ⟨_, rfl, h⟩ h')
-        | .done c => return c
-      | .skip it' h => recur it' acc (fun _ h' => hP _ <| .indirect ⟨_, rfl, h⟩ h')
+        | ⟨.yield c, h'⟩ => recur it' c (fun _ h' => hP _ <| .indirect ⟨_, rfl, h⟩ h') (Or.inl ⟨out, ‹_›, ‹_›⟩)
+        | ⟨.done c, h⟩ => return c
+      | .skip it' h => recur it' acc (fun _ h' => hP _ <| .indirect ⟨_, rfl, h⟩ h') (Or.inr ⟨‹_›, rfl⟩)
       | .done _ => return acc) it init hP
 
 /--
@@ -153,7 +156,7 @@ implementations are possible and should be used instead.
 def IteratorLoop.defaultImplementation {α : Type w} {m : Type w → Type w'} {n : Type x → Type x'}
     [Monad n] [Iterator α m β] :
     IteratorLoop α m n where
-  forIn lift γ it init := IterM.DefaultConsumers.forIn' lift γ it init _ (fun _ => id)
+  forIn lift γ Pl it init := IterM.DefaultConsumers.forIn' lift γ Pl it init _ (fun _ => id)
 
 /--
 Asserts that a given `IteratorLoop` instance is equal to `IteratorLoop.defaultImplementation`.
@@ -164,8 +167,8 @@ class LawfulIteratorLoop (α : Type w) (m : Type w → Type w') (n : Type x →
   lawful lift [LawfulMonadLiftBindFunction lift] γ it init
       (Pl : β → γ → ForInStep γ → Prop) (wf : IteratorLoop.WellFounded α m Pl)
       (f : (b : β) → it.IsPlausibleIndirectOutput b → (c : γ) → n (Subtype (Pl b c))) :
-    i.forIn lift γ it init (Subtype.val <$> f · · ·) =
-      IteratorLoop.defaultImplementation.forIn lift γ it init (Subtype.val <$> f · · ·)
+    i.forIn lift γ Pl it init f =
+      IteratorLoop.defaultImplementation.forIn lift γ Pl it init f
 
 instance (α : Type w) (m : Type w → Type w') (n : Type x → Type x')
     [Monad m] [Monad n] [Iterator α m β] [Finite α m] :
@@ -196,7 +199,7 @@ def IteratorLoop.finiteForIn' {m : Type w → Type w'} {n : Type x → Type x'}
     (lift : ∀ γ δ, (γ → n δ) → m γ → n δ) :
     ForIn' n (IterM (α := α) m β) β ⟨fun it out => it.IsPlausibleIndirectOutput out⟩ where
   forIn' {γ} it init f :=
-    IteratorLoop.forIn (α := α) (m := m) lift γ it init (fun out h acc => (f out h acc))
+    IteratorLoop.forIn (α := α) (m := m) lift γ (fun _ _ _ => True) it init (return ⟨← f · · ·, trivial⟩)
 
 /--
 A `ForIn'` instance for iterators. Its generic membership relation is not easy to use,
@@ -221,8 +224,8 @@ instance {m : Type w → Type w'} {n : Type w → Type w''}
 def IterM.Partial.instForIn' {m : Type w → Type w'} {n : Type w → Type w''}
     {α : Type w} {β : Type w} [Iterator α m β] [IteratorLoop α m n] [MonadLiftT m n] [Monad n] :
     ForIn' n (IterM.Partial (α := α) m β) β ⟨fun it out => it.it.IsPlausibleIndirectOutput out⟩ where
-  forIn' it init f := IteratorLoop.forIn (α := α) (m := m) (n := n)
-      (fun _ _ f x => monadLift x >>= f) _ it.it init f
+  forIn' it init f :=
+    haveI := @IterM.instForIn'; forIn' it.it init f
 
 @[always_inline, inline]
 def IterM.Total.instForIn' {m : Type w → Type w'} {n : Type w → Type w''}

src/Init/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.lean

@@ -247,9 +247,8 @@ instance {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''}
     have : it = IterM.mapWithPostcondition _ it.internalState.inner := by rfl
     generalize it.internalState.inner = it at *
     cases this
-    simp only [LawfulIteratorCollect.toArrayMapped_eq]
     simp only [IteratorCollect.toArrayMapped]
-    rw [LawfulIteratorCollect.toArrayMapped_eq]
+    simp only [LawfulIteratorCollect.toArrayMapped_eq]
     induction it using IterM.inductSteps with | step it ih_yield ih_skip
     rw [IterM.DefaultConsumers.toArrayMapped_eq_match_step]
     rw [IterM.DefaultConsumers.toArrayMapped_eq_match_step]