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 a9164a927bde9cf2f937d77a2b8f0dabadd64428..9d98aea4d9d232758c1145db350da6a78f71d3a6 100644 (file)
--- 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 b8339f374e6019dd054719c9928bf735c63aef4b..f60da5eba31f2c07d7b53c70d62c231d362c2208 100644 (file)
--- 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 846cdf92b3f2224bcf7bd24a904851519740b56d..56e98775f31caf7276303a091dbeb22612128046 100644 (file)
--- 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