X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2Fnat%2Fgcd.ma;h=65f61b581691cdabbdaeeb34fc7d10ac21927a93;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=587314315268fc875ab715ab21ac83fd694c1613;hpb=5a702cea95883f7095c16b450e065ccb1714fc5a;p=helm.git diff --git a/helm/matita/library/nat/gcd.ma b/helm/matita/library/nat/gcd.ma index 587314315..65f61b581 100644 --- a/helm/matita/library/nat/gcd.ma +++ b/helm/matita/library/nat/gcd.ma @@ -22,7 +22,7 @@ match divides_b n m with | false \Rightarrow match p with [O \Rightarrow n - |(S q) \Rightarrow gcd_aux q n (mod m n)]]. + |(S q) \Rightarrow gcd_aux q n (m \mod n)]]. definition gcd : nat \to nat \to nat \def \lambda n,m:nat. @@ -36,29 +36,25 @@ definition gcd : nat \to nat \to nat \def [ O \Rightarrow n | (S p) \Rightarrow gcd_aux (S p) n (S p) ]]. -theorem divides_mod: \forall p,m,n:nat. O < n \to divides p m \to divides p n \to -divides p (mod m n). +theorem divides_mod: \forall p,m,n:nat. O < n \to p \divides m \to p \divides n \to +p \divides (m \mod n). intros.elim H1.elim H2. -apply witness ? ? (n2 - n1*(div m n)). +apply (witness ? ? (n2 - n1*(m / n))). rewrite > distr_times_minus. rewrite < H3. rewrite < assoc_times. rewrite < H4. apply sym_eq. apply plus_to_minus. -rewrite > div_mod m n in \vdash (? ? %). rewrite > sym_times. -apply eq_plus_to_le ? ? (mod m n). -reflexivity. +apply div_mod. assumption. -rewrite > sym_times. -apply div_mod.assumption. qed. theorem divides_mod_to_divides: \forall p,m,n:nat. O < n \to -divides p (mod m n) \to divides p n \to divides p m. +p \divides (m \mod n) \to p \divides n \to p \divides m. intros.elim H1.elim H2. -apply witness p m ((n1*(div m n))+n2). +apply (witness p m ((n1*(m / n))+n2)). rewrite > distr_times_plus. rewrite < H3. rewrite < assoc_times. @@ -67,34 +63,32 @@ apply div_mod.assumption. qed. theorem divides_gcd_aux_mn: \forall p,m,n. O < n \to n \le m \to n \le p \to -divides (gcd_aux p m n) m \land divides (gcd_aux p m n) n. +gcd_aux p m n \divides m \land gcd_aux p m n \divides n. intro.elim p. -absurd O < n.assumption.apply le_to_not_lt.assumption. -cut (divides n1 m) \lor \not (divides n1 m). +absurd (O < n).assumption.apply le_to_not_lt.assumption. +cut ((n1 \divides m) \lor (n1 \ndivides m)). change with -(divides -(match divides_b n1 m with +((match divides_b n1 m with [ true \Rightarrow n1 -| false \Rightarrow gcd_aux n n1 (mod m n1)]) m) \land -(divides +| false \Rightarrow gcd_aux n n1 (m \mod n1)]) \divides m \land (match divides_b n1 m with [ true \Rightarrow n1 -| false \Rightarrow gcd_aux n n1 (mod m n1)]) n1). +| false \Rightarrow gcd_aux n n1 (m \mod n1)]) \divides n1). elim Hcut.rewrite > divides_to_divides_b_true. simplify. -split.assumption.apply witness n1 n1 (S O).apply times_n_SO. +split.assumption.apply (witness n1 n1 (S O)).apply times_n_SO. assumption.assumption. rewrite > not_divides_to_divides_b_false. change with -(divides (gcd_aux n n1 (mod m n1)) m) \land -(divides (gcd_aux n n1 (mod m n1)) n1). -cut (divides (gcd_aux n n1 (mod m n1)) n1) \land -(divides (gcd_aux n n1 (mod m n1)) (mod m n1)). +(gcd_aux n n1 (m \mod n1) \divides m \land +gcd_aux n n1 (m \mod n1) \divides n1). +cut (gcd_aux n n1 (m \mod n1) \divides n1 \land +gcd_aux n n1 (m \mod n1) \divides mod m n1). elim Hcut1. -split.apply divides_mod_to_divides ? ? n1. +split.apply (divides_mod_to_divides ? ? n1). assumption.assumption.assumption.assumption. apply H. -cut O \lt mod m n1 \lor O = mod m n1. +cut (O \lt m \mod n1 \lor O = mod m n1). elim Hcut1.assumption. apply False_ind.apply H4.apply mod_O_to_divides. assumption.apply sym_eq.assumption. @@ -102,18 +96,17 @@ apply le_to_or_lt_eq.apply le_O_n. apply lt_to_le. apply lt_mod_m_m.assumption. apply le_S_S_to_le. -apply trans_le ? n1. -change with mod m n1 < n1. +apply (trans_le ? n1). +change with (m \mod n1 < n1). apply lt_mod_m_m.assumption.assumption. assumption.assumption. -apply decidable_divides n1 m.assumption. +apply (decidable_divides n1 m).assumption. qed. theorem divides_gcd_nm: \forall n,m. -divides (gcd n m) m \land divides (gcd n m) n. +gcd n m \divides m \land gcd n m \divides n. intros. change with -divides (match leb n m with [ true \Rightarrow match n with @@ -122,10 +115,9 @@ divides | false \Rightarrow match m with [ O \Rightarrow n - | (S p) \Rightarrow gcd_aux (S p) n (S p) ]]) m + | (S p) \Rightarrow gcd_aux (S p) n (S p) ] ] \divides m \land - divides -(match leb n m with +match leb n m with [ true \Rightarrow match n with [ O \Rightarrow m @@ -133,90 +125,88 @@ divides | false \Rightarrow match m with [ O \Rightarrow n - | (S p) \Rightarrow gcd_aux (S p) n (S p) ]]) n. -apply leb_elim n m. -apply nat_case1 n. + | (S p) \Rightarrow gcd_aux (S p) n (S p) ] ] \divides n). +apply (leb_elim n m). +apply (nat_case1 n). simplify.intros.split. -apply witness m m (S O).apply times_n_SO. -apply witness m O O.apply times_n_O. +apply (witness m m (S O)).apply times_n_SO. +apply (witness m O O).apply times_n_O. intros.change with -divides (gcd_aux (S m1) m (S m1)) m +(gcd_aux (S m1) m (S m1) \divides m \land -divides (gcd_aux (S m1) m (S m1)) (S m1). +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. +apply (nat_case1 m). simplify.intros.split. -apply witness n O O.apply times_n_O. -apply witness n n (S O).apply times_n_SO. +apply (witness n O O).apply times_n_O. +apply (witness n n (S O)).apply times_n_SO. intros.change with -divides (gcd_aux (S m1) n (S m1)) (S m1) +(gcd_aux (S m1) n (S m1) \divides (S m1) \land -divides (gcd_aux (S m1) n (S m1)) n. -cut divides (gcd_aux (S m1) n (S m1)) n +gcd_aux (S m1) n (S m1) \divides n). +cut (gcd_aux (S m1) n (S m1) \divides n \land -divides (gcd_aux (S m1) n (S m1)) (S m1). +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. -rewrite > H1.apply trans_le ? (S n). +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. -theorem divides_gcd_n: \forall n,m. -divides (gcd n m) n. +theorem divides_gcd_n: \forall n,m. gcd n m \divides n. intros. -exact proj2 ? ? (divides_gcd_nm n m). +exact (proj2 ? ? (divides_gcd_nm n m)). qed. -theorem divides_gcd_m: \forall n,m. -divides (gcd n m) m. +theorem divides_gcd_m: \forall n,m. gcd n m \divides m. intros. -exact proj1 ? ? (divides_gcd_nm n m). +exact (proj1 ? ? (divides_gcd_nm n m)). qed. theorem divides_gcd_aux: \forall p,m,n,d. O < n \to n \le m \to n \le p \to -divides d m \to divides d n \to divides d (gcd_aux p m n). +d \divides m \to d \divides n \to d \divides gcd_aux p m n. intro.elim p. -absurd O < n.assumption.apply le_to_not_lt.assumption. +absurd (O < n).assumption.apply le_to_not_lt.assumption. change with -divides d +(d \divides (match divides_b n1 m with [ true \Rightarrow n1 -| false \Rightarrow gcd_aux n n1 (mod m n1)]). -cut divides n1 m \lor \not (divides n1 m). +| false \Rightarrow gcd_aux n n1 (m \mod n1)])). +cut (n1 \divides m \lor n1 \ndivides m). elim Hcut. rewrite > divides_to_divides_b_true. simplify.assumption. assumption.assumption. rewrite > not_divides_to_divides_b_false. -change with divides d (gcd_aux n n1 (mod m n1)). +change with (d \divides gcd_aux n n1 (m \mod n1)). apply H. -cut O \lt mod m n1 \lor O = mod m n1. +cut (O \lt m \mod n1 \lor O = m \mod n1). elim Hcut1.assumption. -absurd divides n1 m.apply mod_O_to_divides. +absurd (n1 \divides m).apply mod_O_to_divides. assumption.apply sym_eq.assumption.assumption. apply le_to_or_lt_eq.apply le_O_n. apply lt_to_le. apply lt_mod_m_m.assumption. apply le_S_S_to_le. -apply trans_le ? n1. -change with mod m n1 < n1. +apply (trans_le ? n1). +change with (m \mod n1 < n1). apply lt_mod_m_m.assumption.assumption. assumption. apply divides_mod.assumption.assumption.assumption. assumption.assumption. -apply decidable_divides n1 m.assumption. +apply (decidable_divides n1 m).assumption. qed. theorem divides_d_gcd: \forall m,n,d. -divides d m \to divides d n \to divides d (gcd n m). +d \divides m \to d \divides n \to d \divides gcd n m. intros. change with -divides d ( +(d \divides match leb n m with [ true \Rightarrow match n with @@ -226,70 +216,69 @@ match leb n m with match m with [ O \Rightarrow n | (S p) \Rightarrow gcd_aux (S p) n (S p) ]]). -apply leb_elim n m. -apply nat_case1 n.simplify.intros.assumption. +apply (leb_elim n m). +apply (nat_case1 n).simplify.intros.assumption. intros. -change with divides d (gcd_aux (S m1) m (S m1)). +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. +apply (nat_case1 m).simplify.intros.assumption. intros. -change with divides d (gcd_aux (S m1) n (S m1)). +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. theorem eq_minus_gcd_aux: \forall p,m,n.O < n \to n \le m \to n \le p \to -ex nat (\lambda a. ex nat (\lambda b. -a*n - b*m = (gcd_aux p m n) \lor b*m - a*n = (gcd_aux p m n))). +\exists a,b. a*n - b*m = gcd_aux p m n \lor b*m - a*n = gcd_aux p m n. intro. elim p. -absurd O < n.assumption.apply le_to_not_lt.assumption. -cut O < m. -cut (divides n1 m) \lor \not (divides n1 m). +absurd (O < n).assumption.apply le_to_not_lt.assumption. +cut (O < m). +cut (n1 \divides m \lor n1 \ndivides m). change with -ex nat (\lambda a. ex nat (\lambda b. +(\exists a,b. a*n1 - b*m = match divides_b n1 m with [ true \Rightarrow n1 -| false \Rightarrow gcd_aux n n1 (mod m n1)] +| false \Rightarrow gcd_aux n n1 (m \mod n1)] \lor b*m - a*n1 = match divides_b n1 m with [ true \Rightarrow n1 -| false \Rightarrow gcd_aux n n1 (mod m n1)])). +| false \Rightarrow gcd_aux n n1 (m \mod n1)]). elim Hcut1. rewrite > divides_to_divides_b_true. simplify. -apply ex_intro ? ? (S O). -apply ex_intro ? ? O. +apply (ex_intro ? ? (S O)). +apply (ex_intro ? ? O). left.simplify.rewrite < plus_n_O. apply sym_eq.apply minus_n_O. assumption.assumption. rewrite > not_divides_to_divides_b_false. change with -ex nat (\lambda a. ex nat (\lambda b. -a*n1 - b*m = gcd_aux n n1 (mod m n1) +(\exists a,b. +a*n1 - b*m = gcd_aux n n1 (m \mod n1) \lor -b*m - a*n1 = gcd_aux n n1 (mod m n1))). +b*m - a*n1 = gcd_aux n n1 (m \mod n1)). cut -ex nat (\lambda a. ex nat (\lambda b. -a*(mod m n1) - b*n1= gcd_aux n n1 (mod m n1) +(\exists a,b. +a*(m \mod n1) - b*n1= gcd_aux n n1 (m \mod n1) \lor -b*n1 - a*(mod m n1) = gcd_aux n n1 (mod m n1))). +b*n1 - a*(m \mod n1) = gcd_aux n n1 (m \mod n1)). elim Hcut2.elim H5.elim H6. (* first case *) rewrite < H7. -apply ex_intro ? ? (a1+a*(div m n1)). -apply ex_intro ? ? a. +apply (ex_intro ? ? (a1+a*(m / n1))). +apply (ex_intro ? ? a). right. rewrite < sym_plus. -rewrite < sym_times n1. +rewrite < (sym_times n1). rewrite > distr_times_plus. -rewrite > sym_times n1. -rewrite > sym_times n1. -rewrite > div_mod m n1 in \vdash (? ? (? % ?) ?). +rewrite > (sym_times n1). +rewrite > (sym_times n1). +rewrite > (div_mod m n1) in \vdash (? ? (? % ?) ?). rewrite > assoc_times. rewrite < sym_plus. rewrite > distr_times_plus. @@ -301,14 +290,15 @@ apply le_n. assumption. (* second case *) rewrite < H7. -apply ex_intro ? ? (a1+a*(div m n1)). -apply ex_intro ? ? a. +apply (ex_intro ? ? (a1+a*(m / n1))). +apply (ex_intro ? ? a). left. +(* clear Hcut2.clear H5.clear H6.clear H. *) rewrite > sym_times. rewrite > distr_times_plus. rewrite > sym_times. -rewrite > sym_times n1. -rewrite > div_mod m n1 in \vdash (? ? (? ? %) ?). +rewrite > (sym_times n1). +rewrite > (div_mod m n1) in \vdash (? ? (? ? %) ?). rewrite > distr_times_plus. rewrite > assoc_times. rewrite < eq_minus_minus_minus_plus. @@ -317,93 +307,70 @@ rewrite < plus_minus. rewrite < minus_n_n.reflexivity. apply le_n. assumption. -apply H n1 (mod m n1). -cut O \lt mod m n1 \lor O = mod m n1. +apply (H n1 (m \mod n1)). +cut (O \lt m \mod n1 \lor O = m \mod n1). elim Hcut2.assumption. -absurd divides n1 m.apply mod_O_to_divides. +absurd (n1 \divides m).apply mod_O_to_divides. assumption. symmetry.assumption.assumption. apply le_to_or_lt_eq.apply le_O_n. apply lt_to_le. apply lt_mod_m_m.assumption. apply le_S_S_to_le. -apply trans_le ? n1. -change with mod m n1 < n1. +apply (trans_le ? n1). +change with (m \mod n1 < n1). apply lt_mod_m_m. assumption.assumption.assumption.assumption. -apply decidable_divides n1 m.assumption. -apply lt_to_le_to_lt ? n1.assumption.assumption. +apply (decidable_divides n1 m).assumption. +apply (lt_to_le_to_lt ? n1).assumption.assumption. qed. -theorem eq_minus_gcd: \forall m,n. -ex nat (\lambda a. ex nat (\lambda b. -a*n - b*m = (gcd n m) \lor b*m - a*n = (gcd n m))). +theorem eq_minus_gcd: + \forall m,n.\exists a,b.a*n - b*m = (gcd n m) \lor b*m - a*n = (gcd n m). intros. -change with -ex nat (\lambda a. ex nat (\lambda b. -a*n - b*m = -match leb n m with - [ true \Rightarrow - match n with - [ O \Rightarrow m - | (S p) \Rightarrow gcd_aux (S p) m (S p) ] - | false \Rightarrow - match m with - [ O \Rightarrow n - | (S p) \Rightarrow gcd_aux (S p) n (S p) ]] -\lor b*m - a*n = -match leb n m with - [ true \Rightarrow - match n with - [ O \Rightarrow m - | (S p) \Rightarrow gcd_aux (S p) m (S p) ] - | false \Rightarrow - match m with - [ O \Rightarrow n - | (S p) \Rightarrow gcd_aux (S p) n (S p) ]] -)). -apply leb_elim n m. -apply nat_case1 n. +unfold gcd. +apply (leb_elim n m). +apply (nat_case1 n). simplify.intros. -apply ex_intro ? ? O. -apply ex_intro ? ? (S O). +apply (ex_intro ? ? O). +apply (ex_intro ? ? (S O)). right.simplify. rewrite < plus_n_O. apply sym_eq.apply minus_n_O. intros. change with -ex nat (\lambda a. ex nat (\lambda b. +(\exists a,b. 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)))). +\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. +apply (nat_case1 m). simplify.intros. -apply ex_intro ? ? (S O). -apply ex_intro ? ? O. +apply (ex_intro ? ? (S O)). +apply (ex_intro ? ? O). left.simplify. rewrite < plus_n_O. apply sym_eq.apply minus_n_O. intros. change with -ex nat (\lambda a. ex nat (\lambda b. +(\exists a,b. a*n - b*(S m1) = (gcd_aux (S m1) n (S m1)) -\lor b*(S m1) - a*n = (gcd_aux (S m1) n (S m1)))). +\lor b*(S m1) - a*n = (gcd_aux (S m1) n (S m1))). cut -ex nat (\lambda a. ex nat (\lambda b. +(\exists a,b. a*(S m1) - b*n = (gcd_aux (S m1) n (S m1)) \lor -b*n - a*(S m1) = (gcd_aux (S m1) n (S m1)))). +b*n - a*(S m1) = (gcd_aux (S m1) n (S m1))). elim Hcut.elim H2.elim H3. -apply ex_intro ? ? a1. -apply ex_intro ? ? a. +apply (ex_intro ? ? a1). +apply (ex_intro ? ? a). right.assumption. -apply ex_intro ? ? a1. -apply ex_intro ? ? a. +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. @@ -416,20 +383,30 @@ qed. theorem gcd_O_to_eq_O:\forall m,n:nat. (gcd m n) = O \to m = O \land n = O. -intros.cut divides O n \land divides O m. +intros.cut (O \divides n \land O \divides m). elim Hcut.elim H2.split. assumption.elim H1.assumption. 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. +(\forall n,m:nat. gcd n m = gcd m n). intros. -cut O < (gcd n m) \lor O = (gcd n m). +cut (O < (gcd n m) \lor O = (gcd n m)). elim Hcut. -cut O < (gcd m n) \lor O = (gcd m n). +cut (O < (gcd m n) \lor O = (gcd m n)). elim Hcut1. apply antisym_le. apply divides_to_le.assumption. @@ -437,12 +414,12 @@ apply divides_d_gcd.apply divides_gcd_n.apply divides_gcd_m. apply divides_to_le.assumption. apply divides_d_gcd.apply divides_gcd_n.apply divides_gcd_m. rewrite < H1. -cut m=O \land n=O. +cut (m=O \land n=O). elim Hcut2.rewrite > H2.rewrite > H3.reflexivity. apply gcd_O_to_eq_O.apply sym_eq.assumption. apply le_to_or_lt_eq.apply le_O_n. rewrite < H. -cut n=O \land m=O. +cut (n=O \land m=O). elim Hcut1.rewrite > H1.rewrite > H2.reflexivity. apply gcd_O_to_eq_O.apply sym_eq.assumption. apply le_to_or_lt_eq.apply le_O_n. @@ -451,90 +428,181 @@ 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. +cut (O < gcd (S O) n \lor O = gcd (S O) n). elim Hcut.assumption. apply False_ind. -apply not_eq_O_S O. -cut (S O)=O \land n=O. +apply (not_eq_O_S O). +cut ((S O)=O \land n=O). elim Hcut1.apply sym_eq.assumption. apply gcd_O_to_eq_O.apply sym_eq.assumption. apply le_to_or_lt_eq.apply le_O_n. qed. -theorem prime_to_gcd_SO: \forall n,m:nat. prime n \to \not (divides n 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. +apply divides_mod.assumption. +apply divides_gcd_n. +apply divides_gcd_m. +apply divides_gcd_m. +qed. + +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. +apply divides_gcd_n. +apply (divides_mod_to_divides ? ? n). +assumption. +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. -change with (S (S O)) \le gcd n m \to False.intro. -apply H1.rewrite < H3 (gcd n m). +change with ((S (S O)) \le gcd n m \to False).intro. +apply H1.rewrite < (H3 (gcd n m)). apply divides_gcd_m. apply divides_gcd_n.assumption. -cut O < gcd n m \lor O = gcd n m. +cut (O < gcd n m \lor O = gcd n m). elim Hcut.assumption. apply False_ind. -apply not_le_Sn_O (S O). -cut n=O \land m=O. +apply (not_le_Sn_O (S O)). +cut (n=O \land m=O). elim Hcut1.rewrite < H5 in \vdash (? ? %).assumption. apply gcd_O_to_eq_O.apply sym_eq.assumption. apply le_to_or_lt_eq.apply le_O_n. qed. -(* esempio di sfarfallalmento !!! *) -(* -theorem bad: \forall n,p,q:nat.prime n \to divides n (p*q) \to -divides n p \lor divides n q. +theorem divides_times_to_divides: \forall n,p,q:nat.prime n \to n \divides p*q \to +n \divides p \lor n \divides q. intros. -cut divides n p \lor \not (divides n p). -elim Hcut.left.assumption. -right. -cut ex nat (\lambda a. ex nat (\lambda b. -a*n - b*p = (S O) \lor b*p - a*n = (S O))). -elim Hcut1.elim H3.*) - -theorem divides_times_to_divides: \forall n,p,q:nat.prime n \to divides n (p*q) \to -divides n p \lor divides n q. -intros. -cut divides n p \lor \not (divides n p). +cut (n \divides p \lor n \ndivides p). elim Hcut. left.assumption. right. -cut ex nat (\lambda a. ex nat (\lambda b. -a*n - b*p = (S O) \lor b*p - a*n = (S O))). +cut (\exists a,b. a*n - b*p = (S O) \lor b*p - a*n = (S O)). elim Hcut1.elim H3.elim H4. (* first case *) -rewrite > times_n_SO q.rewrite < H5. +rewrite > (times_n_SO q).rewrite < H5. rewrite > distr_times_minus. -rewrite > sym_times q (a1*p). -rewrite > assoc_times a1. +rewrite > (sym_times q (a1*p)). +rewrite > (assoc_times a1). elim H1.rewrite > H6. -rewrite < sym_times n.rewrite < assoc_times. -rewrite > sym_times q.rewrite > assoc_times. -rewrite < assoc_times a1.rewrite < sym_times n. -rewrite > assoc_times n. +rewrite < (sym_times n).rewrite < assoc_times. +rewrite > (sym_times q).rewrite > assoc_times. +rewrite < (assoc_times a1).rewrite < (sym_times n). +rewrite > (assoc_times n). rewrite < distr_times_minus. -apply witness ? ? (q*a-a1*n2).reflexivity. +apply (witness ? ? (q*a-a1*n2)).reflexivity. (* second case *) -rewrite > times_n_SO q.rewrite < H5. +rewrite > (times_n_SO q).rewrite < H5. rewrite > distr_times_minus. -rewrite > sym_times q (a1*p). -rewrite > assoc_times a1. +rewrite > (sym_times q (a1*p)). +rewrite > (assoc_times a1). elim H1.rewrite > H6. rewrite < sym_times.rewrite > assoc_times. -rewrite < assoc_times q. -rewrite < sym_times n. +rewrite < (assoc_times q). +rewrite < (sym_times n). rewrite < distr_times_minus. -apply witness ? ? (n2*a1-q*a).reflexivity. +apply (witness ? ? (n2*a1-q*a)).reflexivity. (* end second case *) -rewrite < prime_to_gcd_SO n p. +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 (decidable_divides n p). +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.