When producing large formally verified mathematical developments that make use of typeclasses it is easy to introduce overly strong assumptions for theorems and definitions. We consider the problem of recognizing from the elaborated proof terms when typeclass assumptions are stronger than necessary. We introduce a metaprogram for the Lean theorem prover that finds and informs the user about possible generalizations.
Developing and maintaining large libraries of formalized mathematics in an interactive theorem
prover, such as the libraries mathlib [
The goal of this paper is to demonstrate that when typeclasses are used to implement hierarchies of assumptions on formalized objects it is possible to automate the process of generalizing results by relaxing typeclass assumptions. Pons [6] has previously considered a similar problem, and describes a mechanism for generalizing assumptions about functions and types, but without specifically considering heierachies of typeclasses.
Our focus is mostly on the applications to the formalization of mathematics, it is also conceivable however that relaxing typeclass assumptions can be of use for other users of interactive theorem provers, such as for software verification.
Typeclasses were introduced by Wadler [7] as a way to provide polymorphism in strongly typed programming languages. They are used in interactive theorem provers [8] and their libraries of formalized mathematics to manage levels of mathematical structures on an object [9, 10]. When a term is used the user does not ordinarily supply typeclass arguments, instead they are inserted automatically by a typeclass system that finds instances to match the needed argument, possibly by chaining together the instances declared in the library. From the perspective of interactive theorem provers, typeclasses reduce the burden on the user of the tool to be explicit about which instances are used and in fact hide them completely from the end user.
Commonly used typeclass hierarchies for mathematical libraries include: algebraic structures, including binary operations and their properties, properties of relations and ordering, topological spaces, (pseudo-)metric spaces, and their properties. Additionally mixtures of the aforementioned hierarchies that interact, such as ordered algebraic structures, topological groups and normed algebraic structures may also be included in the typeclass system, leading to a highly nontrivial hierarchy.
In addition to the situation mentioned in the introduction, where results introduced for one purpose may be generalized to a more widely useful form, generalization can also become possible when new typeclasses are inserted into an existing hierarchy. For instance in the mathlib library the concepts of non-unital and/or non-associative rings were added in March 20211, several years after rings were introduced in core Lean. In the interim period several thousand lemmas and theorems were added to mathlib concerning rings. This leaves the dificult library maintenance problem of filling out the library of lemmas for these newly introduced algebraic structures, without duplicating existing work.
We introduce some of the key considerations by looking at some examples in the Lean theorem prover using the mathlib library.
Consider the following lemma: lemma mul_inv {G : Type* } [ordered_comm_group G] (a b : G) : (a * b)− 1 = a− 1 * b− 1 := by rw [mul_inv_rev, mul_comm] It is clear that the statement and the proof require a commutative group structure, but that the assumption that be an ordered commutative group plays no role. Despite the shortness of the statement and proof script the generated proof term contains many chains of typeclass instances including those shown in Figure 1.
There are in addition other instances between these classes, not made use of in the original proof, but available to the typeclass system.
The only typeclass parameters actually required to satisfy the assumptions of the applied lemmas mul_inv_rev and mul_comm are group G and comm_semigroup G. We cannot 1See https://github.com/leanprover-community/mathlib/pull/6786. ordered_cancel_comm_monoid
comm_group ordered_comm_monoid comm_monoid comm_semigroup
group div_inv_monoid monoid semigroup
mul_one_class has_mul replace the assumption ordered_comm_group G with this pair of assumptions however as they have overlapping fields, they both should refer to the same multiplication operation. This is visible in the figure as there is an instance chain from each of these to has_mul. Instead a meet of these two typeclasses in the typeclass graph should be chosen as the generalization, in this case it is comm_group.
The following theorem states that given a ring homomorphism between two fields and a natural number , one of the fields has characteristic if and only if the other has characteristic (including = 0): lemma ring_hom.char_p_iff_char_p {K L : Type* } [field K] [field L] (f : K →+* L) (p : N) : char_p K p ↔ char_p L p := begin split; { introI _c, constructor, intro n, rw [← @char_p.cast_eq_zero_iff _ _ p _c n, ← f.injective.eq_iff, f.map_nat_cast, f.map_zero] } end We see that the proof script splits the if statement into each direction, but both directions are proved by the same tactic block. It is non-trivial to determine just by reading the proof given what the weakest assumptions possible are, and it is not immediately clear from the statement either. While it is of course possible to work out the correct generality by hand by inspecting the assumptions needed for each lemma applied, we hope this provides a realistic example where the “right” answer is not immediately clear.
In fact the weakest possible typeclass assumptions for the proof of ring_hom.char_p_iff_char_p are precisely the assumptions needed to apply ring_hom.injective to perform the rewrite ← f.injective.eq_iff. These are that should be a division ring, and should be a nontrivial semiring. This example highlights another important point; simply taking the meet in the typeclass graph of the required classes is not always optimal. The meet of the classes nontrivial and semiring in the present version of mathlib is domain, once again an overly strong assumption, as there is no reason not to simply assume [nontrivial K] [semiring K]. We should allow one assumption to be replaced by several distinct assumptions if there is no conflict in doing so. The typeclasses nontrivial and semiring both provide instances of the nonempty typeclass, which contains no data, so it is a Prop and hence a subsingleton in Lean. Thus despite the fact that they do both provide instances of the same class, the instances will be equal and there is no issue allowing both assumptions separately.
We now describe in more detail an algorithm to find possible typeclass generalizations, given a proof term.
One important thing to note here is that we also handle typeclasses with more than one argument that are partially applied. For instance it is desirable to be able to generalize group G to has_pow G Z. This is distinct from monoid G generalizing to has_pow G N, so we treat these partially applied typeclasses as the basic objects of interest, we call them bound classes.
The first step is to traverse the entire environment and build a directed graph of bound classes with instances between them. We also precompute the transitive closure and a topological sort of this graph.
Algorithm 1: Generalising typeclasses assumptions in a declaration.
foreach typeclass argument c do ← []; foreach maximal chain of instances ending in c in the statement or proof do add the head bound class of the chain to ; end ← the set of strongly connected components for the subgraph of bound classes reachable from (ignoring subsingletons); ← []; foreach in do
add a meet of to ; end end return o
We have implemented the above ideas for the Lean theorem prover as a metaprogram written in Lean itself2. This means that no external tools beyond Lean itself are needed for users to 2the implementation is available at https://github.com/alexjbest/lean-generalisation integrate this tool into their Lean developments. We may also make use of the linter framework [11] which provides a convenient means for users to run diferent checks on the current file, and for continuous integration tools to regularly lint an entire library on multiple cores. This introduces a dependency on mathlib itself, but this tool can be imported and applied to any Lean development, and the import removed when generalization is complete.
We note that it is important to precompute and cache useful information about the typeclass graph, such as a topological sort of the graph, and its transitive closure. With the current size of mathlib this precomputation is quite reasonable, even with non-optimal algorithms.
By running the metaprogram described above on a current version of the mathlib library3, which contains around 80,000 declarations we can gauge the efectiveness of this approach. Note that the process of generalizing typeclass assumptions using such a tool is naturally an iterative process, by generalizing one theorem other theorems that made use of the original theorem may also become generalizable. This makes it most natural to use such a tool interactively in a file when formalizing some theory. Nevertheless, for ease of measurement we simply apply a single pass in our test, thus there are likely many more interesting or useful typeclass relaxations that can be discovered by such a tool if used iteratively.
In total the current implementation produces 2877 results, some of these are false positives, or at least not particularly useful generalizations. To get a sense of what generalizations were possible in a library like mathlib, we list in Table 1 some of the most common generalizations found by this pass.
Here several generalizations such as changing a field typeclass to a (commutative) ring give rather large relaxations of structure, and potentially introduce a large number of new useful lemmas in the library.
The replacement of integral_domain with comm_ring and no_zero_divisors appears mathematically trivial, but in fact results in the removal of the assumption that the ring in question be nontrivial (which is part of mathlib’s definition of an integral domain). Replacements such as this are mathematically not significant and it is not the case that this generalization would be useful to an end user directly. However, making this generalization relieves the user of such a theorem from the burden of adding a non-trivial assumption which can then proliferate through the library. These small assumptions that nonetheless need verifying whenever a theorem is applied can slow down formalization eforts and make future formalization unduly time consuming and tedious compared with the actual mathematics being formalized.
It is important that such a tool be usable interactively when working on formalizing a mathematical theory. Running our implementation on the mathlib file topology/ordered/basic.lean (the second longest in mathlib by number of lines) takes between 1 and 2 minutes on a modern laptop, depending on if the typeclass graph is already computed and cached. This checks 475 declarations and reports 183 results currently. 3commit 29b63a7e91d079b159dfc2cf0fb4d2a1ce1c409b, not including core Lean library
By only inspecting the existing proof of a theorem naturally not all possible generalizations of theorems can be found. It is quite easy to write proofs that require stronger assumptions than necessary, especially when using powerful automation. Trying to remove this limitation completely shifts the problem to one of automatic theorem proving. However, an intermediate problem where some automation may be possible is to find theorems for which the same proof script proves a generalized theorem. This is especially likely with small proofs that make heavy use of automation to begin with. Here a brute force strategy of weakening typeclasses in theorem statements and re-running the same proof script seems far too slow to be used on the scale of a large library in a prover such as Lean, however similar techniques have been used in the Mizar system [12]. Nevertheless, a tool to automate this process could still be useful for small new developments.
Currently the system as implemented in Lean will provide to the user a list of possible typeclass generalizations by printing the name of the declaration and describing the argument that can be generalized. The structure of Lean files allows for variables to be defined within a section these assumptions can then hold for all declarations in large chunks of the file. This decoupling of the location of the assumptions used for each theorem and the theorems themselves sometimes makes it tedious to rearrange the file to actually implement the suggestions. Therefore better tooling to reorganise Lean files in a content-aware manner will improve the usability of the tool described in this paper.
A mild extension of this work would be to consider not just assumptions, but also concrete types in a theorem statement. For instance theorems proven about explicitly constructed types such as the natural, rational or real numbers often make use of (ordered) algebraic properties of these types, which are filled in via typeclasses. Recognizing these typeclass chains in the same way as described here could allow parts of libraries concerning these concrete types to be generalized to include any object satisfying some typeclass hypotheses.
A core design principle of Lean 4, the next iteration of the Lean theorem prover [13], is that the majority of the system be written in Lean itself. This allows for extensibility of the Lean system by users, rather than having to build diferent vesions of Lean for user extensions. Using this it may be possible to integrate the minimisation of typeclass assumption into Lean’s own typeclass system, providing a more accurate and eficient tool.
Recognizing too strong typeclass assumptions automatically is possible, and can be done eficiently. Such tools can save maintainers of mathematical libraries time by providing more general results for free from an existing library, and provide users of formal proof systems with interesting information about what generality theorems hold in. 8.1. Acknowledgements I would like to thank Floris van Doorn for helpful discussions on an earlier version of this work, and the referees for their useful comments and suggestions. This work was supported by the Hariri Institute for Computing, the Simons Collaboration on Arithmetic Geometry, Number Theory, and Computation, via Simons Foundation grant #550023, and NWO Vidi grant 639.032.613.