整数の引き算とAddCommGroup

前回はMyNatの同値類として整数MyIntを構築しました。今回はMyIntの引き算を定義し、さらにMathlibが提供するアーベル群のクラスAddCommGroupにMyIntを登録することで、これまで証明してきた法則を再利用できるようにします。本記事はゼロから始めるLean言語入門 手を動かして学ぶ形式数学ライブラリ開発を参考にしています。

引き算を定義する

整数の引き算は、加法の逆元を足すことで定義できます。MyInt.subを定義し、Subインスタンスに登録します。あわせて x - y と x + -y が等しいことをsub_defとして示し、simpで書き換えに使えるようにしておきます。

def MyInt.sub (m n : MyInt) : MyInt := m + -n

instance : Sub MyInt where
  sub := MyInt.sub

@[notation_simp, simp]
theorem MyInt.sub_def (x y : MyInt) : x -y = x + -y := rfl

あわせて、加法の逆元をキャンセルできることを示すneg_add_cancelも証明しておきます。unfold_int₁で定義を展開したあと、ac_rflで示せます。

theorem MyInt.neg_add_cancel (m : MyInt) : -m + m = 0 := by
  revert m
  unfold_int₁
  ac_rfl

AddCommGroupとして登録する

MyIntをMathlibのAddCommGroupに登録すると、可換群についてMathlibが持つ補題やタクティクをそのまま利用できるようになります。nsmulは自然数倍、zsmulは整数倍を表すフィールドで、既定の実装であるnsmulRecとzsmulRecを渡します。add_assocやadd_commなど、これまでに証明してきた法則はそのままフィールドに渡すだけで登録できます。

instance : AddCommGroup MyInt where
  add_assoc := MyInt.add_assoc
  add_comm := MyInt.add_comm
  zero_add := MyInt.zero_add
  add_zero := MyInt.add_zero
  neg_add_cancel := MyInt.neg_add_cancel
  nsmul := nsmulRec
  zsmul := zsmulRec

abelタクティクを利用する

AddCommGroupとして登録したことで、可換群における等式をまとめて処理できるabelタクティクが使えるようになります。

example (a b : MyInt) : (a + b) - b = a := by
  abel

⟦⟧記法の衝突を回避する

Mathlibをインポートすると、Quotient.mkに対して用意していた⟦⟧記法がMathlib側の記法と衝突することがあります。この場合、notationをscopedにしてPreInt名前空間の中に閉じ込めることで衝突を回避できます。

namespace PreInt
scoped notation "⟦" a "⟧" => Quotient.mk PreInt.sr a
end PreInt
open scoped PreInt

今回のコードは以下のリポジトリにあります。
https://github.com/ringring-creator/LearnLean