From 6423f1b6e3056883016598e454c55cab1004dfd2 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Fri, 16 Mar 2007 08:04:32 +0000 Subject: [PATCH] Extensions required for the moebius function (in Z). --- .../matita/library/nat/div_and_mod.ma | 19 + .../matita/library/nat/euler_theorem.ma | 39 + helm/software/matita/library/nat/exp.ma | 49 ++ .../matita/library/nat/factorization.ma | 21 +- .../software/matita/library/nat/iteration2.ma | 683 ++++++++++++++++++ helm/software/matita/library/nat/lt_arith.ma | 22 + .../matita/library/nat/minimization.ma | 51 +- helm/software/matita/library/nat/nth_prime.ma | 11 + helm/software/matita/library/nat/ord.ma | 204 +++++- helm/software/matita/library/nat/orders.ma | 2 +- helm/software/matita/library/nat/primes.ma | 57 +- 11 files changed, 1136 insertions(+), 22 deletions(-) create mode 100644 helm/software/matita/library/nat/iteration2.ma diff --git a/helm/software/matita/library/nat/div_and_mod.ma b/helm/software/matita/library/nat/div_and_mod.ma index ccddcca3f..65ba0e9e5 100644 --- a/helm/software/matita/library/nat/div_and_mod.ma +++ b/helm/software/matita/library/nat/div_and_mod.ma @@ -193,6 +193,25 @@ unfold lt.apply le_S_S.apply le_O_n. rewrite < plus_n_O.rewrite < sym_times.reflexivity. qed. +lemma div_plus_times: \forall m,q,r:nat. r < m \to (q*m+r)/ m = q. +intros. +apply (div_mod_spec_to_eq (q*m+r) m ? ((q*m+r) \mod m) ? r) + [apply div_mod_spec_div_mod. + apply (le_to_lt_to_lt ? r) + [apply le_O_n|assumption] + |apply div_mod_spec_intro[assumption|reflexivity] + ] +qed. + +lemma mod_plus_times: \forall m,q,r:nat. r < m \to (q*m+r) \mod m = r. +intros. +apply (div_mod_spec_to_eq2 (q*m+r) m ((q*m+r)/ m) ((q*m+r) \mod m) q r) + [apply div_mod_spec_div_mod. + apply (le_to_lt_to_lt ? r) + [apply le_O_n|assumption] + |apply div_mod_spec_intro[assumption|reflexivity] + ] +qed. (* some properties of div and mod *) theorem div_times: \forall n,m:nat. ((S n)*m) / (S n) = m. intros. diff --git a/helm/software/matita/library/nat/euler_theorem.ma b/helm/software/matita/library/nat/euler_theorem.ma index d58f7c2b0..43638fca6 100644 --- a/helm/software/matita/library/nat/euler_theorem.ma +++ b/helm/software/matita/library/nat/euler_theorem.ma @@ -17,7 +17,46 @@ set "baseuri" "cic:/matita/nat/euler_theorem". include "nat/map_iter_p.ma". include "nat/totient.ma". +lemma gcd_n_n: \forall n.gcd n n = n. +intro.elim n + [reflexivity + |apply le_to_le_to_eq + [apply divides_to_le + [apply lt_O_S + |apply divides_gcd_n + ] + |apply divides_to_le + [apply lt_O_gcd.apply lt_O_S + |apply divides_d_gcd + [apply divides_n_n|apply divides_n_n] + ] + ] + ] +qed. + + +lemma count_card: \forall p.\forall n. +p O = false \to count (S n) p = card n p. +intros.elim n + [simplify.rewrite > H. reflexivity + |simplify. + rewrite < plus_n_O. + apply eq_f.assumption + ] +qed. + +lemma count_card1: \forall p.\forall n. +p O = false \to p n = false \to count n p = card n p. +intros 3.apply (nat_case n) + [intro.simplify.rewrite > H. reflexivity + |intros.rewrite > (count_card ? ? H). + simplify.rewrite > H1.reflexivity + ] +qed. + + (* a reformulation of totient using card insted of count *) + lemma totient_card: \forall n. totient n = card n (\lambda i.eqb (gcd i n) (S O)). intro.apply (nat_case n) diff --git a/helm/software/matita/library/nat/exp.ma b/helm/software/matita/library/nat/exp.ma index e40844e3f..c69be6b5f 100644 --- a/helm/software/matita/library/nat/exp.ma +++ b/helm/software/matita/library/nat/exp.ma @@ -15,6 +15,7 @@ set "baseuri" "cic:/matita/nat/exp". include "nat/div_and_mod.ma". +include "nat/lt_arith.ma". let rec exp n m on m\def match m with @@ -95,3 +96,51 @@ qed. variant inj_exp_r: \forall p:nat. (S O) < p \to \forall n,m:nat. p \sup n = p \sup m \to n = m \def injective_exp_r. + +theorem le_exp: \forall n,m,p:nat. O < p \to n \le m \to exp p n \le exp p m. +apply nat_elim2 + [intros. + apply lt_O_exp.assumption + |intros. + apply False_ind. + apply (le_to_not_lt ? ? ? H1). + apply le_O_n + |intros. + simplify. + apply le_times + [apply le_n + |apply H[assumption|apply le_S_S_to_le.assumption] + ] + ] +qed. + +theorem lt_exp: \forall n,m,p:nat. S O < p \to n < m \to exp p n < exp p m. +apply nat_elim2 + [intros. + apply (lt_O_n_elim ? H1).intro. + simplify.unfold lt. + rewrite > times_n_SO. + apply le_times + [assumption + |apply lt_O_exp. + apply (trans_lt ? (S O))[apply le_n|assumption] + ] + |intros. + apply False_ind. + apply (le_to_not_lt ? ? ? H1). + apply le_O_n + |intros.simplify. + apply lt_times_r1 + [apply (trans_lt ? (S O))[apply le_n|assumption] + |apply H + [apply H1 + |apply le_S_S_to_le.assumption + ] + ] + ] +qed. + + + + + \ No newline at end of file diff --git a/helm/software/matita/library/nat/factorization.ma b/helm/software/matita/library/nat/factorization.ma index 85351c06d..37a704592 100644 --- a/helm/software/matita/library/nat/factorization.ma +++ b/helm/software/matita/library/nat/factorization.ma @@ -27,10 +27,10 @@ definition max_prime_factor \def \lambda n:nat. theorem divides_max_prime_factor_n: \forall n:nat. (S O) < n \to nth_prime (max_prime_factor n) \divides n. -intros; apply divides_b_true_to_divides; -[ apply lt_O_nth_prime_n; -| apply (f_max_true (\lambda p:nat.eqb (n \mod (nth_prime p)) O) n); - cut (\exists i. nth_prime i = smallest_factor n); +intros. +apply divides_b_true_to_divides. +apply (f_max_true (\lambda p:nat.eqb (n \mod (nth_prime p)) O) n); +cut (\exists i. nth_prime i = smallest_factor n); [ elim Hcut. apply (ex_intro nat ? a); split; @@ -56,7 +56,7 @@ intros; apply divides_b_true_to_divides; (* apply prime_to_nth_prime; apply prime_smallest_factor_n; - assumption; *) ] ] + assumption; *) ] qed. theorem divides_to_max_prime_factor : \forall n,m. (S O) < n \to O < m \to n \divides m \to @@ -90,6 +90,17 @@ auto. *) qed. +theorem divides_to_max_prime_factor1 : \forall n,m. O < n \to O < m \to n \divides m \to +max_prime_factor n \le max_prime_factor m. +intros 3. +elim (le_to_or_lt_eq ? ? H) + [apply divides_to_max_prime_factor + [assumption|assumption|assumption] + |rewrite < H1. + simplify.apply le_O_n. + ] +qed. + theorem p_ord_to_lt_max_prime_factor: \forall n,p,q,r. O < n \to p = max_prime_factor n \to (pair nat nat q r) = p_ord n (nth_prime p) \to diff --git a/helm/software/matita/library/nat/iteration2.ma b/helm/software/matita/library/nat/iteration2.ma new file mode 100644 index 000000000..0c3091d30 --- /dev/null +++ b/helm/software/matita/library/nat/iteration2.ma @@ -0,0 +1,683 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| A.Asperti, C.Sacerdoti Coen, *) +(* ||A|| E.Tassi, S.Zacchiroli *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU Lesser General Public License Version 2.1 *) +(* *) +(**************************************************************************) + +set "baseuri" "cic:/matita/nat/iteration2.ma". + +include "nat/primes.ma". +include "nat/ord.ma". + +let rec sigma_p n p (g:nat \to nat) \def + match n with + [ O \Rightarrow O + | (S k) \Rightarrow + match p k with + [true \Rightarrow (g k)+(sigma_p k p g) + |false \Rightarrow sigma_p k p g] + ]. + +theorem true_to_sigma_p_Sn: +\forall n:nat. \forall p:nat \to bool. \forall g:nat \to nat. +p n = true \to sigma_p (S n) p g = +(g n)+(sigma_p n p g). +intros.simplify. +rewrite > H.reflexivity. +qed. + +theorem false_to_sigma_p_Sn: +\forall n:nat. \forall p:nat \to bool. \forall g:nat \to nat. +p n = false \to sigma_p (S n) p g = sigma_p n p g. +intros.simplify. +rewrite > H.reflexivity. +qed. + +theorem eq_sigma_p: \forall p1,p2:nat \to bool. +\forall g1,g2: nat \to nat.\forall n. +(\forall x. x < n \to p1 x = p2 x) \to +(\forall x. x < n \to g1 x = g2 x) \to +sigma_p n p1 g1 = sigma_p n p2 g2. +intros 5.elim n + [reflexivity + |apply (bool_elim ? (p1 n1)) + [intro. + rewrite > (true_to_sigma_p_Sn ? ? ? H3). + rewrite > true_to_sigma_p_Sn + [apply eq_f2 + [apply H2.apply le_n. + |apply H + [intros.apply H1.apply le_S.assumption + |intros.apply H2.apply le_S.assumption + ] + ] + |rewrite < H3.apply sym_eq.apply H1.apply le_n + ] + |intro. + rewrite > (false_to_sigma_p_Sn ? ? ? H3). + rewrite > false_to_sigma_p_Sn + [apply H + [intros.apply H1.apply le_S.assumption + |intros.apply H2.apply le_S.assumption + ] + |rewrite < H3.apply sym_eq.apply H1.apply le_n + ] + ] + ] +qed. + +theorem sigma_p_false: +\forall g: nat \to nat.\forall n.sigma_p n (\lambda x.false) g = O. +intros. +elim n[reflexivity|simplify.assumption] +qed. + +theorem sigma_p_plus: \forall n,k:nat.\forall p:nat \to bool. +\forall g: nat \to nat. +sigma_p (k+n) p g += sigma_p k (\lambda x.p (x+n)) (\lambda x.g (x+n)) + sigma_p n p g. +intros. +elim k + [reflexivity + |apply (bool_elim ? (p (n1+n))) + [intro. + simplify in \vdash (? ? (? % ? ?) ?). + rewrite > (true_to_sigma_p_Sn ? ? ? H1). + rewrite > (true_to_sigma_p_Sn n1 (\lambda x.p (x+n)) ? H1). + rewrite > assoc_plus. + rewrite < H.reflexivity + |intro. + simplify in \vdash (? ? (? % ? ?) ?). + rewrite > (false_to_sigma_p_Sn ? ? ? H1). + rewrite > (false_to_sigma_p_Sn n1 (\lambda x.p (x+n)) ? H1). + assumption. + ] + ] +qed. + +theorem false_to_eq_sigma_p: \forall n,m:nat.n \le m \to +\forall p:nat \to bool. +\forall g: nat \to nat. (\forall i:nat. n \le i \to i < m \to +p i = false) \to sigma_p m p g = sigma_p n p g. +intros 5. +elim H + [reflexivity + |simplify. + rewrite > H3 + [simplify. + apply H2. + intros. + apply H3[apply H4|apply le_S.assumption] + |assumption + |apply le_n + ] + ] +qed. + +theorem sigma_p2 : +\forall n,m:nat. +\forall p1,p2:nat \to bool. +\forall g: nat \to nat \to nat. +sigma_p (n*m) + (\lambda x.andb (p1 (div x m)) (p2 (mod x m))) + (\lambda x.g (div x m) (mod x m)) = +sigma_p n p1 + (\lambda x.sigma_p m p2 (g x)). +intros. +elim n + [simplify.reflexivity + |apply (bool_elim ? (p1 n1)) + [intro. + rewrite > (true_to_sigma_p_Sn ? ? ? H1). + simplify in \vdash (? ? (? % ? ?) ?); + rewrite > sigma_p_plus. + rewrite < H. + apply eq_f2 + [apply eq_sigma_p + [intros. + rewrite > sym_plus. + rewrite > (div_plus_times ? ? ? H2). + rewrite > (mod_plus_times ? ? ? H2). + rewrite > H1. + simplify.reflexivity + |intros. + rewrite > sym_plus. + rewrite > (div_plus_times ? ? ? H2). + rewrite > (mod_plus_times ? ? ? H2). + rewrite > H1. + simplify.reflexivity. + ] + |reflexivity + ] + |intro. + rewrite > (false_to_sigma_p_Sn ? ? ? H1). + simplify in \vdash (? ? (? % ? ?) ?); + rewrite > sigma_p_plus. + rewrite > H. + apply (trans_eq ? ? (O+(sigma_p n1 p1 (\lambda x:nat.sigma_p m p2 (g x))))) + [apply eq_f2 + [rewrite > (eq_sigma_p ? (\lambda x.false) ? (\lambda x:nat.g ((x+n1*m)/m) ((x+n1*m)\mod m))) + [apply sigma_p_false + |intros. + rewrite > sym_plus. + rewrite > (div_plus_times ? ? ? H2). + rewrite > (mod_plus_times ? ? ? H2). + rewrite > H1. + simplify.reflexivity + |intros.reflexivity. + ] + |reflexivity + ] + |reflexivity + ] + ] + ] +qed. + +lemma sigma_p_gi: \forall g: nat \to nat. +\forall n,i.\forall p:nat \to bool.i < n \to p i = true \to +sigma_p n p g = g i + sigma_p n (\lambda x. andb (p x) (notb (eqb x i))) g. +intros 2. +elim n + [apply False_ind. + apply (not_le_Sn_O i). + assumption + |apply (bool_elim ? (p n1));intro + [elim (le_to_or_lt_eq i n1) + [rewrite > true_to_sigma_p_Sn + [rewrite > true_to_sigma_p_Sn + [rewrite < assoc_plus. + rewrite < sym_plus in \vdash (? ? ? (? % ?)). + rewrite > assoc_plus. + apply eq_f2 + [reflexivity + |apply H[assumption|assumption] + ] + |rewrite > H3.simplify. + change with (notb (eqb n1 i) = notb false). + apply eq_f. + apply not_eq_to_eqb_false. + unfold Not.intro. + apply (lt_to_not_eq ? ? H4). + apply sym_eq.assumption + ] + |assumption + ] + |rewrite > true_to_sigma_p_Sn + [rewrite > H4. + apply eq_f2 + [reflexivity + |rewrite > false_to_sigma_p_Sn + [apply eq_sigma_p + [intros. + elim (p x) + [simplify. + change with (notb false = notb (eqb x n1)). + apply eq_f. + apply sym_eq. + apply not_eq_to_eqb_false. + apply (lt_to_not_eq ? ? H5) + |reflexivity + ] + |intros.reflexivity + ] + |rewrite > H3. + rewrite > (eq_to_eqb_true ? ? (refl_eq ? n1)). + reflexivity + ] + ] + |assumption + ] + |apply le_S_S_to_le.assumption + ] + |rewrite > false_to_sigma_p_Sn + [elim (le_to_or_lt_eq i n1) + [rewrite > false_to_sigma_p_Sn + [apply H[assumption|assumption] + |rewrite > H3.reflexivity + ] + |apply False_ind. + apply not_eq_true_false. + rewrite < H2. + rewrite > H4. + assumption + |apply le_S_S_to_le.assumption + ] + |assumption + ] + ] + ] +qed. + +theorem eq_sigma_p_gh: +\forall g,h,h1: nat \to nat.\forall n,n1. +\forall p1,p2:nat \to bool. +(\forall i. i < n \to p1 i = true \to p2 (h i) = true) \to +(\forall i. i < n \to p1 i = true \to h1 (h i) = i) \to +(\forall i. i < n \to p1 i = true \to h i < n1) \to +(\forall j. j < n1 \to p2 j = true \to p1 (h1 j) = true) \to +(\forall j. j < n1 \to p2 j = true \to h (h1 j) = j) \to +(\forall j. j < n1 \to p2 j = true \to h1 j < n) \to +sigma_p n p1 (\lambda x.g(h x)) = sigma_p n1 (\lambda x.p2 x) g. +intros 4. +elim n + [generalize in match H5. + elim n1 + [reflexivity + |apply (bool_elim ? (p2 n2));intro + [apply False_ind. + apply (not_le_Sn_O (h1 n2)). + apply H7 + [apply le_n|assumption] + |rewrite > false_to_sigma_p_Sn + [apply H6. + intros. + apply H7[apply le_S.apply H9|assumption] + |assumption + ] + ] + ] + |apply (bool_elim ? (p1 n1));intro + [rewrite > true_to_sigma_p_Sn + [rewrite > (sigma_p_gi g n2 (h n1)) + [apply eq_f2 + [reflexivity + |apply H + [intros. + rewrite > H1 + [simplify. + change with ((\not eqb (h i) (h n1))= \not false). + apply eq_f. + apply not_eq_to_eqb_false. + unfold Not.intro. + apply (lt_to_not_eq ? ? H8). + rewrite < H2 + [rewrite < (H2 n1) + [apply eq_f.assumption|apply le_n|assumption] + |apply le_S.assumption + |assumption + ] + |apply le_S.assumption + |assumption + ] + |intros. + apply H2[apply le_S.assumption|assumption] + |intros. + apply H3[apply le_S.assumption|assumption] + |intros. + apply H4 + [assumption + |generalize in match H9. + elim (p2 j) + [reflexivity|assumption] + ] + |intros. + apply H5 + [assumption + |generalize in match H9. + elim (p2 j) + [reflexivity|assumption] + ] + |intros. + elim (le_to_or_lt_eq (h1 j) n1) + [assumption + |generalize in match H9. + elim (p2 j) + [simplify in H11. + absurd (j = (h n1)) + [rewrite < H10. + rewrite > H5 + [reflexivity|assumption|auto] + |apply eqb_false_to_not_eq. + generalize in match H11. + elim (eqb j (h n1)) + [apply sym_eq.assumption|reflexivity] + ] + |simplify in H11. + apply False_ind. + apply not_eq_true_false. + apply sym_eq.assumption + ] + |apply le_S_S_to_le. + apply H6 + [assumption + |generalize in match H9. + elim (p2 j) + [reflexivity|assumption] + ] + ] + ] + ] + |apply H3[apply le_n|assumption] + |apply H1[apply le_n|assumption] + ] + |assumption + ] + |rewrite > false_to_sigma_p_Sn + [apply H + [intros.apply H1[apply le_S.assumption|assumption] + |intros.apply H2[apply le_S.assumption|assumption] + |intros.apply H3[apply le_S.assumption|assumption] + |intros.apply H4[assumption|assumption] + |intros.apply H5[assumption|assumption] + |intros. + elim (le_to_or_lt_eq (h1 j) n1) + [assumption + |absurd (j = (h n1)) + [rewrite < H10. + rewrite > H5 + [reflexivity|assumption|assumption] + |unfold Not.intro. + apply not_eq_true_false. + rewrite < H7. + rewrite < H10. + rewrite > H4 + [reflexivity|assumption|assumption] + ] + |apply le_S_S_to_le. + apply H6[assumption|assumption] + ] + ] + |assumption + ] + ] + ] +qed. + +definition p_ord_times \def +\lambda p,m,x. + match p_ord x p with + [pair q r \Rightarrow r*m+q]. + +theorem eq_p_ord_times: \forall p,m,x. +p_ord_times p m x = (ord_rem x p)*m+(ord x p). +intros.unfold p_ord_times. unfold ord_rem. +unfold ord. +elim (p_ord x p). +reflexivity. +qed. + +theorem div_p_ord_times: +\forall p,m,x. ord x p < m \to p_ord_times p m x / m = ord_rem x p. +intros.rewrite > eq_p_ord_times. +apply div_plus_times. +assumption. +qed. + +theorem mod_p_ord_times: +\forall p,m,x. ord x p < m \to p_ord_times p m x \mod m = ord x p. +intros.rewrite > eq_p_ord_times. +apply mod_plus_times. +assumption. +qed. + +theorem sigma_p_divides: +\forall n,m,p:nat.O < n \to prime p \to Not (divides p n) \to +\forall g: nat \to nat. +sigma_p (S (n*(exp p m))) (\lambda x.divides_b x (n*(exp p m))) g = +sigma_p (S n) (\lambda x.divides_b x n) + (\lambda x.sigma_p (S m) (\lambda y.true) (\lambda y.g (x*(exp p y)))). +intros. +cut (O < p) + [rewrite < sigma_p2. + apply (trans_eq ? ? + (sigma_p (S n*S m) (\lambda x:nat.divides_b (x/S m) n) + (\lambda x:nat.g (x/S m*(p)\sup(x\mod S m))))) + [apply sym_eq. + apply (eq_sigma_p_gh g ? (p_ord_times p (S m))) + [intros. + lapply (divides_b_true_to_lt_O ? ? H H4). + apply divides_to_divides_b_true + [rewrite > (times_n_O O). + apply lt_times + [assumption + |apply lt_O_exp.assumption + ] + |apply divides_times + [apply divides_b_true_to_divides.assumption + |apply (witness ? ? (p \sup (m-i \mod (S m)))). + rewrite < exp_plus_times. + apply eq_f. + rewrite > sym_plus. + apply plus_minus_m_m. + auto + ] + ] + |intros. + lapply (divides_b_true_to_lt_O ? ? H H4). + unfold p_ord_times. + rewrite > (p_ord_exp1 p ? (i \mod (S m)) (i/S m)) + [change with ((i/S m)*S m+i \mod S m=i). + apply sym_eq. + apply div_mod. + apply lt_O_S + |assumption + |unfold Not.intro. + apply H2. + apply (trans_divides ? (i/ S m)) + [assumption| + apply divides_b_true_to_divides;assumption] + |apply sym_times. + ] + |intros. + apply le_S_S. + apply le_times + [apply le_S_S_to_le. + change with ((i/S m) < S n). + apply (lt_times_to_lt_l m). + apply (le_to_lt_to_lt ? i) + [auto|assumption] + |apply le_exp + [assumption + |apply le_S_S_to_le. + apply lt_mod_m_m. + apply lt_O_S + ] + ] + |intros. + cut (ord j p < S m) + [rewrite > div_p_ord_times + [apply divides_to_divides_b_true + [apply lt_O_ord_rem + [elim H1.assumption + |apply (divides_b_true_to_lt_O ? ? ? H4). + rewrite > (times_n_O O). + apply lt_times + [assumption|apply lt_O_exp.assumption] + ] + |cut (n = ord_rem (n*(exp p m)) p) + [rewrite > Hcut2. + apply divides_to_divides_ord_rem + [apply (divides_b_true_to_lt_O ? ? ? H4). + rewrite > (times_n_O O). + apply lt_times + [assumption|apply lt_O_exp.assumption] + |rewrite > (times_n_O O). + apply lt_times + [assumption|apply lt_O_exp.assumption] + |assumption + |apply divides_b_true_to_divides. + assumption + ] + |unfold ord_rem. + rewrite > (p_ord_exp1 p ? m n) + [reflexivity + |assumption + |assumption + |apply sym_times + ] + ] + ] + |assumption + ] + |cut (m = ord (n*(exp p m)) p) + [apply le_S_S. + rewrite > Hcut1. + apply divides_to_le_ord + [apply (divides_b_true_to_lt_O ? ? ? H4). + rewrite > (times_n_O O). + apply lt_times + [assumption|apply lt_O_exp.assumption] + |rewrite > (times_n_O O). + apply lt_times + [assumption|apply lt_O_exp.assumption] + |assumption + |apply divides_b_true_to_divides. + assumption + ] + |unfold ord. + rewrite > (p_ord_exp1 p ? m n) + [reflexivity + |assumption + |assumption + |apply sym_times + ] + ] + ] + |intros. + cut (ord j p < S m) + [rewrite > div_p_ord_times + [rewrite > mod_p_ord_times + [rewrite > sym_times. + apply sym_eq. + apply exp_ord + [elim H1.assumption + |apply (divides_b_true_to_lt_O ? ? ? H4). + rewrite > (times_n_O O). + apply lt_times + [assumption|apply lt_O_exp.assumption] + ] + |cut (m = ord (n*(exp p m)) p) + [apply le_S_S. + rewrite > Hcut2. + apply divides_to_le_ord + [apply (divides_b_true_to_lt_O ? ? ? H4). + rewrite > (times_n_O O). + apply lt_times + [assumption|apply lt_O_exp.assumption] + |rewrite > (times_n_O O). + apply lt_times + [assumption|apply lt_O_exp.assumption] + |assumption + |apply divides_b_true_to_divides. + assumption + ] + |unfold ord. + rewrite > (p_ord_exp1 p ? m n) + [reflexivity + |assumption + |assumption + |apply sym_times + ] + ] + ] + |assumption + ] + |cut (m = ord (n*(exp p m)) p) + [apply le_S_S. + rewrite > Hcut1. + apply divides_to_le_ord + [apply (divides_b_true_to_lt_O ? ? ? H4). + rewrite > (times_n_O O). + apply lt_times + [assumption|apply lt_O_exp.assumption] + |rewrite > (times_n_O O). + apply lt_times + [assumption|apply lt_O_exp.assumption] + |assumption + |apply divides_b_true_to_divides. + assumption + ] + |unfold ord. + rewrite > (p_ord_exp1 p ? m n) + [reflexivity + |assumption + |assumption + |apply sym_times + ] + ] + ] + |intros. + rewrite > eq_p_ord_times. + rewrite > sym_plus. + apply (lt_to_le_to_lt ? (S m +ord_rem j p*S m)) + [apply lt_plus_l. + apply le_S_S. + cut (m = ord (n*(p \sup m)) p) + [rewrite > Hcut1. + apply divides_to_le_ord + [apply (divides_b_true_to_lt_O ? ? ? H4). + rewrite > (times_n_O O). + apply lt_times + [assumption|apply lt_O_exp.assumption] + |rewrite > (times_n_O O). + apply lt_times + [assumption|apply lt_O_exp.assumption] + |assumption + |apply divides_b_true_to_divides. + assumption + ] + |unfold ord. + rewrite > sym_times. + rewrite > (p_ord_exp1 p ? m n) + [reflexivity + |assumption + |assumption + |reflexivity + ] + ] + |change with (S (ord_rem j p)*S m \le S n*S m). + apply le_times_l. + apply le_S_S. + cut (n = ord_rem (n*(p \sup m)) p) + [rewrite > Hcut1. + apply divides_to_le + [apply lt_O_ord_rem + [elim H1.assumption + |rewrite > (times_n_O O). + apply lt_times + [assumption|apply lt_O_exp.assumption] + ] + |apply divides_to_divides_ord_rem + [apply (divides_b_true_to_lt_O ? ? ? H4). + rewrite > (times_n_O O). + apply lt_times + [assumption|apply lt_O_exp.assumption] + |rewrite > (times_n_O O). + apply lt_times + [assumption|apply lt_O_exp.assumption] + |assumption + |apply divides_b_true_to_divides. + assumption + ] + ] + |unfold ord_rem. + rewrite > sym_times. + rewrite > (p_ord_exp1 p ? m n) + [reflexivity + |assumption + |assumption + |reflexivity + ] + ] + ] + ] + |apply eq_sigma_p + [intros. + elim (divides_b (x/S m) n);reflexivity + |intros.reflexivity + ] + ] +|elim H1.apply lt_to_le.assumption +] +qed. + + diff --git a/helm/software/matita/library/nat/lt_arith.ma b/helm/software/matita/library/nat/lt_arith.ma index 6635a8b0d..b01bd5461 100644 --- a/helm/software/matita/library/nat/lt_arith.ma +++ b/helm/software/matita/library/nat/lt_arith.ma @@ -111,6 +111,28 @@ assumption. apply (ltn_to_ltO p q H2). qed. +theorem lt_times_r1: +\forall n,m,p. O < n \to m < p \to n*m < n*p. +intros. +elim H;apply lt_times_r;assumption. +qed. + +theorem lt_times_l1: +\forall n,m,p. O < n \to m < p \to m*n < p*n. +intros. +elim H;apply lt_times_l;assumption. +qed. + +theorem lt_to_le_to_lt_times : +\forall n,n1,m,m1. n < n1 \to m \le m1 \to O < m1 \to n*m < n1*m1. +intros. +apply (le_to_lt_to_lt ? (n*m1)) + [apply le_times_r.assumption + |apply lt_times_l1 + [assumption|assumption] + ] +qed. + theorem lt_times_to_lt_l: \forall n,p,q:nat. p*(S n) < q*(S n) \to p < q. intros. diff --git a/helm/software/matita/library/nat/minimization.ma b/helm/software/matita/library/nat/minimization.ma index 0abed5ad3..2d273e180 100644 --- a/helm/software/matita/library/nat/minimization.ma +++ b/helm/software/matita/library/nat/minimization.ma @@ -72,11 +72,6 @@ intro.simplify.rewrite < H3. rewrite > H2.simplify.apply le_n. qed. - -definition max_spec \def \lambda f:nat \to bool.\lambda n: nat. -\exists i. (le i n) \land (f i = true) \to -(f n) = true \land (\forall i. i < n \to (f i = false)). - theorem f_max_true : \forall f:nat \to bool. \forall n:nat. (\exists i:nat. le i n \land f i = true) \to f (max n f) = true. intros 2. @@ -119,6 +114,52 @@ apply le_S_S_to_le.assumption. intro.rewrite > H7.assumption. qed. +definition max_spec \def \lambda f:nat \to bool.\lambda n,m: nat. +m \le n \land (f m)=true \land (\forall i. m < i \to i \le n \to (f i = false)). + +theorem max_spec_to_max: \forall f:nat \to bool.\forall n,m:nat. +max_spec f n m \to max n f = m. +intros 2. +elim n + [elim H.elim H1.apply (le_n_O_elim ? H3). + apply max_O_f + |elim H1. + elim (max_S_max f n1) + [elim H4. + rewrite > H6. + apply le_to_le_to_eq + [apply not_lt_to_le. + unfold Not.intro. + apply not_eq_true_false. + rewrite < H5. + apply H3 + [assumption|apply le_n] + |elim H2.assumption + ] + |elim H4. + rewrite > H6. + apply H. + elim H2. + split + [split + [elim (le_to_or_lt_eq ? ? H7) + [apply le_S_S_to_le.assumption + |apply False_ind. + apply not_eq_true_false. + rewrite < H8. + rewrite > H9. + assumption + ] + |assumption + ] + |intros. + apply H3 + [assumption|apply le_S.assumption] + ] + ] + ] +qed. + let rec min_aux off n f \def match f (n-off) with [ true \Rightarrow (n-off) diff --git a/helm/software/matita/library/nat/nth_prime.ma b/helm/software/matita/library/nat/nth_prime.ma index e174266e6..9d01e99f2 100644 --- a/helm/software/matita/library/nat/nth_prime.ma +++ b/helm/software/matita/library/nat/nth_prime.ma @@ -159,6 +159,17 @@ intros.apply (trans_lt O (S O)). unfold lt. apply le_n.apply lt_SO_nth_prime_n. qed. +theorem lt_n_nth_prime_n : \forall n:nat. n \lt nth_prime n. +intro. +elim n + [apply lt_O_nth_prime_n + |apply (lt_to_le_to_lt ? (S (nth_prime n1))) + [unfold.apply le_S_S.assumption + |apply lt_nth_prime_n_nth_prime_Sn + ] + ] +qed. + theorem ex_m_le_n_nth_prime_m: \forall n: nat. nth_prime O \le n \to \exists m. nth_prime m \le n \land n < nth_prime (S m). diff --git a/helm/software/matita/library/nat/ord.ma b/helm/software/matita/library/nat/ord.ma index b7d02f87f..159e8613b 100644 --- a/helm/software/matita/library/nat/ord.ma +++ b/helm/software/matita/library/nat/ord.ma @@ -19,8 +19,6 @@ include "nat/exp.ma". include "nat/gcd.ma". include "nat/relevant_equations.ma". (* required by auto paramod *) -(* this definition of log is based on pairs, with a remainder *) - let rec p_ord_aux p n m \def match n \mod m with [ O \Rightarrow @@ -240,4 +238,204 @@ apply le_to_not_lt. apply divides_to_le.unfold.apply le_n.assumption. rewrite < times_n_SO. apply exp_n_SO. -qed. \ No newline at end of file +qed. + +(* spostare *) +theorem le_plus_to_le: +\forall a,n,m. a + n \le a + m \to n \le m. +intro. +elim a + [assumption + |apply H. + apply le_S_S_to_le.assumption + ] +qed. + +theorem le_times_to_le: +\forall a,n,m. O < a \to a * n \le a * m \to n \le m. +intro. +apply nat_elim2;intros + [apply le_O_n + |apply False_ind. + rewrite < times_n_O in H1. + generalize in match H1. + apply (lt_O_n_elim ? H). + intros. + simplify in H2. + apply (le_to_not_lt ? ? H2). + apply lt_O_S + |apply le_S_S. + apply H + [assumption + |rewrite < times_n_Sm in H2. + rewrite < times_n_Sm in H2. + apply (le_plus_to_le a). + assumption + ] + ] +qed. + +theorem le_exp_to_le: +\forall a,n,m. S O < a \to exp a n \le exp a m \to n \le m. +intro. +apply nat_elim2;intros + [apply le_O_n + |apply False_ind. + apply (le_to_not_lt ? ? H1). + simplify. + rewrite > times_n_SO. + apply lt_to_le_to_lt_times + [assumption + |apply lt_O_exp.apply lt_to_le.assumption + |apply lt_O_exp.apply lt_to_le.assumption + ] + |simplify in H2. + apply le_S_S. + apply H + [assumption + |apply (le_times_to_le a) + [apply lt_to_le.assumption|assumption] + ] + ] +qed. + +theorem divides_to_p_ord: \forall p,a,b,c,d,n,m:nat. +O < n \to O < m \to prime p +\to divides n m \to p_ord n p = pair ? ? a b \to +p_ord m p = pair ? ? c d \to divides b d \land a \le c. +intros. +cut (S O < p) + [lapply (p_ord_to_exp1 ? ? ? ? Hcut H H4). + lapply (p_ord_to_exp1 ? ? ? ? Hcut H1 H5). + elim Hletin. clear Hletin. + elim Hletin1. clear Hletin1. + rewrite > H9 in H3. + split + [apply (gcd_SO_to_divides_times_to_divides (exp p c)) + [elim (le_to_or_lt_eq ? ? (le_O_n b)) + [assumption + |apply False_ind. + apply (lt_to_not_eq O ? H). + rewrite > H7. + rewrite < H10. + auto + ] + |elim c + [rewrite > sym_gcd. + apply gcd_SO_n + |simplify. + apply eq_gcd_times_SO + [apply lt_to_le.assumption + |apply lt_O_exp.apply lt_to_le.assumption + |rewrite > sym_gcd. + (* hint non trova prime_to_gcd_SO e + auto non chiude il goal *) + apply prime_to_gcd_SO + [assumption|assumption] + |assumption + ] + ] + |apply (trans_divides ? n) + [apply (witness ? ? (exp p a)). + rewrite > sym_times. + assumption + |assumption + ] + ] + |apply (le_exp_to_le p) + [assumption + |apply divides_to_le + [apply lt_O_exp.apply lt_to_le.assumption + |apply (gcd_SO_to_divides_times_to_divides d) + [apply lt_O_exp.apply lt_to_le.assumption + |elim a + [apply gcd_SO_n + |simplify.rewrite < sym_gcd. + apply eq_gcd_times_SO + [apply lt_to_le.assumption + |apply lt_O_exp.apply lt_to_le.assumption + |rewrite > sym_gcd. + (* hint non trova prime_to_gcd_SO e + auto non chiude il goal *) + apply prime_to_gcd_SO + [assumption|assumption] + |rewrite > sym_gcd. assumption + ] + ] + |apply (trans_divides ? n) + [apply (witness ? ? b).assumption + |rewrite > sym_times.assumption + ] + ] + ] + ] + ] + |elim H2.assumption + ] +qed. + +definition ord :nat \to nat \to nat \def +\lambda n,p. fst ? ? (p_ord n p). + +definition ord_rem :nat \to nat \to nat \def +\lambda n,p. snd ? ? (p_ord n p). + +theorem divides_to_ord: \forall p,n,m:nat. +O < n \to O < m \to prime p +\to divides n m +\to divides (ord_rem n p) (ord_rem m p) \land (ord n p) \le (ord m p). +intros. +apply (divides_to_p_ord p ? ? ? ? n m H H1 H2 H3) + [unfold ord.unfold ord_rem.apply eq_pair_fst_snd + |unfold ord.unfold ord_rem.apply eq_pair_fst_snd + ] +qed. + +theorem divides_to_divides_ord_rem: \forall p,n,m:nat. +O < n \to O < m \to prime p \to divides n m \to +divides (ord_rem n p) (ord_rem m p). +intros. +elim (divides_to_ord p n m H H1 H2 H3).assumption. +qed. + +theorem divides_to_le_ord: \forall p,n,m:nat. +O < n \to O < m \to prime p \to divides n m \to +(ord n p) \le (ord m p). +intros. +elim (divides_to_ord p n m H H1 H2 H3).assumption. +qed. + +theorem exp_ord: \forall p,n. (S O) \lt p +\to O \lt n \to n = p \sup (ord n p) * (ord_rem n p). +intros. +elim (p_ord_to_exp1 p n (ord n p) (ord_rem n p)) + [assumption + |assumption + |assumption + |unfold ord.unfold ord_rem. + apply eq_pair_fst_snd + ] +qed. + +theorem divides_ord_rem: \forall p,n. (S O) < p \to O < n +\to divides (ord_rem n p) n. +intros. +apply (witness ? ? (p \sup (ord n p))). +rewrite > sym_times. +apply exp_ord[assumption|assumption] +qed. + +theorem lt_O_ord_rem: \forall p,n. (S O) < p \to O < n \to O < ord_rem n p. +intros. +elim (le_to_or_lt_eq O (ord_rem n p)) + [assumption + |apply False_ind. + apply (lt_to_not_eq ? ? H1). + lapply (divides_ord_rem ? ? H H1). + rewrite < H2 in Hletin. + elim Hletin. + rewrite > H3. + reflexivity + |apply le_O_n + ] +qed. diff --git a/helm/software/matita/library/nat/orders.ma b/helm/software/matita/library/nat/orders.ma index 8c6ce942e..8be62ae0b 100644 --- a/helm/software/matita/library/nat/orders.ma +++ b/helm/software/matita/library/nat/orders.ma @@ -201,7 +201,7 @@ apply H2.reflexivity. apply H3. apply le_S_S. assumption. qed. -(* le to eq *) +(* le and eq *) lemma le_to_le_to_eq: \forall n,m. n \le m \to m \le n \to n = m. apply nat_elim2 [intros.apply le_n_O_to_eq.assumption diff --git a/helm/software/matita/library/nat/primes.ma b/helm/software/matita/library/nat/primes.ma index c5fe7bd29..4298eb942 100644 --- a/helm/software/matita/library/nat/primes.ma +++ b/helm/software/matita/library/nat/primes.ma @@ -193,7 +193,7 @@ qed. (* boolean divides *) definition divides_b : nat \to nat \to bool \def \lambda n,m :nat. (eqb (m \mod n) O). - + theorem divides_b_to_Prop : \forall n,m:nat. O < n \to match divides_b n m with @@ -205,7 +205,7 @@ intro.simplify.apply mod_O_to_divides.assumption.assumption. intro.simplify.unfold Not.intro.apply H1.apply divides_to_mod_O.assumption.assumption. qed. -theorem divides_b_true_to_divides : +theorem divides_b_true_to_divides1: \forall n,m:nat. O < n \to (divides_b n m = true ) \to n \divides m. intros. @@ -217,7 +217,21 @@ rewrite < H1.apply divides_b_to_Prop. assumption. qed. -theorem divides_b_false_to_not_divides : +theorem divides_b_true_to_divides: +\forall n,m:nat. divides_b n m = true \to n \divides m. +intros 2.apply (nat_case n) + [apply (nat_case m) + [intro.apply divides_n_n + |simplify.intros.apply False_ind. + apply not_eq_true_false.apply sym_eq.assumption + ] + |intros. + apply divides_b_true_to_divides1 + [apply lt_O_S|assumption] + ] +qed. + +theorem divides_b_false_to_not_divides1: \forall n,m:nat. O < n \to (divides_b n m = false ) \to n \ndivides m. intros. @@ -229,6 +243,22 @@ rewrite < H1.apply divides_b_to_Prop. assumption. qed. +theorem divides_b_false_to_not_divides: +\forall n,m:nat. divides_b n m = false \to n \ndivides m. +intros 2.apply (nat_case n) + [apply (nat_case m) + [simplify.unfold Not.intros. + apply not_eq_true_false.assumption + |unfold Not.intros.elim H1. + apply (not_eq_O_S m1).apply sym_eq. + assumption + ] + |intros. + apply divides_b_false_to_not_divides1 + [apply lt_O_S|assumption] + ] +qed. + theorem decidable_divides: \forall n,m:nat.O < n \to decidable (n \divides m). intros.unfold decidable. @@ -263,6 +293,21 @@ absurd (n \divides m).assumption.assumption. reflexivity. qed. +theorem divides_b_true_to_lt_O: \forall n,m. O < n \to divides_b m n = true \to O < m. +intros. +elim (le_to_or_lt_eq ? ? (le_O_n m)) + [assumption + |apply False_ind. + elim H1. + rewrite < H2 in H1. + simplify in H1. + apply (lt_to_not_eq O n H). + apply sym_eq. + apply eqb_true_to_eq. + assumption + ] +qed. + (* divides and pi *) theorem divides_f_pi_f : \forall f:nat \to nat.\forall n,m,i:nat. m \le i \to i \le n+m \to f i \divides pi n f m. @@ -323,10 +368,8 @@ theorem not_divides_S_fact: \forall n,i:nat. (S O) < i \to i \le n \to i \ndivides S n!. intros. apply divides_b_false_to_not_divides. -apply (trans_lt O (S O)).apply (le_n (S O)).assumption. unfold divides_b. -rewrite > mod_S_fact.simplify.reflexivity. -assumption.assumption. +rewrite > mod_S_fact[simplify.reflexivity|assumption|assumption]. qed. (* prime *) @@ -401,7 +444,6 @@ intro.apply (nat_case m).intro. simplify. apply (witness ? ? (S O)). simplify.reflexivity. intros. apply divides_b_true_to_divides. -apply (lt_O_smallest_factor ? H). change with (eqb ((S(S m1)) \mod (min_aux m1 (S(S m1)) (\lambda m.(eqb ((S(S m1)) \mod m) O)))) O = true). @@ -431,7 +473,6 @@ apply (nat_case n).intro.apply False_ind.apply (not_le_Sn_O (S O) H). intro.apply (nat_case m).intro. apply False_ind.apply (not_le_Sn_n (S O) H). intros. apply divides_b_false_to_not_divides. -apply (trans_lt O (S O)).apply (le_n (S O)).assumption.unfold divides_b. apply (lt_min_aux_to_false (\lambda i:nat.eqb ((S(S m1)) \mod i) O) (S(S m1)) m1 i). cut ((S(S O)) = (S(S m1)-m1)). -- 2.39.2