]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/library/nat/gcd_properties1.ma
- oCic2NCic and nCic2OCic moved to ng_library
[helm.git] / helm / software / matita / library / nat / gcd_properties1.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 include "nat/gcd.ma".
16
17 (* this file contains some important properites of gcd in N *)
18
19 (* an alternative characterization for gcd *)
20 theorem gcd1: \forall a,b,c:nat.
21 c \divides a \to c \divides b \to
22 (\forall d:nat. d \divides a \to d \divides b \to d \divides c) \to (gcd a b) = c.
23 intros.
24 elim (H2 ((gcd a b)))
25 [ apply (antisymmetric_divides (gcd a b) c)
26   [ apply (witness (gcd a b) c n1).
27     assumption
28   | apply divides_d_gcd;
29       assumption
30   ]
31 | apply divides_gcd_n
32 | rewrite > sym_gcd.
33   apply divides_gcd_n
34 ]
35 qed.
36
37
38 theorem eq_gcd_times_times_times_gcd: \forall a,b,c:nat.
39 (gcd (c*a) (c*b)) = c*(gcd a b).
40 intros.
41 apply (nat_case1 c)
42 [ intros. 
43   simplify.
44   reflexivity
45 | intros.
46   rewrite < H.
47   apply gcd1
48   [ apply divides_times
49     [ apply divides_n_n
50     | apply divides_gcd_n.
51     ]
52   | apply divides_times
53     [ apply divides_n_n
54     | rewrite > sym_gcd.  
55       apply divides_gcd_n
56     ]
57   | intros.
58     apply (divides_d_times_gcd)
59     [ rewrite > H.
60       apply lt_O_S  
61     | assumption
62     | assumption
63     ]
64   ]
65 ]
66 qed.
67
68 theorem associative_nat_gcd: associative nat gcd.
69 change with (\forall a,b,c:nat. (gcd (gcd a b) c) = (gcd a (gcd b c))).
70 intros.
71 apply gcd1
72 [ apply divides_d_gcd
73   [ apply (trans_divides ? (gcd b c) ?)
74     [ apply divides_gcd_m
75     | apply divides_gcd_n
76     ]
77   | apply divides_gcd_n
78   ]
79 | apply (trans_divides ? (gcd b c) ?)
80   [ apply divides_gcd_m
81   | apply divides_gcd_m
82   ]
83 | intros.
84   cut (d \divides a \land d \divides b)
85   [ elim Hcut.
86     cut (d \divides (gcd b c))
87     [ apply (divides_d_gcd (gcd b c) a d Hcut1 H2)
88     | apply (divides_d_gcd c b d H1 H3)
89     ]
90   | split
91     [ apply (trans_divides d (gcd a b) a H).
92       apply divides_gcd_n
93     | apply (trans_divides d (gcd a b) b H).
94       apply divides_gcd_m
95     ]
96   ]
97 ]
98 qed.
99
100
101 theorem eq_gcd_div_div_div_gcd: \forall a,b,m:nat.
102 O \lt m \to m \divides a \to m \divides b \to 
103 (gcd (a/m) (b/m)) = (gcd a b) / m.
104 intros.
105 apply (inj_times_r1 m H).
106 rewrite > (sym_times m ((gcd a b)/m)).
107 rewrite > (divides_to_div m (gcd a b))
108 [ rewrite < eq_gcd_times_times_times_gcd.
109   rewrite > (sym_times m (a/m)).
110   rewrite > (sym_times m (b/m)).
111   rewrite > (divides_to_div m a H1).
112   rewrite > (divides_to_div m b H2).
113   reflexivity
114 | apply divides_d_gcd;
115     assumption
116 ]
117 qed.
118
119
120
121 theorem divides_times_to_divides_div_gcd: \forall a,b,c:nat.
122 a \divides (b*c) \to (a/(gcd a b)) \divides c.
123 intros.
124 apply (nat_case1 a)
125 [ intros.
126   apply (nat_case1 b)
127   [ (*It's an impossible situation*)
128     intros. 
129     simplify.
130     apply divides_SO_n
131   | intros.    
132     cut (c = O)
133     [ rewrite > Hcut.
134       apply (divides_n_n O)
135     | apply (lt_times_eq_O b c)
136       [ rewrite > H2.
137         apply lt_O_S
138       | apply antisymmetric_divides
139         [ apply divides_n_O
140         | rewrite < H1.
141           assumption
142         ]
143       ]
144     ]
145   ]
146 | intros.
147   rewrite < H1.
148   elim H.
149   cut (O \lt a)
150   [ cut (O \lt (gcd a b))
151     [ apply (gcd_SO_to_divides_times_to_divides (b/(gcd a b)) (a/(gcd a b)) c)
152       [ apply (O_lt_times_to_O_lt (a/(gcd a b)) (gcd a b)).
153         rewrite > (divides_to_div (gcd a b) a)
154         [ assumption      
155         | apply divides_gcd_n
156         ]
157       | rewrite < (div_n_n (gcd a b)) in \vdash (? ? ? %)
158         [ apply eq_gcd_div_div_div_gcd
159           [ assumption
160           | apply divides_gcd_n
161           | apply divides_gcd_m
162           ]
163         | assumption
164         ]
165       | apply (witness ? ? n1).
166         apply (inj_times_r1 (gcd a b) Hcut1).
167         rewrite < assoc_times.
168         rewrite < sym_times in \vdash (? ? (? % ?) ?).
169         rewrite > (divides_to_div (gcd a b) b)
170         [ rewrite < assoc_times in \vdash (? ? ? %).
171           rewrite < sym_times in \vdash (? ? ? (? % ?)).
172           rewrite > (divides_to_div (gcd a b) a)
173           [ assumption
174           | apply divides_gcd_n
175           ]
176         | apply divides_gcd_m
177         ]
178       ]
179     | rewrite > sym_gcd.
180       apply lt_O_gcd.
181       assumption    
182     ]
183   | rewrite > H1.
184     apply lt_O_S
185   ]    
186 ]
187 qed.
188
189 theorem gcd_plus_times_gcd: \forall a,b,d,m:nat. 
190 (gcd (a+m*b) b) = (gcd a b).
191 intros.
192 apply gcd1
193 [ apply divides_plus
194   [ apply divides_gcd_n
195   | apply (trans_divides ? b ?)
196     [ apply divides_gcd_m
197     | rewrite > sym_times.
198       apply (witness b (b*m) m).
199       reflexivity
200     ]
201   ]
202 | apply divides_gcd_m
203 | intros.
204   apply divides_d_gcd
205   [ assumption
206   | rewrite > (minus_plus_m_m a (m*b)). 
207     apply divides_minus
208     [ assumption
209     | apply (trans_divides ? b ?)
210       [ assumption
211       | rewrite > sym_times.
212         apply (witness b (b*m) m).
213         reflexivity
214       ] 
215     ]
216   ]
217 ]
218 qed.
219
220
221
222 theorem gcd_SO_to_divides_to_divides_to_divides_times: \forall c,e,f:nat.
223 (gcd e f) = (S O)  \to e \divides c \to f \divides c \to 
224 (e*f) \divides c.
225 intros.
226 apply (nat_case1 c); intros
227 [ apply divides_n_O 
228 | rewrite < H3.
229   elim H1.
230   elim H2.
231   rewrite > H5.
232   rewrite > (sym_times e f).
233   apply (divides_times)
234   [ apply (divides_n_n)
235   | rewrite > H5 in H1.
236     apply (gcd_SO_to_divides_times_to_divides f e n)
237     [ rewrite < H5 in H1.
238       rewrite > H3 in H1.
239       apply (divides_to_lt_O e (S m))
240       [ apply lt_O_S
241       | assumption
242       ]
243     | assumption
244     | assumption
245     ]
246   ]
247 ]
248 qed.
249 (* the following theorem shows that gcd is a multiplicative function in 
250    the following sense: if a1 and a2 are relatively prime, then 
251    gcd(a1·a2, b) = gcd(a1, b)·gcd(a2, b). 
252  *)
253 theorem gcd_SO_to_eq_gcd_times_times_gcd_gcd: \forall a,b,c:nat.
254 (gcd a b) = (S O) \to (gcd (a*b) c) = (gcd a c) * (gcd b c).
255 intros.
256 apply gcd1
257 [ apply divides_times; 
258     apply divides_gcd_n
259 | apply (gcd_SO_to_divides_to_divides_to_divides_times c (gcd a c) (gcd b c))
260   [ apply gcd1
261     [ apply divides_SO_n  
262     | apply divides_SO_n
263     | intros.
264       cut (d \divides a)
265       [ cut (d \divides b)
266         [ rewrite < H.
267           apply (divides_d_gcd b a d Hcut1 Hcut)
268         | apply (trans_divides d (gcd b c) b)
269           [ assumption
270           | apply (divides_gcd_n)
271           ]
272         ]
273       | apply (trans_divides d (gcd a c) a)
274         [ assumption
275         | apply (divides_gcd_n)
276         ]
277       ]
278     ]
279   | apply (divides_gcd_m)
280   | apply (divides_gcd_m)      
281   ]
282 | intros.
283   rewrite < (eq_gcd_times_times_times_gcd b c (gcd a c)).
284   rewrite > (sym_times (gcd a c) b).
285   rewrite > (sym_times (gcd a c) c).
286   rewrite < (eq_gcd_times_times_times_gcd a c b).
287   rewrite < (eq_gcd_times_times_times_gcd a c c).
288   apply (divides_d_gcd)
289   [ apply (divides_d_gcd)
290     [ rewrite > (times_n_SO d).
291       apply (divides_times)
292       [ assumption
293       | apply divides_SO_n
294       ]
295     | rewrite > (times_n_SO d).
296       apply (divides_times)
297       [ assumption
298       | apply divides_SO_n
299       ]
300     ]
301   | apply (divides_d_gcd)
302     [ rewrite > (times_n_SO d).
303       rewrite > (sym_times d (S O)).
304       apply (divides_times)
305       [ apply (divides_SO_n)
306       | assumption
307       ]
308     | rewrite < (sym_times a b).
309       assumption
310     ]
311   ]
312 ]
313 qed.
314   
315   
316 theorem eq_gcd_gcd_minus: \forall a,b:nat.
317 a \lt b \to (gcd a b) = (gcd (b - a) b).
318 intros.
319 apply sym_eq.
320 apply gcd1
321 [ apply (divides_minus (gcd a b) b a)
322   [ apply divides_gcd_m
323   | apply divides_gcd_n
324   ]
325 | apply divides_gcd_m
326 | intros.
327   elim H1.
328   elim H2.
329   cut(b = (d*n1) + a) 
330   [ cut (b - (d*n1) = a)
331     [ rewrite > H4 in Hcut1.
332       rewrite < (distr_times_minus d n n1) in Hcut1.
333       apply divides_d_gcd
334       [ assumption
335       | apply (witness d a (n - n1)).
336         apply sym_eq.
337         assumption
338       ]
339     | apply (plus_to_minus ? ? ? Hcut)      
340     ]
341   | rewrite > sym_plus.
342     apply (minus_to_plus)
343     [ apply lt_to_le.
344       assumption
345     | assumption
346     ]
347   ]
348 ]
349 qed.
350