引言

Lean 是 Microsoft Research 开发的交互式定理证明器，基于依值类型论（Dependent Type Theory）。 依值类型论将程序和证明的世界统一了起来，因此，Lean 也是一门编程语言。 Lean 认真地对待其双重性质，并且被设计为适合作为通用编程语言使用，Lean 甚至是用它自己实现的。本书介绍了如何使用 Lean 编程。

作为一门编程语言，Lean 是一种具有依值类型的严格纯函数式语言。 学习使用 Lean 编程很大一部分内容在于学习这些属性是如何影响程序编写方式的， 以及如何像函数式程序员一样思考。

• 严格性（Strictness） 意味着 Lean 中的函数调用与大多数语言中的工作方式类似： 在函数体开始运行之前，参数会被完全计算。
• 纯粹性（Purity） 意味着 Lean 程序除非明确声明，否则无法产生副作用， 例如修改内存中的位置、发送电子邮件或删除文件等。 Lean 是一种 函数式（Functional） 语言，这意味着函数就像任何其他值一样是一等值， 并且执行模型受数学表达式的求值启发。
• 依值类型（Dependent type） 是 Lean 最不寻常的特性，它使类型成为语言的一等部分， 允许类型包含程序，而程序计算类型。

本书面向想要学习 Lean 的程序员，但未必以前使用过函数式编程语言。 读者不需要熟悉 Haskell、OCaml 或 F# 等函数式语言。而另一方面，本书确实假定读者了解循环、 函数和数据结构等大多数编程语言中的常见概念。虽然本书旨在成为一本关于函数式编程的优秀入门书， 但它并不是一本关于一般编程的入门书。

对于将 Lean 作为证明助手的数学家来说，他们可能需要在某个时间点编写自定义的证明自动化工具， 本书也适用于他们。随着这些工具变得越来越复杂，它们也会越来越像函数式语言编写的程序， 但大多数在职数学家接受的是 Python 和 Mathematica 等语言的培训。 本书可以帮助他们弥合这一差距，让更多数学家能够编写可维护且易于理解的证明自动化工具。

本书旨在从头到尾线性阅读。概念一次引入一个，后面的章节会假定读者熟悉前面的章节。 有时，后面的章节会深入探讨一个之前仅简要讨论过的主题。本书的某些章节包含练习。 为了巩固你对该章节的理解，这些练习值得一做。在阅读本书时探索 Lean 也很有用， 可以发现能利用你所学知识的创造性新方法。

获取 Lean

在编写并运行 Lean 所编写的程序之前，你需要在自己的计算机上设置 Lean。Lean 工具包括以下内容：

• elan：用于管理 Lean 编译器工具链，类似于 rustup 或 ghcup。
• lake：用于构建 Lean 包及其依赖项，类似于 cargo、make 或 Gradle。
• lean：用于对 Lean 文件进行类型检查和编译，并向程序员工具提供当前正在编写的文件的相关信息。 通常，lean 是由其他工具而非用户直接调用的。
• 编辑器插件，如 Visual Studio Code 或 Emacs，可与 Lean 通信并方便地显示其信息。

有关安装 Lean 的最新说明，请参阅 Lean 手册。

排版约定

作为 输入 提供给 Lean 的代码示例格式如下：

def add1 (n : Nat) : Nat := n + 1

#eval add1 7

上面最后一行（以 #eval 开头）是指示 Lean 计算答案的命令。Lean 的回复格式如下：

8

Lean 返回的错误消息格式如下：

application type mismatch
  add1 "seven"
argument
  "seven"
has type
  String : Type
but is expected to have type
  Nat : Type

警告格式如下：

declaration uses 'sorry'

Unicode

惯用的 Lean 代码会使用各种不属于 ASCII 的 Unicode 字符。例如，希腊字母（如 α 和 β） 和箭头（→）都出会现在本书的第一章中。这使得 Lean 代码更接近于普通的数学记法。

在默认的 Lean 设置中，Visual Studio Code 和 Emacs 都允许使用反斜杠 (\) 后跟名称来输入这些字符。 例如，要输入 α，请键入 \alpha。要了解如何在 Visual Studio Code 中键入字符， 请将鼠标指向该字符并查看工具提示。在 Emacs 中，将光标置于相关字符上，然后使用 C-c C-k 即可查看提示。