对列表做归纳

做完这一节，你会证明自己写的反转函数满足“反转两次等于没反转”。更要紧的是，你会经历一次证明卡住，并学会从卡住的地方看出缺什么。

学完你能做什么

• 对列表写出归纳证明：空列表，和“前面加一个元素”
• 从没证完的目标里读出需要的辅助引理
• 先证引理，再用它证完主定理

第 1 步：写一个反转函数

def rev : List α → List α
  | [] => []
  | x :: xs => rev xs ++ [x]

• [] 是空列表，反转还是空。
• x :: xs 是“第一个元素 x，后面是列表 xs”。反转它，就是先反转后面的，再把 x 接到最后。++ 是拼接两个列表。

试一下：

#eval rev [1, 2, 3]

[3, 2, 1]

• 我的 rev 能反转 [1, 2, 3]

第 2 步：直接证，然后卡住

要证的是：对任何列表，rev (rev xs) = xs。

列表的归纳和自然数一样是两个分支：nil 是空列表，cons x xs ih 是“x 后面跟着 xs”，ih 说命题对 xs 成立。照上一节的套路写：

theorem rev_rev_try (xs : List α) : rev (rev xs) = xs := by
  induction xs with
  | nil => rfl
  | cons x xs ih => simp [rev, ih]

你应该看到：Lean 说还有没证完的目标：

unsolved goals
case cons
α : Type u_1
x : α
xs : List α
ih : rev (rev xs) = xs
⊢ rev (rev xs ++ [x]) = x :: xs

别急着换策略，读一读这个目标。左边是 rev (rev xs ++ [x])，对一个“拼接起来的列表”做反转。ih 说的是 rev (rev xs)，中间多了一个 ++ [x]，所以用不上。

缺的是一条知识：反转一个拼接，结果是什么？

• 我看到了 unsolved goals，并且能指出目标和 ih 差在哪

第 3 步：先证一个帮手

想一个具体例子：把 [1, 2] 和 [3, 4] 拼起来再反转，得到 [4, 3, 2, 1]，也就是“后一半的反转”接上“前一半的反转”。把它写成定理，同样用归纳：

theorem rev_append (xs ys : List α) : rev (xs ++ ys) = rev ys ++ rev xs := by
  induction xs with
  | nil =>
    simp [rev]
  | cons x xs ih =>
    simp [rev, ih]

这种为了证主定理而先证的小定理，叫引理。

• rev_append 通过了

第 4 步：证完主定理

把引理交给 simp：

theorem rev_rev (xs : List α) : rev (rev xs) = xs := by
  induction xs with
  | nil =>
    rfl
  | cons x xs ih =>
    simp [rev, rev_append, ih]

你应该看到：没有报错。

有了 rev_append，卡住的 rev (rev xs ++ [x]) 被改写成 rev [x] ++ rev (rev xs)，这时 ih 能用了，剩下的 simp 自己算完。

• rev_rev 通过了

考考你证明卡住，Lean 显示 unsolved goals。下一步最该做什么？

检查点

• 我能写出列表归纳的两个分支：nil 和 cons x xs ih
• 我能解释为什么第一次尝试会卡住
• 我知道引理是什么，以及这一节的引理是怎么想出来的
• rev_append 和 rev_rev 都通过了

没成功？

rev_rev 报错说不认识 rev_append。 引理要写在用它的定理前面。Lean 从上往下读文件。

simp 之后还剩目标。 对照上面的代码，看方括号里是不是漏了 rev_append 或 ih。

下一节

你已经会验证一个函数了。最后一节用同样的三步，定义、卡住找引理、归纳，证明一个迷你编译器是对的。