#check
#check
コマンドは、項の型を表示します。Lean ではすべての項に型があるので、どんな項にも使えます。#check term
というコマンドで、term
の型を表示します。逆に term
の型が T
であることを確かめるには example
コマンドを使用して example : T := term
とします。
基本的な項の型
-- 文字
#check 'a'
-- 文字列
#check "Hello"
-- 自然数
#check 1
-- 浮動小数点数
#check 1.0
-- 整数
#check -2
-- `1` はそのままだと自然数扱いになるが、整数にキャストできる
#check (1 : Int)
-- 自然数のリスト
#check [1, 2, 3]
-- 自然数の配列
#check #[1, 2, 3]
-- 関数
#check fun x ↦ x + 42
-- Bool, 真偽値
#check true
-- 命題
#check True
型の型
「すべての」項には型があるので、型も型を持ちます。
-- 宇宙変数を宣言する
universe u
#check (Prop : Type)
-- Lean では `List` は Type を受け取って、Type を返す関数。
#check (List : (α : Type u) → Type u)
-- 配列も同じ。型を型に変換する関数。
#check (Array : (α : Type u) → Type u)
-- `Type` 自身も型を持っており…
#check (Type : Type 1)
#check (Type 1 : Type 2)
-- この調子で限りなく続く
#check (Type u : Type (u + 1))
命題と証明
Lean では命題やその証明にも型があります。命題の型は Prop
で、命題の項が証明になっています。逆に言えば、Lean ではある命題 P : Prop
を証明するということは、P
という型を持つ項 proof : P
を構成することと同じです。
#check (1 + 1 = 2 : Prop)
-- `1 + 1 = 2` の証明 `two_eq_add_one` を構成
theorem two_eq_add_one : 2 = 1 + 1 := by rfl
-- 証明の型が命題になっている
#check (two_eq_add_one : 2 = 1 + 1)
型としての True/False
True
は型としては一点集合であり、
False
は型としては空集合です。
-- `trivial : True` は `True` 型を持つ項
#check trivial
関数としての証明
命題 P → Q
の証明は、P → Q
という型を持つ項です。
つまり、P
の証明 h : P
に対して Q
の証明を返す関数です。
theorem tautology : True -> True := fun a ↦ a
-- 暗黙の変数を明示的にするために `@` を付けた。
-- `tautology : True → True` と出力されるので、
-- `tautology` は `True → True` という関数であることがわかる
#check (@tautology : True → True)
-- 実際に `trivial : True` を「代入」すると
-- `tautology trivial : True` となり、
-- 確かに `True` 型の項が得られていることがわかる。
#check (tautology trivial : True)