The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Le 9 oct. 09 à 13:23, 
Benedikt.AHRENS AT unice.fr
 a écrit :

> Hello,
>
> for the complementary theorem about vectors of length 0 (code at the
> bottom), Adam's suggestion can be adopted [1], whereas a proof similar
> to Laurent's [2] fails, since the abstraction in the inversion step
> gives an ill-typed term.
> Is there a way to prove the lemma by tactics anyway?

Yes, using [dependent destruction] [1]:

<<
Require Import Bvector Program.Equality.

Lemma is_nil: forall A (v:vector A 0),
       v = Vnil A.
Proof.
intros A v. dependent destruction v. reflexivity.
Qed.
>>

[1] 
http://coq.inria.fr/refman/Reference-Manual013.html#dependent-induction-example

-- Matthieu