Lean 4 证明样例

下面给出一个 Lean 4 证明题的简单示例，证明加法的交换律 $a + b = b + a$。该示例展示了如何在 Lean 4 中使用“归纳法”(induction)和基础战术来完成一个比较基础的自然数相关证明。

lean
import Lean

open Nat

-- 我们声明一个定理 (theorem) 来说明对任意自然数 a 和 b，它们的加法满足交换律。
theorem add_comm (a b : Nat) : a + b = b + a := by
  -- 对 a 做归纳(induction)，分为 a = 0 和 a = succ a' 两种情况
  induction a with
  | zero =>
    -- 当 a = 0 时，需要证明 0 + b = b + 0
    -- 利用 zero_add 和 add_zero 两个引理即可得到结论
    rw [zero_add, add_zero]
  | succ a' ih =>
    -- 当 a = succ a' 时，假设 a' + b = b + a' (这是归纳假设 ih)
    -- 再通过对 succ 形式的运算性质做相应替换和重写
    rw [succ_add, ih, add_succ]

解释：

1. theorem add_comm (a b : Nat) : a + b = b + a := by ...

   • 声明了一个名为 add_comm 的定理，要求证明：对任意自然数 $a$ 与 $b$，都有 $a + b = b + a$。

2. induction a with

   • 对自然数 $a$ 进行归纳(induction)。Lean 会自动拆分为两种情况：
     • | zero =>：当 $a = 0$ 时
     • | succ a' ih =>：当 $a = \mathrm{succ}(a')$ 时，并且 Lean 会在 ih 中提供归纳假设：$a' + b = b + a'$

3. 在 | zero => 这一支，我们需要证明 $0 + b = b + 0$。

   • 利用标准库中的 zero_add（$0 + b = b$）和 add_zero（$b + 0 = b$）这两个引理，可以很容易地完成简化和重写(rw)。

4. 在 | succ a' ih => 这一支，我们先使用 rw [succ_add] 和 add_succ 等引理，把加法拆解成更易处理的形式，然后用 ih（即归纳假设：$a' + b = b + a'$）完成重写，得到最后的结论。

以上就是一个 Lean 4 中常见的自然数证明示例。通过此例可以看到 Lean 4 的归纳结构与战术用法，日常可以将其扩展到更复杂的数学或逻辑证明中去。

在 Lean 4 中，Nat.zero_add 和 Nat.add_zero 这类引理在默认环境里并不像 Lean 3 那样直接可用；如果直接 rw [zero_add, add_zero]，Lean 往往会报「unknown identifier 'zero_add'」之类的错。要么自行定义这些引理，要么使用 Lean 4 中的「可直接化简」(definitional equality) 来完成证明。

下面给出两种可行的做法。

---

做法一：直接依赖「可直接化简」(definitional equality)

Lean 4 对 0 + b 与 b 的相等是「定义层面」就成立的（definitional equality），因此在 a = 0 这一分支可以直接用 rfl (reflection lemma) 完成证明，而不需要借助 zero_add。同理，Nat.succ_add 与 Nat.add_succ 这两个性质在 Lean 4 标准库是已存在的。以下代码可以正常编译：

lean
import Lean

open Nat

theorem add_comm (a b : Nat) : a + b = b + a := by
  induction a with
  | zero =>
    -- Lean 4 会将 0 + b 与 b 视为“定义上相同”
    rfl
  | succ a ih =>
    -- succ_add:    succ a + b = succ (a + b)
    -- add_succ:    b + succ a = succ (b + a)
    -- ih:          a + b = b + a
    rw [Nat.succ_add, ih, Nat.add_succ]

• | zero => rfl：在分支 $a = 0$ 时，0 + b 与 b 是定义层面（defeq）相同，所以 rfl 即可证明 0 + b = b + 0。
• | succ a ih =>：在分支 $a = \mathrm{succ}(a')$ 时，分别用 Nat.succ_add、归纳假设 ih、Nat.add_succ 进行重写即可。

这样做不需要显式使用 zero_add、add_zero 这些名字。

---

做法二：手动定义并使用 zero_add、add_zero

如果你想在 Lean 4 中保留与 Lean 3 类似的思路，显式「重写」0 + b = b 和 b + 0 = b，可以自己先定义它们：

lean
import Lean

open Nat

-- 手动为 Lean 4 补充 zero_add 和 add_zero
theorem zero_add (b : Nat) : 0 + b = b := rfl

theorem add_zero (b : Nat) : b + 0 = b := by
  induction b with
  | zero => 
    -- 0 + 0 = 0
    rfl
  | succ n ih => 
    -- (n+1) + 0 = n+1
    -- 利用 succ_add: (n+1) + 0 = succ (n + 0)
    rw [Nat.succ_add, ih]
    rfl

theorem add_comm (a b : Nat) : a + b = b + a := by
  induction a with
  | zero =>
    rw [zero_add, add_zero]
  | succ a ih =>
    rw [Nat.succ_add, ih, Nat.add_succ]

• 这里 theorem zero_add (b : Nat) : 0 + b = b := rfl 告诉 Lean 4：0 + b 和 b 在本质上是相同的（即可直接用 rfl）。
• theorem add_zero (b : Nat) : b + 0 = b 里，我们对 b 进行归纳，再用 Nat.succ_add（Lean 4 中自带的引理）简化得到最终结果。
• 在证明 add_comm 时，就可以像 Lean 3 那样 rw [zero_add, add_zero]。

---

小结

• 若想图省事：直接用 Lean 4 自带的「定义等价」(defeq) 处理 0 + b 和 b + 0，在归纳时对 0 分支用 rfl，对 succ 分支各用 Nat.succ_add / Nat.add_succ 即可。
• 若想保留原先 Lean 3 那种写法：可以手动声明 zero_add、add_zero，然后用 rw 重写。

这两种做法都可以解决「unknown identifier 'zero_add'」的报错，并成功完成对加法交换律的证明。

在 Lean 4 中，0 + b 和 b 之间通常是「定义上相同」(defeq) 的，但这并不意味着 Lean 4 会将 0 + b 和 b + 0 也直接当作相同。因为要证明的是 0 + b = b + 0，Lean 会告诉你它无法直接用 rfl 证明二者「定义层面相等」。这就是

text
error: tactic 'rfl' failed, the left-hand side
  0 + b
is not definitionally equal to the right-hand side
  b + 0

报错的原因。

下面给出几种可行的解决方案。

---

方案一：手动声明并使用 zero_add、add_zero 引理

如果你想和 Lean 3 一样使用 rw [zero_add, add_zero]，则需要自己在 Lean 4 中先声明这两个引理。示例代码如下：

lean
import Lean

open Nat

-- 声明 'zero_add' 证明 0 + b 与 b 在定义上相同
theorem zero_add (b : Nat) : 0 + b = b := rfl

-- 声明 'add_zero' 证明 b + 0 与 b 在定义上相同
theorem add_zero (b : Nat) : b + 0 = b := by
  induction b with
  | zero => 
    rfl
  | succ n ih =>
    -- (n+1) + 0 = succ (n + 0) ，再用归纳假设 ih : n + 0 = n
    rw [Nat.succ_add, ih]
    rfl

theorem add_comm (a b : Nat) : a + b = b + a := by
  induction a with
  | zero =>
    -- 这里就可以直接重写
    rw [zero_add, add_zero]
  | succ a ih =>
    -- succ_add:    succ a + b = succ (a + b)
    -- add_succ:    b + succ a = succ (b + a)
    rw [Nat.succ_add, ih, Nat.add_succ]

这样就能成功编译通过，也能在分支 | zero => ... 处使用 rw [zero_add, add_zero] 了。

---

方案二：利用 Lean 4 的“定义化简”配合手动步骤

如果不想声明这两个引理，那么在 a = 0 的分支，Lean 4 只“定义化简”得到 0 + b = b。但是我们最终要的形状是 b + 0。我们可以手动把 b 变成 b + 0，比如：

lean
import Lean

open Nat

theorem add_comm (a b : Nat) : a + b = b + a := by
  induction a with
  | zero =>
    -- 先用 dsimp 让 Lean 做一次简单化简 (0 + b → b)
    dsimp
    -- 现在我们的目标变为证明 b = b + 0，
    -- 这在 Lean 4 中依然不是“定义层面”相同，
    -- 可以通过归纳 b 或使用上面自定义的 add_zero。
    -- 这里我们直接对 b 做归纳：
    induction b with
    | zero => rfl
    | succ n ih =>
      rw [Nat.add_succ]
      -- 现在目标是 n.succ = Nat.succ n，
      -- 这是 rfl 能处理的（定义上相同）
      rfl
  | succ a ih =>
    -- 与之前一样处理
    rw [Nat.succ_add, ih, Nat.add_succ]

此写法看起来稍显繁琐，因为为了把 b 变成 b + 0，我们又对 b 做了一次归纳。不过也能证明结果。

---

方案三：不要求「0 + b = b + 0」直接 rfl，而是一步步 rewrites

还有一种思路是：在 | zero => ... 分支先把 b + 0 改写为 b，再用 rfl 即可。例如：

lean
import Lean

open Nat

theorem add_comm (a b : Nat) : a + b = b + a := by
  induction a with
  | zero =>
    -- 先把右边的 b + 0 重写为 b
    -- 这里 Lean 4 自带的 `Nat.add_zero` 通常可以用
    -- 如果不可用，就像方案一那样手动声明
    rw [Nat.add_zero]
    -- 现在目标变为 0 + b = b
    -- 这个等式在 Lean 4 中是定义层面相同，可以用 rfl
    rfl
  | succ a ih =>
    rw [Nat.succ_add, ih, Nat.add_succ]

要点：

• 你可以先把“右边”(b + 0)改写成 b，再用 rfl 就成功了，因为 0 + b 与 b 定义上相同。
• 这需要 Nat.add_zero 这个引理可用。如果 Lean 告诉你「unknown identifier Nat.add_zero」，就需要像方案一那样先手动声明 theorem add_zero ...。

---

小结

• 如果你想直接 rw [zero_add, add_zero]，请手动声明这两个引理；Lean 4 默认环境里，它们不像 Lean 3 那样“随手可用”。
• 若不想声明，可以用 Lean 4 对「0 + b = b」的定义化简，然后对 b + 0 做一步 rewrite，再 rfl。
• 或者在 | zero => ... 里对 b 再归纳，显式把 b 变成 b + 0。

以上几种方式都能让 Lean 4 接受你的证明，从而修复「rfl failed」或「unknown identifier zero_add」之类的报错。

在 Lean 3 中，类似 zero_add、add_zero 这类关于加法的基本引理往往「开箱即用」，所以可以直接 rw [zero_add, add_zero] 或用 rfl 解决 0 + b = b 之类的目标；然而 Lean 4 的默认环境并不会直接提供这些引理，也不一定把 0 + b 和 b 认作「定义层面(defeq)」相等，从而导致

text
tactic 'rfl' failed, the left-hand side
  0 + b
is not definitionally equal to the right-hand side
  b

这样的报错。

要解决这个问题，有两条常见路径：

---

路径一：手动定义 zero_add、add_zero

最直接的方式是自己在 Lean 4 中把这两个基础引理补齐，然后在需要的地方重写 (rw) 即可。示例如下：

lean
import Lean

open Nat

-- 1. 声明 zero_add: 证明 0 + b = b
theorem zero_add (b : Nat) : 0 + b = b := by
  induction b with
  | zero => 
    -- 目标是 0 + 0 = 0，Lean 4 认为是“定义层面相同”，rfl 即可
    rfl
  | succ n ih =>
    -- 现在目标是 (n+1) + 0 = (n+1)，我们可以用 succ_add
    rw [Nat.succ_add, ih]
    rfl

-- 2. 声明 add_zero: 证明 b + 0 = b
theorem add_zero (b : Nat) : b + 0 = b := by
  induction b with
  | zero => 
    rfl
  | succ n ih =>
    rw [Nat.succ_add, ih]
    rfl

-- 3. 利用上述两个引理完成加法交换律的证明
theorem add_comm (a b : Nat) : a + b = b + a := by
  induction a with
  | zero =>
    -- 当 a = 0 时，需要证明 0 + b = b + 0
    -- 我们可以先把 0 + b 重写成 b，再把 b + 0 重写成 b
    -- 也可以直接 rw [zero_add, add_zero] 一次到位
    rw [zero_add, add_zero]
  | succ a ih =>
    -- 当 a = succ a 时，目标是 (succ a) + b = b + (succ a)
    -- Lean 4 默认提供了 succ_add, add_succ 这两个引理可用
    rw [Nat.succ_add, ih, Nat.add_succ]

这样编译通过后，就不会再报“unknown identifier 'zero_add'”或“tactic 'rfl' failed”的错了。

---

路径二：不定义引理，改用分步或二次归纳

如果你不想显式声明 zero_add、add_zero，也可以在分支 a = 0 时对 b 再做一次归纳，手动把 0 + b 化简到 b，再把 b + 0 化简到 b，最后用 rfl。写法相对啰嗦一些：

lean
import Lean

open Nat

theorem add_comm (a b : Nat) : a + b = b + a := by
  induction a with
  | zero =>
    -- 目标：0 + b = b + 0
    -- 先对 b 做归纳
    induction b with
    | zero => 
      -- 目标：0 + 0 = 0 + 0
      rfl
    | succ n ih =>
      -- 目标：0 + (n+1) = (n+1) + 0
      -- 先把左边化简为 n+1，再把右边化简为 n+1
      rw [Nat.succ_add]  -- 0 + (n+1) = n+1
      rw [Nat.succ_add]  -- (n+1) + 0 = n+1
      rfl
  | succ a ih =>
    -- 与往常类似，直接对 succ 情况用已知引理
    rw [Nat.succ_add, ih, Nat.add_succ]

这样也能最终得到 a + b = b + a。只不过，每次在 a=0 的分支上你都要额外多写一层对 b 的归纳。

---

总结

• 推荐做法：** 手动在 Lean 4 中声明 zero_add、add_zero**（就像上面第一种路径所示），然后在需要处 rw [zero_add, add_zero]。这样可以重现 Lean 3 里熟悉的写法，也不用二次归纳，代码简洁。
• 如果不想声明额外引理，可以用「对 b 归纳」或其他手动重写的方式，但代码往往会啰嗦一些，还需要你自己把 0 + b、b + 0 都化简到同一个“中间形状”，Lean 4 才能用 rfl。