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: ℕ, ℤ, ℚ, …
- 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.
Here is a SVG diagram showing all files and their dependencies with links to the coqdoc dependencies.
Here are two diagrams showing the main components of the algebraic hierarchy and the various orders in math classes.
Math classes is used in C-CoRN to implement high performance exact real number arithmetic.