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".
18 include "nat/lt_arith.ma".
20 let rec gcd_aux p m n: nat \def
21 match divides_b n m with
26 |(S q) \Rightarrow gcd_aux q n (m \mod n)]].
28 definition gcd : nat \to nat \to nat \def
34 | (S p) \Rightarrow gcd_aux (S p) m (S p) ]
38 | (S p) \Rightarrow gcd_aux (S p) n (S p) ]].
40 theorem divides_mod: \forall p,m,n:nat. O < n \to p \divides m \to p \divides n \to
41 p \divides (m \mod n).
42 intros.elim H1.elim H2.
43 (* apply (witness ? ? (n2 - n1*(m / n))). *)
45 rewrite > distr_times_minus.
46 rewrite < H3 in \vdash (? ? ? (? % ?)).
47 rewrite < assoc_times.
48 rewrite < H4 in \vdash (? ? ? (? ? (? % ?))).
49 apply sym_eq.apply plus_to_minus.
52 rewrite < (div_mod ? ? H).
57 theorem divides_mod_to_divides: \forall p,m,n:nat. O < n \to
58 p \divides (m \mod n) \to p \divides n \to p \divides m.
59 intros.elim H1.elim H2.
60 apply (witness p m ((n1*(m / n))+n2)).
61 rewrite > distr_times_plus.
63 rewrite < assoc_times.
64 rewrite < H4.rewrite < sym_times.
65 apply div_mod.assumption.
68 theorem divides_gcd_aux_mn: \forall p,m,n. O < n \to n \le m \to n \le p \to
69 gcd_aux p m n \divides m \land gcd_aux p m n \divides n.
71 absurd (O < n).assumption.apply le_to_not_lt.assumption.
72 cut ((n1 \divides m) \lor (n1 \ndivides m)).
74 elim Hcut.rewrite > divides_to_divides_b_true.
76 split.assumption.apply (witness n1 n1 (S O)).apply times_n_SO.
77 assumption.assumption.
78 rewrite > not_divides_to_divides_b_false.
80 cut (gcd_aux n n1 (m \mod n1) \divides n1 \land
81 gcd_aux n n1 (m \mod n1) \divides mod m n1).
83 split.apply (divides_mod_to_divides ? ? n1).
84 assumption.assumption.assumption.assumption.
86 cut (O \lt m \mod n1 \lor O = mod m n1).
87 elim Hcut1.assumption.
88 apply False_ind.apply H4.apply mod_O_to_divides.
89 assumption.apply sym_eq.assumption.
90 apply le_to_or_lt_eq.apply le_O_n.
92 apply lt_mod_m_m.assumption.
94 apply (trans_le ? n1).
95 change with (m \mod n1 < n1).
96 apply lt_mod_m_m.assumption.assumption.
97 assumption.assumption.
98 apply (decidable_divides n1 m).assumption.
101 theorem divides_gcd_nm: \forall n,m.
102 gcd n m \divides m \land gcd n m \divides n.
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)).
167 theorem divides_times_gcd_aux: \forall p,m,n,d,c.
168 O \lt c \to O < n \to n \le m \to n \le p \to
169 d \divides (c*m) \to d \divides (c*n) \to d \divides c*gcd_aux p m n.
174 | apply le_to_not_lt.
178 cut (n1 \divides m \lor n1 \ndivides m)
180 [ rewrite > divides_to_divides_b_true
186 | rewrite > not_divides_to_divides_b_false
190 | cut (O \lt m \mod n1 \lor O = m \mod n1)
193 | absurd (n1 \divides m)
194 [ apply mod_O_to_divides
202 | apply le_to_or_lt_eq.
208 | apply le_S_S_to_le.
209 apply (trans_le ? n1)
210 [ change with (m \mod n1 < n1).
216 | rewrite < times_mod
217 [ rewrite < (sym_times c m).
218 rewrite < (sym_times c n1).
220 [ rewrite > (S_pred c)
221 [ rewrite > (S_pred n1)
222 [ apply (lt_O_times_S_S)
238 | apply (decidable_divides n1 m).
244 (*a particular case of the previous theorem (setting c=1)*)
245 theorem divides_gcd_aux: \forall p,m,n,d. O < n \to n \le m \to n \le p \to
246 d \divides m \to d \divides n \to d \divides gcd_aux p m n.
248 rewrite > (times_n_SO (gcd_aux p m n)).
249 rewrite < (sym_times (S O)).
250 apply (divides_times_gcd_aux)
255 | rewrite > (sym_times (S O)).
256 rewrite < (times_n_SO m).
258 | rewrite > (sym_times (S O)).
259 rewrite < (times_n_SO n).
264 theorem divides_d_times_gcd: \forall m,n,d,c.
265 O \lt c \to d \divides (c*m) \to d \divides (c*n) \to d \divides c*gcd n m.
273 | (S p) \Rightarrow gcd_aux (S p) m (S p) ]
277 | (S p) \Rightarrow gcd_aux (S p) n (S p) ]]).
279 [ apply (nat_case1 n)
284 change with (d \divides c*gcd_aux (S m1) m (S m1)).
285 apply divides_times_gcd_aux
291 | apply (le_n (S m1))
297 | apply (nat_case1 m)
302 change with (d \divides c * gcd_aux (S m1) n (S m1)).
303 apply divides_times_gcd_aux
305 change with (O \lt c).
311 | apply (le_n (S m1)).
320 (*a particular case of the previous theorem (setting c=1)*)
321 theorem divides_d_gcd: \forall m,n,d.
322 d \divides m \to d \divides n \to d \divides gcd n m.
324 rewrite > (times_n_SO (gcd n m)).
325 rewrite < (sym_times (S O)).
326 apply (divides_d_times_gcd)
328 | rewrite > (sym_times (S O)).
329 rewrite < (times_n_SO m).
331 | rewrite > (sym_times (S O)).
332 rewrite < (times_n_SO n).
337 theorem eq_minus_gcd_aux: \forall p,m,n.O < n \to n \le m \to n \le p \to
338 \exists a,b. a*n - b*m = gcd_aux p m n \lor b*m - a*n = gcd_aux p m n.
343 |apply le_to_not_lt.assumption
346 [cut (n1 \divides m \lor n1 \ndivides m)
349 [rewrite > divides_to_divides_b_true
351 apply (ex_intro ? ? (S O)).
352 apply (ex_intro ? ? O).
361 |rewrite > not_divides_to_divides_b_false
363 (\exists a,b.a*n1 - b*m = gcd_aux n n1 (m \mod n1)
364 \lor b*m - a*n1 = gcd_aux n n1 (m \mod n1)).
366 (\exists a,b.a*(m \mod n1) - b*n1= gcd_aux n n1 (m \mod n1)
367 \lor b*n1 - a*(m \mod n1) = gcd_aux n n1 (m \mod n1))
368 [elim Hcut2.elim H5.elim H6
371 apply (ex_intro ? ? (a1+a*(m / n1))).
372 apply (ex_intro ? ? a).
375 rewrite < (sym_times n1).
376 rewrite > distr_times_plus.
377 rewrite > (sym_times n1).
378 rewrite > (sym_times n1).
379 rewrite > (div_mod m n1) in \vdash (? ? (? % ?) ?)
380 [rewrite > assoc_times.
382 rewrite > distr_times_plus.
383 rewrite < eq_minus_minus_minus_plus.
386 [rewrite < minus_n_n.reflexivity
393 apply (ex_intro ? ? (a1+a*(m / n1))).
394 apply (ex_intro ? ? a).
396 (* clear Hcut2.clear H5.clear H6.clear H. *)
398 rewrite > distr_times_plus.
400 rewrite > (sym_times n1).
401 rewrite > (div_mod m n1) in \vdash (? ? (? ? %) ?)
402 [rewrite > distr_times_plus.
403 rewrite > assoc_times.
404 rewrite < eq_minus_minus_minus_plus.
407 [rewrite < minus_n_n.reflexivity
413 |apply (H n1 (m \mod n1))
414 [cut (O \lt m \mod n1 \lor O = m \mod n1)
417 |absurd (n1 \divides m)
418 [apply mod_O_to_divides
425 |apply le_to_or_lt_eq.
432 apply (trans_le ? n1)
433 [change with (m \mod n1 < n1).
444 |apply (decidable_divides n1 m).
447 |apply (lt_to_le_to_lt ? n1);assumption
452 theorem eq_minus_gcd:
453 \forall m,n.\exists a,b.a*n - b*m = (gcd n m) \lor b*m - a*n = (gcd n m).
456 apply (leb_elim n m).
459 apply (ex_intro ? ? O).
460 apply (ex_intro ? ? (S O)).
463 apply sym_eq.apply minus_n_O.
467 a*(S m1) - b*m = (gcd_aux (S m1) m (S m1))
468 \lor b*m - a*(S m1) = (gcd_aux (S m1) m (S m1))).
469 apply eq_minus_gcd_aux.
470 unfold lt. apply le_S_S.apply le_O_n.
471 assumption.apply le_n.
474 apply (ex_intro ? ? (S O)).
475 apply (ex_intro ? ? O).
478 apply sym_eq.apply minus_n_O.
482 a*n - b*(S m1) = (gcd_aux (S m1) n (S m1))
483 \lor b*(S m1) - a*n = (gcd_aux (S m1) n (S m1))).
486 a*(S m1) - b*n = (gcd_aux (S m1) n (S m1))
488 b*n - a*(S m1) = (gcd_aux (S m1) n (S m1))).
489 elim Hcut.elim H2.elim H3.
490 apply (ex_intro ? ? a1).
491 apply (ex_intro ? ? a).
493 apply (ex_intro ? ? a1).
494 apply (ex_intro ? ? a).
496 apply eq_minus_gcd_aux.
497 unfold lt. apply le_S_S.apply le_O_n.
498 apply lt_to_le.apply not_le_to_lt.assumption.
502 (* some properties of gcd *)
504 theorem gcd_O_n: \forall n:nat. gcd O n = n.
505 intro.simplify.reflexivity.
508 theorem gcd_O_to_eq_O:\forall m,n:nat. (gcd m n) = O \to
510 intros.cut (O \divides n \land O \divides m).
511 elim Hcut.elim H2.split.
512 assumption.elim H1.assumption.
514 apply divides_gcd_nm.
517 theorem lt_O_gcd:\forall m,n:nat. O < n \to O < gcd m n.
519 apply (nat_case1 (gcd m n)).
521 generalize in match (gcd_O_to_eq_O m n H1).
523 rewrite < H4 in \vdash (? ? %).assumption.
524 intros.unfold lt.apply le_S_S.apply le_O_n.
527 theorem gcd_n_n: \forall n.gcd n n = n.
530 |apply le_to_le_to_eq
536 [apply lt_O_gcd.apply lt_O_S
538 [apply divides_n_n|apply divides_n_n]
544 theorem gcd_SO_to_lt_O: \forall i,n. (S O) < n \to gcd i n = (S O) \to
547 elim (le_to_or_lt_eq ? ? (le_O_n i))
549 |absurd ((gcd i n) = (S O))
554 apply (lt_to_not_eq (S O) n H).
555 apply sym_eq.assumption
560 theorem gcd_SO_to_lt_n: \forall i,n. (S O) < n \to i \le n \to gcd i n = (S O) \to
563 elim (le_to_or_lt_eq ? ? H1)
565 |absurd ((gcd i n) = (S O))
570 apply (lt_to_not_eq (S O) n H).
571 apply sym_eq.assumption
576 theorem gcd_n_times_nm: \forall n,m. O < m \to gcd n (n*m) = n.
577 intro.apply (nat_case n)
582 [apply lt_O_S|apply divides_gcd_n]
584 [apply lt_O_gcd.rewrite > (times_n_O O).
585 apply lt_times[apply lt_O_S|assumption]
587 [apply (witness ? ? m1).reflexivity
595 theorem symmetric_gcd: symmetric nat gcd.
597 (\forall n,m:nat. gcd n m = gcd m n).
599 cut (O < (gcd n m) \lor O = (gcd n m)).
601 cut (O < (gcd m n) \lor O = (gcd m n)).
604 apply divides_to_le.assumption.
605 apply divides_d_gcd.apply divides_gcd_n.apply divides_gcd_m.
606 apply divides_to_le.assumption.
607 apply divides_d_gcd.apply divides_gcd_n.apply divides_gcd_m.
610 elim Hcut2.rewrite > H2.rewrite > H3.reflexivity.
611 apply gcd_O_to_eq_O.apply sym_eq.assumption.
612 apply le_to_or_lt_eq.apply le_O_n.
615 elim Hcut1.rewrite > H1.rewrite > H2.reflexivity.
616 apply gcd_O_to_eq_O.apply sym_eq.assumption.
617 apply le_to_or_lt_eq.apply le_O_n.
620 variant sym_gcd: \forall n,m:nat. gcd n m = gcd m n \def
623 theorem le_gcd_times: \forall m,n,p:nat. O< p \to gcd m n \le gcd m (n*p).
625 apply (nat_case n).apply le_n.
629 rewrite > (times_n_O O).
630 apply lt_times.unfold lt.apply le_S_S.apply le_O_n.assumption.
632 apply (transitive_divides ? (S m1)).
634 apply (witness ? ? p).reflexivity.
638 theorem gcd_times_SO_to_gcd_SO: \forall m,n,p:nat. O < n \to O < p \to
639 gcd m (n*p) = (S O) \to gcd m n = (S O).
641 apply antisymmetric_le.
643 apply le_gcd_times.assumption.
644 change with (O < gcd m n).
645 apply lt_O_gcd.assumption.
648 (* for the "converse" of the previous result see the end of this development *)
650 theorem eq_gcd_SO_to_not_divides: \forall n,m. (S O) < n \to
651 (gcd n m) = (S O) \to \lnot (divides n m).
654 generalize in match H1.
658 [elim (gcd_times_SO_to_gcd_SO n n n2 ? ? H4)
659 [cut (gcd n (n*n2) = n)
660 [apply (lt_to_not_eq (S O) n)
661 [assumption|rewrite < H4.assumption]
662 |apply gcd_n_times_nm.assumption
664 |apply (trans_lt ? (S O))[apply le_n|assumption]
667 |elim (le_to_or_lt_eq O n2 (le_O_n n2));
670 apply (le_to_not_lt n (S O))
673 [rewrite > H4.apply lt_O_S
675 [apply (witness ? ? n2).reflexivity
685 theorem gcd_SO_n: \forall n:nat. gcd (S O) n = (S O).
687 apply antisym_le.apply divides_to_le.unfold lt.apply le_n.
689 cut (O < gcd (S O) n \lor O = gcd (S O) n).
690 elim Hcut.assumption.
692 apply (not_eq_O_S O).
693 cut ((S O)=O \land n=O).
694 elim Hcut1.apply sym_eq.assumption.
695 apply gcd_O_to_eq_O.apply sym_eq.assumption.
696 apply le_to_or_lt_eq.apply le_O_n.
699 theorem divides_gcd_mod: \forall m,n:nat. O < n \to
700 divides (gcd m n) (gcd n (m \mod n)).
703 apply divides_mod.assumption.
709 theorem divides_mod_gcd: \forall m,n:nat. O < n \to
710 divides (gcd n (m \mod n)) (gcd m n) .
714 apply (divides_mod_to_divides ? ? n).
720 theorem gcd_mod: \forall m,n:nat. O < n \to
721 (gcd n (m \mod n)) = (gcd m n) .
723 apply antisymmetric_divides.
724 apply divides_mod_gcd.assumption.
725 apply divides_gcd_mod.assumption.
730 theorem prime_to_gcd_SO: \forall n,m:nat. prime n \to n \ndivides m \to
732 intros.unfold prime in H.
735 apply not_lt_to_le.unfold Not.unfold lt.
737 apply H1.rewrite < (H3 (gcd n m)).
739 apply divides_gcd_n.assumption.
740 cut (O < gcd n m \lor O = gcd n m).
741 elim Hcut.assumption.
743 apply (not_le_Sn_O (S O)).
745 elim Hcut1.rewrite < H5 in \vdash (? ? %).assumption.
746 apply gcd_O_to_eq_O.apply sym_eq.assumption.
747 apply le_to_or_lt_eq.apply le_O_n.
750 (* primes and divides *)
751 theorem divides_times_to_divides: \forall n,p,q:nat.prime n \to n \divides p*q \to
752 n \divides p \lor n \divides q.
754 cut (n \divides p \lor n \ndivides p)
758 cut (\exists a,b. a*n - b*p = (S O) \lor b*p - a*n = (S O))
759 [elim Hcut1.elim H3.elim H4
761 rewrite > (times_n_SO q).rewrite < H5.
762 rewrite > distr_times_minus.
763 rewrite > (sym_times q (a1*p)).
764 rewrite > (assoc_times a1).
768 applyS (witness n (n*(q*a-a1*n2)) (q*a-a1*n2))
770 applyS (witness n ? ? (refl_eq ? ?)) (* timeout=50 *).
772 rewrite < (sym_times n).rewrite < assoc_times.
773 rewrite > (sym_times q).rewrite > assoc_times.
774 rewrite < (assoc_times a1).rewrite < (sym_times n).
775 rewrite > (assoc_times n).
776 rewrite < distr_times_minus.
777 apply (witness ? ? (q*a-a1*n2)).reflexivity
780 rewrite > (times_n_SO q).rewrite < H5.
781 rewrite > distr_times_minus.
782 rewrite > (sym_times q (a1*p)).
783 rewrite > (assoc_times a1).
784 elim H1.rewrite > H6.
785 rewrite < sym_times.rewrite > assoc_times.
786 rewrite < (assoc_times q).
787 rewrite < (sym_times n).
788 rewrite < distr_times_minus.
789 apply (witness ? ? (n2*a1-q*a)).reflexivity
790 ](* end second case *)
791 |rewrite < (prime_to_gcd_SO n p)
792 [apply eq_minus_gcd|assumption|assumption
796 |apply (decidable_divides n p).
797 apply (trans_lt ? (S O))
798 [unfold lt.apply le_n
799 |unfold prime in H.elim H. assumption
804 theorem divides_exp_to_divides:
805 \forall p,n,m:nat. prime p \to
806 p \divides n \sup m \to p \divides n.
807 intros 3.elim m.simplify in H1.
808 apply (transitive_divides p (S O)).assumption.
810 cut (p \divides n \lor p \divides n \sup n1).
811 elim Hcut.assumption.
812 apply H.assumption.assumption.
813 apply divides_times_to_divides.assumption.
817 theorem divides_exp_to_eq:
818 \forall p,q,m:nat. prime p \to prime q \to
819 p \divides q \sup m \to p = q.
823 apply (divides_exp_to_divides p q m).
824 assumption.assumption.
825 unfold prime in H.elim H.assumption.
828 theorem eq_gcd_times_SO: \forall m,n,p:nat. O < n \to O < p \to
829 gcd m n = (S O) \to gcd m p = (S O) \to gcd m (n*p) = (S O).
831 apply antisymmetric_le.
834 cut (divides (smallest_factor (gcd m (n*p))) n \lor
835 divides (smallest_factor (gcd m (n*p))) p).
837 apply (not_le_Sn_n (S O)).
838 change with ((S O) < (S O)).
839 rewrite < H2 in \vdash (? ? %).
840 apply (lt_to_le_to_lt ? (smallest_factor (gcd m (n*p)))).
841 apply lt_SO_smallest_factor.assumption.
843 rewrite > H2.unfold lt.apply le_n.
844 apply divides_d_gcd.assumption.
845 apply (transitive_divides ? (gcd m (n*p))).
846 apply divides_smallest_factor_n.
847 apply (trans_lt ? (S O)). unfold lt. apply le_n. assumption.
849 apply (not_le_Sn_n (S O)).
850 change with ((S O) < (S O)).
851 rewrite < H3 in \vdash (? ? %).
852 apply (lt_to_le_to_lt ? (smallest_factor (gcd m (n*p)))).
853 apply lt_SO_smallest_factor.assumption.
855 rewrite > H3.unfold lt.apply le_n.
856 apply divides_d_gcd.assumption.
857 apply (transitive_divides ? (gcd m (n*p))).
858 apply divides_smallest_factor_n.
859 apply (trans_lt ? (S O)). unfold lt. apply le_n. assumption.
861 apply divides_times_to_divides.
862 apply prime_smallest_factor_n.
864 apply (transitive_divides ? (gcd m (n*p))).
865 apply divides_smallest_factor_n.
866 apply (trans_lt ? (S O)).unfold lt. apply le_n. assumption.
868 change with (O < gcd m (n*p)).
870 rewrite > (times_n_O O).
871 apply lt_times.assumption.assumption.
874 theorem gcd_SO_to_divides_times_to_divides: \forall m,n,p:nat. O < n \to
875 gcd n m = (S O) \to n \divides (m*p) \to n \divides p.
877 cut (n \divides p \lor n \ndivides p)
880 |cut (\exists a,b. a*n - b*m = (S O) \lor b*m - a*n = (S O))
881 [elim Hcut1.elim H4.elim H5
883 rewrite > (times_n_SO p).rewrite < H6.
884 rewrite > distr_times_minus.
885 rewrite > (sym_times p (a1*m)).
886 rewrite > (assoc_times a1).
888 applyS (witness n ? ? (refl_eq ? ?)) (* timeout=50 *).
890 rewrite > (times_n_SO p).rewrite < H6.
891 rewrite > distr_times_minus.
892 rewrite > (sym_times p (a1*m)).
893 rewrite > (assoc_times a1).
895 applyS (witness n ? ? (refl_eq ? ?)).
896 ](* end second case *)
897 |rewrite < H1.apply eq_minus_gcd.
900 |apply (decidable_divides n p).
906 theorem divides_to_divides_times1: \forall p,q,n. prime p \to prime q \to p \neq q \to
907 divides p n \to divides q n \to divides (p*q) n.
910 elim (divides_times_to_divides ? ? ? H1 H4)
911 [elim H.apply False_ind.
912 apply H2.apply sym_eq.apply H8
914 |apply prime_to_lt_SO.assumption
917 apply (witness ? ? n1).
918 rewrite > assoc_times.
919 rewrite < H7.assumption
924 theorem divides_to_divides_times: \forall p,q,n. prime p \to p \ndivides q \to
925 divides p n \to divides q n \to divides (p*q) n.
928 elim (divides_times_to_divides ? ? ? H H2)
929 [apply False_ind.apply H1.assumption
931 apply (witness ? ? n1).
932 rewrite > sym_times in ⊢ (? ? ? (? % ?)).
933 rewrite > assoc_times.
934 rewrite < H6.assumption