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.
49 rewrite > div_mod m n in \vdash (? ? %).
51 apply eq_plus_to_le ? ? (m \mod n).
55 apply div_mod.assumption.
58 theorem divides_mod_to_divides: \forall p,m,n:nat. O < n \to
59 p \divides (m \mod n) \to p \divides n \to p \divides m.
60 intros.elim H1.elim H2.
61 apply witness p m ((n1*(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 gcd_aux p m n \divides m \land gcd_aux p m n \divides n.
72 absurd O < n.assumption.apply le_to_not_lt.assumption.
73 cut (n1 \divides m) \lor (n1 \ndivides m).
75 (match divides_b n1 m with
77 | false \Rightarrow gcd_aux n n1 (m \mod n1)]) \divides m \land
78 (match divides_b n1 m with
80 | false \Rightarrow gcd_aux n n1 (m \mod n1)]) \divides n1.
81 elim Hcut.rewrite > divides_to_divides_b_true.
83 split.assumption.apply witness n1 n1 (S O).apply times_n_SO.
84 assumption.assumption.
85 rewrite > not_divides_to_divides_b_false.
87 gcd_aux n n1 (m \mod n1) \divides m \land
88 gcd_aux n n1 (m \mod n1) \divides n1.
89 cut gcd_aux n n1 (m \mod n1) \divides n1 \land
90 gcd_aux n n1 (m \mod n1) \divides mod m n1.
92 split.apply divides_mod_to_divides ? ? n1.
93 assumption.assumption.assumption.assumption.
95 cut O \lt m \mod n1 \lor O = mod m n1.
96 elim Hcut1.assumption.
97 apply False_ind.apply H4.apply mod_O_to_divides.
98 assumption.apply sym_eq.assumption.
99 apply le_to_or_lt_eq.apply le_O_n.
101 apply lt_mod_m_m.assumption.
104 change with m \mod n1 < n1.
105 apply lt_mod_m_m.assumption.assumption.
106 assumption.assumption.
107 apply decidable_divides n1 m.assumption.
110 theorem divides_gcd_nm: \forall n,m.
111 gcd n m \divides m \land gcd n m \divides n.
118 | (S p) \Rightarrow gcd_aux (S p) m (S p) ]
122 | (S p) \Rightarrow gcd_aux (S p) n (S p) ]] \divides m
128 | (S p) \Rightarrow gcd_aux (S p) m (S p) ]
132 | (S p) \Rightarrow gcd_aux (S p) n (S p) ]] \divides n.
135 simplify.intros.split.
136 apply witness m m (S O).apply times_n_SO.
137 apply witness m O O.apply times_n_O.
139 gcd_aux (S m1) m (S m1) \divides m
141 gcd_aux (S m1) m (S m1) \divides (S m1).
142 apply divides_gcd_aux_mn.
143 simplify.apply le_S_S.apply le_O_n.
144 assumption.apply le_n.
147 simplify.intros.split.
148 apply witness n O O.apply times_n_O.
149 apply witness n n (S O).apply times_n_SO.
151 gcd_aux (S m1) n (S m1) \divides (S m1)
153 gcd_aux (S m1) n (S m1) \divides n.
154 cut gcd_aux (S m1) n (S m1) \divides n
156 gcd_aux (S m1) n (S m1) \divides S m1.
157 elim Hcut.split.assumption.assumption.
158 apply divides_gcd_aux_mn.
159 simplify.apply le_S_S.apply le_O_n.
160 apply not_lt_to_le.simplify.intro.apply H.
161 rewrite > H1.apply trans_le ? (S n).
162 apply le_n_Sn.assumption.apply le_n.
165 theorem divides_gcd_n: \forall n,m. gcd n m \divides n.
167 exact proj2 ? ? (divides_gcd_nm n m).
170 theorem divides_gcd_m: \forall n,m. gcd n m \divides m.
172 exact proj1 ? ? (divides_gcd_nm n m).
175 theorem divides_gcd_aux: \forall p,m,n,d. O < n \to n \le m \to n \le p \to
176 d \divides m \to d \divides n \to d \divides gcd_aux p m n.
178 absurd O < n.assumption.apply le_to_not_lt.assumption.
181 (match divides_b n1 m with
182 [ true \Rightarrow n1
183 | false \Rightarrow gcd_aux n n1 (m \mod n1)]).
184 cut n1 \divides m \lor n1 \ndivides m.
186 rewrite > divides_to_divides_b_true.
188 assumption.assumption.
189 rewrite > not_divides_to_divides_b_false.
190 change with d \divides gcd_aux n n1 (m \mod n1).
192 cut O \lt m \mod n1 \lor O = m \mod n1.
193 elim Hcut1.assumption.
194 absurd n1 \divides m.apply mod_O_to_divides.
195 assumption.apply sym_eq.assumption.assumption.
196 apply le_to_or_lt_eq.apply le_O_n.
198 apply lt_mod_m_m.assumption.
201 change with m \mod n1 < n1.
202 apply lt_mod_m_m.assumption.assumption.
204 apply divides_mod.assumption.assumption.assumption.
205 assumption.assumption.
206 apply decidable_divides n1 m.assumption.
209 theorem divides_d_gcd: \forall m,n,d.
210 d \divides m \to d \divides n \to d \divides gcd n m.
218 | (S p) \Rightarrow gcd_aux (S p) m (S p) ]
222 | (S p) \Rightarrow gcd_aux (S p) n (S p) ]].
224 apply nat_case1 n.simplify.intros.assumption.
226 change with d \divides gcd_aux (S m1) m (S m1).
227 apply divides_gcd_aux.
228 simplify.apply le_S_S.apply le_O_n.assumption.apply le_n.assumption.
229 rewrite < H2.assumption.
230 apply nat_case1 m.simplify.intros.assumption.
232 change with d \divides gcd_aux (S m1) n (S m1).
233 apply divides_gcd_aux.
234 simplify.apply le_S_S.apply le_O_n.
235 apply lt_to_le.apply not_le_to_lt.assumption.apply le_n.assumption.
236 rewrite < H2.assumption.
239 theorem eq_minus_gcd_aux: \forall p,m,n.O < n \to n \le m \to n \le p \to
240 \exists a,b. a*n - b*m = gcd_aux p m n \lor b*m - a*n = gcd_aux p m n.
243 absurd O < n.assumption.apply le_to_not_lt.assumption.
245 cut n1 \divides m \lor n1 \ndivides m.
248 a*n1 - b*m = match divides_b n1 m with
249 [ true \Rightarrow n1
250 | false \Rightarrow gcd_aux n n1 (m \mod n1)]
252 b*m - a*n1 = match divides_b n1 m with
253 [ true \Rightarrow n1
254 | false \Rightarrow gcd_aux n n1 (m \mod n1)].
256 rewrite > divides_to_divides_b_true.
258 apply ex_intro ? ? (S O).
259 apply ex_intro ? ? O.
260 left.simplify.rewrite < plus_n_O.
261 apply sym_eq.apply minus_n_O.
262 assumption.assumption.
263 rewrite > not_divides_to_divides_b_false.
266 a*n1 - b*m = gcd_aux n n1 (m \mod n1)
268 b*m - a*n1 = gcd_aux n n1 (m \mod n1).
271 a*(m \mod n1) - b*n1= gcd_aux n n1 (m \mod n1)
273 b*n1 - a*(m \mod n1) = gcd_aux n n1 (m \mod n1).
274 elim Hcut2.elim H5.elim H6.
277 apply ex_intro ? ? (a1+a*(m / n1)).
278 apply ex_intro ? ? a.
281 rewrite < sym_times n1.
282 rewrite > distr_times_plus.
283 rewrite > sym_times n1.
284 rewrite > sym_times n1.
285 rewrite > div_mod m n1 in \vdash (? ? (? % ?) ?).
286 rewrite > assoc_times.
288 rewrite > distr_times_plus.
289 rewrite < eq_minus_minus_minus_plus.
291 rewrite < plus_minus.
292 rewrite < minus_n_n.reflexivity.
297 apply ex_intro ? ? (a1+a*(m / n1)).
298 apply ex_intro ? ? a.
300 (* clear Hcut2.clear H5.clear H6.clear H. *)
302 rewrite > distr_times_plus.
304 rewrite > sym_times n1.
305 rewrite > div_mod m n1 in \vdash (? ? (? ? %) ?).
306 rewrite > distr_times_plus.
307 rewrite > assoc_times.
308 rewrite < eq_minus_minus_minus_plus.
310 rewrite < plus_minus.
311 rewrite < minus_n_n.reflexivity.
314 apply H n1 (m \mod n1).
315 cut O \lt m \mod n1 \lor O = m \mod n1.
316 elim Hcut2.assumption.
317 absurd n1 \divides m.apply mod_O_to_divides.
319 symmetry.assumption.assumption.
320 apply le_to_or_lt_eq.apply le_O_n.
322 apply lt_mod_m_m.assumption.
325 change with m \mod n1 < n1.
327 assumption.assumption.assumption.assumption.
328 apply decidable_divides n1 m.assumption.
329 apply lt_to_le_to_lt ? n1.assumption.assumption.
332 theorem eq_minus_gcd:
333 \forall m,n.\exists a,b.a*n - b*m = (gcd n m) \lor b*m - a*n = (gcd n m).
339 apply ex_intro ? ? O.
340 apply ex_intro ? ? (S O).
343 apply sym_eq.apply minus_n_O.
347 a*(S m1) - b*m = (gcd_aux (S m1) m (S m1))
348 \lor b*m - a*(S m1) = (gcd_aux (S m1) m (S m1)).
349 apply eq_minus_gcd_aux.
350 simplify. apply le_S_S.apply le_O_n.
351 assumption.apply le_n.
354 apply ex_intro ? ? (S O).
355 apply ex_intro ? ? O.
358 apply sym_eq.apply minus_n_O.
362 a*n - b*(S m1) = (gcd_aux (S m1) n (S m1))
363 \lor b*(S m1) - a*n = (gcd_aux (S m1) n (S m1)).
366 a*(S m1) - b*n = (gcd_aux (S m1) n (S m1))
368 b*n - a*(S m1) = (gcd_aux (S m1) n (S m1)).
369 elim Hcut.elim H2.elim H3.
370 apply ex_intro ? ? a1.
371 apply ex_intro ? ? a.
373 apply ex_intro ? ? a1.
374 apply ex_intro ? ? a.
376 apply eq_minus_gcd_aux.
377 simplify. apply le_S_S.apply le_O_n.
378 apply lt_to_le.apply not_le_to_lt.assumption.
382 (* some properties of gcd *)
384 theorem gcd_O_n: \forall n:nat. gcd O n = n.
385 intro.simplify.reflexivity.
388 theorem gcd_O_to_eq_O:\forall m,n:nat. (gcd m n) = O \to
390 intros.cut O \divides n \land O \divides m.
391 elim Hcut.elim H2.split.
392 assumption.elim H1.assumption.
394 apply divides_gcd_nm.
397 theorem symmetric_gcd: symmetric nat gcd.
399 \forall n,m:nat. gcd n m = gcd m n.
401 cut O < (gcd n m) \lor O = (gcd n m).
403 cut O < (gcd m n) \lor O = (gcd m n).
406 apply divides_to_le.assumption.
407 apply divides_d_gcd.apply divides_gcd_n.apply divides_gcd_m.
408 apply divides_to_le.assumption.
409 apply divides_d_gcd.apply divides_gcd_n.apply divides_gcd_m.
412 elim Hcut2.rewrite > H2.rewrite > H3.reflexivity.
413 apply gcd_O_to_eq_O.apply sym_eq.assumption.
414 apply le_to_or_lt_eq.apply le_O_n.
417 elim Hcut1.rewrite > H1.rewrite > H2.reflexivity.
418 apply gcd_O_to_eq_O.apply sym_eq.assumption.
419 apply le_to_or_lt_eq.apply le_O_n.
422 variant sym_gcd: \forall n,m:nat. gcd n m = gcd m n \def
425 theorem gcd_SO_n: \forall n:nat. gcd (S O) n = (S O).
427 apply antisym_le.apply divides_to_le.simplify.apply le_n.
429 cut O < gcd (S O) n \lor O = gcd (S O) n.
430 elim Hcut.assumption.
433 cut (S O)=O \land n=O.
434 elim Hcut1.apply sym_eq.assumption.
435 apply gcd_O_to_eq_O.apply sym_eq.assumption.
436 apply le_to_or_lt_eq.apply le_O_n.
439 theorem prime_to_gcd_SO: \forall n,m:nat. prime n \to n \ndivides m \to
441 intros.simplify in H.change with gcd n m = (S O).
445 change with (S (S O)) \le gcd n m \to False.intro.
446 apply H1.rewrite < H3 (gcd n m).
448 apply divides_gcd_n.assumption.
449 cut O < gcd n m \lor O = gcd n m.
450 elim Hcut.assumption.
452 apply not_le_Sn_O (S O).
454 elim Hcut1.rewrite < H5 in \vdash (? ? %).assumption.
455 apply gcd_O_to_eq_O.apply sym_eq.assumption.
456 apply le_to_or_lt_eq.apply le_O_n.
459 theorem divides_times_to_divides: \forall n,p,q:nat.prime n \to n \divides p*q \to
460 n \divides p \lor n \divides q.
462 cut n \divides p \lor n \ndivides p.
466 cut \exists a,b. a*n - b*p = (S O) \lor b*p - a*n = (S O).
467 elim Hcut1.elim H3.elim H4.
469 rewrite > times_n_SO q.rewrite < H5.
470 rewrite > distr_times_minus.
471 rewrite > sym_times q (a1*p).
472 rewrite > assoc_times a1.
473 elim H1.rewrite > H6.
474 rewrite < sym_times n.rewrite < assoc_times.
475 rewrite > sym_times q.rewrite > assoc_times.
476 rewrite < assoc_times a1.rewrite < sym_times n.
477 rewrite > assoc_times n.
478 rewrite < distr_times_minus.
479 apply witness ? ? (q*a-a1*n2).reflexivity.
481 rewrite > times_n_SO q.rewrite < H5.
482 rewrite > distr_times_minus.
483 rewrite > sym_times q (a1*p).
484 rewrite > assoc_times a1.
485 elim H1.rewrite > H6.
486 rewrite < sym_times.rewrite > assoc_times.
487 rewrite < assoc_times q.
488 rewrite < sym_times n.
489 rewrite < distr_times_minus.
490 apply witness ? ? (n2*a1-q*a).reflexivity.
491 (* end second case *)
492 rewrite < prime_to_gcd_SO n p.
494 assumption.assumption.
495 apply decidable_divides n p.
496 apply trans_lt ? (S O).simplify.apply le_n.
497 simplify in H.elim H. assumption.