Mathematical Components
Assia Mahboubi, Tassi, Enrico
Abstract
Mathematical Components is the name of a library of formalized mathematics for the Coq<br> system. It covers a variety of topics, from the theory of basic data structures (e.g., numbers,<br> lists, finite sets) to advanced results in various flavors of algebra. This library constitutes<br> the infrastructure for the machine-checked proofs of the Four Color Theorem and<br> of the Odd Order Theorem.<br> The reason of existence of this book is to break down the barriers to entry. While there<br> are several books around covering the usage of the Coq system<br> and the theory it is based on, the Mathematical Components library<br> is built in an unconventional way. As a consequence, this book provides a non-standard<br> presentation of Coq, putting upfront the formalization choices and the proof style that<br> are the pillars of the library.<br> This books targets two classes of public. On the one hand, newcomers, even the more<br> mathematically inclined ones, find a soft introduction to the programming language of<br> Coq, Gallina, and the SSReflect proof language. On the other hand accustomed Coq<br> users find a substantial account of the formalization style that made the Mathematical<br> Components library possible.