Chapter 01: 命題論理と述語論理の形式証明

Lean では，命題は Prop という型の項として表されます． つまり P : Prop は「P は命題である」という意味です． そして，命題 P の証明は，型 P をもつ項 h : P として扱われます． このような項を，P の証明，あるいは証明項と呼びます． この見方は「命題を型，証明を項として見る」考え方で，Curry--Howard 対応あるいは propositions-as-types（命題＝型対応）と呼ばれます． 証明項 h : P を作ることと，命題 P を証明することは同じことであり，Lean の型検査器が証明の正しさを保証します． つまり，Lean における形式証明では「正しい証明であること」を，最終的には「指定された型をもつ項が構成できていること」として確認します．

タクティックモードでは，Lean が現在の「ゴール」を表示し，ユーザは intro，exact，constructor，cases などのタクティックでゴールを変形していきます． 各タクティックは最終的に証明項を作るための補助であり，完成した証明は Lean の小さなカーネルによって再度型検査されます． 以下では，直観主義自然演繹でよく使う推論規則を 1 つずつ確認し，対応する Lean の書き方を見ます．