The Coq mailing list

[Vladimir Voevodsky <vladimir AT ias.edu>]

Thanks!!

As a reply to Adam's comment - I am writing my mathematical library based on 
Univalent Foundations which uses for some proofs a kind of extensionality 
axiom. 
I do eval-computes on simple examples from time to time to see if the axiom 
interferes with normalization and if it does then in what precise way.  This 
particular example is a result of one of these check-ups which I decided to 
investigate in more detail just because it gives such a clean demonstration 
of how sensitive eval-compute is to details of the proofs. 

Vladimir.





> 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.''