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: [Coq-Club] Nested positivity
- Date: Tue, 7 Feb 2023 22:18:54 +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=tBKGHeC6RLE5SBmAzh2RySsgrOws2N789tVLRNlt++4=; b=jmjgKe4xdK9D2ZF7E9XT2rhJtzB2zQoUl4XcMD00rVRCHy1doCWHHwJixfLI9l4IpV3yL5NllqKeifkp2WgeBdg+YDwQHiInFbPzvjLGb2hA0I7g3mMJc59MLPCVVrgqJyrvQj96lFAMDl96Y91Gq1siKDTtKYOmePigfG9ZqOqQOj2UJnNz7Mo6Ox5FzIqF5bgKYlTKnYCCwYrE7/O2tqML/LibZtuOXVg62AA7yLN0W6QTK8y9z4j/YaEA6FNn7mikn0HrX1jnZsCFoIlAvWizpkp8yJfLmUxU+49USJBWuPJpXpkGaQo6IBFr+HaNsBsdj7BDVtTty6F1Siuqog==
- Arc-seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=BQBtybW12P6WeEuRCCGb8ysMeIDvX+vJWxIsseOUTowR0uxoErbSSjldHa9yOhvXU3L73JZIHZht7gEz+7OlPZd5tiljio7++2xsdPYAbPyKx0sv0JNzTyCl9w46u/huodCekaDd38mvKP2IiFJyfkDwOIoEddQpz1TgjCE8rB+8BGAUybA5lSKF4D0bF8OyQYxdRqaCOwUI83JXJZZa+Zu5zmriMH+mFrP0R2Qihp/nJWo6UA4QElW7mGMGNlLR5TS8/jM1JSK+6++MtTm31bnuCH+c1+lLRBJzcn27W9i2hnF07STVdgkeyqIWSJNAJuqKE/K4o/F91J6a1ABlwQ==
- Authentication-results: mail2-smtp-roc.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:s+fhzaMU+5WgEsXvrR2inMFynXyQoLVcMsEvi/4bfWQNrUp20zFWx mNKX2vSPKrfYWejLtl+O9i28kMFsZ+AyNYwGnM5pCpnJ55ogZqcVI7Bdi8cHAvLc5adFBo/h yk6QoOdRCzhZiaE/n9BCpC48T8mk/jgqoPUUIbsIjp2SRJvVBAvgBdin/9RqoNziLBVOSvU0 T/Ji5CZaQDNNwJcaDpOsPrZ8Ew35pwehRtB1rAATaAT1LPhvyJNZH4vDfnZB2f1RIBSAtm7S 47rpF1u1j6xE78FU7tJo56jGqE4aua60Tum1hK6b5Ofbi1q/UTe5EqU2M00Mi+7gx3R9zx4J U4kWZaYEW/FNYWU8AgRvoUx/4iT8sSq9ZeeSUVTv/B/wGXBK3qw6vdqEnoxLNM41uZtIT1l+ sAHfWVlghCr34pawZqRbLJUvJx7B/SzZNpapH98iDbTALAhXIzJRLjM6ZlAxjAsi8tSHPHYI c0EdT5oaxeGaBpKUrsVIM9k2r7w3z+iLXsB9Tp5poJvi4TX5Apqz7HoIfLQe9eQQt5SkFrer WXDl4j8KkBDaoXDlGTYmp6qrreejDziQJ8DL7CH8fFvhW/Qw3QfNgJDADNXptHi0xXlA4sFQ 6AOwQIlqrF3/0i2RPHmThigqTiFuAQdUpxeCYUHBBqlz6PV50OUD3MYUyUbYc4hspZvHWZyj gbU2dT0GTZorbuZD2qH8auZpi+zPi5TKnIeYSgDTk0O5NyLTJwPYgznSY5iTIe3isPOHiCu4 xyKtghirLovkptev0mkxmzvjzWpr5nPawc64ATLQ26ohj9EiJ6Zi5+AsgaFsK0cRGqNZhze7 CNbxpD2APUmV8nlqcCbfAka8FhFDd6vNyzQnVlpd3XK3272qif8FWy8Dc4XGauEGsMNeDusb UbIpR5KvpZBO33zNPctO9roVoIt0LTqEsnjWrbMdN1Sb5NtdQiBuiZzeUqX2GOrm08p+U3eB Xt5WZr8ZZr5If49pNZTewv7+eR6rszZ7TiILa0XNzz9jdKjiIe9EN/pymemYOEj97+jqw7I6 dtZPMbi40wBD7ChM3WJq99CdQ5iwZ0H6Xbe+50/mgmrclsOJY3dI6WIqV/cU9A7z/QMy7+Tl p1DchYGkwCi2RUr1jlmmlg4Mei0Bc8lxZ7KFSktNkyvwH8tfc6m/roFevMKkUoPpYReIQpPZ 6BdIa2oW6wfIhyeomR1RcSj8ORKKUr67SrQZXbNSGZkJfZIGVeWkuIIiyO1r0Hi+ALr7ZRhy 1BhvyuHKac+q/NKVp2OMqjwkg/r4BDwWotaBiP1HzWaQ220mKACFsA7pqZfzxgkeE6TlAiJn R2bGwkZruTrqoo4uouBz6OdoovjV6M0EkNGFiOJpfy7JAvLzFqFmIVgaeeveSyCdWXW/K75W /5Z4cuhO9I6nXFLkbFGLZBV8YwE6eDCmZpm3yV/PXCSb12UGrJqeXaH+s9Ut5xy/LxSuCroe 0Gt3fwDE46sFOnJLmI4Oy8eN76x08gIkGPw6dAwcRz2yw1p8IXaUmFUFQiG0xZZHeBPKIl/n for4/BO4SPulBM7b9SM1HhV00+uLXUwdbotmb9HIY3siystkkpjZ76FAADIwZi/Ufd+GWh0H S2xm4z5mKV6+kXZVng4SFzh/LZ43MwVmRZoyFQiGQy4quDdjKVq4CwLoCUFcAtF6z5mjcdhM XdPHG9oL/ys+zxIupByb1q0EVscOCzDq13D8HpXpmj3VELya3fsKlc6MuOz/Ew01WJQUzxY3 bOAwlbeTjfYU5Dt7xQ2RHJahaTvff5p+i3GvfKXLcCPMp05QDji26GVdTUprTnjCpgPn0Hpn 7Rh09txTqzZDhQuhZMHJbOU74lNdyDcFld+Galg2IgrAVDjfCqD3GnSCkKpJeJICf/40W65L M1MOstwcQW0jwCQnDYiGJ9WcqNVneEo1vUGaLjENW4LiJrBjztL4bb71Dnyu38vePpqyf0CE 4L2cymTNFCQiV9/uX7/nOMdNkWWOdA7NRDBhsar++A3Jrc/meBLc3Bq9ICrvn+QYTBVzzjNs CztP6bpnvFfk6JylI7RE4JGNQW+CfX3cM+qqAmTkdB/XenjAPf0lTE+iwfYZlxNHL4rRd5Iu 6yHs4f30GP7rb8GaT3ltKfbJZZZx/eZfbRxAprsIWh4jBmyfpbmwyE+9lCSLb1Ll9Jg5febe TaoVfvodfMoX4Zy+X4ETQlfDBcXNIrvZIjCuy6WjqqBGzod4yP9PfKl8n7jUmVZfSpZKZekO FfQvtCw7Ot5t6VJPgcPXNt9Mq97IXjieKooTMLwvj+mFVuVgkuOl7/htBg44xTJNyW0K9n76 pf7WRTOThS+l6XWxtV/sYYpnBkoIFtioOs3JGQxxsVXjm2kMWs4MugtC5UKJZVKmCjU1pujR jXsbnMnOBrtTwZ/bhTwz9TybDixXtVUFI/CGQUo2EeIZwOdJoCKWuJh/xg9xUZGQGLoyeX/J OwO/nH1AAOK/ahoYuQtt8yL2bItgruQw38T4knynvDjGxtUU/1AyHVlGxELTiDdVd3EkELQP 2UuWGRYWweBRFXsFdp7MWtgcP3DUOgDEx1zBctO/Dreh2lf5Mdmk8XFY7nY7+VbNYEUKqJLQ nn6AWyQ/2qRx3of/7MzvM4kirN1DvTNGdWmKKjkRksZmKTYBqEPIZYZhSRWJC090Fc3Lr8fv mDED7sC6ICtLUFawrqNzgsVvZl2VxrgyhnX2RXnq2aufQMRlrDkltvD8O4/AZTxoLLkpEJWX HEZa0P5T5h6ctf7jWEWi8n3bWBrzS3c+bcon8zool7Pfs+QdVJg
- Ironport-hdrordr: A9a23:x4s4DqDfEAwrRqrlHegysceALOsnbusQ8zAXPh9KJCC9I/bzqy nxpp8mPEfP+VAssQIb6Km90ci7MAXhHPtOjbX5Uo3SODUO1FHIEGgA1/qq/9SDIVyYygc178 4JHMZD4bbLfDtHZLPBkWyF+qEbsbu6Gc6T5dv2/jNId0VHeqtg5wB2BkKwCUttXjRLApI/Cd 61+tdHjyDIQwVdUu2LQl0+G8TTrdzCk5zrJTQcAQQ81QWIhTS0rJbnDhmj2AsEWT8n+8ZpzY GFqX212kyQiYD19vbu7R6c032Qoqqh9jJ3Pr3BtiHSEESttu/nXvUjZ1TIhkFMnAjm0idQrD CLmWZpAy070QKtQom4zCGdoTXIwXIg7WTvxkSfhmamqcvlRCgiA84Eno5BdADFgnBQye2U/Z g7rF5xjaAnfy/ojWD4/ZzFRhtqnk27rT4rlvMSlWVWVc8bZKVKpYIS8UtJGNNYdRiKn7wPAa 1rFoXR9fxWeVSVYzTQuXRu2sWlWjA2Eg2dSkYPt8SJ23xdnWx/zUEf2MsD901wgK4VWt1B/a DJI65onLZBQosfar98Hv4IRY+tBmnEUXv3QRKvyJTcZdA60l722uDKCe8OlZ2XkbQzveQPpK g=
- Ironport-phdr: A9a23:lOHABhZ9o0H+H+zo5cwQeeb/LTHD2IqcDmcuAnoPtbtCf+yZ8oj4O wSHvLMx1gKPBNmLoKsZ1qL/iOPJZy8p2d65qncMcZhBBVcuqP49uEgeOvODElDxN/XwbiY3T 4xoXV5h+GynYwAOQJ6tL1LdrWev4jEMBx7xKRR6JvjvGo7Vks+7y/2+94fcbglWhDexe65+I Rq1oAneq8UbgYtvIbstxxXUpXdFZ+tZyWR0KFyJgh3y/N2w/Jlt8yRRv/Iu6ctNWrjkcqo7U LJVEi0oP3g668P3uxbDSxCP5mYHXWUNjhVIGQnF4wrkUZr3ryD3q/By2CiePc3xULA0RTGv5 LplRRP0lCsKMSMy/WfKgcJyka1bugqsqRxhzYDJfIGbOvlwcb/Sct4BX2VNQtpdWjZdDo+gc ocCCfcKM+ZCr4n6olsDtQOwBQivBOPvyz9IgmL907A00us7FAHH3BErEtUIsHTPotT6LqISU OCuwanNzDXMc+lW2TDm6IjPfBAhveuAUq53ccrU0EQiER7OgVqMp4L/JTyVyvgNvHaB7+pmT e+jl2EppgBsrjWu2MsihJTFiI0Ux13A+yh0wok7KcC8RUN7b9CpEJRduiWVOYdqQM4vXXxkt SIkxrAIpJO2eDUGxZI6zBDRbPyHdpKH4hPlVOuJIDd4gmhleLOliBqo/0ig0OvxXdS33lZSt idIksfAumoQ2xDP98SLUPtw80a71TqS1w3f8v9ILEEomafVLpMt36I8mYESvEnGHiL7nVv6g a+IeUgh/+Wk9ufqb7P7rZGGLYB0kBvxMqE2l8y/H+s4Ng8OUnCG9Oqk2rDt51H3TKlWgvAon KbVrIzWKdkCqq6nDQ9Vzp8v6xGkADi4ytgYmmQHLE5edxKAkojpPUzBLOrgDfelhFSsjClky OzaPr3gBZXNKGLPkLD8fbZh705czw0zzdNF651IDbEBJer/Wk73tNPGEh80Kwy5z/j9BNlgy o8SRHiDD6+YPa/IrFOF5vojI+yWa48UvDb9JeIl5/nrjXIhn18dZqeo0oESaHG4BflmJkSZb mb2gtcGCmcKuQQ+TPDwhFKeVj5TYm6+X6Qn6T4jEoKpEZ/DRpyxgLyGxCq3A4VaZnpaBVCUD Xfoa4KEVu8QZyKVO89tiyALVby8S4A6zhyurw/7y79/LuXO4CEYtJTj1MJ05+LJjx0y+yZ0X Iyh1DTHRGZt22gMWjUe3aZloEU7xE3JmfxzhOUdHthO7dtIVB07PNjS1bopJcr1X1fnf9SJS VLuecqvBCB5GtQq3NYLcm54Gt64iQvE0TbsCLgQwe/YTKco+77RiiCib/12zGzLgfFJZzgOR 8JOMTfjnatj703JAIWPlUyFlqGsfKBa3SjX9W7Fw3Dd9FpAXltWVqPIFWsaelOQtc7ws0XZU LarGJwiMwBbztWFJLcMYdrs3h1dXPm2AN3FeCqqnnuoQxOBx7eCdo3vLmMGwyzYGWABkgsJ+ m2BOxR4DSCk8CrFFDI7LVv0eAv39PVm7nO2Skhh1waRc0hozKa44DY/o6ekcatL9Y9c4H5kt TtoWVG30pTRFsaKoBdncONEe9Qh7Vxb1GXf8QtgIpinKKMkjVkbG+hul2Xp0Rg/SoBJkMxw6 Wgv0BI3M6WTllVIazKf25n0fLzRMGj7uh61OebQ3RnF3dCa971qirxwokj/vAyvCksp8ml2m 9hT3XyG45zWDQ0UGZvvW0cz/hJ+qvnUeC44r4/T0HRtN+GzvFqgk5ovH/QszweIetZUKqSfE wHuVcYdAonmKeAnnUSocgNRJPpbp+Y/O8KrcefD2bb+YbwmxWr/yzkZptkggSfuv2JmR+XF3 ogI2aSd1wqDDXLniUu599rwksZCbC0TGWy2zW7lApRQb+t8Z9Vuay/mLsupy9F5n5OoVWRf8 QvpAUgZ0cq4UR+TZEb6xgpeyQIcpnntyk7ah3Rk1iokqKaSxnmExf/9fR8WEmtKT3NlllDiP c6/iNVQDy3KJ0A50RCi40j93a1Soq9yenLSTUl/dC/zN2h+U6G0u9JueuZ34Ygz+WVSWeW4O xWBT6Ll5gEd2GXlFndfwzYyc3ervI/4llp0kjDVIHF2pXvfMcZ+oHWXrNrHWvdUzxIDRSJij iLQCET6NN6stdmZjJbMtOmiWnnpC8cVKHGyi97e8nLmrWRxSQWyhfWyhsHqHW1YmWfg2t9mW D+J5Bfwb4/31rirZOduf01mHlj5uIJxHoBzlJd1hYlFhCJc383MuydZ1z6uYrA5kerkYXEAR CAG2YvQ6Qnhggh4K26Rgpj+XTOby9dgYN+zZiUX3Dg85oZEEvTxjvQMkC1rr16/tQ+Ub+J6m 2JXz+Ax4XsLq+QIsxAq1SKTHvYZGkwSbkmO31yYqsuzqqlafjPld6Ov3U9vtdWgB6uFuQZSR DDyfZJoTkoSpo1vdVnL1nP08ITtftLdOMkSuhOjmBDFl+FJKZg1m6lClW99NGn6p3Fg1/8jg Ekkw8ShpIbeYTYInurxEltCOzbyfc9W5jz9kfMUgJONx472VpR5RmdXBN25F7TwVmpV7KmvN h7SQmFk7C7DRvyHW1fYsRkDzTqHEoj3ZSzNYiBBlZM6AkHafRAXgRhIDmxiwthlSUbygpSmK Rgx5yhPtATx8kIek7sxZRejCj+N9kD0OlJWANCeNEQEtAgavhWMaJXM4L4rRHMKucHw5A2Vd D7BblwRXzhQAx6KWwi4bOn2vYGSoa/FXo/cZ7PPeevc8+UGDqXRnMv93Nc+pGSHbp3XbCslU qRz21IdDypwQ52LwmxWGSJLz3mfYZbD/EXuvXAty6L3uPXtUwby6YbdEKNcPZN34ReqjKyfN umWwiFkNTJf0ZBKznjNgP0W2FpY4813XwGkCq9I9SvETaaK37RSEwZecSR4cs1B86M72ABJf 8/dkNL8kLBi3LY5DFJMVFqpnc/MB4RCO2amKFbOH1qGLpysA2bz+ZmvSp7kEeQVkutI8hq6t HCcDlPpOSmFm3/xTRezPOpQjSadehtDpIW6dRUrAm/mKbCuIhG2K954izQqzKZ82ymMbDZFd 2UiNRoQ5rSLpTtVmPB+B3BM4jJ+IO+IljzYp+jUJ5AKsOd6VyR5k+UJhRZyg7BR7SxCWLl0g H6P9Jg3+wjgz7fJk2c0NXgG4ixGj4+Ko0h4bKDQ950aHG3B4ApI92KbTRIDu9piDNTr/aFW0 NnG0qzpe1Igu5rZ+9URA8/MJYeJKn0kZFDvAyHdCRotSD+gL2bEgEJB1vqV8zfGy/py4oipg 5cIRrJBARYtEegGD01+ANEYCL1RBQseyeawsZZQvD+gogWUQ89X+JfaSviVHPPjbi6DiqVJb AcJxrW+KpkPMor82AppbVwwz+GoUwLAGNtKpCNmdAo9pk5ApWN/QmME0EXgcgqx4XUXGK38j lsshwB5e+ho6Cb07gJ9OA/RvCVp2hpU+52tkXWLfTX2Nqv1QYxGF3++qR0qKp2iCwdtMV/ux Qo1bnGcAeoW1uYodHg32lOE/8IXRrgEC/UDOUF1p7nfZu10gwkG7Hz/nQkfo7OCUMcqlRN2I 8f08zQchEQ7KoZyfPOYJbIXnAJZ3vvc53bxhO5tmFdMdQFRoAbwMGYJoBJabLB+fnjxp7U+5 1DawGkRPzRdH/sy/KAw/xtkab3ZlnDuj+YYeBDpb7TNfeTE4w2i3YaJWg1ijEpQzhscpOEk3 5t7KBifDxh3nunWSk1BNNKce1tcN5MArSGKLyjS6b6fz8otZ9fvUb2yKI3G/KcSiUa5EAt7B JwC4oIZBJ6w3UrELMDharkY1REq4wetL1KARLFAfBbB+N/mi+uZl6dNhdF2G2lFWCBjPzny4 bza4Ag3nPCEQdE6JG8AWZcJPW43X8v8nDNFu3NHD3+81edLkWBqChf5py/KCyL7YcYlb/CRN 0sE4D6e/DQ06a+tjlDLtJ7ZIjOjXek=
- Ironport-sdr: 63e2ce52_Naldj1He2ewj9egVSyxTfTmy3g1yQNWZUKipAIEirJvpirH bM7TSzIqfVwjU/D/j0CioL2G2JiNppWCzos/4Qg==
- 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-07T22:18:54.171Z;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;
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+.