The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

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.