From e1b382b7a82e69cb009571017c16a3665f9946c4 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 22 Feb 2006 21:17:16 +0000 Subject: [PATCH] Bug fixed in simplify: delta expansion of constants applied to more arguments than head lambda abstractions was always performed (even if no "interesting" reduction took place). --- .../components/tactics/proofEngineReduction.ml | 9 +++++---- helm/software/matita/library/algebra/groups.ma | 10 ++-------- 2 files changed, 7 insertions(+), 12 deletions(-) diff --git a/helm/software/components/tactics/proofEngineReduction.ml b/helm/software/components/tactics/proofEngineReduction.ml index 0dc4ce4ee..1502b600f 100644 --- a/helm/software/components/tactics/proofEngineReduction.ml +++ b/helm/software/components/tactics/proofEngineReduction.ml @@ -859,10 +859,11 @@ let simpl context = | C.LetIn (_,s,t) -> aux l (S.subst s t) | t -> let simplified = reduceaux context l t in - if t = simplified then - raise AlreadySimplified - else - simplified + let t' = if l = [] then t else C.Appl (t::l) in + if t' = simplified then + raise AlreadySimplified + else + simplified in (try aux l body with diff --git a/helm/software/matita/library/algebra/groups.ma b/helm/software/matita/library/algebra/groups.ma index 5d3be8cb1..e9b144acc 100644 --- a/helm/software/matita/library/algebra/groups.ma +++ b/helm/software/matita/library/algebra/groups.ma @@ -243,14 +243,8 @@ theorem member_of_subgroup_op_inv_x_y_to_left_coset_eq: ∀G.∀x,y.∀H:subgroup G. (x \sup -1 ·y) ∈ H → x*H = y*H. intros; unfold left_coset_eq; -simplify in ⊢ (? → ? ? ? (? ? % ?)); -simplify in ⊢ (? → ? ? ? (? ? ? (? ? ? (? ? %) ?))); -simplify in ⊢ (? ? % → ?); -intros; -unfold member_of_left_coset; -simplify in ⊢ (? ? (λy:?.? ? ? (? ? ? (? ? ? (? ? %) ?)))); -simplify in ⊢ (? ? (λy:? ? %.?)); -simplify in ⊢ (? ? (λy:?.? ? ? (? ? % ?))); +simplify; +intro; unfold member_of_subgroup in H1; elim H1; clear H1; -- 2.39.2