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/euler_theorem".
17 include "nat/map_iter_p.ma".
18 include "nat/totient.ma".
21 lemma count_card: \forall p.\forall n.
22 p O = false \to count (S n) p = card n p.
24 [simplify.rewrite > H. reflexivity
31 lemma count_card1: \forall p.\forall n.
32 p O = false \to p n = false \to count n p = card n p.
33 intros 3.apply (nat_case n)
34 [intro.simplify.rewrite > H. reflexivity
35 |intros.rewrite > (count_card ? ? H).
36 simplify.rewrite > H1.reflexivity
41 ( a reformulation of totient using card insted of count )
43 lemma totient_card: \forall n.
44 totient n = card n (\lambda i.eqb (gcd i n) (S O)).
45 intro.apply (nat_case n)
47 |intro.apply (nat_case m)
49 |intro.apply count_card1
51 |rewrite > gcd_n_n.reflexivity
59 (*this obvious property is useful because simplify, sometimes,
60 "simplifies too much", and doesn't allow to obtain this simple result.
62 theorem card_Sn: \forall n:nat. \forall p:nat \to bool.
63 card (S n) p = (bool_to_nat (p (S n))) + (card n p).
69 (* a reformulation of totient using card insted of sigma_p *)
71 theorem totient_card_aux: \forall n,m: nat.
73 sigma_p (S (S n)) (\lambda m:nat.eqb (gcd m (S (S n))) (S O)) (\lambda x:nat. (S O))
74 = card (S n) (\lambda m:nat.eqb (gcd m (S (S n))) (S O)).
76 rewrite < H in \vdash (? ? (? % ? ?) ?).
77 rewrite < H in \vdash (? ? ? (? % ?)).
80 cut ((eqb (gcd (S O)(S (S n))) (S O) ) = true)
82 simplify in \vdash (? ? ? %).
83 rewrite > true_to_sigma_p_Sn
84 [ rewrite > false_to_sigma_p_Sn in \vdash (? ? (? ? %) ?)
85 [ simplify in \vdash (? ? % ?).
88 apply not_eq_to_eqb_false.
89 apply cic:/matita/nat/nat/not_eq_S.con.
93 [ apply (not_le_Sn_n n ?).
94 apply (transitive_le (S n) O n ? ?);
104 | apply eq_to_eqb_true.
108 | cut ((eqb (gcd (S (S n1)) (S (S n))) (S O)) = true
109 \lor (eqb (gcd (S (S n1)) (S (S n))) (S O)) = false)
112 rewrite > true_to_sigma_p_Sn
114 simplify in \vdash (? ? ? (? % ?)).
120 rewrite > false_to_sigma_p_Sn
122 simplify in \vdash (? ? ? (? % ?)).
129 | elim (eqb (gcd (S (S n1)) (S (S n))) (S O))
140 lemma totient_card: \forall n.
141 totient n = card n (\lambda i.eqb (gcd i n) (S O)).
152 (* here simplify creates problems: it seems it simplifies too much. I had to
153 * introduce the obvious theorem card_Sn.
156 rewrite > (gcd_n_n (S (S n2))).
157 cut ((eqb (S (S n2)) (S O)) = false)
159 simplify in \vdash (? ? ? (? % ?)).
161 rewrite < (plus_n_O).
163 apply (totient_card_aux n2 n2).
165 | apply not_eq_to_eqb_false.
166 apply cic:/matita/nat/nat/not_eq_S.con.
170 [ apply (not_le_Sn_n n2 ?).
171 apply (transitive_le (S n2) O n2 ? ?);
183 theorem gcd_pi_p: \forall n,k. O < k \to k \le n \to
184 gcd n (pi_p (\lambda i.eqb (gcd i n) (S O)) k) = (S O).
187 cut (eqb (gcd (S O) n) (S O) = true)
189 change with ((gcd n (S O)) = (S O)).
190 apply (transitive_eq nat (gcd n (S O)) (gcd (S O) n) (S O) ? ?);
191 [ apply (sym_eq nat (gcd (S O) n) (gcd n (S O)) ?).
192 apply (symmetric_gcd (S O) n).
193 | apply (gcd_SO_n n).
195 |apply eq_to_eqb_true.
202 ((gcd n ((S n1)*(pi_p (\lambda i.eqb (gcd i n) (S O)) n1))) = (S O)).
203 apply eq_gcd_times_SO
204 [unfold.apply le_S.assumption
206 |rewrite > sym_gcd. assumption.
208 apply (trans_le ? (S n1))[apply le_n_Sn|assumption]
212 (gcd n (pi_p (\lambda i.eqb (gcd i n) (S O)) n1) = (S O)).
214 apply (trans_le ? (S n1))[apply le_n_Sn|assumption]
219 theorem congruent_map_iter_p_times:\forall f:nat \to nat. \forall a,n:nat.
222 (map_iter_p n (\lambda i.eqb (gcd i a) (S O)) (\lambda x.f x) (S O) times)
223 (map_iter_p n (\lambda i.eqb (gcd i a) (S O))
224 (\lambda x.f x \mod a) (S O) times) a.
227 [rewrite > map_iter_p_O.
228 apply (congruent_n_n ? a)
229 |apply (eqb_elim (gcd (S n1) a) (S O))
231 rewrite > map_iter_p_S_true
232 [rewrite > map_iter_p_S_true
233 [apply congruent_times
235 |apply congruent_n_mod_n.assumption
238 |apply eq_to_eqb_true.assumption
240 |apply eq_to_eqb_true.assumption
243 rewrite > map_iter_p_S_false
244 [rewrite > map_iter_p_S_false
246 |apply not_eq_to_eqb_false.assumption
248 |apply not_eq_to_eqb_false.assumption
254 theorem permut_p_mod: \forall a,n. S O < n \to O < a \to gcd a n = (S O) \to
255 permut_p (\lambda x:nat.a*x \mod n) (\lambda i:nat.eqb (gcd i n) (S O)) n.
257 lapply (lt_S_to_lt ? ? H) as H3.
268 [apply eq_to_eqb_true.
270 apply eq_gcd_times_SO
272 |apply (gcd_SO_to_lt_O i n H).
273 apply eqb_true_to_eq.
275 |rewrite > sym_gcd.assumption
276 |rewrite > sym_gcd.apply eqb_true_to_eq.
283 lapply (gcd_SO_to_lt_n ? ? H H4 (eqb_true_to_eq ? ? H5)) as H9.
284 lapply (gcd_SO_to_lt_n ? ? H H7 (eqb_true_to_eq ? ? H6)) as H10.
285 lapply (gcd_SO_to_lt_O ? ? H (eqb_true_to_eq ? ? H5)) as H11.
286 lapply (gcd_SO_to_lt_O ? ? H (eqb_true_to_eq ? ? H6)) as H12.
289 apply (nat_compare_elim i j)
294 apply (trans_le ? (j -i))
297 apply (lt_plus_to_lt_l i).
299 rewrite < (plus_minus_m_m)
300 [assumption|apply lt_to_le.assumption]
301 |apply (gcd_SO_to_divides_times_to_divides a)
303 |rewrite > sym_gcd.assumption
304 |apply mod_O_to_divides
306 |rewrite > distr_times_minus.
307 apply (divides_to_mod_O n (minus (times a j) (times a i)) ? ?);
309 | apply (eq_mod_to_divides (times a j) (times a i) n ? ?);
311 |apply (sym_eq nat (mod (times a i) n) (mod (times a j) n) ?).
318 | apply (le_minus_m j i).
326 apply (trans_le ? (i -j))
329 apply (lt_plus_to_lt_l j).
331 rewrite < (plus_minus_m_m)
332 [assumption|apply lt_to_le.assumption]
333 |apply (gcd_SO_to_divides_times_to_divides a)
335 |rewrite > sym_gcd.assumption
336 |apply mod_O_to_divides
338 |rewrite > distr_times_minus.
339 apply (divides_to_mod_O n (minus (times a i) (times a j)) ? ?);
341 | apply (eq_mod_to_divides (times a i) (times a j) n ? ?);
349 | apply (le_minus_m i j).
356 theorem congruent_exp_totient_SO: \forall n,a:nat. (S O) < n \to
357 gcd a n = (S O) \to congruent (exp a (totient n)) (S O) n.
360 [ apply divides_to_congruent
361 [apply (trans_lt ? (S O)).apply lt_O_S. assumption
362 |change with (O < exp a (totient n)).apply lt_O_exp.assumption
363 |apply (gcd_SO_to_divides_times_to_divides (pi_p (\lambda i.eqb (gcd i n) (S O)) n))
364 [apply (trans_lt ? (S O)).apply lt_O_S. assumption
366 [apply (trans_lt ? (S O)).apply lt_O_S. assumption
369 |rewrite < sym_times.
370 rewrite > times_minus_l.
371 rewrite > (sym_times (S O)).
372 rewrite < times_n_SO.
373 rewrite > totient_card.
374 rewrite > a_times_pi_p.
375 apply congruent_to_divides
376 [apply (trans_lt ? (S O)).apply lt_O_S. assumption
377 | apply (transitive_congruent n ?
378 (map_iter_p n (\lambda i.eqb (gcd i n) (S O)) (\lambda x.a*x \mod n) (S O) times))
379 [apply (congruent_map_iter_p_times ? n n).
380 apply (trans_lt ? (S O))
381 [apply lt_O_S|assumption]
383 cut ( (map_iter_p n (\lambda i:nat.eqb (gcd i n) (S O)) (\lambda n:nat.n) (S O) times)
384 = (map_iter_p n (\lambda i:nat.eqb (gcd i n) (S O)) (\lambda x:nat.a*x\mod n) (S O) times))
385 [rewrite < Hcut1.apply congruent_n_n
386 |apply (eq_map_iter_p_permut ? ? ? ? ? (λm.m))
389 |apply (permut_p_mod ? ? H Hcut H1)
391 apply not_eq_to_eqb_false.
393 apply (lt_to_not_eq (S O) n)
394 [assumption|apply sym_eq.assumption]
401 |elim (le_to_or_lt_eq O a (le_O_n a))
403 |absurd (gcd a n = S O)
408 apply (lt_to_not_eq (S O) n)
409 [assumption|apply sym_eq.assumption]