The Coq mailing list

[casteran AT labri.fr]

Hello all,

  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 ?

Pierre




Require Import Bvector.



Require Import JMeq.

Lemma pim: forall (n:nat)(v:vector bool n), n=0 -> JMeq v (Vnil bool).
 intros n  v; case v.
 reflexivity.
 discriminate 1.
Qed.


Lemma pam: forall (v:vector bool 0), JMeq v (Vnil bool).
 intro v; apply pim.
 trivial.
Qed.

Lemma  poum : forall (v:vector bool 0), eq v (Vnil bool).
 intros  v.
 apply JMeq_eq.
 apply pam.
Qed.


----------------------------------------------------------------
This message was sent using IMP, the Internet Messaging Program.