#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)