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

State before:
ι : Type
α : Type u_1
a b s✝ : Stream ι α
inst✝¹ : Preorder ι
s : Stream ι α
inst✝ : IsBounded s
q : { q // s.valid q = true }
i : ι
hr : ¬s.ready q = true ∨ s.index q ≠ i
⊢ (evalMultiset s ↑q) i = (evalMultiset s (advance s ↑q)) i
Tactic:
suffices (s.map fun x => ({x} : Multiset α)).eval₀ q i = 0 by
  simpa [Stream.evalMultiset]
State after:
ι : Type
α : Type u_1
a b s✝ : Stream ι α
inst✝¹ : Preorder ι
s : Stream ι α
inst✝ : IsBounded s
q : { q // s.valid q = true }
i : ι
hr : ¬s.ready q = true ∨ s.index q ≠ i
⊢ (eval₀ (map (fun x => {x}) s) q) i = 0

State before:
ι : Type
α : Type u_1
a b s✝ : Stream ι α
inst✝¹ : Preorder ι
s : Stream ι α
inst✝ : IsBounded s
q : { q // s.valid q = true }
i : ι
hr : ¬s.ready q = true ∨ s.index q ≠ i
this : (eval₀ (map (fun x => {x}) s) q) i = 0
⊢ (evalMultiset s ↑q) i = (evalMultiset s (advance s ↑q)) i
Tactic:
simpa [Stream.evalMultiset]
State after:
no goals

State before:
case inl
ι : Type
α : Type u_1
a b s✝ : Stream ι α
inst✝¹ : Preorder ι
s : Stream ι α
inst✝ : IsBounded s
q : { q // s.valid q = true }
i : ι
hr : ¬s.ready q = true
⊢ (eval₀ (map (fun x => {x}) s) q) i = 0
Tactic:
simp [Stream.eval₀, hr]
State after:
no goals

State before:
case inr
ι : Type
α : Type u_1
a b s✝ : Stream ι α
inst✝¹ : Preorder ι
s : Stream ι α
inst✝ : IsBounded s
q : { q // s.valid q = true }
i : ι
hr : s.index q ≠ i
⊢ (eval₀ (map (fun x => {x}) s) q) i = 0
Tactic:
simp only [Stream.eval₀]
State after:
case inr
ι : Type
α : Type u_1
a b s✝ : Stream ι α
inst✝¹ : Preorder ι
s : Stream ι α
inst✝ : IsBounded s
q : { q // s.valid q = true }
i : ι
hr : s.index q ≠ i
⊢ (if h₂ : (map (fun x => {x}) s).ready q = true then
        fun₀ | (map (fun x => {x}) s).index q => (map (fun x => {x}) s).value { val := q, property := h₂ }
      else 0)
      i =
    0

State before:
case inr
ι : Type
α : Type u_1
a b s✝ : Stream ι α
inst✝¹ : Preorder ι
s : Stream ι α
inst✝ : IsBounded s
q : { q // s.valid q = true }
i : ι
hr : s.index q ≠ i
⊢ (if h₂ : (map (fun x => {x}) s).ready q = true then
        fun₀ | (map (fun x => {x}) s).index q => (map (fun x => {x}) s).value { val := q, property := h₂ }
      else 0)
      i =
    0
Tactic:
split_ifs
State after:
case pos
ι : Type
α : Type u_1
a b s✝ : Stream ι α
inst✝¹ : Preorder ι
s : Stream ι α
inst✝ : IsBounded s
q : { q // s.valid q = true }
i : ι
hr : s.index q ≠ i
h✝ : (map (fun x => {x}) s).ready q = true
⊢ (fun₀ | (map (fun x => {x}) s).index q => (map (fun x => {x}) s).value { val := q, property := h✝ }) i = 0

case neg
ι : Type
α : Type u_1
a b s✝ : Stream ι α
inst✝¹ : Preorder ι
s : Stream ι α
inst✝ : IsBounded s
q : { q // s.valid q = true }
i : ι
hr : s.index q ≠ i
h✝ : ¬(map (fun x => {x}) s).ready q = true
⊢ 0 i = 0

State before:
case pos
ι : Type
α : Type u_1
a b s✝ : Stream ι α
inst✝¹ : Preorder ι
s : Stream ι α
inst✝ : IsBounded s
q : { q // s.valid q = true }
i : ι
hr : s.index q ≠ i
h✝ : (map (fun x => {x}) s).ready q = true
⊢ (fun₀ | (map (fun x => {x}) s).index q => (map (fun x => {x}) s).value { val := q, property := h✝ }) i = 0

case neg
ι : Type
α : Type u_1
a b s✝ : Stream ι α
inst✝¹ : Preorder ι
s : Stream ι α
inst✝ : IsBounded s
q : { q // s.valid q = true }
i : ι
hr : s.index q ≠ i
h✝ : ¬(map (fun x => {x}) s).ready q = true
⊢ 0 i = 0
Tactic:
swap
State after:
case neg
ι : Type
α : Type u_1
a b s✝ : Stream ι α
inst✝¹ : Preorder ι
s : Stream ι α
inst✝ : IsBounded s
q : { q // s.valid q = true }
i : ι
hr : s.index q ≠ i
h✝ : ¬(map (fun x => {x}) s).ready q = true
⊢ 0 i = 0

case pos
ι : Type
α : Type u_1
a b s✝ : Stream ι α
inst✝¹ : Preorder ι
s : Stream ι α
inst✝ : IsBounded s
q : { q // s.valid q = true }
i : ι
hr : s.index q ≠ i
h✝ : (map (fun x => {x}) s).ready q = true
⊢ (fun₀ | (map (fun x => {x}) s).index q => (map (fun x => {x}) s).value { val := q, property := h✝ }) i = 0

State before:
case pos
ι : Type
α : Type u_1
a b s✝ : Stream ι α
inst✝¹ : Preorder ι
s : Stream ι α
inst✝ : IsBounded s
q : { q // s.valid q = true }
i : ι
hr : s.index q ≠ i
h✝ : (map (fun x => {x}) s).ready q = true
⊢ (fun₀ | (map (fun x => {x}) s).index q => (map (fun x => {x}) s).value { val := q, property := h✝ }) i = 0
Tactic:
simp [hr]
State after:
no goals

State before:
case neg
ι : Type
α : Type u_1
a b s✝ : Stream ι α
inst✝¹ : Preorder ι
s : Stream ι α
inst✝ : IsBounded s
q : { q // s.valid q = true }
i : ι
hr : s.index q ≠ i
h✝ : ¬(map (fun x => {x}) s).ready q = true
⊢ 0 i = 0
Tactic:
rfl
State after:
no goals