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
58 (*this obvious property is useful because simplify, sometimes,
59 "simplifies too much", and doesn't allow to obtain this simple result.
61 theorem card_Sn: \forall n:nat. \forall p:nat \to bool.
62 card (S n) p = (bool_to_nat (p (S n))) + (card n p).
68 (* a reformulation of totient using card insted of sigma_p *)
70 theorem totient_card_aux: \forall n,m: nat.
72 sigma_p (S (S n)) (\lambda m:nat.eqb (gcd m (S (S n))) (S O)) (\lambda x:nat. (S O))
73 = card (S n) (\lambda m:nat.eqb (gcd m (S (S n))) (S O)).
75 rewrite < H in \vdash (? ? (? % ? ?) ?).
76 rewrite < H in \vdash (? ? ? (? % ?)).
79 cut ((eqb (gcd (S O)(S (S n))) (S O) ) = true)
81 simplify in \vdash (? ? ? %).
82 rewrite > true_to_sigma_p_Sn
83 [ rewrite > false_to_sigma_p_Sn in \vdash (? ? (? ? %) ?)
84 [ simplify in \vdash (? ? % ?).
87 apply not_eq_to_eqb_false.
88 apply cic:/matita/nat/nat/not_eq_S.con.
92 [ apply (not_le_Sn_n n ?).
93 apply (transitive_le (S n) O n ? ?);
103 | apply eq_to_eqb_true.
107 | cut ((eqb (gcd (S (S n1)) (S (S n))) (S O)) = true
108 \lor (eqb (gcd (S (S n1)) (S (S n))) (S O)) = false)
111 rewrite > true_to_sigma_p_Sn
113 simplify in \vdash (? ? ? (? % ?)).
119 rewrite > false_to_sigma_p_Sn
121 simplify in \vdash (? ? ? (? % ?)).
128 | elim (eqb (gcd (S (S n1)) (S (S n))) (S O))
138 lemma totient_card: \forall n.
139 totient n = card n (\lambda i.eqb (gcd i n) (S O)).
150 (* here simplify creates problems: it seems it simplifies too much. I had to
151 * introduce the obvious theorem card_Sn.
154 rewrite > (gcd_n_n (S (S n2))).
155 cut ((eqb (S (S n2)) (S O)) = false)
157 simplify in \vdash (? ? ? (? % ?)).
159 rewrite < (plus_n_O).
161 apply (totient_card_aux n2 n2).
163 | apply not_eq_to_eqb_false.
164 apply cic:/matita/nat/nat/not_eq_S.con.
168 [ apply (not_le_Sn_n n2 ?).
169 apply (transitive_le (S n2) O n2 ? ?);
181 theorem gcd_pi_p: \forall n,k. O < k \to k \le n \to
182 gcd n (pi_p (\lambda i.eqb (gcd i n) (S O)) k) = (S O).
185 cut (eqb (gcd (S O) n) (S O) = true)
187 change with ((gcd n (S O)) = (S O)).
188 apply (transitive_eq nat (gcd n (S O)) (gcd (S O) n) (S O) ? ?);
189 [ apply (sym_eq nat (gcd (S O) n) (gcd n (S O)) ?).
190 apply (symmetric_gcd (S O) n).
191 | apply (gcd_SO_n n).
193 |apply eq_to_eqb_true.
200 ((gcd n ((S n1)*(pi_p (\lambda i.eqb (gcd i n) (S O)) n1))) = (S O)).
201 apply eq_gcd_times_SO
202 [unfold.apply le_S.assumption
204 |rewrite > sym_gcd. assumption.
206 apply (trans_le ? (S n1))[apply le_n_Sn|assumption]
210 (gcd n (pi_p (\lambda i.eqb (gcd i n) (S O)) n1) = (S O)).
212 apply (trans_le ? (S n1))[apply le_n_Sn|assumption]
217 theorem congruent_map_iter_p_times:\forall f:nat \to nat. \forall a,n:nat.
220 (map_iter_p n (\lambda i.eqb (gcd i a) (S O)) (\lambda x.f x) (S O) times)
221 (map_iter_p n (\lambda i.eqb (gcd i a) (S O))
222 (\lambda x.f x \mod a) (S O) times) a.
225 [rewrite > map_iter_p_O.
226 apply (congruent_n_n ? a)
227 |apply (eqb_elim (gcd (S n1) a) (S O))
229 rewrite > map_iter_p_S_true
230 [rewrite > map_iter_p_S_true
231 [apply congruent_times
233 |apply congruent_n_mod_n.assumption
236 |apply eq_to_eqb_true.assumption
238 |apply eq_to_eqb_true.assumption
241 rewrite > map_iter_p_S_false
242 [rewrite > map_iter_p_S_false
244 |apply not_eq_to_eqb_false.assumption
246 |apply not_eq_to_eqb_false.assumption
252 theorem permut_p_mod: \forall a,n. S O < n \to O < a \to gcd a n = (S O) \to
253 permut_p (\lambda x:nat.a*x \mod n) (\lambda i:nat.eqb (gcd i n) (S O)) n.
255 lapply (lt_S_to_lt ? ? H) as H3.
266 [apply eq_to_eqb_true.
268 apply eq_gcd_times_SO
270 |apply (gcd_SO_to_lt_O i n H).
271 apply eqb_true_to_eq.
273 |rewrite > sym_gcd.assumption
274 |rewrite > sym_gcd.apply eqb_true_to_eq.
281 lapply (gcd_SO_to_lt_n ? ? H H4 (eqb_true_to_eq ? ? H5)) as H9.
282 lapply (gcd_SO_to_lt_n ? ? H H7 (eqb_true_to_eq ? ? H6)) as H10.
283 lapply (gcd_SO_to_lt_O ? ? H (eqb_true_to_eq ? ? H5)) as H11.
284 lapply (gcd_SO_to_lt_O ? ? H (eqb_true_to_eq ? ? H6)) as H12.
287 apply (nat_compare_elim i j)
292 apply (trans_le ? (j -i))
295 apply (lt_plus_to_lt_l i).
297 rewrite < (plus_minus_m_m)
298 [assumption|apply lt_to_le.assumption]
299 |apply (gcd_SO_to_divides_times_to_divides a)
301 |rewrite > sym_gcd.assumption
302 |apply mod_O_to_divides
304 |rewrite > distr_times_minus.
305 apply (divides_to_mod_O n (minus (times a j) (times a i)) ? ?);
307 | apply (eq_mod_to_divides (times a j) (times a i) n ? ?);
309 |apply (sym_eq nat (mod (times a i) n) (mod (times a j) n) ?).
316 | apply (le_minus_m j i).
324 apply (trans_le ? (i -j))
327 apply (lt_plus_to_lt_l j).
329 rewrite < (plus_minus_m_m)
330 [assumption|apply lt_to_le.assumption]
331 |apply (gcd_SO_to_divides_times_to_divides a)
333 |rewrite > sym_gcd.assumption
334 |apply mod_O_to_divides
336 |rewrite > distr_times_minus.
337 apply (divides_to_mod_O n (minus (times a i) (times a j)) ? ?);
339 | apply (eq_mod_to_divides (times a i) (times a j) n ? ?);
347 | apply (le_minus_m i j).
354 theorem congruent_exp_totient_SO: \forall n,a:nat. (S O) < n \to
355 gcd a n = (S O) \to congruent (exp a (totient n)) (S O) n.
358 [ apply divides_to_congruent
359 [apply (trans_lt ? (S O)).apply lt_O_S. assumption
360 |change with (O < exp a (totient n)).apply lt_O_exp.assumption
361 |apply (gcd_SO_to_divides_times_to_divides (pi_p (\lambda i.eqb (gcd i n) (S O)) n))
362 [apply (trans_lt ? (S O)).apply lt_O_S. assumption
364 [apply (trans_lt ? (S O)).apply lt_O_S. assumption
367 |rewrite < sym_times.
368 rewrite > times_minus_l.
369 rewrite > (sym_times (S O)).
370 rewrite < times_n_SO.
371 rewrite > totient_card.
372 rewrite > a_times_pi_p.
373 apply congruent_to_divides
374 [apply (trans_lt ? (S O)).apply lt_O_S. assumption
375 | apply (transitive_congruent n ?
376 (map_iter_p n (\lambda i.eqb (gcd i n) (S O)) (\lambda x.a*x \mod n) (S O) times))
377 [apply (congruent_map_iter_p_times ? n n).
378 apply (trans_lt ? (S O))
379 [apply lt_O_S|assumption]
381 cut ( (map_iter_p n (\lambda i:nat.eqb (gcd i n) (S O)) (\lambda n:nat.n) (S O) times)
382 = (map_iter_p n (\lambda i:nat.eqb (gcd i n) (S O)) (\lambda x:nat.a*x\mod n) (S O) times))
383 [rewrite < Hcut1.apply congruent_n_n
384 |apply (eq_map_iter_p_permut ? ? ? ? ? (λm.m))
387 |apply (permut_p_mod ? ? H Hcut H1)
389 apply not_eq_to_eqb_false.
391 apply (lt_to_not_eq (S O) n)
392 [assumption|apply sym_eq.assumption]
399 |elim (le_to_or_lt_eq O a (le_O_n a))
401 |absurd (gcd a n = S O)
406 apply (lt_to_not_eq (S O) n)
407 [assumption|apply sym_eq.assumption]