Theorem Proving in Lean 4

1. 引言🔗

1.1. 计算机与定理证明🔗

形式化验证（Formal verification）涉及使用逻辑和计算方法来确证那些以精确数学术语表达的断言。这些断言可以包括普通的数学定理，也可以包括关于硬件或软件、网络协议以及机械和混合系统满足其规约的断言。在实践中，验证一个数学论断与验证一个系统的正确性之间并没有截然的区别：形式化验证需要用数学术语描述硬件和软件系统，此时确证其正确性的断言就成了一种定理证明。反过来，一个数学定理的证明可能需要大量的计算，在这种情况下，验证该定理的真实性就需要验证计算按预期执行。

支持一个数学断言的黄金标准是提供证明，而二十世纪逻辑学的发展表明，几乎所有传统的证明方法都可以在任意一个基础系统中被归约为少量的公理（axioms）和规则（rules）。借助这种归约，计算机可以在两个方面帮助确证一个断言：它可以帮助寻找证明，也可以帮助验证一个声称的证明是否正确。

自动定理证明（Automated theorem proving）侧重于“寻找”方面。归结定理证明器、表推演定理证明器、快速的 SAT 求解器等为命题逻辑和一阶逻辑中的公式有效性提供了确证手段。其他系统则为特定语言和领域（如整数或实数上的线性或非线性表达式）提供搜索过程和判定过程。像 SMT（Satisfiability Modulo Theories，即可满足性模理论）这样的架构将领域通用的搜索方法与领域特定的过程相结合。计算机代数系统和专门的数学软件包提供了执行数学计算、确定数学界限或寻找数学对象的手段。计算也可被视为一种证明，这些系统同样有助于确证数学断言。

自动推理系统（Automated reasoning systems）追求强大和高效，但往往以牺牲可靠性的保证为代价。这样的系统可能存在错误，且难以确保其交付的结果是正确的。相比之下，交互式定理证明（Interactive theorem proving）侧重于定理证明的“验证”方面，要求每个断言都有合适公理基础中的证明作支撑。这设定了一个非常高的标准：每一个推理规则和每一个计算步骤都必须通过引用先前的定义和定理来证成，一直回溯到基本的公理和规则。事实上，大多数此类系统都提供完全详细的“证明对象（proof objects）”，可以传递给其他系统并独立检查。构造这样的证明通常需要更多的用户输入和交互，但它允许你获得更深入、更复杂的证明。

Lean 定理证明器（Lean Theorem Prover）旨在通过在支持用户交互和完全指定的公理化证明构造的框架中融入自动化工具和方法，来弥合交互式与自动定理证明之间的鸿沟。其目标是支持数学推理和复杂系统的推理，并在这两个领域验证断言。

Lean 的底层逻辑具有计算解释，Lean 同样可以看作是一门编程语言。更进一步地说，它可以被看作是一个系统，用于编写具有精确语义的程序，以及推理程序所计算的函数。Lean 还具有作为其自身的元编程语言（metaprogramming language）的机制，这意味着你可以使用 Lean 本身来实现自动化和扩展 Lean 的功能。Lean 的这些方面在免费的在线书籍 Functional Programming in Lean 中有所描述，不过系统的计算方面也会在此书中出现。

1.2. 关于 Lean🔗

Lean 项目由 Leonardo de Moura 于 2013 年在微软研究院雷蒙德实验室发起。这是一项长期持续的努力，许多自动化的潜力将随着时间逐步实现。Lean 以 Apache 2.0 许可证发布，这是一种宽松的开源许可证，允许他人自由使用和扩展代码以及数学库。

要在你的计算机上安装 Lean，请参考 Quickstart 说明。Lean 的源代码及构建说明可在 https://github.com/leanprover/lean4/ 获取。

本教程描述的是 Lean 的当前版本，即 Lean 4。

1.3. 关于本书🔗

本书旨在教你如何在 Lean 中开发和验证证明。为此所需的许多背景知识其实并非 Lean 所特有。首先，你将学习 Lean 所基于的逻辑系统，它是依值类型论（Dependent Type Theory）的一个版本，其功能强大到足以证明几乎任何常规的数学定理，并且足够具有表现力来以自然的方式完成这项工作。更具体地说，Lean 基于一个称为构造演算（Calculus of Constructions）的系统版本，并带有归纳类型（inductive types）。Lean 不仅可以在依值类型论中定义数学对象和表达数学断言，还可以用作编写证明的语言。

由于完全详细的公理化证明非常复杂，定理证明的挑战在于让计算机尽可能多地填充细节。你将学习在依值类型论中支持这一点的各种方法。例如，项重写（term rewriting），以及 Lean 用于自动简化项和表达式的自动化方法。类似地，还有精化（elaboration）和类型推断（type inference）方法，可用于支持灵活的代数推理形式。

最后，你将学习 Lean 特有的特性，包括你用来与系统通信的语言，以及 Lean 提供的用于管理复杂理论和数据的机制。

在全书各处，你将看到类似下面的 Lean 代码示例：

theorem and_commutative (p q : Prop) : p ∧ q → q ∧ p := fun hpq : p ∧ q => have hp : p := And.left hpq have hq : q := And.right hpq show q ∧ p from And.intro hq hp

在本书中每个代码示例旁边，你会看到一个标有 “Copy to clipboard” 的按钮。按下该按钮会将示例及其足够的上下文一起复制，以使代码能够正确编译。你可以将示例代码粘贴到 VS Code 中并修改示例，Lean 将在你输入时持续检查结果并提供反馈。我们建议在阅读后续章节时自行运行这些示例并进行代码实验。你可以通过使用命令 “Lean 4: Docs: Show Documentation Resources” 并选择 “Theorem Proving in Lean 4” 在打开的标签页中在 VS Code 中打开本书。

1.4. 致谢🔗

本教程是一个在 Github 上维护的开放获取项目。许多人为此付出了努力，提供了修正、建议、示例和文字。我们感谢 Ulrik Buchholz、Kevin Buzzard、Mario Carneiro、Nathan Carter、Eduardo Cavazos、Amine Chaieb、Joe Corneli、William DeMeo、Marcus Klaas de Vries、Ben Dyer、Gabriel Ebner、Anthony Hart、Simon Hudon、Sean Leather、Assia Mahboubi、Gihan Marasingha、Patrick Massot、Christopher John Mazey、Sebastian Ullrich、Floris van Doorn、Daniel Velleman、Théo Zimmerman、Paul Chisholm、Chris Lovett 和 Siddhartha Gadgil 的贡献。请访问 lean prover 和 lean community 获取我们杰出贡献者的最新列表。