Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Dependent Functions

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Dependent Functions


chronological Thread 
  • 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.





Archive powered by MhonArc 2.6.16.

Top of Page