coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Understanding non strictly positive occurrence error

From: Murali Vijayaraghavan <vmurali AT csail.mit.edu>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Understanding non strictly positive occurrence error
Date: Thu, 1 May 2025 07:46:44 -0700
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=vmurali AT csail.mit.edu; spf=Pass smtp.mailfrom=vmurali AT csail.mit.edu; spf=None smtp.helo=postmaster AT outgoing2021.csail.mit.edu
Ironport-data: A9a23:Aaucd6+X18pfzmEf2A9UDrUDG3qTJUtcMsCJ2f8bNWPcYEJGY0x3z jFNXj2AOf3YZmSnLdxxa96x/BgG7J/Xz95lTAps+CxEQiMRo6IpJ/zJdxaqZ3v6wu7rFR88s Z1GMrEsCOhuExcwcz/0auCJQUFUjP3OHPymYAL9EngZbRd+Tys8gg5Ulec8g4p56fC0GArlV ena+qUzA3f7nWcpWo4ow/jb8k434ayr4GpwUmEWPJingneOzxH5M7pEfcldH1OgKqFIE+izQ fr0zb3R1gs1KD9wYj8Nuu+TnnwiGtY+DyDW4pZlc/TKbix5m8AH+v1T2Mzwxqtgo27hc9hZk L2hvHErIOsjFvWkdO81C3G0H8ziVEHvFXCuzXWX6KSuI0P6n3TE88lQIXoTG84i59lKUHh/8 +YSDgsNcUXW7w626OrTpuhEgdk/I87qOoxF4is5izrCBPciB5XCX+PH6cIwMDUY35oeW62GI ZBfNmoHgBfoO3WjPn8JDY8kleOprnLkejxc7leUuew673W7IAlZiuK1a4KLIofXLSlTthfHo EvPpV3/PhEHEvq41x6KwHOzotaayEsXX6pLSeTjrZaGmma7zWsKTRYSSFGTuui8kkf4WtRFK kVS9DBGkEQp3Eu2Utb6Xhu3+ibe51gXQNNRF6s/6R3Lx6bJi+qEOoQaZg59VvEdkel1fyEV6 w6QrtXzDxpUsKLAHBpx6YyohT+1PCEUK0oLaikFURYJ7rHfTGcb006nojFLTfPdszHlJQwc1 Qxmu8TXuln+pckWy6q8/FbI2Wr2/97CVQc04kPSX37j4w9kDGJEW2BKwQWHhRqjBNzDJrVkg JTis5PEhAzpJcrW/BFhuM1XQNmUCw+taVUwe2JHEZg77CiK8HW+Z41W6zwWDB42bphcImC4P xSM5VM5CHpv0J2CMPQfj2WZVphC8EQcPY29PhwpRoAVPMYtKlPvEN9GPxXBgjuFfLcQfVEXY MrCKp3E4YcyDK181zO9R/oG3KM33Wg/w3jPRIzm0xnv1rTWeHOeSbECNFyBf4gEAFCs/W3oH yJkH5LSkX13CbSuCgGJqtR7BQ5RchAG6WXe8Jc/mhireVE+QDlJ5j646e9JRrGJaIwMz7uTp y3iBB8JoLc97FWeQTi3hrlYQOuHdf5CQbgTZETA5H75iihxUpXl96oFaZo8cJ8u8eEpn7Y+T OAId4/ESr5DQyjOsWZVJ5Tsjp1QRDLyjyK3Pg2hfGceebxkTFf34dPKRFbk2xQPKSuVjvEAh YOc+DnVerc9YjhzLd33bauvxmyhvHJGl+NVWVDJE+Zpe07t0dZLLn2ogtA7PcgzdBPmxBKL8 j3LAxxCi/HHiNIp+enwmJK7ld6IEvR/LGVeDWL0/ba7DgiE32uBkKtrcveEQiDZb0zwoJ6dX ORyy+qmFu8qh3NIjtZMKKlqxqcA+Nffnb9W4QB6FnHtbV7wKLdfDlSZ/MtI7Ith+6R4vFaoZ 0ex5dVqA7WFF8f7Glo3JgB+TOCi1+kRqwbC/8YOP0T2yy9mzoWpCXwIEUG3txVcC79pPKcO4 +Qr4pcW4jPirCsaCI+NiyQM+lmcKnAFbb4ciagbJ43WkSsu9EBJZM3NKy3x4azXUe52DGsRH ma2ipbB1pNm/WiTV1ooFHPI4/hRuoRWhjBO0205Bgqonvjru6YJ+SN/oBoLSjZb9BFl695IG 3NKMhR1LJqe/j0zi8lkWXutKj57BxaY2xLQzn0bpVLdVG2tD3TBBzA5C8aw/WQy0WFVTh5E9 p62lUfnVjfLepnq/y0QAERKld3qfeZTxCbjxv+1Lp+gJIYrRwbljouFR3s6mzG+Dewf3ET49 PRXpsBuYqjFBAssiqwcCbjC848PSRqBdVdwcds48IwnRWjjKSyPgx6QIEWMe+RIFfzA0Wm8L +dMfstvdRCP5ByinwAhJ5wnAuFLxaYyxd84ZLnUC3YMsOKfohpXoZvgzHXCq1Fxcep+s/QWC 933TC2DIFyylHEPum7qret4AESaT+QARjXB2LGSzL1UObMF6PphYGMj4IuS5n+1CjZqzziQn QHEZpLV8dBc9JRRr9PsP5hHViqJKoLVdeWX8QqMncxEQvHRPOzv6Q4EiFnVED5HHLkWWuUss 7SEj8Hq1nzB5JIzbWPVoLiaNqxz/c7pdvFmAsH2C3h7nCW5R87n5SUYyV24MZBklNB85NGtY QmzeO+cVIcydY9G5Xt3byN+LU4sO57vZP29mRLn/uW+NBcN9CfmcvWlzCbNRkNGfHYqP5beN FfFi8y27IoFkLUWVQ42PNA4MZpWO1S5ZLAHcef2vjymDmWFpFOOl7/htBg44wHwFXi2P5fm0 K3BWyTBWky+iIPQwPFdlr5CjBkdIXJ+oOs3J2Y22dp9jRKkB28nc8UZF7g7Ca9vry+j76GgO Qnxb1YjBxukDH4AOV/57c/4VwiSOv0WN52rbnY19keTcGGtCJnGHLJl8Tx67mxrfif4ituqM swa5ma6Ky3ZLkuFngrPzqfTbSZbKvLmKrYg/l3hnMvzBRlEWe9Tknd6FQtJEynGD4fAmFijy a3Zg4xbaBnTdKIzOZ8Il71p9NUxtyjmzjFuaCaThtvTpu13CcVenebnNbibPqIrNaw3yX1ne Z8zb2CW6mGSnHkSpe0kt89BbWqYzx6UNpDSEZIPjjH+U019BqrL8i/CcecyoBkexTNi
Ironport-hdrordr: A9a23:ahXAQqlQgiyVSeKkVnnGRYgdsbbpDfLl3DAbv31ZSRFFG/Fw9v re58jzsCWetN9/YgBEpTntAtjjfZqYz+8X3WBzB9aftWvdyQ2VxehZhOOJrgEIWRefygc379 YYT0ERMqyJMXFKyej/pCa1G8s929WcmZrY4ts2DE0AcShaL49l5wd9TiCBEkN3QwFCQb40Do CV6MYChxfIQwVyUi12PBY4tiH4yeH2qA==
Ironport-phdr: A9a23:GPvNkh9CnM+R4f9uWdK2ngc9DxPPW53KNwIYoqAql6hJOvz6uci5Z gqHvb430g6ZAc3y0LFttan/i+PaZSQ4+5GPsXQPItRndiQuroEopTEmG9OPEkbhLfTnPGQQF cVGU0J5rTngaRAGUMnxaEfPrXKs8DUcBgvwNRZvJuTyB4Xek9m72/q99pDdfQlEniaxba99I BmorAjcssobjIR/Iast1xXFpWdFdOtRyW50P1yfmAry6Nmt95B56SRQvPwh989EUarkeqkzU KJVAjc7PW0r/cPnrRbMQxeB6XsaSWUWjwFHAxPZ4xHgX5f+qTX1u+xg0ySHJ8L2TLQ0WTO/7 6d3TRLjlSkKOyIl/GzRl8d9ir9QrhC8qBxl24Pbb4+VO/h+cK3Tft0UWHRPUdpKWiNbHo+xd ZECA/YdMetaqYT2ulsArQG5BQmpHO7hzSJIhmXs0q0+0uQqDA7J3A0iH90UsHXbts/1O70dU eC11qbI0y/Mb/VL0jr69ojIdw0hoeuWUrJ0cMrc0lUgFxjfgVWRrYzpJTaV1uURs2SB8eVvS P+vhnchpgpsrTeh2t0ihZPVhoIJ1F/E7yN5zZ42KNC4SUN2YcCpHZVQui2GKYZ7Tc0vT31ot is517AIuZ+2cicLxZg52xPTd/OKfouJ7x/hSeqcLyp0iGx5db+igRu57Eauyur5Vsau0VZKq DJIk9jRtnAJ1hzT8tSISvtn8Ue9wzqAywfT6uRcLU8olarbL58hwqYqmZoXq0vPBCn2l1vqj KKQa04q+fCo5vz6brn4pZKQLYF5hh3kPqgwgMCyA+c1PhAQU2SH/emwzr7u8E3jTLlUk/E7k 7PVvZ/eKMkdu6W0HQtV0ps46xajETimyskWnXgGLV1bYB+Lk47kMEzULv/iF/ewmVGsnS9rx //YOr3hBY3ALn/ekLf9crZ97E9cyAw8zdxB+55YFKwNLOjvVU/qrtPYDxs5Pxaxw+bmFNVxz J0RVn+SAqOBMaPSt0GH5v43LuWReoMYuyzxJvY56/L0k3M1g10QcKqx0ZsScn+4H/BmI0uDY Xrrh9cMCXkKvg8jTOzwklKCVT9Tam2uUKIn/D47CYamAZ3GRoCsnLyNxjm0EYBLZmxeDFCDC m/nd5+YVPcUdCKSPshhnyQZWbS5UY8uyQmutBPmy7pgNufb5ioYtYv62Ndp4+3TiAo9+CdvD 8Wd1mGNV3t7knkJRz8wxqB/oFZyxk2N0ahi0LRkEolY4OoMWQMnP7bdyfZ7Apb8QFHvZNCMH XO7WNyiAHkPT9A40tYUakl9EsuriFiXwS+3GbYRlpSAH5U19uTZ3mS3KspgnSWVnJI9hkUrF 5McfVatgbRyolC77+/hlkyYk/zvbqEAxGvX82zFy2OSvUZeWQo2UKPfXHlZaFGF5c/h6BbkS LmjQa8iLhMH0dSLf7VPd8fgiVRuT+zqOdCYZmOt3Wq8GEXA3auCObLjYH5VxyDBEA4BmgEX8 2yBMF0gAzq7qmbfJDd1HFPrJUbt7a9zpG7oBlQswVSsaEtsn6Gw5gZThfGYTKYL2akYvS46t zhuNFGgw93RCtyP/VI7JeNXeto85BFC1H6fugBgVnC5B4ZlgFNWMwF+vke0kg5yFp0Fi88h6 nUj0At1L6ucllJHbTKRm57qaPXRLSHp8RajZrSzuBmW2cuK+qoJ9PUzqkny9ACvGE049nx70 t5Tm3KC75TOBQAWXNr/SEEyvxR9orjbZGE66ea2nTVyNLSuuzvD89kyDeohjBOhY5FSPL7FX A7+HssGBtS/ffQwkgvhZRYFMeZOsa8sapr8J73dgOjxerkwz1fExSxd7Ytw01yB7X95Q+/Mh dMexu2AmxGAXHH6hUugtcb+ncZFYysTFyyx03uBZsYZa6tscIIMEWrrLdeww4A0mZvwQXdc9 XaoHFoH3ImseAbUYlDgl141twxfsTm8lC20wiYh2S8ss7CW2C3myP/rdR5BP29XAmRukB2/R Or8x8BfV0+uYQ8zkRKj7kuv3KlXqpN0KGzLSFtJdSz7R417epO5raHKI8tG6Zdy9D5STPz5e 1eRDLj0vxod1SrnWWpY3jEyMT+w6N31mBlziWTVK3gWzjKRZ8Rt3x7b5fTXXvdQ2nwDRTU+h DXKTlSxJNim+9yImoyL67ruETn5EMcVLnmjxJjIrCah4Gx2HRCz+pL70sbqFwQ3y26z1tVnU znJsAepZ4Dq06qgNuc0NkJsBVL69497AtQnyNt238lWgz5F1sbwnzJPi2r4PNRF1LiraXMMQ WRO2NvJ+E3/30YlKHuVxoX/X3Hbw817ZtD8bHlFv0B1p81MFqqQ66RJ2CVvpV/t5xzUfOJ0m jY1wuAn6XpchuAV/gch02/OZ9JaVVkdJiHqmxmSupqgqbhNbWKuWbOr3Ut629WgEPePrhwWC xObMt8yWCR36Mt4KlfF1nb+v5rldNfnZtUWrhSIkh3EgrsdONcrm/ENnyYiJXPlsChv1bsgl RI3l8Lf3sDPOyB38am+GBIdKjDle5ZZ5GT2lagH1seOg9L2RMUnQW1NBN2wCqv1WDMK6aa+Z 0DUTntk7C/cQOS6f0fX6V86/SufVcvycSnRfD5Ak51jXEXPfRYPxl1OGm18xtlgSEir3JKzK hkhvWJNvgbx+EkLkbggLwXlGmLPwWXgIjYyQ5yCIBcE6wBeoUrZLISI5+Z3VUm057WHqwqAY iyebgVMVyQSX1CcQkrkNf+o7MXB9O6RAqy/KeHPaPOAs74WUfDA3p+p3oZ8mlTEfsySInlvC eE60UtfTDh4HcregTAGVy0QkWrEcceaoB62/iA/oNq49bznXwfm5I3HDLU3U50n4xetnaKKL PKdng5+NCpX0ZIKyiWQkuFZ10UbiiUocjixV7kMqG+FTa7dnLNWEw9Oay53M5gtjep01Q1MN MjHz9Ltg+ci3rhuUxEfEwOxyaTLLYQQLmqwNU3KHhOOPbWCf3jQxt3vJLm7QvtWhflVsBu5v XCaFVXiN3KNjWqMNVjnPOdSgSWcJBEbtpu6d0MnF23+VtviazWwK9Z2iXszwKFyi3/Xfz15U 3A0YwZWo7uc4DkNyO14AHBE52F5IPOsnDuF4O7ZLJlM6aEyRC9vnuNepnE71/1Y4DwOF5kX0 GPC69VppV+hiOyGzDFqBQFPpjh8j4WOpUx+OK/d+/GouF7D4Q4C6mSWBE5S/YIjAcbmuqQWz 9nT0q//NWUamzox1cAHDsnQbseGLDwsPQe7QFY84yMOVjeqMSfahlAbnf2PpCT9kw==
Ironport-sdr: 68138962_iDFM6RLpzGBXvFO+sC+t1n5MekPzCtRD4zGSKB7GTqt1Re9 jkzoxUXvz/AexPupyAY+a/jMf9LxcTjHwz5CiYw==

Moved the discussion to Zulip #Rocq users > Understanding non strictly positive occurrence error. Let's chat there, thanks!

On Thu, May 1, 2025 at 7:29 AM Murali Vijayaraghavan <vmurali AT csail.mit.edu> wrote:

Does that mean the above definition does not lead to an inconsistency? I want to know if I can keep the above definition with the fixed point instead of having an isomorphic definition (almost like) below which is accepted by default, and convert back and forth in my development.

Inductive Foo: Type :=
| Simple: nat -> Foo
| Bad n (vals: Fin.t n -> Foo): Foo.

Would one be able to fix the (strict) positivity requirement to allow these cases in the future?

On Thu, May 1, 2025 at 7:14 AM Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net> wrote:
fixpoints are not understood by the positivity checker, so it rejects the declaration.

Gaëtan Gilbert

On 01/05/2025 08.15, Murali Vijayaraghavan wrote:
> Hi
>
> I was wondering why the following definition fails:
>
> Inductive Foo: Type :=
> | Simple: nat -> Foo
> | Bad n (vals: (fix helper n :=
> match n with
> | 0 => unit
> | S m => (Foo * helper m)%type
> end) n): Foo.
> Error: Non strictly positive occurrence of "Foo" in
> "forall n : nat, (fix helper (n0 : nat) : Set :=
> match n0 with
> | 0 => unit
> | S m => (Foo * helper m)%type
> end) n -> Foo".
>
> From my understanding, strictly positive occurrence requirement is violated if I supply the inductive type as an argument to one of the constructor arguments (as discussed in http://adam.chlipala.net/cpdt/html/Cpdt.InductiveTypes.html#lab30 <http://adam.chlipala.net/cpdt/html/Cpdt.InductiveTypes.html#lab30>), but in the above example, I am just trying to use an size-indexed tuple as a constructor argument. How can I prove False if the above definition were accepted?
>
> Thanks
> Murali

[Coq-Club] Understanding non strictly positive occurrence error, Murali Vijayaraghavan, 05/01/2025
- Re: [Coq-Club] Understanding non strictly positive occurrence error, Gaëtan Gilbert, 05/01/2025
  - Re: [Coq-Club] Understanding non strictly positive occurrence error, Murali Vijayaraghavan, 05/01/2025
    - Re: [Coq-Club] Understanding non strictly positive occurrence error, Murali Vijayaraghavan, 05/01/2025