]> matita.cs.unibo.it Git - helm.git/blob - matita/library_auto/auto/nat/euler_theorem.ma
debian package for matita
[helm.git] / matita / library_auto / auto / 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 set "baseuri" "cic:/matita/library_auto/nat/euler_theorem".
16
17 include "auto/nat/map_iter_p.ma".
18 include "auto/nat/totient.ma".
19
20 (* a reformulation of totient using card insted of count *)
21 lemma totient_card: \forall n. 
22 totient n = card n (\lambda i.eqb (gcd i n) (S O)).
23 intro.
24 apply (nat_case n)
25 [ reflexivity
26 | intro.
27   apply (nat_case m)
28   [ reflexivity
29   | intro.
30     apply count_card1;auto
31     (*[ reflexivity
32     | auto.rewrite > gcd_n_n.
33       reflexivity
34     ]*)
35   ]
36 ]
37 qed.
38
39 theorem gcd_pi_p: \forall n,k. O < k \to k \le n \to
40 gcd n (pi_p (\lambda i.eqb (gcd i n) (S O)) k) = (S O).
41 intros 3.
42 elim H
43 [ rewrite > pi_p_S.
44   cut (eqb (gcd (S O) n) (S O) = true)
45   [ rewrite > Hcut.
46     auto
47     (*change with ((gcd n (S O)) = (S O)).
48     auto*)
49   | auto
50     (*apply eq_to_eqb_true.auto*)
51   ]
52 | rewrite > pi_p_S.
53   apply eqb_elim
54   [ intro.
55     change with 
56      ((gcd n ((S n1)*(pi_p (\lambda i.eqb (gcd i n) (S O)) n1))) = (S O)).
57     apply eq_gcd_times_SO
58     [ auto
59       (*unfold.
60       apply le_S.
61       assumption*)
62     | apply lt_O_pi_p.
63     | auto
64       (*rewrite > sym_gcd. 
65       assumption.*)
66     | apply H2.
67       auto
68       (*apply (trans_le ? (S n1))
69       [ apply le_n_Sn
70       | assumption
71       ]*)
72     ]
73   | intro.
74     change with 
75       (gcd n (pi_p (\lambda i.eqb (gcd i n) (S O)) n1) = (S O)).
76     apply H2.
77     auto
78     (*apply (trans_le ? (S n1))
79     [ apply le_n_Sn
80     | assumption
81     ]*)
82   ]
83 ]
84 qed.
85
86 theorem congruent_map_iter_p_times:\forall f:nat \to nat. \forall a,n:nat.
87 O < a \to
88 congruent
89 (map_iter_p n (\lambda i.eqb (gcd i a) (S O)) (\lambda x.f x) (S O) times)
90 (map_iter_p n (\lambda i.eqb (gcd i a) (S O)) 
91  (\lambda x.f x \mod a) (S O) times) a.     
92 intros.
93 elim n
94 [ auto
95   (*rewrite > map_iter_p_O.
96   apply (congruent_n_n ? a)*)
97 | apply (eqb_elim (gcd (S n1) a) (S O))
98   [ intro.
99     rewrite > map_iter_p_S_true
100     [ rewrite > map_iter_p_S_true
101       [ apply congruent_times
102         [ assumption
103         | auto
104           (*apply congruent_n_mod_n.
105           assumption*)
106         | (*NB qui auto non chiude il goal*)
107           assumption
108         ]
109       | auto
110         (*apply eq_to_eqb_true.
111         assumption*)
112       ]
113     | auto
114       (*apply eq_to_eqb_true.
115       assumption*)
116     ]
117   | intro. 
118     rewrite > map_iter_p_S_false
119     [ rewrite > map_iter_p_S_false
120       [ (*BN qui auto non chiude il goal*)
121         assumption
122       | auto
123         (*apply not_eq_to_eqb_false.
124         assumption*)
125       ]
126     | auto
127       (*apply not_eq_to_eqb_false.
128       assumption*)
129     ]
130   ]
131 ]
132 qed.
133
134 theorem permut_p_mod: \forall a,n. S O < n \to O < a \to gcd a n = (S O) \to
135 permut_p (\lambda x:nat.a*x \mod n) (\lambda i:nat.eqb (gcd i n) (S O)) n.
136 intros.
137 lapply (lt_S_to_lt ? ? H) as H3.
138 unfold permut_p.
139 simplify.
140 intros.
141 split
142 [ split
143   [ auto
144     (*apply lt_to_le.
145     apply lt_mod_m_m.
146     assumption*)
147   | rewrite > sym_gcd.
148     rewrite > gcd_mod
149     [ apply eq_to_eqb_true.
150       rewrite > sym_gcd.
151       apply eq_gcd_times_SO
152       [ assumption
153       | apply (gcd_SO_to_lt_O i n H).
154         auto
155         (*apply eqb_true_to_eq.
156         assumption*)
157       | auto
158         (*rewrite > sym_gcd.
159         assumption*)
160       | auto
161         (*rewrite > sym_gcd.
162         apply eqb_true_to_eq.
163         assumption*)
164       ]
165     | assumption
166    ]
167   ]
168 | intros.
169   lapply (gcd_SO_to_lt_n ? ? H H4 (eqb_true_to_eq ? ? H5)) as H9.
170   lapply (gcd_SO_to_lt_n ? ? H H7 (eqb_true_to_eq ? ? H6)) as H10.
171   lapply (gcd_SO_to_lt_O ? ? H (eqb_true_to_eq ? ? H5)) as H11.
172   lapply (gcd_SO_to_lt_O ? ? H (eqb_true_to_eq ? ? H6)) as H12.
173   unfold Not.
174   intro.
175   apply H8.
176   apply (nat_compare_elim i j)
177   [ intro.
178     absurd (j < n)
179     [ assumption
180     | apply le_to_not_lt.
181       apply (trans_le ? (j -i))
182       [ apply divides_to_le
183         [(*fattorizzare*)
184           unfold lt.auto.
185           (*apply (lt_plus_to_lt_l i).
186           simplify.
187           rewrite < (plus_minus_m_m)
188           [ assumption
189           | apply lt_to_le.
190             assumption
191           ]*)
192         | apply (gcd_SO_to_divides_times_to_divides a)
193           [ assumption
194           | auto
195             (*rewrite > sym_gcd.
196             assumption*)
197           | apply mod_O_to_divides
198             [ assumption
199             | rewrite > distr_times_minus.
200               auto
201             ]
202           ]
203         ]
204       | auto
205       ]
206     ]
207   | auto
208     (*intro.
209     assumption*)
210   | intro.
211     absurd (i < n)
212     [ assumption
213     | apply le_to_not_lt.
214       apply (trans_le ? (i -j))
215       [ apply divides_to_le
216         [(*fattorizzare*)
217           unfold lt.auto.
218           (*apply (lt_plus_to_lt_l j).
219           simplify.
220           rewrite < (plus_minus_m_m)
221           [ assumption
222           | apply lt_to_le.
223             assumption
224           ]*)
225         | apply (gcd_SO_to_divides_times_to_divides a)
226           [ assumption
227           | auto
228             (*rewrite > sym_gcd.
229             assumption*)
230           | apply mod_O_to_divides
231             [ assumption
232             | rewrite > distr_times_minus.
233               auto
234             ]
235           ]
236         ]
237       | auto
238       ]
239     ]
240   ]
241 ]
242 qed.
243
244 theorem congruent_exp_totient_SO: \forall n,a:nat. (S O) < n \to
245 gcd a n = (S O) \to congruent (exp a (totient n)) (S O) n. 
246 intros.
247 cut (O < a)
248 [ apply divides_to_congruent
249   [ auto
250     (*apply (trans_lt ? (S O)).
251     apply lt_O_S.
252     assumption*)
253   | auto
254     (*change with (O < exp a (totient n)).
255     apply lt_O_exp.
256     assumption*)
257   | apply (gcd_SO_to_divides_times_to_divides (pi_p (\lambda i.eqb (gcd i n) (S O)) n))
258     [ auto
259       (*apply (trans_lt ? (S O)).
260       apply lt_O_S. 
261       assumption*)
262     | auto
263       (*apply gcd_pi_p
264       [ apply (trans_lt ? (S O)).
265         apply lt_O_S. 
266         assumption
267       | apply le_n
268       ]*)
269     | rewrite < sym_times.
270       rewrite > times_minus_l.
271       rewrite > (sym_times (S O)).
272       rewrite < times_n_SO.
273       rewrite > totient_card.
274       rewrite > a_times_pi_p.
275       apply congruent_to_divides
276       [ auto
277         (*apply (trans_lt ? (S O)).
278         apply lt_O_S. 
279         assumption*)
280       | apply (transitive_congruent n ? 
281          (map_iter_p n (\lambda i.eqb (gcd i n) (S O)) (\lambda x.a*x \mod n) (S O) times))
282         [ auto
283           (*apply (congruent_map_iter_p_times ? n n).
284           apply (trans_lt ? (S O))
285           [ apply lt_O_S
286           | assumption
287           ]*)
288         | unfold pi_p.
289           cut ( (map_iter_p n (\lambda i:nat.eqb (gcd i n) (S O)) (\lambda n:nat.n) (S O) times)
290              = (map_iter_p n (\lambda i:nat.eqb (gcd i n) (S O)) (\lambda x:nat.a*x\mod n) (S O) times))
291           [ rewrite < Hcut1.
292             apply congruent_n_n
293           | apply (eq_map_iter_p_permut ? ? ? ? ? (λm.m))
294             [ apply assoc_times
295             | apply sym_times
296             | apply (permut_p_mod ? ? H Hcut H1)
297             | simplify.
298               apply not_eq_to_eqb_false.
299               unfold.
300               intro.
301               auto
302               (*apply (lt_to_not_eq (S O) n)
303               [ assumption
304               | apply sym_eq.
305                 assumption
306               ]*)
307             ]
308           ]
309         ]
310       ]
311     ]
312   ] 
313 | elim (le_to_or_lt_eq O a (le_O_n a));auto
314   (*[ assumption
315   | auto.absurd (gcd a n = S O)
316     [ assumption
317     | rewrite < H2.
318       simplify.
319       unfold.intro.
320       apply (lt_to_not_eq (S O) n)
321       [ assumption
322       | apply sym_eq.
323         assumption
324       ] 
325     ]
326   ]*)     
327 ]       
328 qed.  
329