The Coq mailing list

[Vladimir Voevodsky <vladimir AT ias.edu>]

1. In this particular example you would get (if it worked) tata (n) = 
emptytype since what you define is a family over nat whose fiber over n is 
freely generated by the constructor (nat^n -> X) -> X and emptytype is the 
"initial algebra " for these constructors for any n\ge 0.

2. it does not work because the left hand side of the constructor is not a 
strictly positive type expression of tata. Strict positivity is a syntactic 
condition.The expression toto n (tata n) is not strictly positive in (tata 
n).  For each individual n:nat of the form S.....S 0 the expression toto n 
(tata n) normalizes to  (nat->(nat->...(nat-> tata n)..)) which is strictly 
positive but for an "abstract" n:nat it is not strictly positive. 


3. To make this particular constructors work you may, for example, define, 
inductively a function nat_n:nat -> Type whose value on n is nat^n (may be in 
two steps first a function Prod: Type -> Type -> Type as Inductive Prod(X 
Y:Type):Type := X -> Y -> Prod X Y. and then nat_n by the rule nat_n(S 
n)=Prod nat nat_n(n)). Then you can write your constructor sem as (nat_n n -> 
tata n) -> tata n .

V.





On Jan 18, 2010, at 5:48 AM, Gyesik Lee wrote:

> 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?
> 
> Gyesik