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

State before:
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : NonUnitalNonAssocSemiring α
a b : Stream ι α
q : { q // (mul a b).valid q = true }
⊢ eval₀ (mul a b) q = eval₀ a (mul.valid.fst q) * eval₀ b (mul.valid.snd q)
Tactic:
rw [Stream.eval₀]
State after:
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : NonUnitalNonAssocSemiring α
a b : Stream ι α
q : { q // (mul a b).valid q = true }
⊢ (if h₂ : (mul a b).ready q = true then fun₀ | (mul a b).index q => (mul a b).value { val := q, property := h₂ }
    else 0) =
    eval₀ a (mul.valid.fst q) * eval₀ b (mul.valid.snd q)

State before:
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : NonUnitalNonAssocSemiring α
a b : Stream ι α
q : { q // (mul a b).valid q = true }
⊢ (if h₂ : (mul a b).ready q = true then fun₀ | (mul a b).index q => (mul a b).value { val := q, property := h₂ }
    else 0) =
    eval₀ a (mul.valid.fst q) * eval₀ b (mul.valid.snd q)
Tactic:
split_ifs with hr
State after:
case pos
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : NonUnitalNonAssocSemiring α
a b : Stream ι α
q : { q // (mul a b).valid q = true }
hr : (mul a b).ready q = true
⊢ (fun₀ | (mul a b).index q => (mul a b).value { val := q, property := hr }) =
    eval₀ a (mul.valid.fst q) * eval₀ b (mul.valid.snd q)

case neg
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : NonUnitalNonAssocSemiring α
a b : Stream ι α
q : { q // (mul a b).valid q = true }
hr : ¬(mul a b).ready q = true
⊢ 0 = 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 ι α
q : { q // (mul a b).valid q = true }
hr : (mul a b).ready q = true
⊢ (fun₀ | (mul a b).index q => (mul a b).value { val := q, property := hr }) =
    eval₀ a (mul.valid.fst q) * eval₀ b (mul.valid.snd q)
Tactic:
simp only [mul_ready, Bool.and_eq_true, decide_eq_true_eq] at hr
State after:
case pos
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : NonUnitalNonAssocSemiring α
a b : Stream ι α
q : { q // (mul a b).valid q = true }
hr✝ : (mul a b).ready q = true
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)
⊢ (fun₀ | (mul a b).index q => (mul a b).value { val := q, property := hr✝ }) =
    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 ι α
q : { q // (mul a b).valid q = true }
hr✝ : (mul a b).ready q = true
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)
⊢ (fun₀ | (mul a b).index q => (mul a b).value { val := q, property := hr✝ }) =
    eval₀ a (mul.valid.fst q) * eval₀ b (mul.valid.snd q)
Tactic:
rcases hr with ⟨⟨hr₁, hr₂⟩, hr₃⟩
State after:
case pos.intro.intro
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : NonUnitalNonAssocSemiring α
a b : Stream ι α
q : { q // (mul a b).valid q = true }
hr : (mul a b).ready q = true
hr₃ : a.index (mul.valid.fst q) = b.index (mul.valid.snd q)
hr₁ : a.ready (mul.valid.fst q) = true
hr₂ : b.ready (mul.valid.snd q) = true
⊢ (fun₀ | (mul a b).index q => (mul a b).value { val := q, property := hr }) =
    eval₀ a (mul.valid.fst q) * eval₀ b (mul.valid.snd q)

State before:
case pos.intro.intro
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : NonUnitalNonAssocSemiring α
a b : Stream ι α
q : { q // (mul a b).valid q = true }
hr : (mul a b).ready q = true
hr₃ : a.index (mul.valid.fst q) = b.index (mul.valid.snd q)
hr₁ : a.ready (mul.valid.fst q) = true
hr₂ : b.ready (mul.valid.snd q) = true
⊢ (fun₀ | (mul a b).index q => (mul a b).value { val := q, property := hr }) =
    eval₀ a (mul.valid.fst q) * eval₀ b (mul.valid.snd q)
Tactic:
simp [Stream.eval₀, hr₁, hr₂, hr₃]
State after:
case pos.intro.intro
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : NonUnitalNonAssocSemiring α
a b : Stream ι α
q : { q // (mul a b).valid q = true }
hr : (mul a b).ready q = true
hr₃ : a.index (mul.valid.fst q) = b.index (mul.valid.snd q)
hr₁ : a.ready (mul.valid.fst q) = true
hr₂ : b.ready (mul.valid.snd q) = true
⊢ ((fun₀ | b.index (mul.valid.snd q) => a.value (mul.ready.fst { val := q, property := hr })) *
      fun₀ | b.index (mul.valid.snd q) => b.value (mul.ready.snd { val := q, property := hr })) =
    (fun₀ | b.index (mul.valid.snd q) => a.value { val := mul.valid.fst q, property := ⋯ }) *
      fun₀ | b.index (mul.valid.snd q) => b.value { val := mul.valid.snd q, property := ⋯ }

State before:
case pos.intro.intro
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : NonUnitalNonAssocSemiring α
a b : Stream ι α
q : { q // (mul a b).valid q = true }
hr : (mul a b).ready q = true
hr₃ : a.index (mul.valid.fst q) = b.index (mul.valid.snd q)
hr₁ : a.ready (mul.valid.fst q) = true
hr₂ : b.ready (mul.valid.snd q) = true
⊢ ((fun₀ | b.index (mul.valid.snd q) => a.value (mul.ready.fst { val := q, property := hr })) *
      fun₀ | b.index (mul.valid.snd q) => b.value (mul.ready.snd { val := q, property := hr })) =
    (fun₀ | b.index (mul.valid.snd q) => a.value { val := mul.valid.fst q, property := ⋯ }) *
      fun₀ | b.index (mul.valid.snd q) => b.value { val := mul.valid.snd q, property := ⋯ }
Tactic:
rfl
State after:
no goals

State before:
case neg
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : NonUnitalNonAssocSemiring α
a b : Stream ι α
q : { q // (mul a b).valid q = true }
hr : ¬(mul a b).ready q = true
⊢ 0 = eval₀ a (mul.valid.fst q) * eval₀ b (mul.valid.snd q)
Tactic:
simp only [Stream.eval₀]
State after:
case neg
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : NonUnitalNonAssocSemiring α
a b : Stream ι α
q : { q // (mul a b).valid q = true }
hr : ¬(mul a b).ready q = true
⊢ 0 =
    (if h₂ : a.ready (mul.valid.fst q) = true then
        fun₀ | a.index (mul.valid.fst q) => a.value { val := mul.valid.fst q, property := h₂ }
      else 0) *
      if h₂ : b.ready (mul.valid.snd q) = true then
        fun₀ | b.index (mul.valid.snd q) => b.value { val := mul.valid.snd q, property := h₂ }
      else 0

State before:
case neg
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : NonUnitalNonAssocSemiring α
a b : Stream ι α
q : { q // (mul a b).valid q = true }
hr : ¬(mul a b).ready q = true
⊢ 0 =
    (if h₂ : a.ready (mul.valid.fst q) = true then
        fun₀ | a.index (mul.valid.fst q) => a.value { val := mul.valid.fst q, property := h₂ }
      else 0) *
      if h₂ : b.ready (mul.valid.snd q) = true then
        fun₀ | b.index (mul.valid.snd q) => b.value { val := mul.valid.snd q, property := h₂ }
      else 0
Tactic:
split_ifs with h₁ h₂ <;> try simp
State after:
case pos
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : NonUnitalNonAssocSemiring α
a b : Stream ι α
q : { q // (mul a b).valid q = true }
hr : ¬(mul a b).ready q = true
h₁ : a.ready (mul.valid.fst q) = true
h₂ : b.ready (mul.valid.snd q) = true
⊢ 0 =
    (fun₀ | a.index (mul.valid.fst q) => a.value { val := mul.valid.fst q, property := h₁ }) *
      fun₀ | b.index (mul.valid.snd q) => b.value { val := mul.valid.snd q, property := h₂ }

State before:
case pos
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : NonUnitalNonAssocSemiring α
a b : Stream ι α
q : { q // (mul a b).valid q = true }
hr : ¬(mul a b).ready q = true
h₁ : a.ready (mul.valid.fst q) = true
h₂ : b.ready (mul.valid.snd q) = true
⊢ 0 =
    (fun₀ | a.index (mul.valid.fst q) => a.value { val := mul.valid.fst q, property := h₁ }) *
      fun₀ | b.index (mul.valid.snd q) => b.value { val := mul.valid.snd q, property := h₂ }
Tactic:
simp only [mul_ready, h₁, h₂, Bool.and_self, Bool.true_and, decide_eq_true_eq] at hr
State after:
case pos
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : NonUnitalNonAssocSemiring α
a b : Stream ι α
q : { q // (mul a b).valid q = true }
h₁ : a.ready (mul.valid.fst q) = true
h₂ : b.ready (mul.valid.snd q) = true
hr : ¬a.index (mul.valid.fst q) = b.index (mul.valid.snd q)
⊢ 0 =
    (fun₀ | a.index (mul.valid.fst q) => a.value { val := mul.valid.fst q, property := h₁ }) *
      fun₀ | b.index (mul.valid.snd q) => b.value { val := mul.valid.snd q, property := h₂ }

State before:
case pos
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : NonUnitalNonAssocSemiring α
a b : Stream ι α
q : { q // (mul a b).valid q = true }
h₁ : a.ready (mul.valid.fst q) = true
h₂ : b.ready (mul.valid.snd q) = true
hr : ¬a.index (mul.valid.fst q) = b.index (mul.valid.snd q)
⊢ 0 =
    (fun₀ | a.index (mul.valid.fst q) => a.value { val := mul.valid.fst q, property := h₁ }) *
      fun₀ | b.index (mul.valid.snd q) => b.value { val := mul.valid.snd q, property := h₂ }
Tactic:
rw [Finsupp.mul_single_eq_zero]
State after:
case pos.hi
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : NonUnitalNonAssocSemiring α
a b : Stream ι α
q : { q // (mul a b).valid q = true }
h₁ : a.ready (mul.valid.fst q) = true
h₂ : b.ready (mul.valid.snd q) = true
hr : ¬a.index (mul.valid.fst q) = b.index (mul.valid.snd q)
⊢ a.index (mul.valid.fst q) ≠ b.index (mul.valid.snd q)

State before:
case pos.hi
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : NonUnitalNonAssocSemiring α
a b : Stream ι α
q : { q // (mul a b).valid q = true }
h₁ : a.ready (mul.valid.fst q) = true
h₂ : b.ready (mul.valid.snd q) = true
hr : ¬a.index (mul.valid.fst q) = b.index (mul.valid.snd q)
⊢ a.index (mul.valid.fst q) ≠ b.index (mul.valid.snd q)
Tactic:
assumption
State after:
no goals

State before:
case neg
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : NonUnitalNonAssocSemiring α
a b : Stream ι α
q : { q // (mul a b).valid q = true }
hr : ¬(mul a b).ready q = true
h₁ : ¬a.ready (mul.valid.fst q) = true
h✝ : ¬b.ready (mul.valid.snd q) = true
⊢ 0 = 0 * 0
Tactic:
simp
State after:
no goals