The Coq mailing list

[Conor McBride <conor AT strictlypositive.org>]

Hi

I just about got coqtop running, so I was able to check what
I guessed would work here (having previously emailed Samuel
speculatively). Adam's plan is the right one, but it's possible
to adjust it very slightly, sidestepping Eqdep.

On 27 Aug 2008, at 23:04, Adam Chlipala wrote:

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

  generalize (f n).
  intros until e.
  case e.
  intros.
  reflexivity.
Qed.

Somehow, one should always suspect that the combination of

>  rewrite (p n).
>  rewrite (UIP_refl _ _ e).

can be replaced by a single dependent elimination of the
equation. Or vice versa.

Non-dependent substitutivity and UIP together imply the
full dependent eliminator. (Indeed, proof-irrelevance and
other eta-like rules tend to make dependent eliminators
follow from non-dependent ones.)

All the best

Conor

PS One day, not far away, it will be possible to ensure that
eq_rect commutes with constructors even in the *definitional*
equality. We know how to implement it, but we have yet to
persuade people to believe it.