安全な配列のインデックス

Array と Nat についての GetElem インスタンスは与えられた Nat が配列よりも小さいことの証明を要求します。実際には、これらの証明はインデックスと一緒に関数に渡されることが多いです。インデックスと証明を別々に渡すのではなく、Fin という型を使うことで、インデックスと証明を1つの値にまとめることができます。これによりコードはさらに読みやすくなります。さらに、配列に対する組み込み操作の多くは、インデックスの引数を Nat ではなく Fin として受け取るため、これらの組み込み操作を使用するには Fin の使い方を理解する必要があります。

型 Fin n は n 未満の数を表します。つまり、Fin 3 は 0 ・1 ・2 を表し、Fin 0 は全く値を持ちません。Fin n はある Nat とそれが n より小さいことの証明を含む構造体であるため、Fin の定義は Subtype に似ています：

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

Leanは Fin の値を数値として便利に使うために ToString と OfNat のインスタンスを有しています。つまり、#eval (5 : Fin 8) の結果は {val := 5, isLt := _} ではなく 5 です。

与えた数値がその範囲より大きい場合に 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

演習問題

与えられた値の1つ大きい数値が範囲内であればその Fin を、そうでなければ none を返す関数 Fin.next? : Fin n → Option (Fin n) を書いてください。これが以下に対して

#eval (3 : Fin 8).next?

以下を出力し、

some 4

また以下に対して

#eval (7 : Fin 8).next?

以下を出力することを確かめてください。

none