diff options
Diffstat (limited to 'mathcomp/algebra')
| -rw-r--r-- | mathcomp/algebra/intdiv.v | 27 | ||||
| -rw-r--r-- | mathcomp/algebra/matrix.v | 10 | ||||
| -rw-r--r-- | mathcomp/algebra/mxalgebra.v | 24 | ||||
| -rw-r--r-- | mathcomp/algebra/mxpoly.v | 4 | ||||
| -rw-r--r-- | mathcomp/algebra/poly.v | 63 | ||||
| -rw-r--r-- | mathcomp/algebra/polyXY.v | 2 | ||||
| -rw-r--r-- | mathcomp/algebra/polydiv.v | 228 | ||||
| -rw-r--r-- | mathcomp/algebra/ssralg.v | 2 | ||||
| -rw-r--r-- | mathcomp/algebra/ssrint.v | 30 | ||||
| -rw-r--r-- | mathcomp/algebra/vector.v | 12 | ||||
| -rw-r--r-- | mathcomp/algebra/zmodp.v | 2 |
11 files changed, 264 insertions, 140 deletions
diff --git a/mathcomp/algebra/intdiv.v b/mathcomp/algebra/intdiv.v index 808d21d..336b6df 100644 --- a/mathcomp/algebra/intdiv.v +++ b/mathcomp/algebra/intdiv.v @@ -601,11 +601,11 @@ Proof. by rewrite /gcdz abszM => /Gauss_gcdr->. Qed. Lemma Gauss_gcdzl p m n : coprimez p n -> gcdz p (m * n) = gcdz p m. Proof. by move=> co_pn; rewrite mulrC Gauss_gcdzr. Qed. -Lemma coprimez_mulr p m n : coprimez p (m * n) = coprimez p m && coprimez p n. -Proof. by rewrite -coprime_mulr -abszM. Qed. +Lemma coprimezMr p m n : coprimez p (m * n) = coprimez p m && coprimez p n. +Proof. by rewrite -coprimeMr -abszM. Qed. -Lemma coprimez_mull p m n : coprimez (m * n) p = coprimez m p && coprimez n p. -Proof. by rewrite -coprime_mull -abszM. Qed. +Lemma coprimezMl p m n : coprimez (m * n) p = coprimez m p && coprimez n p. +Proof. by rewrite -coprimeMl -abszM. Qed. Lemma coprimez_pexpl k m n : (0 < k)%N -> coprimez (m ^+ k) n = coprimez m n. Proof. by rewrite /coprimez /gcdz abszX; apply: coprime_pexpl. Qed. @@ -613,11 +613,11 @@ Proof. by rewrite /coprimez /gcdz abszX; apply: coprime_pexpl. Qed. Lemma coprimez_pexpr k m n : (0 < k)%N -> coprimez m (n ^+ k) = coprimez m n. Proof. by move=> k_gt0; rewrite !(coprimez_sym m) coprimez_pexpl. Qed. -Lemma coprimez_expl k m n : coprimez m n -> coprimez (m ^+ k) n. -Proof. by rewrite /coprimez /gcdz abszX; apply: coprime_expl. Qed. +Lemma coprimezXl k m n : coprimez m n -> coprimez (m ^+ k) n. +Proof. by rewrite /coprimez /gcdz abszX; apply: coprimeXl. Qed. -Lemma coprimez_expr k m n : coprimez m n -> coprimez m (n ^+ k). -Proof. by rewrite !(coprimez_sym m); apply: coprimez_expl. Qed. +Lemma coprimezXr k m n : coprimez m n -> coprimez m (n ^+ k). +Proof. by rewrite !(coprimez_sym m); apply: coprimezXl. Qed. Lemma coprimez_dvdl m n p : (m %| n)%N -> coprimez n p -> coprimez m p. Proof. exact: coprime_dvdl. Qed. @@ -878,7 +878,7 @@ Lemma dvdpP_rat_int p q : {p1 : {poly int} & {a | a != 0 & p = a *: pZtoQ p1} & {r | q = p1 * r}}. Proof. have{p} [p [a nz_a ->]] := rat_poly_scale p. -rewrite dvdp_scalel ?invr_eq0 ?intr_eq0 // dvdp_rat_int => dv_p_q. +rewrite dvdpZl ?invr_eq0 ?intr_eq0 // dvdp_rat_int => dv_p_q. exists (zprimitive p); last exact: dvdpP_int. have [-> | nz_p] := eqVneq p 0. by exists 1; rewrite ?oner_eq0 // zprimitive0 map_poly0 !scaler0. @@ -1074,3 +1074,12 @@ rewrite -defS -2!mulmxA; have ->: T *m pinvmx T = 1%:M. by apply: (row_free_inj uT); rewrite mul1mx mulmxKpV. by move=> i; rewrite mulmx1 -map_mxM 2!mxE denq_int mxE. Qed. + +Notation "@ 'coprimez_expl'" := + (deprecate coprimez_expl coprimezXl) (at level 10, only parsing) : fun_scope. +Notation "@ 'coprimez_expr'" := + (deprecate coprimez_expr coprimezXr) (at level 10, only parsing) : fun_scope. +Notation coprimez_mull := (deprecate coprimez_mull coprimezMl) (only parsing). +Notation coprimez_mulr := (deprecate coprimez_mulr coprimezMr) (only parsing). +Notation coprimez_expl := (fun k => @coprimez_expl k _ _) (only parsing). +Notation coprimez_expr := (fun k => @coprimez_expr k _ _) (only parsing). diff --git a/mathcomp/algebra/matrix.v b/mathcomp/algebra/matrix.v index feb9edd..f7d7730 100644 --- a/mathcomp/algebra/matrix.v +++ b/mathcomp/algebra/matrix.v @@ -1699,12 +1699,12 @@ Proof. by apply/matrixP=> i j; rewrite !mxE raddfN. Qed. Lemma map_mxD A B : (A + B)^f = A^f + B^f. Proof. by apply/matrixP=> i j; rewrite !mxE raddfD. Qed. -Lemma map_mx_sub A B : (A - B)^f = A^f - B^f. +Lemma map_mxB A B : (A - B)^f = A^f - B^f. Proof. by rewrite map_mxD map_mxN. Qed. Definition map_mx_sum := big_morph _ map_mxD map_mx0. -Canonical map_mx_additive := Additive map_mx_sub. +Canonical map_mx_additive := Additive map_mxB. End MapZmodMatrix. @@ -2691,7 +2691,7 @@ Proof. by apply/matrixP=> i j; rewrite !mxE cofactor_map_mx. Qed. End FixedSize. Lemma map_copid_mx n r : (copid_mx r)^f = copid_mx r :> 'M_n. -Proof. by rewrite map_mx_sub map_mx1 map_pid_mx. Qed. +Proof. by rewrite map_mxB map_mx1 map_pid_mx. Qed. Lemma map_mx_is_multiplicative n' (n := n'.+1) : multiplicative (map_mx f : 'M_n -> 'M_n). @@ -3687,3 +3687,7 @@ Canonical mxOver_subringPred (S : {pred R}) (ringS : subringPred S) End mxRingOver. End mxOver. + +Notation "@ 'map_mx_sub'" := + (deprecate map_mx_sub map_mxB) (at level 10, only parsing) : fun_scope. +Notation map_mx_sub := (fun f => @map_mx_sub _ _ f) (only parsing). diff --git a/mathcomp/algebra/mxalgebra.v b/mathcomp/algebra/mxalgebra.v index 7e213b8..e65bc3c 100644 --- a/mathcomp/algebra/mxalgebra.v +++ b/mathcomp/algebra/mxalgebra.v @@ -2581,8 +2581,8 @@ rewrite mulmx_suml linear_sum summx_sub //= => i _. by rewrite -mulmxA !mem_mulsmx. Qed. -Lemma mulsmx_addl m1 m2 m3 n - (R1 : 'A_(m1, n)) (R2 : 'A_(m2, n)) (R3 : 'A_(m3, n)) : +Lemma mulsmxDl m1 m2 m3 n + (R1 : 'A_(m1, n)) (R2 : 'A_(m2, n)) (R3 : 'A_(m3, n)) : ((R1 + R2) * R3 = R1 * R3 + R2 * R3)%MS. Proof. rewrite -(genmx_muls R2 R3) -(genmx_muls R1 R3) -genmx_muls -genmx_adds. @@ -2591,8 +2591,8 @@ apply/mulsmx_subP=> _ A3 /memmx_addsP[A [R_A1 R_A2 ->]] R_A3. by rewrite mulmxDl linearD addmx_sub_adds ?mem_mulsmx. Qed. -Lemma mulsmx_addr m1 m2 m3 n - (R1 : 'A_(m1, n)) (R2 : 'A_(m2, n)) (R3 : 'A_(m3, n)) : +Lemma mulsmxDr m1 m2 m3 n + (R1 : 'A_(m1, n)) (R2 : 'A_(m2, n)) (R3 : 'A_(m3, n)) : (R1 * (R2 + R3) = R1 * R2 + R1 * R3)%MS. Proof. rewrite -(genmx_muls R1 R3) -(genmx_muls R1 R2) -genmx_muls -genmx_adds. @@ -2857,7 +2857,7 @@ set pAnz := [pred k | A k.1 k.2 != 0]. rewrite (@eq_pick _ _ pAnz) => [|k]; last by rewrite /= mxE fmorph_eq0. case: {+}(pick _) => [[i j]|]; last by rewrite !map_mx1. rewrite mxE -fmorphV -map_xcol -map_xrow -map_dlsubmx -map_drsubmx. -rewrite -map_ursubmx -map_mxZ -map_mxM -map_mx_sub {}IHm /=. +rewrite -map_ursubmx -map_mxZ -map_mxM -map_mxB {}IHm /=. case: {+}(Gaussian_elimination _) => [[L U] r] /=; rewrite map_xrow map_xcol. by rewrite !(@map_block_mx _ _ f 1 _ 1) !map_mx0 ?map_mx1 ?map_scalar_mx. Qed. @@ -2952,7 +2952,7 @@ by rewrite -!map_capmx !map_submx -!diffmxE andbb. Qed. Lemma map_eigenspace n (g : 'M_n) a : (eigenspace g a)^f = eigenspace g^f (f a). -Proof. by rewrite map_kermx map_mx_sub ?map_scalar_mx. Qed. +Proof. by rewrite map_kermx map_mxB ?map_scalar_mx. Qed. Lemma eigenvalue_map n (g : 'M_n) a : eigenvalue g^f (f a) = eigenvalue g a. Proof. by rewrite /eigenvalue -map_eigenspace map_mx_eq0. Qed. @@ -2972,12 +2972,18 @@ Qed. Lemma map_cent_mx m n (E : 'A_(m, n)) : ('C(E)%MS)^f = 'C(E^f)%MS. Proof. -rewrite map_kermx //; congr (kermx _); apply: map_lin_mx => // A. -rewrite map_mxM //; congr (_ *m _); apply: map_lin_mx => //= B. -by rewrite map_mx_sub ? map_mxM. +rewrite map_kermx; congr kermx; apply: map_lin_mx => A; rewrite map_mxM. +by congr (_ *m _); apply: map_lin_mx => B; rewrite map_mxB ?map_mxM. Qed. Lemma map_center_mx m n (E : 'A_(m, n)) : (('Z(E))^f :=: 'Z(E^f))%MS. Proof. by rewrite /center_mx -map_cent_mx; apply: map_capmx. Qed. End MapMatrixSpaces. + +Notation "@ 'mulsmx_addl'" := + (deprecate mulsmx_addl mulsmxDl) (at level 10, only parsing) : fun_scope. +Notation "@ 'mulsmx_addr'" := + (deprecate mulsmx_addr mulsmxDr) (at level 10, only parsing) : fun_scope. +Notation mulsmx_addl := (@mulsmx_addl _ _ _ _ _) (only parsing). +Notation mulsmx_addr := (@mulsmx_addr _ _ _ _ _) (only parsing). diff --git a/mathcomp/algebra/mxpoly.v b/mathcomp/algebra/mxpoly.v index 74d524e..c7f8fb1 100644 --- a/mathcomp/algebra/mxpoly.v +++ b/mathcomp/algebra/mxpoly.v @@ -890,7 +890,7 @@ rewrite !big_cons; case: ifP => [Pj|PNj]; rewrite ?ihjs ?submx_refl//. suff cjjs: coprimep (p_ j) (\prod_(i <- js | P i) p_ i). by rewrite !kermxpolyM// !(adds_eqmx (eqmx_refl _) (ihjs _)) ?submx_refl. rewrite (@big_morph _ _ _ true andb) ?big_all_cond ?coprimep1//; last first. - by move=> p q; rewrite coprimep_mulr. + by move=> p q; rewrite coprimepMr. apply/allP => i i_js; apply/implyP => Pi; apply: p_coprime => //. by apply: contraNneq jNjs => <-. Qed. @@ -907,7 +907,7 @@ have cpNi : {in [pred j | P j && (j != i)] &, rewrite -!(cap_eqmx (eqmx_refl _) (kermxpoly_prod g _))//. rewrite mxdirect_kermxpoly ?submx_refl//. rewrite (@big_morph _ _ _ true andb) ?big_all_cond ?coprimep1//; last first. - by move=> p q; rewrite coprimep_mulr. + by move=> p q; rewrite coprimepMr. by apply/allP => j _; apply/implyP => /andP[Pj neq_ji]; apply: p_coprime. Qed. diff --git a/mathcomp/algebra/poly.v b/mathcomp/algebra/poly.v index a33788d..e9e9c45 100644 --- a/mathcomp/algebra/poly.v +++ b/mathcomp/algebra/poly.v @@ -428,26 +428,25 @@ Lemma coef_sum I (r : seq I) (P : pred I) (F : I -> {poly R}) k : (\sum_(i <- r | P i) F i)`_k = \sum_(i <- r | P i) (F i)`_k. Proof. exact: (raddf_sum (coefp_additive k)). Qed. -Lemma polyC_add : {morph polyC : a b / a + b}. +Lemma polyCD : {morph polyC : a b / a + b}. Proof. by move=> a b; apply/polyP=> [[|i]]; rewrite coefD !coefC ?addr0. Qed. -Lemma polyC_opp : {morph polyC : c / - c}. +Lemma polyCN : {morph polyC : c / - c}. Proof. by move=> c; apply/polyP=> [[|i]]; rewrite coefN !coefC ?oppr0. Qed. -Lemma polyC_sub : {morph polyC : a b / a - b}. -Proof. by move=> a b; rewrite polyC_add polyC_opp. Qed. +Lemma polyCB : {morph polyC : a b / a - b}. +Proof. by move=> a b; rewrite polyCD polyCN. Qed. -Canonical polyC_additive := Additive polyC_sub. +Canonical polyC_additive := Additive polyCB. -Lemma polyC_muln n : {morph polyC : c / c *+ n}. -Proof. exact: raddfMn. Qed. +Lemma polyCMn n : {morph polyC : c / c *+ n}. Proof. exact: raddfMn. Qed. Lemma size_opp p : size (- p) = size p. Proof. by apply/eqP; rewrite eqn_leq -{3}(opprK p) -[-%R]/opp_poly unlock !size_poly. Qed. -Lemma lead_coef_opp p : lead_coef (- p) = - lead_coef p. +Lemma lead_coefN p : lead_coef (- p) = - lead_coef p. Proof. by rewrite /lead_coef size_opp coefN. Qed. Lemma size_add p q : size (p + q) <= maxn (size p) (size q). @@ -621,15 +620,14 @@ rewrite coefMr big_ord_recl subn0. by rewrite big1 => [|j _]; rewrite coefC !simp. Qed. -Lemma polyC_mul : {morph polyC : a b / a * b}. +Lemma polyCM : {morph polyC : a b / a * b}. Proof. by move=> a b; apply/polyP=> [[|i]]; rewrite coefCM !coefC ?simp. Qed. Fact polyC_multiplicative : multiplicative polyC. -Proof. by split; first apply: polyC_mul. Qed. +Proof. by split; first apply: polyCM. Qed. Canonical polyC_rmorphism := AddRMorphism polyC_multiplicative. -Lemma polyC_exp n : {morph polyC : c / c ^+ n}. -Proof. exact: rmorphX. Qed. +Lemma polyC_exp n : {morph polyC : c / c ^+ n}. Proof. exact: rmorphX. Qed. Lemma size_exp_leq p n : size (p ^+ n) <= ((size p).-1 * n).+1. Proof. @@ -665,7 +663,7 @@ by case: leqP => // le_p_n; rewrite nth_default ?mulr0. Qed. Fact scale_polyA a b p : scale_poly a (scale_poly b p) = scale_poly (a * b) p. -Proof. by rewrite !scale_polyE mulrA polyC_mul. Qed. +Proof. by rewrite !scale_polyE mulrA polyCM. Qed. Fact scale_1poly : left_id 1 scale_poly. Proof. by move=> p; rewrite scale_polyE mul1r. Qed. @@ -761,9 +759,7 @@ by elim: {p}(p : seq R) => //= p c IHp; rewrite cons_poly_def; apply: Kcons. Qed. Lemma polyseqXsubC a : 'X - a%:P = [:: - a; 1] :> seq R. -Proof. -by rewrite -['X]mul1r -polyC_opp -cons_poly_def polyseq_cons polyseq1. -Qed. +Proof. by rewrite -['X]mul1r -polyCN -cons_poly_def polyseq_cons polyseq1. Qed. Lemma size_XsubC a : size ('X - a%:P) = 2%N. Proof. by rewrite polyseqXsubC. Qed. @@ -843,7 +839,7 @@ Lemma poly_def n E : \poly_(i < n) E i = \sum_(i < n) E i *: 'X^i. Proof. rewrite unlock; elim: n => [|n IHn] in E *; first by rewrite big_ord0. rewrite big_ord_recl /= cons_poly_def addrC expr0 alg_polyC. -congr (_ + _); rewrite (iota_addl 1 0) -map_comp IHn big_distrl /=. +congr (_ + _); rewrite (iotaDl 1 0) -map_comp IHn big_distrl /=. by apply: eq_bigr => i _; rewrite -scalerAl exprSr. Qed. @@ -1065,7 +1061,7 @@ Proof. by elim/big_rec2: _ => [|i _ p _ <-]; rewrite (horner0, hornerD). Qed. Lemma hornerCM a p x : (a%:P * p).[x] = a * p.[x]. Proof. elim/poly_ind: p => [|p c IHp]; first by rewrite !(mulr0, horner0). -by rewrite mulrDr mulrA -polyC_mul !hornerMXaddC IHp mulrDr mulrA. +by rewrite mulrDr mulrA -polyCM !hornerMXaddC IHp mulrDr mulrA. Qed. Lemma hornerZ c p x : (c *: p).[x] = c * p.[x]. @@ -1528,7 +1524,7 @@ Proof. by case: n => // n; rewrite derivSn derivC linear0. Qed. Lemma derivnD n : {morph derivn n : p q / p + q}. Proof. exact: linearD. Qed. -Lemma derivn_sub n : {morph derivn n : p q / p - q}. +Lemma derivnB n : {morph derivn n : p q / p - q}. Proof. exact: linearB. Qed. Lemma derivnMn n m p : (p *+ m)^`(n) = p^`(n) *+ m. @@ -2219,7 +2215,7 @@ Definition poly_inv p := if p \in poly_unit then (p`_0)^-1%:P else p. Fact poly_mulVp : {in poly_unit, left_inverse 1 poly_inv *%R}. Proof. move=> p Up; rewrite /poly_inv Up. -by case/andP: Up => /size_poly1P[c _ ->]; rewrite coefC -polyC_mul => /mulVr->. +by case/andP: Up => /size_poly1P[c _ ->]; rewrite coefC -polyCM => /mulVr->. Qed. Fact poly_intro_unit p q : q * p = 1 -> p \in poly_unit. @@ -2264,7 +2260,7 @@ Proof. by []. Qed. Lemma poly_invE p : p ^-1 = if p \in GRing.unit then (p`_0)^-1%:P else p. Proof. by []. Qed. -Lemma polyC_inv c : c%:P^-1 = (c^-1)%:P. +Lemma polyCV c : c%:P^-1 = (c^-1)%:P. Proof. have [/rmorphV-> // | nUc] := boolP (c \in GRing.unit). by rewrite !invr_out // poly_unitE coefC (negbTE nUc) andbF. @@ -2771,3 +2767,28 @@ by rewrite monic_prod => // i; rewrite monicXsubC. Qed. End ClosedField. + +Notation "@ 'polyC_add'" := + (deprecate polyC_add polyCD) (at level 10, only parsing) : fun_scope. +Notation "@ 'polyC_opp'" := + (deprecate polyC_opp polyCN) (at level 10, only parsing) : fun_scope. +Notation "@ 'polyC_sub'" := + (deprecate polyC_sub polyCB) (at level 10, only parsing) : fun_scope. +Notation "@ 'polyC_muln'" := + (deprecate polyC_muln polyCMn) (at level 10, only parsing) : fun_scope. +Notation "@ 'polyC_mul'" := + (deprecate polyC_mul polyCM) (at level 10, only parsing) : fun_scope. +Notation "@ 'polyC_inv'" := + (deprecate polyC_inv polyCV) (at level 10, only parsing) : fun_scope. +Notation "@ 'lead_coef_opp'" := + (deprecate lead_coef_opp lead_coefN) (at level 10, only parsing) : fun_scope. +Notation "@ 'derivn_sub'" := + (deprecate derivn_sub derivnB) (at level 10, only parsing) : fun_scope. +Notation polyC_add := (@polyC_add _) (only parsing). +Notation polyC_opp := (@polyC_opp _) (only parsing). +Notation polyC_sub := (@polyC_sub _) (only parsing). +Notation polyC_muln := (@polyC_muln _) (only parsing). +Notation polyC_mul := (@polyC_mul _) (only parsing). +Notation polyC_inv := (@polyC_inv _) (only parsing). +Notation lead_coef_opp := (@lead_coef_opp _) (only parsing). +Notation derivn_sub := (@derivn_sub _) (only parsing). diff --git a/mathcomp/algebra/polyXY.v b/mathcomp/algebra/polyXY.v index 9bc8fd5..fe0acb4 100644 --- a/mathcomp/algebra/polyXY.v +++ b/mathcomp/algebra/polyXY.v @@ -228,7 +228,7 @@ Proof. by rewrite -!size_poly_eq0 size_poly_XmY. Qed. Lemma lead_coef_poly_XaY p : lead_coef (poly_XaY p) = (lead_coef p)%:P. Proof. -rewrite lead_coef_comp ?size_XaddC // -['Y]opprK -polyC_opp lead_coefXsubC. +rewrite lead_coef_comp ?size_XaddC // -['Y]opprK -polyCN lead_coefXsubC. by rewrite expr1n mulr1 lead_coef_map_inj //; apply: polyC_inj. Qed. diff --git a/mathcomp/algebra/polydiv.v b/mathcomp/algebra/polydiv.v index a7d3b1e..8459c45 100644 --- a/mathcomp/algebra/polydiv.v +++ b/mathcomp/algebra/polydiv.v @@ -365,7 +365,7 @@ elim: (size m) 0%N 0 {1 4 6}m (leqnn (size m)) => [|n IHn] k q r Hr /=. by rewrite size_poly0 size_poly_gt0. case: ltnP => Hlt Heq; first by constructor. apply/IHn=> [|Cda]; last first. - rewrite mulrDl addrAC -addrA subrK exprSr polyC_mul mulrA Heq //. + rewrite mulrDl addrAC -addrA subrK exprSr polyCM mulrA Heq //. by rewrite mulrDl -mulrA Cda mulrA. apply/leq_sizeP => j Hj; rewrite coefB coefMC -scalerAl coefZ coefXnM. rewrite ltn_subRL ltnNge (leq_trans Hr) /=; last first. @@ -465,7 +465,7 @@ suff: by rewrite rreg_size ?ltn_rmodp //; exact: rregX. rewrite mulrDl addrAC mulNr -!mulrA polyC_exp -(commrX (m-v) Cdl). rewrite -polyC_exp mulrA -mulrDl -rdivp_eq // [(_ ^+ (m - k))%:P]polyC_exp. -rewrite -(commrX (m-k) Cdl) -polyC_exp mulrA -he -!mulrA -!polyC_mul -/v. +rewrite -(commrX (m-k) Cdl) -polyC_exp mulrA -he -!mulrA -!polyCM -/v. by rewrite -!exprD addnC subnK ?leq_maxl // addnC subnK ?subrr ?leq_maxr. Qed. @@ -553,15 +553,15 @@ case: (monic_comreg mond)=> Hc Hr; rewrite [r in _ * _ + r]rdivp_eq addrA. by rewrite -mulrDl rdivp_addl_mul_small // ltn_rmodp monic_neq0. Qed. -Lemma rdivp_addl q r : rdvdp d q -> rdivp (q + r) d = rdivp q d + rdivp r d. +Lemma rdivpDl q r : rdvdp d q -> rdivp (q + r) d = rdivp q d + rdivp r d. Proof. case: (monic_comreg mond)=> Hc Hr; rewrite [r in q + r]rdivp_eq addrA. rewrite [q in q + _ + _]rdivp_eq; move/rmodp_eq0P->. by rewrite addr0 -mulrDl rdivp_addl_mul_small // ltn_rmodp monic_neq0. Qed. -Lemma rdivp_addr q r : rdvdp d r -> rdivp (q + r) d = rdivp q d + rdivp r d. -Proof. by rewrite addrC; move/rdivp_addl->; rewrite addrC. Qed. +Lemma rdivpDr q r : rdvdp d r -> rdivp (q + r) d = rdivp q d + rdivp r d. +Proof. by rewrite addrC; move/rdivpDl->; rewrite addrC. Qed. Lemma rdivp_mull p : rdivp (p * d) d = p. Proof. by rewrite -[p * d]addr0 rdivp_addl_mul rdiv0p addr0. Qed. @@ -581,7 +581,7 @@ Proof. by move=> Hd; case: (monic_comreg mond)=> Hc Hr; rewrite /rmodp redivp_eq. Qed. -Lemma rmodp_add p q : rmodp (p + q) d = rmodp p d + rmodp q d. +Lemma rmodpD p q : rmodp (p + q) d = rmodp p d + rmodp q d. Proof. rewrite [p in LHS]rdivp_eq [q in LHS]rdivp_eq addrACA -mulrDl. rewrite rmodp_addl_mul_small //; apply: (leq_ltn_trans (size_add _ _)). @@ -590,7 +590,7 @@ Qed. Lemma rmodp_mulmr p q : rmodp (p * (rmodp q d)) d = rmodp (p * q) d. Proof. -by rewrite [q in RHS]rdivp_eq mulrDr rmodp_add mulrA rmodp_mull add0r. +by rewrite [q in RHS]rdivp_eq mulrDr rmodpD mulrA rmodp_mull add0r. Qed. Lemma rdvdpp : rdvdp d d. @@ -623,6 +623,19 @@ Lemma rdivpK p : rdvdp d p -> (rdivp p d) * d = p. Proof. by move=> dvddp; rewrite [RHS]rdivp_eq rmodp_eq0 ?addr0. Qed. End MonicDivisor. + +Notation "@ 'rdivp_addl'" := + (deprecate rdivp_addl rdivpDl) (at level 10, only parsing) : fun_scope. +Notation "@ 'rdivp_addr'" := + (deprecate rdivp_addr rdivpDr) (at level 10, only parsing) : fun_scope. +Notation "@ 'rmodp_add'" := + (deprecate rmodp_add rmodpD) (at level 10, only parsing) : fun_scope. +Notation rdivp_addl := + (fun d_monic => @rdivp_addl _ _ d_monic _) (only parsing). +Notation rdivp_addr := + (fun d_monic q => @rdivp_addr _ _ d_monic q _) (only parsing). +Notation rmodp_add := (@rmodp_add _ _) (only parsing). + End RingMonic. Module Ring. @@ -824,7 +837,7 @@ rewrite unlock ud redivp_def; constructor => //. rewrite -scalerAl -scalerDr -mul_polyC. have hn0 : (lead_coef d ^+ rscalp m d)%:P != 0. by rewrite polyC_eq0; apply: expf_neq0. - apply: (mulfI hn0); rewrite !mulrA -exprVn !polyC_exp -exprMn -polyC_mul. + apply: (mulfI hn0); rewrite !mulrA -exprVn !polyC_exp -exprMn -polyCM. by rewrite divrr // expr1n mul1r -polyC_exp mul_polyC rdivp_eq. move=> dn0; rewrite size_scale ?ltn_rmodp // -exprVn expf_eq0 negb_and. by rewrite invr_eq0 cdn0 orbT. @@ -1415,13 +1428,18 @@ suff Hmn m n: m %= n -> (m %| p) -> (n %| p). by rewrite /eqp; case/andP=> dd' d'd dp; apply: (dvdp_trans d'd). Qed. -Lemma dvdp_scaler c m n : c != 0 -> m %| c *: n = (m %| n). +Lemma dvdpZr c m n : c != 0 -> m %| c *: n = (m %| n). Proof. by move=> cn0; exact/eqp_dvdr/eqp_scale. Qed. -Lemma dvdp_scalel c m n : c != 0 -> (c *: m %| n) = (m %| n). +Lemma dvdpZl c m n : c != 0 -> (c *: m %| n) = (m %| n). Proof. by move=> cn0; exact/eqp_dvdl/eqp_scale. Qed. -Lemma dvdp_opp d p : d %| (- p) = (d %| p). +Lemma dvdpNl d p : (- d) %| p = (d %| p). +Proof. +by rewrite -scaleN1r; apply/eqp_dvdl/eqp_scale; rewrite oppr_eq0 oner_neq0. +Qed. + +Lemma dvdpNr d p : d %| (- p) = (d %| p). Proof. by apply: eqp_dvdr; rewrite -scaleN1r eqp_scale ?oppr_eq0 ?oner_eq0. Qed. Lemma eqp_mul2r r p q : r != 0 -> (p * r %= q * r) = (p %= q). @@ -1660,7 +1678,7 @@ rewrite (polySpred mn0) addSn /= -[n in _ <= n]add0n leq_add2r -ltnS. rewrite -polySpred //= leq_eqVlt ltnS size_poly_leq0 (negPf mn0) orbF. case/size_poly1P=> c cn0 -> {mn0 m}; rewrite mul_polyC. suff -> : n %% (c *: n) = 0 by rewrite gcd0p; apply: eqp_scale. -by apply/modp_eq0P; rewrite dvdp_scalel. +by apply/modp_eq0P; rewrite dvdpZl. Qed. Lemma gcdp_mulr m n : gcdp n (n * m) %= n. @@ -1670,8 +1688,8 @@ Lemma gcdp_scalel c m n : c != 0 -> gcdp (c *: m) n %= gcdp m n. Proof. move=> cn0; rewrite /eqp dvdp_gcd [gcdp m n %| _]dvdp_gcd !dvdp_gcdr !andbT. apply/andP; split; last first. - by apply: dvdp_trans (dvdp_gcdl _ _) _; rewrite dvdp_scaler. -by apply: dvdp_trans (dvdp_gcdl _ _) _; rewrite dvdp_scalel. + by apply: dvdp_trans (dvdp_gcdl _ _) _; rewrite dvdpZr. +by apply: dvdp_trans (dvdp_gcdl _ _) _; rewrite dvdpZl. Qed. Lemma gcdp_scaler c m n : c != 0 -> gcdp m (c *: n) %= gcdp m n. @@ -1764,10 +1782,10 @@ Proof. by rewrite /coprimep=> /eqP. Qed. Lemma coprimep_def p q : coprimep p q = (size (gcdp p q) == 1%N). Proof. done. Qed. -Lemma coprimep_scalel c m n : c != 0 -> coprimep (c *: m) n = coprimep m n. +Lemma coprimepZl c m n : c != 0 -> coprimep (c *: m) n = coprimep m n. Proof. by move=> ?; rewrite !coprimep_def (eqp_size (gcdp_scalel _ _ _)). Qed. -Lemma coprimep_scaler c m n: c != 0 -> coprimep m (c *: n) = coprimep m n. +Lemma coprimepZr c m n: c != 0 -> coprimep m (c *: n) = coprimep m n. Proof. by move=> ?; rewrite !coprimep_def (eqp_size (gcdp_scaler _ _ _)). Qed. Lemma coprimepp p : coprimep p p = (size p == 1%N). @@ -1981,7 +1999,7 @@ Qed. Lemma Gauss_gcdpl p m n : coprimep p n -> gcdp p (m * n) %= gcdp p m. Proof. by move=> co_pn; rewrite mulrC Gauss_gcdpr. Qed. -Lemma coprimep_mulr p q r : coprimep p (q * r) = (coprimep p q && coprimep p r). +Lemma coprimepMr p q r : coprimep p (q * r) = (coprimep p q && coprimep p r). Proof. apply/coprimepP/andP=> [hp | [/coprimepP-hq hr]]. by split; apply/coprimepP=> d dp dq; rewrite hp //; @@ -1991,8 +2009,8 @@ rewrite Gauss_dvdpl in dqr; first exact: hq. by move/coprimep_dvdr: hr; apply. Qed. -Lemma coprimep_mull p q r: coprimep (q * r) p = (coprimep q p && coprimep r p). -Proof. by rewrite ![coprimep _ p]coprimep_sym coprimep_mulr. Qed. +Lemma coprimepMl p q r: coprimep (q * r) p = (coprimep q p && coprimep r p). +Proof. by rewrite ![coprimep _ p]coprimep_sym coprimepMr. Qed. Lemma modp_coprime k u n : k != 0 -> (k * u) %% n %= 1 -> coprimep k n. Proof. @@ -2005,7 +2023,7 @@ Qed. Lemma coprimep_pexpl k m n : 0 < k -> coprimep (m ^+ k) n = coprimep m n. Proof. case: k => // k _; elim: k => [|k IHk]; first by rewrite expr1. -by rewrite exprS coprimep_mull -IHk andbb. +by rewrite exprS coprimepMl -IHk andbb. Qed. Lemma coprimep_pexpr k m n : 0 < k -> coprimep m (n ^+ k) = coprimep m n. @@ -2108,8 +2126,8 @@ have dn0 : d != 0 by rewrite gcdp_eq0 negb_and nn0 orbT. have c1n0 : c1 != 0 by rewrite !expf_neq0 // lead_coef_eq0. have c2n0 : c2 != 0 by rewrite !expf_neq0 // lead_coef_eq0. have c2k_n0 : c2 ^+ k != 0 by rewrite !expf_neq0 // lead_coef_eq0. -rewrite -(@dvdp_scaler (c1 ^+ k)) ?expf_neq0 ?lead_coef_eq0 //. -rewrite -(@dvdp_scalel (c2 ^+ k)) // -!exprZn def_m def_n !exprMn. +rewrite -(@dvdpZr (c1 ^+ k)) ?expf_neq0 ?lead_coef_eq0 //. +rewrite -(@dvdpZl (c2 ^+ k)) // -!exprZn def_m def_n !exprMn. rewrite dvdp_mul2r ?expf_neq0 //. have: coprimep (m' ^+ k) (n' ^+ k). by rewrite coprimep_pexpl // coprimep_pexpr // coprimep_div_gcd ?mn0. @@ -2120,8 +2138,8 @@ have /size_poly1P [c cn0 em'] : size m' == 1%N. have := hc _ (dvdpp _) hd; rewrite -size_poly_eq1. rewrite polySpred; last by rewrite expf_eq0 negb_and m'_n0 orbT. by rewrite size_exp eqSS muln_eq0 orbC eqn0Ngt k_gt0 /= -eqSS -polySpred. -rewrite -(@dvdp_scalel c2) // def_m em' mul_polyC dvdp_scalel //. -by rewrite -(@dvdp_scaler c1) // def_n dvdp_mull. +rewrite -(@dvdpZl c2) // def_m em' mul_polyC dvdpZl //. +by rewrite -(@dvdpZr c1) // def_n dvdp_mull. Qed. Lemma root_gcd p q x : root (gcdp p q) x = root p x && root q x. @@ -2285,7 +2303,7 @@ Qed. Lemma coprimep_XsubC p c : coprimep p ('X - c%:P) = ~~ root p c. Proof. rewrite -coprimep_modl modp_XsubC /root -alg_polyC. -have [-> | /coprimep_scalel->] := eqVneq; last exact: coprime1p. +have [-> | /coprimepZl->] := eqVneq; last exact: coprime1p. by rewrite scale0r /coprimep gcd0p size_XsubC. Qed. @@ -2340,6 +2358,28 @@ End IDomainPseudoDivision. Hint Resolve eqpxx divp0 divp1 mod0p modp0 modp1 dvdp_mull dvdp_mulr dvdpp : core. Hint Resolve dvdp0 : core. +Notation "@ 'dvdp_scalel'" := + (deprecate dvdp_scalel dvdpZl) (at level 10, only parsing) : fun_scope. +Notation "@ 'dvdp_scaler'" := + (deprecate dvdp_scaler dvdpZr) (at level 10, only parsing) : fun_scope. +Notation "@ 'dvdp_opp'" := + (deprecate dvdp_opp dvdpNr) (at level 10, only parsing) : fun_scope. +Notation "@ 'coprimep_scalel'" := + (deprecate coprimep_scalel coprimepZl) (at level 10, only parsing) : fun_scope. +Notation "@ 'coprimep_scaler'" := + (deprecate coprimep_scaler coprimepZr) (at level 10, only parsing) : fun_scope. +Notation "@ 'coprimep_mull'" := + (deprecate coprimep_mull coprimepMl) (at level 10, only parsing) : fun_scope. +Notation "@ 'coprimep_mulr'" := + (deprecate coprimep_mulr coprimepMr) (at level 10, only parsing) : fun_scope. +Notation dvdp_scalel := (@dvdp_scalel _ _) (only parsing). +Notation dvdp_scaler := (@dvdp_scaler _ _) (only parsing). +Notation dvdp_opp := (@dvdp_opp _) (only parsing). +Notation coprimep_scalel := (@coprimep_scalel _ _) (only parsing). +Notation coprimep_scaler := (@coprimep_scaler _ _) (only parsing). +Notation coprimep_mull := (@coprimep_mull _) (only parsing). +Notation coprimep_mulr := (@coprimep_mulr _) (only parsing). + End CommonIdomain. Module Idomain. @@ -2461,7 +2501,7 @@ move=> ulcq /eqp_eq; move/(congr1 ( *:%R (lead_coef q)^-1 )). by rewrite !scalerA mulrC divrr // scale1r mulrC. Qed. -Lemma modp_scalel c p : (c *: p) %% d = c *: (p %% d). +Lemma modpZl c p : (c *: p) %% d = c *: (p %% d). Proof. have [-> | cn0] := eqVneq c 0; first by rewrite !scale0r mod0p. have e : (c *: p) = (c *: (p %/ d)) * d + c *: (p %% d). @@ -2472,7 +2512,7 @@ rewrite size_polyC cn0 addSn add0n /= ltn_modp -lead_coef_eq0. by apply: contraTneq ulcd => ->; rewrite unitr0. Qed. -Lemma divp_scalel c p : (c *: p) %/ d = c *: (p %/ d). +Lemma divpZl c p : (c *: p) %/ d = c *: (p %/ d). Proof. have [-> | cn0] := eqVneq c 0; first by rewrite !scale0r div0p. have e : (c *: p) = (c *: (p %/ d)) * d + c *: (p %% d). @@ -2486,22 +2526,22 @@ Qed. Lemma eqp_modpl p q : p %= q -> (p %% d) %= (q %% d). Proof. case/eqpP=> [[c1 c2]] /andP /= [c1n0 c2n0 e]. -by apply/eqpP; exists (c1, c2); rewrite ?c1n0 //= -!modp_scalel e. +by apply/eqpP; exists (c1, c2); rewrite ?c1n0 //= -!modpZl e. Qed. Lemma eqp_divl p q : p %= q -> (p %/ d) %= (q %/ d). Proof. case/eqpP=> [[c1 c2]] /andP /= [c1n0 c2n0 e]. -by apply/eqpP; exists (c1, c2); rewrite ?c1n0 // -!divp_scalel e. +by apply/eqpP; exists (c1, c2); rewrite ?c1n0 // -!divpZl e. Qed. -Lemma modp_opp p : (- p) %% d = - (p %% d). -Proof. by rewrite -mulN1r -[RHS]mulN1r -polyC_opp !mul_polyC modp_scalel. Qed. +Lemma modpN p : (- p) %% d = - (p %% d). +Proof. by rewrite -mulN1r -[RHS]mulN1r -polyCN !mul_polyC modpZl. Qed. -Lemma divp_opp p : (- p) %/ d = - (p %/ d). -Proof. by rewrite -mulN1r -[RHS]mulN1r -polyC_opp !mul_polyC divp_scalel. Qed. +Lemma divpN p : (- p) %/ d = - (p %/ d). +Proof. by rewrite -mulN1r -[RHS]mulN1r -polyCN !mul_polyC divpZl. Qed. -Lemma modp_add p q : (p + q) %% d = p %% d + q %% d. +Lemma modpD p q : (p + q) %% d = p %% d + q %% d. Proof. have/edivpP [] // : (p + q) = (p %/ d + q %/ d) * d + (p %% d + q %% d). by rewrite mulrDl addrACA -!divp_eq. @@ -2510,7 +2550,7 @@ rewrite gtn_max !ltn_modp andbb -lead_coef_eq0. by apply: contraTneq ulcd => ->; rewrite unitr0. Qed. -Lemma divp_add p q : (p + q) %/ d = p %/ d + q %/ d. +Lemma divpD p q : (p + q) %/ d = p %/ d + q %/ d. Proof. have/edivpP [] // : (p + q) = (p %/ d + q %/ d) * d + (p %% d + q %% d). by rewrite mulrDl addrACA -!divp_eq. @@ -2527,16 +2567,14 @@ Qed. Lemma mulKp q : (d * q) %/ d = q. Proof. by rewrite mulrC; apply: mulpK. Qed. -Lemma divp_addl_mul_small q r : - size r < size d -> (q * d + r) %/ d = q. -Proof. by move=> srd; rewrite divp_add (divp_small srd) addr0 mulpK. Qed. +Lemma divp_addl_mul_small q r : size r < size d -> (q * d + r) %/ d = q. +Proof. by move=> srd; rewrite divpD (divp_small srd) addr0 mulpK. Qed. -Lemma modp_addl_mul_small q r : - size r < size d -> (q * d + r) %% d = r. -Proof. by move=> srd; rewrite modp_add modp_mull add0r modp_small. Qed. +Lemma modp_addl_mul_small q r : size r < size d -> (q * d + r) %% d = r. +Proof. by move=> srd; rewrite modpD modp_mull add0r modp_small. Qed. Lemma divp_addl_mul q r : (q * d + r) %/ d = q + r %/ d. -Proof. by rewrite divp_add mulpK. Qed. +Proof. by rewrite divpD mulpK. Qed. Lemma divpp : d %/ d = 1. Proof. by rewrite -[d in d %/ _]mul1r mulpK. Qed. @@ -2584,7 +2622,7 @@ Lemma divp_mulCA p q : d %| p -> d %| q -> p * (q %/ d) = q * (p %/ d). Proof. by move=> hdp hdq; rewrite mulrC divp_mulAC // divp_mulA. Qed. Lemma modp_mul p q : (p * (q %% d)) %% d = (p * q) %% d. -Proof. by rewrite [q in RHS]divp_eq mulrDr modp_add mulrA modp_mull add0r. Qed. +Proof. by rewrite [q in RHS]divp_eq mulrDr modpD mulrA modp_mull add0r. Qed. End UnitDivisor. @@ -2644,7 +2682,7 @@ Qed. Lemma divpAC p q : lead_coef p \in GRing.unit -> q %/ d %/ p = q %/ p %/ d. Proof. by move=> ulcp; rewrite !divp_divl // mulrC. Qed. -Lemma modp_scaler c p : c \in GRing.unit -> p %% (c *: d) = (p %% d). +Lemma modpZr c p : c \in GRing.unit -> p %% (c *: d) = (p %% d). Proof. case: (eqVneq d 0) => [-> | dn0 cn0]; first by rewrite scaler0 !modp0. have e : p = (c^-1 *: (p %/ d)) * (c *: d) + (p %% d). @@ -2654,7 +2692,7 @@ suff s : size (p %% d) < size (c *: d). by rewrite size_scale ?ltn_modp //; apply: contraTneq cn0 => ->; rewrite unitr0. Qed. -Lemma divp_scaler c p : c \in GRing.unit -> p %/ (c *: d) = c^-1 *: (p %/ d). +Lemma divpZr c p : c \in GRing.unit -> p %/ (c *: d) = c^-1 *: (p %/ d). Proof. case: (eqVneq d 0) => [-> | dn0 cn0]; first by rewrite scaler0 !divp0 scaler0. have e : p = (c^-1 *: (p %/ d)) * (c *: d) + (p %% d). @@ -2666,6 +2704,31 @@ Qed. End MoreUnitDivisor. +Notation "@ 'modp_scalel'" := + (deprecate modp_scalel modpZl) (at level 10, only parsing) : fun_scope. +Notation "@ 'modp_scaler'" := + (deprecate modp_scaler modpZr) (at level 10, only parsing) : fun_scope. +Notation "@ 'modp_opp'" := + (deprecate modp_opp modpN) (at level 10, only parsing) : fun_scope. +Notation "@ 'modp_add'" := + (deprecate modp_add modpD) (at level 10, only parsing) : fun_scope. +Notation "@ 'divp_scalel'" := + (deprecate divp_scalel divpZl) (at level 10, only parsing) : fun_scope. +Notation "@ 'divp_scaler'" := + (deprecate divp_scaler divpZr) (at level 10, only parsing) : fun_scope. +Notation "@ 'divp_opp'" := + (deprecate divp_opp divpN) (at level 10, only parsing) : fun_scope. +Notation "@ 'divp_add'" := + (deprecate divp_add divpD) (at level 10, only parsing) : fun_scope. +Notation modp_scalel := (@modp_scalel _ _) (only parsing). +Notation modp_scaler := (fun d_unit => @modp_scaler _ _ d_unit _) (only parsing). +Notation modp_opp := (@modp_opp _ _) (only parsing). +Notation modp_add := (@modp_add _ _) (only parsing). +Notation divp_scalel := (@divp_scalel _ _) (only parsing). +Notation divp_scaler := (fun d_unit => @divp_scaler _ _ d_unit _) (only parsing). +Notation divp_opp := (@divp_opp _ _) (only parsing). +Notation divp_add := (@divp_add _ _) (only parsing). + End IdomainUnit. Module Field. @@ -2724,10 +2787,10 @@ case/IdomainUnit.ulc_eqpP; first by rewrite unitfE lead_coef_eq0. by move=> c nz_c ->; exists c. Qed. -Lemma modp_scalel c p q : (c *: p) %% q = c *: (p %% q). +Lemma modpZl c p q : (c *: p) %% q = c *: (p %% q). Proof. have [-> | qn0] := eqVneq q 0; first by rewrite !modp0. -by apply: IdomainUnit.modp_scalel; rewrite unitfE lead_coef_eq0. +by apply: IdomainUnit.modpZl; rewrite unitfE lead_coef_eq0. Qed. Lemma mulpK p q : q != 0 -> p * q %/ q = p. @@ -2736,13 +2799,13 @@ Proof. by move=> qn0; rewrite IdomainUnit.mulpK // unitfE lead_coef_eq0. Qed. Lemma mulKp p q : q != 0 -> q * p %/ q = p. Proof. by rewrite mulrC; apply: mulpK. Qed. -Lemma divp_scalel c p q : (c *: p) %/ q = c *: (p %/ q). +Lemma divpZl c p q : (c *: p) %/ q = c *: (p %/ q). Proof. have [-> | qn0] := eqVneq q 0; first by rewrite !divp0 scaler0. -by apply: IdomainUnit.divp_scalel; rewrite unitfE lead_coef_eq0. +by apply: IdomainUnit.divpZl; rewrite unitfE lead_coef_eq0. Qed. -Lemma modp_scaler c p d : c != 0 -> p %% (c *: d) = (p %% d). +Lemma modpZr c p d : c != 0 -> p %% (c *: d) = (p %% d). Proof. case: (eqVneq d 0) => [-> | dn0 cn0]; first by rewrite scaler0 !modp0. have e : p = (c^-1 *: (p %/ d)) * (c *: d) + (p %% d). @@ -2751,7 +2814,7 @@ suff s : size (p %% d) < size (c *: d) by rewrite (modpP e s). by rewrite size_scale ?ltn_modp. Qed. -Lemma divp_scaler c p d : c != 0 -> p %/ (c *: d) = c^-1 *: (p %/ d). +Lemma divpZr c p d : c != 0 -> p %/ (c *: d) = c^-1 *: (p %/ d). Proof. case: (eqVneq d 0) => [-> | dn0 cn0]; first by rewrite scaler0 !divp0 scaler0. have e : p = (c^-1 *: (p %/ d)) * (c *: d) + (p %% d). @@ -2763,20 +2826,20 @@ Qed. Lemma eqp_modpl d p q : p %= q -> (p %% d) %= (q %% d). Proof. case/eqpP=> [[c1 c2]] /andP /= [c1n0 c2n0 e]. -by apply/eqpP; exists (c1, c2); rewrite ?c1n0 // -!modp_scalel e. +by apply/eqpP; exists (c1, c2); rewrite ?c1n0 // -!modpZl e. Qed. Lemma eqp_divl d p q : p %= q -> (p %/ d) %= (q %/ d). Proof. case/eqpP=> [[c1 c2]] /andP /= [c1n0 c2n0 e]. -by apply/eqpP; exists (c1, c2); rewrite ?c1n0 // -!divp_scalel e. +by apply/eqpP; exists (c1, c2); rewrite ?c1n0 // -!divpZl e. Qed. Lemma eqp_modpr d p q : p %= q -> (d %% p) %= (d %% q). Proof. case/eqpP=> [[c1 c2]] /andP [c1n0 c2n0 e]. have -> : p = (c1^-1 * c2) *: q by rewrite -scalerA -e scalerA mulVf // scale1r. -by rewrite modp_scaler ?eqpxx // mulf_eq0 negb_or invr_eq0 c1n0. +by rewrite modpZr ?eqpxx // mulf_eq0 negb_or invr_eq0 c1n0. Qed. Lemma eqp_mod p1 p2 q1 q2 : p1 %= p2 -> q1 %= q2 -> p1 %% q1 %= p2 %% q2. @@ -2786,7 +2849,7 @@ Lemma eqp_divr (d m n : {poly F}) : m %= n -> (d %/ m) %= (d %/ n). Proof. case/eqpP=> [[c1 c2]] /andP [c1n0 c2n0 e]. have -> : m = (c1^-1 * c2) *: n by rewrite -scalerA -e scalerA mulVf // scale1r. -by rewrite divp_scaler ?eqp_scale // ?invr_eq0 mulf_eq0 negb_or invr_eq0 c1n0. +by rewrite divpZr ?eqp_scale // ?invr_eq0 mulf_eq0 negb_or invr_eq0 c1n0. Qed. Lemma eqp_div p1 p2 q1 q2 : p1 %= p2 -> q1 %= q2 -> p1 %/ q1 %= p2 %/ q2. @@ -2823,37 +2886,37 @@ case: ifP=> // _; apply: ihn => //; apply: eqp_trans (eqp_rdiv_div _ _) _. by apply: eqp_div => //; apply: eqp_trans (eqp_rgcd_gcd _ _) _; apply: eqp_gcd. Qed. -Lemma modp_add d p q : (p + q) %% d = p %% d + q %% d. +Lemma modpD d p q : (p + q) %% d = p %% d + q %% d. Proof. have [-> | dn0] := eqVneq d 0; first by rewrite !modp0. -by apply: IdomainUnit.modp_add; rewrite unitfE lead_coef_eq0. +by apply: IdomainUnit.modpD; rewrite unitfE lead_coef_eq0. Qed. -Lemma modp_opp p q : (- p) %% q = - (p %% q). -Proof. by apply/eqP; rewrite -addr_eq0 -modp_add addNr mod0p. Qed. +Lemma modpN p q : (- p) %% q = - (p %% q). +Proof. by apply/eqP; rewrite -addr_eq0 -modpD addNr mod0p. Qed. -Lemma modNp p q : (- p) %% q = - (p %% q). Proof. exact: modp_opp. Qed. +Lemma modNp p q : (- p) %% q = - (p %% q). Proof. exact: modpN. Qed. -Lemma divp_add d p q : (p + q) %/ d = p %/ d + q %/ d. +Lemma divpD d p q : (p + q) %/ d = p %/ d + q %/ d. Proof. have [-> | dn0] := eqVneq d 0; first by rewrite !divp0 addr0. -by apply: IdomainUnit.divp_add; rewrite unitfE lead_coef_eq0. +by apply: IdomainUnit.divpD; rewrite unitfE lead_coef_eq0. Qed. -Lemma divp_opp p q : (- p) %/ q = - (p %/ q). -Proof. by apply/eqP; rewrite -addr_eq0 -divp_add addNr div0p. Qed. +Lemma divpN p q : (- p) %/ q = - (p %/ q). +Proof. by apply/eqP; rewrite -addr_eq0 -divpD addNr div0p. Qed. Lemma divp_addl_mul_small d q r : size r < size d -> (q * d + r) %/ d = q. Proof. -move=> srd; rewrite divp_add (divp_small srd) addr0 mulpK //. -by rewrite -size_poly_gt0; apply: leq_trans srd. +move=> srd; rewrite divpD (divp_small srd) addr0 mulpK // -size_poly_gt0. +exact: leq_trans srd. Qed. Lemma modp_addl_mul_small d q r : size r < size d -> (q * d + r) %% d = r. -Proof. by move=> srd; rewrite modp_add modp_mull add0r modp_small. Qed. +Proof. by move=> srd; rewrite modpD modp_mull add0r modp_small. Qed. Lemma divp_addl_mul d q r : d != 0 -> (q * d + r) %/ d = q + r %/ d. -Proof. by move=> dn0; rewrite divp_add mulpK. Qed. +Proof. by move=> dn0; rewrite divpD mulpK. Qed. Lemma divpp d : d != 0 -> d %/ d = 1. Proof. @@ -2962,9 +3025,7 @@ by rewrite -size_poly_gt0; apply: leq_trans srd. Qed. Lemma modp_mul p q m : (p * (q %% m)) %% m = (p * q) %% m. -Proof. -by rewrite [in RHS](divp_eq q m) mulrDr modp_add mulrA modp_mull add0r. -Qed. +Proof. by rewrite [in RHS](divp_eq q m) mulrDr modpD mulrA modp_mull add0r. Qed. Lemma dvdpP p q : reflect (exists qq, p = qq * q) (q %| p). Proof. @@ -3131,6 +3192,31 @@ End FieldMap. End FieldDivision. +Notation "@ 'modp_scalel'" := + (deprecate modp_scalel modpZl) (at level 10, only parsing) : fun_scope. +Notation "@ 'modp_scaler'" := + (deprecate modp_scaler modpZr) (at level 10, only parsing) : fun_scope. +Notation "@ 'modp_opp'" := + (deprecate modp_opp modpN) (at level 10, only parsing) : fun_scope. +Notation "@ 'modp_add'" := + (deprecate modp_add modpD) (at level 10, only parsing) : fun_scope. +Notation "@ 'divp_scalel'" := + (deprecate modp_scalel divpZl) (at level 10, only parsing) : fun_scope. +Notation "@ 'divp_scaler'" := + (deprecate modp_scaler divpZr) (at level 10, only parsing) : fun_scope. +Notation "@ 'divp_opp'" := + (deprecate modp_opp divpN) (at level 10, only parsing) : fun_scope. +Notation "@ 'divp_add'" := + (deprecate modp_add divpD) (at level 10, only parsing) : fun_scope. +Notation modp_scalel := (@modp_scalel _) (only parsing). +Notation modp_scaler := (@modp_scaler _ _) (only parsing). +Notation modp_opp := (@modp_opp _) (only parsing). +Notation modp_add := (@modp_add _) (only parsing). +Notation divp_scalel := (@divp_scalel _) (only parsing). +Notation divp_scaler := (@divp_scaler _ _) (only parsing). +Notation divp_opp := (@divp_opp _) (only parsing). +Notation divp_add := (@divp_add _) (only parsing). + End Field. Module ClosedField. diff --git a/mathcomp/algebra/ssralg.v b/mathcomp/algebra/ssralg.v index 5680a24..b449d66 100644 --- a/mathcomp/algebra/ssralg.v +++ b/mathcomp/algebra/ssralg.v @@ -4693,7 +4693,7 @@ Lemma natf_neq0 n : (n%:R != 0 :> R) = [char R]^'.-nat n. Proof. have [-> | /prod_prime_decomp->] := posnP n; first by rewrite eqxx. rewrite !big_seq; elim/big_rec: _ => [|[p e] s /=]; first by rewrite oner_eq0. -case/mem_prime_decomp=> p_pr _ _; rewrite pnat_mul pnat_exp eqn0Ngt orbC => <-. +case/mem_prime_decomp=> p_pr _ _; rewrite pnatM pnatX eqn0Ngt orbC => <-. by rewrite natrM natrX mulf_eq0 expf_eq0 negb_or negb_and pnatE ?inE p_pr. Qed. diff --git a/mathcomp/algebra/ssrint.v b/mathcomp/algebra/ssrint.v index f54a957..6d7899b 100644 --- a/mathcomp/algebra/ssrint.v +++ b/mathcomp/algebra/ssrint.v @@ -1005,24 +1005,17 @@ Lemma expr1z x : x ^ 1 = x. Proof. by []. Qed. Lemma exprN1 x : x ^ (-1) = x^-1. Proof. by []. Qed. Lemma invr_expz x n : (x ^ n)^-1 = x ^ (- n). -Proof. -by case: (intP n)=> // [|m]; rewrite ?opprK ?expr0z ?invr1 // invrK. -Qed. +Proof. by case: (intP n)=> // [|m]; rewrite ?opprK ?expr0z ?invr1 // invrK. Qed. Lemma exprz_inv x n : (x^-1) ^ n = x ^ (- n). -Proof. -by case: (intP n)=> // m; rewrite -[_ ^ (- _)]exprVn ?opprK ?invrK. -Qed. +Proof. by case: (intP n)=> // m; rewrite -[_ ^ (- _)]exprVn ?opprK ?invrK. Qed. Lemma exp1rz n : 1 ^ n = 1 :> R. -Proof. -by case: (intP n)=> // m; rewrite -?exprz_inv ?invr1; apply: expr1n. -Qed. +Proof. by case: (intP n)=> // m; rewrite -?exprz_inv ?invr1; apply: expr1n. Qed. Lemma exprSz x (n : nat) : x ^ n.+1 = x * x ^ n. Proof. exact: exprS. Qed. -Lemma exprSzr x (n : nat) : x ^ n.+1 = x ^ n * x. -Proof. exact: exprSr. Qed. +Lemma exprSzr x (n : nat) : x ^ n.+1 = x ^ n * x. Proof. exact: exprSr. Qed. Fact exprzD_nat x (m n : nat) : x ^ (m%:Z + n) = x ^ m * x ^ n. Proof. exact: exprD. Qed. @@ -1682,7 +1675,7 @@ Proof. wlog le_n21: n1 n2 / n2 <= n1. move=> IH; case/orP: (leq_total n2 n1) => /IH //. by rewrite (addnC (n2 ^ 2)) (mulnC n2) distnC. -by rewrite distnEl ?sqrn_sub ?subnK ?nat_Cauchy. +by rewrite distnEl ?sqrnB ?subnK ?nat_Cauchy. Qed. End Distn. @@ -1718,11 +1711,8 @@ Implicit Types p q r : {poly R}. Lemma coefMrz : forall p n i, (p *~ n)`_i = (p`_i *~ n). Proof. by move=> p [] n i; rewrite ?NegzE (coefMNn, coefMn). Qed. -Lemma polyC_mulrz : forall n, {morph (@polyC R) : c / c *~ n}. -Proof. -move=> [] n c; rewrite ?NegzE -?pmulrn ?polyC_muln //. -by rewrite polyC_opp mulrNz polyC_muln nmulrn. -Qed. +Lemma polyCMz : forall n, {morph (@polyC R) : c / c *~ n}. +Proof. by case/intP => // n c; rewrite ?mulrNz -!pmulrn ?polyCN ?polyCMn. Qed. Lemma hornerMz : forall n (p : {poly R}) x, (p *~ n).[x] = p.[x] *~ n. Proof. by case=> *; rewrite ?NegzE ?mulNzr ?(hornerN, hornerMn). Qed. @@ -1740,7 +1730,7 @@ Section PolyZintOIdom. Variable R : realDomainType. Lemma mulpz (p : {poly R}) (n : int) : p *~ n = n%:~R *: p. -Proof. by rewrite -[p *~ n]mulrzl -mul_polyC polyC_mulrz polyC1. Qed. +Proof. by rewrite -[p *~ n]mulrzl -mul_polyC polyCMz polyC1. Qed. End PolyZintOIdom. @@ -1787,3 +1777,7 @@ Lemma rpredXsign R S (divS : @divrPred R S) (kS : keyed_pred divS) n x : Proof. by rewrite -signr_odd; case: (odd n); rewrite ?rpredV. Qed. End rpred. + +Notation "@ 'polyC_mulrz'" := + (deprecate polyC_mulrz polyCMz) (at level 10, only parsing) : fun_scope. +Notation polyC_mulrz := (@polyC_mulrz _) (only parsing). diff --git a/mathcomp/algebra/vector.v b/mathcomp/algebra/vector.v index 21394bd..462f8ad 100644 --- a/mathcomp/algebra/vector.v +++ b/mathcomp/algebra/vector.v @@ -1491,7 +1491,7 @@ move=> eq_fg; apply/vspaceP=> y. by apply/memv_imgP/memv_imgP=> [][x Vx ->]; exists x; rewrite ?eq_fg. Qed. -Lemma limg_add f : {morph lfun_img f : U V / U + V}%VS. +Lemma limgD f : {morph lfun_img f : U V / U + V}%VS. Proof. move=> U V; apply/eqP; rewrite unlock eqEsubv /subsetv /= -genmx_adds. by rewrite !genmxE !(eqmxMr _ (genmxE _)) !addsmxMr submx_refl. @@ -1499,7 +1499,7 @@ Qed. Lemma limg_sum f I r (P : pred I) Us : (f @: (\sum_(i <- r | P i) Us i) = \sum_(i <- r | P i) f @: Us i)%VS. -Proof. exact: (big_morph _ (limg_add f) (limg0 f)). Qed. +Proof. exact: (big_morph _ (limgD f) (limg0 f)). Qed. Lemma limg_cap f U V : (f @: (U :&: V) <= f @: U :&: f @: V)%VS. Proof. by rewrite subv_cap !limgS ?capvSl ?capvSr. Qed. @@ -1551,7 +1551,7 @@ Proof. by apply: (iffP subvP) => E x /E/eqlfunP. Qed. Lemma limg_ker_compl f U : (f @: (U :\: lker f) = f @: U)%VS. Proof. -rewrite -{2}(addv_diff_cap U (lker f)) limg_add; apply/esym/addv_idPl. +rewrite -{2}(addv_diff_cap U (lker f)) limgD; apply/esym/addv_idPl. by rewrite (subv_trans _ (sub0v _)) // subv0 -lkerE capvSr. Qed. @@ -1701,7 +1701,7 @@ Proof. by move=> sVW; rewrite addvS // limgS // capvS. Qed. Lemma lpreimK f W : (W <= limg f)%VS -> (f @: (f @^-1: W))%VS = W. Proof. -move=> sWf; rewrite limg_add (capv_idPl sWf) // -limg_comp. +move=> sWf; rewrite limgD (capv_idPl sWf) // -limg_comp. have /eqP->: (f @: lker f == 0)%VS by rewrite -lkerE. have /andP[/eqP defW _] := vbasisP W; rewrite addv0 -defW limg_span. rewrite map_id_in // => x Xx; rewrite lfunE /= limg_lfunVK //. @@ -2044,3 +2044,7 @@ by apply/ffunP=> i; rewrite (lfunE (Linear lhsZ)) !ffunE sol_u. Qed. End Solver. + +Notation "@ 'limg_add'" := + (deprecate limg_add limgD) (at level 10, only parsing) : fun_scope. +Notation limg_add := (@limg_add _ _ _) (only parsing). diff --git a/mathcomp/algebra/zmodp.v b/mathcomp/algebra/zmodp.v index 015d971..505fda9 100644 --- a/mathcomp/algebra/zmodp.v +++ b/mathcomp/algebra/zmodp.v @@ -142,7 +142,7 @@ Proof. by move=> Ux; rewrite /= Zp_mulC Zp_mulVz. Qed. Lemma Zp_intro_unit x y : Zp_mul y x = Zp1 -> coprime p x. Proof. case=> yx1; have:= coprimen1 p. -by rewrite -coprime_modr -yx1 coprime_modr coprime_mulr; case/andP. +by rewrite -coprime_modr -yx1 coprime_modr coprimeMr; case/andP. Qed. Lemma Zp_inv_out x : ~~ coprime p x -> Zp_inv x = x. |