From ef3f78973c2fa3151c09681bcdb60107cd73c518 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 19 Jan 2006 18:52:13 +0000 Subject: [PATCH] New reduction strategy (that behaves much better during simplification). Unfortunately, the new reduction is a bit slower on one test (paramodulation). To be investigated. --- helm/matita/library/algebra/groups.ma | 5 ----- helm/matita/library/nat/lt_arith.ma | 8 ++++++-- helm/ocaml/cic_proof_checking/cicReduction.ml | 4 ++-- 3 files changed, 8 insertions(+), 9 deletions(-) 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 -- 2.39.2