ホーム / Technical /

Defining Addition on MyInt

Saturday, 15 August 2026

Lean Mathematics Technical

t f B! P L

Last time we prepared PreInt and its equivalence relation in order to define MyInt. This time we define addition on MyInt. This article is based on "ゼロから始めるLean言語入門 手を動かして学ぶ形式数学ライブラリ開発".

Defining addition on PreInt

First we define addition on PreInt, the type before taking the quotient. Since PreInt is a pair of natural numbers, we simply add the corresponding components.

def PreInt.add (m n : PreInt) : MyInt :=
  match m, n with
  | (m1, m2), (n1, n2) => ⟦(m1 + n1, m2 + n2)⟧

Defining addition on MyInt with Quotient.lift₂

To define addition on MyInt, we lift the domain of PreInt.add to the quotient using Quotient.lift₂. Since addition takes two arguments, we use Quotient.lift₂ instead of Quotient.lift. To use Quotient.lift₂, we need to prove that the result does not depend on the choice of representatives, in other words that the equivalence relation is preserved.

The proof applies Quotient.sound to move back into the world of PreInt, uses notation_simp to move into the world of addition, and then finishes with equational reasoning.

def MyInt.add : MyInt → MyInt → MyInt := Quotient.lift₂ PreInt.add <| by
  -- ⊢ ∀ (a₁ b₁ a₂ b₂ : PreInt), a₁ ≈ a₂ → b₁ ≈ b₂ → a₁.add b₁ = a₂.add b₂
  intro (m1, m2) (n1, n2) (m'1, m'2) (n'1, n'2) rm rn
  dsimp [PreInt.add]
  -- rm : (m1, m2) ≈ (m'1, m'2)
  -- rn : (n1, n2) ≈ (n'1, n'2)
  -- ⊢ Quotient.mk PreInt.sr (m1 + n1, m2 + n2) = Quotient.mk PreInt.sr (m'1 + n'1, m'2 + n'2)
  apply Quotient.sound -- ⊢ (m1 + n1, m2 + n2) ≈ (m'1 + n'1, m'2 + n'2)
  notation_simp at *
  -- rm : m1 + m'2 = m2 + m'1
  -- rn : n1 + n'2 = n2 + n'1
  -- ⊢ m1 + n1 + (m'2 + n'2) = m2 + n2 + (m'1 + n'1)
  have : m1 + n1 + (m'2 + n'2) = m2 + n2 + (m'1 + n'1) := calc
    _ = (m1 + m'2) + (n1 + n'2) := by ac_rfl
    _ = (m2 + m'1) + (n1 + n'2) := by rw [rm]
    _ = (m2 + m'1) + (n2 + n'1) := by rw [rn]
    _ = m2 + n2 + (m'1 + n'1) := by ac_rfl
  assumption

instance instAddMyInt : Add MyInt where
  add := MyInt.add

#check (3 + 4 : MyInt)

Registering addition with simp

We also register addition with simp. The textbook proves this with dsimp, but that resulted in an error here, so we use rfl instead.

@[simp]
theorem MyInt.add_def (x1 x2 y1 y2 : MyNat)
  : ⟦(x1, y1)⟧ + ⟦(x2, y2)⟧ = (⟦(x1 + x2, y1 + y2)⟧ : MyInt) := by rfl

Proving that adding zero leaves an integer unchanged

We prove that adding zero to an integer does not change its value, and register the result with simp. The proof uses Quotient.inductionOn. Quotient.inductionOn is the induction principle stating that to prove a proposition about an element m of a quotient type Quotient s, it suffices to prove it for a representative a of its equivalence class.

Passing m and leaving ?_ generates a new subgoal for the second argument of Quotient.inductionOn m, namely the proof that the proposition holds for an arbitrary representative a. As a result, the goal changes from m + 0 = m to a statement about a representative a of type PreInt.

@[simp]
theorem MyInt.add_zero (m : MyInt) : m + 0 = m := by
  refine Quotient.inductionOn m ?_
  -- ∀ (a : PreInt), Quotient.mk PreInt.sr a + 0 = Quotient.mk PreInt.sr a

  intro (a1, a2)
  apply Quot.sound
  notation_simp
  -- a1 a2 : MyNat
  -- ⊢ a1 + 0 + a2 = a2 + 0 + a1

  ac_rfl

@[simp]
theorem MyInt.zero_add (m : MyInt) : 0 + m = m := by
  refine Quotient.inductionOn m ?_
  intro (a1, a2)
  apply Quot.sound
  notation_simp
  ac_rfl

Sharing the proof steps with a macro

We turn the steps that repeatedly appeared in the proofs above, which reduce a statement about integers to a statement about natural numbers, into a macro. Referencing an out-of-scope variable directly, such as m in the code below, results in an error. This is due to a mechanism called macro hygiene.

section
  local macro "unfold_int₁" : tactic => `(tactic| focus
    refine Quotient.inductionOn m ?_
    intro (a1, a2)
    apply Quot.sound
    notation_simp
  )

  example (m : MyInt) : m + 0 = m := by
    fail_if_success unfold_int₁
    sorry
end

This error could be suppressed with set_option hygiene false, but that is not desirable. Instead, we use revert m to remove m from the local context, turning the goal into ⊢ ∀ (m : MyInt), 0 + m = m, and have the macro declare m again with intro. This solves the problem.

macro "unfold_int₁" : tactic => `(tactic| focus
  intro m
  refine Quotient.inductionOn m ?_
  intro (a1, a2)
  apply Quot.sound
  notation_simp
)

example (m : MyInt) : 0 + m = m := by
  revert m -- ⊢ ∀ (m : MyInt), 0 + m = m
  unfold_int₁
  ac_rfl

Proving associativity and commutativity

Similarly, we create unfold_int₂ and unfold_int₃, prove associativity and commutativity of addition, and register them as instances.

macro "unfold_int₂" : tactic => `(tactic| focus
  intro m n
  refine Quotient.inductionOn₂ m n ?_
  intro (a1, a2) (b1, b2)
  apply Quot.sound
  notation_simp
)

macro "unfold_int₃" : tactic => `(tactic| focus
  intro m n k
  refine Quotient.inductionOn₃ m n k ?_
  intro (a1, a2) (b1, b2) (c1, c2)
  apply Quot.sound
  notation_simp
)

theorem MyInt.add_assoc (m n k : MyInt) : m + n + k = m + (n + k) := by
  revert m n k
  unfold_int₃
  ac_rfl

theorem MyInt.add_comm (m n : MyInt) : m + n = n + m := by
  revert m n
  unfold_int₂
  ac_rfl

instance : Std.Associative (α := MyInt) (· + ·) where
  assoc := MyInt.add_assoc

instance : Std.Commutative (α := MyInt) (· + ·) where
  comm := MyInt.add_comm

The full source code is available on GitHub.

QooQ