Skip to content

Commit

Permalink
backport ssralg and poly
Browse files Browse the repository at this point in the history
  • Loading branch information
@Tragicus
Tragicus committed Mar 22, 2024
1 parent 80b9812 commit f9a8968
Showing 1 changed file with 85 additions and 191 deletions.
276 changes: 85 additions & 191 deletions theories/xmathcomp/various.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand All @@ -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).
Expand Down Expand Up @@ -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).
Expand All @@ -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 *)
(**********)
Expand Down

0 comments on commit f9a8968

Please sign in to comment.