6. Abstract Algebra

Modern mathematics makes essential use of algebraic structures, which encapsulate patterns that can be instantiated in multiple settings. The subject provides various ways of defining such structures and constructing particular instances.

Lean therefore provides corresponding ways of defining structures formally and working with them. You have already seen examples of algebraic structures in Lean, such as rings and lattices, which were discussed in Chapter 2. This chapter will explain the mysterious square bracket annotations that you saw there, [ring α] and [lattice α]. It will also show you how to define and use algebraic structures on your own.

For more technical detail, you can consult Theorem Proving in Lean, and a paper by Anne Baanen, Use and abuse of instance parameters in the Lean mathematical library.

6.1. Structures

In the broadest sense of the term, a structure is a specification of a collection of data, possibly with constraints that the data is required to satisfy. An instance of the structure is a particular bundle of data satisfying the constraints. For example, we can specify that a point is a tuple of three real numbers:

@[ext] structure point := (x : ℝ) (y : ℝ) (z : ℝ)

The @[ext] annotation tells Lean to automatically generate theorems that can be used to prove that two instances of a structure are equal when their components are equal, a property known as extensionality.

#check point.ext

example (a b : point) (hx : a.x = b.x) (hy : a.y = b.y) (hz : a.z = b.z) :
  a = b :=
begin
  ext,
  repeat { assumption }
end

We can then define particular instances of the point structure. Lean provides multiple ways of doing that.

def my_point1 : point :=
{ x := 2,
  y := -1,
  z := 4 }

def my_point2 :=
{ point .
  x := 2,
  y := -1,
  z := 4 }

def my_point3 : point := ⟨2, -1, 4⟩

def my_point4 := point.mk 2 (-1) 4

In the first two examples, the fields of the structure are named explicitly. In the first case, because Lean knows that the expected type of my_point1 is a point, you can start the definition by writing an underscore, _. Clicking on the light bulb that appears nearby in VS Code will then give you the option of inserting a template definition with the field names listed for you.

The function point.mk referred to in the definition of my_point4 is known as the constructor for the point structure, because it serves to construct elements. You can specify a different name if you want, like build.

structure point' := build :: (x : ℝ) (y : ℝ) (z : ℝ)

#check point'.build 2 (-1) 4

The next two examples show how to define functions on structures. Whereas the second example makes the point.mk constructor explicit, the first example uses an anonymous constructor for brevity. Lean can infer the relevant constructor from the indicated type of add. It is conventional to put definitions and theorems associated with a structure like point in a namespace with the same name. In the example below, because we have opened the point namespace, the full name of add is point.add. When the namespace is not open, we have to use the full name. But remember that it is often convenient to use anonymous projection notation, which allows us to write a.add b instead of point.add a b. Lean interprets the former as the latter because a has type point.

namespace point

def add (a b : point) : point := ⟨a.x + b.x, a.y + b.y, a.z + b.z⟩

def add' (a b : point) : point :=
{ x := a.x + b.x,
  y := a.y + b.y,
  z := a.z + b.z }

#check add my_point1 my_point2
#check my_point1.add my_point2

end point

#check point.add my_point1 my_point2
#check my_point1.add my_point2

Below we will continue to put definitions in the relevant namespace, but we will leave the namespacing commands out of the quoted snippets. To prove properties of the addition function, we can use rw to expand the definition and ext to reduce an equation between two elements of the structure to equations between the components. Below we use the protected keyword so that the name of the theorem is point.add_comm, even when the namespace is open. This is helpful when we want to avoid ambiguity with a generic theorem like add_comm.

protected theorem add_comm (a b : point) : add a b = add b a :=
begin
  rw [add, add],
  ext; dsimp,
  repeat { apply add_comm }
end

example (a b : point) : add a b = add b a :=
by simp [add, add_comm]

Because Lean can unfold definitions and simplify projections internally, sometimes the equations we want hold definitionally.

theorem add_x (a b : point) : (a.add b).x = a.x + b.x := rfl

It is also possible to define functions on structures using pattern matching, in a manner similar to the way we defined recursive functions in Section 5.2. The definitions add_alt and add_alt' below are essentially the same; the only difference is that we use anonymous constructor notation in the second. Although it is sometimes convenient to define functions this way, the definitional properties are not as convenient. For example, the expressions add_alt a b and add_alt' a b cannot be simplified until we decompose a and b into components, which we can do with cases, rcases, etc.

def add_alt : point → point → point
| (point.mk x₁ y₁ z₁) (point.mk x₂ y₂ z₂) := ⟨x₁ + x₂, y₁ + y₂, z₁ + z₂⟩

def add_alt' : point → point → point
| ⟨x₁, y₁, z₁⟩ ⟨x₂, y₂, z₂⟩ := ⟨x₁ + x₂, y₁ + y₂, z₁ + z₂⟩

theorem add_alt_x (a b : point) : (a.add_alt b).x = a.x + b.x :=
by { cases a, cases b, refl }

theorem add_alt_comm (a b : point) : add_alt a b = add_alt b a :=
begin
  rcases a with ⟨xa, ya, za⟩,
  rcases b with ⟨xb, yb, zb⟩,
  rw [add_alt, add_alt],
  ext; dsimp,
  apply add_comm,
  repeat { apply add_comm },
end

example (a b : point) : add_alt a b = add_alt b a :=
begin
  rcases a with ⟨xa, ya, za⟩,
  rcases b with ⟨xb, yb, zb⟩,
  simp [add_alt, add_comm]
end

example : ∀ a b : point, add_alt a b = add_alt b a :=
begin
  rintros ⟨xa, ya, za⟩ ⟨xb, yb, zb⟩,
  simp [add_alt, add_comm]
end

example : ∀ a b : point, add a b = add b a :=
λ ⟨xa, ya, za⟩ ⟨xb, yb, zb⟩, by simp [add, add_comm]

Mathematical constructions often involve taking apart bundled information and putting it together again in different ways. It therefore makes sense that Lean and mathlib offer so many ways of doing this efficiently. As an exercise, try proving that point.add is associative. Then define scalar multiplication for a point and show that it distributes over addition.

protected theorem add_assoc (a b c : point) :
  (a.add b).add c = a.add (b.add c) :=
sorry

def smul (r : ℝ) (a : point) : point :=
sorry

theorem smul_distrib (r : ℝ) (a b : point) :
  (smul r a).add (smul r b) = smul r (a.add b) :=
sorry

Using structures is only the first step on the road to algebraic abstraction. We don’t yet have a way to link point.add to the generic + symbol, or to connect point.add_comm and point.add_assoc to the generic add_comm and add_assoc theorems. These tasks belong to the algebraic aspect of using structures, and we will explain how to carry them out in the next section. For now, just think of a structure as a way of bundling together objects and information.

It is especially useful that a structure can specify not only data types but also constraints that the data must satisfy. In Lean, the latter are represented as fields of type Prop. For example, the standard 2-simplex is defined to be the set of points \((x, y, z)\) satisfying \(x ≥ 0\), \(y ≥ 0\), \(z ≥ 0\), and \(x + y + z = 1\). If you are not familiar with the notion, you should draw a picture, and convince yourself that this set is the equilateral triangle in three-space with vertices \((1, 0, 0)\), \((0, 1, 0)\), and \((0, 0, 1)\), together with its interior. We can represent it in Lean as follows:

structure standard_two_simplex :=
(x : ℝ)
(y : ℝ)
(z : ℝ)
(x_nonneg : 0 ≤ x)
(y_nonneg : 0 ≤ y)
(z_nonneg : 0 ≤ z)
(sum_eq   : x + y + z = 1)

Notice that the last four fields refer to x, y, and z, that is, the first three fields. We can define a map from the two-simplex to itself that swaps x and y:

def swap_xy (a : standard_two_simplex) : standard_two_simplex :=
{ x := a.y,
  y := a.x,
  z := a.z,
  x_nonneg := a.y_nonneg,
  y_nonneg := a.x_nonneg,
  z_nonneg := a.z_nonneg,
  sum_eq   := by rw [add_comm a.y a.x, a.sum_eq] }

More interestingly, we can compute the midpoint of two points on the simplex. We need to add noncomputable theory in order to use division on the real numbers.

noncomputable theory

def midpoint (a b : standard_two_simplex) : standard_two_simplex :=
{ x        := (a.x + b.x) / 2,
  y        := (a.y + b.y) / 2,
  z        := (a.z + b.z) / 2,
  x_nonneg := div_nonneg (add_nonneg a.x_nonneg b.x_nonneg) (by norm_num),
  y_nonneg := div_nonneg (add_nonneg a.y_nonneg b.y_nonneg) (by norm_num),
  z_nonneg := div_nonneg (add_nonneg a.z_nonneg b.z_nonneg) (by norm_num),
  sum_eq   := by { field_simp, linarith [a.sum_eq, b.sum_eq]} }

Here we have established x_nonneg, y_nonneg, and z_nonneg with concise proof terms, but establish sum_eq in tactic mode, using by. You can just as well use a begin ... end block for that purpose.

Given a parameter \(\lambda\) satisfying \(0 \le \lambda \le 1\), we can take the weighted average \(\lambda a + (1 - \lambda) b\) of two points \(a\) and \(b\) in the standard 2-simplex. We challenge you to define that function, in analogy to the midpoint function above.

def weighted_average (lambda : real)
    (lambda_nonneg : 0 ≤ lambda) (lambda_le : lambda ≤ 1)
    (a b : standard_two_simplex) :
  standard_two_simplex :=
sorry

Structures can depend on parameters. For example, we can generalize the standard 2-simplex to the standard \(n\)-simplex for any \(n\). At this stage, you don’t have to know anything about the type fin n except that it has \(n\) elements, and that Lean knows how to sum over it.

open_locale big_operators

structure standard_simplex (n : ℕ) :=
(v          : fin n → ℝ)
(nonneg     : ∀ i : fin n, 0 ≤ v i)
(sum_eq_one : ∑ i, v i = 1)

namespace standard_simplex

def midpoint (n : ℕ) (a b : standard_simplex n) : standard_simplex n :=
{ v := λ i, (a.v i + b.v i) / 2,
  nonneg :=
    begin
      intro i,
      apply div_nonneg,
      { linarith [a.nonneg i, b.nonneg i] },
      norm_num
    end,
  sum_eq_one :=
    begin
      simp [div_eq_mul_inv, ←finset.sum_mul, finset.sum_add_distrib,
        a.sum_eq_one, b.sum_eq_one],
      field_simp
    end  }

end standard_simplex

As an exercise, see if you can define the weighted average of two points in the standard \(n\)-simplex. You can use finset.sum_add_distrib and finset.mul_sum to manipulate the relevant sums.

We have seen that structures can be used to bundle together data and properties. Interestingly, they can also be used to bundle together properties without the data. For example, the next structure, is_linear, bundles together the two components of linearity.

structure is_linear (f : ℝ → ℝ) :=
(is_additive : ∀ x y, f (x + y) = f x + f y)
(preserves_mul : ∀ x c, f (c * x) = c * f x)

section
variables (f : ℝ → ℝ) (linf : is_linear f)

#check linf.is_additive
#check linf.preserves_mul

end

It is worth pointing out that structures are not the only way to bundle together data. The point data structure can be defined using the generic type product, and is_linear can be defined with a simple and.

def point'' := ℝ × ℝ × ℝ

def is_linear' (f : ℝ → ℝ) :=
(∀ x y, f (x + y) = f x + f y) ∧ (∀ x c, f (c * x) = c * f x)

Generic type constructions can even be used in place of structures with dependencies between their components. For example, the subtype construction combines a piece of data with a property. You can think of the type preal in the next example as being the type of positive real numbers. Any x : preal has two components: the value, and the property of being positive. You can access these components as x.val, which has type ℝ, and x.property, which represents the fact 0 < x.val.

def preal := { y : ℝ // 0 < y }

section
variable x : preal

#check x.val
#check x.property

#check x.1
#check x.2

end

We could have used subtypes to define the standard 2-simplex, as well as the standard \(n\)-simplex for an arbitrary \(n\).

def standard_two_simplex' :=
{ p : ℝ × ℝ × ℝ // 0 ≤ p.1 ∧ 0 ≤ p.2.1 ∧ 0 ≤ p.2.2 ∧ p.1 + p.2.1 + p.2.2 = 1 }

def standard_simplex' (n : ℕ) :=
{ v : fin n → ℝ // (∀ i : fin n, 0 ≤ v i) ∧ (∑ i, v i = 1) }

Similarly, Sigma types are generalizations of ordered pairs, whereby the type of the second component depends on the type of the first.

def std_simplex := Σ n : ℕ, standard_simplex n

section
variable s : std_simplex

#check s.fst
#check s.snd

#check s.1
#check s.2

end

Given s : std_simplex, the first component s.fst is a natural number, and the second component is an element of the corresponding simplex standard_simplex s.fst. The difference between a Sigma type and a subtype is that the second component of a Sigma type is data rather than a proposition.

But even though we can use products, subtypes, and Sigma types instead of structures, using structures has a number of advantages. Defining a structure abstracts away the underlying representation and provides custom names for the functions that access the components. This makes proofs more robust: proofs that rely only on the interface to a structure will generally continue to work when we change the definition, as long as we redefine the old accessors in terms of the new definition. Moreover, as we are about to see, Lean provides support for weaving structures together into a rich, interconnected hierarchy, and for managing the interactions between them.

6.2. Algebraic Structures

To clarify what we mean by the phrase algebraic structure, it will help to consider some examples.

  1. A partially ordered set consists of a set \(P\) and a binary relation \(\le\) on \(P\) that is transitive and antireflexive.

  2. A group consists of a set \(G\) with an associative binary operation, an identity element \(1\), and a function \(g \mapsto g^{-1}\) that returns an inverse for each \(g\) in \(G\). A group is abelian or commutative if the operation is commutative.

  3. A lattice is a partially ordered set with meets and joins.

  4. A ring consists of an (additively written) abelian group \((R, +, 0, x \mapsto -x)\) together with an associative multiplication operation \(\cdot\) and an identity \(1\), such that multiplication distributes over addition. A ring is commutative if the multiplication is commutative.

  5. An ordered ring \((R, +, 0, -, \cdot, 1, \le)\) consists of a ring together with a partial order on its elements, such that \(a \le b\) implies \(a + c \le b + c\) for every \(a\), \(b\), and \(c\) in \(R\), and \(0 \le a\) and \(0 \le b\) implies \(0 \le a b\) for every \(a\) and \(b\) in \(R\).

  6. A metric space consists of a set \(X\) and a function \(d : X \times X \to \mathbb{R}\) such that the following hold:

    • \(d(x, y) \ge 0\) for every \(x\) and \(y\) in \(X\).

    • \(d(x, y) = 0\) if and only if \(x = y\).

    • \(d(x, y) = d(y, x)\) for every \(x\) and \(y\) in \(X\).

    • \(d(x, z) \le d(x, y) + d(y, z)\) for every \(x\), \(y\), and \(z\) in \(X\).

  7. A topological space consists of a set \(X\) and a collection \(\mathcal T\) of subsets of \(X\), called the open subsets of \(X\), such that the following hold:

    • The empty set and \(X\) are open.

    • The intersection of two open sets is open.

    • An arbitrary union of open sets is open.

In each of these examples, the elements of the structure belong to a set, the carrier set, that sometimes stands proxy for the entire structure. For example, when we say “let \(G\) be a group” and then “let \(g \in G\),” we are using \(G\) to stand for both the structure and its carrier. Not every algebraic structure is associated with a single carrier set in this way. For example, a bipartite graph involves a relation between two sets, as does a Galois connection, A category also involves two sets of interest, commonly called the objects and the morphisms.

The examples indicate some of the things that a proof assistant has to do in order to support algebraic reasoning. First, it needs to recognize concrete instances of structures. The number systems \(\mathbb{Z}\), \(\mathbb{Q}\), and \(\mathbb{R}\) are all ordered rings, and we should be able to apply a generic theorem about ordered rings in any of these instances. Sometimes a concrete set may be an instance of a structure in more than one way. For example, in addition to the usual topology on \(\mathbb{R}\), which forms the basis for real analysis, we can also consider the discrete topology on \(\mathbb{R}\), in which every set is open.

Second, a proof assistant needs to support generic notation on structures. In Lean, the notation * is used for multiplication in all the usual number systems, as well as for multiplication in generic groups and rings. When we use an expression like f x * y, Lean has to use information about the types of f, x, and y to determine which multiplication we have in mind.

Third, it needs to deal with the fact that structures can inherit definitions, theorems, and notation from other structures in various ways. Some structures extend others by adding more axioms. A commutative ring is still a ring, so any definition that makes sense in a ring also makes sense in a commutative ring, and any theorem that holds in a ring also holds in a commutative ring. Some structures extend others by adding more data. For example, the additive part of any ring is an additive group. The ring structure adds a multiplication and an identity, as well as axioms that govern them and relate them to the additive part. Sometimes we can define one structure in terms of another. Any metric space has a canonical topology associated with it, the metric space topology, and there are various topologies that can be associated with any linear ordering.

Finally, it is important to keep in mind that mathematics allows us to use functions and operations to define structures in the same way we use functions and operations to define numbers. Products and powers of groups are again groups. For every \(n\), the integers modulo \(n\) form a ring, and for every \(k > 0\), the \(k \times k\) matrices of polynomials with coefficients in that ring again form a ring. Thus we can calculate with structures just as easily as we can calculate with their elements. This means that algebraic structures lead dual lives in mathematics, as containers for collections of objects and as objects in their own right. A proof assistant has to accommodate this dual role.

When dealing with elements of a type that has an algebraic structure associated with it, a proof assistant needs to recognize the structure and find the relevant definitions, theorems, and notation. All this should sound like a lot of work, and it is. But Lean uses a small collection of fundamental mechanisms to carry out these tasks. The goal of this section is to explain these mechanisms and show you how to use them.

The first ingredient is almost too obvious to mention: formally speaking, algebraic structures are structures in the sense of Section 6.1. An algebraic structure is a specification of a bundle of data satisfying some axiomatic hypotheses, and we saw in Section 6.1 that this is exactly what the structure command is designed to accommodate. It’s a marriage made in heaven!

Given a data type α, we can define the group structure on α as follows.

structure group₁ (α : Type*) :=
(mul: α → α → α)
(one: α)
(inv: α → α)
(mul_assoc : ∀ x y z : α, mul (mul x y) z = mul x (mul y z))
(mul_one: ∀ x : α, mul x one = x)
(one_mul: ∀ x : α, mul one x = x)
(mul_left_inv : ∀ x : α, mul (inv x) x = one)

Notice that the type α is a parameter in the definition of group₁. So you should think of an object struc : group₁ α as being a group structure on α. We saw in Section 2.2 that the counterpart mul_right_inv to mul_left_inv follows from the other group axioms, so there is no need to add it to the definition.

This definition of a group is similar to the definition of group in mathlib, and we have chosen the name group₁ to distinguish our version. If you write #check group and ctrl-click on the definition, you will see that the mathlib version of group is defined to extend another structure; we will explain how to do that later. If you type #print group you will also see that the mathlib version of group has a number of extra fields. For reasons we will explain later, sometimes it is useful to add redundant information to a structure, so that there are additional fields for objects and functions that can be defined from the core data. Don’t worry about that for now. Rest assured that our simplified version group₁ is morally the same as the definition of a group that mathlib uses.

It is sometimes useful to bundle the type together with the structure, and mathlib also contains a definition of a Group structure that is equivalent to the following:

structure Group₁ :=
(α : Type*)
(str : group₁ α)

The mathlib version is found in algebra.category.Group.basic, and you can #check it if you add this to the imports at the beginning of the examples file.

For reasons that will become clearer below, it is more often useful to keep the type α separate from the structure group α. We refer to the two objects together as a partially bundled structure, since the representation combines most, but not all, of the components into one structure. It is common in mathlib to use capital roman letters like G for a type when it is used as the carrier type for a group.

Let’s construct a group, which is to say, an element of the group₁ type. For any pair of types α and β, Mathlib defines the type equiv α β of equivalences between α and β. Mathlib also defines the suggestive notation α ≃ β for this type. An element f : α ≃ β is a bijection between α and β represented by four components: a function f.to_fun from α to β, the inverse function f.inv_fun from β to α, and two properties that specify these functions are indeed inverse to one another.

variables (α β γ : Type*)
variables (f : α ≃ β) (g : β ≃ γ)

#check equiv α β
#check (f.to_fun : α → β)
#check (f.inv_fun : β → α)
#check (f.right_inv: ∀ x : β, f (f.inv_fun x) = x)
#check (f.left_inv: ∀ x : α, f.inv_fun (f x) = x)

#check (equiv.refl α : α ≃ α)
#check (f.symm : β ≃ α)
#check (f.trans g : α ≃ γ)

Notice the creative naming of the last three constructions. We think of the identity function equiv.refl, the inverse operation equiv.symm, and the composition operation equiv.trans as explicit evidence that the property of being in bijective correspondence is an equivalence relation.

Notice also that f.trans g requires composing the forward functions in reverse order. Mathlib has declared a coercion from equiv α β to the function type α → β, so we can omit writing .to_fun and have Lean insert it for us.

example (x : α) : (f.trans g).to_fun x = g.to_fun (f.to_fun x) := rfl

example (x : α) : (f.trans g) x = g (f x) := rfl

example : (f.trans g : α → γ) = g ∘ f := rfl

Mathlib also defines the type perm α of equivalences between α and itself.

example (α : Type*) : equiv.perm α = (α ≃ α) := rfl

It should be clear that equiv.perm α forms a group under composition of equivalences. We orient things so that mul f g is equal to g.trans f, whose forward function is f ∘ g. In other words, multiplication is what we ordinarily think of as composition of the bijections. Here we define this group:

def perm_group {α : Type*} : group₁ (equiv.perm α) :=
{ mul          := λ f g, equiv.trans g f,
  one          := equiv.refl α,
  inv          := equiv.symm,
  mul_assoc    := λ f g h, (equiv.trans_assoc _ _ _).symm,
  one_mul      := equiv.trans_refl,
  mul_one      := equiv.refl_trans,
  mul_left_inv := equiv.self_trans_symm }

In fact, mathlib defines exactly this group structure on equiv.perm α in the file group_theory.perm.basic. As always, you can hover over the theorems used in the definition of perm_group to see their statements, and you can jump to their definitions in the original file to learn more about how they are implemented.

In ordinary mathematics, we generally think of notation as independent of structure. For example, we can consider groups \((G_1, \cdot, 1, \cdot^{-1})\), \((G_2, \circ, e, i(\cdot))\), and \((G_3, +, 0, -)\). In the first case, we write the binary operation as \(\cdot\), the identity at \(1\), and the inverse function as \(x \mapsto x^{-1}\). In the second and third cases, we use the notational alternatives shown. When we formalize the notion of a group in Lean, however, the notation is more tightly linked to the structure. In Lean, the components of any group are named mul, one, and inv, and in a moment we will see how multiplicative notation is set up to refer to them. If we want to use additive notation, we instead use an isomorphic structure additive_group. Its components are named add, zero, and neg, and the associated notation is what you would expect it to be.

Recall the type point that we defined in Section 6.1, and the addition function that we defined there. These definitions are reproduced in the examples file that accompanies this section. As an exercise, define an add_group₁ structure that is similar to the group₁ structure we defined above, except that it uses the additive naming scheme just described. Define negation and a zero on the point data type, and define the add_group₁ structure on point.

structure add_group₁ (α : Type*) :=
(add : α → α → α)
-- fill in the rest

@[ext] structure point := (x : ℝ) (y : ℝ) (z : ℝ)

namespace point

def add (a b : point) : point := ⟨a.x + b.x, a.y + b.y, a.z + b.z⟩

def neg (a : point) : point := sorry

def zero : point := sorry

def add_group_point : add_group₁ point := sorry

end point

We are making progress. Now we know how to define algebraic structures in Lean, and we know how to define instances of those structures. But we also want to associate notation with structures so that we can use it with each instance. Moreover, we want to arrange it so that we can define an operation on a structure and use it with any particular instance, and we want to arrange it so that we can prove a theorem about a structure and use it with any instance.

In fact, mathlib is already set up to use generic group notation, definitions, and theorems for equiv.perm α.

variables {α : Type*} (f g : equiv.perm α) (n : ℕ)

#check f * g
#check mul_assoc f g g⁻¹

-- group power, defined for any group
#check g^n

example : f * g * (g⁻¹) = f :=
by { rw [mul_assoc, mul_right_inv, mul_one] }

example : f * g * (g⁻¹) = f := mul_inv_cancel_right f g

example {α : Type*} (f g : equiv.perm α) : g.symm.trans (g.trans f) = f :=
mul_inv_cancel_right f g

You can check that this is not the case for the additive group structure on point that we asked you to define above. Our task now is to understand that magic that goes on under the hood in order to make the examples for equiv.perm α work the way they do.

The issue is that Lean needs to be able to find the relevant notation and the implicit group structure, using the information that is found in the expressions that we type. Similarly, when we write x + y with expressions x and y that have type ℝ, Lean needs to interpret the + symbol as the relevant addition function on the reals. It also has to recognize the type ℝ as an instance of a commutative ring, so that all the definitions and theorems for a commutative ring are available. For another example, continuity is defined in Lean relative to any two topological spaces. When we have f : ℝ → ℂ and we write continuous f, Lean has to find the relevant topologies on ℝ and ℂ.

The magic is achieved with a combination of three things.

  1. Logic. A definition that should be interpreted in any group takes, as arguments, the type of the group and the group structure as arguments. Similarly, a theorem about the elements of an arbitrary group begins with universal quantifiers over the type of the group and the group structure.

  2. Implicit arguments. The arguments for the type and the structure are generally left implicit, so that we do not have to write them or see them in the Lean information window. Lean fills the information in for us silently.

  3. Type class inference. Also known as class inference, this is a simple but powerful mechanism that enables us to register information for Lean to use later on. When Lean is called on to fill in implicit arguments to a definition, theorem, or piece of notation, it can make use of information that has been registered.

Whereas an annotation (grp : group G) tells Lean that it should expect to be given that argument explicitly and the annotation {grp : group G} tells Lean that it should try to figure it out from contextual cues in the expression, the annotation [grp : group G] tells Lean that the corresponding argument should be synthesized using type class inference. Since the whole point to the use of such arguments is that we generally do not need to refer to them explicitly, Lean allows us to write [group G] and leave the name anonymous. You have probably already noticed that Lean chooses names like _inst_1 automatically. When we use the anonymous square-bracket annotation with the variables command, then as long as the variables are still in scope, Lean automatically adds the argument [group G] to any definition or theorem that mentions G.

How do we register the information that Lean needs to use to carry out the search? Returning to our group example, we need only make two changes. First, instead of using the structure command to define the group structure, we use the keyword class to indicate that it is a candidate for class inference. Second, instead of defining particular instances with def, we use the keyword instance to register the particular instance with Lean. As with the names of class variables, we are allowed to leave the name of an instance definition anonymous, since in general we intend Lean to find it and put it to use without troubling us with the details.

class group₂ (α : Type*) :=
(mul: α → α → α)
(one: α)
(inv: α → α)
(mul_assoc : ∀ x y z : α, mul (mul x y) z = mul x (mul y z))
(mul_one: ∀ x : α, mul x one = x)
(one_mul: ∀ x : α, mul one x = x)
(mul_left_inv : ∀ x : α, mul (inv x) x = one)

instance {α : Type*} : group₂ (equiv.perm α) :=
{ mul          := λ f g, equiv.trans g f,
  one          := equiv.refl α,
  inv          := equiv.symm,
  mul_assoc    := λ f g h, (equiv.trans_assoc _ _ _).symm,
  one_mul      := equiv.trans_refl,
  mul_one      := equiv.refl_trans,
  mul_left_inv := equiv.self_trans_symm }

The following illustrates their use.

#check @group₂.mul

def my_square {α : Type*} [group₂ α] (x : α) := group₂.mul x x

#check @my_square

section
variables {β : Type*} (f g : equiv.perm β)

example : group₂.mul f g = g.trans f := rfl

example : my_square f = f.trans f := rfl

end

The #check command shows that group₂.mul has an implicit argument [group₂ α] that we expect to be found by class inference, where α is the type of the arguments to group₂.mul. In other words, {α : Type*} is the implicit argument for the type of the group elements and [group₂ α] is the implicit argument for the group structure on α. Similarly, when we define a generic squaring function my_square for group₂, we use an implicit argument {α : Type*} for the type of the elements and an implicit argument [group₂ α] for the group₂ structure.

In the first example, when we write group₂.mul f g, the type of f and g tells Lean that in the argument α to group₂.mul has to be instantiated to equiv.perm β. That means that Lean has to find an element of group₂ (equiv.perm β). The previous instance declaration tells Lean exactly how to do that. Problem solved!

This simple mechanism for registering information so that Lean can find it when it needs it is remarkably useful. Here is one way it comes up. In Lean’s foundation, a data type α may be empty. In a number of applications, however, it is useful to know that a type has at least one element. For example, the function list.head, which returns the first element of a list, can return the default value when the list is empty. To make that work, the Lean library defines a class inhabited α, which does nothing more than store a default value. We can show that the point type is an instance:

instance : inhabited point := { default := ⟨0, 0, 0⟩ }

#check (default : point)

example : ([] : list point).head = default := rfl

The class inference mechanism is also used for generic notation. The expression x + y is an abbreviation for has_add.add x y where—you guessed it—has_add α is a class that stores a binary function on α. Writing x + y tells Lean to find a registered instance of [has_add.add α] and use the corresponding function. Below, we register the addition function for point.

instance : has_add point := { add := point.add }

section
variables x y : point

#check x + y

example : x + y = point.add x y := rfl

end

In this way, we can assign the notation + to binary operations on other types as well.

But we can do even better. We have seen that * can be used in any group, + can be used in any additive group, and both can be used in any ring. When we define a new instance of a ring in Lean, we don’t have to define + and * for that instance, because Lean knows that these are defined for every ring. We can use this method to specify notation for our group₂ class:

instance has_mul_group₂ {α : Type*} [group₂ α] : has_mul α := ⟨group₂.mul⟩

instance has_one_group₂ {α : Type*} [group₂ α] : has_one α := ⟨group₂.one⟩

instance has_inv_group₂ {α : Type*} [group₂ α] : has_inv α := ⟨group₂.inv⟩

section
variables {α : Type*} (f g : equiv.perm α)

#check f * 1 * g⁻¹

def foo: f * 1 * g⁻¹ = g.symm.trans ((equiv.refl α).trans f) := rfl

end

In this case, we have to supply names for the instances, because Lean has a hard time coming up with good defaults. What makes this approach work is that Lean carries out a recursive search. According to the instances we have declared, Lean can find an instance of has_mul (equiv.perm α) by finding an instance of group₂ (equiv.perm α), and it can find an instance of group₂ (equiv.perm α) because we have provided one. Lean is capable of finding these two facts and chaining them together.

The example we have just given is dangerous, because Lean’s library also has an instance of group (equiv.perm α), and multiplication is defined on any group. So it is ambiguous as to which instance is found. In fact, Lean favors more recent declarations unless you explicitly specify a different priority. Also, there is another way to tell Lean that one structure is an instance of another, using the extends keyword. This is how mathlib specifies that, for example, every commutative ring is a ring. You can find more information in a section on class inference in Theorem Proving in Lean.

In general, it is a bad idea to specify a value of * for an instance of an algebraic structure that already has the notation defined. Redefining the notion of group in Lean is an artificial example. In this case, however, both interpretations of the group notation unfold to equiv.trans, equiv.refl, and equiv.symm, in the same way.

As a similarly artificial exercise, define a class add_group₂ in analogy to group₂. Define the usual notation for addition, negation, and zero on any add_group₂ using the classes has_add, has_neg, and has_zero. Then show point is an instance of add_group₂. Try it out and make sure that the additive group notation works for elements of point.

class add_group₂ (α : Type*) :=
(add : α → α → α)
-- fill in the rest

It is not a big problem that we have already declared instances has_add, has_neg, and has_zero for point above. Once again, the two ways of synthesizing the notation should come up with the same answer.

Class inference is subtle, and you have to be careful when using it, because it configures automation that invisibly governs the interpretation of the expressions we type. When used wisely, however, class inference is a powerful tool. It is what makes algebraic reasoning possible in Lean.

6.3. Building the Gaussian Integers

We will now illustrate the use of the algebraic hierarchy in Lean by building an important mathematical object, the Gaussian integers, and showing that it is a Euclidean domain. In other words, according to the terminology we have been using, we will define the Gaussian integers and show that they are an instance of the Euclidean domain structure.

In ordinary mathematical terms, the set of Gaussian integers \(\Bbb{Z}[i]\) is the set of complex numbers \(\{ a + b i \mid a, b \in \Bbb{Z}\}\). But rather than define them as a subset of the complex numbers, our goal here is to define them as a data type in their own right. We do this by representing a Gaussian integer as a pair of integers, which we think of as the real and imaginary parts.

@[ext] structure gaussint := (re : ℤ) (im : ℤ)

We first show that the Gaussian integers have the structure of a ring, with 0 defined to be ⟨0, 0⟩, 1 defined to be ⟨1, 0⟩, and addition defined pointwise. To work out the definition of multiplication, remember that we want the element \(i\), represented by ⟨0, 1⟩, to be a square root of \(-1\). Thus we want

\[\begin{split}(a + bi) (c + di) & = ac + bci + adi + bd i^2 \\ & = (ac - bd) + (bc + ad)i.\end{split}\]

This explains the definition of has_mul below.

instance : has_zero gaussint := ⟨⟨0, 0⟩⟩
instance : has_one gaussint  := ⟨⟨1, 0⟩⟩
instance : has_add gaussint  := ⟨λ x y, ⟨x.re + y.re, x.im + y.im⟩⟩
instance : has_neg gaussint  := ⟨λ x, ⟨-x.re, -x.im⟩⟩
instance : has_mul gaussint  :=
  ⟨λ x y, ⟨x.re * y.re - x.im * y.im, x.re * y.im + x.im * y.re⟩⟩

As noted in Section 6.1, it is a good idea to put all the definitions related to a data type in a namespace with the same name. Thus in the Lean files associated with this chapter, these definitions are made in the gaussint namespace.

Notice that here we are defining the interpretations of the notation 0, 1, +, -, and * directly, rather than naming them gaussint.zero and the like and assigning the notation to those. It is often useful to have an explicit name for the definitions, for example, to use with simp and rewrite.

theorem zero_def : (0 : gaussint) = ⟨0, 0⟩ := rfl
theorem one_def : (1 : gaussint) = ⟨1, 0⟩ := rfl
theorem add_def (x y : gaussint) : x + y = ⟨x.re + y.re, x.im + y.im⟩ := rfl
theorem neg_def (x : gaussint) : -x = ⟨-x.re, -x.im⟩ := rfl
theorem mul_def (x y : gaussint) :
  x * y = ⟨x.re * y.re - x.im * y.im, x.re * y.im + x.im * y.re⟩ := rfl

It is also useful to name the rules that compute the real and imaginary parts, and to declare them to the simplifier.

@[simp] theorem zero_re : (0 : gaussint).re = 0 := rfl
@[simp] theorem zero_im : (0 : gaussint).im = 0 := rfl
@[simp] theorem one_re : (1 : gaussint).re = 1 := rfl
@[simp] theorem one_im : (1 : gaussint).im = 0 := rfl
@[simp] theorem add_re (x y : gaussint) : (x + y).re = x.re + y.re := rfl
@[simp] theorem add_im (x y : gaussint) : (x + y).im = x.im + y.im := rfl
@[simp] theorem neg_re (x : gaussint) : (-x).re = - x.re := rfl
@[simp] theorem neg_im (x : gaussint) : (-x).im = - x.im := rfl
@[simp] theorem mul_re (x y : gaussint) : (x * y).re = x.re * y.re - x.im * y.im := rfl
@[simp] theorem mul_im (x y : gaussint) : (x * y).im = x.re * y.im + x.im * y.re := rfl

It is now surprisingly easy to show that the Gaussian integers are an instance of a commutative ring. We are putting the structure concept to good use. Each particular Gaussian integer is an instance of the gaussint structure, whereas the type gaussint itself, together with the relevant operations, is an instance of the comm_ring structure. The comm_ring structure, in turn, extends the notational structures has_zero, has_one, has_add, has_neg, and has_mul.

If you type instance : comm_ring gaussint := _, click on the light bulb that appears in VS Code, and then ask Lean to fill in a skeleton for the structure definition, you will see a scary number of entries. Jumping to the definition of the structure, however, shows that many of the fields have default definitions that Lean will fill in for you automatically. The essential ones appear in the definition below. In each case, the relevant identity is proved by unfolding definitions, using the ext tactic to reduce the identities to their real and imaginary components, simplifying, and, if necessary, carrying out the relevant ring calculation in the integers.

instance : comm_ring gaussint :=
{ zero := 0,
  one := 1,
  add := (+),
  neg := λ x, -x,
  mul := (*),

  add_assoc := by { intros, ext; simp; ring },
  zero_add := by { intros, ext; simp },
  add_zero := by { intros, ext; simp },
  add_left_neg := by { intros, ext; simp },
  add_comm := by { intros, ext; simp; ring },
  mul_assoc := by { intros, ext; simp; ring },
  one_mul := by { intros, ext; simp },
  mul_one := by { intros, ext; simp },
  left_distrib := by { intros, ext; simp; ring },
  right_distrib := by { intros, ext; simp; ring },
  mul_comm := by { intros, ext; simp; ring } }

Lean’s library defines the class of nontrivial types to be types with at least two distinct elements. In the context of a ring, this is equivalent to saying the the zero is not equal to the one. Since some common theorems depend on that fact, we may as well establish it now.

instance : nontrivial gaussint :=
by { use [0, 1], rw [ne, gaussint.ext_iff], simp }

We will now show that the Gaussian integers have an important additional property. A Euclidean domain is a ring \(R\) equipped with a norm function \(N : R \to \mathbb{N}\) with the following two properties:

  • For every \(a\) and \(b \ne 0\) in \(R\), there are \(q\) and \(r\) in \(R\) such that \(a = bq + r\) and either \(r = 0\) or N(r) < N(b).

  • For every \(a\) and \(b \ne 0\), \(N(a) \le N(ab)\).

The ring of integers \(\Bbb{Z}\) with \(N(a) = |a|\) is an archetypal example of a Euclidean domain. In that case, we can take \(q\) to be the result of integer division of \(a\) by \(b\) and \(r\) to be the remainder. These functions are defined in Lean so that the satisfy the following:

example (a b : ℤ) : a = b * (a / b) + a % b := eq.symm $ int.div_add_mod a b

example (a b : ℤ) : b ≠ 0 → 0 ≤ a % b := int.mod_nonneg a

example (a b : ℤ) : b ≠ 0 → a % b < abs b := int.mod_lt a

In an arbitrary ring, an element \(a\) is said to be a unit if it divides \(1\). A nonzero element \(a\) is said to be irreducible if it cannot be written in the form \(a = bc\) where neither \(b\) nor \(c\) is a unit. In the integers, every irreducible element \(a\) is prime, which is to say, whenever \(a\) divides a product \(bc\), it divides either \(b\) or \(c\). But in other rings this property can fail. In the ring \(\Bbb{Z}[\sqrt{-5}]\), we have

\[6 = 2 \cdot 3 = (1 + \sqrt{-5})(1 - \sqrt{-5}),\]

and the elements \(2\), \(3\), \(1 + \sqrt{-5}\), and \(1 - \sqrt{-5}\) are all irreducible, but they are not prime. For example, \(2\) divides the product \((1 + \sqrt{-5})(1 - \sqrt{-5})\), but it does not divide either factor. In particular, we no longer have unique factorization: the number \(6\) can be factored into irreducible elements in more than one way.

In contrast, every Euclidean domain is a unique factorization domain, which implies that every irreducible element is prime. The axioms for a Euclidean domain imply that one can write any nonzero element as a finite product of irreducible elements. They also imply that one can use the Euclidean algorithm to find a greatest common divisor of any two nonzero elements a and b, i.e.~an element that is divisible by any other common divisor. This, in turn, implies that factorization into irreducible elements is unique up to multiplication by units.

We now show that the Gaussian integers are a Euclidean domain with the norm defined by \(N(a + bi) = (a + bi)(a - bi) = a^2 + b^2\). The Gaussian integer \(a - bi\) is called the conjugate of \(a + bi\). It is not hard to check that for any complex numbers \(x\) and \(y\), we have \(N(xy) = N(x)N(y)\).

To see that this definition of the norm makes the complex numbers a Euclidean domain, only the first property is challenging. Suppose we want to write \(a + bi = (c + di) q + r\) for suitable \(q\) and \(r\). Treating \(a + bi\) and \(c + di\) are complex numbers, carry out the division

\[\frac{a + bi}{c + di} = \frac{(a + bi)(c - di)}{(c + di)(c-di)} = \frac{ac + bd}{c^2 + d^2} + \frac{bc -ad}{c^2+d^2} i.\]

The real and imaginary parts might not be integers, but we can round them to the nearest integers \(u\) and \(v\). We can then express the right-hand size as \((u + vi) + (u' + v'i)\), where \(u' + v'i\) is the part left over. Note that we have \(|u'| \le 1/2\) and \(|v'| \le 1/2\), and hence

\[N(u' + v' i) = (u')^2 + (v')^2 \le 1/4 + 1/4 \le 1/2.\]

Multiplying through by \(c + di\), we have

\[a + bi = (c + di) (u + vi) + (c + di) (u' + v'i).\]

Setting \(q = u + vi\) and \(r = (c + di) (u' + v'i)\), we have \(a + bi = (c + di) q + r\), and we only need to bound \(N(r)\):

\[N(r) = N(c + di)N(u' + v'i) \le N(c + di) \cdot 1/2 < N(c + di).\]

The argument we just carried out requires viewing the Gaussian integers as a subset of the complex numbers. One option for formalizing it in Lean is therefore to embed the Gaussian integers in the complex numbers, embed the integers in the Gaussian integers, define the rounding function from the real numbers to the integers, and take great care to pass back and forth between these number systems appropriately. In fact, this is exactly the approach that is followed in mathlib, where the Gaussian integers themselves are constructed as a special case of a ring of quadratic integers. See the file gaussian_int.lean.

Here we will instead carry out an argument that stays in the integers. This illustrates an choice one commonly faces when formalizing mathematics. Given an argument that requires concepts or machinery that is not already in the library, one has two choices: either formalizes the concepts or machinery needed, or adapt the argument to make use of concepts and machinery you already have. The first choice is generally a good investment of time when the results can be used in other contexts. Pragmatically speaking, however, sometimes seeking a more elementary proof is more efficient.

The usual quotient-remainder theorem for the integers says that for every \(a\) and nonzero \(b\), there are \(q\) and \(r\) such that \(a = b q + r\) and \(0 \le r < b\). Here we will make use of the following variation, which says that there are \(q'\) and \(r'\) such that \(a = b q' + r'\) and \(|r'| \le b/2\). You can check that if the value of \(r\) in the first statement satisfies \(r \le b/2\), we can take \(q' = q\) and \(r' = r\), and otherwise we can take \(q' = q + 1\) and \(r' = r - b\). We are grateful to Heather Macbeth for suggesting the following more elegant approach, which avoids definition by cases. We simply add b / 2 to a before dividing and then subtract it from the remainder.

def div' (a b : ℤ) := (a + b / 2) / b

def mod' (a b : ℤ) := (a + b / 2) % b - b / 2

theorem div'_add_mod' (a b : ℤ) : b * div' a b + mod' a b = a :=
begin
  rw [div', mod'],
  linarith [int.div_add_mod (a + b / 2) b],
end

theorem abs_mod'_le (a b : ℤ) (h : 0 < b): abs (mod' a b) ≤ b / 2 :=
begin
  rw [mod', abs_le],
  split,
  { linarith [int.mod_nonneg (a + b / 2) h.ne'] },
  have := int.mod_lt_of_pos (a + b / 2) h,
  have := int.div_add_mod b 2,
  have := int.mod_lt_of_pos b zero_lt_two,
  linarith
end

Note the use of our old friend, linarith. We will also need to express mod' in terms of div'.

theorem mod'_eq (a b : ℤ) : mod' a b = a - b * div' a b :=
by linarith [div'_add_mod' a b]

We will use the fact that \(x^2 + y^2\) is equal to zero if and only if \(x\) and \(y\) are both zero. As an exercise, we ask you to prove that this holds in any ordered ring.

theorem sq_add_sq_eq_zero {α : Type*} [linear_ordered_ring α] (x y : α) :
  x^2 + y^2 = 0 ↔ x = 0 ∧ y = 0 :=
  sorry

We will put all the remaining definitions and theorems in this section in the gaussint namespace. First, we define the norm function and ask you to establish some of its properties. The proofs are all short.

def norm (x : gaussint) := x.re^2 + x.im^2

@[simp] theorem norm_nonneg (x : gaussint) : 0 ≤ norm x :=
sorry

theorem norm_eq_zero (x : gaussint) : norm x = 0 ↔ x = 0 :=
sorry

theorem norm_pos (x : gaussint) : 0 < norm x ↔ x ≠ 0 :=
sorry

theorem norm_mul (x y : gaussint) : norm (x * y) = norm x * norm y :=
sorry

Next we define the conjugate function:

def conj (x : gaussint) : gaussint := ⟨x.re, -x.im⟩

@[simp] theorem conj_re (x : gaussint) : (conj x).re = x.re := rfl
@[simp] theorem conj_im (x : gaussint) : (conj x).im = - x.im := rfl

theorem norm_conj (x : gaussint) : norm (conj x) = norm x :=
by { simp [norm] }

Finally, we define division for the Gaussian integers with the notation x / y, that rounds the complex quotient to the nearest Gaussian integer. We use our bespoke int.div' for that purpose. As we calculated above, if x is \(a + bi\) and y is \(c + di\), then the real and imaginary parts of x / y are the nearest integers to

\[\frac{ac + bd}{c^2 + d^2} \quad \text{and} \quad \frac{bc -ad}{c^2+d^2},\]

respectively. Here the numerators are the real and imaginary parts of \((a + bi) (c - di)\), and the denominators are both equal to the norm of \(c + di\).

instance : has_div gaussint :=
⟨λ x y, ⟨int.div' (x * conj y).re (norm y), int.div' (x * conj y).im (norm y)⟩⟩

Having defined x / y, We define x % y to be the remainder, x - (x / y) * y. As above, we record the definitions in the theorems div_def and mod_def so that we can use them with simp and rewrite.

instance : has_mod gaussint := ⟨λ x y, x - y * (x / y)⟩

theorem div_def (x y : gaussint) :
  x / y = ⟨int.div' (x * conj y).re (norm y), int.div' (x * conj y).im (norm y)⟩ := rfl

theorem mod_def (x y : gaussint) : x % y = x - y * (x / y) := rfl

These definitions immediately yield x = y * (x / y) + x % y for every x and y, so all we need to do is show that the norm of x % y is less than the norm of y when y is not zero.

We just defined the real and imaginary parts of x / y to be div' (x * conj y).re (norm y) and div' (x * conj y).im (norm y), respectively. Calculating, we have

(x % y) * conj y = (x - x / y * y) * conj y = x * conj y - x * (y * conj j)

The real and imaginary parts of the right-hand side are exactly mod' (x * conj y).re (norm y) and mod' (x * conj y).im (norm y). By the properties of div' and mod', these are guaranteed to be less than or equal to norm y / 2. So we have

norm ((x % y) * conj y) ≤ (norm y / 2)^2 + (norm y / 2)^2 ≤ (norm y / 2) * norm y.

On the other hand, we have

norm ((x % y) * conj y) = norm (x % y) * norm (conj y) = norm (x % y) * norm y.

Dividing through by norm y we have norm (x % y) ≤ (norm y) / 2 < norm y, as required.

This messy calculation is carried out in the next proof. We encourage you to step through the details and see if you can find a nicer argument.

lemma norm_mod_lt (x : gaussint) {y : gaussint} (hy : y ≠ 0) : (x % y).norm < y.norm :=
begin
  have norm_y_pos : 0 < norm y,
    by rwa [norm_pos],
  have : (x % y) * conj y =
    ⟨int.mod' (x * conj y).re (norm y), int.mod' (x * conj y).im (norm y)⟩,
  { rw [mod_def, sub_mul, int.mod'_eq, int.mod'_eq, sub_eq_add_neg, norm, div_def],
    ext; simp; ring },
  have : norm (x % y) * norm y ≤ (norm y / 2) * norm y,
  { conv { to_lhs, rw [←norm_conj y, ←norm_mul, this, norm] },
    simp,
    transitivity 2 * (y.norm / 2)^2,
    { rw [two_mul],
      apply add_le_add;
      { rw [sq_le_sq],
        apply le_trans (int.abs_mod'_le _ _ norm_y_pos),
        apply le_abs_self } },
      rw [pow_two, ←mul_assoc, mul_comm, mul_comm (2 : ℤ)],
      apply mul_le_mul_of_nonneg_left,
      { apply int.div_mul_le, norm_num },
      apply int.div_nonneg (norm_nonneg y), norm_num },
  have : norm (x % y) ≤ norm y / 2 := le_of_mul_le_mul_right this norm_y_pos,
  apply lt_of_le_of_lt this,
  apply int.div_lt_of_lt_mul, { norm_num },
  linarith
end

We are in the home stretch. Our norm function maps Gaussian integers to nonnegative integers. We need a function that maps Gaussian integers to natural numbers, and we obtain that by composing norm with the function int.nat_abs, which maps integers to the natural numbers. The first of the next two lemmas establishes that mapping the norm to the natural numbers and back to the integers does not change the value. The second one re-expresses the fact that the norm is decreasing.

lemma coe_nat_abs_norm (x : gaussint) : (x.norm.nat_abs : ℤ) = x.norm :=
int.nat_abs_of_nonneg (norm_nonneg _)

lemma nat_abs_norm_mod_lt (x y : gaussint) (hy : y ≠ 0) :
  (x % y).norm.nat_abs < y.norm.nat_abs :=
begin
  apply int.coe_nat_lt.1,
  simp only [int.coe_nat_abs, abs_of_nonneg, norm_nonneg],
  apply norm_mod_lt x hy
end

We also need to establish the second key property of the norm function on a Euclidean domain.

lemma not_norm_mul_left_lt_norm (x : gaussint) {y : gaussint} (hy : y ≠ 0) :
  ¬ (norm (x * y)).nat_abs < (norm x).nat_abs :=
begin
  apply not_lt_of_ge,
  rw [norm_mul, int.nat_abs_mul],
  apply le_mul_of_one_le_right (nat.zero_le _),
  apply int.coe_nat_le.1,
  rw [coe_nat_abs_norm],
  exact int.add_one_le_of_lt ((norm_pos _).mpr hy)
end

We can now put it together to show that the Gaussian integers are an instance of a Euclidean domain. We use the quotient and remainder function we have defined. The mathlib definition of a Euclidean domain is more general than the one above in that it allows us to show that remainder decreases with respect to any well-founded measure. Comparing the values of a norm function that returns natural numbers is just one instance of such a measure, and in that case, the required properties are the theorems nat_abs_norm_mod_lt and not_norm_mul_left_lt_norm.

instance : euclidean_domain gaussint :=
{ quotient        := (/),
  remainder       := (%),
  quotient_mul_add_remainder_eq :=
                     λ x y, by {rw [mod_def, add_comm, sub_add_cancel] },
  quotient_zero   := λ x, by { simp [div_def, norm, int.div'], refl },
  r               := measure (int.nat_abs ∘ norm),
  r_well_founded  := measure_wf (int.nat_abs ∘ norm),
  remainder_lt    := nat_abs_norm_mod_lt,
  mul_left_not_lt := not_norm_mul_left_lt_norm,
  .. gaussint.comm_ring }

An immediate payoff is that we now know that, in the Gaussian integers, the notions of being prime and being irreducible coincide.

example (x : gaussint) : irreducible x ↔ prime x :=
principal_ideal_ring.irreducible_iff_prime