coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Adam Chlipala <adamc AT hcoop.net>
- To: Jeff Terrell <jeff AT kc.com>
- Cc: coq-club AT pauillac.inria.fr
- Subject: Re: [Coq-Club] Dependent Functions
- Date: Tue, 31 Mar 2009 13:15:50 -0400
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Jeff Terrell wrote:
I'm trying to construct the proof of a transformation - please see the attached class diagram. Informally, the transformation is as follows:
Map every instance of A to an instance of X.
Map every instance of B to an instance of Y, provided that the instance of A to which B is related via R1, is different from the instance of A to which B is related via R2.
The diagram also shows an example input model and the corresponding output model.
I originally represented the classes as mutually inductive types, but I gather that would lead to a model that couldn't be instantiated.
I have a feeling that you would be better off using relations instead of recursive datatypes.
- [Coq-Club] Dependent Functions, Jeff Terrell
- Re: [Coq-Club] Dependent Functions,
Adam Chlipala
- Re: [Coq-Club] Dependent Functions,
Jeff Terrell
- Re: [Coq-Club] Dependent Functions, Adam Chlipala
- Re: [Coq-Club] Dependent Functions,
Jeff Terrell
- Re: [Coq-Club] Dependent Functions,
Adam Chlipala
Archive powered by MhonArc 2.6.16.