Lean4で証明する順序関係を和の形で表現する

これまで、`MyNat.le` を帰納的に定義し、反射律や推移律などの基本的な性質を証明してきました。今回は、この順序関係が「和」を使った形でも表現できることを証明します。教材には引き続き「ゼロから始めるLean言語入門 手を動かして学ぶ形式数学ライブラリ開発」です。

つまり、同値性を示します。

\( n \le m \iff \exists k,\ n + k = m \)

直感的には、「n が m 以下である」ということは「n に何か（0 以上の値）を足せば m になる」ということと同じです。この事実を Lean で証明していきます。

≤ から和の形へ（MyNat.le.dest）

まず、n ≤ m ならば ∃ k, n + k = m であることを証明します。`MyNat.le` はコンストラクタ `refl` と `step` を持つ帰納的な定義なので、`induction` タクティクで証明できます。

theorem MyNat.le.dest (h : n ≤ m) : ∃ k, n + k = m := by
  induction h with
  | refl => exists 0
  | @step l h ih =>
    -- h : n ≤ l
    -- ih : ∃ k, n + k = l
    -- ⊢ ∃ k, n + k = l + 1
    obtain ⟨ k, ih ⟩ := ih
    exists k + 1
    rw [← ih]
    -- h : n ≤ l
    -- k : MyNat
    -- ih : n + k = l
    -- ⊢ n + (k + 1) = n + k + 1
    ac_rfl

`refl` の場合は n = m なので、k = 0 とすれば n + 0 = m が成り立ちます。`exists 0` でこれを示します。

`step` の場合は、帰納法の仮定 ih として ∃ k, n + k = l が得られています。`obtain` でこの k を取り出し、ゴールの k として k + 1 を与えます。すると、ゴールは n + (k + 1) = l + 1 になります。ここで ih : n + k = l を使って l を n + k に書き換えると、ゴールは n + (k + 1) = n + k + 1 という、足し算の結合性だけで成り立つ式になるので、`ac_rfl` で証明が完了します。

和の形から ≤ へ（MyNat.le.intro）

逆方向、つまり ∃ k, n + k = m ならば n ≤ m であることを証明します。この証明のために、まず補題 `MyNat.le_add_right` を用意します。これは「n ≤ n + m」、つまり n に何かを足した値は常に n 以上であるという性質です。

theorem MyNat.le_add_right (n m : MyNat) : n ≤ n + m := by
  induction m with
  | zero => rfl
  | succ k ih =>
    -- ih : n ≤ n + k
    -- ⊢ n ≤ n + (k + 1)
    rw [show n + (k + 1) = (n + k) + 1 from by ac_rfl]
    exact MyNat.le_step ih

theorem MyNat.le.intro (h : n + k = m) : n ≤ m := by
  -- h : n + k = m ⊢ n ≤ n + k
  rw [← h]
  induction k with
  | zero => rfl
  | succ k ih =>
    -- ih : n + k = m → n ≤ n + k
    -- h : n + (k + 1) = m
    -- ⊢ n ≤ n + (k + 1)
    apply MyNat.le_add_right

`MyNat.le_add_right` は m についての帰納法で証明できます。m = 0 の場合は n = n + 0 なので `rfl` が使えます。m = k + 1 の場合は、n + (k + 1) を (n + k) + 1 に書き換えたうえで、帰納法の仮定 ih : n ≤ n + k に `MyNat.le_step` を適用すれば証明できます。

`MyNat.le.intro` では、まず仮定 h : n + k = m を使ってゴールを n ≤ n + k に書き換えます。この形は `MyNat.le_add_right` そのものなので、あとは `apply` で証明が完了します。

MyNat.le_iff_add でまとめる

ここまでの `MyNat.le.dest` と `MyNat.le.intro` を組み合わせれば、≤ と和の形が同値であることを示せます。

theorem MyNat.le_iff_add : n ≤ m ↔ ∃ k, n + k = m := by
  constructor <;> intro h
  · exact MyNat.le.dest h
  · obtain ⟨ k, hk ⟩ := h
    exact MyNat.le.intro hk

`constructor` で ↔ を両方向の → に分解し、それぞれ `MyNat.le.dest` と `MyNat.le.intro` を適用するだけで証明できます。

具体的な不等式の証明

和の形にできるようになると、具体的な値を与えることで不等式を直接証明できるようになります。

example : 1 ≤ 4 := by
  exact MyNat.le_iff_add.mpr ⟨ 3, rfl ⟩

1 ≤ 4 を示すには、1 + 3 = 4 という和の形の証明があればよく、これは `rfl` でそのまま成り立ちます。`MyNat.le_iff_add.mpr` にこの組を渡すことで、≤ の証明に変換できます。

リポジトリはこちらです。
https://github.com/ringring-creator/LearnLean