8.3. 数组与终止性
为了编写高效代码，选择合适的数据结构十分重要。 链表有其用武之地：在某些应用中，共享列表尾部的能力非常重要。 然而，对于可变长度的数据序列集合的大多数用例，数组都能提供更好的支持，因为数组既有更少的内存开销，也有更好的局部性。
然而，相对于列表，数组有两个缺点：
-
数组通过索引访问，而不是通过模式匹配访问；为了保持安全性，这会施加 证明义务。
-
从左到右处理整个数组的循环是一个尾递归函数，但它没有在每次调用时递减的参数。
要有效使用数组，需要知道如何向 Lean 证明某个数组索引在界内，以及如何证明一个趋近于数组大小的数组索引也会使程序终止。 这二者都是用不等式命题来表达的，而不是用命题等式来表达。
8.3.1. 不等式
由于不同类型具有不同的序关系概念，不等式由两个类型类支配，称为 LE 和 LT。
关于 标准类型类 的一节中的表格说明了这些类如何与语法相关联：
表达式 | 脱糖 | 类名 |
|---|---|---|
|
| |
|
| |
|
| |
|
|
换言之，一个类型可以自定义 < 和 ≤ 运算符的含义，而 > 和 ≥ 的含义则由 < 和 ≤ 派生而来。
类 LT 和 LE 具有返回命题而非 Bool 的方法：
class LE (α : Type u) where
le : α → α → Prop
class LT (α : Type u) where
lt : α → α → Prop
instance : LE Nat where
le := Nat.le
定义 Nat.le 需要 Lean 的一个尚未介绍的特性：它是一个归纳定义的关系。
8.3.1.1. 归纳定义的命题、谓词与关系
Nat.le 是一个归纳定义的关系。
正如 inductive 可用于创建新的数据类型一样，它也可用于创建新的命题。
当一个命题接受一个参数时，它被称为一个谓词，它可能对某些潜在参数为真，但不一定对所有潜在参数都为真。
接受多个参数的命题称为关系。
一个归纳定义的命题的每个构造子都是证明该命题的一种方式。 换言之，该命题的声明描述了表明它为真的各种证据形式。 一个没有参数且只有单个构造子的命题可能相当容易证明：
inductive EasyToProve : Prop where
| heresTheProof : EasyToProve该证明由使用其构造子组成：
theorem fairlyEasy : EasyToProve := ⊢ EasyToProve
All goals completed! 🐙
事实上，命题 True 应当总是容易证明的，它的定义正如 EasyToProve：
inductive True : Prop where
| intro : True
不带参数的归纳定义命题远不如归纳定义的数据类型有趣。
这是因为数据本身就很有意义——自然数 3 不同于数 35，而订购了 3 个披萨的人，如果 30 分钟后送到门口的是 35 个披萨，就会感到不满。
命题的构造子描述了该命题可以为真的方式，但一旦一个命题已经被证明，就没有必要知道底层使用了哪些构造子。
这就是为什么 Prop 宇宙中大多数有趣的归纳定义类型都带有参数。
归纳定义的谓词 IsThree 表明其参数是三：
inductive IsThree : Nat → Prop where
| isThree : IsThree 3
这里使用的机制正如 诸如 HasCol 这样的索引族，只是所得类型是可以被证明的命题，而不是可以被使用的数据。
使用这个谓词，可以证明三确实是三：
theorem three_is_three : IsThree 3 := ⊢ IsThree 3
All goals completed! 🐙
类似地，IsFive 是一个谓词，表示其参数是 5：
inductive IsFive : Nat → Prop where
| isFive : IsFive 5如果一个数是三，那么给它加二的结果应当是五。 这可以表达为一个定理陈述：
theorem three_plus_two_five : IsThree n → IsFive (n + 2) := n:Nat⊢ IsThree n → IsFive (n + 2)
n:Nat⊢ IsThree n → IsFive (n + 2)所得目标具有函数类型：
因此，intro 策略可用于把该参数转换为一个假设：
theorem three_plus_two_five : IsThree n → IsFive (n + 2) := n:Nat⊢ IsThree n → IsFive (n + 2)
n:Natthree:IsThree n⊢ IsFive (n + 2)
给定 n 为三这一假设，应当可以使用 IsFive 的构造子来完成证明：
theorem three_plus_two_five : IsThree n → IsFive (n + 2) := n:Nat⊢ IsThree n → IsFive (n + 2)
n:Natthree:IsThree n⊢ IsFive (n + 2)
n:Natthree:IsThree n⊢ IsFive (n + 2)然而，这会导致一个错误：
这个错误发生的原因是 n + 2 与 5 并非定义相等。
在普通的函数定义中，可以对假设 three 进行依值模式匹配，从而将 n 精化为 3。
与依值模式匹配对应的策略是 cases，其语法类似于 induction：
theorem three_plus_two_five : IsThree n → IsFive (n + 2) := n:Nat⊢ IsThree n → IsFive (n + 2)
n:Natthree:IsThree n⊢ IsFive (n + 2)
cases three with
⊢ IsFive (3 + 2)
在剩余情形中，n 已被细化为 3：
由于 3 + 2 按定义等于 5，该构造子现在可以应用：
theorem three_plus_two_five : IsThree n → IsFive (n + 2) := n:Nat⊢ IsThree n → IsFive (n + 2)
n:Natthree:IsThree n⊢ IsFive (n + 2)
cases three with
⊢ IsFive (3 + 2) All goals completed! 🐙
标准的假命题 False 没有构造子，因此不可能为其提供直接证据。
为 False 提供证据的唯一方式是某个假设本身不可能成立，这类似于 nomatch 可用于标记类型系统能够看出不可达的代码。
如 关于证明的最初插曲 中所述，否定 Not A 是 A → False 的缩写。
Not A 也可以写作 ¬A。
四并不是三：
theorem four_is_not_three : ¬ IsThree 4 := ⊢ ¬IsThree 4
⊢ ¬IsThree 4
初始证明目标包含 Not：
它实际上是函数类型这一事实可以用 unfold 暴露出来：
theorem four_is_not_three : ¬ IsThree 4 := ⊢ ¬IsThree 4
⊢ IsThree 4 → False
由于目标是函数类型，可以使用 intro 将参数转换为一个假设。
没有必要保留 unfold，因为 intro 本身可以展开 Not 的定义：
theorem four_is_not_three : ¬ IsThree 4 := ⊢ ¬IsThree 4
h:IsThree 4⊢ False
在这个证明中，cases 策略会立即解决目标：
theorem four_is_not_three : ¬ IsThree 4 := ⊢ ¬IsThree 4
h:IsThree 4⊢ False
All goals completed! 🐙
正如对 Vect String 2 进行模式匹配时不需要包含 Vect.nil 的情况一样，对 IsThree 4 进行按情况证明时也不需要包含 isThree 的情况。
8.3.1.2. 自然数的不等式
Nat.le 的定义有一个参数和一个索引：
inductive Nat.le (n : Nat) : Nat → Prop
| refl : Nat.le n n
| step : Nat.le n m → Nat.le n (m + 1)
参数 n 是应当较小的数，而索引是应当大于或等于 n 的数。
当两个数相等时使用 refl 构造子；当索引大于 n 时使用 step 构造子。
从证据的角度看，对 n \leq k 的证明由寻找某个数 d，使得 n + d = m 成立所组成。
在 Lean 中，该证明于是由一个 Nat.le.refl 构造子组成，并由 d 个 Nat.le.step 实例包裹。
每个 step 构造子都会给其索引参数加一，因此 d 个 step 构造子会给较大的数加上 d。
例如，四小于等于七的证据由三个围绕一个 refl 的 step 组成：
theorem four_le_seven : 4 ≤ 7 :=
open Nat.le in
step (step (step refl))严格小于关系通过给左侧的数加一来定义：
def Nat.lt (n m : Nat) : Prop :=
Nat.le (n + 1) m
instance : LT Nat where
lt := Nat.lt
四严格小于七的证据由包围着一个 refl 的两个 step 组成：
theorem four_lt_seven : 4 < 7 :=
open Nat.le in
step (step refl)
这是因为 4 < 7 等价于 5 ≤ 7。
8.3.2. 证明终止性
函数 Array.map 用一个函数变换数组，返回一个新数组，其中包含将该函数应用于输入数组每个元素所得的结果。
将它写成尾递归函数遵循通常的模式：委托给一个把输出数组作为累加器传递的函数。
该累加器初始化为空数组。
这个传递累加器的辅助函数还接受一个参数，用以跟踪数组中的当前索引；该索引从 0 开始：
def Array.map (f : α → β) (arr : Array α) : Array β :=
arrayMapHelper f arr Array.empty 0
该辅助函数应当在每次迭代时检查索引是否仍在界内。
若在界内，它应当将变换后的元素添加到累加器末尾，并将索引增加 1，然后再次循环。
若不在界内，则它应当终止并返回累加器。
这段代码的初始实现会失败，因为 Lean 无法证明数组索引是有效的：
def arrayMapHelper (f : α → β) (arr : Array α)
(soFar : Array β) (i : Nat) : Array β :=
if i < arr.size then
arrayMapHelper f arr (soFar.push (f arr[i])) (i + 1)
else soFar
然而，条件表达式已经检查了数组索引的有效性所要求的精确条件（即 i < arr.size）。
给 if 添加一个名称可以解决该问题，因为它添加了一个可供数组索引策略使用的假设：
def arrayMapHelper (f : α → β) (arr : Array α)
(soFar : Array β) (i : Nat) : Array β :=
if inBounds : i < arr.size then
arrayMapHelper f arr (soFar.push (f arr[i])) (i + 1)
else soFarLean 接受这个修改后的程序，尽管递归调用并不是在某个输入构造子的参数上进行的。 事实上，累加器和索引都在增长，而不是缩小。
在幕后，Lean 的证明自动化会构造一个终止性证明。 重构这个证明可以使那些 Lean 无法自动识别的情形更容易理解。
为什么 arrayMapHelper 会终止？
每次迭代都会检查索引 i 是否仍在数组 arr 的边界内。
如果在边界内，则 i 递增并重复循环。
如果不在边界内，则程序终止。
因为 arr.size 是一个有限数，所以 i 只能递增有限多次。
尽管该函数没有任何参数在每次调用时递减，arr.size - i 却朝着零递减。
在每次递归调用中递减的值称为度量。
可以通过在定义末尾提供 termination_by 子句，指示 Lean 使用某个特定表达式作为终止性的度量。
对于 arrayMapHelper，显式的度量如下所示：
def arrayMapHelper (f : α → β) (arr : Array α)
(soFar : Array β) (i : Nat) : Array β :=
if inBounds : i < arr.size then
arrayMapHelper f arr (soFar.push (f arr[i])) (i + 1)
else soFar
termination_by arr.size - i
可以使用类似的终止性证明来编写 Array.find，这是一个函数，它在数组中寻找第一个满足某个布尔函数的元素，并返回该元素及其索引：
def Array.find (arr : Array α) (p : α → Bool) :
Option (Nat × α) :=
findHelper arr p 0
同样，辅助函数会终止，因为随着 i 增大，arr.size - i 会减小：
def findHelper (arr : Array α) (p : α → Bool)
(i : Nat) : Option (Nat × α) :=
if h : i < arr.size then
let x := arr[i]
if p x then
some (i, x)
else findHelper arr p (i + 1)
else none
给 termination_by 添加一个问号（也就是说，使用 termination_by?）会使 Lean 明确建议它所选择的度量。
点击 [apply] 会将 termination_by? 替换为所建议的度量：
def findHelper (arr : Array α) (p : α → Bool)
(i : Nat) : Option (Nat × α) :=
if h : i < arr.size then
let x := arr[i]
if p x then
some (i, x)
else findHelper arr p (i + 1)
else none
termination_by?并非所有终止性论证都像这个一样简单。 然而，在所有终止性证明中，都会出现这样一种基本结构：基于函数的参数识别某个表达式，并使它在每次调用中减小。 有时，为了弄清楚一个函数究竟为什么会终止，可能需要创造性；有时，Lean 需要额外的证明才能接受该度量确实会减小。