The Coq mailing list

[Thery Laurent <thery AT ns.di.univaq.it>]

Hi,

>  Below is a simple proof that the only vector of length 0 is
> Vnil. But this proof uses the axiom JMeq_eq. Is there any axiom-free
> proof of the same result ?

It is always the same trick as explained by Pierre Letouze:

http://coq.inria.fr/mailing-lists/coqclub/200404/msg00002.html

It is also used in the definition of monomials in my buchberger 
development:

ftp://ftp-sop.inria.fr/lemme/Laurent.Thery/Buchberger/index.html

You first define a variant of the identity function to get rid of the 
dependency:

Definition vector_id : forall n : nat, vector bool n -> vector bool n.
intros n; case n.
intros H'; exact (Vnil bool).
intros n1 H'; exact H'.
Defined.

Prove that it is indeed the identity


Theorem vector_id_is_id : forall n (v: vector bool n), v = vector_id n v.
intros n v; case v; simpl in |- *; auto.
Qed.

And the trick is done

Theorem vector_eq_0 : forall v : vector bool 0, v = Vnil bool.
intros v; exact (vector_id_is_id 0 v).
Qed.

--
Laurent