From 4efbd5e75ff51c4104be8c5f35dbabb65f51461f Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Mon, 22 Aug 2005 08:17:28 +0000 Subject: [PATCH] New entries in nat: factorial.ma minimization.ma primes.ma primes1.ma sigma_and_pi.ma --- helm/matita/library/nat/factorial.ma | 59 +++ helm/matita/library/nat/minimization.ma | 180 +++++++ helm/matita/library/nat/primes.ma | 592 ++++++++++++++++++++++++ helm/matita/library/nat/primes1.ma | 39 ++ helm/matita/library/nat/sigma_and_pi.ma | 30 ++ 5 files changed, 900 insertions(+) create mode 100644 helm/matita/library/nat/factorial.ma create mode 100644 helm/matita/library/nat/minimization.ma create mode 100644 helm/matita/library/nat/primes.ma create mode 100644 helm/matita/library/nat/primes1.ma create mode 100644 helm/matita/library/nat/sigma_and_pi.ma diff --git a/helm/matita/library/nat/factorial.ma b/helm/matita/library/nat/factorial.ma new file mode 100644 index 000000000..742ca2a3b --- /dev/null +++ b/helm/matita/library/nat/factorial.ma @@ -0,0 +1,59 @@ +(**************************************************************************) +(* ___ *) +(* ||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/factorial". + +include "nat/lt_arith.ma". + +let rec fact n \def + match n with + [ O \Rightarrow (S O) + | (S m) \Rightarrow (S m)*(fact m)]. + +theorem le_SO_fact : \forall n. (S O) \le (fact n). +intro.elim n.simplify.apply le_n. +change with (S O) \le (S n1)*(fact n1). +apply trans_le ? ((S n1)*(S O)).simplify. +apply le_S_S.apply le_O_n. +apply le_times_r.assumption. +qed. + +theorem le_SSO_fact : \forall n. (S O) < n \to (S(S O)) \le (fact n). +intro.apply nat_case n.intro.apply False_ind.apply not_le_Sn_O (S O) H. +intros.change with (S (S O)) \le (S m)*(fact m). +apply trans_le ? ((S(S O))*(S O)).apply le_n. +apply le_times.exact H.apply le_SO_fact. +qed. + +theorem le_n_fact_n: \forall n. n \le (fact n). +intro. elim n.apply le_O_n. +change with S n1 \le (S n1)*(fact n1). +apply trans_le ? ((S n1)*(S O)). +rewrite < times_n_SO.apply le_n. +apply le_times.apply le_n. +apply le_SO_fact. +qed. + +theorem lt_n_fact_n: \forall n. (S(S O)) < n \to n < (fact n). +intro.apply nat_case n.intro.apply False_ind.apply not_le_Sn_O (S(S O)) H. +intros.change with (S m) < (S m)*(fact m). +apply lt_to_le_to_lt ? ((S m)*(S (S O))). +rewrite < sym_times. +simplify. +apply le_S_S.rewrite < plus_n_O. +apply le_plus_n. +apply le_times_r.apply le_SSO_fact. +simplify.apply le_S_S_to_le.exact H. +qed. + diff --git a/helm/matita/library/nat/minimization.ma b/helm/matita/library/nat/minimization.ma new file mode 100644 index 000000000..8aa1deed3 --- /dev/null +++ b/helm/matita/library/nat/minimization.ma @@ -0,0 +1,180 @@ +(**************************************************************************) +(* ___ *) +(* ||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/minimization". + +include "nat/minus.ma". +include "datatypes/bool.ma". + +let rec max i f \def + match (f i) with + [ true \Rightarrow i + | false \Rightarrow + match i with + [ O \Rightarrow O + | (S j) \Rightarrow max j f ]]. + +theorem max_O_f : \forall f: nat \to bool. max O f = O. +intro. simplify. +elim f O. +simplify.reflexivity. +simplify.reflexivity. +qed. + +theorem max_S_max : \forall f: nat \to bool. \forall n:nat. +(f (S n) = true \land max (S n) f = (S n)) \lor +(f (S n) = false \land max (S n) f = max n f). +intros.simplify.elim (f (S n)). +simplify.left.split.reflexivity.reflexivity. +simplify.right.split.reflexivity.reflexivity. +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)). + +(* perche' si blocca per mezzo minuto qui ??? *) +theorem f_max_true : \forall f:nat \to bool. \forall n:nat. +ex nat (\lambda i:nat. (le i n) \land (f i = true)) \to f (max n f) = true. +intros 2. +elim n.elim H.elim H1.generalize in match H3. +apply le_n_O_elim a H2.intro.simplify.rewrite > H4. +simplify.assumption. +simplify. +apply bool_ind (\lambda b:bool. +(f (S n1) = b) \to (f ([\lambda b:bool.nat] match b in bool with +[ true \Rightarrow (S n1) +| false \Rightarrow (max n1 f)])) = true) ? ? ?. +reflexivity. +simplify.intro.assumption. +simplify.intro.apply H. +elim H1.elim H3.generalize in match H5. +apply le_n_Sm_elim a n1 H4. +intros. +apply ex_intro nat ? a. +split.apply le_S_S_to_le.assumption.assumption. +intros.apply False_ind.apply not_eq_true_false ?. +rewrite < H2.rewrite < H7.rewrite > H6. reflexivity. +qed. + +theorem lt_max_to_false : \forall f:nat \to bool. +\forall n,m:nat. (max n f) < m \to m \leq n \to f m = false. +intros 2. +elim n.absurd le m O.assumption. +cut O < m.apply lt_O_n_elim m Hcut.exact not_le_Sn_O. +rewrite < max_O_f f.assumption. +generalize in match H1. +(* ?? non posso generalizzare su un goal implicativo ?? *) +elim max_S_max f n1. +elim H3. +absurd m \le S n1.assumption. +apply lt_to_not_le.rewrite < H6.assumption. +elim H3. +apply le_n_Sm_elim m n1 H2. +intro. +apply H.rewrite < H6.assumption. +apply le_S_S_to_le.assumption. +intro.rewrite > H7.assumption. +qed. + +let rec min_aux off n f \def + match f (n-off) with + [ true \Rightarrow (n-off) + | false \Rightarrow + match off with + [ O \Rightarrow n + | (S p) \Rightarrow min_aux p n f]]. + +definition min : nat \to (nat \to bool) \to nat \def +\lambda n.\lambda f. min_aux n n f. + +theorem min_aux_O_f: \forall f:nat \to bool. \forall i :nat. +min_aux O i f = i. +intros.simplify.rewrite < minus_n_O. +elim f i. +simplify.reflexivity. +simplify.reflexivity. +qed. + +theorem min_O_f : \forall f:nat \to bool. +min O f = O. +intro.apply min_aux_O_f f O. +qed. + +theorem min_aux_S : \forall f: nat \to bool. \forall i,n:nat. +(f (n -(S i)) = true \land min_aux (S i) n f = (n - (S i))) \lor +(f (n -(S i)) = false \land min_aux (S i) n f = min_aux i n f). +intros.simplify.elim (f (n - (S i))). +simplify.left.split.reflexivity.reflexivity. +simplify.right.split.reflexivity.reflexivity. +qed. + +theorem f_min_aux_true: \forall f:nat \to bool. \forall off,m:nat. +ex nat (\lambda i:nat. (le (m-off) i) \land (le i m) \land (f i = true)) \to +f (min_aux off m f) = true. +intros 2. +elim off.elim H.elim H1.elim H2. +cut a = m. +rewrite > min_aux_O_f f.rewrite < Hcut.assumption. +apply antisym_le a m .assumption.rewrite > minus_n_O m.assumption. +simplify. +apply bool_ind (\lambda b:bool. +(f (m-(S n)) = b) \to (f ([\lambda b:bool.nat] match b in bool with +[ true \Rightarrow m-(S n) +| false \Rightarrow (min_aux n m f)])) = true) ? ? ?. +reflexivity. +simplify.intro.assumption. +simplify.intro.apply H. +elim H1.elim H3.elim H4. +elim (le_to_or_lt_eq (m-(S n)) a H6). +apply ex_intro nat ? a. +split.split. +apply lt_minus_S_n_to_le_minus_n.assumption. +assumption.assumption. +absurd f a = false.rewrite < H8.assumption. +rewrite > H5. +apply not_eq_true_false. +qed. + +theorem lt_min_aux_to_false : \forall f:nat \to bool. +\forall n,off,m:nat. (n-off) \leq m \to m < (min_aux off n f) \to f m = false. +intros 3. +elim off.absurd le n m.rewrite > minus_n_O.assumption. +apply lt_to_not_le.rewrite < min_aux_O_f f n.assumption. +generalize in match H1. +elim min_aux_S f n1 n. +elim H3. +absurd n - S n1 \le m.assumption. +apply lt_to_not_le.rewrite < H6.assumption. +elim H3. +elim le_to_or_lt_eq (n -(S n1)) m. +apply H.apply lt_minus_S_n_to_le_minus_n.assumption. +rewrite < H6.assumption.assumption. +rewrite < H7.assumption. +qed. + +theorem le_min_aux : \forall f:nat \to bool. +\forall n,off:nat. (n-off) \leq (min_aux off n f). +intros 3. +elim off.rewrite < minus_n_O. +rewrite > min_aux_O_f f n.apply le_n. +elim min_aux_S f n1 n. +elim H1.rewrite > H3.apply le_n. +elim H1.rewrite > H3. +apply trans_le (n-(S n1)) (n-n1) ?. +apply monotonic_le_minus_r. +apply le_n_Sn. +assumption. +qed. + diff --git a/helm/matita/library/nat/primes.ma b/helm/matita/library/nat/primes.ma new file mode 100644 index 000000000..dddd91516 --- /dev/null +++ b/helm/matita/library/nat/primes.ma @@ -0,0 +1,592 @@ +(**************************************************************************) +(* ___ *) +(* ||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/primes". + +include "nat/div_and_mod.ma". +include "nat/minimization.ma". +include "nat/sigma_and_pi.ma". +include "nat/factorial.ma". + +inductive divides (n,m:nat) : Prop \def +witness : \forall p:nat.m = times n p \to divides n m. + +theorem reflexive_divides : reflexive nat divides. +simplify. +intros. +exact witness x x (S O) (times_n_SO x). +qed. + +theorem divides_to_div_mod_spec : +\forall n,m. O < n \to divides n m \to div_mod_spec m n (div m n) O. +intros.elim H1.rewrite > H2. +constructor 1.assumption. +apply lt_O_n_elim n H.intros. +rewrite < plus_n_O. +rewrite > div_times.apply sym_times. +qed. + +theorem div_mod_spec_to_div : +\forall n,m,p. div_mod_spec m n p O \to divides n m. +intros.elim H. +apply witness n m p. +rewrite < sym_times. +rewrite > plus_n_O (p*n).assumption. +qed. + +theorem divides_to_mod_O: +\forall n,m. O < n \to divides n m \to (mod m n) = O. +intros.apply div_mod_spec_to_eq2 m n (div m n) (mod m n) (div m n) O. +apply div_mod_spec_div_mod.assumption. +apply divides_to_div_mod_spec.assumption.assumption. +qed. + +theorem mod_O_to_divides: +\forall n,m. O< n \to (mod m n) = O \to divides n m. +intros. +apply witness n m (div m n). +rewrite > plus_n_O (n*div m n). +rewrite < H1. +rewrite < sym_times. +(* perche' hint non lo trova ?*) +apply div_mod. +assumption. +qed. + +theorem divides_n_O: \forall n:nat. divides n O. +intro. apply witness n O O.apply times_n_O. +qed. + +theorem divides_SO_n: \forall n:nat. divides (S O) n. +intro. apply witness (S O) n n. simplify.apply plus_n_O. +qed. + +theorem divides_plus: \forall n,p,q:nat. +divides n p \to divides n q \to divides n (p+q). +intros. +elim H.elim H1. apply witness n (p+q) (n2+n1). +rewrite > H2.rewrite > H3.apply sym_eq.apply distr_times_plus. +qed. + +theorem divides_minus: \forall n,p,q:nat. +divides n p \to divides n q \to divides n (p-q). +intros. +elim H.elim H1. apply witness n (p-q) (n2-n1). +rewrite > H2.rewrite > H3.apply sym_eq.apply distr_times_minus. +qed. + +theorem divides_times: \forall n,m,p,q:nat. +divides n p \to divides m q \to divides (n*m) (p*q). +intros. +elim H.elim H1. apply witness (n*m) (p*q) (n2*n1). +rewrite > H2.rewrite > H3. +apply trans_eq nat ? (n*(m*(n2*n1))). +apply trans_eq nat ? (n*(n2*(m*n1))). +apply assoc_times. +apply eq_f. +apply trans_eq nat ? ((n2*m)*n1). +apply sym_eq. apply assoc_times. +rewrite > sym_times n2 m.apply assoc_times. +apply sym_eq. apply assoc_times. +qed. + +theorem transitive_divides: \forall n,m,p. +divides n m \to divides m p \to divides n p. +intros. +elim H.elim H1. apply witness n p (n2*n1). +rewrite > H3.rewrite > H2. +apply assoc_times. +qed. + +(* divides le *) +theorem divides_to_le : \forall n,m. O < m \to divides n m \to n \le m. +intros. elim H1.rewrite > H2.cut O < n2. +apply lt_O_n_elim n2 Hcut.intro.rewrite < sym_times. +simplify.rewrite < sym_plus. +apply le_plus_n. +elim le_to_or_lt_eq O n2. +assumption.apply le_O_n. +absurd O H2.rewrite < H3.rewrite < times_n_O. +apply not_le_Sn_n O. +qed. + +theorem divides_to_lt_O : \forall n,m. O < m \to divides n m \to O < n. +intros.elim H1. +elim le_to_or_lt_eq O n (le_O_n n). +assumption. +rewrite < H3.absurd O < m.assumption. +rewrite > H2.rewrite < H3. +simplify.exact not_le_Sn_n O. +qed. + +(* boolean divides *) +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 +match divides_b n m with +[ true \Rightarrow divides n m +| false \Rightarrow \lnot (divides n m)]. +intros. +change with +match eqb (mod m n) O with +[ true \Rightarrow divides n m +| 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. +qed. + +theorem divides_b_true_to_divides : +\forall n,m:nat. O < n \to O < m \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. +qed. + +theorem divides_b_false_to_not_divides : +\forall n,m:nat. O < n \to O < m \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. +qed. + +(* divides and pi *) +theorem divides_f_pi_f : \forall f:nat \to nat.\forall n,i:nat. +i < n \to divides (f i) (pi n f). +intros 3.elim n.apply False_ind.apply not_le_Sn_O i H. +simplify. +apply le_n_Sm_elim (S i) n1 H1. +intro. +apply transitive_divides ? (pi n1 f). +apply H.simplify.apply le_S_S_to_le. assumption. +apply witness ? ? (f n1).apply sym_times. +intro.cut i = n1. +rewrite > Hcut. +apply witness ? ? (pi n1 f).reflexivity. +apply inj_S.assumption. +qed. + +theorem mod_S_pi: \forall f:nat \to nat.\forall n,i:nat. +i < n \to (S O) < (f i) \to mod (S (pi n f)) (f i) = (S O). +intros.cut mod (pi n f) (f i) = O. +rewrite < Hcut. +apply mod_S.apply trans_lt O (S O).apply le_n (S O).assumption. +rewrite > Hcut.assumption. +apply divides_to_mod_O.apply trans_lt O (S O).apply le_n (S O).assumption. +apply divides_f_pi_f.assumption. +qed. + +(* divides and fact *) +theorem divides_fact : \forall n,i:nat. +O < i \to i \le n \to divides i (fact n). +intros 3.elim n.absurd O H3. +apply witness ? ? (fact n1).reflexivity. +qed. + +theorem mod_S_fact: \forall n,i:nat. +(S O) < i \to i \le n \to mod (S (fact n)) i = (S O). +intros.cut mod (fact n) i = O. +rewrite < Hcut. +apply mod_S.apply trans_lt O (S O).apply le_n (S O).assumption. +rewrite > Hcut.assumption. +apply divides_to_mod_O.apply trans_lt O (S O).apply le_n (S O).assumption. +apply divides_fact.apply trans_lt O (S O).apply le_n (S O).assumption. +assumption. +qed. + +theorem not_divides_S_fact: \forall n,i:nat. +(S O) < i \to i \le n \to \not (divides i (S (fact n))). +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. +qed. + +(* prime *) +definition prime : nat \to Prop \def +\lambda n:nat. (S O) < n \land +(\forall m:nat. divides m n \to (S O) < m \to m = n). + +theorem not_prime_O: \lnot (prime O). +simplify.intro.elim H.apply not_le_Sn_O (S O) H1. +qed. + +theorem not_prime_SO: \lnot (prime (S O)). +simplify.intro.elim H.apply not_le_Sn_n (S O) H1. +qed. + +(* smallest factor *) +definition smallest_factor : nat \to nat \def +\lambda n:nat. +match n with +[ O \Rightarrow O +| (S p) \Rightarrow + match p with + [ O \Rightarrow (S O) + | (S q) \Rightarrow min_aux q (S(S q)) (\lambda m.(eqb (mod (S(S q)) m) O))]]. + +(* it works ! +theorem example1 : smallest_prime_factor (S(S(S O))) = (S(S(S O))). +normalize.reflexivity. +qed. + +theorem example2: smallest_prime_factor (S(S(S(S O)))) = (S(S O)). +normalize.reflexivity. +qed. + +theorem example3 : smallest_prime_factor (S(S(S(S(S(S(S O))))))) = (S(S(S(S(S(S(S O))))))). +simplify.reflexivity. +qed. *) + +(* not sure this is what we need *) +theorem lt_S_O_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. +intro.apply nat_case m.intro. apply False_ind.apply not_le_Sn_n (S O) H. +intros. +change with +S O < min_aux m1 (S(S m1)) (\lambda m.(eqb (mod (S(S m1)) m) O)). +apply lt_to_le_to_lt ? (S (S O)). +apply le_n (S(S O)). +cut (S(S O)) = (S(S m1)) - m1. +rewrite > Hcut. +apply le_min_aux. +apply sym_eq.apply plus_to_minus.apply le_S.apply le_n_Sn. +rewrite < sym_plus.simplify.reflexivity. +qed. + +theorem divides_smallest_factor_n : +\forall n:nat. (S 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. +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. +change with +eqb (mod (S(S m1)) (min_aux m1 (S(S m1)) + (\lambda m.(eqb (mod (S(S m1)) m) O)))) O = true. +apply f_min_aux_true. +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. +qed. + +theorem le_smallest_factor_n : +\forall n:nat. smallest_factor n \le n. +intro.apply nat_case n.simplify.reflexivity. +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. +qed. + +theorem lt_smallest_factor_to_not_divides: \forall n,i:nat. +(S O) < n \to (S O) < i \to i < (smallest_factor n) \to \lnot (divides i n). +intros 2. +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. +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. +cut (S(S O)) = (S(S m1)-m1). +rewrite < Hcut.exact H1. +apply sym_eq. apply plus_to_minus. +apply le_S.apply le_n_Sn. +rewrite < sym_plus.simplify.reflexivity. +exact H2. +qed. + +theorem prime_smallest_factor_n : +\forall n:nat. (S O) < n \to 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. +intros. +cut le m (smallest_factor n). +elim le_to_or_lt_eq m (smallest_factor n) Hcut. +absurd divides m n. +apply transitive_divides m (smallest_factor n). +assumption. +apply divides_smallest_factor_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. +exact H. +assumption. +qed. + +theorem prime_to_smallest_factor: \forall n. prime n \to +smallest_factor n = n. +intro.apply nat_case n.intro.apply False_ind.apply not_prime_O H. +intro.apply nat_case m.intro.apply False_ind.apply not_prime_SO H. +intro. +change with +(S O) < (S(S m1)) \land +(\forall m:nat. divides m (S(S m1)) \to (S O) < m \to m = (S(S m1))) \to +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. +assumption. +qed. + +(* a number n > O is prime iff its smallest factor is n *) +definition primeb \def \lambda n:nat. +match n with +[ O \Rightarrow false +| (S p) \Rightarrow + match p with + [ O \Rightarrow false + | (S q) \Rightarrow eqb (smallest_factor (S(S q))) (S(S q))]]. + +(* it works! +theorem example4 : primeb (S(S(S O))) = true. +normalize.reflexivity. +qed. + +theorem example5 : primeb (S(S(S(S(S(S O)))))) = false. +normalize.reflexivity. +qed. + +theorem example6 : primeb (S(S(S(S((S(S(S(S(S(S(S O)))))))))))) = true. +normalize.reflexivity. +qed. + +theorem example7 : primeb (S(S(S(S(S(S((S(S(S(S((S(S(S(S(S(S(S O))))))))))))))))))) = true. +normalize.reflexivity. +qed. *) + +theorem primeb_to_Prop: \forall n. +match primeb n with +[ true \Rightarrow prime n +| false \Rightarrow \not (prime n)]. +intro. +apply nat_case n.simplify.intro.elim H.apply not_le_Sn_O (S O) H1. +intro.apply nat_case m.simplify.intro.elim H.apply not_le_Sn_n (S O) H1. +intro. +change with +match eqb (smallest_factor (S(S m1))) (S(S m1)) with +[ true \Rightarrow prime (S(S m1)) +| false \Rightarrow \not (prime (S(S m1)))]. +apply eqb_elim (smallest_factor (S(S m1))) (S(S m1)). +intro.change with prime (S(S m1)). +rewrite < H. +apply prime_smallest_factor_n. +simplify.apply le_S_S.apply le_S_S.apply le_O_n. +intro.change with \not (prime (S(S m1))). +change with prime (S(S m1)) \to False. +intro.apply H. +apply prime_to_smallest_factor. +assumption. +qed. + +theorem primeb_true_to_prime : \forall n:nat. +primeb n = true \to prime n. +intros.change with +match true with +[ true \Rightarrow prime n +| false \Rightarrow \not (prime n)]. +rewrite < H. +apply primeb_to_Prop. +qed. + +theorem primeb_false_to_not_prime : \forall n:nat. +primeb n = false \to \not (prime n). +intros.change with +match false with +[ true \Rightarrow prime n +| false \Rightarrow \not (prime n)]. +rewrite < H. +apply primeb_to_Prop. +qed. + +theorem decidable_prime : \forall n:nat.decidable (prime n). +intro.change with (prime n) \lor \not (prime n). +cut +match primeb n with +[ true \Rightarrow prime n +| false \Rightarrow \not (prime n)] \to (prime n) \lor \not (prime n). +apply Hcut.apply primeb_to_Prop. +elim (primeb n).left.apply H.right.apply H. +qed. + +theorem prime_to_primeb_true: \forall n:nat. +prime n \to primeb n = true. +intros. +cut match (primeb n) with +[ true \Rightarrow prime n +| false \Rightarrow \not (prime n)] \to ((primeb n) = true). +apply Hcut.apply primeb_to_Prop. +elim primeb n.reflexivity. +absurd (prime n).assumption.assumption. +qed. + +theorem not_prime_to_primeb_false: \forall n:nat. +\not(prime n) \to primeb n = false. +intros. +cut match (primeb n) with +[ true \Rightarrow prime n +| false \Rightarrow \not (prime n)] \to ((primeb n) = false). +apply Hcut.apply primeb_to_Prop. +elim primeb n. +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. +(* 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. \ No newline at end of file diff --git a/helm/matita/library/nat/primes1.ma b/helm/matita/library/nat/primes1.ma new file mode 100644 index 000000000..55d643262 --- /dev/null +++ b/helm/matita/library/nat/primes1.ma @@ -0,0 +1,39 @@ +(**************************************************************************) +(* ___ *) +(* ||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/primes1". + +include "datatypes/constructors.ma". +include "nat/primes.ma". +include "nat/exp.ma". + +(* p is just an upper bound, acc is an accumulator *) +let rec n_divides_aux p n m acc \def + match (mod n m) with + [ O \Rightarrow + match p with + [ O \Rightarrow pair nat nat acc n + | (S p) \Rightarrow n_divides_aux p (div n m) m (S acc)] + | (S a) \Rightarrow pair nat nat acc n]. + +(* n_divides n m = if m divides n q times, with remainder r *) +definition n_divides \def \lambda n,m:nat.n_divides_aux n n m O. + +(* +theorem n_divides_to_Prop: \forall n,m,p,a. + match n_divides_aux p n m a with + [ (pair q r) \Rightarrow n = (exp m a)*r]. +intros. +apply nat_case (mod n m). *) + diff --git a/helm/matita/library/nat/sigma_and_pi.ma b/helm/matita/library/nat/sigma_and_pi.ma new file mode 100644 index 000000000..b9b8065aa --- /dev/null +++ b/helm/matita/library/nat/sigma_and_pi.ma @@ -0,0 +1,30 @@ +(**************************************************************************) +(* ___ *) +(* ||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/sigma_and_pi". + +include "nat/times.ma". + +let rec sigma n f \def + match n with + [ O \Rightarrow O + | (S p) \Rightarrow (f p)+(sigma p f)]. + +let rec pi n f \def + match n with + [ O \Rightarrow (S O) + | (S p) \Rightarrow (f p)*(pi p f)]. + + + -- 2.39.2