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/count.ma".
18 include "nat/chinese_reminder.ma".
20 definition totient : nat \to nat \def
21 \lambda n. count n (\lambda m. eqb (gcd m n) (S O)).
23 theorem totient3: totient (S(S(S O))) = (S(S O)).
27 theorem totient6: totient (S(S(S(S(S(S O)))))) = (S(S O)).
31 theorem totient_times: \forall n,m:nat. (gcd m n) = (S O) \to
32 totient (n*m) = (totient n)*(totient m).
35 [intros.simplify.reflexivity
36 |intros 2.apply (nat_case m1)
38 rewrite < (sym_times (totient O)).
39 simplify.intro.reflexivity.
42 apply (count_times m m2 ? ? ?
43 (\lambda b,a. cr_pair (S m) (S m2) a b)
44 (\lambda x. x \mod (S m)) (\lambda x. x \mod (S m2)))
45 [intros.unfold cr_pair.
46 apply (le_to_lt_to_lt ? (pred ((S m)*(S m2))))
50 apply (nat_case ((S m)*(S m2)))
51 [apply le_n|intro.apply le_n]
54 generalize in match (mod_cr_pair (S m) (S m2) a b H1 H2 H).
58 generalize in match (mod_cr_pair (S m) (S m2) a b H1 H2 H).
62 generalize in match (mod_cr_pair (S m) (S m2) a b H1 H2 H).
66 rewrite > eq_to_eqb_true
67 [rewrite > eq_to_eqb_true
72 [apply (gcd_times_SO_to_gcd_SO ? ? (S m2))
73 [unfold lt.apply le_S_S.apply le_O_n
74 |unfold lt.apply le_S_S.apply le_O_n
77 |unfold lt.apply le_S_S.apply le_O_n
83 [apply (gcd_times_SO_to_gcd_SO ? ? (S m))
84 [unfold lt.apply le_S_S.apply le_O_n
85 |unfold lt.apply le_S_S.apply le_O_n
86 |rewrite > sym_times.assumption
88 |unfold lt.apply le_S_S.apply le_O_n
94 [intro.apply False_ind.
97 [unfold lt.apply le_S_S.apply le_O_n.
98 |unfold lt.apply le_S_S.apply le_O_n.
101 rewrite > sym_gcd.assumption
102 |unfold lt.apply le_S_S.apply le_O_n
106 rewrite > sym_gcd.assumption
107 |unfold lt.apply le_S_S.apply le_O_n