Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Suspicious instance of non-strictly-positive-occurence error

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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


Chronological Thread 
  • From: Julia Belyakova <julbinb AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Suspicious instance of non-strictly-positive-occurence error
  • Date: Thu, 14 Jun 2018 17:02:53 +0200
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=julbinb AT gmail.com; spf=Pass smtp.mailfrom=julbinb AT gmail.com; spf=None smtp.helo=postmaster AT mail-pl0-f47.google.com
  • Ironport-phdr: 9a23:YwhAZxYhQi9VS2mXPDhkPmL/LSx+4OfEezUN459isYplN5qZocS9bnLW6fgltlLVR4KTs6sC17KL9fi4EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQpFiCa9bL9oMBm6sRjau9ULj4dlNqs/0AbCrGFSe+RRy2NoJFaTkAj568yt4pNt8Dletuw4+cJYXqr0Y6o3TbpDDDQ7KG81/9HktQPCTQSU+HQRVHgdnwdSDAjE6BH6WYrxsjf/u+Fg1iSWIdH6QLYpUjmk8qxlSgLniD0fOjE2/mHYiMx+gqxYrhy8uRJw35XZb5uJOPdkZK7RYc8WSGhHU81MVyJBGIS8b44XAuQFIOZYq4j9qEETphajGwasAOPuxSVLhn/xw601yfkqHAbE3Aw9G9IBq3XUrNPuO6oJXuC1ybPHzTTHb/9MxTj9743IfwknrPqRXrxwadLcxVczGw7BlFmdqozoMymI2ukMr2SX9eVtWOCphmU6sQ9+uCKvyd0pioTRhoIa1FTE9SJhzYYwP9K4SUp7bce8EJtUqy2WLoV2T8wgTm1ytyY6zboGuZG/fCcU0pgo2xnfa/mff4iJ5BLsSvqRLC9miH55fL+znRW//Ei6xuHhV8S4zExGoyVHn9XUs3ACzR3T6syJSvtn+Ueh3C6C1wLO6uFAOk80lKzbJIU6z74/k5ocq0XDHivslErqi6+Wc10o+vK05OT/frXmupicOpdohQH5K6Qig9CwAeAlMgcVRGWb4uS91Lj7/ULjWrlKj/s2krPYsJ/AP8gbqLS5UEdp1dMo7A/6BDO72vwZm2MGJRRLYkGplY/sbnPTJPHxRd2yh0WlkzB1zriSPKDlCJTLJFDMlb7gefB27EsKm1l79sxW+58BUuJJG/n0QEKk7IWJXC98CBS9xqPcMPs404ofXWyVBarAafHdtFaJ4qQkJOzePdZJ6ga4EOAs4rvVtVF8gUUUJPD70p4eaXT+FfNjcR3APCjcx+wZGGJPhTIQCeznjFrYDGxWbne2Gro4vnQ1VN3gAoDESYSgxreG2XXjEw==

Perfect, this will do! Thanks a lot!

--
Kind regards, Julia

чт, 14 июн. 2018 г. в 17:01, Li-yao Xia <lysxia AT gmail.com>:
The match somehow gets in the way of strict positivity. Replacing n1
with (fst nn) makes Coq accept the definition.

Li-yao

On 06/14/2018 10:36 AM, 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



Archive powered by MHonArc 2.6.18.

Top of Page