The Coq mailing list

[Vadim Zaliva <vzaliva AT cmu.edu>]

> On Nov 23, 2014, at 10:16 , Vadim Zaliva 
> <vzaliva AT cmu.edu>
>  wrote:
> 
> I also wanted to ask about another trivial Proper proof which I could not 
> make to work:

I have been able to make it work as shown below. The trick was to use Equiv 
vs. vecequiv, as you mentioned.

Require Import Setoid.
Require Import Morphisms.
Require Vector.

Notation vector := Vector.t.
Notation Vhead := Vector.hd.
Implicit Arguments Vhead [A n].

Set Printing Implicit.

Class Equiv A := equiv : relation A.
Class Setoid A {Ae : Equiv A} : Prop := setoid_eq :> Equivalence (@equiv A 
Ae).

Instance vecequiv A `{Equiv A} n : Equiv (vector A n).
admit.
Defined.

Global Instance Vhead_proper A `{H:Equiv A} n:
  Proper (@equiv (vector A (S n)) (@vecequiv A H (S n)) ==> equiv) (@Vhead A 
n).

Lemma hd_eqiv: forall A `{Setoid A} {n} (u v: vector A (S n)), u=v -> (Vhead 
u) = (Vhead v).
Proof.
  intros.
  rewrite H0.
  f_equiv.
Qed.


Sincerely,
Vadim Zaliva

--
CMU ECE PhD student
Mobile: +1(510)220-1060
Skype: vzaliva