The Coq mailing list

[Yves Bertot <Yves.Bertot AT sophia.inria.fr>]

Sebastien Hinderer wrote:

> Dear all,
> 
> Assume the followng definitions, inspired by the Bvector module of Coq's
> standard library :
> 
> Section VECTORS.
> 
> Variable A : Set.
> 
> Inductive vector : nat -> Set :=
>   | Vnil : vector 0
>   | Vcons : forall (a:A) (n:nat), vector n -> vector (S n).
> 
> Implicit Arguments Vcons [n].
> 
> Definition Vhead : forall n:nat, vector (S n) -> A.
> Proof.
>       intros n v; inversion v as [|a p w]; exact a.
> Defined.
> 
> Implicit Arguments Vhead [n].
> 
> Definition Vtail : forall n:nat, vector (S n) -> vector n.
> Proof.
>       intros n v; inversion v as [| a p w]; exact w.
> Defined.
> 
> Implicit Arguments Vtail [n].
> 
> (How) Is it sossible to prove the following theorem in Coq ?
> 
> Theorem VSn_eq :
>   forall (n : nat) (v : vector (S n)),
>   v = Vcons (Vhead v) (Vtail v).


The problem is that you want to perform a case analysis on "v", but the
case where v has type "vector 0" poses a problem because Vhead and
Vtail only accept to be applied on elements of "vector (S p)" for some 
p.  The solution I propose is to de-couple the various instance of v
in the statement by introducing an auxiliary variable "w" and to
decouple the types of "v" and "w" by using Connor McBride's
heterogeneous equality JMeq.  Here is my solution.

intros n v; apply JMeq_eq.
assert
 (Hw:forall (w : vector (S n)), JMeq v w ->  JMeq v (Vcons (Vhead w) (Vtail 
w))).
(* this equality is introduced to mimick the behavior of inversion. *)
generalize (refl_equal (S n)).
(* this step should be feasible with pattern, but I don't master it
   well enough to understand how it works in presence of dependent
   types. *)
change
 ((fun n0 =>
   fun (v' : vector n0) =>
   n0 = S n ->
   forall (w : vector (S n)),
   @JMeq (vector n0) v' (vector (S n)) w ->
    @JMeq (vector n0) v' (vector (S n)) (Vcons (Vhead w) (Vtail w))) (S n) v).
case v.
intros; discriminate.
intros a n0 v0 Heq; injection Heq; intros Heq'; rewrite <- Heq'.
intros w HJeq; rewrite <- HJeq; auto.
auto.
Qed.