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.
You have full access to this open access chapter, Download conference paper PDF
Similar content being viewed by others
Keywords
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 [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 record type formalizes a structure with two operators, and , and one axiom . 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 has a single constructor named , and four projections (also called fields) , , , and , onto the respective components of the tuple:
The axioms makes use of to avoid the introduction of a 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 , which packages the corresponding instances of carrier, data, and proofs. For example, here is an instance on carrier (using the and functions from the standard library resp. as the and the 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, and 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 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 ). To endow the operator with a generic infix notation, we introduce a definition , parameterized by an instance of . In the definition of the corresponding notation, the wildcard is a placeholder for the instance of to be inferred from the context.
We can build an instance of the 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 notation available:
To type-check the expression just above, Coq needs to fill the wildcard in the notation, which amounts to solving the equation , where 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 is a canonical solution by declaring it as a canonical instance:
This way, Coq fills the wildcard in with 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 structure of Sect. 2.2 with a norm operator and a property (the fact that is 0 for any ):
The new mixin for the norm appears at line 1 (it takes a structure as parameter), the new class appears at line 4, and the structureFootnote 1 at line 7. It is the class that defines the inheritance relation between and (at line 6 precisely). The definitions above are however not enough to achieve proper inheritance. For example, does not yet enjoy the notation coming with the structure:
Here, Coq tries to solve the following equationFootnote 2:
The solution consists in declaring a canonical way to build a structure out of a structure in the form of a function that Coq can use to solve the equation above (using 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 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 structure out of a 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 structures, and tag it as canonical:
Similarly, we define canonical products of and :
The problem is that our setting leads Coq’s type-checker to fail in unexpected ways, as illustrated by the following example:
The hypothesis applies to any goal where the type of is of type , so that one may be led to think that it should also apply in the case of a product of , 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 , which does not satisfy the equation. In particular, is definitionally equal to on the left-hand side and 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.
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 , the following lemma about balls is always true for any :
For the sake of the example, we define canonical instances of the and structures with integers:
Since the generic lemma 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 with the relation, while on the right-hand side it infers the instance whose is definitionally equal to , which is not definitionally equal to the newly defined . In other words, the problem is the multiple ways to construct a “canonical instance” of with carrier , as in Fig. 2.
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 be a mere erasure. This means that one needs to include inside each instance of a canonical (line 7 below). Furthermore the must record the compatibility between the operators and (line 4 below):
Since every includes a canonical , the construction of the canonical given a is exactly a projection:
As a consequence, the equation
holds with and the diagram in Fig. 1 (properly updated with the new 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 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 .
In our running example, one can actually derive, from the previously defined , two mixins for both :
(where the relation is the one induced by the norm, by construction) and :
These two mixins make 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 and [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 declarations with appropriate 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 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 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.
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:
or at the level of pseudometric spaces as a set A that contains a ball containing p:
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 ), 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, corresponds to the set of supersets of balls). The rest of the definition (line 11) are axioms about 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 and to infer (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 is always an endofunction of type . 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 , 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 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 to be parameterized by such a structure. However the codomain should also inherit from to share the notations for norm and absolute value.
Our solution is to dispatch the order and the norm originally contained in between normed Abelian groups and partially ordered types as depicted in Fig. 3. We define the two following mixins for and .
Now we define (which is an abbreviation for ) using these two mixins but without declaring inheritance from (yet to be defined). More precisely, the class of includes the mixin for (at line 5 below), which will allow for forgetful inheritance:
Finally, we define the class of , parameterized by a :
It is only then that we declare inheritance from the structure to , 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 where is the type of coefficients. The norm 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 . Similarly, we define a norm for pairs of elements by taking the maximum of the absolute value of the two projectionsFootnote 3:
We then go on proving that these definitions satisfy the properties of the norm and declare canonical instances of 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 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 instance, a user also needs now to declare canonical and instances of the same type. Here, the idea of factories (Sect. 3.2) comes in handy for the original mixin has been re-designed as a factory producing , , and 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, should inherit from . To do so, we can (1) insert a new structure above , or (2) create a common extension of and . We choose (2) to avoid amending the MathComp library. This makes both and its extension 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 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 ( ) with a left-module ( 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 [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.
Notes
- 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 to fix type-mismatches, transparently for the user.
- 2.
The application of is not necessary in our case thanks to the coercion explained in footnote (see footnote 1).
- 3.
The actual code of and is slightly more complicated because it uses a type for non-negative numeric values, see [31, file normedtype.v].
References
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
Affeldt, R., Cohen, C., Rouhling, D.: Formalization techniques for asymptotic reasoning in classical analysis. J. Formaliz. Reason. 11, 43–76 (2018)
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_8
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
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)
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_11
Boldo, S., Lelay, C., Melquiond, G.: Coquelicot: a user-friendly library of real analysis for Coq. Math. Comput. Sci. 9(1), 41–62 (2015)
Bourbaki, N.: The architecture of mathematics. Am. Math. Mon. 57(4), 221–232 (1950), http://www.jstor.org/stable/2305937
Bourbaki, N.: Théorie des ensembles. Éléments de mathématique. Springer (2006). Original Edition published by Hermann, Paris (1970)
de Bruijn, N.G.: Telescopic mappings in typed lambda calculus. Inf. Comput. 91(2), 189–204 (1991)
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)
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
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
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
Constable, R.L., et al.: Implementing Mathematics with the NuPRL Proof Development System. Prentice-Hall, Upper Saddle River (1986)
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_47
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_23
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
Harrison, J.: The HOL Light System REFERENCE (2017). https://www.cl.cam.ac.uk/~jrh13/hol-light/index.html
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_5
Microsoft Reasearch: L\(\exists \forall \)N THEOREM PROVER (2020). https://leanprover.github.io
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_26
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
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)
Sakaguchi, K.: Validating mathematical structures. In: Peltier, N., Sofronie-Stokkermans, V. (eds.) IJCAR 2020. LNAI, vol. 12167, pp. 138–157. Springer, Heidelberg (2020)
Selsam, D., Ullrich, S., de Moura, L.: Tabled typeclass resolution (2020). https://arxiv.org/abs/2001.04301
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_23
Spitters, B., van der Weegen, E.: Type classes for mathematics in type theory. Math. Struct. Comput. Sci. 21(4), 795–825 (2011)
The Agda Team: The Agda User Manual (2020). https://agda.readthedocs.io/en/v2.6.0.1. Version 2.6.0.1
The Coq Development Team: The Coq Proof Assistant Reference Manual. Inria (2019). https://coq.inria.fr. Version 8.10.2
The Mathematical Components Analysis Team: The Mathematical Components Analysis library (2017). https://github.com/math-comp/analysis
The Mathematical Components Team: The Mathematical Components library (2007). https://github.com/math-comp/math-comp
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)
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.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2020 Springer Nature Switzerland AG
About this paper
Cite this paper
Affeldt, R., Cohen, C., Kerjean, M., Mahboubi, A., Rouhling, D., Sakaguchi, K. (2020). Competing Inheritance Paths in Dependent Type Theory: A Case Study in Functional Analysis. In: Peltier, N., Sofronie-Stokkermans, V. (eds) Automated Reasoning. IJCAR 2020. Lecture Notes in Computer Science(), vol 12167. Springer, Cham. https://doi.org/10.1007/978-3-030-51054-1_1
Download citation
DOI: https://doi.org/10.1007/978-3-030-51054-1_1
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-51053-4
Online ISBN: 978-3-030-51054-1
eBook Packages: Computer ScienceComputer Science (R0)