McCoy's theorem

Stream: maths

[Johan Commelin]

In #12950, @Riccardo Brasca has a proof of McCoy's theorem, and I've been completely nerdsniped by it :see_no_evil:
Here is what I have now

import Mathlib.Algebra.Polynomial.RingDivision

open Polynomial

@[elab_as_elim]
lemma Nat.strongDecreasingInduction {P : ℕ → Prop}
    (base : ∃ n, ∀ m > n, P m) (step : ∀ n, (∀ m > n, P m) → P n) (n : ℕ) : P n := by
  apply Nat.decreasing_induction_of_not_bddAbove (P := fun n ↦ ∀ m ≥ n, P m) _ _ n n le_rfl
  · intro n ih m hm
    rcases hm.eq_or_lt with rfl | hm
    · exact step n ih
    · exact ih m hm
  · rintro ⟨b, hb⟩
    rcases base with ⟨n, hn⟩
    specialize @hb (n + b + 1) (fun m hm ↦ hn _ _)
    all_goals omega

variable {R : Type*} [CommSemiring R]

theorem McCoy (f : R[X]) (h : ∀ r : R, r • f = 0 → r = 0) :
    ∀ (g : R[X]), f * g = 0 → g = 0 := by
  intro g hg
  suffices ∀ i, f.coeff i • g = 0 by
    rw [← leadingCoeff_eq_zero]
    apply h
    simpa [ext_iff, mul_comm g.leadingCoeff] using fun i ↦ congr_arg (·.coeff g.natDegree) (this i)
  apply Nat.strongDecreasingInduction
  · use f.natDegree
    intro i hi
    rw [coeff_eq_zero_of_natDegree_lt hi, zero_smul]
  intro l IH
  obtain _|hl := (natDegree_smul_le (f.coeff l) g).lt_or_eq
  · apply McCoy f h (f.coeff l • g)
    rw [smul_eq_C_mul, mul_left_comm, hg, mul_zero]
  suffices f.coeff l * g.leadingCoeff = 0 by
    rwa [← leadingCoeff_eq_zero, ← coeff_natDegree, coeff_smul, hl, coeff_natDegree, smul_eq_mul]
  let m := g.natDegree
  suffices (f * g).coeff (l + m) = f.coeff l * g.leadingCoeff by rw [← this, hg, coeff_zero]
  rw [coeff_mul]
  apply Finset.sum_eq_single (l, m) _ (by simp)
  simp only [Finset.mem_antidiagonal, ne_eq, Prod.forall, Prod.mk.injEq, not_and]
  intro i j hij H
  obtain hi|rfl|hi := lt_trichotomy i l
  · have hj : m < j := by omega
    rw [coeff_eq_zero_of_natDegree_lt hj, mul_zero]
  · omega
  · rw [← coeff_C_mul, ← smul_eq_C_mul, IH _ hi, coeff_zero]
termination_by g => g.natDegree

[Johan Commelin]

1. Is this the right statement of Nat.strongDecreasingInduction or should we want a different statement there?
2. Can someone optimize this further?

[Riccardo Brasca]

I am having a look. Is this an improved version of your review?

[Johan Commelin]

Yes, modulo the fact that I'm not sure about that induction lemma

[Riccardo Brasca]

base and step seem a little too strong: it is enough that the statement holds for infinitely many n (this replace base) and that for all n we have P (n+1) → P n. Let me see if I can write down a proof.

[Johan Commelin]

Ooh, that version already exists.

[Johan Commelin]

But P (n+1) -> P n is annoying in the application.

[Riccardo Brasca]

Ah, even better. It is stronger than yours, isn't it?

[Johan Commelin]

This version gives a stronger IH.

[Riccardo Brasca]

Ops, you use it in the proof :D

[Riccardo Brasca]

Maybe I am missing something, but isn't your step strictly stronger than ∀ n, P (n + 1) → P n?

[Riccardo Brasca]

No, it is not.

[Ruben Van de Velde]

I don't think it should be camelCase if it eliminates into Prop

[Riccardo Brasca]

I was confused by the number of ∀, but assuming that ∀ n, (∀ m > n, P m) → P n is better than assuming ∀ n , P (n + 1) → P n (in the sense that it is weaker), sorry for the noise.

[Riccardo Brasca]

But this

@[elab_as_elim]
lemma Nat.strongDecreasingInduction {P : ℕ → Prop} (hP : ¬BddAbove {x | (fun n ↦ ∀ m ≥ n, P m) x})
  (step : ∀ n, (∀ m > n, P m) → P n) (n : ℕ) : P n := by
  refine Nat.decreasing_induction_of_not_bddAbove (fun n ih m hm ↦ ?_) hP n n le_rfl
  · rcases hm.eq_or_lt with rfl | hm
    · exact step n ih
    · exact ih m hm

is a better version, there is no need to assume that P holds starting at some point (it can even replace docs#Nat.decreasing_induction_of_not_bddAbove in my opinion).

[Johan Commelin]

@Riccardo Brasca That version looks good!

[Riccardo Brasca]

I am opening a PR replacing ∀ n, P (n + 1) → P n with your condition in all the results around docs#Nat.decreasing_induction_of_not_bddAbove

[Riccardo Brasca]

Actually I now think your version is better. In mine, it is the set x | (fun n ↦ ∀ m ≥ n, P m) x} that is unbounded, not x | P x}, and this seems a rather convoluted assumption.

[Riccardo Brasca]

Added directly in #12950