idris - idris 定理证明

我正在阅读 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) 在另一个land Void 中？

Void 输出以什么方式表示矛盾？

附言。我所知道的证明是“所有的东西都不匹配，那么它就是错误的”。或“找出一件自相矛盾的事情”...

最佳答案

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



是的，你是对的。



让我在这里重复一下 disjointTy 的定义:

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

disjointTy 的目的是成为 replace 函数需要的谓词。这种考虑决定了 disjointTy 的类型，即。 [domain] -> Type 。由于我们在自然数之间具有相等性，因此 [domain] 是 Nat 。

要了解 body 是如何构建的，我们需要再看一次 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 = () 定义的 disjointTy 子句。当然这不是唯一的选择，我们可以使用任何其他有人居住的(非空)类型，如 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 不能首先构造，因为它会导致矛盾。

关于idris - idris 定理证明，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/49528519/