The Coq mailing list

["Jean.Duprat" <duprat AT ens-lyon.fr>]

Hi Sebastien,

May I add my solution after Yve's and Pierre's ones.

First, you build the identity function upon vectors :

Definition Vid : forall n:nat, vector n -> vector n.
Proof.
destruct n; intros.
exact Vnil.
exact (Vcons (Vhead H) (Vtail H)).
Defined.

Then you prove that this function is exactly the identity :

Lemma Viq_eq : forall (n:nat) (v:vector n), v=(Vid n v).
Proof.
destruct v; auto.
Qed.

End, you use it for proving your theorem :

Theorem VSn_eq :
 forall (n : nat) (v : vector (S n)),
 v = Vcons (Vhead v) (Vtail v).
Proof.
intros.
change (Vcons (Vhead v) (Vtail v)) with (Vid (S n) v).
apply Vid_eq.
Qed.

Yours,

        Jean.

Sébastien Hinderer wrote:

> 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.
> --------------------------------------------------------
> Bug reports: http://coq.inria.fr/bin/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>          http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club