The Coq mailing list

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

Hi Aaron, these are two goods questions you are raising, but it seems
to me they have more to do with habits you have than with flaws in the
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}.

The rationale behind my definition of EqDec class is that there are
two different "views" of equality: [equal] is for computations, i.e.
more generally for Set and above; while [eq_dec] is for Prop. What's
wrong with your lemma here is that since you wrote 'Lemma' you are
somehow thinking of it as a proposition and trying to prove it as
such, while this thing is really a program. You should  first use
[equal] to decide in which case of the sumbool you are, i.e. what
proof you are going to return, and then use [eq_dec] to make these two
proofs. 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.

In the first line, I use the computational view to remove the sumbool
and go down to Prop level, and then I can  use the logical view to
conclude.

> 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?

Indeed one solution would be to define [equal_spec] in Type, and I
once did that for a similar specification for ordered types. Pierre
Letouzey talked me out of it, and rightly so, because he convinced me
that [equal_spec] should not be a computational object and that Type
should only be for objects which have a computational interpretation,
for instance [equal_spec] should not end up in an extracted program.
If one needs the result in Type, one can prove it once and for all as
we did for the sumbool lemma above, but really I don't see any reason
why one would need that. Im intersted actually, were you trying to
prove this lemma for the sake of curiosity or did you find any use for
it ?

> Second (and indirectly related), consider this datatype:
>
> Inductive nat_tree: Set :=
> | node: nat -> list nat_tree -> nat_tree.
> ....
> However (and I think you know where this is going at this point :)),

Yes I am :) This has to do with the way you defined the nested
fixpoint. First of all, proving that [equal_spec x y (nat_tree_equal x
y)] holds for all trees [x] and [y] is no different from proving the
[nat_tree_eq_dec] lemma: its the same difficulty, with the same
induction principle and the same arguments etc. In particular in both
cases you are proving two results (one for trees, one for list of
trees) by mutual induction. 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. The only problem
is because of the way you defined [nat_tree_equal], you don't have
access to [list_nat_tree_equal] and therefore you cant express your
induction property easily. When using sumbool, the functions are
hidden in the proof therefore you don't need to have a name for them,
but if you separate proofs and programs you don't have that luxury
anymore (fortunately!). Note that it is not a useless constraint, it
also allows you to define an instance of EqDec (list nat_tree), wihch
you don't have otherwise. What you are doing is really proving two
instances by mutual induction, if you want.

So you should explicitely define the auxiliary function
[list_nat_tree_equal]. The support for nested induction in Coq is
really unsatisfactory, I grant you that, so here are are the two
"generic" ways of proceeding. 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. So I wrote
an extension which does all the tedious work of the second solution
automatically and I always use this solution.
Now assuming you have [list_nat_tree_equal] and an adequate induction
principle [nat_tree_mutual_ind] available, the definition of the
instance is simply:

Instance nat_tree_EqDec: EqDec nat_tree := {
  equal := nat_tree_equal
}.
Proof.
  intro x; pattern x; apply nat_tree_mutual_ind with
    (Pl := fun lx => forall ly, equal_spec lx ly list_nat_tree_equal lx ly));
    intros; simpl.
  (* lift *)
  destruct y; destruct (eq_dec n n0).
  fold list_nat_tree_equal; destruct (H l0); subst; constructor congruence.
  constructor congruence.
  (* nil *)
  destruct ly; constructor congruence.
  (* cons *)
  destruct ly; [constructor congruence |].
  destruct (H n); [destruct (H0 ly) |]; constructor congruence.
Qed.

but in practice I would probably first prove a lemma with both results
proved mutually, and then define two instances for trees and lists of
trees. To that end you can use "Combined Scheme" to combine the
induction principles for lists and lists of trees in one single
induction principle for the conjunction.

Combined Scheme nat_tree_combined from nat_tree_mutual_ind,
list_nat_tree_mutual_ind.
Theorem nat_tree_eq_dec :
  (forall t t', equal_spec t t' (nat_tree_equal t t')) /\
  (forall l l', equal_spec l l' (list_nat_tree_equal l l')).
....

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
}.

That's it, I hope this answers your questions.
Cheers,

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