Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Nested positivity

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Nested positivity


Chronological Thread 
  • 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:
https://coq.inria.fr/refman/language/core/inductive.html#nested-positivity

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




Archive powered by MHonArc 2.6.19+.

Top of Page