To play this document inside your browser use ALT-N and ALT-P. If you get stack overflow errors, try to use Google Chrome or Chromium with the command line option --js-flags="--harmony-tailcalls".

You can save your edits inside your browser and load them back (edits are also saved when you close the window). Finally you can download the file for offline editing.

The Polynomials Library :

poly.v

  • A library for univariate polynomials over ring structures
  • with extensions for polynomials whose coefficients range over
    • commutative rings
    • integral domains

The Polynomials

Roadmap of the lesson:

  • Definitions
  • Ring Structure
  • Evaluation
  • Derivative
  • Roots

Definition

  • P = a_n X^n + ... + a_2 X^2 + a_1 X + a_0
    • list of coefficients (decreasing/increasing degrees)
    • list of pairs (degree, coef)

Math Components library choice:

  • P = a_0 + a_1 X + a_2 X^2 + ... + a_n X^n
    • A normalized (i.e. no trailing 0) sequence of coefficients

Record polynomial (R : ringType) := Polynomial {polyseq :> seq R; _ : last 1 polyseq != 0}.

First properties

Polynomials are coercible to sequences:

  • one can directly take the k_th element of a polynomial
    • P'_k i.e. retrieve the coefficient of X^k in P.

  • size of a polynomial
  • the degree of a polynomial is its size minus 1

Notations

  • {poly R}: polynomials over R (a Ring)
  • Poly s : the polynomial built from sequence s
  • 'X: monomial
  • 'X^n : monomial to the power of n
  • a%:P : constant polynomial
  • standard notations of ssralg (+, -, *, *:, ^+)

Definition by extension

  • \poly(i < n) E i is the polynomial:
    • (E 0) + (E 1) *: 'X + ... + E (n - 1) *: 'X^(n-1)

Ring Structure

  • addition
  • multiplication

The ring of polynomials

  • The type of polynomials has been equipped with a (commutative / integral) ring structure.

  • All related lemmas of ssralg can be used.

Evaluation of polynomials

  • Warning: type of x

Properties of coefficients

  • Lifting a ring predicate to polynomials.

polyOver's lemmas

  • predicate associate to S: at least an addrPred
    • polyOver0
    • polyOverC
    • polyOverX
    • rpred* (from ssralg)

Derivative

  • definition
  • notation
  • properties

Roots

  • root p x == x is a root of p

Division

  • division and its theory are in the polydiv.v file