contribution: induction on polynomial degree

Stream: new members

[Way Yan Win]

Hi, it seems that (strong) induction on polynomial.nat_degree isn't supported yet, so as a first contribution to mathlib I'd like to add that. Here is the code I have, inspired by their analogues nat.strong_induction_on and nat.case_strong_induction_on:

import data.polynomial.degree.definitions

variables {R : Type*} [semiring R]

lemma polynomial_nat_degree_strong_induction_on {P : polynomial R → Prop}
  (p : polynomial R)
  (h : ∀ (p : polynomial R) (n : ℕ),
    (∀ (m : ℕ), m < n →
      (∀ (p' : polynomial R), p'.nat_degree = m → P p')) →
        p.nat_degree = n → P p) :
  P p :=
begin
  generalize hd : p.nat_degree = d,
  revert hd p,
  apply nat.strong_induction_on d, clear d,
  intros n h' p,
  exact h p n h',
end

lemma polynomial_nat_degree_case_strong_induction_on {P : polynomial R → Prop}
  (p : polynomial R)
  (hz : ∀ (p : polynomial R), p.nat_degree = 0 → P p)
  (hi : ∀ (p : polynomial R) (n : ℕ),
    (∀ (m : ℕ), m ≤ n →
      (∀ (p' : polynomial R), p'.nat_degree = m → P p')) →
        p.nat_degree = n.succ → P p) :
  P p :=
begin
  generalize hd : p.nat_degree = d,
  revert hd p,
  apply nat.case_strong_induction_on d, clear d,
  { exact hz },
  { intros n h p, exact hi p n h }
end

If it is ok, can I have write access to the mathlib repository? My username is greysome.

[Eric Wieser]

I'd argue that strong induction on nat_degree is supported, and the spelling is pretty much what you have there. I don't think it makes much sense to duplicate nat strong_induction for every nat-valued property of other types.

[Eric Wieser]

Does induction h : p.nat_degree using nat.strong_induction_on do what you need?

[Way Yan Win]

ohh, I didn't know that was possible. thanks!

[Way Yan Win]

hmm wait actually there is a difference, because in the induction hypothesis there is an additional quantifier (namely, if for all m < n the property holds for all polynomials of degree m, then the property holds for all polynomials of degree n)

[Way Yan Win]

I think induction h : p.nat_degree using nat.strong_induction_on with i hi generalizing p would be correct

[Eric Wieser]

Ah, I forgot that it didn't generalize that automatically

[Eric Wieser]

If it is ok, can I have write access to the mathlib repository? My username is greysome.

I've sent an invite; even though I think the lemmas above are redundant, you're certainly welcome to contribute other things to mathlib

[Yaël Dillies]

This induction is a bit dull, but there are many inductions on the polynomials that we don't have. For example, p P -> p Q -> p (P * Q) and p (X - a)^n

[Eric Rodriguez]

That also needs p y for y in the base field or some similar condition

[Eric Wieser]

A variant of docs#polynomial.rec_on_horner for mv_polynomial might be nice too

[Way Yan Win]

Since we're already on this topic, there are some other results on polynomials that I've needed, which are oddly missing:

variables {R : Type*} [semiring R]
theorem nat_degree_pow_le (p : polynomial R) (n : ℕ) : (p ^ n).nat_degree ≤ n * p.nat_degree := sorry
theorem coeff_pow_degree_mul_degree (p : polynomial R) (n : ℕ) : (p ^ n).coeff (n * p.nat_degree) = p.leading_coeff ^ n := sorry

This seems like a reasonable contribution since there's already nat_degree_mul_le and coeff_mul_degree_add_degree

[Yaël Dillies]

And maybe do the constant coeff version as well?

[Eric Wieser]

Note we already have docs#polynomial.nat_degree_pow and docs#polynomial.nat_degree_pow'; the new pow lemma should reference those and maybe go somewhere near them

[Way Yan Win]

Yaël Dillies said:

And maybe do the constant coeff version as well?

Which specific result is that?

[Way Yan Win]

Eric Wieser said:

Note we already have docs#polynomial.nat_degree_pow and docs#polynomial.nat_degree_pow'; the new pow lemma should reference those and maybe go somewhere near them

Ah ok I'll try that

[Eric Wieser]

If you're looking for more contributions, we should probably have the degree variant of that nat.degree lemma

[Way Yan Win]

Right now I'm trying to copy the proof for nat_degree_mul_le in nat_degree_pow_le:

import data.polynomial.degree.definitions
open polynomial

variables {R : Type*} [semiring R]

lemma nat_degree_pow_le {p : polynomial R} {n : ℕ} : nat_degree (p ^ n) ≤ n * nat_degree p :=
begin
  apply nat_degree_le_of_degree_le,
  apply le_trans (degree_pow_le p n),
  rw [nsmul_eq_mul, with_bot.coe_mul],
  sorry
end

So I'm stuck at showing that ↑n * p.degree ≤ ↑n * ↑p.nat_degree. The other proof continued with refine add_le_add _ _, but the corresponding refine mul_le_mul_left' _ _ doesn't work. I suspect it's because with_bot.ordered_add_comm_monoid has been established but not with_bot.ordered_comm_monoid. Hopefully I'm on the right track with this?

[Eric Wieser]

Is it easier to prove the degree_pow_le version first?

[Eric Wieser]

Then do case analysis on whether p = 0 to handle the \bot and nat cases?

[Ruben Van de Velde]

Yeah, I don't think getting to a goal like p.degree ≤ ↑(p.nat_degree) is going to help you

[Kevin Buzzard]

Maybe direct induction on n is far less painful?

[Ruben Van de Velde]

rw [nat.cast_with_bot, degree_eq_nat_degree hp] will help though, after the case split

[Eric Wieser]

This is a mess, but works:

lemma nat_degree_pow_le {p : polynomial R} {n : ℕ} : nat_degree (p ^ n) ≤ n * nat_degree p :=
begin
  by_cases hn : n = 0,
  { rw hn, simp },
  by_cases hpn : p ^ n = 0,
  { rw hpn, simp },
  have hp : p ≠ 0,
  { rintro rfl,
    apply hpn,
    simp [hn], },
  rw [←with_bot.coe_le_coe, with_bot.coe_mul],
  rw [←degree_eq_nat_degree hpn, ←degree_eq_nat_degree hp],
  convert degree_pow_le _ _,
  simp,
end

[Ruben Van de Velde]

Six lines with either approach:

import data.polynomial.degree

open polynomial

variables {R : Type*} [semiring R]
lemma nat_degree_pow_le {p : polynomial R} {n : ℕ} : nat_degree (p ^ n) ≤ n * nat_degree p :=
begin
  obtain rfl|hp := eq_or_ne p 0,
  { obtain rfl|hn := eq_or_ne n 0; simp [*] },
  apply nat_degree_le_of_degree_le,
  apply le_trans (degree_pow_le p n),
  rw [nsmul_eq_mul, with_bot.coe_mul, nat.cast_with_bot, degree_eq_nat_degree hp],
  exact le_rfl,
end

lemma nat_degree_pow_le' {p : polynomial R} {n : ℕ} : nat_degree (p ^ n) ≤ n * nat_degree p :=
begin
  induction n with n ih,
  { simp },
  { rw [pow_succ],
    apply le_trans nat_degree_mul_le,
    apply le_trans (add_le_add_left ih _),
    rw [nat.succ_mul, add_comm] },
end

[Eric Wieser]

I think proving it in terms of the degree version is nicer than using induction

[Kevin Buzzard]

despite the fact that the induction proof has fewer characters, is more primitive, and probably compiles more quickly? ;-)

[Eric Wieser]

Yes, because the one proved from degree gives a template for "how to prove things about nat_degree from things about degree" that you can blindly repeat

[Eric Wieser]

Of course, it would also be good to make the proof less messy.

[Way Yan Win]

Thanks, I'll try the above approaches then. I was initially worried that the proof will look different from the existing proofs, but I guess it's good to have something working at least