Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Why do we have "Prop < Set" ? Why not just "Prop ≤ Set" ?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Why do we have "Prop < Set" ? Why not just "Prop ≤ Set" ?


Chronological Thread 
  • From: Matej Kosik <5764c029b688c1c0d24a2e97cd764f AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Why do we have "Prop < Set" ? Why not just "Prop ≤ Set" ?
  • Date: Wed, 18 Jan 2017 17:25:03 +0100
  • Authentication-results: mail3-smtp-sop.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-f52.google.com
  • Ironport-phdr: 9a23:pT4bBhDATRghMH67t1UJUyQJP3N1i/DPJgcQr6AfoPdwSPX6pMbcNUDSrc9gkEXOFd2CrakV16yN4uuwAiQp2tWoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6nK94iQPFRrhKAF7Ovr6GpLIj8Swyuu+54Dfbx9GiTe5br5+Nhu7oAHeusQVj4ZpN7o8xAbOrnZUYepd2HlmJUiUnxby58ew+IBs/iFNsP8/9MBOTLv3cb0gQbNXEDopPWY15Nb2tRbYVguA+mEcUmQNnRVWBQXO8Qz3UY3wsiv+sep9xTWaMMjrRr06RTiu86FmQwLuhSwaNTA27XvXh9RtgqxFrhKvpx9xzYDab46aNvVxYqzTcMgGRWdCRMtdSzBND42+YoYJEuEPPfxYr474p1YWqhWxHxWsC/3tyjRVg3H22rY60+UiEQrb2wEtH9ADvXXbodrpKKseT+S4w7LJwDjAbP5ZxSrx55TUfh88v/2BUqh/fdTPxkQrFQ7KkkifpI7kMj6a2OQAqGeb7+96WuKuj24rsR1+oj+qxso1jITCm4wbylfB9SpjwYY1I8W1R1J8Yd6+FptfqSWaN49sTsw8Xm5opT42yrwAuZ6hfSgF0o4rxxDFa/CffIiI4w7jVOaMIThjnn5qZLW/hxO0/EO9yeP8TtG53EhWoidBiNXBtXAA2wbN5sSaSvZx5Ees1SiX2wzO7uxJL1o4mKrGJ5I73LI8ipkevV7dEiPonEj7irKdeF8+9eiy8evnZ63rpp+COI9wjQHzKqEulda+AeQ8KwQOW2ab9fil2L3t/UD1Xq9GjvIxkqnev5DaIdoUqrSlDA9S14Yv8xe/DzG439QEhXQLMk5JdRadg4XqO1zCOu70Aeq/jli2kDpn2ejKPrj7DZXMKnjDnq3hfbF460NEyAc+z9FS6p1IBb0dPv7+XlT+ud3bAxI6LwO43vroBMlg2Y8AVm+AGLGVP73WvFKK+u0gPuuBaY4atTbzMPUl6PvugmU4mV8ZZ6WmwZwXaHWgEvR8P0qZeWbsgssGEWoSogU+S/XqhESeXj5Xena9RLkx5io7CYKjFYfMXJqhgL2H3CehH51ZfHpKCl6WESSgS4LRUPAVLSmWP8VJkzoeVLHnRZVy+wupsVrfwqZqLKL3/TYZttq3iYcru+aLz0A4q2wkBJ2Wi23XE2gukzJXTDNpgvxxiUN4w1aHl6N/hqoLRpRo+/pVX1JiZtbnxOtgBoWqVw==

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



Archive powered by MHonArc 2.6.18.

Top of Page