Idris定理证明：disjoint函数代码及等式证明相关疑问

首先直接给你答案：没错，你说的Z = S n就是那个等式命题，而函数参数p就是这个命题的“证明”——当然我们知道这个命题是不可能成立的，这段代码就是用Idris的类型系统来严格证明这一点。

咱们一步一步拆解这段代码：

1. 函数签名的意义 #

先看函数的类型声明：

disjoint : (n : Nat) -> Z = S n -> Void

它的意思是：对于任意自然数n，如果有人能提供一个“Z等于S n”的证明（也就是参数p），那我们就能构造出一个Void类型的值。而Void是空类型，根本没有合法的值——这就相当于说，不可能存在这样的证明p，也就是“Z = S n”这个命题是绝对假的。

2. 自定义谓词disjointTy的作用 #

函数内部的where块定义了一个谓词disjointTy：

disjointTy : Nat -> Type
disjointTy Z = ()
disjointTy (S k) = Void

这个谓词给不同的自然数绑定了不同的类型：

• 当输入是Z（也就是0）时，它对应单位类型()——这个类型有一个现成的值，就是()本身，很容易构造。
• 当输入是S k（任意自然数的后继，也就是大于0的数）时，它对应空类型Void——这个类型没有任何合法值。

3. replace如何利用等式证明导出矛盾 #

核心就是这行代码：

replace {P = disjointTy} p ()

结合你已经了解的replace的类型(x = y) -> P x -> P y，这里的参数对应关系是：

• x是Z，y是S n
• P就是我们定义的disjointTy
• p就是Z = S n的等式证明（也就是你疑惑的那个等式对应的证明参数）
• P x就是disjointTy Z，也就是()，我们传入的()就是这个类型的合法值

根据replace的逻辑，既然p证明了Z和S n相等，那我们就可以把P Z的一个值（()）转换成P (S n)的一个值。而P (S n)就是Void——这就意味着，只要p存在，我们就能构造出一个Void类型的值，这显然是矛盾的（因为Void没有值）。

所以这段代码的本质就是：假设存在“Z = S n”的证明p，我们就能导出矛盾，反过来证明这样的p根本不可能存在，完美实现了函数要做的“证明0和任何后继数不相交（不可能相等）”的目标。

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