The Coq mailing list

[Kirill Taran <kirill.t256 AT gmail.com>]

Adam and Guillaume,

Thank you for the reference and examples; they clearly show how to construct such fixpoints.

Sincerely,
Kirill Taran

On Sat, Apr 26, 2014 at 1:12 AM, Guillaume Melquiond <guillaume.melquiond AT inria.fr> wrote:

On 25/04/2014 19:45, Kirill Taran wrote:

Didn't know about ConstructiveEpsilon module. Thanks for example.
But why will your example not compute? I don't see any axiom usage there.

This is not related to axioms. The lack of axioms tells you that the existence of f' is consistent; it does not tell you that (f' some_x) will reduce to a value of Y different from (f' some_x).

The rule of thumb is that, whenever Coq needs to perform a step of computation, it has to consume a constructor from a term somewhere. If there are no constructor left to consume, Coq will stop reducing things. So, as soon as you have some opaque definitions around, e.g. the termination lemma, Coq is cut off from its sources of constructors and it stops computing.

But that is not an issue, you just need to artificially introduce sufficiently many constructors. The attached example shows how to do it. It adds 2^64 constructors, which should guarantee that your computer will break down before Coq runs out off constructors.

There is a small test at the end that shows the difference between the version that does not compute and the one that does.

Best regards,

Guillaume

PS: Do not try to "Print" the f' function. There seems to be a bug in Coq that causes it to display garbage. What you see is definitely not how f' is defined; what you see is not even well-typed. (I hope it is only a display issue.)