The Coq mailing list

[Jeff Vaughan <jeff AT seas.harvard.edu>]

Hi,

I'm trying to prove some simple theorems using types defined in terms of 
vectors.  I'm getting suck because I'm not sure how to destruct a vector 
when there are constraints on its length.

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.

The problem---as I understand it---is that induction 
(elim/destruct/generalized induction...) on v produces goals that are 
ill-typed.  For instance,

  exists a, exists v0, vnil = vcons a v0

Note that the left hand side of the equality has type (vector A 0) and 
the right hand side has type (vector A (S _)).  I tried using John Major 
equality.  This let me take a small step forward, but didn't enable real 
progress.

Any tips?

Best,
Jeff Vaughan