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".
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.apply (nat_case n)
25 |intro.apply (nat_case m)
27 |intro.apply count_card1
29 |rewrite > gcd_n_n.reflexivity
35 theorem gcd_pi_p: \forall n,k. O < k \to k \le n \to
36 gcd n (pi_p (\lambda i.eqb (gcd i n) (S O)) k) = (S O).
39 cut (eqb (gcd (S O) n) (S O) = true)
41 change with ((gcd n (S O)) = (S O)).auto
42 |apply eq_to_eqb_true.auto
48 ((gcd n ((S n1)*(pi_p (\lambda i.eqb (gcd i n) (S O)) n1))) = (S O)).
50 [unfold.apply le_S.assumption
52 |rewrite > sym_gcd. assumption.
54 apply (trans_le ? (S n1))[apply le_n_Sn|assumption]
58 (gcd n (pi_p (\lambda i.eqb (gcd i n) (S O)) n1) = (S O)).
60 apply (trans_le ? (S n1))[apply le_n_Sn|assumption]
65 theorem congruent_map_iter_p_times:\forall f:nat \to nat. \forall a,n:nat.
68 (map_iter_p n (\lambda i.eqb (gcd i a) (S O)) (\lambda x.f x) (S O) times)
69 (map_iter_p n (\lambda i.eqb (gcd i a) (S O))
70 (\lambda x.f x \mod a) (S O) times) a.
73 [rewrite > map_iter_p_O.
74 apply (congruent_n_n ? a)
75 |apply (eqb_elim (gcd (S n1) a) (S O))
77 rewrite > map_iter_p_S_true
78 [rewrite > map_iter_p_S_true
79 [apply congruent_times
81 |apply congruent_n_mod_n.assumption
84 |apply eq_to_eqb_true.assumption
86 |apply eq_to_eqb_true.assumption
89 rewrite > map_iter_p_S_false
90 [rewrite > map_iter_p_S_false
92 |apply not_eq_to_eqb_false.assumption
94 |apply not_eq_to_eqb_false.assumption
100 theorem permut_p_mod: \forall a,n. S O < n \to O < a \to gcd a n = (S O) \to
101 permut_p (\lambda x:nat.a*x \mod n) (\lambda i:nat.eqb (gcd i n) (S O)) n.
103 lapply (lt_S_to_lt ? ? H) as H3.
114 [apply eq_to_eqb_true.
116 apply eq_gcd_times_SO
118 |apply (gcd_SO_to_lt_O i n H).
119 apply eqb_true_to_eq.
121 |rewrite > sym_gcd.assumption
122 |rewrite > sym_gcd.apply eqb_true_to_eq.
129 lapply (gcd_SO_to_lt_n ? ? H H4 (eqb_true_to_eq ? ? H5)) as H9.
130 lapply (gcd_SO_to_lt_n ? ? H H7 (eqb_true_to_eq ? ? H6)) as H10.
131 lapply (gcd_SO_to_lt_O ? ? H (eqb_true_to_eq ? ? H5)) as H11.
132 lapply (gcd_SO_to_lt_O ? ? H (eqb_true_to_eq ? ? H6)) as H12.
135 apply (nat_compare_elim i j)
140 apply (trans_le ? (j -i))
143 apply (lt_plus_to_lt_l i).
145 rewrite < (plus_minus_m_m)
146 [assumption|apply lt_to_le.assumption]
147 |apply (gcd_SO_to_divides_times_to_divides a)
149 |rewrite > sym_gcd.assumption
150 |apply mod_O_to_divides
152 |rewrite > distr_times_minus.
165 apply (trans_le ? (i -j))
168 apply (lt_plus_to_lt_l j).
170 rewrite < (plus_minus_m_m)
171 [assumption|apply lt_to_le.assumption]
172 |apply (gcd_SO_to_divides_times_to_divides a)
174 |rewrite > sym_gcd.assumption
175 |apply mod_O_to_divides
177 |rewrite > distr_times_minus.
189 theorem congruent_exp_totient_SO: \forall n,a:nat. (S O) < n \to
190 gcd a n = (S O) \to congruent (exp a (totient n)) (S O) n.
193 [apply divides_to_congruent
194 [apply (trans_lt ? (S O)).apply lt_O_S. assumption
195 |change with (O < exp a (totient n)).apply lt_O_exp.assumption
196 |apply (gcd_SO_to_divides_times_to_divides (pi_p (\lambda i.eqb (gcd i n) (S O)) n))
197 [apply (trans_lt ? (S O)).apply lt_O_S. assumption
199 [apply (trans_lt ? (S O)).apply lt_O_S. assumption
202 |rewrite < sym_times.
203 rewrite > times_minus_l.
204 rewrite > (sym_times (S O)).
205 rewrite < times_n_SO.
206 rewrite > totient_card.
207 rewrite > a_times_pi_p.
208 apply congruent_to_divides
209 [apply (trans_lt ? (S O)).apply lt_O_S. assumption
210 | apply (transitive_congruent n ?
211 (map_iter_p n (\lambda i.eqb (gcd i n) (S O)) (\lambda x.a*x \mod n) (S O) times))
212 [apply (congruent_map_iter_p_times ? n n).
213 apply (trans_lt ? (S O))
214 [apply lt_O_S|assumption]
216 cut ( (map_iter_p n (\lambda i:nat.eqb (gcd i n) (S O)) (\lambda n:nat.n) (S O) times)
217 = (map_iter_p n (\lambda i:nat.eqb (gcd i n) (S O)) (\lambda x:nat.a*x\mod n) (S O) times))
218 [rewrite < Hcut1.apply congruent_n_n
219 |apply (eq_map_iter_p_permut ? ? ? ? ? (λm.m))
222 |apply (permut_p_mod ? ? H Hcut H1)
224 apply not_eq_to_eqb_false.
226 apply (lt_to_not_eq (S O) n)
227 [assumption|apply sym_eq.assumption]
234 |elim (le_to_or_lt_eq O a (le_O_n a))
236 |absurd (gcd a n = S O)
241 apply (lt_to_not_eq (S O) n)
242 [assumption|apply sym_eq.assumption]