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

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