Library mathcomp.algebra.poly

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

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

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.

The multi-rule coefE simplifies p`_i

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 odd_poly p == monomials of odd degree of p even_poly p == monomials of even degree of p take_poly n p == polynomial p without its monomials of degree >= n drop_poly n p == polynomial p divided by X^n 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). Pdeg2.Field (exported by the present library) : theory of the degree 2 polynomials. Pdeg2.FieldMonic : theory of Pdeg2.Field specialized to monic polynomials.

Set Implicit Arguments.

Declare Scope unity_root_scope.

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

Local Notation simp := Monoid.simpm.

Section Polynomial.

Variable R : semiRingType.

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


Lemma poly_inj : injective polyseq.

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

Local Notation "{poly}" := (poly_of (Phant R)).


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.
Bind Scope ring_scope with poly_of.
Bind Scope ring_scope with polynomial.
Arguments polyseq {R} p%R.
Arguments poly_inj {R} [p1%R p2%R] : rename.
Arguments coefp {R} i%N / p%R.
Notation "{ 'poly' T }" := (poly_of (Phant T)) : type_scope.

Section SemiPolynomialTheory.

Variable R : semiRingType.
Implicit Types (a b c x y z : R) (p q r d : {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].

Local Notation "c %:P" := (polyC 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 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 else (size p).+1).

Lemma coef_cons c p i : (cons_poly c p)`_i = if i == 0 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].
Local Notation "\poly_ ( i < n ) E" := (poly n (fun i : natE)).

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.

Nmodule 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) = (p == 0).

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

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

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

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

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 semiring 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 mul_0poly : left_zero 0%:P mul_poly.

Fact mul_poly0 : right_zero 0%:P mul_poly.

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


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

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

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

Lemma coef1 i : (1 : {poly R})`_i = (i == 0)%: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}.

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

End SemiPolynomialTheory.

Section PolynomialTheory.

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

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

Local Notation "\poly_ ( i < n ) E" := (poly n (fun i : natE)).

Zmodule structure for polynomial
Size, leading coef, morphism properties of coef

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

Lemma coefB p q i : (p - q)`_i = p`_i - q`_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 polyCN : {morph (@polyC R) : c / - c}.

Lemma polyCB : {morph (@polyC R) : a b / a - b}.


Lemma polyCMn n : {morph (@polyC R) : c / c *+ n}.

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

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

Polynomial ring structure.
Algebra structure of polynomials.
The indeterminate, at last!
Definition polyX_def := @Poly R [:: 0; 1].
Fact polyX_key : unit.
Definition polyX : {poly R} := locked_with polyX_key polyX_def.
Canonical polyX_unlockable := [unlockable of polyX].
Local Notation "'X" := 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)%: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.

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

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

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 size_mulXn n p : p != 0 size (p × 'X^n) = (n + size p)%N.

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

Lemma coef_sumMXn I (r : seq I) (P : pred I) (p : I R) (n : I nat) k :
  (\sum_(i <- r | P i) p i *: 'X^(n i))`_k =
    \sum_(i <- r | P i && (n i == k)) p i.

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.

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

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 comm_polyD p q x: comm_poly p x comm_poly q x comm_poly (p + q) 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 comm_polyM p q x: comm_poly p x comm_poly q x comm_poly (p × q) x.

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

Lemma comm_poly_exp p n x: comm_poly p x comm_poly (p ^+ n) x.

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).
Local Notation "n .-unity_root" := (root_of_unity n) : ring_scope.

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)].
Local Notation "n .-primitive_root" := (primitive_root_of_unity n) : ring_scope.

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

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

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

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

Lemma polyOver_deriv (ringS : semiringClosed R) :
  {in polyOver ringS, p, p^`() \is a polyOver ringS}.

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.

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.

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

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 (ringS : semiringClosed R) :
  {in polyOver ringS, p n, p^`(n) \is a polyOver ringS}.

Fact derivn_is_linear n : linear (derivn n).

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

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

Lemma derivnB 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)).

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

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 (ringS : semiringClosed R) :
  {in polyOver ringS, p n, p^`N(n) \in polyOver ringS}.

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

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 : ( i, i < n E1 i = E2 i)
  poly n E1 = poly n E2 :> {poly R}.

End PolynomialTheory.

Arguments monic {R}.
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.

Arguments monic_pred _ _ /.
Arguments monicP {R p}.
Arguments rootP {R p x}.
Arguments rootPf {R p x}.
Arguments rootPt {R p x}.
Arguments unity_rootP {R n z}.
Arguments polyOver_pred _ _ _ /.
Arguments polyOverP {R S p}.
Arguments polyC_inj {R} [x1 x2] eq_x12P.
Arguments eq_poly {R n} [E1] E2 eq_E12.

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).
Local Notation "p ^f" := (map_poly f p) : ring_scope.

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

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

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

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

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

Fact map_poly_is_multiplicative : multiplicative (map_poly f).


Lemma map_polyZ c p : (c *: p)^f = f c *: p^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_linear : linear_for (f \; *%R) (horner_morph cfu).

Fact horner_is_multiplicative : multiplicative (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].

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

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 (ringS : semiringClosed R) :
  {in polyOver ringS &, p q, p \Po q \in polyOver ringS}.

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

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.

Lemma comp_Xn_poly p n : 'X^n \Po p = p ^+ n.

Lemma coef_comp_poly_Xn p n i : 0 < n
  (p \Po 'X^n)`_i = if n %| i then p`_(i %/ n) else 0.

Lemma comp_poly_Xn p n : 0 < n
  p \Po 'X^n = \poly_(i < size p × n) if n %| i then p`_(i %/ n) else 0.

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

Variable R : ringType.

Implicit Type p q : {poly R}.

Even part of a polynomial
Odd part of a polynomial
Decomposition in odd and even part
take and drop for polynomials

Definition take_poly m p := \poly_(i < m) p`_i.

Lemma size_take_poly m p : size (take_poly m p) m.

Lemma coef_take_poly m p i : (take_poly m p)`_i = if i < m then p`_i else 0.

Lemma take_poly_id m p : size p m take_poly m p = p.

Lemma take_polyD m p q : take_poly m (p + q) = take_poly m p + take_poly m q.

Lemma take_polyZ k m p : take_poly m (k *: p) = k *: take_poly m p.

Fact take_poly_is_linear m : linear (take_poly m).


Lemma take_poly_sum m I r P (p : I {poly R}) :
  take_poly m (\sum_(i <- r | P i) p i) = \sum_(i <- r| P i) take_poly m (p i).

Lemma take_poly0l p : take_poly 0 p = 0.

Lemma take_poly0r m : take_poly m 0 = 0.

Lemma take_polyMXn m n p :
  take_poly m (p × 'X^n) = take_poly (m - n) p × 'X^n.

Lemma take_polyMXn_0 n p : take_poly n (p × 'X^n) = 0.

Lemma take_polyDMXn n p q : size p n take_poly n (p + q × 'X^n) = p.

Definition drop_poly m p := \poly_(i < size p - m) p`_(i + m).

Lemma coef_drop_poly m p i : (drop_poly m p)`_i = p`_(i + m).

Lemma drop_poly_eq0 m p : size p m drop_poly m p = 0.

Lemma size_drop_poly n p : size (drop_poly n p) = (size p - n)%N.

Lemma sum_drop_poly n p :
  \sum_(n i < size p) p`_i *: 'X^i = drop_poly n p × 'X^n.

Lemma drop_polyD m p q : drop_poly m (p + q) = drop_poly m p + drop_poly m q.

Lemma drop_polyZ k m p : drop_poly m (k *: p) = k *: drop_poly m p.

Fact drop_poly_is_linear m : linear (drop_poly m).


Lemma drop_poly_sum m I r P (p : I {poly R}) :
  drop_poly m (\sum_(i <- r | P i) p i) = \sum_(i <- r | P i) drop_poly m (p i).

Lemma drop_poly0l p : drop_poly 0 p = p.

Lemma drop_poly0r m : drop_poly m 0 = 0.

Lemma drop_polyMXn m n p :
  drop_poly m (p × 'X^n) = drop_poly (m - n) p × 'X^(n - m).

Lemma drop_polyMXn_id n p : drop_poly n (p × 'X^ n) = p.

Lemma drop_polyDMXn n p q : size p n drop_poly n (p + q × 'X^n) = q.

Lemma poly_take_drop n p : take_poly n p + drop_poly n p × 'X^n = p.

Lemma eqp_take_drop n p q :
  take_poly n p = take_poly n q drop_poly n p = drop_poly n q p = q.

End Surgery.

Definition coefE :=
  (coef0, coef1, coefC, coefX, coefXn, coef_sumMXn,
   coefZ, coefMC, coefCM, coefXnM, coefMXn, coefXM, coefMX, coefMNn, coefMn,
   coefN, coefB, coefD, coef_even_poly, coef_odd_poly,
   coef_take_poly, coef_drop_poly, coef_cons, coef_Poly, coef_poly,
   coef_deriv, coef_nderivn, coef_derivn, coef_map, coef_sum,
   coef_comp_poly_Xn, coef_comp_poly).

Section PolynomialComRing.

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

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


Lemma coef_prod_XsubC (ps : seq R) (n : nat) :
  (n size ps)%N
  (\prod_(p <- ps) ('X - p%:P))`_n =
  (-1) ^+ (size ps - n)%N ×
    \sum_(I in {set 'I_(size ps)} | #|I| == (size ps - n)%N)
        \prod_(i in I) ps`_i.

Lemma coefPn_prod_XsubC (ps : seq R) : size ps != 0
  (\prod_(p <- ps) ('X - p%:P))`_((size ps).-1) =
  - \sum_(p <- ps) p.

Lemma coef0_prod_XsubC (ps : seq R) :
  (\prod_(p <- ps) ('X - p%:P))`_0 =
  (-1) ^+ (size ps) × \prod_(p <- ps) p.

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_exp,
   simp, hornerCM, hornerZ, hornerM, horner_cons).

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

Fact horner_eval_is_linear x : linear_for *%R (horner_eval x).

Fact horner_eval_is_multiplicative x : multiplicative (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.


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

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.

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) && (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}.



Lemma poly_unitE p :
  (p \in GRing.unit) = (size p == 1) && (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 root_exp p n a: comm_poly p a (0 < n)%N root (p ^+ n) a = root p a.

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}) :