noncomputable def Std.Iterators.Iter.Intermediate.zip {α₁ α₂ β₁ β₂ : Type w} [Iterator α₁ Id β₁] (it₁ : Iter β₁) (memo : Option { out : β₁ // ∃ (it : Iter β₁), it.toIterM.IsPlausibleOutput out }) (it₂ : Iter β₂) : 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.

def Std.Iterators.Iter.Intermediate.zip_inj {α₁ α₂ β₁ β₂ : Type w} [Iterator α₁ Id β₁] {it₁ it₁' : Iter β₁} {memo memo' : Option { out : β₁ // ∃ (it : Iter β₁), it.toIterM.IsPlausibleOutput out }} {it₂ it₂' : Iter β₂} : zip it₁ memo it₂ = zip it₁' memo' it₂' ↔ it₁ = it₁' ∧ memo = memo' ∧ it₂ = it₂'

def Std.Iterators.Iter.Intermediate.zip_surj {α₁ α₂ β₁ β₂ : Type w} [Iterator α₁ Id β₁] (it : Iter (β₁ × β₂)) : ∃ (it₁ : Iter β₁), ∃ (memo : Option { out : β₁ // ∃ (it : Iter β₁), it.toIterM.IsPlausibleOutput out }), ∃ (it₂ : Iter β₂), it = zip it₁ memo it₂

theorem Std.Iterators.Iter.zip_eq_intermediateZip {α₁ α₂ β₁ β₂ : Type w} [Iterator α₁ Id β₁] [Iterator α₂ Id β₂] (it₁ : Iter β₁) (it₂ : Iter β₂) : it₁.zip it₂ = Intermediate.zip it₁ none it₂

theorem Std.Iterators.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.Iterators.Iter.toList_intermediateZip_of_finite {α₁ α₂ β₁ β₂ : Type w} [Iterator α₁ Id β₁] [Iterator α₂ Id β₂] {it₁ : Iter β₁} {memo : Option { out : β₁ // ∃ (it : Iter β₁), it.toIterM.IsPlausibleOutput out }} {it₂ : Iter β₂} [Finite α₁ Id] [Finite α₂ Id] [IteratorCollect α₁ Id Id] [LawfulIteratorCollect α₁ Id Id] [IteratorCollect α₂ Id Id] [LawfulIteratorCollect α₂ Id Id] [IteratorCollect (Zip α₁ Id α₂ β₂) Id Id] [LawfulIteratorCollect (Zip α₁ Id α₂ β₂) Id Id] : (Intermediate.zip it₁ memo it₂).toList = ((Option.map Subtype.val memo).toList ++ it₁.toList).zip it₂.toList

theorem Std.Iterators.Iter.atIdxSlow?_intermediateZip {α₁ α₂ β₁ β₂ : Type w} [Iterator α₁ Id β₁] [Iterator α₂ Id β₂] [Productive α₁ Id] [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.Iterators.Iter.atIdxSlow?_zip {α₁ α₂ β₁ β₂ : Type u_1} [Iterator α₁ Id β₁] [Iterator α₂ Id β₂] [Productive α₁ Id] [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]

theorem Std.Iterators.Iter.toList_zip_of_finite {α₁ α₂ β₁ β₂ : Type u_1} [Iterator α₁ Id β₁] [Iterator α₂ Id β₂] {it₁ : Iter β₁} {it₂ : Iter β₂} [Finite α₁ Id] [Finite α₂ Id] [IteratorCollect α₁ Id Id] [LawfulIteratorCollect α₁ Id Id] [IteratorCollect α₂ Id Id] [LawfulIteratorCollect α₂ Id Id] [IteratorCollect (Zip α₁ Id α₂ β₂) Id Id] [LawfulIteratorCollect (Zip α₁ Id α₂ β₂) Id Id] : (it₁.zip it₂).toList = it₁.toList.zip it₂.toList

theorem Std.Iterators.Iter.toList_zip_of_finite_left {α₁ α₂ β₁ β₂ : Type u_1} [Iterator α₁ Id β₁] [Iterator α₂ Id β₂] {it₁ : Iter β₁} {it₂ : Iter β₂} [Finite α₁ Id] [Productive α₂ Id] [IteratorCollect α₁ Id Id] [LawfulIteratorCollect α₁ Id Id] [IteratorCollect (Zip α₁ Id α₂ β₂) Id Id] [LawfulIteratorCollect (Zip α₁ Id α₂ β₂) Id Id] : (it₁.zip it₂).toList = it₁.toList.zip (take it₁.toList.length it₂).toList

theorem Std.Iterators.Iter.toList_zip_of_finite_right {α₁ α₂ β₁ β₂ : Type u_1} [Iterator α₁ Id β₁] [Iterator α₂ Id β₂] {it₁ : Iter β₁} {it₂ : Iter β₂} [Productive α₁ Id] [Finite α₂ Id] [IteratorCollect α₂ Id Id] [LawfulIteratorCollect α₂ Id Id] [IteratorCollect (Zip α₁ Id α₂ β₂) Id Id] [LawfulIteratorCollect (Zip α₁ Id α₂ β₂) Id Id] : (it₁.zip it₂).toList = (take it₂.toList.length it₁).toList.zip it₂.toList

@[simp]

theorem Std.Iterators.Iter.toListRev_zip_of_finite {α₁ α₂ β₁ β₂ : Type u_1} [Iterator α₁ Id β₁] [Iterator α₂ Id β₂] {it₁ : Iter β₁} {it₂ : Iter β₂} [Finite α₁ Id] [Finite α₂ Id] [IteratorCollect α₁ Id Id] [LawfulIteratorCollect α₁ Id Id] [IteratorCollect α₂ Id Id] [LawfulIteratorCollect α₂ Id Id] [IteratorCollect (Zip α₁ Id α₂ β₂) Id Id] [LawfulIteratorCollect (Zip α₁ Id α₂ β₂) Id Id] : (it₁.zip it₂).toListRev = (it₁.toList.zip it₂.toList).reverse

theorem Std.Iterators.Iter.toListRev_zip_of_finite_left {α₁ α₂ β₁ β₂ : Type u_1} [Iterator α₁ Id β₁] [Iterator α₂ Id β₂] {it₁ : Iter β₁} {it₂ : Iter β₂} [Finite α₁ Id] [Productive α₂ Id] [IteratorCollect α₁ Id Id] [LawfulIteratorCollect α₁ Id Id] [IteratorCollect (Zip α₁ Id α₂ β₂) Id Id] [LawfulIteratorCollect (Zip α₁ Id α₂ β₂) Id Id] : (it₁.zip it₂).toListRev = (it₁.toList.zip (take it₁.toList.length it₂).toList).reverse

theorem Std.Iterators.Iter.toListRev_zip_of_finite_right {α₁ α₂ β₁ β₂ : Type u_1} [Iterator α₁ Id β₁] [Iterator α₂ Id β₂] {it₁ : Iter β₁} {it₂ : Iter β₂} [Productive α₁ Id] [Finite α₂ Id] [IteratorCollect α₂ Id Id] [LawfulIteratorCollect α₂ Id Id] [IteratorCollect (Zip α₁ Id α₂ β₂) Id Id] [LawfulIteratorCollect (Zip α₁ Id α₂ β₂) Id Id] : (it₁.zip it₂).toListRev = ((take it₂.toList.length it₁).toList.zip it₂.toList).reverse

@[simp]

theorem Std.Iterators.Iter.toArray_zip_of_finite {α₁ α₂ β₁ β₂ : Type u_1} [Iterator α₁ Id β₁] [Iterator α₂ Id β₂] {it₁ : Iter β₁} {it₂ : Iter β₂} [Finite α₁ Id] [Finite α₂ Id] [IteratorCollect α₁ Id Id] [LawfulIteratorCollect α₁ Id Id] [IteratorCollect α₂ Id Id] [LawfulIteratorCollect α₂ Id Id] [IteratorCollect (Zip α₁ Id α₂ β₂) Id Id] [LawfulIteratorCollect (Zip α₁ Id α₂ β₂) Id Id] : (it₁.zip it₂).toArray = it₁.toArray.zip it₂.toArray

theorem Std.Iterators.Iter.toArray_zip_of_finite_left {α₁ α₂ β₁ β₂ : Type u_1} [Iterator α₁ Id β₁] [Iterator α₂ Id β₂] {it₁ : Iter β₁} {it₂ : Iter β₂} [Finite α₁ Id] [Productive α₂ Id] [IteratorCollect α₁ Id Id] [LawfulIteratorCollect α₁ Id Id] [IteratorCollect (Zip α₁ Id α₂ β₂) Id Id] [LawfulIteratorCollect (Zip α₁ Id α₂ β₂) Id Id] : (it₁.zip it₂).toArray = it₁.toArray.zip (take it₁.toArray.size it₂).toArray

theorem Std.Iterators.Iter.toArray_zip_of_finite_right {α₁ α₂ β₁ β₂ : Type u_1} [Iterator α₁ Id β₁] [Iterator α₂ Id β₂] {it₁ : Iter β₁} {it₂ : Iter β₂} [Productive α₁ Id] [Finite α₂ Id] [IteratorCollect α₂ Id Id] [LawfulIteratorCollect α₂ Id Id] [IteratorCollect (Zip α₁ Id α₂ β₂) Id Id] [LawfulIteratorCollect (Zip α₁ Id α₂ β₂) Id Id] : (it₁.zip it₂).toArray = (take it₂.toArray.size it₁).toArray.zip it₂.toArray

@[simp]

theorem Std.Iterators.Iter.toList_take_zip {α₁ α₂ β₁ β₂ : Type u_1} [Iterator α₁ Id β₁] [Iterator α₂ Id β₂] [Productive α₁ Id] [Productive α₂ Id] {it₁ : Iter β₁} {it₂ : Iter β₂} {n : Nat} : (take n (it₁.zip it₂)).toList = (take n it₁).toList.zip (take n it₂).toList

@[simp]

theorem Std.Iterators.Iter.toListRev_take_zip {α₁ α₂ β₁ β₂ : Type u_1} [Iterator α₁ Id β₁] [Iterator α₂ Id β₂] [Productive α₁ Id] [Productive α₂ Id] {it₁ : Iter β₁} {it₂ : Iter β₂} {n : Nat} : (take n (it₁.zip it₂)).toListRev = ((take n it₁).toList.zip (take n it₂).toList).reverse

@[simp]

theorem Std.Iterators.Iter.toArray_take_zip {α₁ α₂ β₁ β₂ : Type u_1} [Iterator α₁ Id β₁] [Iterator α₂ Id β₂] [Productive α₁ Id] [Productive α₂ Id] {it₁ : Iter β₁} {it₂ : Iter β₂} {n : Nat} : (take n (it₁.zip it₂)).toArray = ((take n it₁).toList.zip (take n it₂).toList).toArray