Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Why subtyping rule is not contravariant in input types for Pi

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Why subtyping rule is not contravariant in input types for Pi


Chronological Thread 
  • From: Jason Hu <fdhzs2010 AT hotmail.com>
  • To: Coq Club <coq-club AT inria.fr>
  • Subject: [Coq-Club] Why subtyping rule is not contravariant in input types for Pi
  • Date: Thu, 20 Jun 2024 15:11:47 +0000
  • Accept-language: en-US, en-CA
  • Arc-authentication-results: i=1; mx.microsoft.com 1; spf=none; dmarc=none; dkim=none; arc=none
  • Arc-message-signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=microsoft.com; s=arcselector9901; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-AntiSpam-MessageData-ChunkCount:X-MS-Exchange-AntiSpam-MessageData-0:X-MS-Exchange-AntiSpam-MessageData-1; bh=/ad960Eyc6TOwbBxAhBmM3ncaYDqYnGGtDb6s90dqHM=; b=B+HXOSIH/chLyyt3mzBzvD8qkymzVQ64XioRPVwNOSLOEf8UykNFZ45ujNNArMlTFsYwMvuo9swZZcmwvHXDgArD2YZ6/tX9P64CFJUMIMl73XUhDEpXISYhHpBviyA/unVFx6Nl9Dlmcxvpb/de+tjy/VcoO6Ztd6UNxW1hTPILKOll9WrLZsFQcJqMI1e9XuMIM41lhwL6U15JDMwvwbK/TG3AZlLRCr1h3HyW+3k3t5QUCba1mJgfSuXqvNJ//SVcBo05JjoN0WhdNQl2tjzhPvdHhqRvCkeZxa2Dgn9elYuxVLTgLWDqke5x7Og+WuEf+mXCupJsLcGQoJEiMw==
  • Arc-seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=na5svm14JTptG9CoYlfGnsnXAMt7CDHGbf9vTgSSxJ/zfkZUFKru8u0Z2gxtP2C06NeGnb7Qlx7rsX5Sk99zHfAS2wdPZ8a/alD+MwLNwxMqSh2ixv5DTX9Xq1uBQYiZr7AV9OgYasjS/g88H5auLsgOGECmiSxpVKCOvTPYTiFqr/SdiHUWdecKxgwaYX1UB/B3AfHnefxw5x+4l8pIcHyTk8ShO/YNxVyPIoIgHAlwQrVSV7GH8wA98sR1T3ctTL4lIEpGbNRx3nfaVMGFs44mUhhSG7ZW84sGCLe24mP160HGH0jIX+iqbFh3LDwEgSijzgz40PyVhr/2WgNHvw==
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=fdhzs2010 AT hotmail.com; spf=Pass smtp.mailfrom=fdhzs2010 AT hotmail.com; spf=Pass smtp.helo=postmaster AT NAM04-BN8-obe.outbound.protection.outlook.com
  • Ironport-data: A9a23:2tE3C63KaHljdwciFvbD5fl6kn2cJEfYwER7XKvMYLTBsI5bpzNWz GUdDW6CO//bYDDze4t1aYi+oRwAscODyYBrQQdo3Hw8FHgiRejtVY3IdB+oV8+xBpSeFxw/t 512hv3odp1coqr0/0/1WlTZhSAgk/vOHNIQMcacUghpXwhoVSw9vhxqnu89k+ZAjMOwa++3k YqaT/b3Zhn9i1aYDkpOs/jf8E015Kyr0N8llgVWic5j7Ae2e0Y9V8p3yZGZdxPQXoRSF+imc OfPpJnRErTxon/Bovv8+lrKWhViroz6ZWBiuVIKM0SWuSWukwRpukoN2FXwXm8M49mBt4gZJ NygLvVcQy9xVkHHsLx1vxW1j0iSlECJkVPKCSHXjCCd86HJW3XvhNpcVkEIBq033/pZMzFgs vI2axlYO3hvh8ruqF66Ys9Fo5x/aePNbMYYsHwmyizFB/E7R5yFW7/N+dJTwDY3gIZJAOraY M0aLzFoaXwsYTUTYhFGUtRiw6H12RETcBUAwL6RjaQ743rIllQoiJDtN8bQc92OA85Smy50o 0qfoD2nU0BEaof3JTyt7G6RiL/dhAXCWdw3DJ678q5sqUC5yTlGYPERfQDg+6Xm4qKkYPpUL FVR8S4zp4Ap5UmzR5/8WQe5qTiKpHYht8F4FuQ77ESHzPrS6gPBWm8ATTgbMIF58sgrWTYty 1mF2cvzAiBiu6GUTnTb8aqIqTS1Om4eKmpqiTI4oRUt7dqkj7Npjiz0bvlGDICH3vOyFx+z6 mXfxMQhvIk7gckO3qS92FnIhTOwu5TEJjLZAC2HDwpJCSspNeaYi5yU1LTN0RpXwG+korSpu XEFn42U6rAIBJTVyCuJQ+NXROz2ofGYLDfbnFhjWYE78Cig8GKieoYW5yxiIEBuMYAPfjqBj K7vVeF5u8c70JiCNPUfj2eN5yICkfKI+TPNCqm8Uza2SsItHDJrBQk3DaJq40jjkVI3jYY0M oqBfMCnAB4yUPs+nGrsHrdCi+Fyl0jSIF8/o7irnnxLNpLONRaopUstbQPQNojVEYvY/lqJq IYHZ6NmNT0DD7KmOXW/HXEvwaAidiNhWc+eRz1/c++IOA19H289Q/TW26tJRmCWt/U9qws8x VnkAhUw4AOn2xXvcFzWAlg9Mu+Hdcgk9xoTY3dzVWtELlB4PO5DGo9EK8BoFVTmncQ/pcNJo w4tIZnbW6kSF2SZo1zwr/DV9eRfSfhivirWVwLNXdT1V8cIq9Xho4e5Llnc52MVAzCptMAzh bSl20mJCdAAXgluRoKeIv6m01r77zBXlfNQTnn4BIBZWHzt14x2dA33rPs8eP8XJTv5mzC16 gexADUjn9frnbMbytfzuP27n9+bKNcmRkt+NEvH3ImyLhjfrzaCw5cfceOmfgL9dWLT+Yelb 75v08DDNOYjmXBUubFdCJdu97o1vPH0lo9ZzyNlPXTFVEuqAbVeOUu73dFDm6lO571Bsy20U VKr1vgDHp6WKubJLUU0JgE0Xt+c1PoRpCbe3c41LGr++iVz2riNCmdWADWhlw1fK6lTIqo+4 OJ8pvMT1ROzuiAqPvmCkCpQ0WaGdV4Ecqc/s6AlEJ3ZsRUqxn5CcK7jJHfPur/XUOp1M24uP jOwr4jBje4FxkP9LlwCJUKU1u9Z3ZkzqBRGyWEZHGuwm/3Hu+QW2SNA+jFmXyVXyRR6i9hIA FZJDHEsB6uy/GZPvvNhDkSMAABKASOL9nPhk2UpkHLrdGj2d2jvAlBkB8Oz0hE4yV9MRhla4 7CS90j9WxnIYsza/3U/SGxlmdPZXP1z8Qz+m+6BOui8A6A5PWbBvf6vV1FVtRfXO8I733Pal 8I34+11OPXJCghIqpJqFq2fhO0cZwCaLjZZXMA7rb8oHH7dSh62yzOhO0C8QeITBv3ooGuTK d1iGdJLbDu6jB2xlzE8AbUdBYN7h9s7zYMmVpK3AH8Z6Z2NgyFMspmNxhPhhWQufcpiofw9J qzVaTiGNG6a3llQpEPgs+hGPXiec/AfRQihwt2wzvoFJ6gDvM5ob0s29Lm+5FeREQl/+iOrr BHxXLDXw8Ni2LZTsdPVSIsbPDqNKPT3SOis2yKwuY4XbdrwbOH/hzlMoVzjZwlrLb8dXupsr ou0sfn14VjkuYgnWGWIiriDEKh0vf+JZtR1Cf6uDndmnnqlYvTOsj8j4GGzLKJbnOxNvveHQ xSKU+ruVNo3deoE+lhrRXl/KTg/BZ7zTJ/cngKmjvHVChEiwQ3Nd9ym0nnybFBkTCwDOrygK wr0pfqBv9BRk5tRNUVVG9BnHJ5KD1vxUoQ2d9DKlGe5D0v5pnigq7fdhR4bxjWTMUa9EeH++ sjjVDXlURaP5IXk6c5/iJNjmA81AFJWo/gCTmhE9/FY0zmFXXM7d8IDOpA4O7Rouy3V1rSjQ RrSbWEnWB7PbR4dfTrSuN3cDxqiXMoQMdLEJxsszUOeSwGyIKiiWLJB1CNR001aSwvZ7tOMC I8hoyXrHx2L3JtWa/4Z5aW7jcdZ1/rq/C801n6nofPiISQ1IOss72NgLjpvRCacMsDqlWf3H 0YXa11AYnmGTR/WLZ49VV9TQR0XhWa6hXFgJyKC283WtIin3fVNgq+3cf361roYKt8GPvgST HfwXHGA+H2SxmdVg6YyptY1muVhPJpnxCRhwHPLGWX+Xp1c61jL++sktA9XEIQI3l4aFFnQ0 D6x/3I5GUKJblhL36GbwhkI/JQ3VW8QCzbOj0j0ojqufdkR0Y3CYxbzpO7kAciYlkQhlxwwr PQugIK5o1qKsTLloX91sfFzSpmvH5QKDXedOsw3Zsqar/pvIVOx0Jhh1F0/3tNVtnZDw+24s UpXP8oVoOqaY89E4+wocBr1rFSqQ3ft1znvU4PUwS8=
  • Ironport-hdrordr: A9a23:5BnYh6GJvyNi2e7fpLqFN5HXdLJyesId70hD6qkvc3Fom52j/f xGws5x6fatskd2ZJhSo6H4BEDgewKpyXcR2+Us1NiZLW3bUQeTTb2KjrGStAEIeReOkdK1vJ 0IG8cRNDSaNykYsS+O2njcLz9W+qjkzEnHv4fj5kYoaTsvR7Br7g9/BAreOFZxXhN6CZ0wE4 fZztZbphK7EE5nJ/iTNz0gZazuttfLnJXpbVotHBg88jSDijuu9frTDwWY5BEDSDlCqI1SuV Qt0jaJrJlK/pmAu1ThPl3onthrcejau5R+7fm3+4Uowm2FsHfnWG0uYczCgNl/mpDW1L9jqq i2n/5nBbUE15vcE1vF2ycF9jOQoArG0UWSumOwkD/mu4j0VTg6A81OicZQdQbY8VMpuJV53L hQ12yUupJLBVeY9R6NkuTgRlVvjA65sHAimekcgzhWVpYfcqZYqcga8FlOGJkNESrm4MQsEf VoDsvb+PFKGGnqHUwwlQFUsaGRt1gIb2a7qxI5y7OoOhBt7Q5EJ2tx/r1ioks9
  • Ironport-phdr: A9a23:tQxFQRRQKvlwWiH7oPrrvPSLAtpsohqXAWYlg6HPa5pwe6iut67vI FbYra00ygOTDMOAsKgP27aempujcFJDyK7CikxKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxB sVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSizexf7d/I A+4oAjfqMUajohvJ6kswRbVv3VEfPhbymxvKV+PhRjw4du+8oB++CpKofIh8MBAUaT+f6smS LFTESorPWMo6sD1rBfPVQSA6GcSXWUQiRpIHhPK7ArmUZfrsyv1rfRy1S+HNsDrV780WDCi7 6B2SB/0jSoMKjA0/H3LhsF2kalWuwyqqQBhzIHIYYGVLPt+cb3bfdMGXmpKQ8JdWzVcDo+gc 4cDCuwMMuFFoYngvFsOtQWxChWwBO3hzT9Ig2X53aw80+88FQ3L0wgtE9cIvX/Jrtv6Kb0SX Pi1wqfW0DvDc/1Y1zTh54fHaR0uu+2AUa5qfMbN1UUjCgXIhUiQp4z/ODOV0/wAvWyB4Op7U uKvjXMspQNsojOywcoshJTGhoIUy1Df6yl13Js5KcGjRU57Zt6kDJ5QuDubN4tyWM8tX2Zou CMjx7AApJW0czQExo49yB7Dd/yIbZKI4hT7WeuRJTp1i3JrdbC7ihus/kWt1/PxW8up3FtWs idLksfAu3EQ2hHN6cWKSuVx80m81TuByw3e5eVJLF06m6TVNpMsxKM7mJQUsUTGBCD2mUP2g beXdkUi4Oio6v7obq/opp+GL4N0hQD+MrgumsyiGus0KAkOX2+d9O+h17Pj5VX0TbpWgvEsl qTVrorWKMsZq6KjAwJY0J4v5wi+Aju63tkVmGQLIE5edx+GioXkO0zCLOz9APuijFmjjDJmy vXEM7DnH57AMHzDkKr6fbZh9UFc0hc9zdFe5p1KErwNPPT+UVLrutPCFB82KQm0zv7nCNpj0 oMeXnqCDLeFPa3VrVOF6fsjLvSUaoIWoTr9LOMq6OD0gX8+hF8dYbKm3ZwKaHC+A/tqOV2ZY WDrgtcdD2gFohY+TO3tiF2ESzJTYGuyX7445jE8D4KmDp3PSZyqgLyExCu7H5tWaX5aCl2UH nrka5+IVvMSZC6ILcJskCYIWLijRoM50BGhrg76y75pLurO/S0YsIru1NZo6O3TlBAy7iJ4A 9iA322RVGx0nmQIRyMz3K9loEx9zk2P3rR/g/xdDdBT4ehGXR8gNZHA1+x6F8zyWgXZc9uUU FqmWMmpASktTtItxN8De1pyG9K7jhzawyWqB6IVmKeQCZwv8qPc2mDxKNxnx3bH0qkhlVgmT dFVOW2onK4svzTUUqXOig2yk7ugPfAX2zeI/2Oex0KPultZWUh+S/OWc2oYYx70pM/+4AviU vf6B7gnIBAbkZfaAqtNdtjgjFEAT/DmboeNK1mtknu9UE7bjoiHa5DnLiBAhU01aWABmgEXp zOdMBQmQz2mqCTYBSBvElTmZwXt9/N/oTW1VBx81BmEOmtm0bf94RsJnbqEUfpG0L4Eqjx78 2wsNFa6w9ffCt7GrA1kL+1Hed1o2F5czirCshBleJmpLqRsnFkbJgp7v1H1jU0uUq1AltQvp XIuigF1LPHQy0tPIguRxou4IbjLMi/y8RSoPrbRwU3b2c2K970nzt0d8wmmlif5U00o/jNgz sVf1Gaa6tPSFg0OXJntU0ExsR9nu7XdZSp77ITRvZF1GY+ztDKKm9cgBe9/jw2lY88aKqSPU gn7D8wdAcGqbu0sgVmgKBwebqhU8+YvMsWqeuHjuubjNft8nD+gkWVM4ZxsmkOK+S1mT+fU3 pEDi/iG1wqDXj34gR+vqMfy0YxDYDgTGCK4x02GTMZfaq1gZtxTUD+GI8qrw9x/g9jmXHsZv F+vClUa2dO4LAKIZg+11glR2EIL5H2/zHfgiW0u1W126PfAj0msi6z4eREKO3BGXjxnhFboe 82viswCGVKvZE4vnQek4kDzw+5aor5+Ji/dWxQtHWC+Imd8X6+3rrfHbdRI7cZivylXQv/mO QnCYr76vx4T0ielFGxbjmNeFXniqtDikhp2hXjIZnh/rGjCI5kpnT/f48DZTP9VmDEBQWMr7 FufTkj5NN6v89KOkp7Fue3rTGOtWKpYdizzxJ+Bvi+2jYFzKSW2hOv72tjuEAxglDT+y8EvT yLD6hD1fojs0a2+d+NhZEhhQlHmuYJ2HYR3k414g591uzBSiJmV72FdyT6rGdVcxaf3bX5LT jkOi9LY+wnq3kR/I2nBm9q/By/bnpQnOobya3hewi8n6sFWFKqYid4M1TB4pFa1t0OZYPRwm Csc1ep77Xcbh+8Tvw9+hi6ZA70UAQxZJXmwz1LZtZbi8+MKOzXKE/D4zkd1kNG/AavXpwhdX Cy8YZI+BWpq6c45NlvQ0Xr144Wied/KbNtVuAfH9nWIx+VTNp81keIHwCR9Pmeo93Mpy/wg1 0Q3hbm6u5SCImRpuqm+B1QLU1+9L9NW4TzrgatEy4yY04C9Bc85Q20jXJz0SPupFHQZsvGtZ GPsWHUs73ycH7TYBwqW7kxr+mnOH56cPHaSPHAFzN9mSUrVNAlFjQsTRjl/go8hG1Xg2pn6a EkgrGN0hBawul5Wx+lvLRW6TmrPuFLidGIvUJbGZBtOslMfvQGMaZfYtqQrWHgHtpy58F7Uc jDdO1sOVSdRHRXbYjKrdri2uYucq67JXKzmaaOJOOvGqPQCBa7QmdTzjc08p3DUcZ/Udnh6U 69ighYFAS8/QpyJ3W1IEXdy9WqFbtbH9k7kpmsr8YbgrbKzH1izrYqXV+kLaYkpp0/w3PzFa rbX3noxKC4GhMkFnSaakeFGjlBO03k8JX7xQdFi/WbMVPyCwKYPVkxCMnohOpcQtPBumVUcc c/D1IGv3+Yh3KdsUgVLCQS6yJHxPZRYcSbgbDalTA6KLOrUfzSTmpOuOPruR+EI17df70Xo6 2TcTharPyzdxWPgD0n9aLgV3i/HZEcMttnlKkQ/TjW5BJfvbhnxWDNupQU/2qZ8xnbDNGpGd CN5b1sItLqbqyVRnvR4HWVFqHtjN+iN3SiDvaHULZMfsP0jBSoR9aoS+HMh175c9z1JXtRTs Q6K8ptEhQHjleOCjD16TBBJtzBHwpqRullvMrnY8Z8GXmvY+BUK7iObDBFvxZMtBtD0uq9Ww 8TCj+qvcHETqZSIoo1BWIDdM4qfPWAkMAb1FTKcFwYDQTOxdCnei0FbjPCO5yiVo5w9+f2O0 NIFTr5WUkBwF+tPVhwjTYZEfMgxA2x39NzTxNQF7ne/shTLEcBTv5SdE+mXHe2qMjGSy79Ne xoPx7r8a4UVLIzynUJ4OTwY1MzHHVTdWddVr2hvdAgx9Q9D/HhsVTdrghrNagSx5XYSEbi/m Rt82W4cKaw9sSzh5Vs6PA+AvCwrjEw4gsnomxi3WRupcOKae9ETDCD58U8sLpn8XgB5KxWom lBpPyvFQLQXiKZ8cWdsi0nXvp4FSps+BeVUJRQXw/+QffAh119R/z6myUFw7uzAEZJ+lQEuf M3kvzda1glkdtJwOb3IKf8D0A1LnqzX9HzNtKh50EoEKk0K6m/XZCMYpBlCKOw9PyTxtu10t V7ew30SIi5UEaJt+68i91thabjYiXu4jPgbbBj2brL6TevRunCcx5PSBApojgVQ0RECpOQ+0 N9/IRPMCwZzk/3JUUxObJWKKBkLPZBbrCGBJH/X4+uRmconbcLhRoWKBaePrPhG2Ev8RVRwR t1e4JhZRcv+lx2JZcb/cuxfwE10tl2yfQeLUKwSKkLTyG9V8YbilfoVlcFcPm9PW2wlaHfuv ++FqFNy26iIBI9uMCVdA9JMN2poCpezw3cL5i0ZXjfrirlLxlDat22u4XmKRHz1a94pDB91T TVFLYnqvB8Zo+2xg1OR9YjCLWbnM9gkosXI9e4Ru5eADbVTUKV5tEDf3YJfQi7zO4YqOd6yO 535ao1qZtvxWC7SurOXizUpSs7wOJCmKa3a2GnV
  • Ironport-sdr: 667446ba_huX0jM9Pc7Udss7G2MYbkIDTxqPY5Jiot3jyMuchJGE1vPz XrW3XawfPXDWYKec6fffzbbtgSUBwBasEc3za6w==
  • Msip_labels:

Hi all,

I am reading the subtyping rules for Coq: https://coq.inria.fr/doc/V8.18.0/refman/language/cic.html#subtyping-rules

Rule 5 says that Coq only checks equivalence for the input types while only the output types are subject to subtyping. How is the subtyping rule is not contravariant in the input types?

I understand that in System F, this rule is problematic and causes undecidability but I don't think it applies here. In particular, if for the sake of discussion we let U <: T and compare x : U |- T' <: U', this extra information of x : U should affect the result of comparing T' <: U' at all. How is the rule designed in this way? What consideration am I missing here?

Thanks,
Jason Hu
https://hustmphrrr.github.io/



Archive powered by MHonArc 2.6.19+.

Top of Page