Lean4で整数MyIntを順序群にする

今回は MyInt が加法に関して可換な順序群であることを証明します。順序群であることを示しておくと、Mathlib が用意している順序に関する補題やタクティクを MyInt でもそのまま利用できるようになります。あわせて、比較演算 \( \le \) を計算可能にするための decidable インスタンス登録も行います。本記事は書籍ゼロから始めるLean言語入門 手を動かして学ぶ形式数学ライブラリ開発を参考に進めています。

順序群とは

順序群とは、順序が定義されていて、演算がその順序を保つ群のことです。具体的には、次の2つの性質を満たします。

\( \forall x, y, z \in X,\ x \le y \to x + z \le y + z \)

\( \forall x, y, z \in X,\ x \le y \to z + x \le z + y \)

MyIntが順序群であることの証明

まずは1つ目の性質にあたる add_le_add_left を証明します。

theorem MyInt.add_le_add_left (a b : MyInt) (h : a ≤ b) (c : MyInt)
  : a + c ≤ b + c := by
  notation_simp at *
  obtain ⟨m, hm⟩ := h
  use m
  -- hm : a + ↑m = b
  -- ⊢ a + c + ↑m = b + c
  have : a + c + ↑m = b + c := calc
    _ = c + (a + ↑m) := by ac_rfl
    _ = c + b := by rw [hm]
    _ = b + c := by ac_rfl
  assumption

a ≤ b の定義を展開すると、b = a + m となる自然数 m の存在に帰着します。あとは ac_rfl で加法の可換性・結合性を使って項を並べ替えれば証明できます。

この性質を Mathlib 側で使えるようにするため、IsOrderedAddMonoid のインスタンスとして登録します。

instance : IsOrderedAddMonoid MyInt where
  add_le_add_left := MyInt.add_le_add_left

比較演算を計算可能にする

ここまでで順序群であることは示せましたが、このままでは ≤ は命題として存在するだけで、実際に計算して真偽を確かめることはできません。decide タクティクや #eval で扱えるようにするには、Decidable インスタンスを登録する必要があります。

方針は MyNat のときと同じで、n ≤ m の決定可能性を 0 ≤ m - n の決定可能性に帰着させます。そのための補題として、まず 0 ≤ n の決定可能性を示します。

最初に 0 ≤ n を計算する関数 bpos を用意します。

-- n1 - n2 ≥ 0
def PreInt.bpos (n : PreInt) : Bool :=
  match n with
  | (n1, n2) => decide (n2 ≤ n1)

-- n1 - n2 ≥ 0 for MyInt
def MyInt.bpos : MyInt → Bool := Quotient.lift PreInt.bpos <| by
  intro (a1, a2) (b1, b2) hr
  notation_simp at hr
  -- hr : a1 + b2 = a2 + b1
  -- ⊢ PreInt.bpos (a1, a2) = PreInt.bpos (b1, b2)
  dsimp [PreInt.bpos]
  -- ⊢ PreInt.bpos (a1, a2) = PreInt.bpos (b1, b2)
  suffices a2 ≤ a1 ↔ b2 ≤ b1 from by
    simp_all
  constructor <;> intro h
  case mp =>
    have : a1 + b2 ≤ a1 + b1 := calc
      _ = a2 + b1 := by rw [hr]
      _ ≤ a1 + b1 := by compatible
    simp at this
    assumption
  case mpr =>
    have : a2 + b1 ≤ a1 + b1 := calc
      _ = a1 + b2 := by rw [hr]
      _ ≤ a1 + b1 := by compatible
    simp at this
    assumption

@[simp]
theorem MyInt.bpos_def (m n : MyNat) : MyInt.bpos (⟦(m, n)⟧) = true ↔ n ≤ m := by
  dsimp [MyInt.bpos, PreInt.bpos]
  simp

MyInt.bpos は商型 MyInt 上の関数なので、Quotient.lift を使って well-defined であることを示しながら定義しています。代表元の取り方によらず結果が変わらないことを、同値関係 hr をもとに確認しています。

次に、MyInt.bpos z = true ↔ 0 ≤ z を証明するために必要な補題を順に用意します。

@[norm_cast]
theorem MyInt.ofMyNat_le (m n : MyNat) : (m : MyInt) ≤ (n : MyInt) ↔ m ≤ n := by
  rw [MyNat.le_iff_add]
  notation_simp
  constructor <;> intro ⟨k, hk⟩
  case mp =>
    use k
    have : ↑(m + k) = (n : MyInt) := by
      norm_cast at hk
    norm_cast at *
  case mpr =>
    use k
    rw [← hk]
    norm_cast

theorem MyInt.le_sub_iff (x y z : MyInt) : z ≤ x - y ↔ z + y ≤ x := by
  notation_simp
  constructor <;> intro ⟨k, hk⟩
  case mp =>
    use k
    have : z + y + ↑k = x := calc
      _ = z + ↑k + y := by ac_rfl
      _ = (x - y) + y := by simp [hk]
      _ = x := by abel
    assumption
  case mpr =>
    use k
    have : z + ↑k = x - y:= calc
      _ = (z + y + ↑k) - y := by abel
      _ = x - y := by rw [hk]
    assumption

theorem MyInt.sub_nonneg (m n : MyInt) : 0 ≤ m - n ↔ n ≤ m := by
  have := MyInt.le_sub_iff m n 0
  simp_all

ofMyNat_le は MyNat の順序が MyInt への埋め込みで保存されることを示す補題、le_sub_iff と sub_nonneg は不等式を引き算の形に変形するための補題です。これらを組み合わせることで目的の定理を証明します。

theorem MyInt.bpos_iff (z : MyInt) : MyInt.bpos z = true ↔ 0 ≤ z := by
  induction z using Quotient.inductionOn with
  | h a =>
    obtain ⟨x, y⟩ := a
    rw [MyInt.bpos_def, MyInt.mk_def]
    rw [MyInt.sub_nonneg]
    norm_cast

induction z using Quotient.inductionOn with により、商型の元 \( z \in \text{MyInt} \) に関する主張が、同値類の中身である代表元 \( a \in \text{MyNat} \times \text{MyNat} \) に関する主張に置き換わります。あとは用意しておいた補題を並べて適用するだけです。

ここまでの決定可能性を DecidablePred に登録し、decide タクティクを使えるようにします。

instance : DecidablePred (0 ≤ · : MyInt → Prop) := by
  intro n
  apply decidable_of_iff (MyInt.bpos n = true)
  exact MyInt.bpos_iff n

example : 0 ≤ (3 : MyInt) := by
  decide

n ≤ m の決定可能性も DecidableLE に登録します。

instance : DecidableLE MyInt := by
  intro n m
  apply decidable_of_iff (0 ≤ m - n)
  exact MyInt.sub_nonneg m n

#eval で評価できるようになり、decide タクティクも使えるようになったことが確認できます。

#eval (3 : MyInt) ≤ 4

example : (3 : MyInt) ≤ 4 := by
  decide

狭義順序についても同様に登録します。infer_instance は「すでにシステムが知っている型クラスのインスタンスでこのゴールを解決せよ」という指示です。dsimp による変換で n m : MyInt ⊢ Decidable (n ≤ m ∧ ¬m ≤ n) という形になるので、あとは登録済みの広義順序の Decidable インスタンスで解決できます。

instance : DecidableLT MyInt := by
  intro n m
  dsimp [(· < ·), MyInt.lt]
  infer_instance

#eval (3 : MyInt) < 4

example : (3 : MyInt) < 4 := by
  decide

最後に等号についてもインスタンスを登録します。x = y ↔ x ≤ y ∧ y ≤ x という関係を利用すれば、既存の DecidableLE から計算できます。

instance : DecidableEq MyInt := decidableEqOfDecidableLE

#eval (3 : MyInt) = 4

example : ¬ (3 : MyInt) = 4 := by
  decide

これで MyInt は順序群として扱えるようになり、比較演算もすべて計算可能になりました。コードは以下のリポジトリにまとめています。

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