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:

• Option.lt (fun n k : Nat => n < k) none none = False
• Option.lt (fun n k : Nat => n < k) none (some 3) = False
• Option.lt (fun n k : Nat => n < k) (some 3) none = True
• Option.lt (fun n k : Nat => n < k) (some 4) (some 5) = True
• Option.lt (fun n k : Nat => n < k) (some 4) (some 4) = False

theorem Std.Internal.Option.wellFounded_lt {α : Type u_1} {rel : α → α → Prop} (h : WellFounded rel) : WellFounded (Option.lt rel)

theorem Std.Internal.Option.SomeLtNone.wellFounded_lt {α : Type u_1} {r : α → α → Prop} (h : WellFounded r) : WellFounded (lt r)

@[unbox]

structure Std.Iterators.Zip (α₁ : Type w) (m : Type w → Type w') {β₁ : Type w} [Iterator α₁ m β₁] (α₂ β₂ : Type w) : Type w

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

• left : IterM m β₁
• memoizedLeft : Option { out : β₁ // ∃ (it : IterM m β₁), it.IsPlausibleOutput out }
• right : IterM m β₂

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.

• yieldLeft {m : Type w → Type w'} {α₁ β₁ : Type w} [Iterator α₁ m β₁] {α₂ β₂ : Type w} [Iterator α₂ m β₂] {it : IterM m (β₁ × β₂)} (hm : it.internalState.memoizedLeft = none) {it' : IterM m β₁} {out : β₁} (hp : it.internalState.left.IsPlausibleStep (IterStep.yield it' out)) : PlausibleStep it (IterStep.skip { internalState := { left := it', memoizedLeft := some ⟨out, ⋯⟩, right := it.internalState.right } })
• skipLeft {m : Type w → Type w'} {α₁ β₁ : Type w} [Iterator α₁ m β₁] {α₂ β₂ : Type w} [Iterator α₂ m β₂] {it : IterM m (β₁ × β₂)} (hm : it.internalState.memoizedLeft = none) {it' : IterM m β₁} (hp : it.internalState.left.IsPlausibleStep (IterStep.skip it')) : PlausibleStep it (IterStep.skip { internalState := { left := it', memoizedLeft := none, right := it.internalState.right } })
• doneLeft {m : Type w → Type w'} {α₁ β₁ : Type w} [Iterator α₁ m β₁] {α₂ β₂ : Type w} [Iterator α₂ m β₂] {it : IterM m (β₁ × β₂)} (hm : it.internalState.memoizedLeft = none) (hp : it.internalState.left.IsPlausibleStep IterStep.done) : PlausibleStep it IterStep.done
• yieldRight {m : Type w → Type w'} {α₁ β₁ : Type w} [Iterator α₁ m β₁] {α₂ β₂ : Type w} [Iterator α₂ m β₂] {it : IterM m (β₁ × β₂)} {out₁ : { out : β₁ // ∃ (it : IterM m β₁), it.IsPlausibleOutput out }} (hm : it.internalState.memoizedLeft = some out₁) {it₂' : IterM m β₂} {out₂ : β₂} (hp : it.internalState.right.IsPlausibleStep (IterStep.yield it₂' out₂)) : PlausibleStep it (IterStep.yield { internalState := { left := it.internalState.left, memoizedLeft := none, right := it₂' } } (out₁.val, out₂))
• skipRight {m : Type w → Type w'} {α₁ β₁ : Type w} [Iterator α₁ m β₁] {α₂ β₂ : Type w} [Iterator α₂ m β₂] {it : IterM m (β₁ × β₂)} {out₁ : { out : β₁ // ∃ (it : IterM m β₁), it.IsPlausibleOutput out }} (hm : it.internalState.memoizedLeft = some out₁) {it₂' : IterM m β₂} (hp : it.internalState.right.IsPlausibleStep (IterStep.skip it₂')) : PlausibleStep it (IterStep.skip { internalState := { left := it.internalState.left, memoizedLeft := some out₁, right := it₂' } })
• doneRight {m : Type w → Type w'} {α₁ β₁ : Type w} [Iterator α₁ m β₁] {α₂ β₂ : Type w} [Iterator α₂ m β₂] {it : IterM m (β₁ × β₂)} {out₁ : { out : β₁ // ∃ (it : IterM m β₁), it.IsPlausibleOutput out }} (hm : it.internalState.memoizedLeft = some out₁) (hp : it.internalState.right.IsPlausibleStep IterStep.done) : PlausibleStep it IterStep.done

instance Std.Iterators.Zip.instIterator {m : Type w → Type w'} {α₁ β₁ : Type w} [Iterator α₁ m β₁] {α₂ β₂ : Type w} [Iterator α₂ m β₂] [Monad m] : Iterator (Zip α₁ m α₂ β₂) m (β₁ × β₂)

@[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.

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

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

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

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

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

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

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

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

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

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