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/library_auto/nat/gcd".
17 include "auto/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 (? ? ? (? ? (? % ?))).
53 rewrite < (div_mod ? ? H).
58 theorem divides_mod_to_divides: \forall p,m,n:nat. O < n \to
59 p \divides (m \mod n) \to p \divides n \to p \divides m.
63 apply (witness p m ((n1*(m / n))+n2)).
64 rewrite > distr_times_plus.
66 rewrite < assoc_times.
75 theorem divides_gcd_aux_mn: \forall p,m,n. O < n \to n \le m \to n \le p \to
76 gcd_aux p m n \divides m \land gcd_aux p m n \divides n.
84 | cut ((n1 \divides m) \lor (n1 \ndivides m))
87 [ rewrite > divides_to_divides_b_true
92 | apply (witness n1 n1 (S O)).
98 | rewrite > not_divides_to_divides_b_false
100 cut (gcd_aux n n1 (m \mod n1) \divides n1 \land
101 gcd_aux n n1 (m \mod n1) \divides mod m n1)
105 [ apply (divides_mod_to_divides ? ? n1);assumption
109 [ cut (O \lt m \mod n1 \lor O = mod m n1)
115 apply mod_O_to_divides
122 (*apply le_to_or_lt_eq.
129 | apply le_S_S_to_le.
130 apply (trans_le ? n1);auto
131 (*[ auto.change with (m \mod n1 < n1).
143 (*apply (decidable_divides n1 m).
149 theorem divides_gcd_nm: \forall n,m.
150 gcd n m \divides m \land gcd n m \divides n.
152 (*CSC: simplify simplifies too much because of a redex in gcd *)
158 | (S p) \Rightarrow gcd_aux (S p) m (S p) ]
162 | (S p) \Rightarrow gcd_aux (S p) n (S p) ] ] \divides m
168 | (S p) \Rightarrow gcd_aux (S p) m (S p) ]
172 | (S p) \Rightarrow gcd_aux (S p) n (S p) ] ] \divides n).
174 [ apply (nat_case1 n)
179 [ apply (witness m m (S O)).
181 | apply (witness m O O).
186 (gcd_aux (S m1) m (S m1) \divides m
188 gcd_aux (S m1) m (S m1) \divides (S m1)).
190 (*apply divides_gcd_aux_mn
205 [ apply (witness n O O).
207 | apply (witness n n (S O)).
212 (gcd_aux (S m1) n (S m1) \divides (S m1)
214 gcd_aux (S m1) n (S m1) \divides n).
215 cut (gcd_aux (S m1) n (S m1) \divides n
217 gcd_aux (S m1) n (S m1) \divides S m1)
221 | apply divides_gcd_aux_mn
226 | apply not_lt_to_le.
233 (*apply (trans_le ? (S n))
244 theorem divides_gcd_n: \forall n,m. gcd n m \divides n.
246 exact (proj2 ? ? (divides_gcd_nm n m)). (*auto non termina la dimostrazione*)
249 theorem divides_gcd_m: \forall n,m. gcd n m \divides m.
251 exact (proj1 ? ? (divides_gcd_nm n m)). (*auto non termina la dimostrazione*)
254 theorem divides_gcd_aux: \forall p,m,n,d. O < n \to n \le m \to n \le p \to
255 d \divides m \to d \divides n \to d \divides gcd_aux p m n.
258 [ absurd (O < n);auto
260 | apply le_to_not_lt.
264 cut (n1 \divides m \lor n1 \ndivides m)
266 rewrite > divides_to_divides_b_true;auto.
272 rewrite > not_divides_to_divides_b_false
275 [ cut (O \lt m \mod n1 \lor O = m \mod n1)
279 absurd (n1 \divides m);auto
280 (*[ apply mod_O_to_divides
282 | apply sym_eq.assumption.
288 (*apply le_to_or_lt_eq.
295 | apply le_S_S_to_le.
297 (*apply (trans_le ? n1)
298 [ change with (m \mod n1 < n1).
312 (*apply (decidable_divides n1 m).
317 theorem divides_d_gcd: \forall m,n,d.
318 d \divides m \to d \divides n \to d \divides gcd n m.
320 (*CSC: here simplify simplifies too much because of a redex in gcd *)
327 | (S p) \Rightarrow gcd_aux (S p) m (S p) ]
331 | (S p) \Rightarrow gcd_aux (S p) n (S p) ]]).
333 [ apply (nat_case1 n)
338 change with (d \divides gcd_aux (S m1) m (S m1)).
339 apply divides_gcd_aux
345 | apply le_n. (*chiude il goal anche con auto*)
351 | apply (nat_case1 m)
356 change with (d \divides gcd_aux (S m1) n (S m1)).
357 apply divides_gcd_aux
366 | apply le_n (*chiude il goal anche con auto*)
375 theorem eq_minus_gcd_aux: \forall p,m,n.O < n \to n \le m \to n \le p \to
376 \exists a,b. a*n - b*m = gcd_aux p m n \lor b*m - a*n = gcd_aux p m n.
379 [ absurd (O < n);auto
385 [ cut (n1 \divides m \lor n1 \ndivides m)
388 [ rewrite > divides_to_divides_b_true
390 apply (ex_intro ? ? (S O)).
391 apply (ex_intro ? ? O).
396 apply sym_eq.apply minus_n_O*)
400 | rewrite > not_divides_to_divides_b_false
403 a*n1 - b*m = gcd_aux n n1 (m \mod n1)
405 b*m - a*n1 = gcd_aux n n1 (m \mod n1)).
408 a*(m \mod n1) - b*n1= gcd_aux n n1 (m \mod n1)
410 b*n1 - a*(m \mod n1) = gcd_aux n n1 (m \mod n1))
416 apply (ex_intro ? ? (a1+a*(m / n1))).
417 apply (ex_intro ? ? a).
420 rewrite < (sym_times n1).
421 rewrite > distr_times_plus.
422 rewrite > (sym_times n1).
423 rewrite > (sym_times n1).
424 rewrite > (div_mod m n1) in \vdash (? ? (? % ?) ?);auto
425 (*[ rewrite > assoc_times.
427 rewrite > distr_times_plus.
428 rewrite < eq_minus_minus_minus_plus.
429 rewrite < sym_plus.auto.
431 [ rewrite < minus_n_n.
439 apply (ex_intro ? ? (a1+a*(m / n1))).
440 apply (ex_intro ? ? a).
442 (* clear Hcut2.clear H5.clear H6.clear H. *)
444 rewrite > distr_times_plus.
446 rewrite > (sym_times n1).
447 rewrite > (div_mod m n1) in \vdash (? ? (? ? %) ?)
448 [ rewrite > distr_times_plus.
449 rewrite > assoc_times.
450 rewrite < eq_minus_minus_minus_plus.
452 (*rewrite < sym_plus.
454 [ rewrite < minus_n_n.
461 | apply (H n1 (m \mod n1))
462 [ cut (O \lt m \mod n1 \lor O = m \mod n1)
465 | absurd (n1 \divides m);auto
466 (*[ apply mod_O_to_divides
475 (*apply le_to_or_lt_eq.
482 | apply le_S_S_to_le.
484 (*apply (trans_le ? n1)
485 [ change with (m \mod n1 < n1).
497 (*apply (decidable_divides n1 m).
501 (*apply (lt_to_le_to_lt ? n1);assumption *)
506 theorem eq_minus_gcd:
507 \forall m,n.\exists a,b.a*n - b*m = (gcd n m) \lor b*m - a*n = (gcd n m).
511 [ apply (nat_case1 n)
514 apply (ex_intro ? ? O).
515 apply (ex_intro ? ? (S O)).
524 a*(S m1) - b*m = (gcd_aux (S m1) m (S m1))
525 \lor b*m - a*(S m1) = (gcd_aux (S m1) m (S m1))).
527 (*apply eq_minus_gcd_aux
535 | apply (nat_case1 m)
538 apply (ex_intro ? ? (S O)).
539 apply (ex_intro ? ? O).
548 a*n - b*(S m1) = (gcd_aux (S m1) n (S m1))
549 \lor b*(S m1) - a*n = (gcd_aux (S m1) n (S m1))).
552 a*(S m1) - b*n = (gcd_aux (S m1) n (S m1))
554 b*n - a*(S m1) = (gcd_aux (S m1) n (S m1)))
557 elim H3;apply (ex_intro ? ? a1);auto
558 (*[ apply (ex_intro ? ? a1).
559 apply (ex_intro ? ? a).
562 | apply (ex_intro ? ? a1).
563 apply (ex_intro ? ? a).
567 | apply eq_minus_gcd_aux;auto
571 | auto.apply lt_to_le.
581 (* some properties of gcd *)
583 theorem gcd_O_n: \forall n:nat. gcd O n = n.
585 (*intro.simplify.reflexivity.*)
588 theorem gcd_O_to_eq_O:\forall m,n:nat. (gcd m n) = O \to
591 cut (O \divides n \land O \divides m)
605 theorem lt_O_gcd:\forall m,n:nat. O < n \to O < gcd m n.
608 (*apply (nat_case1 (gcd m n))
610 generalize in match (gcd_O_to_eq_O m n H1).
613 rewrite < H4 in \vdash (? ? %).
622 theorem gcd_n_n: \forall n.gcd n n = n.
627 | apply le_to_le_to_eq
628 [ apply divides_to_le
630 | apply divides_gcd_n
632 | apply divides_to_le
633 [ apply lt_O_gcd.apply lt_O_S
634 | apply divides_d_gcd
643 theorem gcd_SO_to_lt_O: \forall i,n. (S O) < n \to gcd i n = (S O) \to
646 elim (le_to_or_lt_eq ? ? (le_O_n i))
648 | absurd ((gcd i n) = (S O))
654 apply (lt_to_not_eq (S O) n H).
662 theorem gcd_SO_to_lt_n: \forall i,n. (S O) < n \to i \le n \to gcd i n = (S O) \to
665 elim (le_to_or_lt_eq ? ? H1)
667 |absurd ((gcd i n) = (S O))
672 apply (lt_to_not_eq (S O) n H).
673 apply sym_eq.assumption
678 theorem gcd_n_times_nm: \forall n,m. O < m \to gcd n (n*m) = n.
679 intro.apply (nat_case n)
684 [apply lt_O_S|apply divides_gcd_n]
686 [apply lt_O_gcd.rewrite > (times_n_O O).
687 apply lt_times[apply lt_O_S|assumption]
689 [apply (witness ? ? m1).reflexivity
697 theorem symmetric_gcd: symmetric nat gcd.
698 (*CSC: bug here: unfold symmetric does not work *)
700 (\forall n,m:nat. gcd n m = gcd m n).
703 (*cut (O < (gcd n m) \lor O = (gcd n m))
705 [ cut (O < (gcd m n) \lor O = (gcd m n))
708 [ apply divides_to_le
710 | apply divides_d_gcd
711 [ apply divides_gcd_n
712 | apply divides_gcd_m
715 | apply divides_to_le
717 | apply divides_d_gcd
718 [ apply divides_gcd_n
719 | apply divides_gcd_m
729 | apply gcd_O_to_eq_O.
734 | apply le_to_or_lt_eq.
743 | apply gcd_O_to_eq_O.apply sym_eq.
747 | apply le_to_or_lt_eq.
752 variant sym_gcd: \forall n,m:nat. gcd n m = gcd m n \def
755 theorem le_gcd_times: \forall m,n,p:nat. O< p \to gcd m n \le gcd m (n*p).
763 (*rewrite > (times_n_O O).
770 | apply divides_d_gcd;auto
771 (*[ apply (transitive_divides ? (S m1))
772 [ apply divides_gcd_m
773 | apply (witness ? ? p).
776 | apply divides_gcd_n
782 theorem gcd_times_SO_to_gcd_SO: \forall m,n,p:nat. O < n \to O < p \to
783 gcd m (n*p) = (S O) \to gcd m n = (S O).
785 apply antisymmetric_le
788 (*apply le_gcd_times.
791 (*change with (O < gcd m n).
797 (* for the "converse" of the previous result see the end of this development *)
799 theorem eq_gcd_SO_to_not_divides: \forall n,m. (S O) < n \to
800 (gcd n m) = (S O) \to \lnot (divides n m).
803 generalize in match H1.
807 [ elim (gcd_times_SO_to_gcd_SO n n n2 ? ? H4)
808 [ cut (gcd n (n*n2) = n);auto
809 (*[ auto.apply (lt_to_not_eq (S O) n)
814 | apply gcd_n_times_nm.
818 (*apply (trans_lt ? (S O))
824 | elim (le_to_or_lt_eq O n2 (le_O_n n2))
827 apply (le_to_not_lt n (S O))
829 apply divides_to_le;auto
832 | apply divides_d_gcd
833 [ apply (witness ? ? n2).
844 theorem gcd_SO_n: \forall n:nat. gcd (S O) n = (S O).
848 [ apply divides_to_le
851 | apply divides_gcd_n
853 | cut (O < gcd (S O) n \lor O = gcd (S O) n)
857 apply (not_eq_O_S O).
858 cut ((S O)=O \land n=O)
862 | apply gcd_O_to_eq_O.
867 | apply le_to_or_lt_eq.
873 theorem divides_gcd_mod: \forall m,n:nat. O < n \to
874 divides (gcd m n) (gcd n (m \mod n)).
877 (*apply divides_d_gcd
880 | apply divides_gcd_n
881 | apply divides_gcd_m
883 | apply divides_gcd_m.
887 theorem divides_mod_gcd: \forall m,n:nat. O < n \to
888 divides (gcd n (m \mod n)) (gcd m n) .
891 (*apply divides_d_gcd
892 [ apply divides_gcd_n
893 | apply (divides_mod_to_divides ? ? n)
895 | apply divides_gcd_m
896 | apply divides_gcd_n
901 theorem gcd_mod: \forall m,n:nat. O < n \to
902 (gcd n (m \mod n)) = (gcd m n) .
905 (*apply antisymmetric_divides
906 [ apply divides_mod_gcd.
908 | apply divides_gcd_mod.
915 theorem prime_to_gcd_SO: \forall n,m:nat. prime n \to n \ndivides m \to
917 intros.unfold prime in H.
920 [ apply not_lt_to_le.unfold Not.unfold lt.
923 rewrite < (H3 (gcd n m));auto
924 (*[ apply divides_gcd_m
925 | apply divides_gcd_n
928 | cut (O < gcd n m \lor O = gcd n m)
932 apply (not_le_Sn_O (S O)).
935 rewrite < H5 in \vdash (? ? %).
938 (*apply gcd_O_to_eq_O.
944 (*apply le_to_or_lt_eq.
950 theorem divides_times_to_divides: \forall n,p,q:nat.prime n \to n \divides p*q \to
951 n \divides p \lor n \divides q.
953 cut (n \divides p \lor n \ndivides p)
957 cut (\exists a,b. a*n - b*p = (S O) \lor b*p - a*n = (S O))
958 [elim Hcut1.elim H3.elim H4
960 rewrite > (times_n_SO q).rewrite < H5.
961 rewrite > distr_times_minus.
962 rewrite > (sym_times q (a1*p)).
963 rewrite > (assoc_times a1).
967 applyS (witness n (n*(q*a-a1*n2)) (q*a-a1*n2))
969 applyS (witness n ? ? (refl_eq ? ?)) (* timeout=50 *)
971 rewrite < (sym_times n).rewrite < assoc_times.
972 rewrite > (sym_times q).rewrite > assoc_times.
973 rewrite < (assoc_times a1).rewrite < (sym_times n).
974 rewrite > (assoc_times n).
975 rewrite < distr_times_minus.
976 apply (witness ? ? (q*a-a1*n2)).reflexivity
979 rewrite > (times_n_SO q).rewrite < H5.
980 rewrite > distr_times_minus.
981 rewrite > (sym_times q (a1*p)).
982 rewrite > (assoc_times a1).
986 rewrite < sym_times.rewrite > assoc_times.
987 rewrite < (assoc_times q).
988 rewrite < (sym_times n).
989 rewrite < distr_times_minus.
990 apply (witness ? ? (n2*a1-q*a)).
992 ](* end second case *)
993 | rewrite < (prime_to_gcd_SO n p);auto
994 (* [ apply eq_minus_gcd
1000 | apply (decidable_divides n p).
1001 apply (trans_lt ? (S O))
1005 | unfold prime in H.
1012 theorem eq_gcd_times_SO: \forall m,n,p:nat. O < n \to O < p \to
1013 gcd m n = (S O) \to gcd m p = (S O) \to gcd m (n*p) = (S O).
1015 apply antisymmetric_le
1016 [ apply not_lt_to_le.
1018 cut (divides (smallest_factor (gcd m (n*p))) n \lor
1019 divides (smallest_factor (gcd m (n*p))) p)
1021 [ apply (not_le_Sn_n (S O)).
1022 change with ((S O) < (S O)).
1023 rewrite < H2 in \vdash (? ? %).
1024 apply (lt_to_le_to_lt ? (smallest_factor (gcd m (n*p))))
1026 (*apply lt_SO_smallest_factor.
1028 | apply divides_to_le;auto
1032 | apply divides_d_gcd
1034 | apply (transitive_divides ? (gcd m (n*p)))
1035 [ apply divides_smallest_factor_n.
1036 apply (trans_lt ? (S O))
1041 | apply divides_gcd_n
1046 | apply (not_le_Sn_n (S O)).
1047 change with ((S O) < (S O)).
1048 rewrite < H3 in \vdash (? ? %).
1049 apply (lt_to_le_to_lt ? (smallest_factor (gcd m (n*p))))
1050 [ apply lt_SO_smallest_factor.
1052 | apply divides_to_le;auto
1056 | apply divides_d_gcd
1058 | apply (transitive_divides ? (gcd m (n*p)))
1059 [ apply divides_smallest_factor_n.
1060 apply (trans_lt ? (S O))
1065 | apply divides_gcd_n
1071 | apply divides_times_to_divides;auto
1072 (*[ apply prime_smallest_factor_n.
1074 | auto.apply (transitive_divides ? (gcd m (n*p)))
1075 [ apply divides_smallest_factor_n.
1076 apply (trans_lt ? (S O))
1081 | apply divides_gcd_m
1086 (*change with (O < gcd m (n*p)).
1088 rewrite > (times_n_O O).
1089 apply lt_times;assumption.*)
1093 theorem gcd_SO_to_divides_times_to_divides: \forall m,n,p:nat. O < n \to
1094 gcd n m = (S O) \to n \divides (m*p) \to n \divides p.
1096 cut (n \divides p \lor n \ndivides p)
1099 | cut (\exists a,b. a*n - b*m = (S O) \lor b*m - a*n = (S O))
1100 [ elim Hcut1.elim H4.elim H5
1102 rewrite > (times_n_SO p).rewrite < H6.
1103 rewrite > distr_times_minus.
1104 rewrite > (sym_times p (a1*m)).
1105 rewrite > (assoc_times a1).
1107 applyS (witness n ? ? (refl_eq ? ?)) (* timeout=50 *).
1109 rewrite > (times_n_SO p).rewrite < H6.
1110 rewrite > distr_times_minus.
1111 rewrite > (sym_times p (a1*m)).
1112 rewrite > (assoc_times a1).
1114 applyS (witness n ? ? (refl_eq ? ?)).
1115 ](* end second case *)
1121 (*apply (decidable_divides n p).