]> matita.cs.unibo.it Git - helm.git/blob - weblib/arithmetics/gcd.ma
- transitivity of parallel telescopic substitution closed!
[helm.git] / weblib / arithmetics / gcd.ma
1 (*
2     ||M||  This file is part of HELM, an Hypertextual, Electronic        
3     ||A||  Library of Mathematics, developed at the Computer Science     
4     ||T||  Department of the University of Bologna, Italy.                     
5     ||I||                                                                 
6     ||T||  
7     ||A||  This file is distributed under the terms of the 
8     \   /  GNU General Public License Version 2        
9      \ /      
10       V_______________________________________________________________ *)
11
12 include "arithmetics/primes.ma".
13   
14 let rec gcd_aux p m n: nat ≝
15 match p with 
16   [O ⇒ m
17   |S q ⇒ 
18     match dividesb n m with
19     [ true ⇒ n
20     | false ⇒ gcd_aux q n (m \mod n)]].
21     
22 definition gcd : nat → nat → nat ≝ λn,m:nat.
23   match leb n m with
24   [ true ⇒ gcd_aux n m n 
25   | false ⇒ gcd_aux m n m ].
26   
27 theorem commutative_gcd: ∀n,m. gcd n m = gcd m n.
28 #n #m normalize @leb_elim 
29   [#lenm cases(le_to_or_lt_eq … lenm)
30     [#ltnm >not_le_to_leb_false // @lt_to_not_le //
31     |#eqnm >eqnm (cases (leb m m)) //
32     ]
33   |#notlenm >le_to_leb_true // @(transitive_le ? (S m)) //
34    @not_le_to_lt //
35   ]
36 qed.
37
38 theorem gcd_O_l: ∀m. gcd O m = m. 
39 // qed.  
40   
41 theorem divides_mod: ∀p,m,n:nat. O < n → 
42   p ∣ m → p ∣ n → p ∣ (m \mod n).
43 #p #m #n #posn * #qm #eqm * #qn #eqn
44 @(quotient ?? (qm - qn*(m / n))) >distributive_times_minus
45 <eqm <associative_times <eqn @sym_eq @plus_to_minus /2/
46 qed.
47
48 theorem divides_mod_to_divides: ∀p,m,n:nat. O < n →
49   p ∣ (m \mod n) → p ∣ n → p ∣ m.
50 #p #m #n #posn * #q1 #eq1 * #q2 #eq2
51 @(quotient p m ((q2*(m / n))+q1)) >distributive_times_plus
52 <eq1 <associative_times <eq2 /2/
53 qed.
54
55 lemma divides_to_gcd_aux: ∀p,m,n. O < p → O < n →n ∣ m → 
56   gcd_aux p m n = n.
57 #p #m #n #posp @(lt_O_n_elim … posp) #l #posn #divnm normalize 
58 >divides_to_dividesb_true normalize //
59 qed.
60
61 theorem divides_to_gcd: ∀m,n. O < n → n ∣ m → 
62   gcd n m = n.
63 #m #n #posn (cases m)
64  [>commutative_gcd //
65  |#l #divn (cut (n ≤ (S l))) [@divides_to_le //] #len normalize
66   >le_to_leb_true // normalize @divides_to_gcd_aux //
67  ]
68 qed.
69
70 lemma not_divides_to_gcd_aux: ∀p,m,n. 0 < n → n ∤ m → 
71   gcd_aux (S p) m n = gcd_aux p n (m \mod n).
72 #p #m #n #lenm #divnm normalize >not_divides_to_dividesb_false
73 normalize // qed.
74
75 theorem divides_gcd_aux_mn: ∀p,m,n. O < n → n ≤ m → n ≤ p →
76   gcd_aux p m n ∣ m ∧ gcd_aux p m n ∣ n. 
77 #p (elim p)
78   [#m #n #posn #lenm #lenO @False_ind @(absurd … posn) /2/
79   |#q #Hind #m #n #posn #lenm #lenS cases(decidable_divides n m)
80     [#divnm >(divides_to_gcd_aux … posn divnm) // % //
81     |#ndivnm >(not_divides_to_gcd_aux … posn ndivnm)
82      cut (gcd_aux q n (m \mod n) ∣ n ∧
83           gcd_aux q n (m \mod n) ∣ mod m n)
84       [cut (m \mod n < n) [@lt_mod_m_m //] #ltmod
85        @Hind
86         [cases(le_to_or_lt_eq … (le_O_n (m \mod n))) // #modO
87          @False_ind @(absurd ?? ndivnm) @mod_O_to_divides //
88         |/2/
89         |@le_S_S_to_le @(transitive_le … ltmod lenS)
90         ]
91       |* #H #H1 % [@(divides_mod_to_divides … posn H1) // |//]
92       ]
93     ]
94   ]
95 qed.
96
97 theorem divides_gcd_nm: ∀n,m.
98   gcd n m ∣ m ∧ gcd n m ∣ n.
99 #n #m cases(le_to_or_lt_eq …(le_O_n n)) [|#eqnO <eqnO /2/]
100 #posn cases(le_to_or_lt_eq …(le_O_n m)) [|#eqmO <eqmO /2/]
101 #posm normalize @leb_elim normalize  
102   [#lenm @divides_gcd_aux_mn //
103   |#notlt normalize cut (∀A,B. A∧B → B∧A) [#A #B * /2/] #sym_and
104    @sym_and @divides_gcd_aux_mn // @(transitive_le ? (S m)) //
105    @not_le_to_lt //
106   ]
107 qed. 
108
109 theorem divides_gcd_l: ∀n,m. gcd n m ∣ n.
110 #n #m @(proj2  ? ? (divides_gcd_nm n m)).
111 qed.
112
113 theorem divides_gcd_r: \forall n,m. gcd n m ∣ m.
114 #n #m @(proj1 ? ? (divides_gcd_nm n m)).
115 qed.
116
117 theorem divides_times_gcd_aux: ∀p,m,n,d,c. 
118   O < c → O < n → n ≤ m → n ≤ p →
119     d ∣ (c*m) → d ∣ (c*n) → d ∣ c*gcd_aux p m n. 
120 #p (elim p) 
121   [#m #n #d #c #_ #posn #_ #lenO @False_ind @(absurd … lenO) /2/
122   |#q #Hind #m #n #d #c #posc #posn #lenm #lenS #dcm #dcn
123    cases(decidable_divides n m)
124     [#divnm >(divides_to_gcd_aux … posn divnm) //
125     |#ndivnm >(not_divides_to_gcd_aux … posn ndivnm)
126      cut (m \mod n < n) [@lt_mod_m_m //] #ltmod
127      @Hind //
128       [cases(le_to_or_lt_eq … (le_O_n (m \mod n))) // #modO
129        @False_ind @(absurd ?? ndivnm) @mod_O_to_divides //
130       |/2/
131       |@le_S_S_to_le @(transitive_le … ltmod lenS)
132       |<times_mod // < (commutative_times c m)
133        <(commutative_times c n) @divides_mod //
134        >(times_n_O 0) @lt_times //
135       ]
136     ]
137   ]
138 qed. 
139
140 (*a particular case of the previous theorem, with c=1 *)
141 theorem divides_gcd_aux: ∀p,m,n,d. O < n → n ≤ m → n ≤ p →
142   d ∣ m \to d ∣ n \to d ∣ gcd_aux p m n.
143   (* bell'esempio di smart application *)
144 /2/ qed. 
145
146 theorem divides_d_times_gcd: ∀m,n,d,c. O < c → 
147   d ∣ (c*m) → d ∣ (c*n) → d ∣ c*gcd n m. 
148 #m #n #d #c #posc #dcm #dcn 
149 cases(le_to_or_lt_eq …(le_O_n n)) [|#eqnO <eqnO @dcm] #posn 
150 cases(le_to_or_lt_eq …(le_O_n m)) [|#eqmO <eqmO <commutative_gcd @dcn] #posm
151 normalize @leb_elim normalize
152   [#lenm @divides_times_gcd_aux //
153   |#nlenm @divides_times_gcd_aux //
154    @(transitive_le ? (S m)) // @not_le_to_lt //
155   ]
156 qed.
157
158 (* a particular case of the previous theorem, with c=1 *)
159 theorem divides_d_gcd: ∀m,n,d. 
160  d ∣ m → d ∣ n → d ∣ gcd n m.
161 #m #n #d #divdn #divdn applyS (divides_d_times_gcd m n d 1) //
162 qed.
163
164 theorem eq_minus_gcd_aux: ∀p,m,n.O < n → n ≤ m →  n ≤ p →
165   ∃a,b. a*n - b*m = gcd_aux p m n ∨ b*m - a*n = gcd_aux p m n.
166 #p (elim p)
167   [#m #n #posn #lenm #lenO @False_ind @(absurd … posn) /2/
168   |#q #Hind #m #n #posn #lenm #lenS 
169    cut (0 < m) [@lt_to_le_to_lt //] #posm 
170    cases(decidable_divides n m)
171     [#divnm >(divides_to_gcd_aux … posn divnm) // 
172      @(ex_intro ?? 1) @(ex_intro ?? 0) %1 //
173     |#ndivnm >(not_divides_to_gcd_aux … posn ndivnm)
174      cut (m \mod n < n) [@lt_mod_m_m //] #ltmod
175      lapply (Hind n (m \mod n) ???)
176       [@le_S_S_to_le @(transitive_le … ltmod lenS)
177       |/2/
178       |cases(le_to_or_lt_eq … (le_O_n (m \mod n))) // #modO
179        @False_ind @(absurd ?? ndivnm) @mod_O_to_divides //
180       ]
181      * #a * #b * #H
182       [(* first case *)
183        <H @(ex_intro ?? (b+a*(m / n))) @(ex_intro ?? a) %2
184        <commutative_plus >distributive_times_plus_r 
185        >(div_mod m n) in ⊢(? ? (? % ?) ?)
186        >associative_times <commutative_plus >distributive_times_plus
187        <minus_plus <commutative_plus <plus_minus //
188       |(* second case *)
189         <H @(ex_intro ?? (b+a*(m / n))) @(ex_intro ?? a) %1
190         >distributive_times_plus_r
191         >(div_mod m n) in ⊢ (? ? (? ? %) ?)
192         >distributive_times_plus >associative_times
193         <minus_plus <commutative_plus <plus_minus //
194       ]
195     ]
196   ]
197 qed.
198
199 theorem eq_minus_gcd:
200   ∀m,n.∃ a,b.a*n - b*m = gcd n m ∨ b*m - a*n = gcd n m.
201   #m #n cases(le_to_or_lt_eq …(le_O_n n)) 
202   [|#eqn0 >eqn0 @(ex_intro ?? O) @(ex_intro ? ? 1) %2 applyS minus_n_O]
203 #posn cases(le_to_or_lt_eq …(le_O_n m)) 
204   [|#eqm0 >eqm0 @(ex_intro ?? 1) @(ex_intro ? ? 0) %1 applyS minus_n_O]
205 #posm normalize @leb_elim normalize
206   [#lenm @eq_minus_gcd_aux //
207   |#nlenm lapply(eq_minus_gcd_aux m n m posm ? (le_n m))
208     [@(transitive_le … (not_le_to_lt … nlenm)) //]
209    * #a * #b * #H @(ex_intro ?? b) @(ex_intro ?? a) [%2 // |%1 //]
210   ]
211 qed.
212
213 (* some properties of gcd *)
214
215 theorem gcd_O_to_eq_O:∀m,n:nat. 
216   gcd m n = O → m = O ∧ n = O.
217 #m #n #H cut (O ∣ n ∧ O ∣ m)
218   [<H @divides_gcd_nm| * * #q1 #H1 * #q2 #H2 % // ]
219 qed.
220
221 theorem lt_O_gcd:∀m,n:nat. O < n → O < gcd m n.
222 #m #n #posn @(nat_case (gcd m n)) // 
223 #H (cases (gcd_O_to_eq_O m n H)) //
224 qed.
225
226 theorem gcd_n_n: ∀n.gcd n n = n.
227 #n (cases n) //
228 #m @le_to_le_to_eq
229   [@divides_to_le //
230   |@divides_to_le (*/2/*) [@lt_O_gcd // |@divides_d_gcd // ]
231   ]
232 qed.
233
234 (* some properties or relative primes - i.e. gcd = 1 *)
235 theorem gcd_1_to_lt_O: ∀i,n. 1 < n → gcd i n = 1 → O < i.
236 #i #n #lt1n #gcd1 cases (le_to_or_lt_eq ?? (le_O_n i)) //
237 #iO @False_ind @(absurd … gcd1) <iO normalize
238 @sym_not_eq @lt_to_not_eq //
239 qed.
240
241 theorem gcd_1_to_lt_n: ∀i,n. 1 < n → 
242   i ≤ n → gcd i n = 1 → i < n.
243 #i #n #lt1n #lein #gcd1 cases (le_to_or_lt_eq ?? lein) //
244 (* impressive *)
245 qed.
246
247 theorem  gcd_n_times_nm: ∀n,m. O < m → gcd n (n*m) = n.
248 #n #m #posm @(nat_case n) //
249 #l #eqn @le_to_le_to_eq
250   [@divides_to_le //
251   |@divides_to_le
252     [@lt_O_gcd >(times_n_O O) @lt_times // |@divides_d_gcd /2/]
253   ]
254 qed.
255
256 theorem le_gcd_times: ∀m,n,p. O< p → gcd m n ≤ gcd m (n*p).
257 #m #n #p #posp @(nat_case n) // 
258 #l #eqn @divides_to_le [@lt_O_gcd >(times_n_O O) @lt_times //] 
259 @divides_d_gcd [@(transitive_divides ? (S l)) /2/ |//]
260 qed.
261
262 theorem gcd_times_SO_to_gcd_SO: ∀m,n,p:nat. O < n → O < p → 
263   gcd m (n*p) = 1 → gcd m n = 1.
264 #m #n #p #posn #posp #gcd1 @le_to_le_to_eq
265   [<gcd1 @le_gcd_times // | @lt_O_gcd //]
266 qed.
267
268 (* for the "converse" of the previous result see the end  of this development *)
269
270 theorem eq_gcd_SO_to_not_divides: ∀n,m. 1 < n → 
271   gcd n m = 1 → n ∤ m.
272 #n #m #lt1n #gcd1 @(not_to_not … (gcd n m = n))
273   [#divnm @divides_to_gcd /2/ | /2/]
274 qed.
275
276 theorem gcd_SO_n: ∀n:nat. gcd 1 n = 1.
277 #n @le_to_le_to_eq
278   [@divides_to_le // |>commutative_gcd @lt_O_gcd //]
279 qed.
280
281 theorem divides_gcd_mod: ∀m,n:nat. O < n →
282   gcd m n ∣ gcd n (m \mod n).
283 #m #n #posn @divides_d_gcd [@divides_mod // | //]
284 qed.
285
286 theorem divides_mod_gcd: ∀m,n:nat. O < n →
287   gcd n (m \mod n) ∣ gcd m n.
288 #m #n #posn @divides_d_gcd
289   [@divides_gcd_l |@(divides_mod_to_divides ?? n) //]
290 qed.
291
292 theorem gcd_mod: ∀m,n:nat. O < n →
293   gcd n (m \mod n) = gcd m n.
294 #m #n #posn @antisymmetric_divides
295   [@divides_mod_gcd // | @divides_gcd_mod //]
296 qed.
297
298 (* gcd and primes *)
299
300 theorem prime_to_gcd_1: ∀n,m:nat. prime n → n ∤ m →
301   gcd n m = 1.
302 (* bella dimostrazione *)
303 #n #m * #lt1n #primen #ndivnm @le_to_le_to_eq
304   [@not_lt_to_le @(not_to_not … (primen (gcd n m) (divides_gcd_l …)))
305    @(not_to_not ? (n ∣m)) //
306   |@lt_O_gcd @not_eq_to_le_to_lt // @(not_to_not ? (n ∣ m)) //
307   ]
308 qed.
309
310 (* primes and divides *)
311 theorem divides_times_to_divides: ∀p,n,m:nat.prime p → 
312   p ∣ n*m → p ∣ n ∨ p ∣ m.
313 #p #n #m #primp * #c #nm
314 cases (decidable_divides p n) /2/ #ndivpn %2 
315 cut (∃a,b. a*n - b*p = 1 ∨ b*p - a*n = 1)
316   [<(prime_to_gcd_1 … primp ndivpn) >commutative_gcd @eq_minus_gcd]
317 * #a * #b * #H
318   [@(quotient ?? (a*c-b*m)) >distributive_times_minus <associative_times 
319    >(commutative_times p) >associative_times <nm <associative_times
320    <associative_times <commutative_times >(commutative_times (p*b))
321    <distributive_times_minus //
322   |@(quotient ?? (b*m -a*c)) >distributive_times_minus <(associative_times p)
323    <(associative_times p) <(commutative_times a) >(associative_times a)
324    <nm <(associative_times a) <commutative_times >(commutative_times (a*n))
325    <distributive_times_minus //
326   ]
327 qed.
328
329 theorem divides_exp_to_divides: 
330 ∀p,n,m:nat. prime p → p ∣n^m → p ∣ n.
331 #p #n #m #primep (elim m) normalize /2/
332 #l #Hind #H cases(divides_times_to_divides  … primep H) /2/
333 qed.
334
335 theorem divides_exp_to_eq: 
336 ∀p,q,m:nat. prime p → prime q →
337   p ∣ q^m → p = q.
338 #p #q #m #H * #lt1q #primeq #H @primeq /2/
339 qed.
340
341 (* relative primes *)
342 theorem eq_gcd_times_1: ∀p,n,m:nat. O < n → O < m →
343  gcd p n = 1 → gcd p m = 1 → gcd p (n*m) = 1.
344 #p #n #m #posn #posm #primepn #primepm 
345 @le_to_le_to_eq [|@lt_O_gcd >(times_n_O 0) @lt_times //]
346 @not_lt_to_le % #lt1gcd
347 cut (smallest_factor (gcd p (n*m)) ∣ n ∨ 
348      smallest_factor (gcd p (n*m)) ∣ m)
349   [@divides_times_to_divides
350     [@prime_smallest_factor_n //
351     |@(transitive_divides ? (gcd p (n*m))) // 
352      @divides_smallest_factor_n /2/
353     ]
354   |* #H
355     [@(absurd ?? (lt_to_not_le …(lt_SO_smallest_factor … lt1gcd)))
356      <primepn @divides_to_le // @divides_d_gcd //
357      @(transitive_divides … (divides_smallest_factor_n …))
358        [@lt_O_gcd >(times_n_O 0) @lt_times // | //]
359     |@(absurd ?? (lt_to_not_le … (lt_SO_smallest_factor …lt1gcd)))
360      <primepm @divides_to_le // @divides_d_gcd //
361      @(transitive_divides … (divides_smallest_factor_n …))
362        [@lt_O_gcd >(times_n_O 0) @lt_times // | //]
363   ]
364 qed.
365
366
367 theorem gcd_1_to_divides_times_to_divides: ∀p,n,m:nat. O < p →
368 gcd p n = 1 → p ∣ (n*m) → p ∣ m.
369 #p #m #n #posn #gcd1 * #c #nm
370 cases(eq_minus_gcd m p) #a * #b * #H >gcd1 in H #H 
371   [@(quotient ?? (a*n-c*b)) >distributive_times_minus <associative_times 
372    <associative_times <nm >(commutative_times m) >commutative_times
373    >associative_times <distributive_times_minus //
374   |@(quotient ?? (c*b-a*n)) >distributive_times_minus <associative_times 
375    <associative_times <nm >(commutative_times m) <(commutative_times n)
376    >associative_times <distributive_times_minus //
377   ]
378 qed.
379
380 (*
381 theorem divides_to_divides_times1: \forall p,q,n. prime p \to prime q \to p \neq q \to
382 divides p n \to divides q n \to divides (p*q) n.
383 intros.elim H3.
384 rewrite > H5 in H4.
385 elim (divides_times_to_divides ? ? ? H1 H4)
386   [elim H.apply False_ind.
387    apply H2.apply sym_eq.apply H8
388     [assumption
389     |apply prime_to_lt_SO.assumption
390     ]
391   |elim H6.
392    apply (witness ? ? n1).
393    rewrite > assoc_times.
394    rewrite < H7.assumption
395   ]
396 qed.
397 *)
398
399 theorem divides_to_divides_times: ∀p,q,n. prime p  → p ∤ q →
400  p ∣ n → q ∣ n → p*q ∣ n.
401 #p #q #n #primep #notdivpq #divpn * #b #eqn (>eqn in divpn)
402 #divpn cases(divides_times_to_divides ??? primep divpn) #H
403   [@False_ind /2/ 
404   |cases H #c #eqb @(quotient ?? c) >eqb <associative_times //
405   ]
406 qed.