插曲：命题、证明与索引

与许多语言一样，Lean 使用方括号对数组和列表进行索引。 例如，若 woodlandCritters 定义如下：

def woodlandCritters : List String :=
  ["hedgehog", "deer", "snail"]

则可以提取各个组件：

def hedgehog := woodlandCritters[0]
def deer := woodlandCritters[1]
def snail := woodlandCritters[2]

然而，试图提取第四个元素会导致编译时错误，而非运行时错误：

def oops := woodlandCritters[3]

failed to prove index is valid, possible solutions:
  - Use `have`-expressions to prove the index is valid
  - Use `a[i]!` notation instead, runtime check is perfomed, and 'Panic' error message is produced if index is not valid
  - Use `a[i]?` notation instead, result is an `Option` type
  - Use `a[i]'h` notation instead, where `h` is a proof that index is valid
⊢ 3 < List.length woodlandCritters

此错误消息表明 Lean 尝试自动数学证明 3 < List.length oodlandCritters， 这意味着查找是安全的，但它无法做到。越界错误是一类常见的错误，而 Lean 会利用其作为编程语言和定理证明器的双重特性来排除尽可能多的错误。

要理解它是如何工作的，需要理解三个关键概念：命题、证明与策略。

命题与证明

命题（Proposition） 是可以为真或为假的陈述句。以下所有句子都是命题：

• 1 + 1 = 2
• 加法满足交换律
• 质数有无穷多个
• 1 + 1 = 15
• 巴黎是法国的首都
• 布宜诺斯艾利斯是韩国的首都
• 所有鸟都会飞

另一方面，无意义的陈述不是命题。以下都不是命题：

• 1 + 绿色 = 冰激凌
• 所有首都都是质数
• 至少有一个韟韚是一个棴囄䪖

命题有两种类型：纯粹的数学命题，仅依赖于我们对概念的定义；以及关于世界的事实。 像 Lean 这样的定理证明器关注的是前一类，而对企鹅的飞行能力或城市的法律地位无话可说。

证明（Proof） 是说明命题是否为真的令人信服的论证。对于数学命题， 这些论证利用了所涉及概念的定义以及逻辑论证规则。 大多数证明都是为人的理解而写的，并省略了许多繁琐的细节。 像 Lean 这样的计算机辅助定理证明器旨在允许数学家在省略许多细节的情况下编写证明， 而软件负责填写缺失的明显步骤。这降低了疏忽或出错的可能性。

在 Lean 中，程序的类型描述了与它交互的方式。例如，类型为 Nat → List String 的程序是一个函数，它接受一个 Nat 参数并生成一个字符串列表。 换句话说，每个类型都指定了具有该类型的程序的内容。

在 Lean 中，命题即是类型。它们指定了语句为真的证据应有的内容。 通过提供此证据即可证明命题。另一方面，如果命题为假，则不可能构造此证据。

例如，命题「1 + 1 = 2」可以直接写在 Lean 中。此命题的证据是构造子 rfl， 它是 自反性（Reflexivity） 的缩写：

def onePlusOneIsTwo : 1 + 1 = 2 := rfl

另一方面，rfl 不能证明错误命题「1 + 1 = 15」：

def onePlusOneIsFifteen : 1 + 1 = 15 := rfl

type mismatch
  rfl
has type
  1 + 1 = 1 + 1 : Prop
but is expected to have type
  1 + 1 = 15 : Prop

此错误消息表明，当等式语句的两边已经是相同的数字时，rfl 可以证明两个表达式相等。 因为 1 + 1 直接计算为 2，所以它们被认为是相同的，这允许接受 onePlusOneIsTwo。 就像 Type 描述了表示数据结构和函数的类型（例如 Nat、String 和 List (Nat × String × (Int → Float))）一样，Prop 描述了命题。

当一个命题被证明后，它被称为一个 定理（Theorem） 。 在 Lean 中，惯例是用 theorem 关键字而非 def 来声明定理。 这有助于读者看出哪些声明旨在被解读为数学证明，哪些是定义。 一般来说，对于一个证明，重要的是有证据表明一个命题是正确的， 但提供 哪个 个证据并不特别重要。另一方面，对于定义，选择哪个特定值非常重要。 毕竟，一个总是返回 0 的加法定义显然是错误的。

前面的例子可以改写如下：

def OnePlusOneIsTwo : Prop := 1 + 1 = 2

theorem onePlusOneIsTwo : OnePlusOneIsTwo := rfl

策略

证明通常使用 策略（Tactic） 来编写，而非直接提供证据。策略是为命题构建证据的小程序。 这些程序在一个 证明状态（Proof Statemen） 中运行，该状态跟踪要证明的陈述（称为 目标（Goal）） 以及可用于证明它的假设。在目标上运行策略会产生一个包含新目标的新证明状态。 当所有目标都被证明后，证明就完成了。

要使用策略编写证明，请以 by 开始定义。编写 by 会将 Lean 置于策略模式， 直到下一个缩进块的末尾。在策略模式下，Lean 会持续提供有关当前证明状态的反馈。 使用策略编写的 onePlusOneIsTwo 仍然很短：

theorem onePlusOneIsTwo : 1 + 1 = 2 := by
  simp

simp 策略，即「化简（Simplify）」的缩写，是 Lean 证明的主力。 它将目标重写为尽可能简单的形式，处理足够小的证明部分。特别是，它用于证明简单的相等陈述。 在幕后，它会构建一个详细的形式化证明，但使用 simp 隐藏了这种复杂性。

策略在许多方面很有用：

1. 许多证明在写到最小的细节时都很复杂且乏味，而策略可以自动完成这些无趣的部分。
2. 使用策略编写的证明更容易维护，因为灵活的自动化可以弥补定义的细微更改。
3. 由于一个策略可以证明许多不同的定理，Lean 可以使用幕后的策略来解放用户亲手写证明。 例如，数组查找需要证明索引在范围内，而策略通常可以在用户无需担心它的情况下构造该证明。

在幕后，索引记法使用策略来证明用户的查找操作是安全的。 这个策略是 simp，它被配置为考虑某些算术恒等式。

连词

逻辑的基本构建块，例如「与」、「或」、「真」、「假」和「非」，称为 逻辑连词（Logical Connective）。 每个连词定义了什么算作其真值的证据。例如，要证明一个陈述「A 与 B」，必须证明 A 和 B。 这意味着「A 与 B」的证据是一对，其中包含 A 的证据和 B 的证据。 类似地，「A 或 B」的证据由 A 的证据或 B 的证据组成。

特别是，大多数这些连词都像数据类型一样定义，并且它们有构造子。若 A 和 B 是命题， 则「A 与 B」（写作 A ∧ B）也是一个命题。 A ∧ B 的证据由构造子 And.intro 组成， 其类型为 A → B → A ∧ B。用具体命题替换 A 和 B， 可以用 And.intro rfl rfl 证明 1 + 1 = 2 ∧ "Str".append "ing" = "String"。 当然，simp 也足够强大到可以找到这个证明：

theorem addAndAppend : 1 + 1 = 2 ∧ "Str".append "ing" = "String" := by simp

与此类似，「A 或 B」（写作 A ∨ B）有两个构造子， 因为「A 或 B」的证明仅要求两个底层命题中的一个为真。它有两个构造子： Or.inl， 类型为 A → A ∨ B， 以及 Or.inr， 类型为 B → A ∨ B。

蕴含（若 A 则 B）使用函数表示。特别是，将 A 的证据转换为 B 的证据的函数本身就是 A 蕴涵 B 的证据。这与蕴涵的通常描述不同， 其中 A → B 是 ¬A ∨ B 的简写，但这两个式子是等价的。

由于「与」的证据是一个构造子，所以它可以与模式匹配一起使用。 例如，证明 A 且 B 蕴涵 A 或 B 的证明是一个函数， 它从 A 和 B 的证据中提取 A（或 B）的证据，然后使用此证据来生成 A 或 B 的证据：

theorem andImpliesOr : A ∧ B → A ∨ B :=
  fun andEvidence =>
    match andEvidence with
    | And.intro a b => Or.inl a

The simp 策略可以证明使用了这些连接词的定理。例如：

theorem onePlusOneAndLessThan : 1 + 1 = 2 ∨ 3 < 5 := by simp
theorem notTwoEqualFive : ¬(1 + 1 = 5) := by simp
theorem trueIsTrue : True := True.intro
theorem trueOrFalse : True ∨ False := by simp
theorem falseImpliesTrue : False → True := by simp

证据作为参数

尽管 simp 在证明涉及特定数字的等式和不等式的命题时表现出色， 但它在证明涉及变量的语句时效果不佳。例如，simp 可以证明 4 < 15， 但它不能轻易地判断出因为 x < 4，所以 x < 15 也成立。由于索引记法在幕后使用 simp 来证明数组访问是安全的，因此它可能需要一些人工干预。

要让索引记法正常工作的最简单的方式之一，就是让执行数据结构查找的函数将所需的安全性证据作为参数。 例如，返回列表中第三个条目的函数通常不安全，因为列表可能包含零、一或两个条目：

def third (xs : List α) : α := xs[2]

failed to prove index is valid, possible solutions:
  - Use `have`-expressions to prove the index is valid
  - Use `a[i]!` notation instead, runtime check is perfomed, and 'Panic' error message is produced if index is not valid
  - Use `a[i]?` notation instead, result is an `Option` type
  - Use `a[i]'h` notation instead, where `h` is a proof that index is valid
α : Type ?u.3908
xs : List α
⊢ 2 < List.length xs

然而，可以通过添加一个参数来强制调用者证明列表至少有三个条目，该参数包含索引操作安全的证据：

def third (xs : List α) (ok : xs.length > 2) : α := xs[2]

在本例中，xs.length > 2 并不是一个检查 xs 是否有 2 个以上条目的程序。 它是一个可能是真或假的命题，参数 ok 必须是它为真的证据。

当函数在一个具体的列表上调用时，它的长度是已知的。在这些情况下，by simp 可以自动构造证据：

#eval third woodlandCritters (by simp)

"snail"

无证据索引

在无法证明索引操作在边界内的情况下，还有其他选择。添加一个问号会产生一个 Option， 如果索引在边界内，结果为 some，否则为 none。例如：

def thirdOption (xs : List α) : Option α := xs[2]?

#eval thirdOption woodlandCritters

some "snail"

#eval thirdOption ["only", "two"]

none

还有一个版本，当索引超出边界时会使程序崩溃，而非返回一个 Option：

#eval woodlandCritters[1]!

"deer"

小心！因为使用 #eval 运行的代码在 Lean 编译器的上下文中运行， 选择错误的索引可能会使你的 IDE 崩溃。

你可能会遇到的信息

除了 Lean 在找不到编译时证据而无法证明索引操作安全时产生的错误之外， 使用不安全索引的多态函数可能会产生以下消息：

def unsafeThird (xs : List α) : α := xs[2]!

failed to synthesize instance
  Inhabited α

这是由于技术限制，该限制是将 Lean 同时用作证明定理的逻辑和编程语言的一部分。 特别是，只有类型中至少包含一个值的程序才允许崩溃。 这是因为 Lean 中的命题是一种对真值证据进行分类的类型。假命题没有这样的证据。 如果具有空类型的程序可能崩溃，那么该崩溃程序可以用作对假命题的一种假的证据。

在内部，Lean 包含一个已知至少有一个值的类型的表。此错误表明某个任意类型 α 不一定在该表中。 下一章描述如何向此表添加内容，以及如何成功编写诸如 unsafeThird 之类的函数。

在列表和用于查找的括号之间添加空格会产生另一条消息：

#eval woodlandCritters [1]

function expected at
  woodlandCritters
term has type
  List String

添加空格会导致 Lean 将表达式视为函数应用，并将索引视为包含单个数字的列表。 此错误消息是由 Lean 尝试将 woodlandCritters 视为函数而产生的。

练习

• 使用 rfl 证明以下定理：2 + 3 = 5、15 - 8 = 7、 "Hello, ".append "world" = "Hello, world"。 如果使用 rfl 证明 5 < 18 会发生什么？为什么？
• 使用 by simp 证明以下定理：2 + 3 = 5、15 - 8 = 7、 "Hello, ".append "world" = "Hello, world"、5 < 18。
• 编写一个函数，用于查找列表中的第五个条目。将此查找安全的证据作为参数传递给函数。