Coq'Art Examples and Exercises

Coq'Art is the familiar name for the first book on the Coq proof assistant and its underlying theory the Calculus of Inductive Constructions, written by Yves Bertot and Pierre Castéran. See Springer's book website. 
Interactive Theorem Proving and Program Development
Coq'Art: The Calculus of Inductive Constructions
Series: Texts in Theoretical Computer Science. An EATCS Series
Bertot, Yves, and Castéran, Pierre
2004, XXV, 469 p., Hardcover 
ISBN: 3-540-20854-2
DOI: 10.1007/978-3-662-07964-5
The examples and exercises on this site are copyright Yves Bertot and Pierre Castéran, unless explicitely mentioned. The tutorial on type classes and user-defined relations was written by Pierre Castéran and Matthieu Sozeau. The tutorial on [co-]inductive type was written by Eduardo Giménez and Pierre Castéran. All material is available under the open-source MIT license.

Drawing "Oiseau de feu" by courtesy of Michel Mendès France

Contents

16 directories, each one associated with a chapter of the book

Each directory contains a list of exercises, and an adaptation to recent versions of Coq of the scripts presented in the corresponding chapter of the book. Each index file contains also corrections of the errors that were kindly signalled to us by the readers.
  1. A Brief Presentation of Coq
  2. Gallina: Coq as a Programming Language
  3. Propositions and Proofs
  4. Dependent Product
  5. Everyday logic
  6. Inductive Data Structures
  7. Tactics and automation
  8. Inductive Predicates
  9. Functions and their specification
  10. Extraction and imperative programming
  11. A Case Study: binary search trees
  12. The Module System
  13. Infinite Objects and Proofs
  14. Foundations of Inductive Types
  15. General Recursion
  16. Proof by reflection

Additional material

Errata

Some typos were found after the printing of the book. They are reported chapter by chapter, after the sources and exercises. Many thanks to Stefan Karrmann for all the remarks he sent to us.

Comments are welcome

Comments, alternative solutions, and suggestions to improve this site are welcome as issues and pull requests on GitHub. Thank you in advance!