安全数组索引

Array 和 Nat 的 GetElem 实例需要证明提供的 Nat 小于数组。在实践中，这些证明通常最终会连同索引一起传递给函数。与其分别传递索引和证明，可以使用名为 Fin 的类型将索引和证明捆绑到单个值中。这可以使代码更易阅。此外，许多对数组的内置操作将其索引参数作为 Fin 而非 Nat，因此使用这些内置操作需要了解如何使用 Fin。

类型 Fin n 表示严格小于 n 的数字。换句话说，Fin 3 描述 0、1 和 2，而 Fin 0 没有任何值。Fin 的定义类似于 Subtype，因为 Fin n 是一个包含 Nat 和小于 n 的证明的结构体：

structure Fin (n : Nat) where
  val  : Nat
  isLt : LT.lt val n

Lean 包含 ToString 和 OfNat 的实例，允许将 Fin 值方便地用作数字。换句话说，#eval (5 : Fin 8) 的输出为 5，而非类似 {val := 5, isLt := _} 的值。

当提供的数字大于边界时，OfNat 实例对于 Fin 不会失败，而是返回一个对边界取模的值。这意味着 #eval (45 : Fin 10) 的结果是 5，而非编译时错误。

在返回类型中，将 Fin 作为找到的索引返回，能够让它与其所在的数据结构的连接更加清晰。上一节中的 Array.find 返回一个索引，调用者不能立即使用它来执行数组查找，因为有关其有效性的信息已丢失。更具体类型的值可以直接使用，而不会使程序变得复杂得多：

def findHelper (arr : Array α) (p : α → Bool) (i : Nat) : Option (Fin arr.size × α) :=
  if h : i < arr.size then
    let x := arr[i]
    if p x then
      some (⟨i, h⟩, x)
    else findHelper arr p (i + 1)
  else none
termination_by findHelper arr p i => arr.size - i

def Array.find (arr : Array α) (p : α → Bool) : Option (Fin arr.size × α) :=
  findHelper arr p 0

练习

编写一个函数 Fin.next? : Fin n → Option (Fin n) 当 Fin 在边界内时返回下一个最大的 Fin，否则返回 none。检查

#eval (3 : Fin 8).next?

会输出

some 4

而

#eval (7 : Fin 8).next?

会输出

none

Lean 函数式编程

安全数组索引

练习