X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fnat%2Fprimes.ma;h=67d8254641379f309669e8dc0fa3ee6e1001caea;hb=4dc47c9675ffd5fa50296ffaa9b5997501518c98;hp=4298eb9425f11914cdf6f036d310285d0baea6ec;hpb=6423f1b6e3056883016598e454c55cab1004dfd2;p=helm.git diff --git a/helm/software/matita/library/nat/primes.ma b/helm/software/matita/library/nat/primes.ma index 4298eb942..67d825464 100644 --- a/helm/software/matita/library/nat/primes.ma +++ b/helm/software/matita/library/nat/primes.ma @@ -12,8 +12,6 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/nat/primes". - include "nat/div_and_mod.ma". include "nat/minimization.ma". include "nat/sigma_and_pi.ma". @@ -22,9 +20,8 @@ include "nat/factorial.ma". inductive divides (n,m:nat) : Prop \def witness : \forall p:nat.m = times n p \to divides n m. -interpretation "divides" 'divides n m = (cic:/matita/nat/primes/divides.ind#xpointer(1/1) n m). -interpretation "not divides" 'ndivides n m = - (cic:/matita/logic/connectives/Not.con (cic:/matita/nat/primes/divides.ind#xpointer(1/1) n m)). +interpretation "divides" 'divides n m = (divides n m). +interpretation "not divides" 'ndivides n m = (Not (divides n m)). theorem reflexive_divides : reflexive nat divides. unfold reflexive. @@ -83,36 +80,36 @@ qed. theorem divides_plus: \forall n,p,q:nat. n \divides p \to n \divides q \to n \divides p+q. intros. -elim H.elim H1. apply (witness n (p+q) (n2+n1)). +elim H.elim H1. apply (witness n (p+q) (n1+n2)). 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)). +elim H.elim H1. apply (witness n (p-q) (n1-n2)). rewrite > H2.rewrite > H3.apply sym_eq.apply distr_times_minus. qed. theorem divides_times: \forall n,m,p,q:nat. n \divides p \to m \divides q \to n*m \divides p*q. intros. -elim H.elim H1. apply (witness (n*m) (p*q) (n2*n1)). +elim H.elim H1. apply (witness (n*m) (p*q) (n1*n2)). rewrite > H2.rewrite > H3. -apply (trans_eq nat ? (n*(m*(n2*n1)))). -apply (trans_eq nat ? (n*(n2*(m*n1)))). +apply (trans_eq nat ? (n*(m*(n1*n2)))). +apply (trans_eq nat ? (n*(n1*(m*n2)))). apply assoc_times. apply eq_f. -apply (trans_eq nat ? ((n2*m)*n1)). +apply (trans_eq nat ? ((n1*m)*n2)). apply sym_eq. apply assoc_times. -rewrite > (sym_times n2 m).apply assoc_times. +rewrite > (sym_times n1 m).apply assoc_times. apply sym_eq. apply assoc_times. qed. theorem transitive_divides: transitive ? divides. unfold. intros. -elim H.elim H1. apply (witness x z (n2*n)). +elim H.elim H1. apply (witness x z (n1*n)). rewrite > H3.rewrite > H2. apply assoc_times. qed. @@ -152,7 +149,7 @@ qed. theorem antisymmetric_divides: antisymmetric nat divides. unfold antisymmetric.intros.elim H. elim H1. -apply (nat_case1 n2).intro. +apply (nat_case1 n1).intro. rewrite > H3.rewrite > H2.rewrite > H4. rewrite < times_n_O.reflexivity. intros. @@ -169,11 +166,11 @@ qed. (* divides le *) theorem divides_to_le : \forall n,m. O < m \to n \divides m \to n \le m. -intros. elim H1.rewrite > H2.cut (O < n2). -apply (lt_O_n_elim n2 Hcut).intro.rewrite < sym_times. +intros. elim H1.rewrite > H2.cut (O < n1). +apply (lt_O_n_elim n1 Hcut).intro.rewrite < sym_times. simplify.rewrite < sym_plus. apply le_plus_n. -elim (le_to_or_lt_eq O n2). +elim (le_to_or_lt_eq O n1). assumption. absurd (O H2.rewrite < H3.rewrite < times_n_O. @@ -190,6 +187,125 @@ rewrite > H2.rewrite < H3. simplify.exact (not_le_Sn_n O). qed. +(*a variant of or_div_mod *) +theorem or_div_mod1: \forall n,q. O < q \to +(divides q (S n)) \land S n = (S (div n q)) * q \lor +(\lnot (divides q (S n)) \land S n= (div n q) * q + S (n\mod q)). +intros.elim (or_div_mod n q H);elim H1 + [left.split + [apply (witness ? ? (S (n/q))). + rewrite > sym_times.assumption + |assumption + ] + |right.split + [intro. + apply (not_eq_O_S (n \mod q)). + (* come faccio a fare unfold nelleipotesi ? *) + cut ((S n) \mod q = O) + [rewrite < Hcut. + apply (div_mod_spec_to_eq2 (S n) q (div (S n) q) (mod (S n) q) (div n q) (S (mod n q))) + [apply div_mod_spec_div_mod. + assumption + |apply div_mod_spec_intro;assumption + ] + |apply divides_to_mod_O;assumption + ] + |assumption + ] + ] +qed. + +theorem divides_to_div: \forall n,m.divides n m \to m/n*n = m. +intro. +elim (le_to_or_lt_eq O n (le_O_n n)) + [rewrite > plus_n_O. + rewrite < (divides_to_mod_O ? ? H H1). + apply sym_eq. + apply div_mod. + assumption + |elim H1. + generalize in match H2. + rewrite < H. + simplify. + intro. + rewrite > H3. + reflexivity + ] +qed. + +theorem divides_div: \forall d,n. divides d n \to divides (n/d) n. +intros. +apply (witness ? ? d). +apply sym_eq. +apply divides_to_div. +assumption. +qed. + +theorem div_div: \forall n,d:nat. O < n \to divides d n \to +n/(n/d) = d. +intros. +apply (inj_times_l1 (n/d)) + [apply (lt_times_n_to_lt d) + [apply (divides_to_lt_O ? ? H H1). + |rewrite > divides_to_div;assumption + ] + |rewrite > divides_to_div + [rewrite > sym_times. + rewrite > divides_to_div + [reflexivity + |assumption + ] + |apply (witness ? ? d). + apply sym_eq. + apply divides_to_div. + assumption + ] + ] +qed. + +theorem divides_to_eq_times_div_div_times: \forall a,b,c:nat. +O \lt b \to c \divides b \to a * (b /c) = (a*b)/c. +intros. +elim H1. +rewrite > H2. +rewrite > (sym_times c n1). +cut(O \lt c) +[ rewrite > (lt_O_to_div_times n1 c) + [ rewrite < assoc_times. + rewrite > (lt_O_to_div_times (a *n1) c) + [ reflexivity + | assumption + ] + | assumption + ] +| apply (divides_to_lt_O c b); + assumption. +] +qed. + +theorem eq_div_plus: \forall n,m,d. O < d \to +divides d n \to divides d m \to +(n + m ) / d = n/d + m/d. +intros. +elim H1. +elim H2. +rewrite > H3.rewrite > H4. +rewrite < distr_times_plus. +rewrite > sym_times. +rewrite > sym_times in ⊢ (? ? ? (? (? % ?) ?)). +rewrite > sym_times in ⊢ (? ? ? (? ? (? % ?))). +rewrite > lt_O_to_div_times + [rewrite > lt_O_to_div_times + [rewrite > lt_O_to_div_times + [reflexivity + |assumption + ] + |assumption + ] + |assumption + ] +qed. + (* boolean divides *) definition divides_b : nat \to nat \to bool \def \lambda n,m :nat. (eqb (m \mod n) O). @@ -223,7 +339,8 @@ 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 + apply not_eq_true_false.apply sym_eq. + assumption ] |intros. apply divides_b_true_to_divides1 @@ -281,6 +398,22 @@ elim (divides_b n m).reflexivity. absurd (n \divides m).assumption.assumption. qed. +theorem divides_to_divides_b_true1 : \forall n,m:nat. +O < m \to n \divides m \to divides_b n m = true. +intro. +elim (le_to_or_lt_eq O n (le_O_n n)) + [apply divides_to_divides_b_true + [assumption|assumption] + |apply False_ind. + rewrite < H in H2. + elim H2. + simplify in H3. + apply (not_le_Sn_O O). + rewrite > H3 in H1. + assumption + ] +qed. + theorem not_divides_to_divides_b_false: \forall n,m:nat. O < n \to \lnot(n \divides m) \to (divides_b n m) = false. intros. @@ -293,6 +426,18 @@ absurd (n \divides m).assumption.assumption. reflexivity. qed. +theorem divides_b_div_true: +\forall d,n. O < n \to + divides_b d n = true \to divides_b (n/d) n = true. +intros. +apply divides_to_divides_b_true1 + [assumption + |apply divides_div. + apply divides_b_true_to_divides. + assumption + ] +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)) @@ -385,6 +530,15 @@ 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. + +theorem prime_to_lt_SO: \forall p. prime p \to S O < p. +intros.elim H. +assumption. +qed. + (* smallest factor *) definition smallest_factor : nat \to nat \def \lambda n:nat. @@ -393,18 +547,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. *) @@ -415,7 +569,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). @@ -445,15 +599,18 @@ apply (witness ? ? (S O)). simplify.reflexivity. intros. apply divides_b_true_to_divides. 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 : @@ -474,12 +631,9 @@ 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 (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 :