Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] rose tree equality

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] rose tree equality


chronological Thread 
  • From: Pierre Courtieu <pierre.courtieu AT cnam.fr>
  • To: "Ethan Aubin" <ethan.aubin AT gmail.com>
  • Cc: coq-club AT pauillac.inria.fr
  • Subject: Re: [Coq-Club] rose tree equality
  • Date: Tue, 18 Sep 2007 08:46:26 +0200
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

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





Archive powered by MhonArc 2.6.16.

Top of Page