The Coq mailing list

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

> Here's a quick solution.

Wow!  That is quick.  Thanks!

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

I was able to remove the dependence on K, using tricks shown to me by 
Rob Dockins.  I've pasted the code below, which also incorporates Conor 
McBride's suggestions.

So, it looks like the use of ``generalize'' is the trick that I was missing.

When you get the error ``Cannot solve a second-order unification 
problem'', that means that Coq thinks you are asking it to infer a 
function, correct?

In the code below, if you comment out the use of ``generalize'', you get 
this error.  So, if the above is right, what is the function that it 
thinks you are asking it to infer in this case?

Is there a way to find this out, in general?

> There's probably a functorized way of 
> getting the same effect in this case without an axiom.

I don't know if this is the same thing, but I have wondered if there was 
a theorem in the standard library that would do the following in one step.

    apply eq_proofs_unicity.
    decide equality.

If anyone knows of such a theorem, I would be interested.

Thanks to Andrew, Conor, and Adam for their most generous help!

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

(* Require Import Eqdep. *)
Require Import Eqdep_dec.

Lemma Lem_cleaner_cons_eq_rect : forall (m n : nat) (q : m = n)
 (a : Type) (x : a) (xs : vector m a),
   cons x (eq_rect m (fun m => vector m a) xs n q)
     = eq_rect (S m) (fun m => vector m a) (cons x xs) (S n)
       (f_equal S q).
Proof.
    intros until x.
    generalize q.
    rewrite q.
    intros.
    replace q0 with (refl_equal n).
    auto.
    apply eq_proofs_unicity.
    decide equality.
Qed.

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)).
Proof.
    intros.
    apply (Lem_cleaner_cons_eq_rect (f n) n (p n)).
Qed.