証明項としての証明¶
命題 P : Prop は型であり，その証明は型 P の項です．
言い換えると，P : Prop は命題そのもの，hP : P は命題 P の証明，あるいは証明項です．
そのため，すでに hP : P を持っていれば，hP そのものが P の証明です．
含意 P → Q の証明は，P の証明を受け取って Q の証明を返す関数です．
したがって，fun hP => ... という関数として書けます．
全称命題 ∀ x : α, P x も，同じく入力 x に応じて証明 P x を返す依存関数です．
example (P Q : Prop) (hQ : Q) : P → Q :=
fun _hP => hQ
example (P : Nat → Prop) (h : ∀ n : Nat, P n) : P 0 :=
h 0
structure や inductive 型の命題は，constructor を使って証明項を作ります．
連言 P ∧ Q は And P Q という structure なので，And.intro hP hQ で証明できます．
山括弧 ⟨...⟩ は，constructor 名を省略して値や証明を作る notation です．
example (P Q : Prop) (hP : P) (hQ : Q) : P ∧ Q :=
And.intro hP hQ
example (P Q : Prop) (hP : P) (hQ : Q) : P ∧ Q :=
⟨hP, hQ⟩
example (P Q : Prop) (hP : P) : P ∨ Q :=
Or.inl hP
example : ∃ n : Nat, n + 2 = 5 :=
Exists.intro 3 rfl
example : ∃ n : Nat, n + 2 = 5 :=
⟨3, rfl⟩
等式 a = b は Eq a b という inductive 型です．
反射律 Eq.refl a は a = a の証明項です．
Lean は両辺を計算・定義展開して同じ式になる場合にも，Eq.refl や rfl を使えます．
#check Eq
#check Eq.refl
example : Eq 3 3 :=
Eq.refl 3
example : (fun n : Nat => n + 1) 2 = 3 :=
Eq.refl 3
証明を書いている途中では，未完成の証明項として sorry を一時的に置けます．
sorry はどんな型の項も仮に作ったことにしますが，Lean はその宣言に warning を出します．
したがって，演習問題や作業中の証明では便利ですが，完成した定義や定理には残さないものです．
このコードは型検査自体は通りますが，「この宣言は sorry を使っている」という警告が残ります．
sorry は証明探索の道具ではなく，あとで証明項に置き換えるべき穴です．
演習¶
fun や constructor を使って，次の証明項を tactic モードなしで書いてください．