Zulip Chat Archive

Stream: maths

Topic: Proving degree lemmas for polynomials


view this post on Zulip Chris Hughes (Aug 07 2018 at 19:19):

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?

view this post on Zulip Kevin Buzzard (Aug 07 2018 at 19:38):

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

view this post on Zulip Kevin Buzzard (Aug 07 2018 at 19:40):

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?

view this post on Zulip Chris Hughes (Aug 07 2018 at 20:09):

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


Last updated: May 09 2021 at 10:11 UTC