module plfa.part1.Induction where

归纳会让你对无中生有感到内疚 ……但它却是文明中最伟大的思想之一。 —— Herbert Wilf

现在我们定义了自然数及其运算，下一步是学习如何证明它们满足的性质。 顾名思义，归纳数据类型（Inductive Datatype）是通过归纳（Induction） 来证明的。

导入

我们需要上一章中的相等性，加上自然数及其运算。我们还导入了一些新的运算： cong、sym 和 _≡⟨_⟩_，之后会解释它们：

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong; sym)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; step-≡; _∎)
open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_;_^_)

(Importing step-≡ defines _≡⟨_⟩_.)

运算符的性质

运算符随处可见，而数学家们统一了一些最常见的性质的名称。

  • 幺元（Identity）：对于所有的 n，若 0 + n ≡ n，则 + 有左幺元 0； 若 n + 0 ≡ n，则 + 有右幺元 0。同时为左幺元和右幺元的值称简称幺元。 幺元有时也称作单位元（Unit）。

  • 结合律（Associativity）：若括号的位置无关紧要，则称运算符 + 满足结合律， 即对于所有的 m、n 和 p，有 (m + n) + p ≡ m + (n + p)。

  • 交换律（Commutativity）：若参数的顺序无关紧要，则称运算符 + 满足交换律， 即对于所有的 m 和 n，有 m + n ≡ n + m。

  • 分配律（Distributivity）：对于所有的 m、n 和 p，若 m * (p + q) ≡ (m * p) + (m * q)，则运算符 * 对运算符 + 满足左分配律； 对于所有的 m、n 和 p，若 (m + n) * p ≡ (m * p) + (n * p)，则满足右分配律。

加法的幺元为 0，乘法的幺元为 1。加法和乘法都满足结合律和交换律， 乘法对加法满足分配律。

如果你在一个舞会上碰见了一位操作员，那么你可以跟他闲聊，问问他是否有单位元， 能不能结合或者交换。如果你碰见了两位操作员，那么可以问他们某一位是否在另一位上面分布。

【译注：作者的双关冷笑话，运算符（Operator）也有操作员的意思。】

正经来说，如果你在阅读技术论文时遇到了一个运算符，那么你可以考察它是否拥有幺元， 是否满足结合律或分配律，或者是否对另一个运算符满足分配律，这能为你提供一种视角。 细心的作者通常会指出它们是否满足这些性质，比如说指明一个新引入的运算符满足结合律 但不满足交换律。

练习 operators（实践）

请给出另一对运算符，它们拥有一个幺元，满足结合律、交换律，且其中一个对另一个满足分配律。 （你不必证明这些性质）

-- 请将代码写在此处。

请给出一个运算符的例子，它拥有幺元、满足结合律但不满足交换律。 （你不必证明这些性质）

-- 请将代码写在此处。

结合律

加法的一个性质是满足结合律，即括号的位置无关紧要：

(m + n) + p ≡ m + (n + p)

这里的变量 m、n 和 p 的取值范围都是全体自然数。

我们可以为这三个变量选取特定的数值来验证此命题：

_ : (3 + 4) + 5 ≡ 3 + (4 + 5)
_ =
  begin
    (3 + 4) + 5
  ≡⟨⟩
    7 + 5
  ≡⟨⟩
    12
  ≡⟨⟩
    3 + 9
  ≡⟨⟩
    3 + (4 + 5)
  ∎

在这里，我们将计算过程写成了等式链，每行一个式子。这样的等式链通常非常易读， 你可以从上到下，直到遇到最简形式（本例中为 12），也可以从下到上，直到回到同样的式子。

该测试揭示了结合律可能没有它初看起来那么显然。为什么 7 + 5 与 3 + 9 相同？ 我们可能需要收集更多证据，选择其它的数值来验证此命题。但由于自然数是无限的， 因此测试永远无法完成。那么我们还有其它可以确保结合律对于所有自然数都成立的方法吗？

当然有！我们可以用归纳证明（Proof by Induction） 来确保某个性质对于所有的自然数都成立。

归纳证明

回想自然数的定义，它由一个起始步骤「zero 是一个自然数」 和一个归纳步骤「若 m 是一个自然数，则 suc m 也是一个自然数」构成。

归纳证明遵循此定义的结构。要通过归纳证明自然数的某个性质，我们需要两个步骤。 其一是起始步骤，即需要证明此性质对 zero 成立。其二是归纳步骤， 即假设此性质对一个任意自然数 m 成立（我们称之为归纳假设（Induction Hypothesis）），然后证明该性质对 suc m 必定成立。

若将 m 的某种性质（Property）写作 P m，那么我们需要证明的就是以下两个推导规则：

------
P zero

P m
---------
P (suc m)

先来分析一下这些规则。第一条规则是起始步骤，它需要我们证明性质 P 对 zero 成立。第二条规则是归纳步骤，它需要我们证明若归纳假设「P 对 m 成立」， 那么 P 也对 suc m 成立。

为什么可以这样做呢？它也可以用创世故事来讲解。起初，我们对性质一无所知：

-- 起初，世上没有已知的性质。

现在我们对所有已知的性质应用上述两条规则。起始步骤告诉我们 P zero 成立， 所以我们将它加入已知的性质集合中。归纳步骤告诉我们若「昨天的」P m 成立， 那么「今天的」P (suc m) 也成立。我们在今天之前并不知道任何性质， 因此归纳步骤在这里不适用：

-- 第一天，我们知道了一个性质。
P zero

然后我们重复此过程。在接下来的一天我们知道今天之前的所有性质， 以及任何通过此规则添加的性质。起始步骤告诉我们 P zero 成立，我们已经知道这件事了。而如今归纳步骤告诉我们，由于 P zero 在昨天成立，那么 P (suc zero) 今天也成立。

-- 第二天，我们知道了两个性质。
P zero
P (suc zero)

我们再重复此过程。现在归纳步骤告诉我们由于 P zero 和 P (suc zero) 都成立， 因此 P (suc zero) 和 P (suc (suc zero)) 也成立。我们已经知道第一个成立了， 但第二个是新引入的：

-- 第三天，我们知道了三个性质。
P zero
P (suc zero)
P (suc (suc zero))

此时规律已经很明显了：

-- 第四天，我们知道了四个性质。
P zero
P (suc zero)
P (suc (suc zero))
P (suc (suc (suc zero)))

此过程可以继续下去。在第 n 天会有 n 个不同的性质成立。 每个自然数的性质都会在某一天出现。具体来说，性质 P n 会在第 n+1 天 首次出现。

第一个证明：结合律

要证明结合律，我们需要将 P m 看做以下性质：

(m + n) + p ≡ m + (n + p)

这里的 n 和 p 是任意自然数，因此若我们可以证明该等式对所有的 m 都成立，那么它也会对所有的 n 和 p 成立。其推理规则的对应实例如下：

-------------------------------
(zero + n) + p ≡ zero + (n + p)

(m + n) + p ≡ m + (n + p)
---------------------------------
(suc m + n) + p ≡ suc m + (n + p)

如果我们可以证明这两条规则，那么加法结合律就可以用归纳法来证明。

以下为此性质的陈述和证明：

+-assoc : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
+-assoc zero n p =
  begin
    (zero + n) + p
  ≡⟨⟩
    n + p
  ≡⟨⟩
    zero + (n + p)
  ∎
+-assoc (suc m) n p =
  begin
    (suc m + n) + p
  ≡⟨⟩
    suc (m + n) + p
  ≡⟨⟩
    suc ((m + n) + p)
  ≡⟨ cong suc (+-assoc m n p) ⟩
    suc (m + (n + p))
  ≡⟨⟩
    suc m + (n + p)
  ∎

我们将此证明命名为 +-assoc。在 Agda 中，标识符可以由除空格和 @.(){};_ 之外的任何字符序列构成。

我们来分析一下这段代码。其签名（Signature）描述了我们定义的标识符 +-assoc 为以下命题提供了证据（Evidence）：

∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)

倒 A 符号读作「对于所有（for all）」，而该命题断言对于所有的自然数 m、n 和 p，等式 (m + n) + p ≡ m + (n + p) 成立。该命题的证据是一个接受三个自然数的函数， 将它们绑定到 m、n 和 p，并返回该等式对应实例的证据。

对于起始步骤，我们必须证明：

(zero + n) + p ≡ zero + (n + p)

用加法的起始步骤化简等式两边会得到：

n + p ≡ n + p

此式平凡成立。阅读此证明中起始步骤中的等式链，其最初和最末的式子分别匹配待证等式的两边， 从上到下或从下到上读都会让我们在中间遇到 n + p 。此步骤无需多言，化简即可。

对于归纳步骤，我们必须证明：

(suc m + n) + p ≡ suc m + (n + p)

用加法的归纳步骤化简等式两边会得到：

suc ((m + n) + p) ≡ suc (m + (n + p))

反之，它也可以通过在归纳假设

(m + n) + p ≡ m + (n + p)

两边之前加上 suc 得到。

阅读此证明中归纳步骤的等式链，其最初和最末的式子分别匹配待证等式的两边， 从上到下或从下到上读都会让我们到达上面化简等式的地方。剩下的等式单化简还不行， 我们还需要为推理链使用一个附加的运算符 _≡⟨_⟩_， 并将等式的依据放在尖括号中。这里给出的依据是：

⟨ cong suc (+-assoc m n p) ⟩

在这里，递归调用的 +-assoc m n p 拥有归纳假设的类型，而 cong suc 会在等式两边的前面加上 suc 以得到需要的等式。

若某个关系在应用了给定的函数后仍然保持不变，则称该关系满足合同性（Congruence）。 若 e 是 x ≡ y 的证据，那么对于任意函数 f，cong f e 就是 f x ≡ f y 的证据。

在这里并未假定归纳假设，而是通过递归调用我们定义的函数 +-assoc m n p 来证明。 对于加法，这是良基的（well-founded），因为更大数值的结合律可基于更小数值的结合律 来证明。在此步骤中，assoc (suc m) n p 是用 assoc m n p 证明的。 归纳证明和递归定义之间的这种对应是 Agda 中最吸引人的方面之一。

归纳即递归

下面是归纳如何对应于递归的具体例子，它是在结合律的证明中，将 m 实例化为 2 时的计算过程。

+-assoc-0 : ∀ (n p : ℕ) → (0 + n) + p ≡ 0 + (n + p)
+-assoc-0 n p =
  begin
    (0 + n) + p
  ≡⟨⟩
    n + p
  ≡⟨⟩
    0 + (n + p)
  ∎

+-assoc-1 : ∀ (n p : ℕ) → (1 + n) + p ≡ 1 + (n + p)
+-assoc-1 n p =
  begin
    (1 + n) + p
  ≡⟨⟩
    suc (0 + n) + p
  ≡⟨⟩
    suc ((0 + n) + p)
  ≡⟨ cong suc (+-assoc-0 n p) ⟩
    suc (0 + (n + p))
  ≡⟨⟩
    1 + (n + p)
  ∎

+-assoc-2 : ∀ (n p : ℕ) → (2 + n) + p ≡ 2 + (n + p)
+-assoc-2 n p =
  begin
    (2 + n) + p
  ≡⟨⟩
    suc (1 + n) + p
  ≡⟨⟩
    suc ((1 + n) + p)
  ≡⟨ cong suc (+-assoc-1 n p) ⟩
    suc (1 + (n + p))
  ≡⟨⟩
    2 + (n + p)
  ∎

术语与记法

在结合律的陈述中出现的符号 ∀ 表示它对于所有的 m、n 和 p 都成立。 我们将 ∀ 称为全称量词（Universal Quantifier），我们会在 Quantifiers 章节中进一步讨论。

全称量词的证据是一个函数。函数签名

+-assoc : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)

和

+-assoc : ∀ (m : ℕ) → ∀ (n : ℕ) → ∀ (p : ℕ) → (m + n) + p ≡ m + (n + p)

是等价的。和 ℕ → ℕ → ℕ 这样的函数类型不同，上述函数中的变量 与每一个实参类型相关联，且其结果类型可能会涉及（或依赖于）这些变量， 因此它们叫做依赖函数（Dependent Function）。

Ordinary functions are a special case of dependent functions. For instance, the signatures

_+_ : ℕ → ℕ → ℕ

and

_+_ : ∀ (m n : ℕ) → ℕ

and

_+_ : ∀ (m : ℕ) → ∀ (n : ℕ) → ℕ

are all equivalent.

第二个证明：交换律

加法的另一个重要性质是满足交换律（Commutativity），即运算数的顺序无关紧要：

m + n ≡ n + m

要证明它，我们需要先证明两条引理（Lemma）。

第一条引理

加法定义的起始步骤说明零是一个左幺元：

zero + n ≡ n

我们的第一条引理则说明零也是一个右幺元：

m + zero ≡ m

下面是该引理的陈述和证明：

+-identityʳ : ∀ (m : ℕ) → m + zero ≡ m
+-identityʳ zero =
  begin
    zero + zero
  ≡⟨⟩
    zero
  ∎
+-identityʳ (suc m) =
  begin
    suc m + zero
  ≡⟨⟩
    suc (m + zero)
  ≡⟨ cong suc (+-identityʳ m) ⟩
    suc m
  ∎

其签名说明我们定义的标识符 +-identityʳ 提供了以下命题的证据：

∀ (m : ℕ) → m + zero ≡ m

该命题的证据是一个函数，它接受一个自然数，将其绑定到 m，然后返回 该等式对应实例的证据。它通过对 m 进行归纳来证明。

对于起始步骤，我们必须证明：

zero + zero ≡ zero

根据加法的起始步骤化简，这很显然。

对于归纳步骤，我们必须证明：

(suc m) + zero = suc m

根据加法的归纳步骤化简等式两边可得：

suc (m + zero) = suc m

反之，它也可以通过在归纳假设

m + zero ≡ m

两边之前加上 suc 得到。

阅读此等式链，从上到下和从下到上读都会让我们到达上面化简等式的地方。 剩下的等式可由以下依据得出：

⟨ cong suc (+-identityʳ m) ⟩

在这里，递归调用的 +-identityʳ m 拥有归纳假设的类型，而 cong suc 会在等式两边的前面加上 suc 以得到需要的等式。第一条引理证毕。

第二条引理

加法定义的归纳步骤将第一个参数的 suc 推到了外面：

suc m + n ≡ suc (m + n)

我们的第二条引理则对第二个参数的 suc 做同样的事情：

m + suc n ≡ suc (m + n)

下面是该引理的陈述和证明：

+-suc : ∀ (m n : ℕ) → m + suc n ≡ suc (m + n)
+-suc zero n =
  begin
    zero + suc n
  ≡⟨⟩
    suc n
  ≡⟨⟩
    suc (zero + n)
  ∎
+-suc (suc m) n =
  begin
    suc m + suc n
  ≡⟨⟩
    suc (m + suc n)
  ≡⟨ cong suc (+-suc m n) ⟩
    suc (suc (m + n))
  ≡⟨⟩
    suc (suc m + n)
  ∎

其签名说明我们定义的标识符 +-suc 提供了以下命题的证据：

∀ (m n : ℕ) → m + suc n ≡ suc (m + n)

该命题的证据是一个函数，它接受两个自然数，将二者分别绑定到 m 和 n， 并返回该等式对应实例的证据。它通过对 m 进行归纳来证明。

对于起始步骤，我们必须证明：

zero + suc n ≡ suc (zero + n)

根据加法的起始步骤化简，这很显然。

对于归纳步骤，我们必须证明：

suc m + suc n ≡ suc (suc m + n)

根据加法的归纳步骤化简等式两边可得：

suc (m + suc n) ≡ suc (suc (m + n))

反之，它也可以通过在归纳假设

m + suc n ≡ suc (m + n)

两边之前加上 suc 得到。

从上到下或从下到上阅读等式链都会让我们在中间遇到化简后的等式。剩下的等式 可由以下依据得出：

⟨ cong suc (+-suc m n) ⟩

在这里，递归调用的 +-suc m n 拥有归纳假设的类型，而 cong suc 会在等式两边的前面加上 suc 以得到需要的等式。第二条引理证毕。

命题

最后，以下是我们的命题的陈述和证明：

+-comm : ∀ (m n : ℕ) → m + n ≡ n + m
+-comm m zero =
  begin
    m + zero
  ≡⟨ +-identityʳ m ⟩
    m
  ≡⟨⟩
    zero + m
  ∎
+-comm m (suc n) =
  begin
    m + suc n
  ≡⟨ +-suc m n ⟩
    suc (m + n)
  ≡⟨ cong suc (+-comm m n) ⟩
    suc (n + m)
  ≡⟨⟩
    suc n + m
  ∎

第一行说明我们定义的标识符 +-comm 提供了以下命题的证据：

∀ (m n : ℕ) → m + n ≡ n + m

该命题的证据是一个函数，它接受两个自然数，将二者分别绑定到 m 和 n， 并返回该等式对应实例的证据。它通过对 n 进行归纳来证明。（这次不是 m！）

对于起始步骤，我们必须证明：

m + zero ≡ zero + m

根据加法的起始步骤化简等式两边可得：

m + zero ≡ m

剩下的等式可由依据 ⟨ +-identityʳ m ⟩ 得出，它调用第一条引理。

对于归纳步骤，我们必须证明：

m + suc n ≡ suc n + m

根据加法的归纳步骤化简等式两边可得：

m + suc n ≡ suc (n + m)

我们分两步来证明它。首先，我们有：

m + suc n ≡ suc (m + n)

它依据第二条引理 ⟨ +-suc m n ⟩ 得出。之后我们有：

suc (m + n) ≡ suc (n + m)

它依据合同性和归纳假设 ⟨ cong suc (+-comm m n) ⟩ 得出。证毕。

Agda 要求标识符必须在使用前定义，因此我们必须在主命题之前列出引理， 如前例所示。在实践中，我们通常会先试着证明主命题，之后所需的等式会说明 需要证明哪些引理。

第一个推论：重排定理

我们可以随意应用结合律来重排括号。例如：

+-rearrange : ∀ (m n p q : ℕ) → (m + n) + (p + q) ≡ m + (n + p) + q
+-rearrange m n p q =
  begin
    (m + n) + (p + q)
  ≡⟨ sym (+-assoc (m + n) p q) ⟩
    ((m + n) + p) + q
  ≡⟨ cong (_+ q) (+-assoc m n p) ⟩
    (m + (n + p)) + q
  ∎

无需归纳法，我们只不过应用了两次结合律就完成了证明。其中有几点需要注意的地方。

第一，加法是左结合的，因此 m + (n + p) + q 表示 (m + (n + p)) + q。

第二，我们用 sym 来交换等式的两边。命题 +-assoc (m + n) p q 会将括号从左边移到右边：

((m + n) + p) + q ≡ (m + n) + (p + q)

要往另一个方向移动括号，我们要用 sym (+-assoc (m + n) p q)：

(m + n) + (p + q) ≡ ((m + n) + p) + q

一般来说，若 e 提供了 x ≡ y 的证据，那么 sym e 就提供了 y ≡ x 的证据。

第三，Agda 支持 Richard Bird 引入的片段（Section）记法。我们将应用到 x 并返回 x + y 的函数写作 (_+ y)。因此，对于 assoc m n p 应用合同性 cong (_+ q) 会将等式：

(m + n) + p  ≡  m + (n + p)

转换成:

((m + n) + p) + q  ≡  (m + (n + p)) + q

类似地，我们将应用到 x 并返回 x + y 的函数写作 (x +_ )。 这同样适用于任何中缀运算符。

创世，最后一次

我们回到结合律的证明上来，把归纳证明（或等价的递归定义）看做一个创世故事会有助于理解。 这次我们专注于判断结合律的断言：

 -- 起初，我们对结合律一无所知。

现在，我们将规则应用到所有已知的判断上来。起始步骤告诉我们对于所有的自然数 n 和 p 来说，(zero + n) + p ≡ zero + (n + p)。归纳步骤告我我们若 (m + n) + p ≡ m + (n + p)（在昨天）成立，那么 (suc m + n) + p ≡ suc m + (n + p) （在今天）也成立。我们在今天之前并不知道任何关于结合律的判断， 因此此规则并未给出任何新的判断：

-- 第一天，我们知道了关于 0 的结合律。
(0 + 0) + 0 ≡ 0 + (0 + 0)   ...   (0 + 4) + 5 ≡ 0 + (4 + 5)   ...

之后我们重复此过程，因此接下来一天我们知道今天以前的所有判断， 以及任何通过此规则添加的判断。起始步骤并未告诉我们新的东西， 而如今归归纳步骤添加了更多的判断：

-- 第二天，我们知道了关于 0 和 1 的结合律。
(0 + 0) + 0 ≡ 0 + (0 + 0)   ...   (0 + 4) + 5 ≡ 0 + (4 + 5)   ...
(1 + 0) + 0 ≡ 1 + (0 + 0)   ...   (1 + 4) + 5 ≡ 1 + (4 + 5)   ...

我们再次重复此过程：

-- 第三天，我们知道了关于 0、1 和 2 的结合律。
(0 + 0) + 0 ≡ 0 + (0 + 0)   ...   (0 + 4) + 5 ≡ 0 + (4 + 5)   ...
(1 + 0) + 0 ≡ 1 + (0 + 0)   ...   (1 + 4) + 5 ≡ 1 + (4 + 5)   ...
(2 + 0) + 0 ≡ 2 + (0 + 0)   ...   (2 + 4) + 5 ≡ 2 + (4 + 5)   ...

此时规律已经很明显了：

-- 第四天，我们知道了关于 0、1、2 和 3 的结合律。
(0 + 0) + 0 ≡ 0 + (0 + 0)   ...   (0 + 4) + 5 ≡ 0 + (4 + 5)   ...
(1 + 0) + 0 ≡ 1 + (0 + 0)   ...   (1 + 4) + 5 ≡ 1 + (4 + 5)   ...
(2 + 0) + 0 ≡ 2 + (0 + 0)   ...   (2 + 4) + 5 ≡ 2 + (4 + 5)   ...
(3 + 0) + 0 ≡ 3 + (0 + 0)   ...   (3 + 4) + 5 ≡ 3 + (4 + 5)   ...

此过程可以继续下去。在第 m 天我们会知道所有第一个数小于 m 的判断。

还有一种完全有限的方法来生成同样的等式，它的证明留作读者的练习。

练习 finite-+-assoc（延伸）

请参考前文写出前四天已知的加法结合律的创世故事。

-- 请将代码写在此处。

用改写来证明结合律

证明可不止一种方法。下面是第二种在 Agda 中证明加法结合律的方法，使用 rewrite（改写） 而非等式链：

+-assoc′ : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
+-assoc′ zero    n p                          =  refl
+-assoc′ (suc m) n p  rewrite +-assoc′ m n p  =  refl

对于起始步骤，我们必须证明：

(zero + n) + p ≡ zero + (n + p)

根据加法的起始步骤化简等式两边可得：

n + p ≡ n + p

此式平凡成立。一个项等于其自身的证明写作 refl（自反性）。

对于归纳步骤，我们必须证明：

(suc m + n) + p ≡ suc m + (n + p)

根据加法的归纳步骤化简等式两边可得：

suc ((m + n) + p) ≡ suc (m + (n + p))

This is our goal to be proved. Rewriting by a given equation is indicated by the keyword rewrite followed by a proof of that equation. Rewriting replaces each occurrence of the left-hand side of the equation in the goal by the right-hand side. In this case, after rewriting by the inductive hypothesis our goal becomes

suc (m + (n + p)) ≡ suc (m + (n + p))

其证明同样由 refl 给出。改写不仅可以省去等式链还可以避免调用 cong.

使用改写证明交换律

下面是加法交换律的第二个证明，使用 rewrite 而非等式链：

+-identity′ : ∀ (n : ℕ) → n + zero ≡ n
+-identity′ zero = refl
+-identity′ (suc n) rewrite +-identity′ n = refl

+-suc′ : ∀ (m n : ℕ) → m + suc n ≡ suc (m + n)
+-suc′ zero n = refl
+-suc′ (suc m) n rewrite +-suc′ m n = refl

+-comm′ : ∀ (m n : ℕ) → m + n ≡ n + m
+-comm′ m zero rewrite +-identity′ m = refl
+-comm′ m (suc n) rewrite +-suc′ m n | +-comm′ m n = refl

在最后一行中，用两个等式进行改写被表示为用一条竖线分隔两个相关等式的证明。 左边的改写会在右边之前被执行。

交互式构造证明

看看如何在 Emacs 中用 Agda 的交互式特性来构造另一种结合律的证明会很有启发性。 我们从输入以下内容开始：

+-assoc′ : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
+-assoc′ m n p = ?

其中的问号表示你想要 Agda 帮你填充的代码。如果你按下 C-c C-l （先按 Ctrl-c 再按 Ctrl-l），那么问号会被替换为：

+-assoc′ : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
+-assoc′ m n p = { }0

空的大括号叫做洞（Hole），0 是用来指代此洞的编号。洞可能会以绿色高亮显示。 Emacs 还会在屏幕下方创建一个新的窗口并显示文本：

?0 : ((m + n) + p) ≡ (m + (n + p))

这表示 0 号洞需要以所提示的判断的证明来填充。

我们希望对 m 进行归纳来证明此命题。将光标移动到洞中并按下 C-c C-c。它会给出提示：

pattern variables to case (empty for split on result):

按下 m 会拆分该变量，并更新此代码：

+-assoc′ : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
+-assoc′ zero n p = { }0
+-assoc′ (suc m) n p = { }1

现在有两个洞了，下方的窗口会告诉你每个洞中需要证明的内容：

?0 : ((zero + n) + p) ≡ (zero + (n + p))
?1 : ((suc m + n) + p) ≡ (suc m + (n + p))

进入 0 号洞并按下 C-c C-, 会显示以下文本：

Goal: (n + p) ≡ (n + p)
————————————————————————————————————————————————————————————
p : ℕ
n : ℕ

它表示在化简之后，0 号洞的目标如上所示，所示类型的变量 p 和 n 可在证明中使用。 给定目标的证明很平凡，只需进入该目标并按下 C-c C-r 即可填充。按下 C-c C-l 会将剩下的洞重新编号为 0：

+-assoc′ : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
+-assoc′ zero n p = refl
+-assoc′ (suc m) n p = { }0

进入新的 0 号洞并按下 C-c C-, 会显示以下文本：

Goal: suc ((m + n) + p) ≡ suc (m + (n + p))
————————————————————————————————————————————————————————————
p : ℕ
n : ℕ
m : ℕ

同样，它会给出化简后的目标和可用的变量。在此步骤中，我们需要根据归纳假设进行改写， 于是我们来编辑这些文本：

+-assoc′ : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
+-assoc′ zero n p = refl
+-assoc′ (suc m) n p rewrite +-assoc′ m n p = { }0

进入剩下的洞中并按下 C-c C-, 会显示以下文本：

Goal: suc (m + (n + p)) ≡ suc (m + (n + p))
————————————————————————————————————————————————————————————
p : ℕ
n : ℕ
m : ℕ

给定目标的证明很平凡，只需进入该目标并按下 C-c C-r 即可填充并完成证明：

+-assoc′ : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
+-assoc′ zero n p = refl
+-assoc′ (suc m) n p rewrite +-assoc′ m n p = refl

练习：+-swap（推荐）

请证明对于所有的自然数 m、n 和 p，

m + (n + p) ≡ n + (m + p)

成立。无需归纳证明，只需应用前面满足结合律和交换律的结果即可。

-- 请将代码写在此处。

练习 *-distrib-+（推荐）

请证明乘法对加法满足分配律，即对于所有的自然数 m、n 和 p，

(m + n) * p ≡ m * p + n * p

成立。

-- 请将代码写在此处。

练习 *-assoc（推荐）

请证明乘法满足结合律，即对于所有的自然数 m、n 和 p，

(m * n) * p ≡ m * (n * p)

成立。

-- 请将代码写在此处。

练习 *-comm（实践）

请证明乘法满足交换律，即对于所有的自然数 m 和 n，

m * n ≡ n * m

成立。和加法交换律一样，你需要陈述并证明配套的引理。

-- 请将代码写在此处。

练习 0∸n≡0（实践）

请证明对于所有的自然数 n，

zero ∸ n ≡ zero

成立。你的证明需要归纳法吗？

-- 请将代码写在此处。

练习 ∸-+-assoc（实践）

请证明饱和减法与加法满足结合律，即对于所有的自然数 m、n 和 p，

m ∸ n ∸ p ≡ m ∸ (n + p)

成立。

-- 请将代码写在此处。

练习 +*^ （延伸）

证明下列三条定律

 m ^ (n + p) ≡ (m ^ n) * (m ^ p)  (^-distribˡ-+-*)
 (m * n) ^ p ≡ (m ^ p) * (n ^ p)  (^-distribʳ-*)
 (m ^ n) ^ p ≡ m ^ (n * p)        (^-*-assoc)

对于所有 m、n 和 p 成立。

-- 请将代码写在此处。

练习 Bin-laws（延伸）

回想练习 Bin 中定义的一种表示自然数的比特串数据类型 Bin 以及要求你定义的函数：

inc   : Bin → Bin
to    : ℕ → Bin
from  : Bin → ℕ

考虑以下定律，其中 n 表示自然数，b 表示比特串：

from (inc b) ≡ suc (from b)
to (from b) ≡ b
from (to n) ≡ n

对于每一条定律：若它成立，请证明；若不成立，请给出一个反例。

-- 请将代码写在此处。

标准库

本章中类似的定义可在标准库中找到：

import Data.Nat.Properties using (+-assoc; +-identityʳ; +-suc; +-comm)

Unicode

本章中使用了以下 Unicode：

∀  U+2200  对于所有 (\forall, \all)
ʳ  U+02B3  修饰符小写字母 r (\^r)
′  U+2032  撇号 (\')
″  U+2033  双撇号 (\')
‴  U+2034  三撇号 (\')
⁗  U+2057  四撇号 (\')

与 \r 类似，命令 \^r 列出了多种上标右箭头的变体，以及上标的字母 r。 命令 \' 列出了一些撇号（′ ″ ‴ ⁗）。