The Coq mailing list

[Santiago Zanella <Santiago.Zanella AT sophia.inria.fr>]

I don't see any impediment in the current implementation of setoids for
handling relations of relations. However, when declaring a morphism Coq
apparently tries to match syntactically the signature with the type of
the morphism, and so fails to recognize types that are equal up to
unification. In that cases an explicit casting is a practical
workaround, like in

Add Morphism (union : forall A, relation A -> relation A -> relation A)
 with signature same_relation ==> same_relation ==> same_relation
 as union_morphism.

Unfortunately, this just pushes the problem forward since you may
experience the same problem with unification when rewriting inside the
declared morphism. I hope someone can give some insight or a better
solution though.

On Wed, 2007-03-21 at 14:22 +0100, "Koprowski, A." wrote: 
>    Hello,
> 
>  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? From the documentation
> I gather that this should be possible (resulting in a setoid relation
> with 'relation A' as a carrier). This would be immensely helpful in many
> applications! I managed to declare this as a setoid as follows:
> 
>  
> 
> Lemma same_relation_refl : forall A, reflexive (same_relation A).
> 
> Lemma same_relation_sym : forall A, symmetric (same_relation A).
> 
> Lemma same_relation_trans : forall A, transitive (same_relation A).
> 
>  
> 
> Add Relation relation same_relation
> 
>   reflexivity proved by (same_relation_refl)
> 
>   symmetry proved by (same_relation_sym)
> 
>   transitivity proved by (same_relation_trans) as same_relation_rel.
> 
>  
> 
>   However I'm having trouble with declaring morphisms as:
> 
>  
> 
> Add Morphism union
> 
>   with signature same_relation ==> same_relation ==> same_relation
> 
>   as inclusion_morph.
> 
>  
> 
>   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). Any help? Thanks!
> 
>    Adam Koprowski
> 
>  
> 
> --
> 
> =======================================================================
>  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 
> 
> =======================================================================