The Coq mailing list

[Venanzio Capretta <venanzio AT cs.ru.nl>]

Adam Chlipala wrote:
> Programs written like this with proof scripts seem hard to read and 
> maintain.  Does anyone have any arguments for writing in this style 
> instead of in the style I used in my solution?
I agree with you: For the prefix function, it seems that your recursive 
implementation of vectors is much nicer that the inductive one. But is 
it always preferable.

Btw: I have a little module with the equivalence of the two 
implementations and a third one of vectors as functions on finite types.
See http://www.cs.ru.nl/~venanzio/Coq/Vectors.v.

Using some of the definitions in there,  here is another possible way is 
to answer Samuel's original question:

Fixpoint vec_split (A:Set)(n1 n2:nat){struct n1}:
 vector A (n1+n2) -> (vector A n1 * vector A n2)%type :=
match n1 return vector A (n1+n2) -> (vector A n1 * vector A n2)%type with
 O => fun v => (vec_nil A, v)
| (S n1') => fun v => let (w1,w2):= vec_split A n1' n2 (vec_tail v) in
                       (vec_cons (vec_head v) w1, w2)
end.

Using vec_split is easy to define prefix, but you still have to use 
rewriting steps inside the definition.

Venanzio