The Coq mailing list

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

On 01/18/2017 05:25 PM, Matej Kosik wrote:
> 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.
> 

... fails ...

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

My question is about weakening (not strengthening)

  Prop < Set

to

  Prop <= Set

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