The Coq mailing list

[Thorsten Altenkirch <Thorsten.Altenkirch AT nottingham.ac.uk>]

Thank you for your nice summary, Cody.

From: <coq-club-request AT inria.fr> on behalf of roux cody <cody.roux AT gmail.com>
Reply-To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Date: Monday, 29 February 2016 19:00
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Is Coq SN ?

Thorsten gives a model construction for CoC (with *impredicative set* and a Martin-Lof style universe) and large eliminations, and sketches the case of general inductives, though I'm afraid I can't quite understand the full extent of the inductive families that are handled. This model seems to justify much of Coq + impredicative sets - universes. I can't tell whether eta is handled or not for the SN result.

I didn’t do eta and it is not obvious how to extend the construction from my PhD to handle eta. General inductive families should be no problem but I only did an example in my PhD (I was running out of time :-) and after I moved on to NBE).

> Benjamin Werner's thesis *does* have eta reductions (but only one universe), but it's not clear to me whether it addresses the crucial difficulty mentioned by Thorsten: Pi injectivity is needed
>  somewhere in the proof, and it is easily seen as a consequence of confluence on untyped reduction, but this is false on pre-terms with eta. It seems to me that this can be circumvented with a *separate* (and difficult!) proof that typed terms have confluent
>  reductions, and then working with only well-typed terms.

I never tried to read Benjamin’s PhD properly partially because it is written in french. :-) I don’t have time just now but I’d be grateful if sb could explain this to me. 

Cheers,

Thorsten

This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please send it back to me, and immediately delete it. 

Please do not use, copy or disclose the information contained in this
message or in any attachment.  Any views or opinions expressed by the
author of this email do not necessarily reflect the views of the
University of Nottingham.

This message has been checked for viruses but the contents of an
attachment may still contain software viruses which could damage your
computer system, you are advised to perform your own checks. Email
communications with the University of Nottingham may be monitored as
permitted by UK legislation.