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: Li-yao Xia <lysxia 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 11:01:23 -0400
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=lysxia AT gmail.com; spf=Pass smtp.mailfrom=lysxia AT gmail.com; spf=None smtp.helo=postmaster AT mail-qt0-f179.google.com
  • Ironport-phdr: 9a23:AiAFjh2cXsd3dJiSsmDT+DRfVm0co7zxezQtwd8Zse0TK/ad9pjvdHbS+e9qxAeQG9mDtrQc06L/iOPJYSQ4+5GPsXQPItRndiQuroEopTEmG9OPEkbhLfTnPGQQFcVGU0J5rTngaRAGUMnxaEfPrXKs8DUcBgvwNRZvJuTyB4Xek9m72/q99pHPYwhEniaxba9vJxiqsAvdsdUbj5F/Iagr0BvJpXVIe+VSxWx2IF+Yggjx6MSt8pN96ipco/0u+dJOXqX8ZKQ4UKdXDC86PGAv5c3krgfMQA2S7XYBSGoWkx5IAw/Y7BHmW5r6ryX3uvZh1CScIMb7S60/Vza/4KdxUBLmlTkJNzA5/m/UhMJ/gq1UrxC9qBJw2IPUfIKYOeBicq/Bc94XR2xMVdtRWSxbBYO8apMCAewAPepBr4jyvVwOpga/CgmtHuzk1zhFhnv23K0h3OUhEBvJ0RcvH9ILqnvUrdH1OL0OXuCyyanF1DPOZO5V1zfl8IXEbAwtrPWWUb9zccfd01cjGx7Eg1mKtIDoPTeY2vwTv2Wa8+ZtV+eii2AopgxzvjSiw8Yhh4zGi44J1lzE+yB0z5ovKt22SkN2ZNCpHZVetyGUMoZ2TN0tTH1ytys/0bILu4W0cSwMxZ863RDQceaHfJKN4h/7VOaePzN4hHV9dbK6nRmy8EygxvTlVsmozFpGtyRFnsTOu30JzRDT5c+HSvxy/kelxzmDzRzc6uZBIUwslKrbLYAuwqIom5YNrUjOGjX6lUb2gaOMaEko5+ml5/76brjkopKQL4p0hRv/MqQqlMy/G+M4Mg0WUmif+eW8z7Li/UzjT7hRgf02l7PWsJHeJcgBuqG5BApV3p456xmjFzemzMgYnX4fIV1ZfxKHlpHlNE3KIPDlFviymE+skTdux/DeJLLtGJTNLn7ZkLfgZ7lx8UBcyBBghexYsplTE/QKJO/5ck73rt3RSBEjYCKuxOOyLNQ4x4oZEVKOC+fNNLLJoV6Bzu0qKuiIIoQSvWCueLAe+/fygCphyhcmdq6z0M5PMSHqLrFdO0ycJEHUrJIEGGYOsBA5SbWz2lKHWD9XIX21WvBlv21pOMedFY7GA7uVrvmZxi7iR89ZY2lHDhaHFnK6L9zZCcdJUzqbJ4paqhJBVbWlTNV/hxSntQu/0qY/a+SNpXxeupXk29x4oebUkENq+A==

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