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".
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 (* an alternative characterization for gcd *)
161 theorem gcd1: \forall a,b,c:nat.
162 c \divides a \to c \divides b \to
163 (\forall d:nat. d \divides a \to d \divides b \to d \divides c) \to (gcd a b) = c.
165 elim (H2 ((gcd a b)))
166 [ apply (antisymmetric_divides (gcd a b) c)
167 [ apply (witness (gcd a b) c n2).
169 | apply divides_d_gcd;
172 | apply divides_gcd_n
179 theorem eq_gcd_times_times_times_gcd: \forall a,b,c:nat.
180 (gcd (c*a) (c*b)) = c*(gcd a b).
189 [ apply divides_times
191 | apply divides_gcd_n.
193 | apply divides_times
199 apply (divides_d_times_gcd)
209 theorem associative_nat_gcd: associative nat gcd.
210 change with (\forall a,b,c:nat. (gcd (gcd a b) c) = (gcd a (gcd b c))).
213 [ apply divides_d_gcd
214 [ apply (trans_divides ? (gcd b c) ?)
215 [ apply divides_gcd_m
216 | apply divides_gcd_n
218 | apply divides_gcd_n
220 | apply (trans_divides ? (gcd b c) ?)
221 [ apply divides_gcd_m
222 | apply divides_gcd_m
225 cut (d \divides a \land d \divides b)
227 cut (d \divides (gcd b c))
228 [ apply (divides_d_gcd (gcd b c) a d Hcut1 H2)
229 | apply (divides_d_gcd c b d H1 H3)
232 [ apply (trans_divides d (gcd a b) a H).
234 | apply (trans_divides d (gcd a b) b H).
242 theorem eq_gcd_div_div_div_gcd: \forall a,b,m:nat.
243 O \lt m \to m \divides a \to m \divides b \to
244 (gcd (a/m) (b/m)) = (gcd a b) / m.
246 apply (inj_times_r1 m H).
247 rewrite > (sym_times m ((gcd a b)/m)).
248 rewrite > (divides_to_times_div (gcd a b) m)
249 [ rewrite < eq_gcd_times_times_times_gcd.
250 rewrite > (sym_times m (a/m)).
251 rewrite > (sym_times m (b/m)).
252 rewrite > (divides_to_times_div a m H H1).
253 rewrite > (divides_to_times_div b m H H2).
256 | apply divides_d_gcd;
263 theorem divides_times_to_divides_div_gcd: \forall a,b,c:nat.
264 a \divides (b*c) \to (a/(gcd a b)) \divides c.
269 [ (*It's an impossible situation*)
276 apply (divides_n_n O)
277 | apply (lt_times_eq_O b c)
280 | apply antisymmetric_divides
292 [ cut (O \lt (gcd a b))
293 [ apply (gcd_SO_to_divides_times_to_divides (b/(gcd a b)) (a/(gcd a b)) c)
294 [ apply (O_lt_times_to_O_lt (a/(gcd a b)) (gcd a b)).
295 rewrite > (divides_to_times_div a (gcd a b))
298 | apply divides_gcd_n
300 | rewrite < (div_n_n (gcd a b)) in \vdash (? ? ? %)
301 [ apply eq_gcd_div_div_div_gcd
303 | apply divides_gcd_n
304 | apply divides_gcd_m
308 | apply (witness ? ? n2).
309 apply (inj_times_r1 (gcd a b) Hcut1).
310 rewrite < assoc_times.
311 rewrite < sym_times in \vdash (? ? (? % ?) ?).
312 rewrite > (divides_to_times_div b (gcd a b))
313 [ rewrite < assoc_times in \vdash (? ? ? %).
314 rewrite < sym_times in \vdash (? ? ? (? % ?)).
315 rewrite > (divides_to_times_div a (gcd a b))
318 | apply divides_gcd_n
321 | apply divides_gcd_m
334 theorem gcd_plus_times_gcd: \forall a,b,d,m:nat.
335 (gcd (a+m*b) b) = (gcd a b).
339 [ apply divides_gcd_n
340 | apply (trans_divides ? b ?)
341 [ apply divides_gcd_m
342 | rewrite > sym_times.
343 apply (witness b (b*m) m).
347 | apply divides_gcd_m
351 | rewrite > (minus_plus_m_m a (m*b)).
354 | apply (trans_divides ? b ?)
356 | rewrite > sym_times.
357 apply (witness b (b*m) m).
367 theorem gcd_SO_to_divides_to_divides_to_divides_times: \forall c,e,f:nat.
368 (gcd e f) = (S O) \to e \divides c \to f \divides c \to
371 apply (nat_case1 c); intros
377 rewrite > (sym_times e f).
378 apply (divides_times)
379 [ apply (divides_n_n)
380 | rewrite > H5 in H1.
381 apply (gcd_SO_to_divides_times_to_divides f e n)
382 [ rewrite < H5 in H1.
384 apply (divides_to_lt_O e (S m))
394 (* the following theorem shows that gcd is a multiplicative function in
395 the following sense: if a1 and a2 are relatively prime, then
396 gcd(a1·a2, b) = gcd(a1, b)·gcd(a2, b).
398 theorem gcd_SO_to_eq_gcd_times_times_gcd_gcd: \forall a,b,c:nat.
399 (gcd a b) = (S O) \to (gcd (a*b) c) = (gcd a c) * (gcd b c).
402 [ apply divides_times;
404 | apply (gcd_SO_to_divides_to_divides_to_divides_times c (gcd a c) (gcd b c))
412 apply (divides_d_gcd b a d Hcut1 Hcut)
413 | apply (trans_divides d (gcd b c) b)
415 | apply (divides_gcd_n)
418 | apply (trans_divides d (gcd a c) a)
420 | apply (divides_gcd_n)
424 | apply (divides_gcd_m)
425 | apply (divides_gcd_m)
428 rewrite < (eq_gcd_times_times_times_gcd b c (gcd a c)).
429 rewrite > (sym_times (gcd a c) b).
430 rewrite > (sym_times (gcd a c) c).
431 rewrite < (eq_gcd_times_times_times_gcd a c b).
432 rewrite < (eq_gcd_times_times_times_gcd a c c).
433 apply (divides_d_gcd)
434 [ apply (divides_d_gcd)
435 [ rewrite > (times_n_SO d).
436 apply (divides_times)
440 | rewrite > (times_n_SO d).
441 apply (divides_times)
446 | apply (divides_d_gcd)
447 [ rewrite > (times_n_SO d).
448 rewrite > (sym_times d (S O)).
449 apply (divides_times)
450 [ apply (divides_SO_n)
453 | rewrite < (sym_times a b).
461 theorem eq_gcd_gcd_minus: \forall a,b:nat.
462 a \lt b \to (gcd a b) = (gcd (b - a) b).
466 [ apply (divides_minus (gcd a b) b a)
467 [ apply divides_gcd_m
468 | apply divides_gcd_n
470 | apply divides_gcd_m
475 [ cut (b - (d*n2) = a)
476 [ rewrite > H4 in Hcut1.
477 rewrite < (distr_times_minus d n n2) in Hcut1.
480 | apply (witness d a (n - n2)).
484 | apply (plus_to_minus ? ? ? Hcut)
486 | rewrite > sym_plus.
487 apply (minus_to_plus)