The Coq mailing list

["Samuel E. Moelius III" <moelius AT cis.udel.edu>]

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))).

If I specialize n to 0, I can get as far as to show that the left hand 
side of the equation is (cons x (nil a)).  Beyond that, I'm stuck.

Can anyone offer some suggestions?

Separate question: in Coq, is there a way to add a conjunct to a goal, 
e.g., for the purpose of obtaining a stronger induction hypothesis?

Sam

(*=======================================================================*)

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].

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))).
Proof.
    intros.
(* Experimenting with the case n = 0. *)
    destruct n.
    set (ys := eq_rect (f 0) (fun m : nat => vector m a) xs 0 (p 0)).
    assert (ys = nil a).
    destruct ys.
    auto.
    rewrite H.
(* Stuck here.  Here is the context:

f : nat -> nat
p : forall m : nat, f m = m
a : Type
x : a
xs : vector (f 0) a
ys := eq_rect (f 0) (fun m : nat => vector m a) xs 0 (p 0)
   : (fun m : nat => vector m a) 0
H : ys = nil a
______________________________________(1/2)
cons x (n:=0) (nil a) =
eq_rect (S (f 0)) (fun m : nat => vector m a) (cons x (n:=f 0) xs) 1
  (f_equal S (p 0))

*)