The Coq mailing list

[Eric Finster <ericfinster AT gmail.com>]

Hi All,

I'm trying to do a case analysis over an inductive type where the
allowed constructors are restricted by the type of a term.  It
essentially equivalent to the following setup with indexed lists:

Inductive Vect (A : Type) : nat → Type :=
| VNil : Vect A 0
| VCons : forall n : nat, A → Vect A n → Vect A (S n).

Lemma zero_len_is_nil (A : Type) (v : Vect A 0) : v = VNil A.
Proof.
  inversion?
  induction?
  ???

Is it possible to express the fact that this vector of length zero can
only be VNil?  I have also tried using a fixpoint.  Perhaps some kind
of "match annotations" would help, but I confess I do not completely
understand how to use them.

Fixpoint zero_len_eq (A : Type) (v : Vect A 0) :  v = VNil A :=
  match v with
    | VNil => identity_refl (VNil A)
  end.

Any help would be greatly appreciated.

Eric Finster