Lean における証明のヒント

今回は、Lean 4 の証明を楽にするためのタクティクスをいくつか学んでいきます。教材には引き続き「ゼロから始めるLean言語入門 手を動かして学ぶ形式数学ライブラリ開発」です。

証明が少し複雑になってくると、ゴールを段階的に整理したり、使いたい補題の名前を素早く調べたりできると便利です。have、suffices、exact?、show ... from by の 4 つを、具体的なコード例を通して確認していきます。

have タクティクス ― ローカル補題の宣言

have タクティクスを使うと、証明の途中でローカルな補題を宣言し、以降のゴールで名前を使って参照することができます。次の例では ¬¬¬P → ¬P を証明する過程で、途中に ¬¬P という補題をローカルに示しています。

example (P : Prop) : ¬¬¬ P → ¬ P := by
  intro hn3p -- ¬¬¬ P
  intro hp   -- P ⊢ False

  -- ローカルで使用する補題を示す
  have hn2p : ¬¬ P := by
    intro hnp -- ¬ P → False
    contradiction -- hp と hnp が矛盾

  exact hn3p hn2p

have 名前 : 型 := by の形で補題を宣言し、by ブロック内でその証明を与えます。示した補題は宣言以降の証明で名前を使って参照できるため、複雑な証明を小さなステップに分割して整理するのに役立ちます。

suffices タクティクス ― 「〜を示せば十分」という証明

suffices タクティクスは、「〜を示せば元のゴールが証明できる」という論法を記述するためのものです。元のゴールを直接攻めるのが難しい場合に、より扱いやすい命題を経由して証明を進めることができます。

example (P : Prop) : ¬¬ (P ∨ ¬P) := by
  intro h -- ¬ (P ∨ ¬P) ⊢ False
  -- ¬ P を示せば十分である
  suffices hyp : ¬ P from by
    -- ¬ P から元のゴールを導く
    have : P ∨ ¬ P := by
      right
      exact hyp
    exact h this

  guard_target =ₛ ¬ P

  intro hq -- P
  have : P ∨ ¬ P := by
    left
    exact hq
  contradiction

suffices hyp : ¬ P from by ... と書くと、まず from by 以降で「¬ P があれば元のゴールが証明できること」を示し、そのあとに ¬ P そのものを証明するという 2 段階の構造になります。

exact? タクティクス ― ライブラリから証明項を検索

exact? は、インポートされているライブラリやローカルの定義の中から、現在のゴールに合致する証明項を自動的に検索してくれるタクティクスです。候補が見つかると Try this: として提案が表示されます。

example (P : Prop) : (P → True) ↔ True := by
  exact?
  -- Try this:
  -- [apply] exact imp_true_iff P

Mathlib のような大規模なライブラリを使っていると、目的の定理が存在するはずだとわかっていても名前を知らないことがよくあります。そういった場面で exact? を使えば、自分でドキュメントを検索しなくても候補を提案してもらえるので非常に便利です。

show ... from by ― 使い捨ての補題をインラインで

show P from by *** を使うと、一時的な補題を名前をつけずにインラインで宣言しながら証明することができます。have との使い分けの目安は参照する回数で、補題を一度しか使わない場合は show ... from by の方がすっきりした書き方になります。

次の例では、rw が (P → False) ↔ ¬ P という書き換えを一度だけ利用しており、show ... from by が適している場面です。

example (P Q : Prop) (h : ¬ P ↔ Q) : (P → False) ↔ Q := by
  rw [show (P → False) ↔ ¬ P from by rfl]
  rw [h]