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

State before:
ι : Type
inst✝ : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
ha : IsStrictMono a
hb : IsStrictMono b
q : { q // (zip a b).valid q = true }
i : StreamOrder ι
H : toOrder (zip a b) q ≤ i
hr : (zip a b).ready q = true
⊢ index' (zip a b) ↑q < index' (zip a b) ((zip a b).seek q i)
Tactic:
simp only [zip_index']
State after:
ι : Type
inst✝ : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
ha : IsStrictMono a
hb : IsStrictMono b
q : { q // (zip a b).valid q = true }
i : StreamOrder ι
H : toOrder (zip a b) q ≤ i
hr : (zip a b).ready q = true
⊢ max (index' a (↑q).1) (index' b (↑q).2) < max (index' a ((zip a b).seek q i).1) (index' b ((zip a b).seek q i).2)

State before:
ι : Type
inst✝ : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
ha : IsStrictMono a
hb : IsStrictMono b
q : { q // (zip a b).valid q = true }
i : StreamOrder ι
H : toOrder (zip a b) q ≤ i
hr : (zip a b).ready q = true
⊢ max (index' a (↑q).1) (index' b (↑q).2) < max (index' a ((zip a b).seek q i).1) (index' b ((zip a b).seek q i).2)
Tactic:
have := order_eq_of_zip_ready hr
State after:
ι : Type
inst✝ : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
ha : IsStrictMono a
hb : IsStrictMono b
q : { q // (zip a b).valid q = true }
i : StreamOrder ι
H : toOrder (zip a b) q ≤ i
hr : (zip a b).ready q = true
this : toOrder a (mul.valid.fst q) = toOrder (zip a b) q ∧ toOrder b (mul.valid.snd q) = toOrder (zip a b) q
⊢ max (index' a (↑q).1) (index' b (↑q).2) < max (index' a ((zip a b).seek q i).1) (index' b ((zip a b).seek q i).2)

State before:
ι : Type
inst✝ : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
ha : IsStrictMono a
hb : IsStrictMono b
q : { q // (zip a b).valid q = true }
i : StreamOrder ι
H : toOrder (zip a b) q ≤ i
hr : (zip a b).ready q = true
this : toOrder a (mul.valid.fst q) = toOrder (zip a b) q ∧ toOrder b (mul.valid.snd q) = toOrder (zip a b) q
⊢ max (index' a (↑q).1) (index' b (↑q).2) < max (index' a ((zip a b).seek q i).1) (index' b ((zip a b).seek q i).2)
Tactic:
simp at hr
State after:
ι : Type
inst✝ : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
ha : IsStrictMono a
hb : IsStrictMono b
q : { q // (zip a b).valid q = true }
i : StreamOrder ι
H : toOrder (zip a b) q ≤ i
this : toOrder a (mul.valid.fst q) = toOrder (zip a b) q ∧ toOrder b (mul.valid.snd q) = toOrder (zip a b) q
hr :
  (a.ready (mul.valid.fst q) = true ∧ b.ready (mul.valid.snd q) = true) ∧
    a.index (mul.valid.fst q) = b.index (mul.valid.snd q)
⊢ max (index' a (↑q).1) (index' b (↑q).2) < max (index' a ((zip a b).seek q i).1) (index' b ((zip a b).seek q i).2)

State before:
ι : Type
inst✝ : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
ha : IsStrictMono a
hb : IsStrictMono b
q : { q // (zip a b).valid q = true }
i : StreamOrder ι
H : toOrder (zip a b) q ≤ i
this : toOrder a (mul.valid.fst q) = toOrder (zip a b) q ∧ toOrder b (mul.valid.snd q) = toOrder (zip a b) q
hr :
  (a.ready (mul.valid.fst q) = true ∧ b.ready (mul.valid.snd q) = true) ∧
    a.index (mul.valid.fst q) = b.index (mul.valid.snd q)
⊢ max (index' a (↑q).1) (index' b (↑q).2) < max (index' a ((zip a b).seek q i).1) (index' b ((zip a b).seek q i).2)
Tactic:
apply max_lt_max (ha.lt (hr := hr.1.1) ..) (hb.lt (hr := hr.1.2) ..) <;>
  simpa [this]
State after:
no goals