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