idris - 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 在一个类型“土地” () 中并且 (S k) 在另一个土地上Void ?

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

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

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 .

要了解 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 类型的术语。 .

In what way can an Void output represent contradiction?

Void定义如下:

data Void : Type where

它没有构造函数!无论如何都无法创建这种类型的术语(在某些条件下:例如 Idris 的实现是正确的，并且 Idris 的底层逻辑是健全的，等等)。因此，如果某个函数声称它可以返回 Void 类型的术语。一定有什么可疑的事情发生。我们的函数说:如果你给我一个 Z = S n 的证明，我将返回一个空类型的术语。这意味着 Z = S n一开始就不能构造，因为它会导致矛盾。