coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club]theorems from inductive type declarations

From: "Ethan Aubin" <ethan.aubin AT gmail.com>
To: coq-club AT pauillac.inria.fr
Subject: [Coq-Club]theorems from inductive type declarations
Date: Mon, 17 Apr 2006 16:02:54 -0400
Domainkey-signature: a=rsa-sha1; q=dns; c=nofws; s=beta; d=gmail.com; h=received:message-id:date:from:to:subject:mime-version:content-type:content-transfer-encoding:content-disposition; b=toVFr7DHiNijja2ZyHvqC8MOpNiSc0QhZ9MlTlJUM4Kyw5ic3kGW6+ViSIXvy/BEUkxf0VUyL4Eq8tJWFMMJEpJLZuHLJtgqeCIIvxYfPLIVGEtVeYq3+EHwSLF48TEcP1xkYRtHpwO8PMTXja3v+loeoqyJdUSnQlLUi9QLDsM=
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Hi, I'm wondering if/how coq can be made to generate additional
lemmas on a per inductive type basis.

More specifically, I'd like to generate a 'fold-fusion' and
'fold-unfold' theorem from the datatype definition. Can anyone point
me in the right direction? Thanks! - Ethan

[Coq-Club]theorems from inductive type declarations, Ethan Aubin