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

State before:
ι : Type
α : Type u_2
a b s✝ : Stream ι α
inst✝³ : Preorder ι
β : Type u_1
inst✝² : AddCommMonoid α
inst✝¹ : AddCommMonoid β
f : α →+ β
s : Stream ι α
inst✝ : IsBounded s
q : s.σ
⊢ eval (map (⇑f) s) q = (Finsupp.mapRange.addMonoidHom f) (eval s q)
Tactic:
apply s.wf.induction q
State after:
ι : Type
α : Type u_2
a b s✝ : Stream ι α
inst✝³ : Preorder ι
β : Type u_1
inst✝² : AddCommMonoid α
inst✝¹ : AddCommMonoid β
f : α →+ β
s : Stream ι α
inst✝ : IsBounded s
q : s.σ
⊢ ∀ (x : s.σ),
    (∀ (y : s.σ), WfRel s y x → eval (map (⇑f) s) y = (Finsupp.mapRange.addMonoidHom f) (eval s y)) →
      eval (map (⇑f) s) x = (Finsupp.mapRange.addMonoidHom f) (eval s x)

State before:
ι : Type
α : Type u_2
a b s✝ : Stream ι α
inst✝³ : Preorder ι
β : Type u_1
inst✝² : AddCommMonoid α
inst✝¹ : AddCommMonoid β
f : α →+ β
s : Stream ι α
inst✝ : IsBounded s
q : s.σ
⊢ ∀ (x : s.σ),
    (∀ (y : s.σ), WfRel s y x → eval (map (⇑f) s) y = (Finsupp.mapRange.addMonoidHom f) (eval s y)) →
      eval (map (⇑f) s) x = (Finsupp.mapRange.addMonoidHom f) (eval s x)
Tactic:
clear q
State after:
ι : Type
α : Type u_2
a b s✝ : Stream ι α
inst✝³ : Preorder ι
β : Type u_1
inst✝² : AddCommMonoid α
inst✝¹ : AddCommMonoid β
f : α →+ β
s : Stream ι α
inst✝ : IsBounded s
⊢ ∀ (x : s.σ),
    (∀ (y : s.σ), WfRel s y x → eval (map (⇑f) s) y = (Finsupp.mapRange.addMonoidHom f) (eval s y)) →
      eval (map (⇑f) s) x = (Finsupp.mapRange.addMonoidHom f) (eval s x)

State before:
ι : Type
α : Type u_2
a b s✝ : Stream ι α
inst✝³ : Preorder ι
β : Type u_1
inst✝² : AddCommMonoid α
inst✝¹ : AddCommMonoid β
f : α →+ β
s : Stream ι α
inst✝ : IsBounded s
⊢ ∀ (x : s.σ),
    (∀ (y : s.σ), WfRel s y x → eval (map (⇑f) s) y = (Finsupp.mapRange.addMonoidHom f) (eval s y)) →
      eval (map (⇑f) s) x = (Finsupp.mapRange.addMonoidHom f) (eval s x)
Tactic:
intro q ih
State after:
ι : Type
α : Type u_2
a b s✝ : Stream ι α
inst✝³ : Preorder ι
β : Type u_1
inst✝² : AddCommMonoid α
inst✝¹ : AddCommMonoid β
f : α →+ β
s : Stream ι α
inst✝ : IsBounded s
q : s.σ
ih : ∀ (y : s.σ), WfRel s y q → eval (map (⇑f) s) y = (Finsupp.mapRange.addMonoidHom f) (eval s y)
⊢ eval (map (⇑f) s) q = (Finsupp.mapRange.addMonoidHom f) (eval s q)

State before:
ι : Type
α : Type u_2
a b s✝ : Stream ι α
inst✝³ : Preorder ι
β : Type u_1
inst✝² : AddCommMonoid α
inst✝¹ : AddCommMonoid β
f : α →+ β
s : Stream ι α
inst✝ : IsBounded s
q : s.σ
ih : ∀ (y : s.σ), WfRel s y q → eval (map (⇑f) s) y = (Finsupp.mapRange.addMonoidHom f) (eval s y)
⊢ eval (map (⇑f) s) q = (Finsupp.mapRange.addMonoidHom f) (eval s q)
Tactic:
by_cases hq : s.valid q
State after:
case pos
ι : Type
α : Type u_2
a b s✝ : Stream ι α
inst✝³ : Preorder ι
β : Type u_1
inst✝² : AddCommMonoid α
inst✝¹ : AddCommMonoid β
f : α →+ β
s : Stream ι α
inst✝ : IsBounded s
q : s.σ
ih : ∀ (y : s.σ), WfRel s y q → eval (map (⇑f) s) y = (Finsupp.mapRange.addMonoidHom f) (eval s y)
hq : s.valid q = true
⊢ eval (map (⇑f) s) q = (Finsupp.mapRange.addMonoidHom f) (eval s q)

case neg
ι : Type
α : Type u_2
a b s✝ : Stream ι α
inst✝³ : Preorder ι
β : Type u_1
inst✝² : AddCommMonoid α
inst✝¹ : AddCommMonoid β
f : α →+ β
s : Stream ι α
inst✝ : IsBounded s
q : s.σ
ih : ∀ (y : s.σ), WfRel s y q → eval (map (⇑f) s) y = (Finsupp.mapRange.addMonoidHom f) (eval s y)
hq : ¬s.valid q = true
⊢ eval (map (⇑f) s) q = (Finsupp.mapRange.addMonoidHom f) (eval s q)

State before:
case pos
ι : Type
α : Type u_2
a b s✝ : Stream ι α
inst✝³ : Preorder ι
β : Type u_1
inst✝² : AddCommMonoid α
inst✝¹ : AddCommMonoid β
f : α →+ β
s : Stream ι α
inst✝ : IsBounded s
q : s.σ
ih : ∀ (y : s.σ), WfRel s y q → eval (map (⇑f) s) y = (Finsupp.mapRange.addMonoidHom f) (eval s y)
hq : s.valid q = true
⊢ eval (map (⇑f) s) q = (Finsupp.mapRange.addMonoidHom f) (eval s q)

case neg
ι : Type
α : Type u_2
a b s✝ : Stream ι α
inst✝³ : Preorder ι
β : Type u_1
inst✝² : AddCommMonoid α
inst✝¹ : AddCommMonoid β
f : α →+ β
s : Stream ι α
inst✝ : IsBounded s
q : s.σ
ih : ∀ (y : s.σ), WfRel s y q → eval (map (⇑f) s) y = (Finsupp.mapRange.addMonoidHom f) (eval s y)
hq : ¬s.valid q = true
⊢ eval (map (⇑f) s) q = (Finsupp.mapRange.addMonoidHom f) (eval s q)
Tactic:
swap
State after:
case neg
ι : Type
α : Type u_2
a b s✝ : Stream ι α
inst✝³ : Preorder ι
β : Type u_1
inst✝² : AddCommMonoid α
inst✝¹ : AddCommMonoid β
f : α →+ β
s : Stream ι α
inst✝ : IsBounded s
q : s.σ
ih : ∀ (y : s.σ), WfRel s y q → eval (map (⇑f) s) y = (Finsupp.mapRange.addMonoidHom f) (eval s y)
hq : ¬s.valid q = true
⊢ eval (map (⇑f) s) q = (Finsupp.mapRange.addMonoidHom f) (eval s q)

case pos
ι : Type
α : Type u_2
a b s✝ : Stream ι α
inst✝³ : Preorder ι
β : Type u_1
inst✝² : AddCommMonoid α
inst✝¹ : AddCommMonoid β
f : α →+ β
s : Stream ι α
inst✝ : IsBounded s
q : s.σ
ih : ∀ (y : s.σ), WfRel s y q → eval (map (⇑f) s) y = (Finsupp.mapRange.addMonoidHom f) (eval s y)
hq : s.valid q = true
⊢ eval (map (⇑f) s) q = (Finsupp.mapRange.addMonoidHom f) (eval s q)

State before:
case neg
ι : Type
α : Type u_2
a b s✝ : Stream ι α
inst✝³ : Preorder ι
β : Type u_1
inst✝² : AddCommMonoid α
inst✝¹ : AddCommMonoid β
f : α →+ β
s : Stream ι α
inst✝ : IsBounded s
q : s.σ
ih : ∀ (y : s.σ), WfRel s y q → eval (map (⇑f) s) y = (Finsupp.mapRange.addMonoidHom f) (eval s y)
hq : ¬s.valid q = true
⊢ eval (map (⇑f) s) q = (Finsupp.mapRange.addMonoidHom f) (eval s q)
Tactic:
rw [Stream.eval_invalid, Stream.eval_invalid] <;> simp [hq]
State after:
no goals

State before:
case pos
ι : Type
α : Type u_2
a b s✝ : Stream ι α
inst✝³ : Preorder ι
β : Type u_1
inst✝² : AddCommMonoid α
inst✝¹ : AddCommMonoid β
f : α →+ β
s : Stream ι α
inst✝ : IsBounded s
q : s.σ
ih : ∀ (y : s.σ), WfRel s y q → eval (map (⇑f) s) y = (Finsupp.mapRange.addMonoidHom f) (eval s y)
hq : s.valid q = true
⊢ eval (map (⇑f) s) q = (Finsupp.mapRange.addMonoidHom f) (eval s q)
Tactic:
rw [s.eval_valid ⟨_, hq⟩, (s.map f).eval_valid ⟨_, hq⟩]
State after:
case pos
ι : Type
α : Type u_2
a b s✝ : Stream ι α
inst✝³ : Preorder ι
β : Type u_1
inst✝² : AddCommMonoid α
inst✝¹ : AddCommMonoid β
f : α →+ β
s : Stream ι α
inst✝ : IsBounded s
q : s.σ
ih : ∀ (y : s.σ), WfRel s y q → eval (map (⇑f) s) y = (Finsupp.mapRange.addMonoidHom f) (eval s y)
hq : s.valid q = true
⊢ eval₀ (map (⇑f) s) { val := q, property := hq } +
      eval (map (⇑f) s) (advance (map (⇑f) s) ↑{ val := q, property := hq }) =
    (Finsupp.mapRange.addMonoidHom f)
      (eval₀ s { val := q, property := hq } + eval s (advance s ↑{ val := q, property := hq }))

State before:
case pos
ι : Type
α : Type u_2
a b s✝ : Stream ι α
inst✝³ : Preorder ι
β : Type u_1
inst✝² : AddCommMonoid α
inst✝¹ : AddCommMonoid β
f : α →+ β
s : Stream ι α
inst✝ : IsBounded s
q : s.σ
ih : ∀ (y : s.σ), WfRel s y q → eval (map (⇑f) s) y = (Finsupp.mapRange.addMonoidHom f) (eval s y)
hq : s.valid q = true
⊢ eval₀ (map (⇑f) s) { val := q, property := hq } +
      eval (map (⇑f) s) (advance (map (⇑f) s) ↑{ val := q, property := hq }) =
    (Finsupp.mapRange.addMonoidHom f)
      (eval₀ s { val := q, property := hq } + eval s (advance s ↑{ val := q, property := hq }))
Tactic:
simp only [map_σ, map_valid, map_add, Finsupp.mapRange.addMonoidHom_apply]
State after:
case pos
ι : Type
α : Type u_2
a b s✝ : Stream ι α
inst✝³ : Preorder ι
β : Type u_1
inst✝² : AddCommMonoid α
inst✝¹ : AddCommMonoid β
f : α →+ β
s : Stream ι α
inst✝ : IsBounded s
q : s.σ
ih : ∀ (y : s.σ), WfRel s y q → eval (map (⇑f) s) y = (Finsupp.mapRange.addMonoidHom f) (eval s y)
hq : s.valid q = true
⊢ eval₀ (map (⇑f) s) { val := q, property := hq } + eval (map (⇑f) s) (advance (map (⇑f) s) q) =
    Finsupp.mapRange ⇑f ⋯ (eval₀ s { val := q, property := hq }) + Finsupp.mapRange ⇑f ⋯ (eval s (advance s q))

State before:
case pos
ι : Type
α : Type u_2
a b s✝ : Stream ι α
inst✝³ : Preorder ι
β : Type u_1
inst✝² : AddCommMonoid α
inst✝¹ : AddCommMonoid β
f : α →+ β
s : Stream ι α
inst✝ : IsBounded s
q : s.σ
ih : ∀ (y : s.σ), WfRel s y q → eval (map (⇑f) s) y = (Finsupp.mapRange.addMonoidHom f) (eval s y)
hq : s.valid q = true
⊢ eval₀ (map (⇑f) s) { val := q, property := hq } + eval (map (⇑f) s) (advance (map (⇑f) s) q) =
    Finsupp.mapRange ⇑f ⋯ (eval₀ s { val := q, property := hq }) + Finsupp.mapRange ⇑f ⋯ (eval s (advance s q))
Tactic:
congr 1
State after:
case pos.e_a
ι : Type
α : Type u_2
a b s✝ : Stream ι α
inst✝³ : Preorder ι
β : Type u_1
inst✝² : AddCommMonoid α
inst✝¹ : AddCommMonoid β
f : α →+ β
s : Stream ι α
inst✝ : IsBounded s
q : s.σ
ih : ∀ (y : s.σ), WfRel s y q → eval (map (⇑f) s) y = (Finsupp.mapRange.addMonoidHom f) (eval s y)
hq : s.valid q = true
⊢ eval₀ (map (⇑f) s) { val := q, property := hq } = Finsupp.mapRange ⇑f ⋯ (eval₀ s { val := q, property := hq })

case pos.e_a
ι : Type
α : Type u_2
a b s✝ : Stream ι α
inst✝³ : Preorder ι
β : Type u_1
inst✝² : AddCommMonoid α
inst✝¹ : AddCommMonoid β
f : α →+ β
s : Stream ι α
inst✝ : IsBounded s
q : s.σ
ih : ∀ (y : s.σ), WfRel s y q → eval (map (⇑f) s) y = (Finsupp.mapRange.addMonoidHom f) (eval s y)
hq : s.valid q = true
⊢ eval (map (⇑f) s) (advance (map (⇑f) s) q) = Finsupp.mapRange ⇑f ⋯ (eval s (advance s q))

State before:
case pos.e_a
ι : Type
α : Type u_2
a b s✝ : Stream ι α
inst✝³ : Preorder ι
β : Type u_1
inst✝² : AddCommMonoid α
inst✝¹ : AddCommMonoid β
f : α →+ β
s : Stream ι α
inst✝ : IsBounded s
q : s.σ
ih : ∀ (y : s.σ), WfRel s y q → eval (map (⇑f) s) y = (Finsupp.mapRange.addMonoidHom f) (eval s y)
hq : s.valid q = true
⊢ eval₀ (map (⇑f) s) { val := q, property := hq } = Finsupp.mapRange ⇑f ⋯ (eval₀ s { val := q, property := hq })
Tactic:
rw [Stream.eval₀_map]
State after:
no goals

State before:
case pos.e_a
ι : Type
α : Type u_2
a b s✝ : Stream ι α
inst✝³ : Preorder ι
β : Type u_1
inst✝² : AddCommMonoid α
inst✝¹ : AddCommMonoid β
f : α →+ β
s : Stream ι α
inst✝ : IsBounded s
q : s.σ
ih : ∀ (y : s.σ), WfRel s y q → eval (map (⇑f) s) y = (Finsupp.mapRange.addMonoidHom f) (eval s y)
hq : s.valid q = true
⊢ eval (map (⇑f) s) (advance (map (⇑f) s) q) = Finsupp.mapRange ⇑f ⋯ (eval s (advance s q))
Tactic:
exact ih (s.advance q) (s.next_wf ⟨q, hq⟩)
State after:
no goals