-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 +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.
-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 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 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. +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.
-The book in PDF format. -(last update Sat Aug 11 18:12:20 CEST 2018) +Download the book in PDF format. +Cite it.
--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 @@ -88,10 +91,8 @@
-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. +Interested? Chat with us on +Zulip.