Lean 公理系统
引言
Lean是一种交互式定理证明器，广泛用于形式化数学和编程验证。它的核心是公理系统，即一组基本的假设和规则，用于构建数学证明。理解Lean的公理系统是掌握Lean证明基础的关键。本文将带你逐步了解Lean公理系统的结构、工作原理以及如何在实际中应用它。
什么是公理系统？
公理系统是数学和逻辑学中的基础框架，由一组公理（axioms）和推理规则（inference rules）组成。公理是无需证明的基本命题，而推理规则则定义了如何从已知命题推导出新命题。
在Lean中，公理系统是形式化数学的基础。它允许用户通过定义公理和规则来构建复杂的数学结构，并验证其正确性。
Lean 公理系统的核心组件
Lean的公理系统由以下几个核心组件构成：
- 公理（Axioms）：无需证明的基本命题。
- 定义（Definitions）：基于公理或已有定义的新概念。
- 推理规则（Inference Rules）：从已知命题推导出新命题的规则。
- 类型系统（Type System）：用于描述数学对象的结构和关系。
1. 公理
公理是Lean中最基本的构建块。它们是不可证明的命题，但被接受为真。例如，在Lean中，我们可以定义一个简单的公理：
axiom my_axiom : Prop
这里，my_axiom 是一个命题（Prop 类型），但我们没有提供它的证明。
2. 定义
定义是基于公理或已有定义的新概念。例如，我们可以定义一个命题 my_prop，它依赖于 my_axiom：
def my_prop : Prop := my_axiom
3. 推理规则
推理规则定义了如何从已知命题推导出新命题。例如，Lean中的 intro 规则用于引入假设：
example : my_prop → my_prop :=
begin
intro h,
exact h,
end
在这个例子中，intro h 引入了假设 h : my_prop，然后 exact h 证明了目标。
4. 类型系统
Lean的类型系统是其公理系统的重要组成部分。它允许我们定义和操作各种数学对象。例如，我们可以定义一个自然数类型：
inductive Nat : Type
| zero : Nat
| succ : Nat → Nat
这里，Nat 是一个归纳类型，zero 是自然数的起点，succ 是后继函数。
实际案例：证明一个简单命题
让我们通过一个简单的例子来展示Lean公理系统的实际应用。假设我们要证明命题 A → A，即“如果A成立，那么A成立”。
example : ∀ (A : Prop), A → A :=
begin
intros A h,
exact h,
end
解释
intros A h：引入假设A : Prop和h : A。exact h：使用假设h直接证明目标。
这个例子展示了Lean公理系统的基本推理过程。
总结
Lean的公理系统是形式化数学和编程验证的强大工具。通过公理、定义、推理规则和类型系统，Lean允许用户构建复杂的数学结构并验证其正确性。本文介绍了Lean公理系统的核心组件，并通过实际案例展示了其应用。
附加资源与练习
资源
- Lean官方文档
- 《Theorem Proving in Lean》：一本深入讲解Lean的书籍。
练习
- 在Lean中定义一个公理
my_axiom2 : Prop，并基于它定义一个命题my_prop2。 - 尝试证明命题
∀ (A B : Prop), A → (B → A)。 - 使用Lean的类型系统定义一个布尔类型
Bool，并实现逻辑与运算and。
通过练习，你将更深入地理解Lean公理系统的工作原理和应用场景。