The Coq mailing list

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

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?

Or perhaps I should put False in my hypotheses so that I can build a
witness of termination on the fly without any computation?

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.

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

Best regards,

Guillaume