Documentation

Std.Data.Iterators.Combinators.Monadic.Zip

Monadic zip combinator #

This file provides an iterator combinator IterM.zip that combines two iterators into an iterator of pairs.

def Std.Internal.Option.SomeLtNone.lt {α : Type u_1} (r : ααProp) :
Option αOption αProp

Lifts an ordering relation to Option, such that none is the greatest element.

It can be understood as adding a distinguished greatest element, represented by none, to both α and β.

Caution: Given LT α, Option.SomeLtNone.lt LT.lt differs from the LT (Option α) instance, which is implemented by Option.lt Lt.lt.

Examples:

Equations
Instances For
    theorem Std.Internal.Option.wellFounded_lt {α : Type u_1} {rel : ααProp} (h : WellFounded rel) :
    theorem Std.Internal.Option.SomeLtNone.wellFounded_lt {α : Type u_1} {r : ααProp} (h : WellFounded r) :
    @[unbox]
    structure Std.Iterators.Zip (α₁ : Type w) (m : Type w → Type w') {β₁ : Type w} [Iterator α₁ m β₁] (α₂ β₂ : Type w) :

    Internal state of the zip combinator. Do not depend on its internals.

    Instances For
      inductive Std.Iterators.Zip.PlausibleStep {m : Type w → Type w'} {α₁ β₁ : Type w} [Iterator α₁ m β₁] {α₂ β₂ : Type w} [Iterator α₂ m β₂] (it : IterM m (β₁ × β₂)) :
      IterStep (IterM m (β₁ × β₂)) (β₁ × β₂)Prop

      it.PlausibleStep step is the proposition that step is a possible next step from the zip iterator it. This is mostly internally relevant, except if one needs to manually prove termination (Finite or Productive instances, for example) of a zip iterator.

      Instances For
        instance Std.Iterators.Zip.instIterator {m : Type w → Type w'} {α₁ β₁ : Type w} [Iterator α₁ m β₁] {α₂ β₂ : Type w} [Iterator α₂ m β₂] [Monad m] :
        Iterator (Zip α₁ m α₂ β₂) m (β₁ × β₂)
        Equations
        • One or more equations did not get rendered due to their size.
        @[inline]
        def Std.Iterators.IterM.zip {m : Type w → Type w'} {α₁ β₁ : Type w} [Iterator α₁ m β₁] {α₂ β₂ : Type w} (left : IterM m β₁) (right : IterM m β₂) :
        IterM m (β₁ × β₂)

        Given two iterators left and right, left.zip right is an iterator that yields pairs of outputs of left and right. When one of them terminates, the zip iterator will also terminate.

        Marble diagram:

        left               --a        ---b        --c
        right                 --x         --y        --⊥
        left.zip right     -----(a, x)------(b, y)-----⊥
        

        Termination properties:

        • Finite instance: only if either left or right is finite and the other is productive
        • Productive instance: only if left and right are productive

        There are situations where left.zip right is finite (or productive) but none of the instances above applies. For example, if the computation happens in an Except monad and left immediately fails when calling step, then left.zip right will also do so. In such a case, the Finite (or Productive) instance needs to be proved manually.

        Performance:

        This combinator incurs an additional O(1) cost with each step taken by left or right.

        Right now, the compiler does not unbox the internal state, leading to worse performance than possible.

        Equations
        Instances For
          def Std.Iterators.Zip.Rel₁ (m : Type w → Type w') {α₁ β₁ : Type w} [Iterator α₁ m β₁] {α₂ β₂ : Type w} [Iterator α₂ m β₂] [Finite α₁ m] [Productive α₂ m] :
          IterM m (β₁ × β₂)IterM m (β₁ × β₂)Prop
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            theorem Std.Iterators.Zip.rel₁_of_left {m : Type w → Type w'} {α₁ β₁ : Type w} [Iterator α₁ m β₁] {α₂ β₂ : Type w} [Iterator α₂ m β₂] [Finite α₁ m] [Productive α₂ m] {it' it : IterM m (β₁ × β₂)} (h : it'.internalState.left.finitelyManySteps.Rel it.internalState.left.finitelyManySteps) :
            Rel₁ m it' it
            theorem Std.Iterators.Zip.rel₁_of_memoizedLeft {m : Type w → Type w'} {α₁ β₁ : Type w} [Iterator α₁ m β₁] {α₂ β₂ : Type w} [Iterator α₂ m β₂] [Finite α₁ m] [Productive α₂ m] {left : IterM m β₁} {b' b : Option { out : β₁ // (it : IterM m β₁), it.IsPlausibleOutput out }} {right' right : IterM m β₂} (h : Option.lt emptyRelation b' b) :
            Rel₁ m { internalState := { left := left, memoizedLeft := b', right := right' } } { internalState := { left := left, memoizedLeft := b, right := right } }
            theorem Std.Iterators.Zip.rel₁_of_right {m : Type w → Type w'} {α₁ β₁ : Type w} [Iterator α₁ m β₁] {α₂ β₂ : Type w} [Iterator α₂ m β₂] [Finite α₁ m] [Productive α₂ m] {left : IterM m β₁} {b b' : Option { out : β₁ // (it : IterM m β₁), it.IsPlausibleOutput out }} {it' it : IterM m β₂} (h : b' = b) (h' : it'.finitelyManySkips.Rel it.finitelyManySkips) :
            Rel₁ m { internalState := { left := left, memoizedLeft := b', right := it' } } { internalState := { left := left, memoizedLeft := b, right := it } }
            def Std.Iterators.Zip.instFinitenessRelation₁ {m : Type w → Type w'} {α₁ β₁ : Type w} [Iterator α₁ m β₁] {α₂ β₂ : Type w} [Iterator α₂ m β₂] [Monad m] [Finite α₁ m] [Productive α₂ m] :
            FinitenessRelation (Zip α₁ m α₂ β₂) m
            Equations
            Instances For
              instance Std.Iterators.Zip.instFinite₁ {m : Type w → Type w'} {α₁ β₁ : Type w} [Iterator α₁ m β₁] {α₂ β₂ : Type w} [Iterator α₂ m β₂] [Monad m] [Finite α₁ m] [Productive α₂ m] :
              Finite (Zip α₁ m α₂ β₂) m
              def Std.Iterators.Zip.Rel₂ (m : Type w → Type w') {α₁ β₁ : Type w} [Iterator α₁ m β₁] {α₂ β₂ : Type w} [Iterator α₂ m β₂] [Productive α₁ m] [Finite α₂ m] :
              IterM m (β₁ × β₂)IterM m (β₁ × β₂)Prop
              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                theorem Std.Iterators.Zip.rel₂_of_right {m : Type w → Type w'} {α₁ β₁ : Type w} [Iterator α₁ m β₁] {α₂ β₂ : Type w} [Iterator α₂ m β₂] [Productive α₁ m] [Finite α₂ m] {it' it : IterM m (β₁ × β₂)} (h : it'.internalState.right.finitelyManySteps.Rel it.internalState.right.finitelyManySteps) :
                Rel₂ m it' it
                theorem Std.Iterators.Zip.rel₂_of_memoizedLeft {m : Type w → Type w'} {α₁ β₁ : Type w} [Iterator α₁ m β₁] {α₂ β₂ : Type w} [Iterator α₂ m β₂] [Productive α₁ m] [Finite α₂ m] {right : IterM m β₂} {b' b : Option { out : β₁ // (it : IterM m β₁), it.IsPlausibleOutput out }} {left' left : IterM m β₁} (h : Internal.Option.SomeLtNone.lt emptyRelation b' b) :
                Rel₂ m { internalState := { left := left, memoizedLeft := b', right := right } } { internalState := { left := left', memoizedLeft := b, right := right } }
                theorem Std.Iterators.Zip.rel₂_of_left {m : Type w → Type w'} {α₁ β₁ : Type w} [Iterator α₁ m β₁] {α₂ β₂ : Type w} [Iterator α₂ m β₂] [Productive α₁ m] [Finite α₂ m] {right : IterM m β₂} {b b' : Option { out : β₁ // (it : IterM m β₁), it.IsPlausibleOutput out }} {it' it : IterM m β₁} (h : b' = b) (h' : it'.finitelyManySkips.Rel it.finitelyManySkips) :
                Rel₂ m { internalState := { left := it', memoizedLeft := b', right := right } } { internalState := { left := it, memoizedLeft := b, right := right } }
                def Std.Iterators.Zip.instFinitenessRelation₂ {m : Type w → Type w'} {α₁ β₁ : Type w} [Iterator α₁ m β₁] {α₂ β₂ : Type w} [Iterator α₂ m β₂] [Monad m] [Productive α₁ m] [Finite α₂ m] :
                FinitenessRelation (Zip α₁ m α₂ β₂) m
                Equations
                Instances For
                  instance Std.Iterators.Zip.instFinite₂ {m : Type w → Type w'} {α₁ β₁ : Type w} [Iterator α₁ m β₁] {α₂ β₂ : Type w} [Iterator α₂ m β₂] [Monad m] [Productive α₁ m] [Finite α₂ m] :
                  Finite (Zip α₁ m α₂ β₂) m
                  def Std.Iterators.Zip.Rel₃ (m : Type w → Type w') {α₁ β₁ : Type w} [Iterator α₁ m β₁] {α₂ β₂ : Type w} [Iterator α₂ m β₂] [Productive α₁ m] [Productive α₂ m] :
                  IterM m (β₁ × β₂)IterM m (β₁ × β₂)Prop
                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    theorem Std.Iterators.Zip.rel₃_of_memoizedLeft {m : Type w → Type w'} {α₁ β₁ : Type w} [Iterator α₁ m β₁] {α₂ β₂ : Type w} [Iterator α₂ m β₂] [Productive α₁ m] [Productive α₂ m] {it' it : IterM m (β₁ × β₂)} (h : Internal.Option.SomeLtNone.lt emptyRelation it'.internalState.memoizedLeft it.internalState.memoizedLeft) :
                    Rel₃ m it' it
                    theorem Std.Iterators.Zip.rel₃_of_left {m : Type w → Type w'} {α₁ β₁ : Type w} [Iterator α₁ m β₁] {α₂ β₂ : Type w} [Iterator α₂ m β₂] [Productive α₁ m] [Productive α₂ m] {left' left : IterM m β₁} {b : Option { out : β₁ // (it : IterM m β₁), it.IsPlausibleOutput out }} {right' right : IterM m β₂} (h : left'.finitelyManySkips.Rel left.finitelyManySkips) :
                    Rel₃ m { internalState := { left := left', memoizedLeft := b, right := right' } } { internalState := { left := left, memoizedLeft := b, right := right } }
                    theorem Std.Iterators.Zip.rel₃_of_right {m : Type w → Type w'} {α₁ β₁ : Type w} [Iterator α₁ m β₁] {α₂ β₂ : Type w} [Iterator α₂ m β₂] [Productive α₁ m] [Productive α₂ m] {left : IterM m β₁} {b b' : Option { out : β₁ // (it : IterM m β₁), it.IsPlausibleOutput out }} {it' it : IterM m β₂} (h : b' = b) (h' : it'.finitelyManySkips.Rel it.finitelyManySkips) :
                    Rel₃ m { internalState := { left := left, memoizedLeft := b', right := it' } } { internalState := { left := left, memoizedLeft := b, right := it } }
                    def Std.Iterators.Zip.instProductivenessRelation {m : Type w → Type w'} {α₁ β₁ : Type w} [Iterator α₁ m β₁] {α₂ β₂ : Type w} [Iterator α₂ m β₂] [Monad m] [Productive α₁ m] [Productive α₂ m] :
                    ProductivenessRelation (Zip α₁ m α₂ β₂) m
                    Equations
                    Instances For
                      instance Std.Iterators.Zip.instProductive {m : Type w → Type w'} {α₁ β₁ : Type w} [Iterator α₁ m β₁] {α₂ β₂ : Type w} [Iterator α₂ m β₂] [Monad m] [Productive α₁ m] [Productive α₂ m] :
                      Productive (Zip α₁ m α₂ β₂) m
                      instance Std.Iterators.Zip.instIteratorCollect {m : Type w → Type w'} {α₁ β₁ : Type w} [Iterator α₁ m β₁] {α₂ β₂ : Type w} [Iterator α₂ m β₂] {n : Type w → Type u_1} [Monad m] [Monad n] :
                      IteratorCollect (Zip α₁ m α₂ β₂) m n
                      Equations
                      instance Std.Iterators.Zip.instIteratorCollectPartial {m : Type w → Type w'} {α₁ β₁ : Type w} [Iterator α₁ m β₁] {α₂ β₂ : Type w} [Iterator α₂ m β₂] {n : Type w → Type u_1} [Monad m] [Monad n] :
                      IteratorCollectPartial (Zip α₁ m α₂ β₂) m n
                      Equations
                      instance Std.Iterators.Zip.instIteratorLoop {m : Type w → Type w'} {α₁ β₁ : Type w} [Iterator α₁ m β₁] {α₂ β₂ : Type w} [Iterator α₂ m β₂] {n : Type w → Type u_1} [Monad m] [Monad n] :
                      IteratorLoop (Zip α₁ m α₂ β₂) m n
                      Equations
                      instance Std.Iterators.Zip.instIteratorLoopPartial {m : Type w → Type w'} {α₁ β₁ : Type w} [Iterator α₁ m β₁] {α₂ β₂ : Type w} [Iterator α₂ m β₂] {n : Type w → Type u_1} [Monad m] [Monad n] :
                      IteratorLoopPartial (Zip α₁ m α₂ β₂) m n
                      Equations