Mathematical Components
Assia Mahboubi, Tassi, Enrico · Zenodo (CERN European Organization for Nuclear Research) · 2022
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 the one hand, newcomers, even the more mathematically 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.