The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT cnam.fr>]

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.

You may consider defining rose tree with a mutual inductive type and
define (the rose and list_rose) and use the Scheme command to build
the good induction Scheme.

Regards,
Pierre Courtieu