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 lemma gcd_n_n: \forall n.gcd n n = n.
29 [apply lt_O_gcd.apply lt_O_S
31 [apply divides_n_n|apply divides_n_n]
38 lemma count_card: \forall p.\forall n.
39 p O = false \to count (S n) p = card n p.
41 [simplify.rewrite > H. reflexivity
48 lemma count_card1: \forall p.\forall n.
49 p O = false \to p n = false \to count n p = card n p.
50 intros 3.apply (nat_case n)
51 [intro.simplify.rewrite > H. reflexivity
52 |intros.rewrite > (count_card ? ? H).
53 simplify.rewrite > H1.reflexivity
58 (* a reformulation of totient using card insted of count *)
60 lemma totient_card: \forall n.
61 totient n = card n (\lambda i.eqb (gcd i n) (S O)).
62 intro.apply (nat_case n)
64 |intro.apply (nat_case m)
66 |intro.apply count_card1
68 |rewrite > gcd_n_n.reflexivity
74 theorem gcd_pi_p: \forall n,k. O < k \to k \le n \to
75 gcd n (pi_p (\lambda i.eqb (gcd i n) (S O)) k) = (S O).
78 cut (eqb (gcd (S O) n) (S O) = true)
80 change with ((gcd n (S O)) = (S O)).auto
81 |apply eq_to_eqb_true.auto
87 ((gcd n ((S n1)*(pi_p (\lambda i.eqb (gcd i n) (S O)) n1))) = (S O)).
89 [unfold.apply le_S.assumption
91 |rewrite > sym_gcd. assumption.
93 apply (trans_le ? (S n1))[apply le_n_Sn|assumption]
97 (gcd n (pi_p (\lambda i.eqb (gcd i n) (S O)) n1) = (S O)).
99 apply (trans_le ? (S n1))[apply le_n_Sn|assumption]
104 theorem congruent_map_iter_p_times:\forall f:nat \to nat. \forall a,n:nat.
107 (map_iter_p n (\lambda i.eqb (gcd i a) (S O)) (\lambda x.f x) (S O) times)
108 (map_iter_p n (\lambda i.eqb (gcd i a) (S O))
109 (\lambda x.f x \mod a) (S O) times) a.
112 [rewrite > map_iter_p_O.
113 apply (congruent_n_n ? a)
114 |apply (eqb_elim (gcd (S n1) a) (S O))
116 rewrite > map_iter_p_S_true
117 [rewrite > map_iter_p_S_true
118 [apply congruent_times
120 |apply congruent_n_mod_n.assumption
123 |apply eq_to_eqb_true.assumption
125 |apply eq_to_eqb_true.assumption
128 rewrite > map_iter_p_S_false
129 [rewrite > map_iter_p_S_false
131 |apply not_eq_to_eqb_false.assumption
133 |apply not_eq_to_eqb_false.assumption
139 theorem permut_p_mod: \forall a,n. S O < n \to O < a \to gcd a n = (S O) \to
140 permut_p (\lambda x:nat.a*x \mod n) (\lambda i:nat.eqb (gcd i n) (S O)) n.
142 lapply (lt_S_to_lt ? ? H) as H3.
153 [apply eq_to_eqb_true.
155 apply eq_gcd_times_SO
157 |apply (gcd_SO_to_lt_O i n H).
158 apply eqb_true_to_eq.
160 |rewrite > sym_gcd.assumption
161 |rewrite > sym_gcd.apply eqb_true_to_eq.
168 lapply (gcd_SO_to_lt_n ? ? H H4 (eqb_true_to_eq ? ? H5)) as H9.
169 lapply (gcd_SO_to_lt_n ? ? H H7 (eqb_true_to_eq ? ? H6)) as H10.
170 lapply (gcd_SO_to_lt_O ? ? H (eqb_true_to_eq ? ? H5)) as H11.
171 lapply (gcd_SO_to_lt_O ? ? H (eqb_true_to_eq ? ? H6)) as H12.
174 apply (nat_compare_elim i j)
179 apply (trans_le ? (j -i))
182 apply (lt_plus_to_lt_l i).
184 rewrite < (plus_minus_m_m)
185 [assumption|apply lt_to_le.assumption]
186 |apply (gcd_SO_to_divides_times_to_divides a)
188 |rewrite > sym_gcd.assumption
189 |apply mod_O_to_divides
191 |rewrite > distr_times_minus.
204 apply (trans_le ? (i -j))
207 apply (lt_plus_to_lt_l j).
209 rewrite < (plus_minus_m_m)
210 [assumption|apply lt_to_le.assumption]
211 |apply (gcd_SO_to_divides_times_to_divides a)
213 |rewrite > sym_gcd.assumption
214 |apply mod_O_to_divides
216 |rewrite > distr_times_minus.
228 theorem congruent_exp_totient_SO: \forall n,a:nat. (S O) < n \to
229 gcd a n = (S O) \to congruent (exp a (totient n)) (S O) n.
232 [apply divides_to_congruent
233 [apply (trans_lt ? (S O)).apply lt_O_S. assumption
234 |change with (O < exp a (totient n)).apply lt_O_exp.assumption
235 |apply (gcd_SO_to_divides_times_to_divides (pi_p (\lambda i.eqb (gcd i n) (S O)) n))
236 [apply (trans_lt ? (S O)).apply lt_O_S. assumption
238 [apply (trans_lt ? (S O)).apply lt_O_S. assumption
241 |rewrite < sym_times.
242 rewrite > times_minus_l.
243 rewrite > (sym_times (S O)).
244 rewrite < times_n_SO.
245 rewrite > totient_card.
246 rewrite > a_times_pi_p.
247 apply congruent_to_divides
248 [apply (trans_lt ? (S O)).apply lt_O_S. assumption
249 | apply (transitive_congruent n ?
250 (map_iter_p n (\lambda i.eqb (gcd i n) (S O)) (\lambda x.a*x \mod n) (S O) times))
251 [apply (congruent_map_iter_p_times ? n n).
252 apply (trans_lt ? (S O))
253 [apply lt_O_S|assumption]
255 cut ( (map_iter_p n (\lambda i:nat.eqb (gcd i n) (S O)) (\lambda n:nat.n) (S O) times)
256 = (map_iter_p n (\lambda i:nat.eqb (gcd i n) (S O)) (\lambda x:nat.a*x\mod n) (S O) times))
257 [rewrite < Hcut1.apply congruent_n_n
258 |apply (eq_map_iter_p_permut ? ? ? ? ? (λm.m))
261 |apply (permut_p_mod ? ? H Hcut H1)
263 apply not_eq_to_eqb_false.
265 apply (lt_to_not_eq (S O) n)
266 [assumption|apply sym_eq.assumption]
273 |elim (le_to_or_lt_eq O a (le_O_n a))
275 |absurd (gcd a n = S O)
280 apply (lt_to_not_eq (S O) n)
281 [assumption|apply sym_eq.assumption]