The Coq mailing list

[Pierre Letouzey <Pierre.Letouzey AT lri.fr>]

On Fri, 2 Apr 2004, 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.

To complete Yves's answer, it is also feasible to stick to usual Coq
equality, but it's not what I would call simple. Below is an (indirect)
way to proof your original statement, if you really want it:

Pierre Letouzey


Definition Vhead_bis :  forall n:nat, n<>0 -> vector n -> A.
Proof.
destruct n.
tauto.
intros _ a; exact (Vhead a).
Defined.

Definition Vtail_bis :  forall n:nat, n<>0 -> vector n -> vector (pred n).
Proof.
destruct n.
tauto.
intros _ a; exact (Vtail a).
Defined.

Definition hack : forall n, n<>0 -> vector (S (pred n)) -> vector n.
Proof.
destruct n; tauto; trivial.
Defined.

Theorem VSn_eq_bis :
  forall (n : nat) (v : vector n)(H:n<>0),
  v = hack n H (Vcons (Vhead_bis n H v) (Vtail_bis n H v)).
Proof.
destruct v.
intros H; elim H; auto.
simpl; auto.
Defined.

Theorem VSn_eq :
  forall (n : nat) (v : vector (S n)),
  v = Vcons (Vhead v) (Vtail v).
Proof.
intros n v.
change n with (pred (S n)).
assert (S n<>0). auto.
pattern v at 1; rewrite (VSn_eq_bis (S n) v H); auto.
Defined.