The Coq mailing list

[S�bastien Hinderer <Sebastien.Hinderer AT loria.fr>]

Dear all,

Assume the followng definitions, inspired by the Bvector module of Coq's
standard library :

Section VECTORS.

Variable A : Set.

Inductive vector : nat -> Set :=
  | Vnil : vector 0
  | Vcons : forall (a:A) (n:nat), vector n -> vector (S n).

Implicit Arguments Vcons [n].

Definition Vhead : forall n:nat, vector (S n) -> A.
Proof.
        intros n v; inversion v as [|a p w]; exact a.
Defined.

Implicit Arguments Vhead [n].

Definition Vtail : forall n:nat, vector (S n) -> vector n.
Proof.
        intros n v; inversion v as [| a p w]; exact w.
Defined.

Implicit Arguments Vtail [n].

(How) Is it sossible to prove the following theorem in Coq ?

Theorem VSn_eq :
  forall (n : nat) (v : vector (S n)),
  v = Vcons (Vhead v) (Vtail v).


Thanks in advance for your help,
Sébastien.