Theorem: Etch.Verification.Stream.zip_ready_eq' (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 : { x // (zip a b).valid x = true }
h : (zip a b).ready q = true
⊢ evalOption a (↑(mul.valid.fst q)) ((zip a b).index q) = some (a.value (mul.ready.fst { val := q, property := h })) ∧
    evalOption b (↑(mul.valid.snd q)) ((zip a b).index q) = some (b.value (mul.ready.snd { val := q, property := h }))
Tactic:
have Ha : (a.zip b).index q = (a.index <| mul.valid.fst q) := by aesop
State after:
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
q : { x // (zip a b).valid x = true }
h : (zip a b).ready q = true
Ha : (zip a b).index q = a.index (mul.valid.fst q)
⊢ evalOption a (↑(mul.valid.fst q)) ((zip a b).index q) = some (a.value (mul.ready.fst { val := q, property := h })) ∧
    evalOption b (↑(mul.valid.snd q)) ((zip a b).index q) = some (b.value (mul.ready.snd { val := q, property := h }))

State before:
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
q : { x // (zip a b).valid x = true }
h : (zip a b).ready q = true
Ha : (zip a b).index q = a.index (mul.valid.fst q)
⊢ evalOption a (↑(mul.valid.fst q)) ((zip a b).index q) = some (a.value (mul.ready.fst { val := q, property := h })) ∧
    evalOption b (↑(mul.valid.snd q)) ((zip a b).index q) = some (b.value (mul.ready.snd { val := q, property := h }))
Tactic:
have Hb : (a.zip b).index q = (b.index <| mul.valid.snd q) := by aesop
State after:
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
q : { x // (zip a b).valid x = true }
h : (zip a b).ready q = true
Ha : (zip a b).index q = a.index (mul.valid.fst q)
Hb : (zip a b).index q = b.index (mul.valid.snd q)
⊢ evalOption a (↑(mul.valid.fst q)) ((zip a b).index q) = some (a.value (mul.ready.fst { val := q, property := h })) ∧
    evalOption b (↑(mul.valid.snd q)) ((zip a b).index q) = some (b.value (mul.ready.snd { val := q, property := h }))

State before:
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
q : { x // (zip a b).valid x = true }
h : (zip a b).ready q = true
Ha : (zip a b).index q = a.index (mul.valid.fst q)
Hb : (zip a b).index q = b.index (mul.valid.snd q)
⊢ evalOption a (↑(mul.valid.fst q)) ((zip a b).index q) = some (a.value (mul.ready.fst { val := q, property := h })) ∧
    evalOption b (↑(mul.valid.snd q)) ((zip a b).index q) = some (b.value (mul.ready.snd { val := q, property := h }))
Tactic:
constructor
State after:
case left
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
q : { x // (zip a b).valid x = true }
h : (zip a b).ready q = true
Ha : (zip a b).index q = a.index (mul.valid.fst q)
Hb : (zip a b).index q = b.index (mul.valid.snd q)
⊢ evalOption a (↑(mul.valid.fst q)) ((zip a b).index q) = some (a.value (mul.ready.fst { val := q, property := h }))

case right
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
q : { x // (zip a b).valid x = true }
h : (zip a b).ready q = true
Ha : (zip a b).index q = a.index (mul.valid.fst q)
Hb : (zip a b).index q = b.index (mul.valid.snd q)
⊢ evalOption b (↑(mul.valid.snd q)) ((zip a b).index q) = some (b.value (mul.ready.snd { val := q, property := h }))

State before:
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
q : { x // (zip a b).valid x = true }
h : (zip a b).ready q = true
⊢ (zip a b).index q = a.index (mul.valid.fst q)
Tactic:
aesop
State after:
no goals

State before:
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
q : { x // (zip a b).valid x = true }
h : (zip a b).ready q = true
Ha : (zip a b).index q = a.index (mul.valid.fst q)
⊢ (zip a b).index q = b.index (mul.valid.snd q)
Tactic:
aesop
State after:
no goals

State before:
case left
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
q : { x // (zip a b).valid x = true }
h : (zip a b).ready q = true
Ha : (zip a b).index q = a.index (mul.valid.fst q)
Hb : (zip a b).index q = b.index (mul.valid.snd q)
⊢ evalOption a (↑(mul.valid.fst q)) ((zip a b).index q) = some (a.value (mul.ready.fst { val := q, property := h }))
Tactic:
rw [Ha, a.strictMono.evalOption_ready]
State after:
case left
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
q : { x // (zip a b).valid x = true }
h : (zip a b).ready q = true
Ha : (zip a b).index q = a.index (mul.valid.fst q)
Hb : (zip a b).index q = b.index (mul.valid.snd q)
⊢ some (a.value { val := mul.valid.fst q, property := ?left }) =
    some (a.value (mul.ready.fst { val := q, property := h }))

case left
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
q : { x // (zip a b).valid x = true }
h : (zip a b).ready q = true
Ha : (zip a b).index q = a.index (mul.valid.fst q)
Hb : (zip a b).index q = b.index (mul.valid.snd q)
⊢ a.ready (mul.valid.fst q) = true

State before:
case left
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
q : { x // (zip a b).valid x = true }
h : (zip a b).ready q = true
Ha : (zip a b).index q = a.index (mul.valid.fst q)
Hb : (zip a b).index q = b.index (mul.valid.snd q)
⊢ some (a.value { val := mul.valid.fst q, property := ?left }) =
    some (a.value (mul.ready.fst { val := q, property := h }))

case left
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
q : { x // (zip a b).valid x = true }
h : (zip a b).ready q = true
Ha : (zip a b).index q = a.index (mul.valid.fst q)
Hb : (zip a b).index q = b.index (mul.valid.snd q)
⊢ a.ready (mul.valid.fst q) = true
Tactic:
rfl
State after:
no goals

State before:
case right
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
q : { x // (zip a b).valid x = true }
h : (zip a b).ready q = true
Ha : (zip a b).index q = a.index (mul.valid.fst q)
Hb : (zip a b).index q = b.index (mul.valid.snd q)
⊢ evalOption b (↑(mul.valid.snd q)) ((zip a b).index q) = some (b.value (mul.ready.snd { val := q, property := h }))
Tactic:
rw [Hb, b.strictMono.evalOption_ready]
State after:
case right
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
q : { x // (zip a b).valid x = true }
h : (zip a b).ready q = true
Ha : (zip a b).index q = a.index (mul.valid.fst q)
Hb : (zip a b).index q = b.index (mul.valid.snd q)
⊢ some (b.value { val := mul.valid.snd q, property := ?right }) =
    some (b.value (mul.ready.snd { val := q, property := h }))

case right
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
q : { x // (zip a b).valid x = true }
h : (zip a b).ready q = true
Ha : (zip a b).index q = a.index (mul.valid.fst q)
Hb : (zip a b).index q = b.index (mul.valid.snd q)
⊢ b.ready (mul.valid.snd q) = true

State before:
case right
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
q : { x // (zip a b).valid x = true }
h : (zip a b).ready q = true
Ha : (zip a b).index q = a.index (mul.valid.fst q)
Hb : (zip a b).index q = b.index (mul.valid.snd q)
⊢ some (b.value { val := mul.valid.snd q, property := ?right }) =
    some (b.value (mul.ready.snd { val := q, property := h }))

case right
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
q : { x // (zip a b).valid x = true }
h : (zip a b).ready q = true
Ha : (zip a b).index q = a.index (mul.valid.fst q)
Hb : (zip a b).index q = b.index (mul.valid.snd q)
⊢ b.ready (mul.valid.snd q) = true
Tactic:
rfl
State after:
no goals