]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/library/nat/euler_theorem.ma
- transcript: we have now two styles of mma's from grafite:
[helm.git] / helm / software / matita / library / nat / euler_theorem.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 include "nat/map_iter_p.ma".
16 include "nat/totient.ma".
17
18 (*
19 lemma count_card: \forall p.\forall n.
20 p O = false \to count (S n) p = card n p.
21 intros.elim n
22   [simplify.rewrite > H. reflexivity
23   |simplify.
24    rewrite < plus_n_O.
25    apply eq_f.assumption
26   ]
27 qed.
28
29 lemma count_card1: \forall p.\forall n.
30 p O = false \to p n = false \to count n p = card n p.
31 intros 3.apply (nat_case n)
32   [intro.simplify.rewrite > H. reflexivity
33   |intros.rewrite > (count_card ? ? H).
34    simplify.rewrite > H1.reflexivity
35   ]
36 qed.
37  
38
39 ( a reformulation of totient using card insted of count )
40
41 lemma totient_card: \forall n. 
42 totient n = card n (\lambda i.eqb (gcd i n) (S O)).
43 intro.apply (nat_case n)
44   [reflexivity
45   |intro.apply (nat_case m)
46     [reflexivity
47     |intro.apply count_card1
48       [reflexivity
49       |rewrite > gcd_n_n.reflexivity
50       ]
51     ]
52   ]
53 qed.
54 *)
55
56 (*this obvious property is useful because simplify, sometimes,
57   "simplifies too much", and doesn't allow to obtain this simple result.
58  *)
59 theorem card_Sn: \forall n:nat. \forall p:nat \to bool.
60 card (S n) p = (bool_to_nat (p (S n))) + (card n p).
61 intros.
62 simplify.
63 reflexivity.
64 qed.
65
66 (* a reformulation of totient using card insted of sigma_p *)
67
68 theorem totient_card_aux: \forall n,m: nat.
69 m = n \to
70 sigma_p (S (S n)) (\lambda m:nat.eqb (gcd m (S (S n))) (S O)) (\lambda x:nat. (S O)) 
71 = card (S n) (\lambda m:nat.eqb (gcd m (S (S n))) (S O)).
72 intros.
73 rewrite < H in \vdash (? ? (? % ? ?) ?).
74 rewrite < H in \vdash (? ? ? (? % ?)).
75 elim (m)
76 [ rewrite > card_Sn.
77   cut ((eqb (gcd (S O)(S (S n))) (S O) ) = true)
78   [ rewrite > Hcut.
79     simplify in \vdash (? ? ? %).
80     rewrite > true_to_sigma_p_Sn
81     [ rewrite > false_to_sigma_p_Sn in \vdash (? ? (? ? %) ?)
82       [ simplify in \vdash (? ? % ?).
83         reflexivity
84       | rewrite > gcd_O_n.
85         apply not_eq_to_eqb_false.
86         apply not_eq_S.             
87         unfold Not.
88         intro.        
89         cut ( (S n) \le O)
90         [ apply (not_le_Sn_n n ?).
91           apply (transitive_le (S n) O n ? ?);
92           [ apply (Hcut1)
93           | apply (le_O_n n)
94           ]
95         | rewrite > H1.
96           apply le_n
97         ]
98       ]
99     | assumption
100     ]
101   | apply eq_to_eqb_true.
102     rewrite > gcd_SO_n.
103     reflexivity   
104   ]
105 | cut ((eqb (gcd (S (S n1)) (S (S n))) (S O))  = true 
106     \lor (eqb (gcd (S (S n1)) (S (S n))) (S O))  = false)
107   [ elim Hcut
108     [ rewrite > card_Sn.
109       rewrite > true_to_sigma_p_Sn
110       [ rewrite > H2.
111         simplify in \vdash (? ? ? (? % ?)).
112         apply eq_f.
113         assumption
114       | assumption
115       ]      
116     | rewrite > card_Sn.
117       rewrite > false_to_sigma_p_Sn
118       [ rewrite > H2.
119         simplify in \vdash (? ? ? (? % ?)).
120         rewrite > sym_plus.
121         rewrite < plus_n_O.
122         assumption
123       | assumption  
124       ]
125     ]
126   | elim (eqb (gcd (S (S n1)) (S (S n))) (S O))
127     [ left.
128       reflexivity
129     | right.
130       reflexivity
131     ]
132   ]
133 ]
134 qed.
135   
136 lemma totient_card: \forall n.
137 totient n = card n (\lambda i.eqb (gcd i n) (S O)).
138 intros.
139 elim n
140 [ simplify.
141   reflexivity
142 | elim n1
143   [ simplify.
144     reflexivity
145   |
146     (*unfold card.
147     intros.*)
148     (* here simplify creates problems: it seems it simplifies too much. I had to 
149      * introduce the obvious theorem card_Sn.
150      *)
151     rewrite > card_Sn.
152     rewrite > (gcd_n_n (S (S n2))).
153     cut ((eqb (S (S n2)) (S O)) = false)
154     [ rewrite > Hcut.
155       simplify in \vdash (? ? ? (? % ?)).
156       rewrite > sym_plus.
157       rewrite < (plus_n_O).
158       unfold totient.      
159       apply (totient_card_aux n2 n2).
160       reflexivity    
161     | apply not_eq_to_eqb_false.
162       apply not_eq_S.
163       unfold Not.
164       intro.
165       cut ( (S n2) \le O)
166         [ apply (not_le_Sn_n n2 ?).
167           apply (transitive_le (S n2) O n2 ? ?);
168           [ apply (Hcut)
169           | apply (le_O_n n2)
170           ]
171         | rewrite > H2.
172           apply le_n
173         ]
174     ]
175   ]
176 ]
177 qed.
178   
179 theorem gcd_pi_p: \forall n,k. O < k \to k \le n \to
180 gcd n (pi_p (\lambda i.eqb (gcd i n) (S O)) k) = (S O).
181 intros 3.elim H
182   [rewrite > pi_p_S.
183    cut (eqb (gcd (S O) n) (S O) = true)
184     [rewrite > Hcut.
185      change with ((gcd n (S O)) = (S O)).
186      apply (transitive_eq nat (gcd n (S O)) (gcd (S O) n) (S O) ? ?);
187      [ apply (sym_eq nat (gcd (S O) n) (gcd n (S O)) ?).
188        apply (symmetric_gcd (S O) n).
189      | apply (gcd_SO_n n).
190      ]
191     |apply eq_to_eqb_true.
192      apply (gcd_SO_n n)
193     ]
194   |rewrite > pi_p_S.
195    apply eqb_elim
196     [intro.
197      change with 
198        ((gcd n ((S n1)*(pi_p (\lambda i.eqb (gcd i n) (S O)) n1))) = (S O)).
199      apply eq_gcd_times_SO
200       [unfold.apply le_S.assumption
201       |apply lt_O_pi_p.
202       |rewrite > sym_gcd. assumption.
203       |apply H2.
204        apply (trans_le ? (S n1))[apply le_n_Sn|assumption]
205       ]
206     |intro.
207      change with 
208        (gcd n (pi_p (\lambda i.eqb (gcd i n) (S O)) n1) = (S O)).
209      apply H2.
210      apply (trans_le ? (S n1))[apply le_n_Sn|assumption]
211     ]
212   ]
213 qed.
214
215 theorem congruent_map_iter_p_times:\forall f:nat \to nat. \forall a,n:nat.
216 O < a \to
217 congruent
218 (map_iter_p n (\lambda i.eqb (gcd i a) (S O)) (\lambda x.f x) (S O) times)
219 (map_iter_p n (\lambda i.eqb (gcd i a) (S O)) 
220  (\lambda x.f x \mod a) (S O) times) a.     
221 intros.
222 elim n
223   [rewrite > map_iter_p_O.
224    apply (congruent_n_n ? a)
225   |apply (eqb_elim (gcd (S n1) a) (S O))
226     [intro.
227      rewrite > map_iter_p_S_true
228       [rewrite > map_iter_p_S_true
229         [apply congruent_times
230           [assumption
231           |apply congruent_n_mod_n.assumption
232           |assumption
233           ]
234         |apply eq_to_eqb_true.assumption
235         ]
236       |apply eq_to_eqb_true.assumption
237       ]
238     |intro. 
239      rewrite > map_iter_p_S_false
240       [rewrite > map_iter_p_S_false
241         [assumption
242         |apply not_eq_to_eqb_false.assumption
243         ]
244       |apply not_eq_to_eqb_false.assumption
245       ]
246     ]
247   ]
248 qed.
249
250 theorem permut_p_mod: \forall a,n. S O < n \to O < a \to gcd a n = (S O) \to
251 permut_p (\lambda x:nat.a*x \mod n) (\lambda i:nat.eqb (gcd i n) (S O)) n.
252 intros.
253 lapply (lt_S_to_lt ? ? H) as H3.
254 unfold permut_p.
255 simplify.
256 intros.
257 split
258   [split
259     [apply lt_to_le.
260      apply lt_mod_m_m.
261      assumption
262     |rewrite > sym_gcd.
263      rewrite > gcd_mod
264       [apply eq_to_eqb_true.
265        rewrite > sym_gcd.
266        apply eq_gcd_times_SO
267         [assumption
268         |apply (gcd_SO_to_lt_O i n H).
269          apply eqb_true_to_eq.
270          assumption
271         |rewrite > sym_gcd.assumption
272         |rewrite > sym_gcd.apply eqb_true_to_eq.
273          assumption
274         ]
275       |assumption
276       ]
277     ]
278   |intros.
279    lapply (gcd_SO_to_lt_n ? ? H H4 (eqb_true_to_eq ? ? H5)) as H9.
280    lapply (gcd_SO_to_lt_n ? ? H H7 (eqb_true_to_eq ? ? H6)) as H10.
281    lapply (gcd_SO_to_lt_O ? ? H (eqb_true_to_eq ? ? H5)) as H11.
282    lapply (gcd_SO_to_lt_O ? ? H (eqb_true_to_eq ? ? H6)) as H12.
283    unfold Not.intro.
284    apply H8.
285    apply (nat_compare_elim i j)
286     [intro.
287      absurd (j < n)
288       [assumption
289       |apply le_to_not_lt.
290        apply (trans_le ? (j -i))
291         [apply divides_to_le
292           [(*fattorizzare*)
293            apply (lt_plus_to_lt_l i).
294            simplify.
295            rewrite < (plus_minus_m_m)
296             [assumption|apply lt_to_le.assumption]
297           |apply (gcd_SO_to_divides_times_to_divides a)
298             [assumption
299             |rewrite > sym_gcd.assumption
300             |apply mod_O_to_divides
301               [assumption
302               |rewrite > distr_times_minus.
303                apply (divides_to_mod_O n (minus (times a j) (times a i)) ? ?);
304                [ apply (H3).
305                | apply (eq_mod_to_divides (times a j) (times a i) n ? ?);
306                 [ apply (H3).
307                 |apply (sym_eq nat (mod (times a i) n) (mod (times a j) n) ?).
308                  apply (H13).
309                 ]
310                ]
311               ]
312             ]
313           ]
314         | apply (le_minus_m j i).
315         ]
316       ]
317     |intro.assumption
318     |intro.
319      absurd (i < n)
320       [assumption
321       |apply le_to_not_lt.
322        apply (trans_le ? (i -j))
323         [apply divides_to_le
324           [(*fattorizzare*)
325            apply (lt_plus_to_lt_l j).
326            simplify.
327            rewrite < (plus_minus_m_m)
328             [assumption|apply lt_to_le.assumption]
329           |apply (gcd_SO_to_divides_times_to_divides a)
330             [assumption
331             |rewrite > sym_gcd.assumption
332             |apply mod_O_to_divides
333               [assumption
334               |rewrite > distr_times_minus.
335                apply (divides_to_mod_O n (minus (times a i) (times a j)) ? ?);
336                [apply (H3).
337                | apply (eq_mod_to_divides (times a i) (times a j) n ? ?);
338                  [apply (H3).
339                  |apply (H13).
340                  ]
341                ]
342               ]
343             ]
344           ]
345         | apply (le_minus_m i j).
346         ]
347       ]
348     ]
349   ]
350 qed.
351
352 theorem congruent_exp_totient_SO: \forall n,a:nat. (S O) < n \to
353 gcd a n = (S O) \to congruent (exp a (totient n)) (S O) n. 
354 intros.
355 cut (O < a)
356   [ apply divides_to_congruent
357     [apply (trans_lt ? (S O)).apply lt_O_S. assumption
358     |change with (O < exp a (totient n)).apply lt_O_exp.assumption
359     |apply (gcd_SO_to_divides_times_to_divides (pi_p (\lambda i.eqb (gcd i n) (S O)) n))
360       [apply (trans_lt ? (S O)).apply lt_O_S. assumption
361       |apply gcd_pi_p
362         [apply (trans_lt ? (S O)).apply lt_O_S. assumption
363         |apply le_n
364         ]
365       |rewrite < sym_times.
366        rewrite > times_minus_l.
367        rewrite > (sym_times (S O)).
368        rewrite < times_n_SO.
369        rewrite > totient_card.
370        rewrite > a_times_pi_p.
371        apply congruent_to_divides
372         [apply (trans_lt ? (S O)).apply lt_O_S. assumption
373         | apply (transitive_congruent n ? 
374                  (map_iter_p n (\lambda i.eqb (gcd i n) (S O)) (\lambda x.a*x \mod n) (S O) times))
375           [apply (congruent_map_iter_p_times ? n n).
376            apply (trans_lt ? (S O))
377             [apply lt_O_S|assumption]
378             |unfold pi_p.
379              cut ( (map_iter_p n (\lambda i:nat.eqb (gcd i n) (S O)) (\lambda n:nat.n) (S O) times)
380                  = (map_iter_p n (\lambda i:nat.eqb (gcd i n) (S O)) (\lambda x:nat.a*x\mod n) (S O) times))
381               [rewrite < Hcut1.apply congruent_n_n
382               |apply (eq_map_iter_p_permut ? ? ? ? ? (λm.m))
383                 [apply assoc_times
384                 |apply sym_times
385                 |apply (permut_p_mod ? ? H Hcut H1)
386                 |simplify.
387                  apply not_eq_to_eqb_false.
388                  unfold.intro.
389                  apply (lt_to_not_eq (S O) n)
390                   [assumption|apply sym_eq.assumption]
391                 ]
392               ]
393             ]
394           ]
395         ]
396       ] 
397     |elim (le_to_or_lt_eq O a (le_O_n a)) 
398       [assumption
399       |absurd (gcd a n = S O)
400         [assumption
401         |rewrite < H2.
402          simplify.
403          unfold.intro.
404          apply (lt_to_not_eq (S O) n)
405           [assumption|apply sym_eq.assumption] 
406         ]
407       ]     
408     ]
409 qed.