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 div ssralg countalg binomial tuple.

This file provides a library for univariate polynomials over ring structures; it also provides an extended theory for polynomials whose coefficients range over commutative rings and integral domains.
{poly R} == the type of polynomials with coefficients of type R, represented as lists with a non zero last element (big endian representation); the coefficient type R must have a canonical ringType structure cR. In fact {poly R} denotes the concrete type polynomial cR; R is just a phantom argument that lets type inference reconstruct the (hidden) ringType structure cR. p : seq R == the big-endian sequence of coefficients of p, via the coercion polyseq : polynomial >-> seq. Poly s == the polynomial with coefficient sequence s (ignoring trailing zeroes). \poly(i < n) E(i) == the polynomial of degree at most n - 1 whose coefficients are given by the general term E(i) 0, 1, - p, p + q, == the usual ring operations: {poly R} has a canonical p * q, p ^+ n, ... ringType structure, which is commutative / integral when R is commutative / integral, respectively. polyC c, c%:P == the constant polynomial c 'X == the (unique) variable 'X^n == a power of 'X; 'X^0 is 1, 'X^1 is convertible to 'X p`_i == the coefficient of 'X^i in p; this is in fact just the ring_scope notation generic seq-indexing using nth 0%R, combined with the polyseq coercion. coefp i == the linear function p |-> p`_i (self-exapanding). size p == 1 + the degree of p, or 0 if p = 0 (this is the generic seq function combined with polyseq). lead_coef p == the coefficient of the highest monomial in p, or 0 if p = 0 (hence lead_coef p = 0 iff p = 0) p \is monic <=> lead_coef p == 1 (0 is not monic). p \is a polyOver S <=> the coefficients of p satisfy S; S should have a key that should be (at least) an addrPred. p. [x] == the evaluation of a polynomial p at a point x using the Horner scheme

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

horner evaluation of a polynomial expression (resp., in a non commutative ring, with side conditions). p^`() == formal derivative of p p^`(n) == formal n-derivative of p p^`N(n) == formal n-derivative of p divided by n! p \Po q == polynomial composition; because this is naturally a a linear morphism in the first argument, this notation is transposed (q comes before p for redex selection, etc). := \sum(i < size p) p`_i *: q ^+ i 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}.


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.

Section PolynomialTheory.

Variable R : ringType.
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%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.


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


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


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.

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


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

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

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.

Section PolynomialComRing.

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

Fact poly_mul_comm p q : p × q = q × 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%N) && (p`_0 \in GRing.unit).

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

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

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

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



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

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

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

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

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

Lemma 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%N) = ((size p == 1%N) && (size q == 1%N)).

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

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

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

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

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

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

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

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

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

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

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

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

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

End PolynomialIdomain.

FIXME: these are seamingly artifical ways to close the inheritance graph We make parameters more and more precise to trigger completion by HB






Section MapFieldPoly.

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


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

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