CODEWITHSUNDEEP
coq
Lepticed
Lepticed

Reputation: 381

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 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?

Upvotes: 0

Views: 215

Answers (2)

Pierre Castéran
Pierre Castéran

Reputation: 916

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

Upvotes: 1

Pierre Jouvelot
Pierre Jouvelot

Reputation: 923

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.

Upvotes: 2

Related Questions