Lean4で整数MyIntの半順序を証明する

今回は、これまで構築してきたMyIntに半順序（partial order）の性質を証明していきます。参考書籍は引き続きゼロから始めるLean言語入門 手を動かして学ぶ形式数学ライブラリ開発です。

半順序とは

集合Xの二項関係が以下を満たすとき、その関係を半順序と呼びます。

• Xに対して前順序集合であること
• 反対称性を満たすこと：\( \forall x, y \in X,\ x \le y \land y \le x \to x = y \)

前回までに\( \le \)の反射律と推移律（前順序）は証明済みなので、今回は反対称性の証明に取り組みます。

反対称性の証明のための補題

まずは補題を用意します。a + b = aであればb = 0であるという主張です。

@[simp ↓]
theorem MyInt.add_right_eq_self {a b : MyInt} : a + b = a ↔ b = 0 := by
  constructor <;> intro h
  case mp => calc
    -- h : a + b = a ⊢ b = 0
    _ = b := by rfl
    _ = a + b - a := by abel
    _ = a - a := by rw [h]
    _ = 0 := by abel
  case mpr => simp [h]

mp方向はcalcでbをa + b - aに読み替え、仮定hでaをa + bに置き換えてからabelで整理し、最終的に0を導きます。mpr方向は仮定を代入するだけなのでsimp一発です。@[simp ↓]属性を付けているので、以降simpタクティク内で自動的に使われるようになります。

反対称性の証明

本題の反対称性です。a ≤ bとb ≤ aからa = bを導きます。≤の定義は自然数の差分で表現されているので、notation_simpで展開してからobtainで証拠を取り出します。

theorem MyInt.le_antisymm (a b : MyInt) (h1: a ≤ b) (h2: b ≤ a) : a = b := by
  notation_simp at *
  obtain ⟨m, hm⟩ := h1
  obtain ⟨n, hn⟩ := h2
  -- hm : a + ↑m = b
  -- hn : b + ↑n = a
  -- ⊢ a = b
  have : a + (↑m + ↑n) = a := calc
    _ = a + ↑m + ↑n := by ac_rfl
    _ = b + ↑n := by rw [hm]
    _ = a := by rw[hn]

  replace : ↑(m + n) = (0 : MyInt) := by
    push_cast
    simp_all

  have : m = 0 ∧ n = 0 := by
    simp_all
  simp_all

流れとしては、まずhmとhnを使ってa + (↑m + ↑n) = aという等式を組み立てます。ac_rflで結合律・可換律の書き換えを行い、hm・hnで順に置き換えていくだけです。

この等式に先ほどの補題を適用すると↑m + ↑n = 0、つまり↑(m + n) = 0が得られます。replaceはhaveと同じ使い方をしますが、既存のthisを上書きする点が異なります。ここでは直前のhaveで作ったthisを、push_castとsimp_allによってMyNatの等式に変換したものへ置き換えています。

自然数の和が0になるのは両方とも0のときだけなので、m = 0 ∧ n = 0が言えます。あとはsimp_allでhmに代入すればa = bが得られ、証明完了です。

PartialOrderへの登録

最後にPartialOrderインスタンスへ登録します。前順序の部分はすでに登録済みなので、le_antisymmだけを追加すれば十分です。

instance : PartialOrder MyInt where
  le_antisymm := by apply MyInt.le_antisymm

example (a b : MyInt) (h1: a ≤ b) (h2: b ≤ a) : a = b := by
  order

登録が完了すると、orderタクティクが使えるようになります。orderは前順序・半順序・線形順序などの構造情報を自動で利用して順序に関するゴールを解決してくれるタクティクなので、今後の証明を大幅に簡略化できます。

コードの全体はGitHubリポジトリで公開しています。