From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 19 Jan 2006 18:52:13 +0000 (+0000)
Subject: New reduction strategy (that behaves much better during simplification).
X-Git-Tag: make_still_working~7808
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ef3f78973c2fa3151c09681bcdb60107cd73c518;p=helm.git

New reduction strategy (that behaves much better during simplification).
Unfortunately, the new reduction is a bit slower on one test (paramodulation).
To be investigated.
---

diff --git a/helm/matita/library/algebra/groups.ma b/helm/matita/library/algebra/groups.ma
index a9164a927..9d98aea4d 100644
--- a/helm/matita/library/algebra/groups.ma
+++ b/helm/matita/library/algebra/groups.ma
@@ -49,15 +49,10 @@ intros;
 unfold left_cancellable;
 intros;
 rewrite < (e_is_left_unit ? ? (monoid_properties G));
-fold simplify (e G);
 rewrite < (e_is_left_unit ? ? (monoid_properties G) z);
-fold simplify (e G);
 rewrite < (opp_is_left_inverse ? ? (group_properties G) x);
-fold simplify (opp G);
 rewrite > (semigroup_properties G);
-fold simplify (op G);
 rewrite > (semigroup_properties G);
-fold simplify (op G);
 apply eq_f;
 assumption.
 qed.
diff --git a/helm/matita/library/nat/lt_arith.ma b/helm/matita/library/nat/lt_arith.ma
index b8339f374..f60da5eba 100644
--- a/helm/matita/library/nat/lt_arith.ma
+++ b/helm/matita/library/nat/lt_arith.ma
@@ -204,10 +204,14 @@ monotonic nat lt f \to injective nat nat f.
 unfold injective.intros.
 apply (nat_compare_elim x y).
 intro.apply False_ind.apply (not_le_Sn_n (f x)).
-rewrite > H1 in \vdash (? ? %).apply H.apply H2.
+rewrite > H1 in \vdash (? ? %).
+change with (f x < f y).
+apply H.apply H2.
 intros.assumption.
 intro.apply False_ind.apply (not_le_Sn_n (f y)).
-rewrite < H1 in \vdash (? ? %).apply H.apply H2.
+rewrite < H1 in \vdash (? ? %).
+change with (f y < f x).
+apply H.apply H2.
 qed.
 
 theorem increasing_to_injective: \forall f:nat\to nat.
diff --git a/helm/ocaml/cic_proof_checking/cicReduction.ml b/helm/ocaml/cic_proof_checking/cicReduction.ml
index 846cdf92b..56e98775f 100644
--- a/helm/ocaml/cic_proof_checking/cicReduction.ml
+++ b/helm/ocaml/cic_proof_checking/cicReduction.ml
@@ -746,8 +746,8 @@ module R = Reduction
  ClosuresOnStackByValueFromEnvOrEnsByNameOnConstantsStrategy;; OK 58.094s
 module R = Reduction(ClosuresOnStackByValueFromEnvOrEnsStrategy);; OK 58.127s
 *)
-(*module R = Reduction(CallByValueByNameForUnwind);; *)
-module R = Reduction(ClosuresOnStackByValueFromEnvOrEnsStrategy);;
+module R = Reduction(CallByValueByNameForUnwind);;
+(*module R = Reduction(ClosuresOnStackByValueFromEnvOrEnsStrategy);;*)
 module U = UriManager;;
 
 let whd = R.whd