The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Hi again,

Actually, I sent this a bit too quickly. There was a simple fix to
make this work if the dependent arguments stay unchanged. It's in
the trunk. I'm not sure that unification will always be good enough
with signatures using [forall_relation] though.

Cheers,
-- Matthieu

Le 22 juin 09 à 16:47, Matthieu Sozeau a écrit :

> 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
>
> --------------------------------------------------------
> Bug reports: http://logical.saclay.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>         http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club