Library polydvd
This file is part of CoqEAL, the Coq Effective Algebra Library.
(c) Copyright INRIA and University of Gothenburg.
Require Import ssreflect ssrfun ssrbool eqtype ssrnat div seq.
Require Import path choice fintype tuple finset ssralg.
Require Import matrix poly.
Require Import bigop polydiv dvdring.
Import GRing.Theory.
Import Pdiv.Ring Pdiv.Idomain Pdiv.RingComRreg dvdring.Notations.
Set Implicit Arguments.
Require Import path choice fintype tuple finset ssralg.
Require Import matrix poly.
Require Import bigop polydiv dvdring.
Import GRing.Theory.
Import Pdiv.Ring Pdiv.Idomain Pdiv.RingComRreg dvdring.Notations.
Set Implicit Arguments.
Local fix for poly notations
Delimit Scope poly_scope with P.
Notation "m %/ d" := (rdivp m d) : poly_scope.
Notation "m %% d" := (rmodp m d) : poly_scope.
Notation "p %| q" := (rdvdp p q) : poly_scope.
Notation "p %= q" := (eqp p q) : poly_scope.
Local Open Scope ring_scope.
Module PolyDvdRing.
Section PolyDvdRing.
Variable R : dvdRingType.
Implicit Types p q : {poly R}.
Notation "m %/ d" := (rdivp m d) : poly_scope.
Notation "m %% d" := (rmodp m d) : poly_scope.
Notation "p %| q" := (rdvdp p q) : poly_scope.
Notation "p %= q" := (eqp p q) : poly_scope.
Local Open Scope ring_scope.
Module PolyDvdRing.
Section PolyDvdRing.
Variable R : dvdRingType.
Implicit Types p q : {poly R}.
Long division of polynomials
Definition odivp_rec q :=
let sq := size q in
let lq := lead_coef q in
fix loop (n : nat) (r p : {poly R}) {struct n} :=
if p == 0 then Some r else
if size p < sq then None else
match odivr (lead_coef p) lq with
| Some x => let m := x%:P * 'X^(size p - sq) in
let r1 := r + m in
let p1 := p - m * q in
if n is n1.+1 then loop n1 r1 p1 else None
| None => None
end.
Definition odivp p q : option {poly R} :=
if p == 0 then Some 0 else odivp_rec q (size p) 0 p.
Lemma odivp_recP : forall q n p r, size p <= n ->
DvdRing.div_spec p q (omap (fun x => x - r) (odivp_rec q n r p)).
Lemma odivpP : forall p q, DvdRing.div_spec p q (odivp p q).
Definition polyDvdRingMixin := DvdRingMixin odivpP.
Canonical Structure polyDvdRingType := DvdRingType {poly R} polyDvdRingMixin.
End PolyDvdRing.
End PolyDvdRing.
Module PolyGcdRing.
Section PolyGcdRing.
let sq := size q in
let lq := lead_coef q in
fix loop (n : nat) (r p : {poly R}) {struct n} :=
if p == 0 then Some r else
if size p < sq then None else
match odivr (lead_coef p) lq with
| Some x => let m := x%:P * 'X^(size p - sq) in
let r1 := r + m in
let p1 := p - m * q in
if n is n1.+1 then loop n1 r1 p1 else None
| None => None
end.
Definition odivp p q : option {poly R} :=
if p == 0 then Some 0 else odivp_rec q (size p) 0 p.
Lemma odivp_recP : forall q n p r, size p <= n ->
DvdRing.div_spec p q (omap (fun x => x - r) (odivp_rec q n r p)).
Lemma odivpP : forall p q, DvdRing.div_spec p q (odivp p q).
Definition polyDvdRingMixin := DvdRingMixin odivpP.
Canonical Structure polyDvdRingType := DvdRingType {poly R} polyDvdRingMixin.
End PolyDvdRing.
End PolyDvdRing.
Module PolyGcdRing.
Section PolyGcdRing.
Polyonomials over gcd rings
Import PolyDvdRing.
Variable R : gcdRingType.
Implicit Types a b : R.
Implicit Types p q : {poly R}.
Double induction for polynomials
Lemma poly_ind2 : forall P : {poly R} -> {poly R} -> Type,
(forall p, P p 0) ->
(forall q, P 0 q) ->
(forall c p d q, P p (q * 'X + d%:P) ->
P (p * 'X + c%:P) q ->
P (p * 'X + c%:P) (q * 'X + d%:P)) ->
(forall p q, P p q).
Lemma elim_poly : forall p, exists p', exists c, p = p' * 'X + c%:P.
Lemma polyC_inj_dvdr : forall a b, (a %| b)%R -> a%:P %| b %:P.
Lemma polyC_inj_eqd : forall a b, a %= b -> a%:P %= b%:P.
(forall p, P p 0) ->
(forall q, P 0 q) ->
(forall c p d q, P p (q * 'X + d%:P) ->
P (p * 'X + c%:P) q ->
P (p * 'X + c%:P) (q * 'X + d%:P)) ->
(forall p q, P p q).
Lemma elim_poly : forall p, exists p', exists c, p = p' * 'X + c%:P.
Lemma polyC_inj_dvdr : forall a b, (a %| b)%R -> a%:P %| b %:P.
Lemma polyC_inj_eqd : forall a b, a %= b -> a%:P %= b%:P.
Properties of gcdsr
Lemma gcdsr0 : gcdsr (0 : {poly R}) = 0.
Lemma gcdsr1 : gcdsr (1 : {poly R}) %= 1.
Lemma gcdsrC : forall c : R, gcdsr c%:P %= c.
Lemma gcdsr_gcdl : forall p c, gcdsr (p * 'X + c%:P) = gcdr c (gcdsr p).
Lemma gcdsr_eq0 : forall p, (gcdsr p == 0) = (p == 0).
Lemma gcdsr_mulX : forall p, gcdsr (p * 'X) %= gcdsr p.
Lemma gcdsrX : gcdsr ('X : {poly R}) %= 1.
Lemma gcdsr_mull : forall a p, gcdsr (a%:P * p) %= a * gcdsr p.
Lemma gcdsr_mulr : forall a p, gcdsr (p * a%:P) %= gcdsr p * a.
Lemma mulr_gcdsr : forall a p, a * gcdsr p %= gcdsr (a%:P * p).
Lemma mulr_gcdsl : forall a p, gcdsr p * a %= gcdsr (p * a %:P).
Lemma eq_eqdgcdsr : forall p q, p = q -> gcdsr p %= gcdsr q.
Key lemma in gauss lemma
Primitive polynomials
Another key lemma
Lemma gcdsr_primitive : forall p, exists q, p = (gcdsr p)%:P * q /\ primitive q.
Lemma gcdsr_dvdr : forall p, (gcdsr p)%:P %| p.
Lemma gcdsr_odivp :
forall p, p != 0 ->
exists x, p %/? (gcdsr p)%:P = Some (x : {poly R}) /\ primitive x.
Lemma prim_mulX : forall p, primitive p -> primitive (p * 'X).
Lemma gauss_lemma : forall p q, gcdsr (p * q) %= gcdsr p * gcdsr q.
Lemma gauss_primitive :
forall p q, primitive p -> primitive q -> primitive (p * q).
Lemma gcdsr_inj_dvdr : forall p q, p %| q -> gcdsr p %| gcdsr q.
Lemma gcdsr_inj_eqd : forall p q, p %= q -> gcdsr p %= gcdsr q.
Lemma gcdsr_dvdr : forall p, (gcdsr p)%:P %| p.
Lemma gcdsr_odivp :
forall p, p != 0 ->
exists x, p %/? (gcdsr p)%:P = Some (x : {poly R}) /\ primitive x.
Lemma prim_mulX : forall p, primitive p -> primitive (p * 'X).
Lemma gauss_lemma : forall p q, gcdsr (p * q) %= gcdsr p * gcdsr q.
Lemma gauss_primitive :
forall p q, primitive p -> primitive q -> primitive (p * q).
Lemma gcdsr_inj_dvdr : forall p q, p %| q -> gcdsr p %| gcdsr q.
Lemma gcdsr_inj_eqd : forall p q, p %= q -> gcdsr p %= gcdsr q.
Primitive part, pp
Definition pp p := match p %/? (gcdsr p)%:P with
| Some x => x
| None => 1
end.
Lemma pp0 : pp 0 = 0.
Lemma ppP : forall p, p = (gcdsr p)%:P * pp p.
Lemma pp_eq0 : forall p, (pp p == 0) = (p == 0).
Lemma ppC : forall c, c != 0 -> pp c%:P %= 1.
Lemma pp1 : pp 1 %= 1.
Lemma ppX : pp 'X %= 'X.
Lemma prim_pp : forall p, p != 0 -> primitive (pp p).
Lemma pp_prim : forall p, primitive p -> (p %= pp p).
Lemma pp_dvdr : forall p, pp p %| p.
Lemma pp_mul : forall p q, pp (p * q) %= pp p * pp q.
Lemma pp_mull : forall a p, a != 0 -> pp (a%:P * p) %= pp p.
Lemma pp_mulX : forall p, pp (p * 'X) %= pp p * 'X.
Lemma pp_inj_dvdr : forall p q, p %| q -> pp p %| pp q.
Lemma pp_inj_eqd : forall p q, p %= q -> pp p %= pp q.
Lemma size_pp : forall p, size p = size (pp p).
Lemma dvdrp_spec :
forall p q, (p %| q) = (gcdsr p %| gcdsr q) && (pp p %| pp q).
Lemma pp_prim_eq : forall p, p != 0 -> primitive p = (p %= pp p).
Lemma dvdrp_prim_mull : forall a p q,
a != 0 -> primitive q -> p %| a%:P * q = (gcdsr p %| a) && (pp p %| q).
Lemma dvdrpC : forall a p, a%:P %| p = (a %| gcdsr p).
Lemma dvdrp_primr : forall p q, p %| q -> primitive q -> primitive p.
Lemma dvdrp_priml :
forall a p q, a != 0 -> p %| a%:P * q -> primitive p -> p %| q.
gcdp
Fixpoint gcdp_rec (n : nat) (p q : {poly R}) :=
let r := rmodp p q in
if r == 0 then q
else if n is n'.+1 then gcdp_rec n' q (pp r) else pp r.
Definition gcdp p q :=
let (p1,q1) := if size p < size q then (q,p) else (p,q) in
let d := (gcdr (gcdsr p1) (gcdsr q1))%:P in
d * gcdp_rec (size (pp p1)) (pp p1) (pp q1).
Lemma gcdp_rec0r : forall p n, gcdp_rec n 0 p = p.
Lemma gcdp_recr0 : forall p n, primitive p -> gcdp_rec n p 0 %= p.
let r := rmodp p q in
if r == 0 then q
else if n is n'.+1 then gcdp_rec n' q (pp r) else pp r.
Definition gcdp p q :=
let (p1,q1) := if size p < size q then (q,p) else (p,q) in
let d := (gcdr (gcdsr p1) (gcdsr q1))%:P in
d * gcdp_rec (size (pp p1)) (pp p1) (pp q1).
Lemma gcdp_rec0r : forall p n, gcdp_rec n 0 p = p.
Lemma gcdp_recr0 : forall p n, primitive p -> gcdp_rec n p 0 %= p.
Show that gcdp_rec return a primitive polynomial
that is the gcd of p and q
Lemma gcdp_recP : forall n p q g,
size q <= n -> q != 0 -> primitive q ->
(g %| gcdp_rec n p q = (g %| p) && (g %| q)) /\ primitive (gcdp_rec n p q).
size q <= n -> q != 0 -> primitive q ->
(g %| gcdp_rec n p q = (g %| p) && (g %| q)) /\ primitive (gcdp_rec n p q).
Correctness of gcdp
Lemma gcdpP : forall p q g, g %| gcdp p q = (g %| p) && (g %| q).
Definition polyGcdRingMixin := GcdRingMixin gcdpP.
Canonical Structure polyGcdRingType := GcdRingType {poly R} polyGcdRingMixin.
End PolyGcdRing.
End PolyGcdRing.
Module PolyPriField.
Section PolyPriField.
Definition polyGcdRingMixin := GcdRingMixin gcdpP.
Canonical Structure polyGcdRingType := GcdRingType {poly R} polyGcdRingMixin.
End PolyGcdRing.
End PolyGcdRing.
Module PolyPriField.
Section PolyPriField.
This section shows that the polynomial ring k[x]
where k is a field is an Euclidean ring
Variable F : fieldType.
Implicit Types p q r : {poly F}.
Definition ediv_rec q :=
let sq := size q in
let lq := lead_coef q in
fix loop (n : nat) (qq r : {poly F}) {struct n} :=
if size r < sq then (qq, r) else
let m := (lead_coef r / lq)%:P * 'X^(size r - sq) in
let qq1 := qq + m in
let r1 := r - m * q in
if n is n1.+1 then loop n1 qq1 r1 else (qq1, r1).
Definition ediv p q : {poly F} * {poly F} :=
if q == 0 then (0, p) else ediv_rec q (size p) 0 p.
Lemma ediv_recP : forall q n p qq, q != 0 -> size p <= n ->
let: (qq', r) := (ediv_rec q n qq p) in
EuclideanRing.edivr_spec (size : {poly F} -> nat) p q (qq' - qq, r).
Lemma edivP : forall p q,
EuclideanRing.edivr_spec (size : {poly F} -> nat) p q (ediv p q).
Lemma poly_size_mull :
forall p q, p != (0 : {poly F}) -> (size q <= size (p * q)%R)%N.
Definition poly_euclidMixin := EuclideanRing.Mixin poly_size_mull edivP.
Definition poly_dvdMixin := EuclidDvdMixin {poly F} poly_euclidMixin.
Canonical Structure poly_dvdRingType := DvdRingType {poly F} poly_dvdMixin.
Definition poly_gcdMixin := EuclidGcdMixin {poly F} poly_euclidMixin.
Canonical Structure poly_gcdType := GcdRingType {poly F} poly_gcdMixin.
Definition poly_bezoutMixin := EuclidBezoutMixin {poly F} poly_euclidMixin.
Canonical Structure poly_bezoutType := BezoutRingType {poly F} poly_bezoutMixin.
Definition poly_priMixin := EuclidPriMixin {poly F} poly_euclidMixin.
Canonical Structure poly_priType := PriRingType {poly F} poly_priMixin.
Canonical Structure poly_euclidType := EuclidRingType {poly F} poly_euclidMixin.
End PolyPriField.
Section PolyPriFieldTheory.
Variable F : fieldType.
Lemma dvdr_dvdp (p q : {poly F}) : (dvdr p q) = (dvdp p q).
End PolyPriFieldTheory.
End PolyPriField.
This page has been generated by coqdoc