The Coq mailing list

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

Hi Théo,

Thank you for the reply!

On 01/18/2017 05:39 PM, Théo Zimmermann wrote:
> 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".

I wonder, why did you think that this might make sense?
(Personally, I do not find the above error message surprising.)

> 
> 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

The above behavior is fully consistent with the fact that Prop is declared to 
be a subtype of Set.
(Reference Manual, Section 4.4, Point 4).
This makes sense.

> 
> As for weakening the constraint to Prop <= Set do you have any reasons in 
> mind?

I think that weakening "Prop < Set" to "Prop ≤ Set" makes sense per se, 
unless we have a good reason for those extra restriction.

If there is a good reason for that restriction, we should document it.

If there is no good reason for that restriction:
- it is strange to insist on it
- it inflates the theory
- it creates unnecessary confusion and raises unnecessary questions

> This kind of weakening should allow in particular a constraint resolution 
> where Prop = Set. But Prop and Set are
> supposed to be different!

The strangeness of the "Prop < Set" universe depends directly on how you 
interpret "_ < _".
If we accept the sloppy definition ("Whatever works, man!"), then there is 
nothing strange about this.
If we are fussy about it we can interpret it like:

  If X and Y are two universes then "X < Y" means that "Y" has strictly more 
inhabitants than "X"
                                and "X ≤ Y" means that "Y" has at least as 
many inhabitants as "X".

In the "fussy interpretation" of "<" and "≤", the restriction "Prop < Set" is 
surprising because after starting the toplevel like this:

  coqtop -noinit

neither Prop nor Set have any inhabitants and thus it is not the case that 
"Prop < Set".
The only thing that we can claim is "Prop ≤ Set".

> Because one is predicative and the other is impredicative.

Are you saying that relaxing "Prop < Set" to "Prop ≤ Set" would prevent us 
from keeping impredicativity of Prop and predicativity of Set?
Why?

> And also to help with extraction.

Are you saying that relaxing "Prop < Set" to "Prop ≤ Set" would somehow make 
the extraction more difficult?
Why?

> 
> 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).

As soon as you an inhabitant of "Set" which is not an inhabitant of "Prop" 
(such as "nat"), then "Prop ≠ Set".
In this special case, we can really claim that "Prop < Set" (wrt. to "fussy 
interpretation" of "_ < _").
This does not imply that it makes sense in general.

> 
> 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