Documentation

Std.Data.Iterators.Lemmas.Combinators.Monadic.Zip

noncomputable def Std.Iterators.IterM.Intermediate.zip {α₁ α₂ β₁ β₂ : Type w} {m : Type w → Type w'} [Iterator α₁ m β₁] (it₁ : IterM m β₁) (memo : Option { out : β₁ // (it : IterM m β₁), it.IsPlausibleOutput out }) (it₂ : IterM m β₂) :
IterM m (β₁ × β₂)

Constructs intermediate states of an iterator created with the combinator IterM.zip. When left.zip right has already obtained a value from left but not yet from right, it remembers left's value in a field of its internal state. This intermediate state cannot be created directly with IterM.zip.

Intermediate.zip is meant to be used only for verification purposes.

Equations
Instances For
    theorem Std.Iterators.IterM.zip_eq_intermediateZip {α₁ α₂ β₁ β₂ : Type w} {m : Type w → Type w'} [Iterator α₁ m β₁] (it₁ : IterM m β₁) (it₂ : IterM m β₂) :
    it₁.zip it₂ = Intermediate.zip it₁ none it₂
    theorem Std.Iterators.IterM.step_intermediateZip {α₁ α₂ β₁ β₂ : Type w} {m : Type w → Type w'} [Monad m] [Iterator α₁ m β₁] [Iterator α₂ m β₂] {it₁ : IterM m β₁} {memo : Option { out : β₁ // (it : IterM m β₁), it.IsPlausibleOutput out }} {it₂ : IterM m β₂} :
    (Intermediate.zip it₁ memo it₂).step = match memo with | none => do let __do_liftit₁.step match __do_lift with | IterStep.yield it₁' out, hp => pure (PlausibleIterStep.skip (Intermediate.zip it₁' (some out, ) it₂) ) | IterStep.skip it₁', hp => pure (PlausibleIterStep.skip (Intermediate.zip it₁' none it₂) ) | IterStep.done, hp => pure (PlausibleIterStep.done ) | some out₁ => do let __do_liftit₂.step match __do_lift with | IterStep.yield it₂' out₂, hp => pure (PlausibleIterStep.yield (Intermediate.zip it₁ none it₂') (out₁.val, out₂) ) | IterStep.skip it₂', hp => pure (PlausibleIterStep.skip (Intermediate.zip it₁ (some out₁) it₂') ) | IterStep.done, hp => pure (PlausibleIterStep.done )
    theorem Std.Iterators.IterM.step_zip {α₁ α₂ β₁ β₂ : Type w} {m : Type w → Type w'} [Monad m] [Iterator α₁ m β₁] [Iterator α₂ m β₂] {it₁ : IterM m β₁} {it₂ : IterM m β₂} :
    (it₁.zip it₂).step = do let __do_liftit₁.step match __do_lift with | IterStep.yield it₁' out, hp => pure (PlausibleIterStep.skip (Intermediate.zip it₁' (some out, ) it₂) ) | IterStep.skip it₁', hp => pure (PlausibleIterStep.skip (Intermediate.zip it₁' none it₂) ) | IterStep.done, hp => pure (PlausibleIterStep.done )