The Coq mailing list

[Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr>]

> I found the following definition to be much easier to work with:
> 
>    Definition vector a n :=
>      { xs : list a | length xs = n }.
> 
> I prefer this definition for a couple reasons ...

Of course it depends on what you want to do with it.

But that definition of vectors as a subtype of lists does 
not *nest* well, typically in the context of dependent trees.

See for instance:

(**************************)

Definition vec1 A n := {xs : list A | length xs = n}.

Inductive vec2 A : nat -> Type :=
  | vec_nil : vec2 A 0
  | vec_cons : A -> forall n, vec2 A n -> vec2 A (S n).

Fail Inductive dtree1 (X : nat -> Type) :=
  | dtree1_cons n : X n -> vec1 (dtree1 X) n -> dtree1 X.

Inductive dtree2 (X : nat -> Type) :=
  | dtree2_cons n : X n -> vec2 (dtree2 X) n -> dtree2 X.

Fail Inductive dtree3 (X : nat -> Type) :=
  | dtree3_cons n : X n -> forall l : list (dtree3 X), length l = n -> dtree3 
X.

Fail Inductive dtree4 (X : nat -> Type) :=
  | dtree4_cons (l : list (dtree4 X)) : X (length l) -> dtree4 X. 

(*************************)

Notice that lists do not nest either if you want to
put a constraint on their length, eg dtree3 or dtree4.

It does not even work when characterizing the constraint length l = n
inductivelly, instead of using a fixpoint (ie length).

(**************************)

Inductive eq_length {A} : list A -> nat -> Prop :=
  | eq_length_0 : eq_length nil 0
  | eq_length_S x l n : eq_length l n -> eq_length (x::l) (S n).

Definition vec3 A n := {xs : list A | eq_length xs n}.

Fail Inductive dtree5 (X : nat -> Type) :=
  | dtree5_cons n : X n -> vec3 (dtree5 X) n -> dtree5 X.

Fail Inductive dtree6 (X : nat -> Type) :=
  | dtree6_cons n : X n -> forall l : list (dtree6 X), eq_length l n -> 
dtree6 X.

(**************************)

So indeed, you have to take your time and think about
how you intend to use those vectors before choosing a
definition.

I also suspect that the vec1 definition above would
give a clumsy access to components when using Fin.t as
indices, by converting Fin.t to nat and then using List.nth ...
Also the proofs in between would certainly block computations
with vec1.

Best,

Dominique