The Coq mailing list

[roconnor AT theorem.ca]

BTW, you may find the Time command useful for this sort of experiment:

Time Eval compute in (boolle 36 20).
     = false
     : bool
Finished transaction in 5. secs (4.844263u,0.s)

Time Eval lazy in (boolle 26 30).
     = true
     : bool
Finished transaction in 0. secs (0.000999u,0.s)

On Fri, 5 Nov 2010, Vladimir Voevodsky wrote:

> 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.
>
> and
>
> Eval lazy in (boolle 36 26) -- takes less than 1 sec.

--
Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''