]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/library/nat/gcd.ma
fixed, it seems the new handling of hints in some rare cases made inference stupid
[helm.git] / helm / software / matita / library / nat / gcd.ma
1 (**************************************************************************)
2 (*       ___                                                                *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
8 (*      ||A||       E.Tassi, S.Zacchiroli                                 *)
9 (*      \   /                                                             *)
10 (*       \ /        Matita is distributed under the terms of the          *)
11 (*        v         GNU Lesser General Public License Version 2.1         *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 include "nat/primes.ma".
16 include "nat/lt_arith.ma".
17
18 let rec gcd_aux p m n: nat \def
19 match divides_b n m with
20 [ true \Rightarrow n
21 | false \Rightarrow 
22   match p with
23   [O \Rightarrow n
24   |(S q) \Rightarrow gcd_aux q n (m \mod n)]].
25   
26 definition gcd : nat \to nat \to nat \def
27 \lambda n,m:nat.
28   match leb n m with
29   [ true \Rightarrow 
30     match n with 
31     [ O \Rightarrow m
32     | (S p) \Rightarrow gcd_aux (S p) m (S p) ]
33   | false \Rightarrow 
34     match m with 
35     [ O \Rightarrow n
36     | (S p) \Rightarrow gcd_aux (S p) n (S p) ]].
37
38 theorem divides_mod: \forall p,m,n:nat. O < n \to p \divides m \to p \divides n \to
39 p \divides (m \mod n).
40 intros.elim H1.elim H2.
41 (* apply (witness ? ? (n2 - n1*(m / n))). *)
42 apply witness[|
43 rewrite > distr_times_minus.
44 rewrite < H3 in \vdash (? ? ? (? % ?)).
45 rewrite < assoc_times.
46 rewrite < H4 in \vdash (? ? ? (? ? (? % ?))).
47 apply sym_eq.apply plus_to_minus.
48 rewrite > sym_times.
49 letin x \def div.
50 rewrite < (div_mod ? ? H).
51 reflexivity.
52 ]
53 qed.
54
55 theorem divides_mod_to_divides: \forall p,m,n:nat. O < n \to
56 p \divides (m \mod n) \to p \divides n \to p \divides m. 
57 intros.elim H1.elim H2.
58 apply (witness p m ((n2*(m / n))+n1)).
59 rewrite > distr_times_plus.
60 rewrite < H3.
61 rewrite < assoc_times.
62 rewrite < H4.rewrite < sym_times.
63 apply div_mod.assumption.
64 qed.
65
66 theorem divides_gcd_aux_mn: \forall p,m,n. O < n \to n \le m \to n \le p \to
67 gcd_aux p m n \divides m \land gcd_aux p m n \divides n. 
68 intro.elim p.
69 absurd (O < n).assumption.apply le_to_not_lt.assumption.
70 cut ((n1 \divides m) \lor (n1 \ndivides m)).
71 simplify.
72 elim Hcut.rewrite > divides_to_divides_b_true.
73 simplify.
74 split.assumption.apply (witness n1 n1 (S O)).apply times_n_SO.
75 assumption.assumption.
76 rewrite > not_divides_to_divides_b_false.
77 simplify.
78 cut (gcd_aux n n1 (m \mod n1) \divides n1 \land
79 gcd_aux n n1 (m \mod n1) \divides mod m n1).
80 elim Hcut1.
81 split.apply (divides_mod_to_divides ? ? n1).
82 assumption.assumption.assumption.assumption.
83 apply H.
84 cut (O \lt m \mod n1 \lor O = mod m n1).
85 elim Hcut1.assumption.
86 apply False_ind.apply H4.apply mod_O_to_divides.
87 assumption.apply sym_eq.assumption.
88 apply le_to_or_lt_eq.apply le_O_n.
89 apply lt_to_le.
90 apply lt_mod_m_m.assumption.
91 apply le_S_S_to_le.
92 apply (trans_le ? n1).
93 change with (m \mod n1 < n1).
94 apply lt_mod_m_m.assumption.assumption.
95 assumption.assumption.
96 apply (decidable_divides n1 m).assumption.
97 qed.
98
99 theorem divides_gcd_nm: \forall n,m.
100 gcd n m \divides m \land gcd n m \divides n.
101 intros.
102 change with
103 (match leb n m with
104   [ true \Rightarrow 
105     match n with 
106     [ O \Rightarrow m
107     | (S p) \Rightarrow gcd_aux (S p) m (S p) ]
108   | false \Rightarrow 
109     match m with 
110     [ O \Rightarrow n
111     | (S p) \Rightarrow gcd_aux (S p) n (S p) ] ] \divides m
112 \land
113 match leb n m with
114   [ true \Rightarrow 
115     match n with 
116     [ O \Rightarrow m
117     | (S p) \Rightarrow gcd_aux (S p) m (S p) ]
118   | false \Rightarrow 
119     match m with 
120     [ O \Rightarrow n
121     | (S p) \Rightarrow gcd_aux (S p) n (S p) ] ] \divides n). 
122 apply (leb_elim n m).
123 apply (nat_case1 n).
124 simplify.intros.split.
125 apply (witness m m (S O)).apply times_n_SO.
126 apply (witness m O O).apply times_n_O.
127 intros.change with
128 (gcd_aux (S m1) m (S m1) \divides m
129 \land 
130 gcd_aux (S m1) m (S m1) \divides (S m1)).
131 apply divides_gcd_aux_mn.
132 unfold lt.apply le_S_S.apply le_O_n.
133 assumption.apply le_n.
134 simplify.intro.
135 apply (nat_case1 m).
136 simplify.intros.split.
137 apply (witness n O O).apply times_n_O.
138 apply (witness n n (S O)).apply times_n_SO.
139 intros.change with
140 (gcd_aux (S m1) n (S m1) \divides (S m1)
141 \land 
142 gcd_aux (S m1) n (S m1) \divides n).
143 cut (gcd_aux (S m1) n (S m1) \divides n
144 \land 
145 gcd_aux (S m1) n (S m1) \divides S m1).
146 elim Hcut.split.assumption.assumption.
147 apply divides_gcd_aux_mn.
148 unfold lt.apply le_S_S.apply le_O_n.
149 apply not_lt_to_le.unfold Not. unfold lt.intro.apply H.
150 rewrite > H1.apply (trans_le ? (S n)).
151 apply le_n_Sn.assumption.apply le_n.
152 qed.
153
154 theorem divides_gcd_n: \forall n,m. gcd n m \divides n.
155 intros. 
156 exact (proj2  ? ? (divides_gcd_nm n m)).
157 qed.
158
159 theorem divides_gcd_m: \forall n,m. gcd n m \divides m.
160 intros. 
161 exact (proj1 ? ? (divides_gcd_nm n m)).
162 qed.
163
164
165 theorem divides_times_gcd_aux: \forall p,m,n,d,c. 
166 O \lt c \to O < n \to n \le m \to n \le p \to
167 d \divides (c*m) \to d \divides (c*n) \to d \divides c*gcd_aux p m n. 
168 intro.
169 elim p
170 [ absurd (O < n)
171   [ assumption
172   | apply le_to_not_lt.
173     assumption
174   ]
175 | simplify.
176   cut (n1 \divides m \lor n1 \ndivides m)
177   [ elim Hcut
178     [ rewrite > divides_to_divides_b_true
179       [ simplify.
180         assumption
181       | assumption
182       | assumption
183       ]
184     | rewrite > not_divides_to_divides_b_false
185       [ simplify.
186         apply H
187         [ assumption
188         | cut (O \lt m \mod n1 \lor O = m \mod n1)
189           [ elim Hcut1
190             [ assumption
191             | absurd (n1 \divides m)
192               [ apply mod_O_to_divides
193                 [ assumption
194                 | apply sym_eq.
195                   assumption
196                 ]
197               | assumption
198               ]
199             ]
200           | apply le_to_or_lt_eq.
201             apply le_O_n
202           ]
203         | apply lt_to_le.
204           apply lt_mod_m_m.
205           assumption
206         | apply le_S_S_to_le.
207           apply (trans_le ? n1)
208           [ change with (m \mod n1 < n1).
209             apply lt_mod_m_m.
210             assumption
211           | assumption
212           ]
213         | assumption
214         | rewrite < times_mod
215           [ rewrite < (sym_times c m).
216             rewrite < (sym_times c n1).
217             apply divides_mod
218             [ rewrite > (S_pred c)
219               [ rewrite > (S_pred n1)
220                 [ apply (lt_O_times_S_S)
221                 | assumption
222                 ]
223               | assumption
224               ]
225             | assumption
226             | assumption
227             ]
228           | assumption
229           | assumption
230           ]
231         ]
232       | assumption
233       | assumption
234       ]
235     ]
236   | apply (decidable_divides n1 m).
237     assumption
238   ]
239 ]
240 qed.
241
242 (*a particular case of the previous theorem (setting c=1)*)
243 theorem divides_gcd_aux: \forall p,m,n,d. O < n \to n \le m \to n \le p \to
244 d \divides m \to d \divides n \to d \divides gcd_aux p m n. 
245 intros.
246 rewrite > (times_n_SO (gcd_aux p m n)).
247 rewrite < (sym_times (S O)).
248 apply (divides_times_gcd_aux)
249 [ apply (lt_O_S O)
250 | assumption
251 | assumption
252 | assumption
253 | rewrite > (sym_times (S O)).
254   rewrite < (times_n_SO m).
255   assumption
256 | rewrite > (sym_times (S O)).
257   rewrite < (times_n_SO n).
258   assumption
259 ]
260 qed.
261
262 theorem divides_d_times_gcd: \forall m,n,d,c. 
263 O \lt c \to d \divides (c*m) \to d \divides (c*n) \to d \divides c*gcd n m. 
264 intros.
265 change with
266 (d \divides c *
267 match leb n m with
268   [ true \Rightarrow 
269     match n with 
270     [ O \Rightarrow m
271     | (S p) \Rightarrow gcd_aux (S p) m (S p) ]
272   | false \Rightarrow 
273     match m with 
274     [ O \Rightarrow n
275     | (S p) \Rightarrow gcd_aux (S p) n (S p) ]]).
276 apply (leb_elim n m)
277 [ apply (nat_case1 n)
278   [ simplify.
279     intros.
280     assumption
281   | intros.
282     change with (d \divides c*gcd_aux (S m1) m (S m1)).
283     apply divides_times_gcd_aux
284     [ assumption
285     | unfold lt.
286       apply le_S_S.
287       apply le_O_n
288     | assumption
289     | apply (le_n (S m1))
290     | assumption
291     | rewrite < H3.
292       assumption
293     ]
294   ]
295 | apply (nat_case1 m)
296   [ simplify.
297     intros.
298     assumption
299   | intros.
300     change with (d \divides c * gcd_aux (S m1) n (S m1)).
301     apply divides_times_gcd_aux
302     [ unfold lt.
303       change with (O \lt c).
304       assumption
305     | apply lt_O_S
306     | apply lt_to_le.
307       apply not_le_to_lt.
308       assumption
309     | apply (le_n (S m1)).
310     | assumption
311     | rewrite < H3.
312       assumption
313     ]
314   ]
315 ]
316 qed.
317
318 (*a particular case of the previous theorem (setting c=1)*)
319 theorem divides_d_gcd: \forall m,n,d. 
320 d \divides m \to d \divides n \to d \divides gcd n m. 
321 intros.
322 rewrite > (times_n_SO (gcd n m)).
323 rewrite < (sym_times (S O)).
324 apply (divides_d_times_gcd)
325 [ apply (lt_O_S O)
326 | rewrite > (sym_times (S O)).
327   rewrite < (times_n_SO m).
328   assumption
329 | rewrite > (sym_times (S O)).
330   rewrite < (times_n_SO n).
331   assumption
332 ]
333 qed.
334
335 theorem eq_minus_gcd_aux: \forall p,m,n.O < n \to n \le m \to n \le p \to
336 \exists a,b. a*n - b*m = gcd_aux p m n \lor b*m - a*n = gcd_aux p m n.
337 intro.
338 elim p
339   [absurd (O < n)
340     [assumption
341     |apply le_to_not_lt.assumption
342     ]
343   |cut (O < m)
344     [cut (n1 \divides m \lor  n1 \ndivides m)
345       [simplify.
346        elim Hcut1
347         [rewrite > divides_to_divides_b_true
348           [simplify.
349            apply (ex_intro ? ? (S O)).
350            apply (ex_intro ? ? O).
351            left.
352            simplify.
353            rewrite < plus_n_O.
354            apply sym_eq.
355            apply minus_n_O
356           |assumption
357           |assumption
358           ]
359         |rewrite > not_divides_to_divides_b_false
360           [change with
361            (\exists a,b.a*n1 - b*m = gcd_aux n n1 (m \mod n1)
362             \lor b*m - a*n1 = gcd_aux n n1 (m \mod n1)).
363            cut 
364            (\exists a,b.a*(m \mod n1) - b*n1= gcd_aux n n1 (m \mod n1)
365             \lor b*n1 - a*(m \mod n1) = gcd_aux n n1 (m \mod n1))
366             [elim Hcut2.elim H5.elim H6
367               [(* first case *)
368                rewrite < H7.
369                apply (ex_intro ? ? (a1+a*(m / n1))).
370                apply (ex_intro ? ? a).
371                right.
372                rewrite < sym_plus.
373                rewrite < (sym_times n1).
374                rewrite > distr_times_plus.
375                rewrite > (sym_times n1).
376                rewrite > (sym_times n1).
377                rewrite > (div_mod m n1) in \vdash (? ? (? % ?) ?)
378                 [rewrite > assoc_times.
379                  rewrite < sym_plus.
380                  rewrite > distr_times_plus.
381                  rewrite < eq_minus_minus_minus_plus.
382                  rewrite < sym_plus.
383                  rewrite < plus_minus
384                   [rewrite < minus_n_n.reflexivity
385                   |apply le_n
386                   ]
387                 |assumption
388                 ]
389               |(* second case *)
390               rewrite < H7.
391                apply (ex_intro ? ? (a1+a*(m / n1))).
392                apply (ex_intro ? ? a).
393                left.
394                (* clear Hcut2.clear H5.clear H6.clear H. *)
395                rewrite > sym_times.
396                rewrite > distr_times_plus.
397                rewrite > sym_times.
398                rewrite > (sym_times n1).
399                rewrite > (div_mod m n1) in \vdash (? ? (? ? %) ?)
400                 [rewrite > distr_times_plus.
401                  rewrite > assoc_times.
402                  rewrite < eq_minus_minus_minus_plus.
403                  rewrite < sym_plus.
404                  rewrite < plus_minus
405                   [rewrite < minus_n_n.reflexivity
406                   |apply le_n
407                   ]
408                 |assumption
409                 ]
410               ]
411             |apply (H n1 (m \mod n1))
412               [cut (O \lt m \mod n1 \lor O = m \mod n1)
413                 [elim Hcut2
414                   [assumption 
415                   |absurd (n1 \divides m)
416                     [apply mod_O_to_divides
417                       [assumption
418                       |symmetry.assumption
419                       ]
420                     |assumption
421                     ]
422                   ]
423                 |apply le_to_or_lt_eq.
424                  apply le_O_n
425                 ]
426               |apply lt_to_le.
427                apply lt_mod_m_m.
428                assumption
429               |apply le_S_S_to_le.
430                apply (trans_le ? n1)
431                 [change with (m \mod n1 < n1).
432                  apply lt_mod_m_m.
433                  assumption
434                 |assumption
435                 ]
436               ]
437             ]
438           |assumption
439           |assumption
440           ]
441         ]
442       |apply (decidable_divides n1 m).
443        assumption
444       ]
445     |apply (lt_to_le_to_lt ? n1);assumption
446     ]
447   ]
448 qed.
449
450 theorem eq_minus_gcd:
451  \forall m,n.\exists a,b.a*n - b*m = (gcd n m) \lor b*m - a*n = (gcd n m).
452 intros.
453 unfold gcd.
454 apply (leb_elim n m).
455 apply (nat_case1 n).
456 simplify.intros.
457 apply (ex_intro ? ? O).
458 apply (ex_intro ? ? (S O)).
459 right.simplify.
460 rewrite < plus_n_O.
461 apply sym_eq.apply minus_n_O.
462 intros.
463 change with 
464 (\exists a,b.
465 a*(S m1) - b*m = (gcd_aux (S m1) m (S m1)) 
466 \lor b*m - a*(S m1) = (gcd_aux (S m1) m (S m1))).
467 apply eq_minus_gcd_aux.
468 unfold lt. apply le_S_S.apply le_O_n.
469 assumption.apply le_n.
470 apply (nat_case1 m).
471 simplify.intros.
472 apply (ex_intro ? ? (S O)).
473 apply (ex_intro ? ? O).
474 left.simplify.
475 rewrite < plus_n_O.
476 apply sym_eq.apply minus_n_O.
477 intros.
478 change with 
479 (\exists a,b.
480 a*n - b*(S m1) = (gcd_aux (S m1) n (S m1)) 
481 \lor b*(S m1) - a*n = (gcd_aux (S m1) n (S m1))).
482 cut 
483 (\exists a,b.
484 a*(S m1) - b*n = (gcd_aux (S m1) n (S m1))
485 \lor
486 b*n - a*(S m1) = (gcd_aux (S m1) n (S m1))).
487 elim Hcut.elim H2.elim H3.
488 apply (ex_intro ? ? a1).
489 apply (ex_intro ? ? a).
490 right.assumption.
491 apply (ex_intro ? ? a1).
492 apply (ex_intro ? ? a).
493 left.assumption.
494 apply eq_minus_gcd_aux.
495 unfold lt. apply le_S_S.apply le_O_n.
496 apply lt_to_le.apply not_le_to_lt.assumption.
497 apply le_n.
498 qed.
499
500 (* some properties of gcd *)
501
502 theorem gcd_O_n: \forall n:nat. gcd O n = n.
503 intro.simplify.reflexivity.
504 qed.
505
506 theorem gcd_O_to_eq_O:\forall m,n:nat. (gcd m n) = O \to
507 m = O \land n = O.
508 intros.cut (O \divides n \land O \divides m).
509 elim Hcut.elim H2.split.
510 assumption.elim H1.assumption.
511 rewrite < H.
512 apply divides_gcd_nm.
513 qed.
514
515 theorem lt_O_gcd:\forall m,n:nat. O < n \to O < gcd m n.
516 intros.
517 apply (nat_case1 (gcd m n)).
518 intros.
519 generalize in match (gcd_O_to_eq_O m n H1).
520 intros.elim H2.
521 rewrite < H4 in \vdash (? ? %).assumption.
522 intros.unfold lt.apply le_S_S.apply le_O_n.
523 qed.
524
525 theorem gcd_n_n: \forall n.gcd n n = n.
526 intro.elim n
527   [reflexivity
528   |apply le_to_le_to_eq
529     [apply divides_to_le
530       [apply lt_O_S
531       |apply divides_gcd_n
532       ]
533     |apply divides_to_le
534       [apply lt_O_gcd.apply lt_O_S
535       |apply divides_d_gcd
536         [apply divides_n_n|apply divides_n_n]
537       ]
538     ]
539   ]
540 qed.
541
542 theorem gcd_SO_to_lt_O: \forall i,n. (S O) < n \to gcd i n = (S O) \to
543 O < i.
544 intros.
545 elim (le_to_or_lt_eq ? ? (le_O_n i))
546   [assumption
547   |absurd ((gcd i n) = (S O))
548     [assumption
549     |rewrite < H2.
550      simplify.
551      unfold.intro.
552      apply (lt_to_not_eq (S O) n H).
553      apply sym_eq.assumption
554     ]
555   ]
556 qed.
557
558 theorem gcd_SO_to_lt_n: \forall i,n. (S O) < n \to i \le n \to gcd i n = (S O) \to
559 i < n.
560 intros.
561 elim (le_to_or_lt_eq ? ? H1)
562   [assumption
563   |absurd ((gcd i n) = (S O))
564     [assumption
565     |rewrite > H3.
566      rewrite > gcd_n_n.
567      unfold.intro.
568      apply (lt_to_not_eq (S O) n H).
569      apply sym_eq.assumption
570     ]
571   ]
572 qed.
573
574 theorem  gcd_n_times_nm: \forall n,m. O < m \to gcd n (n*m) = n.
575 intro.apply (nat_case n)
576   [intros.reflexivity
577   |intros.
578    apply le_to_le_to_eq
579     [apply divides_to_le
580       [apply lt_O_S|apply divides_gcd_n]
581     |apply divides_to_le
582       [apply lt_O_gcd.rewrite > (times_n_O O).
583        apply lt_times[apply lt_O_S|assumption]
584       |apply divides_d_gcd
585         [apply (witness ? ? m1).reflexivity
586         |apply divides_n_n
587         ]
588       ]
589     ]
590   ]
591 qed.
592
593 theorem symmetric_gcd: symmetric nat gcd.
594 change with 
595 (\forall n,m:nat. gcd n m = gcd m n).
596 intros.
597 cut (O < (gcd n m) \lor O = (gcd n m)).
598 elim Hcut.
599 cut (O < (gcd m n) \lor O = (gcd m n)).
600 elim Hcut1.
601 apply antisym_le.
602 apply divides_to_le.assumption.
603 apply divides_d_gcd.apply divides_gcd_n.apply divides_gcd_m.
604 apply divides_to_le.assumption.
605 apply divides_d_gcd.apply divides_gcd_n.apply divides_gcd_m.
606 rewrite < H1.
607 cut (m=O \land n=O).
608 elim Hcut2.rewrite > H2.rewrite > H3.reflexivity.
609 apply gcd_O_to_eq_O.apply sym_eq.assumption.
610 apply le_to_or_lt_eq.apply le_O_n.
611 rewrite < H.
612 cut (n=O \land m=O).
613 elim Hcut1.rewrite > H1.rewrite > H2.reflexivity.
614 apply gcd_O_to_eq_O.apply sym_eq.assumption.
615 apply le_to_or_lt_eq.apply le_O_n.
616 qed.
617
618 variant sym_gcd: \forall n,m:nat. gcd n m = gcd m n \def
619 symmetric_gcd.
620
621 theorem le_gcd_times: \forall m,n,p:nat. O< p \to gcd m n \le gcd m (n*p).
622 intros.
623 apply (nat_case n).apply le_n.
624 intro.
625 apply divides_to_le.
626 apply lt_O_gcd.
627 rewrite > (times_n_O O).
628 apply lt_times.unfold lt.apply le_S_S.apply le_O_n.assumption.
629 apply divides_d_gcd.
630 apply (transitive_divides ? (S m1)).
631 apply divides_gcd_m.
632 apply (witness ? ? p).reflexivity.
633 apply divides_gcd_n.
634 qed.
635
636 theorem gcd_times_SO_to_gcd_SO: \forall m,n,p:nat. O < n \to O < p \to 
637 gcd m (n*p) = (S O) \to gcd m n = (S O).
638 intros.
639 apply antisymmetric_le.
640 rewrite < H2.
641 apply le_gcd_times.assumption.
642 change with (O < gcd m n). 
643 apply lt_O_gcd.assumption.
644 qed.
645
646 (* for the "converse" of the previous result see the end  of this development *)
647
648 theorem eq_gcd_SO_to_not_divides: \forall n,m. (S O) < n \to 
649 (gcd n m) = (S O) \to \lnot (divides n m).
650 intros.unfold.intro.
651 elim H2.
652 generalize in match H1.
653 rewrite > H3.
654 intro.
655 cut (O < n1)
656   [elim (gcd_times_SO_to_gcd_SO n n n1 ? ? H4)
657     [cut (gcd n (n*n1) = n)
658       [apply (lt_to_not_eq (S O) n)
659         [assumption|rewrite < H4.assumption]
660       |apply gcd_n_times_nm.assumption
661       ]
662     |apply (trans_lt ? (S O))[apply le_n|assumption]
663     |assumption
664     ]
665   |elim (le_to_or_lt_eq O n1 (le_O_n n1));
666     [assumption
667     |apply False_ind.
668      apply (le_to_not_lt n (S O))
669       [rewrite < H4.
670        apply divides_to_le
671         [rewrite > H4.apply lt_O_S
672         |apply divides_d_gcd
673           [apply (witness ? ? n1).reflexivity
674           |apply divides_n_n
675           ]
676         ]
677       |assumption
678       ]
679     ]
680   ]
681 qed.
682
683 theorem gcd_SO_n: \forall n:nat. gcd (S O) n = (S O).
684 intro.
685 apply antisym_le.apply divides_to_le.unfold lt.apply le_n.
686 apply divides_gcd_n.
687 cut (O < gcd (S O) n \lor O = gcd (S O) n).
688 elim Hcut.assumption.
689 apply False_ind.
690 apply (not_eq_O_S O).
691 cut ((S O)=O \land n=O).
692 elim Hcut1.apply sym_eq.assumption.
693 apply gcd_O_to_eq_O.apply sym_eq.assumption.
694 apply le_to_or_lt_eq.apply le_O_n.
695 qed.
696
697 theorem divides_gcd_mod: \forall m,n:nat. O < n \to
698 divides (gcd m n) (gcd n (m \mod n)).
699 intros.
700 apply divides_d_gcd.
701 apply divides_mod.assumption.
702 apply divides_gcd_n.
703 apply divides_gcd_m.
704 apply divides_gcd_m.
705 qed.
706
707 theorem divides_mod_gcd: \forall m,n:nat. O < n \to
708 divides (gcd n (m \mod n)) (gcd m n) .
709 intros.
710 apply divides_d_gcd.
711 apply divides_gcd_n.
712 apply (divides_mod_to_divides ? ? n).
713 assumption.
714 apply divides_gcd_m.
715 apply divides_gcd_n.
716 qed.
717
718 theorem gcd_mod: \forall m,n:nat. O < n \to
719 (gcd n (m \mod n)) = (gcd m n) .
720 intros.
721 apply antisymmetric_divides.
722 apply divides_mod_gcd.assumption.
723 apply divides_gcd_mod.assumption.
724 qed.
725
726 (* gcd and primes *)
727
728 theorem prime_to_gcd_SO: \forall n,m:nat. prime n \to n \ndivides m \to
729 gcd n m = (S O).
730 intros.unfold prime in H.
731 elim H.
732 apply antisym_le.
733 apply not_lt_to_le.unfold Not.unfold lt.
734 intro.
735 apply H1.rewrite < (H3 (gcd n m)).
736 apply divides_gcd_m.
737 apply divides_gcd_n.assumption.
738 cut (O < gcd n m \lor O = gcd n m).
739 elim Hcut.assumption.
740 apply False_ind.
741 apply (not_le_Sn_O (S O)).
742 cut (n=O \land m=O).
743 elim Hcut1.rewrite < H5 in \vdash (? ? %).assumption.
744 apply gcd_O_to_eq_O.apply sym_eq.assumption.
745 apply le_to_or_lt_eq.apply le_O_n.
746 qed.
747
748 (* primes and divides *)
749 theorem divides_times_to_divides: \forall n,p,q:nat.prime n \to n \divides p*q \to
750 n \divides p \lor n \divides q.
751 intros.
752 cut (n \divides p \lor n \ndivides p)
753   [elim Hcut
754     [left.assumption
755     |right.
756      cut (\exists a,b. a*n - b*p = (S O) \lor b*p - a*n = (S O))
757        [elim Hcut1.elim H3.elim H4
758          [(* first case *)
759           rewrite > (times_n_SO q).rewrite < H5.
760           rewrite > distr_times_minus.
761           rewrite > (sym_times q (a1*p)).
762           rewrite > (assoc_times a1).
763           elim H1.
764           (*
765              rewrite > H6.
766              applyS (witness n (n*(q*a-a1*n2)) (q*a-a1*n2))
767              reflexivity. *);
768           applyS (witness n ? ? (refl_eq ? ?)) (* timeout=50 *).
769           (*
770           rewrite < (sym_times n).rewrite < assoc_times.
771           rewrite > (sym_times q).rewrite > assoc_times.
772           rewrite < (assoc_times a1).rewrite < (sym_times n).
773           rewrite > (assoc_times n).
774           rewrite < distr_times_minus.
775           apply (witness ? ? (q*a-a1*n2)).reflexivity
776           *)
777          |(* second case *)
778           rewrite > (times_n_SO q).rewrite < H5.
779           rewrite > distr_times_minus.
780           rewrite > (sym_times q (a1*p)).
781           rewrite > (assoc_times a1).
782           elim H1.rewrite > H6.
783           rewrite < sym_times.rewrite > assoc_times.
784           rewrite < (assoc_times q).
785           rewrite < (sym_times n).
786           rewrite < distr_times_minus.
787           apply (witness ? ? (n1*a1-q*a)).reflexivity
788         ](* end second case *)
789      |rewrite < (prime_to_gcd_SO n p)
790        [apply eq_minus_gcd|assumption|assumption
791        ]
792      ]
793    ]
794  |apply (decidable_divides n p).
795   apply (trans_lt ? (S O))
796     [unfold lt.apply le_n
797     |unfold prime in H.elim H. assumption
798     ]
799   ]
800 qed.
801
802 theorem divides_exp_to_divides: 
803 \forall p,n,m:nat. prime p \to 
804 p \divides n \sup m \to p \divides n.
805 intros 3.elim m.simplify in H1.
806 apply (transitive_divides p (S O)).assumption.
807 apply divides_SO_n.
808 cut (p \divides n \lor p \divides n \sup n1).
809 elim Hcut.assumption.
810 apply H.assumption.assumption.
811 apply divides_times_to_divides.assumption.
812 exact H2.
813 qed.
814
815 theorem divides_exp_to_eq: 
816 \forall p,q,m:nat. prime p \to prime q \to
817 p \divides q \sup m \to p = q.
818 intros.
819 unfold prime in H1.
820 elim H1.apply H4.
821 apply (divides_exp_to_divides p q m).
822 assumption.assumption.
823 unfold prime in H.elim H.assumption.
824 qed.
825
826 theorem eq_gcd_times_SO: \forall m,n,p:nat. O < n \to O < p \to
827 gcd m n = (S O) \to gcd m p = (S O) \to gcd m (n*p) = (S O).
828 intros.
829 apply antisymmetric_le.
830 apply not_lt_to_le.
831 unfold Not.intro.
832 cut (divides (smallest_factor (gcd m (n*p))) n \lor 
833      divides (smallest_factor (gcd m (n*p))) p).
834 elim Hcut.
835 apply (not_le_Sn_n (S O)).
836 change with ((S O) < (S O)).
837 rewrite < H2 in \vdash (? ? %).
838 apply (lt_to_le_to_lt ? (smallest_factor (gcd m (n*p)))).
839 apply lt_SO_smallest_factor.assumption.
840 apply divides_to_le.
841 rewrite > H2.unfold lt.apply le_n.
842 apply divides_d_gcd.assumption.
843 apply (transitive_divides ? (gcd m (n*p))).
844 apply divides_smallest_factor_n.
845 apply (trans_lt ? (S O)). unfold lt. apply le_n. assumption.
846 apply divides_gcd_n.
847 apply (not_le_Sn_n (S O)).
848 change with ((S O) < (S O)).
849 rewrite < H3 in \vdash (? ? %).
850 apply (lt_to_le_to_lt ? (smallest_factor (gcd m (n*p)))).
851 apply lt_SO_smallest_factor.assumption.
852 apply divides_to_le.
853 rewrite > H3.unfold lt.apply le_n.
854 apply divides_d_gcd.assumption.
855 apply (transitive_divides ? (gcd m (n*p))).
856 apply divides_smallest_factor_n.
857 apply (trans_lt ? (S O)). unfold lt. apply le_n. assumption.
858 apply divides_gcd_n.
859 apply divides_times_to_divides.
860 apply prime_smallest_factor_n.
861 assumption.
862 apply (transitive_divides ? (gcd m (n*p))).
863 apply divides_smallest_factor_n.
864 apply (trans_lt ? (S O)).unfold lt. apply le_n. assumption.
865 apply divides_gcd_m.
866 change with (O < gcd m (n*p)).
867 apply lt_O_gcd.
868 rewrite > (times_n_O O).
869 apply lt_times.assumption.assumption.
870 qed.
871
872 theorem gcd_SO_to_divides_times_to_divides: \forall m,n,p:nat. O < n \to
873 gcd n m = (S O) \to n \divides (m*p) \to n \divides p.
874 intros.
875 cut (n \divides p \lor n \ndivides p)
876   [elim Hcut
877     [assumption
878     |cut (\exists a,b. a*n - b*m = (S O) \lor b*m - a*n = (S O))
879       [elim Hcut1.elim H4.elim H5         
880         [(* first case *)
881           rewrite > (times_n_SO p).rewrite < H6.
882           rewrite > distr_times_minus.
883           rewrite > (sym_times p (a1*m)).
884           rewrite > (assoc_times a1).
885           elim H2.
886           applyS (witness n ? ? (refl_eq ? ?)) (* timeout=50 *).
887          |(* second case *)
888           rewrite > (times_n_SO p).rewrite < H6.
889           rewrite > distr_times_minus.
890           rewrite > (sym_times p (a1*m)).
891           rewrite > (assoc_times a1).
892           elim H2.
893           applyS (witness n ? ? (refl_eq ? ?)).
894         ](* end second case *)
895      |rewrite < H1.apply eq_minus_gcd.
896      ]
897    ]
898  |apply (decidable_divides n p).
899   assumption.
900  ]
901 qed.
902
903 (*
904 theorem divides_to_divides_times1: \forall p,q,n. prime p \to prime q \to p \neq q \to
905 divides p n \to divides q n \to divides (p*q) n.
906 intros.elim H3.
907 rewrite > H5 in H4.
908 elim (divides_times_to_divides ? ? ? H1 H4)
909   [elim H.apply False_ind.
910    apply H2.apply sym_eq.apply H8
911     [assumption
912     |apply prime_to_lt_SO.assumption
913     ]
914   |elim H6.
915    apply (witness ? ? n1).
916    rewrite > assoc_times.
917    rewrite < H7.assumption
918   ]
919 qed.
920 *)
921
922 theorem divides_to_divides_times: \forall p,q,n. prime p  \to p \ndivides q \to
923 divides p n \to divides q n \to divides (p*q) n.
924 intros.elim H3.
925 rewrite > H4 in H2.
926 elim (divides_times_to_divides ? ? ? H H2)
927   [apply False_ind.apply H1.assumption
928   |elim H5.
929    apply (witness ? ? n2).
930    rewrite > sym_times in ⊢ (? ? ? (? % ?)).
931    rewrite > assoc_times.
932    rewrite < H6.assumption
933   ]
934 qed.