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).
209 rewrite > (sym_times c O).
216 rewrite > (sym_times ? O).
217 rewrite > (sym_gcd a O).
224 [ apply divides_times
226 | apply divides_gcd_n.
228 | apply divides_times
234 apply (divides_d_times_gcd)
247 theorem associative_nat_gcd: associative nat gcd.
248 change with (\forall a,b,c:nat. (gcd (gcd a b) c) = (gcd a (gcd b c))).
251 [ apply divides_d_gcd
252 [ apply (trans_divides ? (gcd b c) ?)
253 [ apply divides_gcd_m
254 | apply divides_gcd_n
256 | apply divides_gcd_n
258 | apply (trans_divides ? (gcd b c) ?)
259 [ apply divides_gcd_m
260 | apply divides_gcd_m
263 cut (d \divides a \land d \divides b)
265 cut (d \divides (gcd b c))
266 [ apply (divides_d_gcd (gcd b c) a d Hcut1 H2)
267 | apply (divides_d_gcd c b d H1 H3)
270 [ apply (trans_divides d (gcd a b) a H).
272 | apply (trans_divides d (gcd a b) b H).
279 theorem aDIVIDES_b_TIMES_c_to_GCD_a_b_eq_d_to_aDIVd_DIVIDES_c: \forall a,b,c,d:nat.
280 a \divides (b*c) \to (gcd a b) = d \to (a/d) \divides c.
290 | rewrite > H2 in H1.
297 [ rewrite > (S_pred d Hcut).
302 apply (divides_n_n O)
303 | apply (lt_times_eq_O b c)
306 | apply (O_div_c_to_c_eq_O (b*c) H)
318 cut (d \divides a \land d \divides b)
322 rewrite < (NdivM_times_M_to_N a d) in H3
323 [ rewrite < (NdivM_times_M_to_N b d) in H3
324 [ cut (b/d*c = a/d*n2)
325 [ apply (gcd_SO_to_divides_times_to_divides (b/d) (a/d) c)
326 [ apply (O_lt_times_to_O_lt (a/d) d).
327 rewrite > (NdivM_times_M_to_N a d);
329 | apply (inj_times_r1 d ? ?)
331 | rewrite < (eq_gcd_times_times_eqv_times_gcd (a/d) (b/d) d).
332 rewrite < (times_n_SO d).
333 rewrite < (sym_times (a/d) d).
334 rewrite < (sym_times (b/d) d).
335 rewrite > (NdivM_times_M_to_N a d)
336 [ rewrite > (NdivM_times_M_to_N b d);
342 | apply (witness (a/d) ((b/d)*c) n2 Hcut3)
344 | apply (inj_times_r1 d ? ?)
346 | rewrite > sym_times.
347 rewrite > (sym_times d ((a/d) * n2)).
348 rewrite > assoc_times.
349 rewrite > (assoc_times (a/d) n2 d).
350 rewrite > (sym_times c d).
351 rewrite > (sym_times n2 d).
352 rewrite < assoc_times.
353 rewrite < (assoc_times (a/d) d n2).
373 [ apply divides_gcd_n
374 | apply divides_gcd_m
380 theorem gcd_sum_times_eq_gcd_aux: \forall a,b,d,m:nat.
381 (gcd (a+m*b) b) = d \to (gcd a b) = d.
384 [ rewrite > (minus_plus_m_m a (m*b)).
388 | rewrite > (times_n_SO d).
389 rewrite > (sym_times d ?).
404 | rewrite > (times_n_SO d1).
405 rewrite > (sym_times d1 ?).
415 theorem gcd_sum_times_eq_gcd: \forall a,b,m:nat.
416 (gcd (a+m*b) b) = (gcd a b).
419 apply (gcd_sum_times_eq_gcd_aux a b (gcd (a+m*b) b) m).
423 theorem gcd_div_div_eq_div_gcd: \forall a,b,m:nat.
424 O \lt m \to m \divides a \to m \divides b \to
425 (gcd (a/m) (b/m)) = (gcd a b) / m.
427 apply (inj_times_r1 m H).
428 rewrite > (sym_times m ((gcd a b)/m)).
429 rewrite > (NdivM_times_M_to_N (gcd a b) m)
430 [ rewrite < eq_gcd_times_times_eqv_times_gcd.
431 rewrite > (sym_times m (a/m)).
432 rewrite > (sym_times m (b/m)).
433 rewrite > (NdivM_times_M_to_N a m H H1).
434 rewrite > (NdivM_times_M_to_N b m H H2).
437 | apply divides_d_gcd;
443 theorem gcdSO_divides_divides_times_divides: \forall c,e,f:nat.
444 (gcd e f) = (S O) \to e \divides c \to f \divides c \to
452 apply (divides_n_n O).
457 [ apply (le_to_not_lt O O)
461 | apply (divides_to_lt_O O c)
473 rewrite > (sym_times e f).
474 apply (divides_times)
475 [ apply (divides_n_n)
476 | rewrite > H5 in H1.
477 apply (gcd_SO_to_divides_times_to_divides f e n)
488 (* the following theorem shows that gcd is a multiplicative function in
489 the following sense: if a1 and a2 are relatively prime, then
490 gcd(a1·a2, b) = gcd(a1, b)·gcd(a2, b).
492 theorem gcd_aTIMESb_c_eq_gcd_a_c_TIMES_gcd_b_c: \forall a,b,c:nat.
493 (gcd a b) = (S O) \to (gcd (a*b) c) = (gcd a c) * (gcd b c).
496 [ apply divides_times;
498 | apply (gcdSO_divides_divides_times_divides c (gcd a c) (gcd b c))
506 apply (divides_d_gcd b a d Hcut1 Hcut)
507 | apply (trans_divides d (gcd b c) b)
509 | apply (divides_gcd_n)
512 | apply (trans_divides d (gcd a c) a)
514 | apply (divides_gcd_n)
518 | apply (divides_gcd_m)
519 | apply (divides_gcd_m)
522 rewrite < (eq_gcd_times_times_eqv_times_gcd b c (gcd a c)).
523 rewrite > (sym_times (gcd a c) b).
524 rewrite > (sym_times (gcd a c) c).
525 rewrite < (eq_gcd_times_times_eqv_times_gcd a c b).
526 rewrite < (eq_gcd_times_times_eqv_times_gcd a c c).
527 apply (divides_d_gcd)
528 [ apply (divides_d_gcd)
529 [ rewrite > (times_n_SO d).
530 apply (divides_times)
534 | rewrite > (times_n_SO d).
535 apply (divides_times)
540 | apply (divides_d_gcd)
541 [ rewrite > (times_n_SO d).
542 rewrite > (sym_times d (S O)).
543 apply (divides_times)
544 [ apply (divides_SO_n)
547 | rewrite < (sym_times a b).
555 theorem gcd_eq_gcd_minus: \forall a,b:nat.
556 a \lt b \to (gcd a b) = (gcd (b - a) b).
560 [ apply (divides_minus (gcd a b) b a)
561 [ apply divides_gcd_m
562 | apply divides_gcd_n
564 | apply divides_gcd_m
569 [ cut (b - (d*n2) = a)
570 [ rewrite > H4 in Hcut1.
571 rewrite < (distr_times_minus d n n2) in Hcut1.
574 | apply (witness d a (n - n2)).
578 | apply (plus_to_minus ? ? ? Hcut)
580 | rewrite > sym_plus.
581 apply (minus_to_plus)