The Coq mailing list

[Gyesik Lee <gslee AT ropas.snu.ac.kr>]

Dear Vladimir and Matthieu,

thank you for the explanation. I think I have understood the way
although I fear that I might have posted a too simplified example.

Gyesik

2010/1/18 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
>
>
>