From a2b703feae630d0fdd1740bd18e80ee1f6654a88 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Tue, 5 May 2009 11:09:36 +0000 Subject: [PATCH] autobatch by --- helm/software/matita/library/nat/gcd.ma | 26 +++++++++++-------------- 1 file changed, 11 insertions(+), 15 deletions(-) diff --git a/helm/software/matita/library/nat/gcd.ma b/helm/software/matita/library/nat/gcd.ma index 395b24248..aa512566e 100644 --- a/helm/software/matita/library/nat/gcd.ma +++ b/helm/software/matita/library/nat/gcd.ma @@ -755,11 +755,10 @@ cut (n \divides p \lor n \ndivides p) |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 > (times_n_SO q).rewrite < H5. rewrite > distr_times_minus. - elim H1. autobatch; - (* + elim H1. autobatch by witness, divides_minus. + (* rewrite > (sym_times q (a1*p)). rewrite > (assoc_times a1). applyS (witness n ? ? (refl_eq ? ?)). @@ -773,7 +772,7 @@ cut (n \divides p \lor n \ndivides p) |(* second case *) rewrite > (times_n_SO q).rewrite < H5. rewrite > distr_times_minus. - elim H1. autobatch; + elim H1. autobatch by witness, divides_minus. (* rewrite > (sym_times q (a1*p)). rewrite > (assoc_times a1). @@ -878,19 +877,15 @@ cut (n \divides p \lor n \ndivides p) |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 *) + elim H2. rewrite > (times_n_SO p).rewrite < H6. rewrite > distr_times_minus. - rewrite > (sym_times p (a1*m)). - rewrite > (assoc_times a1). - elim H2.rewrite > H7. - applyS (witness n ? ? (refl_eq ? ?)) (* timeout=50 *). - |(* second case *) + autobatch by witness, divides_minus. + |(* second case *) + elim H2. rewrite > (times_n_SO p).rewrite < H6. rewrite > distr_times_minus. - rewrite > (sym_times p (a1*m)). - rewrite > (assoc_times a1). - elim H2.rewrite > H7. - applyS (witness n ? ? (refl_eq ? ?)). + autobatch by witness, divides_minus. ](* end second case *) |rewrite < H1.apply eq_minus_gcd. ] @@ -925,7 +920,8 @@ intros.elim H3. rewrite > H4 in H2. elim (divides_times_to_divides ? ? ? H H2) [apply False_ind.apply H1.assumption - |elim H5. + |elim H5. + (* applyS (witness ? ? n2 (refl_eq ? ?)).*) apply (witness ? ? n2). rewrite > sym_times in ⊢ (? ? ? (? % ?)). rewrite > assoc_times. -- 2.39.2