The Coq mailing list

[Patrick Loiseleur <Patrick.Loiseleur AT lri.fr>]

In his message of Wed April 8, 1998, Marc Bezem writes: 
> Hallo,
> 
> How come that sometimes Simpl takes over a minute, whereas Compute
> is almost instantaneous?

It's fairly simple : Compute does dummy bdi-normalization and is optimized
to do that quickly. Simpl does more complicate things : when it
encouters a Fixpoint applied to a constuctor, it unfolds the Fixpoint,
does a step of iota-reduction and then searches occurences of the
unfolded fixpoint and re-fold these occurences (i.e. replace the
corpus of the fixpoint by the name of the constant). For example :

Coq < Eval Simpl in [n,m:nat](plus (S (S m)) n).
     = [n,m:nat](S (S (plus m n)))
     : nat->nat->nat

Coq < Eval Compute in [n,m:nat](plus (S (S m)) n).
     = [n,m:nat]
        (S
          (S
            (Fix plus{plus [n0:nat] : nat->nat := 
                        [m0:nat]
                         Cases n0 of
                           O => m0
                         | (S p) => (S (plus p m0))
                         end} m n)))
     : nat->nat->nat

So :

1) It's normal than Simpl does only partial reduction
2) It's also normal that Simpl is quite (very) slow : this sort of
reduction will be too hard to optimize. 

Best regards,

Papageno