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.
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.
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].
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.
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)
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.
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.
Lemma PolyK c s : last c s != 0 → Poly s = s :> seq R.
Lemma polyseqK p : Poly p = p.
Lemma size_Poly s : size (Poly s) ≤ size s.
Lemma coef_Poly s i : (Poly s)`_i = s`_i.
Build a polynomial from an infinite sequence of coefficients and a bound.
Definition poly_expanded_def n E := Poly (mkseq E n).
Fact poly_key : unit.
Definition poly := locked_with poly_key poly_expanded_def.
Canonical poly_unlockable := [unlockable fun poly].
Lemma polyseq_poly n E :
E n.-1 != 0 → \poly_(i < n) E i = mkseq [eta E] n :> seq R.
Lemma size_poly n E : size (\poly_(i < n) E i) ≤ n.
Lemma size_poly_eq n E : E n.-1 != 0 → size (\poly_(i < n) E i) = n.
Lemma coef_poly n E k : (\poly_(i < n) E i)`_k = (if k < n then E k else 0).
Lemma lead_coef_poly n E :
n > 0 → E n.-1 != 0 → lead_coef (\poly_(i < n) E i) = E n.-1.
Lemma coefK p : \poly_(i < size p) p`_i = p.
Fact poly_key : unit.
Definition poly := locked_with poly_key poly_expanded_def.
Canonical poly_unlockable := [unlockable fun poly].
Lemma polyseq_poly n E :
E n.-1 != 0 → \poly_(i < n) E i = mkseq [eta E] n :> seq R.
Lemma size_poly n E : size (\poly_(i < n) E i) ≤ n.
Lemma size_poly_eq n E : E n.-1 != 0 → size (\poly_(i < n) E i) = n.
Lemma coef_poly n E k : (\poly_(i < n) E i)`_k = (if k < n then E k else 0).
Lemma lead_coef_poly n E :
n > 0 → E n.-1 != 0 → lead_coef (\poly_(i < n) E i) = E n.-1.
Lemma coefK p : \poly_(i < size p) p`_i = p.
Zmodule structure for polynomial
Definition add_poly_def p q := \poly_(i < maxn (size p) (size q)) (p`_i + q`_i).
Fact add_poly_key : unit.
Definition add_poly := locked_with add_poly_key add_poly_def.
Canonical add_poly_unlockable := [unlockable fun add_poly].
Definition opp_poly_def p := \poly_(i < size p) - p`_i.
Fact opp_poly_key : unit.
Definition opp_poly := locked_with opp_poly_key opp_poly_def.
Canonical opp_poly_unlockable := [unlockable fun opp_poly].
Fact coef_add_poly p q i : (add_poly p q)`_i = p`_i + q`_i.
Fact coef_opp_poly p i : (opp_poly p)`_i = - p`_i.
Fact add_polyA : associative add_poly.
Fact add_polyC : commutative add_poly.
Fact add_poly0 : left_id 0%:P add_poly.
Fact add_polyN : left_inverse 0%:P opp_poly add_poly.
Fact add_poly_key : unit.
Definition add_poly := locked_with add_poly_key add_poly_def.
Canonical add_poly_unlockable := [unlockable fun add_poly].
Definition opp_poly_def p := \poly_(i < size p) - p`_i.
Fact opp_poly_key : unit.
Definition opp_poly := locked_with opp_poly_key opp_poly_def.
Canonical opp_poly_unlockable := [unlockable fun opp_poly].
Fact coef_add_poly p q i : (add_poly p q)`_i = p`_i + q`_i.
Fact coef_opp_poly p i : (opp_poly p)`_i = - p`_i.
Fact add_polyA : associative add_poly.
Fact add_polyC : commutative add_poly.
Fact add_poly0 : left_id 0%:P add_poly.
Fact add_polyN : left_inverse 0%:P opp_poly add_poly.
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).
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.
Definition scale_poly_def a (p : {poly R}) := \poly_(i < size p) (a × p`_i).
Fact scale_poly_key : unit.
Definition scale_poly := locked_with scale_poly_key scale_poly_def.
Canonical scale_poly_unlockable := [unlockable fun scale_poly].
Fact scale_polyE a p : scale_poly a p = a%:P × p.
Fact scale_polyA a b p : scale_poly a (scale_poly b p) = scale_poly (a × b) p.
Fact scale_1poly : left_id 1 scale_poly.
Fact scale_polyDr a : {morph scale_poly a : p q / p + q}.
Fact scale_polyDl p : {morph scale_poly^~ p : a b / a + b}.
Fact scale_polyAl a p q : scale_poly a (p × q) = scale_poly a p × q.
Lemma mul_polyC a p : a%:P × p = a *: p.
Lemma alg_polyC a : a%:A = a%:P :> {poly R}.
Lemma coefZ a p i : (a *: p)`_i = a × p`_i.
Lemma size_scale_leq a p : size (a *: p) ≤ size p.
Fact scale_poly_key : unit.
Definition scale_poly := locked_with scale_poly_key scale_poly_def.
Canonical scale_poly_unlockable := [unlockable fun scale_poly].
Fact scale_polyE a p : scale_poly a p = a%:P × p.
Fact scale_polyA a b p : scale_poly a (scale_poly b p) = scale_poly (a × b) p.
Fact scale_1poly : left_id 1 scale_poly.
Fact scale_polyDr a : {morph scale_poly a : p q / p + q}.
Fact scale_polyDl p : {morph scale_poly^~ p : a b / a + b}.
Fact scale_polyAl a p q : scale_poly a (p × q) = scale_poly a p × q.
Lemma mul_polyC a p : a%:P × p = a *: p.
Lemma alg_polyC a : a%:A = a%:P :> {poly R}.
Lemma coefZ a p i : (a *: p)`_i = a × p`_i.
Lemma size_scale_leq a p : size (a *: p) ≤ size p.
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.
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
Definition monic_pred := fun p ⇒ lead_coef p == 1.
Arguments monic_pred _ /.
Definition monic := [qualify p | monic_pred p].
Lemma monicE p : (p \is monic) = (lead_coef p == 1).
Lemma monicP p : reflect (lead_coef p = 1) (p \is monic).
Lemma monic1 : 1 \is monic.
Lemma monicX : 'X \is monic.
Lemma monicXn n : 'X^n \is monic.
Lemma monic_neq0 p : p \is monic → p != 0.
Lemma lead_coef_monicM p q : p \is monic → lead_coef (p × q) = lead_coef q.
Lemma lead_coef_Mmonic p q : q \is monic → lead_coef (p × q) = lead_coef p.
Lemma size_monicM p q :
p \is monic → q != 0 → size (p × q) = (size p + size q).-1.
Lemma size_Mmonic p q :
p != 0 → q \is monic → size (p × q) = (size p + size q).-1.
Lemma monicMl p q : p \is monic → (p × q \is monic) = (q \is monic).
Lemma monicMr p q : q \is monic → (p × q \is monic) = (p \is monic).
Fact monic_mulr_closed : mulr_closed monic.
Lemma monic_exp p n : p \is monic → p ^+ n \is monic.
Lemma monic_prod I rI (P : pred I) (F : I → {poly R}):
(∀ i, P i → F i \is monic) → \prod_(i <- rI | P i) F i \is monic.
Lemma monicXsubC c : 'X - c%:P \is monic.
Lemma monic_prod_XsubC I rI (P : pred I) (F : I → R) :
\prod_(i <- rI | P i) ('X - (F i)%:P) \is monic.
Lemma size_prod_XsubC I rI (F : I → R) :
size (\prod_(i <- rI) ('X - (F i)%:P)) = (size rI).+1.
Lemma size_exp_XsubC n a : size (('X - a%:P) ^+ n) = n.+1.
Arguments monic_pred _ /.
Definition monic := [qualify p | monic_pred p].
Lemma monicE p : (p \is monic) = (lead_coef p == 1).
Lemma monicP p : reflect (lead_coef p = 1) (p \is monic).
Lemma monic1 : 1 \is monic.
Lemma monicX : 'X \is monic.
Lemma monicXn n : 'X^n \is monic.
Lemma monic_neq0 p : p \is monic → p != 0.
Lemma lead_coef_monicM p q : p \is monic → lead_coef (p × q) = lead_coef q.
Lemma lead_coef_Mmonic p q : q \is monic → lead_coef (p × q) = lead_coef p.
Lemma size_monicM p q :
p \is monic → q != 0 → size (p × q) = (size p + size q).-1.
Lemma size_Mmonic p q :
p != 0 → q \is monic → size (p × q) = (size p + size q).-1.
Lemma monicMl p q : p \is monic → (p × q \is monic) = (q \is monic).
Lemma monicMr p q : q \is monic → (p × q \is monic) = (p \is monic).
Fact monic_mulr_closed : mulr_closed monic.
Lemma monic_exp p n : p \is monic → p ^+ n \is monic.
Lemma monic_prod I rI (P : pred I) (F : I → {poly R}):
(∀ i, P i → F i \is monic) → \prod_(i <- rI | P i) F i \is monic.
Lemma monicXsubC c : 'X - c%:P \is monic.
Lemma monic_prod_XsubC I rI (P : pred I) (F : I → R) :
\prod_(i <- rI | P i) ('X - (F i)%:P) \is monic.
Lemma size_prod_XsubC I rI (F : I → R) :
size (\prod_(i <- rI) ('X - (F i)%:P)) = (size rI).+1.
Lemma size_exp_XsubC n a : size (('X - a%:P) ^+ n) = n.+1.
Some facts about regular elements.
Lemma lreg_lead p : GRing.lreg (lead_coef p) → GRing.lreg p.
Lemma rreg_lead p : GRing.rreg (lead_coef p) → GRing.rreg p.
Lemma lreg_lead0 p : GRing.lreg (lead_coef p) → p != 0.
Lemma rreg_lead0 p : GRing.rreg (lead_coef p) → p != 0.
Lemma lreg_size c p : GRing.lreg c → size (c *: p) = size p.
Lemma lreg_polyZ_eq0 c p : GRing.lreg c → (c *: p == 0) = (p == 0).
Lemma lead_coef_lreg c p :
GRing.lreg c → lead_coef (c *: p) = c × lead_coef p.
Lemma rreg_size c p : GRing.rreg c → size (p × c%:P) = size p.
Lemma rreg_polyMC_eq0 c p : GRing.rreg c → (p × c%:P == 0) = (p == 0).
Lemma rreg_div0 q r d :
GRing.rreg (lead_coef d) → size r < size d →
(q × d + r == 0) = (q == 0) && (r == 0).
Lemma monic_comreg p :
p \is monic → GRing.comm p (lead_coef p)%:P ∧ GRing.rreg (lead_coef p).
Lemma monic_lreg p : p \is monic → GRing.lreg p.
Lemma monic_rreg p : p \is monic → GRing.rreg p.
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 x ⇒ hornerM_comm p (comm_polyX x))).
Definition root p : pred R := fun x ⇒ p.[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}.
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 x ⇒ hornerM_comm p (comm_polyX x))).
Definition root p : pred R := fun x ⇒ p.[x] == 0.
Lemma mem_root p x : x \in root p = (p.[x] == 0).
Lemma rootE p x : (root p x = (p.[x] == 0)) × ((x \in root p) = (p.[x] == 0)).
Lemma rootP p x : reflect (p.[x] = 0) (root p x).
Lemma rootPt p x : reflect (p.[x] == 0) (root p x).
Lemma rootPf p x : reflect ((p.[x] == 0) = false) (~~ root p x).
Lemma rootC a x : root a%:P x = (a == 0).
Lemma root0 x : root 0 x.
Lemma root1 x : ~~ root 1 x.
Lemma rootX x : root 'X x = (x == 0).
Lemma rootN p x : root (- p) x = root p x.
Lemma root_size_gt1 a p : p != 0 → root p a → 1 < size p.
Lemma root_XsubC a x : root ('X - a%:P) x = (x == a).
Lemma root_XaddC a x : root ('X + a%:P) x = (x == - a).
Theorem factor_theorem p a : reflect (∃ q, p = q × ('X - a%:P)) (root p a).
Lemma multiplicity_XsubC p a :
{m | exists2 q, (p != 0) ==> ~~ root q a & p = q × ('X - a%:P) ^+ m}.
Roots of unity.
Lemma size_Xn_sub_1 n : n > 0 → size ('X^n - 1 : {poly R}) = n.+1.
Lemma monic_Xn_sub_1 n : n > 0 → 'X^n - 1 \is monic.
Definition root_of_unity n : pred R := root ('X^n - 1).
Lemma unity_rootE n z : n.-unity_root z = (z ^+ n == 1).
Lemma unity_rootP n z : reflect (z ^+ n = 1) (n.-unity_root z).
Definition primitive_root_of_unity n z :=
(n > 0) && [∀ i : 'I_n, i.+1.-unity_root z == (i.+1 == n)].
Lemma prim_order_exists n z :
n > 0 → z ^+ n = 1 → {m | m.-primitive_root z & (m %| n)}.
Section OnePrimitive.
Variables (n : nat) (z : R).
Hypothesis prim_z : n.-primitive_root z.
Lemma prim_order_gt0 : n > 0.
Let n_gt0 := prim_order_gt0.
Lemma prim_expr_order : z ^+ n = 1.
Lemma prim_expr_mod i : z ^+ (i %% n) = z ^+ i.
Lemma prim_order_dvd i : (n %| i) = (z ^+ i == 1).
Lemma eq_prim_root_expr i j : (z ^+ i == z ^+ j) = (i == j %[mod n]).
Lemma exp_prim_root k : (n %/ gcdn k n).-primitive_root (z ^+ k).
Lemma dvdn_prim_root m : (m %| n)%N → m.-primitive_root (z ^+ (n %/ m)).
End OnePrimitive.
Lemma prim_root_exp_coprime n z k :
n.-primitive_root z → n.-primitive_root (z ^+ k) = coprime k n.
Lifting a ring predicate to polynomials.
Implicit Type S : {pred R}.
Definition polyOver_pred S := fun p : {poly R} ⇒ all (mem S) p.
Arguments polyOver_pred _ _ /.
Definition polyOver S := [qualify a p | polyOver_pred S p].
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.
Variable S : addrClosed R.
Lemma polyOverP {p} : reflect (∀ i, p`_i \in S) (p \in polyOver S).
Lemma polyOverC c : (c%:P \in polyOver S) = (c \in S).
Fact polyOver_addr_closed : addr_closed (polyOver S).
End PolyOverAdd.
Fact polyOverNr (zmodS : zmodClosed R) : oppr_closed (polyOver zmodS).
Section PolyOverSemiring.
Variable S : semiringClosed R.
Fact polyOver_mulr_closed : mulr_closed (polyOver S).
Lemma polyOverZ : {in S & polyOver S, ∀ c p, c *: p \is a polyOver S}.
Lemma polyOverX : 'X \in polyOver S.
Lemma rpred_horner : {in polyOver S & S, ∀ p x, p.[x] \in S}.
End PolyOverSemiring.
Section PolyOverRing.
Variable S : subringClosed R.
Lemma polyOverXsubC c : ('X - c%:P \in polyOver S) = (c \in S).
End PolyOverRing.
Single derivative.
Definition deriv p := \poly_(i < (size p).-1) (p`_i.+1 *+ i.+1).
Lemma coef_deriv p i : p^`()`_i = p`_i.+1 *+ i.+1.
Lemma polyOver_deriv (ringS : semiringClosed R) :
{in polyOver ringS, ∀ p, p^`() \is a polyOver ringS}.
Lemma derivC c : c%:P^`() = 0.
Lemma derivX : ('X)^`() = 1.
Lemma derivXn n : 'X^n^`() = 'X^n.-1 *+ n.
Fact deriv_is_linear : linear deriv.
Lemma deriv0 : 0^`() = 0.
Lemma derivD : {morph deriv : p q / p + q}.
Lemma derivN : {morph deriv : p / - p}.
Lemma derivB : {morph deriv : p q / p - q}.
Lemma derivXsubC (a : R) : ('X - a%:P)^`() = 1.
Lemma derivMn n p : (p *+ n)^`() = p^`() *+ n.
Lemma derivMNn n p : (p *- n)^`() = p^`() *- n.
Lemma derivZ c p : (c *: p)^`() = c *: p^`().
Lemma deriv_mulC c p : (c%:P × p)^`() = c%:P × p^`().
Lemma derivMXaddC p c : (p × 'X + c%:P)^`() = p + p^`() × 'X.
Lemma derivM p q : (p × q)^`() = p^`() × q + p × q^`().
Definition derivE := Eval lazy beta delta [morphism_2 morphism_1] in
(derivZ, deriv_mulC, derivC, derivX, derivMXaddC, derivXsubC, derivM, derivB,
derivD, derivN, derivXn, derivM, derivMn).
Iterated derivative.
Definition derivn n p := iter n deriv p.
Lemma derivn0 p : p^`(0) = p.
Lemma derivn1 p : p^`(1) = p^`().
Lemma derivnS p n : p^`(n.+1) = p^`(n)^`().
Lemma derivSn p n : p^`(n.+1) = p^`()^`(n).
Lemma coef_derivn n p i : p^`(n)`_i = p`_(n + i) *+ (n + i) ^_ n.
Lemma polyOver_derivn (ringS : semiringClosed R) :
{in polyOver ringS, ∀ p n, p^`(n) \is a polyOver ringS}.
Fact derivn_is_linear n : linear (derivn n).
Lemma derivnC c n : c%:P^`(n) = if n == 0%N then c%:P else 0.
Lemma derivnD n : {morph derivn n : p q / p + q}.
Lemma derivnB n : {morph derivn n : p q / p - q}.
Lemma derivnMn n m p : (p *+ m)^`(n) = p^`(n) *+ m.
Lemma derivnMNn n m p : (p *- m)^`(n) = p^`(n) *- m.
Lemma derivnN n : {morph derivn n : p / - p}.
Lemma derivnZ n : scalable (derivn n).
Lemma derivnXn m n : 'X^m^`(n) = 'X^(m - n) *+ m ^_ n.
Lemma derivnMXaddC n p c :
(p × 'X + c%:P)^`(n.+1) = p^`(n) *+ n.+1 + p^`(n.+1) × 'X.
Lemma derivn_poly0 p n : size p ≤ n → p^`(n) = 0.
Lemma lt_size_deriv (p : {poly R}) : p != 0 → size p^`() < size p.
Lemma derivn0 p : p^`(0) = p.
Lemma derivn1 p : p^`(1) = p^`().
Lemma derivnS p n : p^`(n.+1) = p^`(n)^`().
Lemma derivSn p n : p^`(n.+1) = p^`()^`(n).
Lemma coef_derivn n p i : p^`(n)`_i = p`_(n + i) *+ (n + i) ^_ n.
Lemma polyOver_derivn (ringS : semiringClosed R) :
{in polyOver ringS, ∀ p n, p^`(n) \is a polyOver ringS}.
Fact derivn_is_linear n : linear (derivn n).
Lemma derivnC c n : c%:P^`(n) = if n == 0%N then c%:P else 0.
Lemma derivnD n : {morph derivn n : p q / p + q}.
Lemma derivnB n : {morph derivn n : p q / p - q}.
Lemma derivnMn n m p : (p *+ m)^`(n) = p^`(n) *+ m.
Lemma derivnMNn n m p : (p *- m)^`(n) = p^`(n) *- m.
Lemma derivnN n : {morph derivn n : p / - p}.
Lemma derivnZ n : scalable (derivn n).
Lemma derivnXn m n : 'X^m^`(n) = 'X^(m - n) *+ m ^_ n.
Lemma derivnMXaddC n p c :
(p × 'X + c%:P)^`(n.+1) = p^`(n) *+ n.+1 + p^`(n.+1) × 'X.
Lemma derivn_poly0 p n : size p ≤ n → p^`(n) = 0.
Lemma lt_size_deriv (p : {poly R}) : p != 0 → size p^`() < size p.
A normalising version of derivation to get the division by n! in Taylor
Definition nderivn n p := \poly_(i < size p - n) (p`_(n + i) *+ 'C(n + i, n)).
Lemma coef_nderivn n p i : p^`N(n)`_i = p`_(n + i) *+ 'C(n + i, n).
Here is the division by n!
Lemma nderivn_def n p : p^`(n) = p^`N(n) *+ n`!.
Lemma polyOver_nderivn (ringS : semiringClosed R) :
{in polyOver ringS, ∀ p n, p^`N(n) \in polyOver ringS}.
Lemma nderivn0 p : p^`N(0) = p.
Lemma nderivn1 p : p^`N(1) = p^`().
Lemma nderivnC c n : (c%:P)^`N(n) = if n == 0%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 i ⇒ E)) : 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.
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 i ⇒ E)) : 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.
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.
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}.
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
Definition even_poly p : {poly R} := \poly_(i < uphalf (size p)) p`_i.*2.
Lemma size_even_poly p : size (even_poly p) ≤ uphalf (size p).
Lemma coef_even_poly p i : (even_poly p)`_i = p`_i.*2.
Lemma even_polyE s p : size p ≤ s.*2 → even_poly p = \poly_(i < s) p`_i.*2.
Lemma size_even_poly_eq p : odd (size p) →
size (even_poly p) = uphalf (size p).
Lemma even_polyD p q : even_poly (p + q) = even_poly p + even_poly q.
Lemma even_polyZ k p : even_poly (k *: p) = k *: even_poly p.
Fact even_poly_is_linear : linear even_poly.
Lemma even_polyC (c : R) : even_poly c%:P = c%:P.
Odd part of a polynomial
Definition odd_poly p : {poly R} := \poly_(i < (size p)./2) p`_i.*2.+1.
Lemma size_odd_poly p : size (odd_poly p) ≤ (size p)./2.
Lemma coef_odd_poly p i : (odd_poly p)`_i = p`_i.*2.+1.
Lemma odd_polyE s p :
size p ≤ s.*2.+1 → odd_poly p = \poly_(i < s) p`_i.*2.+1.
Lemma odd_polyC (c : R) : odd_poly c%:P = 0.
Lemma odd_polyD p q : odd_poly (p + q) = odd_poly p + odd_poly q.
Lemma odd_polyZ k p : odd_poly (k *: p) = k *: odd_poly p.
Fact odd_poly_is_linear : linear odd_poly.
Lemma size_odd_poly_eq p : ~~ odd (size p) → size (odd_poly p) = (size p)./2.
Lemma odd_polyMX p : odd_poly (p × 'X) = even_poly p.
Lemma even_polyMX p : even_poly (p × 'X) = odd_poly p × 'X.
Lemma sum_even_poly p :
\sum_(i < size p | ~~ odd i) p`_i *: 'X^i = even_poly p \Po 'X^2.
Lemma sum_odd_poly p :
\sum_(i < size p | odd i) p`_i *: 'X^i = (odd_poly p \Po 'X^2) × 'X.
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.
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