coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Yannick Forster <yannick AT yforster.de>
- To: <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] Nested positivity
- Date: Wed, 08 Feb 2023 09:13:01 +0100
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=yannick AT yforster.de; spf=Pass smtp.mailfrom=yannick AT yforster.de; spf=None smtp.helo=postmaster AT himalia.uberspace.de
- Ironport-data: A9a23:+JTAPaDWGDIrYhVW/0fnw5YqxClBgxIJ4kV8jS/XYbTApGkr0zBVn TcdUTjXbvyDYTT3Ld4nPduy8RtXusLQyNZhOVdlrnsFo1Bi+ZOUX4zBRqvTF3rPdZObFBoPA +E2MISowBUcFyeEzvuVGuG96yM6jMlkf5KkYMbcICd9WAR4fykojBNnioYRj5Vh6TSDK1rlV eja/ouOZzdJ5xYuajhPs/jb+Es21BjPkGpwUmIWNagjUGD2zCF94KI3fcmZM3b+S49IKe+2L 86rIGaRows1Vz90Yj+Uuu6Tnn8iGtY+DiDS4pZiYJVOtzAZzsAEPgnXA9JHAatfo23hc9mcU 7yhv7ToIesiFvWkdOjwz3C0usyxVEFL0OavHJSxjSCc5xfYXHm2599vN00ZD84e2900JFpEr uNNfVjhbjjb7w636LK6T+Boh81lMcPmJpgHs3ptiz3UZRokacmTHuOQu5kBgWl235oQdRrdT 5JxhT5HfR3GZRxEOX8GBpUkh/ulnD/zflW0rXrJ+vNpvDSKkGSd1pCzLvqLd/uKQ/lum36mg z/lw37zGR8VYYn3JT2tqy713baQ9c/hY6oZE6T9/fp3inWI12kLAVsXU0G6qL+3kCaDt8l3K 00R8y4vpO4v/kGxVcH0VBD+rHPsUgMgt8R4SfMV6lup4Kvv7ymrRW4ldX1kU9Z9q5pjLdA17 WOhk9TsDD1plbSaT3OB67uZxQ9e3wBJfAfuggdZF2M4D8nfTJIb00uVH4c4eEKhpoypSGioq 9yfhHJm390uYdg3O7KT0X2vvt5BjpjISwcx5wyRQ2io9BhhbYWoIYClgbQ60RqiBNvJJrVil CJY8yR70AzpJcvV/BFhuM1XQNmUCw+taVUwe2JHEZg77CiK8HW+Z41W6zwWDB43bZtbKGO3O xaO4Fo5CHpv0J2CMPYfj2WZVphC8EQcPYiNug38MIQTPPCdiifYrXwGibGsM5DFyRR1yvhgU XtqWduyAHABGL8vwz+8R48gPUwDmEgDKZfobcmjlXyPiOPODEN5vJ9ZaDNimMhltvLbyOgUm v4DX/a3J+J3CbGgPXaIqNZCRb3IRFBiba3LRwVsXrbrCmJb9KsJUpc9GJtxJdI3rLcfjerS4 HC2V2lRzVe11zWNKhyHZjonIPnjVIp25yBzdyE9H0ea6156a6aW7YAba8QWe5sj/7dd1vJad aQOVPiBJfVtcQ753QohQ6Pzl6FYTyTztzmyZ3KkRBMdY69fQxf4/464Xwn3qwgLICmFleo/h LyCizHeEIsIHD5mB8eLa8CU7kiQuEIFk7lYRHr4Idh0eWTt/rN1Kif3sOQFHsEUJTjHxRqYz wymOggZruzzvIMFytnFqqSapYOPEeElPE5lM0TEzLSxbw/2w3GCxNJebeO2YjztbmP416G8b +FzzfunEvkmnk5PgrVsAYRQ0qMyyNv+lYB0lj0+Mi3wUG2qLbd8Ll2t/8pF7PRNz4AEnzqGY BuE/90CNIiZPM/gLkUqGzMkSea9hNU0gTjZ6MonLHrqvBFX+KW1amQMHh2uphEEEp5LHtIL/ eMTtvQSyTSDsTsxE9Pfjilr52WGdXMBdKM8t6AlOozgiyt161dGZJaHKD36z6+eT9B2NmgrP T6mq67QjJtMxkf5UiQSFFqc+cF/lJgxqBRx41taHGuwm/3BmvMT9z9AwwQdFwh64E1O7LNuB zJNKUZwG5Srwx5po8pyB0aXBABLAUyiyHzbklcmujXQcBi1azbrMmY4BOeq+XIZ+UJ6ehxw3 umR6EThYAbQUPDB5AkAcm87lKW7Vv10zBPIp+6/FcfcH5UaXyvsspXzWUU28SnYEeEDr2yZg 9ky5+thS7zJBQhJqY0BNoSq/7AxSheFGW98fc9c7J45RWHyRBzi2BylCVyARcdWFvmbrW66E 5NPI+xMZTSf1QGPjDcSOvcMKZBwnNov2tswSpH5LkEosYmk8zlbi7PL1y3EnGRwac5focU8D YLwdjy5DW2bg0VPqVLNtMVpPmmZY8EOQQ/BgNCO7+QCEqwcvNFWcU0d1qW+u1OXOlBF+y24k RziZaiM6cBf0qVpwpXRF5tcCzWOKd/cUPqC9CaxuY9safLNKcL/iBMHmGL4Pgh5PaojZPovr O6j6OXI5ULiuKo6d0v7mJPbTqlA2piUbdpta8nyKCFXoDuGVMrS+CA8wmGfK6IYoOMFs4PjD 0G9ZdCrfNEYZ8ZFyTcHI2JCGhIaEOLsYr2muSq5qO+WBwMA1RDcaumq7mLtcXoRYxpg10cS0 eMok63GChFkQIVw6NssB/BjCpt5KRn+U6Y8bMX4vjTeAmTAbpZufFf9vUJI1N0JIiDs/AXGD VbtVxb5bg+utbuOwNwxX0laoEgMFHgk6QUvVht1xjO14gxWyEYXI+MHKokLENdYn0QeEX0+i C7lNAMfNMk2YdiIndgQLjgussdzy9Hi4uvEGwE=
- Ironport-hdrordr: A9a23:OqgNr69yNZ79n37gP1Vuk+ASI+orL9Y04lQ7vn2ZKSY+TiX4rb HLoB1/726OtN9/Yh4dcLy7VZVoBEm8yXcX2/h1AV7BZmfbUQKTRekInPPfKn/bexEWndQtt5 uIHZITNDS9NykYse/KpDKjCt4lzZ2t+LvAv5a4815dCTpxcqll4kNDBh+cCVAefnghObMJUK GH/8JCqn6bc3INYq2AdwA4Y9Q=
- Ironport-phdr: A9a23:XWSOwhAR6xJNYZ6KX3boUyQUg0gY04WdBeb1wqQuh78GSKm/5ZOqZ BWZua8wygaVDM6CsqkMotGVmp6jcFRI2YyGvnEGfc4EfD4+ouJSoTYdBtWYA1bwNv/gYn9yN s1DUFh44yPzahANS47xaFLIv3K98yMZFAnhOgppPOT1HZPZg9iq2+yo9JDffQVFiCCgbb59K Bi6ohjdutQYjIB/Nqs/1xzFr2dHdOhR2W5mP0+YkQzm5se38p5j8iBQtOwk+sVdT6j0fLk2Q KJBAjg+PG87+MPktR/YTQuS/XQcSXkZkgBJAwfe8h73WIr6vzbguep83CmaOtD2TawxVD+/4 apnVAPkhSEaPDM/7WrZiNF/jLhDrRyhuRJxzY3ab4ObNPVwY63Scs8VSHFbUcpNTSFMGJ+wY pENAucHIO1Wr5P9p1wLrRamBwajHuXvyjlJhnDq3q0xzuQvEQbc3Aw7A9IBrm7Up8jyOaYSS ++1yq/IzTTfYPNVwjr86IbIchc7ofGXQbJ/b9DRxVMyGAzbl1idr5HuMDyJ2OoXqWeb8/ZgW vy1i24hswx8rCaiyMcwhoTLhI8Yy1PJ+ThnzIopOdG1VE12bcOrHpdMqS2XM4R7T8w+T2xmu Ss31qEKtJy7ciYF1pkqxB7SZvqaeIaG5RLjUfyeITZ+hH99d7K/hgqy8Ui9yuLnTMW7zFFKr i9dntnNsHANzR3T5dKdRvtz5Ees3yuE2QPL6uxcPEw5lqrWJ4Q/zrMxjJYfrETOEy7slEnrk qObd0Mp8fWy5ev9eLXpvJqcOpd0ig7gNqQundSyAeQ5MggLRWeb/eW826f58U3kW7pFkOc2k rLBsJ/AOcsUuLS1DBJL3Yo76ha/CSmp0MgAkHUaL19IeAiLg5boNl3UPfz1Dfayj06xnDt1x v3KJrjhDY/MLnjHnrfhZ7F960tExQsz199f4ZRUCrAdL/LwQULwtNLYDhgjMwyv3+boFs992 pkDVm2RGqOZNrjdvkeS5u0zO+mMeJMVuDHlJvQ4//Lul2M2mUcBfam12psacGy3HvN/I0mAf XXshsoBHnwRswolTO3qjUWCXiRJa3azWaI8/DA7B5i8AYfNXID+yICGiXOwGYQTbWRbAHiNF 23pfsOKQaFfRjiVJ5pQmzoCVLOiA6EmzwqyuRWyn6tuKOzV8S4wpJzkzsNp6veVmRxkpm88N NiUz2zYFzI8pWgPXTJjhMiXwGR4w1aHiu1jhuBAUMdU/7VPWxs7MpjVy6p7DcrzU0TPZITBU 06oF/OhBzx5Vdct25kWeU8oCtykiBHI3AK7DbgPjKCGHto4//GUxGD/cv500G2Oz6w9lx8jS 8pLO3ehg/tu/g7VBoXKu1SXkLyxaakGmiLApy+Y1WTbmkZeXUZrVLndG3ASYkyDtdPi+kbLV KOjE5wnMw5Izc+LbLZAZ8fylVxNSbHvNbwyekqXnGG9TVaNz7KIN8/xfnkFmT7aEA4CmhwS+ nCPMU4/AD2gqiTQFm4mE1WneE7q/eRkzRHzBkYp0wGHaVFg3Lup61YUg/KbUfYawrMDvm8ot Tx1GF+329+eBcCHokJte6BVYNV151kityqRpgV7OJ2rLIhziFkEaBh6pQXi2lQ/C4lNl9Qrs GJ/1BB7euqT1FJMcS/d3IilY+2KbDOsuknyNeiPgA+NtbTesr0C4/k5tVj56QSgF055tm5iz 8EQyHyEoJPDEAsVV5v1FEcx7Rlz4b/AMUxfr8vZ02NhNa6sv3rMwdUsUaE0wxCmftxcGLKKE xXpD8AAQcSjYr9P+RDhflcfMeZe+bRhddKvcf2H062DLehnhim6gH4B7I03gQqcsiF7TODPx ZMMxfqVixCGWznLh1CkqsnrmIpAaFn+B0KHwDP/TM5Ub6x2JsMQDHu2Ztaw3pN4joLsXHhR8 BiiAUkH0YmnY0jaY1v41AxWnUMZxB7v0TqxyTp1mDIBv6SYxjfSzv6keBdPNmNQRWZkhEvhO sDt341cBhbuNlV30kL/uw7z3OBDqb56LnXPTEstHWC+NGxkXqaq9/KDb8NJ9JI0oHBSWeW4b 0qdT+21qB8b3iX/WmpGkWlrKnfw5NOgwkI80TjDfxMR5DLDdMp9xAnS/onZTP9VhX8dQTVgz CLQHh66NsWo+tOdk9HCtPq/XiSvTM42E2GjwIWeuS+8/WAvDwe4mqX5i9ThFwkx0gfq2d5wT jnFtlDwb8O4ssbyefIiZURuCFLmvoBrE4d4k4AzrIAe3mIBmpiPu3YK2zSWU50Tyef1a3wDQ iQOytje7V3+2UFtGXmOwprwSnSXxsYyL8n/eG4d3TgxqtxbEKrBpqIRhjN7+xDryGCZKeg4h DoWzuEirWIXk/1c8hR41T2TW/gXDQFONCjo3Xxk9viYq6NaLCaqeLm0jw9lmMy5SaqFukdaU Wr4fZErGWlx6N9+ORTCyi+77IasY9TWYd8J03/c2x7dk+hYLo4wnfsWlGJmP2z6p3gs1+88i 1Rnw5i7uIGNL2gl8ri+B1ZUMTj8ZsVb/T+I7+4WhsGNw4WmBYlsAB0LXZ7hSfOhVi8YuO78L w+FHXswpzbTGLbSGxOe9FYzr3/LFMPOVTnfL30YwNN+ARiFcRUP3UZOAnNjw8B/T1r0l6mDO A9j6zsc50D1sE5Jw+NsbFzkV3vH4RyvcnEyQYSeKxxf6kdD4V3UOIqQ9LEWfWkQ85u/oQiKM mHeaR5PCDRDS0WCAVHoPZG/697a6PSVHKyyIrGdBNfG4fwbTPqOyZ+1h8F++C2QM8yUInR4J /0630NHXHk/Bs7UgS4XQica0S7AJZ3+xl/06mh8qcax9+7uUQTk6N6UCrdcBt5o/gi/naaJM +P4bMlRODhfzIgQyGWOxLVNhTb6agludjykFbUJ8zPHQbjLgqZcAlgXZnErXCOtx7My2RNWJ cPBzN/4hOYQsw==
- Ironport-sdr: 63e35990_Depuity4RsT8aIYgUcF0f3nvYHYqNPj+WHxOKyfpgeWeswj 7wH2TXJsdogwVQaqc/6vcyUl7Zfd2+bHs/UBGpQ==
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+.