'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 question:

  • 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. Somethin like Notation "x o y" := fC x y.. Is this the good way to 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?

coq


Solution 1:[1]

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.

Solution 2:[2]

If you define x 'o y as a proposition, you will lose the intuition of o being a binary operation on Entity (i.e x o y should have type Entity).

You may write some variation like

Notation "x 'o y '= z" := (unique (fun t => C t x y)) (at level 10).

Otherwise, If your relation satisfies:

Hypothesis C_fun: forall x y,  {z : Entity | unique  (fun t => C t x y) z}.

then you may define:

Notation "x 'o y" := (proj1_sig (C_fun x y)) (at level 10).
Check fun a b: Entity =>  a 'o b.

Otherwise (if you have only have a weaker version of C_fun, with existsinstead of sig) and accept to use classical logic and axioms), you may use the Epsilon operator https://coq.inria.fr/distrib/current/stdlib/Coq.Logic.ClassicalEpsilon.html

Sources

This article follows the attribution requirements of Stack Overflow and is licensed under CC BY-SA 3.0.

Source: Stack Overflow

Solution Source
Solution 1 Pierre Jouvelot
Solution 2 Pierre Castéran

Related Questions