如何在 Coq 中编写 iota 描述符？

Question

我正在使用 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

。

在Google上搜索后，我在标准库中找到了这个：Library Coq.Logic.ClassicalDescription，特别是iota运算符的定义，但我不明白如何使用它。

因此，我有两个问题：我的实施选择（特别是

Parameter

s

Entity

和

P

）可以吗？如果是这样，我该如何实现操作“x - y”？

Answer 1

在

https://coq-community.org/hydra-battles/doc/hydras.pdf

（从第 163 页开始）中有一个使用

iota

和 epsilon 运算符的示例的简短描述。

例如，任何序数的后继由

定义

Definition succ (alpha : Ord)
  := the_least (fun beta => alpha < beta).

其中

the_least

是根据

iota

定义的。

还有一些定义和简单的引理https://github.com/coq-community/hydra-battles/blob/master/theories/ordinals/Schutte/MoreEpsilonIota.v