Idris 中的定理证明

Question

我正在阅读 Idris tutorial。而且我看不懂下面的代码。

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是空类型，用来证明某事是不可能的。

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

我的问题是：

哪个是等式证明？ (Z = S n)?
哪个是谓词？ disjointTy 函数?
disjointTy的目的是什么？ disjointTy Z = () 是否意味着 Z 在一个类型 "land" () 中并且 (S k) 在另一个土地 Void?
Void输出在哪些方面可以表示矛盾？

Ps。我所知道的证明是 "all things are no matched then it is false." 或 "find one thing that is contradictory"...

Answer 1

which one is an equality proof? (Z = S n)?

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

which one is a predicate? the disjointTy function?

是的，你是对的。

What's the purpose of 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 return 类型必须易于构造，例如单位类型是理想的选择。我们已经证明了 disjointTy 定义的 disjointTy Z = () 子句。当然这不是唯一的选择，我们可以使用任何其他有人居住的 (non-empty) 类型，例如 Bool 或 Nat 等

disjointTy 的第二个子句中的 return 值现在很明显了——我们希望 replace 到 return 一个 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.

类型项的能力

In what way can an Void output represent contradiction?

Void 定义如下：

data Void : Type where

它没有构造函数！无论如何都无法创建这种类型的术语（在某些情况下：比如 Idris 的实现是正确的并且 Idris 的底层逻辑是健全的，等等）。因此，如果某个函数声称它可以 return 类型为 Void 的术语，那么一定有什么可疑的事情发生了。我们的函数说：如果你给我一个 Z = S n 的证明，我将 return 一个 empty 类型的项。这意味着 Z = S n 不能首先构造，因为它会导致矛盾。

Answer 2

是的，p : x = y是等式证明。所以p是等式证明，Z = S k是等式。
也是，通常任何 P : a -> Type 都称为谓词，例如 IsSucc : Nat -> Type。在布尔逻辑中，谓词会将 Nat 映射为 true 或 false。在这里，如果我们可以为它构造一个证明，则谓词成立。如果我们可以构造它 (prf : ItIsSucc 4)，这是真的。如果我们无法构造它（ItIsSucc Z 中没有成员），它就是假的。
最后，我们想要Void。将replace调用读作Z = S k -> disjointTy Z -> disjointTy (S k)，即Z = S K -> () -> Void。所以 replace 需要两个参数：证明 p : Z = S k 和单位 () : ()，瞧，我们有一个 void。顺便说一句，你可以使用任何你可以构造的类型来代替 ()，例如disjointTy Z = Nat 然后使用 Z 而不是 ().
在依赖类型理论中，我们构建了类似 prf : IsSucc 4 的证明。我们会说，我们有 prf 证明 IsSucc 4 是真的。 prf 也称为 IsSucc 4 的见证人。但仅凭这一点，我们只能证明事情是真的。这是 Void:
的定义
data Void : Type where

没有构造函数。所以我们无法构建 Void 持有的证人。如果你以某种方式以 prf : Void 结束，那就有问题了，你就有了矛盾。

Idris 中的定理证明

Theorem Proving in Idris

theorem-proving

idris