A first example: the integers under addition

Consider packaging $(\mathbb{Z}, +, 0, -(-))$ as a Group Int. The construction proceeds field by field, proving each obligation with a short, explicit tactic proof.

def intGroup : Group Int where
  op := fun a b => a + b
  id := 0
  inv := fun a => -a
  assoc := by
    intro a b c
    -- Goal: (a + b) + c = a + (b + c)
    exact Int.add_assoc a b c
  id_left := by
    intro a
    -- Goal: 0 + a = a
    exact Int.zero_add a
  id_right := by
    intro a
    -- Goal: a + 0 = a
    exact Int.add_zero a
  inv_left := by
    intro a
    -- Goal: (-a) + a = 0
    exact Int.add_left_neg a
  inv_right := by
    intro a
    -- Goal: a + (-a) = 0
    exact Int.add_right_neg a

Each field is proved separately. Each proof is a single intro (to name the universally quantified variables) followed by exact naming the exact core-library lemma that already states this fact about Int. No step is hidden: Int.add_assoc, Int.zero_add, and the rest are themselves proved (elsewhere, in Lean’s core library) by induction on the same Nat/Int representation introduced in Chapter 4. These lemmas are reused here rather than re-deriving integer arithmetic from scratch.

Mathematical reading. This shows $(\mathbb{Z}, +, 0, -)$ as an object of the category $\mathbf{Grp}$. The term intGroup is a proof that $\mathbb{Z}$ is a group, built by giving the data $(+, 0, -)$ and verifying each axiom. The verification is not re-proved here but cited: associativity is $\mathrm{Int.add_assoc}$, the identity laws are $0 + a = a = a + 0$, and the inverse laws are $(-a) + a = 0 = a + (-a)$. In textbook terms this is the one-line remark “$\mathbb{Z}$ under addition is an abelian group,” with the underlying lemmas about $\mathbb{Z}$ (themselves ultimately inductions on the integers) written out in full instead of just assumed.

Mathlib equivalent. Mathlib requires no intGroup-style bundle at all: Int is already registered as an AddCommGroup instance, and the five axioms above are available as free-standing lemmas that apply to every additive group, not just Int:

example : AddCommGroup Int := inferInstance

example (a b c : Int) : (a + b) + c = a + (b + c) := add_assoc a b c
example (a : Int) : 0 + a = a := zero_add a
example (a : Int) : a + 0 = a := add_zero a
example (a : Int) : -a + a = 0 := neg_add_cancel a
example (a : Int) : a + -a = 0 := add_neg_cancel a

This is the same content as intGroup, the same five facts about $\mathbb{Z}$. But where the book assembles a Group Int term by hand, Mathlib’s version has nothing to assemble: the instance already exists, found automatically by inferInstance. And add_assoc/zero_add/etc. are generic lemmas about any AddCommGroup, so they read somewhat differently from Int.add_assoc: they apply equally well to Chapter 6’s perm3Group-style examples once those are phrased in Mathlib’s Group/AddCommGroup classes (Chapter 6, Section 4 does exactly that next).

← Translating into Lean

Index

Next: Permutations example →