8.5. 有界数🔗

Array 和 Nat 的 GetElem 实例要求有一个证明，证明所提供的 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 := _} 的东西。

当给定的数大于界限时，Fin 的 OfNat 实例并不失败，而是返回该数对界限取模后的值。这意味着 #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

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

8.5.1. 练习🔗

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

some 4#eval (3 : Fin 8).next?

输出

some 4

并且

none#eval (7 : Fin 8).next?

输出

none