1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
|
------------------------
Introduction
------------------------
This document is the Reference Manual of the |Coq| proof assistant.
To start using Coq, it is advised to first read a tutorial.
Links to several tutorials can be found at
https://coq.inria.fr/documentation (see also
https://github.com/coq/coq/wiki#coq-tutorials).
The |Coq| system is designed to develop mathematical proofs, and
especially to write formal specifications, programs and to verify that
programs are correct with respect to their specification. It provides a
specification language named |Gallina|. Terms of |Gallina| can represent
programs as well as properties of these programs and proofs of these
properties. Using the so-called *Curry-Howard isomorphism*, programs,
properties and proofs are formalized in the same language called
*Calculus of Inductive Constructions*, that is a
:math:`\lambda`-calculus with a rich type system. All logical judgments
in |Coq| are typing judgments. The very heart of the |Coq| system is the
type-checking algorithm that checks the correctness of proofs, in other
words that checks that a program complies to its specification. |Coq| also
provides an interactive proof assistant to build proofs using specific
programs called *tactics*.
All services of the |Coq| proof assistant are accessible by interpretation
of a command language called *the vernacular*.
Coq has an interactive mode in which commands are interpreted as the
user types them in from the keyboard and a compiled mode where commands
are processed from a file.
- The interactive mode may be used as a debugging mode in which the
user can develop his theories and proofs step by step, backtracking
if needed and so on. The interactive mode is run with the `coqtop`
command from the operating system (which we shall assume to be some
variety of UNIX in the rest of this document).
- The compiled mode acts as a proof checker taking a file containing a
whole development in order to ensure its correctness. Moreover,
|Coq|’s compiler provides an output file containing a compact
representation of its input. The compiled mode is run with the `coqc`
command from the operating system.
These two modes are documented in Chapter :ref:`thecoqcommands`.
Other modes of interaction with |Coq| are possible: through an emacs shell
window, an emacs generic user-interface for proof assistant (Proof
General :cite:`ProofGeneral`) or through a customized
interface (PCoq :cite:`Pcoq`). These facilities are not
documented here. There is also a |Coq| Integrated Development Environment
described in :ref:`coqintegrateddevelopmentenvironment`.
How to read this book
=====================
This is a Reference Manual, not a User Manual, so it is not made for a
continuous reading. However, it has some structure that is explained
below.
- The first part describes the specification language, |Gallina|.
Chapters :ref:`gallinaspecificationlanguage` and :ref:`extensionsofgallina` describe the concrete
syntax as well as the meaning of programs, theorems and proofs in the
Calculus of Inductive Constructions. Chapter :ref:`thecoqlibrary` describes the
standard library of |Coq|. Chapter :ref:`calculusofinductiveconstructions` is a mathematical description
of the formalism. Chapter :ref:`themodulesystem` describes the module
system.
- The second part describes the proof engine. It is divided in five
chapters. Chapter :ref:`vernacularcommands` presents all commands (we
call them *vernacular commands*) that are not directly related to
interactive proving: requests to the environment, complete or partial
evaluation, loading and compiling files. How to start and stop
proofs, do multiple proofs in parallel is explained in
Chapter :ref:`proofhandling`. In Chapter :ref:`tactics`, all commands that
realize one or more steps of the proof are presented: we call them
*tactics*. The language to combine these tactics into complex proof
strategies is given in Chapter :ref:`ltac`. Examples of tactics
are described in Chapter :ref:`detailedexamplesoftactics`.
- The third part describes how to extend the syntax of |Coq|. It
corresponds to the Chapter :ref:`syntaxextensionsandinterpretationscopes`.
- In the fourth part more practical tools are documented. First in
Chapter :ref:`thecoqcommands`, the usage of `coqc` (batch mode) and
`coqtop` (interactive mode) with their options is described. Then,
in Chapter :ref:`utilities`, various utilities that come with the
|Coq| distribution are presented. Finally, Chapter :ref:`coqintegrateddevelopmentenvironment`
describes the |Coq| integrated development environment.
- The fifth part documents a number of advanced features, including coercions,
canonical structures, typeclasses, program extraction, and specialized
solvers and tactics. See the table of contents for a complete list.
At the end of the document, after the global index, the user can find
specific indexes for tactics, vernacular commands, and error messages.
List of additional documentation
================================
This manual does not contain all the documentation the user may need
about |Coq|. Various informations can be found in the following documents:
Tutorial
A companion volume to this reference manual, the |Coq| Tutorial, is
aimed at gently introducing new users to developing proofs in |Coq|
without assuming prior knowledge of type theory. In a second step,
the user can read also the tutorial on recursive types (document
`RecTutorial.ps`).
Installation
A text file `INSTALL` that comes with the sources explains how to
install |Coq|.
The |Coq| standard library
A commented version of sources of the |Coq| standard library
(including only the specifications, the proofs are removed) is given
in the additional document `Library.ps`.
|
