The Coq mailing list

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

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