Lean4で証明する自作の自然数における順序関係の定義と基本性質

今回は、自作した自然数型 MyNat に対して順序関係 ≤ を定義し、その基本的な性質である反射律と推移律を証明していきます。教材には引き続き「ゼロから始めるLean言語入門 手を動かして学ぶ形式数学ライブラリ開発」です。

順序関係の定義

順序関係も自然数そのものの定義と同様に、inductive キーワードを使って帰納的に定義します。まず反射律として、任意の自然数 n に対して n ≤ n が成り立つことを宣言します。次に、すでに n ≤ m が成り立っているならば n ≤ m + 1 も成り立つことを宣言します。この step コンストラクタを再帰的に適用していくことで、任意の m にたどり着けるようになっています。

inductive MyNat.le (n : MyNat) : MyNat → Prop
  -- ∀ n, n ≤ n
  | refl : MyNat.le n n
  -- n ≤ m → n ≤ m + 1
  | step {m : MyNat} : MyNat.le n m → MyNat.le n (m + 1)

-- use ≤ as MyNat.le
instance : LE MyNat where
  le := MyNat.le

反射律の証明

反射律は順序関係の定義そのものなので、証明は非常に単純です。

theorem MyNat.le_refl (n : MyNat) : n ≤ n := by
  exact MyNat.le.refl

推移律の証明

続いて、n ≤ m かつ m ≤ k ならば n ≤ k が成り立つという推移律を証明します。証明の方針としては、hmk : m ≤ k の証明構造そのものに対して帰納法を適用します。

refl ケース(k = m の場合)では、前提の hnm : n ≤ m がそのまま n ≤ k として使えます。step ケースでは、1段階手前まで n ≤ k が成り立っているという帰納法の仮定 ih が得られているので、MyNat.le.step を1回適用するだけの補題 MyNat.le_step を使って n ≤ k から n ≤ k + 1 を導きます。

このように、hnm を土台として、hmk に含まれる step の回数だけ n ≤ _ を段階的に伸ばしていくことで、最終的に n ≤ k が得られる、という流れになっています。

-- transitivity
variable {m n k : MyNat}

theorem MyNat.le_step (h : n ≤ m) : n ≤ m + 1 := by
  apply MyNat.le.step
  exact h

theorem MyNat.le_trans (hnm : n ≤ m) (hmk : m ≤ k) : n ≤ k := by
  induction hmk with
  | refl =>
    -- hnm : n ≤ m
    -- ⊢ n ≤ m
    exact hnm
  | @step k hmk ih =>
    -- hnm : n ≤ m
    -- k : MyNat
    -- hmk : m ≤ k
    -- ih : n ≤ k
    -- ⊢ n ≤ k + 1
    exact MyNat.le_step ih

なお、@step のように @ を付けることで、暗黙引数を含めたすべての引数に明示的に名前を付けられるようにしています。今回の場合、step ケースで生成される暗黙引数の k にも k という名前でアクセスできるようになっています。

属性の付与

最後に、証明した定理をタクティクから利用しやすくするために属性を付与していきます。反射律には [refl] 属性を付与することで、rfl や関連するタクティクから自動的に利用できるようになります。

attribute [refl] MyNat.le_refl

theorem MyNat.le_add_one_right (n : MyNat) : n ≤ n + 1 := by
  apply MyNat.le_step
  rfl

推移律については、Trans 型クラスのインスタンスとして登録することで、calc ブロックなどで ≤ を使った推移的な計算を自動的に扱えるようになります。

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

theorem MyNat.le_add_one_left (n : MyNat) : n ≤ 1 + n := calc
  _ ≤  n + 1 := by apply le_add_one_right
  _ = 1 + n := by ac_rfl

最後に、simp タクティクの中でも自動的に使用できるように [simp] 属性も付与しておきます。

attribute [simp] MyNat.le_refl MyNat.le_add_one_right MyNat.le_add_one_left

コードはこちらのリポジトリにまとめています。
https://github.com/ringring-creator/LearnLean