PREFACE

The Coq system is a computer tool for verifying theorem proofs. These theorems may concern usual mathematics, proof theory, or program verification. Our main objective is to give a practical understanding of the Coq system and its underlying theory, the Calculus of Inductive Constructions. For this reason, our book contains many examples, all of which can be replayed by the reader on a computer. For pedagogical reasons, some examples also exhibit erroneous or clumsy uses and guidelines to avoid problems. We have often tried to decompose the dialogues so that the user can reproduce them, either with pen and paper or directly with the Coq system. Sometimes, we have also included synthetic expressions that may look impressive at first sight, but these terms have also been obtained with the help of the Coq proof assistant. The reader should decompose these expressions in practical experiments, modify them, understand their structure, and get a practical feeling for them. Our book has an associated site,1 where the reader can download and replay all the examples of proofs and—in cases of emergency—the solutions of the 200 exercises of the book. Our book and our site both use Coq V8 ,2 released in the beginning of 2004. The confidence the user can have in theorems proved with the Coq system relies on the properties of the Calculus of Inductive Constructions, a formalism that combines several of the recent advances in logic from the point of view of λ-calculus and typing. The main properties of this calculus are presented herein, since we believe that some knowledge of both theory and practice is the best way to use Coq ’s full expressive power. The Coq language is extremely powerful and expressive, both for reasoning and for programming. There are several levels of competence, from the ability to construct simple terms and perform simple proofs to building whole theories and studying complex algorithms. We annotate chapters and sections with