internlm/Lean-Github huggingface dataset:
Theorem: Etch.Verification.Stream.min_toOrder_le
Proof state before:
ι : Type
inst✝ : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
q : { p // mul.valid a b p = true }
⊢ min (toOrder a (mul.valid.fst q)).1 (toOrder b (mul.valid.snd q)).1 ≤ (toOrder (zip a b) q).1 ∧
    (min (toOrder a (mul.valid.fst q)).1 (toOrder b (mul.valid.snd q)).1 = (toOrder (zip a b) q).1 →
      (min (toOrder a (mul.valid.fst q)) (toOrder b (mul.valid.snd q))).2 ≤ (toOrder (zip a b) q).2)
Tactic:
constructor
Proof state after:
case left
ι : Type
inst✝ : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
q : { p // mul.valid a b p = true }
⊢ min (toOrder a (mul.valid.fst q)).1 (toOrder b (mul.valid.snd q)).1 ≤ (toOrder (zip a b) q).1

case right
ι : Type
inst✝ : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
q : { p // mul.valid a b p = true }
⊢ min (toOrder a (mul.valid.fst q)).1 (toOrder b (mul.valid.snd q)).1 = (toOrder (zip a b) q).1 →
    (min (toOrder a (mul.valid.fst q)) (toOrder b (mul.valid.snd q))).2 ≤ (toOrder (zip a b) q).2
Theorem: Etch.Verification.Stream.min_toOrder_le
Proof state before:
case left
ι : Type
inst✝ : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
q : { p // mul.valid a b p = true }
⊢ min (toOrder a (mul.valid.fst q)).1 (toOrder b (mul.valid.snd q)).1 ≤ (toOrder (zip a b) q).1
Tactic:
exact min_le_max
Proof state after:
no goals
Theorem: Etch.Verification.Stream.min_toOrder_le
Proof state before:
case right
ι : Type
inst✝ : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
q : { p // mul.valid a b p = true }
⊢ min (toOrder a (mul.valid.fst q)).1 (toOrder b (mul.valid.snd q)).1 = (toOrder (zip a b) q).1 →
    (min (toOrder a (mul.valid.fst q)) (toOrder b (mul.valid.snd q))).2 ≤ (toOrder (zip a b) q).2
Tactic:
simp only [toOrder]
Proof state after:
case right
ι : Type
inst✝ : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
q : { p // mul.valid a b p = true }
⊢ min (a.index (mul.valid.fst q)) (b.index (mul.valid.snd q)) = (zip a b).index q →
    (min (a.index (mul.valid.fst q), a.ready (mul.valid.fst q))
          (b.index (mul.valid.snd q), b.ready (mul.valid.snd q))).2 ≤
      (zip a b).ready q
Theorem: Etch.Verification.Stream.min_toOrder_le
Proof state before:
case right
ι : Type
inst✝ : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
q : { p // mul.valid a b p = true }
⊢ min (a.index (mul.valid.fst q)) (b.index (mul.valid.snd q)) = (zip a b).index q →
    (min (a.index (mul.valid.fst q), a.ready (mul.valid.fst q))
          (b.index (mul.valid.snd q), b.ready (mul.valid.snd q))).2 ≤
      (zip a b).ready q
Tactic:
aesop
Proof state after:
no goals
Theorem: Etch.Verification.Stream.toOrder_le_max
Proof state before:
ι : Type
inst✝ : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
q : { q // (zip a b).valid q = true }
⊢ toOrder (zip a b) q ≤ max (toOrder a (mul.valid.fst q)) (toOrder b (mul.valid.snd q))
Tactic:
rw [Prod.Lex.le_iff']
Proof state after:
ι : Type
inst✝ : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
q : { q // (zip a b).valid q = true }
⊢ (toOrder (zip a b) q).1 < (max (toOrder a (mul.valid.fst q)) (toOrder b (mul.valid.snd q))).1 ∨
    (toOrder (zip a b) q).1 = (max (toOrder a (mul.valid.fst q)) (toOrder b (mul.valid.snd q))).1 ∧
      (toOrder (zip a b) q).2 ≤ (max (toOrder a (mul.valid.fst q)) (toOrder b (mul.valid.snd q))).2
Theorem: Etch.Verification.Stream.toOrder_le_max
Proof state before:
ι : Type
inst✝ : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
q : { q // (zip a b).valid q = true }
⊢ (toOrder (zip a b) q).1 < (max (toOrder a (mul.valid.fst q)) (toOrder b (mul.valid.snd q))).1 ∨
    (toOrder (zip a b) q).1 = (max (toOrder a (mul.valid.fst q)) (toOrder b (mul.valid.snd q))).1 ∧
      (toOrder (zip a b) q).2 ≤ (max (toOrder a (mul.valid.fst q)) (toOrder b (mul.valid.snd q))).2
Tactic:
right
Proof state after:
case h
ι : Type
inst✝ : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
q : { q // (zip a b).valid q = true }
⊢ (toOrder (zip a b) q).1 = (max (toOrder a (mul.valid.fst q)) (toOrder b (mul.valid.snd q))).1 ∧
    (toOrder (zip a b) q).2 ≤ (max (toOrder a (mul.valid.fst q)) (toOrder b (mul.valid.snd q))).2
Theorem: Etch.Verification.Stream.toOrder_le_max
Proof state before:
case h
ι : Type
inst✝ : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
q : { q // (zip a b).valid q = true }
⊢ (toOrder (zip a b) q).1 = (max (toOrder a (mul.valid.fst q)) (toOrder b (mul.valid.snd q))).1 ∧
    (toOrder (zip a b) q).2 ≤ (max (toOrder a (mul.valid.fst q)) (toOrder b (mul.valid.snd q))).2
Tactic:
constructor
Proof state after:
case h.left
ι : Type
inst✝ : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
q : { q // (zip a b).valid q = true }
⊢ (toOrder (zip a b) q).1 = (max (toOrder a (mul.valid.fst q)) (toOrder b (mul.valid.snd q))).1

case h.right
ι : Type
inst✝ : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
q : { q // (zip a b).valid q = true }
⊢ (toOrder (zip a b) q).2 ≤ (max (toOrder a (mul.valid.fst q)) (toOrder b (mul.valid.snd q))).2
Theorem: Etch.Verification.Stream.toOrder_le_max
Proof state before:
case h.left
ι : Type
inst✝ : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
q : { q // (zip a b).valid q = true }
⊢ (toOrder (zip a b) q).1 = (max (toOrder a (mul.valid.fst q)) (toOrder b (mul.valid.snd q))).1
Tactic:
simp [Monotone.map_max (@Prod.Lex.fst_mono ι Bool _ _)]
Proof state after:
no goals
Theorem: Etch.Verification.Stream.toOrder_le_max
Proof state before:
case h.right
ι : Type
inst✝ : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
q : { q // (zip a b).valid q = true }
⊢ (toOrder (zip a b) q).2 ≤ (max (toOrder a (mul.valid.fst q)) (toOrder b (mul.valid.snd q))).2
Tactic:
simp only [Bool.le_iff_imp, toOrder]
Proof state after:
case h.right
ι : Type
inst✝ : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
q : { q // (zip a b).valid q = true }
⊢ (zip a b).ready q = true →
    (max (a.index (mul.valid.fst q), a.ready (mul.valid.fst q))
          (b.index (mul.valid.snd q), b.ready (mul.valid.snd q))).2 =
      true
Theorem: Etch.Verification.Stream.toOrder_le_max
Proof state before:
case h.right
ι : Type
inst✝ : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
q : { q // (zip a b).valid q = true }
⊢ (zip a b).ready q = true →
    (max (a.index (mul.valid.fst q), a.ready (mul.valid.fst q))
          (b.index (mul.valid.snd q), b.ready (mul.valid.snd q))).2 =
      true
Tactic:
aesop
Proof state after:
no goals
Theorem: Etch.Verification.Stream.zip_mono
Proof state before:
ι : Type
inst✝ : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
ha : IsMonotonic a
hb : IsMonotonic b
⊢ IsMonotonic (zip a b)
Tactic:
intro q i
Proof state after:
ι : Type
inst✝ : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
ha : IsMonotonic a
hb : IsMonotonic b
q : { q // (zip a b).valid q = true }
i : Lex (ι × Bool)
⊢ index' (zip a b) ↑q ≤ index' (zip a b) ((zip a b).seek q i)
Theorem: Etch.Verification.Stream.zip_mono
Proof state before:
ι : Type
inst✝ : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
ha : IsMonotonic a
hb : IsMonotonic b
q : { q // (zip a b).valid q = true }
i : Lex (ι × Bool)
⊢ index' (zip a b) ↑q ≤ index' (zip a b) ((zip a b).seek q i)
Tactic:
simp only [zip_index']
Proof state after:
ι : Type
inst✝ : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
ha : IsMonotonic a
hb : IsMonotonic b
q : { q // (zip a b).valid q = true }
i : Lex (ι × Bool)
⊢ 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)
Theorem: Etch.Verification.Stream.zip_mono
Proof state before:
ι : Type
inst✝ : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
ha : IsMonotonic a
hb : IsMonotonic b
q : { q // (zip a b).valid q = true }
i : Lex (ι × Bool)
⊢ 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:
exact max_le_max (ha _ _) (hb _ _)
Proof state after:
no goals
Theorem: Etch.Verification.Stream.zip_strict_mono
Proof 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']
Proof 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)
Theorem: Etch.Verification.Stream.zip_strict_mono
Proof 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
Proof 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)
Theorem: Etch.Verification.Stream.zip_strict_mono
Proof 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
Proof 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)
Theorem: Etch.Verification.Stream.zip_strict_mono
Proof 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]
Proof state after:
no goals
Theorem: Etch.Verification.Stream.zip_eq_zero_of_lt_toOrder
Proof 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 (zip a b) (↑q) i = none
Tactic:
have := (zip_strict_mono a.strictMono b.strictMono).1.eq_empty_of_lt_index (q := q) i (by rwa [index'_val, WithTop.coe_lt_coe])
Proof 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 < (zip a b).index q
this : (evalMultiset (zip a b) ↑q) i = 0
⊢ evalOption (zip a b) (↑q) i = none
Theorem: Etch.Verification.Stream.zip_eq_zero_of_lt_toOrder
Proof 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
this : (evalMultiset (zip a b) ↑q) i = 0
⊢ evalOption (zip a b) (↑q) i = none
Tactic:
rw [Stream.evalOption, this, Multiset.get_zero]
Proof state after:
no goals
Theorem: Etch.Verification.Stream.zip_eq_zero_of_lt_toOrder
Proof 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
⊢ ↑i < index' (zip a b) ↑q
Tactic:
rwa [index'_val, WithTop.coe_lt_coe]
Proof state after:
no goals
Theorem: Etch.Verification.Stream.zip_left_or_right_eq_zero_of_lt_toOrder
Proof 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
Proof 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
Theorem: Etch.Verification.Stream.zip_left_or_right_eq_zero_of_lt_toOrder
Proof 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
Proof 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
Theorem: Etch.Verification.Stream.zip_left_or_right_eq_zero_of_lt_toOrder
Proof 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])
Proof 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
Theorem: Etch.Verification.Stream.zip_left_or_right_eq_zero_of_lt_toOrder
Proof 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]
Proof state after:
no goals
Theorem: Etch.Verification.Stream.zip_left_or_right_eq_zero_of_lt_toOrder
Proof 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]
Proof state after:
no goals
Theorem: Etch.Verification.Stream.zip_left_or_right_eq_zero_of_lt_toOrder
Proof 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])
Proof 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
Theorem: Etch.Verification.Stream.zip_left_or_right_eq_zero_of_lt_toOrder
Proof 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]
Proof state after:
no goals
Theorem: Etch.Verification.Stream.zip_left_or_right_eq_zero_of_lt_toOrder
Proof 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]
Proof state after:
no goals
Theorem: Etch.Verification.Stream.zip_ready_eq
Proof 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 (zip a b) (↑q) ((zip a b).index q) =
    some (a.value (mul.ready.fst { val := q, property := h }), b.value (mul.ready.snd { val := q, property := h }))
Tactic:
rw [(zip_strict_mono a.strictMono b.strictMono).evalOption_ready h]
Proof 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
⊢ some ((zip a b).value { val := q, property := h }) =
    some (a.value (mul.ready.fst { val := q, property := h }), b.value (mul.ready.snd { val := q, property := h }))
Theorem: Etch.Verification.Stream.zip_ready_eq
Proof 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
⊢ some ((zip a b).value { val := q, property := h }) =
    some (a.value (mul.ready.fst { val := q, property := h }), b.value (mul.ready.snd { val := q, property := h }))
Tactic:
rfl
Proof state after:
no goals
Theorem: Etch.Verification.Stream.zip_ready_eq'
Proof 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
Proof 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 }))
Theorem: Etch.Verification.Stream.zip_ready_eq'
Proof 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
Proof 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 }))