Use and Abuse of Instance Parameters in the Lean Mathematical Library: Use and Abuse of Instance Parameters...
Author: 
Anne BaanenAuthors Info & Claims
Abstract
The Lean mathematical library Mathlib features extensive use of the typeclass pattern for organising mathematical structures, based on Lean’s mechanism of instance parameters. Related mechanisms for typeclasses are available in other provers including Agda, Coq and Isabelle with varying degrees of adoption. This paper analyses representative examples of design patterns involving instance parameters in the finalized Lean 3 version of Mathlib, focussing on complications arising at scale and how the Mathlib community deals with them.
References
[1]
Affeldt R, Cohen C, Kerjean M, Mahboubi A, Rouhling D, and Sakaguchi K Peltier N and Sofronie-Stokkermans V Competing inheritance paths in dependent type theory: a case study in functional analysis IJCAR 2020 2020 Berlin Springer 3-20 12167
[2]
Allamigeon, X., Canu, Q., Cohen, C., Sakaguchi, K., Strub, P.-Y.: Design patterns of hierarchies for order structures. ITP 2023, Version 1 (February 2023) (Submitted) (2023). https://hal.inria.fr/hal-04008820
[3]
Asperti A, Ricciotti W, Sacerdoti Coen C, and Tassi E Berghofer S, Nipkow T, Urban C, and Wenzel M Hints in unification TPHOLs 2009 2009 Berlin Springer 84-98 5674
[4]
Baanen, T.: Use and abuse of instance parameters in the Lean mathematical library. In: Andronick, J., Moura, L. (eds.) ITP 2022. LIPIcs, vol. 237, pp. 4–1420. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, Dagstuhl (2022).
[5]
Ballarin C Locales: A module system for mathematical theories J. Autom. Reason. 2014 52 2 123-153
[6]
Ballarin C Exploring the structure of an algebra text with locales J. Autom. Reason. 2020 64 6 1093-1121
[7]
Brady EC Idris, a general-purpose dependently typed programming language: design and implementation J. Funct. Program. 2013 23 5 552-593
[8]
Buzzard, K., Commelin, J., Massot, P.: Formalising perfectoid spaces. In: CPP ’20. Certified programs and proofs, pp. 299–312. ACM, New York (2020).
[9]
Cohen C, Sakaguchi K, and Tassi E Ariola ZM Hierarchy builder: algebraic hierarchies made easy in Coq with ELPI (system description) FSCD 2020 2020 Dagstuhl Schloss Dagstuhl-Leibniz-Zentrum für Informatik 34-13421 167
[10]
Commelin J and Lewis RY Hrițcu C and Popescu A Formalizing the ring of Witt vectors CPP ’21. Certified Programs and Proofs 2021 New York ACM 264-277
[11]
Devriese D and Piessens F On the bright side of type classes: instance arguments in Agda SIGPLAN Not. 2011 46 9 143-155
[12]
Doorn F, Ebner G, and Lewis RY Benzmüller C and Miller BR Maintaining a library of formal mathematics CICM 2020 2020 Berlin Springer 251-267 12236
[13]
Garillot F, Gonthier G, Mahboubi A, and Rideau L Berghofer S, Nipkow T, Urban C, and Wenzel M Packaging mathematical structures TPHOLs 2009 2009 Berlin Springer 327-342 5674
[14]
Gonthier G and Tassi E Beringer L and Felty A A language of patterns for subterm selection ITP 2012 2012 Berlin Springer 361-376
[15]
Gonthier G, Ziliani B, Nanevski A, and Dreyer D How to make ad hoc proof automation less ad hoc J. Funct. Program. 2013 23 4 357-401
[16]
Grabowski A, Kornilowicz A, and Schwarzweller C Ganzha M, Maciaszek LA, and Paprzycki M On algebraic hierarchies in mathematical repository of Mizar FedCSIS 2016. Annals of Computer Science and Information Systems 2016 New York IEEE 363-371 8
[17]
Hölzl J, Immler F, and Huffman B Blazy S, Paulin-Mohring C, and Pichardie D Type classes and filters for mathematical analysis in Isabelle/HOL ITP 2013 2013 Berlin Springer 279-294 7998
[18]
Jones MP Smolka G Type classes with functional dependencies Programming Languages and Systems 2000 Berlin Springer 230-244
[19]
Jung, R.: Exponential blowup when using unbundled typeclasses to model algebraic hierarchies (2019). https://www.ralfj.de/blog/2019/05/15/typeclasses-exponential-blowup.html. Accessed 1 Feb 2022
[20]
Kammüller F, Wenzel M, and Paulson LC Bertot Y, Dowek G, Hirschowitz A, Paulin-Mohring C, and Théry L Locales—a sectioning concept for Isabelle TPHOLs’99 1999 Berlin Springer 149-166 1690
[21]
Mahboubi A and Tassi E The Mathematical Components Libraries 2017 Genève Zenodo
[22]
Moura, L., Avigad, J., Kong, S., Roux, C.: Elaboration in dependent type theory. CoRR abs/1505.04324 (2015) arxiv:1505.04324
[23]
Moura L, Kong S, Avigad J, Doorn F, and Raumer J Felty AP and Middeldorp A The Lean theorem prover (system description) Automated Deduction—CADE-25 2015 Berlin Springer 378-388 9195
[24]
Moura L and Ullrich S Platzer A and Sutcliffe G The Lean 4 theorem prover and programming language Automated Deduction—CADE-28 2021 Berlin Springer 625-635 12699
[25]
Oliveira BCS, Moors A, and Odersky M Type classes as objects and implicits SIGPLAN Not. 2010 45 10 341-360
[26]
Ramakrishnan, I.V., Sekar, R., Voronkov, A.: Term indexing. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, pp. 1853–1964. Elsevier and MIT Press, Amsterdam and Cambridge (2001).
[27]
Saïbi, A.: Typing algorithm in type theory with inheritance. In: Principles of Programming Languages—POPL ’97, pp. 292–301. ACM, New York (1997).
[28]
Sakaguchi, K.: Reflexive tactics for algebra, revisited. In: Andronick, J., Moura, L. (eds.) ITP 2022. LIPIcs, vol. 237, pp. 29–12922. Schloss Dagstuhl–Leibniz-Zentrum für Informatik, Dagstuhl (2022).
[29]
Sakaguchi K Peltier N and Sofronie-Stokkermans V Validating mathematical structures IJCAR 2020 2020 Berlin Springer 138-157 12167
[30]
Selsam, D., Ullrich, S., Moura, L.: Tabled typeclass resolution. CoRR (2020). arxiv:2001.04301
[31]
Sozeau M and Oury N Mohamed OA, Muñoz CA, and Tahar S First-class type classes TPHOLs 2008 2008 Berlin Springer 278-293 5170
[32]
Spitters B and Weegen E Kaufmann M and Paulson LC Developing the algebraic hierarchy with type classes in Coq ITP 2010 2010 Berlin Springer 490-493 6172
[33]
The mathlib Community: The Lean mathematical library. In: Blanchette, J., Hrițcu, C. (eds.) CPP 2020. Certified Programs and Proofs, pp. 367–381. ACM, New York City, USA (2020).
[34]
The Rust team: The Rust Reference 1.57.0 (2021). https://doc.rust-lang.org/1.57.0/reference/index.html. Accessed 22 Dec 2021
[35]
Wadler, P., Blott, S.: How to make ad-hoc polymorphism less ad hoc. In: Principles of Programming Languages. POPL ’89, pp. 60–76. ACM, New York (1989).
[36]
Wenzel M Gunter EL and Felty AP Type classes and overloading in higher-order logic TPHOLs’97 1997 Berlin Springer 307-322 1275
[37]
Wieser E Dubois C and Kerber M Multiple-inheritance hazards in dependently-typed algebraic hierarchies CICM 2023 2023 Berlin Springer 222-236 14101
[38]
Wieser, E.: Scalar actions in Lean’s mathlib. CoRR (2021). arxiv:2108.10700
Index Terms
- Use and Abuse of Instance Parameters in the Lean Mathematical Library: Use and Abuse of Instance Parameters...
Index terms have been assigned to the content through auto-classification.
Recommendations
Competing Inheritance Paths in Dependent Type Theory: A Case Study in Functional Analysis
Automated ReasoningAbstractThis 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 ...
LF in LF: mechanizing the metatheories of LF in twelf
LFMTP '12: Proceedings of the seventh international workshop on Logical frameworks and meta-languages, theory and practiceWe present a mechanized metatheoretic development of two presentations of LF: the Canonical presentation (in which only beta-short, eta-long terms are well-formed) and the original version based on definitional equivalence. We prove the standard ...
Practical Proof Search for Coq by Type Inhabitation
Automated ReasoningAbstractWe present a practical proof search procedure for Coq based on a direct search for type inhabitants in an appropriate normal form. The procedure is more general than any of the automation tactics natively available in Coq. It aims to handle as ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
© The Author(s) 2024.
Publisher
Springer-Verlag
Berlin, Heidelberg
Publication History
Published: 12 December 2024
Accepted: 26 August 2024
Received: 31 March 2023
Author Tags
Qualifiers
- Research-article
Funding Sources
- Nederlandse Organisatie voor Wetenschappelijk Onderzoek
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 0Total Downloads
- Downloads (Last 12 months)0
- Downloads (Last 6 weeks)0
Reflects downloads up to 05 Mar 2025