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 (* \ / Matita is distributed under the terms of the *)
11 (* v GNU Lesser General Public License Version 2.1 *)
13 (**************************************************************************)
15 set "baseuri" "cic:/matita/nat/gcd".
17 include "nat/primes.ma".
19 let rec gcd_aux p m n: nat \def
20 match divides_b n m with
25 |(S q) \Rightarrow gcd_aux q n (m \mod n)]].
27 definition gcd : nat \to nat \to nat \def
33 | (S p) \Rightarrow gcd_aux (S p) m (S p) ]
37 | (S p) \Rightarrow gcd_aux (S p) n (S p) ]].
39 theorem divides_mod: \forall p,m,n:nat. O < n \to p \divides m \to p \divides n \to
40 p \divides (m \mod n).
41 intros.elim H1.elim H2.
42 apply (witness ? ? (n2 - n1*(m / n))).
43 rewrite > distr_times_minus.
45 rewrite < assoc_times.
54 theorem divides_mod_to_divides: \forall p,m,n:nat. O < n \to
55 p \divides (m \mod n) \to p \divides n \to p \divides m.
56 intros.elim H1.elim H2.
57 apply (witness p m ((n1*(m / n))+n2)).
58 rewrite > distr_times_plus.
60 rewrite < assoc_times.
61 rewrite < H4.rewrite < sym_times.
62 apply div_mod.assumption.
65 theorem divides_gcd_aux_mn: \forall p,m,n. O < n \to n \le m \to n \le p \to
66 gcd_aux p m n \divides m \land gcd_aux p m n \divides n.
68 absurd (O < n).assumption.apply le_to_not_lt.assumption.
69 cut ((n1 \divides m) \lor (n1 \ndivides m)).
71 ((match divides_b n1 m with
73 | false \Rightarrow gcd_aux n n1 (m \mod n1)]) \divides m \land
74 (match divides_b n1 m with
76 | false \Rightarrow gcd_aux n n1 (m \mod n1)]) \divides n1).
77 elim Hcut.rewrite > divides_to_divides_b_true.
79 split.assumption.apply (witness n1 n1 (S O)).apply times_n_SO.
80 assumption.assumption.
81 rewrite > not_divides_to_divides_b_false.
83 (gcd_aux n n1 (m \mod n1) \divides m \land
84 gcd_aux n n1 (m \mod n1) \divides n1).
85 cut (gcd_aux n n1 (m \mod n1) \divides n1 \land
86 gcd_aux n n1 (m \mod n1) \divides mod m n1).
88 split.apply (divides_mod_to_divides ? ? n1).
89 assumption.assumption.assumption.assumption.
91 cut (O \lt m \mod n1 \lor O = mod m n1).
92 elim Hcut1.assumption.
93 apply False_ind.apply H4.apply mod_O_to_divides.
94 assumption.apply sym_eq.assumption.
95 apply le_to_or_lt_eq.apply le_O_n.
97 apply lt_mod_m_m.assumption.
99 apply (trans_le ? n1).
100 change with (m \mod n1 < n1).
101 apply lt_mod_m_m.assumption.assumption.
102 assumption.assumption.
103 apply (decidable_divides n1 m).assumption.
106 theorem divides_gcd_nm: \forall n,m.
107 gcd n m \divides m \land gcd n m \divides n.
114 | (S p) \Rightarrow gcd_aux (S p) m (S p) ]
118 | (S p) \Rightarrow gcd_aux (S p) n (S p) ] ] \divides m
124 | (S p) \Rightarrow gcd_aux (S p) m (S p) ]
128 | (S p) \Rightarrow gcd_aux (S p) n (S p) ] ] \divides n).
129 apply (leb_elim n m).
131 simplify.intros.split.
132 apply (witness m m (S O)).apply times_n_SO.
133 apply (witness m O O).apply times_n_O.
135 (gcd_aux (S m1) m (S m1) \divides m
137 gcd_aux (S m1) m (S m1) \divides (S m1)).
138 apply divides_gcd_aux_mn.
139 simplify.apply le_S_S.apply le_O_n.
140 assumption.apply le_n.
143 simplify.intros.split.
144 apply (witness n O O).apply times_n_O.
145 apply (witness n n (S O)).apply times_n_SO.
147 (gcd_aux (S m1) n (S m1) \divides (S m1)
149 gcd_aux (S m1) n (S m1) \divides n).
150 cut (gcd_aux (S m1) n (S m1) \divides n
152 gcd_aux (S m1) n (S m1) \divides S m1).
153 elim Hcut.split.assumption.assumption.
154 apply divides_gcd_aux_mn.
155 simplify.apply le_S_S.apply le_O_n.
156 apply not_lt_to_le.simplify.intro.apply H.
157 rewrite > H1.apply (trans_le ? (S n)).
158 apply le_n_Sn.assumption.apply le_n.
161 theorem divides_gcd_n: \forall n,m. gcd n m \divides n.
163 exact (proj2 ? ? (divides_gcd_nm n m)).
166 theorem divides_gcd_m: \forall n,m. gcd n m \divides m.
168 exact (proj1 ? ? (divides_gcd_nm n m)).
171 theorem divides_gcd_aux: \forall p,m,n,d. O < n \to n \le m \to n \le p \to
172 d \divides m \to d \divides n \to d \divides gcd_aux p m n.
174 absurd (O < n).assumption.apply le_to_not_lt.assumption.
177 (match divides_b n1 m with
178 [ true \Rightarrow n1
179 | false \Rightarrow gcd_aux n n1 (m \mod n1)])).
180 cut (n1 \divides m \lor n1 \ndivides m).
182 rewrite > divides_to_divides_b_true.
184 assumption.assumption.
185 rewrite > not_divides_to_divides_b_false.
186 change with (d \divides gcd_aux n n1 (m \mod n1)).
188 cut (O \lt m \mod n1 \lor O = m \mod n1).
189 elim Hcut1.assumption.
190 absurd (n1 \divides m).apply mod_O_to_divides.
191 assumption.apply sym_eq.assumption.assumption.
192 apply le_to_or_lt_eq.apply le_O_n.
194 apply lt_mod_m_m.assumption.
196 apply (trans_le ? n1).
197 change with (m \mod n1 < n1).
198 apply lt_mod_m_m.assumption.assumption.
200 apply divides_mod.assumption.assumption.assumption.
201 assumption.assumption.
202 apply (decidable_divides n1 m).assumption.
205 theorem divides_d_gcd: \forall m,n,d.
206 d \divides m \to d \divides n \to d \divides gcd n m.
214 | (S p) \Rightarrow gcd_aux (S p) m (S p) ]
218 | (S p) \Rightarrow gcd_aux (S p) n (S p) ]]).
219 apply (leb_elim n m).
220 apply (nat_case1 n).simplify.intros.assumption.
222 change with (d \divides gcd_aux (S m1) m (S m1)).
223 apply divides_gcd_aux.
224 simplify.apply le_S_S.apply le_O_n.assumption.apply le_n.assumption.
225 rewrite < H2.assumption.
226 apply (nat_case1 m).simplify.intros.assumption.
228 change with (d \divides gcd_aux (S m1) n (S m1)).
229 apply divides_gcd_aux.
230 simplify.apply le_S_S.apply le_O_n.
231 apply lt_to_le.apply not_le_to_lt.assumption.apply le_n.assumption.
232 rewrite < H2.assumption.
235 theorem eq_minus_gcd_aux: \forall p,m,n.O < n \to n \le m \to n \le p \to
236 \exists a,b. a*n - b*m = gcd_aux p m n \lor b*m - a*n = gcd_aux p m n.
239 absurd (O < n).assumption.apply le_to_not_lt.assumption.
241 cut (n1 \divides m \lor n1 \ndivides m).
244 a*n1 - b*m = match divides_b n1 m with
245 [ true \Rightarrow n1
246 | false \Rightarrow gcd_aux n n1 (m \mod n1)]
248 b*m - a*n1 = match divides_b n1 m with
249 [ true \Rightarrow n1
250 | false \Rightarrow gcd_aux n n1 (m \mod n1)]).
252 rewrite > divides_to_divides_b_true.
254 apply (ex_intro ? ? (S O)).
255 apply (ex_intro ? ? O).
256 left.simplify.rewrite < plus_n_O.
257 apply sym_eq.apply minus_n_O.
258 assumption.assumption.
259 rewrite > not_divides_to_divides_b_false.
262 a*n1 - b*m = gcd_aux n n1 (m \mod n1)
264 b*m - a*n1 = gcd_aux n n1 (m \mod n1)).
267 a*(m \mod n1) - b*n1= gcd_aux n n1 (m \mod n1)
269 b*n1 - a*(m \mod n1) = gcd_aux n n1 (m \mod n1)).
270 elim Hcut2.elim H5.elim H6.
273 apply (ex_intro ? ? (a1+a*(m / n1))).
274 apply (ex_intro ? ? a).
277 rewrite < (sym_times n1).
278 rewrite > distr_times_plus.
279 rewrite > (sym_times n1).
280 rewrite > (sym_times n1).
281 rewrite > (div_mod m n1) in \vdash (? ? (? % ?) ?).
282 rewrite > assoc_times.
284 rewrite > distr_times_plus.
285 rewrite < eq_minus_minus_minus_plus.
287 rewrite < plus_minus.
288 rewrite < minus_n_n.reflexivity.
293 apply (ex_intro ? ? (a1+a*(m / n1))).
294 apply (ex_intro ? ? a).
296 (* clear Hcut2.clear H5.clear H6.clear H. *)
298 rewrite > distr_times_plus.
300 rewrite > (sym_times n1).
301 rewrite > (div_mod m n1) in \vdash (? ? (? ? %) ?).
302 rewrite > distr_times_plus.
303 rewrite > assoc_times.
304 rewrite < eq_minus_minus_minus_plus.
306 rewrite < plus_minus.
307 rewrite < minus_n_n.reflexivity.
310 apply (H n1 (m \mod n1)).
311 cut (O \lt m \mod n1 \lor O = m \mod n1).
312 elim Hcut2.assumption.
313 absurd (n1 \divides m).apply mod_O_to_divides.
315 symmetry.assumption.assumption.
316 apply le_to_or_lt_eq.apply le_O_n.
318 apply lt_mod_m_m.assumption.
320 apply (trans_le ? n1).
321 change with (m \mod n1 < n1).
323 assumption.assumption.assumption.assumption.
324 apply (decidable_divides n1 m).assumption.
325 apply (lt_to_le_to_lt ? n1).assumption.assumption.
328 theorem eq_minus_gcd:
329 \forall m,n.\exists a,b.a*n - b*m = (gcd n m) \lor b*m - a*n = (gcd n m).
332 apply (leb_elim n m).
335 apply (ex_intro ? ? O).
336 apply (ex_intro ? ? (S O)).
339 apply sym_eq.apply minus_n_O.
343 a*(S m1) - b*m = (gcd_aux (S m1) m (S m1))
344 \lor b*m - a*(S m1) = (gcd_aux (S m1) m (S m1))).
345 apply eq_minus_gcd_aux.
346 simplify. apply le_S_S.apply le_O_n.
347 assumption.apply le_n.
350 apply (ex_intro ? ? (S O)).
351 apply (ex_intro ? ? O).
354 apply sym_eq.apply minus_n_O.
358 a*n - b*(S m1) = (gcd_aux (S m1) n (S m1))
359 \lor b*(S m1) - a*n = (gcd_aux (S m1) n (S m1))).
362 a*(S m1) - b*n = (gcd_aux (S m1) n (S m1))
364 b*n - a*(S m1) = (gcd_aux (S m1) n (S m1))).
365 elim Hcut.elim H2.elim H3.
366 apply (ex_intro ? ? a1).
367 apply (ex_intro ? ? a).
369 apply (ex_intro ? ? a1).
370 apply (ex_intro ? ? a).
372 apply eq_minus_gcd_aux.
373 simplify. apply le_S_S.apply le_O_n.
374 apply lt_to_le.apply not_le_to_lt.assumption.
378 (* some properties of gcd *)
380 theorem gcd_O_n: \forall n:nat. gcd O n = n.
381 intro.simplify.reflexivity.
384 theorem gcd_O_to_eq_O:\forall m,n:nat. (gcd m n) = O \to
386 intros.cut (O \divides n \land O \divides m).
387 elim Hcut.elim H2.split.
388 assumption.elim H1.assumption.
390 apply divides_gcd_nm.
393 theorem symmetric_gcd: symmetric nat gcd.
395 (\forall n,m:nat. gcd n m = gcd m n).
397 cut (O < (gcd n m) \lor O = (gcd n m)).
399 cut (O < (gcd m n) \lor O = (gcd m n)).
402 apply divides_to_le.assumption.
403 apply divides_d_gcd.apply divides_gcd_n.apply divides_gcd_m.
404 apply divides_to_le.assumption.
405 apply divides_d_gcd.apply divides_gcd_n.apply divides_gcd_m.
408 elim Hcut2.rewrite > H2.rewrite > H3.reflexivity.
409 apply gcd_O_to_eq_O.apply sym_eq.assumption.
410 apply le_to_or_lt_eq.apply le_O_n.
413 elim Hcut1.rewrite > H1.rewrite > H2.reflexivity.
414 apply gcd_O_to_eq_O.apply sym_eq.assumption.
415 apply le_to_or_lt_eq.apply le_O_n.
418 variant sym_gcd: \forall n,m:nat. gcd n m = gcd m n \def
421 theorem gcd_SO_n: \forall n:nat. gcd (S O) n = (S O).
423 apply antisym_le.apply divides_to_le.simplify.apply le_n.
425 cut (O < gcd (S O) n \lor O = gcd (S O) n).
426 elim Hcut.assumption.
428 apply (not_eq_O_S O).
429 cut ((S O)=O \land n=O).
430 elim Hcut1.apply sym_eq.assumption.
431 apply gcd_O_to_eq_O.apply sym_eq.assumption.
432 apply le_to_or_lt_eq.apply le_O_n.
435 theorem prime_to_gcd_SO: \forall n,m:nat. prime n \to n \ndivides m \to
437 intros.simplify in H.change with (gcd n m = (S O)).
441 change with ((S (S O)) \le gcd n m \to False).intro.
442 apply H1.rewrite < (H3 (gcd n m)).
444 apply divides_gcd_n.assumption.
445 cut (O < gcd n m \lor O = gcd n m).
446 elim Hcut.assumption.
448 apply (not_le_Sn_O (S O)).
450 elim Hcut1.rewrite < H5 in \vdash (? ? %).assumption.
451 apply gcd_O_to_eq_O.apply sym_eq.assumption.
452 apply le_to_or_lt_eq.apply le_O_n.
455 theorem divides_times_to_divides: \forall n,p,q:nat.prime n \to n \divides p*q \to
456 n \divides p \lor n \divides q.
458 cut (n \divides p \lor n \ndivides p).
462 cut (\exists a,b. a*n - b*p = (S O) \lor b*p - a*n = (S O)).
463 elim Hcut1.elim H3.elim H4.
465 rewrite > (times_n_SO q).rewrite < H5.
466 rewrite > distr_times_minus.
467 rewrite > (sym_times q (a1*p)).
468 rewrite > (assoc_times a1).
469 elim H1.rewrite > H6.
470 rewrite < (sym_times n).rewrite < assoc_times.
471 rewrite > (sym_times q).rewrite > assoc_times.
472 rewrite < (assoc_times a1).rewrite < (sym_times n).
473 rewrite > (assoc_times n).
474 rewrite < distr_times_minus.
475 apply (witness ? ? (q*a-a1*n2)).reflexivity.
477 rewrite > (times_n_SO q).rewrite < H5.
478 rewrite > distr_times_minus.
479 rewrite > (sym_times q (a1*p)).
480 rewrite > (assoc_times a1).
481 elim H1.rewrite > H6.
482 rewrite < sym_times.rewrite > assoc_times.
483 rewrite < (assoc_times q).
484 rewrite < (sym_times n).
485 rewrite < distr_times_minus.
486 apply (witness ? ? (n2*a1-q*a)).reflexivity.
487 (* end second case *)
488 rewrite < (prime_to_gcd_SO n p).
490 assumption.assumption.
491 apply (decidable_divides n p).
492 apply (trans_lt ? (S O)).simplify.apply le_n.
493 simplify in H.elim H. assumption.