跳到主要内容

Lean 第一个程序

Lean 是一种交互式定理证明器和编程语言，广泛应用于数学证明和函数式编程。对于初学者来说，编写并运行第一个程序是掌握 Lean 的第一步。本文将带你从零开始，编写并运行你的第一个 Lean 程序。

什么是 Lean？​

Lean 是一种基于依赖类型的函数式编程语言，专为数学证明和形式化验证设计。它结合了编程语言和定理证明器的功能，允许用户编写程序并验证其正确性。

安装 Lean​

在开始编写程序之前，你需要确保 Lean 已经安装在你的计算机上。你可以通过以下步骤安装 Lean：

  1. 访问 Lean 官方网站 并按照安装指南进行操作。
  2. 安装完成后，打开终端并输入 lean --version 来验证安装是否成功。

编写第一个 Lean 程序​

让我们从一个简单的程序开始。我们将编写一个函数，计算两个整数的和。

步骤 1: 创建 Lean 文件​

首先，创建一个新的 Lean 文件，命名为 FirstProgram.lean。你可以使用任何文本编辑器或 IDE 来创建这个文件。

步骤 2: 编写代码​

在 FirstProgram.lean 文件中，输入以下代码：

lean
def add (a b : ℕ) : ℕ :=
  a + b

步骤 3: 解释代码​

  • def 是 Lean 中定义函数的关键字。
  • add 是函数的名称。
  • (a b : ℕ) 表示函数接受两个自然数（ℕ 是自然数的类型）作为参数。
  • : ℕ 表示函数的返回值类型也是自然数。
  • := 是定义函数体的符号。
  • a + b 是函数体，表示将两个参数相加。

步骤 4: 运行程序​

要运行这个程序，你可以使用 Lean 的交互式环境。打开终端并导航到 FirstProgram.lean 文件所在的目录，然后输入以下命令：

bash
lean --run FirstProgram.lean

如果一切顺利，你将不会看到任何输出，因为我们的程序只是定义了一个函数，并没有调用它。

步骤 5: 调用函数​

为了看到函数的效果，我们需要调用它并打印结果。修改 FirstProgram.lean 文件，添加以下代码：

lean
#eval add 2 3
  • #eval 是 Lean 中用于评估表达式并打印结果的命令。
  • add 2 3 是调用 add 函数，传入参数 2 和 3。

再次运行程序，你将看到输出：

bash
5

实际应用场景​

在实际应用中，Lean 常用于数学证明和形式化验证。例如，你可以使用 Lean 来证明一个数学定理，或者验证一个算法的正确性。

示例：证明加法交换律​

让我们通过一个简单的例子来展示 Lean 的证明功能。我们将证明加法的交换律，即 a + b = b + a。

lean
theorem add_comm (a b : ℕ) : a + b = b + a :=
begin
  induction a with d hd,
  { simp },
  { simp [hd] }
end
  • theorem 是 Lean 中定义定理的关键字。
  • add_comm 是定理的名称。
  • (a b : ℕ) 表示定理适用于任意两个自然数。
  • : a + b = b + a 是定理的陈述。
  • begin ... end 是证明的主体部分。
  • induction a with d hd 是对 a 进行归纳法证明。
  • simp 是 Lean 中的简化策略，用于简化表达式。

运行这个定理，Lean 将验证 a + b = b + a 的正确性。

总结​

通过本文，你已经学会了如何在 Lean 中编写并运行第一个程序。我们从简单的加法函数开始，逐步深入，展示了 Lean 在数学证明中的应用。Lean 不仅是一种编程语言，更是一个强大的工具，能够帮助你验证数学定理和算法的正确性。

附加资源​

练习​

  1. 修改 add 函数，使其能够处理整数（ℤ）而不是自然数（ℕ）。
  2. 编写一个函数 multiply，计算两个自然数的乘积，并使用 #eval 测试它。
  3. 尝试证明乘法的结合律，即 (a * b) * c = a * (b * c)。

通过完成这些练习，你将进一步巩固对 Lean 的理解和应用能力。