一个关于证明与用户界面的说明🔗

本书展现了编写证明的过程，仿佛它们是一次就写就并交付给 Lean 运行似的，接着 Lean 会报错，描述剩余任务的错误信息。 实际上，与 Lean 互动的过程要愉快得多。Lean 在光标移动时提供有关证明的信息，并且有许多互动功能使证明更容易。 请查阅您的 Lean 开发环境的文档以获取更多信息。

本书中的方法侧重于逐步构建证明并显示产生的消息，这展示了 Lean 在编写证明时提供的各种互动反馈，尽管这比专家使用的过程慢得多。 同时，看到不完整的证明逐步趋向完整是一种对证明有益的视角。随着您编写证明技能的提高，Lean 的反馈将不再感觉像错误， 而更像是对您自己思维过程的支持。学习互动方法非常重要。

递归和归纳🔗

上一章中的函数 plusR_succ_left 和 plusR_zero_left 可以从两个角度看待。 从一方面看，它们是递归函数，构建了命题的证明，就像其他递归函数可能构建列表、字符串或任何其他数据结构一样。 从另一方面上看，它们也对应于 数学归纳法 (Mathematical Induction) 的证明。

数学归纳是一种证明技术，通过两个步骤证明一个命题对 所有 自然数成立：

1. 证明该命题对 0 成立。这称为 基本情况(Base Case)。

2. 在假设命题对某个任意选择的数 n 成立的前提下，证明它对 n + 1 成立。这称为 归纳步骤(Induction Step)。假设命题对 n 成立的假设称为 归纳假设(Induction Hypothesis)。

因为我们不可能对 每个 自然数进行检查，归纳提供了一种手段来编写原则上可以扩展到任何特定自然数的证明。 例如，如果需要对数字 3 进行具体证明，那么可以首先使用基本情况，然后归纳步骤三次，分别证明命题对 0、1、2，最后对 3 成立。 因此，它证明了该命题对所有自然数成立。

归纳策略🔗

通过递归函数编写归纳证明，使用诸如 congrArg 之类的辅助函数并不总是能很好地表达证明背后的意图。 虽然递归函数确实具有归纳的结构，但它们应该被视为一种证明的 编码。 此外，Lean 的策略系统提供了许多自动构建证明的机会，这是显式编写递归函数时无法实现的。 Lean 提供了一种归纳 策略，可以在单个策略块中完成整个归纳证明。 在幕后，Lean 构建了对应于归纳使用的递归函数。

要使用 induction 策略证明 plusR_zero_left，首先编写其签名（使用 theorem，因为这确实是一个证明）。 然后，使用 by induction k 作为定义的主体：

产生的消息表明有两个目标：

unsolved goals
zero⊢ 0 = Nat.plusR 0 0

succn✝:Nata✝:n✝ = Nat.plusR 0 n✝⊢ n✝ + 1 = Nat.plusR 0 (n✝ + 1)

策略块是在 Lean 类型检查器处理文件时运行的程序，有点像功能更强大的 C 预处理器宏。 策略生成实际的程序。

在策略语言中，可能有多个目标。每个目标由类型和一些假设组成。 这些类似于使用下划线作为占位符——目标中的类型表示要证明的内容，假设表示在作用域内且可以使用的内容。 在 case zero 的目标中，没有假设，类型是 Nat.zero = Nat.plusR 0 Nat.zero ——这是定理陈述，其中 0 代替 k。 在 case succ 的目标中，有两个假设，分别命名为 n✝ 和 n_ih✝。 在幕后，induction 策略创建了一个依赖模式匹配来优化整体类型，n✝ 表示模式中 Nat.succ 的参数。 假设 n_ih✝ 表示递归调用生成的函数在 n✝ 上的结果。 其类型是定理的整体类型，只是用 n✝ 代替 k。 case succ 目标的类型是定理陈述的整体，用 Nat.succ n✝ 代替 k。

使用 induction 策略得到的两个目标对应于数学归纳描述中的基本情况和归纳步骤。 基本情况是 case zero。 在 case succ 中，n_ih✝ 对应于归纳假设，而整个 case succ 是归纳步骤。

编写证明的下一步是依次关注两个目标中的每一个。 就像在 do 块中使用 pure () 来表示“什么也不做”一样，策略语言有一个语句 skip 也什么也不做。 当 Lean 的语法需要一个策略时，但尚不清楚应该使用哪个策略时，可以使用 skip。 将 with 添加到 induction 语句的末尾提供了一种类似于模式匹配的语法：

每个 skip 语句都有一个与之关联的消息。 第一个显示了基本情况：

unsolved goals
zero⊢ 0 = Nat.plusR 0 0

第二个显示了归纳步骤：

unsolved goals
succn:Natih:n = Nat.plusR 0 n⊢ n + 1 = Nat.plusR 0 (n + 1)

在归纳步骤中，不可访问的带匕首的名称已被提供的名称替换，分别为 succ 后的 n 和 ih。

induction ...with 后的 case 不是模式：它们由目标的名称和零个或多个名称组成。 名称用于在目标中引入的假设；如果提供的名称超过目标引入的名称数，则会出现错误：

Too many variable names provided at alternative 'succ': 5 provided, but 2 expected

关注基本情况，rfl 策略在 induction 策略中与在递归函数中一样有效：

在递归函数版本的证明中，类型注释使得预期类型更容易理解。 在策略语言中，有许多具体的方法可以转换目标，使其更容易解决。 unfold 策略用其定义替换定义的名称：

现在，目标中等式的右侧已变为 Nat.plusR 0 n + 1 而不是 Nat.plusR 0 (Nat.succ n)：

unsolved goals
succn:Natih:n = Nat.plusR 0 n⊢ n + 1 = Nat.plusR 0 n + 1

代替使用诸如 congrArg 之类的函数和运算符如 ▸，存在允许使用等式证明转换证明目标的策略。 最重要的策略之一是 rw，它接受等式证明列表，并在目标中用右侧替换左侧。 这几乎在 plusR_zero_left 中完成了正确的操作：

然而，重写的方向不正确。 将 n 替换为 Nat.plusR 0 n 使得目标更复杂而不是更简单：

unsolved goals
succn:Natih:n = Nat.plusR 0 n⊢ Nat.plusR 0 n + 1 = Nat.plusR 0 (Nat.plusR 0 n) + 1

通过在 rw 调用中的 ih 前加一个左箭头，可以解决这个问题，指示它用左侧替换等式的右侧：

这个重写使得等式的两边相同，Lean 会自己处理 rfl。 证毕。

策略高尔夫🔗

到目前为止，策略语言尚未显示出其真正的价值。 上面的证明并不比递归函数短，只是用特定领域的语言而不是完整的 Lean 语言编写。 但是，用策略编写的证明可以更短、更容易、更易维护。 就像高尔夫比赛中分数越低越好一样，策略高尔夫比赛中的证明越短越好。

plusR_zero_left 的归纳步骤可以使用简化策略 simp 证明。 单独使用 simp 并没有帮助：

`simp` made no progress

然而，simp 可以配置为使用一组定义。 就像 rw 一样，这些参数在列表中提供。 要求 simp 考虑 Nat.plusR 的定义导致一个更简单的目标：

unsolved goals
succn:Natih:n = Nat.plusR 0 n⊢ n = Nat.plusR 0 n

特别是，目标现在与归纳假设相同。 除了自动证明简单的等式外，简化器还会自动将目标如 Nat.succ A = Nat.succ B 替换为 A = B。 由于归纳假设 ih 具有完全正确的类型，exact 策略可以指示它应该被使用：

然而，使用 exact 有点脆弱。 重命名归纳假设（在“打高尔夫”证明时可能会发生）会导致此证明停止工作。 assumption 策略解决了当前目标，如果 任何 假设与之匹配：

这个证明并不比使用展开和显式重写的先前证明短。 然而，一系列变换可以使它更短，利用 simp 可以解决许多类型的目标这一事实。 第一步是去掉 induction 末尾的 with。 对于结构化、可读的证明，with 语法是方便的。 如果缺少任何情况，它会抱怨，并且它清楚地显示归纳的结构。 但是缩短证明通常需要更宽松的方法。

使用不带 with 的 induction 仅会产生两个目标。 case 策略可以像在 induction ...with 策略的分支中一样选择其中一个目标。 换句话说，以下证明等同于前一个证明：

在具有单个目标的上下文中（即 k = Nat.plusR 0 k），induction k 策略产生两个目标。 通常，策略要么失败并产生错误，要么接受一个目标并将其转换为零个或多个新目标。 每个新目标表示剩下要证明的内容。 如果结果是零个目标，则策略成功，该部分证明完成。

<;> 运算符接受两个策略作为参数，生成一个新策略。 T1 <;> T2 将 T1 应用于当前目标，然后在 T1 创建的所有目标中应用 T2。 换句话说，<;> 允许通用策略一次性用于多个新目标。 一个这样的通用策略是 simp。

Because simp can both complete the proof of the base case and make progress on the proof of the induction step, using it with induction and <;> shortens the proof:

因为 simp 既可以完成基本情况的证明，又可以在归纳步骤的证明中取得进展，所以使用它与 induction 和 <;> 缩短了证明：

这仅产生一个目标，即转换后的归纳步骤：

unsolved goals
succn✝:Nata✝:n✝ = Nat.plusR 0 n✝⊢ n✝ = Nat.plusR 0 n✝

在这个目标中运行 assumption 完成了证明：

在这里，exact 是不可能的，因为 ih 从未被显式命名。

对于初学者来说，这个证明并不容易阅读。 然而，专家用户的常见模式是使用像 simp 这样的强大策略处理一些简单情况，使他们可以将证明的文本集中在有趣的情况下。 此外，这些证明在面对函数和数据类型的小变化时往往更稳健。 策略高尔夫游戏是培养编写证明时的良好品味和风格的有用部分。

其他数据类型的归纳🔗

数学归纳通过为 Nat.zero 提供基本情况和为 Nat.succ 提供归纳步骤来证明自然数的命题。 归纳原则对于其他数据类型也是有效的。 没有递归参数的构造函数形成基本情况，而具有递归参数的构造函数形成归纳步骤。 进行归纳证明的能力是它们被称为 归纳 数据类型的原因。

这方面的一个例子是对二叉树的归纳。 对二叉树进行归纳是一种证明技术，通过两个步骤证明一个命题对 所有 二叉树成立：

1. 证明该命题对 BinTree.leaf 成立。这称为基本情况。

2. 在假设该命题对某些任意选择的树 l 和 r 成立的前提下，证明它对 BinTree.branch l x r 成立，其中 x 是任意选择的新数据点。这称为 归纳步骤。假设该命题对 l 和 r 成立的假设称为 归纳假设。

BinTree.count 计算树中分支的数量：

镜像树不会改变树中的分支数量。 可以通过对树进行归纳证明这一点。 第一步是声明定理并调用 induction：

基本情况表明，计算镜像叶子的数量与计算叶子相同：

unsolved goals
leafα:Type⊢ leaf.mirror.count = leaf.count

归纳步骤允许假设镜像左右子树不会影响其分支计数，并要求证明镜像具有这些子树的分支也保留整体分支计数：

unsolved goals
branchα:Typel:BinTree αx:αr:BinTree αihl:l.mirror.count = l.countihr:r.mirror.count = r.count⊢ (l.branch x r).mirror.count = (l.branch x r).count

基本情况成立，因为镜像 leaf 结果为 leaf，因此左右两边定义上相等。 这可以通过使用带有展开 BinTree.mirror 指令的 simp 表达：

在归纳步骤中，目标中没有任何东西与归纳假设立即匹配。 使用 BinTree.count 和 BinTree.mirror 的定义简化显示了关系：

unsolved goals
branchα:Typel:BinTree αx:αr:BinTree αihl:l.mirror.count = l.countihr:r.mirror.count = r.count⊢ 1 + r.mirror.count + l.mirror.count = 1 + l.count + r.count

可以使用两个归纳假设重写目标的左侧，使其与右侧几乎相同：

unsolved goals
branchα:Typel:BinTree αx:αr:BinTree αihl:l.mirror.count = l.countihr:r.mirror.count = r.count⊢ 1 + r.count + l.count = 1 + l.count + r.count

simp 策略在传递 +arith 选项时可以使用额外的算术等式。 这足以证明此目标，从而得到：

除了要展开的定义外，简化器还可以传递等式证明的名称以在简化证明目标时用作重写。 BinTree.mirror_count 还可以这样写：