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

State before:
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
i : ι
q : { x // (zip a b).valid x = true }
hi : i < (zip a b).index q
⊢ evalOption a (↑(mul.valid.fst q)) i = none ∨ evalOption b (↑(mul.valid.snd q)) i = none
Tactic:
simp only [zip_index, lt_max_iff] at hi
State after:
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
i : ι
q : { x // (zip a b).valid x = true }
hi : i < a.index (mul.valid.fst q) ∨ i < b.index (mul.valid.snd q)
⊢ evalOption a (↑(mul.valid.fst q)) i = none ∨ evalOption b (↑(mul.valid.snd q)) i = none

State before:
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
i : ι
q : { x // (zip a b).valid x = true }
hi : i < a.index (mul.valid.fst q) ∨ i < b.index (mul.valid.snd q)
⊢ evalOption a (↑(mul.valid.fst q)) i = none ∨ evalOption b (↑(mul.valid.snd q)) i = none
Tactic:
refine hi.imp ?_ ?_ <;> intro hi
State after:
case refine_1
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
i : ι
q : { x // (zip a b).valid x = true }
hi✝ : i < a.index (mul.valid.fst q) ∨ i < b.index (mul.valid.snd q)
hi : i < a.index (mul.valid.fst q)
⊢ evalOption a (↑(mul.valid.fst q)) i = none

case refine_2
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
i : ι
q : { x // (zip a b).valid x = true }
hi✝ : i < a.index (mul.valid.fst q) ∨ i < b.index (mul.valid.snd q)
hi : i < b.index (mul.valid.snd q)
⊢ evalOption b (↑(mul.valid.snd q)) i = none

State before:
case refine_1
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
i : ι
q : { x // (zip a b).valid x = true }
hi✝ : i < a.index (mul.valid.fst q) ∨ i < b.index (mul.valid.snd q)
hi : i < a.index (mul.valid.fst q)
⊢ evalOption a (↑(mul.valid.fst q)) i = none
Tactic:
have := a.mono.eq_empty_of_lt_index (q := mul.valid.fst q) i (by rwa [index'_val, WithTop.coe_lt_coe])
State after:
case refine_1
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
i : ι
q : { x // (zip a b).valid x = true }
hi✝ : i < a.index (mul.valid.fst q) ∨ i < b.index (mul.valid.snd q)
hi : i < a.index (mul.valid.fst q)
this : (evalMultiset a ↑(mul.valid.fst q)) i = 0
⊢ evalOption a (↑(mul.valid.fst q)) i = none

State before:
case refine_1
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
i : ι
q : { x // (zip a b).valid x = true }
hi✝ : i < a.index (mul.valid.fst q) ∨ i < b.index (mul.valid.snd q)
hi : i < a.index (mul.valid.fst q)
this : (evalMultiset a ↑(mul.valid.fst q)) i = 0
⊢ evalOption a (↑(mul.valid.fst q)) i = none
Tactic:
rw [Stream.evalOption, this, Multiset.get_zero]
State after:
no goals

State before:
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
i : ι
q : { x // (zip a b).valid x = true }
hi✝ : i < a.index (mul.valid.fst q) ∨ i < b.index (mul.valid.snd q)
hi : i < a.index (mul.valid.fst q)
⊢ ↑i < index' a ↑(mul.valid.fst q)
Tactic:
rwa [index'_val, WithTop.coe_lt_coe]
State after:
no goals

State before:
case refine_2
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
i : ι
q : { x // (zip a b).valid x = true }
hi✝ : i < a.index (mul.valid.fst q) ∨ i < b.index (mul.valid.snd q)
hi : i < b.index (mul.valid.snd q)
⊢ evalOption b (↑(mul.valid.snd q)) i = none
Tactic:
have := b.mono.eq_empty_of_lt_index (q := mul.valid.snd q) i (by rwa [index'_val, WithTop.coe_lt_coe])
State after:
case refine_2
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
i : ι
q : { x // (zip a b).valid x = true }
hi✝ : i < a.index (mul.valid.fst q) ∨ i < b.index (mul.valid.snd q)
hi : i < b.index (mul.valid.snd q)
this : (evalMultiset b ↑(mul.valid.snd q)) i = 0
⊢ evalOption b (↑(mul.valid.snd q)) i = none

State before:
case refine_2
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
i : ι
q : { x // (zip a b).valid x = true }
hi✝ : i < a.index (mul.valid.fst q) ∨ i < b.index (mul.valid.snd q)
hi : i < b.index (mul.valid.snd q)
this : (evalMultiset b ↑(mul.valid.snd q)) i = 0
⊢ evalOption b (↑(mul.valid.snd q)) i = none
Tactic:
rw [Stream.evalOption, this, Multiset.get_zero]
State after:
no goals

State before:
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
i : ι
q : { x // (zip a b).valid x = true }
hi✝ : i < a.index (mul.valid.fst q) ∨ i < b.index (mul.valid.snd q)
hi : i < b.index (mul.valid.snd q)
⊢ ↑i < index' b ↑(mul.valid.snd q)
Tactic:
rwa [index'_val, WithTop.coe_lt_coe]
State after:
no goals