Proving degree lemmas for polynomials

Stream: maths

[Chris Hughes]

I wrote some stuff on polynomials recently, which has been merged, but I was never that happy with it, because I knew that proving basic lemmas about degree was going to be quite hard. For example

import data.polynomial

example {α : Type*} [integral_domain α] [decidable_eq α] :
  degree ((X : polynomial α) ^ 2 + 1) = 2 :=
have h₁ : degree ((X : polynomial α) ^ 2) = 2,
  by rw [degree_pow_eq, degree_X]; refl,
have h₂ : degree (1 : polynomial α) < degree ((X : polynomial α) ^ 2),
  by rw [degree_one, h₁]; exact dec_trivial,
by rw [add_comm, degree_add_eq_of_degree_lt h₂, h₁]

What's the best way of dealing with problems like this, tactics or lemmas?

[Kevin Buzzard]

That looks like the proof I would have written -- but are you suggesting that the proof should be dec_trivial?

[Kevin Buzzard]

because I guess there's an algorithm; however it reminds me a bit of the ring tactic. Do you think you could modify that simple baby ring tactic that Mario wrote to turn it into a tactic which computes degree?

[Chris Hughes]

It would be dec_trivial if it was integers, the fact that the type is a variable is the problem.