Documentation

Std.Data.Iterators.Lemmas.Combinators.Zip

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.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    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₂'
    Equations
    • =
    Instances For
      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₂
      Equations
      • =
      Instances For
        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_liftatIdxSlow? n it₁ let __do_lift_1atIdxSlow? n it₂ pure (__do_lift, __do_lift_1) | some memo => match n with | 0 => do let __do_liftatIdxSlow? n it₂ pure (memo.val, __do_lift) | n'.succ => do let __do_liftatIdxSlow? n' it₁ let __do_lift_1atIdxSlow? (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_liftatIdxSlow? n it₁ let __do_lift_1atIdxSlow? 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