述語論理¶
述語論理では，命題変数だけでなく，対象の型 α : Type と，その対象に依存する命題
P : α → Prop を扱います．
P a は「対象 a : α が性質 P を満たす」という命題です．
Lean の ∀ x : α, P x は，依存関数型，つまり「各 x : α に対して P x の証明を返す関数型」です．
そのため，全称命題の証明 h : ∀ x : α, P x は，関数のように具体的な項 a : α に適用して h a : P a を得ます．
一方，∃ x : α, P x は，証拠（witness） x : α とその証拠が性質を満たす証明 P x の組です．
全称導入 ∀ introduction¶
∀ x : α, Q x を証明するには，任意の x : α を 1 つ取って Q x を証明します．
Lean では intro x により，全称量化された変数を仮定として導入します．
ここで重要なのは，導入した x は特別な性質を仮定していない「任意の」対象だという点です．
自然演繹では，この条件を固有変数条件と呼びます．
証明図:
具体例: 「任意の実数 \(x\) について \(x^2 \ge 0\)」を示すには，特別な性質を仮定しない任意の実数 \(x\) を 1 つ取り，その \(x\) について \(x^2 \ge 0\) を示します．
example (α : Type) (P Q : α → Prop)
(hPQ : ∀ x : α, P x → Q x) (hP : ∀ x : α, P x) :
∀ x : α, Q x := by
intro x
exact hPQ x (hP x)
全称除去 ∀ elimination¶
h : ∀ x : α, P x があるなら，具体的な a : α に代入して h a : P a を得られます．
Lean では，全称命題の証明を関数のように適用します．
これは Curry--Howard 対応のもとで，全称量化が依存関数型として扱われていることの現れです．
証明図:
具体例: 「任意の実数 \(x\) について \(x^2 \ge 0\)」が分かっていれば，具体的な実数 \(a\) に代入して「\(a^2 \ge 0\)」を得られます．
存在導入 ∃ introduction¶
∃ x : α, P x を証明するには，具体的な証拠 a : α と，その証拠が性質を満たす証明 ha : P a を与えます．
Lean では Exists.intro a ha と書けます．
証明図:
具体例: 「\(2\) は偶数である」と分かっていれば，証拠として \(2\) を与えることで「偶数が存在する」と証明できます．
example (α : Type) (P : α → Prop) (a : α) (ha : P a) : ∃ x : α, P x := by
exact Exists.intro a ha
example (α : Type) (P : α → Prop) (a : α) (ha : P a) : ∃ x : α, P x := by
exists a
存在除去 ∃ elimination¶
hExists : ∃ x : α, P x から結論を得るには，証拠 x と証明 hx : P x を取り出し，そのもとで結論を示します．
Lean では cases hExists with で存在命題を分解できます．
取り出した証拠の名前はその枝の中だけで使える局所的な名前です．
したがって，結論そのものはその名前に依存してはいけません．
これも自然演繹では固有変数条件として表されます．
証明図:
具体例: 「正の実数が存在する」と分かっていて，さらに任意の正の実数 \(x\) から \(x^2 > 0\) が従うなら，存在する証拠を 1 つ取り出して「平方が正である実数が存在する」と結論できます．
example (α : Type) (P Q : α → Prop)
(hExists : ∃ x : α, P x) (hPQ : ∀ x : α, P x → Q x) :
∃ x : α, Q x := by
cases hExists with
| intro x hx =>
exact Exists.intro x (hPQ x hx)
全称と連言の組み合わせ¶
量化子と命題論理の規則は組み合わせて使います．
たとえば，すべての x について P x ∧ Q x が成り立つなら，すべての x について P x が成り立ち，すべての x について Q x が成り立ちます．
この例の証明図:
Lean のコードでは，constructor で連言の 2 つの成分を別々に証明します．
それぞれの枝で intro x により任意の x を導入し，h x : P x ∧ Q x から .left または .right で必要な成分を取り出します．
具体例: 集合 \(A\) のすべての元が「有理数であり，かつ正である」と分かっているなら，「すべての元が有理数である」と「すべての元が正である」を別々に取り出せます．
example (α : Type) (P Q : α → Prop) (h : ∀ x : α, P x ∧ Q x) :
(∀ x : α, P x) ∧ (∀ x : α, Q x) := by
constructor
· intro x
exact (h x).left
· intro x
exact (h x).right
存在と選言の組み合わせ¶
存在命題を使う証明では，まず証拠を取り出してから，命題論理の規則を適用することがよくあります．
次の例では，∃ x, P x と ∀ x, P x → Q x ∨ R x から，∃ x, Q x ∨ R x を示します．
この例の証明図:
存在除去で得た局所的な証拠 x は，そのまま結論の存在命題の証拠として再利用できます．
このとき外に出しているのは局所変数そのものではなく，Exists.intro x ... で包み直した存在命題の証明です．
具体例: ある整数 \(n\) が存在し，任意の整数は偶数または奇数であると分かっているなら，証拠 \(n\) を取り出して「偶数または奇数である整数が存在する」と結論できます．
example (α : Type) (P Q R : α → Prop)
(hExists : ∃ x : α, P x) (hPQR : ∀ x : α, P x → Q x ∨ R x) :
∃ x : α, Q x ∨ R x := by
cases hExists with
| intro x hx =>
exact Exists.intro x (hPQR x hx)
等号導入 = introduction¶
等号つきの述語論理では，任意の項は自分自身に等しいです．
Lean では反射律を rfl で証明します．
rfl は単に文字列として同じ式だけでなく，定義展開や計算によって同じ式になる等式も閉じられます．
このような同一性を定義的に等しい（definitionally equal）と呼びます．
証明図:
具体例: 任意の数 \(a\) について，\(a = a\) は反射律により成り立ちます．
等号除去: 置換¶
hEq : a = b があり，ha : P a があるなら，等しいものは同じ性質を満たすので P b が得られます．
Lean では hEq ▸ ha により，ha の型に現れる a を b に置き換えます．
反対向きに置換したいときは，等式を逆向きに使います．
たとえば ← hEq は b を a に戻す向きの等式として使えます．
証明図:
具体例: \(a = b\) と \(a > 0\) が分かっていれば，等しいものは同じ性質を持つので \(b > 0\) と結論できます．
等号除去: 書き換え¶
等式はゴールの書き換えにも使えます．
rw [hEq] は，ゴール中の左辺を右辺に書き換えます．
仮定を書き換える場合は rw [hEq] at h のように書きます．
反対向きに書き換える場合は rw [← hEq] を使います．
次の例では，ゴール f a = f b の左辺に現れる a を b に書き換えることで，f b = f b になり，反射律で閉じられます．
証明図:
具体例: \(a = b\) が分かっていれば，同じ関数 \(f\) を両辺に適用して \(f(a) = f(b)\) と書き換えられます． たとえば \(a = b\) から \(\sin a = \sin b\) が従います．