1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 set "baseuri" "cic:/matita/nat/gcd_properties1".
17 include "nat/propr_div_mod_lt_le_totient1_aux.ma".
19 (* this file contains some important properites of gcd in N *)
21 (*it's a generalization of the existing theorem divides_gcd_aux (in which
22 c = 1), proved in file gcd.ma
24 theorem divides_times_gcd_aux: \forall p,m,n,d,c.
25 O \lt c \to O < n \to n \le m \to n \le p \to
26 d \divides (c*m) \to d \divides (c*n) \to d \divides c*gcd_aux p m n.
35 cut (n1 \divides m \lor n1 \ndivides m)
37 [ rewrite > divides_to_divides_b_true
43 | rewrite > not_divides_to_divides_b_false
47 | cut (O \lt m \mod n1 \lor O = m \mod n1)
50 | absurd (n1 \divides m)
51 [ apply mod_O_to_divides
59 | apply le_to_or_lt_eq.
67 [ change with (m \mod n1 < n1).
74 [ rewrite < (sym_times c m).
75 rewrite < (sym_times c n1).
77 [ rewrite > (S_pred c)
78 [ rewrite > (S_pred n1)
79 [ apply (lt_O_times_S_S)
95 | apply (decidable_divides n1 m).
101 (*it's a generalization of the existing theorem divides_gcd_d (in which
102 c = 1), proved in file gcd.ma
104 theorem divides_d_times_gcd: \forall m,n,d,c.
105 O \lt c \to d \divides (c*m) \to d \divides (c*n) \to d \divides c*gcd n m.
113 | (S p) \Rightarrow gcd_aux (S p) m (S p) ]
117 | (S p) \Rightarrow gcd_aux (S p) n (S p) ]]).
119 [ apply (nat_case1 n)
124 change with (d \divides c*gcd_aux (S m1) m (S m1)).
125 apply divides_times_gcd_aux
131 | apply (le_n (S m1))
137 | apply (nat_case1 m)
142 change with (d \divides c * gcd_aux (S m1) n (S m1)).
143 apply divides_times_gcd_aux
145 change with (O \lt c).
151 | apply (le_n (S m1)).
160 (* 2 basic properties of divides predicate *)
161 theorem aDIVb_to_bDIVa_to_aEQb:
163 a \divides b \to b \divides a \to a = b.
165 apply antisymmetric_divides;
170 theorem O_div_c_to_c_eq_O: \forall c:nat.
171 O \divides c \to c = O.
173 apply aDIVb_to_bDIVa_to_aEQb
179 (* an alternative characterization for gcd *)
180 theorem gcd1: \forall a,b,c:nat.
181 c \divides a \to c \divides b \to
182 (\forall d:nat. d \divides a \to d \divides b \to d \divides c) \to (gcd a b) = c.
184 elim (H2 ((gcd a b)))
185 [ apply (aDIVb_to_bDIVa_to_aEQb (gcd a b) c)
186 [ apply (witness (gcd a b) c n2).
188 | apply divides_d_gcd;
191 | apply divides_gcd_n
198 theorem eq_gcd_times_times_eqv_times_gcd: \forall a,b,c:nat.
199 (gcd (c*a) (c*b)) = c*(gcd a b).
208 [ apply divides_times
210 | apply divides_gcd_n.
212 | apply divides_times
218 apply (divides_d_times_gcd)
231 rewrite > (sym_times c O).
238 rewrite > (sym_times ? O).
239 rewrite > (sym_gcd a O).
246 [ apply divides_times
248 | apply divides_gcd_n.
250 | apply divides_times
256 apply (divides_d_times_gcd)
269 theorem associative_nat_gcd: associative nat gcd.
270 change with (\forall a,b,c:nat. (gcd (gcd a b) c) = (gcd a (gcd b c))).
273 [ apply divides_d_gcd
274 [ apply (trans_divides ? (gcd b c) ?)
275 [ apply divides_gcd_m
276 | apply divides_gcd_n
278 | apply divides_gcd_n
280 | apply (trans_divides ? (gcd b c) ?)
281 [ apply divides_gcd_m
282 | apply divides_gcd_m
285 cut (d \divides a \land d \divides b)
287 cut (d \divides (gcd b c))
288 [ apply (divides_d_gcd (gcd b c) a d Hcut1 H2)
289 | apply (divides_d_gcd c b d H1 H3)
292 [ apply (trans_divides d (gcd a b) a H).
294 | apply (trans_divides d (gcd a b) b H).
301 theorem aDIVIDES_b_TIMES_c_to_GCD_a_b_eq_d_to_aDIVd_DIVIDES_c: \forall a,b,c,d:nat.
302 a \divides (b*c) \to (gcd a b) = d \to (a/d) \divides c.
312 | rewrite > H2 in H1.
319 [ rewrite > (S_pred d Hcut).
324 apply (divides_n_n O)
325 | apply (lt_times_eq_O b c)
328 | apply (O_div_c_to_c_eq_O (b*c) H)
340 cut (d \divides a \land d \divides b)
344 rewrite < (NdivM_times_M_to_N a d) in H3
345 [ rewrite < (NdivM_times_M_to_N b d) in H3
346 [ cut (b/d*c = a/d*n2)
347 [ apply (gcd_SO_to_divides_times_to_divides (b/d) (a/d) c)
348 [ apply (O_lt_times_to_O_lt (a/d) d).
349 rewrite > (NdivM_times_M_to_N a d);
351 | apply (inj_times_r1 d ? ?)
353 | rewrite < (eq_gcd_times_times_eqv_times_gcd (a/d) (b/d) d).
354 rewrite < (times_n_SO d).
355 rewrite < (sym_times (a/d) d).
356 rewrite < (sym_times (b/d) d).
357 rewrite > (NdivM_times_M_to_N a d)
358 [ rewrite > (NdivM_times_M_to_N b d);
364 | apply (witness (a/d) ((b/d)*c) n2 Hcut3)
366 | apply (inj_times_r1 d ? ?)
368 | rewrite > sym_times.
369 rewrite > (sym_times d ((a/d) * n2)).
370 rewrite > assoc_times.
371 rewrite > (assoc_times (a/d) n2 d).
372 rewrite > (sym_times c d).
373 rewrite > (sym_times n2 d).
374 rewrite < assoc_times.
375 rewrite < (assoc_times (a/d) d n2).
395 [ apply divides_gcd_n
396 | apply divides_gcd_m
402 theorem gcd_sum_times_eq_gcd_aux: \forall a,b,d,m:nat.
403 (gcd (a+m*b) b) = d \to (gcd a b) = d.
406 [ rewrite > (minus_plus_m_m a (m*b)).
410 | rewrite > (times_n_SO d).
411 rewrite > (sym_times d ?).
426 | rewrite > (times_n_SO d1).
427 rewrite > (sym_times d1 ?).
437 theorem gcd_sum_times_eq_gcd: \forall a,b,m:nat.
438 (gcd (a+m*b) b) = (gcd a b).
441 apply (gcd_sum_times_eq_gcd_aux a b (gcd (a+m*b) b) m).
445 theorem gcd_div_div_eq_div_gcd: \forall a,b,m:nat.
446 O \lt m \to m \divides a \to m \divides b \to
447 (gcd (a/m) (b/m)) = (gcd a b) / m.
449 apply (inj_times_r1 m H).
450 rewrite > (sym_times m ((gcd a b)/m)).
451 rewrite > (NdivM_times_M_to_N (gcd a b) m)
452 [ rewrite < eq_gcd_times_times_eqv_times_gcd.
453 rewrite > (sym_times m (a/m)).
454 rewrite > (sym_times m (b/m)).
455 rewrite > (NdivM_times_M_to_N a m H H1).
456 rewrite > (NdivM_times_M_to_N b m H H2).
459 | apply divides_d_gcd;
465 theorem gcdSO_divides_divides_times_divides: \forall c,e,f:nat.
466 (gcd e f) = (S O) \to e \divides c \to f \divides c \to
474 apply (divides_n_n O).
479 [ apply (le_to_not_lt O O)
483 | apply (divides_to_lt_O O c)
495 rewrite > (sym_times e f).
496 apply (divides_times)
497 [ apply (divides_n_n)
498 | rewrite > H5 in H1.
499 apply (gcd_SO_to_divides_times_to_divides f e n)
510 (* the following theorem shows that gcd is a multiplicative function in
511 the following sense: if a1 and a2 are relatively prime, then
512 gcd(a1·a2, b) = gcd(a1, b)·gcd(a2, b).
514 theorem gcd_aTIMESb_c_eq_gcd_a_c_TIMES_gcd_b_c: \forall a,b,c:nat.
515 (gcd a b) = (S O) \to (gcd (a*b) c) = (gcd a c) * (gcd b c).
518 [ apply divides_times;
520 | apply (gcdSO_divides_divides_times_divides c (gcd a c) (gcd b c))
528 apply (divides_d_gcd b a d Hcut1 Hcut)
529 | apply (trans_divides d (gcd b c) b)
531 | apply (divides_gcd_n)
534 | apply (trans_divides d (gcd a c) a)
536 | apply (divides_gcd_n)
540 | apply (divides_gcd_m)
541 | apply (divides_gcd_m)
544 rewrite < (eq_gcd_times_times_eqv_times_gcd b c (gcd a c)).
545 rewrite > (sym_times (gcd a c) b).
546 rewrite > (sym_times (gcd a c) c).
547 rewrite < (eq_gcd_times_times_eqv_times_gcd a c b).
548 rewrite < (eq_gcd_times_times_eqv_times_gcd a c c).
549 apply (divides_d_gcd)
550 [ apply (divides_d_gcd)
551 [ rewrite > (times_n_SO d).
552 apply (divides_times)
556 | rewrite > (times_n_SO d).
557 apply (divides_times)
562 | apply (divides_d_gcd)
563 [ rewrite > (times_n_SO d).
564 rewrite > (sym_times d (S O)).
565 apply (divides_times)
566 [ apply (divides_SO_n)
569 | rewrite < (sym_times a b).
577 theorem gcd_eq_gcd_minus: \forall a,b:nat.
578 a \lt b \to (gcd a b) = (gcd (b - a) b).
582 [ apply (divides_minus (gcd a b) b a)
583 [ apply divides_gcd_m
584 | apply divides_gcd_n
586 | apply divides_gcd_m
591 [ cut (b - (d*n2) = a)
592 [ rewrite > H4 in Hcut1.
593 rewrite < (distr_times_minus d n n2) in Hcut1.
596 | apply (witness d a (n - n2)).
600 | apply (plus_to_minus ? ? ? Hcut)
602 | rewrite > sym_plus.
603 apply (minus_to_plus)