backport ssralg and poly

Author: Tragicus

theories/xmathcomp/various.v

@@ -110,28 +110,35 @@ Qed.
 (* package algebra *)
 (*******************)
 
-Import GRing.Theory.
-Local Open Scope ring_scope.
-Notation has_char0 L := ([char L] =i pred0).
-
 (**********)
-(* ssralg *)
+(* ssrint *)
 (**********)
 
-Lemma iter_addr (V : zmodType) n x y : iter n (+%R x) y = x *+ n + y :> V.
-Proof. by elim: n => [|n ih]; rewrite ?add0r //= ih mulrS addrA. Qed.
-
-Lemma prodrMl {R : comRingType} {I : finType} (A : pred I) (x : R) F :
-  \prod_(i in A) (x * F i) = x ^+ #|A| * \prod_(i in A) F i.
+Lemma dvdz_charf (R : ringType) (p : nat) :
+  p \in [char R] -> forall n : int, (p %| n)%Z = (n%:~R == 0 :> R).
 Proof.
-rewrite -sum1_card; elim/big_rec3: _; first by rewrite expr0 mulr1.
-by move=> i y p z iA ->; rewrite mulrACA exprS.
+move=> charRp [] n; rewrite [LHS](dvdn_charf charRp)//.
+by rewrite NegzE abszN rmorphN// oppr_eq0.
 Qed.
 
-Lemma expr_sum {R : ringType} {T : Type} (x : R) (F : T -> nat) P s :
-  x ^+ (\sum_(i <- s | P i) F i) = \prod_(i <- s | P i) x ^+ (F i).
-Proof. by apply: big_morph; [exact: exprD | exact: expr0]. Qed.
+(********)
+(* poly *)
+(********)
+
+Local Notation "p ^^ f" := (map_poly f p)
+  (at level 30, f at level 30, format "p  ^^  f").
 
+#[deprecated(since="mathcomp 2.2.0",note="Use polyOverXsubC instead.")]
+Lemma poly_XsubC_over {R : ringType} c (S : {pred R}) (addS : subringPred S)
+  (kS : keyed_pred addS): c \in kS -> 'X - c%:P \is a polyOver kS.
+Proof. by move=> cS; rewrite rpredB ?polyOverC ?polyOverX. Qed.
+
+#[deprecated(since="mathcomp 2.2.0",note="Use polyOverXnsubC instead.")]
+Lemma poly_XnsubC_over {R : ringType} n c (S : {pred R}) (addS : subringPred S)
+  (kS : keyed_pred addS): c \in kS -> 'X^n - c%:P \is a polyOver kS.
+Proof. by move=> cS; rewrite rpredB ?rpredX ?polyOverX ?polyOverC. Qed.
+
+#[deprecated(since="mathcomp 2.2.0",note="Use prim_root_natf_eq0 instead.")]
 Lemma prim_root_natf_neq0 (F : fieldType) n (w : F) :
   n.-primitive_root w -> (n%:R != 0 :> F).
 Proof.
@@ -150,125 +157,85 @@ rewrite pfactor_dvdn// ltn_geF// -[k]muln1 logn_Gauss ?logn1//.
 by rewrite logn_gt0 mem_primes p_prime dvdpn n_gt0.
 Qed.
 
-(**********)
-(* ssrnum *)
-(**********)
-
-Section ssrnum.
-Import Num.Theory.
-
-Lemma CrealJ (C : numClosedFieldType) :
-  {mono (@conjC C) : x / x \is Num.real}.
+#[deprecated(since="mathcomp 2.2.0",note="Use prim_root_eq0 instead.")]
+Lemma primitive_root_eq0 (F : fieldType) n (w : F) :
+  n.-primitive_root w -> (w == 0) = (n == 0%N).
 Proof.
-suff realK : {homo (@conjC C) : x / x \is Num.real}.
-  by move=> x; apply/idP/idP => /realK//; rewrite conjCK.
-by move=> x xreal; rewrite conj_Creal.
+move=> wp; apply/eqP/idP => [w0|/eqP p0]; move: wp; rewrite ?w0 ?p0; last first.
+  by move=> /prim_order_gt0//.
+move=> /prim_expr_order/esym/eqP.
+by rewrite expr0n; case: (n =P 0%N); rewrite ?oner_eq0.
 Qed.
-End ssrnum.
 
 (**********)
-(* ssrint *)
+(* intdiv *)
 (**********)
 
-Lemma dvdz_charf (R : ringType) (p : nat) :
-  p \in [char R] -> forall n : int, (p %| n)%Z = (n%:~R == 0 :> R).
+Lemma eisenstein (p : nat) (q : {poly int}) : prime p -> (size q != 1)%N ->
+  (~~ (p %| lead_coef q))%Z -> (~~ ((p : int) ^+ 2 %| q`_0))%Z ->
+  (forall i, (i < (size q).-1)%N -> p %| q`_i)%Z ->
+  irreducible_poly (map_poly (intr : int -> rat) q).
 Proof.
-move=> charRp [] n; rewrite [LHS](dvdn_charf charRp)//.
-by rewrite NegzE abszN rmorphN// oppr_eq0.
+move=> p_prime qN1 Ndvd_pql Ndvd_pq0 dvd_pq.
+have qN0 : q != 0 by rewrite -lead_coef_eq0; apply: contraNneq Ndvd_pql => ->.
+split.
+   rewrite size_map_poly_id0 ?intr_eq0 ?lead_coef_eq0//.
+   by rewrite ltn_neqAle eq_sym qN1 size_poly_gt0.
+move=> f' +/dvdpP_rat_int[f [d dN0 feq]]; rewrite {f'}feq size_scale// => fN1.
+move=> /= [g q_eq]; rewrite q_eq (eqp_trans (eqp_scale _ _))//.
+have fN0 : f != 0 by apply: contra_neq qN0; rewrite q_eq => ->; rewrite mul0r.
+have gN0 : g != 0 by apply: contra_neq qN0; rewrite q_eq => ->; rewrite mulr0.
+rewrite size_map_poly_id0 ?intr_eq0 ?lead_coef_eq0// in fN1.
+have [/eqP/size_poly1P[c cN0 ->]|gN1] := eqVneq (size g) 1%N.
+  by rewrite mulrC mul_polyC map_polyZ/= eqp_sym eqp_scale// intr_eq0.
+have c_neq0 : (lead_coef q)%:~R != 0 :> 'F_p
+   by rewrite -(dvdz_charf (char_Fp _)).
+have : map_poly (intr : int -> 'F_p) q = (lead_coef q)%:~R *: 'X^(size q).-1.
+  apply/val_inj/(@eq_from_nth _ 0) => [|i]; rewrite size_map_poly_id0//.
+    by rewrite size_scale// size_polyXn -polySpred.
+  move=> i_small; rewrite coef_poly i_small coefZ coefXn lead_coefE.
+  move: i_small; rewrite polySpred// ltnS/=.
+  case: ltngtP => // [i_lt|->]; rewrite (mulr1, mulr0)//= => _.
+  by apply/eqP; rewrite -(dvdz_charf (char_Fp _))// dvd_pq.
+rewrite [in LHS]q_eq rmorphM/=.
+set c := (X in X *: _); set n := (_.-1).
+set pf := map_poly _ f; set pg := map_poly _ g => pfMpg.
+have dvdXn (r : {poly _}) : size r != 1%N -> r %| c *: 'X^n -> r`_0 = 0.
+  move=> rN1; rewrite (eqp_dvdr _ (eqp_scale _ _))//.
+  rewrite -['X]subr0; move=> /dvdp_exp_XsubC[k lekn]; rewrite subr0.
+  move=> /eqpP[u /andP[u1N0 u2N0]]; have [->|k_gt0] := posnP k.
+    move=> /(congr1 (size \o val))/eqP.
+    by rewrite /= !size_scale// size_polyXn (negPf rN1).
+  move=> /(congr1 (fun p : {poly _} => p`_0))/eqP.
+  by rewrite !coefZ coefXn ltn_eqF// mulr0 mulf_eq0 (negPf u1N0) => /eqP.
+suff : ((p : int) ^+ 2 %| q`_0)%Z by rewrite (negPf Ndvd_pq0).
+have := c_neq0; rewrite q_eq coefM big_ord1.
+rewrite lead_coefM rmorphM mulf_eq0 negb_or => /andP[lpfN0 qfN0].
+have pfN1 : size pf != 1%N by rewrite size_map_poly_id0.
+have pgN1 : size pg != 1%N by rewrite size_map_poly_id0.
+have /(dvdXn _ pgN1) /eqP : pg %| c *: 'X^n by rewrite -pfMpg dvdp_mull.
+have /(dvdXn _ pfN1) /eqP : pf %| c *: 'X^n by rewrite -pfMpg dvdp_mulr.
+by rewrite !coef_map// -!(dvdz_charf (char_Fp _))//; apply: dvdz_mul.
 Qed.
 
-(********)
-(* poly *)
-(********)
-
-Local Notation "p ^^ f" := (map_poly f p)
-  (at level 30, f at level 30, format "p  ^^  f").
-
+(***********)
+(* polydiv *)
+(***********)
 Lemma irredp_XaddC (F : fieldType) (x : F) : irreducible_poly ('X + x%:P).
 Proof. by rewrite -[x]opprK rmorphN; apply: irredp_XsubC. Qed.
 
-Lemma lead_coef_XnsubC {R : ringType} n (c : R) : (0 < n)%N ->
-  lead_coef ('X^n - c%:P) = 1.
-Proof.
-move=> gt0_n; rewrite lead_coefDl ?lead_coefXn //.
-by rewrite size_opp size_polyC size_polyXn ltnS (leq_trans (leq_b1 _)).
-Qed.
-
-Lemma lead_coef_XsubC {R : ringType} (c : R) :
-  lead_coef ('X - c%:P) = 1.
-Proof. by apply: (@lead_coef_XnsubC _ 1%N). Qed.
-
-Lemma monic_XsubC {R : ringType} (c : R) : 'X - c%:P \is monic.
-Proof. by rewrite monicE lead_coef_XsubC. Qed.
-
-Lemma monic_XnsubC {R : ringType} n (c : R) : (0 < n)%N -> 'X^n - c%:P \is monic.
-Proof. by move=> gt0_n; rewrite monicE lead_coef_XnsubC. Qed.
-
-Lemma size_XnsubC {R : ringType} n (c : R) : (0 < n)%N -> size ('X^n - c%:P) = n.+1.
-Proof.
-move=> gt0_n; rewrite size_addl ?size_polyXn //.
-by rewrite size_opp size_polyC; case: (c =P 0).
-Qed.
-
-Lemma map_polyXsubC (aR rR : ringType) (f : {rmorphism aR -> rR}) x :
-   map_poly f ('X - x%:P) = 'X - (f x)%:P.
-Proof. by rewrite rmorphB/= map_polyX map_polyC. Qed.
-
-Lemma poly_XsubC_over {R : ringType} c (S : {pred R}) (addS : subringPred S)
-  (kS : keyed_pred addS): c \in kS -> 'X - c%:P \is a polyOver kS.
-Proof. by move=> cS; rewrite rpredB ?polyOverC ?polyOverX. Qed.
-
-Lemma poly_XnsubC_over {R : ringType} n c (S : {pred R}) (addS : subringPred S)
-  (kS : keyed_pred addS): c \in kS -> 'X^n - c%:P \is a polyOver kS.
-Proof. by move=> cS; rewrite rpredB ?rpredX ?polyOverX ?polyOverC. Qed.
-
-Lemma lead_coef_prod {R : idomainType} (ps : seq {poly R}) :
-  lead_coef (\prod_(p <- ps) p) = \prod_(p <- ps) lead_coef p.
-Proof. by apply/big_morph/lead_coef1; apply: lead_coefM. Qed.
-
-Lemma lead_coef_prod_XsubC {R : idomainType} (cs : seq R) :
-  lead_coef (\prod_(c <- cs) ('X - c%:P)) = 1.
-Proof.
-rewrite -(big_map (fun c : R => 'X - c%:P) xpredT idfun) /=.
-rewrite lead_coef_prod big_seq (eq_bigr (fun=> 1)) ?big1 //=.
-by move=> i /mapP[c _ ->]; apply: lead_coef_XsubC.
-Qed.
-
-Lemma coef0M {R : ringType} (p q : {poly R}) : (p * q)`_0 = p`_0 * q`_0.
-Proof. by rewrite coefM big_ord1. Qed.
-
-Lemma coef0_prod {R : ringType} {T : Type} (ps : seq T) (F : T -> {poly R}) P :
-  (\prod_(p <- ps | P p) F p)`_0 = \prod_(p <- ps | P p) (F p)`_0.
-Proof.
-by apply: (big_morph (fun p : {poly R} => p`_0));
-   [apply: coef0M | rewrite coefC eqxx].
-Qed.
-
-Lemma map_prod_XsubC (aR rR : ringType) (f : {rmorphism aR -> rR}) rs :
-  map_poly f (\prod_(x <- rs) ('X - x%:P)) =
-  \prod_(x <- map f rs) ('X - x%:P).
-Proof.
-by rewrite rmorph_prod big_map; apply/eq_bigr => x /=; rewrite map_polyXsubC.
-Qed.
+Lemma eqpW (R : idomainType) (p q : {poly R}) : p = q -> p %= q.
+Proof. by move->; rewrite eqpxx. Qed.
 
-Lemma eq_in_map_poly_id0 (aR rR : ringType) (f g : aR -> rR)
-  (S0 : {pred aR}) (addS : addrPred S0) (kS : keyed_pred addS) :
-  f 0 = 0 -> g 0 = 0 ->
-  {in kS, f =1 g} -> {in polyOver kS, map_poly f =1 map_poly g}.
+Lemma horner_mod (R : fieldType) (p q : {poly R}) x : root q x ->
+  (p %% q).[x] = p.[x].
 Proof.
-move=> f0 g0 eq_fg p pP; apply/polyP => i.
-by rewrite !coef_map_id0// eq_fg// (polyOverP _).
+by move=> /eqP qx0; rewrite [p in RHS](divp_eq p q) !hornerE qx0 mulr0 add0r.
 Qed.
 
-Lemma eq_in_map_poly (aR rR : ringType) (f g : {additive aR -> rR})
-  (S0 : {pred aR}) (addS : addrPred S0) (kS : keyed_pred addS) :
-  {in kS, f =1 g} -> {in polyOver kS, map_poly f =1 map_poly g}.
-Proof. by move=> /eq_in_map_poly_id0; apply; rewrite //?raddf0. Qed.
-
-Lemma mapf_root (F : fieldType) (R : ringType) (f : {rmorphism F -> R})
-    (p : {poly F}) (x : F) :
-  root (p ^^ f) (f x) = root p x.
-Proof. by rewrite !rootE horner_map fmorph_eq0. Qed.
+Lemma root_dvdp (F : idomainType) (p q : {poly F}) (x : F) :
+  root p x -> p %| q -> root q x.
+Proof. rewrite -!dvdp_XsubCl; exact: dvdp_trans. Qed.
 
 Section multiplicity.
 Variable (L : fieldType).
@@ -351,15 +318,6 @@ Qed.
 
 End multiplicity.
 
-Lemma primitive_root_eq0 (F : fieldType) n (w : F) :
-  n.-primitive_root w -> (w == 0) = (n == 0%N).
-Proof.
-move=> wp; apply/eqP/idP => [w0|/eqP p0]; move: wp; rewrite ?w0 ?p0; last first.
-  by move=> /prim_order_gt0//.
-move=> /prim_expr_order/esym/eqP.
-by rewrite expr0n; case: (n =P 0%N); rewrite ?oner_eq0.
-Qed.
-
 Lemma dvdp_exp_XsubC (R : idomainType) (p : {poly R}) (c : R) n :
   reflect (exists2 k, (k <= n)%N & p %= ('X - c%:P) ^+ k)
           (p %| ('X - c%:P) ^+ n).
@@ -380,70 +338,6 @@ move: rNc; rewrite -coprimep_XsubC => /(coprimep_expr n) /coprimepP.
 by move=> /(_ _ (dvdpp _)); rewrite -size_poly_eq1 => /(_ _)/eqP.
 Qed.
 
-Lemma eisenstein (p : nat) (q : {poly int}) : prime p -> (size q != 1)%N ->
-  (~~ (p %| lead_coef q))%Z -> (~~ ((p : int) ^+ 2 %| q`_0))%Z ->
-  (forall i, (i < (size q).-1)%N -> p %| q`_i)%Z ->
-  irreducible_poly (map_poly (intr : int -> rat) q).
-Proof.
-move=> p_prime qN1 Ndvd_pql Ndvd_pq0 dvd_pq.
-have qN0 : q != 0 by rewrite -lead_coef_eq0; apply: contraNneq Ndvd_pql => ->.
-split.
-   rewrite size_map_poly_id0 ?intr_eq0 ?lead_coef_eq0//.
-   by rewrite ltn_neqAle eq_sym qN1 size_poly_gt0.
-move=> f' +/dvdpP_rat_int[f [d dN0 feq]]; rewrite {f'}feq size_scale// => fN1.
-move=> /= [g q_eq]; rewrite q_eq (eqp_trans (eqp_scale _ _))//.
-have fN0 : f != 0 by apply: contra_neq qN0; rewrite q_eq => ->; rewrite mul0r.
-have gN0 : g != 0 by apply: contra_neq qN0; rewrite q_eq => ->; rewrite mulr0.
-rewrite size_map_poly_id0 ?intr_eq0 ?lead_coef_eq0// in fN1.
-have [/eqP/size_poly1P[c cN0 ->]|gN1] := eqVneq (size g) 1%N.
-  by rewrite mulrC mul_polyC map_polyZ/= eqp_sym eqp_scale// intr_eq0.
-have c_neq0 : (lead_coef q)%:~R != 0 :> 'F_p
-   by rewrite -(dvdz_charf (char_Fp _)).
-have : map_poly (intr : int -> 'F_p) q = (lead_coef q)%:~R *: 'X^(size q).-1.
-  apply/val_inj/(@eq_from_nth _ 0) => [|i]; rewrite size_map_poly_id0//.
-    by rewrite size_scale// size_polyXn -polySpred.
-  move=> i_small; rewrite coef_poly i_small coefZ coefXn lead_coefE.
-  move: i_small; rewrite polySpred// ltnS/=.
-  case: ltngtP => // [i_lt|->]; rewrite (mulr1, mulr0)//= => _.
-  by apply/eqP; rewrite -(dvdz_charf (char_Fp _))// dvd_pq.
-rewrite [in LHS]q_eq rmorphM/=.
-set c := (X in X *: _); set n := (_.-1).
-set pf := map_poly _ f; set pg := map_poly _ g => pfMpg.
-have dvdXn (r : {poly _}) : size r != 1%N -> r %| c *: 'X^n -> r`_0 = 0.
-  move=> rN1; rewrite (eqp_dvdr _ (eqp_scale _ _))//.
-  rewrite -['X]subr0; move=> /dvdp_exp_XsubC[k lekn]; rewrite subr0.
-  move=> /eqpP[u /andP[u1N0 u2N0]]; have [->|k_gt0] := posnP k.
-    move=> /(congr1 (size \o val))/eqP.
-    by rewrite /= !size_scale// size_polyXn (negPf rN1).
-  move=> /(congr1 (fun p : {poly _} => p`_0))/eqP.
-  by rewrite !coefZ coefXn ltn_eqF// mulr0 mulf_eq0 (negPf u1N0) => /eqP.
-suff : ((p : int) ^+ 2 %| q`_0)%Z by rewrite (negPf Ndvd_pq0).
-have := c_neq0; rewrite q_eq coefM big_ord1.
-rewrite lead_coefM rmorphM mulf_eq0 negb_or => /andP[lpfN0 qfN0].
-have pfN1 : size pf != 1%N by rewrite size_map_poly_id0.
-have pgN1 : size pg != 1%N by rewrite size_map_poly_id0.
-have /(dvdXn _ pgN1) /eqP : pg %| c *: 'X^n by rewrite -pfMpg dvdp_mull.
-have /(dvdXn _ pfN1) /eqP : pf %| c *: 'X^n by rewrite -pfMpg dvdp_mulr.
-by rewrite !coef_map// -!(dvdz_charf (char_Fp _))//; apply: dvdz_mul.
-Qed.
-
-(***********)
-(* polydiv *)
-(***********)
-
-Lemma eqpW (R : idomainType) (p q : {poly R}) : p = q -> p %= q.
-Proof. by move->; rewrite eqpxx. Qed.
-
-Lemma horner_mod (R : fieldType) (p q : {poly R}) x : root q x ->
-  (p %% q).[x] = p.[x].
-Proof.
-by move=> /eqP qx0; rewrite [p in RHS](divp_eq p q) !hornerE qx0 mulr0 add0r.
-Qed.
-
-Lemma root_dvdp (F : idomainType) (p q : {poly F}) (x : F) :
-  root p x -> p %| q -> root q x.
-Proof. rewrite -!dvdp_XsubCl; exact: dvdp_trans. Qed.
-
 (**********)
 (* vector *)
 (**********)