Type Classes For Mathematics in Coq

By Eelis van der Weegen and Bas Spitters.

Introduction

We have been working on a new set of foundational interfaces for formalized constructive mathematics in Coq, heavily based on Coq's new type classes, used in a systematic way in order to achieve:

• elegant and mathematically sound abstract interfaces for algebraic and numeric structures up to and including rationals (with practical use of universal algebra and category theory);
• a very flexible purely predicate-based representation of algebraic structures that makes sharing, multiple inheritance, and derived inheriance, all trivial;
• clean expression terms that neither refer to proofs nor require deeply nested record projections;
• fluent rewriting;
• easy and flexible replacement and specialization of data representations and operations with more efficient versions;
• ordinary mathematical notation and overloaded names not reliant on Coq's notation scopes.

MSCS paper

We have submitted a paper (PDF) presenting our development for the MSCS Special Issue on Advances and Perspectives in the Mechanization of Mathematics.

ITP "Rough Diamond"

We have submitted a "rough diamond" extended abstract (PDF) presenting our development for ITP-10.

Coq sources

The development can be browsed and downloaded at the GitHub repository at

(Click the "Download Source" button for a tarball containing all the source code.)

Alternatively, you can browse the coqdoc-generated documentation.