key: cord-0046580-u8wjxnw2
authors: Sakaguchi, Kazuhiko
title: Validating Mathematical Structures
date: 2020-06-06
journal: Automated Reasoning
DOI: 10.1007/978-3-030-51054-1_8
sha: ab7e846fb15ceb1ad0f91c9c6995acbf01cf29ad
doc_id: 46580
cord_uid: u8wjxnw2

Sharing of notations and theories across an inheritance hierarchy of mathematical structures, e.g., groups and rings, is important for productivity when formalizing mathematics in proof assistants. The packed classes methodology is a generic design pattern to define and combine mathematical structures in a dependent type theory with records. When combined with mechanisms for implicit coercions and unification hints, packed classes enable automated structure inference and subtyping in hierarchies, e.g., that a ring can be used in place of a group. However, large hierarchies based on packed classes are challenging to implement and maintain. We identify two hierarchy invariants that ensure modularity of reasoning and predictability of inference with packed classes, and propose algorithms to check these invariants. We implement our algorithms as tools for the Coq proof assistant, and show that they significantly improve the development process of Mathematical Components, a library for formalized mathematics.

Mathematical structures are a key ingredient of modern formalized mathematics in proof assistants, e.g., [1, 18, 25, 41] [46, Sect. 4] . Since mathematical structures have an inheritance/subtyping hierarchy such that "a ring is a group and a group is a monoid", it is usual practice in mathematics to reuse notations and theories of superclasses implicitly to reason about a subclass. Similarly, the sharing of notations and theories across the hierarchy is important for productivity when formalizing mathematics.

The packed classes methodology [16, 17] is a generic design pattern to define and combine mathematical structures in a dependent type theory with records. Hierarchies using packed classes support multiple inheritance, and maximal sharing notations and theories. When combined with mechanisms for implicit coercions [32, 33] and for extending unification procedure, such as the canonical structures [26, 33] of the Coq proof assistant [42] , and the unification hints [4] of the Lean theorem prover [6, 27] and the Matita interactive theorem prover [5] , packed classes enable subtyping and automated inference of structures in hierarchies. Compared to approaches based on type classes [22, 40] , packed classes are more robust, and their inference approach is efficient and predictable [1] . The success of the packed classes methodology in formalized mathematics can be seen in the Mathematical Components library [45] library [8] , and especially the formal proof of the Odd Order Theorem [20] . It has also been successfully applied for program verification tasks, e.g., a hierarchy of monadic effects [2] and a hierarchy of partial commutative monoids [28] for Fine-grained Concurrent Separation Logic [39] . In spite of its success, the packed classes methodology is hard to master for library designers and requires a substantial amount of work to maintain as libraries evolve. For instance, the strict application of packed classes requires defining quadratically many implicit coercions and unification hints in the number of structures. To give some figures, the MathComp library 1.10.0 uses this methodology ubiquitously to define the 51 mathematical structures depicted in Fig. 1 , and declares 554 implicit coercions and 746 unification hints to implement their inheritance. Moreover, defining new intermediate structures between existing ones requires fixing their subclasses and their inheritance accordingly; thus, it can be a challenging task.

In this paper, we indentify two hierarchy invariants concerning implicit coercions and unification hints in packed classes, and propose algorithms to check these invariants. We implement our algorithms as tools for the Coq system, evaluate our tools on a large-scale development, the MathComp library 1.7.0, and then successfully detect and fix several inheritance bugs with the help of our tools. The invariant concerning implicit coercions ensures the modularity of reasoning with packed classes and is also useful in other approaches, such as type classes and telescopes [26, Sect. 2.3] , in a dependent type theory. This invariant was proposed before as a coherence of inheritance graphs [7] . The invariant concerning unification hints, that we call well-formedness, ensures the predictability of structure inference. Our tool not only checks well-formedness, but also generates an exhaustive set of assertions for structure inference, and these assertions can be tested inside Coq. We state the predictability of inference as a metatheorem on a simplified model of hierarchies, that we formally prove in Coq.

The paper is organized as follows: Sect. 2 reviews the packed classes methodology using a running example. Section 3 studies the implicit coercion mechanism of Coq, and then presents the new coherence checking algorithm and its implementation. Section 4 reviews the use of canonical structures for structure inference in packed classes, and introduces the notion of well-formedness. Section 5 defines a simplified model of hierarchies and structure inference, and shows the metatheorem that states the predictability of structure inference. Section 6 presents the well-formedness checking algorithm and its implementation. Section 7 evaluates our checking tools on the MathComp library 1.7.0. Section 8 discusses related work and concludes the paper. Our running example for Sect. 2, Sect. 4, and Sect. 6, the formalization for Sect. 5, and the evaluation script for Sect. 7 are available at [37] .

This section reviews the packed classes methodology [16, 17] through an example, but elides canonical structures. Our example is a minimal hierarchy with multiple inheritance, consisting of the following four algebraic structures (Fig. 2 Additive monoids (A, +, 0): Monoids have an associative binary operation + on the set A and an identity element 0 ∈ A. Semirings (A, +, 0, ×, 1): Semirings have the monoid axioms, commutativity of addition, multiplication, and an element 1 ∈ A. Multiplication × is an associative binary operation on A that is left and right distributive over addition. 0 and 1 are absorbing and identity elements with respect to multiplication, respectively. Additive groups (A, +, 0, −): Groups have the monoid axioms and a unary operation − on A. −x is the additive inverse of x for any x ∈ A. Rings (A, +, 0, −, ×, 1): Rings have all the semiring and group axioms, but no additional axioms.

We start by defining the base class, namely, the Monoid structure. }. 10 11 Record class_of (A : Type) := Class { mixin : mixin_of A }. 12 13 Structure type := Pack { sort : Type; class : class_of sort }. 14 15 End Monoid.

The above definitions are enclosed by the Monoid module, which forces users to write qualified names such as Monoid.type. Thus, we can reuse the same name of record types (mixin_of, class_of, and type), their constructors (Mixin, Class, and Pack), and constants (e.g., sort and class) for other structures to indicate their roles. Structures are written as records that have three different roles: mixins, classes, and structures. The mixin record (line 3) gathers operators and axioms newly introduced by the Monoid structure. Since monoids do not inherit any other structure in Fig. 2 , those are all the monoid operators, namely 0 and +, and their axioms. The class record (line 11) assembles all the mixins of the superclasses of the Monoid structure (including itself), which is the singleton record consisting of the monoid mixin. The structure record (line 13) is the actual interface of the structure that bundles a carrier of type Type and its class instance. Record and Structure are synonyms in Coq, but we reserve the latter for actual interfaces of structures. In a hierarchy of algebraic structures, a carrier set A has type Type; hence, for each structure, the first field of the type record should have type Type, and the class_of record should be parameterized by that carrier. In general, it can be other types, e.g., Type → Type in the hierarchy of functors and monads [2] , but should be fixed in each hierarchy of structures. Mixin and monoid records are internal definitions of mathematical structures; in contrast, the structure record is a part of the interface of the monoid structure when reasoning about monoids. For this reason, we lift the projections for Monoid.mixin_of to definitions and lemmas for Monoid.type as follows. The curly brackets enclosing A mark it as an implicit argument; in contrast, @ is the explicit application symbol that deactivates the hiding of implicit arguments.

Since a monoid instance A : Monoid.type can be seen as a type equipped with monoid axioms, it is natural to declare Monoid.sort as an implicit coercion. The types of zero can be written and shown as ∀ A : Monoid.type, A rather than ∀ A : Monoid.type, Monoid.sort A thanks to this implicit coercion.

Next, we define the Semiring structure. Since semirings inherit from monoids and the semiring axioms interact with the monoid operators, e.g., distributivity of multiplication over addition, the semiring mixin should take Monoid.type rather than Type as its argument.

Module Semiring.

Record mixin_of (A : Monoid.type) := Mixin { one : A; mul : A → A → A; addC : commutative (@add A); (* 'add' is commutative. *) mulA : associative mul;

(* 'mul' is associative. *) mul1x : left_id one mul;

(* 'one' is the left and right *) mulx1 : right_id one mul;

(* identity element w.r.t. 'mul'. *) mulDl : left_distributive mul add;

(* 'mul' is left and right *) mulDr : right_distributive mul add; (* distributive over 'add'. *) mul0x : left_zero zero mul;

(* 'zero' is the left and right *) mulx0 : right_zero zero mul;

(* absorbing element w.r.t. 'mul'. *) }.

The Semiring class packs the Semiring mixin together with the Monoid class to assemble the mixin records of monoids and semirings. We may also assemble all the required mixins as record fields directly rather than nesting class records, yielding what is called the flat variant of packed classes [14, Sect. 4] . Since the semiring mixin requires Monoid.type as its type argument, we have to bundle the monoid class with the carrier to provide that Monoid.type instance, as follows. The inheritance from monoids to semirings can then be expressed as a canonical way to construct a monoid from a semiring as below.

Following the above method, we declare Semiring.sort as an implicit coercion, and then lift mul, one, and the semiring axioms from projections for the mixin to definitions for Semiring.type. 1 Coercion Semiring.sort : Semiring.type >-> Sortclass. Semiring.mul _ (Semiring.mixin _ (Semiring.class A)). 6 Lemma addC {A : Semiring.type} : commutative (@add (Semiring.monoidType A)). 7 ...

In the statement of the addC axiom (line 6 just above), we need to explicitly write Semiring.monoidType A to get the canonical Monoid.type instance for A : Semiring.type. We omit this subtyping function Semiring.monoidType by declaring it as an implicit coercion. In general, for a structure S inheriting from other structures, we define implicit coercions from S to all its superclasses.

Coercion Semiring.monoidType : Semiring.type >-> Monoid.type.

The Group structure is monoids extended with an additive inverse. Following the above method, it can be defined as follows. The Ring structure can be seen both as groups extended by the semiring axioms and as semirings extended by the group axioms. Here, we define it in the first way, but one may also define it in the second way. Since rings have no other axioms than the group and semiring axioms, no additional mixin_of record is needed. The ring structure inherits from monoids, groups, and semirings. Here, we define implicit coercions from the ring structure to those superclasses. 

This section describes the implicit coercion mechanism of Coq and the coherence property [7] of inheritance graphs that ensures modularity of reasoning with packed classes, and presents the coherence checking mechanism we implemented in Coq. More details on implicit coercions can be found in the Coq reference manual [44] , and its typing algorithm is described in [32] . First, we define classes and implicit coercions. An implicit coercion f : C D can be seen as a subtyping C ≤ D and applied to fill type mismatches to a term of class C placed in a context that expects to have a term of class D. Implicit coercions form an inheritance graph with classes as nodes and coercions as edges, whose path [

can also be seen as a subtyping 

Before our work, if multiple inheritance paths existed between the same source and target class, only the oldest one was kept as a valid one in the inheritance graph in Coq, and all the others were reported as ambiguous paths and ignored. We improved this mechanism to report only paths that break the coherence conditions and also to minimize the number of reported ambiguous paths [34, 35] . The second condition ensures the modularity of reasoning with packed classes. For example, proving ∀(R : Ring.type) (x, y : R), (−x) × y = −(x × y) requires using both Semiring.monoidType (Ring.semiringType R) and Group.monoidType (Ring.groupType R) implicitly. If those Monoid instances are not definitionally equal, it will prevent us from proving the lemma by reporting type mismatch between R and R.

Convertibility checking for inheritance paths consisting of implicit coercions as in Definition 3.2 requires constructing a composition of functions for a given inheritance path. One can reduce any unification problem to this well-typed term construction problem, that in the higher-order case is undecidable [19] . However, the inheritance paths that make the convertibility checking undecidable can never be applied as implicit coercions in type inference, because they do not respect the uniform inheritance condition. 

Remark 3.1. Names that can be declared as implicit coercions are defined as constants that respect the uniform inheritance condition in [32, Sect. 3.2] . However, the actual implementation in the modern Coq system accepts almost any function as in Definition 3.2 as a coercion.

Saïbi claimed that the uniform inheritance condition "ensures that any coercion can be applied to any object of its source class" [32, Sect. 3.2], but the actual condition ensures additional properties. The number and ordering of parameters of a uniform implicit coercion are the same as those of its source class; thus, convertibility checking of uniform implicit coercions f, g : C D does not require any special treatment such as permuting parameters of f and g. Moreover, function composition preserves this uniformity, that is, the following lemma holds. Proof. Let us assume that C, D, and E are classes with n, m, and k parameters respectively, and f and g have the following types:

Then, the function composition of f and g can be defined and typed as follows:

. . .

The terms u 1 , . . . , u m contain the free variables x 1 , . . . , x n+1 and we omitted substitutions for them by using the same names for the binders in the above definition. Nevertheless, (g • f ) : C E respects the uniform inheritance condition.

In the above definition of the function composition g • f of implicit coercions, the types of x 1 , . . . , x n , x n+1 and the parameters of g can be automatically inferred in Coq; thus, it can be abbreviated as follows: For implicit coercions f 1 :

. . , f n : C n C n+1 that have m 1 , m 2 , . . . , m n parameters respectively, the function composition of the inheritance path [f 1 ; f 2 ; . . . ; f n ] can be written as follows by repeatedly applying Lemma 3.1 and the above abbreviation.

If f 1 , . . . , f n are all uniform, the numbers of their parameters m 1 , . . . , m n are equal to the numbers of parameters of C 1 , . . . , C n . Consequently, the type inference algorithm always produces the typed closed term of most general function composition of f 1 , . . . , f n from the above term. If not all of f 1 , . . . , f n are uniform, type inference may fail or produce an open term, but if this produces a typed closed term, it is the most general function composition of f 1 , . . . , f n .

Our coherence checking mechanism constructs the function composition of p : C C and compares it with the identity function of class C to check the first condition, and also constructs the function compositions of p, q : C D and performs the conversion test for them to check the second condition.

This section reviews how the automated structure inference mechanism [26] works on our example and in general. The first example is 0+1, whose desugared form is @add _ (@zero _) (@one _), where holes _ stand for implicit pieces of information to be inferred. The left-and right-hand sides of the top application can be type-checked without any use of canonical structures, as follows: In general, for any structures A and B such that B inherits from A with an implicit coercion B.aType : B.type >-> A.type, B.aType should be declared as a canonical instance to allow Coq to solve unification problems of the form A.sort ? A≡ B.sort ? B by instantiating ? A with B.aType ? B .

The second example is −1, whose desugared form is @opp _ (@one _). The left-and right-hand sides of the top application can be type-checked as follows: Ring.semiringType ? R , respectively. Right after defining Ring.semiringType, this unification hint can be defined as follows.

Local Definition semiring_groupType (cT : type) : Group.type := Group.Pack (Semiring.sort (semiringType cT)) (base _ (class cT)).

This definition is definitionally equal to Ring.groupType, but has a different head symbol, Semiring.sort instead of Ring.sort, in its first field Group.sort. Thus, the unification hint we need between Group.sort and Semiring.sort can be synthesized by the following declarations.

Canonical Ring.semiring_groupType.

This unification hint can also be defined conversely as follows. Whichever of those is acceptable, but at least one of them should be declared.

Local Definition group_semiringType (cT : type) : Semiring.type := Semiring.Pack (Group.sort (groupType cT)) (Semiring.Class _ (Group.base _ (base _ (class cT))) (mixin _ (class cT))).

For any structures A and B that have common (non-strict) subclasses C, we say that C ∈ C is a join of A and B if C does not inherit from any other structures in C. For example, if we add the structure of commutative rings to the hierarchy of Sect. 2, the commutative ring structure is a common subclass of the group and semiring structures, but is not a join of them because the commutative ring structure inherits from the ring structure which is another common subclass of them. In general, the join of any two structures must be unique, and we should declare a canonical instance to infer the join C as the canonical solution of unification problems of the form A.sort ? A≡ B.sort ? B . For any structures A and B such that B inherits from A, B is the join of A and B; thus, the first criteria to define canonical instances is just an instance of the second criteria. Figure 3 shows a minimal hierarchy that has ambiguous joins. If we declare that C (resp. D) is the canonical join of A and B in this hierarchy, it will also be accidentally inferred for a user who wants to reason about D (resp. C). Since C and D do not inherit from each other, inferred C (resp. D) can never be instantiated with D (resp. C); therefore, we have to disambiguate it as in Fig. 4 , so that the join of A and B can be specialized to both C and D afterwards.

In this section, we define a simplified formal model of hierarchies and show a metatheorem that ensures the predictability of structure inference. First, we define the model of hierarchies and inheritance relations.

* ; that is, * is reflexive, antisymmetric, and transitive. We denote the corresponding strict (irreflexive) inheritance relation by + . A * B and A + B respectively mean that B non-strictly and strictly inherits from A. We encoded the above definitions on hierarchies in Coq by using the structure of partially ordered finite types finPOrderType of the mathcomp-finmap library [12] and proved the following theorem.

Theorem 5.1. The join operator on an extended well-formed hierarchy is associative, commutative, and idempotent; that is, an extended well-formed hierarchy is a join-semilattice.

If the unification algorithm of Coq respects our model of hierarchies and joins during structure inference, Theorem 5.1 implies that permuting, duplicating, and contracting unification problems do not change the result of inference; thus, it states the predictability of structure inference at a very abstract level.

This section presents a well-formedness checking algorithm that can also generate the exhaustive set of assertions for joins. We implemented this checking mechanism as a tool hierarchy.ml written in OCaml, which is available as a MathComp developer utility [45, /etc/utils/hierarchy.ml]. Our checking tool outputs the assertions as a Coq proof script which can detect missing and misimplemented unification hints for joins.

Since a hierarchy must be a finite set of structures (Definition 5.1), Definitions 5.2, 5.5, and 5.3 give us computable (yet inefficient) descriptions of joins and the well-formedness; in other words, for a given hierarchy H and any two structures A, B ∈ H, one may enumerate their minimal common subclasses. Algorithm 1 is the checking algorithm we present, that takes in input an inheritance relation in the form of an indexed family of strict subclasses subof(A) := {B ∈ H | A + B}. The join function in this algorithm takes two structures as arguments, checks the uniqueness of their join, and then returns the join if it uniquely exists. In this function, the enumeration of minimal common subclasses is done by constructing the set of common subclasses C, and filtering out subof(C) from C for every C ∈ C. In this filtering process, which is written as a foreach statement, we can skip elements already filtered out and do not need to care about ordering of picking up elements, thanks to transitivity.

The hierarchy.ml utility extracts the inheritance relation from a Coq library by interacting with coqtop, and then executes Algorithm 1 to check the wellformedness and to generate assertions. The assertions generated from our running example are shown below. An assertion check_join t1 t2 t3 asserts that the join of t1 and t2 is t3, and check_join is implemented as a tactic that fails if the assertion is false. For instance, if we do not declare Ring.semiringType as a canonical instance, the assertion of line 9 fails and reports the following error.

There is no join of Ring.type and Semiring.type but it is expected to be Ring.type.

One may declare incorrect canonical instances that overwrite an existing join. For example, the join of groups and monoids must be groups; however, defining the following canonical instance in the Ring section overwrites this join. By declaring Ring.bad_monoid_groupType as a canonical instance, the join of Monoid.type and Group.type is still Group.type, but the join of Group.type and Monoid.type becomes Ring.type, because of asymmetry of the unification mechanism. The assertion of line 1 fails and reports the following error.

The join of Group.type and Monoid.type is Ring.type but it is expected to be Group.type.

This section reports the results of applying our tools to the MathComp library 1.7.0 and on recent development efforts to extend the hierarchy in MathComp using our tools. MathComp 1.7.0 provides the structures depicted in Fig. 1 , except comAlgType and comUnitAlgType, and lacked a few of the edges; thus, its hierarchy is quite large. Our coherence checking mechanism found 11 inconvertible multiple inheritance paths in the ssralg library. Fortunately, those paths concern proof terms and are intended to be irrelevant; hence, we can ensure no implicit coercion breaks the modularity of reasoning. Our well-formedness checking tool discovered 7 ambiguous joins, 8 missing unification hints, and one overwritten join due to an incorrect declaration of a canonical instance. These inheritance bugs were found and fixed with the help of our tools; thus, similar issues cannot be found in the later versions of MathComp.

The first issue was that inheritance from the CountRing structures (countZmodType and its subclasses with the prefix count) to the FinRing structures (finZmodType and its subclasses) was not implemented, and consequently it introduced 7 ambiguous joins. For instance, finZmodType did not inherit from countZmodType as it should; consequently, they became ambiguous joins of countType and zmodType. 6 out of 8 missing unification hints should infer

CountRing or FinRing structures. The other 2 unification hints are in numeric field (numFieldType and realFieldType) structures. Fixing the issue of missing inheritance from CountRing to FinRing was a difficult task without tool support. The missing inheritance itself was a known issue from before our tooling work, but the sub-hierarchy consisting of the GRing, CountRing, and FinRing structures in Fig. 1 is quite dense; as a result, it prevents the library developers from enumerating joins correctly without automation [38] .

The second issue was that the following canonical finType instance for extremal_group overwrote the join of finType and countType, which should be finType.

Canonical extremal_group_finType := FinType _ extremal_group_finMixin.

In this declaration, FinType is a packager [26, Sect. 7 ] that takes a type T and a Finite mixin of T as its arguments and construct a finType instance from the given mixin and the canonical countType instance for T. However, if one omits its first argument T with a placeholder as in the above, the packager may behave unpredictably as a unification hint. In the above case, the placeholder was instantiated with extremal_group_countType by type inference; as a result, it incorrectly overwrote the join of finType and countType.

Our tools can also help finding inheritance bugs when extending the hierarchy of MathComp, improve the development process by reducing the reviewing and maintenance burden, and allow developers and contributors to focus better on mathematical contents and other design issues. For instance, Hivert [24] added new structures of commutative algebras and redefined the field extension and splitting field structures to inherit from them. In this extension process, he fixed some inheritance issues with help from us and our tools; at the same time, we made sure there is no inheritance bug without reviewing the whole boilerplate code of structures. We ported the order sub-library of the mathcomp-finmap library [12] to MathComp, redefined numeric domain structures [10, Chap. 4] [11, Sect. 3.1] to inherit from ordered types, and factored out the notion of norms and absolute values as normed Abelian groups [1, Sect. 4.2] with the help of our tools [13, 36] . This modification resulted in approximately 10,000 lines of changes; thus, reducing the reviewing burden was an even more critical issue. This work is motivated by an improvement of the MathComp Analysis library [ 

This paper has provided a thorough analysis of the packed classes methodology, introduced two invariants that ensure the modularity of reasoning and the predictability of structure inference, and presented systematic ways to check those invariants. We implemented our invariant checking mechanisms as a part of the Coq system and a tool bundled with MathComp. With the help of these tools, many inheritance bugs in MathComp have been found and fixed. The MathComp development process has also been improved significantly.

Coq had no coherence checking mechanism before our work. Saïbi [32, Sect. 7 ] claimed that the coherence property "is too restrictive in practice" and "it is better to replace conversion by Leibniz equality to compare path coercions because Leibniz equality is a bigger relation than conversion". However, most proof assistants based on dependent type theories including Coq still rely heavily on conversion, particularly in their type checking/inference mechanisms. Coherence should not be relaxed with Leibniz equality; otherwise, the type mismatch problems described in Sect. 3 will occur. With our coherence checking mechanism, users can still declare inconvertible multiple inheritance at their own risk and responsibility, because ambiguous paths messages are implemented as warnings rather than errors. The Lean system has an implicit coercion mechanism based on type class resolution, that allows users to define and use non-uniform implicit coercions; thus, coherence checking can be more difficult. Actually, Lean has no coherence checking mechanism; thus, users get more flexibility with this approach but need to be careful about being coherent.

There are three kinds of approaches to defining mathematical structures in dependent type theories: unbundled, semi-bundled, and bundled approaches [46, Sect. 4.1.1]. The unbundled approach uses an interface that is parameterized by carriers and operators, and gathers axioms as its fields, e.g., [41] ; in contrast, the semi-bundled approach bundles operators together with axioms as in class_of records, but still places carriers as parameters, e.g., [46] . The bundled approach uses an interface that bundles carriers together with operators and axioms, e.g., packed classes and telescopes [26, Sect. 2.3] [9, 18, 29] . The above difference between definitions of interfaces, in particular, whether carriers are bundled or not, leads to the use of different instance resolution and inference mechanisms: type classes [22, 40] for the unbundled and semi-bundled approaches, and canonical structures or other unification hint mechanisms for the bundled approach. Researchers have observed unpredictable behaviors [23] and efficiency issues [46, Sect. 4.3] [41, Sect. 11] in inference with type classes; in contrast, structure inference with packed classes is predictable, and Theorem 5.1 states this predictability more formally, except for concrete instance resolution. The resolution of canonical structures is carried out by consulting a table of unification hints indexed by pairs of two head symbols and optionally with its recursive application and backtracking [21, Sect. 2.3] . The packed classes methodology is designed to use this recursive resolution not for structure inference [17, Sect. 2.3] but only for parametric instances [26, Sect. 4] such as lists and products, and not to use backtracking. Thus, there is no efficiency issue in structure inference, except that nested class records and chains of their projections exponentially slow down the conversion which flat variant of packed classes [14, Sect. 4] can mitigate. In the unbundled and semi-bundled approaches, a carrier may be associated with multiple classes; thus, inference of join and our work on structure inference (Sect. 4, 5, and 6) are problems specific to the bundled approach. A detailed comparison of type classes and packed classes has also been provided in [1] . There are a few mechanisms to extend the unification engines of proof assistants other than canonical structures that can implement structure inference for packed classes: unification hints [4] and coercions pullback [31] . For any of those cases, our invariants are fundamental properties to implement packed classes and structure inference, but the invariant checking we propose has not been made yet at all.

Packed classes require the systematic use of records, implicit coercions, and canonical structures. This leads us to automated generation of structures from their higher-level descriptions [14] , which is work in progress.

Competing inheritance paths in dependent type theory: a case study in functional analysis

A hierarchy of monadic effects for program verification using equational reasoning

Hints in unification

The matita interactive theorem prover

Theorem Proving in Lean

Implicit coercions in type systems

Coquelicot: a user-friendly library of real analysis for coq

Telescopic mappings in typed lambda calculus

Formalized algebraic numbers: construction and first-order theory. (Formalisation des nombres algébriques : construction

Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination

A finset and finmap library

Dispatching order and norm, and anticipating normed modules

Hierarchy Builder: algebraic hierarchies made easy in Coq with Elpi (system description) (2020)

The calculus of constructions

Generic proof tools and finite group theory. (Outils génériques de preuve et théorie des groupes finis)

Packaging mathematical structures

A constructive algebraic hierarchy in Coq

The undecidability of the second-order unification problem

A machine-checked proof of the odd order theorem

How to make ad hoc proof automation less ad hoc

Constructive type classes in isabelle

A review of the Lean theorem prover

Commutative algebras

Type classes and filters for mathematical analysis in Isabelle/HOL

Canonical structures for the working coq user

The lean theorem prover (system description)

The PCM library

Dependently typed records in type theory

Formalisation tools for classical analysis -a case study in control theory. (Outils pour la Formalisation en Analyse Classique -UneÉtude de Cas en Théorie du Contrôle)

Working with mathematical structures in type theory

Typing algorithm in type theory with inheritance

Applicationà la Théorie des Catégories. (Formalization of Mathematics in Type Theory. Generic tools of Modelisation and Demonstration. Application to Category Theory)

Coherence checking for coercions

Relax the ambiguous path condition of coercion

Non-distributive lattice structures

Supplementary materials of this manuscript

Fix inheritances from countalg to finalg

Mechanized verification of fine-grained concurrent programs

First-class type classes

Type classes for mathematics in type theory

The Coq Development Team: The Coq Proof Assistant Reference Manual

The PDF version with numbered sections is

The Coq Development Team: Sect. 8.2 "Implicit Coercions

The Mathematical Components project: The mathematical components repository

The mathlib Community: The Lean mathematical library

We appreciate the support from the STAMP (formerly MARELLE) project-team, INRIA Sophia Antipolis. In particular, we would like to thank Cyril Cohen and Enrico Tassi for their help in understanding packed classes and implementing our checking tools. We are grateful to Reynald Affeldt, Yoichi Hirai, Yukiyoshi Kameyama, Enrico Tassi, and the anonymous reviewers for helpful comments on early drafts. We are deeply grateful to Karl Palmskog for his careful proofreading and comments. We would like to thank the organizers and participants of The Coq Workshop 2019 where we presented preliminary work of this paper. In particular, an insightful question from Damien Pous was the starting point of our formal model of hierarchies presented in Sect. 5. This work was supported by JSPS Research Fellowships for Young Scientists and JSPS KAKENHI Grant Number 17J01683.