The Coq mailing list

["Koprowski, A." <A.Koprowski AT tue.nl>]

> >     I'm wondering whether the new setoid implementation is powerful
> enough to
> >    handle arbitrary relations with equality being `same_relation'
from
> >    `Relation_Definitions' in Coq's standard library?
>  Yes, it is. 
 That's just great! 

> However, the type of union in the standard library is
>  forall A, relation A -> relation A -> A -> A -> Prop
>  To be handled correctly it should be
>  forall A, relation A -> relation A -> relation A.
>
>  You can do like this:
> 
>  Definition union: forall A, relation A -> relation A -> relation A :=
> union.
> 
>  and now Add Relation works (tested in the current SVN version of
Coq).

 Well, from my point of view that's not very satisfactory. It would be
much better if, as suggested by Frederic Blanqui in another post,
instead the standard library was modified (and I think that this setoid
declaration should find its way into library anyway!). It would be even
better if setoid mechanism was able to detect that the types in question
are convertible - isn't that possible? 

> >      produces a <<Impossible to unify "Prop" with "relation ?XXX">>
or
> >    <<Impossible to unify "_UNBOUND_REL_X" with "relation ?X">> error
> message
> >    (depending on whether I try to declare union or inclusion as a
> morphism).
> 
>  I agree that these error messages should definitely be improved.

 Well, I think so. A short remark in the manual about this limitation of
setoid (purely syntactic matching of types) also wouldn't hurt :-).

   Thanks for help!
   Adam

--
========================================================================
 Adam Koprowski, 
(A.Koprowski AT tue.nl,
 http://www.win.tue.nl/~akoprows)
 Department of Mathematics and Computer Science
 Eindhoven University of Technology (TU/e)
 The difference between impossible and possible lies in determination
      Tommy Lasorda 
========================================================================