]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/library/nat/totient1.ma
some theorems have been moved to more appropriate files in library.
[helm.git] / helm / software / matita / library / nat / totient1.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 set "baseuri" "cic:/matita/nat/totient1".
16
17 include "nat/totient.ma".
18 include "nat/iteration2.ma".
19 include "nat/gcd_properties1.ma".
20
21 (* This file contains the proof of the following theorem about Euler's totient
22  * function:
23  
24    The sum of the applications of Phi function over the divisor of a natural
25    number n is equal to n
26  *)
27
28 theorem eq_div_times_div_times: \forall a,b,c:nat.
29 O \lt b \to b \divides a \to b \divides c \to
30 a / b * c = a * (c/b).
31 intros.
32 elim H1.
33 elim H2.
34 rewrite > H3.
35 rewrite > H4.    
36 rewrite > (sym_times) in \vdash (? ? ? (? ? (? % ?))).
37 rewrite > (sym_times) in \vdash (? ? (? (? % ?) ?) ?).
38 rewrite > (lt_O_to_div_times ? ? H).
39 rewrite > (lt_O_to_div_times ? ? H) in \vdash (? ? ? (? ? %)).
40 rewrite > (sym_times b n2).
41 rewrite > assoc_times.
42 reflexivity.
43 qed.
44     
45 theorem lt_O_to_divides_to_lt_O_div:
46 \forall a,b:nat.
47 O \lt b \to a \divides b \to O \lt (b/a).
48 intros.
49 apply (O_lt_times_to_O_lt ? a).
50 rewrite > (divides_to_times_div b a)
51 [ assumption
52 | apply (divides_to_lt_O a b H H1)
53 | assumption
54 ]
55 qed.
56
57 (*tha main theorem*) 
58 theorem sigma_p_Sn_divides_b_totient_n': \forall n. O \lt n \to sigma_p (S n) (\lambda d.divides_b d n) totient = n.
59 intros. 
60 unfold totient.
61 apply (trans_eq ? ? 
62 (sigma_p (S n) (\lambda d:nat.divides_b d n)
63 (\lambda d:nat.sigma_p (S n) (\lambda m:nat.andb (leb (S m) d) (eqb (gcd m d) (S O))) (\lambda m:nat.S O))))
64 [ apply eq_sigma_p1
65   [ intros.
66     reflexivity
67   | intros.
68     apply sym_eq.
69     apply (trans_eq ? ? 
70      (sigma_p x (\lambda m:nat.leb (S m) x\land eqb (gcd m x) (S O)) (\lambda m:nat.S O)))
71     [ apply false_to_eq_sigma_p
72       [ apply lt_to_le.          
73         assumption
74       | intros.
75         rewrite > lt_to_leb_false
76         [ reflexivity
77         | apply le_S_S.
78           assumption
79         ]
80       ]
81     | apply eq_sigma_p
82       [ intros.
83         rewrite > le_to_leb_true
84         [ reflexivity
85         | assumption
86         ]
87       | intros.
88         reflexivity
89       ]
90     ]
91   ]
92 | apply (trans_eq ? ? (sigma_p n (\lambda x.true) (\lambda x.S O)))
93   [ apply sym_eq.
94     apply (sigma_p_knm
95      (\lambda x. (S O))
96      (\lambda i,j.j*(n/i))
97      (\lambda p. n / (gcd p n))
98      (\lambda p. p / (gcd p n))
99     );intros
100     [ cut (O \lt (gcd x n))
101       [split
102       [ split
103         [ split
104           [ split
105             [ apply divides_to_divides_b_true
106               [ apply (O_lt_times_to_O_lt ? (gcd x n)).
107                 rewrite > (divides_to_times_div n (gcd x n))
108                 [ assumption
109                 | assumption
110                 | apply (divides_gcd_m)
111                 ]
112               | rewrite > sym_gcd.
113                 apply (divides_times_to_divides_div_gcd).
114                 apply (witness n (x * n) x).
115                 apply (symmetric_times x n)
116               ]
117             | apply (true_to_true_to_andb_true)
118               [ apply (le_to_leb_true).
119                 change with (x/(gcd x n) \lt n/(gcd x n)).
120                 apply (lt_times_n_to_lt (gcd x n) ? ?)
121                 [ assumption
122                 | rewrite > (divides_to_times_div x (gcd x n))
123                   [ rewrite > (divides_to_times_div n (gcd x n))
124                     [ assumption
125                     | assumption
126                     | apply divides_gcd_m
127                     ]
128                   | assumption
129                   | apply divides_gcd_n
130                   ]
131                 ]
132               | apply cic:/matita/nat/compare/eq_to_eqb_true.con.
133                 rewrite > (eq_gcd_div_div_div_gcd x n (gcd x n))
134                 [ apply (div_n_n (gcd x n) Hcut)
135                 | assumption
136                 | apply divides_gcd_n
137                 | apply divides_gcd_m                  
138                 ]
139               ]
140             ] 
141           | apply (inj_times_l1 (n/(gcd x n)))
142             [ apply lt_O_to_divides_to_lt_O_div
143               [ assumption
144               | apply divides_gcd_m 
145               ]
146             | rewrite > associative_times.
147               rewrite > (divides_to_times_div n (n/(gcd x n)))
148               [ apply eq_div_times_div_times
149                 [ assumption
150                 | apply divides_gcd_n
151                 | apply divides_gcd_m
152                 ]
153                 (*rewrite > sym_times.
154                 rewrite > (divides_to_eq_times_div_div_times n).
155                 rewrite > (divides_to_eq_times_div_div_times x).
156                 rewrite > (sym_times n x).
157                 reflexivity. 
158                 assumption.
159                 apply divides_gcd_m.
160                 apply (divides_to_lt_O (gcd x n)).
161                 apply lt_O_gcd.
162                 assumption.                
163                 apply divides_gcd_n.*)
164               | apply lt_O_to_divides_to_lt_O_div
165                 [ assumption
166                 | apply divides_gcd_m 
167                 ] 
168               | apply (witness ? ? (gcd x n)).
169                 rewrite > divides_to_times_div
170                 [ reflexivity
171                 | assumption
172                 | apply divides_gcd_m
173                 
174                 ]                
175               ]
176             ]  
177           ]
178         | apply (le_to_lt_to_lt ? n)
179           [ apply cic:/matita/Z/dirichlet_product/le_div.con.
180             assumption
181           | change with ((S n) \le (S n)).
182             apply le_n 
183           ]
184         ]
185       | apply (le_to_lt_to_lt ? x)
186         [ apply cic:/matita/Z/dirichlet_product/le_div.con.
187           assumption   
188         | apply (trans_lt ? n ?)
189           [ assumption
190           | change with ((S n) \le (S n)).
191             apply le_n
192           ]
193         ]
194       ]
195     | apply (divides_to_lt_O ? n)
196       [ assumption
197       | apply divides_gcd_m
198       ]
199     ]  
200     | cut (i \divides n)
201       [ cut (j \lt i)
202         [ cut ((gcd j i) = (S O) )
203           [ cut ((gcd (j*(n/i)) n) = n/i)
204             [ split
205               [ split
206                 [ split
207                   [ reflexivity
208                   | rewrite > Hcut3.
209                     apply (cic:/matita/Z/dirichlet_product/div_div.con);
210                       assumption
211                   ]               
212                 | rewrite > Hcut3.
213                   rewrite < divides_to_eq_times_div_div_times
214                   [ rewrite > div_n_n  
215                     [ apply sym_eq.
216                       apply times_n_SO.
217                     | apply lt_O_to_divides_to_lt_O_div; (*n/i 1*)
218                         assumption
219                     ]
220                   | apply lt_O_to_divides_to_lt_O_div; (*n/i 2*)
221                       assumption
222                   | apply divides_n_n
223                   ]
224                 ]
225               | rewrite < (divides_to_times_div n i) in \vdash (? ? %)
226                 [ rewrite > sym_times.
227                   apply (lt_times_r1)
228                   [ apply lt_O_to_divides_to_lt_O_div; (*n/i 3*)
229                       assumption
230                   | assumption
231                   ]
232                 | apply (divides_to_lt_O i n); assumption
233                 | assumption
234                 ]               
235               ]
236             | rewrite < (divides_to_times_div n i) in \vdash (? ? (? ? %) ?)
237               [ rewrite > (sym_times j).
238                 rewrite > times_n_SO in \vdash (? ? ? %).
239                 rewrite < Hcut2.
240                 apply eq_gcd_times_times_times_gcd.                
241               | apply (divides_to_lt_O i n); assumption
242               | assumption
243               ]
244             ]
245           | apply eqb_true_to_eq.
246             apply (andb_true_true_r (leb (S j) i)).            
247             assumption            
248           ]
249         | change with ((S j) \le i).
250           cut((leb (S j) i) = true)
251           [ change with(
252             match (true) with
253             [ true  \Rightarrow ((S j) \leq i) 
254             | false \Rightarrow ((S j) \nleq i)]
255             ).
256             rewrite < Hcut1.
257             apply (leb_to_Prop)
258           | apply (andb_true_true (leb (S j) i) (eqb (gcd j i) (S O))).            
259             assumption
260           ]
261         ]
262         | apply (divides_b_true_to_divides).
263           assumption
264       ]
265     ]
266   | apply (sigma_p_true).
267   ]
268 ]
269 qed.  
270     
271