The Coq mailing list

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

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. 
>
> 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. 
>   
Hello,

If you inspect the definition of boolle, you will see that it is not
suitable for a call-by-value evaluation (irrelevant parts elided):

fun m =>
nat_rec _ (fun _ => true)
(fun _ (IHm : nat -> bool) n =>
nat_rec _ false (fun n0 (_ : bool) => IHm n0) n) m

The problem is in this subterm: (nat_rec _ false (fun n0 _ => IHm n0) n)

When n=20, (let F = fun n0 _ => IHm n0)
nat_rec false F 20 --> F 19 (nat_rec false F 19) --> F 19 (F 18 (nat_rec
false F 18))
--> ... --> IHm 19

In call-by-value, (nat_rec false F 19) is evaluated but it is not needed
(and lazy reduction will not evaluate it) because F does not use its 2nd
argument.
This means that you will compute IHm 0, IHm 1, ... IHm 19 but only the
last one is needed.

At the higher level, (boolle 36 20) results in the following recursive
calls:
(boolle 35 0), (boolle 35 1), ... (boole 35 19). The asymptotic
complexity is exponential in n, as you observed.

Also, replacing induction by destruct will turn the second nat_rec into
a match => no more recursive calls on n.

As a rule of thumb, you'd better not use eval compute on programs built
using tactics, unless you take great care to use the induction tactic
only when you need the induction hypothesis.

If you really insist in making the proof using tactics, you can do some
partial evaluation on boolle, to make it cbv-friendly:
Definition boolle' :=
Eval cbv beta delta [boolle nat_rec nat_rect] iota in boolle.

Unfolding all *_rec and *_rect constants is a good start. boolle' still
contains 2 fixpoints, but the second one is not used. This is more or
less what the extraction does, so that the extracted programs can
reasonably be evaluated in cbv.

> I am not sure whether this example calls for any changes or not but it has 
> definitely been educational to me. 
>
>   
This is another instance of the usual dilemna between cbv and lazy
programming languages...

Hope this helps.

Bruno.