The Coq mailing list

[Aaron Bohannon <bohannon AT cis.upenn.edu>]

Hi, I found your comment below intriguing, but I don't understand in
what sense that method is "simpler".  What problem is it solving?  Is
the problem specific to type classes?  If it's better, why wasn't it
done this way in the standard library (i.e., in SetoidDec)?  I'm
trying to understand what is the right way to define decidable
equality on a bunch of types, and there seems to be four options now:

1) Don't use type classes at all (actually, not too painful, except
for lack of convenient notation).
2) Use the naive EqDec type class definition that Alexandre described.
3) Use the EqDec type class definition below.
4) Use the definition in SetoidDec, applied to the trivial eq_setoid for a 
type.

Is there any consensus about this issue?

 - Aaron

2010/10/1 Stéphane Lescuyer 
<stephane.lescuyer AT polytechnique.org>:
> PS : This is unrelated to your issue, but for the formalization of
> your EqDec class, it's usually simpler to use a boolean test with an
> inductive specification:
> <<<
> Inductive equal_spec {A} (x y : A) : bool -> Prop :=
> | equal_true : x = y -> equal_spec x y true
> | equal_false : x <> y -> equal_spec x y false.
> Class EqDec (A:Type) := {
>  equal : A -> A -> bool;
>  eq_dec : forall x y, equal_spec x y (equal x y)
> }.
> Notation "x == y" := (equal x y) (at level 70, no associativity).
>>>>
> You have a pure equality test and you can perform case analysis for x
> == y by calling "destruct (eq_dec x y)".