The Coq mailing list

[Julia Belyakova <julbinb AT gmail.com>]

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