The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

Vladimir Voevodsky wrote:
> Here is a very simple example of a situation where [eval compute] behaves in a very 
> non-linear fashion and slows down terribly on small inputs while [eval lazy] returns an 
> answer in less than a second. There are no hidden axioms or anything like in this 
> example. The function in question is a boolean version of "less or equal" 
> predicate.
>
>
> Definition boolle (m n : nat): bool.
> Proof. intro. induction m. intro. apply true. intro.  induction n.  apply 
> false.  apply (IHm n). Defined.
>    

A bit of a meta-answer to complement Bruno Barras's more specific answer:

I recommend never using tactics to write anything that you think of a 
program.  Many people use tactics to write programs with complicated 
dependent types, but I recommend not allowing any exceptions to the "no 
tactics for programs" rule.  This evaluation performance example shows 
just one way that things can go wrong if you depend at all on the 
computational behavior of a term you defined with tactics.

A big chunk of CPDT (http://adam.chlipala.net/cpdt/) explains how to 
code dependently-typed programs manually, so that there's no need to 
rely on any kind of tactics.