2024年3月23日

『Theorem Proving in Lean 4』読了

2024年2月から読み始めていた『Theorem Proving in Lean 4』の（非公式）日本語訳 ⧉を読み終えました。 Visual Studio CodeでLean 4の環境を整え、文章中のコード片を写経したり練習問題を解いたりしながら読みました。 ただし、タクティク関係の5章、6章、11章は他の章で出てきたときに必要に応じて読み、最後の12章はざっと目を通す程度に読みました。

以前Coqにも入門したことがありますが、タクティク（tactic）を使って前提やゴールを書き換えて証明を進める方法で、 どのタクティクでどの定理を使えば進められるのかが分からず難しかったです。 Lean 4でも同様にタクティクを使った証明もできますが、命題の型を持つ項を構成することでも証明でき、私にはこちらのほうが分かりやすく感じました。

例えば、任意の命題$P, Q$に対して$P \land Q \to Q \land P$が成り立つことの証明を、Lean 4では以下のように書くことができます。

example (P Q : Prop) : P ∧ Q → Q ∧ P :=
  fun (h : P ∧ Q) => And.intro h.right h.left

含意（「ならば」、$\mathbin\to$）が関数に対応し、含意の仮定が関数の引数になっています。 And.introは引数の2つの項からそれらの論理積の項を生成する関数です。 ここでは仮定の項$\mathtt{h} \colon P ∧ Q$から、その右の項$\mathtt{h.right} \colon Q$と左の項$\mathtt{h.left} \colon P$を取り出して、And.introに適用することで$Q ∧ P$型の項を生成しています。

このようにカリー＝ハワード対応に基づく命題と型・証明と項の関係がそのままコードに現れていることに感銘を受けました。