Use and Abuse of Instance Parameters in the Lean Mathematical Library

Anne Baanen

doi:10.4230/LIPIcs.ITP.2022.4

Use and Abuse of Instance Parameters in the Lean Mathematical Library

Anne Baanen^*

^*Corresponding author for this work

Research output: Chapter in Book / Report / Conference proceeding › Conference contribution › Academic › peer-review

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 current Lean 3 version of mathlib, focussing on complications arising at scale and how the mathlib community deals with them.

Original language	English
Title of host publication	13th International Conference on Interactive Theorem Proving (ITP 2022)
Editors	June Andronick, Leonardo de Moura
Publisher	Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
Pages	1-20
Number of pages	20
ISBN (Electronic)	9783959772525
DOIs	https://doi.org/10.4230/LIPIcs.ITP.2022.4
Publication status	Published - 2022
Event	13th International Conference on Interactive Theorem Proving, ITP 2022 - Haifa, Israel Duration: 7 Aug 2022 → 10 Aug 2022

Publication series

Name	Leibniz International Proceedings in Informatics, LIPIcs
Volume	237
ISSN (Print)	1868-8969

Conference

Conference	13th International Conference on Interactive Theorem Proving, ITP 2022
Country/Territory	Israel
City	Haifa
Period	7/08/22 → 10/08/22

Bibliographical note

Funding Information:
Funding NWO Vidi grant No. 016.Vidi.189.037, Lean Forward.

Publisher Copyright:
© Anne Baanen.

Keywords

algebraic hierarchy
dependent type theory
formalization of mathematics
Lean prover
typeclasses

Access to Document

10.4230/LIPIcs.ITP.2022.4

Persistent URL (handle)

Persistent link

Cite this

Baanen, A. (2022). Use and Abuse of Instance Parameters in the Lean Mathematical Library. In J. Andronick, & L. de Moura (Eds.), 13th International Conference on Interactive Theorem Proving (ITP 2022) (pp. 1-20). (Leibniz International Proceedings in Informatics, LIPIcs; Vol. 237). Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing. https://doi.org/10.4230/LIPIcs.ITP.2022.4

@inproceedings{49a4603ebd964a27b40841031b9a65ee,

title = "Use and Abuse of Instance Parameters in the Lean Mathematical Library",

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 current Lean 3 version of mathlib, focussing on complications arising at scale and how the mathlib community deals with them. ",

keywords = "algebraic hierarchy, dependent type theory, formalization of mathematics, Lean prover, typeclasses",

author = "Anne Baanen",

note = "Funding Information: Funding NWO Vidi grant No. 016.Vidi.189.037, Lean Forward. Publisher Copyright: {\textcopyright} Anne Baanen.; 13th International Conference on Interactive Theorem Proving, ITP 2022 ; Conference date: 07-08-2022 Through 10-08-2022",

year = "2022",

doi = "10.4230/LIPIcs.ITP.2022.4",

language = "English",

series = "Leibniz International Proceedings in Informatics, LIPIcs",

publisher = "Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing",

pages = "1--20",

editor = "June Andronick and {de Moura}, Leonardo",

booktitle = "13th International Conference on Interactive Theorem Proving (ITP 2022)",

}

Baanen, A 2022, Use and Abuse of Instance Parameters in the Lean Mathematical Library. in J Andronick & L de Moura (eds), 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics, LIPIcs, vol. 237, Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, pp. 1-20, 13th International Conference on Interactive Theorem Proving, ITP 2022, Haifa, Israel, 7/08/22. https://doi.org/10.4230/LIPIcs.ITP.2022.4

Use and Abuse of Instance Parameters in the Lean Mathematical Library. / Baanen, Anne.
13th International Conference on Interactive Theorem Proving (ITP 2022). ed. / June Andronick; Leonardo de Moura. Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 2022. p. 1-20 (Leibniz International Proceedings in Informatics, LIPIcs; Vol. 237).

Research output: Chapter in Book / Report / Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Use and Abuse of Instance Parameters in the Lean Mathematical Library

AU - Baanen, Anne

N1 - Funding Information: Funding NWO Vidi grant No. 016.Vidi.189.037, Lean Forward. Publisher Copyright: © Anne Baanen.

PY - 2022

Y1 - 2022

N2 - 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 current Lean 3 version of mathlib, focussing on complications arising at scale and how the mathlib community deals with them.

AB - 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 current Lean 3 version of mathlib, focussing on complications arising at scale and how the mathlib community deals with them.

KW - algebraic hierarchy

KW - dependent type theory

KW - formalization of mathematics

KW - Lean prover

KW - typeclasses

UR - http://www.scopus.com/inward/record.url?scp=85136285588&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85136285588&partnerID=8YFLogxK

U2 - 10.4230/LIPIcs.ITP.2022.4

DO - 10.4230/LIPIcs.ITP.2022.4

M3 - Conference contribution

AN - SCOPUS:85136285588

T3 - Leibniz International Proceedings in Informatics, LIPIcs

SP - 1

EP - 20

BT - 13th International Conference on Interactive Theorem Proving (ITP 2022)

A2 - Andronick, June

A2 - de Moura, Leonardo

PB - Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing

T2 - 13th International Conference on Interactive Theorem Proving, ITP 2022

Y2 - 7 August 2022 through 10 August 2022

ER -

Baanen A. Use and Abuse of Instance Parameters in the Lean Mathematical Library. In Andronick J, de Moura L, editors, 13th International Conference on Interactive Theorem Proving (ITP 2022). Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing. 2022. p. 1-20. (Leibniz International Proceedings in Informatics, LIPIcs). Epub 2022 Aug 3. doi: 10.4230/LIPIcs.ITP.2022.4

Use and Abuse of Instance Parameters in the Lean Mathematical Library

Abstract

Publication series

Conference

Bibliographical note

Keywords

Access to Document

Persistent URL (handle)

Other files and links

Fingerprint

Cite this