noncomputable def Std.Iter.Intermediate.zip {α₁ α₂ β₁ β₂ : Type w} [Iterator α₁ Id β₁] (it₁ : Iter β₁) (memo : Option { out : β₁ // ∃ (it : Iter β₁), it.toIterM.IsPlausibleOutput out }) (it₂ : Iter β₂) :
Constructs intermediate states of an iterator created with the combinator Iter.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 Iter.zip.
Intermediate.zip is meant to be used only for verification purposes.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem Std.Iter.step_intermediateZip {α₁ α₂ β₁ β₂ : Type w} [Iterator α₁ Id β₁] [Iterator α₂ Id β₂] {it₁ : Iter β₁} {memo : Option { out : β₁ // ∃ (it : Iter β₁), it.toIterM.IsPlausibleOutput out }} {it₂ : Iter β₂} :
(Intermediate.zip it₁ memo it₂).step = match memo with
| none =>
match it₁.step with
| ⟨IterStep.yield it₁' out, hp⟩ => PlausibleIterStep.skip (Intermediate.zip it₁' (some ⟨out, ⋯⟩) it₂) ⋯
| ⟨IterStep.skip it₁', hp⟩ => PlausibleIterStep.skip (Intermediate.zip it₁' none it₂) ⋯
| ⟨IterStep.done, hp⟩ => PlausibleIterStep.done ⋯
| some out₁ =>
match it₂.step with
| ⟨IterStep.yield it₂' out₂, hp⟩ => PlausibleIterStep.yield (Intermediate.zip it₁ none it₂') (out₁.val, out₂) ⋯
| ⟨IterStep.skip it₂', hp⟩ => PlausibleIterStep.skip (Intermediate.zip it₁ (some out₁) it₂') ⋯
| ⟨IterStep.done, hp⟩ => PlausibleIterStep.done ⋯
theorem Std.Iter.toList_intermediateZip_of_finite {α₁ α₂ β₁ β₂ : Type w} [Iterator α₁ Id β₁] [Iterator α₂ Id β₂] {it₁ : Iter β₁} {memo : Option { out : β₁ // ∃ (it : Iter β₁), it.toIterM.IsPlausibleOutput out }} {it₂ : Iter β₂} [Iterators.Finite α₁ Id] [Iterators.Finite α₂ Id] :
(Intermediate.zip it₁ memo it₂).toList = ((Option.map Subtype.val memo).toList ++ it₁.toList).zip it₂.toList
theorem Std.Iter.atIdxSlow?_intermediateZip {α₁ α₂ β₁ β₂ : Type w} [Iterator α₁ Id β₁] [Iterator α₂ Id β₂] [Iterators.Productive α₁ Id] [Iterators.Productive α₂ Id] {it₁ : Iter β₁} {memo : Option { out : β₁ // ∃ (it : Iter β₁), it.toIterM.IsPlausibleOutput out }} {it₂ : Iter β₂} {n : Nat} :
atIdxSlow? n (Intermediate.zip it₁ memo it₂) = match memo with
| none => do
let __do_lift ← atIdxSlow? n it₁
let __do_lift_1 ← atIdxSlow? n it₂
pure (__do_lift, __do_lift_1)
| some memo =>
match n with
| 0 => do
let __do_lift ← atIdxSlow? n it₂
pure (memo.val, __do_lift)
| n'.succ => do
let __do_lift ← atIdxSlow? n' it₁
let __do_lift_1 ← atIdxSlow? (n' + 1) it₂
pure (__do_lift, __do_lift_1)
theorem Std.Iter.atIdxSlow?_zip {α₁ α₂ β₁ β₂ : Type u_1} [Iterator α₁ Id β₁] [Iterator α₂ Id β₂] [Iterators.Productive α₁ Id] [Iterators.Productive α₂ Id] {it₁ : Iter β₁} {it₂ : Iter β₂} {n : Nat} :
atIdxSlow? n (it₁.zip it₂) = do
let __do_lift ← atIdxSlow? n it₁
let __do_lift_1 ← atIdxSlow? n it₂
pure (__do_lift, __do_lift_1)
@[simp]