coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Suspicious instance of non-strictly-positive-occurence error

From: Maxime Dénès <mail AT maximedenes.fr>
To: coq-club AT inria.fr
Subject: [Coq-Club] Suspicious instance of non-strictly-positive-occurence error
Date: Thu, 14 Jun 2018 17:23:55 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=mail AT maximedenes.fr; spf=Pass smtp.mailfrom=mail AT maximedenes.fr; spf=None smtp.helo=postmaster AT 5.mo5.mail-out.ovh.net
Autocrypt: addr=mail AT maximedenes.fr; prefer-encrypt=mutual; keydata= xsFNBFRYkvgBEAC0Zot4S5lKkhzYK68sSb69wVyEsugASVeWPHjVpxgFG44BLFB7Te0zWHjg jK76yCUmDdpKFdIufw5PQr+3At/8G75Y3x+dGC2rg+31fPAUJvp/AfrMloH+qd+tqxbaKjtC kymLGE01Yj8m3xaV7bN9wuYwL03+staTESJFVm3CZwNAqFgIZCG6KgBGT93ybUgbPYRrTv+n Oleags7nHdPubX6SAWbZVhuweHCwiooRBVSjzyxuhTtDuAwmeZ+ca4WE3IkOWmJmq4KbCeij HJ9B2b6qSopM19dq+iBByPu+LpBCwSA9Nr9hL1XRnoNngwf0OtJ0CNiKjKsNKlAmsCHw/o48 0IoiKP40sH+zsNFeNepbIqILPaWDvTOFvtHc9FDcH2X9NHaWx73GckMzi2z5Ty4tVoEU4Tap JlDVaKWyhvtHRwxbekgk3Vq3PcKKhcLy/xsbyknVLFw8UbFj+sYwGPrzb7j2WhpisfSct3Ii vxv2FUzM3etqM+tsJ/1Oq8u1A5lQ7lSEZmsCQdeyzMXmrUgXAEZvcx5anmTlNR3TjoG6sOxm axp9f/zgZmr9pV/FRq9tLIu8Eqv8+HqeUcHfxICcnXHVPz2x1h6H6ft45h9LGPEi1riCiZZ5 eFnq/epTkpQF411fo7sY1osaZ0Sp9yrHIPAtmJT40tmPQflSYQARAQABzSZNYXhpbWUgRMOp bsOocyA8bWF4aW1lLmRlbmVzQGlucmlhLmZyPsLBdwQTAQoAIQUCVFiS+AIbAwULCQgHAwUV CgkICwUWAgMBAAIeAQIXgAAKCRAWr2+lkXvTQPz8D/4lUpXfqOp0ZVc9WTBr8bDxHE334Bd9 FnekcYCRrmOUE76oMsK1/MhoKCEmr5bdyn8oh/r2GsNTWB1lsHpTEjYc2Sf17LNW2ncVu4OB EsD38chB9aTEev5Pc2jAA7l/WF8ceF5mkt6OjWrBfDp6yBfXwrzDfdzLixVHVyJUYA/04T7U JZc7Rjz1CdXE2wg8KL7+uq/QGc5TCPPQmlpdXJYpDgK7FtJasRoh34/pVFGHXXA1PnCe+IIL 52DynkF+bCL3sWk8A71ebUkyTO6ytqUKYafCPjrrGv4y13O+/2QcB3Iz4gDiKgvL8FWMhmhJ QF5C8BucOE87JWb5nJmq+Gs13NVofYMpmI+DDaBNJ6ns/sbR68vRfoXEhr0adPDLZOohZKJM Lu6WTjyFNNOgj1jgG0I00+tctmtW00W+U3oi36vbUXalbi5WPlIBpIXkjI9p7xoHe1mJwN40 jn/ExEXnY9uZ4H/NorJ7OzGdEOlz+ZpkcBpW34N5GZfOg7UXScA3tAFPyWcxCKsxAti0sRAR fIQXkxwt+BTBMm5m7n+wxe/2sf+xxO6AYyedWRbLaTCexJEw4Tx4+hocFT8lD6y/cGPORcak AkoWz2aiGQK07gbJ5dxymCP6g0Xcl8CloXodwV124G2++eQpucydK4BRFDTyJLJJNAR3nkei s1BBj87BTQRUWJL4ARAAqLecjPrMCx42r822nQT6e8GTHrFKwppkRqSXAucAZ4ICJ1YoT2Hy z+DtehqEV5IdIDGRivKvQYQF1Yz2NpgO7vfmB1M8ZsxyTyFeQiBkFIb5BKVhUk0xat2Xjgmb PJ59GsEbH5DCIrUqFRRGshjgul/z0adUF5DjFyuqo5TMAJdgXtJbTzmCTXoBwJmNuaUHwieK s47K9pmnnaUnkSy+CDTjtOihNeSx+lmrzieo8OyYuwvY1V1av+dJlF6YF7D5X9gHUAMsSypq pdQX0PhUZ4XheCiC0HojVzT3NEEkZ3LjuAGD7+1yaWNepGgqFqiaGEq4ihjihbvW3rCO84RS 9rSb6F7Eru7HMDUKLmUDc37GhOC0xcrTJ5zZ0CwTaM6V2P2n/FxOXEoKwRVGdAAWvh521N7k pYQpGsamfCzl8ruaEf/IhksPZiyJC95W5jXl98UDf6WNm/xKXwF60oK56iSBj+YWmUgjAzGf XRCJyiXAlMtBhErkije2iIqKVungP3N4IPEhmDOLVa9BsdXAsptkWSmWzvJA+z0A52hta0/2 B71dreoGFVnmLWWSCR+O6P9yivnfEKq75QPjBLj6xw6nXxtyhyrVT2/xOy1Osvf2mM7Gx9wR Q0Ktv7fjX2AyIrcvR3r3/RgsDA3/elqkcrY1hdu+NkOHOKtME43htXsAEQEAAcLBXwQYAQoA CQUCVFiS+AIbDAAKCRAWr2+lkXvTQNfiD/0fD2LeHa/7Vq7ClzMgjaCm5Jt2afGZi9xrD+Z8 4/wlVjFI8TZsYoiq6OTbvn6eNFE7J0wYpAouYS6GP/Ga+e/eo9Hm3BeK9+1gP0QSfwcA1+ci n+zvD5q58Movy7qo4BOoJM2eb8FpdyeloViTUlxgqocZK35ewTK0q3JcMlSZZxdOvCol3F8r CWkXqHlJoA9dL16VxBbxmT57ogqgpOFfIbc9PHMjQaNY5BWLz1+qj4bXN5UXvibP97tas1LE 4OilGPIW/ZOMItfVcxi9//huyTJt0l4lRJRochpmppItYeDs6tFyFu4XpEgUbAXwTnANqHr2 N0OSZT3j+BTMgVrs5sUgjMlqNJkMKjZmkIuSoIZbtYHfQgSY2VBPImLyWpu+XdzjBwFbuMJK 8q9tvgG2ydZCDbpC6Bi0FF+WKmZZqSkqgIFjUOkLGh624JQLbU/aezYrrhORDGEIAGtHbdn3 pC1fcAJHwI3JpRpNwou+lc8SORjUoTpSOmc5C0qWu0P7D1Y3k8gFngN/c42TX6eyyVpQw44h A6bxBs56DrE8OPyt15lveeMxT/0scd/MJlFJY/Dy+XelA0Utt0SUgSqI+TaL2eTlwNCmhNL+ ShCTVRcfb1UFlSA+GyURCLoUjrbukm7GS0pKhF+O9eCj1DkYEdi9NTjs83wKHHYu8CspWw==
Ironport-phdr: 9a23:VRpl5RcPbReFl/JDfHAklcMolGMj4u6mDksu8pMizoh2WeGdxcu/Yh7h7PlgxGXEQZ/co6odzbaO7ua4ASQp2tWoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6nK94iQPFRrhKAF7Ovr6GpLIj8Swyuu+54Dfbx9HiTahYb5+Ngm6oRnMvcQKnIVuLbo8xAHUqXVSYeRWwm1oJVOXnxni48q74YBu/SdNtf8/7sBMSar1cbg2QrxeFzQmLns65Nb3uhnZTAuA/WUTX2MLmRdVGQfF7RX6XpDssivms+d2xSeXMdHqQb0yRD+v6bpgRh31hycdLzM38HzZhNJ+jKxYrhyuqRNwzIzIb4+aL/d+YqDQcMkGSWZdUMtcVSpMCZ68YYsVCOoBOP5VoY7nqFoBrBu+ABejD/7hxDhSgH/xxLY62PkmHAHDxgMgHtYOvW/RrNrvO6YSUOW1w7fVwjrdafNZxyz95JLGchA7uPyBW697f8TWyUkqDQzFj1OQpJTqPzOUyuQNs3Wb4PF6We2zjG4nrgd8qSWsyMc0koTEhYAYxkrA+Ch62oo5ON+1RUBhbdK5DJdduTmWO5Z4T84hWW1lvCc3xqcYtZKnYCQG0okryh3ZZveaaYaH+AjjW/yUITpghHJqZra/hxGq/EWg0OH8U8603VZQoipAiNbMt3QN2wXU6siaVvtx5ECh2SiP1wzJ7OFLP1w0mbLaK54n3LEwioIevEfBEyPsnEj7j7Waelgm9+Wm8ejrf6nqq5GEO49xkA7+M6AumsKlAeQ/NwgDR22b9v691L3n5kD5Ra9Fj/I3kqncrp/VONoUpqinDA9OyIoj5Qy/Ay+80NsEhXkHME5FeBWfgof1PFHOOen0Auu7g1Sxizhm3OvGP73kApXVNHfPirbhfbBn605d0gU/195f54gHQo0Gdfn0Qwr6sMHSJh4/KQ29hej9W/tn0YZLfGufA6qUeI9Tt9+TrrYqKuiITIocqDf4JvQo4fP1y3EjzwxONZK11IcaPSjrVs9tJF+UNCK104UxVFwStw97d9TEzViLUDpdfXG3Bvxu4zgrCYerAYrFS5vrjqbThX7nTK0TXXhPDxW3KVmtb5+NAqlebSuCI8psnjECWKPnRZVzjUjz5j+/8KJuK6/vwgNdtZ/n04IptbCVkBZvszl9DsDY1HyRCWZqniUOSiNkhK0=
Openpgp: preference=signencrypt

Hello,

This problem has already been reported here some time ago:
https://github.com/coq/coq/issues/1433

Jason even gave an argument for the validity of the extension, but as
far as I know it hasn't been validated by theoreticians yet. If proved
sound, it should be easy to implement (I could do it).

Otherwise, as suggested by Li-yao, you can use defined projections.

Maxime.

On 06/14/2018 04:36 PM, Julia Belyakova wrote:
> Dear all,
>
> I want to define a relation with the rule similar to FOO_4 (see below).
> However, I got an error _Non strictly positive occurrence of "foo"_.
> This does not look like a non-strictly-positive occurrence to me, and I
> also don't see a big difference between FOO_4 and FOO_3. The problem
> stays if replace _let_ with _match_ for the "nn" argument. Is it a
> non-strictly-positive occurrence or is it a bug?
>
> I use Coq 8.8.0.
>
> Inductive foo : nat -> Prop :=
> | FOO_1 : foo 1
> | FOO_2 : forall (ns : list nat),
>       Forall foo ns ->
>       foo 3
> | FOO_3 : forall (ns : list nat),
>       Forall (fun n => foo n) ns ->
>       foo 4
> | FOO_4 : forall (ns : list nat),
>       Forall (fun (nn : nat*nat) => let (n1, n2) := nn in foo n1) (zip
> ns ns) ->
>       foo 5
> .
>
> where "zip" is defined as
>
> Fixpoint zip {A B} (xs : list A) (ys : list B) : list (A * B) :=
> match xs, ys with
> | x :: xs', y :: ys' => (x, y) :: zip xs' ys'
> | _, _ => nil
> end.
>
> --
> Kind regards, Julia

[Coq-Club] Suspicious instance of non-strictly-positive-occurence error, Julia Belyakova, 06/14/2018
- Re: [Coq-Club] Suspicious instance of non-strictly-positive-occurence error, Gaëtan Gilbert, 06/14/2018
- Re: [Coq-Club] Suspicious instance of non-strictly-positive-occurence error, Li-yao Xia, 06/14/2018
  - Re: [Coq-Club] Suspicious instance of non-strictly-positive-occurence error, Julia Belyakova, 06/14/2018
- [Coq-Club] Suspicious instance of non-strictly-positive-occurence error, Maxime Dénès, 06/14/2018
  - Re: [Coq-Club] Suspicious instance of non-strictly-positive-occurence error, Julia Belyakova, 06/14/2018