The Coq mailing list

[frederic.blanqui AT loria.fr]

On Mon, 26 May 2008, Edsko de Vries wrote:

> This works quite nicely, but I got stuck in the following proof:
>
> Lemma vec_decompose : forall (n : nat) (v : vec (S n)),
>  v = vcons n (vhead n v) (vtail n v).
>
> Any hints?

you may perhaps find some solution reusing CoLoR/Util/Vector/VecUtil.v 
available on http://color.loria.fr/.

there, we have:

Definition Vid n : vec n -> vec n :=
  match n return vec n -> vec n with
    | O => fun _ => Vnil
    | _ => fun v => Vcons (Vhead v) (Vtail v)
  end.

Lemma Vid_eq : forall n (v : vec n), v = Vid v.

Proof.
destruct v; auto.
Defined.

Lemma VSn_eq : forall n (v : vec (S n)), v = Vcons (Vhead v) (Vtail v).

Proof.
intros. change (Vcons (Vhead v) (Vtail v)) with (Vid v). apply Vid_eq.
Defined.