The Coq mailing list

[Pierre Courtieu <Pierre.Courtieu AT cnam.fr>]

Hello,
First of all your comp type is not a valid inductive type, it should
be more like

Inductive comp : Set := E: list all -> comp

Since you need to define comp and all simultaneously, you need to
define them as mutual indutive types:

Inductive comp : Set := E: list all -> comp
with all : Set :=
   C : prim -> all
 | D : comp -> all.

However I would recommend you to use one of the following instead:

(* 1 *)
 Inductive all : Set :=
   C : prim -> all
 | D : list all -> all.

OR:
(* 2 *)
Inductive comp : Set :=
 compNil: comp
 | compCons: all
with Inductive all : Set :=
   C : prim -> all
 | D : comp -> all.


1 is the recommended choice because you will be able to use lemmas of
file List.v of coq library, but you will probably need to define and
prove induction principles by hand because the default one generated
by coq is not so good (it is not merged with the principle of lists).


2 will produce much better induction principles using this command:

Scheme compind := Induction for comp Sort Prop
with allind := Induction for all Sort Prop.

but you will not be able to use List.v. I would recommend to use this
definition only to see how the induction principle build by hand of 1
should look like.

Hope this helps,
Pierre Courtieu

2010/5/5 geng chen 
<chengeng4001 AT gmail.com>:
> Inductive prim : Set :=
>   A : prim
> | B : prim.
>
> Inductive comp : Set := list all.
>
> Inductive all : Set :=
>   C : prim -> all
> | D : comp -> all.