coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Nikhil Swamy <nswamy AT microsoft.com>
- To: "coq-club AT inria.fr" <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] Nested positivity
- Date: Wed, 8 Feb 2023 17:06:27 +0000
- Accept-language: en-US
- Arc-authentication-results: i=1; mx.microsoft.com 1; spf=pass smtp.mailfrom=microsoft.com; dmarc=pass action=none header.from=microsoft.com; dkim=pass header.d=microsoft.com; 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=DF7OyyvKq+tnPRkkbkPuf3mK+Q4gmnMpU13/MWjGsl4=; b=Fc5Yo6SqUUQIOUp5BPad69N2Z2bBj3jtFVUXaYaZu/19IYnHE/MSe867rGG8OYUjIHR8NA36qgHVJAy9lX/gCDo0ojdnEPyPP1mEHbSWvWC278Ll9mlOL7ULIrgz9sxJ+uAZOyVYXhpajQ4gkhWBT53a70vZssKCv0W83luiXaAYOdsrinrHdpGipKwU9E70rlPJLxOD8NxAdX/NvLVnbRdax9koOM1xwVD7qFKQGxNdOBXarNhdrKwUlQ2mNrI4mK9Gc9YOc8OlUVHCGrRHcKGp4E/74uwNvrvdWBdo/wT2LzZ5wuM9lOYH8Ptfat7/SnUvKmFBhOpRF5TbxUYkTg==
- Arc-seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=KoPHBssKPU+EKI3k7+g4PBWrUuWAAc2g+v/E1L6nl9i49kaFuSjLEwWLvh74IM0KIAtiv7cyAkPdN45MRa9QtIyDFq7Vk8C3+45RdlOJqB0KeKUXBnEBsjyI6z2CVzDx80W7kIU4vac+nJzT0/JpRn2FJJng0J4N6OdU+aOMhmmnQVfKeVTE1CqXnlWiSiG7BhGgHt0xJnO4WvX+nmablyxud4JmxuQ0/IW+d+8G+HbziunQdchfJuikRFaHQ9uMRSHHQfYBBkx56r7N5cDV7fxaue9kYG4Qo1WYmehBDsM+cDWK+e9EPSxjB8Sl5tSc8DM10WUWncYrxCq+Eti1UA==
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=nswamy AT microsoft.com; spf=Pass smtp.mailfrom=nswamy AT microsoft.com; spf=Pass smtp.helo=postmaster AT BN3PR00CU001-vft-obe.outbound.protection.outlook.com
- Ironport-data: A9a23:5YvNTq5TI42m7fmT4gKIMQxRtDfMchMFZxGqfqrLsTDasY5as4F+v mIcXDqFa/fZa2H0L9kkO4ix9k0Av8fRy9RjHgVs/igyZn8b8sCt6faxfh6hZXvKRiHgZBs6t JtGMoGowOQcFCK0SsKFa+C5xZVE/fjUAOC6UYYoAwgpLSd8UiAtlBl/rOAwh49skLCRDhiE0 T/Ii5S31GSNhnglbQr414rZ8Ek05K6q6GtC1rADTakjUGH2xyF94K03fvnZw0vQGuF8AuO8T uDf+7C1lkuxE8AFV7tJOp6iGqE7aua60Tqm0hK6aID+6vR2nRHe545gXBYqhei7vB3S9zx54 I0lWZVd0m7FNIWU8AgWe0Ew/y2TocSqUVIISJSymZX78qHIT5fj6/ZAB2o6G9Qnw6V6I2AU9 uUIKjRWXCnW0opawJrjIgVtru4Fd/HRZNs0hyk4lHTHA+pjRprOBaLX+dVfwTE8wNhUGurTb NYYbjwpawncZxpIOREcD5dWcOWA2yO5KmUB7g/L4/Nri4TQ5FQZPLzFNsHKc9mbbcBUlVyfv WXI4yLyBRRy2Nm3lWXfqCP91rKncSXTeZAbEbGb99BQi2KimjZQIQcbCQGjvqzs4qK5c4kGc BdMo3BGQbIJ3EesV5z2WwCyiGWVuwYVHdtWCewzrg+Xopc4+C6cD2kACzNIc8A7r5U/Vzssj wbRxYuxXGApt6CJQ3WA8LvStSm1JSUeMW4FY2kDUBcB5N7g5oo0i3ojU+qPDoa2oNbeFRep/ AnJoQo/3bYKncwPjJeCqAWvby2XmrDFSQs85wPyV22j7x9kaIPNW7FE+WQ3/t4bctjEFQXpU Gws3pfOt79TVflhgQTXGI0w8KeVC+Fp2dE2qXRoDpU98DLFF5WLJ9sBuW4WyKuEza85ldLBZ UbSvUZc7YRPIWDwZL1wZdvoU55ylfG8U9P4SvrTc9xCJIBrcxOK9z1vYkjW2H3xlE8rkuc0P pLznSeQ4ZQyVfQPINmeHb11PVoXKsYWnjK7qXfTlE/P7FZmTCTJIYrpymemYOEj97+jqw7I6 dtZPMbi40wBD7ChM3WJq99CdQ5iwZ0H6Xbe+50/mgmrclsOJY3dI6WIqV/cU9A7z/QMy7+Tl p1DchYGkwCi2RUr1jlmmlg4Mei0Bc8lxZ7KFSktNkyvwH8tfc6m/roFevMKkUoPpYReIQpPZ 6BdIa2oW6wRIhyeomh1RcSj8ORKKUr67SrQZXbNSGZkJfZIGVeWkuIIiyO0qUEmFDSsj8Iir tWIj0WDKXb1b18+V5m+hTPG5w/ZgEXxb8orDhCWfoEMJhWEHUoDA3WZs8Lb6vokcX3rrgZ2H S7PafvBjbiW890G45PSiLqaroykNeJ7EwAIVyPY9Lu6f22StGaq3YYKAq7CcCH/RVHE3vyoR dxU6PXgb9wBvlJB6LRnH5hRkKkR2trIpp1h9DpCIknlVVqQJ41FHminxuhK761E+a9Ys1C5W 2WJ4dhrBo+KM8LETn8SBi0AN8648N0+tgfuxOsQGxyg1ilO4LDdc0F2OkjVhAN/MrdKbYABx 80wspUs7z3ksAIgaIqbhHtqr26jf2IJQvglvMtCAavAqAki+ndda7PyVw7055CubY1XE08Ie zW7uovLt45+9GHjLUUhMGfr5vVMo6gBozVIxwImC3XVv4Odnd4x/hla0QpvfzRv1h8djt5CY Dl6BXN6NYCl3mlNlsNce0uOBgsYJhmS2nKp+mszjGeDEnWZDD3cHlYcZ9SI0lsSqV9HXz5h+ 7qd9mbpfBDqcOz13QowQURVkOPif/Mg6jz9nN2bIOrdE6kYeTbFhoqcVVgMoTbjAuIzgxTJn vk13eBSbaagCzUcjZdmAKan1JMRaiu+Gkp8fd9b8pk0QF7sIAOJ5WDWKmSaWN98GPjRwErpV +1sPp1uUjq95gavrxcaJ7IFHJlllqUP+ugEQ67afz8akrqArwhGtIDb2Tj+iVQKHfRvs5cZA aHAew2SFle/gSNvpFbMi81fK0yEYdUgTy/t7tCfqekmOcoKj7BxTBsUzLCxgUSwDCJm2BCl5 CX4eK7cyr1Z+7RGxofDPP1KOFSpFInVSu+NzQGUtuZOZ/PpNePllVscinvjDjRsEYohYfZFv pXTj4evx2LAhqg8bE7BkZrYF6Vp29S7bNAKDu3JdktljQmwc+6yxStb4G2pC417oPUE7Omde gaIQs+Rd9kUZtRj+ENoexVuSxYwNqCmQZrj9AWcruuNACczyQboDs2q3l63YHB5dh0nAYzfC Aj1scmq5Ntd/ZZGXi1cI/RAHZVDAUTCXJE+fIbbrgioDWiPg3KDtID9lBEm1yr5N3mcHOv+4 rPHXhLbdinuiJrXzdpcjZN+jicXAFl5n+M0WEAXoPxytByXE08EKr47HagdK5QJjBH36o70V AvNYEQmFy/5ezZOKjf4wdb7WzagFv48Acj4KhMp7nGrRX+PXq3YO4RY9wBk/3tSURngxrv+K dghp1vBDiLoyZRtHesu9vi3hNl8/czjx1UKxxHNo5SnSVJWS7AHz2doEwdxRDTKWZOF3lnCI W8uA3tIWgenQEr2CtxtYGNRBApfhj700jE0dm2a9b4zYWlAIDFok5UT+t0f04HvqOwgAuU2f yuvbFbVuznTxHIP/KwjtpQunLN+Du+NEo6iNqj/SAYOnqa2rGM6I8cFmilJR8YnkOKaO02Ij SGiuhDSG2zcQH29GpXPoenKx361encNBCvOlwnxuXnNlhlRIx3xZU2x1AyiQX3vg/GLgqibK Qv+qG6UolaMsyDjqyU4vfMezrBC7Qf9ClGcOh0VoljOfttAhYOT+H2NE6336j6JzEB5+w==
- Ironport-hdrordr: A9a23:Axrt76gaj2Mh7jv5ZA9P7mf0fHBQX1B13DAbv31ZSRFFG/FwyP rCoB1L73XJYWgqM03IwerwQJVoMkmsjqKdgLNhdYtKOTOLhILGFvAH0WKP+Vzd8mjFh5dgPM RbAuND4b/LfD9HZK/BiWHWferIguP3lpxA7t2urEuFODsaDp2ImD0JaDpzfHcXeCB2Qb4CUL aM7MtOoDStPV4NaN6gO3UDV+/f4/XWiZPPe3c9dlMawTjLqQntxK/xEhCe0BtbeShI260e/W /MlBG8zrm/ssu81gTX2wbonthrcZrau5R+7f63+4kowwbX+0aVjUNaKv6/VQUO0a+SAZAR4Z vxSlkbToFOAjjqDxuISFPWqnTdOXAVmjXfIBaj8ATeScCVfkNHN+NRwY1eaRfX8EwmoZV117 9KxXuQs95NAQrHhzmV3am+a/hGrDvAnZMZq59ms1VPFY8FLLNBp40W+01YVJ8GASLh8YgiVO 1jFtvV6vpaeU6TKymxhBgn/PW8GnAoWhuWSEkLvcKYlzBQgXBi1kMdgMgShG0J+p4xQ4RNo+ 7ELqNrnrdTSdJ+V9MKOM4RBc+sTmDdSxPFN2yfZVzhCaEcInrI74X65b0kjdvaCqDgDKFC66 gpfGkoxVLaIXied/Fm9Kc7gyzwfA==
- Ironport-phdr: A9a23:mbixYBOTOdMpNRP9zq8l6nbeBRdPi9zP1u491JMrhvp0f7i5+Ny6Z QqDv6gr1QKQFt6Bo9t/yMPo8InYEVQa5piAtH1QOLdtbDQizfssogo7HcSeAlf6JvO5JwYzH cBFSUM3tyrjaRsdF8nxfUDdrWOv5jAOBBr/KRB1JuPoEYLOksi7ze+/94PTbglSmTawYa5+I Bq4oAnPq8IbnZZsJqEtxxTGpXdFZ/5Yzn5yK1KJmBb86Maw/Jp9/ClVpvks6c1OX7jkcqohV bBXAygoPG4z5M3wqBnMVhCP6WcGUmUXiRVHHQ7I5wznU5jrsyv6su192DSGPcDzULs5Vyiu4 7ttRRT1jioMKjw3/3zNisFojKxVvg+vpwBxzYDXboGaNuZxcazGcNwAWWZNQtxcWzBdDo+ha YYEEuoPPfxfr4n4v1YAtRq+BQqsBOPuzj9Dm2L43KMg3OQkEQDNwQstH9QVsHXattr1MacTX PuwzKnJ0TrDdfRW2Sz66IjGbhAtu+2DXbV1ccfIz0QkCgzKgEmKp4P/IzOVyvoCs3Kd7+d4S ++ij2EqpxxxrDWgyMkhlonHi58Lx13a9St13oU4KNy7RUN5YtOqH4ZduiKbOoZ0X84uX2Blt Tokx7EbpJK3YC4Hw4kpyR7YbvyIaYmI4hT7WeaeIDd4mHJleK+kiBqo7Uegzej8WtGz0FZXs ipFlt7MtncO1xDJ9seHTf598l+g2TaJzQDT6/tLLVo6larBLZMq370+loILvEnDACP6glj6g LOLekk++uWl6v7rbqjpq5OEKYN5ix3yP6orl8CiHeg3KQkDUm2b9Om5yrHu/VP2TbBPg/Erk aTUto3RK94Bqa6jGQBV154u6xahADei19QVhWQKIkpLdRydk4blJ03CLe72Avujn1igjS5nx +7IPr39G5nNKWPMn6n7cbZ69k5c1BE8zddC55JSF74NOurzWlX2tNzEEBA2LxC0w+fgCNV7z I8eXn+PArOdMKPVtl+I5fgjLPWLZI8QoDr9Kv4l6ODyjXIhmVIRY7Ol0YYLZHylBPhrI0SUb WDxjtoOCWsKuxAxTO3uiF2MSz5TYHOyUro65jEgBoOpF4LDR4C2jbyE3Se0AodWZmddClCLH 3foa5+IVOsLaCKXOsNhlCcLWqC7S4A9zRGuqBP6y71/I+bJ4iEYr47s1MBp5+3PkhE/7SB7D 8OE022UU250mn4ISCQt0aBkoU19z0+D3rJij/xZE9xT/fJJXR0gOZ7S1ewpQ+z1D0jKec7MQ 1K7SP2nByswR5Q/2ZVGN016ApCpig3J9yusGb4c0bKRUs8a6KXZil7wJMZ8zz79y6AknhFyR NBQPGi3rqt+/BLUHInHjwOSkKP8JvdU5zLE6GrWlTnGh0pfSgMlCc0tPFgab0rS9pHi41/aC qSpEfIhOxdAzsiLLu1LbMfohBNIXqSrI8zQNkS2nWr4HhOU3vWUdoO/fX4C1SDMIE0FmBoU5 nGIKU41ASLy63nGAmlWHEn0K1jp7fE4rXq6SkEuyATfaVZ+3r+k0hsUjuabUPQdwvQPvyJy4 y5sEgOF1snNQ8GFuxInfKhYZoYl50xb0GvCqwFnFraGdJhY3gY1Tlwv5gbw2QkyDY9N1883s Hkt0Qx+b7qC109MfC+Z2pa2PaDLLm71/1akbKu+Nkj29tGQ9+9P7f05rw6mpwS1Dg859G0h1 dBJ0nya75GMDQwIUJu3XFxlvx5976rXZCUw/ea2nTVlLLW0vzne2tkoGPptyxCueM1aOb+FE wm6GtMTBsynIugn01azaRdMMOdX/a8yd8SoEpnOkKiwI+9ljRqjjG9d55t63F7K/C15C6bJ0 5sD3/CEz16fTT6vxFyls83xhcVFfWRPRCzmkXGiWdAXP/EhGORDQX2jKMC22Nhk0pvkWnoDs UWmG0tDw8ixPxybc1362wRUk0URu32u3yWinFkW23kkqLSS2CvWzqHsbh0CbyRNX3ZriEbEJ Im/ldcBW0a0KQMukVH2gCSyj7gev6l5I2TJFA1OZDf/KnBKV6q7rL2ZZMBTrpgvtG8ENYb0K UDfQbn7rRwA1irlFGYL3zE3eQahvZDhlgB7gmaQRJpqhELQYto4hRLW5diHAOVUwiJDXy5gz z/eGlm7OdCtu9SSjZbK9O6kBSqtUZhacC+jyo3l1mPz43Z1CBiut/WykcfgCg80zWnw0NwiW SjTrRn6a5XmzOzna6Q+JhAuWQG6spYyE5o2ioYqgZAMxXUW4/fdtWEKl2v+K5QT2K7zamYMW S9extfU5Ab/30gwZnmNxo//SjCc2p48PZ/jOjpQh3x7tpwZbcXcpKZJliZ0vFei+AfYYPwm2 ywY1eNr83kCxecApAsqyCyZRLEUB0hReyL2xHHqp5izqrtaYGG3fP2+zk17yJqnF66LpxB0X XfyYJA5GiFsqM54NRiftR+7opGhY9TWYd8J41eSiAjJivl9LZM6jP0RgiR7f2n6uDd2roxzx Qwr1pa8so+dLmxr96/sGR9UOAr+YMYL8y3sh6JTzY6GmpqiFZJ7FnAXTYPlGLi2RSkKu62tZ GPsWHUs722WEr3FEUqD5Vd6+jjRRouzOSjfJWFFn4k6AkjHYhQZ2EdNAX07hsJrSljsnZS+N h8/vndIuDua4lNN0r46akO5Cz+H4l/uMnBtFNCeNEYEt1keoRuKd5TYtqUqQGlZ5sPz9gXVc z7CPl0aAz1RAh7WQAyzW9vmrdjYrbrCD7LnfaKXOOeA9bQFBaXPmcPn05M4rWyFbpzdZyA7X fNnghERDSghQ5aL3GhXLk5f3yPVMZzBrU/lqHQu95KxrKywCgm3vdPdWfwPaJ1u407k267bb rzJ3X8rJ2oAjcECnSeQmupYgQR36Wkmdj+mFakMuHzWVKzc3LdNCAIWYD9yM80O6L8g2g5KO ojQjda9k7d8irRd505tbVX6gYnpYMULJzr4L1bbHAOQM6zAIzTXwsbxaKf6SLtKjewSuQfi8 TqcFkbiOHyEmVyLH1i3NvpQiSiAIBFEkKubKS5XUTDIcYq+M1ilPsMyijc7h7opmnnNKGgQd yBmdF9ApaGR6iUehehjH2tG7TxuKuzh+W7R4+TDK5kQuOdmGWwpzaQDuC18luUTtX0MTec9g CbIq99yv1yq2vKCzDZqSlsGqzpGgp6KoVQ3Oajd8colOz6M9xYM4GOMThUS8oY/TIS34uYNl J6WyPGWSn8K6d/f8MoCCtKBLcuGNCFkKh/1AHvPCxNDSze3NGbZjkgbkfeI93TToIJpz/qk0 JcIVLJfU0Q4U/0ADUEwVtoZP55yTxshkLWBi9UP62b4px7UDpY/3NiPRreJDPPjJSzMx6FDf AcNyKjkIJ47HKug43Y6MnJHxNyTXlTeQZVKqCAnaRIoqkJQ9nQ4Vnc0x0/udgKq5jkUCOKwm Rk1zAB5ZK5+kVWkq0dyLV3MqiwqlUA3ktiwmjGdfgn6K6KoVJ1XAS755AAhd4n2SAFvYUiuj FRpYX3aEqlJgeIqJgUJwEfM/IFCEvlGQehYbQ8MkLuJMu4w3w0Uqz37lxMfo7qfT8MkzExzL Natty4Sh1olNYZqY/SWfO0QkD0yzuqPpnP6i7p3mVdGYR5LqCTLJGYJoBBab+F6YXb3uLQqs UvbxHNCYDZeDfNy+6AzrxpvNbjYl3CylOITTyL5f+2HcfHDsjCZx5fRGwE+ihtTxRsCoek+0 N99IRCdDxl9leLIRRpVbZGQeVkNN5gAsyWLGETG+eTVn8AvNt3kRLmxFL2A6P5P0En8RF57T cNRt4wABsf+ikiAdJW+dedXx0l1v1blfA3dXqYOJUju8n9Pose0yIJ70NtGPj8RR31nNjm67 arWoQlsh+efWNAxYTERWY5Mc3syXIfSc8FxunVLFj6s1ewFjgOF6m2lzswxJBPaNOJZPK+/W Es0UZSo9yl69KK7z1nK7p/ZOmf2c8x4vcPC4v8boJDBDO5ISb56sAHXnIwKHhRCtkbKENWvI IP3ZZVqZtvxWC7Sbw==
- Ironport-sdr: 63e3d697_4n7hCSYhJtosDI4vn1cLNLKeDvjvLewEt0h5k6v+OO9gJxh m4kYe6GjgbvcKUOCekDyQomRJZRxCFOxH0Vt6ag==
- Msip_labels: MSIP_Label_f42aa342-8706-4288-bd11-ebb85995028c_Enabled=True;MSIP_Label_f42aa342-8706-4288-bd11-ebb85995028c_SiteId=72f988bf-86f1-41af-91ab-2d7cd011db47;MSIP_Label_f42aa342-8706-4288-bd11-ebb85995028c_SetDate=2023-02-08T17:06:27.063Z;MSIP_Label_f42aa342-8706-4288-bd11-ebb85995028c_Name=General;MSIP_Label_f42aa342-8706-4288-bd11-ebb85995028c_ContentBits=0;MSIP_Label_f42aa342-8706-4288-bd11-ebb85995028c_Method=Standard;
Thanks Yannick, that's a useful pointer.
FWIW, Agda also rejects the definition below.
-Nik
From: coq-club-request AT inria.fr <coq-club-request AT inria.fr> on behalf of Yannick Forster <yannick AT yforster.de>
Sent: Wednesday, February 8, 2023 12:13 AM
To: coq-club AT inria.fr <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Nested positivity
Sent: Wednesday, February 8, 2023 12:13 AM
To: coq-club AT inria.fr <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Nested positivity
No answer to the question, just a comment:
Another place where a particular behavior of Coq's positivity checker related to using an inductive nested in index position is Meven Lennon-Bertrand's et al.'s development on logical relations here:
I'm not sure it's related, but it goes in a similar direction.
Best
Yannick
On Tue, 2023-02-07 at 22:18 +0000, Nikhil Swamy wrote:
> Hi Coq-club,>
> Coq rejects the definition of I2 below saying "Non strictly positive
> occurrence of "I2" in "I1 I2 I2 -> I2".".>
> Inductive I1 (A:Type) : Type -> Type :=> | MkI1 : I1 A A.>
> Inductive I2 :=> | MkI2 : I1 I2 I2 -> I2.>
> I think this is due to a violation of the Nested Positivity
> condition, described here:>
> However, I couldn't find a description in the manual for why nested
> positivity is important.>
> In particular, if one were to accept a definition in which the type
> being defined (I2 in this case) appears as an index of some other
> inductive type (e.g., I1), do things become inconsistent?>
> Thanks!> Nik>
- [Coq-Club] Nested positivity, Nikhil Swamy, 02/07/2023
- Re: [Coq-Club] Nested positivity, Stefan Monnier, 02/08/2023
- Re: [Coq-Club] Nested positivity, Nikhil Swamy, 02/08/2023
- Re: [Coq-Club] Nested positivity, Yannick Forster, 02/08/2023
- Re: [Coq-Club] Nested positivity, Nikhil Swamy, 02/08/2023
- Re: [Coq-Club] Nested positivity, Stefan Monnier, 02/08/2023
Archive powered by MHonArc 2.6.19+.