Coq中Mereology定义的参数合理性及iota算子x-y实现咨询

我正在用Cotnoir和Varzi（2021）所著的《Mereology》练习证明能力。书中基于原始二元关系P给出如下定义：

(D1) PPxy := Pxy /\ ~ (x = y)
(D2) Oxy := ∃z (Pzx /\ Pzy)
(D3) Uxy := ∃z (Pxz /\ Pyz)
(D4) Dxy := ~∃z (Pzx /\ Pzy)
(D5) x - y := ιz∀w (Pwz <-> (Pwx /\ Dwy))

我已将原始概念和前四个定义编码如下：

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

Definition PP x y := P x y /\ x <> y.
Definition O x y := exists z, P z x /\ P z y.
Definition U x y := exists z, P x z /\ P y z.
Definition D x y := ~ exists z, P z x /\ P z y.

但我不知道如何编码第五个定义。我确定它应该是类型为Entity -> Entity -> Entity的函数，因为iota算子（ι）指向满足后续公式的唯一z，因此x - y应返回该z。

我尝试用符号定义：

Notation "x - y" := (exists z, forall w ,(P w z <-> (P w x /\ D w y))).

但如预期，这不是我想要的。我检查了x - y的类型：

Variables x y: Entity.
Check x - y.

得到的类型是Prop而非Entity。

我找到了Coq标准库中的ClassicalDescription模块，其中定义了iota算子，但我不知道如何使用它。

因此我有两个问题：

1. 我的实现选择（特别是Parameter Entity和P）是否正确？
2. 如果正确，我该如何实现x - y操作？

问题1：关于Parameter的选择是否正确 #

你的实现选择是合理的。用Parameter声明Entity作为集合、P作为实体间的二元关系，完全符合分体论中把P（部分关系）作为原始概念的设定。这种方式可以让你在后续证明中基于这些未定义的原始概念，添加分体论的公理（比如自反性、传递性、反对称性等）来约束P的行为，是Coq中形式化这类理论的标准做法。

问题2：实现x - y操作 #

要实现带iota算子的x - y，你需要用到ClassicalDescription库中的iota算子，它的作用是从满足某个性质的唯一元素中提取出该元素。具体步骤如下：

步骤1：导入所需库 #

首先需要导入经典描述库及依赖的经典逻辑库：

Require Import Coq.Logic.ClassicalDescription.
Require Import Coq.Logic.Classical.

步骤2：定义差运算的核心性质 #

先定义一个谓词，描述z满足x - y的条件：

Definition diff_property (x y z : Entity) :=
  forall w : Entity, P w z <-> (P w x /\ D w y).

步骤3：用iota算子实现差运算 #

iota算子的类型是forall (A:Type) (P:A->Prop), (exists! x, P x) -> A，它要求你证明存在唯一的z满足diff_property x y z。在分体论中，这个唯一性通常由外延性公理保证（如果两个实体的所有部分都相同，则它们相等）。

你可以先定义依赖唯一存在性证明的差运算：

Definition diff (x y : Entity) (H : exists! z, diff_property x y z) : Entity :=
  iota Entity (diff_property x y) H.

步骤4：添加符号简化写法 #

为了贴近书中的x - y形式，定义对应符号：

Notation "x - y" := (diff x y _) (at level 50, left associativity).

这里的_表示使用时需要传入唯一存在性的证明。如果你的分体论公理已经能保证差运算的唯一存在性，可以添加全局公理：

Axiom diff_unique : forall x y, exists! z, diff_property x y z.

之后可以直接封装成无需手动传参的定义：

Definition diff x y : Entity :=
  iota Entity (diff_property x y) (diff_unique x y).

Notation "x - y" := (diff x y) (at level 50, left associativity).

验证类型 #

现在检查x - y的类型：

Variables x y : Entity.
Check x - y.

会得到Entity类型，符合你的需求。

内容的提问来源于stack exchange，提问作者Lepticed