配列と添え字アクセス

休憩の章ではリスト内の要素を位置で検索するためのインデックス記法の使い方を説明しています。この構文も型クラスによって管理され、様々な異なる型に対して使うことができます。

配列

例えば、Leanの配列は連結リストよりもはるかに効率的です。Leanでは、Array α 型は α 型の値を保持する可変長配列であり、Javaの ArrayList 、C++の std::vector 、Rustの Vec などにとても近いものです。コンストラクタ cons を使用するたびにポインタのインダイレクトが発生する List とは異なり、配列は連続したメモリ領域を占有します。これはプロセッサのキャッシュとかなり相性が良いです。また、配列の値を検索する時間は一定ですが、連結リストの値を検索する時間はアクセスしたい添え字に比例します。

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" と、それに続く他の4つのクモを合わせて合計5つのクモで構成されます：

def idahoSpiders : NonEmptyList String := {
  head := "Banded Garden Spider",
  tail := [
    "Long-legged Sac Spider",
    "Wolf Spider",
    "Hobo Spider",
    "Cat-faced Spider"
  ]
}

再帰関数でこのリストの特定のインデックスの値を調べるには3つの可能性を考慮する必要があります：

添え字が 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 という名前空間修飾子は必要ありません。この関数の別の書き方として、添え字が0より大きい場合にはリストの get? を使う方法があります：

def NonEmptyList.get? : NonEmptyList α → Nat → Option α
  | xs, 0 => some xs.head
  | xs, n + 1 => xs.tail.get? n

リストの要素が1つの場合、0 だけが有効なインデックスです。リストの要素が2つの場合、0 と 1 の両方が有効なインデックスです。リストの要素が3つの場合、 0 、1 、2 が有効なインデックスです。言い換えると、空でないリストへの有効なインデックスはリストの長さ未満の自然数であり、末尾のリストの長さ以下です。

添え字が許容されることの根拠を見つけるために使用されるタクティクによって整数についての不等式を解くことができますが、NonEmptyList.inBounds という名前については何も知らないため、添え字が範囲内であることの意味の定義は abbrev として書かれなければなりません：

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 は4つのパラメータを持ちます：

コレクションの型
インデックスの型
コレクションを展開した時に得られる要素の型
インデックスが範囲内であることの根拠のポイントを決定づける関数

要素の型と根拠の関数はどちらも出力パラメータになっています。GetElem には getElem というメソッドが1つだけあり、コレクションの値、インデックスの値、インデックスが範囲内にあることを示す根拠を引数として受け取り、要素を返します：

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 α の場合、3つのパラメータは以下になります：

コレクションは 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 になります。

Functional Programming in Lean 日本語訳

配列と添え字アクセス

配列

空でないリスト

オーバーロードされた添え字アクセス