coq-club AT inria.fr

Subject: The Coq mailing list

List archive

From: Matej Kosik <5764c029b688c1c0d24a2e97cd764f AT gmail.com>
To: Coq Club <coq-club AT inria.fr>
Subject: [Coq-Club] Why do we have "Prop < Set" ? Why not just "Prop ≤ Set" ?
Date: Wed, 18 Jan 2017 15:27:19 +0100
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=5764c029b688c1c0d24a2e97cd764f AT gmail.com; spf=Pass smtp.mailfrom=5764c029b688c1c0d24a2e97cd764f AT gmail.com; spf=None smtp.helo=postmaster AT mail-lf0-f50.google.com
Ironport-phdr: 9a23:UWnwfROHnkny598aLJcl6mtUPXoX/o7sNwtQ0KIMzox0KP74rarrMEGX3/hxlliBBdydsKMYzbGH+P65ESxYuNDa7yBEKMQNHzY+yuwo3CUYSPafDkP6KPO4JwcbJ+9lEGFfwnegLEJOE9z/bVCB6le77DoVBwmtfVEtfre9Msfogs+2z+G//YHIK0UN3WLlIOA6EBLjhgLI/uISnIEqfq02017CpmZCU+VQ32JhY1yJyUXS/MC1qbtq7ylS89Em7M9DGfGnIPpkRuQCXT54YzA+vcazuUOfRFGCtyQXXjpIzhRgDA3M7RW8VZD05Hip/tFh0TWXaJWlBYs/Xi6vuuIyEEfl

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

[Coq-Club] Why do we have "Prop < Set" ? Why not just "Prop ≤ Set" ?, Matej Kosik, 01/18/2017
- Re: [Coq-Club] Why do we have "Prop < Set" ? Why not just "Prop ≤ Set" ?, Abhishek Anand, 01/18/2017
  - Re: [Coq-Club] Why do we have "Prop < Set" ? Why not just "Prop ≤ Set" ?, Matej Kosik, 01/18/2017
    - Re: [Coq-Club] Why do we have "Prop < Set" ? Why not just "Prop ≤ Set" ?, Matej Kosik, 01/18/2017
      - Re: [Coq-Club] Why do we have "Prop < Set" ? Why not just "Prop ≤ Set" ?, Guillaume Melquiond, 01/18/2017
        
        Re: [Coq-Club] Why do we have "Prop < Set" ? Why not just "Prop ≤ Set" ?, Matej Kosik, 01/19/2017
        
        Re: [Coq-Club] Why do we have "Prop < Set" ? Why not just "Prop ≤ Set" ?, Théo Zimmermann, 01/19/2017
        
        Re: [Coq-Club] Why do we have "Prop < Set" ? Why not just "Prop ≤ Set" ?, Matej Kosik, 01/19/2017
        Re: [Coq-Club] Why do we have "Prop < Set" ? Why not just "Prop ≤ Set" ?, Maxime Dénès, 01/19/2017
        Re: [Coq-Club] Why do we have "Prop < Set" ? Why not just "Prop ≤ Set" ?, Matej Kosik, 01/19/2017
        
        Re: [Coq-Club] Why do we have "Prop < Set" ? Why not just "Prop ≤ Set" ?, Guillaume Melquiond, 01/19/2017