From b7ed6e0e8e98441ae0688b060196994e9a68cc72 Mon Sep 17 00:00:00 2001
From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Thu, 15 Jun 2006 09:39:20 +0000
Subject: [PATCH] examples of applyS

---
 helm/software/matita/library/nat/gcd.ma       | 82 +++++++++++--------
 helm/software/matita/library/nat/nth_prime.ma |  7 +-
 2 files changed, 52 insertions(+), 37 deletions(-)

diff --git a/helm/software/matita/library/nat/gcd.ma b/helm/software/matita/library/nat/gcd.ma
index 982f0f626..2bb22081f 100644
--- a/helm/software/matita/library/nat/gcd.ma
+++ b/helm/software/matita/library/nat/gcd.ma
@@ -506,42 +506,52 @@ qed.
 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 (n \divides p \lor n \ndivides p).
-elim Hcut.
-left.assumption.
-right.
-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 > distr_times_minus.
-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 < distr_times_minus.
-apply (witness ? ? (q*a-a1*n2)).reflexivity.
-(* second case *)
-rewrite > (times_n_SO q).rewrite < H5.
-rewrite > distr_times_minus.
-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 < distr_times_minus.
-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)).unfold lt.apply le_n.
-unfold prime in H.elim H. assumption.
+cut (n \divides p \lor n \ndivides p)
+  [elim Hcut
+    [left.assumption
+    |right.
+     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 > 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))
+             reflexivity. *);
+          applyS (witness n ? ? (refl_eq ? ?)).
+          (*
+          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
+          *)
+         |(* second case *)
+          rewrite > (times_n_SO q).rewrite < H5.
+          rewrite > distr_times_minus.
+          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 < distr_times_minus.
+          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))
+    [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
diff --git a/helm/software/matita/library/nat/nth_prime.ma b/helm/software/matita/library/nat/nth_prime.ma
index 4a054a3b4..e174266e6 100644
--- a/helm/software/matita/library/nat/nth_prime.ma
+++ b/helm/software/matita/library/nat/nth_prime.ma
@@ -77,7 +77,7 @@ match n with
     min_aux (upper_bound - (S previous_prime)) upper_bound primeb].
     
 (* it works, but nth_prime 4 takes already a few minutes -
-it must compute factorial of 7 ...
+it must compute factorial of 7 ...*)
 
 theorem example11 : nth_prime (S(S O)) = (S(S(S(S(S O))))).
 normalize.reflexivity.
@@ -89,6 +89,11 @@ qed.
 
 theorem example13 : nth_prime (S(S(S(S O)))) = (S(S(S(S(S(S(S(S(S(S(S O))))))))))).
 normalize.reflexivity.
+qed.
+
+(*
+theorem example14 : nth_prime (S(S(S(S(S O))))) = (S(S(S(S(S(S(S(S(S(S(S O))))))))))).
+normalize.reflexivity.
 *) 
 
 theorem prime_nth_prime : \forall n:nat.prime (nth_prime n).
-- 
2.39.2