From da83446deba30fbe32b9bf617d83bd22cc9c9770 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Wed, 14 Sep 2005 07:47:11 +0000 Subject: [PATCH] New version of the library. nth_prime, gcd, log. --- helm/matita/library/nat/div_and_mod.ma | 26 ++ helm/matita/library/nat/exp.ma | 54 ++- helm/matita/library/nat/gcd.ma | 539 ++++++++++++++++++++++++ helm/matita/library/nat/log.ma | 194 +++++++++ helm/matita/library/nat/lt_arith.ma | 56 +++ helm/matita/library/nat/minimization.ma | 33 ++ helm/matita/library/nat/minus.ma | 44 ++ helm/matita/library/nat/nat.ma | 8 + helm/matita/library/nat/nth_prime.ma | 204 +++++++++ helm/matita/library/nat/orders.ma | 52 +++ helm/matita/library/nat/primes.ma | 195 +++------ 11 files changed, 1276 insertions(+), 129 deletions(-) create mode 100644 helm/matita/library/nat/gcd.ma create mode 100644 helm/matita/library/nat/log.ma create mode 100644 helm/matita/library/nat/nth_prime.ma diff --git a/helm/matita/library/nat/div_and_mod.ma b/helm/matita/library/nat/div_and_mod.ma index 8c1e0e953..e4645c307 100644 --- a/helm/matita/library/nat/div_and_mod.ma +++ b/helm/matita/library/nat/div_and_mod.ma @@ -227,6 +227,12 @@ apply div_mod. assumption. qed. +theorem mod_O_n: \forall n:nat.mod O n = O. +intro.elim n.simplify.reflexivity. +simplify.reflexivity. +qed. + + (* injectivity *) theorem injective_times_r: \forall n:nat.injective nat nat (\lambda m:nat.(S n)*m). change with \forall n,p,q:nat.(S n)*p = (S n)*q \to p=q. @@ -240,6 +246,16 @@ qed. variant inj_times_r : \forall n,p,q:nat.(S n)*p = (S n)*q \to p=q \def injective_times_r. +theorem lt_O_to_injective_times_r: \forall n:nat. O < n \to injective nat nat (\lambda m:nat.n*m). +change with \forall n. O < n \to \forall p,q:nat.n*p = n*q \to p=q. +intros 4. +apply lt_O_n_elim n H.intros. +apply inj_times_r m.assumption. +qed. + +variant inj_times_r1:\forall n. O < n \to \forall p,q:nat.n*p = n*q \to p=q +\def lt_O_to_injective_times_r. + theorem injective_times_l: \forall n:nat.injective nat nat (\lambda m:nat.m*(S n)). change with \forall n,p,q:nat.p*(S n) = q*(S n) \to p=q. intros. @@ -251,3 +267,13 @@ qed. variant inj_times_l : \forall n,p,q:nat. p*(S n) = q*(S n) \to p=q \def injective_times_l. + +theorem lt_O_to_injective_times_l: \forall n:nat. O < n \to injective nat nat (\lambda m:nat.m*n). +change with \forall n. O < n \to \forall p,q:nat.p*n = q*n \to p=q. +intros 4. +apply lt_O_n_elim n H.intros. +apply inj_times_l m.assumption. +qed. + +variant inj_times_l1:\forall n. O < n \to \forall p,q:nat.p*n = q*n \to p=q +\def lt_O_to_injective_times_l. \ No newline at end of file diff --git a/helm/matita/library/nat/exp.ma b/helm/matita/library/nat/exp.ma index 6fcd9da0e..2f0bfbeaf 100644 --- a/helm/matita/library/nat/exp.ma +++ b/helm/matita/library/nat/exp.ma @@ -15,6 +15,8 @@ set "baseuri" "cic:/matita/nat/exp". include "nat/times.ma". +include "nat/orders.ma". +include "higher_order_defs/functions.ma". let rec exp n m on m\def match m with @@ -43,4 +45,54 @@ intros. elim q.simplify.rewrite < times_n_O.simplify.reflexivity. simplify.rewrite > H.rewrite < exp_plus_times. rewrite < times_n_Sm.reflexivity. -qed. \ No newline at end of file +qed. + +theorem lt_O_exp: \forall n,m:nat. O < n \to O < exp n m. +intros.elim m.simplify.apply le_n. +simplify.rewrite > times_n_SO. +apply le_times.assumption.assumption. +qed. + +theorem lt_m_exp_nm: \forall n,m:nat. (S O) < n \to m < exp n m. +intros.elim m.simplify.reflexivity. +simplify. +apply trans_le ? ((S(S O))*(S n1)). +simplify. +rewrite < plus_n_Sm.apply le_S_S.apply le_S_S. +rewrite < sym_plus. +apply le_plus_n. +apply le_times.assumption.assumption. +qed. + +theorem exp_to_eq_O: \forall n,m:nat. (S O) < n +\to exp n m = (S O) \to m = O. +intros.apply antisym_le.apply le_S_S_to_le. +rewrite < H1.change with m < exp n m. +apply lt_m_exp_nm.assumption. +apply le_O_n. +qed. + +theorem injective_exp_r: \forall n:nat. (S O) < n \to +injective nat nat (\lambda m:nat. exp n m). +simplify.intros 4. +apply nat_elim2 (\lambda x,y.exp n x = exp n y \to x = y). +intros.apply sym_eq.apply exp_to_eq_O n.assumption. +rewrite < H1.reflexivity. +intros.apply exp_to_eq_O n.assumption.assumption. +intros.apply eq_f. +apply H1. +(* esprimere inj_times senza S *) +cut \forall a,b:nat.O < n \to n*a=n*b \to a=b. +apply Hcut.simplify. apply le_S_S_to_le. apply le_S. assumption. +assumption. +intros 2. +apply nat_case n. +intros.apply False_ind.apply not_le_Sn_O O H3. +intros.apply inj_times_r m1.assumption. +qed. + +variant inj_exp_r: \forall p:nat. (S O) < p \to \forall n,m:nat. +(exp p n) = (exp p m) \to n = m \def +injective_exp_r. + + diff --git a/helm/matita/library/nat/gcd.ma b/helm/matita/library/nat/gcd.ma new file mode 100644 index 000000000..5a2fd4647 --- /dev/null +++ b/helm/matita/library/nat/gcd.ma @@ -0,0 +1,539 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| A.Asperti, C.Sacerdoti Coen, *) +(* ||A|| E.Tassi, S.Zacchiroli *) +(* \ / *) +(* \ / Matita is distributed under the terms of the *) +(* v GNU Lesser General Public License Version 2.1 *) +(* *) +(**************************************************************************) + +set "baseuri" "cic:/matita/nat/gcd". + +include "nat/primes.ma". +include "higher_order_defs/functions.ma". + +let rec gcd_aux p m n: nat \def +match divides_b n m with +[ true \Rightarrow n +| false \Rightarrow + match p with + [O \Rightarrow n + |(S q) \Rightarrow gcd_aux q n (mod m n)]]. + +definition gcd : nat \to nat \to nat \def +\lambda n,m:nat. + match leb n m with + [ true \Rightarrow + match n with + [ O \Rightarrow m + | (S p) \Rightarrow gcd_aux (S p) m (S p) ] + | false \Rightarrow + match m with + [ O \Rightarrow n + | (S p) \Rightarrow gcd_aux (S p) n (S p) ]]. + +theorem divides_mod: \forall p,m,n:nat. O < n \to divides p m \to divides p n \to +divides p (mod m n). +intros.elim H1.elim H2. +apply witness ? ? (n2 - n1*(div m n)). +rewrite > distr_times_minus. +rewrite < H3. +rewrite < assoc_times. +rewrite < H4. +apply sym_eq. +apply plus_to_minus. +rewrite > div_mod m n in \vdash (? ? %). +rewrite > sym_times. +apply eq_plus_to_le ? ? (mod m n). +reflexivity. +rewrite > sym_times. +apply div_mod.assumption. assumption. +qed. + +theorem divides_mod_to_divides: \forall p,m,n:nat. O < n \to +divides p (mod m n) \to divides p n \to divides p m. +intros.elim H1.elim H2. +apply witness p m ((n1*(div m n))+n2). +rewrite > distr_times_plus. +rewrite < H3. +rewrite < assoc_times. +rewrite < H4.rewrite < sym_times. +apply div_mod.assumption. +qed. + +theorem divides_gcd_aux_mn: \forall p,m,n. O < n \to n \le m \to n \le p \to +divides (gcd_aux p m n) m \land divides (gcd_aux p m n) n. +intro.elim p. +absurd O < n.assumption.apply le_to_not_lt.assumption. +cut (divides n1 m) \lor \not (divides n1 m). +change with +(divides +(match divides_b n1 m with +[ true \Rightarrow n1 +| false \Rightarrow gcd_aux n n1 (mod m n1)]) m) \land +(divides +(match divides_b n1 m with +[ true \Rightarrow n1 +| false \Rightarrow gcd_aux n n1 (mod m n1)]) n1). +elim Hcut.rewrite > divides_to_divides_b_true. +simplify. +split.assumption.apply witness n1 n1 (S O).apply times_n_SO. +rewrite > not_divides_to_divides_b_false. +change with +(divides (gcd_aux n n1 (mod m n1)) m) \land +(divides (gcd_aux n n1 (mod m n1)) n1). +cut (divides (gcd_aux n n1 (mod m n1)) n1) \land +(divides (gcd_aux n n1 (mod m n1)) (mod m n1)). +elim Hcut1. +split.apply divides_mod_to_divides ? ? n1. +assumption.assumption.assumption.assumption. +apply H. +cut O \lt mod m n1 \lor O = mod m n1. +elim Hcut1.assumption. +apply False_ind.apply H4.apply mod_O_to_divides. +assumption.apply sym_eq.assumption. +apply le_to_or_lt_eq.apply le_O_n. +apply lt_to_le. +apply lt_mod_m_m.assumption. +apply le_S_S_to_le. +apply trans_le ? n1. +change with mod m n1 < n1. +apply lt_mod_m_m.assumption.assumption. +apply decidable_divides n1 m.assumption. +apply lt_to_le_to_lt ? n1.assumption.reflexivity. +assumption. +assumption.assumption. +qed. + +theorem divides_gcd_nm: \forall n,m. +divides (gcd n m) m \land divides (gcd n m) n. +intros. +change with +divides +(match leb n m with + [ true \Rightarrow + match n with + [ O \Rightarrow m + | (S p) \Rightarrow gcd_aux (S p) m (S p) ] + | false \Rightarrow + match m with + [ O \Rightarrow n + | (S p) \Rightarrow gcd_aux (S p) n (S p) ]]) m +\land + divides +(match leb n m with + [ true \Rightarrow + match n with + [ O \Rightarrow m + | (S p) \Rightarrow gcd_aux (S p) m (S p) ] + | false \Rightarrow + match m with + [ O \Rightarrow n + | (S p) \Rightarrow gcd_aux (S p) n (S p) ]]) n. +apply leb_elim n m. +apply nat_case1 n. +simplify.intros.split. +apply witness m m (S O).apply times_n_SO. +apply witness m O O.apply times_n_O. +intros.change with +divides (gcd_aux (S m1) m (S m1)) m +\land +divides (gcd_aux (S m1) m (S m1)) (S m1). +apply divides_gcd_aux_mn. +simplify.apply le_S_S.apply le_O_n. +assumption.apply le_n. +simplify.intro. +apply nat_case1 m. +simplify.intros.split. +apply witness n O O.apply times_n_O. +apply witness n n (S O).apply times_n_SO. +intros.change with +divides (gcd_aux (S m1) n (S m1)) (S m1) +\land +divides (gcd_aux (S m1) n (S m1)) n. +cut divides (gcd_aux (S m1) n (S m1)) n +\land +divides (gcd_aux (S m1) n (S m1)) (S m1). +elim Hcut.split.assumption.assumption. +apply divides_gcd_aux_mn. +simplify.apply le_S_S.apply le_O_n. +apply not_lt_to_le.simplify.intro.apply H. +rewrite > H1.apply trans_le ? (S n). +apply le_n_Sn.assumption.apply le_n. +qed. + +theorem divides_gcd_n: \forall n,m. +divides (gcd n m) n. +intros. +exact proj2 ? ? (divides_gcd_nm n m). +qed. + +theorem divides_gcd_m: \forall n,m. +divides (gcd n m) m. +intros. +exact proj1 ? ? (divides_gcd_nm n m). +qed. + +theorem divides_gcd_aux: \forall p,m,n,d. O < n \to n \le m \to n \le p \to +divides d m \to divides d n \to divides d (gcd_aux p m n). +intro.elim p. +absurd O < n.assumption.apply le_to_not_lt.assumption. +change with +divides d +(match divides_b n1 m with +[ true \Rightarrow n1 +| false \Rightarrow gcd_aux n n1 (mod m n1)]). +cut divides n1 m \lor \not (divides n1 m). +elim Hcut. +rewrite > divides_to_divides_b_true. +simplify.assumption. +rewrite > not_divides_to_divides_b_false. +change with divides d (gcd_aux n n1 (mod m n1)). +apply H. +cut O \lt mod m n1 \lor O = mod m n1. +elim Hcut1.assumption. +absurd divides n1 m.apply mod_O_to_divides. +assumption.apply sym_eq.assumption.assumption. +apply le_to_or_lt_eq.apply le_O_n. +apply lt_to_le. +apply lt_mod_m_m.assumption. +apply le_S_S_to_le. +apply trans_le ? n1. +change with mod m n1 < n1. +apply lt_mod_m_m.assumption.assumption. +assumption. +apply divides_mod.assumption.assumption.assumption. +apply decidable_divides n1 m.assumption. +apply lt_to_le_to_lt ? n1.assumption.reflexivity. +assumption.assumption.assumption. +qed. + +theorem divides_d_gcd: \forall m,n,d. +divides d m \to divides d n \to divides d (gcd n m). +intros. +change with +divides d ( +match leb n m with + [ true \Rightarrow + match n with + [ O \Rightarrow m + | (S p) \Rightarrow gcd_aux (S p) m (S p) ] + | false \Rightarrow + match m with + [ O \Rightarrow n + | (S p) \Rightarrow gcd_aux (S p) n (S p) ]]). +apply leb_elim n m. +apply nat_case1 n.simplify.intros.assumption. +intros. +change with divides d (gcd_aux (S m1) m (S m1)). +apply divides_gcd_aux. +simplify.apply le_S_S.apply le_O_n.assumption.apply le_n.assumption. +rewrite < H2.assumption. +apply nat_case1 m.simplify.intros.assumption. +intros. +change with divides d (gcd_aux (S m1) n (S m1)). +apply divides_gcd_aux. +simplify.apply le_S_S.apply le_O_n. +apply lt_to_le.apply not_le_to_lt.assumption.apply le_n.assumption. +rewrite < H2.assumption. +qed. + +theorem eq_minus_gcd_aux: \forall p,m,n.O < n \to n \le m \to n \le p \to +ex nat (\lambda a. ex nat (\lambda b. +a*n - b*m = (gcd_aux p m n) \lor b*m - a*n = (gcd_aux p m n))). +intro. +elim p. +absurd O < n.assumption.apply le_to_not_lt.assumption. +cut O < m. +cut (divides n1 m) \lor \not (divides n1 m). +change with +ex nat (\lambda a. ex nat (\lambda b. +a*n1 - b*m = match divides_b n1 m with +[ true \Rightarrow n1 +| false \Rightarrow gcd_aux n n1 (mod m n1)] +\lor +b*m - a*n1 = match divides_b n1 m with +[ true \Rightarrow n1 +| false \Rightarrow gcd_aux n n1 (mod m n1)])). +elim Hcut1. +rewrite > divides_to_divides_b_true. +simplify. +apply ex_intro ? ? (S O). +apply ex_intro ? ? O. +left.simplify.rewrite < plus_n_O. +apply sym_eq.apply minus_n_O. +rewrite > not_divides_to_divides_b_false. +change with +ex nat (\lambda a. ex nat (\lambda b. +a*n1 - b*m = gcd_aux n n1 (mod m n1) +\lor +b*m - a*n1 = gcd_aux n n1 (mod m n1))). +cut +ex nat (\lambda a. ex nat (\lambda b. +a*(mod m n1) - b*n1= gcd_aux n n1 (mod m n1) +\lor +b*n1 - a*(mod m n1) = gcd_aux n n1 (mod m n1))). +elim Hcut2.elim H5.elim H6. +(* first case *) +rewrite < H7. +apply ex_intro ? ? (a1+a*(div m n1)). +apply ex_intro ? ? a. +right. +rewrite < sym_plus. +rewrite < sym_times n1. +rewrite > distr_times_plus. +rewrite > sym_times n1. +rewrite > sym_times n1. +rewrite > div_mod m n1 in \vdash (? ? (? % ?) ?). +rewrite > assoc_times. +rewrite < sym_plus. +rewrite > distr_times_plus. +rewrite < eq_minus_minus_minus_plus. +rewrite < sym_plus. +rewrite < plus_minus. +rewrite < minus_n_n.reflexivity. +(* second case *) +rewrite < H7. +apply ex_intro ? ? (a1+a*(div m n1)). +apply ex_intro ? ? a. +left. +rewrite > sym_times. +rewrite > distr_times_plus. +rewrite > sym_times. +rewrite > sym_times n1. +rewrite > div_mod m n1 in \vdash (? ? (? ? %) ?). +rewrite > distr_times_plus. +rewrite > assoc_times. +rewrite < eq_minus_minus_minus_plus. +rewrite < sym_plus. +rewrite < plus_minus. +rewrite < minus_n_n.reflexivity. +(* end second case *) +apply H n1 (mod m n1). +(* a lot of trivialities left *) +cut O \lt mod m n1 \lor O = mod m n1. +elim Hcut2.assumption. +absurd divides n1 m.apply mod_O_to_divides. +assumption.apply sym_eq.assumption.assumption. +apply le_to_or_lt_eq.apply le_O_n. +apply lt_to_le. +apply lt_mod_m_m.assumption. +apply le_S_S_to_le. +apply trans_le ? n1. +change with mod m n1 < n1. +apply lt_mod_m_m.assumption.assumption. +apply decidable_divides n1 m.assumption. +apply lt_to_le_to_lt ? n1.assumption.assumption. +assumption.assumption.assumption.assumption.assumption. +apply le_n.assumption. +apply le_n. +qed. + +theorem eq_minus_gcd: \forall m,n. +ex nat (\lambda a. ex nat (\lambda b. +a*n - b*m = (gcd n m) \lor b*m - a*n = (gcd n m))). +intros. +change with +ex nat (\lambda a. ex nat (\lambda b. +a*n - b*m = +match leb n m with + [ true \Rightarrow + match n with + [ O \Rightarrow m + | (S p) \Rightarrow gcd_aux (S p) m (S p) ] + | false \Rightarrow + match m with + [ O \Rightarrow n + | (S p) \Rightarrow gcd_aux (S p) n (S p) ]] +\lor b*m - a*n = +match leb n m with + [ true \Rightarrow + match n with + [ O \Rightarrow m + | (S p) \Rightarrow gcd_aux (S p) m (S p) ] + | false \Rightarrow + match m with + [ O \Rightarrow n + | (S p) \Rightarrow gcd_aux (S p) n (S p) ]] +)). +apply leb_elim n m. +apply nat_case1 n. +simplify.intros. +apply ex_intro ? ? O. +apply ex_intro ? ? (S O). +right.simplify. +rewrite < plus_n_O. +apply sym_eq.apply minus_n_O. +intros. +change with +ex nat (\lambda a. ex nat (\lambda b. +a*(S m1) - b*m = (gcd_aux (S m1) m (S m1)) +\lor b*m - a*(S m1) = (gcd_aux (S m1) m (S m1)))). +apply eq_minus_gcd_aux. +simplify. apply le_S_S.apply le_O_n. +assumption.apply le_n. +apply nat_case1 m. +simplify.intros. +apply ex_intro ? ? (S O). +apply ex_intro ? ? O. +left.simplify. +rewrite < plus_n_O. +apply sym_eq.apply minus_n_O. +intros. +change with +ex nat (\lambda a. ex nat (\lambda b. +a*n - b*(S m1) = (gcd_aux (S m1) n (S m1)) +\lor b*(S m1) - a*n = (gcd_aux (S m1) n (S m1)))). +cut +ex nat (\lambda a. ex nat (\lambda b. +a*(S m1) - b*n = (gcd_aux (S m1) n (S m1)) +\lor +b*n - a*(S m1) = (gcd_aux (S m1) n (S m1)))). +elim Hcut.elim H2.elim H3. +apply ex_intro ? ? a1. +apply ex_intro ? ? a. +right.assumption. +apply ex_intro ? ? a1. +apply ex_intro ? ? a. +left.assumption. +apply eq_minus_gcd_aux. +simplify. apply le_S_S.apply le_O_n. +apply lt_to_le.apply not_le_to_lt.assumption. +apply le_n. +qed. + +(* some properties of gcd *) + +theorem gcd_O_n: \forall n:nat. gcd O n = n. +intro.simplify.reflexivity. +qed. + +theorem gcd_O_to_eq_O:\forall m,n:nat. (gcd m n) = O \to +m = O \land n = O. +intros.cut divides O n \land divides O m. +elim Hcut.elim H2.split. +assumption.elim H1.assumption. +rewrite < H. +apply divides_gcd_nm. +qed. + +theorem symmetric_gcd: symmetric nat gcd. +change with +\forall n,m:nat. gcd n m = gcd m n. +intros. +cut O < (gcd n m) \lor O = (gcd n m). +elim Hcut. +cut O < (gcd m n) \lor O = (gcd m n). +elim Hcut1. +apply antisym_le. +apply divides_to_le.assumption. +apply divides_d_gcd.apply divides_gcd_n.apply divides_gcd_m. +apply divides_to_le.assumption. +apply divides_d_gcd.apply divides_gcd_n.apply divides_gcd_m. +rewrite < H1. +cut m=O \land n=O. +elim Hcut2.rewrite > H2.rewrite > H3.reflexivity. +apply gcd_O_to_eq_O.apply sym_eq.assumption. +apply le_to_or_lt_eq.apply le_O_n. +rewrite < H. +cut n=O \land m=O. +elim Hcut1.rewrite > H1.rewrite > H2.reflexivity. +apply gcd_O_to_eq_O.apply sym_eq.assumption. +apply le_to_or_lt_eq.apply le_O_n. +qed. + +variant sym_gcd: \forall n,m:nat. gcd n m = gcd m n \def +symmetric_gcd. + +theorem gcd_SO_n: \forall n:nat. gcd (S O) n = (S O). +intro. +apply antisym_le.apply divides_to_le.simplify.apply le_n. +apply divides_gcd_n. +cut O < gcd (S O) n \lor O = gcd (S O) n. +elim Hcut.assumption. +apply False_ind. +apply not_eq_O_S O. +cut (S O)=O \land n=O. +elim Hcut1.apply sym_eq.assumption. +apply gcd_O_to_eq_O.apply sym_eq.assumption. +apply le_to_or_lt_eq.apply le_O_n. +qed. + +theorem prime_to_gcd_SO: \forall n,m:nat. prime n \to \not (divides n m) \to +gcd n m = (S O). +intros.simplify in H.change with gcd n m = (S O). +elim H. +apply antisym_le. +apply not_lt_to_le. +change with (S (S O)) \le gcd n m \to False.intro. +apply H1.rewrite < H3 (gcd n m). +apply divides_gcd_m. +cut O < gcd n m \lor O = gcd n m. +elim Hcut.assumption. +apply False_ind. +apply not_le_Sn_O (S O). +cut n=O \land m=O. +elim Hcut1.rewrite < H5 in \vdash (? ? %).assumption. +apply gcd_O_to_eq_O.apply sym_eq.assumption. +apply le_to_or_lt_eq.apply le_O_n. +apply divides_gcd_n.assumption. +qed. + +(* esempio di sfarfallalmento !!! *) +(* +theorem bad: \forall n,p,q:nat.prime n \to divides n (p*q) \to +divides n p \lor divides n q. +intros. +cut divides n p \lor \not (divides n p). +elim Hcut.left.assumption. +right. +cut ex nat (\lambda a. ex nat (\lambda b. +a*n - b*p = (S O) \lor b*p - a*n = (S O))). +elim Hcut1.elim H3.*) + +theorem divides_times_to_divides: \forall n,p,q:nat.prime n \to divides n (p*q) \to +divides n p \lor divides n q. +intros. +cut divides n p \lor \not (divides n p). +elim Hcut. +left.assumption. +right. +cut ex nat (\lambda a. ex nat (\lambda b. +a*n - b*p = (S O) \lor b*p - a*n = (S O))). +elim Hcut1.elim H3.elim H4. +(* first case *) +rewrite > times_n_SO q.rewrite < H5. +rewrite > distr_times_minus. +rewrite > sym_times q (a1*p). +rewrite > assoc_times a1. +elim H1.rewrite > H6. +rewrite < sym_times n.rewrite < assoc_times. +rewrite > sym_times q.rewrite > assoc_times. +rewrite < assoc_times a1.rewrite < sym_times n. +rewrite > assoc_times n. +rewrite < distr_times_minus. +apply witness ? ? (q*a-a1*n2).reflexivity. +(* second case *) +rewrite > times_n_SO q.rewrite < H5. +rewrite > distr_times_minus. +rewrite > sym_times q (a1*p). +rewrite > assoc_times a1. +elim H1.rewrite > H6. +rewrite < sym_times.rewrite > assoc_times. +rewrite < assoc_times q. +rewrite < sym_times n. +rewrite < distr_times_minus. +apply witness ? ? (n2*a1-q*a).reflexivity. +(* end second case *) +rewrite < prime_to_gcd_SO n p. +apply eq_minus_gcd. +apply decidable_divides n p. +apply trans_lt ? (S O).simplify.apply le_n. +simplify in H.elim H. assumption. +assumption.assumption. +qed. diff --git a/helm/matita/library/nat/log.ma b/helm/matita/library/nat/log.ma new file mode 100644 index 000000000..9f32777b3 --- /dev/null +++ b/helm/matita/library/nat/log.ma @@ -0,0 +1,194 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| A.Asperti, C.Sacerdoti Coen, *) +(* ||A|| E.Tassi, S.Zacchiroli *) +(* \ / *) +(* \ / Matita is distributed under the terms of the *) +(* v GNU Lesser General Public License Version 2.1 *) +(* *) +(**************************************************************************) + +set "baseuri" "cic:/matita/nat/log". + +include "datatypes/constructors.ma". +include "nat/primes.ma". +include "nat/exp.ma". + +(* this definition of log is based on pairs, with a remainder *) + +let rec plog_aux p n m \def + match (mod n m) with + [ O \Rightarrow + match p with + [ O \Rightarrow pair nat nat O n + | (S p) \Rightarrow + match (plog_aux p (div n m) m) with + [ (pair q r) \Rightarrow pair nat nat (S q) r]] + | (S a) \Rightarrow pair nat nat O n]. + +(* plog n m = if m divides n q times, with remainder r *) +definition plog \def \lambda n,m:nat.plog_aux n n m. + +theorem plog_aux_to_Prop: \forall p,n,m. O < m \to + match plog_aux p n m with + [ (pair q r) \Rightarrow n = (exp m q)*r ]. +intro. +elim p. +change with +match ( +match (mod n m) with + [ O \Rightarrow pair nat nat O n + | (S a) \Rightarrow pair nat nat O n] ) +with + [ (pair q r) \Rightarrow n = (exp m q)*r ]. +apply nat_case (mod n m). +simplify.apply plus_n_O. +intros. +simplify.apply plus_n_O. +change with +match ( +match (mod n1 m) with + [ O \Rightarrow + match (plog_aux n (div n1 m) m) with + [ (pair q r) \Rightarrow pair nat nat (S q) r] + | (S a) \Rightarrow pair nat nat O n1] ) +with + [ (pair q r) \Rightarrow n1 = (exp m q)*r]. +apply nat_case1 (mod n1 m).intro. +change with +match ( + match (plog_aux n (div n1 m) m) with + [ (pair q r) \Rightarrow pair nat nat (S q) r]) +with + [ (pair q r) \Rightarrow n1 = (exp m q)*r]. +generalize in match (H (div n1 m) m). +elim plog_aux n (div n1 m) m. +simplify. +rewrite > assoc_times. +rewrite < H3.rewrite > plus_n_O (m*(div n1 m)). +rewrite < H2. +rewrite > sym_times. +rewrite < div_mod.reflexivity. +intros.simplify.apply plus_n_O. +assumption.assumption. +qed. + +theorem plog_aux_to_exp: \forall p,n,m,q,r. O < m \to + (pair nat nat q r) = plog_aux p n m \to n = (exp m q)*r. +intros. +change with +match (pair nat nat q r) with + [ (pair q r) \Rightarrow n = (exp m q)*r ]. +rewrite > H1. +apply plog_aux_to_Prop. +assumption. +qed. +(* questo va spostato in primes1.ma *) +theorem plog_exp: \forall n,m,i. O < m \to \not (mod n m = O) \to +\forall p. i \le p \to plog_aux p ((exp m i)*n) m = pair nat nat i n. +intros 5. +elim i. +simplify. +rewrite < plus_n_O. +apply nat_case p. +change with + match (mod n m) with + [ O \Rightarrow pair nat nat O n + | (S a) \Rightarrow pair nat nat O n] + = pair nat nat O n. +elim (mod n m).simplify.reflexivity.simplify.reflexivity. +intro. +change with + match (mod n m) with + [ O \Rightarrow + match (plog_aux m1 (div n m) m) with + [ (pair q r) \Rightarrow pair nat nat (S q) r] + | (S a) \Rightarrow pair nat nat O n] + = pair nat nat O n. +cut O < mod n m \lor O = mod n m. +elim Hcut.apply lt_O_n_elim (mod n m) H3. +intros. simplify.reflexivity. +apply False_ind. +apply H1.apply sym_eq.assumption. +apply le_to_or_lt_eq.apply le_O_n. +generalize in match H3. +apply nat_case p.intro.apply False_ind.apply not_le_Sn_O n1 H4. +intros. +change with + match (mod ((exp m (S n1))*n) m) with + [ O \Rightarrow + match (plog_aux m1 (div ((exp m (S n1))*n) m) m) with + [ (pair q r) \Rightarrow pair nat nat (S q) r] + | (S a) \Rightarrow pair nat nat O ((exp m (S n1))*n)] + = pair nat nat (S n1) n. +cut (mod ((exp m (S n1))*n) m) = O. +rewrite > Hcut. +change with +match (plog_aux m1 (div ((exp m (S n1))*n) m) m) with + [ (pair q r) \Rightarrow pair nat nat (S q) r] + = pair nat nat (S n1) n. +cut div ((exp m (S n1))*n) m = (exp m n1)*n. +rewrite > Hcut1. +rewrite > H2 m1. simplify.reflexivity. +(* div_exp *) +change with div (m*(exp m n1)*n) m = (exp m n1)*n. +rewrite > assoc_times. +apply lt_O_n_elim m H. +intro.apply div_times. +(* mod_exp = O *) +apply divides_to_mod_O. +assumption. +simplify.rewrite > assoc_times. +apply witness ? ? ((exp m n1)*n).reflexivity. +apply le_S_S_to_le.assumption. +qed. + +theorem plog_aux_to_Prop1: \forall p,n,m. (S O) < m \to O < n \to n \le p \to + match plog_aux p n m with + [ (pair q r) \Rightarrow \lnot (mod r m = O)]. +intro.elim p.absurd O < n.assumption. +apply le_to_not_lt.assumption. +change with +match + (match (mod n1 m) with + [ O \Rightarrow + match (plog_aux n(div n1 m) m) with + [ (pair q r) \Rightarrow pair nat nat (S q) r] + | (S a) \Rightarrow pair nat nat O n1]) +with + [ (pair q r) \Rightarrow \lnot(mod r m = O)]. +apply nat_case1 (mod n1 m).intro. +generalize in match (H (div n1 m) m). +elim (plog_aux n (div n1 m) m). +apply H5.assumption. +apply eq_mod_O_to_lt_O_div. +apply trans_lt ? (S O).simplify.apply le_n. +assumption.assumption.assumption. +apply le_S_S_to_le. +apply trans_le ? n1.change with div n1 m < n1. +apply lt_div_n_m_n.assumption.assumption.assumption. +intros. +change with (\lnot (mod n1 m = O)). +rewrite > H4. +(* META NOT FOUND !!! +rewrite > sym_eq. *) +simplify.intro. +apply not_eq_O_S m1 ?. +rewrite > H5.reflexivity. +qed. + +theorem plog_aux_to_not_mod_O: \forall p,n,m,q,r. (S O) < m \to O < n \to n \le p \to + pair nat nat q r = plog_aux p n m \to \lnot (mod r m = O). +intros. +change with + match (pair nat nat q r) with + [ (pair q r) \Rightarrow \lnot (mod r m = O)]. +rewrite > H3. +apply plog_aux_to_Prop1. +assumption.assumption.assumption. +qed. + diff --git a/helm/matita/library/nat/lt_arith.ma b/helm/matita/library/nat/lt_arith.ma index 9494a28d7..85280fe0f 100644 --- a/helm/matita/library/nat/lt_arith.ma +++ b/helm/matita/library/nat/lt_arith.ma @@ -14,6 +14,7 @@ set "baseuri" "cic:/matita/nat/lt_arith". +include "nat/exp.ma". include "nat/div_and_mod.ma". (* plus *) @@ -161,3 +162,58 @@ apply lt_to_not_eq.assumption. intro.reflexivity. qed. +(* div *) + +theorem eq_mod_O_to_lt_O_div: \forall n,m:nat. O < m \to O < n\to mod n m = O \to O < div n m. +intros 4.apply lt_O_n_elim m H.intros. +apply lt_times_to_lt_r m1. +rewrite < times_n_O. +rewrite > plus_n_O ((S m1)*(div n (S m1))). +rewrite < H2. +rewrite < sym_times. +rewrite < div_mod. +rewrite > H2. +assumption. +simplify.apply le_S_S.apply le_O_n. +qed. + +theorem lt_div_n_m_n: \forall n,m:nat. (S O) < m \to O < n \to div n m \lt n. +intros. +apply nat_case1 (div n m).intro. +assumption.intros.rewrite < H2. +rewrite > (div_mod n m) in \vdash (? ? %). +apply lt_to_le_to_lt ? ((div n m)*m). +apply lt_to_le_to_lt ? ((div n m)*(S (S O))). +rewrite < sym_times. +rewrite > H2. +simplify. +rewrite < plus_n_O. +rewrite < plus_n_Sm. +apply le_S_S. +apply le_S_S. +apply le_plus_n. +apply le_times_r. +assumption. +rewrite < sym_plus. +apply le_plus_n. +apply trans_lt ? (S O). +simplify. apply le_n.assumption. +qed. + +(* general properties of functions *) +theorem monotonic_to_injective: \forall f:nat\to nat. +monotonic nat lt f \to injective nat nat f. +simplify.intros. +apply nat_compare_elim x y. +intro.apply False_ind.apply not_le_Sn_n (f x). +rewrite > H1 in \vdash (? ? %).apply H.apply H2. +intros.assumption. +intro.apply False_ind.apply not_le_Sn_n (f y). +rewrite < H1 in \vdash (? ? %).apply H.apply H2. +qed. + +theorem increasing_to_injective: \forall f:nat\to nat. +increasing f \to injective nat nat f. +intros.apply monotonic_to_injective. +apply increasing_to_monotonic.assumption. +qed. \ No newline at end of file diff --git a/helm/matita/library/nat/minimization.ma b/helm/matita/library/nat/minimization.ma index da76606b4..5eaa02cc3 100644 --- a/helm/matita/library/nat/minimization.ma +++ b/helm/matita/library/nat/minimization.ma @@ -40,6 +40,39 @@ simplify.left.split.reflexivity.reflexivity. simplify.right.split.reflexivity.reflexivity. qed. +theorem le_max_n : \forall f: nat \to bool. \forall n:nat. +max n f \le n. +intros.elim n.rewrite > max_O_f.apply le_n. +simplify.elim (f (S n1)).simplify.apply le_n. +simplify.apply le_S.assumption. +qed. + +theorem le_to_le_max : \forall f: nat \to bool. \forall n,m:nat. +n\le m \to max n f \le max m f. +intros.elim H. +apply le_n. +apply trans_le ? (max n1 f).apply H2. +cut (f (S n1) = true \land max (S n1) f = (S n1)) \lor +(f (S n1) = false \land max (S n1) f = max n1 f). +elim Hcut.elim H3. +rewrite > H5. +apply le_S.apply le_max_n. +elim H3.rewrite > H5.apply le_n. +apply max_S_max. +qed. + +theorem f_m_to_le_max: \forall f: nat \to bool. \forall n,m:nat. +m\le n \to f m = true \to m \le max n f. +intros 3.elim n.apply le_n_O_elim m H. +apply le_O_n. +apply le_n_Sm_elim m n1 H1. +intro.apply trans_le ? (max n1 f). +apply H.apply le_S_S_to_le.assumption.assumption. +apply le_to_le_max.apply le_n_Sn. +intro.simplify.rewrite < H3. +rewrite > H2.simplify.apply le_n. +qed. + definition max_spec \def \lambda f:nat \to bool.\lambda n: nat. ex nat (\lambda i:nat. (le i n) \land (f i = true)) \to (f n) = true \land (\forall i. i < n \to (f i = false)). diff --git a/helm/matita/library/nat/minus.ma b/helm/matita/library/nat/minus.ma index 7945a76e0..6ff744dcb 100644 --- a/helm/matita/library/nat/minus.ma +++ b/helm/matita/library/nat/minus.ma @@ -153,6 +153,12 @@ intros.simplify.apply le_n. intros.simplify.apply le_S.assumption. qed. +theorem lt_minus_m: \forall n,m:nat. O < n \to O < m \to n-m \lt n. +intros.apply lt_O_n_elim n H.intro. +apply lt_O_n_elim m H1.intro. +simplify.apply le_S_S.apply le_minus_m. +qed. + theorem minus_le_O_to_le: \forall n,m:nat. n-m \leq O \to n \leq m. intros 2. apply nat_elim2 (\lambda n,m:nat.n-m \leq O \to n \leq m). @@ -232,3 +238,41 @@ qed. theorem distr_times_minus: \forall n,m,p:nat. n*(m-p) = n*m-n*p \def distributive_times_minus. +theorem eq_minus_minus_minus_plus: \forall n,m,p:nat. (n-m)-p = n-(m+p). +intros. +cut m+p \le n \or \not m+p \le n. +elim Hcut. +apply sym_eq. +apply plus_to_minus.assumption. +rewrite > assoc_plus. +rewrite > sym_plus p. +rewrite < plus_minus_m_m. +rewrite > sym_plus. +rewrite < plus_minus_m_m.reflexivity. +rewrite > eq_minus_n_m_O n (m+p). +rewrite > eq_minus_n_m_O (n-m) p.reflexivity. +apply decidable_le (m+p) n. +apply le_plus_to_minus_r. +rewrite > sym_plus.assumption. +apply trans_le ? (m+p). +rewrite < sym_plus. +apply le_plus_n.assumption. +apply lt_to_le.apply not_le_to_lt.assumption. +apply le_plus_to_minus. +apply lt_to_le.apply not_le_to_lt. +rewrite < sym_plus.assumption. +qed. + +theorem eq_plus_minus_minus_minus: \forall n,m,p:nat. p \le m \to m \le n \to +p+(n-m) = n-(m-p). +intros. +apply sym_eq. +apply plus_to_minus. +apply le_plus_to_minus. +apply trans_le ? n.assumption.rewrite < sym_plus.apply le_plus_n. +rewrite < assoc_plus. +rewrite < plus_minus_m_m. +rewrite < sym_plus. +rewrite < plus_minus_m_m.reflexivity. +assumption.assumption. +qed. diff --git a/helm/matita/library/nat/nat.ma b/helm/matita/library/nat/nat.ma index df045daa7..c85bb25c2 100644 --- a/helm/matita/library/nat/nat.ma +++ b/helm/matita/library/nat/nat.ma @@ -74,6 +74,14 @@ P O \to (\forall m:nat. P (S m)) \to P n. intros.elim n.assumption.apply H1. qed. +theorem nat_case1: +\forall n:nat.\forall P:nat \to Prop. +(n=O \to P O) \to (\forall m:nat. (n=(S m) \to P (S m))) \to P n. +intros 2.elim n. +apply H.reflexivity. +apply H2.reflexivity. +qed. + theorem nat_elim2 : \forall R:nat \to nat \to Prop. (\forall n:nat. R O n) \to diff --git a/helm/matita/library/nat/nth_prime.ma b/helm/matita/library/nat/nth_prime.ma new file mode 100644 index 000000000..5ff937e42 --- /dev/null +++ b/helm/matita/library/nat/nth_prime.ma @@ -0,0 +1,204 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| A.Asperti, C.Sacerdoti Coen, *) +(* ||A|| E.Tassi, S.Zacchiroli *) +(* \ / *) +(* \ / Matita is distributed under the terms of the *) +(* v GNU Lesser General Public License Version 2.1 *) +(* *) +(**************************************************************************) + +set "baseuri" "cic:/matita/nat/nth_prime". + +include "nat/primes.ma". + +(* upper bound by Bertrand's conjecture. *) +(* Too difficult to prove. +let rec nth_prime n \def +match n with + [ O \Rightarrow (S(S O)) + | (S p) \Rightarrow + let previous_prime \def S (nth_prime p) in + min_aux previous_prime ((S(S O))*previous_prime) primeb]. + +theorem example8 : nth_prime (S(S O)) = (S(S(S(S(S O))))). +normalize.reflexivity. +qed. + +theorem example9 : nth_prime (S(S(S O))) = (S(S(S(S(S(S(S O))))))). +normalize.reflexivity. +qed. + +theorem example10 : nth_prime (S(S(S(S O)))) = (S(S(S(S(S(S(S(S(S(S(S O))))))))))). +normalize.reflexivity. +qed. *) + +theorem smallest_factor_fact: \forall n:nat. +n < smallest_factor (S (fact n)). +intros. +apply not_le_to_lt. +change with smallest_factor (S (fact n)) \le n \to False.intro. +apply not_divides_S_fact n (smallest_factor(S (fact n))) ? ?. +apply divides_smallest_factor_n. +simplify.apply le_S_S.apply le_O_n. +apply lt_SO_smallest_factor. +simplify.apply le_S_S.apply le_SO_fact. +assumption. +qed. + +(* mi sembra che il problem sia ex *) +theorem ex_prime: \forall n. (S O) \le n \to ex nat (\lambda m. +n < m \land m \le (S (fact n)) \land (prime m)). +intros. +elim H. +apply ex_intro nat ? (S(S O)). +split.split.apply le_n (S(S O)). +apply le_n (S(S O)).apply primeb_to_Prop (S(S O)). +apply ex_intro nat ? (smallest_factor (S (fact (S n1)))). +split.split. +apply smallest_factor_fact. +apply le_smallest_factor_n. +(* ancora hint non lo trova *) +apply prime_smallest_factor_n. +change with (S(S O)) \le S (fact (S n1)). +apply le_S.apply le_SSO_fact. +simplify.apply le_S_S.assumption. +qed. + +let rec nth_prime n \def +match n with + [ O \Rightarrow (S(S O)) + | (S p) \Rightarrow + let previous_prime \def (nth_prime p) in + let upper_bound \def S (fact previous_prime) in + min_aux (upper_bound - (S previous_prime)) upper_bound primeb]. + +(* it works, but nth_prime 4 takes already a few minutes - +it must compute factorial of 7 ... + +theorem example11 : nth_prime (S(S O)) = (S(S(S(S(S O))))). +normalize.reflexivity. +qed. + +theorem example12: nth_prime (S(S(S O))) = (S(S(S(S(S(S(S O))))))). +normalize.reflexivity. +qed. + +theorem example13 : nth_prime (S(S(S(S O)))) = (S(S(S(S(S(S(S(S(S(S(S O))))))))))). +normalize.reflexivity. +*) + +theorem prime_nth_prime : \forall n:nat.prime (nth_prime n). +intro. +apply nat_case n. +change with prime (S(S O)). +apply primeb_to_Prop (S(S O)). +intro. +(* ammirare la resa del letin !! *) +change with +let previous_prime \def (nth_prime m) in +let upper_bound \def S (fact previous_prime) in +prime (min_aux (upper_bound - (S previous_prime)) upper_bound primeb). +apply primeb_true_to_prime. +apply f_min_aux_true. +apply ex_intro nat ? (smallest_factor (S (fact (nth_prime m)))). +split.split. +cut S (fact (nth_prime m))-(S (fact (nth_prime m)) - (S (nth_prime m))) = (S (nth_prime m)). +rewrite > Hcut.exact smallest_factor_fact (nth_prime m). +(* maybe we could factorize this proof *) +apply plus_to_minus. +apply le_minus_m. +apply plus_minus_m_m. +apply le_S_S. +apply le_n_fact_n. +apply le_smallest_factor_n. +apply prime_to_primeb_true. +apply prime_smallest_factor_n. +change with (S(S O)) \le S (fact (nth_prime m)). +apply le_S_S.apply le_SO_fact. +qed. + +(* properties of nth_prime *) +theorem increasing_nth_prime: increasing nth_prime. +change with \forall n:nat. (nth_prime n) < (nth_prime (S n)). +intros. +change with +let previous_prime \def (nth_prime n) in +let upper_bound \def S (fact previous_prime) in +(S previous_prime) \le min_aux (upper_bound - (S previous_prime)) upper_bound primeb. +intros. +cut upper_bound - (upper_bound -(S previous_prime)) = (S previous_prime). +rewrite < Hcut in \vdash (? % ?). +apply le_min_aux. +apply plus_to_minus. +apply le_minus_m. +apply plus_minus_m_m. +apply le_S_S. +apply le_n_fact_n. +qed. + +variant lt_nth_prime_n_nth_prime_Sn :\forall n:nat. +(nth_prime n) < (nth_prime (S n)) \def increasing_nth_prime. + +theorem injective_nth_prime: injective nat nat nth_prime. +apply increasing_to_injective. +apply increasing_nth_prime. +qed. + +theorem lt_SO_nth_prime_n : \forall n:nat. (S O) \lt nth_prime n. +intros. elim n.simplify.apply le_n. +apply trans_lt ? (nth_prime n1). +assumption.apply lt_nth_prime_n_nth_prime_Sn. +qed. + +theorem lt_O_nth_prime_n : \forall n:nat. O \lt nth_prime n. +intros.apply trans_lt O (S O). +simplify. apply le_n.apply lt_SO_nth_prime_n. +qed. + +theorem ex_m_le_n_nth_prime_m: +\forall n: nat. nth_prime O \le n \to +ex nat (\lambda m. nth_prime m \le n \land n < nth_prime (S m)). +intros. +apply increasing_to_le2. +exact lt_nth_prime_n_nth_prime_Sn.assumption. +qed. + +theorem lt_nth_prime_to_not_prime: \forall n,m. nth_prime n < m \to m < nth_prime (S n) +\to \not (prime m). +intros. +apply primeb_false_to_not_prime. +letin previous_prime \def nth_prime n. +letin upper_bound \def S (fact previous_prime). +apply lt_min_aux_to_false primeb upper_bound (upper_bound - (S previous_prime)) m. +cut S (fact (nth_prime n))-(S (fact (nth_prime n)) - (S (nth_prime n))) = (S (nth_prime n)). +rewrite > Hcut.assumption. +apply plus_to_minus. +apply le_minus_m. +apply plus_minus_m_m. +apply le_S_S. +apply le_n_fact_n. +assumption. +qed. + +(* nth_prime enumerates all primes *) +theorem prime_to_nth_prime : \forall p:nat. prime p \to +ex nat (\lambda i:nat. nth_prime i = p). +intros. +cut ex nat (\lambda m. nth_prime m \le p \land p < nth_prime (S m)). +elim Hcut.elim H1. +cut nth_prime a < p \lor nth_prime a = p. +elim Hcut1. +absurd (prime p). +assumption. +apply lt_nth_prime_to_not_prime a.assumption.assumption. +apply ex_intro nat ? a.assumption. +apply le_to_or_lt_eq.assumption. +apply ex_m_le_n_nth_prime_m. +simplify.simplify in H.elim H.assumption. +qed. + diff --git a/helm/matita/library/nat/orders.ma b/helm/matita/library/nat/orders.ma index 122aebcfa..d592ed0af 100644 --- a/helm/matita/library/nat/orders.ma +++ b/helm/matita/library/nat/orders.ma @@ -248,3 +248,55 @@ apply lt_S_to_le.assumption. apply lt_to_le_to_lt p q (S n1) H3 H2. qed. +(* some properties of functions *) + +definition increasing \def \lambda f:nat \to nat. +\forall n:nat. f n < f (S n). + +theorem increasing_to_monotonic: \forall f:nat \to nat. +increasing f \to monotonic nat lt f. +simplify.intros.elim H1.apply H. +apply trans_le ? (f n1). +assumption.apply trans_le ? (S (f n1)). +apply le_n_Sn. +apply H. +qed. + +theorem le_n_fn: \forall f:nat \to nat. (increasing f) +\to \forall n:nat. n \le (f n). +intros.elim n. +apply le_O_n. +apply trans_le ? (S (f n1)). +apply le_S_S.apply H1. +simplify in H. apply H. +qed. + +theorem increasing_to_le: \forall f:nat \to nat. (increasing f) +\to \forall m:nat. ex nat (\lambda i. m \le (f i)). +intros.elim m. +apply ex_intro ? ? O.apply le_O_n. +elim H1. +apply ex_intro ? ? (S a). +apply trans_le ? (S (f a)). +apply le_S_S.assumption. +simplify in H. +apply H. +qed. + +theorem increasing_to_le2: \forall f:nat \to nat. (increasing f) +\to \forall m:nat. (f O) \le m \to +ex nat (\lambda i. (f i) \le m \land m <(f (S i))). +intros.elim H1. +apply ex_intro ? ? O. +split.apply le_n.apply H. +elim H3.elim H4. +cut (S n1) < (f (S a)) \lor (S n1) = (f (S a)). +elim Hcut. +apply ex_intro ? ? a. +split.apply le_S. assumption.assumption. +apply ex_intro ? ? (S a). +split.rewrite < H7.apply le_n. +rewrite > H7. +apply H. +apply le_to_or_lt_eq.apply H6. +qed. diff --git a/helm/matita/library/nat/primes.ma b/helm/matita/library/nat/primes.ma index 500c8117f..d7ee89d4e 100644 --- a/helm/matita/library/nat/primes.ma +++ b/helm/matita/library/nat/primes.ma @@ -136,7 +136,7 @@ definition divides_b : nat \to nat \to bool \def \lambda n,m :nat. (eqb (mod m n) O). theorem divides_b_to_Prop : -\forall n,m:nat. O < n \to O < m \to +\forall n,m:nat. O < n \to match divides_b n m with [ true \Rightarrow divides n m | false \Rightarrow \lnot (divides n m)]. @@ -147,31 +147,65 @@ match eqb (mod m n) O with | false \Rightarrow \lnot (divides n m)]. apply eqb_elim. intro.simplify.apply mod_O_to_divides.assumption.assumption. -intro.simplify.intro.apply H2.apply divides_to_mod_O.assumption.assumption. +intro.simplify.intro.apply H1.apply divides_to_mod_O.assumption.assumption. qed. theorem divides_b_true_to_divides : -\forall n,m:nat. O < n \to O < m \to +\forall n,m:nat. O < n \to (divides_b n m = true ) \to divides n m. intros. change with match true with [ true \Rightarrow divides n m | false \Rightarrow \lnot (divides n m)]. -rewrite < H2.apply divides_b_to_Prop. -assumption.assumption. +rewrite < H1.apply divides_b_to_Prop. +assumption. qed. theorem divides_b_false_to_not_divides : -\forall n,m:nat. O < n \to O < m \to +\forall n,m:nat. O < n \to (divides_b n m = false ) \to \lnot (divides n m). intros. change with match false with [ true \Rightarrow divides n m | false \Rightarrow \lnot (divides n m)]. -rewrite < H2.apply divides_b_to_Prop. -assumption.assumption. +rewrite < H1.apply divides_b_to_Prop. +assumption. +qed. + +theorem decidable_divides: \forall n,m:nat.O < n \to +decidable (divides n m). +intros.change with (divides n m) \lor \not (divides n m). +cut +match divides_b n m with +[ true \Rightarrow divides n m +| false \Rightarrow \not (divides n m)] \to (divides n m) \lor \not (divides n m). +apply Hcut.apply divides_b_to_Prop.assumption. +elim (divides_b n m).left.apply H1.right.apply H1. +qed. + +theorem divides_to_divides_b_true : \forall n,m:nat. O < n \to +divides n m \to divides_b n m = true. +intros. +cut match (divides_b n m) with +[ true \Rightarrow (divides n m) +| false \Rightarrow \not (divides n m)] \to ((divides_b n m) = true). +apply Hcut.apply divides_b_to_Prop.assumption. +elim divides_b n m.reflexivity. +absurd (divides n m).assumption.assumption. +qed. + +theorem not_divides_to_divides_b_false: \forall n,m:nat. O < n \to +\not(divides n m) \to (divides_b n m) = false. +intros. +cut match (divides_b n m) with +[ true \Rightarrow (divides n m) +| false \Rightarrow \not (divides n m)] \to ((divides_b n m) = false). +apply Hcut.apply divides_b_to_Prop.assumption. +elim divides_b n m. +absurd (divides n m).assumption.assumption. +reflexivity. qed. (* divides and pi *) @@ -232,7 +266,6 @@ theorem not_divides_S_fact: \forall n,i:nat. intros. apply divides_b_false_to_not_divides. apply trans_lt O (S O).apply le_n (S O).assumption. -simplify.apply le_S_S.apply le_O_n. change with (eqb (mod (S (fact n)) i) O) = false. rewrite > mod_S_fact.simplify.reflexivity. assumption.assumption. @@ -274,8 +307,7 @@ theorem example3 : smallest_prime_factor (S(S(S(S(S(S(S O))))))) = (S(S(S(S(S(S( simplify.reflexivity. qed. *) -(* not sure this is what we need *) -theorem lt_S_O_smallest_factor: +theorem lt_SO_smallest_factor: \forall n:nat. (S O) < n \to (S O) < (smallest_factor n). intro. apply nat_case n.intro.apply False_ind.apply not_le_Sn_O (S O) H. @@ -292,15 +324,26 @@ apply sym_eq.apply plus_to_minus.apply le_S.apply le_n_Sn. rewrite < sym_plus.simplify.reflexivity. qed. +theorem lt_O_smallest_factor: \forall n:nat. O < n \to O < (smallest_factor n). +intro. +apply nat_case n.intro.apply False_ind.apply not_le_Sn_n O H. +intro.apply nat_case m.intro. +simplify.apply le_n. +intros.apply trans_lt ? (S O). +simplify. apply le_n. +apply lt_SO_smallest_factor.simplify. apply le_S_S. +apply le_S_S.apply le_O_n. +qed. + theorem divides_smallest_factor_n : -\forall n:nat. (S O) < n \to divides (smallest_factor n) n. +\forall n:nat. O < n \to divides (smallest_factor n) n. intro. -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. +apply nat_case n.intro.apply False_ind.apply not_le_Sn_O O H. +intro.apply nat_case m.intro. simplify. +apply witness ? ? (S O). simplify.reflexivity. intros. apply divides_b_true_to_divides. -apply trans_lt ? (S O).apply le_n (S O).apply lt_S_O_smallest_factor ? H. -apply trans_lt ? (S O).apply le_n (S O).assumption. +apply lt_O_smallest_factor ? H. change with eqb (mod (S(S m1)) (min_aux m1 (S(S m1)) (\lambda m.(eqb (mod (S(S m1)) m) O)))) O = true. @@ -309,7 +352,8 @@ apply ex_intro nat ? (S(S m1)). split.split. apply le_minus_m.apply le_n. rewrite > mod_n_n.reflexivity. -apply trans_lt ? (S O).apply le_n (S O).assumption. +apply trans_lt ? (S O).apply le_n (S O).simplify. +apply le_S_S.apply le_S_S.apply le_O_n. qed. theorem le_smallest_factor_n : @@ -319,7 +363,7 @@ intro.apply nat_case m.simplify.reflexivity. intro.apply divides_to_le. simplify.apply le_S_S.apply le_O_n. apply divides_smallest_factor_n. -simplify.apply le_S_S.apply le_S_S. apply le_O_n. +simplify.apply le_S_S.apply le_O_n. qed. theorem lt_smallest_factor_to_not_divides: \forall n,i:nat. @@ -330,7 +374,6 @@ 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. -apply trans_lt O (S O).apply le_n (S O).assumption. change with (eqb (mod (S(S m1)) i) O) = false. apply lt_min_aux_to_false (\lambda i:nat.eqb (mod (S(S m1)) i) O) (S(S m1)) m1 i. @@ -347,7 +390,7 @@ theorem prime_smallest_factor_n : intro. change with (S(S O)) \le n \to (S O) < (smallest_factor n) \land (\forall m:nat. divides m (smallest_factor n) \to (S O) < m \to m = (smallest_factor n)). intro.split. -apply lt_S_O_smallest_factor.assumption. +apply lt_SO_smallest_factor.assumption. intros. cut le m (smallest_factor n). elim le_to_or_lt_eq m (smallest_factor n) Hcut. @@ -355,13 +398,13 @@ absurd divides m n. apply transitive_divides m (smallest_factor n). assumption. apply divides_smallest_factor_n. -exact H. +apply trans_lt ? (S O). simplify. apply le_n. exact H. apply lt_smallest_factor_to_not_divides. exact H.assumption.assumption.assumption. apply divides_to_le. apply trans_lt O (S O). apply le_n (S O). -apply lt_S_O_smallest_factor. +apply lt_SO_smallest_factor. exact H. assumption. qed. @@ -377,8 +420,8 @@ change with smallest_factor (S(S m1)) = (S(S m1)). intro.elim H.apply H2. apply divides_smallest_factor_n. -assumption. -apply lt_S_O_smallest_factor. +apply trans_lt ? (S O).simplify. apply le_n.assumption. +apply lt_SO_smallest_factor. assumption. qed. @@ -485,107 +528,3 @@ absurd (prime n).assumption.assumption. reflexivity. qed. -(* upper bound by Bertrand's conjecture. *) -(* Too difficult to prove. -let rec nth_prime n \def -match n with - [ O \Rightarrow (S(S O)) - | (S p) \Rightarrow - let previous_prime \def S (nth_prime p) in - min_aux previous_prime ((S(S O))*previous_prime) primeb]. - -theorem example8 : nth_prime (S(S O)) = (S(S(S(S(S O))))). -normalize.reflexivity. -qed. - -theorem example9 : nth_prime (S(S(S O))) = (S(S(S(S(S(S(S O))))))). -normalize.reflexivity. -qed. - -theorem example10 : nth_prime (S(S(S(S O)))) = (S(S(S(S(S(S(S(S(S(S(S O))))))))))). -normalize.reflexivity. -qed. *) - -theorem smallest_factor_fact: \forall n:nat. -n < smallest_factor (S (fact n)). -intros. -apply not_le_to_lt. -change with smallest_factor (S (fact n)) \le n \to False.intro. -apply not_divides_S_fact n (smallest_factor(S (fact n))) ? ?. -apply divides_smallest_factor_n. -simplify.apply le_S_S.apply le_SO_fact. -apply lt_S_O_smallest_factor. -simplify.apply le_S_S.apply le_SO_fact. -assumption. -qed. - -(* mi sembra che il problem sia ex *) -theorem ex_prime: \forall n. (S O) \le n \to ex nat (\lambda m. -n < m \land m \le (S (fact n)) \land (prime m)). -intros. -elim H. -apply ex_intro nat ? (S(S O)). -split.split.apply le_n (S(S O)). -apply le_n (S(S O)).apply primeb_to_Prop (S(S O)). -apply ex_intro nat ? (smallest_factor (S (fact (S n1)))). -split.split. -apply smallest_factor_fact. -apply le_smallest_factor_n. -(* ancora hint non lo trova *) -apply prime_smallest_factor_n. -change with (S(S O)) \le S (fact (S n1)). -apply le_S.apply le_SSO_fact. -simplify.apply le_S_S.assumption. -qed. - -let rec nth_prime n \def -match n with - [ O \Rightarrow (S(S O)) - | (S p) \Rightarrow - let previous_prime \def (nth_prime p) in - let upper_bound \def S (fact previous_prime) in - min_aux (upper_bound - (S previous_prime)) upper_bound primeb]. - -(* it works, but nth_prime 4 takes already a few minutes - -it must compute factorial of 7 ... - -theorem example11 : nth_prime (S(S O)) = (S(S(S(S(S O))))). -normalize.reflexivity. -qed. - -theorem example12: nth_prime (S(S(S O))) = (S(S(S(S(S(S(S O))))))). -normalize.reflexivity. -qed. - -theorem example13 : nth_prime (S(S(S(S O)))) = (S(S(S(S(S(S(S(S(S(S(S O))))))))))). -normalize.reflexivity. -*) - -theorem prime_nth_prime : \forall n:nat.prime (nth_prime n). -intro. -apply nat_case n. -change with prime (S(S O)). -apply primeb_to_Prop (S(S O)). -intro. -change with -let previous_prime \def (nth_prime m) in -let upper_bound \def S (fact previous_prime) in -prime (min_aux (upper_bound - (S previous_prime)) upper_bound primeb). -apply primeb_true_to_prime. -apply f_min_aux_true. -apply ex_intro nat ? (smallest_factor (S (fact (nth_prime m)))). -split.split. -cut S (fact (nth_prime m))-(S (fact (nth_prime m)) - (S (nth_prime m))) = (S (nth_prime m)). -rewrite > Hcut.exact smallest_factor_fact (nth_prime m). -(* maybe we could factorize this proof *) -apply plus_to_minus. -apply le_minus_m. -apply plus_minus_m_m. -apply le_S_S. -apply le_n_fact_n. -apply le_smallest_factor_n. -apply prime_to_primeb_true. -apply prime_smallest_factor_n. -change with (S(S O)) \le S (fact (nth_prime m)). -apply le_S_S.apply le_SO_fact. -qed. \ No newline at end of file -- 2.39.2