The Coq mailing list

[Matthieu Sozeau <sozeau AT lri.fr>]

Le 26 mai 08 à 21:12, Edsko de Vries a écrit :

> Hi,
>
> > The same can be achieved without special tactics using:
> >
> > <<
> > Require Import JMeq.
> >
> > Lemma vec_decompose : forall (n : nat) (v : vec (S n)),
> > v = vcons n (vhead n v) (vtail n v).
> > Proof.
> >  intros.
> >  refine ((_
> >             :forall (gen_x : nat) (v0 : vec gen_x),
> >               JMeq v0 v ->
> >              gen_x = S n -> v = vcons n (vhead n v) (vtail n v))
> >              (S n) v (JMeq_refl v) (refl_equal (S n))).
> >  induction v0 ; intros Hv Hx ; subst.
> >  discriminate.
> >  inversion Hx ; subst.
> >  apply JMeq_eq in Hv. subst.
> >  simpl.
> >  reflexivity.
> > Qed.
> > > >
> >
> > Note the use of heterogeneous equality to keep the equality between
> > [v] and the generalized [v0] variable.
>
> Thanks for your detailed answer. I'm however not sure why we have to
> give this non-trivial (at least to me!) proof. Can you give me an
> intuition?


Well, in this particular case you can get around using inversion  
tactics explicitely using Frederic's trick, but you're still doing  
inversion using the Vid function, learning that a [v : vec (S n)] is  
necessarily equal to a [vcons ...] making the [change ... (Vid v)]  
succeed. Also, I don't think it solves the problem of keeping  
equalities around (case_eq style) if you begin to use induction,  
destruct or any other elimination tactic on objects of type "vec (S  
n)". This general problem and its solution are discussed in  
"Elimination with a motive" by Conor McBride.

-- Matthieu