@[implicit_reducible]

noncomputable def Std.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

• Std.IterM.Intermediate.zip it₁ memo it₂ = { internalState := { left := it₁, memoizedLeft := memo, right := it₂ } }

theorem Std.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.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.inflate with | ⟨IterStep.yield it₁' out, hp⟩ => pure (Shrink.deflate (PlausibleIterStep.skip (Intermediate.zip it₁' (some ⟨out, ⋯⟩) it₂) ⋯)) | ⟨IterStep.skip it₁', hp⟩ => pure (Shrink.deflate (PlausibleIterStep.skip (Intermediate.zip it₁' none it₂) ⋯)) | ⟨IterStep.done, hp⟩ => pure (Shrink.deflate (PlausibleIterStep.done ⋯)) | some out₁ => do let __do_lift ← it₂.step match __do_lift.inflate with | ⟨IterStep.yield it₂' out₂, hp⟩ => pure (Shrink.deflate (PlausibleIterStep.yield (Intermediate.zip it₁ none it₂') (out₁.val, out₂) ⋯)) | ⟨IterStep.skip it₂', hp⟩ => pure (Shrink.deflate (PlausibleIterStep.skip (Intermediate.zip it₁ (some out₁) it₂') ⋯)) | ⟨IterStep.done, hp⟩ => pure (Shrink.deflate (PlausibleIterStep.done ⋯))

theorem Std.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.inflate with | ⟨IterStep.yield it₁' out, hp⟩ => pure (Shrink.deflate (PlausibleIterStep.skip (Intermediate.zip it₁' (some ⟨out, ⋯⟩) it₂) ⋯)) | ⟨IterStep.skip it₁', hp⟩ => pure (Shrink.deflate (PlausibleIterStep.skip (Intermediate.zip it₁' none it₂) ⋯)) | ⟨IterStep.done, hp⟩ => pure (Shrink.deflate (PlausibleIterStep.done ⋯))