The Coq mailing list

["Carlos.SIMPSON" <carlos AT math.unice.fr>]

Dear Russell,

Coq's inductive types have a new functionality which allows one to 
define a wider range of
parametric inductive types than before. This should allow the definition 
of Fin n as a parametric inductive type
with n as a parameter.

(NB: This functionality was used by Marco Maggesi in his contribution 
defining the Lambda calculus using this
new kind of inductive type--Carlos) .


One encounters a little problem due to the fact that (pred 0) = 0. Here 
is a quick work-around to give a definition.
We aren't sure if this could simplify the treatment of finite types, if 
there is a better work-around, etc.; however,
in reply to your message, we feel that it would be good to ask whether 
it is possible to give a more streamlined treatment
of finite types using this new kind of parametrized inductive type.

Here is a proposition for some code, not sure it compiles though:-(? (In 
any case it would require a very recent edition of Coq).

Definition is_zero (n:nat) : bool :=
match n with 0 => true | S m => false end.

Definition non_zero (n:nat) : bool :=
match n with 0 => false | S m => true end.

Inductive boolset : bool -> Set :=
boolset : boolset true. 

(* recall pred n = n-1, the only problem is pred 0 = 0. That is why we define 
FinConditional first. *)

Inductive FinConditional (n : nat) : bool -> Set :=
 | fin_prev : FinConditional (pred n) (non_zero n) -> Fin n true
 | fin_zero : boolset (is_zero n) -> FinConditional n true.

Definition Fin n := FinConditional n true. 


Briefly, FinConditional n false is supposed to always be empty. Thus fin_prev 
doesn't introduce anything new if n=0.
For n=0 the constructer is fin_zero (which in turn doesn't introduce anything if n>0). 


---Marco Maggesi and Carlos Simpson