Library polydiv
Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype.
Require Import bigops ssralg poly.
Import GRing.
Import Prenex Implicits.
Open Scope ring_scope.
Section ExtraArith.
Lemma leqn1 : (forall n, n <= 1 = ((n==0) || (n==1)))%N.
Lemma leqn2 : (forall n, n <= 2 = [|| n == 0, n == 1 | n == 2])%N.
Lemma addn_pred1 : (forall n m, n != 0 -> (n == (m + n).-1) = (m == 1))%N.
End ExtraArith.
Section ExtraPolynomialIdomain.
Variable R : idomainType.
Implicit Types x y c : R.
Implicit Types p q r d : {poly R}.
Lemma size1_is_polyC : forall p,
reflect (exists c, c != 0 /\ p = c%:P) (size p == 1%N).
Lemma size1_dvdp1 : forall p, (size p == 1%N) = (p %= 1).
Lemma neqp01 : 0 %= (1 : {poly R}) = false.
Lemma dvd0p : forall p, 0 %| p = (p == 0).
Lemma dvdp_eqp1 : forall p q, p %| q -> q %= 1 -> p %= 1.
Lemma dvdpn0 : forall p q, p %| q -> q != 0 -> p != 0.
Lemma dvdp_mulIl : forall p q, p %| p * q.
Lemma dvdp_mulIr : forall p q, q %| p * q.
Lemma eqp_polyC: forall c, (c != 0) = (c%:P %= 1).
Lemma gcd1p : forall p, gcdp 1 p %= 1.
Lemma modp_dvd : forall p q, (q %| p) -> p %% q = 0.
Lemma modp_dvd_eq0 : forall p q, (q %| p) = (p %% q == 0).
Lemma eqp_dvdr : forall q p d, p %= q -> d %| p = (d %| q).
Lemma eqp_dvdl : forall d' d p, d %= d' -> d %| p = (d' %| p).
Lemma eqp1_dvd : forall d p, d %= 1 -> d %| p.
Lemma eqp1_dvd1 : forall d, (d %= 1) = (d %| 1).
Lemma eqp_mulC : forall p q c, c != 0 -> c%:P * p %= p.
Lemma dvdp_size_eqp : forall p q, p %| q -> size p == size q = (p %= q).
Lemma size_divp : forall p q, q != 0 -> size q <= size p
-> size (p %/ q) = ((size p) - (size q).-1)%N.
Lemma eqp_transl : left_transitive (@eqp R).
Lemma eqp_transr : right_transitive (@eqp R).
Lemma gcdp_eq0 : forall p q, gcdp p q == 0 = (p == 0) && (q == 0).
Definition coprimep p q := size (gcdp p q) == 1%N.
Lemma size_gcdp1 : forall p q, size (gcdp p q) == 1%N = (coprimep p q).
Lemma gcdp_eqp1 : forall p q, gcdp p q %= 1 = (coprimep p q).
Lemma coprimep_sym : forall p q, coprimep p q = coprimep q p.
Lemma coprime1p: forall p, coprimep 1 p.
Lemma coprimep1 : forall p, coprimep p 1.
Lemma coprimep0 : forall p, coprimep p 0 = (p %= 1).
Lemma coprime0p : forall p, coprimep 0 p = (p %= 1).
Lemma coprimepP : forall p q,
reflect (forall d, d %| p -> d %| q -> d %= 1) (coprimep p q).
Lemma coprimepPn : forall p q, p != 0 ->
reflect (exists d, (d %| gcdp p q) && ~~(d %= 1)) (~~ coprimep p q).
Lemma coprimep_dvdl : forall p q r,
r %| q -> coprimep p q -> coprimep p r.
Lemma modp_mod : forall p q, (p %% q) %% q = p %% q.
Fixpoint egcdp_rec p q n {struct n} :=
if n is n'.+1 then
if q == 0 then (1, 0) else
let: (u, v) := egcdp_rec q (p%%q) n' in
((v * (scalp p q)%:P), (u - v * (p %/ q)))
else (1, 0).
Definition egcdp p q := egcdp_rec p q (size q).
Lemma egcdp_recP : forall n p q, size q <= n -> size q <= size p
-> let e := (egcdp_rec p q n) in gcdp p q %= e.1*p + e.2*q.
Lemma egcdpPS : forall p q, size q <= size p
-> let e := egcdp p q in gcdp p q %= e.1*p + e.2*q.
Lemma egcdpPW : forall p q, exists u, exists v, (u*p + v*q) %= (gcdp p q).
Lemma coprimepPW : forall p q,
reflect (exists u, exists v, (u*p + v*q) %= 1) (coprimep p q).
Lemma eqp_mull : forall p q r, (q %= r) -> (p * q %= p * r).
Lemma gauss : forall p q d, coprimep d q -> d %| p = (d %| p * q).
Require Import bigops ssralg poly.
Import GRing.
Import Prenex Implicits.
Open Scope ring_scope.
Section ExtraArith.
Lemma leqn1 : (forall n, n <= 1 = ((n==0) || (n==1)))%N.
Lemma leqn2 : (forall n, n <= 2 = [|| n == 0, n == 1 | n == 2])%N.
Lemma addn_pred1 : (forall n m, n != 0 -> (n == (m + n).-1) = (m == 1))%N.
End ExtraArith.
Section ExtraPolynomialIdomain.
Variable R : idomainType.
Implicit Types x y c : R.
Implicit Types p q r d : {poly R}.
Lemma size1_is_polyC : forall p,
reflect (exists c, c != 0 /\ p = c%:P) (size p == 1%N).
Lemma size1_dvdp1 : forall p, (size p == 1%N) = (p %= 1).
Lemma neqp01 : 0 %= (1 : {poly R}) = false.
Lemma dvd0p : forall p, 0 %| p = (p == 0).
Lemma dvdp_eqp1 : forall p q, p %| q -> q %= 1 -> p %= 1.
Lemma dvdpn0 : forall p q, p %| q -> q != 0 -> p != 0.
Lemma dvdp_mulIl : forall p q, p %| p * q.
Lemma dvdp_mulIr : forall p q, q %| p * q.
Lemma eqp_polyC: forall c, (c != 0) = (c%:P %= 1).
Lemma gcd1p : forall p, gcdp 1 p %= 1.
Lemma modp_dvd : forall p q, (q %| p) -> p %% q = 0.
Lemma modp_dvd_eq0 : forall p q, (q %| p) = (p %% q == 0).
Lemma eqp_dvdr : forall q p d, p %= q -> d %| p = (d %| q).
Lemma eqp_dvdl : forall d' d p, d %= d' -> d %| p = (d' %| p).
Lemma eqp1_dvd : forall d p, d %= 1 -> d %| p.
Lemma eqp1_dvd1 : forall d, (d %= 1) = (d %| 1).
Lemma eqp_mulC : forall p q c, c != 0 -> c%:P * p %= p.
Lemma dvdp_size_eqp : forall p q, p %| q -> size p == size q = (p %= q).
Lemma size_divp : forall p q, q != 0 -> size q <= size p
-> size (p %/ q) = ((size p) - (size q).-1)%N.
Lemma eqp_transl : left_transitive (@eqp R).
Lemma eqp_transr : right_transitive (@eqp R).
Lemma gcdp_eq0 : forall p q, gcdp p q == 0 = (p == 0) && (q == 0).
Definition coprimep p q := size (gcdp p q) == 1%N.
Lemma size_gcdp1 : forall p q, size (gcdp p q) == 1%N = (coprimep p q).
Lemma gcdp_eqp1 : forall p q, gcdp p q %= 1 = (coprimep p q).
Lemma coprimep_sym : forall p q, coprimep p q = coprimep q p.
Lemma coprime1p: forall p, coprimep 1 p.
Lemma coprimep1 : forall p, coprimep p 1.
Lemma coprimep0 : forall p, coprimep p 0 = (p %= 1).
Lemma coprime0p : forall p, coprimep 0 p = (p %= 1).
Lemma coprimepP : forall p q,
reflect (forall d, d %| p -> d %| q -> d %= 1) (coprimep p q).
Lemma coprimepPn : forall p q, p != 0 ->
reflect (exists d, (d %| gcdp p q) && ~~(d %= 1)) (~~ coprimep p q).
Lemma coprimep_dvdl : forall p q r,
r %| q -> coprimep p q -> coprimep p r.
Lemma modp_mod : forall p q, (p %% q) %% q = p %% q.
Fixpoint egcdp_rec p q n {struct n} :=
if n is n'.+1 then
if q == 0 then (1, 0) else
let: (u, v) := egcdp_rec q (p%%q) n' in
((v * (scalp p q)%:P), (u - v * (p %/ q)))
else (1, 0).
Definition egcdp p q := egcdp_rec p q (size q).
Lemma egcdp_recP : forall n p q, size q <= n -> size q <= size p
-> let e := (egcdp_rec p q n) in gcdp p q %= e.1*p + e.2*q.
Lemma egcdpPS : forall p q, size q <= size p
-> let e := egcdp p q in gcdp p q %= e.1*p + e.2*q.
Lemma egcdpPW : forall p q, exists u, exists v, (u*p + v*q) %= (gcdp p q).
Lemma coprimepPW : forall p q,
reflect (exists u, exists v, (u*p + v*q) %= 1) (coprimep p q).
Lemma eqp_mull : forall p q r, (q %= r) -> (p * q %= p * r).
Lemma gauss : forall p q d, coprimep d q -> d %| p = (d %| p * q).
"gdcop Q P" is the Greatest Divisor of P which is coprime to Q if P null, we pose that gdcop returns 1 if Q null, 0 otherwise
Fixpoint gdcop_rec q p n :=
if n is m.+1 then
if coprimep p q then p
else gdcop_rec q (p %/ (gcdp p q)) m
else (q == 0)%:R.
Definition gdcop q p := gdcop_rec q p (size p).
CoInductive gdcop_spec q p : {poly R} -> Type :=
GdcopSpec r of (r %| p) & ((coprimep r q) || (p == 0))
& (forall d, d %| p -> coprimep d q -> d %| r)
: gdcop_spec q p r.
Lemma gdcop0 : forall q, gdcop q 0 = (q == 0)%:R.
Lemma eqPn0 : (forall n, (n.-1 == 0) = ((n==0) || (n==1)))%N.
Lemma divpp : forall p, p != 0 -> p %/ p = (scalp p p)%:P.
Lemma gdcop_recP : forall q p n,
size p <= n -> gdcop_spec q p (gdcop_rec q p n).
if n is m.+1 then
if coprimep p q then p
else gdcop_rec q (p %/ (gcdp p q)) m
else (q == 0)%:R.
Definition gdcop q p := gdcop_rec q p (size p).
CoInductive gdcop_spec q p : {poly R} -> Type :=
GdcopSpec r of (r %| p) & ((coprimep r q) || (p == 0))
& (forall d, d %| p -> coprimep d q -> d %| r)
: gdcop_spec q p r.
Lemma gdcop0 : forall q, gdcop q 0 = (q == 0)%:R.
Lemma eqPn0 : (forall n, (n.-1 == 0) = ((n==0) || (n==1)))%N.
Lemma divpp : forall p, p != 0 -> p %/ p = (scalp p p)%:P.
Lemma gdcop_recP : forall q p n,
size p <= n -> gdcop_spec q p (gdcop_rec q p n).
should we have a spec for dvdn ? => I also wondered
Lemma gdcopP : forall q p, gdcop_spec q p (gdcop q p).
Lemma dvdp_gdco : forall p q d,
p != 0 -> size d == 2%N ->
(d %| p) && ~~(d %| q) = (d %| (gdcop q p)).
Lemma root_gdco : forall p q, p != 0 ->
forall x, root p x && ~~(root q x) = root (gdcop q p) x.
Lemma root_mul : forall p q x, root (p * q) x = root p x || root q x.
Lemma eqp_root : forall p q, p %= q -> forall x, root p x = root q x.
Lemma root_gcd : forall p q x, root (gcdp p q) x = root p x && root q x.
Lemma root0 : forall x, root 0 x.
Lemma root1n : forall x, ~~root 1 x.
Lemma root_biggcd : forall x (ps : seq {poly R}),
root (\big[@gcdp _/0]_(p<-ps)p) x = all (fun p => root p x) ps.
Lemma root_bigmul : forall x (ps : seq {poly R}),
~~root (\big[@mul _/1]_(p<-ps)p) x = all (fun p => ~~ root p x) ps.
End ExtraPolynomialIdomain.
Section ExtraPolynomialFields.
Variable F : Field.type.
Variable axiom : ClosedField.axiom F.
Lemma root_size_neq1 : forall p : {poly F},
reflect (exists x, root p x) (size p != 1%N).
Lemma ex_px_neq0 : forall p : {poly F}, p != 0 -> exists x, p.[x] != 0.
End ExtraPolynomialFields.