The Coq mailing list

["Eduardo Gimenez" <Eduardo.Gimenez AT trusted-logic.fr>]

Hi Lionel,

> The predicate "check", intuitively and "humanly" is well-defined,
> isn't it? And isn't this semantic "reasonable"?
> Thank you for your time anyway,

Written English is a poor language with respect to spoken English, so I 
would like to apologize if you felt that my message was unpolite, it was 
not my intention.

What I meant is that, to me, case analysis on an element of T
pre-supposes that you already known all the constructors of T, that
is, that you already know their type. As Blanchi and Capretta
mentioned, Peter Dybjer has been working on what he calls
inductive-recursive definitions, where you can make mutually dependent
definitions of inductive types and recursive functions on elements of
that types.  However, as far as I remember (but may be I am wrong, I read
Peter's articles too many years ago), his idea was to simultaneously
define T and a function f:T->C, with C a set possiblt involved 
in the definition of T, but not a function of type f:T->Set (or T->Prop). 
What I wonder is how could you extend the notion of positivity in 
such a framework.

[The notion of positive occurrence of T in a constructors of T is a
syntactical notion which is crucial to make sense of an inductive
definition, since negative occurrences lead to logical paradoxes. You
may find a definition of what positivity means in the Coq reference
manual, but roughly speaking, it says that you can not have an
argument of type T->C in the constructors of T].

For instance, shall T be considered positive in the following variant
of Capretta's example:

Example : Set
  ex1: nat -> Example
  ex2: (e:Example)(check e)->Example
check : Example -> Set
  check (ex1 n)   = Example             <=== notice here
  check (ex2 e h) = (check e)->False

In this example, the type of the second argument of Example2 
seems to have a negative occurrence of T depending on the size 
of its first argument.

>> Neither you can do a universal quantification on the type Example in
>> the argument of a constructor of the type example.
>
>This I most certainly can. This is accepted by Coq:
>
>Inductive Example : Type :=
>   Example1: nat -> Example
> | Example2: (e:Example) Example.

I was actually talking about universal quantification *in the argument
of a constructor*, that is, something like:

Inductive Example : Set :=
   Example1: nat -> Example
 | Example2: (Example->Example)->Example.

You can do this in Coq because of the restriction about positive
occurrences of the defined set in its constructors. My comment was
certainly misleading, since there is no such quantification in the
example you were proposing.

Hope these comments help..

With best wishes,
Eduardo.