Library poly

This file provides a library for univariate polynomials over ring          
 structures; it also provides an extended theory for polynomials whose      
 coefficients range over commutative rings and integral domains.            



{poly R} == the type of polynomials with coefficients of type R, represented as lists with a non zero last element (big endian representation); the coeficient type R must have a canonical ringType structure cR. In fact {poly R} denotes the concrete type polynomial cR; R is just a phantom argument that lets type inference reconstruct the (hidden) ringType structure cR. p : seq R == the big-endian sequence of coefficients of p, via the coercion polyseq: polynomial >-> seq. Poly s == the polynomial with coefficient sequence s (ignoring trailing zeroes). \poly_(i < n) E(i) == the polynomial of degree at most n - 1 whose coefficients are given by the general term E(i) 0, 1, -p, p + q, == the usual ring operations: {poly R} has a canonical p * q, p ^+ n, ... ringType structure, which is commutative / integral when R is commutative / integral, respectively. c%:P == the constant polynomial c 'X == the (unique) variable 'X^n == a power of 'X; 'X^0 is 1, 'X^1 is convertible to 'X p`_i == the coefficient of 'X^i in p; this is in fact just the ring_scope notation generic seq-indexing using nth 0%R, combined with the polyseq coercion. size p == 1 + the degree of p, or 0 if p = 0 (this is the generic seq function combined with polyseq). lead_coef p == the coefficient of the highest monomial in p, or 0 if p = 0 (hence lead_coef p = 0 iff p = 0) monic p == p is monic, i.e., lead_coef p = 1 (0 is not monic) p.[x] == the evaluation of a polynomial p at a point x using the Horner scheme

The multi-rule horner_lin (resp. horner_lin_com)

unwinds horner evaluation of a polynomial expression (resp. in a non commutative ring, under appropriate assumptions). p^`() == formal derivative of p p^`(n) == formal n-derivative of p p^`N(n) == formal n-derivative of p divided by n! com_poly p x == x and p.[x] commute; this is a sufficient condition for evaluating (q * p).[x] as q.[x] * p.[x] when R is not commutative. com_coef p x == x commutes with all the coefficients of p (clearly, this implies com_poly p x). root p x == x is a root of p, i.e., p.[x] = 0 map_poly f p == the image of the polynomial by the function f (which should be a ring morphism). comm_ringM f u == u commutes with the image of f (i.e., with all f x) horner_morph f u == the function mapping p to the value of map_poly f p at u; this is a morphism from {poly R} to the image ring of f when f is a morphism and comm_ringM f u. We define pseudo division on polynomials over an integral domain : m %/ d == the pseudo-quotient m %% d == the pseudo remainder scalp m d == the scaling coefficient of the pseudo-division p %| q <=> q is a pseudo-divisor of p p %= q <=> p and q are equal up to a non-zero scalar factor := (p %| q) && (q %| p)

If R is a field, this means p and q are associate.

gcdp p q == pseudo-gcd of p and q. This is defined for p and q with coefficients in an arbitrary ring; however gcdp is only known to be idempotent and associative when R has an integral domain (idomainType) structure. diff_roots x y == x and y are distinct roots; if R is a field, this just means x != y, but this concept is generalized to the case where R is only a ring with units (i.e., a unitRingType); in which case it means that x and y commute, and that the difference x - y is a unit (i.e., has a multiplicative inverse) in R. to just x != y). uniq_roots s == s is a sequence or pairwise distinct roots, in the sense of diff_roots p above.

We only show that these operations and properties are transferred by

morphisms whose domain is a field (thus ensuring injectivity). We prove the factor_theorem, and the max_poly_roots inequality relating the number of distinct roots of a polynomial and its size.

Import Prenex Implicits.

Import GRing.Theory.
Open Local Scope ring_scope.

Reserved Notation "{ 'poly' T }" (at level 0, format "{ 'poly' T }").
Reserved Notation "c %:P" (at level 2, format "c %:P").
Reserved Notation "'X" (at level 0).
Reserved Notation "''X^' n" (at level 3, n at level 2, format "''X^' n").
Reserved Notation "\poly_ ( i < n ) E"
  (at level 36, E at level 36, i, n at level 50,
   format "\poly_ ( i < n ) E").
Reserved Notation "a ^`()"(at level 3, format "a ^`()").
Reserved Notation "a ^`( n )" (at level 3, format "a ^`( n )").
Reserved Notation "a ^`N( n )" (at level 3, format "a ^`N( n )").

Local Notation simp := Monoid.simpm.

Section Polynomial.

Variable R : ringType.

Defines a polynomial as a sequence with <> 0 last element 
Record polynomial := Polynomial {polyseq :> seq R; _ : last 1 polyseq != 0}.

Canonical Structure polynomial_subType :=
  Eval hnf in [subType for polyseq by polynomial_rect].
Definition polynomial_eqMixin := Eval hnf in [eqMixin of polynomial by <:].
Canonical Structure polynomial_eqType :=
  Eval hnf in EqType polynomial polynomial_eqMixin.
Definition polynomial_choiceMixin := [choiceMixin of polynomial by <:].
Canonical Structure polynomial_choiceType :=
  Eval hnf in ChoiceType polynomial polynomial_choiceMixin.

Lemma poly_inj : injective polyseq.

Definition poly_of of phant R := polynomial.
Identity Coercion type_poly_of : poly_of >-> polynomial.

End Polynomial.

We need to break off the section here to let the argument scope 
 directives take effect.                                         
Notation "{ 'poly' T }" := (poly_of (Phant T)).

Section PolynomialTheory.

Variable R : ringType.

Implicit Types p q : {poly R}.

Canonical Structure poly_subType := Eval hnf in [subType of {poly R}].
Canonical Structure poly_eqType := Eval hnf in [eqType of {poly R}].
Canonical Structure poly_choiceType := Eval hnf in [choiceType of {poly R}].

Definition lead_coef p := p`_(size p).-1.
Lemma lead_coefE : forall p, lead_coef p = p`_(size p).-1.

Definition polyC c : {poly R} :=
  insubd (@Polynomial R [::] (nonzero1r _)) [:: c].

Local Notation "c %:P" := (polyC c).

Remember the boolean (c !=0) is coerced to 1 if true and 0 if false 
Lemma polyseqC : forall c, c%:P = nseq (c != 0) c :> seq R.

Lemma size_polyC : forall c, size c%:P = (c != 0).

Lemma coefC : forall c i, c%:P`_i = if i == 0%N then c else 0.

Lemma polyC_inj : injective polyC.

Lemma lead_coefC : forall c, lead_coef c%:P = c.

Extensional interpretation (poly <=> nat -> R) 
Lemma polyP : forall p1 p2, nth 0 p1 =1 nth 0 p2 <-> p1 = p2.

Lemma size1_polyC : forall p, size p <= 1 -> p = (p`_0)%:P.

Builds a polynomial by extension. 
Definition poly_cons c p : {poly R} :=
  if p is Polynomial ((_ :: _) as s) ns then
     @Polynomial R (c :: s) ns
  else c%:P.

Lemma polyseq_cons : forall c p,
  poly_cons c p = (if size p != 0%N then c :: p else c%:P) :> seq R.

Lemma size_poly_cons : forall c p,
  size (poly_cons c p) =
    (if (size p == 0%N) && (c == 0) then 0%N else (size p).+1).

Lemma coef_cons : forall c p i,
  (poly_cons c p)`_i = if i == 0%N then c else p`_i.-1.

Builds a polynomial from a bare list of coefficients 
Definition Poly := foldr poly_cons 0%:P.

Lemma PolyK : forall c s, last c s != 0 -> Poly s = s :> seq R.

Lemma polyseqK : forall p, Poly p = p.

Lemma size_Poly : forall s, size (Poly s) <= size s.

Lemma coef_Poly : forall s i, (Poly s)`_i = s`_i.

Builds a polynomial from an infinite seq of coef and a bound 
Local Notation "\poly_ ( i < n ) E" := (Poly (mkseq (fun i : nat => E) n)).

Lemma polyseq_poly : forall n E,
  E n.-1 != 0 -> \poly_(i < n) E i = mkseq [eta E] n :> seq R.

Lemma size_poly : forall n E, size (\poly_(i < n) E i) <= n.

Lemma size_poly_eq : forall n E, E n.-1 != 0 -> size (\poly_(i < n) E i) = n.

Lemma coef_poly : forall n E k,
  (\poly_(i < n) E i)`_k = (if k < n then E k else 0).

Lemma lead_coef_poly : forall n E,
  n > 0 -> E n.-1 != 0 -> lead_coef (\poly_(i < n) E i) = E n.-1.

Lemma coefK : forall p, \poly_(i < size p) p`_i = p.

Zmodule structure for polynomial 
Definition add_poly p1 p2 :=
  \poly_(i < maxn (size p1) (size p2)) (p1`_i + p2`_i).

Definition opp_poly p := \poly_(i < size p) - p`_i.

Lemma coef_add_poly : forall p1 p2 i, (add_poly p1 p2)`_i = p1`_i + p2`_i.

Lemma coef_opp_poly : forall p i, (opp_poly p)`_i = - p`_i.

Lemma add_polyA : associative add_poly.

Lemma add_polyC : commutative add_poly.

Lemma add_poly0 : left_id 0%:P add_poly.

Lemma add_poly_opp : left_inverse 0%:P opp_poly add_poly.

Definition poly_zmodMixin :=
  ZmodMixin add_polyA add_polyC add_poly0 add_poly_opp.
Canonical Structure poly_zmodType :=
  Eval hnf in ZmodType {poly R} poly_zmodMixin.
Canonical Structure polynomial_zmodType :=
  Eval hnf in [zmodType of polynomial R for poly_zmodType].

Properties of the zero polynomial 

Lemma polyC0 : 0%:P = 0 :> {poly R}.

Lemma seq_poly0 : (0 : {poly R}) = [::] :> seq R.

Lemma size_poly0 : size (0 : {poly R}) = 0%N.

Lemma coef0 : forall i, (0 : {poly R})`_i = 0.

Lemma lead_coef0 : lead_coef 0 = 0.

Lemma size_poly_eq0 : forall p, (size p == 0%N) = (p == 0).

Lemma poly0Vpos : forall p, {p = 0} + {size p > 0}.

Lemma polySpred : forall p, p != 0 -> size p = (size p).-1.+1.

Lemma lead_coef_eq0 : forall p, (lead_coef p == 0) = (p == 0).

Lemma polyC_eq0 : forall c, (c%:P == 0) = (c == 0).

Size, leading coef, morphism properties of coef 
Lemma leq_size_coef : forall p i,
  (forall j, i <= j -> p`_j = 0) -> size p <= i.

Lemma leq_coef_size : forall p i, p`_i != 0 -> i < size p.

Lemma coef_add : forall p1 p2 i, (p1 + p2)`_i = p1`_i + p2`_i.

Lemma coef_opp : forall p i, (- p)`_i = - p`_i.

Lemma coef_sub : forall p1 p2 i, (p1 - p2)`_i = p1`_i - p2`_i.

Lemma coef_natmul : forall p n i, (p *+ n)`_i = p`_i *+ n.

Lemma coef_negmul : forall p n i, (p *- n)`_i = p`_i *- n.

Lemma coef_sum : forall I r (P : pred I) (F : I -> {poly R}) k,
  (\sum_(i <- r | P i) F i)`_k = \sum_(i <- r | P i) (F i)`_k.

Lemma polyC_add : {morph polyC : c1 c2 / c1 + c2}.

Lemma polyC_opp : {morph polyC : c / - c}.

Lemma polyC_sub : {morph polyC : c1 c2 / c1 - c2}.

Lemma polyC_natmul : forall n, {morph polyC : c / c *+ n}.

Lemma size_opp : forall p, size (- p) = size p.

Lemma lead_coef_opp : forall p, lead_coef (- p) = - lead_coef p.

Lemma size_add : forall p q, size (p + q) <= maxn (size p) (size q).

Lemma size_addl : forall p q, size p > size q -> size (p + q) = size p.

Lemma size_sum : forall I r (P : pred I) (F : I -> {poly R}),
  size (\sum_(i <- r | P i) F i) <= \max_(i <- r | P i) size (F i).

Lemma lead_coef_addl : forall p q,
  size p > size q -> lead_coef (p + q) = lead_coef p.

And now the Ring structure. 

Definition mul_poly p1 p2 :=
  \poly_(i < (size p1 + size p2).-1) (\sum_(j < i.+1) p1`_j * p2`_(i - j)).

Lemma coef_mul_poly : forall p1 p2 i,
  (mul_poly p1 p2)`_i = \sum_(j < i.+1) p1`_j * p2`_(i - j)%N.

Lemma coef_mul_poly_rev : forall p1 p2 i,
  (mul_poly p1 p2)`_i = \sum_(j < i.+1) p1`_(i - j)%N * p2`_j.

Lemma mul_polyA : associative mul_poly.

Lemma mul_1poly : left_id 1%:P mul_poly.

Lemma mul_poly1 : right_id 1%:P mul_poly.

Lemma mul_poly_addl : left_distributive mul_poly +%R.

Lemma mul_poly_addr : right_distributive mul_poly +%R.

Lemma nonzero_poly1 : 1%:P != 0.

Definition poly_ringMixin :=
  RingMixin mul_polyA mul_1poly mul_poly1 mul_poly_addl mul_poly_addr
            nonzero_poly1.
Canonical Structure poly_ringType :=
  Eval hnf in RingType {poly R} poly_ringMixin.
Canonical Structure polynomial_ringType :=
  Eval hnf in [ringType of polynomial R for poly_ringType].

Lemma polyC1 : 1%:P = 1.

Lemma polyseq1 : (1 : {poly R}) = [:: 1] :> seq R.

Lemma size_poly1 : size (1 : {poly R}) = 1%N.

Lemma coef1 : forall i, (1 : {poly R})`_i = (i == 0%N)%:R.

Lemma lead_coef1 : lead_coef 1 = 1.

Lemma coef_mul : forall p1 p2 i,
  (p1 * p2)`_i = \sum_(j < i.+1) p1`_j * p2`_(i - j)%N.

Lemma coef_mul_rev : forall p1 p2 i,
  (p1 * p2)`_i = \sum_(j < i.+1) p1`_(i - j)%N * p2`_j.

Lemma size_mul : forall p1 p2, size (p1 * p2) <= (size p1 + size p2).-1.

Lemma head_coef_mul : forall p q,
  (p * q)`_(size p + size q).-2 = lead_coef p * lead_coef q.

Lemma size_proper_mul : forall p q,
  lead_coef p * lead_coef q != 0 -> size (p * q) = (size p + size q).-1.

Lemma lead_coef_proper_mul : forall p q,
  let c := lead_coef p * lead_coef q in c != 0 -> lead_coef (p * q) = c.

Lemma size_exp : forall p n, size (p ^+ n) <= ((size p).-1 * n).+1.

Lemma coef_Cmul : forall c p i, (c%:P * p)`_i = c * p`_i.

Lemma coef_mulC : forall c p i, (p * c%:P)`_i = p`_i * c.

Lemma polyC_mul : {morph polyC : c1 c2 / c1 * c2}.

Lemma polyC_exp : forall n, {morph polyC : c / c ^+ n}.

Definition scale_poly a p := \poly_(i < size p) (a * p`_i).

Lemma scale_polyE: forall a p, scale_poly a p = a%:P * p.

Lemma scale_polyA : forall a b p,
  scale_poly a (scale_poly b p) = scale_poly (a * b) p.

Lemma scale_poly1 : left_id 1 scale_poly.

Lemma scale_poly_addr: forall a, {morph scale_poly a : p q / p + q}.

Lemma scale_poly_addl: forall p, {morph scale_poly^~ p : a b / a + b}.

Lemma scale_poly_mull: forall a p q, scale_poly a (p * q) = scale_poly a p * q.

Definition poly_lmodMixin :=
  LmodMixin scale_polyA scale_poly1 scale_poly_addr scale_poly_addl.
Canonical Structure poly_lmodType :=
  Eval hnf in LmodType R {poly R} poly_lmodMixin.
Canonical Structure polynomial_lmodType :=
  Eval hnf in [lmodType[R] of polynomial R for poly_lmodType].
Canonical Structure poly_ncalgebraType :=
  Eval hnf in NCalgebraType R {poly R} poly_lmodMixin scale_poly_mull.
Canonical Structure polynomial_ncalgebraType :=
  Eval hnf in [ncalgebraType[R] of polynomial R for poly_ncalgebraType].

Indeterminate, at last! 

Definition polyX := Poly [:: 0; 1].

Local Notation "'X" := polyX.

Lemma polyseqX : 'X = [:: 0; 1] :> seq R.

Lemma size_polyX : size 'X = 2.

Lemma coefX : forall i, 'X`_i = (i == 1%N)%:R.

Lemma lead_coefX : lead_coef 'X = 1.

Lemma comm_polyX : forall p, GRing.comm p 'X.

Lemma coef_mulX : forall p i, (p * 'X)`_i = (if (i == 0)%N then 0 else p`_i.-1).

Lemma coef_Xmul : forall p i, ('X * p)`_i = (if (i == 0)%N then 0 else p`_i.-1).

Lemma poly_cons_def : forall p a, poly_cons a p = p * 'X + a%:P.
Lemma size_amulX p c: size (p * 'X + c%:P) =
         if (size p == 0%N) && (c == 0) then 0%N else (size p).+1.

Lemma poly_ind : forall K : {poly R} -> Type,
  K 0 -> (forall p c, K p -> K (p * 'X + c%:P)) -> (forall p, K p).

Lemma seq_mul_polyX : forall p, p != 0 -> p * 'X = 0 :: p :> seq R.

Lemma lead_coef_mulX : forall p, lead_coef (p * 'X) = lead_coef p.

Local Notation "''X^' n" := ('X ^+ n).

Lemma coef_Xn : forall n i, 'X^n`_i = (i == n)%:R.

Lemma seq_polyXn : forall n, 'X^n = ncons n 0 [:: 1] :> seq R.

Lemma size_polyXn : forall n, size 'X^n = n.+1.

Lemma comm_polyXn : forall p n, GRing.comm p 'X^n.

Lemma lead_coefXn : forall n, lead_coef 'X^n = 1.

Lemma coef_Xn_mul : forall n p i,
  ('X^n * p)`_i = if i < n then 0 else p`_(i - n).

Lemma coef_mulXn : forall n p i,
  (p * 'X^n)`_i = if i < n then 0 else p`_(i - n).

Expansion of a polynomial as an indexed sum 
Lemma poly_def : forall n E, \poly_(i < n) E i = \sum_(i < n) (E i)%:P * 'X^i.

Monic predicate 

Definition monic p := lead_coef p == 1.

Lemma monic1 : monic 1.

Lemma monicX : monic 'X.

Lemma monicXn : forall n, monic 'X^n.

Lemma monic_neq0 : forall p, monic p -> p != 0.

Lemma lead_coef_monic_mul : forall p q,
  monic p -> lead_coef (p * q) = lead_coef q.

Lemma lead_coef_mul_monic : forall p q,
  monic q -> lead_coef (p * q) = lead_coef p.

Lemma size_monic_mul : forall p q,
  monic p -> q != 0 -> size (p * q) = (size p + size q).-1.

Lemma size_mul_monic : forall p q,
  p != 0 -> monic q -> size (p * q) = (size p + size q).-1.

Lemma monic_mull : forall p q, monic p -> monic (p * q) = monic q.

Lemma monic_mulr : forall p q, monic q -> monic (p * q) = monic p.

Lemma monic_exp : forall p n, monic p -> monic (p ^+ n).

Pseudo division, defined on an arbitrary ring 
Definition edivp_rec (q : {poly R}) :=
  let sq := size q in
  let cq := lead_coef q in
  fix loop (n : nat) (c : R) (qq r : {poly R}) {struct n} :=
    if size r < sq then (c, qq, r) else
    let m := (lead_coef r)%:P * 'X^(size r - sq) in
    let c1 := cq * c in
    let qq1 := qq * cq%:P + m in
    let r1 := r * cq%:P - m * q in
    if n is n1.+1 then loop n1 c1 qq1 r1 else (c1, qq1, r1).

Lemma edivp_mon_spec : forall p q n c qq r,
   monic q -> let d := edivp_rec q n c qq r in
 p = qq * q + r -> p = (d.1).2 * q + d.2.

Lemma edivp_mod_spec : forall q n c (qq r : {poly R}),
  q != 0 -> size r <= n -> size (edivp_rec q n c qq r).2 < size q.

Lemma edivp_scal_spec : forall q n c (qq r : {poly R}),
  exists m, (edivp_rec q n c qq r).1.1 = lead_coef q ^+ m * c.

Definition edivp (p q : {poly R}) : R * {poly R} * {poly R} :=
  if q == 0 then (1, 0, p) else edivp_rec q (size p) 1 0 p.

Definition divp p q := ((edivp p q).1).2.
Definition modp p q := (edivp p q).2.
Definition scalp p q := ((edivp p q).1).1.
Definition dvdp p q := modp q p == 0.

Local Notation "m %/ d" := (divp m d) (at level 40, no associativity).
Local Notation "m %% d" := (modp m d) (at level 40, no associativity).
Local Notation "p %| q" := (dvdp p q) (at level 70, no associativity).

Equality up to a constant factor; this is only used when R is integral 
Definition eqp p q := (p %| q) && (q %| p).

Lemma divp_size : forall p q, size p < size q -> p %/ q = 0.

Lemma modp_size : forall p q, size p < size q -> p %% q = p.

Lemma divp_mon_spec : forall p q, monic q -> p = p %/ q * q + p %% q.

Lemma modp_spec : forall p q, q != 0 -> size (p %% q) < size q.

Lemma scalp_spec : forall p q, exists m, scalp p q = lead_coef q ^+ m.

Lemma div0p : forall p, 0 %/ p = 0.

Lemma modp0 : forall p, p %% 0 = p.

Lemma mod0p : forall p, 0 %% p = 0.

Lemma dvdpPm : forall p q, monic q -> reflect (exists qq, p = qq * q) (q %| p).

Lemma dvdp0 : forall p, p %| 0.

Lemma modpC : forall p c, c != 0 -> p %% c%:P = 0.

Lemma modp1 : forall p, p %% 1 = 0.

Lemma divp1 : forall p, p %/ 1 = p.

Lemma dvd1p : forall p, 1 %| p.

Lemma modp_mon_mull : forall p q, monic q -> p * q %% q = 0.

Lemma divp_mon_mull : forall p q, monic q -> p * q %/ q = p.

Lemma dvdp_mon_mull : forall p q, monic q -> q %| p * q.

Pseudo gcd 
Definition gcdp p q :=
  let: (p1, q1) := if size p < size q then (q, p) else (p, q) in
  if p1 == 0 then q1 else
  let fix loop (n : nat) (pp qq : {poly R}) {struct n} :=
      let rr := pp %% qq in
      if rr == 0 then qq else
      if n is n1.+1 then loop n1 qq rr else rr in
  loop (size p1) p1 q1.

Lemma gcd0p : left_id 0 gcdp.

Lemma gcdp0 : right_id 0 gcdp.

Lemma gcdpE : forall p q,
  gcdp p q = if size p < size q then gcdp (q %% p) p else gcdp (p %% q) q.

End PolynomialTheory.

Notation "{ 'poly' T }" := (poly_of (Phant T)) : type_scope.
Notation "\poly_ ( i < n ) E" := (Poly (mkseq (fun i => E) n)) : ring_scope.
Notation "c %:P" := (polyC c) : ring_scope.
Notation "'X" := (polyX _) : ring_scope.
Notation "''X^' n" := ('X ^+ n) : ring_scope.
Notation "m %/ d" := (divp m d) (at level 40, no associativity) : ring_scope.
Notation "m %% d" := (modp m d) (at level 40, no associativity) : ring_scope.
Notation "p %| q" := (dvdp p q) (at level 70, no associativity) : ring_scope.
Notation "p %= q" := (eqp p q) (at level 70, no associativity) : ring_scope.

Horner evaluation of polynomials 

Section EvalPolynomial.

Variable R : ringType.
Implicit Types p q : {poly R}.
Implicit Types x a c : R.

Fixpoint horner s x {struct s} :=
  if s is a :: s' then horner s' x * x + a else 0.

Local Notation "p .[ x ]" := (horner (polyseq p) x) : ring_scope.

Lemma horner0 : forall x, (0 : {poly R}).[x] = 0.

Lemma hornerC : forall c x, (c%:P).[x] = c.

Lemma hornerX : forall x, 'X.[x] = x.

Lemma horner_cons : forall p c x, (poly_cons c p).[x] = p.[x] * x + c.

Lemma horner_amulX : forall p c x, (p * 'X + c%:P).[x] = p.[x] * x + c.

Lemma horner_mulX : forall p x, (p * 'X).[x] = p.[x] * x.

Lemma horner_Poly : forall s x, (Poly s).[x] = horner s x.

Lemma horner_coef : forall p x,
  p.[x] = \sum_(i < size p) p`_i * x ^+ i.

Lemma horner_coef_wide : forall n p x,
  size p <= n -> p.[x] = \sum_(i < n) p`_i * x ^+ i.

Lemma horner_poly : forall n E x,
  (\poly_(i < n) E i).[x] = \sum_(i < n) E i * x ^+ i.

Lemma horner_opp : forall p x, (- p).[x] = - p.[x].

Lemma horner_add : forall p q x, (p + q).[x] = p.[x] + q.[x].

Lemma horner_sum : forall I r (P : pred I) F x,
  (\sum_(i <- r | P i) F i).[x] = \sum_(i <- r | P i) (F i).[x].

Lemma horner_Cmul : forall c p x, (c%:P * p).[x] = c * p.[x].

Lemma horner_mulrn : forall n p x, (p *+ n).[x] = p.[x] *+ n.

Definition com_coef p (x : R) := forall i, p`_i * x = x * p`_i.

Definition com_poly p x := x * p.[x] = p.[x] * x.

Lemma com_coef_poly : forall p x, com_coef p x -> com_poly p x.

Lemma com_poly0 : forall x, com_poly 0 x.

Lemma com_poly1 : forall x, com_poly 1 x.

Lemma com_polyX : forall x, com_poly 'X x.

Lemma horner_mul_com : forall p q x,
  com_poly q x -> (p * q).[x] = p.[x] * q.[x].

Lemma horner_exp_com : forall p x n, com_poly p x -> (p ^+ n).[x] = p.[x] ^+ n.

Lemma hornerXn : forall x n, ('X^n).[x] = x ^+ n.

Definition horner_lin_com :=
  (horner_add, horner_opp, hornerX, hornerC, horner_cons,
   simp, horner_Cmul, (fun p x => horner_mul_com p (com_polyX x))).

Lemma factor0 : forall c, ('X - c%:P).[c] = 0.

Lemma seq_factor : forall c, 'X - c%:P = [:: - c; 1] :> seq R.

Lemma monic_factor : forall c, monic ('X - c%:P).

Theorem factor_theorem : forall p c,
  reflect (exists q, p = q * ('X - c%:P)) (p.[c] == 0).

Definition root p : pred R := fun x => p.[x] == 0.

Lemma root_factor_theorem : forall p x, root p x = ('X - x%:P %| p).

End EvalPolynomial.

Notation "p .[ x ]" := (horner p x) : ring_scope.

Container morphism. 
Section MapPoly.

Variables (aR rR : ringType) (f : aR -> rR).

Definition map_poly (p : {poly aR}) := \poly_(i < size p) f p`_i.

Local Notation "p ^f" := (map_poly p) : ring_scope.

Alternative definition; the one above is more convenient because it lets 
 us use the lemmas on \poly, e.g., size (map_poly p) <= size p is an      
 instance of size_poly.                                                   
Lemma map_polyE : forall p, p^f = Poly (map f p).

Hypothesis fRM : GRing.morphism f.

Lemma coef_map : forall p i, p^f`_i = f p`_i.

Lemma map_polyRM : GRing.morphism map_poly.
Hint Resolve map_polyRM.

Lemma map_polyX : ('X)^f = 'X.

Lemma map_polyXn : forall n, ('X^n)^f = 'X^n.

Lemma map_polyC : forall a, (a%:P)^f = (f a)%:P.

Lemma horner_map : forall p x, p^f.[f x] = f p.[x].

Lemma lead_coef_map_eq : forall p,
  f (lead_coef p) != 0 -> lead_coef p^f = f (lead_coef p).

Lemma map_poly_monic : forall p, monic p -> monic p^f.

Lemma map_com_poly : forall p x, com_poly p x -> com_poly p^f (f x).

Lemma map_com_coef : forall p x, com_coef p x -> com_coef p^f (f x).

Lemma root_map_poly : forall p x, root p x -> root p^f (f x).

Definition comm_ringM u := forall x, GRing.comm u (f x).

Definition horner_morph u := fun p => p^f.[u].

Lemma horner_morphC : forall u a, horner_morph u a%:P = f a.

Lemma horner_morphX : forall u, horner_morph u 'X = u.

Lemma horner_morphRM : forall u,
  comm_ringM u -> GRing.morphism (horner_morph u).

End MapPoly.

Morphisms from the polynomial ring, and the initiality of polynomials  
 with respect to these.                                                 
Section MorphPoly.

Variable (aR rR : ringType) (pf : {poly aR} -> rR).
Hypothesis pfRM : GRing.morphism pf.

Local Notation fC := (@polyC aR).

Lemma polyC_RM : GRing.morphism fC.

Lemma poly_morphX_comm : comm_ringM (pf \o fC) (pf 'X).

Let fC_RM := (comp_ringM pfRM polyC_RM).
Definition poly_morphRM := horner_morphRM fC_RM poly_morphX_comm.
Let ipfRM := poly_morphRM.

Lemma poly_initial : pf =1 horner_morph (pf \o fC) (pf 'X).

End MorphPoly.

Section PolynomialComRing.

Variable R : comRingType.
Implicit Types p q : {poly R}.

Lemma horner_mul : forall p q x, (p * q).[x] = p.[x] * q.[x].

Lemma horner_exp : forall p x n, (p ^+ n).[x] = p.[x] ^+ n.

Definition horner_lin :=
  (horner_add, horner_opp, hornerX, hornerC, horner_cons,
   simp, horner_Cmul, horner_mul).

Lemma poly_mulC : forall p q, p * q = q * p.

Canonical Structure poly_comRingType :=
  Eval hnf in ComRingType {poly R} poly_mulC.
Canonical Structure polynomial_comRingType :=
  Eval hnf in [comRingType of polynomial R for poly_comRingType].

Pseudo-division in a commutative setting 

Lemma edivp_spec : forall p q n c qq r,
  let d := edivp_rec q n c qq r in
  c%:P * p = qq * q + r -> (d.1).1%:P * p = (d.1).2 * q + d.2.

Lemma divp_spec : forall p q, (scalp p q)%:P * p = p %/ q * q + p %% q.

End PolynomialComRing.

Section PolynomialIdomain.

Variable R : idomainType.
Implicit Types x y : R.
Implicit Types p q r m n d : {poly R}.

Lemma size_mul_id : forall p q,
  p != 0 -> q != 0 -> size (p * q) = (size p + size q).-1.

Lemma size_polyC_mul : forall c p, c != 0 -> size (c%:P * p) = size p.

Lemma lead_coef_mul_id : forall p q,
  lead_coef (p * q) = lead_coef p * lead_coef q.

Lemma scalp_id : forall p q, scalp p q != 0.

idomain structure on poly 

Lemma poly_idomainMixin : forall p q, p * q = 0 -> (p == 0) || (q == 0).

Definition poly_unit : pred {poly R} :=
  fun p => (size p == 1%N) && GRing.unit p`_0.

Definition poly_inv p := if poly_unit p then (p`_0)^-1%:P else p.

Lemma poly_mulVp : {in poly_unit, left_inverse 1 poly_inv *%R}.

Lemma poly_intro_unit : forall p q, q * p = 1 -> poly_unit p.

Lemma poly_inv_out : {in predC poly_unit, poly_inv =1 id}.

Definition poly_unitRingMixin :=
  ComUnitRingMixin poly_mulVp poly_intro_unit poly_inv_out.

Canonical Structure poly_unitRingType :=
  Eval hnf in UnitRingType {poly R} poly_unitRingMixin.
Canonical Structure polynomial_unitRingType :=
  Eval hnf in [unitRingType of polynomial R for poly_unitRingType].

Canonical Structure poly_comUnitRingType :=
  Eval hnf in [comUnitRingType of {poly R}].
Canonical Structure polynomial_comUnitRingType :=
  Eval hnf in [comUnitRingType of polynomial R].

Canonical Structure poly_idomainType :=
  Eval hnf in IdomainType {poly R} poly_idomainMixin.
Canonical Structure polynomial_idomainType :=
  Eval hnf in [idomainType of polynomial R for poly_idomainType].

Lemma modp_mull : forall p q, p * q %% q = 0.

Lemma modpp : forall p, p %% p = 0.

Lemma dvdpp : forall p, p %| p.

Lemma divp_mull : forall p q, q != 0 -> p * q %/ q = (scalp (p * q) q)%:P * p.

Lemma dvdpPc : forall p q,
  reflect (exists c, exists qq, c != 0 /\ c%:P * p = qq * q) (q %| p).

Lemma size_dvdp : forall p q, q != 0 -> p %| q -> size p <= size q.

Lemma dvdp_mull : forall d m n, d %| n -> d %| m * n.

Lemma dvdp_mulr : forall d m n, d %| m -> d %| m * n.

Lemma dvdp_mul : forall d1 d2 m1 m2 : {poly R},
  d1 %| m1 -> d2 %| m2 -> d1 * d2 %| m1 * m2.

Lemma dvdp_trans : transitive (@dvdp R).

Lemma dvdp_addr : forall m d n, d %| m -> (d %| m + n) = (d %| n).

Lemma dvdp_addl : forall n d m, d %| n -> (d %| m + n) = (d %| m).

Lemma dvdp_add : forall d m n, d %| m -> d %| n -> d %| m + n.

Lemma dvdp_add_eq : forall d m n, d %| m + n -> (d %| m) = (d %| n).

Lemma dvdp_subr : forall d m n, d %| m -> (d %| m - n) = (d %| n).

Lemma dvdp_subl : forall d m n, d %| n -> (d %| m - n) = (d %| m).

Lemma dvdp_sub : forall d m n, d %| m -> d %| n -> d %| m - n.

Lemma dvdp_mod : forall d m n, d %| m -> (d %| n) = (d %| n %% m).

Lemma gcdpp : idempotent (@gcdp R).

Lemma dvdp_gcd2 : forall m n, (gcdp m n %| m) && (gcdp m n %| n).

Lemma dvdp_gcdl : forall m n, gcdp m n %| m.

Lemma dvdp_gcdr : forall m n, gcdp m n %| n.

Lemma dvdp_gcd : forall p m n, p %| gcdp m n = (p %| m) && (p %| n).

Equality modulo constant factors 

Lemma eqpP : forall m n,
  reflect (exists c1, exists c2, [/\ c1 != 0, c2 != 0 & c1%:P * m = c2%:P * n])
          (m %= n).

Lemma eqpxx : reflexive (@eqp R).

Lemma eqp_sym : symmetric (@eqp R).

Lemma eqp_trans : transitive (@eqp R).

Lemma eqp0E : forall p, (p %= 0) = (p == 0).

Lemma size_eqp : forall p q, p %= q -> size p = size q.

Now we can state that gcd is commutative modulo a factor 
Lemma gcdpC : forall p q, gcdp p q %= gcdp q p.

End PolynomialIdomain.

Section MapFieldPoly.

Variables (F : fieldType) (R : ringType) (f : F -> R).

Local Notation "p ^f" := (map_poly f p) : ring_scope.

Hypothesis fRM : GRing.morphism f.
Let pfRM := map_polyRM fRM.

Lemma size_map_poly : forall p, size p^f = size p.

Lemma lead_coef_map : forall p, lead_coef p^f = f (lead_coef p).

Lemma map_poly_eq0 : forall p, (p^f == 0) = (p == 0).

Lemma map_poly_inj : injective (map_poly f).

Lemma map_field_poly_monic : forall p, monic p^f = monic p.

Lemma map_poly_com : forall p x, com_poly p^f (f x).

Lemma root_field_map_poly : forall p x, root p^f (f x) = root p x.

Lemma edivp_map : forall p q,
  edivp p^f q^f = (f (scalp p q), (p %/ q)^f, (p %% q)^f).

Lemma scalp_map : forall p q, scalp p^f q^f = f (scalp p q).

Lemma map_divp : forall p q, (p %/ q)^f = p^f %/ q^f.

Lemma map_modp : forall p q, (p %% q)^f = p^f %% q^f.

Lemma dvdp_map : forall p q, (p^f %| q^f) = (p %| q).

Lemma eqp_map : forall p q, (p^f %= q^f) = (p %= q).

Lemma gcdp_map : forall p q, (gcdp p q)^f = gcdp p^f q^f.

End MapFieldPoly.

Section MaxRoots.

Variable R : unitRingType.

Definition diff_roots (x y : R) := (x * y == y * x) && GRing.unit (y - x).

Fixpoint uniq_roots (rs : seq R) {struct rs} :=
  if rs is x :: rs' then all (diff_roots x) rs' && uniq_roots rs' else true.

Theorem max_ring_poly_roots : forall (p : {poly R}) rs,
  p != 0 -> all (root p) rs -> uniq_roots rs -> size rs < size p.

End MaxRoots.

Theorem max_poly_roots : forall (F : fieldType) (p : polynomial F) rs,
  p != 0 -> all (root p) rs -> uniq rs -> size rs < size p.

Section MapPolyRoots.

Variables (F : fieldType) (R : unitRingType) (f : F -> R).
Hypothesis fRM : GRing.morphism f.

Lemma map_diff_roots : forall x y, diff_roots (f x) (f y) = (x != y).

Lemma map_uniq_roots : forall s, uniq_roots (map f s) = uniq s.

End MapPolyRoots.

Section Deriv.

Variable R: ringType.

Implicit Types p q : {poly R}.

Definition deriv p :=
  \poly_(i < (size p).-1) (p`_i.+1 *+ i.+1).

Notation "a ^`()" := (deriv a).

Lemma coef_deriv : forall p i, p^`()`_i = p`_i.+1 *+ i.+1.

Lemma derivC : forall c, c%:P^`() = 0.

Lemma derivX : ('X)^`() = 1.

Lemma derivXn : forall n, 'X^n^`() = 'X^n.-1 *+ n.

Lemma deriv_add : {morph deriv : p q / p + q}.

Lemma deriv_mul : forall p q, (p * q)^`() = p^`() * q + p * q^`().

Lemma deriv_mulr : forall p n, (p *+ n)^`() = p^`() *+ n.

Lemma deriv_amulX : forall p c, (p * 'X + c%:P)^`() = p + p^`() * 'X.

Definition derivn p n := iter n deriv p.

Notation "a ^`( n )" := (derivn a n).

Lemma derivn0 : forall p, p^`(0) = p.

Lemma derivn1 : forall p, p^`(1) = p^`().

Lemma derivnS : forall p n, p ^`(n.+1) = p^`(n)^`().

Lemma derivSn : forall p n, p ^`(n.+1) = p^`()^`(n).

Lemma coef_derivn : forall n p i, p^`(n)`_i = p`_(n + i) *+ (n + i) ^_ n.

Lemma derivnC : forall c n, c%:P ^`(n) = if n == 0%N then c%:P else 0.

Lemma derivn_mulr : forall p m n, (p *+ m)^`(n) = p^`(n) *+ m.

Lemma derivnXn : forall m n, 'X^m^`(n) = 'X^(m - n) *+ m ^_ n.

Lemma derivn_amulX : forall n p c,
 (p * 'X + c%:P)^`(n.+1) = p^`(n) *+ n.+1 + p^`(n.+1) * 'X.

Lemma derivn_poly0 : forall p n, size p <= n -> p^`(n) = 0.

A normalising version of derivation to get the division by n! in Taylor 

Definition nderivn p n := \poly_(i < size p - n) (p`_(n + i) *+ 'C(n + i, n)).

Notation "a ^`N( n )" := (nderivn a n).

Lemma coef_nderivn : forall n p i, p^`N(n)`_i = p`_(n + i) *+ 'C(n + i, n).

Here is the division by n! 
Lemma nderivn_def : forall n p, p^`(n) = p^`N(n) *+ n`!.

Lemma nderivn0 : forall p, p^`N(0) = p.

Lemma nderivn1 : forall p, p^`N(1) = p^`().

Lemma nderivnC : forall c n, c%:P ^`N(n) = if n == 0%N then c%:P else 0.

Lemma nderivn_mulr : forall p m n, (p *+ m)^`N(n) = p^`N(n) *+ m.

Lemma nderivnXn : forall m n, 'X^m^`N(n) = 'X^(m - n) *+ 'C(m, n).

Lemma nderivn_amulX : forall n p c,
  (p * 'X + c%:P)^`N(n.+1) = p^`N(n) + p^`N(n.+1) * 'X.

Lemma nderivn_poly0 : forall p n, size p <= n -> p^`N(n) = 0.

Lemma nderiv_taylor : forall p x h,
  GRing.comm x h -> p.[x + h] = \sum_(i < size p) p^`N(i).[x] * h ^+ i.

Lemma nderiv_taylor_wide : forall n p x h,
    GRing.comm x h -> size p <= n ->
  p.[x + h] = \sum_(i < n) p^`N(i).[x] * h ^+ i.

End Deriv.