X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2Fnat%2Fgcd.ma;h=eb1053feb78cb5e88a70a9154ff9af271f15e08b;hb=7273c698dd60c1a8a0f35b44376acb548c6a4a33;hp=5a2fd4647e80bf342b650e0825c3333568b55047;hpb=da83446deba30fbe32b9bf617d83bd22cc9c9770;p=helm.git

diff --git a/helm/matita/library/nat/gcd.ma b/helm/matita/library/nat/gcd.ma
index 5a2fd4647..eb1053feb 100644
--- a/helm/matita/library/nat/gcd.ma
+++ b/helm/matita/library/nat/gcd.ma
@@ -15,7 +15,6 @@
 set "baseuri" "cic:/matita/nat/gcd".
 
 include "nat/primes.ma".
-include "higher_order_defs/functions.ma".
 
 let rec gcd_aux p m n: nat \def
 match divides_b n m with
@@ -23,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.
@@ -37,28 +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.
-rewrite > sym_times.
-apply div_mod.assumption. assumption.
+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,33 +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).
+cut (n1 \divides m) \lor (n1 \ndivides m).
 change with 
-(divides 
 (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.
+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.
 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,20 +97,17 @@ 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.
+change with m \mod n1 < n1.
 apply lt_mod_m_m.assumption.assumption.
-apply decidable_divides n1 m.assumption.
-apply lt_to_le_to_lt ? n1.assumption.reflexivity.
-assumption.
 assumption.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
+match leb n m with
   [ true \Rightarrow 
     match n with 
     [ O \Rightarrow m
@@ -123,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
@@ -134,16 +125,16 @@ divides
   | false \Rightarrow 
     match m with 
     [ O \Rightarrow n
-    | (S p) \Rightarrow gcd_aux (S p) n (S p) ]]) 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.
 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.
 assumption.apply le_n.
@@ -153,12 +144,12 @@ simplify.intros.split.
 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.
@@ -167,57 +158,55 @@ 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).
 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).
 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.
 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.
+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 lt_to_le_to_lt ? n1.assumption.reflexivity.
-assumption.assumption.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,17 +215,17 @@ match leb n m with
   | false \Rightarrow 
     match m with 
     [ O \Rightarrow n
-    | (S p) \Rightarrow gcd_aux (S p) n (S p) ]]).
+    | (S p) \Rightarrow gcd_aux (S p) n (S p) ]].
 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.
 rewrite < H2.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.
 apply lt_to_le.apply not_le_to_lt.assumption.apply le_n.assumption.
@@ -244,22 +233,21 @@ 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).
+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.
@@ -267,21 +255,22 @@ 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 ? ? (a1+a*(m / n1)).
 apply ex_intro ? ? a.
 right.
 rewrite < sym_plus.
@@ -297,11 +286,14 @@ rewrite < eq_minus_minus_minus_plus.
 rewrite < sym_plus.
 rewrite < plus_minus.
 rewrite < minus_n_n.reflexivity.
+apply le_n.
+assumption.
 (* second case *)
 rewrite < H7.
-apply ex_intro ? ? (a1+a*(div m n1)).
+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.
@@ -313,54 +305,30 @@ rewrite < eq_minus_minus_minus_plus.
 rewrite < sym_plus.
 rewrite < plus_minus.
 rewrite < minus_n_n.reflexivity.
-(* end second case *)
-apply H n1 (mod m n1).
-(* a lot of trivialities left *)
-cut O \lt mod m n1 \lor O = mod m n1.
-elim Hcut2.assumption.
-absurd divides n1 m.apply mod_O_to_divides.
-assumption.apply sym_eq.assumption.assumption.
+apply le_n.
+assumption.
+apply H n1 (m \mod n1).
+cut O \lt m \mod n1 \lor O = m \mod n1.
+elim Hcut2.assumption. 
+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 lt_mod_m_m.assumption.assumption.
+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.
-assumption.assumption.assumption.assumption.assumption.
-apply le_n.assumption.
-apply le_n.
 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) ]]
-)).
+unfold gcd.
 apply leb_elim n m.
 apply nat_case1 n.
 simplify.intros.
@@ -371,9 +339,9 @@ 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.
 assumption.apply le_n.
@@ -386,14 +354,14 @@ 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.
@@ -415,7 +383,7 @@ 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.
@@ -464,7 +432,7 @@ 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 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). 
 elim H.
@@ -473,6 +441,7 @@ apply not_lt_to_le.
 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.
 elim Hcut.assumption.
 apply False_ind.
@@ -481,30 +450,16 @@ 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.
-apply divides_gcd_n.assumption.
 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.
@@ -532,8 +487,8 @@ apply witness ? ? (n2*a1-q*a).reflexivity.
 (* end second case *)
 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.
-assumption.assumption.
 qed.