根据 Coq 中的关系定义函数答案

【问题标题】：Define a function based on a relation in Coq根据 Coq 中的关系定义函数
【发布时间】：2022-06-14 13:43:11
【问题描述】：

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

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

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

我想我应该定义一个名为 fC 的“函数”（这个词可能不是正确的），它接受 x 和 y 并返回 z。这样，我可以在 Notation 中使用它。但我不知道如何定义这个“功能”。有可能吗？
我发现我可以使用命令Notation 来定义一个运算符。像Notation "x o y" := fC x y. 这样的东西。这是实现它的好方法吗？

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

【问题讨论】：

标签： coq

【解决方案1】：

除非您的关系 C 具有以下属性，即在给定 x 和 y 时，存在一个唯一的 z，例如 C z x y，否则您无法将其视为代表完整功能的方式建议。这就是在这种情况下需要关系概念的原因。

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

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

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

【讨论】：

我想过，但忘了提。该理论有一个唯一性公理。
如果您没有明确的、有建设性的方式来定义fC，您可以随时添加另一个公理，正如 Pierre 所建议的那样。一个简单的版本可能是::Axiom functionalC : exists fC, forall x y z, C x y z <-> fC x y = z。然后，您可以在证明中使用它在功能和关系观点之间来回切换。 `.
在Coq FAQ 你有一个有用的公理列表，可以安全地添加到 Coq 中。 一般而言，承认一个新的即席公理可能会使开发变得不一致。

【解决方案2】：

如果您将x 'o y 定义为一个命题，您将失去o 作为Entity 上的二元运算的直觉（即 x o y 应该具有@ 类型987654327@).

你可以写一些变体，比如

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

【讨论】：