Theorem: Etch.Verification.Stream.zip_spec (Etch/StreamFusion/Proofs/StreamZip.lean)

State before:
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
q : (zip a b).σ
i : ι
⊢ evalOption (zip a b) q i = Option.map₂ Prod.mk (evalOption a q.1 i) (evalOption b q.2 i)
Tactic:
apply (a.zip b).wf.induction q
State after:
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
q : (zip a b).σ
i : ι
⊢ ∀ (x : (zip a b).σ),
    (∀ (y : (zip a b).σ),
        WfRel (zip a b) y x →
          evalOption (zip a b) y i = Option.map₂ Prod.mk (evalOption a y.1 i) (evalOption b y.2 i)) →
      evalOption (zip a b) x i = Option.map₂ Prod.mk (evalOption a x.1 i) (evalOption b x.2 i)

State before:
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
q : (zip a b).σ
i : ι
⊢ ∀ (x : (zip a b).σ),
    (∀ (y : (zip a b).σ),
        WfRel (zip a b) y x →
          evalOption (zip a b) y i = Option.map₂ Prod.mk (evalOption a y.1 i) (evalOption b y.2 i)) →
      evalOption (zip a b) x i = Option.map₂ Prod.mk (evalOption a x.1 i) (evalOption b x.2 i)
Tactic:
clear q
State after:
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
i : ι
⊢ ∀ (x : (zip a b).σ),
    (∀ (y : (zip a b).σ),
        WfRel (zip a b) y x →
          evalOption (zip a b) y i = Option.map₂ Prod.mk (evalOption a y.1 i) (evalOption b y.2 i)) →
      evalOption (zip a b) x i = Option.map₂ Prod.mk (evalOption a x.1 i) (evalOption b x.2 i)

State before:
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
i : ι
⊢ ∀ (x : (zip a b).σ),
    (∀ (y : (zip a b).σ),
        WfRel (zip a b) y x →
          evalOption (zip a b) y i = Option.map₂ Prod.mk (evalOption a y.1 i) (evalOption b y.2 i)) →
      evalOption (zip a b) x i = Option.map₂ Prod.mk (evalOption a x.1 i) (evalOption b x.2 i)
Tactic:
intro q ih
State after:
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
i : ι
q : (zip a b).σ
ih :
  ∀ (y : (zip a b).σ),
    WfRel (zip a b) y q → evalOption (zip a b) y i = Option.map₂ Prod.mk (evalOption a y.1 i) (evalOption b y.2 i)
⊢ evalOption (zip a b) q i = Option.map₂ Prod.mk (evalOption a q.1 i) (evalOption b q.2 i)

State before:
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
i : ι
q : (zip a b).σ
ih :
  ∀ (y : (zip a b).σ),
    WfRel (zip a b) y q → evalOption (zip a b) y i = Option.map₂ Prod.mk (evalOption a y.1 i) (evalOption b y.2 i)
⊢ evalOption (zip a b) q i = Option.map₂ Prod.mk (evalOption a q.1 i) (evalOption b q.2 i)
Tactic:
by_cases hv : (a.zip b).valid q
State after:
case pos
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
i : ι
q : (zip a b).σ
ih :
  ∀ (y : (zip a b).σ),
    WfRel (zip a b) y q → evalOption (zip a b) y i = Option.map₂ Prod.mk (evalOption a y.1 i) (evalOption b y.2 i)
hv : (zip a b).valid q = true
⊢ evalOption (zip a b) q i = Option.map₂ Prod.mk (evalOption a q.1 i) (evalOption b q.2 i)

case neg
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
i : ι
q : (zip a b).σ
ih :
  ∀ (y : (zip a b).σ),
    WfRel (zip a b) y q → evalOption (zip a b) y i = Option.map₂ Prod.mk (evalOption a y.1 i) (evalOption b y.2 i)
hv : ¬(zip a b).valid q = true
⊢ evalOption (zip a b) q i = Option.map₂ Prod.mk (evalOption a q.1 i) (evalOption b q.2 i)

State before:
case pos
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
i : ι
q : (zip a b).σ
ih :
  ∀ (y : (zip a b).σ),
    WfRel (zip a b) y q → evalOption (zip a b) y i = Option.map₂ Prod.mk (evalOption a y.1 i) (evalOption b y.2 i)
hv : (zip a b).valid q = true
⊢ evalOption (zip a b) q i = Option.map₂ Prod.mk (evalOption a q.1 i) (evalOption b q.2 i)

case neg
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
i : ι
q : (zip a b).σ
ih :
  ∀ (y : (zip a b).σ),
    WfRel (zip a b) y q → evalOption (zip a b) y i = Option.map₂ Prod.mk (evalOption a y.1 i) (evalOption b y.2 i)
hv : ¬(zip a b).valid q = true
⊢ evalOption (zip a b) q i = Option.map₂ Prod.mk (evalOption a q.1 i) (evalOption b q.2 i)
Tactic:
swap
State after:
case neg
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
i : ι
q : (zip a b).σ
ih :
  ∀ (y : (zip a b).σ),
    WfRel (zip a b) y q → evalOption (zip a b) y i = Option.map₂ Prod.mk (evalOption a y.1 i) (evalOption b y.2 i)
hv : ¬(zip a b).valid q = true
⊢ evalOption (zip a b) q i = Option.map₂ Prod.mk (evalOption a q.1 i) (evalOption b q.2 i)

case pos
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
i : ι
q : (zip a b).σ
ih :
  ∀ (y : (zip a b).σ),
    WfRel (zip a b) y q → evalOption (zip a b) y i = Option.map₂ Prod.mk (evalOption a y.1 i) (evalOption b y.2 i)
hv : (zip a b).valid q = true
⊢ evalOption (zip a b) q i = Option.map₂ Prod.mk (evalOption a q.1 i) (evalOption b q.2 i)

State before:
case neg
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
i : ι
q : (zip a b).σ
ih :
  ∀ (y : (zip a b).σ),
    WfRel (zip a b) y q → evalOption (zip a b) y i = Option.map₂ Prod.mk (evalOption a y.1 i) (evalOption b y.2 i)
hv : ¬(zip a b).valid q = true
⊢ evalOption (zip a b) q i = Option.map₂ Prod.mk (evalOption a q.1 i) (evalOption b q.2 i)
Tactic:
have := hv
State after:
case neg
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
i : ι
q : (zip a b).σ
ih :
  ∀ (y : (zip a b).σ),
    WfRel (zip a b) y q → evalOption (zip a b) y i = Option.map₂ Prod.mk (evalOption a y.1 i) (evalOption b y.2 i)
hv this : ¬(zip a b).valid q = true
⊢ evalOption (zip a b) q i = Option.map₂ Prod.mk (evalOption a q.1 i) (evalOption b q.2 i)

State before:
case neg
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
i : ι
q : (zip a b).σ
ih :
  ∀ (y : (zip a b).σ),
    WfRel (zip a b) y q → evalOption (zip a b) y i = Option.map₂ Prod.mk (evalOption a y.1 i) (evalOption b y.2 i)
hv this : ¬(zip a b).valid q = true
⊢ evalOption (zip a b) q i = Option.map₂ Prod.mk (evalOption a q.1 i) (evalOption b q.2 i)
Tactic:
simp only [zip_valid, Bool.and_eq_true, not_and_or, Bool.not_eq_true] at hv
State after:
case neg
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
i : ι
q : (zip a b).σ
ih :
  ∀ (y : (zip a b).σ),
    WfRel (zip a b) y q → evalOption (zip a b) y i = Option.map₂ Prod.mk (evalOption a y.1 i) (evalOption b y.2 i)
this : ¬(zip a b).valid q = true
hv : a.valid q.1 = false ∨ b.valid q.2 = false
⊢ evalOption (zip a b) q i = Option.map₂ Prod.mk (evalOption a q.1 i) (evalOption b q.2 i)

State before:
case neg
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
i : ι
q : (zip a b).σ
ih :
  ∀ (y : (zip a b).σ),
    WfRel (zip a b) y q → evalOption (zip a b) y i = Option.map₂ Prod.mk (evalOption a y.1 i) (evalOption b y.2 i)
this : ¬(zip a b).valid q = true
hv : a.valid q.1 = false ∨ b.valid q.2 = false
⊢ evalOption (zip a b) q i = Option.map₂ Prod.mk (evalOption a q.1 i) (evalOption b q.2 i)
Tactic:
rcases hv with hv' | hv' <;> simp [this, hv']
State after:
no goals

State before:
case pos
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
i : ι
q : (zip a b).σ
ih :
  ∀ (y : (zip a b).σ),
    WfRel (zip a b) y q → evalOption (zip a b) y i = Option.map₂ Prod.mk (evalOption a y.1 i) (evalOption b y.2 i)
hv : (zip a b).valid q = true
⊢ evalOption (zip a b) q i = Option.map₂ Prod.mk (evalOption a q.1 i) (evalOption b q.2 i)
Tactic:
rcases lt_trichotomy (α := StreamOrder ι) (i, true) ((a.zip b).toOrder ⟨q, hv⟩) with h|h|h
State after:
case pos.inl
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
i : ι
q : (zip a b).σ
ih :
  ∀ (y : (zip a b).σ),
    WfRel (zip a b) y q → evalOption (zip a b) y i = Option.map₂ Prod.mk (evalOption a y.1 i) (evalOption b y.2 i)
hv : (zip a b).valid q = true
h : (i, true) < toOrder (zip a b) { val := q, property := hv }
⊢ evalOption (zip a b) q i = Option.map₂ Prod.mk (evalOption a q.1 i) (evalOption b q.2 i)

case pos.inr.inl
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
i : ι
q : (zip a b).σ
ih :
  ∀ (y : (zip a b).σ),
    WfRel (zip a b) y q → evalOption (zip a b) y i = Option.map₂ Prod.mk (evalOption a y.1 i) (evalOption b y.2 i)
hv : (zip a b).valid q = true
h : (i, true) = toOrder (zip a b) { val := q, property := hv }
⊢ evalOption (zip a b) q i = Option.map₂ Prod.mk (evalOption a q.1 i) (evalOption b q.2 i)

case pos.inr.inr
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
i : ι
q : (zip a b).σ
ih :
  ∀ (y : (zip a b).σ),
    WfRel (zip a b) y q → evalOption (zip a b) y i = Option.map₂ Prod.mk (evalOption a y.1 i) (evalOption b y.2 i)
hv : (zip a b).valid q = true
h : toOrder (zip a b) { val := q, property := hv } < (i, true)
⊢ evalOption (zip a b) q i = Option.map₂ Prod.mk (evalOption a q.1 i) (evalOption b q.2 i)

State before:
case pos.inl
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
i : ι
q : (zip a b).σ
ih :
  ∀ (y : (zip a b).σ),
    WfRel (zip a b) y q → evalOption (zip a b) y i = Option.map₂ Prod.mk (evalOption a y.1 i) (evalOption b y.2 i)
hv : (zip a b).valid q = true
h : (i, true) < toOrder (zip a b) { val := q, property := hv }
⊢ evalOption (zip a b) q i = Option.map₂ Prod.mk (evalOption a q.1 i) (evalOption b q.2 i)
Tactic:
rw [Prod.Lex.mk_true_lt_iff_lt, toOrder_fst] at h
State after:
case pos.inl
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
i : ι
q : (zip a b).σ
ih :
  ∀ (y : (zip a b).σ),
    WfRel (zip a b) y q → evalOption (zip a b) y i = Option.map₂ Prod.mk (evalOption a y.1 i) (evalOption b y.2 i)
hv : (zip a b).valid q = true
h : i < (zip a b).index { val := q, property := hv }
⊢ evalOption (zip a b) q i = Option.map₂ Prod.mk (evalOption a q.1 i) (evalOption b q.2 i)

State before:
case pos.inl
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
i : ι
q : (zip a b).σ
ih :
  ∀ (y : (zip a b).σ),
    WfRel (zip a b) y q → evalOption (zip a b) y i = Option.map₂ Prod.mk (evalOption a y.1 i) (evalOption b y.2 i)
hv : (zip a b).valid q = true
h : i < (zip a b).index { val := q, property := hv }
⊢ evalOption (zip a b) q i = Option.map₂ Prod.mk (evalOption a q.1 i) (evalOption b q.2 i)
Tactic:
rw [zip_eq_zero_of_lt_toOrder h]
State after:
case pos.inl
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
i : ι
q : (zip a b).σ
ih :
  ∀ (y : (zip a b).σ),
    WfRel (zip a b) y q → evalOption (zip a b) y i = Option.map₂ Prod.mk (evalOption a y.1 i) (evalOption b y.2 i)
hv : (zip a b).valid q = true
h : i < (zip a b).index { val := q, property := hv }
⊢ none = Option.map₂ Prod.mk (evalOption a q.1 i) (evalOption b q.2 i)

State before:
case pos.inl.inr
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
i : ι
q : (zip a b).σ
ih :
  ∀ (y : (zip a b).σ),
    WfRel (zip a b) y q → evalOption (zip a b) y i = Option.map₂ Prod.mk (evalOption a y.1 i) (evalOption b y.2 i)
hv : (zip a b).valid q = true
h : i < (zip a b).index { val := q, property := hv }
h₂ : evalOption b (↑(mul.valid.snd { val := q, property := hv })) i = none
⊢ none = Option.map₂ Prod.mk (evalOption a q.1 i) (evalOption b q.2 i)
Tactic:
simp only [zip_σ, zip_valid, coe_mul_valid_fst, coe_mul_valid_snd] at h₂
State after:
case pos.inl.inr
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
i : ι
q : (zip a b).σ
ih :
  ∀ (y : (zip a b).σ),
    WfRel (zip a b) y q → evalOption (zip a b) y i = Option.map₂ Prod.mk (evalOption a y.1 i) (evalOption b y.2 i)
hv : (zip a b).valid q = true
h : i < (zip a b).index { val := q, property := hv }
h₂ : evalOption b q.2 i = none
⊢ none = Option.map₂ Prod.mk (evalOption a q.1 i) (evalOption b q.2 i)

State before:
case pos.inl.inr
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
i : ι
q : (zip a b).σ
ih :
  ∀ (y : (zip a b).σ),
    WfRel (zip a b) y q → evalOption (zip a b) y i = Option.map₂ Prod.mk (evalOption a y.1 i) (evalOption b y.2 i)
hv : (zip a b).valid q = true
h : i < (zip a b).index { val := q, property := hv }
h₂ : evalOption b q.2 i = none
⊢ none = Option.map₂ Prod.mk (evalOption a q.1 i) (evalOption b q.2 i)
Tactic:
simp [h₂]
State after:
no goals

State before:
case pos.inr.inl
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
i : ι
q : (zip a b).σ
ih :
  ∀ (y : (zip a b).σ),
    WfRel (zip a b) y q → evalOption (zip a b) y i = Option.map₂ Prod.mk (evalOption a y.1 i) (evalOption b y.2 i)
hv : (zip a b).valid q = true
h : (i, true) = toOrder (zip a b) { val := q, property := hv }
⊢ evalOption (zip a b) q i = Option.map₂ Prod.mk (evalOption a q.1 i) (evalOption b q.2 i)
Tactic:
rw [toOrder, Eq.comm, Prod.ext_iff] at h
State after:
case pos.inr.inl
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
i : ι
q : (zip a b).σ
ih :
  ∀ (y : (zip a b).σ),
    WfRel (zip a b) y q → evalOption (zip a b) y i = Option.map₂ Prod.mk (evalOption a y.1 i) (evalOption b y.2 i)
hv : (zip a b).valid q = true
h :
  ((zip a b).index { val := q, property := hv }, (zip a b).ready { val := q, property := hv }).1 = (i, true).1 ∧
    ((zip a b).index { val := q, property := hv }, (zip a b).ready { val := q, property := hv }).2 = (i, true).2
⊢ evalOption (zip a b) q i = Option.map₂ Prod.mk (evalOption a q.1 i) (evalOption b q.2 i)

State before:
case pos.inr.inl
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
i : ι
q : (zip a b).σ
ih :
  ∀ (y : (zip a b).σ),
    WfRel (zip a b) y q → evalOption (zip a b) y i = Option.map₂ Prod.mk (evalOption a y.1 i) (evalOption b y.2 i)
hv : (zip a b).valid q = true
h :
  ((zip a b).index { val := q, property := hv }, (zip a b).ready { val := q, property := hv }).1 = (i, true).1 ∧
    ((zip a b).index { val := q, property := hv }, (zip a b).ready { val := q, property := hv }).2 = (i, true).2
⊢ evalOption (zip a b) q i = Option.map₂ Prod.mk (evalOption a q.1 i) (evalOption b q.2 i)
Tactic:
simp only [zip_σ, zip_valid, Bool.and_eq_true, decide_eq_true_eq] at h
State after:
case pos.inr.inl
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
i : ι
q : (zip a b).σ
ih :
  ∀ (y : (zip a b).σ),
    WfRel (zip a b) y q → evalOption (zip a b) y i = Option.map₂ Prod.mk (evalOption a y.1 i) (evalOption b y.2 i)
hv : (zip a b).valid q = true
h : (zip a b).index { val := q, property := hv } = i ∧ (zip a b).ready { val := q, property := hv } = true
⊢ evalOption (zip a b) q i = Option.map₂ Prod.mk (evalOption a q.1 i) (evalOption b q.2 i)

State before:
case pos.inr.inl
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
i : ι
q : (zip a b).σ
ih :
  ∀ (y : (zip a b).σ),
    WfRel (zip a b) y q → evalOption (zip a b) y i = Option.map₂ Prod.mk (evalOption a y.1 i) (evalOption b y.2 i)
hv : (zip a b).valid q = true
h : (zip a b).index { val := q, property := hv } = i ∧ (zip a b).ready { val := q, property := hv } = true
⊢ evalOption (zip a b) q i = Option.map₂ Prod.mk (evalOption a q.1 i) (evalOption b q.2 i)
Tactic:
rcases h with ⟨rfl, hr⟩
State after:
case pos.inr.inl.intro
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
q : (zip a b).σ
hv : (zip a b).valid q = true
hr : (zip a b).ready { val := q, property := hv } = true
ih :
  ∀ (y : (zip a b).σ),
    WfRel (zip a b) y q →
      evalOption (zip a b) y ((zip a b).index { val := q, property := hv }) =
        Option.map₂ Prod.mk (evalOption a y.1 ((zip a b).index { val := q, property := hv }))
          (evalOption b y.2 ((zip a b).index { val := q, property := hv }))
⊢ evalOption (zip a b) q ((zip a b).index { val := q, property := hv }) =
    Option.map₂ Prod.mk (evalOption a q.1 ((zip a b).index { val := q, property := hv }))
      (evalOption b q.2 ((zip a b).index { val := q, property := hv }))

State before:
case pos.inr.inl.intro
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
q : (zip a b).σ
hv : (zip a b).valid q = true
hr : (zip a b).ready { val := q, property := hv } = true
ih :
  ∀ (y : (zip a b).σ),
    WfRel (zip a b) y q →
      evalOption (zip a b) y ((zip a b).index { val := q, property := hv }) =
        Option.map₂ Prod.mk (evalOption a y.1 ((zip a b).index { val := q, property := hv }))
          (evalOption b y.2 ((zip a b).index { val := q, property := hv }))
⊢ evalOption (zip a b) q ((zip a b).index { val := q, property := hv }) =
    Option.map₂ Prod.mk (evalOption a q.1 ((zip a b).index { val := q, property := hv }))
      (evalOption b q.2 ((zip a b).index { val := q, property := hv }))
Tactic:
rw [zip_ready_eq hr, (zip_ready_eq'' hr).1, (zip_ready_eq'' hr).2]
State after:
case pos.inr.inl.intro
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
q : (zip a b).σ
hv : (zip a b).valid q = true
hr : (zip a b).ready { val := q, property := hv } = true
ih :
  ∀ (y : (zip a b).σ),
    WfRel (zip a b) y q →
      evalOption (zip a b) y ((zip a b).index { val := q, property := hv }) =
        Option.map₂ Prod.mk (evalOption a y.1 ((zip a b).index { val := q, property := hv }))
          (evalOption b y.2 ((zip a b).index { val := q, property := hv }))
⊢ some
      (a.value (mul.ready.fst { val := { val := q, property := hv }, property := hr }),
        b.value (mul.ready.snd { val := { val := q, property := hv }, property := hr })) =
    Option.map₂ Prod.mk (some (a.value (mul.ready.fst { val := { val := q, property := hv }, property := hr })))
      (some (b.value (mul.ready.snd { val := { val := q, property := hv }, property := hr })))

State before:
case pos.inr.inl.intro
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
q : (zip a b).σ
hv : (zip a b).valid q = true
hr : (zip a b).ready { val := q, property := hv } = true
ih :
  ∀ (y : (zip a b).σ),
    WfRel (zip a b) y q →
      evalOption (zip a b) y ((zip a b).index { val := q, property := hv }) =
        Option.map₂ Prod.mk (evalOption a y.1 ((zip a b).index { val := q, property := hv }))
          (evalOption b y.2 ((zip a b).index { val := q, property := hv }))
⊢ some
      (a.value (mul.ready.fst { val := { val := q, property := hv }, property := hr }),
        b.value (mul.ready.snd { val := { val := q, property := hv }, property := hr })) =
    Option.map₂ Prod.mk (some (a.value (mul.ready.fst { val := { val := q, property := hv }, property := hr })))
      (some (b.value (mul.ready.snd { val := { val := q, property := hv }, property := hr })))
Tactic:
rfl
State after:
no goals

State before:
case pos.inr.inr
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
i : ι
q : (zip a b).σ
ih :
  ∀ (y : (zip a b).σ),
    WfRel (zip a b) y q → evalOption (zip a b) y i = Option.map₂ Prod.mk (evalOption a y.1 i) (evalOption b y.2 i)
hv : (zip a b).valid q = true
h : toOrder (zip a b) { val := q, property := hv } < (i, true)
⊢ evalOption (zip a b) q i = Option.map₂ Prod.mk (evalOption a q.1 i) (evalOption b q.2 i)
Tactic:
have not_ready := not_ready_of_toOrder_lt h
State after:
case pos.inr.inr
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
i : ι
q : (zip a b).σ
ih :
  ∀ (y : (zip a b).σ),
    WfRel (zip a b) y q → evalOption (zip a b) y i = Option.map₂ Prod.mk (evalOption a y.1 i) (evalOption b y.2 i)
hv : (zip a b).valid q = true
h : toOrder (zip a b) { val := q, property := hv } < (i, true)
not_ready : ¬(zip a b).ready { val := q, property := hv } = true ∨ (zip a b).index { val := q, property := hv } ≠ i
⊢ evalOption (zip a b) q i = Option.map₂ Prod.mk (evalOption a q.1 i) (evalOption b q.2 i)

State before:
case pos.inr.inr
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
i : ι
q : (zip a b).σ
ih :
  ∀ (y : (zip a b).σ),
    WfRel (zip a b) y q → evalOption (zip a b) y i = Option.map₂ Prod.mk (evalOption a y.1 i) (evalOption b y.2 i)
hv : (zip a b).valid q = true
h : toOrder (zip a b) { val := q, property := hv } < (i, true)
not_ready : ¬(zip a b).ready { val := q, property := hv } = true ∨ (zip a b).index { val := q, property := hv } ≠ i
⊢ evalOption (zip a b) q i = Option.map₂ Prod.mk (evalOption a q.1 i) (evalOption b q.2 i)
Tactic:
rw [Prod.Lex.lt_mk_true_iff] at h
State after:
case pos.inr.inr
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
i : ι
q : (zip a b).σ
ih :
  ∀ (y : (zip a b).σ),
    WfRel (zip a b) y q → evalOption (zip a b) y i = Option.map₂ Prod.mk (evalOption a y.1 i) (evalOption b y.2 i)
hv : (zip a b).valid q = true
h : toOrder (zip a b) { val := q, property := hv } ≤ (i, false)
not_ready : ¬(zip a b).ready { val := q, property := hv } = true ∨ (zip a b).index { val := q, property := hv } ≠ i
⊢ evalOption (zip a b) q i = Option.map₂ Prod.mk (evalOption a q.1 i) (evalOption b q.2 i)

State before:
case pos.inr.inr
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
i : ι
q : (zip a b).σ
ih :
  ∀ (y : (zip a b).σ),
    WfRel (zip a b) y q → evalOption (zip a b) y i = Option.map₂ Prod.mk (evalOption a y.1 i) (evalOption b y.2 i)
hv : (zip a b).valid q = true
h : toOrder (zip a b) { val := q, property := hv } ≤ (i, false)
not_ready : ¬(zip a b).ready { val := q, property := hv } = true ∨ (zip a b).index { val := q, property := hv } ≠ i
⊢ evalOption (zip a b) q i = Option.map₂ Prod.mk (evalOption a q.1 i) (evalOption b q.2 i)
Tactic:
have := left_right_eval_eq_of_toOrder_le h
State after:
case pos.inr.inr
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
i : ι
q : (zip a b).σ
ih :
  ∀ (y : (zip a b).σ),
    WfRel (zip a b) y q → evalOption (zip a b) y i = Option.map₂ Prod.mk (evalOption a y.1 i) (evalOption b y.2 i)
hv : (zip a b).valid q = true
h : toOrder (zip a b) { val := q, property := hv } ≤ (i, false)
not_ready : ¬(zip a b).ready { val := q, property := hv } = true ∨ (zip a b).index { val := q, property := hv } ≠ i
this :
  evalOption a (advance (zip a b) ↑{ val := q, property := hv }).1 i =
      evalOption a (↑(mul.valid.fst { val := q, property := hv })) i ∧
    evalOption b (advance (zip a b) ↑{ val := q, property := hv }).2 i =
      evalOption b (↑(mul.valid.snd { val := q, property := hv })) i
⊢ evalOption (zip a b) q i = Option.map₂ Prod.mk (evalOption a q.1 i) (evalOption b q.2 i)

State before:
case pos.inr.inr
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
i : ι
q : (zip a b).σ
ih :
  ∀ (y : (zip a b).σ),
    WfRel (zip a b) y q → evalOption (zip a b) y i = Option.map₂ Prod.mk (evalOption a y.1 i) (evalOption b y.2 i)
hv : (zip a b).valid q = true
h : toOrder (zip a b) { val := q, property := hv } ≤ (i, false)
not_ready : ¬(zip a b).ready { val := q, property := hv } = true ∨ (zip a b).index { val := q, property := hv } ≠ i
this :
  evalOption a (advance (zip a b) ↑{ val := q, property := hv }).1 i =
      evalOption a (↑(mul.valid.fst { val := q, property := hv })) i ∧
    evalOption b (advance (zip a b) ↑{ val := q, property := hv }).2 i =
      evalOption b (↑(mul.valid.snd { val := q, property := hv })) i
⊢ evalOption (zip a b) q i = Option.map₂ Prod.mk (evalOption a q.1 i) (evalOption b q.2 i)
Tactic:
rw [(a.zip b).evalOption_not_ready ⟨q, hv⟩ _ not_ready, ih _ ((a.zip b).next_wf ⟨q, hv⟩), this.1, this.2]
State after:
case pos.inr.inr
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
i : ι
q : (zip a b).σ
ih :
  ∀ (y : (zip a b).σ),
    WfRel (zip a b) y q → evalOption (zip a b) y i = Option.map₂ Prod.mk (evalOption a y.1 i) (evalOption b y.2 i)
hv : (zip a b).valid q = true
h : toOrder (zip a b) { val := q, property := hv } ≤ (i, false)
not_ready : ¬(zip a b).ready { val := q, property := hv } = true ∨ (zip a b).index { val := q, property := hv } ≠ i
this :
  evalOption a (advance (zip a b) ↑{ val := q, property := hv }).1 i =
      evalOption a (↑(mul.valid.fst { val := q, property := hv })) i ∧
    evalOption b (advance (zip a b) ↑{ val := q, property := hv }).2 i =
      evalOption b (↑(mul.valid.snd { val := q, property := hv })) i
⊢ Option.map₂ Prod.mk (evalOption a (↑(mul.valid.fst { val := q, property := hv })) i)
      (evalOption b (↑(mul.valid.snd { val := q, property := hv })) i) =
    Option.map₂ Prod.mk (evalOption a q.1 i) (evalOption b q.2 i)

State before:
case pos.inr.inr
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
i : ι
q : (zip a b).σ
ih :
  ∀ (y : (zip a b).σ),
    WfRel (zip a b) y q → evalOption (zip a b) y i = Option.map₂ Prod.mk (evalOption a y.1 i) (evalOption b y.2 i)
hv : (zip a b).valid q = true
h : toOrder (zip a b) { val := q, property := hv } ≤ (i, false)
not_ready : ¬(zip a b).ready { val := q, property := hv } = true ∨ (zip a b).index { val := q, property := hv } ≠ i
this :
  evalOption a (advance (zip a b) ↑{ val := q, property := hv }).1 i =
      evalOption a (↑(mul.valid.fst { val := q, property := hv })) i ∧
    evalOption b (advance (zip a b) ↑{ val := q, property := hv }).2 i =
      evalOption b (↑(mul.valid.snd { val := q, property := hv })) i
⊢ Option.map₂ Prod.mk (evalOption a (↑(mul.valid.fst { val := q, property := hv })) i)
      (evalOption b (↑(mul.valid.snd { val := q, property := hv })) i) =
    Option.map₂ Prod.mk (evalOption a q.1 i) (evalOption b q.2 i)
Tactic:
rfl
State after:
no goals