X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Flibrary%2Fnat%2Ftotient.ma;h=a86986a81f743efd78b0dd004e38653c0788d601;hb=ecdf96be61f7f9cee7336b81d24780e59d1ea554;hp=2c6061e0b80c673158812a259d0e944280d0a8f6;hpb=04e27500136c94e4f2ac072a5e4d330b75da35f0;p=helm.git diff --git a/matita/library/nat/totient.ma b/matita/library/nat/totient.ma index 2c6061e0b..a86986a81 100644 --- a/matita/library/nat/totient.ma +++ b/matita/library/nat/totient.ma @@ -14,88 +14,124 @@ set "baseuri" "cic:/matita/nat/totient". -include "nat/count.ma". include "nat/chinese_reminder.ma". +include "nat/iteration2.ma". +(*a new definition of totient, which uses sigma_p instead of sigma *) +(*there's a little difference between this definition and the classic one: + the classic definition of totient is: + + phi (n) is the number of naturals i (less or equal than n) so then gcd (i,n) = 1. + (so this definition considers the values i=1,2,...,n) + + sigma_p doesn't work on the value n (but the first value it works on is (pred n)) + but works also on 0. That's not a problem, in fact + - if n <> 1, gcd (n,0) <>1 and gcd (n,n) = n <> 1. + - if n = 1, then Phi(n) = 1, and (totient n), as defined below, returns 1. + + *) definition totient : nat \to nat \def -\lambda n. count n (\lambda m. eqb (gcd m n) (S O)). - -theorem totient3: totient (S(S(S O))) = (S(S O)). -reflexivity. -qed. - -theorem totient6: totient (S(S(S(S(S(S O)))))) = (S(S O)). -reflexivity. -qed. +\lambda n.sigma_p n (\lambda m. eqb (gcd m n) (S O)) (\lambda m.S O). + theorem totient_times: \forall n,m:nat. (gcd m n) = (S O) \to totient (n*m) = (totient n)*(totient m). -intro. -apply (nat_case n). -intro.simplify.intro.reflexivity. -intros 2.apply (nat_case m1). -rewrite < sym_times. -rewrite < (sym_times (totient O)). -simplify.intro.reflexivity. intros. unfold totient. -apply (count_times m m2 ? ? ? -(\lambda b,a. cr_pair (S m) (S m2) a b) (\lambda x. x \mod (S m)) (\lambda x. x \mod (S m2))). -intros.unfold cr_pair. -apply (le_to_lt_to_lt ? (pred ((S m)*(S m2)))). -unfold min. -apply le_min_aux_r.unfold lt. -apply (nat_case ((S m)*(S m2))).apply le_n. -intro.apply le_n. -intros. -generalize in match (mod_cr_pair (S m) (S m2) a b H1 H2 H). -intro.elim H3. -apply H4. -intros. -generalize in match (mod_cr_pair (S m) (S m2) a b H1 H2 H). -intro.elim H3. -apply H5. -intros. -generalize in match (mod_cr_pair (S m) (S m2) a b H1 H2 H). -intro.elim H3. -apply eqb_elim. -intro. -rewrite > eq_to_eqb_true. -rewrite > eq_to_eqb_true. -reflexivity. -rewrite < H4. -rewrite > sym_gcd. -rewrite > gcd_mod. -apply (gcd_times_SO_to_gcd_SO ? ? (S m2)). -unfold lt.apply le_S_S.apply le_O_n. -unfold lt.apply le_S_S.apply le_O_n. -assumption. -unfold lt.apply le_S_S.apply le_O_n. -rewrite < H5. -rewrite > sym_gcd. -rewrite > gcd_mod. -apply (gcd_times_SO_to_gcd_SO ? ? (S m)). -unfold lt.apply le_S_S.apply le_O_n. -unfold lt.apply le_S_S.apply le_O_n. -rewrite > sym_times. -assumption. -unfold lt.apply le_S_S.apply le_O_n. -intro. -apply eqb_elim. -intro.apply eqb_elim. -intro.apply False_ind. -apply H6. -apply eq_gcd_times_SO. -unfold lt.apply le_S_S.apply le_O_n. -unfold lt.apply le_S_S.apply le_O_n. -rewrite < gcd_mod. -rewrite > H4. -rewrite > sym_gcd.assumption. -unfold lt.apply le_S_S.apply le_O_n. -rewrite < gcd_mod. -rewrite > H5. -rewrite > sym_gcd.assumption. -unfold lt.apply le_S_S.apply le_O_n. -intro.reflexivity. -intro.reflexivity. -qed. \ No newline at end of file +apply (nat_case1 n) +[ apply (nat_case1 m) + [ intros. + simplify. + reflexivity + | intros. + simplify. + reflexivity + ] +| apply (nat_case1 m) + [ intros. + change in \vdash (? ? ? (? ? %)) with (O). + rewrite > (sym_times (S m1) O). + rewrite > sym_times in \vdash (? ? ? %). + simplify. + reflexivity + | intros. + rewrite > H2 in H. + rewrite > H1 in H. + apply (sigma_p_times m2 m1 ? ? ? + (\lambda b,a. cr_pair (S m2) (S m1) a b) + (\lambda x. x \mod (S m2)) (\lambda x. x \mod (S m1))) + [intros.unfold cr_pair. + apply (le_to_lt_to_lt ? (pred ((S m2)*(S m1)))) + [unfold min. + apply transitive_le; + [2: apply le_min_aux_r | skip | apply le_n] + |unfold lt. + apply (nat_case ((S m2)*(S m1))) + [apply le_n|intro.apply le_n] + ] + |intros. + generalize in match (mod_cr_pair (S m2) (S m1) a b H3 H4 H). + intro.elim H5. + apply H6 + |intros. + generalize in match (mod_cr_pair (S m2) (S m1) a b H3 H4 H). + intro.elim H5. + apply H7 + |intros. + generalize in match (mod_cr_pair (S m2) (S m1) a b H3 H4 H). + intro.elim H5. + apply eqb_elim + [intro. + rewrite > eq_to_eqb_true + [rewrite > eq_to_eqb_true + [reflexivity + |rewrite < H6. + rewrite > sym_gcd. + rewrite > gcd_mod + [apply (gcd_times_SO_to_gcd_SO ? ? (S m1)) + [unfold lt.apply le_S_S.apply le_O_n + |unfold lt.apply le_S_S.apply le_O_n + |assumption + ] + |unfold lt.apply le_S_S.apply le_O_n + ] + ] + |rewrite < H7. + rewrite > sym_gcd. + rewrite > gcd_mod + [apply (gcd_times_SO_to_gcd_SO ? ? (S m2)) + [unfold lt.apply le_S_S.apply le_O_n + |unfold lt.apply le_S_S.apply le_O_n + |rewrite > sym_times.assumption + ] + |unfold lt.apply le_S_S.apply le_O_n + ] + ] + |intro. + apply eqb_elim + [intro.apply eqb_elim + [intro.apply False_ind. + apply H8. + apply eq_gcd_times_SO + [unfold lt.apply le_S_S.apply le_O_n. + |unfold lt.apply le_S_S.apply le_O_n. + |rewrite < gcd_mod + [rewrite > H6. + rewrite > sym_gcd.assumption + |unfold lt.apply le_S_S.apply le_O_n + ] + |rewrite < gcd_mod + [rewrite > H7. + rewrite > sym_gcd.assumption + |unfold lt.apply le_S_S.apply le_O_n + ] + ] + |intro.reflexivity + ] + |intro.reflexivity + ] + ] + ] + ] + ] +qed.