###
About

Mathematical Components is the name of a library of formalized mathematics for
the Coq system. It covers a variety of topics, from the theory of basic data
structures (e.g., numbers, lists, finite sets) to 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.

The reason of existence of this book is to break down the barriers to entry.
While there are several books around covering the usage of the Coq system and
the theory it is based on, the Mathematical Components library is built in an
unconventional way. As a consequence this book provides a 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 classes of public. On one hand newcomers, even the more
mathematical inclined ones, find a soft introduction to the programming
language of Coq, *Gallina*, and the *Ssreflect* proof language.
On the other hand accustomed Coq users find a substantial account of the
formalization style that made the Mathematical Components library possible.

###
Getting the book

The book in PDF format.
(last update Thu Feb 2 09:51:23 CET 2017)

The book printed on demand (TBD)

Coq snippets that can be played in the browser thanks
to jscoq:

ch0,
ch1,
ch2,
ch3,
ch4,
ch6,
ch7.

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?
Subscribe to the ssreflect mailing list
and let us know what you are using our libraries for, ask questions, etc.
You can also browse the archives of the list.

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