X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fnat%2Fprimes.ma;h=a95b2e88fddda2344f0fafc448593de57404d470;hb=d5afc8f8891d0020f5804eb2322fc0d1c8c60702;hp=50b7d1221bfdca8211184a664add8c73aa392bd5;hpb=55b82bd235d82ff7f0a40d980effe1efde1f5073;p=helm.git diff --git a/helm/software/matita/library/nat/primes.ma b/helm/software/matita/library/nat/primes.ma index 50b7d1221..a95b2e88f 100644 --- a/helm/software/matita/library/nat/primes.ma +++ b/helm/software/matita/library/nat/primes.ma @@ -193,23 +193,19 @@ 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 [ true \Rightarrow n \divides m | false \Rightarrow n \ndivides m]. -intros. -change with -match eqb (m \mod n) O with -[ true \Rightarrow n \divides m -| false \Rightarrow n \ndivides m]. +intros.unfold divides_b. apply eqb_elim. 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. @@ -221,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. @@ -233,9 +243,25 @@ 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.change with ((n \divides m) \lor n \ndivides m). +intros.unfold decidable. cut (match divides_b n m with [ true \Rightarrow n \divides m @@ -267,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. @@ -327,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. -change with ((eqb ((S n!) \mod i) O) = false). -rewrite > mod_S_fact.simplify.reflexivity. -assumption.assumption. +unfold divides_b. +rewrite > mod_S_fact[simplify.reflexivity|assumption|assumption]. qed. (* prime *) @@ -346,6 +385,10 @@ theorem not_prime_SO: \lnot (prime (S O)). unfold Not.unfold prime.intro.elim H.apply (not_le_Sn_n (S O) H1). qed. +theorem prime_to_lt_O: \forall p. prime p \to O < p. +intros.elim H.apply lt_to_le.assumption. +qed. + (* smallest factor *) definition smallest_factor : nat \to nat \def \lambda n:nat. @@ -354,18 +397,18 @@ match n with | (S p) \Rightarrow match p with [ O \Rightarrow (S O) - | (S q) \Rightarrow min_aux q (S(S q)) (\lambda m.(eqb ((S(S q)) \mod m) O))]]. + | (S q) \Rightarrow min_aux q (S (S O)) (\lambda m.(eqb ((S(S q)) \mod m) O))]]. -(* it works ! -theorem example1 : smallest_prime_factor (S(S(S O))) = (S(S(S O))). +(* it works ! +theorem example1 : smallest_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)). +theorem example2: smallest_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))))))). +theorem example3 : smallest_factor (S(S(S(S(S(S(S O))))))) = (S(S(S(S(S(S(S O))))))). simplify.reflexivity. qed. *) @@ -376,7 +419,7 @@ 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 ((S(S m1)) \mod m) O))). +(S O < min_aux m1 (S (S O)) (\lambda m.(eqb ((S(S m1)) \mod 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). @@ -405,23 +448,25 @@ 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)) +(eqb ((S(S m1)) \mod (min_aux m1 (S (S O)) (\lambda m.(eqb ((S(S m1)) \mod 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)).unfold lt. -apply le_S_S.apply le_S_S.apply le_O_n. +apply (le_S_S_to_le (S (S O)) (S (S m1)) ?). +apply (minus_le_O_to_le (S (S (S O))) (S (S (S m1))) ?). +apply (le_n O). +rewrite < sym_plus. simplify. apply le_n. +apply (eq_to_eqb_true (mod (S (S m1)) (S (S m1))) O ?). +apply (mod_n_n (S (S m1)) ?). +apply (H). 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 (nat_case n).simplify.apply le_n. +intro.apply (nat_case m).simplify.apply le_n. intro.apply divides_to_le. unfold lt.apply le_S_S.apply le_O_n. apply divides_smallest_factor_n. @@ -435,20 +480,15 @@ 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. -change with ((eqb ((S(S m1)) \mod i) O) = false). 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)). -rewrite < Hcut.exact H1. -apply sym_eq. apply plus_to_minus. -rewrite < sym_plus.simplify.reflexivity. -exact H2. +(\lambda i:nat.eqb ((S(S m1)) \mod i) O) (S (S O)) m1 i). +assumption. +assumption. 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 +intro.change with ((S(S O)) \le n \to (S O) < (smallest_factor n) \land (\forall m:nat. m \divides smallest_factor n \to (S O) < m \to m = (smallest_factor n))). intro.split. apply lt_SO_smallest_factor.assumption. @@ -525,11 +565,11 @@ match eqb (smallest_factor (S(S m1))) (S(S m1)) with [ true \Rightarrow prime (S(S m1)) | false \Rightarrow \lnot (prime (S(S m1)))]. apply (eqb_elim (smallest_factor (S(S m1))) (S(S m1))). -intro.change with (prime (S(S m1))). +intro.simplify. rewrite < H. apply prime_smallest_factor_n. unfold lt.apply le_S_S.apply le_S_S.apply le_O_n. -intro.change with (\lnot (prime (S(S m1)))). +intro.simplify. change with (prime (S(S m1)) \to False). intro.apply H. apply prime_to_smallest_factor. @@ -557,7 +597,7 @@ apply primeb_to_Prop. qed. theorem decidable_prime : \forall n:nat.decidable (prime n). -intro.change with ((prime n) \lor \lnot (prime n)). +intro.unfold decidable. cut (match primeb n with [ true \Rightarrow prime n