X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fnat%2Fgcd.ma;h=9bbce8144ff8885a7c7346bdb9b7937983bd5f7e;hb=10f29fdd78ee089a9a94446207b543d33d6c851c;hp=6da8e13d02780dd627233655593f7dcedf311e2c;hpb=f79585fe2f19c4a545938e189439d87b2611a47a;p=helm.git

diff --git a/helm/software/matita/library/nat/gcd.ma b/helm/software/matita/library/nat/gcd.ma
index 6da8e13d0..9bbce8144 100644
--- a/helm/software/matita/library/nat/gcd.ma
+++ b/helm/software/matita/library/nat/gcd.ma
@@ -15,6 +15,7 @@
 set "baseuri" "cic:/matita/nat/gcd".
 
 include "nat/primes.ma".
+include "nat/lt_arith.ma".
 
 let rec gcd_aux p m n: nat \def
 match divides_b n m with
@@ -163,42 +164,109 @@ intros.
 exact (proj1 ? ? (divides_gcd_nm n m)).
 qed.
 
+
+theorem divides_times_gcd_aux: \forall p,m,n,d,c. 
+O \lt c \to O < n \to n \le m \to n \le p \to
+d \divides (c*m) \to d \divides (c*n) \to d \divides c*gcd_aux p m n. 
+intro.
+elim p
+[ absurd (O < n)
+  [ assumption
+  | apply le_to_not_lt.
+    assumption
+  ]
+| simplify.
+  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
+      [ simplify.
+        apply H
+        [ assumption
+        | cut (O \lt m \mod n1 \lor O = m \mod n1)
+          [ elim Hcut1
+            [ assumption
+            | 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 (m \mod n1 < n1).
+            apply lt_mod_m_m.
+            assumption
+          | assumption
+          ]
+        | assumption
+        | rewrite < times_mod
+          [ rewrite < (sym_times c m).
+            rewrite < (sym_times c n1).
+            apply divides_mod
+            [ rewrite > (S_pred c)
+              [ rewrite > (S_pred n1)
+                [ apply (lt_O_times_S_S)
+                | assumption
+                ]
+              | assumption
+              ]
+            | assumption
+            | assumption
+            ]
+          | assumption
+          | assumption
+          ]
+        ]
+      | assumption
+      | assumption
+      ]
+    ]
+  | apply (decidable_divides n1 m).
+    assumption
+  ]
+]
+qed.
+
+(*a particular case of the previous theorem (setting c=1)*)
 theorem divides_gcd_aux: \forall p,m,n,d. O < n \to n \le m \to n \le p \to
 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.
-simplify.
-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.
-simplify.
-apply H.
-cut (O \lt m \mod n1 \lor O = m \mod n1).
-elim Hcut1.assumption.
-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 (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.
+intros.
+rewrite > (times_n_SO (gcd_aux p m n)).
+rewrite < (sym_times (S O)).
+apply (divides_times_gcd_aux)
+[ apply (lt_O_S O)
+| assumption
+| assumption
+| assumption
+| rewrite > (sym_times (S O)).
+  rewrite < (times_n_SO m).
+  assumption
+| rewrite > (sym_times (S O)).
+  rewrite < (times_n_SO n).
+  assumption
+]
 qed.
 
-theorem divides_d_gcd: \forall m,n,d. 
-d \divides m \to d \divides n \to d \divides gcd n m. 
+theorem divides_d_times_gcd: \forall m,n,d,c. 
+O \lt c \to d \divides (c*m) \to d \divides (c*n) \to d \divides c*gcd n m. 
 intros.
-(*CSC: here simplify simplifies too much because of a redex in gcd *)
 change with
-(d \divides
+(d \divides c *
 match leb n m with
   [ true \Rightarrow 
     match n with 
@@ -208,105 +276,178 @@ 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.
-intros.
-change with (d \divides gcd_aux (S m1) m (S m1)).
-apply divides_gcd_aux.
-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 (leb_elim n m)
+[ apply (nat_case1 n)
+  [ simplify.
+    intros.
+    assumption
+  | intros.
+    change with (d \divides c*gcd_aux (S m1) m (S m1)).
+    apply divides_times_gcd_aux
+    [ assumption
+    | unfold lt.
+      apply le_S_S.
+      apply le_O_n
+    | assumption
+    | apply (le_n (S m1))
+    | assumption
+    | rewrite < H3.
+      assumption
+    ]
+  ]
+| apply (nat_case1 m)
+  [ simplify.
+    intros.
+    assumption
+  | intros.
+    change with (d \divides c * gcd_aux (S m1) n (S m1)).
+    apply divides_times_gcd_aux
+    [ unfold lt.
+      change with (O \lt c).
+      assumption
+    | apply lt_O_S
+    | apply lt_to_le.
+      apply not_le_to_lt.
+      assumption
+    | apply (le_n (S m1)).
+    | assumption
+    | rewrite < H3.
+      assumption
+    ]
+  ]
+]
+qed.
+
+(*a particular case of the previous theorem (setting c=1)*)
+theorem divides_d_gcd: \forall m,n,d. 
+d \divides m \to d \divides n \to d \divides gcd n m. 
 intros.
-change with (d \divides gcd_aux (S m1) n (S m1)).
-apply divides_gcd_aux.
-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.
+rewrite > (times_n_SO (gcd n m)).
+rewrite < (sym_times (S O)).
+apply (divides_d_times_gcd)
+[ apply (lt_O_S O)
+| rewrite > (sym_times (S O)).
+  rewrite < (times_n_SO m).
+  assumption
+| rewrite > (sym_times (S O)).
+  rewrite < (times_n_SO n).
+  assumption
+]
 qed.
 
 theorem eq_minus_gcd_aux: \forall p,m,n.O < n \to n \le m \to n \le p \to
 \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 (n1 \divides m \lor  n1 \ndivides m).
-simplify.
-elim Hcut1.
-rewrite > divides_to_divides_b_true.
-simplify.
-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
-(\exists a,b.
-a*n1 - b*m = gcd_aux n n1 (m \mod n1)
-\lor 
-b*m - a*n1 = gcd_aux n n1 (m \mod n1)).
-cut 
-(\exists a,b.
-a*(m \mod n1) - b*n1= gcd_aux n n1 (m \mod n1)
-\lor
-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*(m / n1))).
-apply (ex_intro ? ? a).
-right.
-rewrite < sym_plus.
-rewrite < (sym_times n1).
-rewrite > distr_times_plus.
-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.
-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*(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 > distr_times_plus.
-rewrite > assoc_times.
-rewrite < eq_minus_minus_minus_plus.
-rewrite < sym_plus.
-rewrite < plus_minus.
-rewrite < minus_n_n.reflexivity.
-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 (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.
+elim p
+  [absurd (O < n)
+    [assumption
+    |apply le_to_not_lt.assumption
+    ]
+  |cut (O < m)
+    [cut (n1 \divides m \lor  n1 \ndivides m)
+      [simplify.
+       elim Hcut1
+        [rewrite > divides_to_divides_b_true
+          [simplify.
+           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
+           (\exists a,b.a*n1 - b*m = gcd_aux n n1 (m \mod n1)
+            \lor b*m - a*n1 = gcd_aux n n1 (m \mod n1)).
+           cut 
+           (\exists a,b.a*(m \mod n1) - b*n1= gcd_aux n n1 (m \mod n1)
+            \lor 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*(m / n1))).
+               apply (ex_intro ? ? a).
+               right.
+               rewrite < sym_plus.
+               rewrite < (sym_times n1).
+               rewrite > distr_times_plus.
+               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.
+                 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*(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 > distr_times_plus.
+                 rewrite > assoc_times.
+                 rewrite < eq_minus_minus_minus_plus.
+                 rewrite < sym_plus.
+                 rewrite < plus_minus
+                  [rewrite < minus_n_n.reflexivity
+                  |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 (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
+    ]
+  ]
 qed.
 
 theorem eq_minus_gcd:
@@ -525,7 +666,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 n2 (le_O_n n2));
     [assumption
     |apply False_ind.
      apply (le_to_not_lt n (S O))
@@ -608,6 +749,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.
@@ -661,6 +803,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.
@@ -736,4 +902,5 @@ cut (n \divides p \lor n \ndivides p)
  |apply (decidable_divides n p).
   assumption.
  ]
-qed.
\ No newline at end of file
+qed.
+