Lean 证明简介
Lean是一种交互式定理证明器，专为形式化数学和编程语言设计。它允许用户通过编写代码来定义数学对象和证明定理。Lean的核心思想是将数学证明转化为计算机可以理解和验证的形式化证明。对于初学者来说，Lean提供了一个强大的工具来学习和实践数学证明。
什么是Lean证明？
Lean证明是指在Lean环境中，通过编写代码来构造和验证数学定理的过程。Lean使用一种称为依赖类型理论的数学基础，这使得它能够表达复杂的数学概念，并确保证明的正确性。
为什么使用Lean？
- 形式化验证：Lean可以自动验证证明的正确性，减少人为错误。
- 交互式学习：Lean提供了即时反馈，帮助用户理解每一步的证明过程。
- 可扩展性：Lean支持自定义数学结构和定理，适合研究和新领域的探索。
Lean 证明的基本结构
在Lean中，证明通常由以下几个部分组成：
- 定义：定义数学对象或概念。
- 定理声明：声明要证明的定理。
- 证明构造：通过一系列步骤构造证明。
示例：证明1 + 1 = 2
让我们从一个简单的例子开始，证明 1 + 1 = 2。
-- 定义自然数
inductive Nat where
| zero : Nat
| succ : Nat → Nat
-- 定义加法
def add : Nat → Nat → Nat
| Nat.zero, n => n
| Nat.succ m, n => Nat.succ (add m n)
-- 定理声明
theorem one_plus_one_eq_two : add (Nat.succ Nat.zero) (Nat.succ Nat.zero) = Nat.succ (Nat.succ Nat.zero) :=
-- 证明构造
rfl
在这个例子中，我们首先定义了自然数 Nat 和加法函数 add。然后，我们声明了一个定理 one_plus_one_eq_two，并使用 rfl（自反性）来证明它。
rfl 是 Lean 中的一个内置策略，用于证明两个表达式在定义上相等。
逐步讲解
1. 定义数学对象
在Lean中，数学对象通常通过归纳类型来定义。例如，自然数可以定义为：
inductive Nat where
| zero : Nat
| succ : Nat → Nat
这里，Nat 是一个归纳类型，zero 表示0，succ 表示后继函数，即 succ n 表示 n + 1。
2. 定义函数
接下来，我们可以定义加法函数 add：
def add : Nat → Nat → Nat
| Nat.zero, n => n
| Nat.succ m, n => Nat.succ (add m n)
这个函数通过模式匹配来定义：如果第一个参数是 zero，则返回第二个参数；否则，递归地计算 m + n 并返回其后续。
3. 声明定理
定理的声明通常使用 theorem 关键字：
theorem one_plus_one_eq_two : add (Nat.succ Nat.zero) (Nat.succ Nat.zero) = Nat.succ (Nat.succ Nat.zero) :=
这里，我们声明了一个定理 one_plus_one_eq_two，表示 1 + 1 = 2。
4. 构造证明
在Lean中，证明通常通过策略（tactics）来构造。在这个例子中，我们使用了 rfl 策略，它表示“自反性”，即如果两个表达式在定义上相等，则它们相等。
rfl
实际案例
证明交换律
让我们证明加法的交换律，即 a + b = b + a。
theorem add_comm : ∀ (a b : Nat), add a b = add b a :=
by
intros a b
induction a with
| zero =>
simp [add]
| succ a ih =>
simp [add]
rw [ih]
在这个证明中，我们使用了归纳法来证明交换律。首先，我们引入变量 a 和 b，然后对 a 进行归纳。在归纳步骤中，我们使用了归纳假设 ih 来简化证明。
simp 是 Lean 中的一个简化策略，用于简化表达式。rw 是重写策略，用于根据等式重写表达式。
总结
Lean证明是一种强大的工具，可以帮助初学者理解和实践数学证明。通过定义数学对象、声明定理和构造证明，Lean使得形式化验证变得简单而直观。希望本文能够帮助你入门Lean证明，并激发你进一步探索的兴趣。
附加资源
练习
- 尝试在Lean中定义乘法函数
mul，并证明2 * 3 = 6。 - 证明加法的结合律，即
(a + b) + c = a + (b + c)。 - 探索Lean中的其他策略，如
induction和cases，并尝试在证明中使用它们。
Happy proving!