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 β₂)
:
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.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_lift ← it₁.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_lift ← it₂.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_lift ← it₁.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 ⋯)