The Coq mailing list

[Adam Koprowski <adam.koprowski AT gmail.com>]

  Dear Jeff,

  I'd just like to point out that the CoLoR library has a rich set of results on vectors (as an extension to Coq's stdlib). You'll also find Vsn_eq there from which your lemma trivially follows. Hope that helps.

  Cheers,
   Adam

On Fri, Oct 9, 2009 at 00:20, Jeff Vaughan <jeff AT seas.harvard.edu> wrote:

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

--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
        http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

-- 
=====================================================
Adam.Koprowski AT gmail.com, http://www.cs.ru.nl/~Adam.Koprowski

The difference between impossible and possible
lies in determination (Tommy Lasorda)
=====================================================