The Coq mailing list

[Bruno Barras <Bruno.Barras AT inria.fr>]

Dear Marc,

Patrick's explanation is sound, but something more should be said
about reduction. There is such a gap between Simpl and Compute
because they have completely different implementations.

Simpl is implemented ``naively'', and is rather inefficient on large
terms, especially when using reflection tactics.
Compute reduces its argument with a call-by-value strategy, and
substitutions are performed using closures, which is more
efficient than the naive implementation with substitutions.
This ``ad-hoc'' implementation, especially designed for reflection
tactics, first appeared in the V6.1.

This was generalized in the V6.2, and a new set of tactics appeared.
For example, Compute is now a tactic (and the old Compute vernac, is
now written Eval Compute in ...), which normalizes the goal.
Two parameterized reduction tactics were implemented: Cbv and Lazy,
followed by flags (such as Beta, Delta, Iota) to control which kind of
redexes must be reduced. Cbv is a call-by-value strategy (indeed,
Compute is an abbreviation for Cbv Beta Delta Iota), and Lazy is a
call-by-name strategy with sharing (this means that arguments of a
function call are computed at most once).
This will be documented in the (very soon) coming documentation of the
V6.2.

Since the reduction done by Simpl is not a combination of the flags
above (as Patrick explained), it is still implemented the old way (but
it is not a desperate case).
For the moment, I would strongly recommend you not to use Simpl in the
cases such as those you showed at TYPES'98. When Compute reduces too
much, you can try to re-fold constants. For instance, nat->(list D)->D
may be refolded with Fold SKF, or Fold plus in Patrick's example (Fold
is also a new conversion tactic of V6.2).

Cheers,

Bruno Barras.