The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT ens-lyon.fr>]

Le lundi 02 juillet 2007 à 05:57 -0400, 
roconnor AT theorem.ca
 a écrit :

> > Or perhaps I should put False in my hypotheses so that I can build a
> > witness of termination on the fly without any computation?
> 
> Adding a False hypothesis won't help of course.  The witness will 
> eventually reduce down to (False_rec false_hypothesis ...) and reduce no 
> further because false_hypothesis is a variable.  Since this expression is 
> not a consturctor, reduction of the fixpoint will no continue.

You are right. Even adding False in the context does not seem to help in
my case.

> > If you have any other suggestions, I would be glad to hear them. I would
> > really like to avoid having to extract functions into ML and then
> > importing back their computed results into Coq.
> 
> You can give a natural number for the number of iterations you wish to 
> evaluate.

No, that was the whole point: I can't give such a number. It probably
sounds strange, so I will try to explain the context a bit more.

In my case, a short proof in classical logic tells that the number of
iterations is finite. Actually, it's almost by definition of the
functions.

For a few functions, there are some complicated "constructive" paper
proofs written by complexity theorists. They tell that the number of
iterations is smaller than several billions. And for the other
functions, we don't even have witnesses: the question is still an open
one.

But for all practical purposes, we are lucky, as these functions only
perform a few iterations before returning the correct result. Let me
stress this point: Even though the theory says that they will take ages,
it is actually realistic to compute with these functions. People do rely
on them in computer programs (e.g. Ziv's mathematical functions are the
default implementation for glibc on amd64 architectures). I would like
to implement such functions in Coq.

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.

Anyway, I'm getting off-topic here.

> > Needless to say, I would rather have the opposite situation: Coq would
> > instantly compute my function since the context is consistent, and it
> > would go into an infinite loop when the context is inconsistent.
> 
> Well it is nice for Coq to terminate when doing a convertability check of 
> a term that happens to be in an inconsistent context.  If not, we might 
> have big problems.

This is really interesting, as I didn't expect that this problem could
actually occur. Do you know of such an occurrence in a real body of Coq
proofs, e.g. the standard library of Coq?

Best regards,

Guillaume