X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Flibrary%2Fnat%2Fgcd.ma;h=0568536dcb0f6d4cbaef1b94c3feb53d79b17824;hb=01b688447c18c1992b0c19ac5583ca9fee692514;hp=fdb1e8d9018dc5b877c52e93918894a6c43194f5;hpb=c34722e7f8ca26ed55a63a02dbfd7f3c4d2038b5;p=helm.git

diff --git a/matita/library/nat/gcd.ma b/matita/library/nat/gcd.ma
index fdb1e8d90..0568536dc 100644
--- a/matita/library/nat/gcd.ma
+++ b/matita/library/nat/gcd.ma
@@ -39,16 +39,18 @@ definition gcd : nat \to nat \to nat \def
 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*(m / n))).
+(* apply (witness ? ? (n2 - n1*(m / n))). *)
+apply witness[|
 rewrite > distr_times_minus.
-rewrite < H3.
+rewrite < H3 in \vdash (? ? ? (? % ?)).
 rewrite < assoc_times.
-rewrite < H4.
-apply sym_eq.
-apply plus_to_minus.
+rewrite < H4 in \vdash (? ? ? (? ? (? % ?))).
+apply sym_eq.apply plus_to_minus.
 rewrite > sym_times.
-apply div_mod.
-assumption.
+letin x \def div.
+rewrite < (div_mod ? ? H).
+reflexivity.
+]
 qed.
 
 theorem divides_mod_to_divides: \forall p,m,n:nat. O < n \to
@@ -225,86 +227,116 @@ 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:
@@ -382,6 +414,74 @@ rewrite < H4 in \vdash (? ? %).assumption.
 intros.unfold lt.apply le_S_S.apply le_O_n.
 qed.
 
+theorem gcd_n_n: \forall n.gcd n n = n.
+intro.elim n
+  [reflexivity
+  |apply le_to_le_to_eq
+    [apply divides_to_le
+      [apply lt_O_S
+      |apply divides_gcd_n
+      ]
+    |apply divides_to_le
+      [apply lt_O_gcd.apply lt_O_S
+      |apply divides_d_gcd
+        [apply divides_n_n|apply divides_n_n]
+      ]
+    ]
+  ]
+qed.
+
+theorem gcd_SO_to_lt_O: \forall i,n. (S O) < n \to gcd i n = (S O) \to
+O < i.
+intros.
+elim (le_to_or_lt_eq ? ? (le_O_n i))
+  [assumption
+  |absurd ((gcd i n) = (S O))
+    [assumption
+    |rewrite < H2.
+     simplify.
+     unfold.intro.
+     apply (lt_to_not_eq (S O) n H).
+     apply sym_eq.assumption
+    ]
+  ]
+qed.
+
+theorem gcd_SO_to_lt_n: \forall i,n. (S O) < n \to i \le n \to gcd i n = (S O) \to
+i < n.
+intros.
+elim (le_to_or_lt_eq ? ? H1)
+  [assumption
+  |absurd ((gcd i n) = (S O))
+    [assumption
+    |rewrite > H3.
+     rewrite > gcd_n_n.
+     unfold.intro.
+     apply (lt_to_not_eq (S O) n H).
+     apply sym_eq.assumption
+    ]
+  ]
+qed.
+
+theorem  gcd_n_times_nm: \forall n,m. O < m \to gcd n (n*m) = n.
+intro.apply (nat_case n)
+  [intros.reflexivity
+  |intros.
+   apply le_to_le_to_eq
+    [apply divides_to_le
+      [apply lt_O_S|apply divides_gcd_n]
+    |apply divides_to_le
+      [apply lt_O_gcd.rewrite > (times_n_O O).
+       apply lt_times[apply lt_O_S|assumption]
+      |apply divides_d_gcd
+        [apply (witness ? ? m1).reflexivity
+        |apply divides_n_n
+        ]
+      ]
+    ]
+  ]
+qed.
+
 theorem symmetric_gcd: symmetric nat gcd.
 (*CSC: bug here: unfold symmetric does not work *)
 change with 
@@ -438,6 +538,41 @@ qed.
 
 (* for the "converse" of the previous result see the end  of this development *)
 
+theorem eq_gcd_SO_to_not_divides: \forall n,m. (S O) < n \to 
+(gcd n m) = (S O) \to \lnot (divides n m).
+intros.unfold.intro.
+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)
+      [apply (lt_to_not_eq (S O) n)
+        [assumption|rewrite < H4.assumption]
+      |apply gcd_n_times_nm.assumption
+      ]
+    |apply (trans_lt ? (S O))[apply le_n|assumption]
+    |assumption
+    ]
+  |elim (le_to_or_lt_eq O n2 (le_O_n n2));
+    [assumption
+    |apply False_ind.
+     apply (le_to_not_lt n (S O))
+      [rewrite < H4.
+       apply divides_to_le
+        [rewrite > H4.apply lt_O_S
+        |apply divides_d_gcd
+          [apply (witness ? ? n2).reflexivity
+          |apply divides_n_n
+          ]
+        ]
+      |assumption
+      ]
+    ]
+  ]
+qed.
+
 theorem gcd_SO_n: \forall n:nat. gcd (S O) n = (S O).
 intro.
 apply antisym_le.apply divides_to_le.unfold lt.apply le_n.
@@ -517,10 +652,12 @@ cut (n \divides p \lor n \ndivides p)
           rewrite > distr_times_minus.
           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))
+          elim H1.
+          (*
+             rewrite > H6.
+             applyS (witness n (n*(q*a-a1*n2)) (q*a-a1*n2))
              reflexivity. *);
-          applyS (witness n ? ? (refl_eq ? ?)) timeout=50.
+          applyS (witness n ? ? (refl_eq ? ?)) (* timeout=50 *).
           (*
           rewrite < (sym_times n).rewrite < assoc_times.
           rewrite > (sym_times q).rewrite > assoc_times.
@@ -599,3 +736,34 @@ apply lt_O_gcd.
 rewrite > (times_n_O O).
 apply lt_times.assumption.assumption.
 qed.
+
+theorem gcd_SO_to_divides_times_to_divides: \forall m,n,p:nat. O < n \to
+gcd n m = (S O) \to n \divides (m*p) \to n \divides p.
+intros.
+cut (n \divides p \lor n \ndivides p)
+  [elim Hcut
+    [assumption
+    |cut (\exists a,b. a*n - b*m = (S O) \lor b*m - a*n = (S O))
+      [elim Hcut1.elim H4.elim H5         
+        [(* first case *)
+          rewrite > (times_n_SO p).rewrite < H6.
+          rewrite > distr_times_minus.
+          rewrite > (sym_times p (a1*m)).
+          rewrite > (assoc_times a1).
+          elim H2.
+          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.
+          applyS (witness n ? ? (refl_eq ? ?)).
+        ](* end second case *)
+     |rewrite < H1.apply eq_minus_gcd.
+     ]
+   ]
+ |apply (decidable_divides n p).
+  assumption.
+ ]
+qed.
\ No newline at end of file