The Coq mailing list

[Edsko de Vries <devriese AT cs.tcd.ie>]

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?

Edsko