9.4. Structural queries🔗

These queries read back the data a caller needs without exposing the array invariant. Hex.DensePoly.size is the stored coefficient count: one more than the degree for a nonzero polynomial, and 0 for the zero polynomial. Hex.DensePoly.degree? turns that into an optional degree.

def

Hex.DensePoly.size.{u} {R : Type u} [Zero R] [DecidableEq R]
  (p : Hex.DensePoly R) : ℕ
Hex.DensePoly.size.{u} {R : Type u}
  [Zero R] [DecidableEq R]
  (p : Hex.DensePoly R) : ℕ

The number of stored coefficients. For a normalized polynomial this is one more than the degree, except for the zero polynomial where it is 0.

def

Hex.DensePoly.isZero.{u} {R : Type u} [Zero R] [DecidableEq R]
  (p : Hex.DensePoly R) : Bool
Hex.DensePoly.isZero.{u} {R : Type u}
  [Zero R] [DecidableEq R]
  (p : Hex.DensePoly R) : Bool

true exactly when the polynomial is zero.

def

Hex.DensePoly.coeff.{u} {R : Type u} [Zero R] [DecidableEq R]
  (p : Hex.DensePoly R) (n : ℕ) : R
Hex.DensePoly.coeff.{u} {R : Type u}
  [Zero R] [DecidableEq R]
  (p : Hex.DensePoly R) (n : ℕ) : R

The coefficient of x^n, defaulting to 0 when n is out of range.

def

Hex.DensePoly.degree?.{u} {R : Type u} [Zero R] [DecidableEq R]
  (p : Hex.DensePoly R) : Option ℕ
Hex.DensePoly.degree?.{u} {R : Type u}
  [Zero R] [DecidableEq R]
  (p : Hex.DensePoly R) : Option ℕ

The largest exponent with a stored coefficient, or none for the zero polynomial.

def

Hex.DensePoly.support.{u} {R : Type u} [Zero R] [DecidableEq R]
  (p : Hex.DensePoly R) : List ℕ
Hex.DensePoly.support.{u} {R : Type u}
  [Zero R] [DecidableEq R]
  (p : Hex.DensePoly R) : List ℕ

The support of a dense polynomial, listed in ascending degree order.

def

Hex.DensePoly.toArray.{u} {R : Type u} [Zero R] [DecidableEq R]
  (p : Hex.DensePoly R) : Array R
Hex.DensePoly.toArray.{u} {R : Type u}
  [Zero R] [DecidableEq R]
  (p : Hex.DensePoly R) : Array R

Return the underlying normalized coefficient array.

The coefficient function is characterised against each constructor, so proofs and simp can read coefficients off ofCoeffs, C, and monomial without unfolding normalization:

theorem

Hex.DensePoly.coeff_ofCoeffs.{u} {R : Type u} [Zero R] [DecidableEq R]
  (coeffs : Array R) (n : ℕ) :
  (Hex.DensePoly.ofCoeffs coeffs).coeff n = coeffs.getD n Zero.zero
Hex.DensePoly.coeff_ofCoeffs.{u}
  {R : Type u} [Zero R] [DecidableEq R]
  (coeffs : Array R) (n : ℕ) :
  (Hex.DensePoly.ofCoeffs coeffs).coeff
      n =
    coeffs.getD n Zero.zero

Coefficient of ofCoeffs arr agrees with arr.getD _ 0: trimming trailing zeros does not change the value at any index.

theorem

Hex.DensePoly.coeff_C.{u} {R : Type u} [Zero R] [DecidableEq R] (c : R)
  (n : ℕ) : (Hex.DensePoly.C c).coeff n = if n = 0 then c else Zero.zero
Hex.DensePoly.coeff_C.{u} {R : Type u}
  [Zero R] [DecidableEq R] (c : R)
  (n : ℕ) :
  (Hex.DensePoly.C c).coeff n =
    if n = 0 then c else Zero.zero

Characterising lemma for the constant polynomial: its coefficient is c at degree 0, zero elsewhere.

theorem

Hex.DensePoly.coeff_monomial.{u} {R : Type u} [Zero R] [DecidableEq R]
  (n : ℕ) (c : R) (i : ℕ) :
  (Hex.DensePoly.monomial n c).coeff i = if i = n then c else Zero.zero
Hex.DensePoly.coeff_monomial.{u}
  {R : Type u} [Zero R] [DecidableEq R]
  (n : ℕ) (c : R) (i : ℕ) :
  (Hex.DensePoly.monomial n c).coeff i =
    if i = n then c else Zero.zero

Characterising lemma for monomials: monomial n c has coefficient c at degree n and zero elsewhere, even when c = 0 (in which case the polynomial is zero and every coefficient is 0).