The Coq mailing list

[St�phane Lescuyer <stephane.lescuyer AT polytechnique.org>]

Hi Aaron,

Well I'm afraid there is no consensus about this issue, but is
there any consensus on any design issue in Coq ? :-) Here are
some of the considerations that make me think the version I
propose is "simpler" (in the sense of more convenient, more
practical, not in a logical sense).

First, I strongly recommend the use of typeclasses (thus
discarding your option #1): as you notice it allows an overloaded
generic notation for all operations related to the considered
class, but it is just the tip of the iceberg. The big advantage
is the ability to declare generic instances of EqDec and let the
system automatically infer decidable equality for compound
types. For instance, you would write generic instances for
[option A], [A * B], [A + B], [list A], etc, based on instances
on [A] and [B], and you could then use complex types built with
these operators as types with a decidable equality. I wrote a
library of ordered types in that fashion and it's just invaluable
when programming in Coq (more or less your typical OCaml's
Pervasives.compare).

Now that you are convinced (or so I hope :)) that using
typeclasses is the way to go, there remains to see what exactly
the EqDec class should be. Note that options #2 and #4 are
actually the same, it's just that #4 is more generalized but it
wouldn't make much difference in practice (only, you couldn't
write generic lemmas that would be true for Leibniz equality but
not for all setoid equalities). In the end, what we want that
class to provide is a function deciding the equality between two
elements, and a proof that that function is correct. Maybe the
most intuitive way of doing so is:

Class EqDec (A : Type) := {
  equal : A -> A -> bool;
  equal_iff : forall x y, equal x y = true <-> x = y
}.

Most people will then typically write two oriented lemmas
[equal_1] and [equal_2] instead of [equal_iff] because it's
easier to reason with. But not yet easy enough. If you have a
goal with an equality test [equal t u], it's tedious to perform
case analysis on the result of this test, you need to eliminate
it with something like [case_eq (equal t u)] in order to be able
to explicitely use the lemmas [equal_*] later. This is why,
instead of using a boolean test, people use a function returning
a proof as well:

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

Destructing [eq_dec t u] then does both case analysis in your
programs and adds the logical consequence of each case. But the
fact that reasoning is less cumbersome is really the only reason
to do that instead of using [equal] as above, because other than
that, having a function like [eq_dec] only raises more issues in
my opinion.

Indeed, the less I mix proofs and programs, the more happy I
am :) Since [eq_dec] contains proofs, you will typically write it
in proof mode, which is not satisfactory: you cannot easily read
how the equality test is performed, and [Print]ing the definition
won't help much either. Unless you have taken extra care,
computing these tests will end up being slower than a purely
computational function. If it computes, that is, because we have
all experienced the dreadful "computation which never ends
because there must be a Qed somewhere instead of Defined but I
dont know where, it might even be down in the standard
library". Of course, you can discipline yourself into only
writing such functions in two steps, in the following way:

Definition equal (x y : A) : bool := ...
Lemma equal_1 (x y : A) : equal x y = true -> x = y.
Lemma equal_2 (x y : A) : equal x y = false -> x <> y.
Definition eq_dec (x y : A) : {x = y} + {x <> y}.
  case_eq (equal x y); intro H.
  left; exact (equal_1 _ _ H).
  right; exact (equal_2 _ _ H).
Defined.

but the truth is, if we were trusting our own discipline, we
wouldn't be using formal methods or Coq in the first
place... There were actually a lot of *_eq_dec or *_compare_dec
lemmas in the standard library which were not written in this way.
We think of the equality test (and use it) as a boolean function and
there is no reason to not implement it as a such just for the sake
of practical ease of reasoning.
For these reasons, I much prefer having a regular boolean
equality test, but the issue of easy reasoning by analysis
remains. This is why I define the inductive [equal_spec] as in
option #3:

Inductive equal_spec {A} (x y : A) : bool -> Prop :=
| equal_true : forall (Heq: x = y), equal_spec x y true
| equal_false : forall (Hneq: 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)
}.

and use it to specify the boolean equality test. By destructing a
term of type [equal_spec x y (equal x y)], you are, in one step,
destructing all occurrences of [equal x y] in your goal, and
getting the corresponding hypotheses added to your context in
each case. This is basically the exact same thing as performing
case analysis on the sumbool type in options #2,#4. I even name
hypotheses in the inductive definition so that they are always
introduced with 'predictable' names.

  1 subgoal
  A : Type
  EqA : EqDec A
  x : A
  y : A
  H : equal x y = true
======================
  x = y
> destruct (eq_dec x y).

  2 subgoals
  A : Type
  EqA : EqDec A
  x : A
  y : A
  H : true = true
  Heq : x = y
======================
  x = y
> assumption.

  2 subgoals
  A : Type
  EqA : EqDec A
  x : A
  y : A
  H : false = true
  Hneq : x <> y
======================
  x = y
> discriminate.

  Proof completed.

That's it, I've been verbose but I wanted to be as exhaustive and
clear as possible. I hope it helps you in deciding how you want
to define your decidable types.

Stéphane


2010/10/12 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)".
>



-- 
I'm the kind of guy that until it happens, I won't worry about it. -
R.H. RoY05, MVP06