no goals
ctx : Context
e : Expr
⊢ Poly.denote ctx (toPoly e) = denote ctx e
induction e with
| num k =>
  simp!; by_cases h : k == 0 <;> simp! [*]
  simp [eq_of_beq h]
| var v => simp!
| add a b => simp! [Poly.add_denote, *]
| mul a b => simp! [Poly.mul_denote, *]
case num
ctx : Context
k : Nat
⊢ Poly.denote ctx (bif k == 0 then [] else [(k, [])]) = k
case num
ctx : Context
k : Nat
⊢ Poly.denote ctx (toPoly (num k)) = denote ctx (num k)
simp!
case num.inl
ctx : Context
k : Nat
h : (k == 0) = true
⊢ 0 = k
case num
ctx : Context
k : Nat
⊢ Poly.denote ctx (bif k == 0 then [] else [(k, [])]) = k
by_cases h : k == 0 <;> simp! [*]
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
v : Var
⊢ Poly.denote ctx (toPoly (var v)) = denote ctx (var v)
simp!
no goals
case add
ctx : Context
a b : Expr
a_ih✝ : Poly.denote ctx (toPoly a) = denote ctx a
b_ih✝ : Poly.denote ctx (toPoly b) = denote ctx b
⊢ Poly.denote ctx (toPoly (add a b)) = denote ctx (add a b)
simp! [Poly.add_denote, *]
no goals
case mul
ctx : Context
a b : Expr
a_ih✝ : Poly.denote ctx (toPoly a) = denote ctx a
b_ih✝ : Poly.denote ctx (toPoly b) = denote ctx b
⊢ Poly.denote ctx (toPoly (mul a b)) = denote ctx (mul a b)
simp! [Poly.mul_denote, *]