The Coq mailing list

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

   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

========================================================================