让 Lean 替你算

做完这一节，你会用四个省力的策略，并且知道该先试哪个。

策略	它做什么	什么时候想到它
rw [h]	用等式 h 把目标里的左边换成右边	手里有一个等式，目标里正好有它的左边
simp	用一批已知的化简规则反复改写	目标看起来“显然”，只是写法啰嗦
omega	证明自然数、整数的加减和比较	目标是带 +、<、≤ 的算术
decide	把具体的命题直接算出真假	目标里全是具体的数，没有变量

学完你能做什么

• 用 rw 做一次等式替换
• 用 #check 查一条现成定理说的是什么
• 判断一个目标该交给 simp、omega 还是 decide

第 1 步：rw，用等式改写

手里有 h : a = b，目标里出现了 a。rw [h] 把目标里的 a 全换成 b：

example (a b : Nat) (h : a = b) : a + 1 = b + 1 := by
  rw [h]

改写之后目标变成 b + 1 = b + 1，两边一样，rw 顺手就把它证完了。

rw 也能用现成的定理。Lean 自带很多，先用 #check 看它说的是什么：

#check Nat.add_comm

你应该看到：

Nat.add_comm (n m : Nat) : n + m = m + n

加法可以交换。拿它来改写：

example (a b : Nat) : a + b = b + a := by
  rw [Nat.add_comm]

• 我知道 rw [h] 是把 h 的左边换成右边

第 2 步：simp，自动化简

很多事实已经被标记成化简规则，比如“一个列表后面接上空列表，还是它自己”。simp 会自己找来用：

example (xs : List Nat) : (xs ++ []).length = xs.length := by
  simp

想让它多用几条规则或定义，写在方括号里：simp [某个定义, 某条定理]。后面几节会一直这样用。

• 我知道目标“显然但啰嗦”时先试 simp

第 3 步：omega，线性算术

带变量的加减和大小比较，交给 omega：

example (a b : Nat) (h : a < b) : a + 1 ≤ b := by
  omega

它会用上手里的假设 h。但它只懂加减和比较，两个变量相乘就不归它管了。

• 我知道 omega 管的是自然数和整数的加、减、比较

第 4 步：decide，直接算

命题里只有具体的数时，让 Lean 算出真假：

example : 17 * 3 = 51 := by
  decide

有变量就不行了，Lean 没法把“所有的 n”一个个算完。那正是下一章归纳法要解决的事。

• 我知道 decide 只适合不含变量的具体命题

考考你目标是 x + 2 > x，其中 x 是任意自然数。先试哪个策略？

检查点

• 我能说出四个策略各自擅长什么
• 我会用 #check 查一条定理的内容
• 我知道 rw [h] 的方向是从左到右
• 我知道 decide 和 omega 的分工：没有变量，有变量

没成功？

rw 报找不到要改写的东西。 目标里没有出现等式的左边。看清楚等式的方向；要反过来用，写成 rw [← h]，箭头用 \l 输入。

simp 没有证完。 它只是化简，剩下的目标会留给你。看一眼还剩什么，再决定下一步。

下一节

这些策略都只能处理“一眼看得完”的情况。要证明一件事对所有自然数成立，需要归纳法。