The Coq mailing list

[Vladimir Voevodsky <vladimir AT ias.edu>]

Hello,

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.


On my machine

Eval compute in (boolle 36 20)   -- takes about 2 sec. 

Eval compute in (boolle 36 25)  -- takes about 70 sec. 

Eval compute in (boolle 36 26) -- takes about 140 sec. 

and

Eval compute in (boolle 37 25) -- takes about 70 sec. 

and 

Eval lazy in (boolle 36 26) -- takes less than 1 sec. 


When the second [induction] in the proof of boolle is replaced by [destruct]  
Eval compute starts to give answers as fast as Eval lazy. In fact I get less 
than a second delay in


Eval compute in (boolle 3700 2500).

I am not sure whether this example calls for any changes or not but it has 
definitely been educational to me. 

Vladimir.