The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

Edsko de Vries wrote:
> I'm stuck again in trying to write some dependent code. I want to index a
> vector:
>   

I'm sure someone else will answer your literal question, but I want to 
offer some advice that would lead to different (easier to discharge) 
goals.  I've found that vectors are _much_ easier to work with if you 
define them by recursion rather than with inductive types.  I'll quote 
some code from my Lambda Tamer library (http://ltamer.sourceforge.net/) 
that does this:

=================
Section repeat.
 Variable T : Type.

 Fixpoint repeat (n : nat) : Type :=
   match n with
     | O => unit
     | S n' => T * repeat n'
   end%type.

 Fixpoint index (n : nat) : Type :=
   match n with
     | O => Empty_set
     | S n' => option (index n')
   end.

 Fixpoint select (n : nat) : repeat n -> index n -> T :=
   match n return (repeat n -> index n -> T) with
     | O => fun _ idx => match idx with end
     | S n' => fun rep idx =>
       match idx with
         | None => fst rep
         | Some idx' => select n' (snd rep) idx'
       end
   end.
End repeat.
=================

You can find examples elsewhere in the library of how to use these 
functions.