gcdScript.sml
1(* ------------------------------------------------------------------------- *)
2(* Elementary Number Theory - a collection of useful results for numbers *)
3(* (gcd = greatest common divisor) *)
4(* *)
5(* Author: (Joseph) Hing-Lun Chan (Australian National University, 2019) *)
6(* ------------------------------------------------------------------------- *)
7Theory gcd[bare]
8Ancestors
9 prim_rec arithmetic divides
10Libs
11 HolKernel Parse boolLib BasicProvers simpLib boolSimps
12 Induction TotalDefn numSimps metisLib
13
14
15val arith_ss = srw_ss() ++ ARITH_ss;
16val std_ss = arith_ss;
17val ARW = RW_TAC arith_ss
18
19val DECIDE = Drule.EQT_ELIM o Arith.ARITH_CONV;
20
21fun DECIDE_TAC (g as (asl,_)) =
22 ((MAP_EVERY UNDISCH_TAC (filter is_arith asl) THEN
23 CONV_TAC Arith.ARITH_CONV)
24 ORELSE tautLib.TAUT_TAC) g;
25
26val decide_tac = DECIDE_TAC;
27val metis_tac = METIS_TAC;
28val rw = SRW_TAC [ARITH_ss];
29val qabbrev_tac = Q.ABBREV_TAC;
30fun simp l = ASM_SIMP_TAC (srw_ss() ++ ARITH_ss) l;
31fun fs l = FULL_SIMP_TAC (srw_ss() ++ ARITH_ss) l;
32
33Definition is_gcd_def[nocompute]:
34 is_gcd a b c <=> divides c a /\ divides c b /\
35 !d. divides d a /\ divides d b ==> divides d c
36End
37
38val IS_GCD = is_gcd_def;
39
40Theorem IS_GCD_UNIQUE:
41 !a b c d. is_gcd a b c /\ is_gcd a b d ==> (c = d)
42Proof
43 PROVE_TAC[IS_GCD,DIVIDES_ANTISYM]
44QED
45
46Theorem IS_GCD_REF:
47 !a. is_gcd a a a
48Proof
49 PROVE_TAC[IS_GCD,DIVIDES_REFL]
50QED
51
52Theorem IS_GCD_SYM:
53 !a b c. (is_gcd a b c) = is_gcd b a c
54Proof
55 PROVE_TAC[IS_GCD]
56QED
57
58Theorem IS_GCD_0R:
59 !a. is_gcd a 0 a
60Proof
61 PROVE_TAC[IS_GCD,DIVIDES_REFL,ALL_DIVIDES_0]
62QED
63
64Theorem IS_GCD_0L:
65 !a. is_gcd 0 a a
66Proof
67 PROVE_TAC[IS_GCD,DIVIDES_REFL,ALL_DIVIDES_0]
68QED
69
70Theorem PRIME_IS_GCD:
71 !p b. prime p ==> divides p b \/ is_gcd p b 1
72Proof
73 ARW[] THEN Cases_on `divides p b` THEN ARW[]
74 THEN ARW[IS_GCD,ONE_DIVIDES_ALL]
75 THEN Cases_on `d=1` THEN ARW[ONE_DIVIDES_ALL]
76 THEN PROVE_TAC[prime_def]
77QED
78
79Theorem IS_GCD_MINUS_L:
80 !a b c. b <= a /\ is_gcd (a-b) b c ==> is_gcd a b c
81Proof
82 ARW[IS_GCD] THENL [
83 PROVE_TAC[SUB_ADD,DIVIDES_ADD_1],
84 PROVE_TAC[SUB_ADD,DIVIDES_ADD_2,ADD_SYM]
85 ]
86QED
87
88Theorem IS_GCD_MINUS_R:
89 !a b c. a <= b /\ is_gcd a (b-a) c ==> is_gcd a b c
90Proof
91 PROVE_TAC[IS_GCD_MINUS_L,IS_GCD_SYM]
92QED
93
94Definition gcd_def:
95 (gcd 0 y = y)
96 /\ (gcd (SUC x) 0 = SUC x)
97 /\ (gcd (SUC x) (SUC y) = if y <= x then gcd (x-y) (SUC y)
98 else gcd (SUC x) (y-x))
99End
100
101val gcd_ind = GEN_ALL (DB.fetch "-" "gcd_ind");
102
103Overload coprime = “\x y. gcd x y = 1” (* from examples/algebra *)
104
105Theorem GCD_IS_GCD:
106 !a b. is_gcd a b (gcd a b)
107Proof
108 recInduct gcd_ind THEN ARW [gcd_def] THEN
109 PROVE_TAC [IS_GCD_0L,IS_GCD_0R,IS_GCD_MINUS_L,
110 IS_GCD_MINUS_R, DECIDE(Term`~(y<=x) ==> SUC x <= SUC y`),
111 LESS_EQ_MONO,SUB_MONO_EQ]
112QED
113
114val GCD_THM = REWRITE_RULE [GCD_IS_GCD] (Q.SPECL [`m`,`n`,`gcd m n`] IS_GCD);
115
116Theorem GCD_IS_GREATEST_COMMON_DIVISOR =
117 REWRITE_RULE [IS_GCD] GCD_IS_GCD
118
119
120Theorem GCD_REF[simp]:
121 !a. gcd a a = a
122Proof
123 PROVE_TAC[GCD_IS_GCD,IS_GCD_UNIQUE,IS_GCD_REF]
124QED
125
126Theorem GCD_SYM:
127 !a b. gcd a b = gcd b a
128Proof
129 PROVE_TAC[GCD_IS_GCD,IS_GCD_UNIQUE,IS_GCD_SYM]
130QED
131
132(* |- gcd a b = gcd b a *)
133Theorem GCD_COMM = GCD_SYM |> SPEC_ALL;
134
135Theorem GCD_0R[simp]:
136 !a. gcd a 0 = a
137Proof
138 PROVE_TAC[GCD_IS_GCD,IS_GCD_UNIQUE,IS_GCD_0R]
139QED
140
141Theorem GCD_0L[simp]:
142 !a. gcd 0 a = a
143Proof
144 PROVE_TAC[GCD_IS_GCD,IS_GCD_UNIQUE,IS_GCD_0L]
145QED
146
147(* Theorem: (gcd 0 x = x) /\ (gcd x 0 = x) *)
148(* Proof: by GCD_0L, GCD_0R *)
149Theorem GCD_0:
150 !x. (gcd 0 x = x) /\ (gcd x 0 = x)
151Proof
152 rw_tac std_ss[GCD_0L, GCD_0R]
153QED
154
155Theorem GCD_ADD_R:
156 !a b. gcd a (a+b) = gcd a b
157Proof
158 ARW[] THEN MATCH_MP_TAC (SPECL[Term `a:num`, Term `a+b`] IS_GCD_UNIQUE)
159 THEN ARW[GCD_IS_GCD,SPECL [Term `a:num`, Term `a+b`] IS_GCD_MINUS_R]
160QED
161
162Theorem GCD_ADD_R_THM[simp] =
163 CONJ GCD_ADD_R (ONCE_REWRITE_RULE [ADD_COMM] GCD_ADD_R)
164
165Theorem GCD_ADD_L:
166 !a b. gcd (a+b) a = gcd a b
167Proof
168 PROVE_TAC[GCD_SYM,GCD_ADD_R]
169QED
170
171Theorem GCD_ADD_L_THM[simp] =
172 CONJ GCD_ADD_L (ONCE_REWRITE_RULE [ADD_COMM] GCD_ADD_L)
173
174Theorem GCD_EQ_0[simp]:
175 !n m. (gcd n m = 0) <=> (n = 0) /\ (m = 0)
176Proof HO_MATCH_MP_TAC gcd_ind THEN SRW_TAC [][gcd_def]
177QED
178
179Theorem GCD_1[simp]:
180 (gcd 1 x = 1) /\ (gcd x 1 = 1)
181Proof
182 Q_TAC SUFF_TAC `!m n. (m = 1) ==> (gcd m n = 1)`
183 THEN1 PROVE_TAC [GCD_SYM] THEN
184 HO_MATCH_MP_TAC gcd_ind THEN SRW_TAC [][gcd_def]
185QED
186
187Theorem PRIME_GCD:
188 !p b. prime p ==> divides p b \/ (gcd p b = 1)
189Proof
190 PROVE_TAC[PRIME_IS_GCD,GCD_IS_GCD,IS_GCD_UNIQUE]
191QED
192
193Theorem EUCLIDES_AUX[local]:
194 !a b c d. divides c (d*a) /\ divides c (d*b)
195 ==>
196 divides c (d*gcd a b)
197Proof
198recInduct gcd_ind THEN SRW_TAC [][gcd_def]
199 THEN FIRST_X_ASSUM MATCH_MP_TAC
200 THENL [`?z. x = y+z` by (Q.EXISTS_TAC `x-y` THEN DECIDE_TAC),
201 `?z. y = x+z` by (Q.EXISTS_TAC `y-x` THEN DECIDE_TAC)]
202 THEN RW_TAC bool_ss [DECIDE (Term`(x + y) - x = y`)]
203 THEN FULL_SIMP_TAC (srw_ss()) [MULT_CLAUSES, LEFT_ADD_DISTRIB]
204 THEN PROVE_TAC [DIVIDES_ADD_2,ADD_ASSOC]
205QED
206
207
208Theorem L_EUCLIDES:
209 !a b c. (gcd a b = 1) /\ divides b (a*c) ==> divides b c
210Proof
211 ARW[]
212 THEN `c = c * gcd a b` by ARW[MULT_CLAUSES]
213 THEN ONCE_ASM_REWRITE_TAC[]
214 THEN PROVE_TAC[EUCLIDES_AUX,DIVIDES_MULT,MULT_SYM,DIVIDES_REFL]
215QED
216
217Theorem divides_coprime_mul:
218 !n m k. gcd n m = 1 ==> (divides n (m * k) <=> divides n k)
219Proof
220 srw_tac[][] >> eq_tac >> srw_tac[][]
221 >- (full_simp_tac bool_ss [Once GCD_SYM] >> drule L_EUCLIDES >> srw_tac[][])
222 >- (drule dividesTheory.DIVIDES_MULT >> simp_tac bool_ss [Once MULT_COMM])
223QED
224
225Theorem P_EUCLIDES:
226 !p a b. prime p /\ divides p (a*b)
227 ==>
228 divides p a \/ divides p b
229Proof
230 ARW[] THEN Cases_on `divides p a` THEN ARW[] THEN
231 `gcd p a = 1` by PROVE_TAC[GCD_IS_GCD,IS_GCD_UNIQUE,PRIME_GCD] THEN
232 PROVE_TAC[L_EUCLIDES,GCD_SYM]
233QED
234
235Theorem FACTOR_OUT_GCD:
236 !n m. ~(n = 0) /\ ~(m = 0) ==>
237 ?p q. (n = p * gcd n m) /\ (m = q * gcd n m) /\
238 (gcd p q = 1)
239Proof
240 REPEAT STRIP_TAC THEN
241 `divides (gcd n m) n` by PROVE_TAC [GCD_THM] THEN
242 `divides (gcd n m) m` by PROVE_TAC [GCD_THM] THEN
243 `?k. k * gcd n m = n` by PROVE_TAC [divides_def] THEN
244 `?j. j * gcd n m = m` by PROVE_TAC [divides_def] THEN
245 MAP_EVERY Q.EXISTS_TAC [`k`, `j`] THEN
246 ASM_REWRITE_TAC [] THEN
247 SPOSE_NOT_THEN ASSUME_TAC THEN
248 `divides (gcd k j) k` by PROVE_TAC [GCD_THM] THEN
249 `divides (gcd k j) j` by PROVE_TAC [GCD_THM] THEN
250 `?u. u * gcd k j = k` by PROVE_TAC [divides_def] THEN
251 `?v. v * gcd k j = j` by PROVE_TAC [divides_def] THEN
252 `divides (gcd k j * gcd n m) n` by
253 PROVE_TAC [MULT_ASSOC, divides_def] THEN
254 `divides (gcd k j * gcd n m) m` by
255 PROVE_TAC [MULT_ASSOC, divides_def] THEN
256 `divides (gcd k j * gcd n m) (gcd n m)`
257 by PROVE_TAC [GCD_IS_GCD, IS_GCD] THEN
258 `gcd n m = 0` by PROVE_TAC [DIVIDES_MULT_LEFT] THEN
259 FULL_SIMP_TAC bool_ss [GCD_EQ_0]
260QED
261
262val lexnum_induct =
263 (SIMP_RULE (srw_ss()) [pairTheory.FORALL_PROD, pairTheory.LEX_DEF] o
264 Q.SPEC `UNCURRY P` o
265 SIMP_RULE bool_ss [pairTheory.WF_LEX, prim_recTheory.WF_LESS] o
266 ISPEC ``(<) LEX (<)``) relationTheory.WF_INDUCTION_THM
267
268(* an induction principle for GCD like situations without any SUCs and without
269 any subtractions *)
270Theorem GCD_SUCfree_ind:
271 !P. (!y. P 0 y) /\ (!x y. P x y ==> P y x) /\ (!x. P x x) /\
272 (!x y. 0 < x /\ 0 < y /\ P x y ==> P x (x + y)) ==>
273 !m n. P m n
274Proof
275 GEN_TAC THEN STRIP_TAC THEN
276 HO_MATCH_MP_TAC lexnum_induct THEN
277 REPEAT STRIP_TAC THEN Cases_on `m = 0` THEN1 SRW_TAC [][] THEN
278 Cases_on `m = n` THEN1 SRW_TAC [][] THEN
279 `0 < m` by DECIDE_TAC THEN
280 Cases_on `m < n` THENL [
281 Q_TAC SUFF_TAC `?z. (n = m + z) /\ 0 < z /\ z < n`
282 THEN1 metisLib.METIS_TAC [] THEN
283 Q.EXISTS_TAC `n - m` THEN DECIDE_TAC,
284 `n < m` by DECIDE_TAC THEN SRW_TAC [][]
285 ]
286QED
287
288(* proof of LINEAR_GCD{_AUX} due to Laurent Thery *)
289Theorem LINEAR_GCD_AUX[local]:
290 !m n. ~(n = 0) /\ ~(m = 0) ==>
291 (?p q. p * n = q * m + gcd m n) /\ ?p q. p * m = q * n + gcd m n
292Proof
293 HO_MATCH_MP_TAC GCD_SUCfree_ind THEN
294 SRW_TAC [][LEFT_ADD_DISTRIB] THEN
295 RULE_ASSUM_TAC (REWRITE_RULE [DECIDE ``0 < x <=> ~(x = 0)``]) THENL [
296 PROVE_TAC [GCD_SYM],
297 PROVE_TAC [GCD_SYM],
298 MAP_EVERY Q.EXISTS_TAC [`1`,`0`] THEN SRW_TAC [][],
299 `?a b. a * n = b * m + gcd m n` by PROVE_TAC [] THEN
300 MAP_EVERY Q.EXISTS_TAC [`a`, `a + b`],
301
302 `?a b. a * m = b * n + gcd m n` by PROVE_TAC [] THEN
303 MAP_EVERY Q.EXISTS_TAC [`a + b`, `b`]
304 ] THEN
305 ASM_SIMP_TAC bool_ss [LEFT_ADD_DISTRIB, RIGHT_ADD_DISTRIB] THEN
306 SIMP_TAC (bool_ss ++ numSimps.ARITH_ss) []
307QED
308
309
310Theorem LINEAR_GCD:
311 !n m. ~(n = 0) ==> ?p q. p * n = q * m + gcd m n
312Proof
313 REPEAT STRIP_TAC THEN Cases_on `m=0` THENL [
314 Q.EXISTS_TAC `1` THEN ARW[GCD_0L],
315 PROVE_TAC[LINEAR_GCD_AUX]
316 ]
317QED
318
319(* Theorem: 0 < j ==> ?p q. p * j = q * k + gcd j k *)
320(* Proof: by LINEAR_GCD, GCD_SYM *)
321Theorem GCD_LINEAR:
322 !j k. 0 < j ==> ?p q. p * j = q * k + gcd j k
323Proof
324 metis_tac[LINEAR_GCD, GCD_SYM, NOT_ZERO]
325QED
326
327Theorem gcd_lemma0[local]:
328 !a b. gcd a b = if b <= a then gcd (a - b) b
329 else gcd a (b - a)
330Proof
331 Cases THEN SIMP_TAC arith_ss [] THEN
332 Cases THEN SIMP_TAC arith_ss [] THEN
333 REWRITE_TAC [gcd_def]
334QED
335
336Theorem gcd_lemma[local]:
337 !n a b. n * b <= a ==> (gcd a b = gcd (a - n * b) b)
338Proof
339 Induct THENL [
340 SIMP_TAC arith_ss [],
341 SIMP_TAC bool_ss [MULT_CLAUSES] THEN REPEAT STRIP_TAC THEN
342 `n * b <= a` by ASM_SIMP_TAC arith_ss [] THEN
343 SIMP_TAC bool_ss [SUB_PLUS] THEN
344 Q.SPECL_THEN [`a - n * b`, `b`] MP_TAC gcd_lemma0 THEN
345 ASM_SIMP_TAC arith_ss []
346 ]
347QED
348
349Theorem GCD_EFFICIENTLY:
350 !a b.
351 gcd a b = if a = 0 then b
352 else gcd (b MOD a) a
353Proof
354 REPEAT STRIP_TAC THEN Cases_on `a = 0` THEN1 SRW_TAC [][] THEN
355 Cases_on `b = 0` THEN1 SRW_TAC [ARITH_ss][] THEN
356 `(b = (b DIV a) * a + b MOD a) /\ b MOD a < a`
357 by (MATCH_MP_TAC DIVISION THEN DECIDE_TAC) THEN
358 Q.ABBREV_TAC `q = b DIV a` THEN Q.ABBREV_TAC `r = b MOD a` THEN
359 markerLib.RM_ALL_ABBREVS_TAC THEN
360 FIRST_X_ASSUM SUBST_ALL_TAC THEN
361 `q * a <= q * a + r` by DECIDE_TAC THEN
362 `gcd a (q * a + r) = gcd a (q * a + r - q * a)`
363 by METIS_TAC [GCD_SYM, gcd_lemma] THEN
364 ASM_SIMP_TAC bool_ss [DECIDE (Term`(x:num) + y - x = y`)] THEN
365 SIMP_TAC bool_ss [GCD_SYM]
366QED
367
368Definition lcm_def:
369 lcm m n = if (m = 0) \/ (n = 0) then 0 else (m * n) DIV gcd m n
370End
371
372val _ = computeLib.add_persistent_funs
373 ["GCD_EFFICIENTLY"
374 ,"lcm_def"];
375
376Theorem LCM_IS_LEAST_COMMON_MULTIPLE:
377 divides m (lcm m n) /\ divides n (lcm m n) /\
378 !p. divides m p /\ divides n p ==> divides (lcm m n) p
379Proof
380 SIMP_TAC (srw_ss()) [lcm_def] THEN
381 Cases_on `m = 0` THEN1 SRW_TAC [][ALL_DIVIDES_0] THEN
382 Cases_on `n = 0` THEN1 SRW_TAC [][ALL_DIVIDES_0] THEN
383 ASM_SIMP_TAC (srw_ss()) [] THEN
384 Q.ABBREV_TAC `g = gcd m n` THEN
385 `?c d. (m = c * g) /\ (n = d * g) /\ (gcd c d = 1)`
386 by METIS_TAC [FACTOR_OUT_GCD] THEN
387 ASM_SIMP_TAC (srw_ss()) [] THEN STRIP_TAC THEN
388 `c * g * (d * g) DIV g = c * g * d`
389 by (MATCH_MP_TAC DIV_UNIQUE THEN Q.EXISTS_TAC `0` THEN
390 FULL_SIMP_TAC (srw_ss() ++ ARITH_ss) [ZERO_LESS_MULT]) THEN
391 REPEAT CONJ_TAC THENL [
392 SRW_TAC [][divides_def] THEN Q.EXISTS_TAC `d` THEN
393 ASM_SIMP_TAC (srw_ss() ++ ARITH_ss) [],
394 SRW_TAC [][divides_def] THEN Q.EXISTS_TAC `c` THEN
395 ASM_SIMP_TAC (srw_ss() ++ ARITH_ss) [],
396 REPEAT STRIP_TAC THEN
397 `?a b. (p = a * (c * g)) /\ (p = b * (d * g))`
398 by PROVE_TAC [divides_def] THEN
399 SRW_TAC [][] THEN
400 `0 < g` by FULL_SIMP_TAC (srw_ss() ++ ARITH_ss) [MULT_EQ_0] THEN
401 `b * d = a * c`
402 by (`b * (d * g) = g * (b * d)` by DECIDE_TAC THEN
403 `a * (c * g) = g * (a * c)` by DECIDE_TAC THEN
404 `g * (b * d) = g * (a * c)` by DECIDE_TAC THEN
405 POP_ASSUM MP_TAC THEN SIMP_TAC (srw_ss()) [EQ_MULT_LCANCEL] THEN
406 SRW_TAC [ARITH_ss][]) THEN
407 Q_TAC SUFF_TAC `divides d a`
408 THEN1 (SRW_TAC [][divides_def] THEN
409 Q.EXISTS_TAC `q` THEN DECIDE_TAC) THEN
410 `divides d (a * c)` by PROVE_TAC [divides_def] THEN
411 PROVE_TAC [L_EUCLIDES, MULT_COMM]
412 ]
413QED
414
415Theorem LCM_0[simp]:
416 (lcm 0 x = 0) /\ (lcm x 0 = 0)
417Proof
418 SRW_TAC [][lcm_def]
419QED
420
421Theorem LCM_1[simp]:
422 (lcm 1 x = x) /\ (lcm x 1 = x)
423Proof
424 SRW_TAC [][lcm_def]
425QED
426
427Theorem LCM_COMM:
428 lcm a b = lcm b a
429Proof
430 SRW_TAC [][lcm_def, GCD_SYM, MULT_COMM]
431QED
432
433(* |- !a b. lcm a b = lcm b a *)
434Theorem LCM_SYM = LCM_COMM |> GEN ``b:num`` |> GEN ``a:num``;
435
436Theorem LCM_LE[simp]:
437 0 < m /\ 0 < n ==> (m <= lcm m n) /\ (m <= lcm n m)
438Proof
439 SIMP_TAC (srw_ss() ++ ARITH_ss) [lcm_def, GCD_SYM] THEN
440 `divides (gcd m n) n` by METIS_TAC [GCD_IS_GCD, IS_GCD] THEN
441 Q.ABBREV_TAC `g = gcd m n` THEN
442 `?a. n = a * g` by METIS_TAC [divides_def] THEN
443 STRIP_TAC THEN SRW_TAC [][] THEN
444 `0 < g` by FULL_SIMP_TAC (srw_ss()) [ZERO_LESS_MULT] THEN
445 `m * (a * g) DIV g = m * a` by METIS_TAC [MULT_DIV, MULT_ASSOC] THEN
446 Q_TAC SUFF_TAC `1 <= a` THEN1 METIS_TAC [LE_MULT_LCANCEL, MULT_CLAUSES] THEN
447 FULL_SIMP_TAC (srw_ss() ++ ARITH_ss) [ZERO_LESS_MULT]
448QED
449
450Theorem LCM_LEAST:
451 0 < m /\ 0 < n ==>
452 !p. 0 < p /\ p < lcm m n ==> ~(divides m p) \/ ~(divides n p)
453Proof
454 REPEAT STRIP_TAC THEN SPOSE_NOT_THEN STRIP_ASSUME_TAC THEN
455 `divides (lcm m n) p` by METIS_TAC [LCM_IS_LEAST_COMMON_MULTIPLE] THEN
456 `lcm m n <= p` by METIS_TAC [DIVIDES_LE] THEN
457 DECIDE_TAC
458QED
459
460
461Theorem GCD_COMMON_FACTOR:
462 !m n k. gcd (k * m) (k * n) = k * gcd m n
463Proof
464 HO_MATCH_MP_TAC GCD_SUCfree_ind
465 THEN REPEAT STRIP_TAC
466 THEN1 REWRITE_TAC [gcd_def,MULT_CLAUSES]
467 THEN1 METIS_TAC [GCD_SYM]
468 THEN1 REWRITE_TAC [GCD_REF]
469 THEN ASM_REWRITE_TAC [LEFT_ADD_DISTRIB,GCD_ADD_R]
470QED
471
472Theorem GCD_EQ_IS_GCD[local]:
473 !m n. (gcd m n = k) = is_gcd m n k
474Proof
475 METIS_TAC [GCD_IS_GCD,IS_GCD_UNIQUE]
476QED
477
478Theorem divides_IMP[local]:
479 !m n p. divides m n ==> divides m (p * n)
480Proof
481 REWRITE_TAC [divides_def] THEN REPEAT STRIP_TAC
482 THEN ASM_REWRITE_TAC [MULT_ASSOC] THEN METIS_TAC []
483QED
484
485Theorem GCD_CANCEL_MULT:
486 !m n k. (gcd m k = 1) ==> (gcd m (k * n) = gcd m n)
487Proof
488 REPEAT STRIP_TAC
489 THEN REWRITE_TAC [GCD_EQ_IS_GCD,IS_GCD,GCD_THM]
490 THEN REPEAT STRIP_TAC
491 THEN1 (MATCH_MP_TAC divides_IMP THEN REWRITE_TAC [GCD_THM])
492 THEN `divides d n` suffices_by METIS_TAC [GCD_THM]
493 THEN MATCH_MP_TAC L_EUCLIDES
494 THEN Q.EXISTS_TAC `k`
495 THEN ASM_REWRITE_TAC []
496 THEN FULL_SIMP_TAC bool_ss [IS_GCD,GCD_EQ_IS_GCD,ONE_DIVIDES_ALL]
497 THEN REPEAT STRIP_TAC
498 THEN Q.PAT_ASSUM `!d.bbb` MATCH_MP_TAC
499 THEN IMP_RES_TAC DIVIDES_TRANS
500 THEN ASM_REWRITE_TAC []
501QED
502
503Theorem ODD_IMP_GCD_CANCEL_EVEN[local]:
504 !n. ODD n ==> (gcd n (2 * m) = gcd n m)
505Proof
506 REPEAT STRIP_TAC
507 THEN MATCH_MP_TAC GCD_CANCEL_MULT
508 THEN ONCE_REWRITE_TAC [GCD_SYM]
509 THEN `~divides 2 n` suffices_by
510 (STRIP_TAC
511 THEN MP_TAC (Q.SPEC `n` (MATCH_MP PRIME_GCD PRIME_2))
512 THEN ASM_REWRITE_TAC [])
513 THEN REWRITE_TAC [divides_def]
514 THEN ONCE_REWRITE_TAC [MULT_COMM]
515 THEN REWRITE_TAC [GSYM EVEN_EXISTS]
516 THEN FULL_SIMP_TAC bool_ss [ODD_EVEN]
517QED
518
519Theorem BINARY_GCD:
520 !m n.
521 (EVEN m /\ EVEN n ==> (gcd m n = 2 * gcd (m DIV 2) (n DIV 2))) /\
522 (EVEN m /\ ODD n ==> (gcd m n = gcd (m DIV 2) n))
523Proof
524 SIMP_TAC bool_ss [EVEN_EXISTS] THEN REVERSE (REPEAT STRIP_TAC)
525 THEN `0 < 2` by (MATCH_MP_TAC PRIME_POS THEN REWRITE_TAC [PRIME_2])
526 THEN FULL_SIMP_TAC bool_ss [GCD_COMMON_FACTOR,
527 ONCE_REWRITE_RULE [MULT_COMM] MULT_DIV,
528 ONCE_REWRITE_RULE [GCD_SYM] ODD_IMP_GCD_CANCEL_EVEN]
529QED
530
531Theorem gcd_LESS_EQ:
532 !m n. n <> 0 ==> gcd m n <= n
533Proof
534 recInduct gcd_ind >> srw_tac[][] >> rewrite_tac[gcd_def] >>
535 IF_CASES_TAC >> FULL_SIMP_TAC (srw_ss()) [] >>
536 irule LESS_EQ_TRANS >> goal_assum drule >>
537 rewrite_tac[SUB_RIGHT_LESS_EQ] >>
538 rewrite_tac[Once ADD_COMM] >>
539 rewrite_tac[ADD_CLAUSES] >>
540 rewrite_tac[ADD_SUC] >>
541 rewrite_tac[LESS_EQ_ADD]
542QED
543
544(* ------------------------------------------------------------------------- *)
545(* Basic GCD, LCM Theorems (from examples/algebra) *)
546(* ------------------------------------------------------------------------- *)
547
548(* Proof:
549 0 < n ==> n <> 0, 0 < m ==> m <> 0, by NOT_ZERO_LT_ZERO
550 hence g = gcd n m <> 0, or 0 < g. by GCD_EQ_0
551 g = gcd n m ==> (g divides n) /\ (g divides m) by GCD_IS_GCD, is_gcd_def
552 ==> (n MOD g = 0) /\ (m MOD g = 0) by DIVIDES_MOD_0
553*)
554Theorem GCD_DIVIDES:
555 !m n. 0 < n /\ 0 < m ==>
556 0 < gcd n m /\ (n MOD (gcd n m) = 0) /\ (m MOD (gcd n m) = 0)
557Proof
558 ntac 3 strip_tac >>
559 conj_asm1_tac >-
560 metis_tac[GCD_EQ_0, NOT_ZERO_LT_ZERO] >>
561 metis_tac[GCD_IS_GCD, is_gcd_def, DIVIDES_MOD_0]
562QED
563
564(* Theorem: gcd n (gcd n m) = gcd n m *)
565(* Proof:
566 If n = 0,
567 gcd 0 (gcd n m) = gcd n m by GCD_0L
568 If m = 0,
569 gcd n (gcd n 0)
570 = gcd n n by GCD_0R
571 = n = gcd n 0 by GCD_REF
572 If n <> 0, m <> 0, d <> 0 by GCD_EQ_0
573 Since d divides n, n MOD d = 0
574 gcd n d
575 = gcd d n by GCD_SYM
576 = gcd (n MOD d) d by GCD_EFFICIENTLY, d <> 0
577 = gcd 0 d by GCD_DIVIDES
578 = d by GCD_0L
579*)
580Theorem GCD_GCD:
581 !m n. gcd n (gcd n m) = gcd n m
582Proof
583 rpt strip_tac >>
584 Cases_on `n = 0` >- rw[] >>
585 Cases_on `m = 0` >- rw[] >>
586 `0 < n /\ 0 < m` by decide_tac >>
587 metis_tac[GCD_SYM, GCD_EFFICIENTLY, GCD_DIVIDES, GCD_EQ_0, GCD_0L]
588QED
589
590(* Theorem: GCD m n * LCM m n = m * n *)
591(* Proof:
592 By lcm_def:
593 lcm m n = if (m = 0) \/ (n = 0) then 0 else m * n DIV gcd m n
594 If m = 0,
595 gcd 0 n * lcm 0 n = n * 0 = 0 = 0 * n, hence true.
596 If n = 0,
597 gcd m 0 * lcm m 0 = m * 0 = 0 = m * 0, hence true.
598 If m <> 0, n <> 0,
599 gcd m n * lcm m n = gcd m n * (m * n DIV gcd m n) = m * n.
600*)
601Theorem GCD_LCM:
602 !m n. gcd m n * lcm m n = m * n
603Proof
604 rw[lcm_def] >>
605 `0 < m /\ 0 < n` by decide_tac >>
606 `0 < gcd m n /\ (n MOD gcd m n = 0)` by rw[GCD_DIVIDES] >>
607 qabbrev_tac `d = gcd m n` >>
608 `m * n = (m * n) DIV d * d + (m * n) MOD d` by rw[DIVISION] >>
609 `(m * n) MOD d = 0` by metis_tac[MOD_TIMES2, ZERO_MOD, MULT_0] >>
610 metis_tac[ADD_0, MULT_COMM]
611QED
612
613(* temporarily make divides an infix *)
614val _ = temp_set_fixity "divides" (Infixl 480);
615 (* relation is 450, +/- is 500, * is 600. *)
616
617(* Theorem: m divides (lcm m n) /\ n divides (lcm m n) *)
618(* Proof: by LCM_IS_LEAST_COMMON_MULTIPLE *)
619Theorem LCM_DIVISORS:
620 !m n. m divides (lcm m n) /\ n divides (lcm m n)
621Proof
622 rw[LCM_IS_LEAST_COMMON_MULTIPLE]
623QED
624
625(* Theorem: m divides p /\ n divides p ==> (lcm m n) divides p *)
626(* Proof: by LCM_IS_LEAST_COMMON_MULTIPLE *)
627Theorem LCM_IS_LCM:
628 !m n p. m divides p /\ n divides p ==> (lcm m n) divides p
629Proof
630 rw[LCM_IS_LEAST_COMMON_MULTIPLE]
631QED
632
633(* Theorem: (lcm m n = 0) <=> ((m = 0) \/ (n = 0)) *)
634(* Proof:
635 If part: lcm m n = 0 ==> m = 0 \/ n = 0
636 By contradiction, suppse m = 0 /\ n = 0.
637 Then gcd m n = 0 by GCD_EQ_0
638 and m * n = 0 by MULT_EQ_0
639 but (gcd m n) * (lcm m n) = m * n by GCD_LCM
640 so RHS <> 0, but LHS = 0 by MULT_0
641 This is a contradiction.
642 Only-if part: m = 0 \/ n = 0 ==> lcm m n = 0
643 True by LCM_0
644*)
645Theorem LCM_EQ_0:
646 !m n. (lcm m n = 0) <=> ((m = 0) \/ (n = 0))
647Proof
648 rw[EQ_IMP_THM] >| [
649 spose_not_then strip_assume_tac >>
650 `(gcd m n) * (lcm m n) = m * n` by rw[GCD_LCM] >>
651 `gcd m n <> 0` by rw[GCD_EQ_0] >>
652 `m * n <> 0` by rw[MULT_EQ_0] >>
653 metis_tac[MULT_0],
654 rw[LCM_0],
655 rw[LCM_0]
656 ]
657QED
658
659(* Theorem: lcm a a = a *)
660(* Proof:
661 If a = 0,
662 lcm 0 0 = 0 by LCM_0
663 If a <> 0,
664 (gcd a a) * (lcm a a) = a * a by GCD_LCM
665 a * (lcm a a) = a * a by GCD_REF
666 lcm a a = a by MULT_LEFT_CANCEL, a <> 0
667*)
668Theorem LCM_REF:
669 !a. lcm a a = a
670Proof
671 metis_tac[num_CASES, LCM_0, GCD_LCM, GCD_REF, MULT_LEFT_CANCEL]
672QED
673
674(* Theorem: a divides n /\ b divides n ==> (lcm a b) divides n *)
675(* Proof: same as LCM_IS_LCM *)
676Theorem LCM_DIVIDES:
677 !n a b. a divides n /\ b divides n ==> (lcm a b) divides n
678Proof
679 rw[LCM_IS_LCM]
680QED
681
682(* Theorem: 0 < m \/ 0 < n ==> 0 < gcd m n *)
683(* Proof: by GCD_EQ_0, NOT_ZERO_LT_ZERO *)
684Theorem GCD_POS:
685 !m n. 0 < m \/ 0 < n ==> 0 < gcd m n
686Proof
687 metis_tac[GCD_EQ_0, NOT_ZERO_LT_ZERO]
688QED
689
690(* Theorem: 0 < m /\ 0 < n ==> 0 < lcm m n *)
691(* Proof: by LCM_EQ_0, NOT_ZERO_LT_ZERO *)
692Theorem LCM_POS:
693 !m n. 0 < m /\ 0 < n ==> 0 < lcm m n
694Proof
695 metis_tac[LCM_EQ_0, NOT_ZERO_LT_ZERO]
696QED
697
698(* Theorem: n divides m <=> gcd n m = n *)
699(* Proof:
700 If part:
701 n divides m ==> ?k. m = k * n by divides_def
702 gcd n m
703 = gcd n (k * n)
704 = gcd (n * 1) (n * k) by MULT_RIGHT_1, MULT_COMM
705 = n * gcd 1 k by GCD_COMMON_FACTOR
706 = n * 1 by GCD_1
707 = n by MULT_RIGHT_1
708 Only-if part: gcd n m = n ==> n divides m
709 If n = 0, gcd 0 m = m by GCD_0L
710 But gcd n m = n = 0 by givien
711 hence m = 0,
712 and 0 divides 0 is true by DIVIDES_REFL
713 If n <> 0,
714 If m = 0, LHS true by GCD_0R
715 RHS true by ALL_DIVIDES_0
716 If m <> 0,
717 then 0 < n and 0 < m,
718 gcd n m = gcd (m MOD n) n by GCD_EFFICIENTLY
719 if (m MOD n) = 0
720 then n divides m by DIVIDES_MOD_0
721 If (m MOD n) <> 0,
722 so (m MOD n) MOD (gcd n m) = 0 by GCD_DIVIDES
723 or (m MOD n) MOD n = 0 by gcd n m = n, given
724 or m MOD n = 0 by MOD_MOD
725 contradicting (m MOD n) <> 0, hence true.
726*)
727Theorem divides_iff_gcd_fix:
728 !m n. n divides m <=> (gcd n m = n)
729Proof
730 rw[EQ_IMP_THM] >| [
731 `?k. m = k * n` by rw[GSYM divides_def] >>
732 `gcd n m = gcd (n * 1) (n * k)` by rw[MULT_COMM] >>
733 rw[GCD_COMMON_FACTOR, GCD_1],
734 Cases_on `n = 0` >-
735 metis_tac[GCD_0L, DIVIDES_REFL] >>
736 Cases_on `m = 0` >-
737 metis_tac[GCD_0R, ALL_DIVIDES_0] >>
738 `0 < n /\ 0 < m` by decide_tac >>
739 Cases_on `m MOD n = 0` >-
740 metis_tac[DIVIDES_MOD_0] >>
741 `0 < m MOD n` by decide_tac >>
742 metis_tac[GCD_EFFICIENTLY, GCD_DIVIDES, MOD_MOD]
743 ]
744QED
745
746(* Theorem: !m n. n divides m <=> (lcm n m = m) *)
747(* Proof:
748 If n = 0,
749 n divides m <=> m = 0 by ZERO_DIVIDES
750 and lcm 0 0 = 0 = m by LCM_0
751 If n <> 0,
752 gcd n m * lcm n m = n * m by GCD_LCM
753 If part: n divides m ==> (lcm n m = m)
754 Then gcd n m = n by divides_iff_gcd_fix
755 so n * lcm n m = n * m by above
756 lcm n m = m by MULT_LEFT_CANCEL, n <> 0
757 Only-if part: lcm n m = m ==> n divides m
758 If m = 0, n divdes 0 = true by ALL_DIVIDES_0
759 If m <> 0,
760 Then gcd n m * m = n * m by above
761 or gcd n m = n by MULT_RIGHT_CANCEL, m <> 0
762 so n divides m by divides_iff_gcd_fix
763*)
764Theorem divides_iff_lcm_fix:
765 !m n. n divides m <=> (lcm n m = m)
766Proof
767 rpt strip_tac >>
768 Cases_on `n = 0` >-
769 metis_tac[ZERO_DIVIDES, LCM_0] >>
770 metis_tac[GCD_LCM, MULT_LEFT_CANCEL, MULT_RIGHT_CANCEL, divides_iff_gcd_fix,
771 ALL_DIVIDES_0]
772QED
773
774(* ------------------------------------------------------------------------- *)
775(* Consequences of Coprime. *)
776(* ------------------------------------------------------------------------- *)
777
778(* Theorem: coprime n x /\ coprime n y ==> coprime n (x * y) *)
779(* Proof:
780 gcd n x = 1 ==> no common factor between x and n
781 gcd n y = 1 ==> no common factor between y and n
782 Hence there is no common factor between (x * y) and n, or gcd n (x * y) = 1
783
784 gcd n (x * y) = gcd n y by GCD_CANCEL_MULT, since coprime n x.
785 = 1 by given
786*)
787Theorem PRODUCT_WITH_GCD_ONE:
788 !n x y. coprime n x /\ coprime n y ==> coprime n (x * y)
789Proof
790 metis_tac[GCD_CANCEL_MULT]
791QED
792
793(* Theorem: For 0 < n, coprime n x ==> coprime n (x MOD n) *)
794(* Proof:
795 Since n <> 0,
796 1 = gcd n x by given
797 = gcd (x MOD n) n by GCD_EFFICIENTLY
798 = gcd n (x MOD n) by GCD_SYM
799*)
800Theorem MOD_WITH_GCD_ONE:
801 !n x. 0 < n /\ coprime n x ==> coprime n (x MOD n)
802Proof
803 rpt strip_tac >>
804 `0 <> n` by decide_tac >>
805 metis_tac[GCD_EFFICIENTLY, GCD_SYM]
806QED
807
808(* Proof:
809 By GCD_IS_GREATEST_COMMON_DIVISOR
810 (gcd a b) divides a [1]
811 and (gcd a b) divides b [2]
812 and !p. p divides a /\ p divides b ==> p divides (gcd a b) [3]
813 Hence if part is true, and for the only-if part,
814 We have c divides (gcd a b) by [3] above,
815 and (gcd a b) divides c by [1], [2] and the given implication
816 Therefore c = gcd a b by DIVIDES_ANTISYM
817*)
818Theorem GCD_PROPERTY:
819 !a b c.
820 c = gcd a b ⇔
821 c divides a ∧ c divides b ∧ ∀x. x divides a ∧ x divides b ⇒ x divides c
822Proof
823 rw[GCD_IS_GREATEST_COMMON_DIVISOR, DIVIDES_ANTISYM, EQ_IMP_THM]
824QED
825
826(* Theorem: gcd a (gcd b c) = gcd (gcd a b) c *)
827(* Proof:
828 Since (gcd a (gcd b c)) divides a by GCD_PROPERTY
829 (gcd a (gcd b c)) divides b by GCD_PROPERTY, DIVIDES_TRANS
830 (gcd a (gcd b c)) divides c by GCD_PROPERTY, DIVIDES_TRANS
831 (gcd (gcd a b) c) divides a by GCD_PROPERTY, DIVIDES_TRANS
832 (gcd (gcd a b) c) divides b by GCD_PROPERTY, DIVIDES_TRANS
833 (gcd (gcd a b) c) divides c by GCD_PROPERTY
834 We have
835 (gcd (gcd a b) c) divides (gcd b c) by GCD_PROPERTY
836 and (gcd (gcd a b) c) divides (gcd a (gcd b c)) by GCD_PROPERTY
837 Also (gcd a (gcd b c)) divides (gcd a b) by GCD_PROPERTY
838 and (gcd a (gcd b c)) divides (gcd (gcd a b) c) by GCD_PROPERTY
839 Therefore gcd a (gcd b c) = gcd (gcd a b) c by DIVIDES_ANTISYM
840*)
841Theorem GCD_ASSOC:
842 !a b c. gcd a (gcd b c) = gcd (gcd a b) c
843Proof
844 rpt strip_tac >>
845 `(gcd a (gcd b c)) divides a` by metis_tac[GCD_PROPERTY] >>
846 `(gcd a (gcd b c)) divides b` by metis_tac[GCD_PROPERTY, DIVIDES_TRANS] >>
847 `(gcd a (gcd b c)) divides c` by metis_tac[GCD_PROPERTY, DIVIDES_TRANS] >>
848 `(gcd (gcd a b) c) divides a` by metis_tac[GCD_PROPERTY, DIVIDES_TRANS] >>
849 `(gcd (gcd a b) c) divides b` by metis_tac[GCD_PROPERTY, DIVIDES_TRANS] >>
850 `(gcd (gcd a b) c) divides c` by metis_tac[GCD_PROPERTY] >>
851 `(gcd (gcd a b) c) divides (gcd a (gcd b c))` by metis_tac[GCD_PROPERTY] >>
852 `(gcd a (gcd b c)) divides (gcd (gcd a b) c)` by metis_tac[GCD_PROPERTY] >>
853 rw[DIVIDES_ANTISYM]
854QED
855
856(* Note:
857 With identity by GCD_1: (gcd 1 x = 1) /\ (gcd x 1 = 1)
858 GCD forms a monoid in numbers.
859*)
860
861(* Theorem: gcd a (gcd b c) = gcd b (gcd a c) *)
862(* Proof:
863 gcd a (gcd b c)
864 = gcd (gcd a b) c by GCD_ASSOC
865 = gcd (gcd b a) c by GCD_SYM
866 = gcd b (gcd a c) by GCD_ASSOC
867*)
868Theorem GCD_ASSOC_COMM:
869 !a b c. gcd a (gcd b c) = gcd b (gcd a c)
870Proof
871 metis_tac[GCD_ASSOC, GCD_SYM]
872QED
873
874(* Proof:
875 By LCM_IS_LEAST_COMMON_MULTIPLE
876 a divides (lcm a b) [1]
877 and b divides (lcm a b) [2]
878 and !p. a divides p /\ divides b p ==> divides (lcm a b) p [3]
879 Hence if part is true, and for the only-if part,
880 We have c divides (lcm a b) by implication and [1], [2]
881 and (lcm a b) divides c by [3]
882 Therefore c = lcm a b by DIVIDES_ANTISYM
883*)
884Theorem LCM_PROPERTY:
885 ∀a b c.
886 c = lcm a b ⇔
887 a divides c ∧ b divides c ∧ ∀x. a divides x ∧ b divides x ⇒ c divides x
888Proof
889 rw[LCM_IS_LEAST_COMMON_MULTIPLE, DIVIDES_ANTISYM, EQ_IMP_THM]
890QED
891
892(* Theorem: lcm a (lcm b c) = lcm (lcm a b) c *)
893(* Proof:
894 Since a divides (lcm a (lcm b c)) by LCM_PROPERTY
895 b divides (lcm a (lcm b c)) by LCM_PROPERTY, DIVIDES_TRANS
896 c divides (lcm a (lcm b c)) by LCM_PROPERTY, DIVIDES_TRANS
897 a divides (lcm (lcm a b) c) by LCM_PROPERTY, DIVIDES_TRANS
898 b divides (lcm (lcm a b) c) by LCM_PROPERTY, DIVIDES_TRANS
899 c divides (lcm (lcm a b) c) by LCM_PROPERTY
900 We have
901 (lcm b c) divides (lcm (lcm a b) c) by LCM_PROPERTY
902 and (lcm a (lcm b c)) divides (lcm (lcm a b) c) by LCM_PROPERTY
903 Also (lcm a b) divides (lcm a (lcm b c)) by LCM_PROPERTY
904 and (lcm (lcm a b) c) divides (lcm a (lcm b c)) by LCM_PROPERTY
905 Therefore lcm a (lcm b c) = lcm (lcm a b) c by DIVIDES_ANTISYM
906*)
907Theorem LCM_ASSOC:
908 !a b c. lcm a (lcm b c) = lcm (lcm a b) c
909Proof
910 rpt strip_tac >>
911 `a divides (lcm a (lcm b c))` by metis_tac[LCM_PROPERTY] >>
912 `b divides (lcm a (lcm b c))` by metis_tac[LCM_PROPERTY, DIVIDES_TRANS] >>
913 `c divides (lcm a (lcm b c))` by metis_tac[LCM_PROPERTY, DIVIDES_TRANS] >>
914 `a divides (lcm (lcm a b) c)` by metis_tac[LCM_PROPERTY, DIVIDES_TRANS] >>
915 `b divides (lcm (lcm a b) c)` by metis_tac[LCM_PROPERTY, DIVIDES_TRANS] >>
916 `c divides (lcm (lcm a b) c)` by metis_tac[LCM_PROPERTY] >>
917 `(lcm a (lcm b c)) divides (lcm (lcm a b) c)` by metis_tac[LCM_PROPERTY] >>
918 `(lcm (lcm a b) c) divides (lcm a (lcm b c))` by metis_tac[LCM_PROPERTY] >>
919 rw[DIVIDES_ANTISYM]
920QED
921
922(* Note:
923 With the identity by LCM_0: (lcm 0 x = 0) /\ (lcm x 0 = 0)
924 LCM forms a monoid in numbers.
925*)
926
927(* Theorem: lcm a (lcm b c) = lcm b (lcm a c) *)
928(* Proof:
929 lcm a (lcm b c)
930 = lcm (lcm a b) c by LCM_ASSOC
931 = lcm (lcm b a) c by LCM_COMM
932 = lcm b (lcm a c) by LCM_ASSOC
933*)
934Theorem LCM_ASSOC_COMM:
935 !a b c. lcm a (lcm b c) = lcm b (lcm a c)
936Proof
937 metis_tac[LCM_ASSOC, LCM_COMM]
938QED
939
940(* Theorem: b <= a ==> gcd (a - b) b = gcd a b *)
941(* Proof:
942 gcd (a - b) b
943 = gcd b (a - b) by GCD_SYM
944 = gcd (b + (a - b)) b by GCD_ADD_L
945 = gcd (a - b + b) b by ADD_COMM
946 = gcd a b by SUB_ADD, b <= a.
947
948Note: If a < b, a - b = 0 for num, hence gcd (a - b) b = gcd 0 b = b.
949*)
950Theorem GCD_SUB_L:
951 !a b. b <= a ==> (gcd (a - b) b = gcd a b)
952Proof
953 metis_tac[GCD_SYM, GCD_ADD_L, ADD_COMM, SUB_ADD]
954QED
955
956(* Theorem: a <= b ==> gcd a (b - a) = gcd a b *)
957(* Proof:
958 gcd a (b - a)
959 = gcd (b - a) a by GCD_SYM
960 = gcd b a by GCD_SUB_L
961 = gcd a b by GCD_SYM
962*)
963Theorem GCD_SUB_R:
964 !a b. a <= b ==> (gcd a (b - a) = gcd a b)
965Proof
966 metis_tac[GCD_SYM, GCD_SUB_L]
967QED
968
969(* Theorem: prime a ==> a divides b iff a divides b ** n for any n *)
970(* Proof:
971 by induction on n.
972 Base case: 0 < 0 ==> (a divides b <=> a divides (b ** 0))
973 True since 0 < 0 is False.
974 Step case: 0 < n ==> (a divides b <=> a divides (b ** n)) ==>
975 0 < SUC n ==> (a divides b <=> a divides (b ** SUC n))
976 i.e. 0 < n ==> (a divides b <=> a divides (b ** n))==>
977 a divides b <=> a divides (b * b ** n) by EXP
978 If n = 0, b ** 0 = 1 by EXP
979 Hence true.
980 If n <> 0, 0 < n,
981 If part: a divides b /\ 0 < n ==>
982 (a divides b <=> a divides (b ** n)) ==>
983 a divides (b ** n)
984 True by DIVIDES_MULT.
985 Only-if part: a divides (b * b ** n) /\ 0 < n ==>
986 (a divides b <=> a divides (b ** n)) ==>
987 a divides (b ** n)
988 Since prime a, a divides b, or a divides (b ** n) by P_EUCLIDES
989 Either case is true.
990*)
991Theorem DIVIDES_EXP_BASE:
992 !a b n. prime a /\ 0 < n ==> (a divides b <=> a divides (b ** n))
993Proof
994 rpt strip_tac >>
995 Induct_on `n` >-
996 rw[] >>
997 rw[EXP] >>
998 Cases_on `n = 0` >-
999 rw[EXP] >>
1000 `0 < n` by decide_tac >>
1001 rw[EQ_IMP_THM] >-
1002 metis_tac[DIVIDES_MULT] >>
1003 `a divides b \/ a divides (b ** n)` by rw[P_EUCLIDES] >>
1004 metis_tac[]
1005QED
1006
1007(* Theorem: coprime m n ==> LCM m n = m * n *)
1008(* Proof:
1009 By GCD_LCM, with gcd m n = 1.
1010*)
1011Theorem LCM_COPRIME:
1012 !m n. coprime m n ==> (lcm m n = m * n)
1013Proof
1014 metis_tac[GCD_LCM, MULT_LEFT_1]
1015QED
1016
1017(* Theorem: 0 < m ==> (gcd m n = gcd m (n MOD m)) *)
1018(* Proof:
1019 gcd m n
1020 = gcd (n MOD m) m by GCD_EFFICIENTLY, m <> 0
1021 = gcd m (n MOD m) by GCD_SYM
1022*)
1023Theorem GCD_MOD:
1024 !m n. 0 < m ==> (gcd m n = gcd m (n MOD m))
1025Proof
1026 rw[Once GCD_EFFICIENTLY, GCD_SYM]
1027QED
1028
1029(* Theorem: 0 < m ==> (gcd n m = gcd (n MOD m) m) *)
1030(* Proof: by GCD_MOD, GCD_COMM *)
1031Theorem GCD_MOD_COMM:
1032 !m n. 0 < m ==> (gcd n m = gcd (n MOD m) m)
1033Proof
1034 metis_tac[GCD_MOD, GCD_COMM]
1035QED
1036
1037(* Theorem: gcd a (b * a + c) = gcd a c *)
1038(* Proof:
1039 If a = 0,
1040 Then b * 0 + c = c by arithmetic
1041 Hence trivially true.
1042 If a <> 0,
1043 gcd a (b * a + c)
1044 = gcd ((b * a + c) MOD a) a by GCD_EFFICIENTLY, 0 < a
1045 = gcd (c MOD a) a by MOD_TIMES, 0 < a
1046 = gcd a c by GCD_EFFICIENTLY, 0 < a
1047*)
1048Theorem GCD_EUCLID:
1049 !a b c. gcd a (b * a + c) = gcd a c
1050Proof
1051 rpt strip_tac >>
1052 Cases_on `a = 0` >-
1053 rw[] >>
1054 metis_tac[GCD_EFFICIENTLY, MOD_TIMES, NOT_ZERO_LT_ZERO]
1055QED
1056
1057(* Theorem: gcd (b * a + c) a = gcd a c *)
1058(* Proof: by GCD_EUCLID, GCD_SYM *)
1059Theorem GCD_REDUCE:
1060 !a b c. gcd (b * a + c) a = gcd a c
1061Proof
1062 rw[GCD_EUCLID, GCD_SYM]
1063QED
1064
1065(* Theorem alias *)
1066Theorem GCD_REDUCE_BY_COPRIME = GCD_CANCEL_MULT;
1067(* val GCD_REDUCE_BY_COPRIME =
1068 |- !m n k. coprime m k ==> gcd m (k * n) = gcd m n: thm *)
1069
1070(* ------------------------------------------------------------------------- *)
1071(* Coprime Theorems (from examples/algebra) *)
1072(* ------------------------------------------------------------------------- *)
1073
1074(* Theorem: coprime n (n + 1) *)
1075(* Proof:
1076 Since n < n + 1 ==> n <= n + 1,
1077 gcd n (n + 1)
1078 = gcd n (n + 1 - n) by GCD_SUB_R
1079 = gcd n 1 by arithmetic
1080 = 1 by GCD_1
1081*)
1082Theorem coprime_SUC:
1083 !n. coprime n (n + 1)
1084Proof
1085 rw[GCD_SUB_R]
1086QED
1087
1088(* Theorem: 0 < n ==> coprime n (n - 1) *)
1089(* Proof:
1090 gcd n (n - 1)
1091 = gcd (n - 1) n by GCD_SYM
1092 = gcd (n - 1) (n - 1 + 1) by SUB_ADD, 0 <= n
1093 = 1 by coprime_SUC
1094*)
1095Theorem coprime_PRE:
1096 !n. 0 < n ==> coprime n (n - 1)
1097Proof
1098 metis_tac[GCD_SYM, coprime_SUC, DECIDE``!n. 0 < n ==> (n - 1 + 1 = n)``]
1099QED
1100
1101(* Theorem: coprime 0 n ==> n = 1 *)
1102(* Proof:
1103 gcd 0 n = n by GCD_0L
1104 = 1 by coprime 0 n
1105*)
1106Theorem coprime_0L:
1107 !n. coprime 0 n <=> (n = 1)
1108Proof
1109 rw[GCD_0L]
1110QED
1111
1112(* Theorem: coprime n 0 ==> n = 1 *)
1113(* Proof:
1114 gcd n 0 = n by GCD_0L
1115 = 1 by coprime n 0
1116*)
1117Theorem coprime_0R:
1118 !n. coprime n 0 <=> (n = 1)
1119Proof
1120 rw[GCD_0R]
1121QED
1122
1123(* Theorem: (coprime 0 n <=> n = 1) /\ (coprime n 0 <=> n = 1) *)
1124(* Proof: by coprime_0L, coprime_0R *)
1125Theorem coprime_0:
1126 !n. (coprime 0 n <=> n = 1) /\ (coprime n 0 <=> n = 1)
1127Proof
1128 simp[coprime_0L, coprime_0R]
1129QED
1130
1131(* Theorem: coprime x y = coprime y x *)
1132(* Proof:
1133 coprime x y
1134 means gcd x y = 1
1135 so gcd y x = 1 by GCD_SYM
1136 thus coprime y x
1137*)
1138Theorem coprime_sym:
1139 !x y. coprime x y = coprime y x
1140Proof
1141 rw[GCD_SYM]
1142QED
1143
1144(* Theorem: coprime k n /\ n <> 1 ==> k <> 0 *)
1145(* Proof: by coprime_0L *)
1146Theorem coprime_neq_1:
1147 !n k. coprime k n /\ n <> 1 ==> k <> 0
1148Proof
1149 fs[coprime_0L]
1150QED
1151
1152(* Theorem: coprime k n /\ 1 < n ==> 0 < k *)
1153(* Proof: by coprime_neq_1 *)
1154Theorem coprime_gt_1:
1155 !n k. coprime k n /\ 1 < n ==> 0 < k
1156Proof
1157 metis_tac[coprime_neq_1, NOT_ZERO_LT_ZERO, DECIDE``~(1 < 1)``]
1158QED
1159
1160(* Note: gcd (c ** n) m = gcd c m is false when n = 0, where c ** 0 = 1. *)
1161
1162(* Theorem: coprime c m ==> !n. coprime (c ** n) m *)
1163(* Proof: by induction on n.
1164 Base case: coprime (c ** 0) m
1165 Since c ** 0 = 1 by EXP
1166 and coprime 1 m is true by GCD_1
1167 Step case: coprime c m /\ coprime (c ** n) m ==> coprime (c ** SUC n) m
1168 coprime c m means
1169 coprime m c by GCD_SYM
1170
1171 gcd m (c ** SUC n)
1172 = gcd m (c * c ** n) by EXP
1173 = gcd m (c ** n) by GCD_CANCEL_MULT, coprime m c
1174 = 1 by induction hypothesis
1175 Hence coprime m (c ** SUC n)
1176 or coprime (c ** SUC n) m by GCD_SYM
1177*)
1178Theorem coprime_exp:
1179 !c m. coprime c m ==> !n. coprime (c ** n) m
1180Proof
1181 rpt strip_tac >>
1182 Induct_on `n` >-
1183 rw[EXP, GCD_1] >>
1184 metis_tac[EXP, GCD_CANCEL_MULT, GCD_SYM]
1185QED
1186
1187(* Theorem: coprime a b ==> !n. coprime a (b ** n) *)
1188(* Proof: by coprime_exp, GCD_SYM *)
1189Theorem coprime_exp_comm:
1190 !a b. coprime a b ==> !n. coprime a (b ** n)
1191Proof
1192 metis_tac[coprime_exp, GCD_SYM]
1193QED
1194
1195(* Theorem: coprime x z /\ coprime y z ==> coprime (x * y) z *)
1196(* Proof:
1197 By GCD_CANCEL_MULT:
1198 |- !m n k. coprime m k ==> (gcd m (k * n) = gcd m n)
1199 Hence follows by coprime_sym.
1200*)
1201Theorem coprime_product_coprime:
1202 !x y z. coprime x z /\ coprime y z ==> coprime (x * y) z
1203Proof
1204 metis_tac[GCD_CANCEL_MULT, GCD_SYM]
1205QED
1206
1207(* Theorem: coprime z x /\ coprime z y ==> coprime z (x * y) *)
1208(* Proof:
1209 Note gcd z x = 1 by given
1210 ==> gcd z (x * y)
1211 = gcd z y by GCD_CANCEL_MULT
1212 = 1 by given
1213*)
1214Theorem coprime_product_coprime_sym:
1215 !x y z. coprime z x /\ coprime z y ==> coprime z (x * y)
1216Proof
1217 rw[GCD_CANCEL_MULT]
1218QED
1219(* This is the same as PRODUCT_WITH_GCD_ONE *)
1220
1221(* Theorem: coprime x z ==> (coprime y z <=> coprime (x * y) z) *)
1222(* Proof:
1223 If part: coprime x z /\ coprime y z ==> coprime (x * y) z
1224 True by coprime_product_coprime
1225 Only-if part: coprime x z /\ coprime (x * y) z ==> coprime y z
1226 Let d = gcd y z.
1227 Then d divides z /\ d divides y by GCD_PROPERTY
1228 so d divides (x * y) by DIVIDES_MULT, MULT_COMM
1229 or d divides (gcd (x * y) z) by GCD_PROPERTY
1230 d divides 1 by coprime (x * y) z
1231 ==> d = 1 by DIVIDES_ONE
1232 or coprime y z by notation
1233*)
1234Theorem coprime_product_coprime_iff:
1235 !x y z. coprime x z ==> (coprime y z <=> coprime (x * y) z)
1236Proof
1237 rw[EQ_IMP_THM] >-
1238 rw[coprime_product_coprime] >>
1239 qabbrev_tac `d = gcd y z` >>
1240 metis_tac[GCD_PROPERTY, DIVIDES_MULT, MULT_COMM, DIVIDES_ONE]
1241QED
1242
1243(* Theorem: a divides n /\ b divides n /\ coprime a b ==> (a * b) divides n *)
1244(* Proof: by LCM_COPRIME, LCM_DIVIDES *)
1245Theorem coprime_product_divides:
1246 !n a b. a divides n /\ b divides n /\ coprime a b ==> (a * b) divides n
1247Proof
1248 metis_tac[LCM_COPRIME, LCM_DIVIDES]
1249QED
1250
1251(* Theorem: 0 < m /\ coprime m n ==> coprime m (n MOD m) *)
1252(* Proof:
1253 gcd m n
1254 = if m = 0 then n else gcd (n MOD m) m by GCD_EFFICIENTLY
1255 = gcd (n MOD m) m by decide_tac, m <> 0
1256 = gcd m (n MOD m) by GCD_SYM
1257 Hence true since coprime m n <=> gcd m n = 1.
1258*)
1259Theorem coprime_mod:
1260 !m n. 0 < m /\ coprime m n ==> coprime m (n MOD m)
1261Proof
1262 metis_tac[GCD_EFFICIENTLY, GCD_SYM, NOT_ZERO_LT_ZERO]
1263QED
1264
1265(* Theorem: 0 < m ==> (coprime m n = coprime m (n MOD m)) *)
1266(* Proof: by GCD_MOD *)
1267Theorem coprime_mod_iff:
1268 !m n. 0 < m ==> (coprime m n = coprime m (n MOD m))
1269Proof
1270 rw[Once GCD_MOD]
1271QED
1272
1273(* Theorem: 1 < n /\ coprime n k /\ 1 < p /\ p divides n ==> ~(p divides k) *)
1274(* Proof:
1275 First, 1 < n ==> n <> 0 and n <> 1
1276 If k = 0, gcd n k = n by GCD_0R
1277 But coprime n k means gcd n k = 1, so k <> 0.
1278 By contradiction.
1279 If p divides k, and given p divides n,
1280 then p divides gcd n k = 1 by GCD_IS_GREATEST_COMMON_DIVISOR, n≠0 and k≠0
1281 or p = 1 by DIVIDES_ONE
1282 which contradicts 1 < p.
1283*)
1284Theorem coprime_factor_not_divides:
1285 !n k. 1 < n /\ coprime n k ==> !p. 1 < p /\ p divides n ==> ~(p divides k)
1286Proof
1287 rpt strip_tac >>
1288 `n <> 0 /\ n <> 1 /\ p <> 1` by decide_tac >>
1289 metis_tac[GCD_IS_GREATEST_COMMON_DIVISOR, DIVIDES_ONE, GCD_0R]
1290QED
1291
1292(* Theorem: m divides n ==> !k. coprime n k ==> coprime m k *)
1293(* Proof:
1294 Let d = gcd m k.
1295 Then d divides m /\ d divides k by GCD_IS_GREATEST_COMMON_DIVISOR
1296 ==> d divides n by DIVIDES_TRANS
1297 so d divides 1 by GCD_IS_GREATEST_COMMON_DIVISOR,
1298 coprime n k
1299 ==> d = 1 by DIVIDES_ONE
1300*)
1301Theorem coprime_factor_coprime:
1302 !m n. m divides n ==> !k. coprime n k ==> coprime m k
1303Proof
1304 rpt strip_tac >>
1305 qabbrev_tac `d = gcd m k` >>
1306 `d divides m /\ d divides k` by rw[GCD_IS_GREATEST_COMMON_DIVISOR, Abbr`d`] >>
1307 `d divides n` by metis_tac[DIVIDES_TRANS] >>
1308 `d divides 1` by metis_tac[GCD_IS_GREATEST_COMMON_DIVISOR] >>
1309 rw[GSYM DIVIDES_ONE]
1310QED
1311
1312(* Idea: common factor of two coprime numbers. *)
1313
1314(* Theorem: coprime a b /\ c divides a /\ c divides b ==> c = 1 *)
1315(* Proof:
1316 Note c divides gcd a b by GCD_PROPERTY
1317 or c divides 1 by coprime a b
1318 so c = 1 by DIVIDES_ONE
1319*)
1320Theorem coprime_common_factor:
1321 !a b c. coprime a b /\ c divides a /\ c divides b ==> c = 1
1322Proof
1323 metis_tac[GCD_PROPERTY, DIVIDES_ONE]
1324QED
1325
1326(* Theorem: prime p /\ ~(p divides n) ==> coprime p n *)
1327(* Proof:
1328 Since divides p 0, so n <> 0. by ALL_DIVIDES_0
1329 If n = 1, certainly coprime p n by GCD_1
1330 If n <> 1,
1331 Let gcd p n = d.
1332 Since d divides p by GCD_IS_GREATEST_COMMON_DIVISOR
1333 and prime p by given
1334 so d = 1 or d = p by prime_def
1335 but d <> p by divides_iff_gcd_fix
1336 Hence d = 1, or coprime p n.
1337*)
1338Theorem prime_not_divides_coprime:
1339 !n p. prime p /\ ~(p divides n) ==> coprime p n
1340Proof
1341 rpt strip_tac >>
1342 `n <> 0` by metis_tac[ALL_DIVIDES_0] >>
1343 Cases_on `n = 1` >-
1344 rw[] >>
1345 `0 < p` by rw[PRIME_POS] >>
1346 `p <> 0` by decide_tac >>
1347 metis_tac[prime_def, divides_iff_gcd_fix, GCD_IS_GREATEST_COMMON_DIVISOR]
1348QED
1349
1350(* Theorem: prime p /\ ~(coprime p n) ==> p divides n *)
1351(* Proof:
1352 Let d = gcd p n.
1353 Then d divides p by GCD_IS_GREATEST_COMMON_DIVISOR
1354 ==> d = p by prime_def
1355 Thus p divides n by divides_iff_gcd_fix
1356
1357 Or: this is just the inverse of prime_not_divides_coprime.
1358*)
1359Theorem prime_not_coprime_divides:
1360 !n p. prime p /\ ~(coprime p n) ==> p divides n
1361Proof
1362 metis_tac[prime_not_divides_coprime]
1363QED
1364
1365(* Proof:
1366 Since coprime n k /\ p divides n
1367 ==> ~(p divides k) by coprime_factor_not_divides
1368 Then prime p /\ ~(p divides k)
1369 ==> coprime p k by prime_not_divides_coprime
1370*)
1371Theorem coprime_prime_factor_coprime:
1372 !n p. 1 < n /\ prime p /\ p divides n ==> !k. coprime n k ==> coprime p k
1373Proof
1374 metis_tac[coprime_factor_not_divides, prime_not_divides_coprime, ONE_LT_PRIME]
1375QED
1376
1377(* This is better:
1378coprime_factor_coprime
1379|- !m n. m divides n ==> !k. coprime n k ==> coprime m k
1380*)
1381
1382(* Idea: a characterisation of the coprime property of two numbers. *)
1383
1384(* Theorem: coprime m n <=> !p. prime p ==> ~(p divides m /\ p divides n) *)
1385(* Proof:
1386 If part: coprime m n /\ prime p ==> ~(p divides m) \/ ~(p divides n)
1387 By contradiction, suppose p divides m /\ p divides n.
1388 Then p = 1 by coprime_common_factor
1389 This contradicts prime p by NOT_PRIME_1
1390 Only-if part:
1391 !p. prime p ==> ~(p divides m) \/ ~(p divides m) ==> coprime m n
1392 Let d = gcd m n.
1393 By contradiction, suppose d <> 1.
1394 Then ?p. prime p /\ p divides d by PRIME_FACTOR, d <> 1.
1395 Now d divides m /\ d divides n by GCD_PROPERTY
1396 so p divides m /\ p divides n by DIVIDES_TRANS
1397 This contradicts the assumption.
1398*)
1399Theorem coprime_by_prime_factor:
1400 !m n. coprime m n <=> !p. prime p ==> ~(p divides m /\ p divides n)
1401Proof
1402 rw[EQ_IMP_THM] >-
1403 metis_tac[coprime_common_factor, NOT_PRIME_1] >>
1404 qabbrev_tac `d = gcd m n` >>
1405 spose_not_then strip_assume_tac >>
1406 `?p. prime p /\ p divides d` by rw[PRIME_FACTOR] >>
1407 `d divides m /\ d divides n` by metis_tac[GCD_PROPERTY] >>
1408 metis_tac[DIVIDES_TRANS]
1409QED
1410
1411(* Idea: coprime_by_prime_factor with reduced testing of primes, useful in
1412 practice. *)
1413
1414(* Theorem: 0 < m /\ 0 < n ==>
1415 (coprime m n <=>
1416 !p. prime p /\ p <= m /\ p <= n ==> ~(p divides m /\ p divides n)) *)
1417(* Proof:
1418 If part: coprime m n /\ prime p /\ ... ==> ~(p divides m) \/ ~(p divides n)
1419 By contradiction, suppose p divides m /\ p divides n.
1420 Then p = 1 by coprime_common_factor
1421 This contradicts prime p by NOT_PRIME_1
1422 Only-if part: !p. prime p /\ p <= m /\ p <= n ==>
1423 ~(p divides m) \/ ~(p divides m) ==> coprime m n
1424 Let d = gcd m n.
1425 By contradiction, suppose d <> 1.
1426 Then ?p. prime p /\ p divides d by PRIME_FACTOR, d <> 1.
1427 Now d divides m /\ d divides n by GCD_PROPERTY
1428 so p divides m /\ p divides n by DIVIDES_TRANS
1429 Thus p <= m /\ p <= n by DIVIDES_LE, 0 < m, 0 < n
1430 This contradicts the assumption.
1431*)
1432Theorem coprime_by_prime_factor_le:
1433 !m n. 0 < m /\ 0 < n ==>
1434 (coprime m n <=>
1435 !p. prime p /\ p <= m /\ p <= n ==> ~(p divides m /\ p divides n))
1436Proof
1437 rw[EQ_IMP_THM] >-
1438 metis_tac[coprime_common_factor, NOT_PRIME_1] >>
1439 qabbrev_tac `d = gcd m n` >>
1440 spose_not_then strip_assume_tac >>
1441 `?p. prime p /\ p divides d` by rw[PRIME_FACTOR] >>
1442 `d divides m /\ d divides n` by metis_tac[GCD_PROPERTY] >>
1443 `0 < p` by rw[PRIME_POS] >>
1444 metis_tac[DIVIDES_TRANS, DIVIDES_LE]
1445QED
1446
1447(* Note: counter-example for converse: gcd 3 11 = 1, but ~(3 divides 10). *)
1448
1449(* Theorem: 0 < m /\ n divides m ==> coprime n (PRE m) *)
1450(* Proof:
1451 Since n divides m
1452 ==> ?q. m = q * n by divides_def
1453 Also 0 < m means m <> 0,
1454 ==> ?k. m = SUC k by num_CASES
1455 = k + 1 by ADD1
1456 so m - k = 1, k = PRE m.
1457 Let d = gcd n k.
1458 Then d divides n /\ d divides k by GCD_IS_GREATEST_COMMON_DIVISOR
1459 and d divides n ==> d divides m by DIVIDES_MULTIPLE, m = q * n
1460 so d divides (m - k) by DIVIDES_SUB
1461 or d divides 1 by m - k = 1
1462 ==> d = 1 by DIVIDES_ONE
1463*)
1464Theorem divides_imp_coprime_with_predecessor:
1465 !m n. 0 < m /\ n divides m ==> coprime n (PRE m)
1466Proof
1467 rpt strip_tac >>
1468 `?q. m = q * n` by rw[GSYM divides_def] >>
1469 `m <> 0` by decide_tac >>
1470 `?k. m = k + 1` by metis_tac[num_CASES, ADD1] >>
1471 `(k = PRE m) /\ (m - k = 1)` by decide_tac >>
1472 qabbrev_tac `d = gcd n k` >>
1473 `d divides n /\ d divides k` by rw[GCD_IS_GREATEST_COMMON_DIVISOR, Abbr`d`] >>
1474 `d divides m` by rw[DIVIDES_MULTIPLE] >>
1475 `d divides (m - k)` by rw[DIVIDES_SUB] >>
1476 metis_tac[DIVIDES_ONE]
1477QED
1478
1479(* Theorem: coprime p n ==> (gcd (p * m) n = gcd m n) *)
1480(* Proof:
1481 Note coprime p n means coprime n p by GCD_SYM
1482 gcd (p * m) n
1483 = gcd n (p * m) by GCD_SYM
1484 = gcd n p by GCD_CANCEL_MULT
1485*)
1486Theorem gcd_coprime_cancel:
1487 !m n p. coprime p n ==> (gcd (p * m) n = gcd m n)
1488Proof
1489 rw[GCD_CANCEL_MULT, GCD_SYM]
1490QED
1491
1492(* The following is a direct, but tricky, proof of the above result *)
1493
1494(* Theorem: coprime p n ==> (gcd (p * m) n = gcd m n) *)
1495(* Proof:
1496 gcd (p * m) n
1497 = gcd (p * m) (n * 1) by MULT_RIGHT_1
1498 = gcd (p * m) (n * (gcd m 1)) by GCD_1
1499 = gcd (p * m) (gcd (n * m) n) by GCD_COMMON_FACTOR
1500 = gcd (gcd (p * m) (n * m)) n by GCD_ASSOC
1501 = gcd (m * (gcd p n)) n by GCD_COMMON_FACTOR, MULT_COMM
1502 = gcd (m * 1) n by coprime p n
1503 = gcd m n by MULT_RIGHT_1
1504
1505 Simple proof of GCD_CANCEL_MULT:
1506 (a*c, b) = (a*c , b*1) = (a * c, b * (c, 1)) = (a * c, b * c, b) =
1507 ((a, b) * c, b) = (c, b) since (a,b) = 1.
1508*)
1509Theorem gcd_coprime_cancel[allow_rebind]:
1510 !m n p. coprime p n ==> (gcd (p * m) n = gcd m n)
1511Proof
1512 rpt strip_tac >>
1513 ‘gcd (p * m) n = gcd (p * m) (n * (gcd m 1))’ by rw[GCD_1] >>
1514 ‘_ = gcd (p * m) (gcd (n * m) n)’ by rw[GSYM GCD_COMMON_FACTOR] >>
1515 ‘_ = gcd (gcd (p * m) (n * m)) n’ by rw[GCD_ASSOC] >>
1516 ‘_ = gcd m n’ by rw[GCD_COMMON_FACTOR, MULT_COMM] >>
1517 rw[]
1518QED
1519
1520(* Theorem: prime p /\ prime q /\ p <> q ==> coprime p q *)
1521(* Proof:
1522 Let d = gcd p q.
1523 By contradiction, suppose d <> 1.
1524 Then d divides p /\ d divides q by GCD_PROPERTY
1525 so d = 1 or d = p by prime_def
1526 and d = 1 or d = q by prime_def
1527 But p <> q by given
1528 so d = 1, contradicts d <> 1.
1529*)
1530Theorem primes_coprime:
1531 !p q. prime p /\ prime q /\ p <> q ==> coprime p q
1532Proof
1533 spose_not_then strip_assume_tac >>
1534 qabbrev_tac `d = gcd p q` >>
1535 `d divides p /\ d divides q` by metis_tac[GCD_PROPERTY] >>
1536 metis_tac[prime_def]
1537QED
1538
1539(* Theorem: prime p ==> p cannot divide k! for p > k.
1540 prime p /\ k < p ==> ~(p divides (FACT k)) *)
1541(* Proof:
1542 Since all terms of k! are less than p, and p has only 1 and p as factor.
1543 By contradiction, and induction on k.
1544 Base case: prime p ==> 0 < p ==> p divides (FACT 0) ==> F
1545 Since FACT 0 = 1 by FACT
1546 and p divides 1 <=> p = 1 by DIVIDES_ONE
1547 but prime p ==> 1 < p by ONE_LT_PRIME
1548 so this is a contradiction.
1549 Step case: prime p /\ k < p ==> p divides (FACT k) ==> F ==>
1550 SUC k < p ==> p divides (FACT (SUC k)) ==> F
1551 Since FACT (SUC k) = SUC k * FACT k by FACT
1552 and prime p /\ p divides (FACT (SUC k))
1553 ==> p divides (SUC k),
1554 or p divides (FACT k) by P_EUCLIDES
1555 But SUC k < p, so ~(p divides (SUC k)) by NOT_LT_DIVIDES
1556 Hence p divides (FACT k) ==> F by induction hypothesis
1557*)
1558Theorem PRIME_BIG_NOT_DIVIDES_FACT:
1559 !p k. prime p /\ k < p ==> ~(p divides (FACT k))
1560Proof
1561 (spose_not_then strip_assume_tac) >>
1562 Induct_on `k` >| [
1563 rw[FACT] >>
1564 metis_tac[ONE_LT_PRIME, LESS_NOT_EQ],
1565 rw[FACT] >>
1566 (spose_not_then strip_assume_tac) >>
1567 `k < p /\ 0 < SUC k` by decide_tac >>
1568 metis_tac[P_EUCLIDES, NOT_LT_DIVIDES]
1569 ]
1570QED
1571
1572(* Theorem: n divides m ==> coprime n (SUC m) *)
1573(* Proof:
1574 If n = 0,
1575 then m = 0 by ZERO_DIVIDES
1576 gcd 0 (SUC 0)
1577 = SUC 0 by GCD_0L
1578 = 1 by ONE
1579 If n = 1,
1580 gcd 1 (SUC m) = 1 by GCD_1
1581 If n <> 0,
1582 gcd n (SUC m)
1583 = gcd ((SUC m) MOD n) n by GCD_EFFICIENTLY
1584 = gcd 1 n by n divides m
1585 = 1 by GCD_1
1586*)
1587Theorem divides_imp_coprime_with_successor:
1588 !m n. n divides m ==> coprime n (SUC m)
1589Proof
1590 rpt strip_tac >>
1591 Cases_on `n = 0` >-
1592 rw[GSYM ZERO_DIVIDES] >>
1593 Cases_on `n = 1` >-
1594 rw[] >>
1595 `0 < n /\ 1 < n` by decide_tac >>
1596 `m MOD n = 0` by rw[GSYM DIVIDES_MOD_0] >>
1597 `(SUC m) MOD n = (m + 1) MOD n` by rw[ADD1] >>
1598 `_ = (m MOD n + 1 MOD n) MOD n` by rw[MOD_PLUS] >>
1599 `_ = (0 + 1) MOD n` by rw[ONE_MOD] >>
1600 `_ = 1` by rw[ONE_MOD] >>
1601 metis_tac[GCD_EFFICIENTLY, GCD_1]
1602QED
1603
1604(* ------------------------------------------------------------------------- *)
1605(* Consequences of Coprime. *)
1606(* ------------------------------------------------------------------------- *)
1607
1608(* Theorem: If 1 < n, !x. coprime n x ==> 0 < x /\ 0 < x MOD n *)
1609(* Proof:
1610 If x = 0, gcd n x = n. But n <> 1, hence x <> 0, or 0 < x.
1611 x MOD n = 0 ==> x a multiple of n ==> gcd n x = n <> 1 if n <> 1.
1612 Hence if 1 < n, coprime n x ==> x MOD n <> 0, or 0 < x MOD n.
1613*)
1614Theorem MOD_NONZERO_WHEN_GCD_ONE:
1615 !n. 1 < n ==> !x. coprime n x ==> 0 < x /\ 0 < x MOD n
1616Proof
1617 ntac 4 strip_tac >>
1618 conj_asm1_tac >| [
1619 `1 <> n` by decide_tac >>
1620 `x <> 0` by metis_tac[GCD_0R] >>
1621 decide_tac,
1622 `1 <> n /\ x <> 0` by decide_tac >>
1623 `?k q. k * x = q * n + 1` by metis_tac[LINEAR_GCD] >>
1624 `(k*x) MOD n = 1` by rw_tac std_ss[MOD_MULT] >>
1625 spose_not_then strip_assume_tac >>
1626 `(x MOD n = 0) /\ 0 < n /\ 1 <> 0` by decide_tac >>
1627 metis_tac[MOD_MULTIPLE_ZERO, MULT_COMM]
1628 ]
1629QED
1630
1631(* Theorem: If 1 < n, coprime n x ==> ?k. ((k * x) MOD n = 1) /\ coprime n k *)
1632(* Proof:
1633 gcd n x = 1 ==> x <> 0 by GCD_0R
1634 Also,
1635 gcd n x = 1
1636 ==> ?k q. k * x = q * n + 1 by LINEAR_GCD
1637 ==> (k * x) MOD n = (q * n + 1) MOD n by arithmetic
1638 ==> (k * x) MOD n = 1 by MOD_MULT, 1 < n.
1639
1640 Let g = gcd n k.
1641 Since 1 < n, 0 < n.
1642 Since q * n+1 <> 0, x <> 0, k <> 0, hence 0 < k.
1643 Hence 0 < g /\ (n MOD g = 0) /\ (k MOD g = 0) by GCD_DIVIDES.
1644 Or n = a * g /\ k = b * g for some a, b.
1645 Therefore:
1646 (b * g) * x = q * (a * g) + 1
1647 (b * x) * g = (q * a) * g + 1 by arithmetic
1648 Hence g divides 1, or g = 1 since 0 < g.
1649*)
1650Theorem GCD_ONE_PROPERTY:
1651 !n x. 1 < n /\ coprime n x ==> ?k. ((k * x) MOD n = 1) /\ coprime n k
1652Proof
1653 rpt strip_tac >>
1654 `n <> 1` by decide_tac >>
1655 `x <> 0` by metis_tac[GCD_0R] >>
1656 `?k q. k * x = q * n + 1` by metis_tac[LINEAR_GCD] >>
1657 `(k * x) MOD n = 1` by rw_tac std_ss[MOD_MULT] >>
1658 `?g. g = gcd n k` by rw[] >>
1659 `n <> 0 /\ q*n + 1 <> 0` by decide_tac >>
1660 `k <> 0` by metis_tac[MULT_EQ_0] >>
1661 `0 < g /\ (n MOD g = 0) /\ (k MOD g = 0)`
1662 by metis_tac[GCD_DIVIDES, NOT_ZERO_LT_ZERO] >>
1663 `g divides n /\ g divides k` by rw[DIVIDES_MOD_0] >>
1664 `g divides (n * q) /\ g divides (k*x)` by rw[DIVIDES_MULT] >>
1665 `g divides (n * q + 1)` by metis_tac [MULT_COMM] >>
1666 `g divides 1` by metis_tac[DIVIDES_ADD_2] >>
1667 metis_tac[DIVIDES_ONE]
1668QED
1669
1670(* Theorem: LCM (k * m) (k * n) = k * LCM m n *)
1671(* Proof:
1672 If m = 0 or n = 0, LHS = 0 = RHS.
1673 If m <> 0 and n <> 0,
1674 lcm (k * m) (k * n)
1675 = (k * m) * (k * n) / gcd (k * m) (k * n) by GCD_LCM
1676 = (k * m) * (k * n) / k * (gcd m n) by GCD_COMMON_FACTOR
1677 = k * m * n / (gcd m n)
1678 = k * LCM m n by GCD_LCM
1679*)
1680Theorem LCM_COMMON_FACTOR:
1681 !m n k. lcm (k * m) (k * n) = k * lcm m n
1682Proof
1683 rpt strip_tac >>
1684 `k * (k * (m * n)) = (k * m) * (k * n)` by rw_tac arith_ss[] >>
1685 `_ = gcd (k * m) (k * n) * lcm (k * m) (k * n) ` by rw[GCD_LCM] >>
1686 `_ = k * (gcd m n) * lcm (k * m) (k * n)` by rw[GCD_COMMON_FACTOR] >>
1687 `_ = k * ((gcd m n) * lcm (k * m) (k * n))` by rw_tac arith_ss[] >>
1688 Cases_on `k = 0` >-
1689 rw[] >>
1690 `(gcd m n) * lcm (k * m) (k * n) = k * (m * n)`
1691 by metis_tac[MULT_LEFT_CANCEL] >>
1692 `_ = k * ((gcd m n) * (lcm m n))` by rw_tac std_ss[GCD_LCM] >>
1693 `_ = (gcd m n) * (k * (lcm m n))` by rw_tac arith_ss[] >>
1694 Cases_on `n = 0` >-
1695 rw[] >>
1696 metis_tac[MULT_LEFT_CANCEL, GCD_EQ_0]
1697QED
1698
1699(* Theorem: coprime a b ==> !c. lcm (a * c) (b * c) = a * b * c *)
1700(* Proof:
1701 lcm (a * c) (b * c)
1702 = lcm (c * a) (c * b) by MULT_COMM
1703 = c * (lcm a b) by LCM_COMMON_FACTOR
1704 = (lcm a b) * c by MULT_COMM
1705 = a * b * c by LCM_COPRIME
1706*)
1707Theorem LCM_COMMON_COPRIME:
1708 !a b. coprime a b ==> !c. lcm (a * c) (b * c) = a * b * c
1709Proof
1710 metis_tac[LCM_COMMON_FACTOR, LCM_COPRIME, MULT_COMM]
1711QED
1712
1713(* Theorem: 0 < n /\ m MOD n = 0 ==> gcd m n = n *)
1714(* Proof:
1715 Since m MOD n = 0
1716 ==> n divides m by DIVIDES_MOD_0
1717 Hence gcd m n = gcd n m by GCD_SYM
1718 = n by divides_iff_gcd_fix
1719*)
1720Theorem GCD_MULTIPLE:
1721 !m n. 0 < n /\ (m MOD n = 0) ==> (gcd m n = n)
1722Proof
1723 metis_tac[DIVIDES_MOD_0, divides_iff_gcd_fix, GCD_SYM]
1724QED
1725
1726(* Theorem: gcd (m * n) n = n *)
1727(* Proof:
1728 gcd (m * n) n
1729 = gcd (n * m) n by MULT_COMM
1730 = gcd (n * m) (n * 1) by MULT_RIGHT_1
1731 = n * (gcd m 1) by GCD_COMMON_FACTOR
1732 = n * 1 by GCD_1
1733 = n by MULT_RIGHT_1
1734*)
1735Theorem GCD_MULTIPLE_ALT:
1736 !m n. gcd (m * n) n = n
1737Proof
1738 rpt strip_tac >>
1739 `gcd (m * n) n = gcd (n * m) n` by rw[MULT_COMM] >>
1740 `_ = gcd (n * m) (n * 1)` by rw[] >>
1741 rw[GCD_COMMON_FACTOR]
1742QED
1743
1744(* ------------------------------------------------------------------------- *)
1745(* Modulo Theorems *)
1746(* ------------------------------------------------------------------------- *)
1747
1748(* Idea: eliminate modulus n when a MOD n = b MOD n. *)
1749
1750(* Theorem: 0 < n /\ b <= a ==> (a MOD n = b MOD n <=> ?c. a = b + c * n) *)
1751(* Proof:
1752 If part: a MOD n = b MOD n ==> ?c. a = b + c * n
1753 Note ?c. a = c * n + b MOD n by MOD_EQN
1754 and b = (b DIV n) * n + b MOD n by DIVISION
1755 Let q = b DIV n,
1756 Then q * n <= c * n by LE_ADD_RCANCEL, b <= a
1757 a
1758 = c * n + (b - q * n) by above
1759 = b + (c * n - q * n) by arithmetic, q * n <= c * n
1760 = b + (c - q) * n by RIGHT_SUB_DISTRIB
1761 Take (c - q) as c.
1762 Only-if part: (b + c * n) MOD n = b MOD n
1763 This is true by MOD_TIMES
1764*)
1765Theorem MOD_MOD_EQN:
1766 !n a b. 0 < n /\ b <= a ==> (a MOD n = b MOD n <=> ?c. a = b + c * n)
1767Proof
1768 rw[EQ_IMP_THM] >| [
1769 `?c. a = c * n + b MOD n` by metis_tac[MOD_EQN] >>
1770 `b = (b DIV n) * n + b MOD n` by rw[DIVISION] >>
1771 qabbrev_tac `q = b DIV n` >>
1772 `q * n <= c * n` by metis_tac[LE_ADD_RCANCEL] >>
1773 `a = b + (c * n - q * n)` by decide_tac >>
1774 `_ = b + (c - q) * n` by decide_tac >>
1775 metis_tac[],
1776 simp[]
1777 ]
1778QED
1779
1780(* Idea: a convenient form of MOD_PLUS. *)
1781
1782(* Theorem: 0 < n ==> (x + y) MOD n = (x + y MOD n) MOD n *)
1783(* Proof:
1784 Let q = y DIV n, r = y MOD n.
1785 Then y = q * n + r by DIVISION, 0 < n
1786 (x + y) MOD n
1787 = (x + (q * n + r)) MOD n by above
1788 = (q * n + (x + r)) MOD n by arithmetic
1789 = (x + r) MOD n by MOD_PLUS, MOD_EQ_0
1790*)
1791Theorem MOD_PLUS2:
1792 !n x y. 0 < n ==> (x + y) MOD n = (x + y MOD n) MOD n
1793Proof
1794 rpt strip_tac >>
1795 `y = (y DIV n) * n + y MOD n` by metis_tac[DIVISION] >>
1796 simp[]
1797QED
1798
1799(* Theorem: If n > 0, a MOD n = b MOD n ==> (a - b) MOD n = 0 *)
1800(* Proof:
1801 a = (a DIV n)*n + (a MOD n) by DIVISION
1802 b = (b DIV n)*n + (b MOD n) by DIVISION
1803 Hence a - b = ((a DIV n) - (b DIV n))* n
1804 = a multiple of n
1805 Therefore (a - b) MOD n = 0.
1806*)
1807Theorem MOD_EQ_DIFF:
1808 !n a b. 0 < n /\ (a MOD n = b MOD n) ==> ((a - b) MOD n = 0)
1809Proof
1810 rpt strip_tac >>
1811 `a = a DIV n * n + a MOD n` by metis_tac[DIVISION] >>
1812 `b = b DIV n * n + b MOD n` by metis_tac[DIVISION] >>
1813 `a - b = (a DIV n - b DIV n) * n` by rw_tac arith_ss[] >>
1814 metis_tac[MOD_EQ_0]
1815QED
1816(* Note: The reverse is true only when a >= b:
1817 (a-b) MOD n = 0 cannot imply a MOD n = b MOD n *)
1818
1819(* Theorem: if n > 0, a >= b, then (a - b) MOD n = 0 <=> a MOD n = b MOD n *)
1820(* Proof:
1821 (a-b) MOD n = 0
1822 ==> n divides (a-b) by MOD_0_DIVIDES
1823 ==> (a-b) = k*n for some k by divides_def
1824 ==> a = b + k*n need b <= a to apply arithmeticTheory.SUB_ADD
1825 ==> a MOD n = b MOD n by arithmeticTheory.MOD_TIMES
1826
1827 The converse is given by MOD_EQ_DIFF.
1828*)
1829Theorem MOD_EQ:
1830 !n a b. 0 < n /\ b <= a ==> (((a - b) MOD n = 0) <=> (a MOD n = b MOD n))
1831Proof
1832 rw[EQ_IMP_THM] >| [
1833 `?k. a - b = k * n` by metis_tac[DIVIDES_MOD_0, divides_def] >>
1834 `a = k*n + b` by rw_tac arith_ss[] >>
1835 metis_tac[MOD_TIMES],
1836 metis_tac[MOD_EQ_DIFF]
1837 ]
1838QED
1839
1840(* Theorem:
1841 [Euclid's Lemma] A prime a divides product iff the prime a divides factor.
1842 [in MOD notation] For prime p, x*y MOD p = 0 <=> x MOD p = 0 or y MOD p = 0
1843*)
1844(* Proof:
1845 The if part is already in P_EUCLIDES:
1846 !p a b. prime p /\ divides p (a * b) ==> p divides a \/ p divides b
1847 Convert the divides to MOD by DIVIDES_MOD_0.
1848 The only-if part is:
1849 (1) divides p x ==> divides p (x * y)
1850 (2) divides p y ==> divides p (x * y)
1851 Both are true by DIVIDES_MULT: !a b c. a divides b ==> a divides (b * c).
1852 The symmetry of x and y can be taken care of by MULT_COMM.
1853*)
1854Theorem EUCLID_LEMMA:
1855 !p x y. prime p ==> (((x * y) MOD p = 0) <=> (x MOD p = 0) \/ (y MOD p = 0))
1856Proof
1857 rpt strip_tac >>
1858 `0 < p` by rw[PRIME_POS] >>
1859 rw[GSYM DIVIDES_MOD_0, EQ_IMP_THM] >>
1860 metis_tac[P_EUCLIDES, DIVIDES_MULT, MULT_COMM]
1861QED
1862
1863(* Idea: For prime p, FACT (p-1) MOD p <> 0 *)
1864
1865(* Theorem: prime p /\ n < p ==> FACT n MOD p <> 0 *)
1866(* Proof:
1867 Note 1 < p by ONE_LT_PRIME
1868 By induction on n.
1869 Base: 0 < p ==> (FACT 0 MOD p = 0) ==> F
1870 Note FACT 0 = 1 by FACT_0
1871 and 1 MOD p = 1 by LESS_MOD, 1 < p
1872 and 1 = 0 is F.
1873 Step: n < p ==> (FACT n MOD p = 0) ==> F ==>
1874 SUC n < p ==> (FACT (SUC n) MOD p = 0) ==> F
1875 If n = 0, SUC 0 = 1 by ONE
1876 Note FACT 1 = 1 by FACT_1
1877 and 1 MOD p = 1 by LESS_MOD, 1 < p
1878 and 1 = 0 is F.
1879 If n <> 0, 0 < n.
1880 (FACT (SUC n)) MOD p = 0
1881 <=> (SUC n * FACT n) MOD p = 0 by FACT
1882 Note (SUC n) MOD p <> 0 by MOD_LESS, SUC n < p
1883 and (FACT n) MOD p <> 0 by induction hypothesis
1884 so (SUC n * FACT n) MOD p <> 0 by EUCLID_LEMMA
1885 This is a contradiction.
1886*)
1887Theorem FACT_MOD_PRIME:
1888 !p n. prime p /\ n < p ==> FACT n MOD p <> 0
1889Proof
1890 rpt strip_tac >>
1891 `1 < p` by rw[ONE_LT_PRIME] >>
1892 Induct_on `n` >-
1893 simp[FACT_0] >>
1894 Cases_on `n = 0` >-
1895 simp[FACT_1] >>
1896 rw[FACT] >>
1897 `n < p` by decide_tac >>
1898 `(SUC n) MOD p <> 0` by fs[] >>
1899 metis_tac[EUCLID_LEMMA]
1900QED