ホーム / Technical /

Integer Subtraction and AddCommGroup

Saturday, 15 August 2026

Lean Mathematics Technical

t f B! P L

Last time we built the integers MyInt as equivalence classes over MyNat. This time we define subtraction on MyInt, and then register MyInt as an instance of Mathlib's abelian group class AddCommGroup so that the laws we've already proven can be reused. This article follows ゼロから始めるLean言語入門 手を動かして学ぶ形式数学ライブラリ開発.

Defining subtraction

Subtraction on the integers can be defined by adding the additive inverse. We define MyInt.sub and register it as the Sub instance. We also prove sub_def, showing that x - y equals x + -y, and mark it simp so it can be used for rewriting.

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

We also prove neg_add_cancel, which shows that an element cancels with its additive inverse. Unfolding the definition with unfold_int₁ and then calling ac_rfl closes the goal.

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

Registering MyInt as an AddCommGroup

Registering MyInt as an instance of Mathlib's AddCommGroup lets us use Mathlib's lemmas and tactics for abelian groups directly. nsmul and zsmul represent multiplication by a natural number and by an integer respectively, and we pass the default implementations nsmulRec and zsmulRec for them. The laws we've already proven, such as add_assoc and add_comm, can simply be passed in as the remaining fields.

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

Using the abel tactic

Now that MyInt is registered as an AddCommGroup, we can use the abel tactic, which handles equalities in abelian groups automatically.

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

Resolving a conflict with the ⟦⟧ notation

After importing Mathlib, the ⟦⟧ notation we defined for Quotient.mk can conflict with Mathlib's own notation. This can be avoided by making the notation scoped and confining it to the PreInt namespace.

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

The code for this article is available in the repository below.
https://github.com/ringring-creator/LearnLean

QooQ