The Coq mailing list

[Edsko de Vries <devriese AT cs.tcd.ie>]

Hi,

I was playing around with the trick posted by James McKinna a while back on
definition of head and tail on vectors without relying on inversion:

Section Vectors.

Variable (A : Set).

Inductive vec : nat -> Set :=
  | vnil : vec 0
  | vcons : forall n, A -> vec n -> vec (S n).

Definition vhead (n : nat) (v : vec (S n)) : A :=
  match v in vec m return (match m with 0 => True | S n' => A end) with
  | vnil => I
  | vcons _ head _ => head
  end.

Definition vtail (n : nat) (v : vec (S n)) : vec n :=
  match v in vec m return (match m with 0 => True | S n' => vec n' end) with
  | vnil => I
  | vcons _ _ tail => tail
  end.

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?

Thanks,

Edsko