## Stream: general

### Topic: equation lemma ugliness

#### Kevin Buzzard (Jun 12 2018 at 22:11):

def poly := list ℤ

def poly.add : poly → poly → poly
| [] g := g
| f [] := f
| (a :: f') (b :: g') := (a + b) :: poly.add f' g'

-- example (p : poly) : poly.add [] p = p := rfl -- fails

/-
...
poly.add.equations._eqn_2 : ∀ (hd : ℤ) (tl : list ℤ), poly.add list.nil (hd :: tl) = hd :: tl
...

-- it did unnecessary cases on g.
-/

example (p : poly) : poly.add [] p = p := by cases p;refl


#### Kevin Buzzard (Jun 12 2018 at 22:13):

Is this just "one of those things" -- is my proof of poly.add using cases something which I should be OK with, or should I now start tweaking things to try and make the example rfl? I am about to make it a simp lemma -- is that "good enough"? As you can see, I can prove the result, I am just worried about whether my proof is somehow bad style. It's my fancy recursive definition which is to blame of course, but the definition is recursive (I'm representing a polynomial as a list of its coefficients starting with the constant term)

Last updated: May 17 2021 at 22:15 UTC