The Coq mailing list

[Alexandre Pilkiewicz <alexandre.pilkiewicz AT polytechnique.org>]

Dear list.

I'm trying to use Coq type classes in one of my developments, but I
run in a problem of duplicated instances:

I have a class for decidable equality

<<<
Class EqDec (A:Type) := {
  eq_dec: forall (x y:A), {x = y} + {x <> y}
}.

Notation "x == y" := (eq_dec x y) (at level 70, no associativity).
>>>

Now, I want to define a module type (for trees), with elements
equipped with a decidable equality.
My only solution is to do something like

<<<
Module Type TREE.
  Parameter elt: Type.
  Instance  EqDec_elt : EqDec elt.
 ...
End TREE.
>>>

Say I now have an implementation of trees for elt := positive

I have to create this new instance EqDec_elt, equal to a predefined EqDec_pos

but now, when x and y are both of type positive, x == y can use one
instance or the other, leading to huge difficulties. For example, if
one of my hypothesis is of the form

<<<
H : if (x == y) then ... else ...
>>>

typing destruct (x == y). will typically not change H because a
different instance was chosen.

Is there a way to express in the signature that the type elt has
decidable equality, without forcing implementations to duplicate the
instance ?

Thanks

Alexandre Pilkiewicz