fix forIn, for now only implemented for finite iterators

Author: datokrat

Iterator/Basic.lean

@@ -128,10 +128,8 @@ instance [Small.{w} α] [Small.{w} β] : Small.{w} (IterStep α β) where
       | .skip it => .skip it.inflate
       | .done => .done
     deflate_inflate {x} := by
-      dsimp only
       cases x <;> simp
     inflate_deflate {x} := by
-      dsimp only
       cases x <;> simp }⟩
 
 def IterStep.successor : IterStep α β → Option α

Iterator/Combinators/Drop.lean

@@ -144,6 +144,6 @@ instance Drop.instFinitenessRelation [Iterator α m β] [Monad m] [Finite α m]
 instance Drop.instIteratorToArray [Monad m] [Iterator α m β] [Finite α m] : IteratorToArray (Drop α m β) m :=
   .defaultImplementation
 
-instance Drop.instIteratorFor [Monad m] [Monad n] [MonadLiftT m n] [Iterator α m β] :
+instance Drop.instIteratorFor [Monad m] [Monad n] [MonadLiftT m n] [Iterator α m β] [Finite α m] :
     IteratorFor (Drop α m β) m n :=
   .defaultImplementation

Iterator/Combinators/FilterMap.lean

@@ -176,7 +176,8 @@ instance {f : β → HetT m (Option γ)} [Finite α m] :
     IteratorToArray (FilterMapMH α f) m :=
   .defaultImplementation
 
-instance FilterMapMH.instIteratorFor [Monad m] [Monad n] [MonadLiftT m n] [Iterator α m β] :
+instance FilterMapMH.instIteratorFor [Monad m] [Monad n] [MonadLiftT m n]
+    [Iterator α m β] [Finite α m] :
     IteratorFor (FilterMapMH α f) m n :=
   .defaultImplementation
 
@@ -191,7 +192,8 @@ instance {f : β → HetT m γ} [IteratorToArray α m] :
       (fun x => do g ((← (f x).computation).inflate (small := _)))
       it.inner.inner
 
-instance MapMH.instIteratorFor [Monad m] [Monad n] [MonadLiftT m n] [Iterator α m β] :
+instance MapMH.instIteratorFor [Monad m] [Monad n] [MonadLiftT m n]
+    [Iterator α m β] [Finite α m] :
     IteratorFor (MapMH α f) m n :=
   .defaultImplementation
 

Iterator/Combinators/FlatMap.lean

@@ -340,7 +340,8 @@ instance FlatMap.instIteratorToArray [Monad m] [Iterator α₂ m γ] [Finite α
     IteratorToArray (FlatMap α f) m :=
   .defaultImplementation
 
-instance FlatMap.instIteratorFor [Monad m] [Monad n] [MonadLiftT m n] [Iterator α₂ m γ] :
+instance FlatMap.instIteratorFor [Monad m] [Monad n] [MonadLiftT m n] [Iterator α₂ m γ]
+    [Finite α m] [Finite α₂ m] :
     IteratorFor (FlatMap α f) m n :=
   .defaultImplementation
 
@@ -452,7 +453,8 @@ instance SigmaIterator.instIteratorToArray [Monad m] [∀ b, Iterator (α b) m 
     IteratorToArray (SigmaIterator α m γ) m :=
   .defaultImplementation
 
-instance SigmaIterator.instIteratorFor [Monad m] [Monad n] [MonadLiftT m n] [∀ b, Iterator (α b) m γ] :
+instance SigmaIterator.instIteratorFor [Monad m] [Monad n] [MonadLiftT m n]
+    [∀ b, Iterator (α b) m γ] [∀ b, Finite (α b) m] :
     IteratorFor (SigmaIterator α m γ) m n :=
   .defaultImplementation
 

Iterator/Combinators/MonadLift.lean

@@ -35,10 +35,6 @@ instance MonadLiftIterator.instIterator {_ : Iterator α m β} {_ : MonadLiftT m
     | .skip it' h => pure <| .deflate <| .skip ⟨⟨it'⟩⟩ (.skip h)
     | .done h => pure <| .deflate <| .done (.done h)
 
-instance MonadLiftIterator.instIteratorFor [Monad n] [Monad n'] [MonadLiftT n n'] {_ : Iterator α m β} {_ : MonadLiftT m n} :
-    IteratorFor (MonadLiftIterator α m n) n n' :=
-  .defaultImplementation
-
 instance {_ : Iterator α m β} [Finite α m] {_ : MonadLiftT m n} : FinitenessRelation (MonadLiftIterator α m n) n where
   rel := InvImage IterM.TerminationMeasures.Finite.rel fun it => it.inner.inner.finitelyManySteps
   wf := by
@@ -56,6 +52,11 @@ instance {_ : Iterator α m β} [Finite α m] {_ : MonadLiftT m n} : FinitenessR
     case done h =>
       cases h
 
+instance MonadLiftIterator.instIteratorFor [Monad n] [Monad n'] [MonadLiftT n n']
+    [Iterator α m β] [Finite α m] {_ : MonadLiftT m n} :
+    IteratorFor (MonadLiftIterator α m n) n n' :=
+  .defaultImplementation
+
 variable (n) in
 @[always_inline, inline]
 def IterM.monadLift [Iterator α m β] {_ : MonadLiftT m n} (it : IterM (α := α) m β) :=

Iterator/Combinators/Take.lean

@@ -168,7 +168,7 @@ instance Take.instFinitenessRelation [Monad m] [Iterator α m β] [Productive α
 instance Take.instIteratorToArray [Monad m] [Iterator α m β] [Productive α m] : IteratorToArray (Take α m β) m :=
   .defaultImplementation
 
-instance Take.instIteratorFor [Monad m] [Monad n] [MonadLiftT m n] [Iterator α m β] :
+instance Take.instIteratorFor [Monad m] [Monad n] [MonadLiftT m n] [Iterator α m β] [Finite α m] :
     IteratorFor (Take α m β) m n :=
   .defaultImplementation
   -- TODO: use [IteratorFor α m n]

Iterator/Consumers/Loop.lean

@@ -1,10 +1,9 @@
 import Iterator.Basic
 
-set_option trace.Elab.Tactic.monotonicity true in
 @[specialize]
 def IterM.DefaultConsumers.forIn {m : Type w → Type w'} {n : Type w → Type w''} [Monad n] [MonadLiftT m n]
-    {α : Type w} {β : Type v} {γ : Type w} [Nonempty (n γ)]
-    [Iterator α m β]
+    {α : Type w} {β : Type v} {γ : Type w}
+    [Iterator α m β] [Finite α m]
     (it : IterM (α := α) m β) (init : γ) {successor_of : β → γ → γ → Prop}
     (f : (b : β) → (c : γ) → n (Subtype fun s : ForInStep γ => successor_of b c s.value)) : n γ := do
   match (← it.stepH).inflate with
@@ -14,24 +13,25 @@ def IterM.DefaultConsumers.forIn {m : Type w → Type w'} {n : Type w → Type w
     | ⟨.done c, _⟩ => return c
   | .skip it' _ => IterM.DefaultConsumers.forIn it' init f
   | .done _ => return init
-partial_fixpoint
+termination_by it.finitelyManySteps
 
 class IteratorFor (α : Type w) (m : Type w → Type w') {β : Type v} [Iterator α m β] (n : Type w → Type w'') where
   forIn : ∀ {γ : Type w}, IterM (α := α) m β → γ → {successor_of : β → γ → γ → Prop} →
       ((b : β) → (c : γ) → n (Subtype fun s : ForInStep γ => successor_of b c s.value)) →
-      (IterM.ForInWillTerminate α m successor_of) → n γ
+      n γ
 
 class LawfulIteratorFor (α : Type w) (m : Type w → Type w') (n : Type w → Type w'')
-    [Monad n] [Iterator α m β] [IteratorFor α m n] [MonadLiftT m n] where
+    [Monad n] [Iterator α m β] [Finite α m] [IteratorFor α m n] [MonadLiftT m n] where
   lawful : ∀ γ, IteratorFor.forIn (α := α) (m := m) (n := n) (γ := γ) =
     IterM.DefaultConsumers.forIn (α := α) (m := m) (n := n) (γ := γ)
 
 def IteratorFor.defaultImplementation {α : Type w} {m : Type w → Type w'} {n : Type w → Type w'}
-    [Monad m] [Monad n] [MonadLiftT m n] [Iterator α m β] : IteratorFor α m n where
+    [Monad m] [Monad n] [MonadLiftT m n] [Iterator α m β] [Finite α m] :
+    IteratorFor α m n where
   forIn := IterM.DefaultConsumers.forIn
 
 instance (α : Type w) (m : Type w → Type w') (n : Type w → Type w')
-    [Monad m] [Monad n] [MonadLiftT m n] [Iterator α m β] :
+    [Monad m] [Monad n] [MonadLiftT m n] [Iterator α m β] [Finite α m] :
     haveI : IteratorFor α m n := .defaultImplementation
     LawfulIteratorFor α m n :=
   letI : IteratorFor α m n := .defaultImplementation
@@ -40,21 +40,9 @@ instance (α : Type w) (m : Type w → Type w') (n : Type w → Type w')
 instance {m : Type w → Type w'} {n : Type w → Type w''}
     {α : Type w} {β : Type v} [Iterator α m β] [Finite α m] [IteratorFor α m n] :
     ForIn n (IterM (α := α) m β) β where
-  forIn it init stepper := by
-    apply IteratorFor.forIn it init (successor_of := fun _ _ _ => True) (fun b c => (⟨·, True.intro⟩) <$> stepper b c)
-    simp only [IterM.ForInWillTerminate]
-    refine Subrelation.wf (r := InvImage IterM.TerminationMeasures.Finite.rel (fun p => p.1.finitelyManySteps)) ?_ ?_
-    · intro p' p h
-      cases h
-      · apply IterM.TerminationMeasures.Finite.rel_of_skip
-        rename_i h
-        exact h.1
-      · rename_i h
-        obtain ⟨out, h, _⟩ := h -- Interesting: Moving `obtain` after `apply` leads to failure
-        apply IterM.TerminationMeasures.Finite.rel_of_yield
-        exact h
-    · apply InvImage.wf
-      exact WellFoundedRelation.wf
+  forIn it init stepper := IteratorFor.forIn it init
+      (successor_of := fun _ _ _ => True)
+      (fun b c => (⟨·, True.intro⟩) <$> stepper b c)
 
 @[specialize]
 def IterM.foldM {m : Type w → Type w'} {n : Type w → Type w'} [Monad n]

Iterator/Producers.lean

@@ -81,7 +81,4 @@ instance [Pure m] : ProductivenessRelation (UnfoldIterator α f) m where
   wf := emptyWf.wf
   subrelation {it it'} h := by cases h
 
-instance [Monad m] [Monad n] [MonadLiftT m n] : IteratorFor (UnfoldIterator α f) m n :=
-  .defaultImplementation
-
 end Unfold

Iterator/Pure/Consumers/Loop.lean

@@ -0,0 +1 @@
+import Iterator.Pure.Basic