The Coq mailing list

[AUGER Cédric <Cedric.Auger AT lri.fr>]

Le Sun, 11 Oct 2009 20:16:56 +0200, Vladimir Voevodsky <vladimir AT ias.edu>  
a écrit:

> I am just trying to understand how the "Inductive" works. I also tried  
> the following:
>
>
>
> Inductive ST1:Type := nat : ST1 .
>
> Inductive ST2:Type  := ST1:ST2 .
>
>
> and the first line compiles while both lines together do not, with the  
> message  "Error: ST1 already exists".
>
> Is it right?

Yes it is, have you ever programmed in Ocaml or other similar languages?
If so inductive types are just (recursive) types with constructors.

Constructors can have parameters, but when filled with them always have  
the type you want to define.
Note also that, the inductives are only the smallest set stable with the  
constructors,
for example, nat is defined as
Inductive nat : Set :=
| O : nat
| S : nat -> nat.

here S is a constructor with one parameter of type nat, and when filled  
returns nat.
So you can't define:

Inductive nat :=
| O : nat
| S : nat -> nat
| even : nat -> nat -> Prop.

Since even is not of type nat.

You can't neither define a nat x such that x = S x; since this element is  
not in the smallest set stable with constructors; in particular, any nat  
'n' must have a finite number of O and S in its
definition (in fact it always have exactly one O and exactly n S)

> Inductive ST1:Type := nat : ST1 .

is probably not what you expect:
ST1 is only a Set with one constructor which is called 'nat'.
It is isomorphic to the type unit defined in Coq as:

Inductive unit : Set := tt : unit.
or its friend in Prop:
Inductive True : Prop := I : True.
> Inductive ST2:Type  := ST1:ST2 .
Is also a set with only one constructor, called ST1; but you defined ST1,  
so there is a conflict.
Unlike most languages, in Coq, types are also values, so there is no way  
to differentiate a
constructor and a type if they share the same name.

What you can do is
Definition ST1 := nat.
to rename nat as ST1 and
Definition ST2 := ST1.
to rename ST1 as ST2.

> V.
>
>
> --------------------------------------------------------
> Bug reports: http://logical.saclay.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club


--
Utilisant le client e-mail révolutionnaire d'Opera :  
http://www.opera.com/mail/