数组与索引

在插入章节中描述了如何使用索引符号来通过位置查找列表中的条目。此语法也由类型类管理，并且可以用于各种不同的类型。

数组

比如说，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 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
⊢ 8 < Array.size northernTrees

非空列表

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

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 命名空间标识符，因为定义内部隐式地在定义的命名空间中。另一种方式来编写这个函数是：当索引大于零时就将 get? 应用在列表上。

def NonEmptyList.get? : NonEmptyList α → Nat → Option α
  | xs, 0 => some xs.head
  | xs, n + 1 => xs.tail.get? 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 simp

theorem notSixSpiders : ¬idahoSpiders.inBounds 5 := by simp

逻辑非运算符有很低的结合度，这意味着 ¬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]

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

重载索引

对于集合类型的索引符号，可通过定义 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[0] 结果为 "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 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
⊢ NonEmptyList.inBounds idahoSpiders 9

因为集合的类型和索引的类型都是 GetElem 类型类的参数，所以可以使用新类型来索引现有的集合。之前的 Pos 是一个完全合理的可以用来索引 List 的类型，但注意它不能指向第一个条目。下面 GetElem 的实例使 Pos 在查找列表条目方面和 Nat 一样方便。

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 命题。

Lean 函数式编程

数组与索引

数组

非空列表

重载索引