NNG4 Solutions 简中版

网站托管于海因里希·海涅杜塞尔多夫大学

假定您对 Lean 4 有基本的了解——至少知道它是做什么的。

教程世界

第1关：rfl 策略

介绍第一个策略（tactic）——rfl，它可以证明所有形如 X = X 的定理。

example (x q : Nat) : 37 * x + q = 37 * x + q := by
  rfl

关于 rfl：

• rfl 是“相等关系的自反性”（reflexivity of equality）的缩写。
• 出于教学目的，我们的 rfl 比标准 Lean 中的版本要弱一些。数学家不区分命题相等与定义相等——在他们看来，zero_add 和 add_zero 都只是“事实”，谁在乎加法是如何定义的呢。
• 因此在标准 Lean 中，2 + 2 = 4 可以用 rfl 来证明，因为它是定义相等。但在 NNG4 中，2 + 2 = 4 无法仅用 rfl 证明。

第2关：rw 策略

证明方法很简单，就是将 h 代入目标表达式，这可以通过 rw [h] 实现。重写之后，目标变为 2 * (x + 7) = 2 * (x + 7)。

example (x y : Nat) (h : y = x + 7) : 2 * y = 2 * (x + 7) := by
  rw [h]
  rfl

关于 rw：

• 如果 h 是一个形如 X = Y 的相等关系的证明，那么 rw [h] 会将目标中所有的 X 替换成 Y。这就是“代入”的方法。

第3关：数字

Lean 中的自然数由两条规则定义。

• 0 是一个自然数。
• 如果 n 是一个自然数，那么 n 的后继（successor）succ n 也是一个自然数。

n 的后继指紧跟在 n 之后的自然数。

example : 2 = succ (succ 0) := by
  rw [two_eq_succ_one]
  rw [one_eq_succ_zero]
  rfl