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

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


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

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

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

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


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.
Lifting a ring predicate to polynomials.

Implicit Type S : {pred R}.

Definition polyOver S := [qualify a p : {poly R} | all [in 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.

Lemma polyOver_mulr_2closed :
  GRing.mulr_2closed kS GRing.mulr_2closed (polyOver kS).

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

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 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 polyOverP {R S0 addS kS p} : rename.
Arguments polyC_inj {R} [x1 x2] eq_x12P.
Arguments eq_poly {R n} [E1] E2 eq_E12.

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.

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

Canonical take_poly_additive m := Additive (take_poly_is_linear m).
Canonical take_poly_linear m := Linear (take_poly_is_linear 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).

Canonical drop_poly_additive m := Additive (drop_poly_is_linear m).
Canonical drop_poly_linear m := Linear (drop_poly_is_linear 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.

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 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%N
  (\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_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