Skip to Content.
Sympa Menu

coq-club - [Coq-Club] subset-as-sigma-type VS subset-as-predicate

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] subset-as-sigma-type VS subset-as-predicate


Chronological Thread 
  • From: Iaroslav Baranov <kciray8 AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: [Coq-Club] subset-as-sigma-type VS subset-as-predicate
  • Date: Sat, 3 Aug 2024 11:48:00 +0400
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=kciray8 AT gmail.com; spf=Pass smtp.mailfrom=kciray8 AT gmail.com; spf=None smtp.helo=postmaster AT mail-yw1-f182.google.com
  • Ironport-data: A9a23:12TDtq2uqHGBgW/mYvbD5U91kn2cJEfYwER7XKvMYLTBsI5bpzxTn GVKW27UbP7fZmb0eY90PYy/oR4A6sKByYM1TlNr3Hw8FHgiRejtVY3IdB+oV8+xBpSeFxw/t 512hv3odp1coqr0/0/1WlTZhSAgk/vOHNIQMcacUghpXwhoVSw9vhxqnu89k+ZAjMOwa++3k YqaT/b3Zhn9ilaYDkpOs/jf8EM356yj0N8llgVWic5j7Ae2e0Y9V8p3yZGZdxPQXoRSF+imc OfPpJnRErTxon/Bovv8+lrKWhViroz6ZWBiuVIKM0SWuSWukwRpukoN2FXwXm8M49mBt4gZJ NygLvVcQy9xVkHHsLx1vxW1j0iSlECJkVPKCSHXjCCd86HJWyXC7vhpUB81BpInq9RbOWhl8 P8gNAlYO3hvh8ruqF66Yuxlh8BmPdayeY1G6ismwjbeAvIrB5vERs0m5/cChGZ21p0IRKyOI ZNJM1KDbzyYC/FLElQcCYg3jbeAiXz2cjkeo1WQzUYyyzmIkVQgjOm0WDbTUoGJXd57tFa6n 0/5pk3yWCxAFvGk6RPQpxpAgceUwHqjB9NMfFGizdZhh0TWzWgOAjUNRF6jqL+4jFS/UpRRM SQpFjEGqKEz8Am6UYC4UUTo+jiLuRkTX9cWGOo/gO2Q9kbKy1i3K2UDEmBCU8MZ5f0afTUB0 1yxg+q8UFSDr4apYX6a876Vqxa7Ni4UMXIOaEc4oe0ts4mLTGYb3kKnczpzLJNZmOEZDt0Z/ txnhC03hrFWnNFSkqvirQqBjDWrqZzECAUy4207v15JDCsoPuZJhKTxtjA3CMqsyq7HFTFtW 1BawKCjABgmV83lqcB0aLxl8EuVz/iEKibAplVkAoMs8T+gk1b6ItoKvG8mexk2aphdEdMMX KM1kVMAjHO0FCv6BZKbn6roWqzGMIC5SYq1Bq2NNLKinLAoKVDWoHkGibGsM5DFyxV1yf5uZ /93gO6jCnEVDakvzTy9AY8gPUwDl0gDKZfobcmjlXyPiOLADFbMEOttGAXUMogRsvjfyC2Lq IY3Cid/408AOAEISnKHr9B7wJFjBSRTOK0aXOQLLrbYclo/QztJ5j246epJRrGJVp99zo/gl kxRkGcBoLYmrSSfc1/YWWMpc771Q5d0oFQyOCFmbx7i2GEubczrpO0Tfoc+N+tvvuFy7+9Gf 99cceW5A9NLVmvm/RYZZsLDt4BMTkmgqj+PGCuHWwIBWaBcaTbHwfLaWzf+1TIvC3O3vPQuo rf72QL8R4ECdjtYD83XSayOygqxtEcChO9CVFvsHehDX2nN7bowejLD1O8zB8QqNx/45yC70 jyOCkwyvtj9oI4S8fjIi5ubroyvLfBMI0pCE0Tf7pe0LSP//Ff/8bRfUe2NQy/RZFn09Iqme +9R6fP2a98Do3pnrKt+FOxN4Z8lxt6yuYJf8BtoLE/LY3uvFLlkBHuMhutLl69Vw45mqRmEY V2O9vZaKIe2FpvcSnBJHzUcb8OHyf0wsRvR565sIEzFuQlGzIDeWkBWZxSxmChRKYVuC7wcw MAjhdU37jKugR97I/eEiSFpr163FEIiaJl+lJ8mA97MsDEJm3Viep3XDxHk7K6fM+tsNlYYG R7Kpa7gqYkF+G/8XSsdKXz/09BZp6wygzFR7VpbJ122itvP3fA2+xtK8AUIdAdezzQZ8ud/J llUM1ZRIIOQ9QxJn+lGZXinQCtaNS2a+2vw6loHr3LYRE+WTV7wLHUxFOKO3UIB+UdeQ2R/0 JSH7l36CBDGUdrU3CQgfWJE8dnYUs1X5AnOvOuFDva1NcA2ThS9i5D/eFdSjQXsBP0AoXHup M5o2b1VQrL6PytBmJ8LIdCW+ppIQS/VOVEYZ+9q+Z4IOmTueDuS/zyqAGLpc+NvI836y2OJO /ZMFOluCSvnjD2vqwoFD5EiO7V3xf4lxOQTc4PReFIpjeGtkSpLgrnxqA7Fm24Zc/d/m50cK 6TQVQ64PE6+uH92o1LJ/e54YjeWQN9cfwDt/vGHwMNQHbI5jexcW0UT0Ly1gnarDDVa7y+k5 APuWquH4NFhmKJNnpTtGJptHw+bC83+f8XW/RGRs+ZhV8LuM8DPhVlMqlDYIBlnZ+oNetVol IaitMz881PFsY0XDUHYucilPItY6fqiWNF4NprME0Bbui+ZSenQ7AAm6UnhDbB0yPZm+diAa y6jTcmBZfo5eox6+iVOSi58Fx09NfzGXp34r3ngk8XWWwkv7wPXCfiGq1r7Zn5/XQ0VMcTcD gTUha6f1upApt4ROC5eVuBUOL4mElrNQqB8SsbQswOfBWyWgl+vnLvuuB4jyDPTAEm/D8fIz sPZdyf6aSiNlvnE/PNBv6x2my8nPnJ3rO0zX0AaovpdqTSxCkwYJuU8b7QCLLxpkRLJ6ZKpX wGVMVMeChj8UwodIF+4qJ7mUxyED+MDBsbhK3Z7twmIYiOxH8WbDKEn6i5k5GxsdyD+yP28b +sT4WD0IgP716QBqTz/PRBnqbwPKjLmKnM0FYTVlsXzB1MPHuxP2iUxRkxCUivIF8yLn0LOT YTwqaaoX2njIXMd0+45E5KWJP3dlDzqxjQsKyyIxb4zfq2FmfZYxqSX1/7bi9U+gQdjGFLKb XzyTmqJpWuR3xT/fEfvV80B2cdJNB5AIiR2wGIPi+Hfc2FcJ1nL5/8/oBc=
  • Ironport-hdrordr: A9a23:RsMKPq6+d0/aPFTUNQPXwMXXdLJyesId70hD6qkRc20zTiX8ra qTdZsgpHzJYVoqOE3I+urgBEDjewK/yXcd2+B4VotKNzOW3VdAQrsSibcKAAeNJ8Q9zINgPG tbHJSWweefMWRH
  • Ironport-phdr: A9a23:jMn7nheVEff4juvH5+Deq/qvlGM+ldTLVj580XLHo4xHfqnrxZn+J kuXvawr0ASRG9WCoKse16L/iOPJZy8p2dW7jDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgH c5PBxdP9nC/NlVJSo6lPwWB6nK94iQPFRrhKAF7Ovr6GpLIj8Swyuu+54Dfbx9HiTezfb9+N ha7oRjeusULn4dvJbs6xwfUrHdPZ+lZymRkKE6JkRr7+sm+4oNo/T5Ku/Im+c5AUKH6cLo9Q LdFEjkoMH076dPyuxXbQgSB+nUTUmMNkhpVGAfF9w31Xo3wsiThqOVw3jSRMNDsQrA1XTSi6 LprSAPthSwaOTM17H3bh8pth69dvRmvpQFww5TMbY6aNPRwcKDTc84ES2VdRcteTTBND5mmY ocTE+YMP+BVpJT9qVsUqhu+ABGhCuD1xT9SgX/2xqk63P4/EQrbwQEvBcgOv27SrNXyKqcZT Oe4zKrUwjXCdfNZwzf85YvTfxAupPGDR7Nwcc7LxUYzEAPFi0ydpIr4NDyayuoDqXKU7/Z8V e2xkW4nrRl8rDaty8kjhITHhowbx0zE+yh73Io4JsC0RU54bNK6DZZdqyOXOoh5TM48TGxlu CI3x7MatJO7YiQEx4gqygDRZvGBboOG4QrjWf6PLTtkgH9pYrGyihao/US91OHxVdO43EtJo yZblNTHq24A1xjO6sicVvty4F2h1yuO1wHS9O5JOVw4mKzGIJA72LEwjIAcsUHbEy/2hkr2i KiWe10h+uey6uTnZqzqp5+SNoNpkw3+PLkil8+hDegiPQgOWG+b+eu41LL950H2XLJKjvgun qnYtpDVO9gbq7anDwNJ1osv8RWyAje83NgFg3UKL0hJdA+EgoT3I13OJer3Dfa7g1Siijdrw PXGM6XiAprRL3jDiq3ufLZ+5kNHxwozyMpQ55NQCr0bPP3zXUrxuMTeDhAiKwO02froCM1h1 oMCXmKCGrKVPLvIsVCU/uIvP/WMZIgNtTnhLPgl/ufigmM9mV8AZqakxoAXaXC9HvR+OUqVe 3vsgtEbEWcLpAUyVuLqiEfRGQJUMn21Ruc34iwxIIOgF4bKAI6305Kb2yLuP5RMYXtCA07EO 37yfoODRb9YaymTOMZwwhQLULGgT8kq0hT451yy8KZuMueBon5QjpnkztUgv4U79Dk3/D1wV IGG1n2VCnpzhiUOTiM326Z2pQp8zE2C2O52ma8QDsRdstVOVApyLpvA16piEdmnWQnAZN6YG H6pR9ynBXc6Sddii8QWbRNFEs65xgvGwzLsBrYUk7KRA5lh8andxXHgd+5yzn/H0O8qiFx1C tBXOziAgahyvxPWG5aPk0idkPOycr8A2SfW6GqZ5W+HvUUdQREpFKucDSpZaUzRotD0oEjFS tdCEJwBNQ1MgY6HI6pOMZjyiEleAezkIJLYan6wnGG5AVCJwKmNZczkYTdV2iKVE0UCnw0Jm BTOfQEjGiespX7fBz1yBBruZU3r6+x3tHK8SAc90QiLa0Rr07f99AQSgLSQTPYa37RMvylEy X08H128xdvHW/KPogNgeONXZtZ8qFZL2GTFthBsa4S6JvMqjVoffgJr+kL2gk8vW8MQzI5z9 iNslVooesf6mBtbejiV3I79IOjSI2j2p1W0brLOn0rZyJCQ87sO7/IxrxPiuhuoHwws6SYCs ZEd3n2C65HNFAdXX4j2VxN99BN7vbjLMgEy4orV0TtnNqz+4Vqgk5o5QfAozBqtZYIVM6iFD gbjQ+UVAsGvLKohnF3jPVoUeetV8qAzJcavcfCLjbWqMOhXlzWjlW1b4Yp53ypg7gJEQ/XTl 9YAyvCchU6cUivkyUymqobxkJxFYjcbGiy+zzLlDchffP86cYEOAGaoa8q5o7c2z53mWmRR5 Q6LCFYP2cvvch2XJ1Dwxgxf000LrGfvw3PpiWwp1Whz/uzGjHaGyv+qbBcdP29XWGRu6DWka ZO5idwXRgngbgQkkgek+VevwqFaoKplKGyACUxMfiXwMyRjSv7q7uvEM5MJscl493wHCrfZA xjSULP2rhoE3jm2GmJfwGt+bDS2otDimAQ8jmuBLXF1pX6feMdqxB6Z6saPIJwZljcAWiR8j iHaQ1amONz8t9aflo3Ko7CWWGeoV5kVei7uh9Dl1mPz9ShxDBuzkurm0N7sEBIzwH/T2NxjV CGOpxH5KNqjx+GxNuRpeVNtDVn35p9hG41wpYA3gYkZxXkQgpjGmBhP2Xe2K9hQ3rjyKWYcX TNeicCA+xDrgQcwZmLM3Y/yUW+Rh9dsd8XvKH1DwToztqUoQO+V9OAWxnYz+wvg61iNPr4l2 W1Bgfo2tCxE36dT41Frl3vFROhVRBgQPDSwxUrWqYnm9uMPIj7oK+DVtgI2nMj9Xu/c5FsAC TCpItF6WnUopsRnbACTijuqtse9KYOWNZVK5lWVi0uS0LQTcchs0KJM3W0+Zwef9TUk07Jp1 EQ+m8jl487XbT0qpvvxAwYEZGSqPIVKq22r1eAG2Z/Il4G3Qsc7QmRNDMauFKj4VmpV7KuCV U7GESVg+C3CR/yCTUnGuR0g9zWWQtiqLy3FfiBHi485FV/GfgoHx1lFFCMzmppzfuyz7Ormd koxpjUY51qj7wBJ1votLB7nFGHWuAavbD4wDpmZNhtfqA9YtQ/TNoSF4+R/Ejs9nNXppRGRK mGdewVDDH0YEk2CCVf5O7Cy5N7Gu+GGD+u6JvHKbP2As+tbH/uPwJuu1MNh8VPufo2XOWJ+C vQgxkdZdXVwGsCciipWDiJOx3iLYMmcqxOxvCZwq4H38fjmXh7u+ZraC7ZWNoYKmVj+iqOCO uiMwSdhfGwAh9VcmDmRkuhZhQ5I2EQMP3G3HL8NtDDAVvfVk65TVFsAbj9rcdBP9+Q61xVMP sjSjpX00KR5h7g7EQQgNxSpl8e3aMgNO2z4OknAARPBN7+HPzTak+n4ZKq9Tftbi+Ae5HjS8 X6LVlTuODiOjWyjTxe0LeRFlz2WJjRbsYC5NwdyUC3tFYK8LBK8N9BzgHs9xrh+1RaofSYMd DN7dU1KtLiZ6yhV1+5+F2J25X1gNeCYmiyd4oEwy74TuPpvRzVrzqdUuSRgjbRS6y5ASbp+n y6A9raGRnmpl+COznxsVx8c8l6ja6qEuExjPePS8ZwSAB75
  • Ironport-sdr: 66ade0bb_TeIskRfkuKv5HQgG/r3BMw0ZKMS1AVsfrZpr2Vr0rC5+Qih 2/lXS6Bp23a64TEmqzxx1I8ixHIwwk5v0IUwzCw==

In coq, subsets are defined as sigma types which are implemented as inducive types without adding extra 4 derivation rules

In type theory textbook (by Rob Nederpelt, chapter 13), subsets are defined as predicates. Rob argues the disadvantaes of sigma types as adding extra rules and overcomplicating the kernel with 4 rules OR inductive types (page 300), but told nothing about their advantages

What are the advantages of sigma types over predicates? 

The info is very scarce on this topic, I was unable to find any info in either software foundations or Adam Chapala book. Only the definition of them in Coq.Init.Specif



Archive powered by MHonArc 2.6.19+.

Top of Page