The Coq mailing list

[Marc Bezem <Marc.Bezem AT phil.ruu.nl>]

Hallo,

How come that sometimes Simpl takes over a minute, whereas Compute
is almost instantaneous?

For example:

1 subgoal
 
  em : EM
  ac : AC
  d : D
  ============================
   (E'' (CLAUS (f_not f_PP)))
 
PP < Simpl.
1 subgoal
 
  em : EM
  ac : AC
  d : D
  ============================
   (f:SKF)
    ((x:D)(A (pub x)))
     ->((x:D)(A (drunk x)))
        ->((x:D)(A (pub (f O (ml D x)))))
           ->((x:D)~(A (drunk (f O (ml D x)))))
              ->((x:D)(A (pub (f (S O) (ml D x)))))->False

takes almost 100 sec.
 
PP < Compute (E'' (CLAUS (f_not f_PP))).
     = (f:nat->(list D)->D)
        ((x:D)(A (pub x)))
         ->((x:D)(A (drunk x)))
            ->((x:D)(A (pub (f O (cons D x (nil D))))))
               ->((x:D)(A (drunk (f O (cons D x (nil D)))))->False)
                  ->((x:D)(A (pub (f (S O) (cons D x (nil D))))))
                     ->False
     : Prop
 
takes 10 sec. AND reduces more (e.g. SKF = nat->(list D)->D)).
By the way, we like result of Simple better, but Simple can be expected
to be too slow on larger examples.

Many thanks, Marc Bezem.