1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| A.Asperti, C.Sacerdoti Coen, *)
8 (* ||A|| E.Tassi, S.Zacchiroli *)
10 (* \ / Matita is distributed under the terms of the *)
11 (* v GNU Lesser General Public License Version 2.1 *)
13 (**************************************************************************)
15 set "baseuri" "cic:/matita/nat/gcd".
17 include "nat/primes.ma".
19 let rec gcd_aux p m n: nat \def
20 match divides_b n m with
25 |(S q) \Rightarrow gcd_aux q n (m \mod n)]].
27 definition gcd : nat \to nat \to nat \def
33 | (S p) \Rightarrow gcd_aux (S p) m (S p) ]
37 | (S p) \Rightarrow gcd_aux (S p) n (S p) ]].
39 theorem divides_mod: \forall p,m,n:nat. O < n \to p \divides m \to p \divides n \to
40 p \divides (m \mod n).
41 intros.elim H1.elim H2.
42 (* apply (witness ? ? (n2 - n1*(m / n))). *)
44 rewrite > distr_times_minus.
45 rewrite < H3 in \vdash (? ? ? (? % ?)).
46 rewrite < assoc_times.
47 rewrite < H4 in \vdash (? ? ? (? ? (? % ?))).
48 apply sym_eq.apply plus_to_minus.
51 rewrite < (div_mod ? ? H).
56 theorem divides_mod_to_divides: \forall p,m,n:nat. O < n \to
57 p \divides (m \mod n) \to p \divides n \to p \divides m.
58 intros.elim H1.elim H2.
59 apply (witness p m ((n1*(m / n))+n2)).
60 rewrite > distr_times_plus.
62 rewrite < assoc_times.
63 rewrite < H4.rewrite < sym_times.
64 apply div_mod.assumption.
67 theorem divides_gcd_aux_mn: \forall p,m,n. O < n \to n \le m \to n \le p \to
68 gcd_aux p m n \divides m \land gcd_aux p m n \divides n.
70 absurd (O < n).assumption.apply le_to_not_lt.assumption.
71 cut ((n1 \divides m) \lor (n1 \ndivides m)).
73 elim Hcut.rewrite > divides_to_divides_b_true.
75 split.assumption.apply (witness n1 n1 (S O)).apply times_n_SO.
76 assumption.assumption.
77 rewrite > not_divides_to_divides_b_false.
79 cut (gcd_aux n n1 (m \mod n1) \divides n1 \land
80 gcd_aux n n1 (m \mod n1) \divides mod m n1).
82 split.apply (divides_mod_to_divides ? ? n1).
83 assumption.assumption.assumption.assumption.
85 cut (O \lt m \mod n1 \lor O = mod m n1).
86 elim Hcut1.assumption.
87 apply False_ind.apply H4.apply mod_O_to_divides.
88 assumption.apply sym_eq.assumption.
89 apply le_to_or_lt_eq.apply le_O_n.
91 apply lt_mod_m_m.assumption.
93 apply (trans_le ? n1).
94 change with (m \mod n1 < n1).
95 apply lt_mod_m_m.assumption.assumption.
96 assumption.assumption.
97 apply (decidable_divides n1 m).assumption.
100 theorem divides_gcd_nm: \forall n,m.
101 gcd n m \divides m \land gcd n m \divides n.
103 (*CSC: simplify simplifies too much because of a redex in gcd *)
109 | (S p) \Rightarrow gcd_aux (S p) m (S p) ]
113 | (S p) \Rightarrow gcd_aux (S p) n (S p) ] ] \divides m
119 | (S p) \Rightarrow gcd_aux (S p) m (S p) ]
123 | (S p) \Rightarrow gcd_aux (S p) n (S p) ] ] \divides n).
124 apply (leb_elim n m).
126 simplify.intros.split.
127 apply (witness m m (S O)).apply times_n_SO.
128 apply (witness m O O).apply times_n_O.
130 (gcd_aux (S m1) m (S m1) \divides m
132 gcd_aux (S m1) m (S m1) \divides (S m1)).
133 apply divides_gcd_aux_mn.
134 unfold lt.apply le_S_S.apply le_O_n.
135 assumption.apply le_n.
138 simplify.intros.split.
139 apply (witness n O O).apply times_n_O.
140 apply (witness n n (S O)).apply times_n_SO.
142 (gcd_aux (S m1) n (S m1) \divides (S m1)
144 gcd_aux (S m1) n (S m1) \divides n).
145 cut (gcd_aux (S m1) n (S m1) \divides n
147 gcd_aux (S m1) n (S m1) \divides S m1).
148 elim Hcut.split.assumption.assumption.
149 apply divides_gcd_aux_mn.
150 unfold lt.apply le_S_S.apply le_O_n.
151 apply not_lt_to_le.unfold Not. unfold lt.intro.apply H.
152 rewrite > H1.apply (trans_le ? (S n)).
153 apply le_n_Sn.assumption.apply le_n.
156 theorem divides_gcd_n: \forall n,m. gcd n m \divides n.
158 exact (proj2 ? ? (divides_gcd_nm n m)).
161 theorem divides_gcd_m: \forall n,m. gcd n m \divides m.
163 exact (proj1 ? ? (divides_gcd_nm n m)).
166 theorem divides_gcd_aux: \forall p,m,n,d. O < n \to n \le m \to n \le p \to
167 d \divides m \to d \divides n \to d \divides gcd_aux p m n.
169 absurd (O < n).assumption.apply le_to_not_lt.assumption.
171 cut (n1 \divides m \lor n1 \ndivides m).
173 rewrite > divides_to_divides_b_true.
175 assumption.assumption.
176 rewrite > not_divides_to_divides_b_false.
179 cut (O \lt m \mod n1 \lor O = m \mod n1).
180 elim Hcut1.assumption.
181 absurd (n1 \divides m).apply mod_O_to_divides.
182 assumption.apply sym_eq.assumption.assumption.
183 apply le_to_or_lt_eq.apply le_O_n.
185 apply lt_mod_m_m.assumption.
187 apply (trans_le ? n1).
188 change with (m \mod n1 < n1).
189 apply lt_mod_m_m.assumption.assumption.
191 apply divides_mod.assumption.assumption.assumption.
192 assumption.assumption.
193 apply (decidable_divides n1 m).assumption.
196 theorem divides_d_gcd: \forall m,n,d.
197 d \divides m \to d \divides n \to d \divides gcd n m.
199 (*CSC: here simplify simplifies too much because of a redex in gcd *)
206 | (S p) \Rightarrow gcd_aux (S p) m (S p) ]
210 | (S p) \Rightarrow gcd_aux (S p) n (S p) ]]).
211 apply (leb_elim n m).
212 apply (nat_case1 n).simplify.intros.assumption.
214 change with (d \divides gcd_aux (S m1) m (S m1)).
215 apply divides_gcd_aux.
216 unfold lt.apply le_S_S.apply le_O_n.assumption.apply le_n.assumption.
217 rewrite < H2.assumption.
218 apply (nat_case1 m).simplify.intros.assumption.
220 change with (d \divides gcd_aux (S m1) n (S m1)).
221 apply divides_gcd_aux.
222 unfold lt.apply le_S_S.apply le_O_n.
223 apply lt_to_le.apply not_le_to_lt.assumption.apply le_n.assumption.
224 rewrite < H2.assumption.
227 theorem eq_minus_gcd_aux: \forall p,m,n.O < n \to n \le m \to n \le p \to
228 \exists a,b. a*n - b*m = gcd_aux p m n \lor b*m - a*n = gcd_aux p m n.
231 absurd (O < n).assumption.apply le_to_not_lt.assumption.
233 cut (n1 \divides m \lor n1 \ndivides m).
236 rewrite > divides_to_divides_b_true.
238 apply (ex_intro ? ? (S O)).
239 apply (ex_intro ? ? O).
240 left.simplify.rewrite < plus_n_O.
241 apply sym_eq.apply minus_n_O.
242 assumption.assumption.
243 rewrite > not_divides_to_divides_b_false.
246 a*n1 - b*m = gcd_aux n n1 (m \mod n1)
248 b*m - a*n1 = gcd_aux n n1 (m \mod n1)).
251 a*(m \mod n1) - b*n1= gcd_aux n n1 (m \mod n1)
253 b*n1 - a*(m \mod n1) = gcd_aux n n1 (m \mod n1)).
254 elim Hcut2.elim H5.elim H6.
257 apply (ex_intro ? ? (a1+a*(m / n1))).
258 apply (ex_intro ? ? a).
261 rewrite < (sym_times n1).
262 rewrite > distr_times_plus.
263 rewrite > (sym_times n1).
264 rewrite > (sym_times n1).
265 rewrite > (div_mod m n1) in \vdash (? ? (? % ?) ?).
266 rewrite > assoc_times.
268 rewrite > distr_times_plus.
269 rewrite < eq_minus_minus_minus_plus.
271 rewrite < plus_minus.
272 rewrite < minus_n_n.reflexivity.
277 apply (ex_intro ? ? (a1+a*(m / n1))).
278 apply (ex_intro ? ? a).
280 (* clear Hcut2.clear H5.clear H6.clear H. *)
282 rewrite > distr_times_plus.
284 rewrite > (sym_times n1).
285 rewrite > (div_mod m n1) in \vdash (? ? (? ? %) ?).
286 rewrite > distr_times_plus.
287 rewrite > assoc_times.
288 rewrite < eq_minus_minus_minus_plus.
290 rewrite < plus_minus.
291 rewrite < minus_n_n.reflexivity.
294 apply (H n1 (m \mod n1)).
295 cut (O \lt m \mod n1 \lor O = m \mod n1).
296 elim Hcut2.assumption.
297 absurd (n1 \divides m).apply mod_O_to_divides.
299 symmetry.assumption.assumption.
300 apply le_to_or_lt_eq.apply le_O_n.
302 apply lt_mod_m_m.assumption.
304 apply (trans_le ? n1).
305 change with (m \mod n1 < n1).
307 assumption.assumption.assumption.assumption.
308 apply (decidable_divides n1 m).assumption.
309 apply (lt_to_le_to_lt ? n1).assumption.assumption.
312 theorem eq_minus_gcd:
313 \forall m,n.\exists a,b.a*n - b*m = (gcd n m) \lor b*m - a*n = (gcd n m).
316 apply (leb_elim n m).
319 apply (ex_intro ? ? O).
320 apply (ex_intro ? ? (S O)).
323 apply sym_eq.apply minus_n_O.
327 a*(S m1) - b*m = (gcd_aux (S m1) m (S m1))
328 \lor b*m - a*(S m1) = (gcd_aux (S m1) m (S m1))).
329 apply eq_minus_gcd_aux.
330 unfold lt. apply le_S_S.apply le_O_n.
331 assumption.apply le_n.
334 apply (ex_intro ? ? (S O)).
335 apply (ex_intro ? ? O).
338 apply sym_eq.apply minus_n_O.
342 a*n - b*(S m1) = (gcd_aux (S m1) n (S m1))
343 \lor b*(S m1) - a*n = (gcd_aux (S m1) n (S m1))).
346 a*(S m1) - b*n = (gcd_aux (S m1) n (S m1))
348 b*n - a*(S m1) = (gcd_aux (S m1) n (S m1))).
349 elim Hcut.elim H2.elim H3.
350 apply (ex_intro ? ? a1).
351 apply (ex_intro ? ? a).
353 apply (ex_intro ? ? a1).
354 apply (ex_intro ? ? a).
356 apply eq_minus_gcd_aux.
357 unfold lt. apply le_S_S.apply le_O_n.
358 apply lt_to_le.apply not_le_to_lt.assumption.
362 (* some properties of gcd *)
364 theorem gcd_O_n: \forall n:nat. gcd O n = n.
365 intro.simplify.reflexivity.
368 theorem gcd_O_to_eq_O:\forall m,n:nat. (gcd m n) = O \to
370 intros.cut (O \divides n \land O \divides m).
371 elim Hcut.elim H2.split.
372 assumption.elim H1.assumption.
374 apply divides_gcd_nm.
377 theorem lt_O_gcd:\forall m,n:nat. O < n \to O < gcd m n.
379 apply (nat_case1 (gcd m n)).
381 generalize in match (gcd_O_to_eq_O m n H1).
383 rewrite < H4 in \vdash (? ? %).assumption.
384 intros.unfold lt.apply le_S_S.apply le_O_n.
387 theorem gcd_n_n: \forall n.gcd n n = n.
390 |apply le_to_le_to_eq
396 [apply lt_O_gcd.apply lt_O_S
398 [apply divides_n_n|apply divides_n_n]
404 theorem gcd_SO_to_lt_O: \forall i,n. (S O) < n \to gcd i n = (S O) \to
407 elim (le_to_or_lt_eq ? ? (le_O_n i))
409 |absurd ((gcd i n) = (S O))
414 apply (lt_to_not_eq (S O) n H).
415 apply sym_eq.assumption
420 theorem gcd_SO_to_lt_n: \forall i,n. (S O) < n \to i \le n \to gcd i n = (S O) \to
423 elim (le_to_or_lt_eq ? ? H1)
425 |absurd ((gcd i n) = (S O))
430 apply (lt_to_not_eq (S O) n H).
431 apply sym_eq.assumption
436 theorem gcd_n_times_nm: \forall n,m. O < m \to gcd n (n*m) = n.
437 intro.apply (nat_case n)
442 [apply lt_O_S|apply divides_gcd_n]
444 [apply lt_O_gcd.rewrite > (times_n_O O).
445 apply lt_times[apply lt_O_S|assumption]
447 [apply (witness ? ? m1).reflexivity
455 theorem symmetric_gcd: symmetric nat gcd.
456 (*CSC: bug here: unfold symmetric does not work *)
458 (\forall n,m:nat. gcd n m = gcd m n).
460 cut (O < (gcd n m) \lor O = (gcd n m)).
462 cut (O < (gcd m n) \lor O = (gcd m n)).
465 apply divides_to_le.assumption.
466 apply divides_d_gcd.apply divides_gcd_n.apply divides_gcd_m.
467 apply divides_to_le.assumption.
468 apply divides_d_gcd.apply divides_gcd_n.apply divides_gcd_m.
471 elim Hcut2.rewrite > H2.rewrite > H3.reflexivity.
472 apply gcd_O_to_eq_O.apply sym_eq.assumption.
473 apply le_to_or_lt_eq.apply le_O_n.
476 elim Hcut1.rewrite > H1.rewrite > H2.reflexivity.
477 apply gcd_O_to_eq_O.apply sym_eq.assumption.
478 apply le_to_or_lt_eq.apply le_O_n.
481 variant sym_gcd: \forall n,m:nat. gcd n m = gcd m n \def
484 theorem le_gcd_times: \forall m,n,p:nat. O< p \to gcd m n \le gcd m (n*p).
486 apply (nat_case n).apply le_n.
490 rewrite > (times_n_O O).
491 apply lt_times.unfold lt.apply le_S_S.apply le_O_n.assumption.
493 apply (transitive_divides ? (S m1)).
495 apply (witness ? ? p).reflexivity.
499 theorem gcd_times_SO_to_gcd_SO: \forall m,n,p:nat. O < n \to O < p \to
500 gcd m (n*p) = (S O) \to gcd m n = (S O).
502 apply antisymmetric_le.
504 apply le_gcd_times.assumption.
505 change with (O < gcd m n).
506 apply lt_O_gcd.assumption.
509 (* for the "converse" of the previous result see the end of this development *)
511 theorem eq_gcd_SO_to_not_divides: \forall n,m. (S O) < n \to
512 (gcd n m) = (S O) \to \lnot (divides n m).
515 generalize in match H1.
519 [elim (gcd_times_SO_to_gcd_SO n n n2 ? ? H4)
520 [cut (gcd n (n*n2) = n)
521 [apply (lt_to_not_eq (S O) n)
522 [assumption|rewrite < H4.assumption]
523 |apply gcd_n_times_nm.assumption
525 |apply (trans_lt ? (S O))[apply le_n|assumption]
528 |elim (le_to_or_lt_eq O n2 (le_O_n n2))
531 apply (le_to_not_lt n (S O))
534 [rewrite > H4.apply lt_O_S
536 [apply (witness ? ? n2).reflexivity
546 theorem gcd_SO_n: \forall n:nat. gcd (S O) n = (S O).
548 apply antisym_le.apply divides_to_le.unfold lt.apply le_n.
550 cut (O < gcd (S O) n \lor O = gcd (S O) n).
551 elim Hcut.assumption.
553 apply (not_eq_O_S O).
554 cut ((S O)=O \land n=O).
555 elim Hcut1.apply sym_eq.assumption.
556 apply gcd_O_to_eq_O.apply sym_eq.assumption.
557 apply le_to_or_lt_eq.apply le_O_n.
560 theorem divides_gcd_mod: \forall m,n:nat. O < n \to
561 divides (gcd m n) (gcd n (m \mod n)).
564 apply divides_mod.assumption.
570 theorem divides_mod_gcd: \forall m,n:nat. O < n \to
571 divides (gcd n (m \mod n)) (gcd m n) .
575 apply (divides_mod_to_divides ? ? n).
581 theorem gcd_mod: \forall m,n:nat. O < n \to
582 (gcd n (m \mod n)) = (gcd m n) .
584 apply antisymmetric_divides.
585 apply divides_mod_gcd.assumption.
586 apply divides_gcd_mod.assumption.
591 theorem prime_to_gcd_SO: \forall n,m:nat. prime n \to n \ndivides m \to
593 intros.unfold prime in H.
596 apply not_lt_to_le.unfold Not.unfold lt.
598 apply H1.rewrite < (H3 (gcd n m)).
600 apply divides_gcd_n.assumption.
601 cut (O < gcd n m \lor O = gcd n m).
602 elim Hcut.assumption.
604 apply (not_le_Sn_O (S O)).
606 elim Hcut1.rewrite < H5 in \vdash (? ? %).assumption.
607 apply gcd_O_to_eq_O.apply sym_eq.assumption.
608 apply le_to_or_lt_eq.apply le_O_n.
611 theorem divides_times_to_divides: \forall n,p,q:nat.prime n \to n \divides p*q \to
612 n \divides p \lor n \divides q.
614 cut (n \divides p \lor n \ndivides p)
618 cut (\exists a,b. a*n - b*p = (S O) \lor b*p - a*n = (S O))
619 [elim Hcut1.elim H3.elim H4
621 rewrite > (times_n_SO q).rewrite < H5.
622 rewrite > distr_times_minus.
623 rewrite > (sym_times q (a1*p)).
624 rewrite > (assoc_times a1).
628 applyS (witness n (n*(q*a-a1*n2)) (q*a-a1*n2))
630 applyS (witness n ? ? (refl_eq ? ?)) (* timeout=50 *).
632 rewrite < (sym_times n).rewrite < assoc_times.
633 rewrite > (sym_times q).rewrite > assoc_times.
634 rewrite < (assoc_times a1).rewrite < (sym_times n).
635 rewrite > (assoc_times n).
636 rewrite < distr_times_minus.
637 apply (witness ? ? (q*a-a1*n2)).reflexivity
640 rewrite > (times_n_SO q).rewrite < H5.
641 rewrite > distr_times_minus.
642 rewrite > (sym_times q (a1*p)).
643 rewrite > (assoc_times a1).
644 elim H1.rewrite > H6.
645 rewrite < sym_times.rewrite > assoc_times.
646 rewrite < (assoc_times q).
647 rewrite < (sym_times n).
648 rewrite < distr_times_minus.
649 apply (witness ? ? (n2*a1-q*a)).reflexivity
650 ](* end second case *)
651 |rewrite < (prime_to_gcd_SO n p)
652 [apply eq_minus_gcd|assumption|assumption
656 |apply (decidable_divides n p).
657 apply (trans_lt ? (S O))
658 [unfold lt.apply le_n
659 |unfold prime in H.elim H. assumption
664 theorem eq_gcd_times_SO: \forall m,n,p:nat. O < n \to O < p \to
665 gcd m n = (S O) \to gcd m p = (S O) \to gcd m (n*p) = (S O).
667 apply antisymmetric_le.
670 cut (divides (smallest_factor (gcd m (n*p))) n \lor
671 divides (smallest_factor (gcd m (n*p))) p).
673 apply (not_le_Sn_n (S O)).
674 change with ((S O) < (S O)).
675 rewrite < H2 in \vdash (? ? %).
676 apply (lt_to_le_to_lt ? (smallest_factor (gcd m (n*p)))).
677 apply lt_SO_smallest_factor.assumption.
679 rewrite > H2.unfold lt.apply le_n.
680 apply divides_d_gcd.assumption.
681 apply (transitive_divides ? (gcd m (n*p))).
682 apply divides_smallest_factor_n.
683 apply (trans_lt ? (S O)). unfold lt. apply le_n. assumption.
685 apply (not_le_Sn_n (S O)).
686 change with ((S O) < (S O)).
687 rewrite < H3 in \vdash (? ? %).
688 apply (lt_to_le_to_lt ? (smallest_factor (gcd m (n*p)))).
689 apply lt_SO_smallest_factor.assumption.
691 rewrite > H3.unfold lt.apply le_n.
692 apply divides_d_gcd.assumption.
693 apply (transitive_divides ? (gcd m (n*p))).
694 apply divides_smallest_factor_n.
695 apply (trans_lt ? (S O)). unfold lt. apply le_n. assumption.
697 apply divides_times_to_divides.
698 apply prime_smallest_factor_n.
700 apply (transitive_divides ? (gcd m (n*p))).
701 apply divides_smallest_factor_n.
702 apply (trans_lt ? (S O)).unfold lt. apply le_n. assumption.
704 change with (O < gcd m (n*p)).
706 rewrite > (times_n_O O).
707 apply lt_times.assumption.assumption.
710 theorem gcd_SO_to_divides_times_to_divides: \forall m,n,p:nat. O < n \to
711 gcd n m = (S O) \to n \divides (m*p) \to n \divides p.
713 cut (n \divides p \lor n \ndivides p)
716 |cut (\exists a,b. a*n - b*m = (S O) \lor b*m - a*n = (S O))
717 [elim Hcut1.elim H4.elim H5
719 rewrite > (times_n_SO p).rewrite < H6.
720 rewrite > distr_times_minus.
721 rewrite > (sym_times p (a1*m)).
722 rewrite > (assoc_times a1).
724 applyS (witness n ? ? (refl_eq ? ?)) (* timeout=50 *).
726 rewrite > (times_n_SO p).rewrite < H6.
727 rewrite > distr_times_minus.
728 rewrite > (sym_times p (a1*m)).
729 rewrite > (assoc_times a1).
731 applyS (witness n ? ? (refl_eq ? ?)).
732 ](* end second case *)
733 |rewrite < H1.apply eq_minus_gcd.
736 |apply (decidable_divides n p).