Idris中的定理证明

Question

我正在阅读 Idris 教程，但是我无法理解以下代码。

disjoint : (n : Nat) -> Z = S n -> Void
disjoint n p = replace {P = disjointTy} p ()
  where
    disjointTy : Nat -> Type
    disjointTy Z = () 
    disjointTy (S k) = Void

到目前为止，我了解到的是......Void是一个空类型，用于证明某些事情是不可能的。

replace: (x = y) -> P x -> P y replace使用等式证明来转换谓词。

我的问题是：

1. 哪个是等式证明？(Z = S n)?

2. 哪个是谓词？disjointTy函数？

3. disjointTy的目的是什么？disjointTy Z = ()表示Z在一个类型“领域”()中，而(S k)在另一个领域Void中吗？

4. 以何种方式可以将Void输出表示矛盾？

附注：我知道关于证明的只有“所有事物都不匹配，那么它就是假的”，或者“找到一个矛盾的东西”...

- Johnny Liao

Answer 1

哪一个是相等证明？(Z = S n)?

这里的相等证明是参数p。类型为Z = S n。

哪个是谓词？disjointTy函数？

是的，你说得对。

disjointTy 的目的是什么？

让我重复一下disjointTy的定义：

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

disjointTy的目的是作为replace函数所需的谓词。这一点决定了disjointTy的类型，即[domain] -> Type。由于自然数之间具有相等性，[domain]是Nat。

要理解构造方法，我们需要再次查看replace：

replace : (x = y) -> P x -> P y

请注意，我们已经有p个Z = S n，因此上述类型中的x是Z，y是S n。调用replace需要构造一个类型为P x的项，即在我们的情况下P Z。这意味着P Z的返回类型必须容易构造，例如，单位类型是理想的候选对象。我们已经证明了disjointTy Z = ()定义中的条款。当然，这不是唯一的选择，我们可以使用任何其他有人居住（非空）类型，例如Bool或Nat等。

现在，我们很容易看出disjointTy的第二个条款中的返回值--我们希望replace返回Void类型的值，因此P (S n)必须是Void。

接下来，我们像这样使用disjointTy：

replace   {P = disjointTy}   p    ()
           ^                 ^    ^
           |                 |    |
           |                 |    the value of `()` type
           |                 |
           |                 proof term of Z = S n 
           |
           we are saying "this is the predicate"

作为加分项，这里有一种替代的证明方法：

disjoint : (n : Nat) -> Z = S n -> Void
disjoint n p = replace {P = disjointTy} p False
  where
    disjointTy : Nat -> Type
    disjointTy Z = Bool
    disjointTy (S k) = Void

我已经使用了False，但也可以使用True——这并不重要。重要的是我们能够构建一个类型为disjointTy Z的术语。

无类型输出如何表示矛盾？

Void的定义如下：

data Void : Type where

它没有构造函数！根据某些条件（例如Idris的实现正确且Idris的基本逻辑是合理的等），无论如何都无法创建此类型的术语。因此，如果某个函数声称它可以返回Void类型的术语，则必须有一些可疑的事情正在发生。我们的函数说：如果您给我一个Z = S n的证明，我将返回一个空类型的术语。这意味着首先无法构建Z = S n，因为它会导致矛盾。请注意保留HTML标记，但不要写解释。

- Anton Trunov

Answer 2

1. 是的，p : x = y 是一个等式证明。因此，p 是一个等式证明，Z = S k 是一个等式类型。
2. 同样地，通常任何 P : a -> Type 都被称为谓词，比如 IsSucc : Nat -> Type。在布尔逻辑中，谓词将 Nat 映射为 true 或 false。在这里，如果我们可以构造出一个证明，则谓词成立（prf : ItIsSucc 4）。如果我们不能构造它（ItIsSucc Z 中没有成员），则它为假。
3. 最后，我们想要 Void。将 replace 调用解读为 Z = S k -> disjointTy Z -> disjointTy (S k)，即 Z = S K -> () -> Void。因此，replace 需要两个参数：证明 p : Z = S k 和单元 () : ()，然后我们就有了一个 void。顺便说一下，您可以使用任何您可以构造的类型，例如 disjointTy Z = Nat，然后使用 Z 替代 ()。

4. 在依赖类型理论中，我们构造像 prf : IsSucc 4 这样的证明。我们会说，我们有一个证明 prf，证明了 IsSucc 4 是真的。prf 也被称为 IsSucc 4 的证人。但仅凭这些，我们只能证明事情是真实的。这是 Void 的定义：

   data Void : Type where

   没有构造器。因此，我们无法构造一个证人表明 Void 成立。如果您以某种方式获得了一个 prf : Void，则说明出现了错误并且存在矛盾。

- xash