The Coq mailing list

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

Hi Stéphane, thanks again for another very informative reply.

2010/10/15 Stéphane Lescuyer 
<stephane.lescuyer AT polytechnique.org>:
> Here is a script illustrating this:
>
> Lemma sumbool_EqDec {A} {E: EqDec A}:
>  forall (x y : A), {x = y} + {x <> y}.
> Proof.
>  intros; case_eq (equal x y); [left | right];
>    destruct (eq_dec x y); auto; discriminate.
> Qed.

Yes, I should have discovered this proof easily.  I was trying some
other tactics and getting stuck.  So, I guess nothing is actually
being lost by having equal_spec in Prop.

>> Second (and indirectly related), consider this datatype:
>>
>> Inductive nat_tree: Set :=
>> | node: nat -> list nat_tree -> nat_tree.
>> ....
> What is going wrong is that in the case of
>  [nat_tree_eq_dec] you are able to naturally express the two mutual
> results using [=]:
>
> - forall (t t' : nat_tree), {t = t'} + {t <> t'}.
> - forall (l l' : list nat_tree), {l = l'} + {l <> l'}.
>
> whereas in the first case you should have proved the two following
> results by mutual induction:
>
> - forall (t t' : nat_tree), equal_spec t t' (nat_tree_equal t t').
> - forall (l l' : list nat_tree), equal_spec l l' (list_nat_tree_eqal l l').
>
> and in both case the proof is quite straightforward.

Now I realize I was already very close to succeeding in doing what you
describe before I finally gave up!

> First solution is you define
> [nat_tree_equal] like you did, and then *after* you redefine
> [list_nat_tree_equal] exactly as it was and also prove an unfolding
> lemma for [nat_tree_equal]:
>
> Fixpoint list_nat_tree_equal (tl1 tl2 : list nat_tree) : bool :=
> 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
> Property nat_tree_equal_unfold : forall t t',
>  match t, t' with
>  | node n l, node n' l' =>
>    n == n' &&& list_nat_tree_equal l l'
>  end.
>
> and then you use [nat_tree_qual_unfold] instead of reduction (making
> [nat_tree_equal] after this lemma would help a lot). The other
> solution is defining [list_nat_tree_equal_] *before*, with an extra
> continuation function in parameter, and then define [nat_tree_equal]
> using this function and passing itself as the continuation.
>
> Section list_nat_tree_equal.
>  Variable nat_tree_equal : tree -> tree -> bool.
>  Fixpoint list_nat_tree_equal_ l l' :=
>    ....
> End list_nat_tree_equal.
> Definition nat_tree_equal t1 t2 :=
>  match t1, t2 with
>  | node n1 l1, node n2 l2 =>
>   n1 == n2 &&& list_nat_tree_equal_ nat_tree_equal l1 l2
>  end.
> Definition list_nat_tree_qual := list_nat_tree_equal_ nat_tree_equal.
>
> The second solution is much more verbose, but I don't like the first
> one because it requires me to explictely rewrite occurrences of
> [nat_tree_equal] instead of just relying on simplification.

I don't think there is as much difference here as you suggest.  In the
first case, you don't need any special unfolding property.  Although
one version of list_nat_tree_equal is buried in nat_tree_equal and the
other is a separate top-level definition, they are actually still
convertible, and I was able to complete my proof with a very simple
use of "fold" at the right time.

However, the second solution is actually slightly *less* verbose, as
far as I can tell.  The use of "Section" is unnecessary if you do
this:

Definition list_nat_tree_equal (nat_tree_equal: tree -> tree -> bool) :=
  let fix tl_equal tl1 tl2 :=
    ...
  in tl_equal.

And doing things in this way, there is no real duplication of code, as
in the first case.

> Instance nat_tree_EqDec := {
>  equal := nat_tree_equal;
>  eq_dec := proj1 nat_tree_eq_dec
> }.
> Instance list_nat_tree_EqDec := {
>  equal := list_nat_tree_equal;
>  eq_dec := proj2 nat_tree_eq_dec
> }.

Assuming one already has a generic EqDec instance for the list type, I
don't see the need for the Instance definition above.  In fact, they
would actually conflict, which might be confusing (although the
conflicting instances might be equivalent and even convertible if one
is lucky).

 - Aaron