no goals
ctx : Context
e : Expr
⊢ Poly.denote ctx (toPoly e) = denote ctx e
induction e with
| num k => by_cases h : k == 0 <;> simp [toPoly, h, Var.denote]; simp [eq_of_beq h]
| var i => simp [toPoly]
| add a b iha ihb => simp [toPoly, iha, ihb]
| mulL k a ih => simp [toPoly, ih, -Poly.mul]
| mulR k a ih => simp [toPoly, ih, -Poly.mul]
case num.inl
ctx : Context
k : Nat
h : (k == 0) = true
⊢ 0 = k
case num
ctx : Context
k : Nat
⊢ Poly.denote ctx (toPoly (num k)) = denote ctx (num k)
by_cases h : k == 0 <;> simp [toPoly, h, Var.denote]
no goals
case num.inl
ctx : Context
k : Nat
h : (k == 0) = true
⊢ 0 = k
simp [eq_of_beq h]
no goals
case var
ctx : Context
i : Var
⊢ Poly.denote ctx (toPoly (var i)) = denote ctx (var i)
simp [toPoly]
no goals
case add
ctx : Context
a b : Expr
iha : Poly.denote ctx (toPoly a) = denote ctx a
ihb : Poly.denote ctx (toPoly b) = denote ctx b
⊢ Poly.denote ctx (toPoly (add a b)) = denote ctx (add a b)
simp [toPoly, iha, ihb]
no goals
case mulL
ctx : Context
k : Nat
a : Expr
ih : Poly.denote ctx (toPoly a) = denote ctx a
⊢ Poly.denote ctx (toPoly (mulL k a)) = denote ctx (mulL k a)
simp [toPoly, ih, -Poly.mul]
no goals
case mulR
ctx : Context
k : Expr
a : Nat
ih : Poly.denote ctx (toPoly k) = denote ctx k
⊢ Poly.denote ctx (toPoly (mulR k a)) = denote ctx (mulR k a)
simp [toPoly, ih, -Poly.mul]