induction on degree of polynomial

Stream: maths

[Kevin Buzzard]

There exists theorems about polynomials whose maths proofs are "trivial by strong induction on degree of the polynomial". How do I write this in Lean?

import data.polynomial.degree

example (R : Type) [comm_ring R] (f : polynomial R)
  (P : polynomial R → Prop)
  -- I want to reduce the goal `P f` to a statement
  -- of the form "if a certain statement is true
  -- for all functions of nat_degree zero and
  -- if some statement about functions of degree d
  -- implies some statement about functions of degree d+1,
  -- then we're done", and that should be nat.rec
  : P f :=
-- Maths proof: "Easy exercise (hint: induction on degree)"
@nat.rec _ _ _ f.nat_degree _ -- computer says no

[Ruben Van de Velde]

induction h : p.nat_degree using nat strong_induction_on or something like that?

[Kevin Buzzard]

Yeah OK I've got it working:

theorem polynomial.degree_induction (R : Type) [comm_ring R] (f : polynomial R)
  (P : polynomial R → Prop)
  (h0 : ∀ g : polynomial R, g.nat_degree = 0 → P g)
  (hsucc : ∀ d : ℕ, (∀ g : polynomial R, g.nat_degree = d → P g) → (∀ g : polynomial R, g.nat_degree = d.succ → P g))
  : P f :=
begin
  let n := f.nat_degree,
  suffices : ∀ q : polynomial R, q.nat_degree = n → P q,
  { exact this _ rfl, },
  -- refine @nat.rec _ h0 hsucc n, -- fails
  -- but the next line guesses the motive anyway
  exact nat.rec h0 hsucc n
end

I'm sure I'm still making a meal of it.

[Kevin Buzzard]

Finally getting the hang of it:

theorem polynomial.degree_strong_induction {R : Type*} [comm_ring R] (f : polynomial R)
  (P : polynomial R → Prop)
  (IH : ∀ (n : ℕ),
  (∀ (m : ℕ), m < n → ∀ (q : polynomial R), q.nat_degree = m → P q) →
  ∀ (q : polynomial R), q.nat_degree = n → P q)
  : P f :=
(nat.strong_induction_on f.nat_degree IH) _ rfl

Dunno why I found these so hard to write; I was occasionally wrestling with the elaborator.

[Eric Wieser]

I think @Ruben Van de Velde's point is that we don't need those lemmas, as the h : syntax of the induction tactic already covers them

[Ruben Van de Velde]

If the lemma is helpful to Kevin, who am I to disagree? :)

[Kevin Buzzard]

Sorry, I moved onto other things (marking for my course appeared and I had to prioritise that) but now I'm back trying to prove the same theorem (and my course is over next week so I'd better get a move on!) and I still do not understand what people are saying here. As shown above I can prove polynomial.degree_strong_induction by explicitly using nat.strong_induction_on but for pedagogical reasons (and also for elaborator reasons) I would rather use the induction tactic. What I want is to formalise "We prove this by strong induction on degree; it now suffices to verify the inductive hypothesis". Hopefully the following Lean code makes it clear what my problem is.

import data.polynomial.degree

-- Goal: to reduce a goal `∀ f, P f` to a statement of the form
-- "if P is true for all polynomials of degree < n then it's true for
-- all polynomials of degree n".

-- What I want:
theorem polynomial.degree_strong_induction {R : Type*} [comm_ring R] (f : polynomial R)
  (P : polynomial R → Prop)
  (IH : ∀ (n : ℕ),
  (∀ (m : ℕ), m < n → ∀ (q : polynomial R), q.nat_degree = m → P q) →
  ∀ (q : polynomial R), q.nat_degree = n → P q)
  : P f :=
begin
  -- INSERT MAGIC INCANTATION HERE
  exact IH, -- or exact IH f.nat_degree or whatever
end

-- Here is a complete proof of the statement.
theorem polynomial.degree_strong_induction1 {R : Type*} [comm_ring R] (f : polynomial R)
  (P : polynomial R → Prop)
  -- Assume we're given IH already.
  (IH : ∀ (n : ℕ),
  (∀ (m : ℕ), m < n → ∀ (q : polynomial R), q.nat_degree = m → P q) →
  ∀ (q : polynomial R), q.nat_degree = n → P q)
  : P f :=
nat.strong_induction_on f.nat_degree IH _ rfl
-- This works, so this is fine *if* you have `IH` to hand, which of course
-- in practice you may not (and you might not want to make it by hand
-- if `P` is complex)
-- Note that `rfl` is a proof of `f.nat_degree = f.nat_degree` and
-- I don't really understand what it's doing there; I seem to be giving
-- nat.strong_induction_on too many arguments (i.e. I don't actually understand this proof;
-- I think the motive is more complicated than I imagine)

theorem polynomial.degree_strong_induction2 {R : Type*} [comm_ring R] (f : polynomial R)
  (P : polynomial R → Prop)
  -- (IH : ∀ (n : ℕ),
  -- (∀ (m : ℕ), m < n → ∀ (q : polynomial R), q.nat_degree = m → P q) →
  -- ∀ (q : polynomial R), q.nat_degree = n → P q)
  : P f :=
begin
  -- want to make Lean make IH automatically from P
  refine nat.strong_induction_on f.nat_degree _ _ (rfl : f.nat_degree = f.nat_degree),
  -- elaboration error which I don't understand and can't fix
end

-- `induction using` attempt:
theorem polynomial.degree_strong_induction3 {R : Type*} [comm_ring R] (f : polynomial R)
  (P : polynomial R → Prop)
  (IH : ∀ (n : ℕ),
  (∀ (m : ℕ), m < n → ∀ (q : polynomial R), q.nat_degree = m → P q) →
  ∀ (q : polynomial R), q.nat_degree = n → P q)
  : P f :=
begin
  induction h : f.nat_degree using nat.strong_induction_on,
  dsimp at ᾰ,
  -- oh dear, notice that ᾰ is useless in the presence of h
  -- as it claims f.nat_degree < f.nat_degree
  sorry,
end

theorem polynomial.degree_strong_induction4 {R : Type*} [comm_ring R] (f : polynomial R)
  (P : polynomial R → Prop)
  (IH : ∀ (n : ℕ),
  (∀ (m : ℕ), m < n → ∀ (q : polynomial R), q.nat_degree = m → P q) →
  ∀ (q : polynomial R), q.nat_degree = n → P q)
  : P f :=
begin
  induction h : f.nat_degree using nat.strong_induction_on generalizing f,
  --
  dsimp at ᾰ,
  -- well now probably ᾰ isn't useless but it's a hypothesis, not the goal.
  sorry,
end

[Eric Rodriguez]

I don't see the issue:

import data.polynomial.degree

theorem polynomial.degree_strong_induction4 {R : Type*} [comm_ring R] (f : polynomial R)
  (P : polynomial R → Prop)
  (IH : ∀ (n : ℕ),
  (∀ (m : ℕ), m < n → ∀ (q : polynomial R), q.nat_degree = m → P q) →
  ∀ (q : polynomial R), q.nat_degree = n → P q)
  : P f :=
begin
  induction h : f.nat_degree using nat.strong_induction_on generalizing f,
  --
  dsimp at ᾰ,
  -- well now probably ᾰ isn't useless but it's a hypothesis, not the goal.
  apply IH _ ᾰ _ h,
end

[Kevin Buzzard]

The point is that in my use case I do not have IH. I want to reduce the goal to IH, not use IH to prove the goal.

[Eric Rodriguez]

then I don't see the issue at all, either; you have h and ǎ in the goal, which give you everything you need. in fact, I did this recently with strong induction on the derivative of a polynomial:

import data.polynomial.derivative

open_locale polynomial
open polynomial

lemma iterate_derivative_eq_zero {R} [comm_semiring R] {p : R[X]} {x : ℕ} (hx : p.nat_degree < x) :
  polynomial.derivative^[x] p = 0 :=
begin
  induction h : p.nat_degree using nat.strong_induction_on with _ ih generalizing p x,
  subst h,
  obtain ⟨t, rfl⟩ := nat.exists_eq_succ_of_ne_zero (pos_of_gt hx).ne',
  rw [function.iterate_succ_apply],
  by_cases hp : p.derivative = 0,
  { rw [hp, polynomial.iterate_derivative_zero] },
  have := nat_degree_derivative_lt hp,
  exact ih _ this (this.trans_le $ nat.le_of_lt_succ hx) rfl
end

[Kevin Buzzard]

Thanks -- I'll think again.

[Eric Rodriguez]

maybe things become clearer if you subst h straight away

[Kevin Buzzard]

You're absolutely right, the key thing is generalizing (which I wasn't using two weeks ago) and it's giving me a goal which is basically a special case of IH. Thanks!

[Patrick Johnson]

Why not just use induction p using polynomial.degree_strong_induction as a custom induction principle?

import data.polynomial.derivative

open_locale polynomial
open polynomial

lemma polynomial.degree_strong_induction {R : Type*} [comm_semiring R]
  {P : polynomial R → Prop}
  (f : polynomial R)
  (ih : ∀ (n : ℕ),
  (∀ (m : ℕ), m < n → ∀ (q : polynomial R), q.nat_degree = m → P q) →
  ∀ (q : polynomial R), q.nat_degree = n → P q)
  : P f :=
begin
  induction h : f.nat_degree using nat.strong_induction_on generalizing f,
  apply ih; assumption,
end

lemma iterate_derivative_eq_zero {R} [comm_semiring R] {p : R[X]} {x : ℕ}
  (hx : p.nat_degree < x) :
  polynomial.derivative^[x] p = 0 :=
begin
  induction p using polynomial.degree_strong_induction with _ ih p h generalizing x,
  obtain ⟨t, rfl⟩ := nat.exists_eq_succ_of_ne_zero (pos_of_gt hx).ne',
  rw [function.iterate_succ_apply],
  by_cases hp : p.derivative = 0,
  { rw [hp, polynomial.iterate_derivative_zero] },
  have := nat_degree_derivative_lt hp, subst h,
  exact ih _ this _ rfl (this.trans_le (nat.le_of_lt_succ hx)),
end

[Eric Rodriguez]

i don't really see how that's really an improvement, and if we have one of those for each ℕ you may do induction on in the library I think we'll have a very long list

[Eric Wieser]

Perhaps we should allow induction rfl : foo to do the subst automatically?

[Eric Wieser]

Or perhaps even induction foo should do it for us when foo is more than a variable

[Antoine Chambert-Loir]

(Aside : docs#polynomial.nat_degree_derivative_lt could be generalized to the more natural :

theorem nat_degree_derivative_lt {p : R[X]} (hp : p.nat_degree ≠ 0) :
  p.derivative.nat_degree < p.nat_degree :=
begin
  cases dec_em (p.derivative = 0) with hp' hp',
  { rw [hp', polynomial.nat_degree_zero],
    exact pos_iff_ne_zero.mpr hp },
  { have hp1 : p ≠ 0,
    { intro h, apply hp, rw [h, polynomial.nat_degree_zero] },
  rw ← with_bot.some_lt_some,
  rw [nat_degree, option.get_or_else_of_ne_none $ mt degree_eq_bot.1 hp',
    nat_degree, option.get_or_else_of_ne_none $ mt degree_eq_bot.1 hp1],
  exact degree_derivative_lt hp1 }
end

[Eric Rodriguez]

these are equivalent under mt+ docs#polynomial.nat_degree_eq_zero_of_derivative_eq_zero, I guess

[Eric Rodriguez]

I'm currently tidying this file a little in #12833, maybe this is a change worth making though

[Junyan Xu]

Equivalent only with the char_zero assumption. nat_degree_derivative_lt is indeed more general.

[Antoine Chambert-Loir]

@Eric Rodriguez , as @Junyan Xu says, one can have $P'=0$ even if $\deg(P)\neq0$. A standard example is $T^p$ in characteristic $p$, but there are many other cases.

[Eric Rodriguez]

Oh, d'ah, I talked about this in another thread, too! I'll update this, thanks!

[Eric Rodriguez]

PR'd this in #12856!

Antoine Chambert-Loir said:

(Aside : docs#polynomial.nat_degree_derivative_lt could be generalized to the more natural :

theorem nat_degree_derivative_lt {p : R[X]} (hp : p.nat_degree ≠ 0) :
  p.derivative.nat_degree < p.nat_degree :=
begin
  cases dec_em (p.derivative = 0) with hp' hp',
  { rw [hp', polynomial.nat_degree_zero],
    exact pos_iff_ne_zero.mpr hp },
  { have hp1 : p ≠ 0,
    { intro h, apply hp, rw [h, polynomial.nat_degree_zero] },
  rw ← with_bot.some_lt_some,
  rw [nat_degree, option.get_or_else_of_ne_none $ mt degree_eq_bot.1 hp',
    nat_degree, option.get_or_else_of_ne_none $ mt degree_eq_bot.1 hp1],
  exact degree_derivative_lt hp1 }
end