The Coq mailing list

[Yves Bertot <Yves.Bertot AT sophia.inria.fr>]

Pierre Courtieu wrote:
> Le Mon, 17 Sep 2007 22:50:56 -0400, "Ethan Aubin"
> <ethan.aubin AT gmail.com>
>  a écrit:
>   
> > Hi, I'm stuck trying to prove decidable equality for rose trees
> >
> >     Inductive rose := Rose : nat -> list rose -> rose.
> >
> >     Lemma rose_eq_dec : forall (x y:rose), {x=y}+{x<>y}.
> >
> > decide equality seems to need rose_eq_dec in the context to pass to
> > list_eq_dec. induction on x doesn't add an induction hypothesis (because the
> > subtrees are contained in the list?). Whats the strategy to solve a problem
> > like this? Many thanks- Ethan
> >     
>
>
> You need to build and proof the right induction principle first, as the
> default one built by coq is not powerfull enough.
>
>   
Rose trees are described in the Coq'Art book, under a different name 
(they are called ltree).
The technique to build the right induction principle is also described: 
Chapter 14, Section 3.3.

Even if you don't have a paper copy of the book, the example appears on 
the web-site for
the book:

http://www.labri.fr/perso/casteran/CoqArt/induc-fond/SRC/chap14.v

Look for ltree and ltree_ind2.

You will need to transpose ltree_ind2 for your needs.  For instance, you 
can try to define
directly your equality decision function using the same structure (this 
may be a little difficult).
If you prefer, you can define ltree_rec2 to work with a P and Q in sort 
Type or Set, and then
define your own function in proof mode (this should be easier).

Now, Pierre's proposal to use a pair of mutually inductive types is 
viable alternative.

Yves