Theorem: Etch.Verification.Stream.IsStrictMono.evalMultiset_length_le (Etch/StreamFusion/Proofs/StreamProof.lean)

State before:
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsBounded s
h : IsStrictMono s
q : s.σ
i : ι
⊢ Multiset.card ((evalMultiset s q) i) ≤ 1
Tactic:
apply s.wf.induction q
State after:
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsBounded s
h : IsStrictMono s
q : s.σ
i : ι
⊢ ∀ (x : s.σ),
    (∀ (y : s.σ), WfRel s y x → Multiset.card ((evalMultiset s y) i) ≤ 1) → Multiset.card ((evalMultiset s x) i) ≤ 1

State before:
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsBounded s
h : IsStrictMono s
q : s.σ
i : ι
⊢ ∀ (x : s.σ),
    (∀ (y : s.σ), WfRel s y x → Multiset.card ((evalMultiset s y) i) ≤ 1) → Multiset.card ((evalMultiset s x) i) ≤ 1
Tactic:
clear q
State after:
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsBounded s
h : IsStrictMono s
i : ι
⊢ ∀ (x : s.σ),
    (∀ (y : s.σ), WfRel s y x → Multiset.card ((evalMultiset s y) i) ≤ 1) → Multiset.card ((evalMultiset s x) i) ≤ 1

State before:
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsBounded s
h : IsStrictMono s
i : ι
⊢ ∀ (x : s.σ),
    (∀ (y : s.σ), WfRel s y x → Multiset.card ((evalMultiset s y) i) ≤ 1) → Multiset.card ((evalMultiset s x) i) ≤ 1
Tactic:
intro q ih
State after:
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsBounded s
h : IsStrictMono s
i : ι
q : s.σ
ih : ∀ (y : s.σ), WfRel s y q → Multiset.card ((evalMultiset s y) i) ≤ 1
⊢ Multiset.card ((evalMultiset s q) i) ≤ 1

State before:
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsBounded s
h : IsStrictMono s
i : ι
q : s.σ
ih : ∀ (y : s.σ), WfRel s y q → Multiset.card ((evalMultiset s y) i) ≤ 1
⊢ Multiset.card ((evalMultiset s q) i) ≤ 1
Tactic:
by_cases hq : s.valid q
State after:
case pos
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsBounded s
h : IsStrictMono s
i : ι
q : s.σ
ih : ∀ (y : s.σ), WfRel s y q → Multiset.card ((evalMultiset s y) i) ≤ 1
hq : s.valid q = true
⊢ Multiset.card ((evalMultiset s q) i) ≤ 1

case neg
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsBounded s
h : IsStrictMono s
i : ι
q : s.σ
ih : ∀ (y : s.σ), WfRel s y q → Multiset.card ((evalMultiset s y) i) ≤ 1
hq : ¬s.valid q = true
⊢ Multiset.card ((evalMultiset s q) i) ≤ 1

State before:
case pos
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsBounded s
h : IsStrictMono s
i : ι
q : s.σ
ih : ∀ (y : s.σ), WfRel s y q → Multiset.card ((evalMultiset s y) i) ≤ 1
hq : s.valid q = true
⊢ Multiset.card ((evalMultiset s q) i) ≤ 1

case neg
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsBounded s
h : IsStrictMono s
i : ι
q : s.σ
ih : ∀ (y : s.σ), WfRel s y q → Multiset.card ((evalMultiset s y) i) ≤ 1
hq : ¬s.valid q = true
⊢ Multiset.card ((evalMultiset s q) i) ≤ 1
Tactic:
swap
State after:
case neg
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsBounded s
h : IsStrictMono s
i : ι
q : s.σ
ih : ∀ (y : s.σ), WfRel s y q → Multiset.card ((evalMultiset s y) i) ≤ 1
hq : ¬s.valid q = true
⊢ Multiset.card ((evalMultiset s q) i) ≤ 1

case pos
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsBounded s
h : IsStrictMono s
i : ι
q : s.σ
ih : ∀ (y : s.σ), WfRel s y q → Multiset.card ((evalMultiset s y) i) ≤ 1
hq : s.valid q = true
⊢ Multiset.card ((evalMultiset s q) i) ≤ 1

State before:
case neg
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsBounded s
h : IsStrictMono s
i : ι
q : s.σ
ih : ∀ (y : s.σ), WfRel s y q → Multiset.card ((evalMultiset s y) i) ≤ 1
hq : ¬s.valid q = true
⊢ Multiset.card ((evalMultiset s q) i) ≤ 1
Tactic:
simp [hq]
State after:
no goals

State before:
case pos
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsBounded s
h : IsStrictMono s
i : ι
q : s.σ
ih : ∀ (y : s.σ), WfRel s y q → Multiset.card ((evalMultiset s y) i) ≤ 1
hq : s.valid q = true
⊢ Multiset.card ((evalMultiset s q) i) ≤ 1
Tactic:
by_cases hr : s.ready ⟨q, hq⟩ ∧ s.index ⟨q, hq⟩ = i
State after:
case pos
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsBounded s
h : IsStrictMono s
i : ι
q : s.σ
ih : ∀ (y : s.σ), WfRel s y q → Multiset.card ((evalMultiset s y) i) ≤ 1
hq : s.valid q = true
hr : s.ready { val := q, property := hq } = true ∧ s.index { val := q, property := hq } = i
⊢ Multiset.card ((evalMultiset s q) i) ≤ 1

case neg
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsBounded s
h : IsStrictMono s
i : ι
q : s.σ
ih : ∀ (y : s.σ), WfRel s y q → Multiset.card ((evalMultiset s y) i) ≤ 1
hq : s.valid q = true
hr : ¬(s.ready { val := q, property := hq } = true ∧ s.index { val := q, property := hq } = i)
⊢ Multiset.card ((evalMultiset s q) i) ≤ 1

State before:
case pos
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsBounded s
h : IsStrictMono s
i : ι
q : s.σ
ih : ∀ (y : s.σ), WfRel s y q → Multiset.card ((evalMultiset s y) i) ≤ 1
hq : s.valid q = true
hr : s.ready { val := q, property := hq } = true ∧ s.index { val := q, property := hq } = i
⊢ Multiset.card ((evalMultiset s q) i) ≤ 1
Tactic:
rw [← hr.2, h.evalMultiset_ready hr.1, Multiset.card_singleton]
State after:
no goals

State before:
case neg
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsBounded s
h : IsStrictMono s
i : ι
q : s.σ
ih : ∀ (y : s.σ), WfRel s y q → Multiset.card ((evalMultiset s y) i) ≤ 1
hq : s.valid q = true
hr : ¬(s.ready { val := q, property := hq } = true ∧ s.index { val := q, property := hq } = i)
⊢ Multiset.card ((evalMultiset s q) i) ≤ 1
Tactic:
rw [Stream.evalMultiset_not_ready (q := ⟨q, hq⟩)]
State after:
case neg
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsBounded s
h : IsStrictMono s
i : ι
q : s.σ
ih : ∀ (y : s.σ), WfRel s y q → Multiset.card ((evalMultiset s y) i) ≤ 1
hq : s.valid q = true
hr : ¬(s.ready { val := q, property := hq } = true ∧ s.index { val := q, property := hq } = i)
⊢ Multiset.card ((evalMultiset s (advance s ↑{ val := q, property := hq })) i) ≤ 1

case neg.hr
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsBounded s
h : IsStrictMono s
i : ι
q : s.σ
ih : ∀ (y : s.σ), WfRel s y q → Multiset.card ((evalMultiset s y) i) ≤ 1
hq : s.valid q = true
hr : ¬(s.ready { val := q, property := hq } = true ∧ s.index { val := q, property := hq } = i)
⊢ ¬s.ready { val := q, property := hq } = true ∨ s.index { val := q, property := hq } ≠ i

State before:
case neg
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsBounded s
h : IsStrictMono s
i : ι
q : s.σ
ih : ∀ (y : s.σ), WfRel s y q → Multiset.card ((evalMultiset s y) i) ≤ 1
hq : s.valid q = true
hr : ¬(s.ready { val := q, property := hq } = true ∧ s.index { val := q, property := hq } = i)
⊢ Multiset.card ((evalMultiset s (advance s ↑{ val := q, property := hq })) i) ≤ 1
Tactic:
apply ih
State after:
case neg.a
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsBounded s
h : IsStrictMono s
i : ι
q : s.σ
ih : ∀ (y : s.σ), WfRel s y q → Multiset.card ((evalMultiset s y) i) ≤ 1
hq : s.valid q = true
hr : ¬(s.ready { val := q, property := hq } = true ∧ s.index { val := q, property := hq } = i)
⊢ WfRel s (advance s ↑{ val := q, property := hq }) q

State before:
case neg.a
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsBounded s
h : IsStrictMono s
i : ι
q : s.σ
ih : ∀ (y : s.σ), WfRel s y q → Multiset.card ((evalMultiset s y) i) ≤ 1
hq : s.valid q = true
hr : ¬(s.ready { val := q, property := hq } = true ∧ s.index { val := q, property := hq } = i)
⊢ WfRel s (advance s ↑{ val := q, property := hq }) q
Tactic:
exact s.next_wf ⟨q, hq⟩
State after:
no goals

State before:
case neg.hr
ι : Type
inst✝¹ : LinearOrder ι
α : Type u_1
s : Stream ι α
inst✝ : IsBounded s
h : IsStrictMono s
i : ι
q : s.σ
ih : ∀ (y : s.σ), WfRel s y q → Multiset.card ((evalMultiset s y) i) ≤ 1
hq : s.valid q = true
hr : ¬(s.ready { val := q, property := hq } = true ∧ s.index { val := q, property := hq } = i)
⊢ ¬s.ready { val := q, property := hq } = true ∨ s.index { val := q, property := hq } ≠ i
Tactic:
exact not_and_or.mp hr
State after:
no goals