The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

On 12/12/2014 02:45, Vadim Zaliva wrote:
> > On Dec 10, 2014, at 23:18 , Guillaume Melquiond 
> > <guillaume.melquiond AT inria.fr>
> >  wrote:
> >
> > Now you are telling me you are not interested in an equivalence based on 
> > eta-convertibility, but without explaining what kind of equivalence you need 
> > instead. So perhaps you want a pointwise equivalence?
>
> Thanks! That was helpful. Pointwise equivalence should work. It worked on 
> trivial example I've sent earlier, but when I tried to extend the approach to 
> more complex functions using dependent types it did not work. Here is a new, 
> more specific example. It looks like Proper instance does not match the 
> requirements.
>
> Class Equiv A := equiv : relation A.
> Class Setoid A {Ae : Equiv A} : Prop := setoid_eq :> Equivalence (@equiv A 
> Ae).
> Class Mult A := mult: A -> A -> A.
> Instance vecequiv A `{Equiv A} n : Equiv (Vector.t A n). admit. Defined.
> Definition Vmap_reord (A B: Type) (n:nat) (f:A->B) (x: Vector.t A n): 
> Vector.t B n := Vector.map f x.
>
> Instance Vmap_reord_proper_pointwise n  (M N:Type) `{Ne:!Equiv N, Me:!Equiv 
> M}:
>   Proper ((pointwise_relation M Ne) ==> (@vecequiv M Me n) ==> (@vecequiv N 
> Ne n)) (@Vmap_reord M N n).

If I am not mistaken, you have never told Coq that vecequiv is an 
equivalence relation (and thus reflexive). As a consequence, it cannot 
prove "@vecequiv A Ae n z z" and thus it is unable to perform the 
replacement due to the "@vecequiv M Me n" part of your Proper.

Best regards,

Guillaume

PS: Do not ask me how I was able to infer that from the error message; I 
didn't.