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

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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']
State after:
no goals

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⟩]
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

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 := α) ..
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 }

State before:
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 }
Tactic:
simp
State after:
no goals