1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| A.Asperti, C.Sacerdoti Coen, *)
8 (* ||A|| E.Tassi, S.Zacchiroli *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU Lesser General Public License Version 2.1 *)
13 (**************************************************************************)
15 set "baseuri" "cic:/matita/nat/totient".
17 include "nat/chinese_reminder.ma".
18 include "nat/iteration2.ma".
20 (*a new definition of totient, which uses sigma_p instead of sigma *)
21 (*there's a little difference between this definition and the classic one:
22 the classic definition of totient is:
24 phi (n) is the number of naturals i (less or equal than n) so then gcd (i,n) = 1.
25 (so this definition considers the values i=1,2,...,n)
27 sigma_p doesn't work on the value n (but the first value it works on is (pred n))
28 but works also on 0. That's not a problem, in fact
29 - if n <> 1, gcd (n,0) <>1 and gcd (n,n) = n <> 1.
30 - if n = 1, then Phi(n) = 1, and (totient n), as defined below, returns 1.
33 definition totient : nat \to nat \def
34 \lambda n.sigma_p n (\lambda m. eqb (gcd m n) (S O)) (\lambda m.S O).
36 lemma totient1: totient (S(S(S(S(S(S O)))))) = ?.
39 theorem totient_times: \forall n,m:nat. (gcd m n) = (S O) \to
40 totient (n*m) = (totient n)*(totient m).
54 change in \vdash (? ? ? (? ? %)) with (O).
55 rewrite > (sym_times (S m1) O).
56 rewrite > sym_times in \vdash (? ? ? %).
62 apply (sigma_p_times m2 m1 ? ? ?
63 (\lambda b,a. cr_pair (S m2) (S m1) a b)
64 (\lambda x. x \mod (S m2)) (\lambda x. x \mod (S m1)))
65 [intros.unfold cr_pair.
66 apply (le_to_lt_to_lt ? (pred ((S m2)*(S m1))))
69 [2: apply le_min_aux_r | skip | apply le_n]
71 apply (nat_case ((S m2)*(S m1)))
72 [apply le_n|intro.apply le_n]
75 generalize in match (mod_cr_pair (S m2) (S m1) a b H3 H4 H).
79 generalize in match (mod_cr_pair (S m2) (S m1) a b H3 H4 H).
83 generalize in match (mod_cr_pair (S m2) (S m1) a b H3 H4 H).
87 rewrite > eq_to_eqb_true
88 [rewrite > eq_to_eqb_true
93 [apply (gcd_times_SO_to_gcd_SO ? ? (S m1))
94 [unfold lt.apply le_S_S.apply le_O_n
95 |unfold lt.apply le_S_S.apply le_O_n
98 |unfold lt.apply le_S_S.apply le_O_n
104 [apply (gcd_times_SO_to_gcd_SO ? ? (S m2))
105 [unfold lt.apply le_S_S.apply le_O_n
106 |unfold lt.apply le_S_S.apply le_O_n
107 |rewrite > sym_times.assumption
109 |unfold lt.apply le_S_S.apply le_O_n
114 [intro.apply eqb_elim
115 [intro.apply False_ind.
117 apply eq_gcd_times_SO
118 [unfold lt.apply le_S_S.apply le_O_n.
119 |unfold lt.apply le_S_S.apply le_O_n.
122 rewrite > sym_gcd.assumption
123 |unfold lt.apply le_S_S.apply le_O_n
127 rewrite > sym_gcd.assumption
128 |unfold lt.apply le_S_S.apply le_O_n