The Coq mailing list

[roconnor AT theorem.ca]

On Mon, 2 Jul 2007, Guillaume Melquiond wrote:

> So I have two choices. Either I bound the number of iterations with an
> arbitrary low value and my functions are no longer guaranteed to return
> the correct result in Coq. Or I bound it with the proved value (which
> don't even exist for all the functions) and Coq will probably die while
> computing this value.

It is my understanding that these are your two choices; although in the 
second case you can, with some care, make sure the the bound is computed 
lazily so that its value is never fully computed.

BTW, could you point me to some introductory material showing easy 
classical proofs of termination that are hard to prove constructively? 
I'd be interested to know more about them.

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