The Coq mailing list

[roconnor AT theorem.ca]

On Mon, 2 Jul 2007, Guillaume Melquiond wrote:

> Le lundi 02 juillet 2007 à 04:10 -0400, 
> roconnor AT theorem.ca
>  a écrit :
> > Coq needs to evalutate the witness of termination into some sort of head
> > normal form before proceeding with one step of recursion.  Coq wants to
> > verify that your proof of termination isn't ``hypothetical'' by making
> > sure that the normal form begins with a constructor.  This means that your
> > proof of termination needs to be sufficently transparent and cannot have
> > axioms that end up at the head position of the witness of termination.
>
> Do I understand correctly from your reply that it is impossible to write
> a recursive function in Coq if you can't explicitly build an inductive
> object that is deeper than the number of recursive calls?

I believe that is correct.

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

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

> > Making sure that the witness of termination isn't hypothetical ensures
> > that Coq will not go into an infinite loop when evaluating a recursive
> > function inside an inconsistent context (such an inconsistency could arise
> > from axioms or from variables or hypothesis of functions).
> >
> > In theory Coq is not going into an infinite loop in your latter case.
> > Evalutation of the fixpoint presumably gets stuck when the head of the
> > witness of termination becomes an axiom of classical logic rather than a
> > constructor.  Then compute proceeds to put the rest of your proof into
> > normal form by eliminating cuts.  I'm not sure how many hours, days, or
> > years it will take for Coq to finish normalizing the remainder of your
> > proof, nor do I know how much memory will be used by the normalized proof.
>
> (Actually, it does not take that long: the Coq process soon gets killed
> by the operating system for having exhausted the whole swap space.)
>
> The situation is kind of ironic. The witness of termination has to be
> explicit so that Coq does not go into an infinite loop when the context
> is inconsistent. But in my case, this restriction causes Coq to go into
> a seemingly infinite loop while the context is consistent.
>
> 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.

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