Search code examples
coq

Define a function based on a relation in Coq

I'm working on a theory in which there is a relation C defined as

Parameter Entity: Set.    
Parameter C : Entity -> Entity -> Entity -> Prop.

The relation C is a relation of composition of some entities. Instead of C z x y, I want to be able to write x o y = z. So I have two questions:

  • I think I should define a "function" (the word is perhaps not the right one) named fC that takes x and y and returns z. This way, I could use it in the Notation. But I don't know how to define this "function". Is it possible?
  • I find that I can use the command Notation to define an operator. Something like Notation "x o y" := fC x y.. Is this the good way to do it?

I tried Notation "x o y" := exists u, C u x y. but it didn't work. Is there a way to do what I want to do?

Solution

  • Unless your relation C has the property that, given x and y, there is a unique z such that C z x y, you cannot view it as representing a full-fledged function the way you suggest. This is why the notion of a relation is needed in that case.

    As for defining a notation for the relation property, you can use:

    Notation "x 'o y" := (exists u, C u x y) (at level 10).

    Note the ' before the o to help the parser handle the notation and the parentheses after the := sign. The level can be changed to suit your parsing preferences.