The Coq mailing list

[Christine Paulin <paulin AT lri.fr>]

Yes there is an explanation. 
    Eval Compute in t 
applies beta-delta-iota reduction to t and then prints the resulting
    term t'

The Compute tactic applies beta-delta-iota reduction to the goal,
get a term t' and then applies something like "Change t'" which checks
again that t is convertible to t' by the usual convertibility function
which tries first convertibility without constant expansion ...

We have changed that in the (hopefully soon to be released) version.

Christine.

In his message of Mon November 8, 1999, Jean Goubault-Larrecq writes: 
> Dear all,
> 
>         I've always thought that Compute and Eval Compute
> implemented the same reduction strategy.  However,
> in recent experiments I realized that Compute was between
> 3 and 4 times slower and used between 6 and 20 times more
> space.  The even stranger thing is that Qed is faster than
> Compute, although I am running all this on examples which
> are meant to be fast under call-by-value.
>         Is there any reasonable explanation?
> 
>         I am using Coq V6.3, and testing things like:
> Coq < Time Eval Compute in (tauto (pb72 (5) (4))).
>      = (ad_x xH)=(ad_x xH)
>      : Prop
> Finished transaction in 61 secs (53.01u,0.3s)
> 
> Coq < Fact gag : (tauto (pb72 (5) (4))).
> Coq < Time Compute.
> 1 subgoal
> 
>   ============================
>    (ad_x xH)=(ad_x xH)
> Finished transaction in 260 secs (177.71u,2.1s)
> 
> gag < Time Reflexivity.
> Subtree proved!
> Finished transaction in 0 secs (0u,0.01s)
> 
> gag < Time Qed.
> Compute.
> Reflexivity.
> 
> gag is defined
> Finished transaction in 146 secs (121.89u,0.6s)
> 
> 
>         All the best,
> 
>         -- Jean.

-- 
  Christine Paulin-Mohring             mailto : 
Christine.Paulin AT lri.fr
  LRI, URA 410 CNRS, Bat 490, Université Paris Sud,   91405 ORSAY Cedex 
  LRI   tel : (+33) (0)1 69 15 66 35       fax : (+33) (0)1 69 15 65 86
  INRIA tel : (+33) (0)1 39 63 54 60       fax : (+33) (0)1 39 63 56 84