coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] rose tree equality

From: "Ethan Aubin" <ethan.aubin AT gmail.com>
To: coq-club AT pauillac.inria.fr
Subject: [Coq-Club] rose tree equality
Date: Mon, 17 Sep 2007 22:50:56 -0400
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=beta; h=received:message-id:date:from:to:subject:mime-version:content-type; b=gY3iY+/UPd9c4uDPwJCF4hGcWrPDQ3TF3FSl5YQ9mwac+Hwte+AU3qWr6eXhVVCR91qQfTteDBi2N36vj4ViodEzA5DNGVfvU9/B2ONb6g8KLYoIdifFnmv221iqV/hv43mVJIdE/PD7lLENdrKxoFDk+M4oVYXJ597pbOstGGM=
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

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

[Coq-Club] rose tree equality, Ethan Aubin
- Re: [Coq-Club] rose tree equality, Pierre Courtieu
  - Re: [Coq-Club] rose tree equality, Yves Bertot
    - Re: [Coq-Club] rose tree equality, roconnor