About

Mathematical Components is the name of a library of formalized mathematics for the Coq proof assistants. It covers a variety of topics, from the theory of basic data structures (e.g., numbers, lists, finite sets) to more advanced results in various flavors of algebra. This library constitutes the infrastructure for the machine checked proofs of the Four Color Theorem and of the Odd Order Theorem.

This book aims at providing an introducing to the design patterns used throughout this library, so as to ease its use for other projects. While there are several books around covering the usage of the Coq system and the theory it is based on, the Mathematical Components library uses a few design patterns that differ from the methodology propose in other sources. As a consequence, this book provides a slightly non-standard presentation of Coq, putting upfront the formalization choices and the proof style that are the pillars of the library.

This books targets two natures of audience. On one hand newcomers, in particular beginners with background in mathematics rather than computer science, should find a soft introduction to the programming language of Coq, Gallina, and to the Ssreflect proof language. On the other hand, accustomed Coq users will find a substantial account of the formalization style that made the Mathematical Components library possible.

Getting the book

Download the book in PDF format. To cite the book look at the bottom right corner on Zenodo.

Play Coq snippets in the browser: Ch0, Ch1, Ch2, Ch3, Ch4, Ch5, Ch6, Ch7_1, Ch7_2, Ch7_3, Ch7_4, Ch7_5, Ch8.
The corresponding .v files are available on github in the coq folder.

Feedback on the book is very welcome. Issues can be reported on the github page of the book.

Getting the library

Web site of the Mathematical Components library

Join the community of users

Interested? Chat with us on Zulip.

Authors and Contributors

The current version of the book "Mathematical Components" was written by Assia Mahboubi and Enrico Tassi with contributions by Yves Bertot and Georges Gonthier.

The Coq painting(s) are by Hanna.

Financial support was provided by the Inria -- Microsoft Research Joint Centre.