]> matita.cs.unibo.it Git - helm.git/blob - helm/matita/library/nat/totient.ma
fix
[helm.git] / helm / matita / library / nat / totient.ma
1 (**************************************************************************)
2 (*       __                                                               *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
8 (*      ||A||       E.Tassi, S.Zacchiroli                                 *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU Lesser General Public License Version 2.1         *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 set "baseuri" "cic:/matita/nat/totient".
16
17 include "nat/count.ma".
18 include "nat/chinese_reminder.ma".
19
20 definition totient : nat \to nat \def
21 \lambda n. count n (\lambda m. eqb (gcd m n) (S O)).
22
23 theorem totient3: totient (S(S(S O))) = (S(S O)).
24 reflexivity.
25 qed.
26
27 theorem totient6: totient (S(S(S(S(S(S O)))))) = (S(S O)).
28 reflexivity.
29 qed.
30
31 theorem totient_times: \forall n,m:nat. (gcd m n) = (S O) \to
32 totient (n*m) = (totient n)*(totient m).
33 intro.
34 apply (nat_case n).
35 intro.simplify.intro.reflexivity.
36 intros 2.apply (nat_case m1).
37 rewrite < sym_times.
38 rewrite < (sym_times (totient O)).
39 simplify.intro.reflexivity.
40 intros.
41 unfold totient.
42 apply (count_times m m2 ? ? ? 
43 (\lambda b,a. cr_pair (S m) (S m2) a b) (\lambda x. x \mod (S m)) (\lambda x. x \mod (S m2))).
44 intros.unfold cr_pair.
45 apply (le_to_lt_to_lt ? (pred ((S m)*(S m2)))).
46 unfold min.
47 apply le_min_aux_r.
48 change with ((S (pred ((S m)*(S m2)))) \le ((S m)*(S m2))).
49 apply (nat_case ((S m)*(S m2))).apply le_n.
50 intro.apply le_n.
51 intros.
52 generalize in match (mod_cr_pair (S m) (S m2) a b H1 H2 H).
53 intro.elim H3.
54 apply H4.
55 intros.
56 generalize in match (mod_cr_pair (S m) (S m2) a b H1 H2 H).
57 intro.elim H3.
58 apply H5.
59 intros.
60 generalize in match (mod_cr_pair (S m) (S m2) a b H1 H2 H).
61 intro.elim H3.
62 apply eqb_elim.
63 intro.
64 rewrite > eq_to_eqb_true.
65 rewrite > eq_to_eqb_true.
66 reflexivity.
67 rewrite < H4.
68 rewrite > sym_gcd.
69 rewrite > gcd_mod.
70 apply (gcd_times_SO_to_gcd_SO ? ? (S m2)).
71 unfold lt.apply le_S_S.apply le_O_n.
72 unfold lt.apply le_S_S.apply le_O_n.
73 assumption.
74 unfold lt.apply le_S_S.apply le_O_n.
75 rewrite < H5.
76 rewrite > sym_gcd.
77 rewrite > gcd_mod.
78 apply (gcd_times_SO_to_gcd_SO ? ? (S m)).
79 unfold lt.apply le_S_S.apply le_O_n.
80 unfold lt.apply le_S_S.apply le_O_n.
81 rewrite > sym_times.
82 assumption.
83 unfold lt.apply le_S_S.apply le_O_n.
84 intro.
85 apply eqb_elim.
86 intro.apply eqb_elim.
87 intro.apply False_ind.
88 apply H6.
89 apply eq_gcd_times_SO.
90 unfold lt.apply le_S_S.apply le_O_n.
91 unfold lt.apply le_S_S.apply le_O_n.
92 rewrite < gcd_mod.
93 rewrite > H4.
94 rewrite > sym_gcd.assumption.
95 unfold lt.apply le_S_S.apply le_O_n.
96 rewrite < gcd_mod.
97 rewrite > H5.
98 rewrite > sym_gcd.assumption.
99 unfold lt.apply le_S_S.apply le_O_n.
100 intro.reflexivity.
101 intro.reflexivity.
102 qed.