internlm/Lean-Github huggingface dataset:
Theorem: Etch.Verification.Stream.mul_map
Proof state before:
ι : Type
inst✝³ : LinearOrder ι
α : Type u
inst✝² : Mul α
β : Type u_1
inst✝¹ : Mul α
inst✝ : Mul β
a b : Stream ι α
f : α → β
hf : ∀ (x y : α), f (x * y) = f x * f y
⊢ map f (mul a b) = mul (map f a) (map f b)
Tactic:
ext <;> try rfl
Proof state after:
case value
ι : Type
inst✝³ : LinearOrder ι
α : Type u
inst✝² : Mul α
β : Type u_1
inst✝¹ : Mul α
inst✝ : Mul β
a b : Stream ι α
f : α → β
hf : ∀ (x y : α), f (x * y) = f x * f y
⊢ HEq (map f (mul a b)).value (mul (map f a) (map f b)).value
Theorem: Etch.Verification.Stream.mul_map
Proof state before:
case value
ι : Type
inst✝³ : LinearOrder ι
α : Type u
inst✝² : Mul α
β : Type u_1
inst✝¹ : Mul α
inst✝ : Mul β
a b : Stream ι α
f : α → β
hf : ∀ (x y : α), f (x * y) = f x * f y
⊢ HEq (map f (mul a b)).value (mul (map f a) (map f b)).value
Tactic:
simp only [heq_iff_eq]
Proof state after:
case value
ι : Type
inst✝³ : LinearOrder ι
α : Type u
inst✝² : Mul α
β : Type u_1
inst✝¹ : Mul α
inst✝ : Mul β
a b : Stream ι α
f : α → β
hf : ∀ (x y : α), f (x * y) = f x * f y
⊢ (map f (mul a b)).value = (mul (map f a) (map f b)).value
Theorem: Etch.Verification.Stream.mul_map
Proof state before:
case value
ι : Type
inst✝³ : LinearOrder ι
α : Type u
inst✝² : Mul α
β : Type u_1
inst✝¹ : Mul α
inst✝ : Mul β
a b : Stream ι α
f : α → β
hf : ∀ (x y : α), f (x * y) = f x * f y
⊢ (map f (mul a b)).value = (mul (map f a) (map f b)).value
Tactic:
ext q₁
Proof state after:
case value.h
ι : Type
inst✝³ : LinearOrder ι
α : Type u
inst✝² : Mul α
β : Type u_1
inst✝¹ : Mul α
inst✝ : Mul β
a b : Stream ι α
f : α → β
hf : ∀ (x y : α), f (x * y) = f x * f y
q₁ : { x // (map f (mul a b)).ready x = true }
⊢ (map f (mul a b)).value q₁ = (mul (map f a) (map f b)).value q₁
Theorem: Etch.Verification.Stream.mul_map
Proof state before:
case value.h
ι : Type
inst✝³ : LinearOrder ι
α : Type u
inst✝² : Mul α
β : Type u_1
inst✝¹ : Mul α
inst✝ : Mul β
a b : Stream ι α
f : α → β
hf : ∀ (x y : α), f (x * y) = f x * f y
q₁ : { x // (map f (mul a b)).ready x = true }
⊢ (map f (mul a b)).value q₁ = (mul (map f a) (map f b)).value q₁
Tactic:
simp [map, hf]
Proof state after:
case value.h
ι : Type
inst✝³ : LinearOrder ι
α : Type u
inst✝² : Mul α
β : Type u_1
inst✝¹ : Mul α
inst✝ : Mul β
a b : Stream ι α
f : α → β
hf : ∀ (x y : α), f (x * y) = f x * f y
q₁ : { x // (map f (mul a b)).ready x = true }
⊢ f (a.value (mul.ready.fst q₁)) * f (b.value (mul.ready.snd q₁)) =
    f (a.value (mul.ready.fst q₁)) * f (b.value (mul.ready.snd q₁))
Theorem: Etch.Verification.Stream.mul_map
Proof state before:
case value.h
ι : Type
inst✝³ : LinearOrder ι
α : Type u
inst✝² : Mul α
β : Type u_1
inst✝¹ : Mul α
inst✝ : Mul β
a b : Stream ι α
f : α → β
hf : ∀ (x y : α), f (x * y) = f x * f y
q₁ : { x // (map f (mul a b)).ready x = true }
⊢ f (a.value (mul.ready.fst q₁)) * f (b.value (mul.ready.snd q₁)) =
    f (a.value (mul.ready.fst q₁)) * f (b.value (mul.ready.snd q₁))
Tactic:
rfl
Proof state after:
no goals
Theorem: Etch.Verification.Stream.mul_map
Proof state before:
case ready
ι : Type
inst✝³ : LinearOrder ι
α : Type u
inst✝² : Mul α
β : Type u_1
inst✝¹ : Mul α
inst✝ : Mul β
a b : Stream ι α
f : α → β
hf : ∀ (x y : α), f (x * y) = f x * f y
⊢ HEq (map f (mul a b)).ready (mul (map f a) (map f b)).ready
Tactic:
rfl
Proof state after:
no goals
Theorem: Etch.Verification.Stream.mul_eval₀_of_neq
Proof state before:
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : NonUnitalNonAssocSemiring α
a b : Stream ι α
q : { p // mul.valid a b p = true }
h : toOrder a (mul.valid.fst q) ≠ toOrder b (mul.valid.snd q)
⊢ eval₀ (mul a b) q = 0
Tactic:
contrapose! h
Proof state after:
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : NonUnitalNonAssocSemiring α
a b : Stream ι α
q : { p // mul.valid a b p = true }
h : eval₀ (mul a b) q ≠ 0
⊢ toOrder a (mul.valid.fst q) = toOrder b (mul.valid.snd q)
Theorem: Etch.Verification.Stream.mul_eval₀_of_neq
Proof state before:
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : NonUnitalNonAssocSemiring α
a b : Stream ι α
q : { p // mul.valid a b p = true }
h : eval₀ (mul a b) q ≠ 0
⊢ toOrder a (mul.valid.fst q) = toOrder b (mul.valid.snd q)
Tactic:
apply Stream.mul.ready.order_eq
Proof state after:
case h
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : NonUnitalNonAssocSemiring α
a b : Stream ι α
q : { p // mul.valid a b p = true }
h : eval₀ (mul a b) q ≠ 0
⊢ mul.ready a b q = true
Theorem: Etch.Verification.Stream.mul_eval₀_of_neq
Proof state before:
case h
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : NonUnitalNonAssocSemiring α
a b : Stream ι α
q : { p // mul.valid a b p = true }
h : eval₀ (mul a b) q ≠ 0
⊢ mul.ready a b q = true
Tactic:
simp only [Stream.eval₀, Stream.mul_ready, Stream.mul_index, ge_iff_le, Stream.mul_value, ne_eq, dite_eq_right_iff,
  Finsupp.single_eq_zero, not_forall] at h
Proof state after:
case h
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : NonUnitalNonAssocSemiring α
a b : Stream ι α
q : { p // mul.valid a b p = true }
h :
  ∃ (x :
    (a.ready (mul.valid.fst q) && b.ready (mul.valid.snd q) &&
        decide (a.index (mul.valid.fst q) = b.index (mul.valid.snd q))) =
      true),
    ¬a.value (mul.ready.fst { val := q, property := ⋯ }) * b.value (mul.ready.snd { val := q, property := ⋯ }) = 0
⊢ mul.ready a b q = true
Theorem: Etch.Verification.Stream.mul_eval₀_of_neq
Proof state before:
case h
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : NonUnitalNonAssocSemiring α
a b : Stream ι α
q : { p // mul.valid a b p = true }
h :
  ∃ (x :
    (a.ready (mul.valid.fst q) && b.ready (mul.valid.snd q) &&
        decide (a.index (mul.valid.fst q) = b.index (mul.valid.snd q))) =
      true),
    ¬a.value (mul.ready.fst { val := q, property := ⋯ }) * b.value (mul.ready.snd { val := q, property := ⋯ }) = 0
⊢ mul.ready a b q = true
Tactic:
exact h.fst
Proof state after:
no goals
Theorem: Etch.Verification.Stream.mul_eval₀
Proof 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₀]
Proof 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)
Theorem: Etch.Verification.Stream.mul_eval₀
Proof 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
Proof 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)
Theorem: Etch.Verification.Stream.mul_eval₀
Proof 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
Proof 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)
Theorem: Etch.Verification.Stream.mul_eval₀
Proof 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₃⟩
Proof 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)
Theorem: Etch.Verification.Stream.mul_eval₀
Proof 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₃]
Proof 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 := ⋯ }
Theorem: Etch.Verification.Stream.mul_eval₀
Proof 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
Proof state after:
no goals
Theorem: Etch.Verification.Stream.mul_eval₀
Proof 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₀]
Proof 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
Theorem: Etch.Verification.Stream.mul_eval₀
Proof 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
Proof 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₂ }
Theorem: Etch.Verification.Stream.mul_eval₀
Proof 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
Proof 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₂ }
Theorem: Etch.Verification.Stream.mul_eval₀
Proof 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]
Proof 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)
Theorem: Etch.Verification.Stream.mul_eval₀
Proof 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
Proof state after:
no goals
Theorem: Etch.Verification.Stream.mul_eval₀
Proof 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
Proof state after:
no goals
Theorem: Etch.Verification.Stream.mul_eval₀_spec
Proof 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
Proof 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))
Theorem: Etch.Verification.Stream.mul_eval₀_spec
Proof 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]
Proof state after:
no goals
Theorem: Etch.Verification.Stream.mul_eval₀_spec
Proof 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]
Proof state after:
no goals
Theorem: Etch.Verification.Stream.mul_eval₀_spec
Proof 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]
Proof state after:
no goals
Theorem: Etch.Verification.Stream.mul_eval₀_spec
Proof 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]
Proof state after:
no goals
Theorem: Etch.Verification.Stream.mul_eval₀_spec
Proof 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
Proof 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
Theorem: Etch.Verification.Stream.mul_eval₀_spec
Proof 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]
Proof 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
Theorem: Etch.Verification.Stream.mul_eval₀_spec
Proof 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
Proof 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
Theorem: Etch.Verification.Stream.mul_eval₀_spec
Proof 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
Proof 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