The Coq mailing list

[Lionel Elie Mamane <lionel AT mamane.lu>]

On Tue, Oct 22, 2002 at 03:51:28PM +0200, Eduardo Gimenez wrote:

> No, you can not do case analysis on the type you are introducing in the
> definition of the type itself (I can hardly imagine what the semantics of
> such construction could be :-).

Well, let's look at my example:

Inductive Example : Type :=
   Example1: nat -> Example
 | Example2:
  let check = [e:Example]
    Cases e of
     (Example1 n) => (lt (S (S O)) n)
    |(Example2 e p) => false
    end
  in
 (e:Example) (check e)-> Example.

This means that the constructor "Example2" awaits:

 0) an Example
 1) A proof that this Example satisfies predicate "check".

In other words, an Example is either:

 0) An Example1 of a natural number
 1) An Example2 of an (Example1 n), with n being at least 2.

The predicate "check", intuitively and "humanly" is well-defined,
isn't it? And isn't this semantic "reasonable"?

> 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.

It is the same as

Inductive Example : Type :=
   Example1: nat -> Example
 | Example2: Example -> Example.

except in the former the user chooses a name for the argument of
constructor Example2. It is the same thing happening as in the
ultra-classic example of natural numbers:

Inductive nat : Set :=
   O: nat
  |S: (p:nat) nat.

(
 which is usually written:

 Inductive nat : Set :=
    O: nat
   |S: nat -> nat.
)


May I remind you that (AFAIK), "P -> Q" is a syntactic shortcut for
"(x:P) Q", with x a "fresh" variable not occurring in Q?

> By the way, what is the intended meaning of the definition of the type
> Example?

It was the simplest I could think of that called for the construct I
wanted, for a more intricate type (that has only one constructor).

You may think of "Example1" Example's as generic Example's. An
(Example1 n) is called "pure" (or clean or ...) if its n is at least
2. An (Example2 e p) is then a "proved pure Example's".


Thank you for your time anyway,

-- 
Lionel

Attachment: pgpEp7kvVrr21.pgp
Description: PGP signature