X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2Fnat%2Fgcd.ma;h=65f61b581691cdabbdaeeb34fc7d10ac21927a93;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=792629aaa04c224689edcf2a152a3c2925aa547f;hpb=b3f74fab711510628cff64aff3e48e73cc9f6e09;p=helm.git diff --git a/helm/matita/library/nat/gcd.ma b/helm/matita/library/nat/gcd.ma index 792629aaa..65f61b581 100644 --- a/helm/matita/library/nat/gcd.ma +++ b/helm/matita/library/nat/gcd.ma @@ -136,7 +136,7 @@ intros.change with \land gcd_aux (S m1) m (S m1) \divides (S m1)). apply divides_gcd_aux_mn. -simplify.apply le_S_S.apply le_O_n. +unfold lt.apply le_S_S.apply le_O_n. assumption.apply le_n. simplify.intro. apply (nat_case1 m). @@ -152,8 +152,8 @@ cut (gcd_aux (S m1) n (S m1) \divides n gcd_aux (S m1) n (S m1) \divides S m1). elim Hcut.split.assumption.assumption. apply divides_gcd_aux_mn. -simplify.apply le_S_S.apply le_O_n. -apply not_lt_to_le.simplify.intro.apply H. +unfold lt.apply le_S_S.apply le_O_n. +apply not_lt_to_le.unfold Not. unfold lt.intro.apply H. rewrite > H1.apply (trans_le ? (S n)). apply le_n_Sn.assumption.apply le_n. qed. @@ -221,13 +221,13 @@ apply (nat_case1 n).simplify.intros.assumption. intros. change with (d \divides gcd_aux (S m1) m (S m1)). apply divides_gcd_aux. -simplify.apply le_S_S.apply le_O_n.assumption.apply le_n.assumption. +unfold lt.apply le_S_S.apply le_O_n.assumption.apply le_n.assumption. rewrite < H2.assumption. apply (nat_case1 m).simplify.intros.assumption. intros. change with (d \divides gcd_aux (S m1) n (S m1)). apply divides_gcd_aux. -simplify.apply le_S_S.apply le_O_n. +unfold lt.apply le_S_S.apply le_O_n. apply lt_to_le.apply not_le_to_lt.assumption.apply le_n.assumption. rewrite < H2.assumption. qed. @@ -343,7 +343,7 @@ change with a*(S m1) - b*m = (gcd_aux (S m1) m (S m1)) \lor b*m - a*(S m1) = (gcd_aux (S m1) m (S m1))). apply eq_minus_gcd_aux. -simplify. apply le_S_S.apply le_O_n. +unfold lt. apply le_S_S.apply le_O_n. assumption.apply le_n. apply (nat_case1 m). simplify.intros. @@ -370,7 +370,7 @@ apply (ex_intro ? ? a1). apply (ex_intro ? ? a). left.assumption. apply eq_minus_gcd_aux. -simplify. apply le_S_S.apply le_O_n. +unfold lt. apply le_S_S.apply le_O_n. apply lt_to_le.apply not_le_to_lt.assumption. apply le_n. qed. @@ -390,6 +390,16 @@ rewrite < H. apply divides_gcd_nm. qed. +theorem lt_O_gcd:\forall m,n:nat. O < n \to O < gcd m n. +intros. +apply (nat_case1 (gcd m n)). +intros. +generalize in match (gcd_O_to_eq_O m n H1). +intros.elim H2. +rewrite < H4 in \vdash (? ? %).assumption. +intros.unfold lt.apply le_S_S.apply le_O_n. +qed. + theorem symmetric_gcd: symmetric nat gcd. change with (\forall n,m:nat. gcd n m = gcd m n). @@ -418,9 +428,36 @@ qed. variant sym_gcd: \forall n,m:nat. gcd n m = gcd m n \def symmetric_gcd. +theorem le_gcd_times: \forall m,n,p:nat. O< p \to gcd m n \le gcd m (n*p). +intros. +apply (nat_case n).reflexivity. +intro. +apply divides_to_le. +apply lt_O_gcd. +rewrite > (times_n_O O). +apply lt_times.unfold lt.apply le_S_S.apply le_O_n.assumption. +apply divides_d_gcd. +apply (transitive_divides ? (S m1)). +apply divides_gcd_m. +apply (witness ? ? p).reflexivity. +apply divides_gcd_n. +qed. + +theorem gcd_times_SO_to_gcd_SO: \forall m,n,p:nat. O < n \to O < p \to +gcd m (n*p) = (S O) \to gcd m n = (S O). +intros. +apply antisymmetric_le. +rewrite < H2. +apply le_gcd_times.assumption. +change with (O < gcd m n). +apply lt_O_gcd.assumption. +qed. + +(* for the "converse" of the previous result see the end of this development *) + theorem gcd_SO_n: \forall n:nat. gcd (S O) n = (S O). intro. -apply antisym_le.apply divides_to_le.simplify.apply le_n. +apply antisym_le.apply divides_to_le.unfold lt.apply le_n. apply divides_gcd_n. cut (O < gcd (S O) n \lor O = gcd (S O) n). elim Hcut.assumption. @@ -432,7 +469,7 @@ apply gcd_O_to_eq_O.apply sym_eq.assumption. apply le_to_or_lt_eq.apply le_O_n. qed. -theorem divides_gcd_mod: \forall m,n:nat. O < n \to O < m \to +theorem divides_gcd_mod: \forall m,n:nat. O < n \to divides (gcd m n) (gcd n (m \mod n)). intros. apply divides_d_gcd. @@ -442,7 +479,7 @@ apply divides_gcd_m. apply divides_gcd_m. qed. -theorem divides_mod_gcd: \forall m,n:nat. O < n \to O < m \to +theorem divides_mod_gcd: \forall m,n:nat. O < n \to divides (gcd n (m \mod n)) (gcd m n) . intros. apply divides_d_gcd. @@ -453,11 +490,19 @@ apply divides_gcd_m. apply divides_gcd_n. qed. +theorem gcd_mod: \forall m,n:nat. O < n \to +(gcd n (m \mod n)) = (gcd m n) . +intros. +apply antisymmetric_divides. +apply divides_mod_gcd.assumption. +apply divides_gcd_mod.assumption. +qed. + (* gcd and primes *) theorem prime_to_gcd_SO: \forall n,m:nat. prime n \to n \ndivides m \to gcd n m = (S O). -intros.simplify in H.change with (gcd n m = (S O)). +intros.unfold prime in H.change with (gcd n m = (S O)). elim H. apply antisym_le. apply not_lt_to_le. @@ -512,6 +557,52 @@ rewrite < (prime_to_gcd_SO n p). apply eq_minus_gcd. assumption.assumption. apply (decidable_divides n p). -apply (trans_lt ? (S O)).simplify.apply le_n. -simplify in H.elim H. assumption. +apply (trans_lt ? (S O)).unfold lt.apply le_n. +unfold prime in H.elim H. assumption. +qed. + +theorem eq_gcd_times_SO: \forall m,n,p:nat. O < n \to O < p \to +gcd m n = (S O) \to gcd m p = (S O) \to gcd m (n*p) = (S O). +intros. +apply antisymmetric_le. +apply not_lt_to_le. +unfold Not.intro. +cut (divides (smallest_factor (gcd m (n*p))) n \lor + divides (smallest_factor (gcd m (n*p))) p). +elim Hcut. +apply (not_le_Sn_n (S O)). +change with ((S O) < (S O)). +rewrite < H2 in \vdash (? ? %). +apply (lt_to_le_to_lt ? (smallest_factor (gcd m (n*p)))). +apply lt_SO_smallest_factor.assumption. +apply divides_to_le. +rewrite > H2.unfold lt.apply le_n. +apply divides_d_gcd.assumption. +apply (transitive_divides ? (gcd m (n*p))). +apply divides_smallest_factor_n. +apply (trans_lt ? (S O)). unfold lt. apply le_n. assumption. +apply divides_gcd_n. +apply (not_le_Sn_n (S O)). +change with ((S O) < (S O)). +rewrite < H3 in \vdash (? ? %). +apply (lt_to_le_to_lt ? (smallest_factor (gcd m (n*p)))). +apply lt_SO_smallest_factor.assumption. +apply divides_to_le. +rewrite > H3.unfold lt.apply le_n. +apply divides_d_gcd.assumption. +apply (transitive_divides ? (gcd m (n*p))). +apply divides_smallest_factor_n. +apply (trans_lt ? (S O)). unfold lt. apply le_n. assumption. +apply divides_gcd_n. +apply divides_times_to_divides. +apply prime_smallest_factor_n. +assumption. +apply (transitive_divides ? (gcd m (n*p))). +apply divides_smallest_factor_n. +apply (trans_lt ? (S O)).unfold lt. apply le_n. assumption. +apply divides_gcd_m. +change with (O < gcd m (n*p)). +apply lt_O_gcd. +rewrite > (times_n_O O). +apply lt_times.assumption.assumption. qed.