插曲：命题、证明与索引
与许多语言一样，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]
此错误消息表明 Lean 尝试自动数学证明 3 < woodlandCritters.length（即 3 < List.length woodlandCritters），
这意味着查找是安全的，但它无法做到。越界错误是一类常见的错误，而 Lean
会利用其作为编程语言和定理证明器的双重特性来排除尽可能多的错误。
要理解它是如何工作的，需要理解三个关键概念：命题、证明与策略。
命题与证明
命题（Proposition） 是可以为真或为假的陈述句。以下所有句子都是命题：
-
1 + 1 = 2 -
加法满足交换律
-
质数有无穷多个
-
1 + 1 = 15 -
巴黎是法国的首都
-
布宜诺斯艾利斯是韩国的首都
-
所有鸟都会飞
另一方面，无意义的陈述不是命题。以下都不是命题：
-
1 + 绿色 = 冰激凌
-
所有首都都是质数
-
至少有一个韟韚是一个棴囄䪖
命题有两种类型：纯粹的数学命题，仅依赖于我们对概念的定义；以及关于世界的事实。 像 Lean 这样的定理证明器关注的是前一类，而对企鹅的飞行能力或城市的法律地位无话可说。
证明（Proof） 是说明命题是否为真的令人信服的论证。对于数学命题， 这些论证利用了所涉及概念的定义以及逻辑论证规则。 大多数证明都是为人的理解而写的，并省略了许多繁琐的细节。 像 Lean 这样的计算机辅助定理证明器旨在允许数学家在省略许多细节的情况下编写证明， 而软件负责填写缺失的明显步骤。这些步骤可以机械地检查。这降低了疏忽或出错的可能性。
在 Lean 中，程序的类型描述了与它交互的方式。例如，类型为 Nat → List String
的程序是一个函数，它接受一个 Nat 参数并生成一个字符串列表。
换句话说，每个类型都指定了具有该类型的程序的内容。
在 Lean 中，命题即是类型。它们指定了语句为真的证据应有的内容。 通过提供此证据即可证明命题。另一方面，如果命题为假，则不可能构造此证据。
例如，命题 1 + 1 = 2 可以直接写在 Lean 中。此命题的证据是构造子 rfl，
它是 自反性（Reflexivity） 的缩写：
在数学中，如果每个元素都与自身相关，则关系是 自反的（reflexive）；这是拥有合理相等概念的基本要求。
因为 1 + 1 计算为 2，所以它们实际上是同一件事：
def onePlusOneIsTwo : 1 + 1 = 2 := rfl
另一方面，rfl 不能证明错误命题 1 + 1 = 15：
def onePlusOneIsFifteen : 1 + 1 = 15 := rfl
此错误消息表明，当等式语句的两边已经是相同的数字时，rfl 可以证明两个表达式相等。
因为 1 + 1 直接计算为 2，所以它们被认为是相同的，这允许接受 onePlusOneIsTwo。
就像 Type 描述了表示数据结构和函数的类型（例如 Nat、String 和
List (Nat × String × (Int → Float))）一样，Prop 描述了命题。
当一个命题被证明后，它被称为一个 定理（Theorem） 。
在 Lean 中，惯例是使用 theorem 关键字而非 def 来声明定理。
这有助于读者看出哪些声明旨在被解读为数学证明，哪些是定义。
一般来说，对于一个证明，重要的是有证据表明一个命题是真实的，
但提供 哪个 个证据并不特别重要。另一方面，对于定义，选择哪个特定值非常重要。
毕竟，一个总是返回 0 的加法定义显然是错误的。
因为证明的细节对后续证明不重要，所以使用 theorem 关键字可以提高 Lean 编译器的并行性。
前面的例子可以改写如下：
def OnePlusOneIsTwo : Prop := 1 + 1 = 2
theorem onePlusOneIsTwo : OnePlusOneIsTwo := rfl策略
证明通常使用 策略（Tactic） 来编写，而非直接提供证据。策略是为命题构建证据的小程序。 这些程序在一个 证明状态（Proof State） 中运行，该状态跟踪要证明的陈述（称为 目标（Goal）） 以及可用于证明它的假设。在目标上运行策略会产生一个包含新目标的新证明状态。 当所有目标都被证明后，证明就完成了。
要使用策略编写证明，请以 by 开始定义。编写 by 会将 Lean 置于策略模式，
直到下一个缩进块的末尾。在策略模式下，Lean 会持续提供有关当前证明状态的反馈。
使用策略编写的 onePlusOneIsTwo 仍然很短：
theorem onePlusOneIsTwo : 1 + 1 = 2 := ⊢ 1 + 1 = 2
All goals completed! 🐙
decide 策略调用 判定过程（decision procedure），这是一个可以检查语句是真还是假，并在两种情况下返回合适证明的程序。
它主要用于处理像 1 和 2 这样的具体值。
本书中其他重要的策略是 simp（化简 simplify 的缩写）和策略 grind ，它们能自动证明很多定理。
策略在许多方面很有用：
-
许多证明在写到最小的细节时都复杂且乏味，而策略可以自动完成这些无趣的部分。
-
使用策略编写的证明更容易维护，因为灵活的自动化可以弥补定义的细微更改。
-
由于一个策略可以证明许多不同的定理，Lean 可以使用幕后的策略来解放用户亲手写证明。例如，数组查找需要证明索引在范围内，而策略通常可以在用户无需担心它的情况下构造该证明。
在幕后，索引记法使用策略来证明用户的查找操作是安全的。 这个策略考虑了许多关于算术的事实，并将它们与任何局部已知的事实结合起来，试图证明索引在界限内。
simp 策略是 Lean 证明的主力。
它将目标重写为尽可能简单的形式。在许多情况下，这种重写将语句简化到可以自动证明的程度。
在幕后，会构造一个详细的形式证明，但使用 simp 隐藏了这种复杂性。
正如 decide，grind 策略也用于完成证明。它运用了一系列来自 SMT 求解器的技术，可以证明各种各样的定理。与 simp 策略不同，grind 策略必须完整地完成证明过程才能取得进展；它要么完全成功，要么完全失败。
grind 策略功能强大、可定制且可扩展；正因如此，当它证明定理失败时，其输出包含大量信息，可以帮助专业 Lean 用户诊断失败原因。一开始可能会觉得信息量太大，因此本章仅使用 decide 和 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"。
当然，decide 也足够强大到可以找到这个证明：
theorem addAndAppend : 1 + 1 = 2 ∧ "Str".append "ing" = "String" := ⊢ 1 + 1 = 2 ∧ "Str".append "ing" = "String"
All goals completed! 🐙
与此类似，「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连词 | Lean 语法 | 证据 |
|---|---|---|
真 | ||
假 | 无证据 | |
|
|
|
|
| |
|
|
将 |
非 |
|
将 |
decide 策略可以证明使用了这些连接词的定理。例如：
theorem onePlusOneOrLessThan : 1 + 1 = 2 ∨ 3 < 5 := ⊢ 1 + 1 = 2 ∨ 3 < 5 All goals completed! 🐙
theorem notTwoEqualFive : ¬(1 + 1 = 5) := ⊢ ¬1 + 1 = 5 All goals completed! 🐙
theorem trueIsTrue : True := ⊢ True All goals completed! 🐙
theorem trueOrFalse : True ∨ False := ⊢ True ∨ False All goals completed! 🐙
theorem falseImpliesTrue : False → True := ⊢ False → True All goals completed! 🐙证据作为参数
要让索引记法正常工作的最简单的方式之一，就是让执行数据结构查找的函数将所需的安全性证据作为参数。 例如，返回列表中第三个条目的函数通常不安全，因为列表可能包含零、一或两个条目：
def third (xs : List α) : α := xs[2]然而，通过添加一个参数来强制调用者证明列表至少有三个条目，该参数包含索引操作安全的证据：
def third (xs : List α) (ok : xs.length > 2) : α := xs[2]
在本例中，xs.length > 2 并不是一个检查 是否 xs 有 2 个以上条目的程序。
它是一个可能是真或假的命题，参数 ok 必须是它为真的证据。
当函数在一个具体的列表上调用时，它的长度是已知的。在这些情况下，by decide 可以自动构造证据：
#eval third woodlandCritters (⊢ woodlandCritters.length > 2 All goals completed! 🐙)无证据的索引
在无法证明索引操作在边界内的情况下，还有其他选择。添加一个问号会产生一个 Option，
如果索引在边界内，结果为 some，否则为 none。例如：
def thirdOption (xs : List α) : Option α := xs[2]?#eval thirdOption woodlandCritters#eval thirdOption ["only", "two"]
还有一个版本，当索引超出边界时会使程序崩溃，而非返回一个 Option：
#eval woodlandCritters[1]!可能遇到的消息
除了证明一个语句是真实的之外，decide 策略还可以证明它是假的。
当被要求证明一个单元素列表有超过两个元素时，它会返回一个错误，表明该语句确实是假的：
#eval third ["rabbit"] (⊢ ["rabbit"].length > 2 ⊢ ["rabbit"].length > 2)
simp 和 decide 策略不会自动展开 def 定义。
尝试使用 OnePlusOneIsTwo 证明 simp 失败：
theorem onePlusOneIsStillTwo : OnePlusOneIsTwo := ⊢ OnePlusOneIsTwo ⊢ OnePlusOneIsTwo
错误消息只是简单地说明它什么也做不了，因为如果不展开 OnePlusOneIsTwo，就无法取得进展：
使用 decide 也失败了：
theorem onePlusOneIsStillTwo : OnePlusOneIsTwo := ⊢ OnePlusOneIsTwo ⊢ OnePlusOneIsTwo
这也是因为它没有展开 OnePlusOneIsTwo：
使用 abbrev 定义 OnePlusOneIsTwo 通过标记定义以进行展开来解决问题。
除了 Lean 在找不到编译时证据而无法证明索引操作安全时产生的错误之外， 使用不安全索引的多态函数可能会产生以下消息：
def unsafeThird (xs : List α) : α := xs[2]!这是由于技术限制，该限制是将 Lean 同时用作证明定理的逻辑和编程语言的一部分。 特别是，只有类型中至少包含一个值的程序才允许崩溃。 这是因为 Lean 中的命题是一种对真值证据进行分类的类型。假命题没有这样的证据。 如果具有空类型的程序可能崩溃，那么该崩溃程序可以用作对假命题的一种假的证据。
在内部，Lean 包含一个已知至少有一个值的类型的表。此错误表明某个任意类型 α 不一定在该表中。
下一章描述如何向此表添加内容，以及如何成功编写诸如 unsafeThird 之类的函数。
在列表和用于查找的括号之间添加空格会产生另一条消息：
#eval woodlandCritters [1]
添加空格会导致 Lean 将表达式视为函数应用，并将索引视为包含单个数字的列表。
此错误消息是由 Lean 尝试将 woodlandCritters 视为函数而产生的。