The Coq mailing list

[roconnor AT theorem.ca]

I've made a small library for finite types of n elements (Fin n):Set and I
believe this is sufficiently general that it ought to be included in the
standard library.  I present two possible implementations of the same
theory.

The first implementation (Fin.v) defines a finite type as an inductive
family:

Inductive Fin : nat -> Set :=
| FinOld : forall n, Fin n -> Fin (S n)
| FinNew : forall n, Fin (S n).

Reasoning with this type is made easy by using the induction lemma
FinSn_rect, which provides an elimination rule for the type Fin (S n).
This elimination rule make programming with this inductive family a
dream.  Anytime x:Fin (S n) is in the content, the command
``destruct x using FinSn_rect'' break it into two cases without complaint.
The lemma FinOldOrNew : forall n, forall y:Fin (S n),
{z:Fin n | y=(FinOld z)}+{y=FinNew n} is provided for those few occasions
when FinSn_rect isn't quite good enough for you.

This library requires K_dec_set to be extended to work with predicates
defined over Type instead of Prop.  This extension ought be done inside
Eqdep_dec, but I provide Eqdep_dec_Type for now.

The alternative implementation (FinAlt.v) that I made defines Fin as a
fixpoint:

Fixpoint Fin (n:nat) : Set :=
match n with
| O => Empty_set
| (S m) => (unit+(Fin m))%type
end.

This implementation doesn't require FinSn_rect, but I include it for
compatibility (the proof is trivial).  The advantage of this is that
objects of type Fin (S n) can be destructed by intros patterns which is
nice.

The disadvantage of the Fixpoint definition, pointed out to me by Pierre
Corbineau, is that the type doesn't extract well.  In Haskell Fin is
extracted to the () type, which is probably the extraction mechanisms way
of saying ``I give up''.  unsafeCoercion is applied everywhere to force
everything into the () type.  This means the Fin type can't be reasonably
used to interface with non-extracted code.

For the above reason, I recommend that the inductive definition for Fin.

-- 
Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''

Attachment: Fin.tar.gz
Description: GNU Zip compressed data