安全な配列のインデックス
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