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 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. 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_head h i (p : poly_of (Phant R)) := let: tt := h in 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)).
Notation coefp i := (coefp_head tt i).

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.
Definition poly_expanded_def n E := Poly (mkseq E n).
Fact poly_key : unit.
Definition poly := locked_with poly_key poly_expanded_def.
Canonical poly_unlockable := [unlockable fun poly].

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

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

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

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

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

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

Zmodule structure for polynomial
Definition add_poly_def p q := \poly_(i < maxn (size p) (size q)) (p`_i + q`_i).
Fact add_poly_key : unit.
Definition add_poly := locked_with add_poly_key add_poly_def.
Canonical add_poly_unlockable := [unlockable fun add_poly].

Definition opp_poly_def p := \poly_(i < size p) - p`_i.
Fact opp_poly_key : unit.
Definition opp_poly := locked_with opp_poly_key opp_poly_def.
Canonical opp_poly_unlockable := [unlockable fun opp_poly].

Fact coef_add_poly p q i : (add_poly p q)`_i = p`_i + q`_i.

Fact coef_opp_poly p i : (opp_poly p)`_i = - p`_i.

Fact add_polyA : associative add_poly.

Fact add_polyC : commutative add_poly.

Fact add_poly0 : left_id 0%:P add_poly.

Fact add_polyN : left_inverse 0%:P opp_poly add_poly.

Definition poly_zmodMixin :=
  ZmodMixin add_polyA add_polyC add_poly0 add_polyN.

Canonical poly_zmodType := Eval hnf in ZmodType {poly R} poly_zmodMixin.
Canonical polynomial_zmodType :=
  Eval hnf in ZmodType (polynomial R) poly_zmodMixin.

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 polyC_add : {morph polyC : a b / a + b}.

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

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

Canonical polyC_additive := Additive polyC_sub.

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

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

Lemma lead_coef_opp 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 polyC_mul : {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.
Definition scale_poly_def a (p : {poly R}) := \poly_(i < size p) (a × p`_i).
Fact scale_poly_key : unit.
Definition scale_poly := locked_with scale_poly_key scale_poly_def.
Canonical scale_poly_unlockable := [unlockable fun scale_poly].

Fact scale_polyE a p : scale_poly a p = a%:P × p.

Fact scale_polyA a b p : scale_poly a (scale_poly b p) = scale_poly (a × b) p.

Fact scale_1poly : left_id 1 scale_poly.

Fact scale_polyDr a : {morph scale_poly a : p q / p + q}.

Fact scale_polyDl p : {morph scale_poly^~ p : a b / a + b}.

Fact scale_polyAl a p q : scale_poly a (p × q) = scale_poly a p × q.

Definition poly_lmodMixin :=
  LmodMixin scale_polyA scale_1poly scale_polyDr scale_polyDl.

Canonical poly_lmodType :=
  Eval hnf in LmodType R {poly R} poly_lmodMixin.
Canonical polynomial_lmodType :=
  Eval hnf in LmodType R (polynomial R) poly_lmodMixin.
Canonical poly_lalgType :=
  Eval hnf in LalgType R {poly R} scale_polyAl.
Canonical polynomial_lalgType :=
  Eval hnf in LalgType R (polynomial R) scale_polyAl.

Lemma mul_polyC a p : a%:P × p = a *: p.

Lemma alg_polyC a : a%:A = a%:P :> {poly R}.

Lemma coefZ a p i : (a *: p)`_i = a × p`_i.

Lemma size_scale_leq a p : size (a *: p) size p.

Canonical coefp_linear i : {scalar {poly R}} :=
  AddLinear ((fun a(coefZ a) ^~ i) : scalable_for *%R (coefp i)).
Canonical coefp0_lrmorphism := [lrmorphism of coefp 0].

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
Lemma poly_def n E : \poly_(i < n) E i = \sum_(i < n) E i *: 'X^i.

Monic predicate
Definition monic := [qualify p | lead_coef p == 1].
Fact monic_key : pred_key monic.
Canonical monic_keyed := KeyedQualifier monic_key.

Lemma monicE p : (p \is monic) = (lead_coef p == 1).
Lemma monicP p : reflect (lead_coef p = 1) (p \is monic).

Lemma monic1 : 1 \is monic.
Lemma monicX : 'X \is monic.
Lemma monicXn n : 'X^n \is monic.

Lemma monic_neq0 p : p \is monic p != 0.

Lemma lead_coef_monicM p q : p \is monic lead_coef (p × q) = lead_coef q.

Lemma lead_coef_Mmonic p q : q \is monic lead_coef (p × q) = lead_coef p.

Lemma size_monicM p q :
  p \is monic q != 0 size (p × q) = (size p + size q).-1.

Lemma size_Mmonic p q :
  p != 0 q \is monic size (p × q) = (size p + size q).-1.

Lemma monicMl p q : p \is monic (p × q \is monic) = (q \is monic).

Lemma monicMr p q : q \is monic (p × q \is monic) = (p \is monic).

Fact monic_mulr_closed : mulr_closed monic.
Canonical monic_mulrPred := MulrPred monic_mulr_closed.

Lemma monic_exp p n : p \is monic p ^+ n \is monic.

Lemma monic_prod I rI (P : pred I) (F : I {poly R}):
  ( i, P i F i \is monic) \prod_(i <- rI | P i) F i \is monic.

Lemma monicXsubC c : 'X - c%:P \is monic.

Lemma monic_prod_XsubC I rI (P : pred I) (F : I R) :
  \prod_(i <- rI | P i) ('X - (F i)%:P) \is monic.

Lemma size_prod_XsubC I rI (F : I R) :
  size (\prod_(i <- rI) ('X - (F i)%:P)) = (size rI).+1.

Lemma size_exp_XsubC n a : size (('X - a%:P) ^+ n) = n.+1.

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 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.

Lemma size_Xn_sub_1 n : n > 0 size ('X^n - 1 : {poly R}) = n.+1.

Lemma monic_Xn_sub_1 n : n > 0 'X^n - 1 \is monic.

Definition root_of_unity n : pred R := root ('X^n - 1).

Lemma unity_rootE n z : n.-unity_root z = (z ^+ n == 1).

Lemma unity_rootP n z : reflect (z ^+ n = 1) (n.-unity_root z).

Definition primitive_root_of_unity n z :=
  (n > 0) && [ i : 'I_n, i.+1.-unity_root z == (i.+1 == n)].

Lemma prim_order_exists n z :
  n > 0 z ^+ n = 1 {m | m.-primitive_root z & (m %| n)}.

Section OnePrimitive.

Variables (n : nat) (z : R).
Hypothesis prim_z : n.-primitive_root z.

Lemma prim_order_gt0 : n > 0.
Let n_gt0 := prim_order_gt0.

Lemma prim_expr_order : z ^+ n = 1.

Lemma prim_expr_mod i : z ^+ (i %% n) = z ^+ i.

Lemma prim_order_dvd i : (n %| i) = (z ^+ i == 1).

Lemma eq_prim_root_expr i j : (z ^+ i == z ^+ j) = (i == j %[mod n]).

Lemma exp_prim_root k : (n %/ gcdn k n).-primitive_root (z ^+ k).

Lemma dvdn_prim_root m : (m %| n)%N m.-primitive_root (z ^+ (n %/ m)).

End OnePrimitive.

Lemma prim_root_exp_coprime n z k :
  n.-primitive_root z n.-primitive_root (z ^+ k) = coprime k n.

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.
Definition derivn n p := iter n deriv p.


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

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

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

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

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

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

Fact derivn_is_linear n : linear (derivn n).
Canonical derivn_additive n := Additive (derivn_is_linear n).
Canonical derivn_linear n := Linear (derivn_is_linear n).

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

Lemma derivnD n : {morph derivn n : p q / p + q}.

Lemma derivn_sub n : {morph derivn n : p q / p - q}.

Lemma derivnMn n m p : (p *+ m)^`(n) = p^`(n) *+ m.

Lemma derivnMNn n m p : (p *- m)^`(n) = p^`(n) *- m.

Lemma derivnN n : {morph derivn n : p / - p}.

Lemma derivnZ n : scalable (derivn n).

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

Lemma derivnMXaddC n p c :
  (p × 'X + c%:P)^`(n.+1) = p^`(n) *+ n.+1 + p^`(n.+1) × 'X.

Lemma derivn_poly0 p n : size p n p^`(n) = 0.

Lemma lt_size_deriv (p : {poly R}) : p != 0 size p^` < size p.

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

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


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

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 polyC_inv 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 MapPolyRoots.

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

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

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

End MapPolyRoots.

Section AutPolyRoot.
The action of automorphisms on roots of unity.

Variable F : fieldType.
Implicit Types u v : {rmorphism F F}.

Lemma aut_prim_rootP u z n :
  n.-primitive_root z {k | coprime k n & u z = z ^+ k}.

Lemma aut_unity_rootP u z n : n > 0 z ^+ n = 1 {k | u z = z ^+ k}.

Lemma aut_unity_rootC u v z n : n > 0 z ^+ n = 1 u (v z) = v (u z).

End AutPolyRoot.

Module UnityRootTheory.

Notation "n .-unity_root" := (root_of_unity n) : unity_root_scope.
Notation "n .-primitive_root" := (primitive_root_of_unity n) : unity_root_scope.
Open Scope unity_root_scope.

Definition unity_rootE := unity_rootE.
Definition unity_rootP := @unity_rootP.

Definition prim_order_exists := prim_order_exists.
Notation prim_order_gt0 := prim_order_gt0.
Notation prim_expr_order := prim_expr_order.
Definition prim_expr_mod := prim_expr_mod.
Definition prim_order_dvd := prim_order_dvd.
Definition eq_prim_root_expr := eq_prim_root_expr.

Definition rmorph_unity_root := rmorph_unity_root.
Definition fmorph_unity_root := fmorph_unity_root.
Definition fmorph_primitive_root := fmorph_primitive_root.
Definition max_unity_roots := max_unity_roots.
Definition mem_unity_roots := mem_unity_roots.
Definition prim_rootP := prim_rootP.

End UnityRootTheory.

Section DecField.

Variable F : decFieldType.

Lemma dec_factor_theorem (p : {poly F}) :
  {s : seq F & {q : {poly F} | p = q × \prod_(x <- s) ('X - x%:P)
                              (q != 0 x, ~~ root q x)}}.

End DecField.

Module PreClosedField.
Section UseAxiom.

Variable F : fieldType.
Hypothesis closedF : GRing.ClosedField.axiom F.
Implicit Type p : {poly F}.

Lemma closed_rootP p : reflect ( x, root p x) (size p != 1%N).

Lemma closed_nonrootP p : reflect ( x, ~~ root p x) (p != 0).

End UseAxiom.
End PreClosedField.

Section ClosedField.

Variable F : closedFieldType.
Implicit Type p : {poly F}.

Let closedF := @solve_monicpoly F.

Lemma closed_rootP p : reflect ( x, root p x) (size p != 1%N).

Lemma closed_nonrootP p : reflect ( x, ~~ root p x) (p != 0).

Lemma closed_field_poly_normal p :
  {r : seq F | p = lead_coef p *: \prod_(z <- r) ('X - z%:P)}.

End ClosedField.