simp：让机器帮你化简

Introduction

回到自然数。还记得第 5 课我们做了 `n + 0 = n` 的归纳证明吗？那次是左边的 +0 情况——这次我们来证右边：`0 + n = n`。看起来一样？其实不一样！加法的定义是递归在**第二个**参数上的，所以 `n + 0` 是定义直接给的，而 `0 + n` 必须用归纳法。但这次我们有新武器：`simp`。 `simp` 是一个智能化简策略——它知道很多基础引理（如 `Nat.add_zero`、`Nat.add_succ`），能自动帮你做重写。第 5 课手动写的 `rw`，`simp` 一行搞定。

本关学到的新东西

策略 (Tactics)

simp智能化简。自动使用已标记的引理（如 Nat.add_succ）进行重写

概念 (Concepts)

@[simp] 引理被标记为 simp 的引理，simp 策略会自动调用它们

加法不对称n+0=n 由加法定义直接可得，0+n=n 则需要归纳法

证明目标

当前目标

⊢∀ n : Nat, 0 + n = n

分步提示

1.和第五课一样，用 `intro n` 把 n 引入，然后 `induction n with` 做归纳。
2.基本情况 `zero`：目标 `0 + 0 = 0`。直接用 `rfl`——加法定义第一句就说了 0+0=0。
3.归纳步 `succ n ih`：目标是 `0 + (n+1) = n+1`。用 `simp [ih]` 一行搞定。
4.`simp [ih]` 做了两件事：(1) 用 `Nat.add_succ` 把左边展开，(2) 用归纳假设 `ih` 代换。比第五课的 `rw [Nat.add_succ, ih]` 更省事。

怎么玩：编辑器里有预写代码。直接点 运行 ▶ 看效果，或修改代码后运行。卡住了看左侧的提示。

Lean 代码编辑器