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

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

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

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

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.

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

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

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

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
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}) :
( 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) = ((size p == 1) && (size q == 1)).

Lemma size_prod_seq_eq1 (I : eqType) (s : seq I) (P : pred I) (F : I {poly R}) :
reflect ( i, P i && (<