The Coq mailing list

[Matej Kosik <5764c029b688c1c0d24a2e97cd764f AT gmail.com>]

On 01/18/2017 05:56 PM, Théo Zimmermann wrote:
> In fact, having Prop < Set, or Prop <= Set as a universe constraint does 
> not force Prop : Set.
> And indeed:
> Coq < Set Printing Universes.
> 
> Coq < Check Prop.
> Prop
>      : Type@{Set+1}
> 
> Coq < Check Set.
> Set
>      : Type@{Set+1}
> 
> That is Prop and Set both are at bottom of the type hierarchy: there are 
> just two distinct bottoms.

Well, if you claim "Prop < Set", how can you say that "Set" is at the bottom 
of the type hierarchy?
(we are back to the question: "What does _ < _ mean to you?")

> One of them is predicative:
> Coq < Check (forall P : Prop, P).
> forall P : Prop, P
>      : Prop
> 
> And one is impredicative:
> Coq < Check (forall P : Set, P).
> forall P : Set, P
>      : Type@{Set+1}

(I guess that you wanted to say "Prop is impredicative" and "Set is 
predicative".)

I am not sure if I understand why would these (desirable) properties prevent 
us from relaxing "Prop < Set" to "Prop ≤ Set".

> 
> Le mer. 18 janv. 2017 à 17:36, Théo Zimmermann 
> <theo.zimmi AT gmail.com
>  
> <mailto:theo.zimmi AT gmail.com>>
>  a écrit :
> 
>     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
>  
> <mailto: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>
>  
> <mailto: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
> 


-- 
Matej Košík