运行示例：自然数加法（Addition of Natural Numbers）

在本教程中，我们将使用 Idris prelude（前置库）中定义的如下函数，该函数定义了自然数的加法：

plus : Nat -> Nat -> Nat
plus Z     m = m
plus (S k) m = S (plus k m)

它由上述等式定义，这意味着我们天然拥有如下性质：将 m 加到零上总是得到 m，而将 m 加到任意非零数 S k 上总是得到 S (plus k m)。我们可以在 Idris REPL（即命令行交互环境）中通过求值看到这一点：

Main> \m => plus Z m
\m => m

Idris> \k,m => plus (S k) m
\k => \m => S (plus k m)

注意，与许多其他语言的 REPL 不同，Idris REPL 可以对*开放*项进行归约，这意味着它可以化简出现在 lambda 绑定中的项，如上例所示。因此，我们可以将未知数 k 和 m 作为 lambda 绑定引入，并观察 plus 的归约过程。

plus 函数还有许多其他有用的性质，例如：

它是*交换的*，即对于所有 Nat 类型的输入 n 和 m，都有 plus n m = plus m n。
它是*结合的*，即对于所有 Nat 类型的输入 n、m 和 p，都有 plus n (plus m p) = plus (plus m n) p。

我们可以在 Idris 程序中使用这些性质，但为此我们必须*证明*它们。

等式证明（Equality Proofs）

Idris 定义了如下命题等式类型：

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

作为语法糖，Equal x y 可以写作 x = y。

这是一种*命题*等式，其类型声明任意两个不同类型 a 和 b 的值都可以被提议为相等。然而，只有一种方式可以*证明*等式，即自反性（Refl）。

这里我们有一个命题等式的*类型*，相应地，实例化该类型的*程序*可以视为对应命题的证明 [1]。因此，我们可以轻松证明 4 等于 4：

four_eq : 4 = 4
four_eq = Refl

然而，尝试证明 4 = 5 会失败：

four_eq_five : 4 = 5
four_eq_five = Refl

类型 4 = 5 是一个完全有效的类型，但它是不可实例化的，因此在类型检查该定义时，Idris 会报如下错误：

When unifying 4 = 4 and (fromInteger 4) = (fromInteger 5)
Mismatch between:
        4
and
        5

等式证明的类型检查（Type checking equality proofs）

在 Idris 程序的类型检查中，一个重要步骤是*统一（unification）*，它尝试解析隐式参数，比如 Refl 中的隐式参数 x。就我们对类型检查证明的理解而言，只需知道统一两个项的过程是将它们都归约为正常形（normal form），然后尝试为隐式参数赋值，使得这两个正常形相等。

在类型检查 Refl 时，Idris 要求类型必须是 x = x 的形式，这可以从 Refl 的类型看出。对于 four_eq_five，Idris 会尝试将期望类型 4 = 5 与 Refl 的类型 x = x 统一，注意到要有解就要求 x 同时为 4 和 5，因此会失败。

由于类型检查会归约到正常形，我们可以直接写出如下等式：

twoplustwo_eq_four : 2 + 2 = 4
twoplustwo_eq_four = Refl

plus_reduces_Z : (m : Nat) -> plus Z m = m
plus_reduces_Z m = Refl

plus_reduces_Sk : (k, m : Nat) -> plus (S k) m = S (plus k m)
plus_reduces_Sk k m = Refl

异类等式（Heterogeneous Equality）

Idris 中的等式是*异类*的，这意味着我们甚至可以提出不同类型值之间的等式：

idris_not_php : Z = "Z"

类型 Z = "Z" 是不可实例化的，有人可能会疑惑为什么要提出不同类型值之间的等式。然而，在依赖类型（dependent types）中，这类等式会自然出现。例如，如果两个向量相等，那么它们的长度也必须相等：

vect_eq_length : (xs : Vect n a) -> (ys : Vect m a) ->
                 (xs = ys) -> n = m

在上述声明中，xs 和 ys 因长度不同而类型不同，但如果它们相等，我们仍希望得出关于长度的结论。我们可以如下定义 vect_eq_length：

vect_eq_length xs xs Refl = Refl

通过对第三个参数使用 Refl 进行模式匹配，我们知道 ys 唯一有效的取值就是 xs，因为它们必须相等，因此类型也必须相等，所以长度也必须相等。

或者，我们可以将第二个 xs 用下划线代替，因为只有一个值能通过类型检查：

vect_eq_length xs _ Refl = Refl

`plus` 的性质（Properties of plus）

利用 (=) 类型，我们现在可以将上述 plus 的性质写成 Idris 类型声明：

plus_commutes : (n, m : Nat) -> plus n m = plus m n
plus_assoc : (n, m, p : Nat) -> plus n (plus m p) = plus (plus n m) p

这两个性质（以及许多其他性质）在 Idris 标准库中都已针对自然数加法被证明，使用的是 Num 接口中的 (+)，而不是直接用 plus。它们分别被命名为 plusCommutative 和 plusAssociative。

在本教程的后续部分，我们将探讨多种证明 plus_commutes 的方法（换句话说，也就是编写该函数）。我们还会讨论如何使用这些等式证明，并了解实际中何时需要它们。