関数型と依存関数型¶
型 α β : Type から構成される型 α → β は関数型です．
たとえば Nat → Nat は，自然数を受け取って自然数を返す型です．
関数型の項は式 fun x => t のように書けます．これは無名関数を作る式で，数学の \(x \mapsto t\) に対応します．
def simpleTypedFunction : Nat → Nat :=
fun n => n + 1
example : simpleTypedFunction 4 = 5 := by
rfl
example (P Q : Prop) (hPQ : P → Q) (hP : P) : Q :=
hPQ hP
より一般には，返り値の型が入力の値に依存することがあります．
これを依存関数型と呼びます．
Lean では (x : α) → β x と書けます．
特に全称命題は，結論が命題であるような依存関数型 (x : α) → P x です．
例として，入力 n に応じて長さ n のベクトルを返す関数を考えます．
Lean では，長さ n の Nat ベクトルを Vector Nat n と書けます．
したがって (n : Nat) → Vector Nat n は，n を受け取ると「長さ n の自然数ベクトル」を返す型です．
これは返り値の型そのものが入力 n に依存しているので，依存関数型の例になっています．
次の zeroVec n は，0 を n 回並べたベクトルです．
表示するときは toList で通常のリストに戻して確認します．
def zeroVec (n : Nat) : Vector Nat n :=
Vector.replicate n 0
#check Vector
#check Vector.replicate
#check zeroVec
#check (zeroVec 4)
#eval (zeroVec 4).toList
example : (zeroVec 4).toList = [0, 0, 0, 0] := by
rfl
#check ((n : Nat) → Vector Nat n)
なお，通常の List Nat でも「0 が並んだリスト」を作れますが，型は常に List Nat なので，長さ n は型には現れません．
Vector Nat n を使うと，長さ n であることが返り値の型に入ります．
次の IsEvenNat n は，「自然数 n が偶数である」という命題です．
これは真偽値 Bool を返す判定関数ではなく，証明すべき命題を返す述語です．
def IsEvenNat (n : Nat) : Prop :=
∃ k : Nat, n = 2 * k
example : IsEvenNat 4 := by
unfold IsEvenNat
exact ⟨2, rfl⟩
ここで ⟨2, rfl⟩ は，「具体的な値」と「その値が条件を満たす証明」をまとめたデータです．
「証拠として k = 2 を選び，4 = 2 * 2 は rfl で示せる」という意味です．
山括弧 ⟨...⟩ は，型が要求している部品を順に与えて値や証明を作るための notation です．
より正確には constructor を使う省略記法ですが，constructor 一般の説明は structure と inductive 型の節で扱います．
次の全称命題
∀ n : Nat, IsEvenNat (2 * n) は，各自然数 n に対して命題 IsEvenNat (2 * n) の証明を返す依存関数型です．
この見方が，Lean で「全称命題の証明を関数のように適用する」理由です．
#check (∀ n : Nat, IsEvenNat (2 * n))
theorem twice_is_even (n : Nat) : IsEvenNat (2 * n) := by
unfold IsEvenNat
exact ⟨n, rfl⟩
example : IsEvenNat (2 * 7) := by
exact twice_is_even 7
演習¶
自然数を 2 倍する関数を def で定義し，簡単な計算例を証明してください．