6. Structures
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. Defining 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 where
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 := by
ext
repeat' assumption
We can then define particular instances of the Point structure.
Lean provides multiple ways of doing that.
def myPoint1 : Point where
x := 2
y := -1
z := 4
def myPoint2 : Point :=
⟨2, -1, 4⟩
def myPoint3 :=
Point.mk 2 (-1) 4
In the first example, the fields of the structure are named
explicitly.
The function Point.mk referred to in the definition of myPoint3
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' where 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 where
x := a.x + b.x
y := a.y + b.y
z := a.z + b.z
#check add myPoint1 myPoint2
#check myPoint1.add myPoint2
end Point
#check Point.add myPoint1 myPoint2
#check myPoint1.add myPoint2
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 := by
rw [add, add]
ext <;> dsimp
repeat' apply add_comm
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 addAlt and addAlt' 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, and structural eta-reduction makes
this alternative definitionally equivalent, it can make things less convenient in later proofs.
In particular, rw [addAlt] leaves us with a messier goal view containing a match statement.
def addAlt : Point → Point → Point
| Point.mk x₁ y₁ z₁, Point.mk x₂ y₂ z₂ => ⟨x₁ + x₂, y₁ + y₂, z₁ + z₂⟩
def addAlt' : Point → Point → Point
| ⟨x₁, y₁, z₁⟩, ⟨x₂, y₂, z₂⟩ => ⟨x₁ + x₂, y₁ + y₂, z₁ + z₂⟩
theorem addAlt_x (a b : Point) : (a.addAlt b).x = a.x + b.x := by
rfl
theorem addAlt_comm (a b : Point) : addAlt a b = addAlt b a := by
rw [addAlt, addAlt]
-- the same proof still works, but the goal view here is harder to read
ext <;> dsimp
repeat' apply 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) := by
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) := by
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 StandardTwoSimplex where
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 swapXy (a : StandardTwoSimplex) : StandardTwoSimplex
where
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 have added the phrase noncomputable section
at the beginning of this file in order to use division on the real numbers.
noncomputable section
def midpoint (a b : StandardTwoSimplex) : StandardTwoSimplex
where
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.
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 weightedAverage (lambda : Real) (lambda_nonneg : 0 ≤ lambda) (lambda_le : lambda ≤ 1)
(a b : StandardTwoSimplex) : StandardTwoSimplex :=
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 BigOperators
structure StandardSimplex (n : ℕ) where
V : Fin n → ℝ
NonNeg : ∀ i : Fin n, 0 ≤ V i
sum_eq_one : (∑ i, V i) = 1
namespace StandardSimplex
def midpoint (n : ℕ) (a b : StandardSimplex n) : StandardSimplex n
where
V i := (a.V i + b.V i) / 2
NonNeg := by
intro i
apply div_nonneg
· linarith [a.NonNeg i, b.NonNeg i]
norm_num
sum_eq_one := by
simp [div_eq_mul_inv, ← Finset.sum_mul, Finset.sum_add_distrib,
a.sum_eq_one, b.sum_eq_one]
field_simp
end StandardSimplex
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, IsLinear, bundles together
the two components of linearity.
structure IsLinear (f : ℝ → ℝ) where
is_additive : ∀ x y, f (x + y) = f x + f y
preserves_mul : ∀ x c, f (c * x) = c * f x
section
variable (f : ℝ → ℝ) (linf : IsLinear 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 IsLinear can be defined with a simple and.
def Point'' :=
ℝ × ℝ × ℝ
def IsLinear' (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 StandardTwoSimplex' :=
{ p : ℝ × ℝ × ℝ // 0 ≤ p.1 ∧ 0 ≤ p.2.1 ∧ 0 ≤ p.2.2 ∧ p.1 + p.2.1 + p.2.2 = 1 }
def StandardSimplex' (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 StdSimplex := Σ n : ℕ, StandardSimplex n
section
variable (s : StdSimplex)
#check s.fst
#check s.snd
#check s.1
#check s.2
end
Given s : StdSimplex, the first component s.fst is a natural
number, and the second component is an element of the corresponding
simplex StandardSimplex 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.
A partially ordered set consists of a set \(P\) and a binary relation \(\le\) on \(P\) that is transitive and reflexive.
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.
A lattice is a partially ordered set with meets and joins.
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.
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\).
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\).
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*) where
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
inv_mul_cancel : ∀ 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_inv_cancel to inv_mul_cancel
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 GroupCat structure that is equivalent to
the following:
structure Group₁Cat where
α : Type*
str : Group₁ α
The Mathlib version is found in Mathlib.Algebra.Category.GroupCat.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.toFun from α to β,
the inverse function f.invFun from β to α,
and two properties that specify these functions are indeed inverse
to one another.
variable (α β γ : Type*)
variable (f : α ≃ β) (g : β ≃ γ)
#check Equiv α β
#check (f.toFun : α → β)
#check (f.invFun : β → α)
#check (f.right_inv : ∀ x : β, f (f.invFun x) = x)
#check (f.left_inv : ∀ x : α, f.invFun (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 .toFun
and have Lean insert it for us.
example (x : α) : (f.trans g).toFun x = g.toFun (f.toFun 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 permGroup {α : Type*} : Group₁ (Equiv.Perm α)
where
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
inv_mul_cancel := Equiv.self_trans_symm
In fact, Mathlib defines exactly this Group structure on Equiv.Perm α
in the file GroupTheory.Perm.Basic.
As always, you can hover over the theorems used in the definition of
permGroup 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
AddGroup (the structure underlying additive groups). 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 AddGroup₁ 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 AddGroup₁ structure on Point.
structure AddGroup₁ (α : Type*) where
(add : α → α → α)
-- fill in the rest
@[ext]
structure Point where
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 addGroupPoint : AddGroup₁ 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 α.
variable {α : 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_inv_cancel, 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.
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.
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.
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*) where
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
inv_mul_cancel : ∀ x : α, mul (inv x) x = one
instance {α : Type*} : Group₂ (Equiv.Perm α) where
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
inv_mul_cancel := Equiv.self_trans_symm
The following illustrates their use.
#check Group₂.mul
def mySquare {α : Type*} [Group₂ α] (x : α) :=
Group₂.mul x x
#check mySquare
section
variable {β : Type*} (f g : Equiv.Perm β)
example : Group₂.mul f g = g.trans f :=
rfl
example : mySquare 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.headI, 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 where default := ⟨0, 0, 0⟩
#check (default : Point)
example : ([] : List Point).headI = default :=
rfl
The class inference mechanism is also used for generic notation.
The expression x + y is an abbreviation for Add.add x y
where—you guessed it—Add α is a class that stores
a binary function on α.
Writing x + y tells Lean to find a registered instance of [Add.add α]
and use the corresponding function.
Below, we register the addition function for Point.
instance : Add Point where add := Point.add
section
variable (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 hasMulGroup₂ {α : Type*} [Group₂ α] : Mul α :=
⟨Group₂.mul⟩
instance hasOneGroup₂ {α : Type*} [Group₂ α] : One α :=
⟨Group₂.one⟩
instance hasInvGroup₂ {α : Type*} [Group₂ α] : Inv α :=
⟨Group₂.inv⟩
section
variable {α : 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
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 Section 7 and 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 AddGroup₂ in analogy to Group₂.
Define the usual notation for addition, negation, and zero
on any AddGroup₂
using the classes Add, Neg, and Zero.
Then show Point is an instance of AddGroup₂.
Try it out and make sure that the additive group notation works for
elements of Point.
class AddGroup₂ (α : Type*) where
add : α → α → α
-- fill in the rest
It is not a big problem that we have already declared instances
Add, Neg, and 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 where
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
This explains the definition of Mul below.
instance : Zero GaussInt :=
⟨⟨0, 0⟩⟩
instance : One GaussInt :=
⟨⟨1, 0⟩⟩
instance : Add GaussInt :=
⟨fun x y ↦ ⟨x.re + y.re, x.im + y.im⟩⟩
instance : Neg GaussInt :=
⟨fun x ↦ ⟨-x.re, -x.im⟩⟩
instance : Mul GaussInt :=
⟨fun 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 CommRing structure. The CommRing structure, in turn,
extends the notational structures Zero, One, Add,
Neg, and Mul.
If you type instance : CommRing 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.
A special case are nsmul and zsmul which should be ignored for now
and will be explained in the next chapter.
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. Note that we could easily avoid repeating all this code, but
this is not the topic of the current discussion.
instance instCommRing : CommRing GaussInt where
zero := 0
one := 1
add := (· + ·)
neg x := -x
mul := (· * ·)
nsmul := nsmulRec
zsmul := zsmulRec
add_assoc := by
intros
ext <;> simp <;> ring
zero_add := by
intro
ext <;> simp
add_zero := by
intro
ext <;> simp
neg_add_cancel := by
intro
ext <;> simp
add_comm := by
intros
ext <;> simp <;> ring
mul_assoc := by
intros
ext <;> simp <;> ring
one_mul := by
intro
ext <;> simp
mul_one := by
intro
ext <;> simp
left_distrib := by
intros
ext <;> simp <;> ring
right_distrib := by
intros
ext <;> simp <;> ring
mul_comm := by
intros
ext <;> simp <;> ring
zero_mul := by
intros
ext <;> simp
mul_zero := by
intros
ext <;> simp
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 that 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.ediv_add_emod a b)
example (a b : ℤ) : b ≠ 0 → 0 ≤ a % b :=
Int.emod_nonneg a
example (a b : ℤ) : b ≠ 0 → a % b < |b| :=
Int.emod_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
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 Gaussian integers 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
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 side 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
Multiplying through by \(c + di\), we have
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)\):
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 GaussianInt.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 := by
rw [div', mod']
linarith [Int.ediv_add_emod (a + b / 2) b]
theorem abs_mod'_le (a b : ℤ) (h : 0 < b) : |mod' a b| ≤ b / 2 := by
rw [mod', abs_le]
constructor
· linarith [Int.emod_nonneg (a + b / 2) h.ne']
have := Int.emod_lt_of_pos (a + b / 2) h
have := Int.ediv_add_emod b 2
have := Int.emod_lt_of_pos b zero_lt_two
revert this; intro this -- FIXME, this should not be needed
linarith
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*} [LinearOrderedRing α] (x y : α) :
x ^ 2 + y ^ 2 = 0 ↔ x = 0 ∧ y = 0 := by
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 := by
sorry
theorem norm_eq_zero (x : GaussInt) : norm x = 0 ↔ x = 0 := by
sorry
theorem norm_pos (x : GaussInt) : 0 < norm x ↔ x ≠ 0 := by
sorry
theorem norm_mul (x y : GaussInt) : norm (x * y) = norm x * norm y := by
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
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 : Div GaussInt :=
⟨fun 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 : Mod GaussInt :=
⟨fun 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 * (y * conj y)
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.
theorem norm_mod_lt (x : GaussInt) {y : GaussInt} (hy : y ≠ 0) :
(x % y).norm < y.norm := by
have norm_y_pos : 0 < norm y := by rwa [norm_pos]
have H1 : x % y * conj y = ⟨Int.mod' (x * conj y).re (norm y), Int.mod' (x * conj y).im (norm y)⟩
· ext <;> simp [Int.mod'_eq, mod_def, div_def, norm] <;> ring
have H2 : norm (x % y) * norm y ≤ norm y / 2 * norm y
· calc
norm (x % y) * norm y = norm (x % y * conj y) := by simp only [norm_mul, norm_conj]
_ = |Int.mod' (x.re * y.re + x.im * y.im) (norm y)| ^ 2
+ |Int.mod' (-(x.re * y.im) + x.im * y.re) (norm y)| ^ 2 := by simp [H1, norm, sq_abs]
_ ≤ (y.norm / 2) ^ 2 + (y.norm / 2) ^ 2 := by gcongr <;> apply Int.abs_mod'_le _ _ norm_y_pos
_ = norm y / 2 * (norm y / 2 * 2) := by ring
_ ≤ norm y / 2 * norm y := by gcongr; apply Int.ediv_mul_le; norm_num
calc norm (x % y) ≤ norm y / 2 := le_of_mul_le_mul_right H2 norm_y_pos
_ < norm y := by
apply Int.ediv_lt_of_lt_mul
· norm_num
· linarith
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.natAbs, 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.
theorem coe_natAbs_norm (x : GaussInt) : (x.norm.natAbs : ℤ) = x.norm :=
Int.natAbs_of_nonneg (norm_nonneg _)
theorem natAbs_norm_mod_lt (x y : GaussInt) (hy : y ≠ 0) :
(x % y).norm.natAbs < y.norm.natAbs := by
apply Int.ofNat_lt.1
simp only [Int.natCast_natAbs, abs_of_nonneg, norm_nonneg]
apply norm_mod_lt x hy
We also need to establish the second key property of the norm function on a Euclidean domain.
theorem not_norm_mul_left_lt_norm (x : GaussInt) {y : GaussInt} (hy : y ≠ 0) :
¬(norm (x * y)).natAbs < (norm x).natAbs := by
apply not_lt_of_ge
rw [norm_mul, Int.natAbs_mul]
apply le_mul_of_one_le_right (Nat.zero_le _)
apply Int.ofNat_le.1
rw [coe_natAbs_norm]
exact Int.add_one_le_of_lt ((norm_pos _).mpr hy)
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
natAbs_norm_mod_lt and not_norm_mul_left_lt_norm.
instance : EuclideanDomain GaussInt :=
{ GaussInt.instCommRing with
quotient := (· / ·)
remainder := (· % ·)
quotient_mul_add_remainder_eq :=
fun x y ↦ by simp only; rw [mod_def, add_comm] ; ring
quotient_zero := fun x ↦ by
simp [div_def, norm, Int.div']
rfl
r := (measure (Int.natAbs ∘ norm)).1
r_wellFounded := (measure (Int.natAbs ∘ norm)).2
remainder_lt := natAbs_norm_mod_lt
mul_left_not_lt := not_norm_mul_left_lt_norm }
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 :=
irreducible_iff_prime