coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Murali Vijayaraghavan <vmurali AT csail.mit.edu>
- To: coq-club AT inria.fr
- Subject: [Coq-Club] Understanding non strictly positive occurrence error
- Date: Wed, 30 Apr 2025 23:15:12 -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:ocYCeKn9LEO+iTdSq3KSyHPo5gwaIkRdPkR7XQ2eYbSJt1+Wr1Gzt xJOXDqHaf7cNmTzLYskOozgoBgOvcfdyIdiS1ZkqCoxRltH+JHPbTi7BhepbnnKdqUvb2o+s p5AMoGYRCwQZiWBzvt4GuG59RGQ7YnRGvymTrSs1hlZHWdMUD0mhQ9oh9k3i4tphcnRKw6Ws LsemeWGULOe82Ayaz98B56r8ks14ayu42tA7jTSWNgS1LPgvylNZH4gDfrpR5fIatE8NvK3Q e/F0Ia48gvxl/v6Io7Nfh7TKyXmc5aKVeS8oiI+t5uK3nCukhcPPpMTb5LwX6v4ZwKhxLidw P0V3XC5pJxA0qfkwIzxWDEAe81y0DEvFBYq7hFTvOTKp3AqfUcAzN1PA2cEEqwz2t1uAGdF1 swDLRU1fEic0rfeLLKTEoGAh+wkMdXkO4IZtSs4l2ifBu0vQJSFRqTWo9JUwV/chOgXR6aYP JJfM3wwPHwsYDUXUrsTIIw7gf2hgnjXeCZRqVbToKsrpWXf0WSd1ZC3aoKPJIHWFZ49ckCw4 UbL/W2mLzMjK/eAygiOy3ymubD/tHauMG4VPOTlr6Ux6LGJ/UQYDwRTXl+mq9Gim0umUpReL VYV82wgt8APGFeDScThUBq5pnHe5kRFHdFLGuw+rgSM1uzZ7xvx6nU4oiBpSdMAhuAXbhwRz 16PlPDZHjlKiK/NVifInluLlg+aNS8QJG4EQCYLSwoZ/tXuyL3faDqSEr6P94bo07XI9SHM/ tyckMQpa1wuYSMj0Lin8lfGhT32/sKQCAUu7wTTGGek8kV0aJPNi22UBbrzsKoowGWxFAPpU J04dy62t7pm4Xalz3flfQn1NOv1j8tpyRWF6bKVI7Ev9i6251modp1K7Td1KS9Ba5lYJ2eyP x6M4lwNtPe/2UdGi4cqOOpd7Ox3kcDd+SjND6i8gidmOMMvKlPZoEmCm2bKhDGwyyDAbp3Ty b/CLJ/3Vh72+IxixSGtTuwdzKQm2jwljWLVXoz60wm73PKZajaJRLwFNlyKae8ohJ5oUy2Im +uzw/Cikk0FOMWnO3m/2dBIdzgicyNkba0aXuQMLYZv1CI9Qzl5U5c8ANoJJ+RYokiivr6Zp SrsAhcDkQCXaL+uAVziV02PoYjHBf5XxU/X9wR1Vbpx8ylyMdSc/+0EeoEpfLIq0uVmwLQmB 7MGYsiMSLAHADjO5z1XP9G3oZ1AZSabo1uEHxOkRzwjIL9mZQjCoeH/ciXVqSIhMyuQtOkFm YOG6D/1e5Q4ajpHMNf3c9OqllO4gmgckrl9XmzOOdhiR3/v+4lLdQ3036Y7DM0SICqewB6Y/ hezOkoarrPju4UercXAtZmZnbiTSsp/AUtoMG3J5pmmNSTh3zSCwK0RdM2qbDziRGfP16H6X tpsztb4K6chjntRlohBT4ZQ0qM14uXwq49gzghLGGvBa3KpAOhCJkaq8NZutKoX4JNkoiqzB 1yy/+dFNYWzOM/KFEAbICwnZL+h0dAWgjzj0uQnEn7l5SNY/Ku1bmsKBkOi0BdiFbpSNJ8p5 cwDu8RMsgy2tUcMA+a81ytR8zyBE2wEX6AZraolOY7MiDcw61R8cJfZWz7X4paOVo12CXMUA ASo3YjMu7cN4XD5USsXNWPM1u9jl5gxqEh07FsdFW+oxPvBpNEKhSN0zxpmYDhR/Bt918BLB lNKLGxwfKWHwCdpjpNMXkeqAABwOyea8U3QlXoMsn/ocE2zcmmUNGEWZOK/3H0Y10l+fTFr2 q6S50i4cDTtfeD3hjATX2w8odPdbNVBzC/ws+H5INa0RLwBfivDvq+iQUEquinXK5o9q2Ofr NY74dsqT7PwMBAhhpESCq6Y5Ow2cw+FLmkTesNR1voFMk+EcQ7jxAXUDV66f/5MAPn48UWYL chKDeAXXjSc0Be+lBwqNZQuEZRVwsFwvMEjf4n1L1Eoq7Gc9zplkKzB/xjE2VMEfY9crtYfG KjwKRS5DW2itVlFkTTsre5FGFaCT/sqWQne5N2xocI1T88tkec0akwj8KqGj1PMOitdwh+kl gfiZajX8u9c9bpRj7bcSqVuOgHlBu7wBcKp8R+yuetgddngE9nDnCJLp0jFPzZ5B6owWdN2p O+rsNfIw17Pg7Jud2XnmJW6NrJo4P+qV7F9KfPHL3h9nAqDVvTz4hAFxXuKFJxRnP5Z5eilX wGeasCgUfI0AvBznGZ0bQpaGDYjU5XHVL/q/36Bnq7dGyoj3hziB/L5033QNEVwVDICYr/6A S/K48ee3MhS9tlwNUVVFsNdIsFKJXH4UvEbbPz3jz6TC1eojn6kurfPkRkB6ynBOkKbEfTVs I70eRzjSCuc4K347slVk4hXjC0lCHxQheoRfEVE3/VUjzu8LnANLMVDEJEgJ6xXrBfP18DDV GmQVFchNCTzY20VO1G0qtHuRRyWCeEyK8/0bG5htV+dbyCtQpiMGv19/yNn+G17YSbn0PrhE 9wF53nsJVKk9/mFnwrICiCT2o+LB882x07kPWj6jtD9BBcYDu9SjiUnFxFEVCiBFsDR0kjHO ADZgIyCrF6TESbM/QRIIha52y31eBvk1DwpaWGKwcqZtomGpAGF4OOqIPn9i9Xvc+xTTIPjh hrLq6+l6Huf23hVvKo1/d8lnMeYzB5N8teSdMfeeOHZo018BqnL8S/PcerjgfzOIDJiLm4=
- Ironport-hdrordr: A9a23:JshZaqsLc/Y0LggSofvAj2rS7skDq9V00zEX/kB9WHVpm62j5r mTdZEgviMc5wxhO03I9erhBEDiexLhHPxOkO0s1N6ZNWGN1VdAR7sSircKrQeQfRHWx6py0e NOf6BiFMb9FzFB/KPHCcqDf+oI8Z2o9KipgKP51HdiTQZjbuVF4x1iAgiWVm1aLTM2Z6bR2K Dy2iOPnVSdRUg=
- Ironport-phdr: A9a23:s593ZR2WJ39b860ksmDOuA4yDhhOgF0UFjAc5pdvsb9SaKPrp82kY BeFo601xwWXDdWBo9t/yMPo8InYGlY8qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpV O5LVVti4m3peRMNQJW2aFLduGC94iAPERvjKwV1Ov71GonPhMiryuy+4ZLebgtWiDanfb9+M Bq6oRvQu8QVgoZuNLs6xwfUrHdPZ+lZymRkKE6JkRr7+sm+4oNo/T5Ku/Im+c5AUKH6cLo9Q LdFEjkoMH076dPyuxXbQgSB+nUTUmMNkhpVGAfF9w31Xo3wsiThqOVw3jSRMNDsQrA1XTSi6 LprSAPthSwaOTM17H3bh8pth69dvRmvpQFww5TMbY6aNPRwcKDTc84ES2VdRcteTTBND5mmY ocTE+YMP+BVpJT9qVsUqhu+ABGhCuTyyj9SnHD22aw62PkuHgHH3gwvBdIPv27OrNrvO6cSU fq6zLfSwjXFcvhb3in96I3VchA7u/6MWbNwfNHNxkk0DQzFj1GQpZbgPzOUyuQBqXaU4Pd9V e+2jWMstg5+rCS1yMg2lonJmpwaykrC9Shh3Yo4Id61Rk50bNOlE5ZdsyOXO5V4TM0sR2xlu yU3x7IatZOlYiUHx5AqywPRZvGbcoWF/B3tWPuPLDp3in9oeLSyjAu8/0inz+3zTMi00FBSo yVZktnMsnEN1wTJ5ciDUPRx5EGh1iiT1w3V9+pKIlg0mLLGJ5I/wbM8jJQevVjZEiPogkn7j qybel069uS07+nreLbrq5+GO4Nqlw3zM74il8OiDek+LwMDQWyb+fmn1L3/40L5WqhEjvw3k 6bHqJ3WOcIWrbOjDQBPyIYs8RO/Ai+m0NsGmXkHK0pIeBWaj4j1NFHOJ/H4DfGwg1iyjDtn2 e3KMqf9DZXWNHfDkbPhcax4605d1Ao/185Q6I9JCr0ZIfLzXFH+tMDAAxMkLQC5wPzrBdth2 o8ER26DGK2UPaDKvV+N/O0vIu2MZIEPuDb6Lvgo/+DujXokmV8HZ6ap2ZoXZWukEfR9OUqZY H7sjs0EEWcLogoyVvLlh0CfUTJLYXa9RLoz5isnB4K+EYfDWoetjaSc0CujBJ1ZenhGCkyQE Xfvb4iLR/AMaDuLLsB9ljwESKOuRpQ61RCusQ/606BoIvDV+i0er5Lj1cJ66/fdlREopnRIC JGW1HjIRGVplEsJQSU31eZxux9T0FCGhI1lmfVcFJRt5vFAQw4gPJHcxvJzDZimRAfcZN6NS X6tWdynBXc0T853ztMTNRUuU+6+hwzOinL5S4QekKaGUcRcGsP02nHwI5w40HPazOw7iFJgR MJTNGqgj6o59g7JBoePnV/K372ye/E62yjAvHyG0XLIpFtRBRB1TL/MWXE3bVDfrNC/40LeC bKiFOdvKRNPnPaLMbACcdj1lRNDTfbnNs7ZZjevnnqqDBKJ7riXZYvuPWAcwGPQBFVX2xsL8 yOgMg4zTjykv3qYDDFqEgf3ZFjw9OBltH6hZkgp0w6NbktujeLvo1genvWdT7UW365CtSs8w 9ltNHC62d+eS9+Jpg47Ob5Zfct4+lBMk2TQqw16OJWkaaFknF8XNQpt7Qvo0F1sB4NMnNJPz jtixRduKa+ezFJKdi+JlZH2NLrNL2Du/RepI6fI01Da2dyS9+8B8vM941nkuQioEAIl/RAFm 5FL1maG75HLJAEJWJP1FEM26153q6ybKigx6oXI1GF9ZLGuu2yK0NYoCe05jxe4Ko4FYOXfT EmoVZJKVK3MYKQwllOkbwwJJrVX/a8wZYa9cueenbSsN6BmlS6nimJO5MZ81FiN/mxyUL2tv d5NzveG0w+ATzq5gk2mt5W9h4VZfzgWH0K00iHlAMhUZ7E0cIoWQzTLQYX/1pBlipjhVmQNv kCmGkkP3M6BcgGbbli72AxMk0kbvDb0/EnwhywxmDYvoK2F2SXIyOm3bxsLNFlAQ2x6hEvtK 4y55zwDdHChdBNh1B6s5EKggrNeuLw6NW7YB0FBYynxKWhmFKq2rLuLJcBVutsktiBeUeL0Z l7/KPa1vR4HySrnHkNV3zk6c3evu4m/khBnwG6QN3d8qnPFdNo4nE2PooeEA6QXgWpOTTIwk TTNA1mgI9SlmLfc34zOtOyzTSPpV5FedzXq0ZLVsSK64WNwBhjs1/u3m9DhDU07yXqijYksD n2O9lCjMtqOtezyK+9sc0h2CUWp7sN7Hts7iY4snNQK3nNcgJyJ/H0BmGO1MNNB2Ku4YmBeI FxDi9PT/gXh31Vua3yTwIesHGuY39FoY9iSaXgf2yZ76sFWTqqY8fYX+Ek96kr9tg/XbfVny 30DzOY04Xobq+oSsQspiCCcHvYfEVQSbkmO31yYqtu5qqtQfmOmd7O9gVF/kd6WB7aHughAW Xz9d8RqDWpq4854Kl6JzGzr59SuZozLddxK/E7x8V+In61PJZk2jPZPmSd3JTe3oyg+0+Bix R12gcPj5tjBcD0rpOThRUcFfjztO5FKqne30+AG2J7Rht7KfN0pGy1XDsK4C6nxVmpU7bO+a U6PCGFu8y3LX+eFW1fZsAA/8TrOC875bS/PfytFlY1rFkvafxYXmBwOFDAq+/xxXgGsz8j8f Eor4zENoFP0t1Naw+ZsfXETS0/5owGlIncxQZmbdl9N6x1aol3SOoqY5/5yGCdR+tugqhaMI yqVfVYAC2ZBQUGCC135W9vmrdDd7+iVAPa/JPrScP2Pr+JZTfKB2ZOo1MNv4T+NMsyFOnQqA ec83wJPWnVwGsKRnDtqKWRfjyXWc8uSvwux4AVws9yw9/XtV1i3v9LJAKBbMNEp/hGqx6qPK q/YhSp0LypZyoJZxXLMz+t6vhZagCVvej+xVLUY4HeXHOSLwukNSUFLOEYRfINS4qkx3xdAI 5veg9LxjPtji+ItTk1CXhrnk92oYsoDJye8MknGDQCFLufjR3WDzsfpbKe7UbAVgv9Tskj6p zOGCUbnPxyIjDDoU1aqMP0KgS2Gdk872sn1YlN2BG7vQcizIAW8K8NyhCYqzKccgW7WOmkdN zcmKxkU6LaL5CJcxPB+BypM4mcvfozm026JquLfLJgRq/5iBC95wvlb7HoNwLxQ9ChYRfZxl UM6S/ZluFinlq+KyyYhXRZT+G4jbGOjulh+NqLY8JYaASyduhkW5GSUTRELu51oBsC948i4J fDEj6vyLHFH8s6S8McBVZG8FQ==
- Ironport-sdr: 6813117e_Mx9AUhFE6c1/6Olyyn9KlMuKo9d1cJaRfeEP+FWvSauxg+f iEJrw97EOPX5lHAmujY/VdiiLzL840HcJtjTKfw==
Hi
I was wondering why the following definition fails:
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
| 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".
| 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), 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
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
- Re: [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
Archive powered by MHonArc 2.6.19+.