diff options
Diffstat (limited to 'mathcomp/ssreflect')
| -rw-r--r-- | mathcomp/ssreflect/bigop.v | 24 | ||||
| -rw-r--r-- | mathcomp/ssreflect/div.v | 27 | ||||
| -rw-r--r-- | mathcomp/ssreflect/fingraph.v | 8 | ||||
| -rw-r--r-- | mathcomp/ssreflect/finset.v | 10 | ||||
| -rw-r--r-- | mathcomp/ssreflect/fintype.v | 13 | ||||
| -rw-r--r-- | mathcomp/ssreflect/path.v | 4 | ||||
| -rw-r--r-- | mathcomp/ssreflect/prime.v | 60 | ||||
| -rw-r--r-- | mathcomp/ssreflect/seq.v | 16 | ||||
| -rw-r--r-- | mathcomp/ssreflect/ssrnat.v | 46 |
9 files changed, 127 insertions, 81 deletions
diff --git a/mathcomp/ssreflect/bigop.v b/mathcomp/ssreflect/bigop.v index 4cf0cef..e8293ae 100644 --- a/mathcomp/ssreflect/bigop.v +++ b/mathcomp/ssreflect/bigop.v @@ -443,14 +443,21 @@ Lemma addmCA : left_commutative add. Proof. exact: mulmCA. Qed. Lemma addmAC : right_commutative add. Proof. exact: mulmAC. Qed. Lemma add0m : left_id idm add. Proof. exact: mul1m. Qed. Lemma addm0 : right_id idm add. Proof. exact: mulm1. Qed. -Lemma mulm_addl : left_distributive mul add. Proof. by case add. Qed. -Lemma mulm_addr : right_distributive mul add. Proof. by case add. Qed. +Lemma mulmDl : left_distributive mul add. Proof. by case add. Qed. +Lemma mulmDr : right_distributive mul add. Proof. by case add. Qed. End Add. Definition simpm := (mulm1, mulm0, mul1m, mul0m, mulmA). End Theory. +Notation "@ 'mulm_addl'" := + (deprecate mulm_addl mulmDl) (at level 10, only parsing) : fun_scope. +Notation "@ 'mulm_addr'" := + (deprecate mulm_addr mulmDr) (at level 10, only parsing) : fun_scope. +Notation mulm_addl := (@mulm_addl _ _ _) (only parsing). +Notation mulm_addr := (@mulm_addr _ _ _) (only parsing). + End Theory. Include Theory. @@ -483,7 +490,7 @@ Canonical addn_addoid := AddLaw mulnDl mulnDr. Canonical maxn_monoid := Law maxnA max0n maxn0. Canonical maxn_comoid := ComLaw maxnC. -Canonical maxn_addoid := AddLaw maxn_mull maxn_mulr. +Canonical maxn_addoid := AddLaw maxnMl maxnMr. Canonical gcdn_monoid := Law gcdnA gcd0n gcdn0. Canonical gcdn_comoid := ComLaw gcdnC. @@ -954,7 +961,7 @@ Lemma big_addn m n a (P : pred nat) F : \big[op/idx]_(m + a <= i < n | P i) F i = \big[op/idx]_(m <= i < n - a | P (i + a)) F (i + a). Proof. -rewrite /index_iota -subnDA addnC iota_addl big_map. +rewrite /index_iota -subnDA addnC iotaDl big_map. by apply: eq_big => ? *; rewrite addnC. Qed. @@ -1277,7 +1284,7 @@ Lemma big_cat_nat n m p (P : pred nat) F : m <= n -> n <= p -> \big[*%M/1]_(m <= i < p | P i) F i = (\big[*%M/1]_(m <= i < n | P i) F i) * (\big[*%M/1]_(n <= i < p | P i) F i). Proof. -move=> le_mn le_np; rewrite -big_cat -{2}(subnKC le_mn) -iota_add subnDA. +move=> le_mn le_np; rewrite -big_cat -{2}(subnKC le_mn) -iotaD subnDA. by rewrite subnKC // leq_sub. Qed. @@ -1315,8 +1322,7 @@ Proof. rewrite -(big_map _ _ (lshift n) _ P F) -(big_map _ _ (@rshift m _) _ P F). rewrite -big_cat; congr bigop; apply: (inj_map val_inj). rewrite map_cat -!map_comp (map_comp (addn m)) /=. -rewrite ![index_enum _]unlock unlock !val_ord_enum. -by rewrite -iota_addl addn0 iota_add. +by rewrite ![index_enum _]unlock unlock !val_ord_enum -iotaDl addn0 iotaD. Qed. Lemma big_flatten I rr (P : pred I) F : @@ -1739,11 +1745,11 @@ Local Notation "x + y" := (plus x y). Lemma big_distrl I r a (P : pred I) F : \big[+%M/0]_(i <- r | P i) F i * a = \big[+%M/0]_(i <- r | P i) (F i * a). -Proof. by rewrite (big_endo ( *%M^~ a)) ?mul0m // => x y; apply: mulm_addl. Qed. +Proof. by rewrite (big_endo ( *%M^~ a)) ?mul0m // => x y; apply: mulmDl. Qed. Lemma big_distrr I r a (P : pred I) F : a * \big[+%M/0]_(i <- r | P i) F i = \big[+%M/0]_(i <- r | P i) (a * F i). -Proof. by rewrite big_endo ?mulm0 // => x y; apply: mulm_addr. Qed. +Proof. by rewrite big_endo ?mulm0 // => x y; apply: mulmDr. Qed. Lemma big_distrlr I J rI rJ (pI : pred I) (pJ : pred J) F G : (\big[+%M/0]_(i <- rI | pI i) F i) * (\big[+%M/0]_(j <- rJ | pJ j) G j) diff --git a/mathcomp/ssreflect/div.v b/mathcomp/ssreflect/div.v index 17e3ac4..4899ee3 100644 --- a/mathcomp/ssreflect/div.v +++ b/mathcomp/ssreflect/div.v @@ -326,7 +326,7 @@ Proof. by rewrite [in RHS](divn_eq m 2) modn2 muln2 addnC half_bit_double. Qed. Lemma odd_mod m d : odd d = false -> odd (m %% d) = odd m. Proof. -by move=> d_even; rewrite [in RHS](divn_eq m d) oddD odd_mul d_even andbF. +by move=> d_even; rewrite [in RHS](divn_eq m d) oddD oddM d_even andbF. Qed. Lemma modnXm m n a : (a %% n) ^ m = a ^ m %[mod n]. @@ -937,33 +937,33 @@ Qed. Lemma Gauss_gcdl p m n : coprime p n -> gcdn p (m * n) = gcdn p m. Proof. by move=> co_pn; rewrite mulnC Gauss_gcdr. Qed. -Lemma coprime_mulr p m n : coprime p (m * n) = coprime p m && coprime p n. +Lemma coprimeMr p m n : coprime p (m * n) = coprime p m && coprime p n. Proof. case co_pm: (coprime p m) => /=; first by rewrite /coprime Gauss_gcdr. apply/eqP=> co_p_mn; case/eqnP: co_pm; apply gcdn_def => // d dv_dp dv_dm. by rewrite -co_p_mn dvdn_gcd dv_dp dvdn_mulr. Qed. -Lemma coprime_mull p m n : coprime (m * n) p = coprime m p && coprime n p. -Proof. by rewrite -!(coprime_sym p) coprime_mulr. Qed. +Lemma coprimeMl p m n : coprime (m * n) p = coprime m p && coprime n p. +Proof. by rewrite -!(coprime_sym p) coprimeMr. Qed. Lemma coprime_pexpl k m n : 0 < k -> coprime (m ^ k) n = coprime m n. Proof. case: k => // k _; elim: k => [|k IHk]; first by rewrite expn1. -by rewrite expnS coprime_mull -IHk; case coprime. +by rewrite expnS coprimeMl -IHk; case coprime. Qed. Lemma coprime_pexpr k m n : 0 < k -> coprime m (n ^ k) = coprime m n. Proof. by move=> k_gt0; rewrite !(coprime_sym m) coprime_pexpl. Qed. -Lemma coprime_expl k m n : coprime m n -> coprime (m ^ k) n. +Lemma coprimeXl k m n : coprime m n -> coprime (m ^ k) n. Proof. by case: k => [|k] co_pm; rewrite ?coprime1n // coprime_pexpl. Qed. -Lemma coprime_expr k m n : coprime m n -> coprime m (n ^ k). -Proof. by rewrite !(coprime_sym m); apply: coprime_expl. Qed. +Lemma coprimeXr k m n : coprime m n -> coprime m (n ^ k). +Proof. by rewrite !(coprime_sym m); apply: coprimeXl. Qed. Lemma coprime_dvdl m n p : m %| n -> coprime n p -> coprime m p. -Proof. by case/dvdnP=> d ->; rewrite coprime_mull => /andP[]. Qed. +Proof. by case/dvdnP=> d ->; rewrite coprimeMl => /andP[]. Qed. Lemma coprime_dvdr m n p : m %| n -> coprime p n -> coprime p m. Proof. by rewrite !(coprime_sym p); apply: coprime_dvdl. Qed. @@ -1040,3 +1040,12 @@ by rewrite chinese_modl chinese_modr !modn_mod !eqxx. Qed. End Chinese. + +Notation "@ 'coprime_expl'" := + (deprecate coprime_expl coprimeXl) (at level 10, only parsing) : fun_scope. +Notation "@ 'coprime_expr'" := + (deprecate coprime_expr coprimeXr) (at level 10, only parsing) : fun_scope. +Notation coprime_mull := (deprecate coprime_mull coprimeMl) (only parsing). +Notation coprime_mulr := (deprecate coprime_mulr coprimeMr) (only parsing). +Notation coprime_expl := (fun k => @coprime_expl k _ _) (only parsing). +Notation coprime_expr := (fun k => @coprime_expr k _ _) (only parsing). diff --git a/mathcomp/ssreflect/fingraph.v b/mathcomp/ssreflect/fingraph.v index b77d1a8..5c933cf 100644 --- a/mathcomp/ssreflect/fingraph.v +++ b/mathcomp/ssreflect/fingraph.v @@ -499,8 +499,8 @@ Lemma iter_finv_in n : {in S, forall x, n <= order x -> iter n finv x = iter (order x - n) f x}. Proof. move=> x xS; rewrite -[x in LHS]iter_order_in => // /subnKC {1}<-. -move: (_ - n) => m; rewrite iter_add; elim: n => // n {2}<-. -by rewrite iterSr /= finv_f_in // -iter_add iter_in. +move: (_ - n) => m; rewrite iterD; elim: n => // n {2}<-. +by rewrite iterSr /= finv_f_in // -iterD iter_in. Qed. Lemma cycle_orbit_in : {in S, forall x, (fcycle f) (orbit x)}. @@ -810,8 +810,8 @@ tfae=> [xorbit_cycle|||[k fkx]|fx y z|/injectivePcycle//]. - apply: (@iter_order_cycle (traject f x k.+1)); rewrite /= ?mem_head//. by apply/fpathP; exists k.+1; rewrite trajectSr -iterSr fkx. - rewrite -!fconnect_orbit => /iter_findex <- /iter_findex <-. - move=> /(congr1 (iter (order x).-1 f)); rewrite -!iterSr !orderSpred. - by rewrite -!iter_add ![order _ + _]addnC !iter_add fx. + move/(congr1 (iter (order x).-1 f)). + by rewrite -!iterSr !orderSpred -!iterD ![order _ + _]addnC !iterD fx. Qed. Lemma order_id_cycle x : fcycle f (orbit x) -> order (f x) = order x. diff --git a/mathcomp/ssreflect/finset.v b/mathcomp/ssreflect/finset.v index 4a3eaf1..5b6e4d0 100644 --- a/mathcomp/ssreflect/finset.v +++ b/mathcomp/ssreflect/finset.v @@ -2289,7 +2289,7 @@ Definition fixset := iterF n. Lemma fixsetK : F fixset = fixset. Proof. suff /'exists_eqP[x /= e]: [exists k : 'I_n.+1, iterF k == iterF k.+1]. - by rewrite /fixset -(subnK (leq_ord x)) /iterF iter_add iter_fix. + by rewrite /fixset -(subnK (leq_ord x)) /iterF iterD iter_fix. apply: contraT => /existsPn /(_ (Ordinal _)) /= neq_iter. suff iter_big k : k <= n.+1 -> k <= #|iter k F set0|. by have := iter_big _ (leqnn _); rewrite ltnNge max_card. @@ -2312,7 +2312,7 @@ Proof. by rewrite iter_fix. Qed. Lemma iter_sub_fix k : iterF k \subset fixset. Proof. have [/subset_iter //|/ltnW/subnK<-] := leqP k n; -by rewrite /iterF iter_add fixsetKn. +by rewrite /iterF iterD fixsetKn. Qed. Lemma fix_order_proof x : x \in fixset -> exists n, x \in iterF n. @@ -2396,6 +2396,8 @@ End Greatest. End SetFixpoint. Notation mem_imset := - ((fun aT rT D x f xD => deprecate mem_imset imset_f aT rT f D x xD) _ _ _ _). + ((fun aT rT D x f xD => deprecate mem_imset imset_f aT rT f D x xD) _ _ _ _) + (only parsing). Notation mem_imset2 := ((fun aT aT2 rT D D2 x x2 f xD xD2 => - deprecate mem_imset2 imset2_f aT aT2 rT f D D2 x x2 xD xD2) _ _ _ _ _ _ _). + deprecate mem_imset2 imset2_f aT aT2 rT f D D2 x x2 xD xD2) _ _ _ _ _ _ _) + (only parsing). diff --git a/mathcomp/ssreflect/fintype.v b/mathcomp/ssreflect/fintype.v index 726b8c2..422d760 100644 --- a/mathcomp/ssreflect/fintype.v +++ b/mathcomp/ssreflect/fintype.v @@ -2041,20 +2041,20 @@ Qed. Lemma unbumpK {h} : {in predC1 h, cancel (unbump h) (bump h)}. Proof. by move=> i /negbTE-neq_h_i; rewrite unbumpKcond neq_h_i. Qed. -Lemma bump_addl h i k : bump (k + h) (k + i) = k + bump h i. +Lemma bumpDl h i k : bump (k + h) (k + i) = k + bump h i. Proof. by rewrite /bump leq_add2l addnCA. Qed. Lemma bumpS h i : bump h.+1 i.+1 = (bump h i).+1. Proof. exact: addnS. Qed. -Lemma unbump_addl h i k : unbump (k + h) (k + i) = k + unbump h i. +Lemma unbumpDl h i k : unbump (k + h) (k + i) = k + unbump h i. Proof. apply: (can_inj (bumpK (k + h))). -by rewrite bump_addl !unbumpKcond eqn_add2l addnCA. +by rewrite bumpDl !unbumpKcond eqn_add2l addnCA. Qed. Lemma unbumpS h i : unbump h.+1 i.+1 = (unbump h i).+1. -Proof. exact: unbump_addl 1. Qed. +Proof. exact: unbumpDl 1. Qed. Lemma leq_bump h i j : (i <= bump h j) = (unbump h i <= j). Proof. @@ -2238,7 +2238,7 @@ Proof. by rewrite /inord /insubd valK. Qed. Lemma enum_ordS : enum 'I_n = ord0 :: map (lift ord0) (enum 'I_n'). Proof. apply: (inj_map val_inj); rewrite val_enum_ord /= -map_comp. -by rewrite (map_comp (addn 1)) val_enum_ord -iota_addl. +by rewrite (map_comp (addn 1)) val_enum_ord -iotaDl. Qed. Lemma lift_max (i : 'I_n') : lift ord_max i = i :> nat. @@ -2345,3 +2345,6 @@ Lemma card_sum : #|{: T1 + T2}| = #|T1| + #|T2|. Proof. by rewrite !cardT !enumT [in LHS]unlock size_cat !size_map. Qed. End SumFinType. + +Notation bump_addl := (deprecate bump_addl bumpDl) (only parsing). +Notation unbump_addl := (deprecate unbump_addl unbumpDl) (only parsing). diff --git a/mathcomp/ssreflect/path.v b/mathcomp/ssreflect/path.v index 7d1f0e9..0965b14 100644 --- a/mathcomp/ssreflect/path.v +++ b/mathcomp/ssreflect/path.v @@ -865,7 +865,7 @@ apply: ihss. rewrite (perm_mem perm_s2) mem_iota => /andP [] _ hy'. apply/allP => n; rewrite (perm_mem perm_s1) mem_iota => /andP []. by rewrite -cat_cons size_cat addnC => /(leq_trans hy'). -- rewrite /= perm_ss andbT perm_merge size_merge size_cat iota_add perm_cat //. +- rewrite /= perm_ss andbT perm_merge size_merge size_cat iotaD perm_cat //. by rewrite addnC -size_cat. Qed. @@ -880,7 +880,7 @@ apply: ihss => /=. apply/allP => m'; rewrite (perm_mem perm_s2) mem_iota => /andP [_ hm']. apply/allP => n; rewrite (perm_mem perm_s1) mem_iota -cat_cons size_cat. by rewrite addnC => /andP [] /(leq_trans hm'). -- rewrite perm_ss andbT perm_merge size_merge size_cat iota_add perm_cat //. +- rewrite perm_ss andbT perm_merge size_merge size_cat iotaD perm_cat //. by rewrite addnC -size_cat. Qed. diff --git a/mathcomp/ssreflect/prime.v b/mathcomp/ssreflect/prime.v index 2f35e35..8e94ef6 100644 --- a/mathcomp/ssreflect/prime.v +++ b/mathcomp/ssreflect/prime.v @@ -269,8 +269,8 @@ case def_d: d if_d0 => [|d'] => [[//|{def_m ltdp pr_p} def_m pr_p pr_m'] | _]. rewrite -addnA -doubleD addnCA def_a addSnnS def_k1 -(addnC k) -mulnSr. by rewrite -[_.*2.+1]/p mulnDl doubleD addnA -mul2n mulnA mul2n -mulSn. have next_pm: lb_dvd p.+2 m. - rewrite /lb_dvd /index_iota 2!subSS subn0 -(subnK lt1p) iota_add. - rewrite has_cat; apply/norP; split=> //=; rewrite orbF subnKC // orbC. + rewrite /lb_dvd /index_iota (addKn 2) -(subnK lt1p) iotaD has_cat. + apply/norP; split; rewrite //= orbF subnKC // orbC. apply/norP; split; apply/dvdnP=> [[q def_q]]. case/hasP: leppm; exists 2; first by rewrite /p -(subnKC lt0k). by rewrite /= def_q dvdn_mull // dvdn2 /= odd_double. @@ -549,18 +549,18 @@ Arguments primePns {n}. Lemma pdivP n : n > 1 -> {p | prime p & p %| n}. Proof. by move=> lt1n; exists (pdiv n); rewrite ?pdiv_dvd ?pdiv_prime. Qed. -Lemma primes_mul m n p : m > 0 -> n > 0 -> +Lemma primesM m n p : m > 0 -> n > 0 -> (p \in primes (m * n)) = (p \in primes m) || (p \in primes n). Proof. move=> m_gt0 n_gt0; rewrite !mem_primes muln_gt0 m_gt0 n_gt0. by case pr_p: (prime p); rewrite // Euclid_dvdM. Qed. -Lemma primes_exp m n : n > 0 -> primes (m ^ n) = primes m. +Lemma primesX m n : n > 0 -> primes (m ^ n) = primes m. Proof. case: n => // n _; rewrite expnS; have [-> // | m_gt0] := posnP m. apply/eq_primes => /= p; elim: n => [|n IHn]; first by rewrite muln1. -by rewrite primes_mul ?(expn_gt0, expnS, IHn, orbb, m_gt0). +by rewrite primesM ?(expn_gt0, expnS, IHn, orbb, m_gt0). Qed. Lemma primes_prime p : prime p -> primes p = [::p]. @@ -588,7 +588,7 @@ Lemma pdiv_id p : prime p -> pdiv p = p. Proof. by move=> p_pr; rewrite /pdiv primes_prime. Qed. Lemma pdiv_pfactor p k : prime p -> pdiv (p ^ k.+1) = p. -Proof. by move=> p_pr; rewrite /pdiv primes_exp ?primes_prime. Qed. +Proof. by move=> p_pr; rewrite /pdiv primesX ?primes_prime. Qed. (* Primes are unbounded. *) @@ -707,7 +707,7 @@ have [m0 | m_gt0] := posnP m; first by rewrite m0 prime_coprime ?dvdn0 in co_pm. have mn_gt0: m * n > 0 by rewrite muln_gt0 m_gt0. apply/eqP; rewrite eqn_leq andbC dvdn_leq_log ?dvdn_mull //. set k := logn p _; have: p ^ k %| m * n by rewrite pfactor_dvdn. -by rewrite Gauss_dvdr ?coprime_expl // -pfactor_dvdn. +by rewrite Gauss_dvdr ?coprimeXl // -pfactor_dvdn. Qed. Lemma logn_coprime p m : coprime p m -> logn p m = 0. @@ -747,7 +747,7 @@ exists (logn p d); first by rewrite -(pfactorK n p_pr) dvdn_leq_log. have d_gt0: d > 0 by apply: dvdn_gt0 dv_d_pn. case: (pfactor_coprime p_pr d_gt0) => q co_p_q def_d. rewrite [LHS]def_d ((q =P 1) _) ?mul1n // -dvdn1. -suff: q %| p ^ n * 1 by rewrite Gauss_dvdr // coprime_sym coprime_expl. +suff: q %| p ^ n * 1 by rewrite Gauss_dvdr // coprime_sym coprimeXl. by rewrite muln1 (dvdn_trans _ dv_d_pn) // def_d dvdn_mulr. Qed. @@ -762,7 +762,7 @@ case/mem_prime_decomp=> pr_p _ _. rewrite (big_nth f0) big_mkord (bigD1 (Ordinal lt_i_n)) //=. rewrite def_f mulnC logn_Gauss ?pfactorK //. apply big_ind => [|m1 m2 com1 com2| [j ltj] /=]; first exact: coprimen1. - by rewrite coprime_mulr com1. + by rewrite coprimeMr com1. rewrite -val_eqE /= => nji; case def_j: (nth _ _ j) => [q e1] /=. have: (q, e1) \in prime_decomp n.+1 by rewrite -def_j mem_nth. case/mem_prime_decomp=> pr_q e1_gt0 _; rewrite coprime_pexpr //. @@ -1092,17 +1092,17 @@ Proof. exact: eq_pnat (negnK pi). Qed. Lemma pnatI pi rho n : [predI pi & rho].-nat n = pi.-nat n && rho.-nat n. Proof. by rewrite /pnat andbCA all_predI !andbA andbb. Qed. -Lemma pnat_mul pi m n : pi.-nat (m * n) = pi.-nat m && pi.-nat n. +Lemma pnatM pi m n : pi.-nat (m * n) = pi.-nat m && pi.-nat n. Proof. rewrite /pnat muln_gt0 andbCA -andbA andbCA. case: posnP => // n_gt0; case: posnP => //= m_gt0. apply/allP/andP=> [pi_mn | [pi_m pi_n] p]. - by split; apply/allP=> p m_p; apply: pi_mn; rewrite primes_mul // m_p ?orbT. -by rewrite primes_mul // => /orP[]; [apply: (allP pi_m) | apply: (allP pi_n)]. + by split; apply/allP=> p m_p; apply: pi_mn; rewrite primesM // m_p ?orbT. +by rewrite primesM // => /orP[]; [apply: (allP pi_m) | apply: (allP pi_n)]. Qed. -Lemma pnat_exp pi m n : pi.-nat (m ^ n) = pi.-nat m || (n == 0). -Proof. by case: n => [|n]; rewrite orbC // /pnat expn_gt0 orbC primes_exp. Qed. +Lemma pnatX pi m n : pi.-nat (m ^ n) = pi.-nat m || (n == 0). +Proof. by case: n => [|n]; rewrite orbC // /pnat expn_gt0 orbC primesX. Qed. Lemma part_pnat pi n : pi.-nat n`_pi. Proof. @@ -1131,13 +1131,13 @@ exact: dvdn_trans p_dv_m m_dv_n. Qed. Lemma pi_ofM m n : m > 0 -> n > 0 -> \pi(m * n) =i [predU \pi(m) & \pi(n)]. -Proof. by move=> m_gt0 n_gt0 p; apply: primes_mul. Qed. +Proof. by move=> m_gt0 n_gt0 p; apply: primesM. Qed. Lemma pi_of_part pi n : n > 0 -> \pi(n`_pi) =i [predI \pi(n) & pi]. Proof. by move=> n_gt0 p; rewrite /pi_of primes_part mem_filter andbC. Qed. Lemma pi_of_exp p n : n > 0 -> \pi(p ^ n) = \pi(p). -Proof. by move=> n_gt0; rewrite /pi_of primes_exp. Qed. +Proof. by move=> n_gt0; rewrite /pi_of primesX. Qed. Lemma pi_of_prime p : prime p -> \pi(p) =i (p : nat_pred). Proof. by move=> pr_p q; rewrite /pi_of primes_prime // mem_seq1. Qed. @@ -1155,11 +1155,11 @@ Lemma pnatPpi pi n p : pi.-nat n -> p \in \pi(n) -> p \in pi. Proof. by case/andP=> _ /allP; apply. Qed. Lemma pnat_dvd m n pi : m %| n -> pi.-nat n -> pi.-nat m. -Proof. by case/dvdnP=> q ->; rewrite pnat_mul; case/andP. Qed. +Proof. by case/dvdnP=> q ->; rewrite pnatM; case/andP. Qed. Lemma pnat_div m n pi : m %| n -> pi.-nat n -> pi.-nat (n %/ m). Proof. -case/dvdnP=> q ->; rewrite pnat_mul andbC => /andP[]. +case/dvdnP=> q ->; rewrite pnatM andbC => /andP[]. by case: m => // m _; rewrite mulnK. Qed. @@ -1295,7 +1295,7 @@ rewrite mem_merge mem_cat; case dv_d_p: (p %| d). case pdiv_d: (_ \in _). by case/mapP: pdiv_d dv_d_p => d' _ ->; rewrite natTrecE dvdn_mulr. rewrite mem_divs Gauss_dvdr // coprime_sym. -by rewrite coprime_expl ?prime_coprime ?dv_d_p. +by rewrite coprimeXl ?prime_coprime ?dv_d_p. Qed. Lemma sorted_divisors n : sorted leq (divisors n). @@ -1365,7 +1365,7 @@ Lemma totient_pfactor p e : prime p -> e > 0 -> totient (p ^ e) = p.-1 * p ^ e.-1. Proof. move=> p_pr e_gt0; rewrite totientE ?expn_gt0 ?prime_gt0 //. -by rewrite primes_exp // primes_prime // unlock /= muln1 pfactorK. +by rewrite primesX // primes_prime // unlock /= muln1 pfactorK. Qed. Lemma totient_prime p : prime p -> totient p = p.-1. @@ -1380,13 +1380,13 @@ rewrite !totientE ?muln_gt0 ?m_gt0 //. have /(perm_big _)->: perm_eq (primes (m * n)) (primes m ++ primes n). apply: uniq_perm => [||p]; first exact: primes_uniq. by rewrite cat_uniq !primes_uniq -coprime_has_primes // co_mn. - by rewrite mem_cat primes_mul. + by rewrite mem_cat primesM. rewrite big_cat /= !big_seq. congr (_ * _); apply: eq_bigr => p; rewrite mem_primes => /and3P[_ _ dvp]. rewrite (mulnC m) logn_Gauss //; move: co_mn. - by rewrite -(divnK dvp) coprime_mull => /andP[]. + by rewrite -(divnK dvp) coprimeMl => /andP[]. rewrite logn_Gauss //; move: co_mn. -by rewrite coprime_sym -(divnK dvp) coprime_mull => /andP[]. +by rewrite coprime_sym -(divnK dvp) coprimeMl => /andP[]. Qed. Lemma totient_count_coprime n : totient n = \sum_(0 <= d < n) coprime n d. @@ -1422,9 +1422,17 @@ have ->: totient np = #|[pred d : 'I_np | coprime np d]|. pose h (d : 'I_n) := (in_mod _ np0 d, in_mod _ np'0 d). pose h' (d : 'I_np * 'I_np') := in_mod _ n0 (chinese np np' d.1 d.2). rewrite -!big_mkcond -sum_nat_const pair_big (reindex_onto h h') => [|[d d'] _]. - apply: eq_bigl => [[d ltd] /=]; rewrite !inE /= -val_eqE /= andbC. - rewrite !coprime_modr def_n -chinese_mod // -coprime_mull -def_n. - by rewrite modn_small ?eqxx. + apply: eq_bigl => [[d ltd] /=]; rewrite !inE -val_eqE /= andbC !coprime_modr. + by rewrite def_n -chinese_mod // -coprimeMl -def_n modn_small ?eqxx. apply/eqP; rewrite /eq_op /= /eq_op /= !modn_dvdm ?dvdn_part //. by rewrite chinese_modl // chinese_modr // !modn_small ?eqxx ?ltn_ord. Qed. + +Notation "@ 'primes_mul'" := + (deprecate primes_mul primesM) (at level 10, only parsing) : fun_scope. +Notation "@ 'primes_exp'" := + (deprecate primes_exp primesX) (at level 10, only parsing) : fun_scope. +Notation primes_mul := (@primes_mul _ _) (only parsing). +Notation primes_exp := (fun m => @primes_exp m _) (only parsing). +Notation pnat_mul := (deprecate pnat_mul pnatM) (only parsing). +Notation pnat_exp := (deprecate pnat_exp pnatX) (only parsing). diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v index 15f9421..7cdc422 100644 --- a/mathcomp/ssreflect/seq.v +++ b/mathcomp/ssreflect/seq.v @@ -284,9 +284,8 @@ Lemma cat_cons x s1 s2 : (x :: s1) ++ s2 = x :: s1 ++ s2. Proof. by []. Qed. Lemma cat_nseq n x s : nseq n x ++ s = ncons n x s. Proof. by elim: n => //= n ->. Qed. -Lemma nseqD n1 n2 x : - nseq (n1 + n2) x = nseq n1 x ++ nseq n2 x. -Proof. by rewrite cat_nseq /nseq /ncons iter_add. Qed. +Lemma nseqD n1 n2 x : nseq (n1 + n2) x = nseq n1 x ++ nseq n2 x. +Proof. by rewrite cat_nseq /nseq /ncons iterD. Qed. Lemma cats0 s : s ++ [::] = s. Proof. by elim: s => //= x s ->. Qed. @@ -2504,15 +2503,15 @@ Fixpoint iota m n := if n is n'.+1 then m :: iota m.+1 n' else [::]. Lemma size_iota m n : size (iota m n) = n. Proof. by elim: n m => //= n IHn m; rewrite IHn. Qed. -Lemma iota_add m n1 n2 : iota m (n1 + n2) = iota m n1 ++ iota (m + n1) n2. +Lemma iotaD m n1 n2 : iota m (n1 + n2) = iota m n1 ++ iota (m + n1) n2. Proof. by elim: n1 m => [|n1 IHn1] m; rewrite ?addn0 // -addSnnS /= -IHn1. Qed. -Lemma iota_addl m1 m2 n : iota (m1 + m2) n = map (addn m1) (iota m2 n). +Lemma iotaDl m1 m2 n : iota (m1 + m2) n = map (addn m1) (iota m2 n). Proof. by elim: n m2 => //= n IHn m2; rewrite -addnS IHn. Qed. Lemma nth_iota p m n i : i < n -> nth p (iota m n) i = m + i. Proof. -by move/subnKC <-; rewrite addSnnS iota_add nth_cat size_iota ltnn subnn. +by move/subnKC <-; rewrite addSnnS iotaD nth_cat size_iota ltnn subnn. Qed. Lemma mem_iota m n i : (i \in iota m n) = (m <= i < m + n). @@ -2583,7 +2582,7 @@ elim: t => [|x t IHt] in s It Est *. have /rot_to[k s1 Ds]: x \in s by rewrite (perm_mem Est) mem_head. have [|Is1 eqIst1 Ds1] := IHt s1; first by rewrite -(perm_cons x) -Ds perm_rot. exists (rotr k (0 :: map succn Is1)). - by rewrite perm_rot /It /= perm_cons (iota_addl 1) perm_map. + by rewrite perm_rot /It /= perm_cons (iotaDl 1) perm_map. by rewrite map_rotr /= -map_comp -(@eq_map _ _ (nth x0 t)) // -Ds1 -Ds rotK. Qed. @@ -3581,3 +3580,6 @@ Notation uniq_perm_eq := (deprecate uniq_perm_eq uniq_perm _ _ _) Notation perm_eq_iotaP := (deprecate perm_eq_iotaP perm_iotaP) (only parsing). Notation perm_undup_count := (deprecate perm_undup_count perm_count_undup _ _) (only parsing). + +Notation iota_add := (deprecate iota_add iotaD) (only parsing). +Notation iota_addl := (deprecate iota_addl iotaDl) (only parsing). diff --git a/mathcomp/ssreflect/ssrnat.v b/mathcomp/ssreflect/ssrnat.v index 8b88821..9f17eb9 100644 --- a/mathcomp/ssreflect/ssrnat.v +++ b/mathcomp/ssreflect/ssrnat.v @@ -939,7 +939,7 @@ Proof. by elim: n => //= n <-. Qed. Lemma iterS n f x : iter n.+1 f x = f (iter n f x). Proof. by []. Qed. -Lemma iter_add n m f x : iter (n + m) f x = iter n f (iter m f x). +Lemma iterD n m f x : iter (n + m) f x = iter n f (iter m f x). Proof. by elim: n => //= n ->. Qed. Lemma iteriS n f x : iteri n.+1 f x = f n (iteri n f x). @@ -1114,17 +1114,17 @@ move=> lt_mn1 lt_mn2; apply (@leq_ltn_trans (m1 * n2)). by rewrite ltn_pmul2r // (leq_trans _ lt_mn2). Qed. -Lemma maxn_mulr : right_distributive muln maxn. +Lemma maxnMr : right_distributive muln maxn. Proof. by case=> // m n1 n2; rewrite /maxn (fun_if (muln _)) ltn_pmul2l. Qed. -Lemma maxn_mull : left_distributive muln maxn. -Proof. by move=> m1 m2 n; rewrite -!(mulnC n) maxn_mulr. Qed. +Lemma maxnMl : left_distributive muln maxn. +Proof. by move=> m1 m2 n; rewrite -!(mulnC n) maxnMr. Qed. -Lemma minn_mulr : right_distributive muln minn. +Lemma minnMr : right_distributive muln minn. Proof. by case=> // m n1 n2; rewrite /minn (fun_if (muln _)) ltn_pmul2l. Qed. -Lemma minn_mull : left_distributive muln minn. -Proof. by move=> m1 m2 n; rewrite -!(mulnC n) minn_mulr. Qed. +Lemma minnMl : left_distributive muln minn. +Proof. by move=> m1 m2 n; rewrite -!(mulnC n) minnMr. Qed. (* Exponentiation. *) @@ -1276,14 +1276,14 @@ Proof. by move=> le_nm; apply: (@canRL bool) (addbK _) _; rewrite -oddD subnK. Qed. -Lemma odd_opp i m : odd m = false -> i <= m -> odd (m - i) = odd i. -Proof. by move=> oddm le_im; rewrite (oddB (le_im)) oddm. Qed. +Lemma oddN i m : odd m = false -> i <= m -> odd (m - i) = odd i. +Proof. by move=> oddm /oddB ->; rewrite oddm. Qed. -Lemma odd_mul m n : odd (m * n) = odd m && odd n. +Lemma oddM m n : odd (m * n) = odd m && odd n. Proof. by elim: m => //= m IHm; rewrite oddD -addTb andb_addl -IHm. Qed. -Lemma odd_exp m n : odd (m ^ n) = (n == 0) || odd m. -Proof. by elim: n => // n IHn; rewrite expnS odd_mul {}IHn orbC; case odd. Qed. +Lemma oddX m n : odd (m ^ n) = (n == 0) || odd m. +Proof. by elim: n => // n IHn; rewrite expnS oddM {}IHn orbC; case odd. Qed. (* Doubling. *) @@ -1405,7 +1405,7 @@ rewrite -!mulnn mul2n mulnDr !mulnDl (mulnC n) -!addnA. by congr (_ + _); rewrite addnA addnn addnC. Qed. -Lemma sqrn_sub m n : n <= m -> (m - n) ^ 2 = m ^ 2 + n ^ 2 - 2 * (m * n). +Lemma sqrnB m n : n <= m -> (m - n) ^ 2 = m ^ 2 + n ^ 2 - 2 * (m * n). Proof. move/subnK <-; rewrite addnK sqrnD -addnA -addnACA -addnA. by rewrite addnn -mul2n -mulnDr -mulnDl addnK. @@ -1414,7 +1414,7 @@ Qed. Lemma sqrnD_sub m n : n <= m -> (m + n) ^ 2 - 4 * (m * n) = (m - n) ^ 2. Proof. move=> le_nm; rewrite -[4]/(2 * 2) -mulnA mul2n -addnn subnDA. -by rewrite sqrnD addnK sqrn_sub. +by rewrite sqrnD addnK sqrnB. Qed. Lemma subn_sqr m n : m ^ 2 - n ^ 2 = (m - n) * (m + n). @@ -1516,7 +1516,7 @@ Proof. without loss le_nm: m n / n <= m. by have [?|/ltnW ?] := leqP n m; last rewrite eq_sym addnC (mulnC m); apply. apply/leqifP; have [-> | ne_mn] := eqVneq; first by rewrite addnn mul2n. -by rewrite -subn_gt0 -sqrn_sub // sqrn_gt0 subn_gt0 ltn_neqAle eq_sym ne_mn. +by rewrite -subn_gt0 -sqrnB // sqrn_gt0 subn_gt0 ltn_neqAle eq_sym ne_mn. Qed. Lemma nat_AGM2 m n : 4 * (m * n) <= (m + n) ^ 2 ?= iff (m == n). @@ -2035,3 +2035,19 @@ Notation decr_inj := (@decr_inj _) (only parsing). Notation "@ 'decr_inj_in'" := (deprecate decr_inj_in decn_inj_in) (at level 10, only parsing) : fun_scope. Notation decr_inj_in := (@decr_inj_in _ _) (only parsing). + +Notation "@ 'iter_add'" := + (deprecate iter_add iterD) (at level 10, only parsing) : fun_scope. +Notation "@ 'odd_opp'" := + (deprecate odd_opp oddN) (at level 10, only parsing) : fun_scope. +Notation "@ 'sqrn_sub'" := + (deprecate sqrn_sub sqrnB) (at level 10, only parsing) : fun_scope. +Notation iter_add := (@iter_add _) (only parsing). +Notation maxn_mulr := (deprecate maxn_mulr maxnMr) (only parsing). +Notation maxn_mull := (deprecate maxn_mull maxnMl) (only parsing). +Notation minn_mulr := (deprecate minn_mulr minnMr) (only parsing). +Notation minn_mull := (deprecate minn_mull minnMl) (only parsing). +Notation odd_opp := (@odd_opp _ _) (only parsing). +Notation odd_mul := (deprecate odd_mul oddM) (only parsing). +Notation odd_exp := (deprecate odd_exp oddX) (only parsing). +Notation sqrn_sub := (@sqrn_sub _ _) (only parsing). |