3.4. 数组和索引🔗

命题，证明与索引一节描述了如何使用索引表示法按位置查找列表中的条目。此语法也由类型类管理，并且可以用于各种不同的类型。

3.4.1. 数组🔗

例如，对于大多数用途，Lean 数组比链表效率高得多。在 Lean 中，类型 Array α 是一个动态大小的数组，用于保存类型为 α 的值，非常类似于 Java ArrayList、C++ std::vector 或 Rust Vec。不像是 List 在每次使用 cons 构造器时都会有一个指针指向每个节点，数组占用连续的内存区域，这对于处理器缓存要好得多。此外，在数组中查找值需要常量时间，而在链表中查找则需要与所访问索引成比例的时间。

在像 Lean 这样的纯函数式语言中，在数据结构中改变某位置上的数据的值是不可能的。相反，Lean 会制作一个副本，该副本具有所需的修改。当使用一个数组时，Lean 编译器和运行时包含了一个优化：当该数组只被引用了一次时，会在幕后将制作副本优化为原地操作。

数组的写法与列表类似，但以 # 开头：

def northernTrees : Array String :=
  #["sloe", "birch", "elm", "oak"]

可以使用 Array.size 计数数组中的值。例如，northernTrees.size 为 4。对于小于数组大小的索引，可以使用索引表示法来查找相应的值，就像列表一样。也就是说，northernTrees[2] 为 "elm"。同样，编译器需要一个索引值未越界的证明。尝试去查找越界的值会导致编译时错误，就和列表一样。例如，northernTrees[8] 会导致：

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 performed, 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
⊢ 8 < northernTrees.size

3.4.2. 非空列表🔗

一个表示非空列表的数据类型可以被定义为一个结构，这个结构有一个列表头字段，和一个尾字段。尾字段是一个常规的，可能为空的列表。

structure NonEmptyList (α : Type) : Type where
  head : α
  tail : List α

例如，非空列表 idahoSpiders（其中包含一些原产于美国爱达荷州的蜘蛛物种）由 "Banded Garden Spider" 和其他四种蜘蛛组成，总共五种蜘蛛：

def idahoSpiders : NonEmptyList String := {
  head := "Banded Garden Spider",
  tail := [
    "Long-legged Sac Spider",
    "Wolf Spider",
    "Hobo Spider",
    "Cat-faced Spider"
  ]
}

使用递归函数在此列表中查找特定索引处的值应考虑三种可能性：

索引为 0，在这种情况下应返回列表的头部。
索引为 n + 1 且尾部为空，在这种情况下索引越界。
索引为 n + 1 且尾部不为空，在这种情况下可以对尾部和 n 递归调用该函数。

例如，一个返回 Option 的查找函数可以写成如下：

def NonEmptyList.get? : NonEmptyList α → Nat → Option α
  | xs, 0 => some xs.head
  | {head := _, tail := []}, _ + 1 => none
  | {head := _, tail := h :: t}, n + 1 => get? {head := h, tail := t} n

模式匹配中的每种情况都对应于上述可能性之一。对 get? 的递归调用不需要 NonEmptyList 命名空间限定符，因为定义的正文隐式地位于定义的命名空间。编写此函数的另一种方法是在索引大于零时使用列表查找 xs.tail[n]?：

def NonEmptyList.get? : NonEmptyList α → Nat → Option α
  | xs, 0 => some xs.head
  | xs, n + 1 => xs.tail[n]?

如果列表包含一个条目，则只有 0 是有效索引。如果它包含两个条目，则 0 和 1 都是有效索引。如果它包含三个条目，则 0、1 和 2 都是有效索引。换句话说，非空列表的有效索引是严格小于列表长度的自然数，即小于或等于尾部长度。

“索引值没有出界”意味着什么的这个定义，应该被写成一个 abbrev。因为这个可以用来证明索引值未越界的策略（tactics）要在不知道 NonEmptyList.inBounds 这个方法的情况下解决数字之间的不等关系。(此处原文表意不明，按原文字面意思译出。原文大致意思应为 abbrev 比 def 对 tactic 的适应性更好)

abbrev NonEmptyList.inBounds (xs : NonEmptyList α) (i : Nat) : Prop :=
  i ≤ xs.tail.length

此函数返回一个可能为真或为假的命题。例如，2 对于 idahoSpiders 未越界，而 5 越界了：

theorem atLeastThreeSpiders : idahoSpiders.inBounds 2 := by⊢ idahoSpiders.inBounds 2 decideAll goals completed! 🐙

theorem notSixSpiders : ¬idahoSpiders.inBounds 5 := by⊢ ¬idahoSpiders.inBounds 5 decideAll goals completed! 🐙

逻辑非运算符的优先级非常低，这意味着 ¬idahoSpiders.inBounds 5 等价于 ¬(idahoSpiders.inBounds 5)。

这个事实可以用来编写一个查找函数，该函数需要索引有效的证据，因此不必返回 Option，方法是委托给在编译时检查证据的列表版本：

def NonEmptyList.get (xs : NonEmptyList α)
    (i : Nat) (ok : xs.inBounds i) : α :=
  match i with
  | 0 => xs.head
  | n + 1 => xs.tail[n]

当然，将这个函数写成直接用证据的形式也是可能的。但这需要会玩证明和命题的一些技术，这些内容会在本书后续内容中提到。

3.4.3. 重载索引🔗

集合类型的索引表示法可以通过定义 GetElem 类型类的实例来重载。为了灵活性，GetElem 有四个参数：

集合的类型
索引的类型
集合中元素的类型
一个函数，用于确定什么是索引在边界内的证据

元素类型和证据函数都是输出参数。 GetElem 有一个方法，getElem，它接受一个集合值、一个索引值和索引在边界内的证据，并返回一个元素：

class GetElem
    (coll : Type)
    (idx : Type)
    (item : outParam Type)
    (inBounds : outParam (coll → idx → Prop)) where
  getElem : (c : coll) → (i : idx) → inBounds c i → item

在 NonEmptyList α 的情况下，这些参数是：

集合是 NonEmptyList α
索引的类型为 Nat
元素的类型为 α
索引如果小于等于列表尾那么就没有越界

实际上，GetElem 实例可以直接使用 NonEmptyList.get：

instance : GetElem (NonEmptyList α) Nat α NonEmptyList.inBounds where
  getElem := NonEmptyList.get

有了这个实例，NonEmptyList 的使用就和 List 一样方便了。计算 idahoSpiders.head 会得到 "Banded Garden Spider"，而 idahoSpiders[9] 会导致编译时错误：

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 performed, 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
⊢ idahoSpiders.inBounds 9

因为集合类型和索引类型都是 GetElem 类型类的输入参数，所以新类型可以用于索引到现有集合中。正数类型 Pos 是一个完全合理的 List 索引，但需要注意的是它不能指向第一个条目。 GetElem 的以下实例允许像使用 Nat 一样方便地使用 Pos 来查找列表条目：

instance : GetElem (List α) Pos α
    (fun list n => list.length > n.toNat) where
  getElem (xs : List α) (i : Pos) ok := xs[i.toNat]

索引对于非数字索引也可能很有意义。例如，Bool 可用于在点的字段之间进行选择，其中 false 对应于 x，true 对应于 y：

instance : GetElem (PPoint α) Bool α (fun _ _ => True) where
  getElem (p : PPoint α) (i : Bool) _ :=
    if not i then p.x else p.y

在这种情况下，两个布尔值都是有效索引。因为每个可能的 Bool 都在边界内，所以证据就是真命题 True。

3.4.1.	数组
3.4.2.	非空列表
3.4.3.	重载索引