The Coq mailing list

[Théo Zimmermann <theo.zimmi AT gmail.com>]

Hi,

Disclaimer: there are people so much more qualified than me on this list who can answer this question. But as they did not wake up yet (maybe they are too engrossed in some POPL presentations) I will try to give a few hints.

My personal, very limited, understanding of the universes was also that Prop : Set : Type 1 : Type 2 : ...

But actually Check Prop : Set. fails both in Coq 8.6 and in your branch. I am not sure I understand why.

Coq < Check Prop:Set.
> ^^^^^^^^^^^^^^^
Error:
The term "Prop" has type "Type" while it is expected to have type "Set".

However, we can see that the constraint allows one to give type Set to something of type Prop:

Coq < Check False : Prop.
False : Prop
     : Prop

Coq < Check False : Set.
False : Set
     : Set

As for weakening the constraint to Prop <= Set do you have any reasons in mind? This kind of weakening should allow in particular a constraint resolution where Prop = Set. But Prop and Set are supposed to be different! Because one is predicative and the other is impredicative. And also to help with extraction.

However, even in your branch where you are supposed to have relaxed the constraint, it seems that there is still something preventing Set and Prop to be considered equal:
Coq < Check nat : Prop.
> Check nat : Prop.
>       ^^^
Error:
The term "nat" has type "Set" while it is expected to have type
"Prop" (universe inconsistency).

Théo

Le mer. 18 janv. 2017 à 17:20, Matej Kosik <5764c029b688c1c0d24a2e97cd764f AT gmail.com> a écrit :

Hi,

On 01/18/2017 05:10 PM, Abhishek Anand wrote:
> 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.

AFAIK this:

  Check Prop:Set.

in all versions of Coq (8.5, 8.6, trunk).
That makes sense.

And precisely for that, the current version of the constraint:

  Prop < Set

does not make sense (to me).

>
> 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/ <http://www.cs.cornell.edu/~aa755/>
>
> On Wed, Jan 18, 2017 at 9:27 AM, Matej Kosik <5764c029b688c1c0d24a2e97cd764f AT gmail.com <mailto: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 <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 <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/coq-contribs/job/coq-contribs/653/console>
>       https://ci.inria.fr/coq/view/opam/job/opam-install/22/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
>
>


--
Matej Košík