基于 Coq 中的关系定义函数

Question

我正在研究一个理论，其中关系 C 定义为

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

关系C是一些实体的组合关系。我希望能够写 x o y = z 而不是 C z x y。所以我有两个问题：

我想我应该定义一个名为 fC 的“函数”（这个词可能不合适），它接受 x 和 y 以及 returns z。这样，我就可以在 Notation 中使用它。但我不知道如何定义这个“功能”。可能吗？
我发现我可以使用命令Notation来定义一个运算符。类似于 Notation "x o y" := fC x y.。这是解决问题的好方法吗？

我试过 Notation "x o y" := exists u, C u x y. 但没用。有没有办法做我想做的事？

Answer 1

除非你的关系 C 具有属性，即给定 x 和 y，存在唯一的 z 使得 C z x y，您不能按照您建议的方式将其视为代表 full-fledged 函数。这就是为什么在这种情况下需要关系的概念。

至于为关系属性定义符号，您可以使用：

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

注意 o 之前的 ' 以帮助解析器处理 := 符号之后的符号和括号。可以更改级别以适合您的解析首选项。

Answer 2

如果你将x 'o y定义为一个命题，你将失去o是对Entity的二元运算的直觉（即 x o y 应该有类型 Entity).

你可以写一些像

这样的变体

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

否则，如果你的关系满足：

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

那么你可以定义：

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

否则（如果您只有 C_fun 的较弱版本，使用 exists 而不是 sig）并接受使用经典逻辑和公理），您可以使用Epsilon 运算符 https://coq.inria.fr/distrib/current/stdlib/Coq.Logic.ClassicalEpsilon.html

Define a function based on a relation in Coq