Lean 4で自然数を作る 順序の反対称律を証明する

今回は順序の反対称律 \( a \le b \to b \le a \to a = b \) を証明します。まずは狭義順序と広義順序が混在した推移律、そして狭義順序の非反射律という2つの補助的な性質を先に整えてから、本題の反対称律に取り組みます。教材には引き続き「ゼロから始めるLean言語入門 手を動かして学ぶ形式数学ライブラリ開発」です。

狭義順序と広義順序が混在した推移律

これまでに \( n < m \) と \( m < k \) から \( n < k \) を導く推移律は証明済みでしたが、\( \le \) と \( < \) が混在するパターン、たとえば \( n \le m \) と \( m < k \) から \( n < k \) を導くようなケースはまだ扱っていませんでした。calcブロックで \( \le \) と \( < \) を自由に繋げるためには、この組み合わせごとに推移律を用意しておく必要があります。

variable {n m k : MyNat}

theorem MyNat.lt_trans (h1 : n < m) (h2 : m < k) : n < k := by
  notation_simp at *
  -- h1 : n + 1 ≤ m
  -- h2 : m + 1 ≤ k
  -- ⊢ n + 1 ≤ k
  have : n + 1 ≤ k := calc
    _ ≤ m := by exact h1
    _ ≤ m + 1 := by simp
    _ ≤ k := by exact h2
  assumption

theorem MyNat.lt_of_le_of_lt (h1 : n ≤ m) (h2 : m < k) : n < k := by
  notation_simp at *
  -- h1 : n ≤ m
  -- h2 : m + 1 ≤ k
  -- ⊢ n + 1 ≤ k
  have : n + 1 ≤ k := calc
    _ ≤ m + 1 := by compatible
    _ ≤ k := by exact h2
  assumption

theorem MyNat.lt_of_lt_of_le (h1 : n < m) (h2 : m ≤ k) : n < k := by
  notation_simp at *
  -- h2 : m ≤ k
  -- h1 : n + 1 ≤ m
  -- ⊢ n + 1 ≤ k
  have : n + 1 ≤ k := calc
    _ ≤ m := by exact h1
    _ ≤ k := by exact h2
  assumption

instance : Trans (· < · : MyNat → MyNat → Prop) (· < ·) (· < ·) where
  trans := MyNat.lt_trans

instance : Trans (· ≤ · : MyNat → MyNat → Prop) (· < ·) (· < ·) where
  trans := MyNat.lt_of_le_of_lt

instance : Trans (· < · : MyNat → MyNat → Prop) (· ≤  ·) (· < ·) where
  trans := MyNat.lt_of_lt_of_le

lt_transでは、notation_simpによって \( < \) が \( \le \) の定義に展開されるため、ゴールは \( n + 1 \le k \) になります。ここから \( m \le m + 1 \) という1ステップ分の余裕を挟むことで、h1 : n + 1 \le mとh2 : m + 1 \le kをうまく繋げています。lt_of_le_of_ltとlt_of_lt_of_leも同様の方針で、片方の仮定を1つずらしてから残りを合成する形になっています。

最後に3つのTransインスタンスを登録することで、calcブロックの中で \( \le \) と \( < \) を自由に混在させて繋げられるようになります。

狭義順序の非反射律

非反射律とは、どんな要素も自分自身とは関係を持たないという性質です。狭義順序でいえば、どんな数 \( n \) についても \( n < n \) は成り立たない、ということになります。今回の反対称律の証明では、最終的に \( n < n \) という矛盾した状況を作り出すことで結論を導くため、この非反射律が鍵になります。

@[simp]
theorem MyNat.lt_irrefl (n : MyNat) : ¬ n < n := by
  intro h
  notation_simp at h
  rw [MyNat.le_iff_add] at *
  obtain ⟨k, hk⟩ := h
  -- hk : n + 1 + k = n ⊢ False
  have : n + (k + 1) = n := calc
    _ = n + 1 + k := by ac_rfl
    _ = n := by rw [hk]
  simp_all

まずn < nを仮定として取り込み、notation_simpで \( n + 1 \le n \) に、さらにMyNat.le_iff_addで \( \exists k,\ n + 1 + k = n \) の形に変換します。得られたhkを使って \( n + (k + 1) = n \) を作ると、これは MyNat.add_right_cancel 相当の仕組みによって \( k + 1 = 0 \) を意味することになり、simp_allが \( k + 1 = 0 \) は成り立たないという事実からFalseを導いてくれます。

順序の反対称律

補助的な性質が揃ったので、いよいよ本題の反対称律 \( n \le m \to m \le n \to n = m \) を証明します。

theorem MyNat.le_antisymm (h1: n ≤ m) (h2: m ≤ n) : n = m := by
  induction h1 with
  | refl => rfl
  | @step m h ih =>
    -- h : n ≤ m
    -- ih : m ≤ n → n = m
    -- h2 : m + 1 ≤ n
    -- ⊢ n = m + 1
    have : n < n := calc
      _ ≤ m := by exact h
      _ < m + 1 := by notation_simp; rfl
      _ ≤ n := by exact h2
    simp at this

h1 : n ≤ mはMyNat.leの帰納的な定義そのものに対する帰納法で扱えます。reflケースは \( n = n \) なのでrflで即座に終わります。stepケースでは \( n \le m \) から1つ進んだ \( n \le m + 1 \) が新しいゴールになり、そのときの仮定として \( h : n \le m \) と \( h2 : m + 1 \le n \) が使えます。

ここでcalcを使い、\( n \le m \)、\( m < m + 1 \)、\( m + 1 \le n \) を順につなげると \( n < n \) が得られます。これは先ほど示した非反射律に反する主張なので、simpがこの矛盾を検出してゴールを閉じてくれます。

混在した推移律と非反射律という2つの補助定理を先に整えておいたことで、反対称律の証明自体は「\( n < n \) を作って矛盾を導く」というシンプルな流れにまとめることができました。

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