Leanにおける数学的帰納法

これまで MyNat 型に対して、定義から直接 rfl で示せる命題を扱ってきました。今回は、rfl だけでは証明できない命題に対して、Lean 4 における数学的帰納法の使い方を整理していきます。教材には引き続き「ゼロから始めるLean言語入門 手を動かして学ぶ形式数学ライブラリ開発」です。

rflで証明できる場合、できない場合

まず、次の命題は問題なく証明できます。

example (n : MyNat) : n + 0 = n := by
  rfl

ところが、左右を入れ替えただけに見える次の命題は、同じように rfl を使っても証明できません。

example (n : MyNat) : 0 + n = n := by
  rfl
-- Tactic `rfl` failed: The left-hand side
--   0 + n
-- is not definitionally equal to the right-hand side
--   n
-- n : MyNat
-- ⊢ 0 + n = n

見た目はほとんど同じ式なのに、なぜ片方は通って片方は通らないのでしょうか。これを理解するために、MyNat.add の定義を確認してみます。

なぜrflが通らないのか

MyNat.add は次のように定義されています。

def MyNat.add (m n : MyNat) : MyNat :=
  match n with
  | .zero => m
  | .succ n => succ (add m n)

ポイントは、match でパターンマッチしているのが第1引数 m ではなく、第2引数 n の方だという点です。

n + 0 の場合、add の第2引数が .zero なので、match はすぐに m（つまり n 自身）を返します。これは計算する前から構造的に決まっているため、rfl で簡約しきることができます。

一方 0 + n の場合、add の第2引数は n という変数です。n が .zero なのか .succ ... なのかは具体的な値が分からないと判定できないため、match をこれ以上展開できません。つまり rfl による単純な簡約だけでは、ゴールを n まで簡約しきれないのです。

実際に #reduce コマンドで両者を簡約してみると、この違いがはっきり表れます。

#reduce fun (n : MyNat) => n + 0
-- fun n => n

#reduce fun (n : MyNat) => 0 + n
-- fun n => (MyNat.rec ⟨MyNat.zero, PUnit.unit⟩
--   (fun n n_ih => ⟨MyNat.succ n_ih.1, n_ih⟩) n).1

n + 0 は n という単純な形に簡約されるのに対し、0 + n は MyNat.rec（再帰子）を使った複雑な式のまま残ってしまいます。これは n という変数自体が確定していないため、再帰的な構造をそれ以上崩せないことを表しています。

inductionタクティクによる数学的帰納法

rfl だけでは n が .succ のケースを処理できないので、ここで数学的帰納法の出番になります。Lean 4 では induction タクティクを使うことで、inductive キーワードで定義された型に対する帰納法を適用できます。

MyNat は zero と succ の2つのコンストラクタを持つ帰納型なので、induction タクティクを使うとゴールが次の2つのケースに分かれます。

• zero のケース：0 + MyNat.zero = MyNat.zero を示す
• succ n' のケース：「0 + n' = n'」という帰納法の仮定（ih）を使って、0 + n'.succ = n'.succ を示す

zero のケースは、0 + 0 が定義よりそのまま 0 に簡約されるので、これまで通り rfl で証明できます。

問題は succ n' のケースです。ここでは 0 + n'.succ という式を、(0 + n').succ という形に置き換えてから、帰納法の仮定 ih : 0 + n' = n' を使う、という手順を踏みます。この「置き換え」のために使うのが、MyNat.add の定義から直接示せる次の補題です。

theorem MyNat.add_succ (m n : MyNat) : m + .succ n = .succ (m + n) := by
  rfl

この add_succ 自体は MyNat.add の定義そのものなので、rfl で証明できます。これを rw タクティクで使うことで、succ のケースを ih が使える形に書き換えられるわけです。

証明全体の流れ

以上を踏まえると、0 + n = n の証明は次のようになります。

example (n : MyNat) : 0 + n = n := by
  induction n with
  | zero => rfl
  | succ n' ih =>
    -- ih : 0 + n' = n' ⊢ 0 + n'.succ = n'.succ
    rw [MyNat.add_succ] -- (0 + n').succ = n'.succ
    rw [ih] -- n'.succ = n'.succ

各ステップを順に確認してみます。

zeroのケース： ゴールは 0 + MyNat.zero = MyNat.zero です。MyNat.add の定義より、これは定義上そのまま成り立つので rfl で証明できます。

succのケース： 帰納法の仮定として ih : 0 + n' = n' が与えられ、ゴールは 0 + n'.succ = n'.succ になります。

まず rw [MyNat.add_succ] によって、ゴールの左辺 0 + n'.succ が (0 + n').succ に書き換えられます。これでゴールは (0 + n').succ = n'.succ になります。

次に rw [ih] によって、ih（0 + n' = n'）を使ってゴール中の 0 + n' を n' に置き換えます。すると、ゴールは n'.succ = n'.succ という自明な形になり、rw タクティクが自動的にこれを rfl で閉じてくれます。

まとめ

今回は、n + 0 = n は rfl で証明できるのに 0 + n = n は証明できない、という一見不思議な現象をきっかけに、MyNat.add の定義（第2引数でのパターンマッチ）と、induction タクティクによる数学的帰納法の使い方を学びました。

定義の構造によって rfl が効く範囲が変わること、そして帰納法の仮定を使うために add_succ のような補題を経由して式を書き換えていくという流れは、今後より複雑な定理を証明していく上でも基本になりそうです。