internlm/Lean-Github huggingface dataset:
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 < 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]
Proof state after:
no goals
Theorem: Etch.Verification.Stream.mul_mono
Proof state before:
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : NonUnitalNonAssocSemiring α
a b : Stream ι α
ha : IsMonotonic a
hb : IsMonotonic b
⊢ IsMonotonic (mul a b)
Tactic:
intro q i
Proof state after:
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : NonUnitalNonAssocSemiring α
a b : Stream ι α
ha : IsMonotonic a
hb : IsMonotonic b
q : { q // (mul a b).valid q = true }
i : Lex (ι × Bool)
⊢ index' (mul a b) ↑q ≤ index' (mul a b) ((mul a b).seek q i)
Theorem: Etch.Verification.Stream.mul_mono
Proof state before:
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : NonUnitalNonAssocSemiring α
a b : Stream ι α
ha : IsMonotonic a
hb : IsMonotonic b
q : { q // (mul a b).valid q = true }
i : Lex (ι × Bool)
⊢ index' (mul a b) ↑q ≤ index' (mul a b) ((mul a b).seek q i)
Tactic:
simp only [Stream.mul_index']
Proof state after:
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : NonUnitalNonAssocSemiring α
a b : Stream ι α
ha : IsMonotonic a
hb : IsMonotonic b
q : { q // (mul a b).valid q = true }
i : Lex (ι × Bool)
⊢ max (index' a (↑q).1) (index' b (↑q).2) ≤ max (index' a ((mul a b).seek q i).1) (index' b ((mul a b).seek q i).2)
Theorem: Etch.Verification.Stream.mul_mono
Proof state before:
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : NonUnitalNonAssocSemiring α
a b : Stream ι α
ha : IsMonotonic a
hb : IsMonotonic b
q : { q // (mul a b).valid q = true }
i : Lex (ι × Bool)
⊢ max (index' a (↑q).1) (index' b (↑q).2) ≤ max (index' a ((mul a b).seek q i).1) (index' b ((mul a b).seek q i).2)
Tactic:
exact max_le_max (ha _ _) (hb _ _)
Proof state after:
no goals
Theorem: Etch.Verification.Stream.mul_strict_mono
Proof state before:
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : NonUnitalNonAssocSemiring α
a b : Stream ι α
ha : IsStrictMono a
hb : IsStrictMono b
q : { q // (mul a b).valid q = true }
i : StreamOrder ι
H : toOrder (mul a b) q ≤ i
hr : (mul a b).ready q = true
⊢ index' (mul a b) ↑q < index' (mul a b) ((mul a b).seek q i)
Tactic:
simp only [Stream.mul_index']
Proof state after:
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : NonUnitalNonAssocSemiring α
a b : Stream ι α
ha : IsStrictMono a
hb : IsStrictMono b
q : { q // (mul a b).valid q = true }
i : StreamOrder ι
H : toOrder (mul a b) q ≤ i
hr : (mul a b).ready q = true
⊢ max (index' a (↑q).1) (index' b (↑q).2) < max (index' a ((mul a b).seek q i).1) (index' b ((mul a b).seek q i).2)
Theorem: Etch.Verification.Stream.mul_strict_mono
Proof state before:
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : NonUnitalNonAssocSemiring α
a b : Stream ι α
ha : IsStrictMono a
hb : IsStrictMono b
q : { q // (mul a b).valid q = true }
i : StreamOrder ι
H : toOrder (mul a b) q ≤ i
hr : (mul a b).ready q = true
⊢ max (index' a (↑q).1) (index' b (↑q).2) < max (index' a ((mul a b).seek q i).1) (index' b ((mul a b).seek q i).2)
Tactic:
have := order_eq_of_mul_ready hr
Proof state after:
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : NonUnitalNonAssocSemiring α
a b : Stream ι α
ha : IsStrictMono a
hb : IsStrictMono b
q : { q // (mul a b).valid q = true }
i : StreamOrder ι
H : toOrder (mul a b) q ≤ i
hr : (mul a b).ready q = true
this : toOrder a (mul.valid.fst q) = toOrder (mul a b) q ∧ toOrder b (mul.valid.snd q) = toOrder (mul a b) q
⊢ max (index' a (↑q).1) (index' b (↑q).2) < max (index' a ((mul a b).seek q i).1) (index' b ((mul a b).seek q i).2)
Theorem: Etch.Verification.Stream.mul_strict_mono
Proof state before:
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : NonUnitalNonAssocSemiring α
a b : Stream ι α
ha : IsStrictMono a
hb : IsStrictMono b
q : { q // (mul a b).valid q = true }
i : StreamOrder ι
H : toOrder (mul a b) q ≤ i
hr : (mul a b).ready q = true
this : toOrder a (mul.valid.fst q) = toOrder (mul a b) q ∧ toOrder b (mul.valid.snd q) = toOrder (mul a b) q
⊢ max (index' a (↑q).1) (index' b (↑q).2) < max (index' a ((mul a b).seek q i).1) (index' b ((mul a b).seek q i).2)
Tactic:
simp at hr
Proof state after:
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : NonUnitalNonAssocSemiring α
a b : Stream ι α
ha : IsStrictMono a
hb : IsStrictMono b
q : { q // (mul a b).valid q = true }
i : StreamOrder ι
H : toOrder (mul a b) q ≤ i
this : toOrder a (mul.valid.fst q) = toOrder (mul a b) q ∧ toOrder b (mul.valid.snd q) = toOrder (mul 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 ((mul a b).seek q i).1) (index' b ((mul a b).seek q i).2)
Theorem: Etch.Verification.Stream.mul_strict_mono
Proof state before:
ι : Type
inst✝¹ : LinearOrder ι
α : Type u
inst✝ : NonUnitalNonAssocSemiring α
a b : Stream ι α
ha : IsStrictMono a
hb : IsStrictMono b
q : { q // (mul a b).valid q = true }
i : StreamOrder ι
H : toOrder (mul a b) q ≤ i
this : toOrder a (mul.valid.fst q) = toOrder (mul a b) q ∧ toOrder b (mul.valid.snd q) = toOrder (mul 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 ((mul a b).seek q i).1) (index' b ((mul 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.next_eval_mul_eq
Proof state before:
ι : Type
inst✝³ : LinearOrder ι
α : Type u
inst✝² : NonUnitalNonAssocSemiring α
a b : Stream ι α
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
q : { q // (mul a b).valid q = true }
⊢ eval a (advance (mul a b) ↑q).1 * eval b (advance (mul a b) ↑q).2 =
    Finsupp.filter (fun i => toOrder (mul a b) q ≤ (i, false)) (eval a ↑(mul.valid.fst q) * eval b ↑(mul.valid.snd q))
Tactic:
ext j
Proof state after:
case h
ι : Type
inst✝³ : LinearOrder ι
α : Type u
inst✝² : NonUnitalNonAssocSemiring α
a b : Stream ι α
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
q : { q // (mul a b).valid q = true }
j : ι
⊢ (eval a (advance (mul a b) ↑q).1 * eval b (advance (mul a b) ↑q).2) j =
    (Finsupp.filter (fun i => toOrder (mul a b) q ≤ (i, false)) (eval a ↑(mul.valid.fst q) * eval b ↑(mul.valid.snd q)))
      j
Theorem: Etch.Verification.Stream.next_eval_mul_eq
Proof state before:
case h
ι : Type
inst✝³ : LinearOrder ι
α : Type u
inst✝² : NonUnitalNonAssocSemiring α
a b : Stream ι α
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
q : { q // (mul a b).valid q = true }
j : ι
⊢ (eval a (advance (mul a b) ↑q).1 * eval b (advance (mul a b) ↑q).2) j =
    (Finsupp.filter (fun i => toOrder (mul a b) q ≤ (i, false)) (eval a ↑(mul.valid.fst q) * eval b ↑(mul.valid.snd q)))
      j
Tactic:
simp only [Finsupp.mul_apply, Finsupp.filter_apply, Stream.advance_val]
Proof state after:
case h
ι : Type
inst✝³ : LinearOrder ι
α : Type u
inst✝² : NonUnitalNonAssocSemiring α
a b : Stream ι α
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
q : { q // (mul a b).valid q = true }
j : ι
⊢ (eval a ((mul a b).seek q (toOrder (mul a b) q)).1) j * (eval b ((mul a b).seek q (toOrder (mul a b) q)).2) j =
    if toOrder (mul a b) q ≤ (j, false) then (eval a ↑(mul.valid.fst q)) j * (eval b ↑(mul.valid.snd q)) j else 0
Theorem: Etch.Verification.Stream.next_eval_mul_eq
Proof state before:
case h
ι : Type
inst✝³ : LinearOrder ι
α : Type u
inst✝² : NonUnitalNonAssocSemiring α
a b : Stream ι α
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
q : { q // (mul a b).valid q = true }
j : ι
⊢ (eval a ((mul a b).seek q (toOrder (mul a b) q)).1) j * (eval b ((mul a b).seek q (toOrder (mul a b) q)).2) j =
    if toOrder (mul a b) q ≤ (j, false) then (eval a ↑(mul.valid.fst q)) j * (eval b ↑(mul.valid.snd q)) j else 0
Tactic:
split_ifs with hj
Proof state after:
case pos
ι : Type
inst✝³ : LinearOrder ι
α : Type u
inst✝² : NonUnitalNonAssocSemiring α
a b : Stream ι α
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
q : { q // (mul a b).valid q = true }
j : ι
hj : toOrder (mul a b) q ≤ (j, false)
⊢ (eval a ((mul a b).seek q (toOrder (mul a b) q)).1) j * (eval b ((mul a b).seek q (toOrder (mul a b) q)).2) j =
    (eval a ↑(mul.valid.fst q)) j * (eval b ↑(mul.valid.snd q)) j

case neg
ι : Type
inst✝³ : LinearOrder ι
α : Type u
inst✝² : NonUnitalNonAssocSemiring α
a b : Stream ι α
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
q : { q // (mul a b).valid q = true }
j : ι
hj : ¬toOrder (mul a b) q ≤ (j, false)
⊢ (eval a ((mul a b).seek q (toOrder (mul a b) q)).1) j * (eval b ((mul a b).seek q (toOrder (mul a b) q)).2) j = 0
Theorem: Etch.Verification.Stream.next_eval_mul_eq
Proof state before:
case pos
ι : Type
inst✝³ : LinearOrder ι
α : Type u
inst✝² : NonUnitalNonAssocSemiring α
a b : Stream ι α
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
q : { q // (mul a b).valid q = true }
j : ι
hj : toOrder (mul a b) q ≤ (j, false)
⊢ (eval a ((mul a b).seek q (toOrder (mul a b) q)).1) j * (eval b ((mul a b).seek q (toOrder (mul a b) q)).2) j =
    (eval a ↑(mul.valid.fst q)) j * (eval b ↑(mul.valid.snd q)) j
Tactic:
simp only [Stream.toOrder, Stream.index'_val, Stream.mul_seek] at hj ⊢
Proof state after:
case pos
ι : Type
inst✝³ : LinearOrder ι
α : Type u
inst✝² : NonUnitalNonAssocSemiring α
a b : Stream ι α
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
q : { q // (mul a b).valid q = true }
j : ι
hj : ((mul a b).index q, (mul a b).ready q) ≤ (j, false)
⊢ (eval a (a.seek (mul.valid.fst q) ((mul a b).index q, (mul a b).ready q))) j *
      (eval b (b.seek (mul.valid.snd q) ((mul a b).index q, (mul a b).ready q))) j =
    (eval a ↑(mul.valid.fst q)) j * (eval b ↑(mul.valid.snd q)) j
Theorem: Etch.Verification.Stream.next_eval_mul_eq
Proof state before:
case neg
ι : Type
inst✝³ : LinearOrder ι
α : Type u
inst✝² : NonUnitalNonAssocSemiring α
a b : Stream ι α
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
q : { q // (mul a b).valid q = true }
j : ι
hj : ¬toOrder (mul a b) q ≤ (j, false)
⊢ (eval a ((mul a b).seek q (toOrder (mul a b) q)).1) j * (eval b ((mul a b).seek q (toOrder (mul a b) q)).2) j = 0
Tactic:
dsimp only [mul_seek]
Proof state after:
case neg
ι : Type
inst✝³ : LinearOrder ι
α : Type u
inst✝² : NonUnitalNonAssocSemiring α
a b : Stream ι α
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
q : { q // (mul a b).valid q = true }
j : ι
hj : ¬toOrder (mul a b) q ≤ (j, false)
⊢ (eval a (a.seek (mul.valid.fst q) (toOrder (mul a b) q))) j *
      (eval b (b.seek (mul.valid.snd q) (toOrder (mul a b) q))) j =
    0
Theorem: Etch.Verification.Stream.next_eval_mul_eq
Proof state before:
case neg
ι : Type
inst✝³ : LinearOrder ι
α : Type u
inst✝² : NonUnitalNonAssocSemiring α
a b : Stream ι α
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
q : { q // (mul a b).valid q = true }
j : ι
hj : ¬toOrder (mul a b) q ≤ (j, false)
⊢ (eval a (a.seek (mul.valid.fst q) (toOrder (mul a b) q))) j *
      (eval b (b.seek (mul.valid.snd q) (toOrder (mul a b) q))) j =
    0
Tactic:
rw [not_le] at hj
Proof state after:
case neg
ι : Type
inst✝³ : LinearOrder ι
α : Type u
inst✝² : NonUnitalNonAssocSemiring α
a b : Stream ι α
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
q : { q // (mul a b).valid q = true }
j : ι
hj : (j, false) < toOrder (mul a b) q
⊢ (eval a (a.seek (mul.valid.fst q) (toOrder (mul a b) q))) j *
      (eval b (b.seek (mul.valid.snd q) (toOrder (mul a b) q))) j =
    0
Theorem: Etch.Verification.Stream.next_eval_mul_eq
Proof state before:
case neg
ι : Type
inst✝³ : LinearOrder ι
α : Type u
inst✝² : NonUnitalNonAssocSemiring α
a b : Stream ι α
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
q : { q // (mul a b).valid q = true }
j : ι
hj : (j, false) < toOrder (mul a b) q
⊢ (eval a (a.seek (mul.valid.fst q) (toOrder (mul a b) q))) j *
      (eval b (b.seek (mul.valid.snd q) (toOrder (mul a b) q))) j =
    0
Tactic:
rcases le_max_iff.mp <| toOrder_le_max a b q with hj' | hj'
Proof state after:
case neg.inl
ι : Type
inst✝³ : LinearOrder ι
α : Type u
inst✝² : NonUnitalNonAssocSemiring α
a b : Stream ι α
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
q : { q // (mul a b).valid q = true }
j : ι
hj : (j, false) < toOrder (mul a b) q
hj' : toOrder (mul a b) q ≤ toOrder a (mul.valid.fst q)
⊢ (eval a (a.seek (mul.valid.fst q) (toOrder (mul a b) q))) j *
      (eval b (b.seek (mul.valid.snd q) (toOrder (mul a b) q))) j =
    0

case neg.inr
ι : Type
inst✝³ : LinearOrder ι
α : Type u
inst✝² : NonUnitalNonAssocSemiring α
a b : Stream ι α
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
q : { q // (mul a b).valid q = true }
j : ι
hj : (j, false) < toOrder (mul a b) q
hj' : toOrder (mul a b) q ≤ toOrder b (mul.valid.snd q)
⊢ (eval a (a.seek (mul.valid.fst q) (toOrder (mul a b) q))) j *
      (eval b (b.seek (mul.valid.snd q) (toOrder (mul a b) q))) j =
    0
Theorem: Etch.Verification.Stream.next_eval_mul_eq
Proof state before:
case neg.inl
ι : Type
inst✝³ : LinearOrder ι
α : Type u
inst✝² : NonUnitalNonAssocSemiring α
a b : Stream ι α
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
q : { q // (mul a b).valid q = true }
j : ι
hj : (j, false) < toOrder (mul a b) q
hj' : toOrder (mul a b) q ≤ toOrder a (mul.valid.fst q)
⊢ (eval a (a.seek (mul.valid.fst q) (toOrder (mul a b) q))) j *
      (eval b (b.seek (mul.valid.snd q) (toOrder (mul a b) q))) j =
    0
Tactic:
rw [a.strictMono.eval_seek_eq_zero, MulZeroClass.zero_mul] <;> assumption
Proof state after:
no goals
Theorem: Etch.Verification.Stream.next_eval_mul_eq
Proof state before:
case neg.inr
ι : Type
inst✝³ : LinearOrder ι
α : Type u
inst✝² : NonUnitalNonAssocSemiring α
a b : Stream ι α
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
q : { q // (mul a b).valid q = true }
j : ι
hj : (j, false) < toOrder (mul a b) q
hj' : toOrder (mul a b) q ≤ toOrder b (mul.valid.snd q)
⊢ (eval a (a.seek (mul.valid.fst q) (toOrder (mul a b) q))) j *
      (eval b (b.seek (mul.valid.snd q) (toOrder (mul a b) q))) j =
    0
Tactic:
rw [b.strictMono.eval_seek_eq_zero, MulZeroClass.mul_zero] <;> assumption
Proof state after:
no goals
Theorem: Etch.Verification.Stream.mul_spec
Proof state before:
ι : Type
inst✝³ : LinearOrder ι
α : Type u
inst✝² : NonUnitalNonAssocSemiring α
a b : Stream ι α
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
q : (mul a b).σ
⊢ eval (mul a b) q = eval a q.1 * eval b q.2
Tactic:
apply (a.mul b).wf.induction q
Proof state after:
ι : Type
inst✝³ : LinearOrder ι
α : Type u
inst✝² : NonUnitalNonAssocSemiring α
a b : Stream ι α
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
q : (mul a b).σ
⊢ ∀ (x : (mul a b).σ),
    (∀ (y : (mul a b).σ), WfRel (mul a b) y x → eval (mul a b) y = eval a y.1 * eval b y.2) →
      eval (mul a b) x = eval a x.1 * eval b x.2
Theorem: Etch.Verification.Stream.mul_spec
Proof state before:
ι : Type
inst✝³ : LinearOrder ι
α : Type u
inst✝² : NonUnitalNonAssocSemiring α
a b : Stream ι α
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
q : (mul a b).σ
⊢ ∀ (x : (mul a b).σ),
    (∀ (y : (mul a b).σ), WfRel (mul a b) y x → eval (mul a b) y = eval a y.1 * eval b y.2) →
      eval (mul a b) x = eval a x.1 * eval b x.2
Tactic:
clear q
Proof state after:
ι : Type
inst✝³ : LinearOrder ι
α : Type u
inst✝² : NonUnitalNonAssocSemiring α
a b : Stream ι α
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
⊢ ∀ (x : (mul a b).σ),
    (∀ (y : (mul a b).σ), WfRel (mul a b) y x → eval (mul a b) y = eval a y.1 * eval b y.2) →
      eval (mul a b) x = eval a x.1 * eval b x.2
Theorem: Etch.Verification.Stream.mul_spec
Proof state before:
ι : Type
inst✝³ : LinearOrder ι
α : Type u
inst✝² : NonUnitalNonAssocSemiring α
a b : Stream ι α
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
⊢ ∀ (x : (mul a b).σ),
    (∀ (y : (mul a b).σ), WfRel (mul a b) y x → eval (mul a b) y = eval a y.1 * eval b y.2) →
      eval (mul a b) x = eval a x.1 * eval b x.2
Tactic:
intro q ih
Proof state after:
ι : Type
inst✝³ : LinearOrder ι
α : Type u
inst✝² : NonUnitalNonAssocSemiring α
a b : Stream ι α
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
q : (mul a b).σ
ih : ∀ (y : (mul a b).σ), WfRel (mul a b) y q → eval (mul a b) y = eval a y.1 * eval b y.2
⊢ eval (mul a b) q = eval a q.1 * eval b q.2
Theorem: Etch.Verification.Stream.mul_spec
Proof state before:
ι : Type
inst✝³ : LinearOrder ι
α : Type u
inst✝² : NonUnitalNonAssocSemiring α
a b : Stream ι α
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
q : (mul a b).σ
ih : ∀ (y : (mul a b).σ), WfRel (mul a b) y q → eval (mul a b) y = eval a y.1 * eval b y.2
⊢ eval (mul a b) q = eval a q.1 * eval b q.2
Tactic:
by_cases hv : (a.mul b).valid q
Proof state after:
case pos
ι : Type
inst✝³ : LinearOrder ι
α : Type u
inst✝² : NonUnitalNonAssocSemiring α
a b : Stream ι α
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
q : (mul a b).σ
ih : ∀ (y : (mul a b).σ), WfRel (mul a b) y q → eval (mul a b) y = eval a y.1 * eval b y.2
hv : (mul a b).valid q = true
⊢ eval (mul a b) q = eval a q.1 * eval b q.2

case neg
ι : Type
inst✝³ : LinearOrder ι
α : Type u
inst✝² : NonUnitalNonAssocSemiring α
a b : Stream ι α
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
q : (mul a b).σ
ih : ∀ (y : (mul a b).σ), WfRel (mul a b) y q → eval (mul a b) y = eval a y.1 * eval b y.2
hv : ¬(mul a b).valid q = true
⊢ eval (mul a b) q = eval a q.1 * eval b q.2
Theorem: Etch.Verification.Stream.mul_spec
Proof state before:
case pos
ι : Type
inst✝³ : LinearOrder ι
α : Type u
inst✝² : NonUnitalNonAssocSemiring α
a b : Stream ι α
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
q : (mul a b).σ
ih : ∀ (y : (mul a b).σ), WfRel (mul a b) y q → eval (mul a b) y = eval a y.1 * eval b y.2
hv : (mul a b).valid q = true
⊢ eval (mul a b) q = eval a q.1 * eval b q.2

case neg
ι : Type
inst✝³ : LinearOrder ι
α : Type u
inst✝² : NonUnitalNonAssocSemiring α
a b : Stream ι α
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
q : (mul a b).σ
ih : ∀ (y : (mul a b).σ), WfRel (mul a b) y q → eval (mul a b) y = eval a y.1 * eval b y.2
hv : ¬(mul a b).valid q = true
⊢ eval (mul a b) q = eval a q.1 * eval b q.2
Tactic:
swap
Proof state after:
case neg
ι : Type
inst✝³ : LinearOrder ι
α : Type u
inst✝² : NonUnitalNonAssocSemiring α
a b : Stream ι α
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
q : (mul a b).σ
ih : ∀ (y : (mul a b).σ), WfRel (mul a b) y q → eval (mul a b) y = eval a y.1 * eval b y.2
hv : ¬(mul a b).valid q = true
⊢ eval (mul a b) q = eval a q.1 * eval b q.2

case pos
ι : Type
inst✝³ : LinearOrder ι
α : Type u
inst✝² : NonUnitalNonAssocSemiring α
a b : Stream ι α
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
q : (mul a b).σ
ih : ∀ (y : (mul a b).σ), WfRel (mul a b) y q → eval (mul a b) y = eval a y.1 * eval b y.2
hv : (mul a b).valid q = true
⊢ eval (mul a b) q = eval a q.1 * eval b q.2
Theorem: Etch.Verification.Stream.mul_spec
Proof state before:
case neg
ι : Type
inst✝³ : LinearOrder ι
α : Type u
inst✝² : NonUnitalNonAssocSemiring α
a b : Stream ι α
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
q : (mul a b).σ
ih : ∀ (y : (mul a b).σ), WfRel (mul a b) y q → eval (mul a b) y = eval a y.1 * eval b y.2
hv : ¬(mul a b).valid q = true
⊢ eval (mul a b) q = eval a q.1 * eval b q.2
Tactic:
have := hv
Proof state after:
case neg
ι : Type
inst✝³ : LinearOrder ι
α : Type u
inst✝² : NonUnitalNonAssocSemiring α
a b : Stream ι α
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
q : (mul a b).σ
ih : ∀ (y : (mul a b).σ), WfRel (mul a b) y q → eval (mul a b) y = eval a y.1 * eval b y.2
hv this : ¬(mul a b).valid q = true
⊢ eval (mul a b) q = eval a q.1 * eval b q.2
Theorem: Etch.Verification.Stream.mul_spec
Proof state before:
case neg
ι : Type
inst✝³ : LinearOrder ι
α : Type u
inst✝² : NonUnitalNonAssocSemiring α
a b : Stream ι α
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
q : (mul a b).σ
ih : ∀ (y : (mul a b).σ), WfRel (mul a b) y q → eval (mul a b) y = eval a y.1 * eval b y.2
hv this : ¬(mul a b).valid q = true
⊢ eval (mul a b) q = eval a q.1 * eval b q.2
Tactic:
simp only [mul_valid, Bool.and_eq_true, not_and_or, Bool.not_eq_true] at hv
Proof state after:
case neg
ι : Type
inst✝³ : LinearOrder ι
α : Type u
inst✝² : NonUnitalNonAssocSemiring α
a b : Stream ι α
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
q : (mul a b).σ
ih : ∀ (y : (mul a b).σ), WfRel (mul a b) y q → eval (mul a b) y = eval a y.1 * eval b y.2
this : ¬(mul a b).valid q = true
hv : a.valid q.1 = false ∨ b.valid q.2 = false
⊢ eval (mul a b) q = eval a q.1 * eval b q.2
Theorem: Etch.Verification.Stream.mul_spec
Proof state before:
case neg
ι : Type
inst✝³ : LinearOrder ι
α : Type u
inst✝² : NonUnitalNonAssocSemiring α
a b : Stream ι α
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
q : (mul a b).σ
ih : ∀ (y : (mul a b).σ), WfRel (mul a b) y q → eval (mul a b) y = eval a y.1 * eval b y.2
this : ¬(mul a b).valid q = true
hv : a.valid q.1 = false ∨ b.valid q.2 = false
⊢ eval (mul a b) q = eval a q.1 * eval b q.2
Tactic:
rcases hv with hv' | hv' <;> simp [this, hv']
Proof state after:
no goals
Theorem: Etch.Verification.Stream.mul_spec
Proof state before:
case pos
ι : Type
inst✝³ : LinearOrder ι
α : Type u
inst✝² : NonUnitalNonAssocSemiring α
a b : Stream ι α
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
q : (mul a b).σ
ih : ∀ (y : (mul a b).σ), WfRel (mul a b) y q → eval (mul a b) y = eval a y.1 * eval b y.2
hv : (mul a b).valid q = true
⊢ eval (mul a b) q = eval a q.1 * eval b q.2
Tactic:
rw [Stream.eval_valid _ ⟨_, hv⟩, ih _ ((a.mul b).next_wf ⟨q, hv⟩), next_eval_mul_eq _ _ ⟨_, hv⟩,
  mul_eval₀_spec _ _ a.strictMono b.strictMono ⟨_, hv⟩]
Proof state after:
case pos
ι : Type
inst✝³ : LinearOrder ι
α : Type u
inst✝² : NonUnitalNonAssocSemiring α
a b : Stream ι α
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
q : (mul a b).σ
ih : ∀ (y : (mul a b).σ), WfRel (mul a b) y q → eval (mul a b) y = eval a y.1 * eval b y.2
hv : (mul a b).valid q = true
⊢ Finsupp.filter (fun i => (i, false) < toOrder (mul a b) { val := q, property := hv })
        (eval a ↑(mul.valid.fst { val := q, property := hv }) * eval b ↑(mul.valid.snd { val := q, property := hv })) +
      Finsupp.filter (fun i => toOrder (mul a b) { val := q, property := hv } ≤ (i, false))
        (eval a ↑(mul.valid.fst { val := q, property := hv }) * eval b ↑(mul.valid.snd { val := q, property := hv })) =
    eval a q.1 * eval b q.2
Theorem: Etch.Verification.Stream.mul_spec
Proof state before:
case pos
ι : Type
inst✝³ : LinearOrder ι
α : Type u
inst✝² : NonUnitalNonAssocSemiring α
a b : Stream ι α
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
q : (mul a b).σ
ih : ∀ (y : (mul a b).σ), WfRel (mul a b) y q → eval (mul a b) y = eval a y.1 * eval b y.2
hv : (mul a b).valid q = true
⊢ Finsupp.filter (fun i => (i, false) < toOrder (mul a b) { val := q, property := hv })
        (eval a ↑(mul.valid.fst { val := q, property := hv }) * eval b ↑(mul.valid.snd { val := q, property := hv })) +
      Finsupp.filter (fun i => toOrder (mul a b) { val := q, property := hv } ≤ (i, false))
        (eval a ↑(mul.valid.fst { val := q, property := hv }) * eval b ↑(mul.valid.snd { val := q, property := hv })) =
    eval a q.1 * eval b q.2
Tactic:
convert Finsupp.filter_pos_add_filter_neg (α := ι) (M := α) ..
Proof state after:
case h.e'_2.h.e'_6.h.e'_4.h.a
ι : Type
inst✝³ : LinearOrder ι
α : Type u
inst✝² : NonUnitalNonAssocSemiring α
a b : Stream ι α
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
q : (mul a b).σ
ih : ∀ (y : (mul a b).σ), WfRel (mul a b) y q → eval (mul a b) y = eval a y.1 * eval b y.2
hv : (mul a b).valid q = true
x✝ : ι
⊢ toOrder (mul a b) { val := q, property := hv } ≤ (x✝, false) ↔
    ¬(x✝, false) < toOrder (mul a b) { val := q, property := hv }