Advertisement

Competing Inheritance Paths in Dependent Type Theory: A Case Study in Functional Analysis

  • Reynald AffeldtEmail author
  • Cyril Cohen
  • Marie Kerjean
  • Assia Mahboubi
  • Damien Rouhling
  • Kazuhiko Sakaguchi
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 12167)

Abstract

This paper discusses the design of a hierarchy of structures which combine linear algebra with concepts related to limits, like topology and norms, in dependent type theory. This hierarchy is the backbone of a new library of formalized classical analysis, for the Coq proof assistant. It extends the Mathematical Components library, geared towards algebra, with topics in analysis. Issues of a more general nature related to the inheritance of poorer structures from richer ones arise due to this combination. We present and discuss a solution, coined forgetful inheritance, based on packed classes and unification hints.

Keywords

Formalization of mathematics Dependent type theory Packed classes Coq 

1 Introduction

Mathematical structures are the backbone of the axiomatic method advocated by Bourbaki [8, 9] to spell out mathematically relevant abstractions and establish the corresponding vocabulary and notations. They are instrumental in making the mathematical literature more precise, concise, and intelligible. Modern libraries of formalized mathematics also rely on hierarchies of mathematical structures to achieve modularity, akin to interfaces in generic programming. By analogy, we call instance a witness of a mathematical structure on a given carrier. Mathematical structures, as interfaces, are essential to factor out the shared vocabulary attached to their instances. This vocabulary comes in the form of formal definitions and generic theorems, but also parsable and printable notations, and sometimes delimited automation. Some mathematical structures are richer than others in the sense that they extend them. Like in generic programming, rich structures inherit the vocabulary attached to poorer structures. Working out the precise meaning of symbols of this shared vocabulary is usually performed by enhanced type inference, which is implemented using type classes [5, 27, 28] or unification hints [3, 17, 20, 24]. In particular, these mechanisms must automatically identify inheritance relations between structures.

This paper discusses the design of a hierarchy of mathematical structures supporting a Coq [30] formal library for functional analysis, i.e., the study of spaces of functions, and of structure-preserving transformations on them. The algebraic vocabulary of linear algebra is complemented with a suitable notion of “closeness” (e.g., topology, distance, norm), so as to formalize convergence, limits, size, etc. This hierarchy is based on the packed classes methodology [17, 20], which represents structures using dependent records. The library strives to provide notations and theories that are as generic as they would be on paper. It is an extension of the “Mathematical Components” library [32] (hereafter MathComp), which is geared towards algebra. This extension is inspired by the Coquelicot real analysis library [7], which has its own hierarchy.

Fusing these two hierarchies, respectively from the MathComp and Coquelicot libraries, happens to trigger several interesting issues, related to inheritance relations. Indeed, when several constructions compete to infer an instance of the poorer structure, the proof assistant displays indiscernible notations, or keywords, for constructions that are actually different. This issue is not at all specific to the formalization of functional analysis: actually, the literature reports examples of this exact problem but in different contexts, e.g., in Lean’s mathlib [11, 33]. It is however more likely to happen when organizing different flavors of mathematics in a same coherent corpus, as this favors the presence of problematic competing constructions. Up to our knowledge, the problem of competing inheritance paths in hierarchies of dependent records was never discussed per se, beyond some isolated reports of failure, and of ad hoc solutions. We thus present and discuss a general methodology to overcome this issue, coined forgetful inheritance, based on packed classes and unification hints.

The paper is organized as follows: in Sect. 2, we recall the packed classes methodology, using a running example. Section 3 provides two concrete examples of the typical issues raised by the presence of competing inheritance paths, before describing the general issue, drawing its solution, and comparing with other type-class-like mechanisms. Finally, Sect. 4 describes the design of our hierarchy of structures for functional analysis, and its features, before Sect. 5 concludes.

2 Structures, Inheritance, Packed Classes

We recall some background on the representation of mathematical structures in dependent type theory, and on the construction of hierarchies using packed classes. For that purpose, we use a toy running example (see the accompanying file Open image in new window  [1]), loosely based on the case study presented in Sect. 4.

2.1 Dependent Records

In essence, a mathematical structure attaches to a carrier set some data (e.g., operators of the structure, collections of subsets of the carrier) and prescribed properties about these data, called the axioms of the structure. The Calculus of Inductive Constructions [16], as implemented, e.g., by Coq [30], Agda [29], or Lean [21, 22], provides a dependent record construct, which allows to represent a given mathematical structure as a type, and its instances as terms of that type. A dependent record is an inductive type with a single constructor, which generalizes dependent pairs to dependent tuples. The elements of such a tuple are the arguments of the single constructor. They form a telescope [10], i.e., collection of terms, whose types can depend on the previous items in the tuple.

For example, the Open image in new window record type formalizes a structure with two operators, Open image in new window and Open image in new window , and one axiom Open image in new window . This structure is a toy generalisation for the mathematical notion of normed module. Its purpose is to simulate one basic axiom of norms via a minimal amount of constructors. Thus, the Open image in new window has a single constructor named Open image in new window , and four projections (also called fields) Open image in new window , Open image in new window , Open image in new window , and Open image in new window , onto the respective components of the tuple:
The Open image in new window axioms makes use of Open image in new window to avoid the introduction of a Open image in new window of carrier type. Fields have a dependent type, parameterized by the one of the structure:
In this case, declaring an instance of this structure amounts to defining a term of type Open image in new window , which packages the corresponding instances of carrier, data, and proofs. For example, here is an instance on carrier Open image in new window (using the Open image in new window and Open image in new window functions from the standard library resp. as the Open image in new window and the Open image in new window operators):

2.2 Inference of Mathematical Structures

Hierarchies of mathematical structures are formalized by nesting dependent records but naive approaches quickly incur scalability issues. Packed classes [17, 20] provide a robust and systematic approach to the organization of structures into hierarchies. In this approach, a structure is a two-field record, which associates a carrier with a class. A class encodes the inheritance relations of the structure and packages various mixins. Mixins in turn provide the data, and their properties. In Coq, Open image in new window and Open image in new window are synonyms, but we reserve the latter for record types that represent actual structures. Let us explain the basics of inference of mathematical structures with packed classes by replacing the structure of Sect. 2.1 with two structures represented as packed classes. The first one provides just a binary operator:
Since the Open image in new window structure is expected to be the bottom of the hierarchy, we are in the special class where the class is the same as the mixin (here, the class would be equal to Open image in new window ). To endow the operator Open image in new window with a generic infix notation, we introduce a definition Open image in new window , parameterized by an instance of Open image in new window . In the definition of the corresponding notation, the wildcard Open image in new window is a placeholder for the instance of Open image in new window to be inferred from the context.
We can build an instance of the Open image in new window structure with the type of integers as the carrier and the subtraction of integers for the operator:
But defining an instance is not enough to make the  Open image in new window notation available:
To type-check the expression just above, Coq needs to fill the wildcard in the Open image in new window notation, which amounts to solving the equation Open image in new window , where Open image in new window is the definitional equality (i.e., equality up to the conversion rules of Coq type theory [30, Section “Conversion Rules” in Chapter “Calculus of Constructions”]). One can indicate that the instance Open image in new window is a canonical solution by declaring it as a canonical instance:
This way, Coq fills the wildcard in Open image in new window with Open image in new window and retrieves as expected the subtraction for integers.

2.3 Inheritance and Packed Classes

We introduce a second structure class to illustrate how inheritance is implemented. This structure extends the Open image in new window structure of Sect. 2.2 with a norm operator and a property (the fact that Open image in new window is 0 for any Open image in new window ):
The new mixin for the norm appears at line 1 (it takes a Open image in new window structure as parameter), the new class appears at line 4, and the structure1 at line 7. It is the class that defines the inheritance relation between Open image in new window and Open image in new window (at line 6 precisely). The definitions above are however not enough to achieve proper inheritance. For example, Open image in new window does not yet enjoy the Open image in new window notation coming with the Open image in new window structure:
Here, Coq tries to solve the following equation2:
The solution consists in declaring a canonical way to build a Open image in new window structure out of a Open image in new window structure in the form of a function that Coq can use to solve the equation above (using Open image in new window in this particular case):

3 Inheritance with Packed Classes and type classes

When several inheritance paths compete to establish that one structure extend the other, the proof assistant may display misleading information to the user and prevent proofs.

3.1 Competing Inheritance Paths

We extend the running example of Sect. 2 with a third and last structure. Our objective is to implement a toy generalisation of the mathematical notion of pseudometric space. This is done by introducing a reflexive relation mimicking the belonging of one of the argument to a unit ball around the other argument. The Open image in new window structure below provides a binary relation (line 2) together with a property of reflexivity (line 3):

For the sake of the example, we furthermore declare a canonical way of building a Open image in new window structure out of a Open image in new window structure:
We first illustrate the issue using a construction (here the Cartesian product) that preserves structures, and that is used to build canonical instances. First, we define the product of Open image in new window structures, and tag it as canonical:
Similarly, we define canonical products of Open image in new window and Open image in new window :
The problem is that our setting leads Coq’s type-checker to fail in unexpected ways, as illustrated by the following example:
The hypothesis Open image in new window applies to any goal Open image in new window where the type of  Open image in new window is of type Open image in new window , so that one may be led to think that it should also apply in the case of a product of Open image in new window , since there is a canonical way to build one. What happens is that the type-checker is looking for an instance of a normed module that satisfies the following equation:
while the canonical instance Coq infers is Open image in new window , which does not satisfy the equation. In particular, Open image in new window is definitionally equal to Open image in new window on the left-hand side and Open image in new window on the right-hand side: the two are not definitionally equal. One can describe the problem as the fact that the diagram in Fig. 1 does not commute definitionally.
Fig. 1.

Diagrammatic explanation for the failure of the first example of Sect. 3.1

This is of course not specific to Cartesian products and similar problems would also occur when lifting dependent products, free algebras, closure, completions, etc., on metric spaces, topological groups, etc. as well as in simpler settings without generic constructions as illustrated by our last example.

As a consequence of the definition of Open image in new window , the following lemma about balls is always true for any Open image in new window :

For the sake of the example, we define canonical instances of the Open image in new window and Open image in new window structures with integers:

Since the generic lemma Open image in new window holds, the user might expect to use it to prove a version specialized to integers. This is however not the case as the following script shows:

The problem is that on the left-hand side Coq infers the instance Open image in new window with the Open image in new window relation, while on the right-hand side it infers the instance Open image in new window whose Open image in new window is definitionally equal to Open image in new window , which is not definitionally equal to the newly defined Open image in new window . In other words, the problem is the multiple ways to construct a “canonical instance” of Open image in new window with carrier Open image in new window , as in Fig. 2.
Fig. 2.

Diagrammatic explanation for the type-checking failure of the second example of Sect. 3.1: the dashed arrows represent the inference of an instance from the carrier type; the outer diagrams commutes, while the inner one does not

The solution to the problems explained in this section is to ensure definitional equality by including poorer structures into richer ones; this way, “deducing” one structure from the other always amounts to erasure of data, and this guarantees there is a unique and canonical way of getting it. We call this technique forgetful inheritance, as it is reminiscent of forgetful functors in category theory.

3.2 Forgetful Inheritance with Packed Classes

When applied to the first problem exposed in Sect. 3.1, forgetful inheritance makes the diagram of Fig. 1 commute definitionally. Indeed, the only way to achieve commutation is to have Open image in new window be a mere erasure. This means that one needs to include inside each instance of Open image in new window a canonical Open image in new window (line 7 below). Furthermore the Open image in new window must record the compatibility between the operators Open image in new window and Open image in new window (line 4 below):
Since every Open image in new window includes a canonical Open image in new window , the construction of the canonical Open image in new window given a Open image in new window is exactly a projection:
As a consequence, the equation
holds with Open image in new window and the diagram in Fig. 1 (properly updated with the new Open image in new window structure) commutes definitionally, and so does the diagram in Fig. 2, for the same reasons.

Factories. Because of the compatibility axioms required by forgetful inheritance, the formal definition of a structure can depart from the expected presentation. In fact, with forgetful inheritance, the very definition of a mathematical structure should be read in factories, i.e., functions that construct the mixins starting from only the expected axioms. And Open image in new window records are rather interfaces, in a software engineering terminology. Note that just like there can be several equivalent presentations of a same mathematical stuctures, several mixins can be associated with a same target Open image in new window .

In our running example, one can actually derive, from the previously defined Open image in new window , two mixins for both Open image in new window :
(where the Open image in new window relation is the one induced by the norm, by construction) and Open image in new window :
These two mixins make Open image in new window the source of two factories we mark as coercions, in order to help building two structures:

The second part of this paper provides concrete examples of factories for our hierarchy for functional analysis.

3.3 Forgetful Inheritance with type classes

Type class mechanisms [5, 27, 28] propose an alternative implementation of hierarchies. Inference relations are coded using parameters rather than projections, and proof search happens by enhancing the resolution of implicit arguments. But the issue of competing inheritance paths does not pertain to the inference mechanism at stake, nor to the prover which implements them. Its essence rather lies in the non definitionally commutative diagrams as in Fig. 1 and Fig. 2.

We illustrate this with a type classes version of our examples, in both Coq and Lean, using a semi-bundled approach (see the accompanying files Open image in new window and Open image in new window  [1]). Compared to the packed class approach, hierarchies implemented using type classes remove the structure layer, which packages the carrier and the class. Hence our example keeps only the records whose name starts with is, declares them as type classes, and substitutes Open image in new window declarations with appropriate Open image in new window declarations.

The choice on the level of bundling in the resulting classes, i.e., what are parameters of the record, and what are its fields, is not unique. For example, one may choose to formalize rings as groups extended with additional operations and axioms, or as a class on a type which is also a group.
By contrast, a structure in the packed class approach must always package with its carrier every mixins and classes that characterize the structure. The transposition of forgetful inheritance to type class would apply to fully bundled classes (where all the operations and axioms are bundled but not the carrier).

Because it triggers no “backtracking search”, the use of packed classes and unification hints described in this paper avoids some issues encountered in mathlib [33, Sect. 4.3], which are more explicitly detailed in the report on the implementation of type classes in Lean 4 [26]. We do not know either how a type class version of forgetful inheritance would interact with the performance issues described in the latter paper, or whether tabling helps. Moreover, with the current implementations of type classes in both Coq and Lean, different choices on bundling may have dramatic consequences on resolution feasibility and performance. For example, former experiments in rewriting MathComp with type classes in Coq did not scale up to modules on a ring. Incidentally, our companion file Open image in new window illustrates some predictability issues of the current implementation of Coq type classes.

4 The Mathematical Components Analysis Library

The Coquelicot library comes with its own hierarchy of mathematical structures and the intent of the MathComp-Analysis library is to improve it with the algebraic constructs of the MathComp library, for the analysis of multivariate functions for example. This section explains three applications of forgetful inheritance that solve three design issues of a different nature raised by merging MathComp and Coquelicot, as highlighted in Fig. 3.

We begin by an overview of the mathematical notions we deal with in this section. A topological space is a set endowed with a topology, i.e., a total collection of open sets closed under finite intersection and arbitrary unions. Equivalently, a topology can be described by the neighborhood filter of each point. A neighborhood of a point x is a set containing an open set around x; the neighborhood filter of a point x is the set of all neighborhoods of x. In MathComp-Analysis, neighborhood filters are the primary component of topological spaces. Pseudometric spaces are intermediate between topological and metric spaces. They were introduced as the minimal setting to handle Cauchy sequences. In Coquelicot, pseudometric spaces are called “uniform spaces” and are formalized as spaces endowed with a suitable Open image in new window predicate. This is the topic of Sect. 4.1. Coquelicot also provides normed spaces, i.e., \(\mathbb {K}\)-vector spaces E endowed with a suitable norm. On the other hand, in MathComp, the minimal structure with a norm operator corresponds to numerical domains [12, Chap. 4][13, Sect. 3.1], i.e., integral domains with order and absolute value. This situation led to a generalization of MathComp described in Sect. 4.2. Finally, in Sect. 4.3, we explain how to do forgetful inheritance across the two distinct libraries MathComp and MathComp-Analysis.
Fig. 3.

Excerpt of MathComp and MathComp-Analysis hierarchies. Each rounded box corresponds to a mathematical structure except for (Com)(Unit)Ring that corresponds to several structures [17]. Dotted boxes correspond to mathematical structures introduced in Sect. 4.2 and Sect. 4.3. Thick, red arrows correspond to forgetful inheritance.

4.1 Forgetful Inheritance from Pseudometric to Topological Spaces

When formalizing topology, we run into a problem akin to Sect. 3.1 because we face several competing notions of neighborhoods; we solve this issue with forgetful inheritance as explained in Sect. 3.

A neighborhood of a point p can be defined at the level of topological spaces using the notion of open as a set A that contains an open set containing p:
$$\begin{aligned} \exists B.\ B \text { is open, } p \in B \text { and } B \subseteq A. \end{aligned}$$
(1)
or at the level of pseudometric spaces as a set A that contains a ball containing p:
$$\begin{aligned} \exists \varepsilon > 0.\ B_{\varepsilon }(p) \subseteq A. \end{aligned}$$
(2)
We ensure these two definitions of neighborhoods coincide by adding to mixins compatibility axioms that constrain a shared function. The function in question maps a point to a set of neighborhoods (hereafter Open image in new window ), it is shared between the mixins for topological and pseudometric spaces, and constrained by the definitions of open set and ball as in Formulas (1) and (2). More precisely, the mixin for topological spaces introduces the set of open sets (see line 3 below) and defines neighborhoods as in Formula (1) (at line 5). We complete the definition by specifying with a specific axiom (not explained in detail here) that neighborhoods are proper filters (line 4) and with an alternative characterization of open set (namely that an open set is a neighborhood of all of its points, line 6).
The mixin for pseudometric spaces introduces the notion of balls (line 10) and defines neighborhoods as in Formula (2) (at line 12, Open image in new window corresponds to the set of supersets of balls). The rest of the definition (line 11) are axioms about  Open image in new window which are omitted for lack of space.

Here, our definition of topological space departs from the standard definition as a space endowed with a family of subsets containing the full set and the empty set and closed under union and by finite intersection. However, the latter definition can be recovered from the former. Factories (see Sect. 3.2) are provided for users who want to give only  Open image in new window and to infer  Open image in new window (using [31, file topology.v, definition topologyOfOpenMixin]), or the other way around.

4.2 Forgetful Inheritance from Numerical Domain to Normed Abelian Group

The second problem we faced when developing the MathComp-Analysis library is the competing formal definitions of norms and absolute values. The setting is more complicated than Sect. 4.1 as it involves amending the hierarchy of mathematical structures of the MathComp library.

While the codomain of a norm is always the set of (non-negative) reals, an absolute value on a Open image in new window is always an endofunction Open image in new window of type Open image in new window . Thanks to this design choice, the absolute value preserves some information about its input, e.g., the integrality of an integer. On the other hand, the Coquelicot library also had several notions of norms: the absolute value of the real numbers (from the Coq standard library), the absolute value of a structure for rings equipped with an absolute value, and the norm operator of normed modules (the latter two are Coquelicot-specific).

We hence generalize the norm provided by the MathComp library to encompass both absolute values on numerical domains and norms on vector spaces, and share notation and lemmas. This is done by introducing a new structure in MathComp called Open image in new window , for normed Abelian groups, since Abelian groups are called \(\mathbb {Z}\)-modules in MathComp. This structure is now the poorest structure with a norm, which every subsequent normed type will inherit from.

The definition of the Open image in new window structure requires to solve a mutual dependency problem. Indeed, to state the fundamental properties of norms, such as the triangle inequality, the codomain of the norm function should be at least an ordered and normed Abelian group, requiring Open image in new window to be parameterized by such a structure. However the codomain should also inherit from Open image in new window to share the notations for norm and absolute value.

Our solution is to dispatch the order and the norm originally contained in Open image in new window between normed Abelian groups Open image in new window and partially ordered types Open image in new window as depicted in Fig. 3. We define the two following mixins for Open image in new window and Open image in new window .
Now we define Open image in new window (which is an abbreviation for Open image in new window ) using these two mixins but without declaring inheritance from Open image in new window (yet to be defined). More precisely, the class of Open image in new window includes the mixin for Open image in new window (at line 5 below), which will allow for forgetful inheritance:
Finally, we define the class of Open image in new window , parameterized by a Open image in new window :
It is only then that we declare inheritance from the Open image in new window structure to Open image in new window , effectively implementing forgetful inheritance. We finally end up with a norm of the general type
Illustration: sharing of norm notation and lemmas. As an example, we explain the construction of two norms and show how they share notation and lemmas. In MathComp, the type of matrices is Open image in new window where Open image in new window is the type of coefficients. The norm Open image in new window takes the maximum of the absolute values of the coefficients:
This definition uses the generic big operator [6] to define a “big max” operation out of the binary operation  Open image in new window . Similarly, we define a norm for pairs of elements by taking the maximum of the absolute value of the two projections3:
We then go on proving that these definitions satisfy the properties of the norm and declare canonical instances of Open image in new window for matrices and pairs (see [31] for details). All this setting is of course carried out in advance and the user only sees one notation and one set of lemmas (for example Open image in new window for the triangle inequality), so that (s)he can mix various norms transparently in the same development, as in the following two examples:

One could fear that the newly introduced structures make the library harder to use since that, to declare a canonical Open image in new window instance, a user also needs now to declare canonical Open image in new window and Open image in new window instances of the same type. Here, the idea of factories (Sect. 3.2) comes in handy for the original Open image in new window mixin has been re-designed as a factory producing Open image in new window , Open image in new window , and Open image in new window mixins in order to facilitate their declaration.

4.3 Forgetful Inheritance from Normed Modules to Pseudometric Spaces

The combination of the MathComp library with topological structures ultimately materializes as a mathematical structure for normed modules. It is made possible by introducing an intermediate structure that combines norm (from algebra) with pseudometric (from topology) into normed Abelian groups. The precise justification for this first step is as follows.

Since normed Abelian groups have topological and pseudometric space structures induced by the norm, Open image in new window should inherit from Open image in new window . To do so, we can (1) insert a new structure above Open image in new window , or (2) create a common extension of Open image in new window and Open image in new window . We choose (2) to avoid amending the MathComp library. This makes both Open image in new window and its extension Open image in new window normed Abelian groups, where the former is inadequate for topological purposes.

The only axiom of this extension is the compatibility between the pseudometric and the norm, as expressed line 5 below, where Open image in new window has been seen in Sect. 4.1 and the right-hand side represents all the ternary relations \(\lambda x,\varepsilon ,y.\,|x-y|<\varepsilon \):
The extension is effectively performed by using this mixin in the following class definition at line 12 (see also Fig. 3):
Finally, the bridge between algebraic and topological structures is completed by a common extension of a normed Abelian group ( Open image in new window ) with a left-module ( Open image in new window from the MathComp library, which provides scalar multiplication), extended with the axiom of linearity of the norm for the scalar product (line 5 below).
One can again observe here the overloaded notation for norms explained in Sect. 4.2. The accompanying file Open image in new window  [1] provides an overview of MathComp-Analysis operations regarding norms and scalar notations.

We ensured that the structure of normed modules indeed serves its intended purpose of enabling multivariate functional analysis by generalizing existing theories of Bachmann-Landau notations and of differentiation [2, Sect. 4].

5 Conclusion and Related Work

This paper has two main contributions: forgetful inheritance using packed classes, and the hierarchy of the MathComp-Analysis library. The latter library is still in its infancy and covers far less real and complex analysis than the libraries available in HOL Light and Isabelle/HOL [19, 23]. However, differences in foundations matter here, and the use of dependent types in type-class-like mechanisms is instrumental in the genericity of notations illustrated in this paper. Up to our knowledge, no other existing formal library in analysis has comparable sharing features.

The methodology presented in this paper to tame competing inheritance paths in hierarchies of dependent records is actually not new. The original description of packed classes [17, end of Sect. 3.1] already mentions that a choice operator (in fact, a mixin) should be included in the definition of a structure for countable types, even if choice operators can be defined for countable types in Coq without axiom. Yet, although the MathComp library uses forgetful inheritance at several places in its hierarchy, this solution was never described in earlier publications, nor was the issue precisely described. Proper descriptions, as well as the comparison with other inference techniques, are contributions of the present paper.

As explained in Sect. 3.3, type classes based on augmented inference of implicit arguments also allow for a variant of forgetful inheritance. For instance, Buzzard et al. mention that this pattern is used for defining metric spaces both in Lean and Isabelle/HOL’s libraries [11, Sect. 3]. In the same paper, the authors describe another formalization issue, about completing abelian groups and rings, pertaining to the same problem [11, Sect. 5.3], and which can be solved as well using forgetful inheritance.

Extensional flavors of dependent type theory could make the problematic diagram in Fig. 1 commute judgmentally. However, to the best of our knowledge, the related tools [4, 15] available at the time of writing do not implement any of the type class mechanisms discussed here.

Packed classes, and forgetful inheritance, already proved robust and efficient enough to formalize and populate large hierarchies [18], where “large” applies both to the number of structures and to the number of instances. Arguably, this approach also has drawbacks: defining deep hierarchies becomes quite verbose, and inserting new structures is tedious and error-prone. We argue that, compared to their obvious benefits in control and efficiency of the proof search, this is not a fundamental issue. As packed classes are governed by systematic patterns and invariants, this rather calls for more inspection [25] and automated generation [14] tooling, which is work in progress.

Footnotes

  1. 1.

    The notation :> in the structure declares the carrier as a coercion [30, Chapter “Implicit Coercions”], which means that Coq has the possibility to use the function Open image in new window to fix type-mismatches, transparently for the user.

  2. 2.

    The application of Open image in new window is not necessary in our case thanks to the coercion explained in footnote (see footnote 1).

  3. 3.

    The actual code of Open image in new window and Open image in new window is slightly more complicated because it uses a type for non-negative numeric values, see [31, file normedtype.v].

Notes

Acknowledgments

The authors are grateful to Georges Gonthier for the many fruitful discussions that helped rewriting parts of MathComp and MathComp-Analysis library. We also thank Arthur Charguéraud and all the anonymous reviewers for their comments on the successive versions of this paper.

References

  1. 1.
    Affeldt, R., Cohen, C., Kerjean, M., Mahboubi, A., Rouhling, D., Sakaguchi, K.: Formalizing functional analysis structures in dependent type theory (accompanying material). https://math-comp.github.io/competing-inheritance-paths-in-dependent-type-theory (2020), contains the files packed_classes.v, packed_classes.v, type_classes.lean, and scalar_notations.v, and a stand-alone archive containing snapshots of the Mathematical Components [32] and Analysis [31] libraries
  2. 2.
    Affeldt, R., Cohen, C., Rouhling, D.: Formalization techniques for asymptotic reasoning in classical analysis. J. Formaliz. Reason. 11, 43–76 (2018)MathSciNetzbMATHGoogle Scholar
  3. 3.
    Asperti, A., Ricciotti, W., Sacerdoti Coen, C., Tassi, E.: Hints in unification. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 84–98. Springer, Heidelberg (2009).  https://doi.org/10.1007/978-3-642-03359-9_8CrossRefzbMATHGoogle Scholar
  4. 4.
    Bauer, A., Gilbert, G., Haselwarter, P.G., Pretnar, M., Stone, C.A.: Design and implementation of the andromeda proof assistant. CoRR abs/1802.06217 (2018). http://arxiv.org/abs/1802.06217
  5. 5.
    Bauer, A., Gross, J., Lumsdaine, P.L., Shulman, M., Sozeau, M., Spitters, B.: The HoTT library: a formalization of homotopy type theory in Coq. In: 6th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP 2017), Paris, France, 16–17 January 2017, pp. 164–172. ACM (2017)Google Scholar
  6. 6.
    Bertot, Y., Gonthier, G., Ould Biha, S., Pasca, I.: Canonical big operators. In: Mohamed, O.A., Muñoz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 86–101. Springer, Heidelberg (2008).  https://doi.org/10.1007/978-3-540-71067-7_11CrossRefGoogle Scholar
  7. 7.
    Boldo, S., Lelay, C., Melquiond, G.: Coquelicot: a user-friendly library of real analysis for Coq. Math. Comput. Sci. 9(1), 41–62 (2015)MathSciNetCrossRefGoogle Scholar
  8. 8.
    Bourbaki, N.: The architecture of mathematics. Am. Math. Mon. 57(4), 221–232 (1950), http://www.jstor.org/stable/2305937
  9. 9.
    Bourbaki, N.: Théorie des ensembles. Éléments de mathématique. Springer (2006). Original Edition published by Hermann, Paris (1970)Google Scholar
  10. 10.
    de Bruijn, N.G.: Telescopic mappings in typed lambda calculus. Inf. Comput. 91(2), 189–204 (1991)MathSciNetCrossRefGoogle Scholar
  11. 11.
    Buzzard, K., Commelin, J., Massot, P.: Formalising perfectoid spaces. In: 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2020), New Orleans, LA, USA, 20–21 January 2020, pp. 299–312. ACM (2020)Google Scholar
  12. 12.
    Cohen, C.: Formalized algebraic numbers: construction and first-order theory. (Formalisation des nombres algébriques : construction et théorie du premier ordre). Ph.D. thesis, Ecole Polytechnique X (2012). https://pastel.archives-ouvertes.fr/pastel-00780446
  13. 13.
    Cohen, C., Mahboubi, A.: Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination. Logic. Methods Comput. Sci. 8(1) (2012).  https://doi.org/10.2168/LMCS-8(1:2)2012
  14. 14.
    Cohen, C., Sakaguchi, K., Tassi, E.: Hierarchy Builder: algebraic hierarchies made easy in Coq with Elpi (2020). Accepted in the proceedings of FSCD 2020. https://hal.inria.fr/hal-02478907
  15. 15.
    Constable, R.L., et al.: Implementing Mathematics with the NuPRL Proof Development System. Prentice-Hall, Upper Saddle River (1986)Google Scholar
  16. 16.
    Coquand, T., Paulin, C.: Inductively defined types. In: Martin-Löf, P., Mints, G. (eds.) COLOG 1988. LNCS, vol. 417, pp. 50–66. Springer, Heidelberg (1990).  https://doi.org/10.1007/3-540-52335-9_47CrossRefGoogle Scholar
  17. 17.
    Garillot, F., Gonthier, G., Mahboubi, A., Rideau, L.: Packaging mathematical structures. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 327–342. Springer, Heidelberg (2009).  https://doi.org/10.1007/978-3-642-03359-9_23CrossRefGoogle Scholar
  18. 18.
    Gonthier, G., et al.: A machine-checked proof of the odd order theorem. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 163–179. Springer, Heidelberg (2013).  https://doi.org/10.1007/978-3-642-39634-2_14
  19. 19.
    Harrison, J.: The HOL Light System REFERENCE (2017). https://www.cl.cam.ac.uk/~jrh13/hol-light/index.html
  20. 20.
    Mahboubi, A., Tassi, E.: Canonical structures for the working Coq user. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 19–34. Springer, Heidelberg (2013).  https://doi.org/10.1007/978-3-642-39634-2_5CrossRefGoogle Scholar
  21. 21.
    Microsoft Reasearch: L\(\exists \forall \)N THEOREM PROVER (2020). https://leanprover.github.io
  22. 22.
    de Moura, L., Kong, S., Avigad, J., van Doorn, F., von Raumer, J.: The lean theorem prover (System Description). In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS (LNAI), vol. 9195, pp. 378–388. Springer, Cham (2015).  https://doi.org/10.1007/978-3-319-21401-6_26CrossRefGoogle Scholar
  23. 23.
    Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle HOL: A Proof Assistant for Higher-Order Logic. Springer (2019). https://isabelle.in.tum.de/doc/tutorial.pdf
  24. 24.
    Saïbi, A.: Outils Génériques de Modélisation et de Démonstration pour la Formalisation des Mathématiques en Théorie des Types. Application à la Théorie des Catégories. (Formalization of Mathematics in Type Theory. Generic tools of Modelisation and Demonstration. Application to Category Theory). Ph.D. thesis, Pierre and Marie Curie University, Paris, France (1999)Google Scholar
  25. 25.
    Sakaguchi, K.: Validating mathematical structures. In: Peltier, N., Sofronie-Stokkermans, V. (eds.) IJCAR 2020. LNAI, vol. 12167, pp. 138–157. Springer, Heidelberg (2020)Google Scholar
  26. 26.
    Selsam, D., Ullrich, S., de Moura, L.: Tabled typeclass resolution (2020). https://arxiv.org/abs/2001.04301
  27. 27.
    Sozeau, M., Oury, N.: First-class type classes. In: Mohamed, O.A., Muñoz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 278–293. Springer, Heidelberg (2008).  https://doi.org/10.1007/978-3-540-71067-7_23CrossRefGoogle Scholar
  28. 28.
    Spitters, B., van der Weegen, E.: Type classes for mathematics in type theory. Math. Struct. Comput. Sci. 21(4), 795–825 (2011)MathSciNetCrossRefGoogle Scholar
  29. 29.
    The Agda Team: The Agda User Manual (2020). https://agda.readthedocs.io/en/v2.6.0.1. Version 2.6.0.1
  30. 30.
    The Coq Development Team: The Coq Proof Assistant Reference Manual. Inria (2019). https://coq.inria.fr. Version 8.10.2
  31. 31.
    The Mathematical Components Analysis Team: The Mathematical Components Analysis library (2017). https://github.com/math-comp/analysis
  32. 32.
    The Mathematical Components Team: The Mathematical Components library (2007). https://github.com/math-comp/math-comp
  33. 33.
    The mathlib Community: The lean mathematical library. In: 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2020), New Orleans, LA, USA, 20–21 January 2020, pp. 367–381. ACM (2020)Google Scholar

Copyright information

© Springer Nature Switzerland AG 2020

Authors and Affiliations

  • Reynald Affeldt
    • 1
    Email author
  • Cyril Cohen
    • 2
  • Marie Kerjean
    • 3
  • Assia Mahboubi
    • 3
  • Damien Rouhling
    • 4
  • Kazuhiko Sakaguchi
    • 5
  1. 1.National Institute of Advanced Industrial Science and Technology (AIST)TsukubaJapan
  2. 2.Université Côte d’Azur, InriaSophia AntipolisFrance
  3. 3.Inria, Rennes-Bretagne AtlantiqueRennesFrance
  4. 4.Inria & Université de Strasbourg, CNRS, ICube, Nancy-Grand EstVillers-lès-NancyFrance
  5. 5.University of TsukubaTsukubaJapan

Personalised recommendations