coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Adam Chlipala <adam AT chlipala.net>
- To: Vladimir Voevodsky <vladimir AT ias.edu>
- Cc: Coq Club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] eval compute example
- Date: Fri, 05 Nov 2010 10:48:02 -0400
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.
- [Coq-Club] eval compute example, Vladimir Voevodsky
- Re: [Coq-Club] eval compute example, Adam Chlipala
- Re: [Coq-Club] eval compute example,
roconnor
- Re: [Coq-Club] eval compute example, Vladimir Voevodsky
- <Possible follow-ups>
- Re: [Coq-Club] eval compute example, Bruno Barras
Archive powered by MhonArc 2.6.16.