Algebra Is Half the Battle: Verifying Presentations of Graded Unipotent Chevalley Groups

In this work, we verify recent results [25, 35] showing that a smaller-than-previously-known subset of the Steinberg relations are sufficient to define three specific Chevalley groups. As we explain later, these groups are used to construct objects with useful topological properties called higher-dimensional expanders (HDXs). While we do not formalize this connection to HDXs, we discuss how this connection motivated and shaped our work.

In order to even state the theorem we proved, we need to cover quite a bit of mathematical background (see Section 3). But informally, we verified the following:

Our theorem verifies results from two papers [35, 25], which we call “KOOS” based on the last names of the authors.¹¹1“KO” is from the first paper, and “OS” is from the second. The “S” is the Singer of this paper. In our opinion, these papers were good candidates for computer verification: their proofs are filled with repetitive, mechanical, and precise calculations that are tedious for humans but rote for computers. The calculations in OS alone spanned 80 pages! Clearly, we thought, computer verification was needed to confirm these results.

Ideally, an automated theorem prover could do the work, but a supermajority of the proofs require solving group-rewriting problems, which are undecidable in general [33]. The natural next choice was to use an interactive theorem prover. We used Lean 4.

Lean [9] is an increasingly popular tool used to formalize mathematics and computer science. One of Lean’s major selling points is the mathlib project [32], which formalizes many branches of math and CS. By placing key definitions, results, and proof tactics in the same project, mathematicians can build on each other’s work. Our work depends on mathlib; through our work, we will contribute to it in turn.

Even though we made heavy use of Lean’s tactics and automation, our proofs were still as mechanical as the ones in the KOOS papers. We tried to reduce some of the proof burden by using custom tactics and macros that automatically completed many lemmas for us, but ultimately, our proofs are a few thousand lines of symbol pushing. We hope to improve our custom automation in future work.

The rest of the paper is organized as follows. We first discuss the connection to HDXs that motivated our work (Section 2). We then define the Chevalley groups that we formalized (Section 3). Next, we give a tour of our formalization by discussing key definitions and the top-level theorem statement (Section 4), the overall shape of the proof (Section 5), and the automation we used (Section 6). We conclude with a reflection on our experience and a discussion of future work (Section 7).

You can find our proofs at https://github.com/singerng/steinberg-formalization.

While Theorem 1 is mathematically interesting on its own, KOOS (and we) were ultimately motivated by its corollary: a method of constructing topologically-useful objects called higher-dimensional expanders (HDXs). We did not formalize this corollary, but we discuss HDXs here to explain how our work fits into the broader research context.

HDXs have only been studied for about two decades, but they have already formed the basis for numerous results in theoretical CS, including better lower bounds for the Sum-of-Squares hierarchy [14, 21], new constructions for locally-testable error correction [13], and new algorithms for low-density quantum error correction [27] and property testing [15, 12, 4, 3]. HDXs also have interesting applications in higher-dimensional geometry [18, 17, 23, 16].

Interest in HDXs grew out of the study of graph expansion. An expander graph is a sparse graph with strong connectivity properties. Like HDXs, expander graphs are used in a wide range of applications, including error-correcting codes, entropy reduction for randomized algorithms, and the design of near-linear-time algorithms. Expander graphs have been studied for many decades; we refer the interested reader to a survey on the topic [20].

Expansion can be defined in several different ways, but the various definitions fall under two umbrellas: spectral expansion and topological expansion. Informally, random walks over spectral expanders spread out quickly, while topological expanders do not contain any bottlenecks. In graph theory, these two kinds of expansion are closely related via the celebrated Cheeger inequality [1]. Thus, in order to build a topological expander, it is sufficient to build a spectral expander and then invoke this black-box relationship.

As their name suggests, higher-dimensional expanders (HDXs) generalize expansion for higher-dimensional objects [29, 18], such as simplicial complexes. But in this setting, spectral and topological expansion are not equivalent [19, 38], and proving topological expansion in particular can be difficult.

Broadly, there are only two known types of good HDX constructions: quotients of Bruhat-Tits buildings [5, 7, 28, 37, 31, 30]; and, more recently discovered, coset complexes of Chevalley groups [24, 25, 35, 26]. Both types are generally known to be spectral expanders, but only in certain special cases are they known to be topological expanders as well. In this paper, we focus on the topological properties of these Chevalley groups.

Chevalley groups were first used in HDX constructions by KO in 2018 [24]. Specifically, KO showed that the coset complexes of graded $A_n$-type Chevalley groups are spectral expanders. In their follow-up work [25], they showed that these complexes are also topological expanders by connecting topological expansion to group-theoretic properties of presentations (see Section 3.2). Separately, O’Donnell and Pratt [34] generalized KO’s construction to show that coset complexes of graded Chevalley groups of other types ($B_n$, $C_n$, $D_n$, and exceptional) are spectral expanders. Most recently, OS [35] showed (again, using the expansion–group theory connection) that the $B_3$-type coset complexes are also topological expanders. Our work confirms the group-theoretic findings for the $A_3$- [25] and $B_3$- [35] types.

We now discuss Chevalley groups, with an eye towards the specific subgroups used to build Chevalley coset complex HDXs [24, 25, 34, 35]. Our definitions start out somewhat abstract; see Section 3.1 for a concrete example.

Chevalley groups [22, 10, 8, 39] are best known as one of the four classes of finite simple groups [2]. Simple groups have no nontrivial normal subgroups, and thus they have no nontrivial quotient groups. As a result, simple groups are to finite group theory what prime numbers are to number theory.

Chevalley groups are related to the more-famous Lie groups. A Lie group is a group on matrices which admits a certain good topological structure. For example, the special linear groups (i.e., groups of determinant-$1$ square matrices of a fixed size) over $ℝ$ and $ℂ$ are Lie groups. Roughly, Chevalley groups are Lie groups defined over finite fields, such as the special linear group over ${𝔽}_q$ (where ${𝔽}_q$ denotes the field with $q$ elements for $q$ a prime power).

One way of capturing how these groups behave is with a set of generators on a particular root system. As it turns out, every Chevalley (and Lie) group can be expressed in this way.

True to their name, the set of all such $\{\zeta ,t\}$ generates $G$, and the algebraic structure of $G$ with respect to these generators (i.e., what happens when you multiply two generators together) is intimately connected to the geometric structure of $\mathrm{\Psi }$.

While the generators $\{\zeta ,t\}$ have a deeper meaning (see Section 3.1), we can interpret them for now as abstract symbols satisfying a set of equations, called Steinberg relations, that describe how the generators behave under multiplication. There are three kinds of Steinberg relations, based on whether the roots of the generators are the same, distinct, or of opposite sign, with each case giving a different kind of relation. These three kinds are, respectively: (i) linearity relations, (ii) commutator relations, and (iii) diagonal relations.

The linearity relations are the simplest: when two generators share a root, multiplication commutes with field addition. In other words, for every $t,u\in {𝔽}_q$, $\{\zeta ,t\}\cdot \{\zeta ,u\}=\{\zeta ,t+u\}$.

The commutator relations describe how generators with distinct roots multiply together by specifying their commutator (hence the name). In a group, the commutator of two elements $g$ and $h$ is defined as $[g,h]:=gh{g}^{-1}{h}^{-1}$, or equivalently, $gh=[g,h]hg$. Intuitively, the commutator is a measure of how much $g$ and $h$ fail to commute. For example, $g$ and $h$ commute iff $[g,h]=𝕀$, where $𝕀$ is the identity element of the group.

As it turns out, if $\eta \ne \pm \zeta \in \mathrm{\Psi }$ are two distinct roots, then every commutator of Chevalley generators $[\{\zeta ,t\},\{\eta ,u\}]$ can be written as a product of generators of the form $\{a\zeta +b\eta ,C_{\zeta ,\eta }^{a,b}{t}^a{u}^b\}$, where $a,b\in {\mathbb{N}}^{+}$ and where $C_{\zeta ,\eta }^{a,b}\in \{\pm 1,\pm 2,\pm 3\}$ is a particular Chevalley constant depending on $\zeta$, $\eta$, $a$, and $b$.²²2These constants (and their signs) have a reputation of making calculations on Chevalley groups inconvenient. The calculations in the KOOS proofs (and thus our formalization) were no exception. Remarkably, the generators in these products are always contained in the positive integer span of the two original roots $\eta$ and $\zeta$. As a result, the commutator relations connect the algebraic structure of the Chevalley group to the geometry of its root system.

The diagonal relations cover the final case, where $\eta =-\zeta$. They are less convenient to state, but luckily for us, we can ignore them. This is because HDX constructions only use unipotent Chevalley subgroups, whose diagonal Steinberg relations are trivial.³³3We only need to consider these subgroups due to the so-called local-to-global theorems for HDXs [17].

Given a positive root system $\mathrm{\Phi }$, there is a corresponding unipotent subgroup $G$ of the Chevalley group that is generated by elements $\{\zeta ,t\}$ for $\zeta \in \mathrm{\Phi }$ and $t\in {𝔽}_q$. To define this subgroup with Steinberg relations, all that is needed are (i) linearity relations for every root in $\mathrm{\Phi }$, and (ii) commutator relations for every pair of distinct, non-opposite roots in $\mathrm{\Phi }$.

In addition to being unipotent, the Chevalley subgroups used to build HDXs are graded, and this gradedness is taken with respect to the heights of the roots.

An important feature of this definition is that, given a fixed positive root system, the graded unipotent subgroup does not depend on $m$, so long as $m$ is larger than the maximum height of any root. This parameter $m$ does not appear in our formalization, but when thinking about HDX constructions, $m$ guarantees that we can make an infinite family of increasingly large groups, which are used to make an infinite family of increasingly large simplicial complexes (i.e., HDXs).

We simplify this setup slightly and restrict our graded generators, without loss of generality, to just those where $f$ is a monomial. We write these generators as triples $\{\zeta ,i,t\}:=\{\zeta ,t{X}^i\}$, where $0\le i\le m$ is the degree of the monomial and $t\in {𝔽}_q$ is its coefficient. Using this notation, the graded unipotent Steinberg relations are now:

• $\mathrm{■}$

  Linearity: For every $\zeta \in \mathrm{\Phi }$, $0\le i\le m$, and $t,u\in {𝔽}_q$, $\{\zeta ,i,t\}\cdot \{\zeta ,i,u\}=\{\zeta ,i,t+u\}$. (A direct consequence of the linarity relations are the identity relations, where $\{\zeta ,i,0\}=𝕀$; and the inverse relations, where ${\{\zeta ,i,t\}}^{-1}=\{\zeta ,i,-t\}$.)

• $\mathrm{■}$

  Commutator: For every $\zeta \ne \eta \in \mathrm{\Phi }$, $0\le i,j\le m$, and $t,u\in {𝔽}_q$, the commutator of $\{\zeta ,i,t\}$ and $\{\eta ,j,u\}$ is a product of generators of the form $\{a\zeta +b\eta ,ai+bj,C_{\zeta ,\eta }^{a,b}{t}^a{u}^b\}$.

• $\mathrm{■}$

  Mixed-degree: For every $\zeta \in \mathrm{\Phi }$, $0\le i,j\le m$, and $t,u\in {𝔽}_q$, $[\{\zeta ,i,t\},\{\zeta ,j,u\}]=𝕀$. (These relations are a consequence of the monomial restriction, and they encode the fact that addition of monomials is commutative.)

Given all this, we can finally define the unipotent subgroups of the graded Chevalley groups that we used in our formalization. The unipotent subgroup we want is the subgroup $G$ generated by the elements $\{\zeta ,i,t\}$, where $\zeta \in \mathrm{\Phi }$, $t\in {𝔽}_q$, and $0\le i\le 0pt(\zeta )$. From a Steinberg-relational perspective, $G$ is defined by the linearity, commutator, and mixed-degree relations involving roots in $\mathrm{\Phi }$.

The proof of Theorem 1, then, is to show that this particular set $R$ of linearity, commutator, and mixed-degree Steinberg relations (and a few more; see Section 3.3) implies the rest. This amounts to showing that any relation not in $R$ can be derived using relations in $R$, along with general facts about groups and the underlying field ${𝔽}_q$.

The technical details for why Theorem 1 is necessary in order to build HDXs are beyond the scope of this paper. But extremely roughly, when building an HDX from one of these Chevalley groups, one builds a coset complex $CC$ with a graded Chevalley group $G$ and certain designated subgroups of $G$, where the subgroups are defined by the relations in $R$. Showing that $CC$ is an HDX is equivalent to showing that every Steinberg relation for $G$ has a short derivation using the relations in $R$. That’s where the statement “$R$ implies the rest of the Steinberg relations” comes in.

In this section, we present the Lean versions of our definitions and top-level theorems. We also discuss some design decisions we made and how they affected our verification.

Our main result, Theorem 1, is stated and proven purely using the language and methods of group theory. And since mathlib has good support for abstract algebra, our formalization was relatively straightforward to set up, with our definitions of root systems, generators, and presentations mapping onto key definitions already present in mathlib. Of course, we still had to muck our way through the hundreds of lemmas from the KOOS papers, but it was the proofs, not the setup, where we spent most of our time.

First, we define our three root systems. Recall that our three graded unipotent Chevalley groups are each associated with a positive root system $\mathrm{\Phi }$ imbued with a height function. In Lean, we use a type class so that we can state things about root systems in general, and then we show that each specific system is an instance of this class. For example, here are the definitions for the $B_3$-large case.

On paper, we would write the linear combinations of roots with “$+$.” For example, $\alpha \beta$ is typically written as “$\alpha +\beta$.” But Lean makes it hard to use reserved symbols in definition names, so we drop the plus signs in the names of the roots in B3LargePosRoot.

Once we have a particular root system and a ring/field for the coefficients, we can define the type⁵⁵5In mathematics, groups and other objects are defined over sets, but in Lean, the same objects are defined over types. To be more consistent with Lean’s view of things, we will refer to “types” over “sets.” We apologize to the mathematicians. of the $\{\zeta ,i,t\}$ triples, which serve as the generators of the (graded) presentation.

An analogous type ChevalleyGenerator represents the ungraded generators $\{\zeta ,t\}$ by omitting the i and hi fields.

However, we want to view the elements of GradedChevGen as elements of a free group, and not as a standalone type. Thus, we need to inject them into the free group on $T$. Fortunately, the FreeGroup type in mathlib already has the needed definitions and theorems. In this case, the function FreeGroup.of : T $\to$ FreeGroup T performs the injecting.

Next, we define the presentations for each Chevalley group from their Steinberg relations. To do so, we use mathlib’s definition of a PresentedGroup, which is the free group on a type $T$, quotiented by a set of relations written in terms of the free group on $T$.

Armed with our definitions of the weak and full sets of relations (which we will discuss shortly), we can state our top-level theorems. For example, here is the theorem statement for the $B_3$-large case:

In other words, all relations in the full set vanish in the group presented by the weak set. (project projects free group elements into the presented graded Chevalley group.)

As is the case for many formalizations, this succinct theorem statement hides much of the complexity of the underlying definitions. We leave the details for those who look at our Lean files, but we highlight three features that are characteristic of working with Chevalley groups in particular and mathlib’s version of presented groups in general.

The first feature is that we decided to manually define the additive structure of the positive root systems $\mathrm{\Phi }$. Ideally, these systems would be implicitly defined by their base, but to define “+” in Lean, we would need to somehow encode the fact that addition on roots is not total, since the sum of any two roots is not necessarily a new root. For example, in the $B_3$ case, $\alpha +3\beta$ is a positive linear combination of $\alpha$ and $\beta$, but it is not a root because $\alpha +3\beta \notin B_3$ (i.e., it is not a long or a short root). So instead of carrying around hypotheses that any particular addition is sound, or defining add : $\mathrm{\Phi }$ $\to$ $\mathrm{\Phi }$ $\to$ Option $\mathrm{\Phi }$ and enforcing that the result be some $\zeta$, we write down all of the needed roots and ensure that their heights are well-behaved by construction.

In our opinion, our decision to manually list the roots made our formalization easier. Because we had to use one of the listed roots, Lean’s type checker was quick to point out when we wrote down the wrong root or the wrong Chevalley constant, and it was easy to prove that the degrees $i$ of graded generators $\{\zeta ,i,t\}$ were less than the height of $\zeta$. (We wrote a custom tactic ht that unfolded height and then called the omega tactic, which is a tactic for solving systems of linear inequations on integers.) That being said, we recognize that this choice becomes less beneficial as the size of the root system increases. If our work continues, then this choice is a good candidate for a refactor.

The second feature we highlight is that our definitions for the various (graded, unipotent) Chevalley groups overlap in a complicated way. We made this design choice in an attempt to reduce code duplication and to abstract out common properties shared by the different groups. While this makes our code harder to understand at first glance, we hope that it provides a good basis for future Chevalley formalizations.

This overlap is most obvious in our definitions of the weak and full sets of relations. Recall that the full set of unipotent Steinberg relations comprises the linearity and commutator relations, while the weak set comprises codimension-1, lifted, and definition relations. To capture the set of Steinberg relations shared by both sets, we define the following:

These four fields contain the relations shared between the two sets, namely, the linearity and mixed-degree relations for the present roots and the commutator relations for pairs of roots spanning zero, one, and two additional roots in the root system.⁶⁶6The division of the relations into these four types is specialized for the $A_n$ and $B_n$ systems. More-complicated systems would need more fields. (The types Single- and DoubleSpanRootPair encode these additional root(s) and their Chevalley constants. We supply them by hand, and then later we verify that they are correct.) The set presentRoots contains every root in the full case, but only the present roots in the weak case.

In the weak case, the PartialChevalleySystem lacks the lifted and definition relations. We add them separately in a new type GradedPartialChevalleyGroup. The lifted relations, we supply directly; the definition relations, we specify via a function define. We require that define acts as the identity function on all of the present roots, and that it commutes with FreeGroup.lift (which extends functions T $\to$ [Group G] to a group homomorphism from T to G). We bundle these two additional kinds of relations as follows:

Recall that the definition relations need an expression $e$. It is in define that we choose this $e$ for each missing root. For example, define for the weak $B_3$-large case looks like this:

(The splitX functions send $i\le \text{height}(\zeta )$ to a pair $(j,k)$, where $j+k=i$ and where $j$ and $k$ are less than the other relevant root heights. Basically, splitX acts as an explicit partitioning function to factor the $X^i$ monomials into two monomials for two different generators.)

In the full case, these two additional fields are trivial: liftedRels is the empty set, and define is the identity function.

The third feature we want to highlight is how the definition of a presentation in Lean often makes it awkward to use relations when reasoning about the presented group. There are three reasons for why this is the case.

The first reason is that all of the relations need to be in one set, but we usually want to focus on a specific subset. When defining a PresentedGroup, we have to lump the relations into one large Set. But as we have already seen, we define different subsets of relations according to their shared properties (e.g., the trivial span relations), and in order to talk about these shared properties (e.g., to assert that one specific pair of generators satisfies a trivial commutator relation), we have to “unpack” this large set of relations into its component pieces. To solve this problem, we wrote a lemma to do this for each kind of subset.

The second reason for this awkwardness is that relations are written in terms of the free group, but we often want to work with equations inside the presented group. These are equivalent notions, since a relation $r$ can be thought of as $r\sim 𝕀$ in the presentation or as $r=𝕀$ in the presented group. But while these are equivalent, it is usually easier to work with the equation view, especially for our purposes, where we are trying to show that some Steinberg relations can be derived from others. In the equation view, this amounts to showing that a relation not in the weak set is equal to $𝕀$ in the presented group, which then allows us to use all of the typical lemmas and machinery associated with group theory.

The third awkward reason is that we often have to convert the relations into a form that is easier to use in proofs. The harder-to-use form is a consequence of how presentations are defined. In a presentation, every relation $r$ encodes $r=𝕀$, (or rather, $r\sim 𝕀$). But we often want to view a relation as a pair of elements $(r_1,r_2)$ such that $r_1=r_2$ (via $r_1{r}_2^{-1}≕r=𝕀$). This allows us to state the commutator relations more naturally and to use them in Lean proof tactics, such as rw and simp. For example, the commutator relations for a pair of roots spanning two additional roots (the DoubleSpanRootPair) is usually written as

but to express it in the $r=1$ form, the right-hand side of the expression needs to be inverted and moved over to the left. As a result, our Lean definition is:

Clearly, this isn’t as nice. So we also have an equivalent definition that restates these relations in the $r_1=r_2$ form, as well as a lemma that converts between the two.

In the introduction, we wrote that the KOOS proofs (and our formalization) involved a lot of casework, and unfortunately, we do not know of a way to simplify their proof approach. Simply put, to show that the full set of Steinberg relations is derivable from the weak set, we showed one-by-one that every missing Steinberg relation holds in the group presented by the weak relations. To put some numbers to it, of the commutator relations (which are more numerous and harder to show than the linearity and the mixed-degree relations), 15 are missing in $A_3$, 21 are missing in $B_3$-small, and 26 are missing in $B_3$-large.

Roughly, most of the missing relations involve one or more missing roots. In the $A_3$ and $B_3$-small cases, there is only one missing root, but in the $B_3$-large case, there are three missing roots: $\alpha +\beta +\psi$, $\alpha +\beta +2\psi$, and $\alpha +2\beta +2\psi$. The key to the proofs is to express the generator involving the missing root in terms of generators of present roots, but there may be several ways of doing so. For example, there are three ways to express $\alpha +2\beta +2\psi$ as a sum of two present roots:

Ultimately, we show that any of these forms works. Then, we use the relations involving the present roots we already have to adjust the group expressions until both sides are equal. This is where the term rewriting problems come from.

To express the missing root $\zeta$ in terms of smaller roots, we apply the definition relation for $\zeta$, which states that $\{\zeta ,i,t\}=e$ for some fixed expression $e$ on present-root generators. But because we should not depend on the choice of $e$ (too much), we show that a set of interchange theorems holds, which allows us to shuffle the degrees and coefficients of the generators to the form most convenient for the relation we are trying to prove.

Here’s an example of an interchange theorem:

Informally, this is almost expressing the commutator $[\{\alpha ,i,tu\},\{\beta +\psi ,j+k,1\}]$, but with the inverses pushed into the generators (via the inverse relations ${\{\zeta ,i,t\}}^{-1}=\{\zeta ,i,-t\}$, which are implied by the linearity relations for $\zeta$) and with the coefficient of the rightmost inverse term ($\{\beta +\psi ,j+k,-1\}$) split in half and added to the front and back of the expression. The precise reasons for why this theorem is true are not important; we merely provide it to show the nature of the interchange theorems, which all shuffle degrees and coefficients in this way.

Of the interchange theorems we need, we get eight of them almost for free from the lifting relations. This is due to how lifting works: when we map ungraded generators into the graded group, we get to pick a degree $i$ for each of the three base roots $\zeta$ such that $i$ is at most the height of $\zeta$. In each of the groups we consider, the base roots all have height 1, meaning that $i\in \{0,1\}$, and thus we have $2^3=8$ possible choices for the degrees.

As it turns out, each of the eight of these lifting relations look very similar to one of the interchange theorems, and so we only need to adjust the relations slightly to prove the theorems. We prove all of the other interchange theorems “the hard way” by solving a group rewriting problem.

Now armed with the definition relations and the interchange theorems, we can start proving that the rest of the missing Steinberg relations hold. We prove a majority of the relations “the hard way.” For example, the proof from the end of Section 3.1, i.e., that the linearity relations hold for the missing root $\beta +\psi +\omega$, looks like this in Lean (albeit cleaned up and with several technical details omitted).

Notice how, despite the automation we used (see Section 6 for grw), the proof has the same form as the one we wrote by hand, with each step explicitly provided. (The mul_one theorem states that $x\ast 1=x$, and is used to express $tu≔t\cdot 1$ and $tu≔(t+u)\cdot 1$.)

Unfortunately, to the best of our knowledge, many relations cannot be proven in this way. Rather, we have to prove that the relation holds for each possible concrete value for the pair of degrees $i$ and $j$. For example, in the $B_3$-large case, we prove the following theorems in order to show that $\alpha$ and $\alpha +2\beta +2\psi$ commute:

(As we said, there’s a lot of casework.)

The good news is that the graded unipotent Chevalley groups have a property called reflection symmetry. The Steinberg relations are closed under replacing every element $\{\zeta ,i,t\}$ with the element $\{\zeta ,\text{height}(\zeta )-i,t\}$. In other words, the degree can be “reflected” about the height of $\zeta$. OS [35] (and we) use this property to derive half of these cases from the other half, which reduces the casework for these relations by a factor of two.

Given the repetitive nature of the theorems and proofs in our formalization, it should come as no surprise that we developed custom macros, tactics, and proof automation to assist us. This automation falls into three categories: custom simp attributes, theorem macros, and group reassociation. None of these are particularly original, but they were quite effective in speeding up the pace of our development.

In Lean, invoking the simplifier tactic simp causes it to apply a library of lemmas and theorems marked with the @[simp] attribute in order to reduce the proof term to a “simp normal form.” Lean developers mark a theorem with @[simp] when they want the simp tactic to apply it automatically. For example, the mul_one theorem is marked with @[simp] since, in most cases, $x\ast 1$ should be replaced with just $x$ automatically.

However, when only a particular subset of lemmas should be applied, one can instead tell simp to use a library of lemmas marked with a label other than @[simp]. Doing so leads to a faster simplifier that doesn’t simplify proof terms “too far.”

In this project, we define a new attribute called chev_simps, and we often invoke simp only [chev_simps] in our proofs. Many relations, such as the linearity, identity, and inverse relations, should be applied automatically in almost all cases to simplify an expression to normal form, and so these relations are marked with chev_simps.

We define a similar attribute height_simps for theorems involving the graded height function, and a tactic ht to discharge inequalities about heights (with ht basically being a wrapper for “simp only [height_simps]; omega”).

Our second form of automation is theorem macros. In addition to the linearity relations, there are many theorems that can easily be derived from others. For example,

In other words, proving the relation on the left gives an easy way to derive the equation on the right. In Lean, these kinds of proofs are typically between three and ten lines, and they happen often enough in our formalization that we wrote macros that expand into an entire theorem statement and proof.

The simplest of these macros is the three for the linearity, identity, and inverse relations. Given a root system w, a ring/field R, and a root r, the macro roughly looks like this (with many Lean-specific meta-programming details omitted):

Basically, the parameters w, R, and r are passed to the correct definitions, and new theorems are declared with the names stored in the identifiers $linOf_r, $idOf_r, and $invOf_r (which are constructed by omitted code). For example, if the root is $\alpha$, then the corresponding identity theorem would be named id_of_$\alpha$.

We have similar macros to prove many different types of theorems, including the trivial commutator example above and the reflected theorems from Section 5. For example, we invoke the reflected theorem macro by giving it the reflected heights, like this:

Overall, our theorem macros automatically fill in many of the relations we get for free in the weak presentation, and they help reduce the amount of boilerplate code.

Our final form of automation is group reassociation. Consider the theorem mul_comm, which states that any two elements commute under a commutative operation $\ast$: $a\ast b=b\ast a$. Now suppose we want to prove that $c\ast a\ast b=c\ast b\ast a$. Showing this seems simple: merely apply mul_comm a b. However, multiplication in Lean is left-associative by default, and so the application of mul_comm a b fails, since the term actually looks like $(c\ast a)\ast b=(c\ast b)\ast a$. In this case, we would need to manually reassociate the terms to look like $c\ast (a\ast b)=c\ast (b\ast a)$ before we could apply mul_comm a b and finish the proof.

However, we want to avoid doing this kind of manual reassociation in our formalization, since our theorems often involve group equations involving products of five or more terms. Thus, we modified a trick from mathlib’s category theory library, reassoc_of%,⁷⁷7Simon Hudon wrote the version of this macro for Lean 3. The version in Lean 4 is mainly due to Kim Morrison. See its source file in mathlib4 on GitHub for more information. to apply to groups. In the category theory setting, reassoc_of% reassociates an arrow to the right by introducing a new term on the left. In our case, we wrote greassoc_of% (“group re-associate”) to multiply by a new group element on the left. Informally, it does the following:

Thus, rw [greassoc_of% (mul_comm a b)] might succeed where rw [mul_comm a b] fails.