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/iteration.ma".
18 include "nat/totient.ma".
21 lemma le_to_le_to_eq: \forall n,m. n \le m \to m \le n \to n = m.
23 [intros.apply le_n_O_to_eq.assumption
24 |intros.apply sym_eq.apply le_n_O_to_eq.assumption
25 |intros.apply eq_f.apply H
26 [apply le_S_S_to_le.assumption
27 |apply le_S_S_to_le.assumption
32 lemma gcd_n_n: \forall n.gcd n n = n.
41 [apply lt_O_gcd.apply lt_O_S
43 [apply divides_n_n|apply divides_n_n]
50 lemma count_card: \forall p.\forall n.
51 p O = false \to count (S n) p = card n p.
53 [simplify.rewrite > H. reflexivity
60 lemma count_card1: \forall p.\forall n.
61 p O = false \to p n = false \to count n p = card n p.
62 intros 3.apply (nat_case n)
63 [intro.simplify.rewrite > H. reflexivity
64 |intros.rewrite > (count_card ? ? H).
65 simplify.rewrite > H1.reflexivity
69 lemma totient_card: \forall n.
70 totient n = card n (\lambda i.eqb (gcd i n) (S O)).
71 intro.apply (nat_case n)
73 |intro.apply (nat_case m)
75 |intro.apply count_card1
77 |rewrite > gcd_n_n.reflexivity
84 lemma gcd_n_times_nm: \forall n,m. O < m \to gcd n (n*m) = n.
85 intro.apply (nat_case n)
90 [apply lt_O_S|apply divides_gcd_n]
92 [apply lt_O_gcd.rewrite > (times_n_O O).
93 apply lt_times[apply lt_O_S|assumption]
95 [apply (witness ? ? m1).reflexivity
104 lemma eq_gcd_SO_to_not_divides: \forall n,m. (S O) < n \to
105 (gcd n m) = (S O) \to \lnot (divides n m).
108 generalize in match H1.
112 [elim (gcd_times_SO_to_gcd_SO n n n2 ? ? H4)
113 [cut (gcd n (n*n2) = n)
114 [apply (lt_to_not_eq (S O) n)
115 [assumption|rewrite < H4.assumption]
116 |apply gcd_n_times_nm.assumption
118 |apply (trans_lt ? (S O))[apply le_n|assumption]
121 |elim (le_to_or_lt_eq O n2 (le_O_n n2))
124 apply (le_to_not_lt n (S O))
127 [rewrite > H4.apply lt_O_S
129 [apply (witness ? ? n2).reflexivity
139 theorem gcd_Pi_P: \forall n,k. O < k \to k \le n \to
140 gcd n (Pi_P (\lambda i.eqb (gcd i n) (S O)) k) = (S O).
143 cut (eqb (gcd (S O) n) (S O) = true)
145 change with ((gcd n (S O)) = (S O)).auto
146 |apply eq_to_eqb_true.auto
152 ((gcd n ((S n1)*(Pi_P (\lambda i.eqb (gcd i n) (S O)) n1))) = (S O)).
153 apply eq_gcd_times_SO
154 [unfold.apply le_S.assumption
156 |rewrite > sym_gcd. assumption.
158 apply (trans_le ? (S n1))[apply le_n_Sn|assumption]
162 (gcd n (Pi_P (\lambda i.eqb (gcd i n) (S O)) n1) = (S O)).
164 apply (trans_le ? (S n1))[apply le_n_Sn|assumption]
169 theorem congruent_map_iter_P_times:\forall f:nat \to nat. \forall a,n:nat.
172 (map_iter_P n (\lambda i.eqb (gcd i a) (S O)) (\lambda x.f x) (S O) times)
173 (map_iter_P n (\lambda i.eqb (gcd i a) (S O))
174 (\lambda x.f x \mod a) (S O) times) a.
177 [rewrite > map_iter_P_O.
178 apply (congruent_n_n ? a)
179 |apply (eqb_elim (gcd (S n1) a) (S O))
181 rewrite > map_iter_P_S_true
182 [rewrite > map_iter_P_S_true
183 [apply congruent_times
185 |apply congruent_n_mod_n.assumption
188 |apply eq_to_eqb_true.assumption
190 |apply eq_to_eqb_true.assumption
193 rewrite > map_iter_P_S_false
194 [rewrite > map_iter_P_S_false
196 |apply not_eq_to_eqb_false.assumption
198 |apply not_eq_to_eqb_false.assumption
204 theorem lt_S_to_lt: \forall n,m. S n < m \to n < m.
206 apply (trans_lt ? (S n))
207 [apply le_n|assumption]
210 theorem gcd_SO_to_lt_O: \forall i,n. (S O) < n \to gcd i n = (S O) \to
213 elim (le_to_or_lt_eq ? ? (le_O_n i))
215 |absurd ((gcd i n) = (S O))
220 apply (lt_to_not_eq (S O) n H).
221 apply sym_eq.assumption
226 theorem gcd_SO_to_lt_n: \forall i,n. (S O) < n \to i \le n \to gcd i n = (S O) \to
229 elim (le_to_or_lt_eq ? ? H1)
231 |absurd ((gcd i n) = (S O))
236 apply (lt_to_not_eq (S O) n H).
237 apply sym_eq.assumption
242 theorem permut_p_mod: \forall a,n. S O < n \to O < a \to gcd a n = (S O) \to
243 permut_p (\lambda x:nat.a*x \mod n) (\lambda i:nat.eqb (gcd i n) (S O)) n.
245 lapply (lt_S_to_lt ? ? H) as H3.
256 [apply eq_to_eqb_true.
258 apply eq_gcd_times_SO
260 |apply (gcd_SO_to_lt_O i n H).
261 apply eqb_true_to_eq.
263 |rewrite > sym_gcd.assumption
264 |rewrite > sym_gcd.apply eqb_true_to_eq.
271 lapply (gcd_SO_to_lt_n ? ? H H4 (eqb_true_to_eq ? ? H5)) as H9.
272 lapply (gcd_SO_to_lt_n ? ? H H7 (eqb_true_to_eq ? ? H6)) as H10.
273 lapply (gcd_SO_to_lt_O ? ? H (eqb_true_to_eq ? ? H5)) as H11.
274 lapply (gcd_SO_to_lt_O ? ? H (eqb_true_to_eq ? ? H6)) as H12.
277 apply (nat_compare_elim i j)
282 apply (trans_le ? (j -i))
285 apply (lt_plus_to_lt_l i).
287 rewrite < (plus_minus_m_m)
288 [assumption|apply lt_to_le.assumption]
289 |apply (gcd_SO_to_divides_times_to_divides a)
291 |rewrite > sym_gcd.assumption
292 |apply mod_O_to_divides
294 |rewrite > distr_times_minus.
307 apply (trans_le ? (i -j))
310 apply (lt_plus_to_lt_l j).
312 rewrite < (plus_minus_m_m)
313 [assumption|apply lt_to_le.assumption]
314 |apply (gcd_SO_to_divides_times_to_divides a)
316 |rewrite > sym_gcd.assumption
317 |apply mod_O_to_divides
319 |rewrite > distr_times_minus.
331 theorem congruent_exp_totient_SO: \forall n,a:nat. (S O) < n \to
332 gcd a n = (S O) \to congruent (exp a (totient n)) (S O) n.
335 [apply divides_to_congruent
336 [apply (trans_lt ? (S O)).apply lt_O_S. assumption
337 |change with (O < exp a (totient n)).apply lt_O_exp.assumption
338 |apply (gcd_SO_to_divides_times_to_divides (Pi_P (\lambda i.eqb (gcd i n) (S O)) n))
339 [apply (trans_lt ? (S O)).apply lt_O_S. assumption
341 [apply (trans_lt ? (S O)).apply lt_O_S. assumption
344 |rewrite < sym_times.
345 rewrite > times_minus_l.
346 rewrite > (sym_times (S O)).
347 rewrite < times_n_SO.
348 rewrite > totient_card.
349 rewrite > a_times_Pi_P.
350 apply congruent_to_divides
351 [apply (trans_lt ? (S O)).apply lt_O_S. assumption
352 | apply (transitive_congruent n ?
353 (map_iter_P n (\lambda i.eqb (gcd i n) (S O)) (\lambda x.a*x \mod n) (S O) times))
354 [apply (congruent_map_iter_P_times ? n n).
355 apply (trans_lt ? (S O))
356 [apply lt_O_S|assumption]
358 cut ( (map_iter_P n (\lambda i:nat.eqb (gcd i n) (S O)) (\lambda n:nat.n) (S O) times)
359 = (map_iter_P n (\lambda i:nat.eqb (gcd i n) (S O)) (\lambda x:nat.a*x\mod n) (S O) times))
360 [rewrite < Hcut1.apply congruent_n_n
361 |apply (eq_map_iter_p_permut ? ? ? ? ? (λm.m))
364 |apply (permut_p_mod ? ? H Hcut H1)
366 apply not_eq_to_eqb_false.
368 apply (lt_to_not_eq (S O) n)
369 [assumption|apply sym_eq.assumption]
376 |elim (le_to_or_lt_eq O a (le_O_n a))
378 |absurd (gcd a n = S O)
383 apply (lt_to_not_eq (S O) n)
384 [assumption|apply sym_eq.assumption]