The Coq mailing list

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

>> 2010/10/12 Stéphane Lescuyer 
>>Â <stephane.lescuyer AT polytechnique.org>:
>>> 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)
>>> }.

Hi Stéphane, I have two more issues to bring up regarding this approach.

First, it seems that this information in your EqDec class is weaker
than the information in an EqDec class using sumbool, i.e., it does
not appear possible to prove the following lemma:

Lemma sumbool_EqDec {A} {E: EqDec A}:
  forall (x y: A), {x = y} + {x <> y}.

However, if you declare equal_spec in Set rather than Prop, it is easy
to prove such a lemma.  Is there a reason you prefer equal_spec to be
in Prop?

Second (and indirectly related), consider this datatype:

Inductive nat_tree: Set :=
| node: nat -> list nat_tree -> nat_tree.

Now I can define a boolean equality function on such a type without
too much trouble:

Fixpoint nat_tree_equal (t1 t2: nat_tree): bool :=
  let fix list_nat_tree_equal (tl1 tl2: list nat_tree) :=
    match tl1, tl2 with
    | nil, nil => true
    | cons t1' tl1', cons t2' tl2' =>
        nat_tree_equal t1' t2' && list_nat_tree_equal tl1' tl2'
    | _, _ => false
    end
  in
  match t1, t2 with
  | node n1 tl1, node n2 tl2 =>
      equal n1 n2 && list_nat_tree_equal tl1 tl2
  end.

However (and I think you know where this is going at this point :)),
now I want to declare nat_tree as an instance of EqDec:

Instance nat_tree_EqDec: EqDec nat_tree := {
  equal := nat_tree_equal
}.
Proof.
  (* good luck! *)
Abort.

This is not to say I cannot construct such an instance, BUT the only
way I have found to do so is like this:

Definition nat_tree_eq_dec:
  forall (t1 t2: nat_tree), {t1 = t2} + {t1 <> t2}.
Proof.
  (* a straightforward proof, once a useful induction principle for
the type has been proved *)
Defined.

Instance nat_tree_EqDec: EqDec nat_tree := {
  equal t1 t2 := if nat_tree_eq_dec t1 t2 then true else false
}.
Proof.
  (* a trivial proof *)
Defined.

I'm not really complaining about this, just wondering if I'm doing
things the right way...

 - Aaron