Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Strange subtyping

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Strange subtyping


Chronological Thread 
  • From: Théo Zimmermann <theo.zimmi AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Strange subtyping
  • Date: Sat, 9 Jun 2018 11:09:23 +0200
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=theo.zimmi AT gmail.com; spf=Pass smtp.mailfrom=theo.zimmi AT gmail.com; spf=None smtp.helo=postmaster AT mail-vk0-f52.google.com
  • Ironport-phdr: 9a23:XIfxAB8jHmCs0P9uRHKM819IXTAuvvDOBiVQ1KB40+gcTK2v8tzYMVDF4r011RmVBdids6oMotGVmpioYXYH75eFvSJKW713fDhBt/8rmRc9CtWOE0zxIa2iRSU7GMNfSA0tpCnjYgBaF8nkelLdvGC54yIMFRXjLwp1Ifn+FpLPg8it2O2+553ebx9UiDahfLh/MAi4oQLNu8cMnIBsMLwxyhzHontJf+RZ22ZlLk+Nkhj/+8m94odt/zxftPw9+cFAV776f7kjQrxDEDsmKWE169b1uhTFUACC+2ETUmQSkhpPHgjF8BT3VYr/vyfmquZw3jSRMMvrRr42RDui9b9mRxDmiCgFNzA3/mLZhNFugq1Hux+uvQBzzpTObY2JKPZzfKXQds4aS2pbWcZRUjRMDJ28b4wVCOoOJeVXr4j4p1sLsxS+HwysC/npyj9Om3T72rE60+Q/HgHBxgAhHtMOsHHRrNX0L6oSXuW1w7PJzTXHdf9ZxTD96I3Rfx0nvPqCXqpwfNLPxUUzEw7JlFadpIz/Mz+Ly+gAvXKX4up+We+plmUpsRt+oiK1yccpkoTJhpwaylTD9ShhxYY6P9y4SEpibd66E5tcqziWN4V2T888WW1otyE6yroJuZ6/YicG0ogoxxnaa/CfcoiI5AzsVPqJLDtmmH5ofKizihWy/ES61OHwS8e53ExKoyZbitXMs2oC1x3X6siJUPt9+UKh1C6T1wDT9O5EJlo4lKvaK54kx74wl4EesUvGHiDsmUX2iLWaeVkj+uit8+jneKnppoeAN49ojQHzKrghmsumAeghLgcOW3Wb9v+n2b34/Uz5Ra1KgecsnqnYtpDaP8UbqbSjDw9byIZwoyq4WjyhyZETmWQNBFNDYhOOyYbzaH/UJ/WtMfc+hGOekTJuyurDN7vnSsHRLnXE1qXgeLN8w0FZwQs3i9tY4sQHWfk6PPvvVxqp55TjBRgjPlnsmre1OJBGzoobHFm3LOqcOaLWv0WP47t2ceaJbY4R/j36Lqp8vqK8vToCgVYYOJKR894PcnnhR6ZpJkyYZTznhdJTST5X7Dp7d/TjjRi5aRAWZ3u2WPhhtDQyCYbjE4SbA47w2vqO2yC0GpAQbWdDWAiB

Yes it is intended: your reasoning is perfectly accurate and unsurprisingly it is confirmed by the Coq type checker.

Le sam. 9 juin 2018 à 01:17, Helmut Brandl <helmut.luis.brandl AT gmail.com> a écrit :
Sorry. I cannot yet get it straight.

From the subtype rules in the reference manual and your response to my question it has to be the case that Prop <= Set.

From the Conv rule I conclude that T:Prop implies T:Set.

This implies that I can feed any proposition into an argument expecting a Set.

Definition idset (A:Set)(x:A):=x.

The term idset (0<=0) (le_n 0) surprisingly passes the type checker.

Is this really the intended behaviour?

Sorry if my question is to stupid. But it puzzles me.

Regards
Helmut
On Thu, Jun 7, 2018, 10:04 Matthieu Sozeau <mattam AT mattam.org> wrote:
Hi,

What we don’t have is Prop : Set indeed, only Prop <= Set and Set <= Type(i). Actually we even have Prop < Set internally, i.e the two sorts are enforced to be distinct. One reason is that the set-theoretic model allows this, the impredicative universe Prop being interpreted as { ø, { ø } } which is a subset of Set’s interpretation. However this subtyping rule is a bit of a pain as it complicates the model: one has to modify the interpretation of function types and applications to use a so-called trace encoding to kind of dynamically detect if a term is in Prop or Set. If we remove it (which is a plan we have for a future version of the calculus), then one can see Prop as a separate universe from the predicative Type hierarchy and your example wouldn’t work anymore.

Hope this helps a little,
— Matthieu
Le jeu. 7 juin 2018 à 16:34, Helmut Brandl <helmut.brandl AT gmx.net> a écrit :
Hi.

I am confused by a subtyping rule mentioned in chapter 4.4 of the reference manual.

It says that Prop is a subtype of Set. I checked it with the identity function

Definition id {T:Set} (x:T):= x.

And indeed the _expression_ "id I" is well typed.

I always thought that both Set and Prop are subtypes of Type(i) for any i but are not related in the subtyping relation.

What is the reason for this subtyping rule? Can anybody explain?

Thanks
Helmut



Archive powered by MHonArc 2.6.18.

Top of Page