From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 31 Jul 2007 10:40:30 +0000 (+0000)
Subject: something was really too slow...
X-Git-Tag: make_still_working~6114
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b348a1a39e17b541fca17d2218a3b91bd7f1fece;p=helm.git

something was really too slow...
---

diff --git a/helm/software/matita/library/algebra/CoRN/SetoidFun.ma b/helm/software/matita/library/algebra/CoRN/SetoidFun.ma
index d78aac70e..67f8ac1d6 100644
--- a/helm/software/matita/library/algebra/CoRN/SetoidFun.ma
+++ b/helm/software/matita/library/algebra/CoRN/SetoidFun.ma
@@ -1247,7 +1247,8 @@ a = b \to b \neq c \to a \neq c.
 intros.
 generalize in match (ap_cotransitive_unfolded ? ? ? H1 a).
 intro.elim H2.apply False_ind.apply (eq_imp_not_ap ? ? ? H).
-autobatch.assumption.
+apply ap_symmetric_unfolded. assumption.
+assumption.
 qed.
 
 lemma Dir_bij : \forall A, B:CSetoid. 
diff --git a/helm/software/matita/library/assembly/byte.ma b/helm/software/matita/library/assembly/byte.ma
index 583051e27..f2d1dc156 100644
--- a/helm/software/matita/library/assembly/byte.ma
+++ b/helm/software/matita/library/assembly/byte.ma
@@ -66,7 +66,7 @@ lemma lt_nat_of_byte_256: ∀b. nat_of_byte b < 256.
   [ letin Hf ≝ (le_plus ? ? ? ? Hcut K'); clearbody Hf;
     simplify in Hf:(? ? %);
     assumption
-  | autobatch
+  | apply le_times_r. apply H'.
   ]
 qed.
 
@@ -107,7 +107,7 @@ lemma eq_nat_of_byte_n_nat_of_byte_mod_n_256:
     rewrite > exadecimal_of_nat_mod in ⊢ (? ? ? %);
     rewrite > divides_to_eq_mod_mod_mod;
      [ reflexivity
-     | autobatch
+     | apply (witness ? ? 16). reflexivity.
      ]
   ]
 qed.
@@ -117,7 +117,8 @@ lemma plusbyte_ok:
   match plusbyte b1 b2 c with
    [ couple r c' ⇒ b1 + b2 + nat_of_bool c = nat_of_byte r + nat_of_bool c' * 256
    ].
- intros;
+ intros; elim daemon.
+ (* 
  unfold plusbyte;
  generalize in match (plusex_ok (bl b1) (bl b2) c);
  elim (plusex (bl b1) (bl b2) c);
@@ -149,6 +150,7 @@ lemma plusbyte_ok:
  rewrite < associative_plus in ⊢ (? ? (? ? (? % ?)) ?);
  rewrite > H; clear H;
  autobatch paramodulation.
+ *)
 qed.
 
 definition bpred ≝
diff --git a/helm/software/matita/library/assembly/exadecimal.ma b/helm/software/matita/library/assembly/exadecimal.ma
index fb1a14ede..761c06c94 100644
--- a/helm/software/matita/library/assembly/exadecimal.ma
+++ b/helm/software/matita/library/assembly/exadecimal.ma
@@ -801,7 +801,8 @@ lemma exadecimal_of_nat_mod:
  change in ⊢ (? ? ? (? (? % ?))) with (n16 \mod 16);
  rewrite < mod_mod;
   [ apply H;
-    autobatch
+    unfold lt;
+    autobatch.
   | autobatch
   ]
 qed.
@@ -848,11 +849,7 @@ lemma plusex_ok:
   match plusex b1 b2 c with
    [ couple r c' ⇒ b1 + b2 + nat_of_bool c = nat_of_exadecimal r + nat_of_bool c' * 16 ].
  intros;
- elim c;
- elim b1;
- elim b2;
- normalize;
- reflexivity.
+ elim b1; (elim b2; (elim c; normalize; reflexivity)).
 qed.
 
 definition xpred ≝