The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Le 18 janv. 10 à 11:48, Gyesik Lee a écrit :

> Dear coq-users,
>
> I have encountered a problem with positivity condition when I was
> trying to define an inductive type.
> Here is a simplified version:
>
> ===============
>
> Fixpoint toto (n : nat) (X : Type) : Type :=
> match n with
>   | 0 => X
>   | S n => nat -> toto n X
> end.
>
> Inductive tata (n : nat) : Type :=
> sem : toto n (tata n) -> tata n.
>
> Error: Non strictly positive occurrence of "tata" in
> "toto n (tata n) -> tata n".
>
> ================
>
> You can easily see that the positivity condition is satisfied.
>
> Is this a Coq restriction? If yes, is there a way to get around it?

Dear Gyesik,

Coq is not able to analyse [toto] to see that [X] occurs only in  
positive
positions. You can use currying to get around it in that case:

=============

Fixpoint totoc (n : nat) : Type :=
match n with
  | 0 => unit
  | S n => nat * totoc n
end%type.

Inductive tata (n : nat) : Type :=
semc : (totoc n -> tata n) -> tata n.

Fixpoint toto (n : nat) (X : Type) : Type :=
match n with
  | 0 => X
  | S n => nat -> toto n X
end%type.


Fixpoint toto_totoc n X : toto n X -> totoc n -> X :=
 match n with
   | 0 => fun f tt => f
   | S n' => fun f tup =>
     let (hd, tl) := tup in
       toto_totoc n' X (f hd) tl
 end.

Definition sem n (f : toto n (tata n)) : tata n :=
 semc n (toto_totoc n (tata n) f).

===============

-- Matthieu