feat: Polynomial.coeffList (#9085)

`Polynomial.coeffList` is the list of coefficients, in descending order from leading term to constant term. (The zero polynomial has coeffList of `[]`). The PR defines coeffList and proves some basic facts, notably relating `P.coeffList` to `P.eraseLead.coeffList`.



Co-authored-by: Alex Meiburg <timeroot.alex@gmail.com>

Author: Timeroot

Mathlib.lean

@@ -899,6 +899,7 @@ import Mathlib.Algebra.Polynomial.Bivariate
 import Mathlib.Algebra.Polynomial.CancelLeads
 import Mathlib.Algebra.Polynomial.Cardinal
 import Mathlib.Algebra.Polynomial.Coeff
+import Mathlib.Algebra.Polynomial.CoeffList
 import Mathlib.Algebra.Polynomial.CoeffMem
 import Mathlib.Algebra.Polynomial.Degree.CardPowDegree
 import Mathlib.Algebra.Polynomial.Degree.Definitions

Mathlib/Algebra/Order/SuccPred.lean

@@ -8,6 +8,7 @@ import Mathlib.Algebra.Order.Monoid.Canonical.Defs
 import Mathlib.Algebra.Order.ZeroLEOne
 import Mathlib.Data.Int.Cast.Defs
 import Mathlib.Order.SuccPred.Limit
+import Mathlib.Order.SuccPred.WithBot
 
 /-!
 # Interaction between successors and arithmetic
@@ -187,6 +188,16 @@ theorem not_isSuccLimit_natCast [AddMonoidWithOne α] [SuccAddOrder α] [Canonic
     (n : ℕ) : ¬ IsSuccLimit (n : α) :=
   fun h ↦ (h.natCast_lt n).false
 
+@[simp]
+theorem succ_eq_zero [AddZeroClass α] [CanonicallyOrderedAdd α] [One α] [NoMaxOrder α]
+    [SuccAddOrder α] {a : WithBot α} : WithBot.succ a = 0 ↔ a = ⊥ := by
+  cases a
+  · simp [bot_eq_zero]
+  · rename_i a
+    simp only [WithBot.succ_coe, WithBot.coe_ne_bot, iff_false]
+    by_contra h
+    simpa [h] using max_of_succ_le (a := a)
+
 end PartialOrder
 
 section LinearOrder

Mathlib/Algebra/Polynomial/Coeff.lean

@@ -5,7 +5,6 @@ Authors: Chris Hughes, Johannes Hölzl, Kim Morrison, Jens Wagemaker
 -/
 import Mathlib.Algebra.MonoidAlgebra.Support
 import Mathlib.Algebra.Polynomial.Basic
-import Mathlib.Algebra.Regular.Basic
 import Mathlib.Data.Nat.Choose.Sum
 
 /-!

Mathlib/Algebra/Polynomial/CoeffList.lean

@@ -0,0 +1,177 @@
+/-
+Copyright (c) 2023 Alex Meiburg. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Alex Meiburg
+-/
+import Mathlib.Algebra.Polynomial.Degree.Definitions
+import Mathlib.Algebra.Polynomial.EraseLead
+import Mathlib.Data.List.Range
+
+/-!
+# A list of coefficients of a polynomial
+
+## Definition
+
+* `coeffList f`: a `List` of the coefficients, from leading term down to constant term.
+* `coeffList 0` is defined to be `[]`.
+
+This is useful for talking about polynomials in terms of list operations. It is "redundant" data in
+the sense that `Polynomial` is already a `Finsupp` (of its coefficients), and `Polynomial.coeff`
+turns this into a function, and these have exactly the same data as `coeffList`. The difference is
+that `coeffList` is intended for working together with list operations: getting `List.head`,
+comparing adjacent coefficients with each other, or anything that involves induction on Pollynomials
+by dropping the leading term (which is `Polynomial.eraseLead`).
+
+Note that `coeffList` _starts_ with the highest-degree terms and _ends_ with the constant term. This
+might seem backwards in the sense that `Polynomial.coeff` and `List.get!` are reversed to one
+another, but it means that induction on `List`s is the same as induction on
+`Polynomial.leadingCoeff`.
+
+The most significant theorem here is `coeffList_eraseLead`, which says that `coeffList P` can be
+written as `leadingCoeff P :: List.replicate k 0 ++ coeffList P.eraseLead`. That is, the list
+of coefficients starts with the leading coefficient, followed by some number of zeros, and then the
+coefficients of `P.eraseLead`.
+-/
+
+namespace Polynomial
+
+variable {R : Type*}
+
+section Semiring
+
+variable [Semiring R]
+
+/-- The list of coefficients starting from the leading term down to the constant term. -/
+def coeffList (P : R[X]) : List R :=
+  (List.range P.degree.succ).reverse.map P.coeff
+
+variable {P : R[X]}
+
+variable (R) in
+@[simp]
+theorem coeffList_zero : (0 : R[X]).coeffList = [] := by
+  simp [coeffList]
+
+/-- Only the zero polynomial has no coefficients. -/
+@[simp]
+theorem coeffList_eq_nil {P : R[X]} : P.coeffList = [] ↔ P = 0 := by
+  simp [coeffList]
+
+@[simp]
+theorem coeffList_C {x : R} (h : x ≠ 0) : (C x).coeffList = [x] := by
+  simp [coeffList, h, List.range_succ, degree_eq_natDegree (C_ne_zero.mpr h)]
+
+theorem coeffList_eq_cons_leadingCoeff (h : P ≠ 0) :
+    ∃ ls, P.coeffList = P.leadingCoeff :: ls := by
+  simp [coeffList, List.range_succ, withBotSucc_degree_eq_natDegree_add_one h]
+
+@[simp]
+theorem head?_coeffList (h : P ≠ 0) :
+    P.coeffList.head? = P.leadingCoeff :=
+  (coeffList_eq_cons_leadingCoeff h).casesOn fun _ ↦ (Eq.symm · ▸ rfl)
+
+@[simp] theorem head_coeffList (P : R[X]) (hP) :
+    P.coeffList.head hP = P.leadingCoeff :=
+  let h := coeffList_eq_nil.not.mp hP
+  (coeffList_eq_cons_leadingCoeff h).casesOn fun _ _ ↦
+    Option.some.injEq _ _ ▸ List.head?_eq_head _ ▸ head?_coeffList h
+
+theorem length_coeffList_eq_withBotSucc_degree (P : R[X]) : P.coeffList.length = P.degree.succ := by
+  simp [coeffList]
+
+@[simp]
+theorem length_coeffList_eq_ite [DecidableEq R] (P : R[X]) :
+    P.coeffList.length = if P = 0 then 0 else P.natDegree + 1 := by
+  by_cases h : P = 0 <;> simp [h, coeffList, withBotSucc_degree_eq_natDegree_add_one]
+
+theorem leadingCoeff_cons_eraseLead (h : P.nextCoeff ≠ 0) :
+    P.leadingCoeff :: P.eraseLead.coeffList = P.coeffList := by
+  have h₂ := ne_zero_of_natDegree_gt (natDegree_pos_of_nextCoeff_ne_zero h)
+  have h₃ := mt nextCoeff_eq_zero_of_eraseLead_eq_zero h
+  simpa [natDegree_eraseLead_add_one h, coeffList, withBotSucc_degree_eq_natDegree_add_one h₂,
+    withBotSucc_degree_eq_natDegree_add_one h₃, List.range_succ] using
+    (Polynomial.eraseLead_coeff_of_ne · ·.ne)
+
+@[simp]
+theorem coeffList_monomial {x : R} (hx : x ≠ 0) (n : ℕ) :
+    (monomial n x).coeffList = x :: List.replicate n 0 := by
+  have h := mt (Polynomial.monomial_eq_zero_iff x n).mp hx
+  apply List.ext_get (by classical simp [hx])
+  rintro (_|k) _ h₁
+  · exact (coeffList_eq_cons_leadingCoeff h).rec (by simp_all)
+  · rw [List.length_cons, List.length_replicate] at h₁
+    have : ((monomial n) x).natDegree.succ = n + 1 := by
+      simp [Polynomial.natDegree_monomial_eq n hx]
+    simpa [coeffList, withBotSucc_degree_eq_natDegree_add_one h]
+      using Polynomial.coeff_monomial_of_ne _ (by omega)
+
+/- Coefficients of a polynomial `P` are always the leading coefficient, some number of zeros, and
+then `coeffList P.eraseLead`. -/
+theorem coeffList_eraseLead (h : P ≠ 0) :
+    P.coeffList =
+      P.leadingCoeff :: (.replicate (P.natDegree - P.eraseLead.degree.succ) 0
+        ++ P.eraseLead.coeffList) := by
+  by_cases hdp : P.natDegree = 0
+  · rw [eq_C_of_natDegree_eq_zero hdp] at h ⊢
+    simp [coeffList_C (C_ne_zero.mp h)]
+  by_cases hep : P.eraseLead = 0
+  · have h₂ : .monomial P.natDegree P.leadingCoeff = P := by
+      simpa [hep] using P.eraseLead_add_monomial_natDegree_leadingCoeff
+    nth_rewrite 1 [← h₂]
+    simp [coeffList_monomial (Polynomial.leadingCoeff_ne_zero.mpr h), hep]
+  have h₁ := withBotSucc_degree_eq_natDegree_add_one h
+  have h₂ := withBotSucc_degree_eq_natDegree_add_one hep
+  obtain ⟨n, hn, hn2⟩ : ∃ d, P.natDegree = P.eraseLead.natDegree + 1 + d ∧
+      d = P.natDegree - P.eraseLead.degree.succ := by
+    use P.natDegree - P.eraseLead.natDegree -  1
+    have := eraseLead_natDegree_le P
+    omega
+  rw [← hn2]; clear hn2
+  apply List.ext_getElem?
+  rintro (_|k)
+  · obtain ⟨w,h⟩ := (coeffList_eq_cons_leadingCoeff h)
+    simp_all
+  simp only [coeffList, support_eq_empty, h, reduceIte, List.map_reverse, hep]
+  by_cases hkd : P.natDegree + 1 ≤ k + 1
+  · rw [List.getElem?_eq_none]
+      <;> simpa [hep, h] using by omega
+  obtain ⟨dk, hdk⟩ := exists_add_of_le (Nat.le_of_lt_succ (Nat.lt_of_not_le hkd))
+  rw [List.getElem?_reverse (by simpa [withBotSucc_degree_eq_natDegree_add_one h] using hkd),
+    List.getElem?_cons_succ, List.length_map, List.length_range, List.getElem?_map,
+    List.getElem?_range (by omega), Option.map_some']
+  conv_lhs => arg 1; equals P.eraseLead.coeff dk =>
+    rw [eraseLead_coeff_of_ne (f := P) dk (by omega)]
+    congr
+    omega
+  by_cases hkn : k < n
+  · simpa [List.getElem?_append, hkn] using coeff_eq_zero_of_natDegree_lt (by omega)
+  · rw [List.getElem?_append_right (List.length_replicate _ _ ▸ Nat.le_of_not_gt hkn),
+      List.length_replicate, List.getElem?_reverse, List.getElem?_map]
+    · rw [List.length_map, List.length_range,
+        List.getElem?_range (by omega), Option.map_some']
+      congr 2
+      omega
+    · simpa using by omega
+
+end Semiring
+section Ring
+variable [Ring R] (P : R[X])
+
+@[simp]
+theorem coeffList_neg : (-P).coeffList = P.coeffList.map (-·) := by
+  by_cases hp : P = 0
+  · rw [hp, coeffList_zero, neg_zero, coeffList_zero, List.map_nil]
+  · simp [coeffList, hp]
+
+end Ring
+
+section DivisionSemiring
+variable [DivisionSemiring R] (P : R[X])
+
+theorem coeffList_C_mul {x : R} (hx : x ≠ 0) : (C x * P).coeffList = P.coeffList.map (x * ·) := by
+  by_cases hp : P = 0
+  · simp [hp]
+  · simp [coeffList, Polynomial.degree_C hx]
+
+end DivisionSemiring
+end Polynomial

Mathlib/Algebra/Polynomial/Degree/Definitions.lean

@@ -7,6 +7,8 @@ import Mathlib.Algebra.MonoidAlgebra.Degree
 import Mathlib.Algebra.Order.Ring.WithTop
 import Mathlib.Algebra.Polynomial.Basic
 import Mathlib.Data.Nat.Cast.WithTop
+import Mathlib.Data.Nat.SuccPred
+import Mathlib.Order.SuccPred.WithBot
 
 /-!
 # Degree of univariate polynomials
@@ -240,6 +242,10 @@ theorem degree_X_le : degree (X : R[X]) ≤ 1 :=
 theorem natDegree_X_le : (X : R[X]).natDegree ≤ 1 :=
   natDegree_le_of_degree_le degree_X_le
 
+theorem withBotSucc_degree_eq_natDegree_add_one (h : p ≠ 0) : p.degree.succ = p.natDegree + 1 := by
+  rw [degree_eq_natDegree h]
+  exact WithBot.succ_coe p.natDegree
+
 end Semiring
 
 section NonzeroSemiring

Mathlib/Data/Nat/SuccPred.lean

@@ -5,11 +5,13 @@ Authors: Yaël Dillies
 -/
 import Mathlib.Algebra.Order.Group.Nat
 import Mathlib.Algebra.Ring.Nat
+import Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
 import Mathlib.Algebra.Order.Sub.Unbundled.Basic
 import Mathlib.Algebra.Order.SuccPred
 import Mathlib.Data.Fin.Basic
 import Mathlib.Order.Nat
 import Mathlib.Order.SuccPred.Archimedean
+import Mathlib.Order.SuccPred.WithBot
 
 /-!
 # Successors and predecessors of naturals
@@ -80,3 +82,9 @@ theorem Fin.coe_covBy_iff {n : ℕ} {a b : Fin n} : (a : ℕ) ⋖ b ↔ a ⋖ b
   and_congr_right' ⟨fun h _c hc => h hc, fun h c ha hb => @h ⟨c, hb.trans b.prop⟩ ha hb⟩
 
 alias ⟨_, CovBy.coe_fin⟩ := Fin.coe_covBy_iff
+
+@[simp]
+theorem withBotSucc_zero : WithBot.succ 0 = 1 := rfl
+
+@[simp]
+theorem withBotSucc_one : WithBot.succ 1 = 2 := rfl

Mathlib/Order/SuccPred/WithBot.lean

@@ -39,6 +39,21 @@ lemma succ_strictMono [NoMaxOrder α] : StrictMono (succ : WithBot α → α)
 @[gcongr] lemma succ_le_succ (hxy : x ≤ y) : x.succ ≤ y.succ := succ_mono hxy
 @[gcongr] lemma succ_lt_succ [NoMaxOrder α] (hxy : x < y) : x.succ < y.succ := succ_strictMono hxy
 
+section LinearOrder
+
+variable {α : Type*} [Nontrivial α] [LinearOrder α] [OrderBot α] [SuccOrder α]
+
+@[simp]
+theorem succ_eq_bot (a : WithBot α) : WithBot.succ a = ⊥ ↔ a = ⊥ := by
+  cases a
+  · simp
+  · simp only [WithBot.succ_coe, WithBot.coe_ne_bot, iff_false]
+    apply ne_of_gt
+    by_contra! h
+    have h₂ : _ = ⊥ := le_bot_iff.mp ((Order.le_succ _).trans h)
+    exact not_isMax_bot (h₂ ▸ Order.max_of_succ_le (h.trans bot_le))
+
+end LinearOrder
 end WithBot
 
 namespace WithTop
@@ -69,4 +84,19 @@ lemma pred_strictMono [NoMinOrder α] : StrictMono (pred : WithTop α → α)
 @[gcongr] lemma pred_le_pred (hxy : x ≤ y) : x.pred ≤ y.pred := pred_mono hxy
 @[gcongr] lemma pred_lt_pred [NoMinOrder α] (hxy : x < y) : x.pred < y.pred := pred_strictMono hxy
 
+section LinearOrder
+
+variable {α : Type*} [Nontrivial α] [LinearOrder α] [OrderTop α] [PredOrder α]
+
+@[simp]
+theorem pred_eq_top (a : WithTop α) : WithTop.pred a = ⊤ ↔ a = ⊤ := by
+  cases a
+  · simp
+  · simp only [WithTop.pred_coe, WithTop.coe_ne_top, iff_false]
+    apply ne_of_lt
+    by_contra! h
+    have h₂ : _ = ⊤ := top_le_iff.mp (h.trans (Order.pred_le _))
+    exact not_isMin_top (h₂ ▸ Order.min_of_le_pred (le_top.trans h))
+
+end LinearOrder
 end WithTop