Theorem: Etch.Verification.Stream.mul_eval₀_spec (Etch/StreamFusion/Proofs/StreamMul.lean)

State before:
ι : Type
inst✝³ : LinearOrder ι
α : Type u
inst✝² : NonUnitalNonAssocSemiring α
a b : Stream ι α
inst✝¹ : IsBounded a
inst✝ : IsBounded b
ha : IsStrictMono a
hb : IsStrictMono b
q : { q // (mul a b).valid q = true }
⊢ eval₀ (mul a b) q =
    Finsupp.filter (fun i => (i, false) < toOrder (mul a b) q) (eval a ↑(mul.valid.fst q) * eval b ↑(mul.valid.snd q))
Tactic:
by_cases H : (a.mul b).ready q
State after:
case pos
ι : Type
inst✝³ : LinearOrder ι
α : Type u
inst✝² : NonUnitalNonAssocSemiring α
a b : Stream ι α
inst✝¹ : IsBounded a
inst✝ : IsBounded b
ha : IsStrictMono a
hb : IsStrictMono b
q : { q // (mul a b).valid q = true }
H : (mul a b).ready q = true
⊢ eval₀ (mul a b) q =
    Finsupp.filter (fun i => (i, false) < toOrder (mul a b) q) (eval a ↑(mul.valid.fst q) * eval b ↑(mul.valid.snd q))

case neg
ι : Type
inst✝³ : LinearOrder ι
α : Type u
inst✝² : NonUnitalNonAssocSemiring α
a b : Stream ι α
inst✝¹ : IsBounded a
inst✝ : IsBounded b
ha : IsStrictMono a
hb : IsStrictMono b
q : { q // (mul a b).valid q = true }
H : ¬(mul a b).ready q = true
⊢ eval₀ (mul a b) q =
    Finsupp.filter (fun i => (i, false) < toOrder (mul a b) q) (eval a ↑(mul.valid.fst q) * eval b ↑(mul.valid.snd q))

State before:
case pos
ι : Type
inst✝³ : LinearOrder ι
α : Type u
inst✝² : NonUnitalNonAssocSemiring α
a b : Stream ι α
inst✝¹ : IsBounded a
inst✝ : IsBounded b
ha : IsStrictMono a
hb : IsStrictMono b
q : { q // (mul a b).valid q = true }
H : (mul a b).ready q = true
⊢ eval₀ (mul a b) q =
    Finsupp.filter (fun i => (i, false) < toOrder (mul a b) q) (eval a ↑(mul.valid.fst q) * eval b ↑(mul.valid.snd q))
Tactic:
calc
  (a.mul b).eval₀ q = a.eval₀ (mul.valid.fst q) * b.eval₀ (mul.valid.snd q) := mul_eval₀ ..
  _ = ((a.eval <| mul.valid.fst q).filter fun i => (i, false) <ₗ a.toOrder (mul.valid.fst q)) *
        ((b.eval <| mul.valid.snd q).filter fun i => (i, false) <ₗ b.toOrder (mul.valid.snd q)) :=
    by rw [ha.eval₀_eq_eval_filter, hb.eval₀_eq_eval_filter]
  _ = (a.eval (mul.valid.fst q) * b.eval (mul.valid.snd q)).filter fun i =>
        (i, false) <ₗ min (a.toOrder (mul.valid.fst q)) (b.toOrder (mul.valid.snd q)) :=
    by simp only [Finsupp.mul_filter, lt_min_iff]
  _ = (a.eval (mul.valid.fst q) * b.eval (mul.valid.snd q)).filter fun i => (i, false) <ₗ (a.mul b).toOrder q :=
    by simp [order_eq_of_mul_ready H]
State after:
no goals

State before:
ι : Type
inst✝³ : LinearOrder ι
α : Type u
inst✝² : NonUnitalNonAssocSemiring α
a b : Stream ι α
inst✝¹ : IsBounded a
inst✝ : IsBounded b
ha : IsStrictMono a
hb : IsStrictMono b
q : { q // (mul a b).valid q = true }
H : (mul a b).ready q = true
⊢ eval₀ a (mul.valid.fst q) * eval₀ b (mul.valid.snd q) =
    Finsupp.filter (fun i => (i, false) < toOrder a (mul.valid.fst q)) (eval a ↑(mul.valid.fst q)) *
      Finsupp.filter (fun i => (i, false) < toOrder b (mul.valid.snd q)) (eval b ↑(mul.valid.snd q))
Tactic:
rw [ha.eval₀_eq_eval_filter, hb.eval₀_eq_eval_filter]
State after:
no goals

State before:
ι : Type
inst✝³ : LinearOrder ι
α : Type u
inst✝² : NonUnitalNonAssocSemiring α
a b : Stream ι α
inst✝¹ : IsBounded a
inst✝ : IsBounded b
ha : IsStrictMono a
hb : IsStrictMono b
q : { q // (mul a b).valid q = true }
H : (mul a b).ready q = true
⊢ Finsupp.filter (fun i => (i, false) < toOrder a (mul.valid.fst q)) (eval a ↑(mul.valid.fst q)) *
      Finsupp.filter (fun i => (i, false) < toOrder b (mul.valid.snd q)) (eval b ↑(mul.valid.snd q)) =
    Finsupp.filter (fun i => (i, false) < min (toOrder a (mul.valid.fst q)) (toOrder b (mul.valid.snd q)))
      (eval a ↑(mul.valid.fst q) * eval b ↑(mul.valid.snd q))
Tactic:
simp only [Finsupp.mul_filter, lt_min_iff]
State after:
no goals

State before:
ι : Type
inst✝³ : LinearOrder ι
α : Type u
inst✝² : NonUnitalNonAssocSemiring α
a b : Stream ι α
inst✝¹ : IsBounded a
inst✝ : IsBounded b
ha : IsStrictMono a
hb : IsStrictMono b
q : { q // (mul a b).valid q = true }
H : (mul a b).ready q = true
⊢ Finsupp.filter (fun i => (i, false) < min (toOrder a (mul.valid.fst q)) (toOrder b (mul.valid.snd q)))
      (eval a ↑(mul.valid.fst q) * eval b ↑(mul.valid.snd q)) =
    Finsupp.filter (fun i => (i, false) < toOrder (mul a b) q) (eval a ↑(mul.valid.fst q) * eval b ↑(mul.valid.snd q))
Tactic:
simp [order_eq_of_mul_ready H]
State after:
no goals

State before:
case neg
ι : Type
inst✝³ : LinearOrder ι
α : Type u
inst✝² : NonUnitalNonAssocSemiring α
a b : Stream ι α
inst✝¹ : IsBounded a
inst✝ : IsBounded b
ha : IsStrictMono a
hb : IsStrictMono b
q : { q // (mul a b).valid q = true }
H : ¬(mul a b).ready q = true
⊢ eval₀ (mul a b) q =
    Finsupp.filter (fun i => (i, false) < toOrder (mul a b) q) (eval a ↑(mul.valid.fst q) * eval b ↑(mul.valid.snd q))
Tactic:
symm
State after:
case neg
ι : Type
inst✝³ : LinearOrder ι
α : Type u
inst✝² : NonUnitalNonAssocSemiring α
a b : Stream ι α
inst✝¹ : IsBounded a
inst✝ : IsBounded b
ha : IsStrictMono a
hb : IsStrictMono b
q : { q // (mul a b).valid q = true }
H : ¬(mul a b).ready q = true
⊢ Finsupp.filter (fun i => (i, false) < toOrder (mul a b) q) (eval a ↑(mul.valid.fst q) * eval b ↑(mul.valid.snd q)) =
    eval₀ (mul a b) q

State before:
case neg
ι : Type
inst✝³ : LinearOrder ι
α : Type u
inst✝² : NonUnitalNonAssocSemiring α
a b : Stream ι α
inst✝¹ : IsBounded a
inst✝ : IsBounded b
ha : IsStrictMono a
hb : IsStrictMono b
q : { q // (mul a b).valid q = true }
H : ¬(mul a b).ready q = true
⊢ Finsupp.filter (fun i => (i, false) < toOrder (mul a b) q) (eval a ↑(mul.valid.fst q) * eval b ↑(mul.valid.snd q)) =
    eval₀ (mul a b) q
Tactic:
simp only [Stream.eval₀, H, dite_false, coe_mul_valid_fst,
  mul.valid, coe_mul_valid_snd, Finsupp.filter_eq_zero_iff]
State after:
case neg
ι : Type
inst✝³ : LinearOrder ι
α : Type u
inst✝² : NonUnitalNonAssocSemiring α
a b : Stream ι α
inst✝¹ : IsBounded a
inst✝ : IsBounded b
ha : IsStrictMono a
hb : IsStrictMono b
q : { q // (mul a b).valid q = true }
H : ¬(mul a b).ready q = true
⊢ ∀ (x : ι), (x, false) < toOrder (mul a b) q → (eval a (↑q).1 * eval b (↑q).2) x = 0

State before:
case neg
ι : Type
inst✝³ : LinearOrder ι
α : Type u
inst✝² : NonUnitalNonAssocSemiring α
a b : Stream ι α
inst✝¹ : IsBounded a
inst✝ : IsBounded b
ha : IsStrictMono a
hb : IsStrictMono b
q : { q // (mul a b).valid q = true }
H : ¬(mul a b).ready q = true
⊢ ∀ (x : ι), (x, false) < toOrder (mul a b) q → (eval a (↑q).1 * eval b (↑q).2) x = 0
Tactic:
intro i hi
State after:
case neg
ι : Type
inst✝³ : LinearOrder ι
α : Type u
inst✝² : NonUnitalNonAssocSemiring α
a b : Stream ι α
inst✝¹ : IsBounded a
inst✝ : IsBounded b
ha : IsStrictMono a
hb : IsStrictMono b
q : { q // (mul a b).valid q = true }
H : ¬(mul a b).ready q = true
i : ι
hi : (i, false) < toOrder (mul a b) q
⊢ (eval a (↑q).1 * eval b (↑q).2) i = 0

State before:
case neg
ι : Type
inst✝³ : LinearOrder ι
α : Type u
inst✝² : NonUnitalNonAssocSemiring α
a b : Stream ι α
inst✝¹ : IsBounded a
inst✝ : IsBounded b
ha : IsStrictMono a
hb : IsStrictMono b
q : { q // (mul a b).valid q = true }
H : ¬(mul a b).ready q = true
i : ι
hi : (i, false) < toOrder (mul a b) q
⊢ (eval a (↑q).1 * eval b (↑q).2) i = 0
Tactic:
simp only [Stream.toOrder, H, mul_index, Prod.Lex.mk_snd_mono_lt_iff, lt_max_iff] at hi
State after:
case neg
ι : Type
inst✝³ : LinearOrder ι
α : Type u
inst✝² : NonUnitalNonAssocSemiring α
a b : Stream ι α
inst✝¹ : IsBounded a
inst✝ : IsBounded b
ha : IsStrictMono a
hb : IsStrictMono b
q : { q // (mul a b).valid q = true }
H : ¬(mul a b).ready q = true
i : ι
hi : i < a.index (mul.valid.fst q) ∨ i < b.index (mul.valid.snd q)
⊢ (eval a (↑q).1 * eval b (↑q).2) i = 0

State before:
case neg
ι : Type
inst✝³ : LinearOrder ι
α : Type u
inst✝² : NonUnitalNonAssocSemiring α
a b : Stream ι α
inst✝¹ : IsBounded a
inst✝ : IsBounded b
ha : IsStrictMono a
hb : IsStrictMono b
q : { q // (mul a b).valid q = true }
H : ¬(mul a b).ready q = true
i : ι
hi : i < a.index (mul.valid.fst q) ∨ i < b.index (mul.valid.snd q)
⊢ (eval a (↑q).1 * eval b (↑q).2) i = 0
Tactic:
refine
    mul_eq_zero_of
      (hi.imp (fun h => ha.1.eq_zero_of_lt_index i ?_) fun h =>
        hb.1.eq_zero_of_lt_index i ?_) <;>
  rwa [Stream.index'_val', WithTop.coe_lt_coe]
State after:
no goals