Lean 4 で injection タクティクを使いこなす

今回は順序関係の定義に進む前に、injection タクティクの応用例として m * n = 0 → m = 0 ∨ n = 0 という定理の証明に取り組みます。教材には引き続き「ゼロから始めるLean言語入門 手を動かして学ぶ形式数学ライブラリ開発」です。

injectionタクティクの復習

injection タクティクは、ペアノの公理が持つ次の性質を利用するタクティクでした。

• 異なる自然数に対する succ の結果は異なる
• 0 と succ の結果は必ず異なる

足し算に対する補題の証明

まずは m * n = 0 → m = 0 ∨ n = 0 の証明に使う準備として、足し算に対して m + n = 0 → m = 0 ∧ n = 0 が成り立つことを証明します。数学的帰納法を使い、仮定とゴールを次のように変形したところで injection を使用します。

ih : m + n = 0 → m = 0 ∧ n = 0
h : m + n + 1 = 0 
⊢ False

m + n + 1 = 0 は m + n + 1 = MyNat.succ (m + n) に簡約されるので、異なる自然数に対する succ の結果は異なるという性質を使って矛盾を示せます。

theorem MyNat.eq_zero_of_add_eq_zero : m + n = 0 → m = 0 ∧ n = 0 := by
  intro h
  induction n with
  | zero => -- h : m + 0 = 0 ⊢ m = 0 ∧ 0 = 0
    simp_all
  | succ n ih =>
    -- ih : m + n = 0 → m = 0 ∧ n = 0
    -- h : m + (n + 1) = 0
    -- ⊢ m = 0 ∧ n + 1 = 0
    exfalso -- ih : m + n = 0 → m = 0 ∧ n = 0 h : m + (n + 1) = 0 ⊢ False
    rw [show m + (n + 1) = m + n + 1 from by ac_rfl] at h
    injection h

逆向きの含意も証明し、両方向をあわせた同値な定理を simp に登録しておきます。

theorem MyNat.add_eq_zero_of_eq_zero : m = 0 ∧ n = 0 → m + n = 0 := by
  intro h
  simp_all

@[simp]
theorem MyNat.add_eq_zero_iff_eq_zero : m + n = 0 ↔ m = 0 ∧ n = 0 := by
  exact ⟨ MyNat.eq_zero_of_add_eq_zero, MyNat.add_eq_zero_of_eq_zero ⟩

m * n = 0 → m = 0 ∨ n = 0 の証明

ここからが本題です。m * n = 0 → m = 0 ∨ n = 0 を証明します。数学的帰納法で n が 0 の場合は自明なので simp_all で片付きます。n + 1 の場合は h : m * (n + 1) = 0 ⊢ m = 0 ∨ n + 1 = 0 を証明することになります。

まず distrib で分配法則を使い、m * (n + 1) = m * n + m に書き換えます。ゴールを見ると n + 1 = 0 は成り立たないので、m = 0 を示せばよいことがわかります。あとは simp_all によって m * n + m = 0 から m = 0 を導けるので、これで証明は完了です。

同値の証明としているので、自明な右から左への含意は simp_all で証明しています。

@[simp]
theorem MyNat.mul_eq_zero (m n : MyNat) : m * n = 0 ↔ m = 0 ∨ n = 0 := by
  constructor <;> intro h
  case mpr =>
    cases h <;> simp_all
  case mp =>
    induction n with
    | zero =>
      simp_all
    | succ n _ =>
    -- a✝ : m * n = 0 → m = 0 ∨ n = 0
    -- h : m * (n + 1) = 0
    -- ⊢ m = 0 ∨ n + 1 = 0
      have : m * n + m = 0 := calc
        _ = m * (n + 1) := by distrib
        _ = 0 := by rw [h]
      simp_all

コードは以下のリポジトリで公開しています。

https://github.com/ringring-creator/LearnLean