The Coq mailing list

[Matthieu Sozeau <sozeau AT lri.fr>]

Le 26 mai 08 à 13:39, Edsko de Vries a écrit :

> Hi,

Hi,

> I was playing around with the trick posted by James McKinna a while  
> back on
> definition of head and tail on vectors without relying on inversion:
>
> Section Vectors.
>
> Variable (A : Set).
>
> Inductive vec : nat -> Set :=
>  | vnil : vec 0
>  | vcons : forall n, A -> vec n -> vec (S n).
>
> Definition vhead (n : nat) (v : vec (S n)) : A :=
>  match v in vec m return (match m with 0 => True | S n' => A end) with
>  | vnil => I
>  | vcons _ head _ => head
>  end.
>
> Definition vtail (n : nat) (v : vec (S n)) : vec n :=
>  match v in vec m return (match m with 0 => True | S n' => vec n'  
> end) with
>  | vnil => I
>  | vcons _ _ tail => tail
>  end.
>
> This works quite nicely, but I got stuck in the following proof:
>
> Lemma vec_decompose : forall (n : nat) (v : vec (S n)),
>  v = vcons n (vhead n v) (vtail n v).

I think you can't avoid using inversion there, especially given the  
fact that the goal mentions [v] itself.
[dependent inversion] can't do it, but we know how to get around that  
using so-called "Ford"-induction due to Conor McBride, available in  
Coq (trunk) as the [dependent induction] tactic.

<<
Require Import Coq.Program.Equality.

Lemma vec_decompose : forall (n : nat) (v : vec (S n)),
 v = vcons n (vhead n v) (vtail n v).
Proof.
  intros.
  dependent induction v.
  simpl.
  reflexivity.
Qed.
>>

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.

Hope this helps,
--
Matthieu Sozeau
http://www.lri.fr/~sozeau