# ** 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 #

(notes)

# - 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 list of coefficients (increasing degrees) - A normalized (i.e. no trailing 0) sequence of coefficients << Record polynomial (R : ringType) := Polynomial {polyseq :> seq R; _ : last 1 polyseq != 0}. >> #

# *) Open Scope ring_scope. Check Polynomial. Variable R: ringType. Variable x :R. Fact hs: last 1 [::1;x;0;1 ] != 0. rewrite /=. exact: GRing.oner_neq0. Qed. Definition P := Polynomial hs. (** #

# #

# ** 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 #

# #

(notes)

# Look theorems ans definitions about size, lead_coef in poly.v #

# *) Check (size P). Eval compute in (size P). Eval compute in P`_1. Definition deg (Q : polynomial R):= ((size Q) - 1)%N. (** #

# #

# ** 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 P1 := Poly [::1;x;0;x]. Check 'X. Check (x*:'X + 1%:P). (** #

# #

# ** 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 #

# *) Let P2: {poly R}:= \poly_(i < 10 ) i%:R. Definition add_poly (p q : {poly R}) := \poly_(i < maxn (size p) (size q)) (p`_i + q`_i). (* multiplication *) Definition mul_poly (p q : {poly R}) := \poly_(i < (size p + size q).-1) (\sum_(j < i.+1) p`_j * q`_(i - j)). (** #

# #

# ** 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 #

# *) Fixpoint horner s (x:R) := if s is a :: s' then horner s' x * x + a else 0. Notation "p .[ x ]" := (horner p x). (** #

# #

# ** Properties of coefficients - Lifting a ring predicate to polynomials. #

# *) Definition polyOver (S : {pred R}) := [qualify a p : {poly R} | all (mem S) p]. Lemma polyOver_poly (S : {pred R}) n E : (forall i, (i < n)%N -> E i \in S) -> \poly_(i < n) E i \is a polyOver S. Admitted. (** #

# #

# ** polyOver's lemmas - predicate associate to S: at least an addrPred - polyOver0 - polyOverC - polyOverX - rpred* (from ssralg) #

# *) Check polyOver0. (** #

# #

# ** Derivative - definition - notation - properties #

# *) Definition deriv (p:{poly R}) := \poly_(i < (size p).-1) (p`_i.+1 *+ i.+1). Local Notation "p ^` ()" := (deriv p). Fact deriv_is_linear : linear deriv. Admitted. Lemma derivM p q : (p * q)^`() = p^`() * q + p * q^`(). Admitted. Definition derivn n p := iter n deriv p. Notation "p ^` ( n )" := (derivn n p) : ring_scope. Check polyOver_deriv. (** #

# #

# ** Roots - root p x == x is a root of p #

# *) Definition root p : pred R := fun x => p.[x] == 0. Theorem factor_theorem p a : reflect (exists q, p = q * ('X - a%:P)) (root p a). Admitted. Theorem max_poly_roots (p: {poly R}) rs : p != 0 -> all (root p) rs -> uniq rs -> (size rs < size p)%N. Admitted. (** #

# #