The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Le 22 juin 09 à 15:13, Adam Koprowski a écrit :

> (*
>    Dear all,
>
>   I'm trying to define a setoid equality on vectors given a setoid
> equality on vector elements. However, I'm having troubles properly
> declaring morphisms for vector operations. It seems to me that the
> problem has to do with declaring morphisms on dependently typed
> functions, however I'd appreciate a comment on whether I'm doing
> something wrong or just hitting a setoid limitation and if so, whether
> there is a work-around. Let me illustrate what I have in mind on a
> simple example.
> *)

Hi Adam, you are indeed hitting a setoid limitation. While there is
primitive setup for building signatures of dependent functions, it is
not currently supported by the setoid tactics. The only workaround is
to put the dependent arguments at the beginning of the type like you
did, if possible. Then they are treated like parameters. If some
dependent arguments appear after some arguments you want to rewrite,
you should build a dependent signature like this:

Add Parametric Morphism A (eqA : Setoid A) n : (@Vnth A n)
  with signature equiv ==> forall_relation (fun i => eq ==> equiv)
    as Vnth_morph2.

But the treatment of dependent morphisms is not implemented yet.
I'm pretty sure it can be done though, I'm working on it.

> (* Setoid equality on [A] yields a setoid on [vector A] *)
> (* [?] Do we need to declare both the relation and a type-class  
> instance?
>        If I omit this declaration then the constraints for the  
> following
>        parametric morhism fail... *)
> Program Instance vec_equality `(eqA : Setoid A) : Setoid (vector A  
> n) :=
>   { equiv := @eq_vec A eqA n; setoid_equiv := _ }.

That's because [equiv] is defined on [Setoid] not [Equivalence], and  
we don't
have an instance of [Equivalence -> Setoid], it would loop with the  
existing
[Setoid -> Equivalence] projection.

Hope this helps,
-- Matthieu