The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

Samuel E. Moelius III wrote:
> I've been experimenting with vectors in the style advocated by Adam 
> Chlipala.  I'm trying to show that cons commutes with eq_rect, in a 
> certain sense, but I'm having trouble.  Here is the lemma.
>
> Lemma lem_cons_eq_rect (f : nat -> nat) (p : forall m, f m = m)
>     : forall (n : nat) (a : Type),
>       (forall (x : a) (xs : vector (f n) a),
>       cons x (eq_rect (f n) (fun m => vector m a) xs n (p n))
>         = eq_rect (S (f n)) (fun m => vector m a) (cons x xs) (S n)
>             (f_equal S (p n))).

Here's a quick solution. It's possible to automate this much better, but 
not without writing a fair amount of Ltac (or using a library that 
does).  And keep in mind that importing Eqdep involves assuming an axiom 
equivalent to Streicher's K.  There's probably a functorized way of 
getting the same effect in this case without an axiom.


Fixpoint vector (n : nat) (a : Type) {struct n} : Type :=
   match n with
     | 0    => unit
     | S n' => (a * vector n' a)%type
   end.

Definition nil (a : Type) := tt.

Definition cons (a : Type) (x : a) (n : nat) (xs : vector n a) := (x, xs).

Implicit Arguments cons [a n].

Require Import Eqdep.

Lemma Lem_cons_eq_rect (f : nat -> nat) (p : forall m, f m = m)
 : forall (n : nat) (a : Type) (x : a) (xs : vector (f n) a),
   cons x (eq_rect (f n) (fun m => vector m a) xs n (p n))
   = eq_rect (S (f n)) (fun m => vector m a) (cons x xs) (S n)
   (f_equal S (p n)).
 intros until x.
 generalize (p n).
 rewrite (p n).
 intros.
 rewrite (UIP_refl _ _ e).
 reflexivity.
Qed.