Library poly

(c) Copyright Microsoft Corporation and Inria. All rights reserved. 
Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq choice fintype.
Require Import bigops ssralg.

This file provides a library for univariate polynomials over ring       
structures and proposes a theory for these objects when coefficients    
range over commutative rings and integral domains.                      
                                                                        
   polynomial R       == the type of polynomials over the ring R,       
                         represented as lists with a non zero last      
                         element (big endian representation)            
     + objects in this type should be casted by the {poly R} annotation 
   c %:P              == the constant polynomial c, 'X and 'X^n the     
                         monomials.                                     
   \poly_ ( i < n ) E == the polynomial of degree strictly less than n, 
                         whose coefficients are given by the general    
                         term E                                         
   p.[x]              == The evaluation of a polynomial p at a point x  
                         following the Horner schema                    
     + The multi-rule horner_lin (resp. horner_lin_com) unwinds horner  
       evaluation of a polynomial expression (resp. in a non            
       commutative case, under the appropriate assumptions)             
                                                                        
Degree is not defined as such, we rather use the size operation on      
sequences. Hence the zero polynomial is the only polynomial of size 0.  
                                                                        
   We define pseudo division on polynomials over an integral domain :   
       m %/ d == the pseudo-quotient                                    
       m %% d == the pseudo remainder                                   
       p %| q <=> q is a pseudo-divisor of p                            
                                                                        
   p %= q             == the equality modulo constant factors           
                      := (p %| q) && (q %| p)                           
      + In the case R is a field p and q are associate                  
                                                                        
      gcdp p q  == pseudo-gcd, for poly with coefficients in a ring,    
         idomain is only require of indempotence and commutativity      
                                                                        
      roots p   == roots of poly with coefficients in an idomain.       
We prove the factor_theorem, and the max_poly_roots inequality relating 
the number of distinct roots of a polynomial and its size               

Import Prenex Implicits.

Import GRing.Theory.
Open Local 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 "'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").

Notation Local simp := Monoid.simpm.

Section Polynomial.

Variable R : ringType.

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

Definition poly_of of phant R := polynomial.
Identity Coercion type_poly_of : poly_of >-> polynomial.
Notation "{ 'poly' T }" := (poly_of (Phant T)).

Implicit Types p q : {poly R}.


Canonical Structure polynomial_subType :=
  Eval hnf in [subType for polyseq by polynomial_rect].
Definition polynomial_eqMixin := Eval hnf in [eqMixin of polynomial by <:].
Canonical Structure polynomial_eqType := Eval hnf in EqType polynomial_eqMixin.
Definition polynomial_choiceMixin := [choiceMixin of polynomial by <:].
Canonical Structure polynomial_choiceType :=
  Eval hnf in ChoiceType polynomial_choiceMixin.
Canonical Structure poly_subType := Eval hnf in [subType of {poly R}].
Canonical Structure poly_eqType := Eval hnf in [eqType of {poly R}].
Canonical Structure poly_choiceType := Eval hnf in [choiceType of {poly R}].

Lemma poly_inj : injective polyseq. Qed.

Definition lead_coef p := p`_(size p).-1.
Lemma lead_coefE : forall p, lead_coef p = p`_(size p).-1. Qed.

Definition polyC c : {poly R} :=
  insubd (@Polynomial [::] (nonzero1r _)) [:: c].

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

Remember the boolean (c !=0) is coerced to 1 if true and 0 if false 
Lemma polyseqC : forall c, c%:P = nseq (c != 0) c :> seq R.

Lemma size_polyC : forall c, size c%:P = (c != 0).

Lemma coefC : forall c i, c%:P`_i = if i == 0%N then c else 0.

Lemma polyC_inj : injective polyC.

Lemma lead_coefC : forall c, lead_coef c%:P = c.

Extensional interpretation (poly <=> nat -> R) 
Lemma polyP : forall p1 p2, nth 0 p1 =1 nth 0 p2 <-> p1 = p2.

Lemma size1_polyC : forall p, size p <= 1 -> p = (p`_0)%:P.

Builds a polynomial by extension. 
Definition poly_cons c p : {poly R} :=
  if p is Polynomial ((_ :: _) as s) ns then @Polynomial (c :: s) ns else c%:P.

Lemma polyseq_cons : forall c p,
  poly_cons c p = (if size p != 0%N then c :: p else c%:P) :> seq R.

Lemma size_poly_cons : forall c p,
  size (poly_cons c p) =
    (if (size p == 0%N) && (c == 0) then 0%N else (size p).+1).

Lemma coef_cons : forall c p i,
  (poly_cons c p)`_i = if i == 0%N then c else p`_i.-1.

Builds a polynomial from a bare list of coefficients 
Definition Poly := foldr poly_cons 0%:P.

Lemma PolyK : forall c s, last c s != 0 -> Poly s = s :> seq R.

Lemma polyseqK : forall p, Poly p = p.

Lemma size_Poly : forall s, size (Poly s) <= size s.

Lemma coef_Poly : forall s i, (Poly s)`_i = s`_i.

Builds a polynomial from an infinite seq of coef and a bound 
Notation "\poly_ ( i < n ) E" := (Poly (mkseq (fun i : nat => E) n)).

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

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

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

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

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

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

Zmodule structure for polynomial 
Definition add_poly p1 p2 :=
  \poly_(i < maxn (size p1) (size p2)) (p1`_i + p2`_i).

Definition opp_poly p := \poly_(i < size p) - p`_i.

Lemma coef_add_poly : forall p1 p2 i, (add_poly p1 p2)`_i = p1`_i + p2`_i.

Lemma coef_opp_poly : forall p i, (opp_poly p)`_i = - p`_i.

Lemma add_polyA : associative add_poly.

Lemma add_polyC : commutative add_poly.

Lemma add_poly0 : left_id 0%:P add_poly.

Lemma add_poly_opp : left_inverse 0%:P opp_poly add_poly.

Definition poly_zmodMixin :=
  ZmodMixin add_polyA add_polyC add_poly0 add_poly_opp.
Canonical Structure poly_zmodType := Eval hnf in ZmodType poly_zmodMixin.
Canonical Structure polynomial_zmodType :=
  Eval hnf in [zmodType of polynomial for poly_zmodType].

Properties of the zero polynomial 

Lemma polyC0 : 0%:P = 0 :> {poly R}. Qed.

Lemma seq_poly0 : (0 : {poly R}) = [::] :> seq R.

Lemma size_poly0 : size (0 : {poly R}) = 0%N.

Lemma coef0 : forall i, (0 : {poly R})`_i = 0.

Lemma lead_coef0 : lead_coef 0 = 0. Qed.

Lemma size_poly_eq0 : forall p, (size p == 0%N) = (p == 0).

Lemma poly0Vpos : forall p, {p = 0} + {size p > 0}.

Lemma polySpred : forall p, p != 0 -> size p = (size p).-1.+1.

Lemma lead_coef_eq0 : forall p, (lead_coef p == 0) = (p == 0).

Lemma polyC_eq0 : forall c, (c%:P == 0) = (c == 0).

Size, leading coef, morphism properties of coef 
Lemma leq_size_coef : forall p i,
  (forall j, i <= j -> p`_j = 0) -> size p <= i.

Lemma leq_coef_size : forall p i, p`_i != 0 -> i < size p.

Lemma coef_add : forall p1 p2 i, (p1 + p2)`_i = p1`_i + p2`_i.

Lemma coef_opp : forall p i, (- p)`_i = - p`_i.

Lemma coef_sub : forall p1 p2 i, (p1 - p2)`_i = p1`_i - p2`_i.

Lemma coef_natmul : forall p n i, (p *+ n)`_i = p`_i *+ n.

Lemma coef_negmul : forall p n i, (p *- n)`_i = p`_i *- n.

Lemma coef_sum : forall I r (P : pred I) (F : I -> {poly R}) k,
  (\sum_(i <- r | P i) F i)`_k = \sum_(i <- r | P i) (F i)`_k.

Lemma polyC_add : {morph polyC : c1 c2 / c1 + c2}.

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

Lemma polyC_sub : {morph polyC : c1 c2 / c1 - c2}.

Lemma polyC_natmul : forall n, {morph polyC : c / c *+ n}.

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

Lemma lead_coef_opp : forall p, lead_coef (- p) = - lead_coef p.

Lemma size_add : forall p q, size (p + q) <= maxn (size p) (size q).

Lemma size_addl : forall p q, size p > size q -> size (p + q) = size p.

Lemma size_sum : forall I r (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_coef_addl : forall p q,
  size p > size q -> lead_coef (p + q) = lead_coef p.

And now the Ring structure. 

Definition mul_poly p1 p2 :=
  \poly_(i < (size p1 + size p2).-1) (\sum_(j < i.+1) p1`_j * p2`_(i - j)).

Lemma coef_mul_poly : forall p1 p2 i,
  (mul_poly p1 p2)`_i = \sum_(j < i.+1) p1`_j * p2`_(i - j)%N.

Lemma coef_mul_poly_rev : forall p1 p2 i,
  (mul_poly p1 p2)`_i = \sum_(j < i.+1) p1`_(i - j)%N * p2`_j.

Lemma mul_polyA : associative mul_poly.

Lemma mul_1poly : left_id 1%:P mul_poly.

Lemma mul_poly1 : right_id 1%:P mul_poly.

Lemma mul_poly_addl : left_distributive mul_poly +%R.

Lemma mul_poly_addr : right_distributive mul_poly +%R.

Lemma nonzero_poly1 : 1%:P != 0. Qed.

Definition poly_ringMixin :=
  RingMixin mul_polyA mul_1poly mul_poly1 mul_poly_addl mul_poly_addr
            nonzero_poly1.
Canonical Structure poly_ringType := Eval hnf in RingType poly_ringMixin.
Canonical Structure polynomial_ringType :=
   Eval hnf in [ringType of polynomial for poly_ringType].

Lemma polyC1 : 1%:P = 1. Qed.

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

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

Lemma coef1 : forall i, (1 : {poly R})`_i = (i == 0%N)%:R.

Lemma lead_coef1 : lead_coef 1 = 1. Qed.

Lemma coef_mul : forall p1 p2 i,
  (p1 * p2)`_i = \sum_(j < i.+1) p1`_j * p2`_(i - j)%N.

Lemma coef_mul_rev : forall p1 p2 i,
  (p1 * p2)`_i = \sum_(j < i.+1) p1`_(i - j)%N * p2`_j.

Lemma size_mul : forall p1 p2, size (p1 * p2) <= (size p1 + size p2).-1.

Lemma head_coef_mul : forall p q,
  (p * q)`_(size p + size q).-2 = lead_coef p * lead_coef q.

Lemma size_proper_mul : forall p q,
  lead_coef p * lead_coef q != 0 -> size (p * q) = (size p + size q).-1.

Lemma lead_coef_proper_mul : forall p q,
  let c := lead_coef p * lead_coef q in c != 0 -> lead_coef (p * q) = c.

Lemma size_exp : forall p n, size (p ^+ n) <= ((size p).-1 * n).+1.

Lemma coef_Cmul : forall c p i, (c%:P * p)`_i = c * p`_i.

Lemma coef_mulC : forall c p i, (p * c%:P)`_i = p`_i * c.

Lemma polyC_mul : {morph polyC : c1 c2 / c1 * c2}.

Lemma polyC_exp : forall n, {morph polyC : c / c ^+ n}.

Indeterminate, at last! 

Definition polyX := Poly [:: 0; 1].

Notation "'X" := polyX.

Lemma polyseqX : 'X = [:: 0; 1] :> seq R.

Lemma size_polyX : size 'X = 2. Qed.

Lemma coefX : forall i, 'X`_i = (i == 1%N)%:R.

Lemma lead_coefX : lead_coef 'X = 1.

Lemma comm_polyX : forall p, GRing.comm p 'X.

Lemma coef_mulX : forall p i, (p * 'X)`_i = (if i is i'.+1 then p`_i' else 0).

Lemma coef_Xmul : forall p i, ('X * p)`_i = (if i is i'.+1 then p`_i' else 0).

Lemma poly_cons_def : forall p a, poly_cons a p = p * 'X + a%:P.

Lemma poly_ind : forall K : {poly R} -> Type,
  K 0 -> (forall p c, K p -> K (p * 'X + c%:P)) -> (forall p, K p).

Lemma seq_mul_polyX : forall p, p != 0 -> p * 'X = 0 :: p :> seq R.

Lemma lead_coef_mulX : forall p, lead_coef (p * 'X) = lead_coef p.

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

Lemma coef_Xn : forall n i, 'X^n`_i = (i == n)%:R.

Lemma seq_polyXn : forall n, 'X^n = ncons n 0 [:: 1] :> seq R.

Lemma size_polyXn : forall n, size 'X^n = n.+1.

Lemma comm_polyXn : forall p n, GRing.comm p 'X^n.

Lemma lead_coefXn : forall n, lead_coef 'X^n = 1.

Lemma coef_Xn_mul : forall n p i,
  ('X^n * p)`_i = if i < n then 0 else p`_(i - n).

Lemma coef_mulXn : forall n p i,
  (p * 'X^n)`_i = if i < n then 0 else p`_(i - n).

Expansion of a polynomial as an indexed sum 
Lemma poly_def : forall n E, \poly_(i < n) E i = \sum_(i < n) (E i)%:P * 'X^i.

Monic predicate 

Definition monic p := lead_coef p == 1.

Lemma monic1 : monic 1. Qed.

Lemma monicX : monic 'X. Qed.

Lemma monicXn : forall n, monic 'X^n.

Lemma monic_neq0 : forall p, monic p -> p != 0.

Lemma lead_coef_monic_mul : forall p q,
  monic p -> lead_coef (p * q) = lead_coef q.

Lemma lead_coef_mul_monic : forall p q,
  monic q -> lead_coef (p * q) = lead_coef p.

Lemma size_monic_mul : forall p q,
  monic p -> q != 0 -> size (p * q) = (size p + size q).-1.

Lemma size_mul_monic : forall p q,
  p != 0 -> monic q -> size (p * q) = (size p + size q).-1.

Lemma monic_mull : forall p q, monic p -> monic (p * q) = monic q.

Lemma monic_mulr : forall p q, monic q -> monic (p * q) = monic p.

Lemma monic_exp : forall p n, monic p -> monic (p ^+ n).

Pseudo division, defined on an arbitrary ring 
Definition edivp_rec (q : {poly R}) :=
  let sq := size q in
  let cq := lead_coef q in
  fix loop (n : nat) (c : R) (qq r : {poly R}) {struct n} :=
    if size r < sq then (c, qq, r) else
    let m := (lead_coef r)%:P * 'X^(size r - sq) in
    let c1 := cq * c in
    let qq1 := qq * cq%:P + m in
    let r1 := r * cq%:P - m * q in
    if n is n1.+1 then loop n1 c1 qq1 r1 else (c1, qq1, r1).

Lemma edivp_mon_spec : forall p q n c qq r,
   monic q -> let d := edivp_rec q n c qq r in
 p = qq * q + r -> p = (d.1).2 * q + d.2.

Lemma edivp_mod_spec : forall q n c (qq r : {poly R}),
  q != 0 -> size r <= n -> size (edivp_rec q n c qq r).2 < size q.

Lemma edivp_scal_spec: forall q n c (qq r : {poly R}),
  exists m, (edivp_rec q n c qq r).1.1 = lead_coef q ^+ m * c.

Definition edivp (p q : {poly R}) : R * {poly R} * {poly R} :=
  if q == 0 then (1, 0, p) else edivp_rec q (size p) 1 0 p.

Definition divp p q := ((edivp p q).1).2.
Definition modp p q := (edivp p q).2.
Definition scalp p q := ((edivp p q).1).1.
Definition dvdp p q := modp q p == 0.

Notation "m %/ d" := (divp m d) (at level 40, no associativity).
Notation "m %% d" := (modp m d) (at level 40, no associativity).
Notation "p %| q" := (dvdp p q) (at level 70, no associativity).

Lemma divp_size : forall p q, size p < size q -> p %/ q = 0.

Lemma modp_size : forall p q, size p < size q -> p %% q = p.

Lemma divp_mon_spec : forall p q, monic q -> p = p %/ q * q + p %% q.

Lemma modp_spec : forall p q, q != 0 -> size (p %% q) < size q.

Lemma scalp_spec : forall p q, exists m, scalp p q = lead_coef q ^+ m.

Lemma div0p : forall p, 0 %/ p = 0.

Lemma modp0 : forall p, p %% 0 = p.

Lemma mod0p : forall p, 0 %% p = 0.

Lemma dvdpPm : forall p q, monic q -> reflect (exists qq, p = qq * q) (q %| p).

Lemma dvdp0: forall p, p %| 0.

Lemma modpC: forall p c, c != 0 -> p %% c%:P = 0.

Lemma modp1: forall p, p %% 1 = 0.

Lemma divp1: forall p, p %/ 1 = p.

Lemma dvd1p: forall p, 1 %| p.

Lemma modp_mon_mull : forall p q, monic q -> p * q %% q = 0.

Lemma divp_mon_mull : forall p q, monic q -> p * q %/ q = p.

Lemma dvdp_mon_mull : forall p q, monic q -> q %| p * q.

Pseudo gcd 
Definition gcdp p q :=
  let: (p1, q1) := if size p < size q then (q, p) else (p, q) in
  if p1 == 0 then q1 else
  let fix loop (n : nat) (pp qq : {poly R}) {struct n} :=
      let rr := pp %% qq in
      if rr == 0 then qq else
      if n is n1.+1 then loop n1 qq rr else rr in
  loop (size p1) p1 q1.

Lemma gcd0p : left_id 0 gcdp.

Lemma gcdp0 : right_id 0 gcdp.

Lemma gcdpE : forall p q,
  gcdp p q = if size p < size q then gcdp (q %% p) p else gcdp (p %% q) q.

End Polynomial.

Notation "{ 'poly' T }" := (poly_of (Phant T)) : type_scope.
Notation "\poly_ ( i < n ) E" := (Poly (mkseq (fun i => E) n)) : ring_scope.
Notation "c %:P" := (polyC c) : ring_scope.
Notation "'X" := (polyX _) : ring_scope.
Notation "''X^' n" := ('X ^+ n) : ring_scope.
Notation "m %/ d" := (divp m d) (at level 40, no associativity) : ring_scope.
Notation "m %% d" := (modp m d) (at level 40, no associativity) : ring_scope.
Notation "p %| q" := (dvdp p q) (at level 70, no associativity) : ring_scope.

Horner evaluation of polynomials 

Section EvalPolynomial.

Variable R : ringType.
Implicit Types p q : {poly R}.
Implicit Types x a c : R.

Fixpoint horner s x {struct s} :=
  if s is a :: s' then horner s' x * x + a else 0.

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

Lemma horner0 : forall x, (0 : {poly R}).[x] = 0.

Lemma hornerC : forall c x, (c%:P).[x] = c.

Lemma hornerX : forall x, 'X.[x] = x.

Lemma horner_cons : forall p c x, (poly_cons c p).[x] = p.[x] * x + c.

Lemma horner_Poly : forall s x, (Poly s).[x] = horner s x.

Lemma horner_coef : forall p x,
  p.[x] = \sum_(i < size p) p`_i * x ^+ i.

Lemma horner_coef_wide : forall n p x,
  size p <= n -> p.[x] = \sum_(i < n) p`_i * x ^+ i.

Lemma horner_poly : forall n E x,
  (\poly_(i < n) E i).[x] = \sum_(i < n) E i * x ^+ i.

Lemma horner_opp : forall p x, (- p).[x] = - p.[x].

Lemma horner_add : forall p q x, (p + q).[x] = p.[x] + q.[x].

Lemma horner_sum : forall I r (P : pred I) F x,
  (\sum_(i <- r | P i) F i).[x] = \sum_(i <- r | P i) (F i).[x].

Lemma horner_Cmul : forall c p x, (c%:P * p).[x] = c * p.[x].

Definition com_coef p (x : R) := forall i, p`_i * x = x * p`_i.

Definition com_poly p x := x * p.[x] = p.[x] * x.

Lemma com_coef_poly : forall p x, com_coef p x -> com_poly p x.

Lemma com_poly0 : forall x, com_poly 0 x.

Lemma com_poly1 : forall x, com_poly 1 x.

Lemma com_polyX : forall x, com_poly 'X x.

Lemma horner_mul_com : forall p q x,
  com_poly q x -> (p * q).[x] = p.[x] * q.[x].

Lemma horner_exp_com : forall p x n, com_poly p x -> (p ^+ n).[x] = p.[x] ^+ n.

Lemma hornerXn : forall x n, ('X^n).[x] = x ^+ n.

Definition horner_lin_com :=
  (horner_add, horner_opp, hornerX, hornerC, horner_cons,
   simp, horner_Cmul, (fun p x => horner_mul_com p (com_polyX x))).

Lemma factor0 : forall c, ('X - c%:P).[c] = 0.

Lemma seq_factor : forall c, 'X - c%:P = [:: - c; 1] :> seq R.

Lemma monic_factor : forall c, monic ('X - c%:P).

Theorem factor_theorem : forall p c,
  reflect (exists q, p = q * ('X - c%:P)) (p.[c] == 0).

Lemma root_factor_theorem : forall (p : {poly R}) x,
  p.[x] == 0 = ('X - x%:P %| p).

End EvalPolynomial.

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

Section PolynomialComRing.

Variable R : comRingType.

Lemma horner_mul : forall (p q : {poly R}) x,
  (p * q).[x] = p.[x] * q.[x].

Lemma horner_exp : forall (p : {poly R}) x n, (p ^+ n).[x] = p.[x] ^+ n.

Definition horner_lin :=
  (horner_add, horner_opp, hornerX, hornerC, horner_cons,
   simp, horner_Cmul, horner_mul).

Lemma poly_mulC : forall p1 p2 : {poly R}, p1 * p2 = p2 * p1.

Canonical Structure poly_comRingType := Eval hnf in ComRingType poly_mulC.
Canonical Structure polynomial_comRingType :=
  Eval hnf in [comRingType of polynomial R for poly_comRingType].

Pseudo-division in a commutative setting 

Lemma edivp_spec: forall (p q: {poly R}) n c qq r,
  let d := edivp_rec q n c qq r in
  c%:P * p = qq * q + r -> (d.1).1%:P * p = (d.1).2 * q + d.2.

Lemma divp_spec: forall p q : {poly R}, (scalp p q)%:P * p = p %/ q * q + p %% q.

End PolynomialComRing.

Section PolynomialIdomain.

Variable R : idomainType.
Implicit Types x y : R.
Implicit Types p q : {poly R}.

Lemma size_mul_id : forall p q,
  p != 0 -> q != 0 -> size (p * q) = (size p + size q).-1.

Lemma size_polyC_mul: forall c p, c != 0 -> size (c%:P * p) = size p.

Lemma lead_coef_mul_id: forall p q,
  lead_coef (p * q) = lead_coef p * lead_coef q.

Lemma scalp_id: forall p q, scalp p q != 0.

idomain structure on poly 

Lemma poly_idomainMixin : forall p q, p * q = 0 -> (p == 0) || (q == 0).

Definition poly_unit : pred {poly R} :=
  fun p => (size p == 1%N) && GRing.unit p`_0.

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

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

Lemma poly_intro_unit : forall p q, q * p = 1 -> poly_unit p.

Lemma poly_inv_out : {in predC poly_unit, poly_inv =1 id}.

Definition poly_unitRingMixin :=
  ComUnitRingMixin poly_mulVp poly_intro_unit poly_inv_out.

Canonical Structure poly_unitRingType :=
   Eval hnf in UnitRingType poly_unitRingMixin.

Canonical Structure poly_comUnitRingType :=
   Eval hnf in ComUnitRingType poly_unitRingMixin.

Canonical Structure poly_idomainType :=
   Eval hnf in IdomainType poly_idomainMixin.

Canonical Structure polynomial_unitRingType :=
   Eval hnf in [unitRingType of polynomial R for poly_unitRingType].

Canonical Structure polynomial_comUnitRingType :=
   Eval hnf in [comUnitRingType of polynomial R for poly_comUnitRingType].

Canonical Structure polynomial_idomainType :=
   Eval hnf in [idomainType of polynomial R for poly_idomainType].

Lemma modp_mull : forall p q, p * q %% q = 0.

Lemma modpp : forall p, p %% p = 0.

Lemma dvdpp : forall p, p %| p.

Lemma divp_mull : forall p q, q != 0 -> p * q %/ q = (scalp (p * q) q)%:P * p.

Lemma dvdpPc : forall p q,
  reflect (exists c, exists qq, c != 0 /\ c%:P * p = qq * q) (q %| p).

Lemma size_dvdp : forall p1 p2, p2 != 0 -> p1 %| p2 -> size p1 <= size p2.

Lemma dvdp_mull : forall d m n : {poly R}, d %| n -> d %| m * n.

Lemma dvdp_mulr: forall d m n: {poly R}, d %| m -> d %| m * n.

Lemma dvdp_mul: forall d1 d2 m1 m2 : {poly R},
  d1 %| m1 -> d2 %| m2 -> d1 * d2 %| m1 * m2.

Lemma dvdp_trans: forall n d m : {poly R}, d %| n -> n %| m -> d %| m.

Lemma dvdp_addr : forall m d n : {poly R},
  d %| m -> (d %| m + n) = (d %| n).

Lemma dvdp_addl : forall n d m : {poly R},
  d %| n -> (d %| m + n) = (d %| m).

Lemma dvdp_add : forall d m n: {poly R}, d %| m -> d %| n -> d %| m + n.

Lemma dvdp_add_eq : forall d m n: {poly R},
  d %| m + n -> (d %| m) = (d %| n).

Lemma dvdp_subr : forall d m n: {poly R},
  d %| m -> (d %| m - n) = (d %| n).

Lemma dvdp_subl : forall d m n: {poly R},
  d %| n -> (d %| m - n) = (d %| m).

Lemma dvdp_sub : forall d m n: {poly R}, d %| m -> d %| n -> d %| m - n.

Lemma dvdp_mod : forall d m n : {poly R},
  d %| m -> (d %| n) = (d %| n %% m).

Lemma gcdpp : idempotent (@gcdp R).

Lemma dvdp_gcd2 : forall m n : {poly R}, (gcdp m n %| m) && (gcdp m n %| n).

Lemma dvdp_gcdl : forall m n : {poly R}, gcdp m n %| m.

Lemma dvdp_gcdr : forall m n : {poly R}, gcdp m n %| n.

Lemma dvdp_gcd : forall p m n: {poly R}, p %| gcdp m n = (p %| m) && (p %| n).

Equality modulo constant factors 

Definition eqp (R : ringType)(p1 p2: {poly R}) := (p1 %| p2) && (p2 %| p1).

Notation "p1 '%=' p2" := (eqp p1 p2)
  (at level 70, no associativity).

Lemma eqpP: forall m n: {poly R},
  reflect (exists c1, exists c2, [/\ c1 != 0, c2 != 0 & c1%:P * m = c2%:P * n])
          (m %= n).

Lemma eqpxx: forall p, p %= p.

Lemma eqp_sym: forall p1 p2, (p1 %= p2) = (p2 %= p1).

Lemma eqp_trans : forall p1 p2 p3, p1 %= p2 -> p2 %= p3 -> p1 %= p3.

Lemma eqp0E : forall p, (p %= 0) = (p == 0).

Lemma size_eqp: forall p1 p2, p1 %= p2 -> size p1 = size p2.

Now we can state that gcd is commutative modulo a factor 
Lemma gcdpC: forall p1 p2, gcdp p1 p2 %= gcdp p2 p1.

End PolynomialIdomain.

Section MaxRoots.

Variable R : unitRingType.

Definition roots (p : {poly R}) : pred R := fun x => p.[x] == 0.

Definition diff_root (x y : R) := (x * y == y * x) && GRing.unit (y - x).

Fixpoint uniq_roots (rs : seq R) {struct rs} :=
  if rs is x :: rs' then all (diff_root x) rs' && uniq_roots rs' else true.

Theorem max_ring_poly_roots : forall (p : {poly R}) rs,
  p != 0 -> all (roots p) rs -> uniq_roots rs -> size rs < size p.

End MaxRoots.

Theorem max_poly_roots : forall (F : fieldType) (p : polynomial F) rs,
  p != 0 -> all (roots p) rs -> uniq rs -> size rs < size p.