The Coq mailing list

[Hugo Herbelin <herbelin AT pauillac.inria.fr>]

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.

Just to anticipate on a modest feature of the forthcoming version 8.2
(we hope to be able to announce the beta version in one or two weeks),
in easy cases as above, it will be possible to omit the return
statement and the contradictory matching clause (and this will produce
about the same code as explicitly given above).

Section Vectors.
Set Implicit Arguments.
Variable (A : Set).

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

Definition vhead n (v : vec (S n)) :=
  match v with
  | vcons _ head _ => head
  end.

Definition vtail n (v : vec (S n)) :=
  match v with
  | vcons _ _ tail => tail
  end.

Hugo Herbelin