The Coq mailing list

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

Thanks Ryan!

Matthieu Sozeau just replied off list and suggested using
dependent destruction/induction.  Like your proof these tactics also use 
JMeq and import an axiom.

Is there any reason to be wary of the JMeq_eq axiom?  Is it possible to 
prove such a theorem without JMeq?

Also, when you suggest a fixpoint based version of vectors, do you mean 
something like the following?

Fixpoint vec' (A: Type) (n: nat) : Type :=
  match n with
    O => unit
  | S m => A * vec' A m
  end.

Best,
Jeff

Ryan Wisnesky wrote:
> Personally, I think the real moral of the story here is to avoid 
> indexing inductive types with terms.  Here's the first  proof I could 
> think of:
>
> Inductive vector (A: Type): nat -> Type :=
>  | vnil: vector A O
>  | vcons: forall len, A -> vector A len -> vector A (S len).
>
> Set Implicit Arguments.
> Require Import JMeq.
>
>  Lemma openVector: forall A n (v: vector A (S n)),
>    exists a, exists v0, v = vcons A n a v0.
>  Proof.
>   intros.
>   refine (match v as v' in vector _ n' return S n = n' -> JMeq v v' ->
>             exists a : A, exists v0 : vector A n, v = vcons A n a v0
>             with
>             | vnil => _
>             | vcons n a v0 => _
>           end (refl_equal (S n)) (JMeq_refl v)).
>   intros. discriminate. (* first case is impossible *)
>   intros. assert (n = n0). congruence. subst. clear H.
>   apply JMeq_eq in H0. (* use jmeq axiom *)
>   eauto.
> Qed.
>
> What's happening here is case analysis on v, just like you wanted, but 
> there an "as" and "in" clause that tells Coq explicitly how to handle 
> the dependency.  The tactics don't generally deal with this well so you 
> may need to write proof terms manually like this.  I'd recommend moving 
> to a fixpoint version of vector instead.
>
> On Oct 8, 2009, at 6:20 PM, Jeff Vaughan 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