coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Positive occurrences below a "match"

From: Gyesik Lee <leegys AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] Positive occurrences below a "match"
Date: Mon, 18 Jan 2010 19:48:45 +0900
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:date:message-id:subject:from:to:content-type; b=Rq7GHzbEcZuYNYlwOzTsxQvQfEUAi/YZ5aBuoDdmVSq1+ci6hluPrnx/Gv72M/kc2j bOJMygLNuqMlEPv/LR7ex1YrAWvW2m12Pzm9GKYJ2StHGmFW1Bz6cgcyS3zNLs5Wy8Lx VEzVZxBIDZoavws3j8+HQtrt5G3imXnHAv9FY=

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

[Coq-Club] Positive occurrences below a "match", Gyesik Lee
- Re: [Coq-Club] Positive occurrences below a "match", Vladimir Voevodsky
- Re: [Coq-Club] Positive occurrences below a "match", Matthieu Sozeau
  - Re: [Coq-Club] Positive occurrences below a "match", Gyesik Lee