Raw Computable Univariate Polynomials

Core definitions for array-backed computable univariate polynomials.

@[reducible, inline, specialize #[]]

def CompPoly.CPolynomial.Raw (R : Type u_1) : Type u_1

A type analogous to Polynomial that supports computable operations. This is defined to be a wrapper around Array.

For example, the Array #[1,2,3] represents the polynomial 1 + 2x + 3x^2. Two arrays may represent the same polynomial via zero-padding, for example #[1,2,3] = #[1,2,3,0,0,0,...].

@[reducible]

def CompPoly.CPolynomial.Raw.mk {R : Type u_1} (coeffs : Array R) : Raw R

Construct a CPolynomial.Raw from an array of coefficients.

@[reducible]

def CompPoly.CPolynomial.Raw.coeffs {R : Type u_1} (p : Raw R) : Array R

Extract the underlying array of coefficients.

@[reducible]

def CompPoly.CPolynomial.Raw.coeff {R : Type u_1} [Zero R] (p : Raw R) (i : ℕ) : R

The coefficient of X^i in the polynomial. Returns 0 if i is out of bounds.

def CompPoly.CPolynomial.Raw.C {R : Type u_1} (r : R) : Raw R

The constant polynomial C r.

def CompPoly.CPolynomial.Raw.X {R : Type u_1} [Zero R] [One R] : Raw R

The variable X.

def CompPoly.CPolynomial.Raw.monomial {R : Type u_1} [Zero R] [DecidableEq R] (n : ℕ) (c : R) : Raw R

Construct a monomial c * X^n as a CPolynomial.Raw R.

The result is an array with n zeros followed by c. For example, monomial 2 3 = #[0, 0, 3] represents 3 * X^2.

Note: If c = 0, this returns #[] (the zero polynomial).

def CompPoly.CPolynomial.Raw.lastNonzero {R : Type u_1} [Zero R] [BEq R] (p : Raw R) : Option (Fin (Array.size p))

Return the index of the last non-zero coefficient of a CPolynomial.Raw

def CompPoly.CPolynomial.Raw.trim {R : Type u_1} [Zero R] [BEq R] (p : Raw R) : Raw R

Remove trailing zeroes from a CPolynomial.Raw. Requires BEq to check if the coefficients are zero.

def CompPoly.CPolynomial.Raw.degree {R : Type u_1} [Zero R] [BEq R] (p : Raw R) : WithBot ℕ

Return the degree of a CPolynomial.Raw.

def CompPoly.CPolynomial.Raw.natDegree {R : Type u_1} [Zero R] [BEq R] (p : Raw R) : ℕ

Natural number degree of a CPolynomial.Raw.

Returns the degree as a natural number. For the zero polynomial, returns 0. This matches Mathlib's Polynomial.natDegree API.

def CompPoly.CPolynomial.Raw.leadingCoeff {R : Type u_1} [Zero R] [BEq R] (p : Raw R) : R

Return the leading coefficient of a CPolynomial.Raw as the last coefficient of the trimmed array, or 0 if the trimmed array is empty.

def CompPoly.CPolynomial.Raw.IsCanonical {R : Type u_1} [Zero R] (p : Raw R) : Prop

Semantic canonicality for raw coefficient arrays: a polynomial is canonical iff its last stored coefficient, when present, is nonzero. This invariant is independent of any particular BEq instance.

def CompPoly.CPolynomial.Raw.canonical {R : Type u_1} [Zero R] [BEq R] (p : Raw R) : Prop

A polynomial is canonical if it has no trailing zeros, i.e. p.trim = p.

theorem CompPoly.CPolynomial.Raw.Trim.lastNonzero_none {R : Type u_1} [Zero R] [BEq R] [LawfulBEq R] {p : Raw R} : (∀ (i : ℕ) (hi : i < Array.size p), p[i] = 0) → p.lastNonzero = none

If all coefficients are zero, lastNonzero is none.

theorem CompPoly.CPolynomial.Raw.Trim.lastNonzero_some {R : Type u_1} [Zero R] [BEq R] [LawfulBEq R] {p : Raw R} {i : ℕ} (hi : i < Array.size p) (h : p[i] ≠ 0) : ∃ (k : Fin (Array.size p)), p.lastNonzero = some k

If there is a non-zero coefficient, lastNonzero is some.

theorem CompPoly.CPolynomial.Raw.Trim.lastNonzero_spec {R : Type u_1} [Zero R] [BEq R] [LawfulBEq R] {p : Raw R} {k : Fin (Array.size p)} : p.lastNonzero = some k → p[k] ≠ 0 ∧ ∀ (j : ℕ) (hj : j < Array.size p), j > ↑k → p[j] = 0

lastNonzero returns the largest index with a non-zero coefficient.

def CompPoly.CPolynomial.Raw.Trim.lastNonzeroProp {R : Type u_1} [Zero R] {p : Raw R} (k : Fin (Array.size p)) : Prop

The property that an index is the last non-zero coefficient.

theorem CompPoly.CPolynomial.Raw.Trim.lastNonzero_unique {Q : Type u_2} [Zero Q] {p : Raw Q} {k k' : Fin (Array.size p)} : lastNonzeroProp k → lastNonzeroProp k' → k = k'

The last non-zero index is unique.

theorem CompPoly.CPolynomial.Raw.Trim.lastNonzero_some_iff {R : Type u_1} [Zero R] [BEq R] [LawfulBEq R] {p : Raw R} {k : Fin (Array.size p)} : p.lastNonzero = some k ↔ p[k] ≠ 0 ∧ ∀ (j : ℕ) (hj : j < Array.size p), j > ↑k → p[j] = 0

Characterization of lastNonzero via lastNonzeroProp.

theorem CompPoly.CPolynomial.Raw.Trim.lastNonzero_induct {R : Type u_1} [Zero R] [BEq R] [LawfulBEq R] {motive : Raw R → Prop} (case1 : ∀ (p : Raw R), p.lastNonzero = none → (∀ (i : ℕ) (hi : i < Array.size p), p[i] = 0) → motive p) (case2 : ∀ (p : Raw R) (k : Fin (Array.size p)), p.lastNonzero = some k → p[k] ≠ 0 → (∀ (j : ℕ) (hj : j < Array.size p), j > ↑k → p[j] = 0) → motive p) (p : Raw R) : motive p

eliminator for p.lastNonzero, e.g. use with the induction tactic as follows:

induction p using lastNonzero_induct with
| case1 p h_none h_all_zero => ...
| case2 p k h_some h_nonzero h_max => ...

theorem CompPoly.CPolynomial.Raw.Trim.induct {R : Type u_1} [Zero R] [BEq R] [LawfulBEq R] {motive : Raw R → Prop} (case1 : ∀ (p : Raw R), p.trim = #[] → (∀ (i : ℕ) (hi : i < Array.size p), p[i] = 0) → motive p) (case2 : ∀ (p : Raw R) (k : Fin (Array.size p)), p.trim = Array.extract p 0 (↑k + 1) → p[k] ≠ 0 → (∀ (j : ℕ) (hj : j < Array.size p), j > ↑k → p[j] = 0) → motive p) (p : Raw R) : motive p

eliminator for p.trim; use with the induction tactic as follows:

induction p using induct with
| case1 p h_empty h_all_zero => ...
| case2 p k h_extract h_nonzero h_max => ...

theorem CompPoly.CPolynomial.Raw.Trim.elim {R : Type u_1} [Zero R] [BEq R] [LawfulBEq R] (p : Raw R) : (p.trim = #[] ∧ ∀ (i : ℕ) (hi : i < Array.size p), p[i] = 0) ∨ ∃ (k : Fin (Array.size p)), p.trim = Array.extract p 0 (↑k + 1) ∧ p[k] ≠ 0 ∧ ∀ (j : ℕ) (hj : j < Array.size p), j > ↑k → p[j] = 0

eliminator for p.trim; e.g. use for case distinction as follows:

rcases (Trim.elim p) with ⟨ h_empty, h_all_zero ⟩ | ⟨ k, h_extract, h_nonzero, h_max ⟩

theorem CompPoly.CPolynomial.Raw.Trim.size_eq_degree_plus_one {R : Type u_1} [Zero R] [BEq R] (p : Raw R) (h_trim : p.trim ≠ mk #[]) : ↑(Array.size p.trim) = p.degree + 1

theorem CompPoly.CPolynomial.Raw.Trim.size_eq_natDegree_plus_one {R : Type u_1} [Zero R] [BEq R] (p : Raw R) (h_trim : p.trim ≠ mk #[]) : Array.size p.trim = p.natDegree + 1

theorem CompPoly.CPolynomial.Raw.Trim.size_eq_natDegree_of_zero {R : Type u_1} [Zero R] [BEq R] (p : Raw R) (h_trim : p.trim = mk #[]) : Array.size p.trim = p.natDegree

theorem CompPoly.CPolynomial.Raw.Trim.size_le_size {R : Type u_1} [Zero R] [BEq R] (p : Raw R) : Array.size p.trim ≤ Array.size p

theorem CompPoly.CPolynomial.Raw.Trim.coeff_eq_getElem_of_lt {R : Type u_1} [Zero R] [BEq R] [LawfulBEq R] {p : Raw R} {i : ℕ} (hi : i < Array.size p) : p.trim.coeff i = p[i]

theorem CompPoly.CPolynomial.Raw.Trim.coeff_eq_coeff {R : Type u_1} [Zero R] [BEq R] [LawfulBEq R] (p : Raw R) (i : ℕ) : p.trim.coeff i = p.coeff i

theorem CompPoly.CPolynomial.Raw.Trim.coeff_eq_getElem {Q : Type u_2} [Zero Q] {p : Raw Q} {i : ℕ} (hp : i < Array.size p) : p.coeff i = p[i]

def CompPoly.CPolynomial.Raw.Trim.equiv {R : Type u_1} [Zero R] (p q : Raw R) : Prop

Equivalence relation: two polynomials are equivalent if all coefficients agree.

theorem CompPoly.CPolynomial.Raw.Trim.coeff_eq_zero {Q : Type u_2} [Zero Q] {p : Raw Q} : (∀ (i : ℕ) (hi : i < Array.size p), p[i] = 0) ↔ ∀ (i : ℕ), p.coeff i = 0

theorem CompPoly.CPolynomial.Raw.Trim.eq_degree_of_equiv {R : Type u_1} [Zero R] [BEq R] [LawfulBEq R] {p q : Raw R} : equiv p q → p.degree = q.degree

theorem CompPoly.CPolynomial.Raw.Trim.eq_of_equiv {R : Type u_1} [Zero R] [BEq R] [LawfulBEq R] {p q : Raw R} : equiv p q → p.trim = q.trim

theorem CompPoly.CPolynomial.Raw.Trim.trim_equiv {R : Type u_1} [Zero R] [BEq R] [LawfulBEq R] (p : Raw R) : equiv p.trim p

theorem CompPoly.CPolynomial.Raw.Trim.trim_twice {R : Type u_1} [Zero R] [BEq R] [LawfulBEq R] (p : Raw R) : p.trim.trim = p.trim

theorem CompPoly.CPolynomial.Raw.Trim.canonical_empty {R : Type u_1} [Zero R] [BEq R] : (mk #[]).trim = #[]

theorem CompPoly.CPolynomial.Raw.Trim.canonical_of_size_zero {R : Type u_1} [Zero R] [BEq R] {p : Raw R} : Array.size p = 0 → p.trim = p

theorem CompPoly.CPolynomial.Raw.Trim.canonical_nonempty_iff {R : Type u_1} [Zero R] [BEq R] [LawfulBEq R] {p : Raw R} (hp : Array.size p > 0) : p.trim = p ↔ p.lastNonzero = some ⟨Array.size p - 1, ⋯⟩

theorem CompPoly.CPolynomial.Raw.Trim.lastNonzero_last_iff {R : Type u_1} [Zero R] [BEq R] [LawfulBEq R] {p : Raw R} (hp : Array.size p > 0) : p.lastNonzero = some ⟨Array.size p - 1, ⋯⟩ ↔ Array.getLast p hp ≠ 0

theorem CompPoly.CPolynomial.Raw.Trim.canonical_iff {R : Type u_1} [Zero R] [BEq R] [LawfulBEq R] {p : Raw R} : p.trim = p ↔ p.IsCanonical

theorem CompPoly.CPolynomial.Raw.Trim.isCanonical_empty {R : Type u_1} [Zero R] : (mk #[]).IsCanonical

theorem CompPoly.CPolynomial.Raw.Trim.isCanonical_of_size_zero {R : Type u_1} [Zero R] {p : Raw R} (hp : Array.size p = 0) : p.IsCanonical

theorem CompPoly.CPolynomial.Raw.Trim.isCanonical_iff_trim_eq {R : Type u_1} [Zero R] [BEq R] [LawfulBEq R] {p : Raw R} : p.IsCanonical ↔ p.trim = p

Canonicality bridge (semantic view to computational view).

theorem CompPoly.CPolynomial.Raw.Trim.isCanonical_iff_size_eq_zero_or_getLastD_ne_zero {R : Type u_1} [Zero R] {p : Raw R} : p.IsCanonical ↔ Array.size p = 0 ∨ Array.getLastD p 0 ≠ 0

Non-dependent canonicality criterion using getLastD.

theorem CompPoly.CPolynomial.Raw.Trim.trim_eq_iff_size_eq_zero_or_getLastD_ne_zero {R : Type u_1} [Zero R] [BEq R] [LawfulBEq R] {p : Raw R} : p.trim = p ↔ Array.size p = 0 ∨ Array.getLastD p 0 ≠ 0

Computational canonicality criterion in non-dependent form.

theorem CompPoly.CPolynomial.Raw.Trim.trim_eq_of_isCanonical {R : Type u_1} [Zero R] [BEq R] [LawfulBEq R] {p : Raw R} (hp : p.IsCanonical) : p.trim = p

theorem CompPoly.CPolynomial.Raw.Trim.isCanonical_of_trim_eq {R : Type u_1} [Zero R] [BEq R] [LawfulBEq R] {p : Raw R} (hp : p.trim = p) : p.IsCanonical

theorem CompPoly.CPolynomial.Raw.Trim.isCanonical_trim {R : Type u_1} [Zero R] [BEq R] [LawfulBEq R] (p : Raw R) : p.trim.IsCanonical

theorem CompPoly.CPolynomial.Raw.Trim.push_trim {R : Type u_1} [Zero R] [BEq R] [LawfulBEq R] (arr : Array R) (c : R) : ¬c = 0 → trim (arr.push c) = arr.push c

theorem CompPoly.CPolynomial.Raw.Trim.non_zero_map {R : Type u_1} [Zero R] [BEq R] [LawfulBEq R] (f : R → R) (hf : ∀ (r : R), f r = 0 → r = 0) (p : Raw R) : have fp := mk (Array.map f p); p.trim = p → fp.trim = fp

theorem CompPoly.CPolynomial.Raw.Trim.canonical_ext {R : Type u_1} [Zero R] [BEq R] [LawfulBEq R] {p q : Raw R} (hp : p.trim = p) (hq : q.trim = q) : equiv p q → p = q

Canonical polynomials enjoy a stronger extensionality theorem: they just need to agree at all coefficients (without assuming equal sizes)

theorem CompPoly.CPolynomial.Raw.Trim.isCanonical_ext {R : Type u_1} [Zero R] [BEq R] [LawfulBEq R] {p q : Raw R} (hp : p.IsCanonical) (hq : q.IsCanonical) : equiv p q → p = q