The Coq mailing list

[Julia Belyakova <julbinb AT gmail.com>]

Hello,

I see, thank you!

--

Kind regards, Julia

чт, 14 июн. 2018 г. в 17:24, Maxime Dénès <mail AT maximedenes.fr>:

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