We report on a formalisation experiment where excerpts from an algebra textbook are compared to their translation into formal texts of the Isabelle/Isar prover, and where an attempt is made in the formal text to stick as closely as possible with the structure of the informal counterpart. The purpose of the exercise is to gain understanding on how adequately a modern algebra text can be represented using the module facilities of Isabelle. Our initial results are promising.
We study an informal mathematical text by translating it to a formal document in the Isabelle/Isar language [17]. Our motivation for this exercise is twofold:
Locales are an extension of Isabelle’s Isar proof language [17] by means for manipulating “knowledge containers” or modules, which were designed for dealing with algebraic structures. The central concept is the locale, a theory functor that maps parameters and a specification to derived operations (that is, operations whose definitions involve the parameters) and theorems.
A locale declaration is of the form
locale n = fixes y + assumes a1 : A1 : : : aj : Aj where y are the parameters and A1 ^ : : : ^ Aj is the specification. The Ai are versions of the user input where free variables except parameters are universally closed. For example, a locale for groups may be declared like this: locale group = fixes G and composition (infixl " " 70) and unit ("1") assumes assoc: "[[a 2 G; b 2 G; c 2 G]] =) (a b) and : : : c = a (b c)" Note that types, in particular types of the parameters, may be left implicit. They are inferred automatically.2 Operations and theorems may be added to n in context blocks :
context n begin : : : end These commands are available in context blocks: definition c where c
theorem b : B abbreviation c where c t t The first two are straightforward: definition declares a new operation symbol with defining equation c t and theorem introduces a theorem B named b; abbreviation also adds a new operation symbol, but in contrast to definitions, the equation is unfolded while parsing and folded while printing terms. This is useful for providing concrete syntax for existing concepts. Declarations in a context block are persistent — that is, they are present when the context is visited again.
Locales are hierarchic and a graph of interdependent locales is maintained by the system. Dependencies may be given when declaring a locale by inserting a locale expression before the fixes and assumes clauses,
locale n = expr + : : : ; or between existing locales through sublocale n
expr rewrites hproofi: 2 While inferred types may involve type classes, locales do not rely on them. An expression is a sequence of locale instances followed by an optional for clause:
I1 + : : : + Ik for x Locale instances Ii are qualified and are either positional or by name. The positional instance qi : ni ti denotes locale ni with parameters, in the order of declaration, instantiated by the terms ti. Likewise the named instance ni where xi = ti denotes ni with parameters occurring in xi instantiated by the ti. In a locale declaration the terms ti are over the x from the for clause, which are (together with the y from the fixes clause) parameters of the declared locale n. In a sublocale declaration the ti are over the parameters from the target locale n. The qualifier qi of an instance Ii is optional and, if present, qualifies symbols of derived operations and theorem names of the instance.
The expression in a locale declaration denotes locale instances that are imported to the declared locale. That is, the specifications of the imported instances contribute to the specifications of the declared locale, and their definitions and theorems are available in its body. Here is a locale declaration involving an expression: locale abelian_group = group G composition unit for G and composition (infixl " " 70) and unit ("1") + assumes comm: "[[a 2 G; b 2 G]] =) a b 2 G" As a notational convenience parameters from instantiated locales may be implicitly added to the for clause by omitting their instantiation. This is convenient when constructing linear locale hierarchies. For example the above declaration may be abbreviated to locale abelian_group = group +
assumes comm: "[[a 2 G; b 2 G]] =) a b 2 G"
The sublocale command enables changing the locale hierarchy. It is
implemented via theory interpretation. Changes are only possible if they are implied
by the specification of the involved locales and must be supported by proofs. The
optional rewrites clause is of the form where eq1 : : : eqm and lets one change
derived operations of the instantiated locales through rewrite rules eqi. In
combination with instantiation they provide signature morphisms [
It is important to note that locales are extra-logical. That is, the functors they represent are not encoded in Isabelle’s logic. However, each locale is accompanied by a locale predicate n which reflects the specification of n in the logic. 3
We study Jacobson’s presentation of monoids, groups and rings and the
congruence relations defined over these structures. For groups and rings congruences can
be characterised by working modulo suitable substructures: normal subgroups in
the case of groups, and ideals for rings. In the sequel, excerpts from Jacobson’s
text [
Preliminaries Fundamental to congruences are equivalence relations over sets and the induced partitions of the sets into equivalence classes:
A relation E on a set S is called an equivalence relation if the following conditions hold for any a, b, c, in S: 1. aEa (reflexive property).
If a 2 S we let aE (or simply a) = fb 2 SjbEag. We call aE the equivalence class (relative to E or E-equivalence class) determined by a.
If E is an equivalence relation, the associated partition = faja 2 Sg is called the quotient set of S relative to the relation E. We shall usually denote as S=E. [11, p 11f] The translation to a locale is straightforward. Set and equivalence relation are parameters of the equivalence locale, class and quotient set derived operations. locale equivalence = fixes S and E assumes carrier: "E S S" and refl: "a 2 S =) (a, a) 2 E" and sym: "(a, b) 2 E =) (b, a) 2 E" and trans: "[[(a, b) 2 E; (b, c) 2 E]] =) (a, c) 2 E" begin definition "class" where "class = ( a 2 S. {b 2 S. (b, a) 2 E})" definition "Quot" where "Quot = {class a | a. a 2 S}" end 3.2
Groups Jacobson’s base for the hierarchy of group structures are monoids: Definition 1.1 A monoid is a triple (M; p; 1) in which M is a nonvacuous set, p is an associative binary composition (or product) in M , and 1 is an element of M such that p(1; a) = a = p(a; 1) for all a 2 M . [11, p 28] It is convenient to split the closedness properties (of p being a composition in M and 1 2 M ) and the algebraic laws into two locales because closure is also part of the definition of submonoid.
locale monoid_closed =
fixes M and composition (infixl " " 70) and unit ("1")
assumes composition_closed: "[[a 2 M; b 2 M]] =) a
and unit_closed: "1 2 M"
locale monoid = monoid_closed +
assumes assoc: "[[a 2 M; b 2 M; c 2 M]] =) (a
and left_unit: "a 2 M =) 1 a = a"
and right_unit: "a 2 M =) a 1 = a"
begin
b)
c = a
(b
c)"
The locales have individual parameters for set and operations while according
to Jacobson a monoid is a triple. While it is possible to use a single locale
parameter for the entire algebraic structure (preferably using records [
In the context of monoids the notions of submonoid, invertible element and inverse are defined:
If M is a monoid, a subset N of M is called a submonoid of M if N contains 1 and N is closed under the product in M , that is, n1n2 2 N for every ni 2 N . [11, p 29] An element of a monoid M is said to be invertible (or a unit ) if there exists a v in M such that uv = 1 = vu: (3) If v0 also satisfies uv0 = 1 = v0u then v0 = (vu)v0 = v(uv0) = v. Hence v satisfying (3) is unique. We call this the inverse of u and write v = u 1. [11, p 31] The translation of these concepts is straightforward, but note the use of the locale predicate monoid_closed in the definition of submonoid: definition submonoid where "submonoid N K !
N K ^ monoid_closed N composition unit" definition inverses
where "[[u 2 M; v 2 M]] =) inverses u v ! u v = 1 ^ v definition invertible
where "u 2 M =) invertible u ! (9 v 2 M. inverses u v)" definition inverse
where "u 2 M =) inverse u = (THE v. v 2 M ^ inverses u v)" end u = 1" In the group definition found in many textbooks, the inverse is a parameter. For Jacobson the inverse is a derived operation.
Definition 1.2 A group G (or (G; p; 1)) is a monoid all of whose elements are invertible. Based on the previously defined predicate invertible the locale for groups is declared thus: locale group = monoid G composition unit for G and composition (infixl " " 70) and unit ("1") + assumes "a 2 G =) invertible a" Jacobson defines subgroups in the context of monoids, not just for groups.
We shall call a submonoid of a monoid M (in particular, of a group) a subgroup if, regarded as a monoid, it is a group. [11, p 31] The translation again involves a locale predicate, namely group. context monoid begin definition subgroup where "subgroup H K !
submonoid H K ^ group H composition unit" end Commutative structures are required later for rings and are introduced now.
If ab = ba in M then a and b are said to commute and if this happens for all a and b in M then M is called a commutative monoid. Commutative groups are generally called abelian groups after Niels Abel, . . . . [11, p 40] The corresponding locales are declared using short notation omitting the for clause.
locale commutative_monoid = monoid +
assumes comm: "[[a 2 M; b 2 M]] =) a b 2 M" locale abelian_group =
group + commutative_monoid G composition unit Next Jacobson introduces cosets. These will later be identified as the elements of the factor group, which is a group obtained through a particular equivalence relation.
it is clear that its HL(G)-orbit is
Hx = fhxjh 2 Hg: (23) . . . . Accordingly, we shall . . . call Hx the right coset of x relative to H. . . . . The orbit of x in this case is xH = fxhjh 2 Hg and this is called the left coset of x relative to H. [11, p 52f] Jacobson constructs right cosets as orbits of the transformation group HL(G) of left translations x ! hx in G for h 2 H. Since the properties of cosets derived from this construction are not relevant in the subsequent discussion, we use his equation 23 as definition. Likewise for left cosets.
context group begin definition Right_Coset (infixl "| " 70)
where "H | x = {h x | h. h 2 H}" definition Left_Coset (infixl " |" 70)
where "x | H = {x h | h. h 2 H}" end Jacobson now introduces congruences in monoids. Composition and unit are lifted to congruence classes, obtaining the quotient monoid.
Definition 1.4 Let (M; ; 1) be a monoid. A congruence (or congruence relation) in M is an equivalence relation in M such that for any a, a0, b, b0 such that a a0 and b b0 one has ab a0b0. (In other words, congruences are equivalence relations which can be multiplied.)
Let be a congruence in the monoid M and consider the quotient set M = M= of M relative to . . . . . Since congruences can be multiplied it is clear in the general case that, if a = a0 and b = b0, then ab = a0b0. Hence
(a; b) ! ab is a well-defined map of M M into M ; that is, this is a binary composition on M . We denote this again as , and we shall now show that (M ; ; 1) is a monoid. . . . . The monoid (M ; ; 1) is called the quotient monoid of M relative to the congruence . [11, p 54f] In the translation to Isabelle we call the conguence relation E. The quotient set is Quot, lifted composition is class_composition and for matters of symmetry lifted unit class_unit.
locale monoid_congruence = monoid + equivalence where S = M + assumes cong:
"[[(a, a’) 2 E; (b, b’) 2 E]] =) (a b, a’ b’) 2 E" begin definition "class_composition = ( X 2 Quot. Y 2 Quot.
THE Z. 9 x 2 X. 9 y 2 Y. Z = class (x y))" definition "class_unit = class 1" end That the quotient set is again a monoid is expressed concisely with a sublocale declaration. We declare a new locale equivalent to monoid_congruence so that the current state of the latter remains available.
locale quotient_monoid = monoid_congruence sublocale quotient_monoid
quotient!: monoid Quot class_composition class_unit hproof i Next Jacobson considers congruences on groups.
We can say a good deal more if M = G is a group and is a congruence on G. In the first place, in this case the quotient monoid (G; ; 1) is a group since aa 1 = 1 = a 1a. Hence every a is invertible and its inverse is a 1. [11, p 55] The corresponding constructions in Isabelle are analogous to those for monoids. Notably the sublocale declaration now involves a rewrite clause for mapping the inverse operation of the quotient group to class_inverse.
locale group_congruence = group + monoid_congruence where M = G begin definition "class_inverse =
( X 2 Quot. THE Y. 9 x 2 X. Y = class (inverse x))" end locale quotient_group = group_congruence sublocale quotient_group quotient!: group Quot class_composition class_unit where "quotient.inverse = class_inverse" hproof i Now follows the main result for congruences on groups: the factor group induced by a normal subgroup. First comes the definition of normal, then the main theorem.
Definition 1.5 A subgroup K of a group G is said to be normal . . . if g 1kg 2 K for every g 2 G and k 2 K. context group begin definition normal where "normal H K !
subgroup H K ^ (8 k 2 K. 8 h 2 H. inverse k end h k 2 H)" Theorem 1.6 Let G be a group and a congruence on G. Then the congruence class K = 1 of the unit is a normal subgroup of G and for any g 2 G, g = Kg = gK, the right or left coset of g relative to K. Conversely let K be any normal subgroup of G, then defined by: a b (mod K) if a 1b 2 K is a congruence relation in G whose associated congruence classes are the left (or right) cosets gK. This theorem consists of two parts. The first is about arbitrary group congruences.
context group_congruence begin theorem "normal class_unit G" hproof i theorem "g 2 G =) class g = class_unit | g" hproof i theorem "g 2 G =) class g = g | class_unit" hproof i end In the second part, a congruence relation is constructed from a normal subgroup K, and the classes are identified as cosets. We call the corresponding locale factor_group since the factor group will be defined in this context as well. locale factor_group = group +
fixes K assumes normal: "normal K G" begin definition "Cong = {(x, y). inverse x y 2 K}" theorem "monoid_congruence G op 1 Cong" hproof i theorem "g 2 G =) equivalence.class G Cong g = K | x" hproof i theorem "g 2 G =) equivalence.class G Cong g = x | K" hproof i end Finally Jacobson identifies the factor group.
We shall now write G=K for G = G=K (mod K) and call this the factor group (or quotient group) of G relative to the normal subgroup K. By definition, the product in G=K is
(gK)(hK) = ghK;
K = 1K is the unit, and the inverse of gK is g 1K.
This is again expressed with a sublocale declaration.
sublocale factor_group quotient_group G composition unit Cong where "class_composition = ( X 2 Quot. Y 2 Quot.
THE Z. 9 g 2 X. 9 h 2 Y. Z = g h | K)" and "class_unit = K" and "class_inverse = ( X 2 Quot.
THE Y. 9 g 2 X. Z = inverse g | K)" hproof i The last result on groups presented here will be needed when studying ideals, which give rise to congruences on rings, such as normal subgroups do for groups: It is clear from the definition that any subgroup of an abelian group is normal. [11, p 57] (26) context abelian_group begin lemma "subgroup H K =) normal H K" hproof i end We are now ready to turn to rings. 3.3
Rings These are built upon groups, and for congruences on rings much of the constructions for groups is reused.
Definition 2.1 A ring is a structure consisting of a non-vacuous set R together with two binary compositions +, in R and two distinguished elements 0; 1 2 R such that 1. (R; +; 0) is an abelian group. 2. (R; ; 1) is a monoid. 3. The distributive laws D a(b + c) = ab + ac (b + c)a = ba + ca hold for all a; b; c 2 R. This definition translates directly to locales. Since the additive inverse of a will be donoted by a and a + ( b) by a b this syntax is introduced here as well. The translation of the notions of subring and congruence into locales is equally simple.
A subset S of a ring R is a subring if S is a subgroup of the additive group and also a submonoid of the multiplicative monoid of R. [11, p 87] definition subring where "subring S T !
additive.subgroup S T ^ multiplicative.submonoid S T" end We define a congruence in a ring to be a relation in R which is a congruence for the additive group (R; +; 0) and the multiplicative monoid (R; ; 1). [11, p 101] locale ring_congruence = ring + additive: group_congruence R addition zero E + multiplicative: monoid_congruence R multiplication one E for E Next Jacobson gives notions for the quotient set and its operations.
Hence is an equivalence relation such that a a0 and b b0 imply a + b a0 + b0 and ab a0b0. Let a denote the congruence class of a 2 R and let R be the quotient set. As we have seen in section 1.5, we have binary compositions + and in R defined by a + b = a + b, a b = ab. [11, p 101] In the translation the quotient set remains Quot. Notation for the operations is as follows: context ring_congruence begin abbreviation "class_addition abbreviation "class_zero abbreviation
"class_multiplication abbreviation "class_one end
additive.class_composition" additive.class_unit" multiplicative.class_composition" multiplicative.class_unit" As with monoids and groups the quotient set and operations give rise to a ring.
These define the group (R; +; 0) and the monoid (R; ; 1). We also have a(b + c) = a(b + c) = a(b + c) = ab + ac = ab + ac = ab + ac: Similarly, (b + c)a = ba + ca. Hence (R; +; ; 0; 1) is a ring which we shall call a quotient (or difference) ring of R. [11, p 101] locale quotient_ring = ring_congruence sublocale quotient_ring quotient!: ring Quot class_addition class_zero
class_multiplication class_one hproof i Coset and ideal are the analog for left coset and normal subgroup.
We recall that the congruences in (R; +; 0) are obtained from the subgroups I (necessarily normal since (R; +) is commutative) by defining a b if a b 2 I. Then the congruence class a is the coset a + I. . . . . We now give the following Definition 2.2 If R is a ring, an ideal I of R is a subgroup of the additive group such that for any a 2 R and b 2 I, ab and ba 2 I. context ring begin abbreviation Coset (infixl "+|" 65) where "Coset definition ideal where "ideal I R’ !
additive.subgroup I R’ ^ (8 a 2 R’. 8 b 2 I. a end
Our results show that congruences in a ring R are obtained from ideals I of R by defining a a0 if a a0 2 I. The corresponding quotient ring will be denoted as R=I and will be called quotient ring of R with respect to the ideal I. The elements of R=I are the cosets a + I and the addition and multiplication in R=I are defined by (a + I) + (b + I) = (a + b) + I (a + I)(b + I) = ab + I (17) Jacobson’s exposition of basic algebra is highly polished. Identifying the sections that lead to factor group and quotient monoid with respect to an ideal respectively required scanning a fairly large body of mathematical text that stretches over about 100 pages, and in which the foundations for much more group and ring theory are layed out than what is considered here. As an experienced author Jacobson takes care to introduce notions in a manner that facilitates reuse and avoids repetition. Monoid and group are the foundations for many concepts, and group is defined as an extension of monoid. Likewise congruence on a monoid is based on equivalence and is extended to congruence on a group. The quotient monoid induced by a congruence is identified and similarly the quotient group. The factor group is obtained from the quotient group of the congruence implied by a normal subgroup.
The concepts around rings are derived from the related concepts for the
additive group and multiplicative monoid. This concerns the definition of ring
itself and the congruence on a ring. As for groups the quotient ring induced by
a congruence is identified. The definition of the congruence relation f(a; b)ja
b 2 Ig from the ideal I is seemingly a duplication of the related definition
f(a; b)ja 1b 2 Kg for groups, but in fact the underlying concepts of normal
subgroup and ideal differ.
The main motivation for translating this corpus of mathematics to a formal proof
document in Isabelle is to understand whether the reuses employed by Jacobson
could be reflected with locales in an adequate fashion. Of course, we are not the
first to formalise these particular pieces of group and ring theory. Incidentally,
already Kammüller [
Definitions of algebraic structures (with associated derived operations and theorems) are translated to locale declarations. Inheritance is achieved through imported locale expressions. Other definitions such as those of subgroups, normal subgrups or ideals simply become definitions in appropriate contexts. Theorems that relate algebraic structures to each other are expressed with sublocale declarations. The quotient structures are notable examples. The morphisms available with locales are sufficiently expressive for declaring dependencies to the contained structures in quotient_monoid, quotient_group and quotient_ring. Likewise for the locales factor_group and quotient_ring_wrt_ideal. All in all the formal text contains no repetitions that would not also be present in the informal text.4 Occasionally, the choice in the informal text as to how a certain concept be introduced is surprising. As one example, subgroups are considered substructures of monoids not groups [11, p 31]. Clearly, utility of a definition is given priority over uniformity. Another example, which is not part of the study in Section 3, concerns homomorphisms on monoids. Jacobson gives this definition: Definition 1.6 If M and M 0 are monoids, then a map is called a homomorphism if of M into M 0 (ab) = (a) (b); (1) = 10; a; b 2 M: If M 0 is a group the second condition is superfluous. For, if the first holds, we have (1) = (12) = (1)2 and multiplying by (1) 1 we obtain 10 = (1). [11, p 58f] 3 But he did not have an analog to the sublocale command available. 4 The formal text is almost as succinct as the informal text, but while we assume that repetitions will be also avoided for proofs, we do not expect the succinctness to carry over.
The second part is easily overlooked, as, so it seems, by authors involved in the MathScheme project, who in the context of a vector space homomorphism h conjecture that h(0) = 00 and similar properties are “obvious” axioms frequently omitted by textbooks [5, Section 4.4], while in fact it is implied by the target structure being an additive group. With locales the definition can be translated thus: locale monoid_map = map M M’ + source: monoid M composition unit + target: monoid M’ composition’ unit’ for and M and composition (infix " " 70) and unit ("1")
and M’ and composition’ (infix " ’’" 70) and unit’ ("1’’") locale monoid_homomorphism = monoid_map + assumes "[[a 2 M; b 2 M]] =) a ’ b =
and " 1 = 1’" locale monoid_homomorphism’ = monoid_map + target: group M’ composition’ unit’ + assumes "[[a 2 M; b 2 M]] =) a ’ b = (a
b)" (a b)" The sublocale command then enables relating these locales to each other: sublocale monoid_homomorphism’
monoid_homomorphism hproof i That it, it is shown that the left hand side implies the right. 5
Translating informal mathematics from a textbook to a formal document processable by a mechanical reasoning system turned out to be an insightful exercise. Even without producing proofs it required studying the text with scrutiny, forcing attention to both detail and high-level connections.
We found that we could express the relations between algebraic structures
in Jacobson’s text well, both in definitions and theorems. This is the case even
where constructions are not uniform — for example, subgroups being defined
for monoids. Linguistic features that identify modularity do not stand out in
the text, except that algebraic structures are denoted by tuples. The amount of
mathematics that was formalised here is very small, but sizable formalisations
have been based on locales, for example a proof of the Basic Perturbation Lemma
in homological algebra [
Of course, proof assistants other than Isabelle provide means for modular
reasoning as well and have been used for formalising abstract algebra. The most
remarkable is perhaps the Mizar system and its library, abstracts of which have
been published since 1990 in Formalized Mathematics, an online journal which
to date has published twenty volumes of mechanically checked mathematics of
various areas [
In spirit our exercise follows Avigad’s reflections on understanding proofs [