The Coq mailing list

[Gabriel Scherer <gabriel.scherer AT gmail.com>]

- [a machine formalized proof] is extremely tough, given the technical complexities involved, and the Godelian meta-theoretical issues (certainly something will have to be assumed as an axiom).

On a practical level, I have tried to do mechanized proofs of simpler systems in the past and I my personal impression was that the lack of induction-recursion made Coq unsuitable for formalization of universe hierarchies. This is one of the reason why I am very happy to hear that Matthieu Sozeau is working on induction-recursion. Of course, adding it worsens the problem of "mecha-meta-theoretizing the whole of Coq", but I think that having a system tomorrow in which the whole of today's situation can be exposed would be very valuable nonetheless.

On Thu, Dec 22, 2016 at 2:27 PM, roux cody <cody.roux AT gmail.com> wrote:

As the discussed example (and the example discussed last week) shows, Gallina/Coq is *not* SN, though as far as we know it *is* WN, which is enough for consistency.

This issue comes up regularly on the list, and I believe that the summary is as follows:

- It's extremely difficult for the theory to keep up with the practical demands of the system.

- We should be trying to have a reasonable meta-theory anyways.

- There are a few papers which prove normalization of various fragments and variants of Coq. However, I know of none that handle CiC + Impredicative Prop + Universes + Large Elimination (don't even ask about impredicative set!). I can try to list them if required, but I always worry about forgetting a crucial one.

- The above works are extremely technical and hard to fully check, this seems to be begging for a machine formalized proof.

- Such a proof is extremely tough, given the technical complexities involved, and the Godelian meta-theoretical issues (certainly something will have to be assumed as an axiom).

My constant call is for a more thorough exploration of the abstract structure of such proofs, so we can clearly separate it into combinatorial considerations + a model construction, which may be more tractable. There's a bunch of work on this as well, including the whole sub-field about normalization-by-evaluation, but CiC + universes seems a bit out of reach for now with such techniques, and again, writing down the whole construction is extremely tedious and error prone.

Hope this helps give the high overview,

Best,

Cody

On Thu, Dec 22, 2016 at 8:10 AM, Bas Spitters <b.a.w.spitters AT gmail.com> wrote:

This page refers to an example showing that Coq is not SN (due to the
guard condition).
https://coq.inria.fr/cocorico/CoqTerminationDiscussion

However, this (unpublished) report claims that CiC (with Prop and
universes) is SN.
http://csweb.rice.edu/uploadedFiles/Computer_Science/Research/Tech_Reports/TR11-01.pdf
Uniform Logical Relations - Eddy Westbrook

Has there been any progress on this? It would be good to update the
wiki/FAQ with this information.