ホーム / Technical /

Constructing the integers `MyInt` from the natural numbers `MyNat` in Lean 4.

Saturday, 15 August 2026

Lean Mathematics Technical

t f B! P L

Now that we have Quotient and MyNat in place, it's time to construct the integers.

Comparing the natural numbers and the integers, natural numbers run 0, 1, 2, ..., while integers extend that to ..., -1, 0, 1, .... The difference between them is subtraction. In this article we construct integers by representing subtraction as a pair of MyNat values. This article follows「ゼロから始めるLean言語入門 手を動かして学ぶ形式数学ライブラリ開発」as its reference.

Defining PreInt

We represent an integer as a pair of MyNat values (a, b), interpreted as \( a - b \). Let's start by defining this pair type as PreInt.

abbrev PreInt := MyNat × MyNat

By declaring it with the abbrev keyword, PreInt is treated as inlined, so we can directly use all the properties MyNat already has, such as commutativity and associativity.

Defining the equivalence relation

This raises a problem: pairs like (0, 1) and (1, 2) both correspond to -1, so we end up with duplicates. We'd like to treat \( (x_1, y_1) \) and \( (x_2, y_2) \) as equivalent whenever \( x_1 - y_1 = x_2 - y_2 \), but MyNat has no subtraction defined. So instead we rewrite the equation as an addition and define equivalence as \( 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

Proving the equivalence relation

Next we prove that PreInt.r is indeed an equivalence relation, meaning it satisfies reflexivity, symmetry, and transitivity.

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

Reflexivity reduces to showing m1 + m2 = m2 + m1, which follows directly from commutativity of addition via 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

For symmetry, we use the hypothesis h to connect m2 + n1 and m1 + n2, then rewrite through calc down to the target equation.

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

For transitivity, we derive the target equation from hlm and hmn by routing through an equation with m1 added to both sides. Since the same m1 is added on both sides, simp_all finally cancels it to reach the goal.

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

Constructing the integers as a quotient

Finally, we give PreInt a Setoid instance and define the integers MyInt as its quotient.

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

abbrev MyInt := Quotient PreInt.sr

With this, we've constructed the integers MyInt as a quotient of pairs of MyNat.

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

QooQ