Idris 中的定理证明

Question

我正在阅读伊德里斯教程。而且我无法理解下面的代码。

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 替换使用等式证明来转换谓词。

我的问题是：

1. 哪一个是平等证明？(Z = S n)？

2. 哪一个是谓词？功能disjointTy？

3. 目的是什么disjointTy？disjointTy Z = () 是否意味着 Z 位于一个类型“land”() 中且 (S k) 位于另一块土地中Void？

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

诗。我所知道的证明是“凡事不匹配则为假”。或者“找到一件矛盾的事情”......

Answer 1

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

这里的参数p就是等式证明。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

回想一下，我们有pof Z = S n，所以x从上面的类型可以看出 isZ和yis S n。要调用，replace我们需要构造一个类型为 的术语P x，即P Z在我们的例子中。这意味着类型P Z返回必须易于构造，例如单元类型是理想的候选者。我们有 的disjointTy Z = ()定义的合理子句disjointTy。当然，这不是唯一的选择，我们可以使用任何其他有人居住（非空）类型，例如BoolorNat等​​。

第二个子句中的返回值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 输出以什么方式表示矛盾？

Void定义如下：

data Void : Type where

它没有构造函数！无论如何，都无法创建这种类型的术语（在某些条件下：比如 Idris 的实现是正确的，并且 Idris 的底层逻辑是健全的，等等）。因此，如果某个函数声称它可以返回一个类型项，Void那么一定有什么可疑之处。我们的函数说：如果你给我一个 的证明Z = S n，我将返回一个空类型的项。这种方式Z = S n一开始就不能被构造，因为它会导致矛盾。