Lean4で自然数 MyNatから整数MyIntを構成する

いよいよ、これまで学んできた商（Quotient）とMyNatを使って、整数を構成していきます。

まず自然数と整数を見比べてみると、自然数は 0, 1, 2, ... と続くのに対し、整数は ..., -1, 0, 1, ... と負の数を含みます。この違いを生み出しているのは引き算です。今回は、MyNatのペアを使って引き算を表現することで、整数を構成していきます。本記事は「ゼロから始めるLean言語入門 手を動かして学ぶ形式数学ライブラリ開発」を参考にしています。

PreIntの定義

整数は、MyNatのペア (a, b) を \( a - b \) と解釈することで表現します。まずはこのペアの型を PreInt として定義します。

abbrev PreInt := MyNat × MyNat

abbrev キーワードで宣言することで、PreInt はインライン展開される扱いになり、MyNat が持つ性質（可換性や結合性など）をそのまま利用できます。

同値関係の定義

ここで問題になるのが、(0, 1) と (1, 2) がどちらも -1 に対応するといった重複です。\( (x_1, y_1) \) と \( (x_2, y_2) \) について \( x_1 - y_1 = x_2 - y_2 \) が成り立つとき、この2つを同値として扱いたいところですが、MyNat には引き算が定義されていません。そこで式を足し算に変形し、\( x_1 + y_2 = x_2 + y_1 \) の形で同値性を定義します。

def PreInt.r (m n : PreInt) : Prop :=
  match m, n with
  | (m1, m2), (n1, n2) => m1 + n2 = m2 + n1

同値関係の証明

PreInt.r が同値関係であること、すなわち反射律・対称律・推移律を満たすことを証明していきます。

theorem PreInt.r.refl : ∀ (m : PreInt), r m m := by
  intro (m1, m2)
  dsimp [r] -- ⊢ m1 + m2 = m2 + m1
  ac_rfl

反射律は m1 + m2 = m2 + m1 を示せばよく、加算の可換性から ac_rfl で解決できます。

theorem PreInt.r.symm : ∀ {m n : PreInt}, r m n → r n m := by
  intro (m1, m2) (n1, n2) h
  dsimp [r] at * -- h : m1 + n2 = m2 + n1 ⊢ n1 + m2 = n2 + m1

  have : n1 + m2 = n2 + m1 := calc
    _ = m2 + n1 := by ac_rfl
    _ = m1 + n2 := by rw [← h]
    _ = n2 + m1 := by ac_rfl
  exact this

対称律では、仮定 h を使って m2 + n1 と m1 + n2 を結び付け、calc で目標の等式まで変形しています。

theorem PreInt.r.trans : ∀ {l m n : PreInt}, r l m → r m n → r l n := by
  intro (l1, l2) (m1, m2) (n1, n2) hlm hmn
  dsimp [r] at *
  -- hlm : l1 + m2 = l2 + m1
  -- hmn : m1 + n2 = m2 + n1
  -- ⊢ l1 + n2 = l2 + n1

  have : m1 + (l1 + n2) = m1 + (l2 + n1) := calc
    _ = m1 + n2 + l1 := by ac_rfl
    _ = m2 + n1 + l1 := by rw [hmn]
    _ = l1 + m2 + n1 := by ac_rfl
    _ = l2 + m1 + n1 := by rw [hlm]
    _ = m1 + (l2 + n1) := by ac_rfl
  simp_all

推移律の証明では、両辺に m1 を加えた等式を経由することで、hlm と hmn から目的の等式を導いています。両辺に同じ m1 を加えているため、最後に simp_all で m1 を消去して目標の形に帰着させています。

theorem PreInt.r.equiv : Equivalence r :=
  {
    refl := r.refl
    symm := r.symm
    trans := r.trans
  }

商による整数の構成

最後に、PreInt に対して Setoid のインスタンスを与え、その商として整数 MyInt を定義します。

@[instance] def PreInt.sr : Setoid PreInt := ⟨r, r.equiv⟩

abbrev MyInt := Quotient PreInt.sr

これで、MyNat のペアの商として整数 MyInt を構成することができました。

本記事のコードは以下のリポジトリで公開しています。
https://github.com/ringring-creator/LearnLean