Math Classes

Math classes is a library of abstract interfaces for mathematical structures, such as:

• Algebraic hierarchy (groups, rings, fields, …)
• Relations, orders, …
• Categories, functors, universal algebra, …
• Numbers: N, Z, Q, …
• Operations, (shift, power, abs, …)

It is heavily based on Coq’s new type classes in order to provide: structure inference, multiple inheritance/sharing, convenient algebraic manipulation (e.g. rewriting) and idiomatic use of notations.

Meta

• Author(s):
  • Eelis van der Weegen (initial)
  • Bas Spitters (initial)
  • Robbert Krebbers (initial)
• Coq-community maintainer(s):
  • Bas Spitters (@spitters)
  • Xia Li-yao (@Lysxia)
• License: MIT License
• Compatible Coq versions: Coq 8.18 or later (use releases for other Coq versions)
• Additional dependencies:
  • BigNums
• Coq namespace: MathClasses
• Related publication(s):
  • Type Classes for Mathematics in Type Theory doi:10.1017/S0960129511000119

Building and installation instructions

The easiest way to install the latest released version of Math Classes is via OPAM:

opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-math-classes

To instead build and install manually, do:

git clone https://github.com/coq-community/math-classes.git
cd math-classes
./configure.sh
make   # or make -j <number-of-cores-on-your-machine>
make install

Directory structure

categories/

Proofs that certain structures form categories.

functors/

interfaces/

Definitions of abstract interfaces/structures.

implementations/

Definitions of concrete data structures and algorithms, and proofs that they are instances of certain structures (i.e. implement certain interfaces).

misc/

Miscellaneous things.

orders/

Theory about orders on different structures.

quote/

Prototype implementation of type class based quoting. To be integrated.

theory/

Proofs of properties of structures.

varieties/

Proofs that certain structures are varieties, and translation to/from type classes dedicated to these structures (defined in interfaces/).

The reason we treat categories and varieties differently from other structures (like groups and rings) is that they are like meta-interfaces whose implementations are not concrete data structures and algorithms but are themselves abstract structures.

To be able to distinguish the various arrows, we recommend using a variable width font.