The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

Jeff Vaughan wrote:
> Vectors are defined as follows:
>
>   Set Implicit Arguments.
>
>   Inductive vector (A: Type): nat -> Type :=
>   | vnil: vector A O
>   | vcons: forall len, A -> vector A len -> vector A (S len).
>   Implicit Arguments vnil [A].
>
> And I would like to prove, for instance, this lemma:
>
>   Lemma openVector: forall A n (v: vector A (S n)),
>     exists a, exists v0, v = vcons a v0.

This is one of my favorite examples, because it's easy to prove directly 
with a proof term:

Definition openVector A n (v: vector A (S n))
 : exists a, exists v0, v = vcons a v0 :=
   match v in vector _ N return match N return vector A N -> Prop with
                                  | O => fun _ => True
                                  | S n => fun v => exists a, exists 
v0, v = vcons a v0
                                end v with
     | vnil => I
     | vcons _ a v0 => ex_intro _ a (ex_intro _ v0 (refl_equal _))
   end.

I could try to "explain" what's going on here, but it's probably better 
to treat this code as a koan and come to your own understanding. :)