This repository contains interactive full versions of the source code showcased in the paper "Use and abuse of instance parameters in the Lean mathematical library", submitted to the Journal of Automated Reasoning.
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.
The code showcased in the paper is based on mathlib commit 3e068ece210, which requires the community fork of Lean 3. To install a full Lean development environment, please follow the "Regular install" instructions at https://leanprover-community.github.io/get_started.html. After installation, you can run the command leanproject get lean-forward/mathlib-classes to obtain copies of the source code and precompiled binaries.
When opening a Lean project in VS Code, you must use the "Open Folder" menu option to open the project's root directory. On the command line, you can run code path/to/mathlib-classes.
Each section of the paper has a corresponding source code file:
- Section 2: Basic instance parameters in Lean 3
- Section 3:
has_mul: notation typeclass - Section 4:
comm_monoid: algebraic hierarchy class - Section 5:
multiplicative: multiple instances on a single type - Section 6:
module: multi-parameter classes - Section 7:
monoid_hom_class: generic bundled morphisms - Section 8:
nsmul: ensuring equality of instances - Section 9: Instance parameters depending on out parameters
- Section 10:
unique: proof-carrying mixin - Section 11:
fact: interfacing between instances and non-instances - Section 12: Performance and bundling
- Section 13: Instances and tactics