# Library mathcomp.algebra.poly

(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
Distributed under the terms of CeCILL-B.                                  *)

From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq choice.
From mathcomp Require Import fintype bigop div ssralg countalg binomial tuple.

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 coefficient 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. polyC c, 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. coefp i == the linear function p |-> p_i (self-exapanding). 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) p \is monic <=> lead_coef p == 1 (0 is not monic). p \is a polyOver S <=> the coefficients of p satisfy S; S should have a key that should be (at least) an addrPred. p. [x] == the evaluation of a polynomial p at a point x using the Horner scheme

### The multi-rule hornerE (resp., hornerE_comm) unwinds

horner evaluation of a polynomial expression (resp., in a non commutative ring, with side conditions). p^ == formal derivative of p p^(n) == formal n-derivative of p p^N(n) == formal n-derivative of p divided by n! p \Po q == polynomial composition; because this is naturally a a linear morphism in the first argument, this notation is transposed (q comes before p for redex selection, etc). := \sum(i < size p) p_i *: q ^+ i comm_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. comm_coef p x == x commutes with all the coefficients of p (clearly, this implies comm_poly p x). root p x == x is a root of p, i.e., p. [x] = 0 n.-unity_root x == x is an nth root of unity, i.e., a root of 'X^n - 1 n.-primitive_root x == x is a primitive nth root of unity, i.e., n is the least positive integer m > 0 such that x ^+ m = 1.

### The submodule poly.UnityRootTheory can be used to

import selectively the part of the theory of roots of unity that doesn't mention polynomials explicitly map_poly f p == the image of the polynomial by the function f (which (locally, p^f) is usually a ring morphism). p^:P == p lifted to {poly {poly R}} (:= map_poly polyC p). commr_rmorph f u == u commutes with the image of f (i.e., with all f x). horner_morph cfu == given cfu : commr_rmorph f u, the function mapping p to the value of map_poly f p at u; this is a ring morphism from {poly R} to the codomain of f when f is a ring morphism. horner_eval u == the function mapping p to p. [u]; this function can only be used for u in a commutative ring, so it is always a linear ring morphism from {poly R} to R. horner_alg a == given a in some R-algebra A, the function evaluating a polynomial p at a; it is always a linear ring morphism from {poly R} to A. 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. The some polynomial lemmas use following suffix interpretation : C - constant polynomial (as in polyseqC : a%:P = nseq (a != 0) a). X - the polynomial variable 'X (as in coefX : 'X_i = (i == 1%N)). Xn - power of 'X (as in monicXn : monic 'X^n).

Set Implicit Arguments.

Import GRing.Theory.
Local Open 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 "p ^:P" (at level 2, format "p ^: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 "p \Po q" (at level 50).
Reserved Notation "p ^N ( n )" (at level 8, format "p ^N ( n )").
Reserved Notation "n .-unity_root" (at level 2, format "n .-unity_root").
Reserved Notation "n .-primitive_root"
(at level 2, format "n .-primitive_root").

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 polynomial_subType := Eval hnf in [subType for polyseq].
Definition polynomial_eqMixin := Eval hnf in [eqMixin of polynomial by <:].
Canonical polynomial_eqType := Eval hnf in EqType polynomial polynomial_eqMixin.
Definition polynomial_choiceMixin := [choiceMixin of polynomial by <:].
Canonical 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.

Definition coefp i (p : poly_of (Phant R)) := p_i.

End Polynomial.

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

Definition poly_countMixin (R : countRingType) :=
[countMixin of polynomial R by <:].
Canonical polynomial_countType R := CountType _ (poly_countMixin R).
Canonical poly_countType (R : countRingType) := [countType of {poly R}].

Section PolynomialTheory.

Variable R : ringType.
Implicit Types (a b c x y z : R) (p q r d : {poly R}).

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

Definition lead_coef p := p_(size p).-1.
Lemma lead_coefE p : lead_coef p = p_(size p).-1.

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

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

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

Lemma coefC c i : c%:P_i = if i == 0%N then c else 0.

Lemma polyCK : cancel polyC (coefp 0).

Lemma polyC_inj : injective polyC.

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

Extensional interpretation (poly <=> nat -> R)
Lemma polyP p q : nth 0 p =1 nth 0 q p = q.

Lemma size1_polyC p : size p 1 p = (p_0)%:P.

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

Lemma polyseq_cons c p :
cons_poly c p = (if ~~ nilp p then c :: p else c%:P) :> seq R.

Lemma size_cons_poly c p :
size (cons_poly c p) = (if nilp p && (c == 0) then 0%N else (size p).+1).

Lemma coef_cons c p i : (cons_poly c p)_i = if i == 0%N then c else p_i.-1.

Build a polynomial directly from a list of coefficients.
Definition Poly := foldr cons_poly 0%:P.

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

Lemma polyseqK p : Poly p = p.

Lemma size_Poly s : size (Poly s) size s.

Lemma coef_Poly s i : (Poly s)_i = s_i.

Build a polynomial from an infinite sequence of coefficients and a bound.
Zmodule structure for polynomial
Properties of the zero polynomial
Lemma polyC0 : 0%:P = 0 :> {poly R}.

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

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

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

Lemma lead_coef0 : lead_coef 0 = 0 :> R.

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

Lemma size_poly_leq0 p : (size p 0) = (p == 0).

Lemma size_poly_leq0P p : reflect (p = 0) (size p 0%N).

Lemma size_poly_gt0 p : (0 < size p) = (p != 0).

Lemma gt_size_poly_neq0 p n : (size p > n)%N p != 0.

Lemma nil_poly p : nilp p = (p == 0).

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

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

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

Lemma polyC_eq0 (c : R) : (c%:P == 0) = (c == 0).

Lemma size_poly1P p : reflect (exists2 c, c != 0 & p = c%:P) (size p == 1%N).

Lemma size_polyC_leq1 (c : R) : (size c%:P 1)%N.

Lemma leq_sizeP p i : reflect ( j, i j p_j = 0) (size p i).

Size, leading coef, morphism properties of coef

Lemma coefD p q i : (p + q)_i = p_i + q_i.

Lemma coefN p i : (- p)_i = - p_i.

Lemma coefB p q i : (p - q)_i = p_i - q_i.

Canonical coefp_additive i :=
Additive ((fun p(coefB p)^~ i) : additive (coefp i)).

Lemma coefMn p n i : (p *+ n)_i = p_i *+ n.

Lemma coefMNn p n i : (p *- n)_i = p_i *- n.

Lemma coef_sum I (r : seq I) (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 polyCD : {morph polyC : a b / a + b}.

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

Lemma polyCB : {morph polyC : a b / a - b}.

Canonical polyC_additive := Additive polyCB.

Lemma polyCMn n : {morph polyC : c / c *+ n}.

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

Lemma lead_coefN p : lead_coef (- p) = - lead_coef p.

Lemma size_add p q : size (p + q) maxn (size p) (size q).

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

Lemma size_sum I (r : seq I) (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_coefDl p q : size p > size q lead_coef (p + q) = lead_coef p.

Lemma lead_coefDr p q : size q > size p lead_coef (p + q) = lead_coef q.

Polynomial ring structure.

Definition mul_poly_def p q :=
\poly_(i < (size p + size q).-1) (\sum_(j < i.+1) p_j × q_(i - j)).
Fact mul_poly_key : unit.
Definition mul_poly := locked_with mul_poly_key mul_poly_def.
Canonical mul_poly_unlockable := [unlockable fun mul_poly].

Fact coef_mul_poly p q i :
(mul_poly p q)_i = \sum_(j < i.+1) p_j × q_(i - j)%N.

Fact coef_mul_poly_rev p q i :
(mul_poly p q)_i = \sum_(j < i.+1) p_(i - j)%N × q_j.

Fact mul_polyA : associative mul_poly.

Fact mul_1poly : left_id 1%:P mul_poly.

Fact mul_poly1 : right_id 1%:P mul_poly.

Fact mul_polyDl : left_distributive mul_poly +%R.

Fact mul_polyDr : right_distributive mul_poly +%R.

Fact poly1_neq0 : 1%:P != 0 :> {poly R}.

Definition poly_ringMixin :=
RingMixin mul_polyA mul_1poly mul_poly1 mul_polyDl mul_polyDr poly1_neq0.

Canonical poly_ringType := Eval hnf in RingType {poly R} poly_ringMixin.
Canonical polynomial_ringType :=
Eval hnf in RingType (polynomial R) poly_ringMixin.

Lemma polyC1 : 1%:P = 1 :> {poly R}.

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

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

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

Lemma lead_coef1 : lead_coef 1 = 1 :> R.

Lemma coefM p q i : (p × q)_i = \sum_(j < i.+1) p_j × q_(i - j)%N.

Lemma coefMr p q i : (p × q)_i = \sum_(j < i.+1) p_(i - j)%N × q_j.

Lemma size_mul_leq p q : size (p × q) (size p + size q).-1.

Lemma mul_lead_coef p q :
lead_coef p × lead_coef q = (p × q)_(size p + size q).-2.

Lemma size_proper_mul p q :
lead_coef p × lead_coef q != 0 size (p × q) = (size p + size q).-1.

Lemma lead_coef_proper_mul p q :
let c := lead_coef p × lead_coef q in c != 0 lead_coef (p × q) = c.

Lemma size_prod_leq (I : finType) (P : pred I) (F : I {poly R}) :
size (\prod_(i | P i) F i) (\sum_(i | P i) size (F i)).+1 - #|P|.

Lemma coefCM c p i : (c%:P × p)_i = c × p_i.

Lemma coefMC c p i : (p × c%:P)_i = p_i × c.

Lemma polyCM : {morph polyC : a b / a × b}.

Fact polyC_multiplicative : multiplicative polyC.
Canonical polyC_rmorphism := AddRMorphism polyC_multiplicative.

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

Lemma size_exp_leq p n : size (p ^+ n) ((size p).-1 × n).+1.

Lemma size_Msign p n : size ((-1) ^+ n × p) = size p.

Fact coefp0_multiplicative : multiplicative (coefp 0 : {poly R} R).

Canonical coefp0_rmorphism := AddRMorphism coefp0_multiplicative.

Algebra structure of polynomials.
The indeterminate, at last!
Definition polyX_def := Poly [:: 0; 1].
Fact polyX_key : unit.
Definition polyX : {poly R} := locked_with polyX_key polyX_def.
Canonical polyX_unlockable := [unlockable of polyX].

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

Lemma size_polyX : size 'X = 2.

Lemma polyX_eq0 : ('X == 0) = false.

Lemma coefX i : 'X_i = (i == 1%N)%:R.

Lemma lead_coefX : lead_coef 'X = 1.

Lemma commr_polyX p : GRing.comm p 'X.

Lemma coefMX p i : (p × 'X)_i = (if (i == 0)%N then 0 else p_i.-1).

Lemma coefXM p i : ('X × p)_i = (if (i == 0)%N then 0 else p_i.-1).

Lemma cons_poly_def p a : cons_poly a p = p × 'X + a%:P.

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

Lemma polyseqXsubC a : 'X - a%:P = [:: - a; 1] :> seq R.

Lemma size_XsubC a : size ('X - a%:P) = 2%N.

Lemma size_XaddC b : size ('X + b%:P) = 2.

Lemma lead_coefXsubC a : lead_coef ('X - a%:P) = 1.

Lemma polyXsubC_eq0 a : ('X - a%:P == 0) = false.

Lemma size_MXaddC p c :
size (p × 'X + c%:P) = (if (p == 0) && (c == 0) then 0%N else (size p).+1).

Lemma polyseqMX p : p != 0 p × 'X = 0 :: p :> seq R.

Lemma size_mulX p : p != 0 size (p × 'X) = (size p).+1.

Lemma lead_coefMX p : lead_coef (p × 'X) = lead_coef p.

Lemma size_XmulC a : a != 0 size ('X × a%:P) = 2.

Lemma coefXn n i : 'X^n_i = (i == n)%:R.

Lemma polyseqXn n : 'X^n = rcons (nseq n 0) 1 :> seq R.

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

Lemma commr_polyXn p n : GRing.comm p 'X^n.

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

Lemma polyseqMXn n p : p != 0 p × 'X^n = ncons n 0 p :> seq R.

Lemma coefMXn n p i : (p × 'X^n)_i = if i < n then 0 else p_(i - n).

Lemma coefXnM n p i : ('X^n × p)_i = if i < n then 0 else p_(i - n).

Expansion of a polynomial as an indexed sum
Monic predicate
Some facts about regular elements.
Horner evaluation of polynomials
Implicit Types s rs : seq R.
Fixpoint horner_rec s x := if s is a :: s' then horner_rec s' x × x + a else 0.
Definition horner p := horner_rec p.

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

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

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

Lemma horner_cons p c x : (cons_poly c p).[x] = p.[x] × x + c.

Lemma horner_coef0 p : p.[0] = p_0.

Lemma hornerMXaddC p c x : (p × 'X + c%:P).[x] = p.[x] × x + c.

Lemma hornerMX p x : (p × 'X).[x] = p.[x] × x.

Lemma horner_Poly s x : (Poly s).[x] = horner_rec s x.

Lemma horner_coef p x : p.[x] = \sum_(i < size p) p_i × x ^+ i.

Lemma horner_coef_wide n p x :
size p n p.[x] = \sum_(i < n) p_i × x ^+ i.

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

Lemma hornerN p x : (- p).[x] = - p.[x].

Lemma hornerD p q x : (p + q).[x] = p.[x] + q.[x].

Lemma hornerXsubC a x : ('X - a%:P).[x] = x - a.

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

Lemma hornerCM a p x : (a%:P × p).[x] = a × p.[x].

Lemma hornerZ c p x : (c *: p).[x] = c × p.[x].

Lemma hornerMn n p x : (p *+ n).[x] = p.[x] *+ n.

Definition comm_coef p x := i, p_i × x = x × p_i.

Definition comm_poly p x := x × p.[x] = p.[x] × x.

Lemma comm_coef_poly p x : comm_coef p x comm_poly p x.

Lemma comm_poly0 x : comm_poly 0 x.

Lemma comm_poly1 x : comm_poly 1 x.

Lemma comm_polyX x : comm_poly 'X x.

Lemma commr_horner a b p : GRing.comm a b comm_coef p a GRing.comm a p.[b].

Lemma hornerM_comm p q x : comm_poly q x (p × q).[x] = p.[x] × q.[x].

Lemma horner_exp_comm p x n : comm_poly p x (p ^+ n).[x] = p.[x] ^+ n.

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

Definition hornerE_comm :=
(hornerD, hornerN, hornerX, hornerC, horner_cons,
simp, hornerCM, hornerZ,
(fun p xhornerM_comm p (comm_polyX x))).

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

Lemma mem_root p x : x \in root p = (p.[x] == 0).

Lemma rootE p x : (root p x = (p.[x] == 0)) × ((x \in root p) = (p.[x] == 0)).

Lemma rootP p x : reflect (p.[x] = 0) (root p x).

Lemma rootPt p x : reflect (p.[x] == 0) (root p x).

Lemma rootPf p x : reflect ((p.[x] == 0) = false) (~~ root p x).

Lemma rootC a x : root a%:P x = (a == 0).

Lemma root0 x : root 0 x.

Lemma root1 x : ~~ root 1 x.

Lemma rootX x : root 'X x = (x == 0).

Lemma rootN p x : root (- p) x = root p x.

Lemma root_size_gt1 a p : p != 0 root p a 1 < size p.

Lemma root_XsubC a x : root ('X - a%:P) x = (x == a).

Lemma root_XaddC a x : root ('X + a%:P) x = (x == - a).

Theorem factor_theorem p a : reflect ( q, p = q × ('X - a%:P)) (root p a).

Lemma multiplicity_XsubC p a :
{m | exists2 q, (p != 0) ==> ~~ root q a & p = q × ('X - a%:P) ^+ m}.

Roots of unity.
Lifting a ring predicate to polynomials.

Implicit Type S : {pred R}.

Definition polyOver S := [qualify a p : {poly R} | all (mem S) p].

Fact polyOver_key S : pred_key (polyOver S).
Canonical polyOver_keyed S := KeyedQualifier (polyOver_key S).

Lemma polyOverS (S1 S2 : {pred R}) :
{subset S1 S2} {subset polyOver S1 polyOver S2}.

Lemma polyOver0 S : 0 \is a polyOver S.

Lemma polyOver_poly S n E :
( i, i < n E i \in S) \poly_(i < n) E i \is a polyOver S.

Section PolyOverAdd.

Variables (S : {pred R}) (addS : addrPred S) (kS : keyed_pred addS).

Lemma polyOverP {p} : reflect ( i, p_i \in kS) (p \in polyOver kS).

Lemma polyOverC c : (c%:P \in polyOver kS) = (c \in kS).

Fact polyOver_addr_closed : addr_closed (polyOver kS).
Canonical polyOver_addrPred := AddrPred polyOver_addr_closed.

End PolyOverAdd.

Fact polyOverNr S (addS : zmodPred S) (kS : keyed_pred addS) :
oppr_closed (polyOver kS).
Canonical polyOver_opprPred S addS kS := OpprPred (@polyOverNr S addS kS).
Canonical polyOver_zmodPred S addS kS := ZmodPred (@polyOverNr S addS kS).

Section PolyOverSemiring.

Variables (S : {pred R}) (ringS : semiringPred S) (kS : keyed_pred ringS).

Fact polyOver_mulr_closed : mulr_closed (polyOver kS).
Canonical polyOver_mulrPred := MulrPred polyOver_mulr_closed.
Canonical polyOver_semiringPred := SemiringPred polyOver_mulr_closed.

Lemma polyOverZ : {in kS & polyOver kS, c p, c *: p \is a polyOver kS}.

Lemma polyOverX : 'X \in polyOver kS.

Lemma rpred_horner : {in polyOver kS & kS, p x, p.[x] \in kS}.

End PolyOverSemiring.

Section PolyOverRing.

Variables (S : {pred R}) (ringS : subringPred S) (kS : keyed_pred ringS).
Canonical polyOver_smulrPred := SmulrPred (polyOver_mulr_closed kS).
Canonical polyOver_subringPred := SubringPred (polyOver_mulr_closed kS).

Lemma polyOverXsubC c : ('X - c%:P \in polyOver kS) = (c \in kS).

End PolyOverRing.

Single derivative.

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

Lemma coef_deriv p i : p^_i = p_i.+1 *+ i.+1.

Lemma polyOver_deriv S (ringS : semiringPred S) (kS : keyed_pred ringS) :
{in polyOver kS, p, p^ \is a polyOver kS}.

Lemma derivC c : c%:P^ = 0.

Lemma derivX : ('X)^ = 1.

Lemma derivXn n : 'X^n^ = 'X^n.-1 *+ n.

Fact deriv_is_linear : linear deriv.
Canonical deriv_additive := Additive deriv_is_linear.
Canonical deriv_linear := Linear deriv_is_linear.

Lemma deriv0 : 0^ = 0.

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

Lemma derivN : {morph deriv : p / - p}.

Lemma derivB : {morph deriv : p q / p - q}.

Lemma derivXsubC (a : R) : ('X - a%:P)^ = 1.

Lemma derivMn n p : (p *+ n)^ = p^ *+ n.

Lemma derivMNn n p : (p *- n)^ = p^ *- n.

Lemma derivZ c p : (c *: p)^ = c *: p^.

Lemma deriv_mulC c p : (c%:P × p)^ = c%:P × p^.

Lemma derivMXaddC p c : (p × 'X + c%:P)^ = p + p^ × 'X.

Lemma derivM p q : (p × q)^ = p^ × q + p × q^.

Definition derivE := Eval lazy beta delta [morphism_2 morphism_1] in
(derivZ, deriv_mulC, derivC, derivX, derivMXaddC, derivXsubC, derivM, derivB,
derivD, derivN, derivXn, derivM, derivMn).

Iterated derivative.
A normalising version of derivation to get the division by n! in Taylor
Here is the division by n!
Lemma nderivn_def n p : p^(n) = p^N(n) *+ n!.

Lemma polyOver_nderivn S (ringS : semiringPred S) (kS : keyed_pred ringS) :
{in polyOver kS, p n, p^N(n) \in polyOver kS}.

Lemma nderivn0 p : p^N(0) = p.

Lemma nderivn1 p : p^N(1) = p^.

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

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

Fact nderivn_is_linear n : linear (nderivn n).
Canonical nderivn_additive n := Additive(nderivn_is_linear n).
Canonical nderivn_linear n := Linear (nderivn_is_linear n).

Lemma nderivnD n : {morph nderivn n : p q / p + q}.

Lemma nderivnB n : {morph nderivn n : p q / p - q}.

Lemma nderivnMn n m p : (p *+ m)^N(n) = p^N(n) *+ m.

Lemma nderivnMNn n m p : (p *- m)^N(n) = p^N(n) *- m.

Lemma nderivnN n : {morph nderivn n : p / - p}.

Lemma nderivnZ n : scalable (nderivn n).

Lemma nderivnMXaddC n p c :
(p × 'X + c%:P)^N(n.+1) = p^N(n) + p^N(n.+1) × 'X.

Lemma nderivn_poly0 p n : size p n p^N(n) = 0.

Lemma nderiv_taylor p x h :
GRing.comm x h p.[x + h] = \sum_(i < size p) p^N(i).[x] × h ^+ i.

Lemma nderiv_taylor_wide n p x h :
GRing.comm x h size p n
p.[x + h] = \sum_(i < n) p^N(i).[x] × h ^+ i.

Lemma eq_poly n E1 E2 : E1 =1 E2 poly n E1 = poly n E2.

End PolynomialTheory.

Notation "\poly_ ( i < n ) E" := (poly n (fun iE)) : ring_scope.
Notation "c %:P" := (polyC c) : ring_scope.
Notation "'X" := (polyX _) : ring_scope.
Notation "''X^' n" := ('X ^+ n) : ring_scope.
Notation "p .[ x ]" := (horner p x) : ring_scope.
Notation "n .-unity_root" := (root_of_unity n) : ring_scope.
Notation "n .-primitive_root" := (primitive_root_of_unity n) : ring_scope.
Notation "a ^ " := (deriv a) : ring_scope.
Notation "a ^ ( n )" := (derivn n a) : ring_scope.
Notation "a ^N ( n )" := (nderivn n a) : ring_scope.

Canonical polynomial_countZmodType (R : countRingType) :=
[countZmodType of polynomial R].
Canonical poly_countZmodType (R : countRingType) := [countZmodType of {poly R}].
Canonical polynomial_countRingType (R : countRingType) :=
[countRingType of polynomial R].
Canonical poly_countRingType (R : countRingType) := [countRingType of {poly R}].

Container morphism.
Section MapPoly.

Section Definitions.

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

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

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 p : map_poly p = Poly (map f p).

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

Definition horner_morph u of commr_rmorph u := fun p(map_poly p).[u].

End Definitions.

Variables aR rR : ringType.

Section Combinatorial.

Variables (iR : ringType) (f : aR rR).

Lemma map_poly0 : 0^f = 0.

Lemma eq_map_poly (g : aR rR) : f =1 g map_poly f =1 map_poly g.

Lemma map_poly_id g (p : {poly iR}) :
{in (p : seq iR), g =1 id} map_poly g p = p.

Lemma coef_map_id0 p i : f 0 = 0 (p^f)_i = f p_i.

Lemma map_Poly_id0 s : f 0 = 0 (Poly s)^f = Poly (map f s).

Lemma map_poly_comp_id0 (g : iR aR) p :
f 0 = 0 map_poly (f \o g) p = (map_poly g p)^f.

Lemma size_map_poly_id0 p : f (lead_coef p) != 0 size p^f = size p.

Lemma map_poly_eq0_id0 p : f (lead_coef p) != 0 (p^f == 0) = (p == 0).

Lemma lead_coef_map_id0 p :
f 0 = 0 f (lead_coef p) != 0 lead_coef p^f = f (lead_coef p).

Hypotheses (inj_f : injective f) (f_0 : f 0 = 0).

Lemma size_map_inj_poly p : size p^f = size p.

Lemma map_inj_poly : injective (map_poly f).

Lemma lead_coef_map_inj p : lead_coef p^f = f (lead_coef p).

End Combinatorial.

Lemma map_polyK (f : aR rR) g :
cancel g f f 0 = 0 cancel (map_poly g) (map_poly f).

Section Additive.

Variables (iR : ringType) (f : {additive aR rR}).

Lemma coef_map p i : p^f_i = f p_i.

Lemma map_Poly s : (Poly s)^f = Poly (map f s).

Lemma map_poly_comp (g : iR aR) p :
map_poly (f \o g) p = map_poly f (map_poly g p).

Fact map_poly_is_additive : additive (map_poly f).
Canonical map_poly_additive := Additive map_poly_is_additive.

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

Lemma lead_coef_map_eq p :
f (lead_coef p) != 0 lead_coef p^f = f (lead_coef p).

End Additive.

Variable f : {rmorphism aR rR}.
Implicit Types p : {poly aR}.

Fact map_poly_is_rmorphism : rmorphism (map_poly f).
Canonical map_poly_rmorphism := RMorphism map_poly_is_rmorphism.

Lemma map_polyZ c p : (c *: p)^f = f c *: p^f.
Canonical map_poly_linear :=
AddLinear (map_polyZ : scalable_for (f \; *:%R) (map_poly f)).
Canonical map_poly_lrmorphism := [lrmorphism of map_poly f].

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

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

Lemma monic_map p : p \is monic p^f \is monic.

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

Lemma map_comm_poly p x : comm_poly p x comm_poly p^f (f x).

Lemma map_comm_coef p x : comm_coef p x comm_coef p^f (f x).

Lemma rmorph_root p x : root p x root p^f (f x).

Lemma rmorph_unity_root n z : n.-unity_root z n.-unity_root (f z).

Section HornerMorph.

Variable u : rR.
Hypothesis cfu : commr_rmorph f u.

Lemma horner_morphC a : horner_morph cfu a%:P = f a.

Lemma horner_morphX : horner_morph cfu 'X = u.

Fact horner_is_lrmorphism : lrmorphism_for (f \; *%R) (horner_morph cfu).
Canonical horner_additive := Additive horner_is_lrmorphism.
Canonical horner_rmorphism := RMorphism horner_is_lrmorphism.
Canonical horner_linear := AddLinear horner_is_lrmorphism.
Canonical horner_lrmorphism := [lrmorphism of horner_morph cfu].

End HornerMorph.

Lemma deriv_map p : p^f^ = (p^)^f.

Lemma derivn_map p n : p^f^(n) = (p^(n))^f.

Lemma nderivn_map p n : p^f^N(n) = (p^N(n))^f.

End MapPoly.

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

Variable (aR rR : ringType) (pf : {rmorphism {poly aR} rR}).

Lemma poly_morphX_comm : commr_rmorph (pf \o polyC) (pf 'X).

Lemma poly_initial : pf =1 horner_morph poly_morphX_comm.

End MorphPoly.

Notation "p ^:P" := (map_poly polyC p) : ring_scope.

Section PolyCompose.

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

Definition comp_poly q p := p^:P.[q].

Lemma size_map_polyC p : size p^:P = size p.

Lemma map_polyC_eq0 p : (p^:P == 0) = (p == 0).

Lemma root_polyC p x : root p^:P x%:P = root p x.

Lemma comp_polyE p q : p \Po q = \sum_(i < size p) p_i *: q^+i.

Lemma coef_comp_poly p q n :
(p \Po q)_n = \sum_(i < size p) p_i × (q ^+ i)_n.

Lemma polyOver_comp S (ringS : semiringPred S) (kS : keyed_pred ringS) :
{in polyOver kS &, p q, p \Po q \in polyOver kS}.

Lemma comp_polyCr p c : p \Po c%:P = p.[c]%:P.

Lemma comp_poly0r p : p \Po 0 = (p_0)%:P.

Lemma comp_polyC c p : c%:P \Po p = c%:P.

Fact comp_poly_is_linear p : linear (comp_poly p).
Canonical comp_poly_additive p := Additive (comp_poly_is_linear p).
Canonical comp_poly_linear p := Linear (comp_poly_is_linear p).

Lemma comp_poly0 p : 0 \Po p = 0.

Lemma comp_polyD p q r : (p + q) \Po r = (p \Po r) + (q \Po r).

Lemma comp_polyB p q r : (p - q) \Po r = (p \Po r) - (q \Po r).

Lemma comp_polyZ c p q : (c *: p) \Po q = c *: (p \Po q).

Lemma comp_polyXr p : p \Po 'X = p.

Lemma comp_polyX p : 'X \Po p = p.

Lemma comp_poly_MXaddC c p q : (p × 'X + c%:P) \Po q = (p \Po q) × q + c%:P.

Lemma comp_polyXaddC_K p z : (p \Po ('X + z%:P)) \Po ('X - z%:P) = p.

Lemma size_comp_poly_leq p q :
size (p \Po q) ((size p).-1 × (size q).-1).+1.

End PolyCompose.

Notation "p \Po q" := (comp_poly q p) : ring_scope.

Lemma map_comp_poly (aR rR : ringType) (f : {rmorphism aR rR}) p q :
map_poly f (p \Po q) = map_poly f p \Po map_poly f q.

Section PolynomialComRing.

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

Fact poly_mul_comm p q : p × q = q × p.

Canonical poly_comRingType := Eval hnf in ComRingType {poly R} poly_mul_comm.
Canonical polynomial_comRingType :=
Eval hnf in ComRingType (polynomial R) poly_mul_comm.
Canonical poly_algType := Eval hnf in CommAlgType R {poly R}.
Canonical polynomial_algType :=
Eval hnf in [algType R of polynomial R for poly_algType].
Canonical poly_comAlgType := Eval hnf in [comAlgType R of {poly R}].

Lemma hornerM p q x : (p × q).[x] = p.[x] × q.[x].

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

Lemma horner_prod I r (P : pred I) (F : I {poly R}) x :
(\prod_(i <- r | P i) F i).[x] = \prod_(i <- r | P i) (F i).[x].

Definition hornerE :=
(hornerD, hornerN, hornerX, hornerC, horner_cons,
simp, hornerCM, hornerZ, hornerM).

Definition horner_eval (x : R) := horner^~ x.
Lemma horner_evalE x p : horner_eval x p = p.[x].

Fact horner_eval_is_lrmorphism x : lrmorphism_for *%R (horner_eval x).
Canonical horner_eval_additive x := Additive (horner_eval_is_lrmorphism x).
Canonical horner_eval_rmorphism x := RMorphism (horner_eval_is_lrmorphism x).
Canonical horner_eval_linear x := AddLinear (horner_eval_is_lrmorphism x).
Canonical horner_eval_lrmorphism x := [lrmorphism of horner_eval x].

Section HornerAlg.

Variable A : algType R. (* For univariate polys, commutativity is not needed *)

Section Defs.

Variable a : A.

Lemma in_alg_comm : commr_rmorph (in_alg A) a.

Definition horner_alg := horner_morph in_alg_comm.

Lemma horner_algC c : horner_alg c%:P = c%:A.

Lemma horner_algX : horner_alg 'X = a.

Fact horner_alg_is_lrmorphism : lrmorphism horner_alg.
Canonical horner_alg_additive := Additive horner_alg_is_lrmorphism.
Canonical horner_alg_rmorphism := RMorphism horner_alg_is_lrmorphism.
Canonical horner_alg_linear := AddLinear horner_alg_is_lrmorphism.
Canonical horner_alg_lrmorphism := [lrmorphism of horner_alg].

End Defs.

Variable (pf : {lrmorphism {poly R} A}).

Lemma poly_alg_initial : pf =1 horner_alg (pf 'X).

End HornerAlg.

Fact comp_poly_multiplicative q : multiplicative (comp_poly q).
Canonical comp_poly_rmorphism q := AddRMorphism (comp_poly_multiplicative q).
Canonical comp_poly_lrmorphism q := [lrmorphism of comp_poly q].

Lemma comp_polyM p q r : (p × q) \Po r = (p \Po r) × (q \Po r).

Lemma comp_polyA p q r : p \Po (q \Po r) = (p \Po q) \Po r.

Lemma horner_comp p q x : (p \Po q).[x] = p.[q.[x]].

Lemma root_comp p q x : root (p \Po q) x = root p (q.[x]).

Lemma deriv_comp p q : (p \Po q) ^ = (p ^ \Po q) × q^.

Lemma deriv_exp p n : (p ^+ n)^ = p^ × p ^+ n.-1 *+ n.

Definition derivCE := (derivE, deriv_exp).

End PolynomialComRing.

Canonical polynomial_countComRingType (R : countComRingType) :=
[countComRingType of polynomial R].
Canonical poly_countComRingType (R : countComRingType) :=
[countComRingType of {poly R}].

Section PolynomialIdomain.

Integral domain structure on poly
Variable R : idomainType.

Implicit Types (a b x y : R) (p q r m : {poly R}).

Lemma size_mul p q : p != 0 q != 0 size (p × q) = (size p + size q).-1.

Fact poly_idomainAxiom p q : p × q = 0 (p == 0) || (q == 0).

Definition poly_unit : pred {poly R} :=
fun p(size p == 1%N) && (p_0 \in GRing.unit).

Definition poly_inv p := if p \in poly_unit then (p_0)^-1%:P else p.

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

Fact poly_intro_unit p q : q × p = 1 p \in poly_unit.

Fact poly_inv_out : {in [predC poly_unit], poly_inv =1 id}.

Definition poly_comUnitMixin :=
ComUnitRingMixin poly_mulVp poly_intro_unit poly_inv_out.

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

Canonical poly_unitAlgType := Eval hnf in [unitAlgType R of {poly R}].
Canonical polynomial_unitAlgType := Eval hnf in [unitAlgType R of polynomial R].

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

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

Lemma poly_unitE p :
(p \in GRing.unit) = (size p == 1%N) && (p_0 \in GRing.unit).

Lemma poly_invE p : p ^-1 = if p \in GRing.unit then (p_0)^-1%:P else p.

Lemma polyCV c : c%:P^-1 = (c^-1)%:P.

Lemma rootM p q x : root (p × q) x = root p x || root q x.

Lemma rootZ x a p : a != 0 root (a *: p) x = root p x.

Lemma size_scale a p : a != 0 size (a *: p) = size p.

Lemma size_Cmul a p : a != 0 size (a%:P × p) = size p.

Lemma lead_coefM p q : lead_coef (p × q) = lead_coef p × lead_coef q.

Lemma lead_coefZ a p : lead_coef (a *: p) = a × lead_coef p.

Lemma scale_poly_eq0 a p : (a *: p == 0) = (a == 0) || (p == 0).

Lemma size_prod (I : finType) (P : pred I) (F : I {poly R}) :
( i, P i F i != 0)
size (\prod_(i | P i) F i) = ((\sum_(i | P i) size (F i)).+1 - #|P|)%N.

Lemma size_prod_seq (I : eqType) (s : seq I) (F : I {poly R}) :
( i, i \in s F i != 0)
size (\prod_(i <- s) F i) = ((\sum_(i <- s) size (F i)).+1 - size s)%N.

Lemma size_mul_eq1 p q :
(size (p × q) == 1%N) = ((size p == 1%N) && (size q == 1%N)).

Lemma size_prod_seq_eq1 (I : eqType) (s : seq I) (P : pred I) (F : I {poly R}) :
reflect ( i, P i && (i \in s) size (F i) = 1%N)
(size (\prod_(i <- s | P i) F i) == 1%N).

Lemma size_prod_eq1 (I : finType) (P : pred I) (F : I {poly R}) :
reflect ( i, P i size (F i) = 1%N)
(size (\prod_(i | P i) F i) == 1%N).

Lemma size_exp p n : (size (p ^+ n)).-1 = ((size p).-1 × n)%N.

Lemma lead_coef_exp p n : lead_coef (p ^+ n) = lead_coef p ^+ n.

Lemma root_prod_XsubC rs x :
root (\prod_(a <- rs) ('X - a%:P)) x = (x \in rs).

Lemma root_exp_XsubC n a x : root (('X - a%:P) ^+ n.+1) x = (x == a).

Lemma size_comp_poly p q :
(size (p \Po q)).-1 = ((size p).-1 × (size q).-1)%N.

Lemma lead_coef_comp p q : size q > 1
lead_coef (p \Po q) = (lead_coef p) × lead_coef q ^+ (size p).-1.

Lemma comp_poly_eq0 p q : size q > 1 (p \Po q == 0) = (p == 0).

Lemma size_comp_poly2 p q : size q = 2 size (p \Po q) = size p.

Lemma comp_poly2_eq0 p q : size q = 2 (p \Po q == 0) = (p == 0).

Theorem max_poly_roots p rs :
p != 0 all (root p) rs uniq rs size rs < size p.

Lemma roots_geq_poly_eq0 p (rs : seq R) : all (root p) rs uniq rs
(size rs size p)%N p = 0.

End PolynomialIdomain.

Canonical polynomial_countUnitRingType (R : countIdomainType) :=
[countUnitRingType of polynomial R].
Canonical poly_countUnitRingType (R : countIdomainType) :=
[countUnitRingType of {poly R}].
Canonical polynomial_countComUnitRingType (R : countIdomainType) :=
[countComUnitRingType of polynomial R].
Canonical poly_countComUnitRingType (R : countIdomainType) :=
[countComUnitRingType of {poly R}].
Canonical polynomial_countIdomainType (R : countIdomainType) :=
[countIdomainType of polynomial R].
Canonical poly_countIdomainType (R : countIdomainType) :=
[countIdomainType of {poly R}].

Section MapFieldPoly.

Variables (F : fieldType) (R : ringType) (f : {rmorphism F R}).

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

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

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

Lemma map_poly_inj : injective (map_poly f).

Lemma map_monic p : (p^f \is monic) = (p \is monic).

Lemma map_poly_com p x : comm_poly p^f (f x).

Lemma fmorph_root p x : root p^f (f x) = root p x.

Lemma fmorph_unity_root n z : n.-unity_root (f z) = n.-unity_root z.

Lemma fmorph_primitive_root n z :
n.-primitive_root (f z) = n.-primitive_root z.

End MapFieldPoly.

Section MaxRoots.

Variable R : unitRingType.
Implicit Types (x y : R) (rs : seq R) (p : {poly R}).

Definition diff_roots (x y : R) := (x × y == y × x) && (y - x \in GRing.unit).

Fixpoint uniq_roots rs :=
if rs is x :: rs' then all (diff_roots x) rs' && uniq_roots rs' else true.

Lemma uniq_roots_prod_XsubC p rs :
all (root p) rs uniq_roots rs
q, p = q × \prod_(z <- rs) ('X - z%:P).

Theorem max_ring_poly_roots p rs :
p != 0 all (root p) rs uniq_roots rs size rs < size p.

Lemma all_roots_prod_XsubC p rs :
size p = (size rs).+1 all (root p) rs uniq_roots rs
p = lead_coef p *: \prod_(z <- rs) ('X - z%:P).

End MaxRoots.

Section FieldRoots.

Variable F : fieldType.
Implicit Types (p : {poly F}) (rs : seq F).

Lemma poly2_root p : size p = 2 {r | root p r}.

Lemma uniq_rootsE rs : uniq_roots rs = uniq rs.

Section UnityRoots.

Variable n : nat.

Lemma max_unity_roots rs :
n > 0 all n.-unity_root rs uniq rs size rs n.

Lemma mem_unity_roots rs :
n > 0 all n.-unity_root rs uniq rs size rs = n
n.-unity_root =i rs.

Showing the existence of a primitive root requires the theory in cyclic.

Variable z : F.
Hypothesis prim_z : n.-primitive_root z.

Let zn := [seq z ^+ i | i <- index_iota 0 n].

Lemma factor_Xn_sub_1 : \prod_(0 i < n) ('X - (z ^+ i)%:P) = 'X^n - 1.

Lemma prim_rootP x : x ^+ n = 1 {i : 'I_n | x = z ^+ i}.

End UnityRoots.

End FieldRoots.

Section