math-classes

by coq-community

coq-community /math-classes

A library of abstract interfaces for mathematical structures in Coq [[email protected]]

133 Stars 37 Forks Last release: 28 days ago (8.12.0) MIT License 668 Commits 6 Releases

Available items

No Items, yet!

The developer of this repository has not created any items for sale yet. Need a bug fixed? Help with integration? A different license? Create a request here:

Math Classes

Travis Contributing Code of Conduct Zulip DOI

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

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 
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.

We use cookies. If you continue to browse the site, you agree to the use of cookies. For more information on our use of cookies please see our Privacy Policy.