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=c5fe7bd298990a596e523bbc8282cd85f8e244ef;hpb=7b4d519aefac94afb371a7e4da94779b40bf8608;p=helm.git diff --git a/helm/software/matita/library/nat/primes.ma b/helm/software/matita/library/nat/primes.ma index c5fe7bd29..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,10 +187,129 @@ 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). - + theorem divides_b_to_Prop : \forall n,m:nat. O < n \to match divides_b n m with @@ -205,7 +321,7 @@ intro.simplify.apply mod_O_to_divides.assumption.assumption. intro.simplify.unfold Not.intro.apply H1.apply divides_to_mod_O.assumption.assumption. qed. -theorem divides_b_true_to_divides : +theorem divides_b_true_to_divides1: \forall n,m:nat. O < n \to (divides_b n m = true ) \to n \divides m. intros. @@ -217,7 +333,22 @@ rewrite < H1.apply divides_b_to_Prop. assumption. qed. -theorem divides_b_false_to_not_divides : +theorem divides_b_true_to_divides: +\forall n,m:nat. divides_b n m = true \to n \divides m. +intros 2.apply (nat_case n) + [apply (nat_case m) + [intro.apply divides_n_n + |simplify.intros.apply False_ind. + apply not_eq_true_false.apply sym_eq. + assumption + ] + |intros. + apply divides_b_true_to_divides1 + [apply lt_O_S|assumption] + ] +qed. + +theorem divides_b_false_to_not_divides1: \forall n,m:nat. O < n \to (divides_b n m = false ) \to n \ndivides m. intros. @@ -229,6 +360,22 @@ rewrite < H1.apply divides_b_to_Prop. assumption. qed. +theorem divides_b_false_to_not_divides: +\forall n,m:nat. divides_b n m = false \to n \ndivides m. +intros 2.apply (nat_case n) + [apply (nat_case m) + [simplify.unfold Not.intros. + apply not_eq_true_false.assumption + |unfold Not.intros.elim H1. + apply (not_eq_O_S m1).apply sym_eq. + assumption + ] + |intros. + apply divides_b_false_to_not_divides1 + [apply lt_O_S|assumption] + ] +qed. + theorem decidable_divides: \forall n,m:nat.O < n \to decidable (n \divides m). intros.unfold decidable. @@ -251,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. @@ -263,6 +426,33 @@ 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)) + [assumption + |apply False_ind. + elim H1. + rewrite < H2 in H1. + simplify in H1. + apply (lt_to_not_eq O n H). + apply sym_eq. + apply eqb_true_to_eq. + assumption + ] +qed. + (* divides and pi *) theorem divides_f_pi_f : \forall f:nat \to nat.\forall n,m,i:nat. m \le i \to i \le n+m \to f i \divides pi n f m. @@ -323,10 +513,8 @@ theorem not_divides_S_fact: \forall n,i:nat. (S O) < i \to i \le n \to i \ndivides S n!. intros. apply divides_b_false_to_not_divides. -apply (trans_lt O (S O)).apply (le_n (S O)).assumption. unfold divides_b. -rewrite > mod_S_fact.simplify.reflexivity. -assumption.assumption. +rewrite > mod_S_fact[simplify.reflexivity|assumption|assumption]. qed. (* prime *) @@ -342,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. @@ -350,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. *) @@ -372,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). @@ -401,17 +598,19 @@ 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 : @@ -431,14 +630,10 @@ apply (nat_case n).intro.apply False_ind.apply (not_le_Sn_O (S O) H). intro.apply (nat_case m).intro. apply False_ind.apply (not_le_Sn_n (S O) H). intros. apply divides_b_false_to_not_divides. -apply (trans_lt O (S O)).apply (le_n (S O)).assumption.unfold divides_b. apply (lt_min_aux_to_false -(\lambda i:nat.eqb ((S(S m1)) \mod i) O) (S(S m1)) m1 i). -cut ((S(S O)) = (S(S m1)-m1)). -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 :