The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

Going by the general rule that Ui:Uj if i<j, I suspect that Prop < Set would allow the following:

Check (Prop:Set)

which fails in Coq 8.5pl3.

So the stronger constraint may allow some new well-typed terms and potentially complicate arguments about normalization/consistency etc.

-- Abhishek

http://www.cs.cornell.edu/~aa755/

On Wed, Jan 18, 2017 at 9:27 AM, Matej Kosik <5764c029b688c1c0d24a2e97cd764f AT gmail.com> wrote:

Hi,

I have noticed that in Coq, we have the following universe constraint:

  Prop < Set

I am wondering what is the reason for that?
Wouldn't

  Prop <= Set

suffice in this case?

The code that makes the decision is here:

  https://github.com/coq/coq/blob/trunk/kernel/uGraph.ml#L716

I wonder whether it is necessary to do:

  enforce_univ_lt Level.prop Level.set empty

as now, or we could simply do

  enforce_univ_leq Level.prop Level.set empty

I've created an experimental branch where I did the change:

  https://github.com/matej-kosik/coq/commit/2fcbb0ced3bc32210ae9fbf4acc40804841c9200

ran some tests:

  https://ci.inria.fr/coq/view/coq-contribs/job/coq-contribs/653/console
  https://ci.inria.fr/coq/view/opam/job/opam-install/22/console

and I do not see any breakage but the major question is, would this kind of change make Coq inconsistent
(enable us to prove False)
or not?

Thank you in advance for any insight on this.
--
Matej Košík