The Coq mailing list

[e AT x80.org (Emilio Jesús Gallego Arias)]

Xavier Leroy 
<Xavier.Leroy AT inria.fr>
 writes:

> I find the following definition of vectors a lot easier to work with
> than the one that is currently in the standard library:
>
> Fixpoint vec (A: Type) (n: nat) : Type :=
>   match n with
>   | O => unit
>   | S m => (A * vec A m)%type
>   end.
>
> With this definition and the "convoy pattern" from CPDT you're in control!

Let me also suggest the approach of using a regular list + a proof of
size. The example I know is done in mathcomp:

Structure tuple_of : Type :=
 Tuple {tval :> list T; _ : length tval == n}.

this has the advantage of extracting reasonably well [with a big of
massage] and avoiding the duplication of most list operations using
automatic inference of proofs.

It can be shown that `tval` is injective, and indeed math-comp provides
a "subType" mechanism that helps in mixing tuples and lists.

[In fact, both definitions of vectors can be declared to be a subType of
 lists, not that this is very useful in practice, see [1] if you are
 curious.]

E.

[1] https://github.com/ejgallego/ssr-tools/tree/master/coq-vector