定理证明

等式（Equality）

Idris 允许声明命题等式（propositional equality），从而可以对程序陈述和证明定理。Prelude（预定义库）中定义的等式类型如下：

data Equal : a -> b -> Type where
     Refl : Equal x x

作为记号上的简化，Equal x y 可以写作 x = y。任意类型的任意值之间都可以提出等式，但只有在值实际相等时才能构造等式的证明。例如：

fiveIsFive : 5 = 5
fiveIsFive = Refl

twoPlusTwo : 2 + 2 = 4
twoPlusTwo = Refl

如果我们尝试……

twoPlusTwoBad : 2 + 2 = 5
twoPlusTwoBad = Refl

……那么会得到一个错误：

Proofs.idr:8:17--10:1:While processing right hand side of Main.twoPlusTwoBad at Proofs.idr:8:1--10:1:
When unifying 4 = 4 and (fromInteger 2 + fromInteger 2) = (fromInteger 5)
Mismatch between:
        4
and
        5

空类型（Empty Type）

有一种空类型 Void，它没有任何构造函数，因此无法构造出空类型的规范元素。我们可以利用空类型来证明某些事情不可能发生，例如 0 永远不等于任意后继数：

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

如果你现在还不能完全理解其工作原理，不用担心——本质上，这里使用了库函数 replace，它通过等式证明来转换谓词。在这里，我们用它将一个可以存在的类型（空元组）的值，通过一个不可能存在的证明，转换为一个不可能存在的类型的值。

一旦我们得到了空类型的元素，就可以证明任何命题。库中定义了 void，用于辅助反证法（proof by contradiction）。

void : Void -> a

定理证明

在对依值类型进行类型检查时，类型本身会被*归约*（normalise）。假设我们想要证明关于 plus 归约行为的如下定理：

plusReduces : (n:Nat) -> plus Z n = n

我们像写程序类型一样写下了定理的陈述。实际上，证明和程序之间并没有本质区别。就本节而言，证明只是一个具有足够精确类型的程序，用以保证某个特定性质成立。

这里不做详细展开，Curry-Howard 对应（Curry-Howard correspondence）[#Timothy]_ 解释了这种关系。该证明本身是直接的，因为根据 plus 的定义，plus Z n 会归约为 n：

plusReduces n = Refl

如果我们将参数顺序调换，证明会稍微复杂一些，因为 plus 是按第一个参数递归定义的。此时，证明也需要对 plus 的第一个参数（即 n）递归进行。

plusReducesZ : (n:Nat) -> n = plus n Z
plusReducesZ Z = Refl
plusReducesZ (S k) = cong S (plusReducesZ k)

cong 是库中定义的一个函数，表明等式在函数应用下是保持的（即等式对函数应用封闭）：

cong : (f : t -> u) -> a = b -> f a = f b

要了解更多细节，我们可以将对 plusReducesZ 的递归调用替换为一个洞（hole）：

plusReducesZ (S k) = cong S ?help

然后在 REPL 中查看该洞的类型，可以看到：

Main> :t help
   k : Nat
-------------------------------------
help : k = (plus k Z)

我们也可以对 plus 在后继数（successor）上的归约行为做类似的证明：

plusReducesS : (n:Nat) -> (m:Nat) -> S (plus n m) = plus n (S m)
plusReducesS Z m = Refl
plusReducesS (S k) m = cong S (plusReducesS k m)

即使是这些简单的定理，一次性构造出完整证明也有些困难。当问题稍微复杂一点时，用这种"批处理模式"来构造证明就会变得难以掌控。

Idris 提供了交互式编辑功能，可以帮助构造证明。关于如何在编辑器中交互式构造证明，详见定理证明。

定理在实践中的应用

在实际编程中，证明定理的需求会自然而然地出现。例如，前文（视图与“with”规则）我们用 parity 函数实现了 natToBin：

parity : (n:Nat) -> Parity n

我们给出了 parity 的定义，但没有解释。我们可能希望它看起来像下面这样：

parity : (n:Nat) -> Parity n
parity Z     = Even {n=Z}
parity (S Z) = Odd {n=Z}
parity (S (S k)) with (parity k)
  parity (S (S (j + j)))     | Even = Even {n=S j}
  parity (S (S (S (j + j)))) | Odd  = Odd {n=S j}

但遗憾的是，这会因类型错误而失败：

With.idr:26:17--27:3:While processing right hand side of Main.with block in 2419 at With.idr:24:3--27:3:
Can't solve constraint between:
        plus j (S j)
and
        S (plus j j)

问题在于，将 S j + S j 归约到 Even 的类型时，并不能得到 Parity 右侧所需的类型。我们知道 S (S (plus j j)) 等于 S j + S j，但需要用证明向 Idris 说明。我们可以先在定义中加上一些*洞*（hole）（见完全性和覆盖性）：

parity : (n:Nat) -> Parity n
parity Z     = Even {n=Z}
parity (S Z) = Odd {n=Z}
parity (S (S k)) with (parity k)
  parity (S (S (j + j)))     | Even = let result = Even {n=S j} in
                                          ?helpEven
  parity (S (S (S (j + j)))) | Odd  = let result = Odd {n=S j} in
                                          ?helpOdd

检查 helpEven 的类型，可以看到在 Even 情况下需要证明什么：

  j : Nat
  result : Parity (S (plus j (S j)))
--------------------------------------
helpEven : Parity (S (S (plus j j)))

因此，我们可以编写一个辅助函数，将类型*重写*为我们需要的形式：

helpEven : (j : Nat) -> Parity (S j + S j) -> Parity (S (S (plus j j)))
helpEven j p = rewrite plusSuccRightSucc j j in p

rewrite ... in 语法允许你根据等式证明重写表达式的类型。在这里，我们用到了 plusSuccRightSucc，其类型如下：

plusSuccRightSucc : (left : Nat) -> (right : Nat) -> S (left + right) = left + S right

我们可以通过将 helpEven 右侧替换为一个洞（hole），逐步观察 rewrite 的效果。首先如下：

helpEven : (j : Nat) -> Parity (S j + S j) -> Parity (S (S (plus j j)))
helpEven j p = ?helpEven_rhs

我们可以查看 helpEven_rhs 的类型：

  j : Nat
  p : Parity (S (plus j (S j)))
--------------------------------------
helpEven_rhs : Parity (S (S (plus j j)))

然后我们可以用 plusSuccRightSucc j j 进行 rewrite，得到等式 S (j + j) = j + S j，从而将类型中的 S (j + j)``（在本例中即 ``S (plus j j)，因为 S (j + j) 会归约为它）替换为 j + S j：

helpEven : (j : Nat) -> Parity (S j + S j) -> Parity (S (S (plus j j)))
helpEven j p = rewrite plusSuccRightSucc j j in ?helpEven_rhs

现在检查 helpEven_rhs 的类型，可以看到发生了什么，包括刚才用到的等式的类型（作为 _rewrite_rule 的类型）：

Main> :t helpEven_rhs
   j : Nat
   p : Parity (S (plus j (S j)))
-------------------------------------
helpEven_rhs : Parity (S (plus j (S j)))

结合 rewrite 和另一个用于 Odd 情况的辅助函数，我们可以如下完成 parity：

helpEven : (j : Nat) -> Parity (S j + S j) -> Parity (S (S (plus j j)))
helpEven j p = rewrite plusSuccRightSucc j j in p

helpOdd : (j : Nat) -> Parity (S (S (j + S j))) -> Parity (S (S (S (j + j))))
helpOdd j p = rewrite plusSuccRightSucc j j in p

parity : (n:Nat) -> Parity n
parity Z     = Even {n=Z}
parity (S Z) = Odd {n=Z}
parity (S (S k)) with (parity k)
  parity (S (S (j + j)))     | Even = helpEven j (Even {n = S j})
  parity (S (S (S (j + j)))) | Odd  = helpOdd j (Odd {n = S j})

rewrite 的全部细节超出了本入门教程的范围，但可在定理证明教程中找到（见定理证明）。

完备性检查（Totality Checking）

如果我们真的想信任我们的证明，重要的一点是它们必须由*完备*（total）函数定义——即对所有可能输入都有定义，并且保证终止。否则我们就可能构造出空类型的元素，从而可以证明任何命题：

-- making use of 'hd' being partially defined
empty1 : Void
empty1 = hd [] where
    hd : List a -> a
    hd (x :: xs) = x

-- not terminating
empty2 : Void
empty2 = empty2

在内部，Idris 会检查每个定义的完备性，我们也可以用 :total 命令在提示符下检查。从结果可以看到，上述两个定义都不是完备的：

Void> :total empty1
Void.empty1 is not covering due to call to function empty1:hd
Void> :total empty2
Void.empty2 is possibly not terminating due to recursive path Void.empty2

注意这里用了“可能（possibly）”一词——由于停机问题不可判定，完备性检查永远无法百分百确定。因此该检查是保守的。我们也可以（尤其在证明时建议）将函数标记为完备，这样如果检查失败就会在编译时报错：

total empty2 : Void
empty2 = empty2

令人欣慰的是，我们在空类型（Empty Type）节中关于 0 和后继构造子互斥的证明是完备的：

Main> :total disjoint
Main.disjoint is Total

完备性检查必然是保守的。要被认定为完备，函数 f 必须：

覆盖所有可能的输入
*良基*（well-founded）——即在一系列（可能互相递归的）调用再次到达 f 时，必须能证明某个参数变小了。
不能使用任何非*严格正*（strictly positive）的数据类型
不能调用任何非完备函数

完备性相关指令与编译器选项

警告

并非所有这些特性都已在 Idris 2 中实现

默认情况下，Idris 允许所有类型良好的定义，无论是否完备。但尽量让函数完备是有益的，因为这能保证它们对所有输入都能在有限时间内给出结果。我们可以通过以下方式强制要求函数完备：

通过使用 --total 编译器选项。
在源文件中添加 %default total 指令。此后所有定义都要求完备，除非显式标记为 partial。

所有在 %default total 声明之后的函数都要求完备。相应地，在 %default partial 声明之后，这一要求会放宽。

最后，编译器选项 --warnpartial 会对所有未声明为 partial 的非完备函数发出警告。

完备性检查相关问题

请注意，完备性检查器并不完美！首先，由于停机问题不可判定，它必然是保守的，因此许多实际上是完备的程序也可能不会被检测出来。其次，目前的实现还不够完善，可能会有一些实际上不完备的函数被误判为完备。在正式证明中请不要完全依赖它！

完备性提示

如果你认为程序是完备的，但 Idris 不认同，可以给检查器一些提示，帮助其更好地判断终止性。检查器的原理是确保所有递归调用链最终会导致某个参数趋向基例（base case），但有时这很难自动判断。例如，下面的定义无法被判定为 total，因为检查器无法确定 filter (< x) xs 总是比 (x :: xs) 更小：

qsort : Ord a => List a -> List a
qsort [] = []
qsort (x :: xs)
   = qsort (filter (< x) xs) ++
      (x :: qsort (filter (>= x) xs))

Prelude 中定义的 assert_smaller 函数就是为了解决这个问题：

assert_smaller : a -> a -> a
assert_smaller x y = y

它只是简单地返回第二个参数，但同时向完备性检查器断言 y 在结构上小于 x。如果检查器无法自动推断，可以用它来解释完备性的理由。上面的例子现在可以这样写：

total
qsort : Ord a => List a -> List a
qsort [] = []
qsort (x :: xs)
   = qsort (assert_smaller (x :: xs) (filter (< x) xs)) ++
      (x :: qsort (assert_smaller (x :: xs) (filter (>= x) xs)))

表达式 assert_smaller (x :: xs) (filter (<= x) xs) 断言 filter 的结果总是比模式 (x :: xs) 更小。

在更极端的情况下，assert_total 函数可以将某个子表达式标记为总是完备的：

assert_total : a -> a
assert_total x = x

一般来说应避免使用该函数，但在推理原语（primitive）或外部定义的函数（如 C 库中的函数）时，如果能用外部理由证明完备性，它会非常有用。