X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fnat%2Fgcd.ma;h=b970fb0c3ba1b1f1096cead8eb4951f1f2dafa87;hb=4dc47c9675ffd5fa50296ffaa9b5997501518c98;hp=ded9d4843ac6cf3cb4da2b4f564568db2df2e02b;hpb=db9c252cc8adb9243892203805b203bafe486bfc;p=helm.git

diff --git a/helm/software/matita/library/nat/gcd.ma b/helm/software/matita/library/nat/gcd.ma
index ded9d4843..b970fb0c3 100644
--- a/helm/software/matita/library/nat/gcd.ma
+++ b/helm/software/matita/library/nat/gcd.ma
@@ -12,8 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/nat/gcd".
-
 include "nat/primes.ma".
 include "nat/lt_arith.ma".
 
@@ -57,7 +55,7 @@ qed.
 theorem divides_mod_to_divides: \forall p,m,n:nat. O < n \to
 p \divides (m \mod n) \to p \divides n \to p \divides m. 
 intros.elim H1.elim H2.
-apply (witness p m ((n1*(m / n))+n2)).
+apply (witness p m ((n2*(m / n))+n1)).
 rewrite > distr_times_plus.
 rewrite < H3.
 rewrite < assoc_times.
@@ -101,7 +99,6 @@ qed.
 theorem divides_gcd_nm: \forall n,m.
 gcd n m \divides m \land gcd n m \divides n.
 intros.
-(*CSC: simplify simplifies too much because of a redex in gcd *)
 change with
 (match leb n m with
   [ true \Rightarrow 
@@ -594,7 +591,6 @@ intro.apply (nat_case n)
 qed.
 
 theorem symmetric_gcd: symmetric nat gcd.
-(*CSC: bug here: unfold symmetric does not work *)
 change with 
 (\forall n,m:nat. gcd n m = gcd m n).
 intros.
@@ -656,9 +652,9 @@ elim H2.
 generalize in match H1.
 rewrite > H3.
 intro.
-cut (O < n2)
-  [elim (gcd_times_SO_to_gcd_SO n n n2 ? ? H4)
-    [cut (gcd n (n*n2) = n)
+cut (O < n1)
+  [elim (gcd_times_SO_to_gcd_SO n n n1 ? ? H4)
+    [cut (gcd n (n*n1) = n)
       [apply (lt_to_not_eq (S O) n)
         [assumption|rewrite < H4.assumption]
       |apply gcd_n_times_nm.assumption
@@ -666,7 +662,7 @@ cut (O < n2)
     |apply (trans_lt ? (S O))[apply le_n|assumption]
     |assumption
     ]
-  |elim (le_to_or_lt_eq O n2 (le_O_n n2));
+  |elim (le_to_or_lt_eq O n1 (le_O_n n1));
     [assumption
     |apply False_ind.
      apply (le_to_not_lt n (S O))
@@ -674,7 +670,7 @@ cut (O < n2)
        apply divides_to_le
         [rewrite > H4.apply lt_O_S
         |apply divides_d_gcd
-          [apply (witness ? ? n2).reflexivity
+          [apply (witness ? ? n1).reflexivity
           |apply divides_n_n
           ]
         ]
@@ -749,6 +745,7 @@ apply gcd_O_to_eq_O.apply sym_eq.assumption.
 apply le_to_or_lt_eq.apply le_O_n.
 qed.
 
+(* primes and divides *)
 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.
@@ -764,10 +761,6 @@ cut (n \divides p \lor n \ndivides p)
           rewrite > (sym_times q (a1*p)).
           rewrite > (assoc_times a1).
           elim H1.
-          (*
-             rewrite > H6.
-             applyS (witness n (n*(q*a-a1*n2)) (q*a-a1*n2))
-             reflexivity. *);
           applyS (witness n ? ? (refl_eq ? ?)) (* timeout=50 *).
           (*
           rewrite < (sym_times n).rewrite < assoc_times.
@@ -783,11 +776,14 @@ cut (n \divides p \lor n \ndivides p)
           rewrite > (sym_times q (a1*p)).
           rewrite > (assoc_times a1).
           elim H1.rewrite > H6.
+          applyS (witness n ? ? (refl_eq ? ?)) (* timeout=50 *).
+          (*
           rewrite < sym_times.rewrite > assoc_times.
           rewrite < (assoc_times q).
           rewrite < (sym_times n).
           rewrite < distr_times_minus.
-          apply (witness ? ? (n2*a1-q*a)).reflexivity
+          apply (witness ? ? (n1*a1-q*a)).reflexivity
+          *)
         ](* end second case *)
      |rewrite < (prime_to_gcd_SO n p)
        [apply eq_minus_gcd|assumption|assumption
@@ -802,6 +798,30 @@ cut (n \divides p \lor n \ndivides p)
   ]
 qed.
 
+theorem divides_exp_to_divides: 
+\forall p,n,m:nat. prime p \to 
+p \divides n \sup m \to p \divides n.
+intros 3.elim m.simplify in H1.
+apply (transitive_divides p (S O)).assumption.
+apply divides_SO_n.
+cut (p \divides n \lor p \divides n \sup n1).
+elim Hcut.assumption.
+apply H.assumption.assumption.
+apply divides_times_to_divides.assumption.
+exact H2.
+qed.
+
+theorem divides_exp_to_eq: 
+\forall p,q,m:nat. prime p \to prime q \to
+p \divides q \sup m \to p = q.
+intros.
+unfold prime in H1.
+elim H1.apply H4.
+apply (divides_exp_to_divides p q m).
+assumption.assumption.
+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.
@@ -861,14 +881,14 @@ cut (n \divides p \lor n \ndivides p)
           rewrite > distr_times_minus.
           rewrite > (sym_times p (a1*m)).
           rewrite > (assoc_times a1).
-          elim H2.
+          elim H2.rewrite > H7. 
           applyS (witness n ? ? (refl_eq ? ?)) (* timeout=50 *).
          |(* second case *)
           rewrite > (times_n_SO p).rewrite < H6.
           rewrite > distr_times_minus.
           rewrite > (sym_times p (a1*m)).
           rewrite > (assoc_times a1).
-          elim H2.
+          elim H2.rewrite > H7.
           applyS (witness n ? ? (refl_eq ? ?)).
         ](* end second case *)
      |rewrite < H1.apply eq_minus_gcd.
@@ -877,4 +897,37 @@ cut (n \divides p \lor n \ndivides p)
  |apply (decidable_divides n p).
   assumption.
  ]
+qed.
+
+(*
+theorem divides_to_divides_times1: \forall p,q,n. prime p \to prime q \to p \neq q \to
+divides p n \to divides q n \to divides (p*q) n.
+intros.elim H3.
+rewrite > H5 in H4.
+elim (divides_times_to_divides ? ? ? H1 H4)
+  [elim H.apply False_ind.
+   apply H2.apply sym_eq.apply H8
+    [assumption
+    |apply prime_to_lt_SO.assumption
+    ]
+  |elim H6.
+   apply (witness ? ? n1).
+   rewrite > assoc_times.
+   rewrite < H7.assumption
+  ]
+qed.
+*)
+
+theorem divides_to_divides_times: \forall p,q,n. prime p  \to p \ndivides q \to
+divides p n \to divides q n \to divides (p*q) n.
+intros.elim H3.
+rewrite > H4 in H2.
+elim (divides_times_to_divides ? ? ? H H2)
+  [apply False_ind.apply H1.assumption
+  |elim H5.
+   apply (witness ? ? n2).
+   rewrite > sym_times in ⊢ (? ? ? (? % ?)).
+   rewrite > assoc_times.
+   rewrite < H6.assumption
+  ]
 qed.
\ No newline at end of file