From d913820cc104a43117604469dc47fca7114a98bd Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Fri, 25 Oct 2019 00:58:26 +0200 Subject: Adding nat lattice under the name natdvd --- mathcomp/ssreflect/prime.v | 41 +++++++++++++++++++++++++++++++++++++++++ 1 file changed, 41 insertions(+) (limited to 'mathcomp/ssreflect/prime.v') diff --git a/mathcomp/ssreflect/prime.v b/mathcomp/ssreflect/prime.v index 4e55abe..4f0ee77 100644 --- a/mathcomp/ssreflect/prime.v +++ b/mathcomp/ssreflect/prime.v @@ -715,6 +715,9 @@ set k := logn p _; have: p ^ k %| m * n by rewrite pfactor_dvdn. by rewrite Gauss_dvdr ?coprime_expl // -pfactor_dvdn. Qed. +Lemma logn_coprime p m : coprime p m -> logn p m = 0. +Proof. by move=> coprime_pm; rewrite -[m]muln1 logn_Gauss// logn1. Qed. + Lemma lognM p m n : 0 < m -> 0 < n -> logn p (m * n) = logn p m + logn p n. Proof. case p_pr: (prime p); last by rewrite /logn p_pr. @@ -738,6 +741,29 @@ case: (posnP n) => [-> |]; first by rewrite div0n logn0. by rewrite -{1 3}def_n muln_gt0 => /andP[q_gt0 m_gt0]; rewrite lognM ?addnK. Qed. +Lemma logn_gcd p m n : 0 < m -> 0 < n -> + logn p (gcdn m n) = minn (logn p m) (logn p n). +Proof. +case p_pr: (prime p); last by rewrite /logn p_pr. +wlog le_log_mn: m n / logn p m <= logn p n => [hwlog m_gt0 n_gt0|]. + have /orP[] := leq_total (logn p m) (logn p n) => /hwlog; first exact. + by rewrite gcdnC minnC; apply. +have xlp := pfactor_coprime p_pr => /xlp[m' cpm' {1}->] /xlp[n' cpn' {1}->]. +rewrite (minn_idPl _)// -(subnK le_log_mn) expnD mulnA -muln_gcdl. +rewrite lognM//; last first. + rewrite Gauss_gcdl ?coprime_expr 1?coprime_sym// gcdn_gt0. + by case: m' cpm' p_pr => //; rewrite /coprime gcdn0 => /eqP->. +rewrite pfactorK// Gauss_gcdl; last by rewrite coprime_expr// coprime_sym. +by rewrite logn_coprime// /coprime gcdnA (eqP cpm') gcd1n. +Qed. + +Lemma logn_lcm p m n : 0 < m -> 0 < n -> + logn p (lcmn m n) = maxn (logn p m) (logn p n). +Proof. +move=> m_gt0 n_gt0; rewrite /lcmn logn_div ?dvdn_mull ?dvdn_gcdr//. +by rewrite lognM// logn_gcd// -addn_min_max addnC addnK. +Qed. + Lemma dvdn_pfactor p d n : prime p -> reflect (exists2 m, m <= n & d = p ^ m) (d %| p ^ n). Proof. @@ -899,6 +925,14 @@ apply: eq_bigr => p _; rewrite ltnS lognE. by case: and3P => [[_ n_gt0 p_dv_n]|]; rewrite ?if_same // andbC dvdn_leq. Qed. +Lemma eq_partn_from_log m n (pi : nat_pred) : 0 < m -> 0 < n -> + (forall p, p \in pi -> logn p m = logn p n) -> m`_pi = n`_pi. +Proof. +move=> m_gt0 n_gt0 eq_log. +rewrite !(@widen_partn (maxn m n)) ?leq_max ?leqnn ?orbT//. +by apply: eq_bigr => p /eq_log ->. +Qed. + Lemma partn0 pi : 0`_pi = 1. Proof. by apply: big1_seq => [] [|n]; rewrite andbC. Qed. @@ -983,6 +1017,13 @@ move=> n_gt0; rewrite -{2}(partn_pi n_gt0) {2}/partn big_mkcond /=. by apply: eq_bigr => p _; rewrite -logn_gt0; case: (logn p _). Qed. +Lemma eqn_from_log m n : 0 < m -> 0 < n -> + (forall p, logn p m = logn p n) -> m = n. +Proof. +move=> m_gt0 n_gt0 eq_log; rewrite -[m]partnT// -[n]partnT//. +exact: eq_partn_from_log. +Qed. + Lemma partnC pi n : n > 0 -> n`_pi * n`_pi^' = n. Proof. move=> n_gt0; rewrite -{3}(partnT n_gt0) /partn. -- cgit v1.2.3 From 696cd421b27ff2bee821c053c3c3d5926e9d68d3 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Thu, 31 Oct 2019 09:41:52 +0100 Subject: Doc, comments, changelog and better proofs - adding a doc paragraph on displays - Changelog - better proofs for new logn, gcdn, lcmn, partn facts - Putting comments in the example of nat --- mathcomp/ssreflect/prime.v | 48 +++++++++++++++++----------------------------- 1 file changed, 18 insertions(+), 30 deletions(-) (limited to 'mathcomp/ssreflect/prime.v') diff --git a/mathcomp/ssreflect/prime.v b/mathcomp/ssreflect/prime.v index 4f0ee77..d8f5939 100644 --- a/mathcomp/ssreflect/prime.v +++ b/mathcomp/ssreflect/prime.v @@ -741,29 +741,6 @@ case: (posnP n) => [-> |]; first by rewrite div0n logn0. by rewrite -{1 3}def_n muln_gt0 => /andP[q_gt0 m_gt0]; rewrite lognM ?addnK. Qed. -Lemma logn_gcd p m n : 0 < m -> 0 < n -> - logn p (gcdn m n) = minn (logn p m) (logn p n). -Proof. -case p_pr: (prime p); last by rewrite /logn p_pr. -wlog le_log_mn: m n / logn p m <= logn p n => [hwlog m_gt0 n_gt0|]. - have /orP[] := leq_total (logn p m) (logn p n) => /hwlog; first exact. - by rewrite gcdnC minnC; apply. -have xlp := pfactor_coprime p_pr => /xlp[m' cpm' {1}->] /xlp[n' cpn' {1}->]. -rewrite (minn_idPl _)// -(subnK le_log_mn) expnD mulnA -muln_gcdl. -rewrite lognM//; last first. - rewrite Gauss_gcdl ?coprime_expr 1?coprime_sym// gcdn_gt0. - by case: m' cpm' p_pr => //; rewrite /coprime gcdn0 => /eqP->. -rewrite pfactorK// Gauss_gcdl; last by rewrite coprime_expr// coprime_sym. -by rewrite logn_coprime// /coprime gcdnA (eqP cpm') gcd1n. -Qed. - -Lemma logn_lcm p m n : 0 < m -> 0 < n -> - logn p (lcmn m n) = maxn (logn p m) (logn p n). -Proof. -move=> m_gt0 n_gt0; rewrite /lcmn logn_div ?dvdn_mull ?dvdn_gcdr//. -by rewrite lognM// logn_gcd// -addn_min_max addnC addnK. -Qed. - Lemma dvdn_pfactor p d n : prime p -> reflect (exists2 m, m <= n & d = p ^ m) (d %| p ^ n). Proof. @@ -926,10 +903,9 @@ by case: and3P => [[_ n_gt0 p_dv_n]|]; rewrite ?if_same // andbC dvdn_leq. Qed. Lemma eq_partn_from_log m n (pi : nat_pred) : 0 < m -> 0 < n -> - (forall p, p \in pi -> logn p m = logn p n) -> m`_pi = n`_pi. + {in pi, logn^~ m =1 logn^~ n} -> m`_pi = n`_pi. Proof. -move=> m_gt0 n_gt0 eq_log. -rewrite !(@widen_partn (maxn m n)) ?leq_max ?leqnn ?orbT//. +move=> m0 n0 eq_log; rewrite !(@widen_partn (maxn m n)) ?leq_maxl ?leq_maxr//. by apply: eq_bigr => p /eq_log ->. Qed. @@ -1017,11 +993,9 @@ move=> n_gt0; rewrite -{2}(partn_pi n_gt0) {2}/partn big_mkcond /=. by apply: eq_bigr => p _; rewrite -logn_gt0; case: (logn p _). Qed. -Lemma eqn_from_log m n : 0 < m -> 0 < n -> - (forall p, logn p m = logn p n) -> m = n. +Lemma eqn_from_log m n : 0 < m -> 0 < n -> logn^~ m =1 logn^~ n -> m = n. Proof. -move=> m_gt0 n_gt0 eq_log; rewrite -[m]partnT// -[n]partnT//. -exact: eq_partn_from_log. +by move=> ? ? /(@in1W _ predT)/eq_partn_from_log; rewrite !partnT// => ->. Qed. Lemma partnC pi n : n > 0 -> n`_pi * n`_pi^' = n. @@ -1089,6 +1063,20 @@ apply/dvdn_biggcdP=> i Pi; rewrite -(partnC pi (F_gt0 i Pi)) dvdn_mul //. by rewrite partn_dvd ?F_gt0 // (@biggcdn_inf _ i). Qed. +Lemma logn_gcd p m n : 0 < m -> 0 < n -> + logn p (gcdn m n) = minn (logn p m) (logn p n). +Proof. +move=> m_gt0 n_gt0; case p_pr: (prime p); last by rewrite /logn p_pr. +by apply: (@expnI p); rewrite ?prime_gt1// expn_min -!p_part partn_gcd. +Qed. + +Lemma logn_lcm p m n : 0 < m -> 0 < n -> + logn p (lcmn m n) = maxn (logn p m) (logn p n). +Proof. +move=> m_gt0 n_gt0; rewrite /lcmn logn_div ?dvdn_mull ?dvdn_gcdr//. +by rewrite lognM// logn_gcd// -addn_min_max addnC addnK. +Qed. + Lemma sub_in_pnat pi rho n : {in \pi(n), {subset pi <= rho}} -> pi.-nat n -> rho.-nat n. Proof. -- cgit v1.2.3