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 (mod m 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 divides p m \to divides p n \to
41 intros.elim H1.elim H2.
42 apply witness ? ? (n2 - n1*(div m n)).
43 rewrite > distr_times_minus.
45 rewrite < assoc_times.
49 rewrite > div_mod m n in \vdash (? ? %).
51 apply eq_plus_to_le ? ? (mod m n).
55 apply div_mod.assumption.
58 theorem divides_mod_to_divides: \forall p,m,n:nat. O < n \to
59 divides p (mod m n) \to divides p n \to divides p m.
60 intros.elim H1.elim H2.
61 apply witness p m ((n1*(div m n))+n2).
62 rewrite > distr_times_plus.
64 rewrite < assoc_times.
65 rewrite < H4.rewrite < sym_times.
66 apply div_mod.assumption.
69 theorem divides_gcd_aux_mn: \forall p,m,n. O < n \to n \le m \to n \le p \to
70 divides (gcd_aux p m n) m \land divides (gcd_aux p m n) n.
72 absurd O < n.assumption.apply le_to_not_lt.assumption.
73 cut (divides n1 m) \lor \not (divides n1 m).
76 (match divides_b n1 m with
78 | false \Rightarrow gcd_aux n n1 (mod m n1)]) m) \land
80 (match divides_b n1 m with
82 | false \Rightarrow gcd_aux n n1 (mod m n1)]) n1).
83 elim Hcut.rewrite > divides_to_divides_b_true.
85 split.assumption.apply witness n1 n1 (S O).apply times_n_SO.
86 assumption.assumption.
87 rewrite > not_divides_to_divides_b_false.
89 (divides (gcd_aux n n1 (mod m n1)) m) \land
90 (divides (gcd_aux n n1 (mod m n1)) n1).
91 cut (divides (gcd_aux n n1 (mod m n1)) n1) \land
92 (divides (gcd_aux n n1 (mod m n1)) (mod m n1)).
94 split.apply divides_mod_to_divides ? ? n1.
95 assumption.assumption.assumption.assumption.
97 cut O \lt mod m n1 \lor O = mod m n1.
98 elim Hcut1.assumption.
99 apply False_ind.apply H4.apply mod_O_to_divides.
100 assumption.apply sym_eq.assumption.
101 apply le_to_or_lt_eq.apply le_O_n.
103 apply lt_mod_m_m.assumption.
106 change with mod m n1 < n1.
107 apply lt_mod_m_m.assumption.assumption.
108 assumption.assumption.
109 apply decidable_divides n1 m.assumption.
112 theorem divides_gcd_nm: \forall n,m.
113 divides (gcd n m) m \land divides (gcd n m) n.
121 | (S p) \Rightarrow gcd_aux (S p) m (S p) ]
125 | (S p) \Rightarrow gcd_aux (S p) n (S p) ]]) m
132 | (S p) \Rightarrow gcd_aux (S p) m (S p) ]
136 | (S p) \Rightarrow gcd_aux (S p) n (S p) ]]) n.
139 simplify.intros.split.
140 apply witness m m (S O).apply times_n_SO.
141 apply witness m O O.apply times_n_O.
143 divides (gcd_aux (S m1) m (S m1)) m
145 divides (gcd_aux (S m1) m (S m1)) (S m1).
146 apply divides_gcd_aux_mn.
147 simplify.apply le_S_S.apply le_O_n.
148 assumption.apply le_n.
151 simplify.intros.split.
152 apply witness n O O.apply times_n_O.
153 apply witness n n (S O).apply times_n_SO.
155 divides (gcd_aux (S m1) n (S m1)) (S m1)
157 divides (gcd_aux (S m1) n (S m1)) n.
158 cut divides (gcd_aux (S m1) n (S m1)) n
160 divides (gcd_aux (S m1) n (S m1)) (S m1).
161 elim Hcut.split.assumption.assumption.
162 apply divides_gcd_aux_mn.
163 simplify.apply le_S_S.apply le_O_n.
164 apply not_lt_to_le.simplify.intro.apply H.
165 rewrite > H1.apply trans_le ? (S n).
166 apply le_n_Sn.assumption.apply le_n.
169 theorem divides_gcd_n: \forall n,m.
172 exact proj2 ? ? (divides_gcd_nm n m).
175 theorem divides_gcd_m: \forall n,m.
178 exact proj1 ? ? (divides_gcd_nm n m).
181 theorem divides_gcd_aux: \forall p,m,n,d. O < n \to n \le m \to n \le p \to
182 divides d m \to divides d n \to divides d (gcd_aux p m n).
184 absurd O < n.assumption.apply le_to_not_lt.assumption.
187 (match divides_b n1 m with
188 [ true \Rightarrow n1
189 | false \Rightarrow gcd_aux n n1 (mod m n1)]).
190 cut divides n1 m \lor \not (divides n1 m).
192 rewrite > divides_to_divides_b_true.
194 assumption.assumption.
195 rewrite > not_divides_to_divides_b_false.
196 change with divides d (gcd_aux n n1 (mod m n1)).
198 cut O \lt mod m n1 \lor O = mod m n1.
199 elim Hcut1.assumption.
200 absurd divides n1 m.apply mod_O_to_divides.
201 assumption.apply sym_eq.assumption.assumption.
202 apply le_to_or_lt_eq.apply le_O_n.
204 apply lt_mod_m_m.assumption.
207 change with mod m n1 < n1.
208 apply lt_mod_m_m.assumption.assumption.
210 apply divides_mod.assumption.assumption.assumption.
211 assumption.assumption.
212 apply decidable_divides n1 m.assumption.
215 theorem divides_d_gcd: \forall m,n,d.
216 divides d m \to divides d n \to divides d (gcd n m).
224 | (S p) \Rightarrow gcd_aux (S p) m (S p) ]
228 | (S p) \Rightarrow gcd_aux (S p) n (S p) ]]).
230 apply nat_case1 n.simplify.intros.assumption.
232 change with divides d (gcd_aux (S m1) m (S m1)).
233 apply divides_gcd_aux.
234 simplify.apply le_S_S.apply le_O_n.assumption.apply le_n.assumption.
235 rewrite < H2.assumption.
236 apply nat_case1 m.simplify.intros.assumption.
238 change with divides d (gcd_aux (S m1) n (S m1)).
239 apply divides_gcd_aux.
240 simplify.apply le_S_S.apply le_O_n.
241 apply lt_to_le.apply not_le_to_lt.assumption.apply le_n.assumption.
242 rewrite < H2.assumption.
245 theorem eq_minus_gcd_aux: \forall p,m,n.O < n \to n \le m \to n \le p \to
246 \exists a,b. a*n - b*m = gcd_aux p m n \lor b*m - a*n = gcd_aux p m n.
249 absurd O < n.assumption.apply le_to_not_lt.assumption.
251 cut (divides n1 m) \lor \not (divides n1 m).
254 a*n1 - b*m = match divides_b n1 m with
255 [ true \Rightarrow n1
256 | false \Rightarrow gcd_aux n n1 (mod m n1)]
258 b*m - a*n1 = match divides_b n1 m with
259 [ true \Rightarrow n1
260 | false \Rightarrow gcd_aux n n1 (mod m n1)].
262 rewrite > divides_to_divides_b_true.
264 apply ex_intro ? ? (S O).
265 apply ex_intro ? ? O.
266 left.simplify.rewrite < plus_n_O.
267 apply sym_eq.apply minus_n_O.
268 assumption.assumption.
269 rewrite > not_divides_to_divides_b_false.
272 a*n1 - b*m = gcd_aux n n1 (mod m n1)
274 b*m - a*n1 = gcd_aux n n1 (mod m n1).
277 a*(mod m n1) - b*n1= gcd_aux n n1 (mod m n1)
279 b*n1 - a*(mod m n1) = gcd_aux n n1 (mod m n1).
280 elim Hcut2.elim H5.elim H6.
283 apply ex_intro ? ? (a1+a*(div m n1)).
284 apply ex_intro ? ? a.
287 rewrite < sym_times n1.
288 rewrite > distr_times_plus.
289 rewrite > sym_times n1.
290 rewrite > sym_times n1.
291 rewrite > div_mod m n1 in \vdash (? ? (? % ?) ?).
292 rewrite > assoc_times.
294 rewrite > distr_times_plus.
295 rewrite < eq_minus_minus_minus_plus.
297 rewrite < plus_minus.
298 rewrite < minus_n_n.reflexivity.
303 apply ex_intro ? ? (a1+a*(div m n1)).
304 apply ex_intro ? ? a.
307 rewrite > distr_times_plus.
309 rewrite > sym_times n1.
310 rewrite > div_mod m n1 in \vdash (? ? (? ? %) ?).
311 rewrite > distr_times_plus.
312 rewrite > assoc_times.
313 rewrite < eq_minus_minus_minus_plus.
315 rewrite < plus_minus.
316 rewrite < minus_n_n.reflexivity.
319 apply H n1 (mod m n1).
320 cut O \lt mod m n1 \lor O = mod m n1.
321 elim Hcut2.assumption.
322 absurd divides n1 m.apply mod_O_to_divides.
324 symmetry.assumption.assumption.
325 apply le_to_or_lt_eq.apply le_O_n.
327 apply lt_mod_m_m.assumption.
330 change with mod m n1 < n1.
332 assumption.assumption.assumption.assumption.
333 apply decidable_divides n1 m.assumption.
334 apply lt_to_le_to_lt ? n1.assumption.assumption.
337 theorem eq_minus_gcd:
338 \forall m,n.\exists a,b.a*n - b*m = (gcd n m) \lor b*m - a*n = (gcd n m).
347 | (S p) \Rightarrow gcd_aux (S p) m (S p) ]
351 | (S p) \Rightarrow gcd_aux (S p) n (S p) ]]
357 | (S p) \Rightarrow gcd_aux (S p) m (S p) ]
361 | (S p) \Rightarrow gcd_aux (S p) n (S p) ]].
365 apply ex_intro ? ? O.
366 apply ex_intro ? ? (S O).
369 apply sym_eq.apply minus_n_O.
373 a*(S m1) - b*m = (gcd_aux (S m1) m (S m1))
374 \lor b*m - a*(S m1) = (gcd_aux (S m1) m (S m1)).
375 apply eq_minus_gcd_aux.
376 simplify. apply le_S_S.apply le_O_n.
377 assumption.apply le_n.
380 apply ex_intro ? ? (S O).
381 apply ex_intro ? ? O.
384 apply sym_eq.apply minus_n_O.
388 a*n - b*(S m1) = (gcd_aux (S m1) n (S m1))
389 \lor b*(S m1) - a*n = (gcd_aux (S m1) n (S m1)).
392 a*(S m1) - b*n = (gcd_aux (S m1) n (S m1))
394 b*n - a*(S m1) = (gcd_aux (S m1) n (S m1)).
395 elim Hcut.elim H2.elim H3.
396 apply ex_intro ? ? a1.
397 apply ex_intro ? ? a.
399 apply ex_intro ? ? a1.
400 apply ex_intro ? ? a.
402 apply eq_minus_gcd_aux.
403 simplify. apply le_S_S.apply le_O_n.
404 apply lt_to_le.apply not_le_to_lt.assumption.
408 (* some properties of gcd *)
410 theorem gcd_O_n: \forall n:nat. gcd O n = n.
411 intro.simplify.reflexivity.
414 theorem gcd_O_to_eq_O:\forall m,n:nat. (gcd m n) = O \to
416 intros.cut divides O n \land divides O m.
417 elim Hcut.elim H2.split.
418 assumption.elim H1.assumption.
420 apply divides_gcd_nm.
423 theorem symmetric_gcd: symmetric nat gcd.
425 \forall n,m:nat. gcd n m = gcd m n.
427 cut O < (gcd n m) \lor O = (gcd n m).
429 cut O < (gcd m n) \lor O = (gcd m n).
432 apply divides_to_le.assumption.
433 apply divides_d_gcd.apply divides_gcd_n.apply divides_gcd_m.
434 apply divides_to_le.assumption.
435 apply divides_d_gcd.apply divides_gcd_n.apply divides_gcd_m.
438 elim Hcut2.rewrite > H2.rewrite > H3.reflexivity.
439 apply gcd_O_to_eq_O.apply sym_eq.assumption.
440 apply le_to_or_lt_eq.apply le_O_n.
443 elim Hcut1.rewrite > H1.rewrite > H2.reflexivity.
444 apply gcd_O_to_eq_O.apply sym_eq.assumption.
445 apply le_to_or_lt_eq.apply le_O_n.
448 variant sym_gcd: \forall n,m:nat. gcd n m = gcd m n \def
451 theorem gcd_SO_n: \forall n:nat. gcd (S O) n = (S O).
453 apply antisym_le.apply divides_to_le.simplify.apply le_n.
455 cut O < gcd (S O) n \lor O = gcd (S O) n.
456 elim Hcut.assumption.
459 cut (S O)=O \land n=O.
460 elim Hcut1.apply sym_eq.assumption.
461 apply gcd_O_to_eq_O.apply sym_eq.assumption.
462 apply le_to_or_lt_eq.apply le_O_n.
465 theorem prime_to_gcd_SO: \forall n,m:nat. prime n \to \not (divides n m) \to
467 intros.simplify in H.change with gcd n m = (S O).
471 change with (S (S O)) \le gcd n m \to False.intro.
472 apply H1.rewrite < H3 (gcd n m).
474 apply divides_gcd_n.assumption.
475 cut O < gcd n m \lor O = gcd n m.
476 elim Hcut.assumption.
478 apply not_le_Sn_O (S O).
480 elim Hcut1.rewrite < H5 in \vdash (? ? %).assumption.
481 apply gcd_O_to_eq_O.apply sym_eq.assumption.
482 apply le_to_or_lt_eq.apply le_O_n.
485 theorem divides_times_to_divides: \forall n,p,q:nat.prime n \to divides n (p*q) \to
486 divides n p \lor divides n q.
488 cut divides n p \lor \not (divides n p).
492 cut \exists a,b. a*n - b*p = (S O) \lor b*p - a*n = (S O).
493 elim Hcut1.elim H3.elim H4.
495 rewrite > times_n_SO q.rewrite < H5.
496 rewrite > distr_times_minus.
497 rewrite > sym_times q (a1*p).
498 rewrite > assoc_times a1.
499 elim H1.rewrite > H6.
500 rewrite < sym_times n.rewrite < assoc_times.
501 rewrite > sym_times q.rewrite > assoc_times.
502 rewrite < assoc_times a1.rewrite < sym_times n.
503 rewrite > assoc_times n.
504 rewrite < distr_times_minus.
505 apply witness ? ? (q*a-a1*n2).reflexivity.
507 rewrite > times_n_SO q.rewrite < H5.
508 rewrite > distr_times_minus.
509 rewrite > sym_times q (a1*p).
510 rewrite > assoc_times a1.
511 elim H1.rewrite > H6.
512 rewrite < sym_times.rewrite > assoc_times.
513 rewrite < assoc_times q.
514 rewrite < sym_times n.
515 rewrite < distr_times_minus.
516 apply witness ? ? (n2*a1-q*a).reflexivity.
517 (* end second case *)
518 rewrite < prime_to_gcd_SO n p.
520 assumption.assumption.
521 apply decidable_divides n p.
522 apply trans_lt ? (S O).simplify.apply le_n.
523 simplify in H.elim H. assumption.