The Coq mailing list

[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