Reduction trick added to simplify (greatly speeding up some examples

in library/algebra. For instance, a simplification that used to be performed
in more than 4h now takes less than 1s).

The idea is simply to avoid delta-reduction of a constant applied to
arguments that are not "active" (i.e. they cannot create a redex when
substituted in the body of the constant).

diff --git a/helm/software/components/tactics/proofEngineReduction.ml b/helm/software/components/tactics/proofEngineReduction.ml
index db25ae575e0aac1a5d706812add3ac1eccd28b2d..1db075c70d96455a80c15ab49865eb3a02cde7be 100644 (file)
--- a/helm/software/components/tactics/proofEngineReduction.ml
+++ b/helm/software/components/tactics/proofEngineReduction.ml
@@ -595,12 +595,24 @@ exception AlreadySimplified;;
 (*CSC: It does not perform simplification in a Case *)
 
 let simpl context =
+ let module C = Cic in
+ let module S = CicSubstitution in
+ (* a simplified term is active if it can create a redex when used as an *)
+ (* actual parameter                                                     *)
+ let rec is_active =
+  function
+     C.Lambda _
+   | C.MutConstruct _
+   | C.Appl (C.MutConstruct _::_)
+   | C.CoFix _ -> true
+   | C.Cast (bo,_) -> is_active bo
+   | C.LetIn _ -> assert false
+   | _ -> false
+ in
  (* reduceaux is equal to the reduceaux locally defined inside *)
  (* reduce, but for the const case.                            *) 
  (**** Step 1 ****)
  let rec reduceaux context l =
-  let module C = Cic in
-  let module S = CicSubstitution in
    function
       C.Rel n as t ->
        (* we never perform delta expansion automatically *)
@@ -653,9 +665,13 @@ let simpl context =
         (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
          match o with
            C.Constant (_,Some body,_,_,_) ->
-            try_delta_expansion context l
-             (C.Const (uri,exp_named_subst'))
-             (CicSubstitution.subst_vars exp_named_subst' body)
+            if List.exists is_active l then
+             try_delta_expansion context l
+              (C.Const (uri,exp_named_subst'))
+              (CicSubstitution.subst_vars exp_named_subst' body)
+            else
+             let t' = C.Const (uri,exp_named_subst') in
+              if l = [] then t' else C.Appl (t'::l)
          | C.Constant (_,None,_,_,_) ->
             let t' = C.Const (uri,exp_named_subst') in
              if l = [] then t' else C.Appl (t'::l)