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
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
|
%BEGIN LATEX
\setheaders{Introduction}
%END LATEX
\chapter*{Introduction}
This document is the Reference Manual of version \coqversion{} of the \Coq\
proof assistant. A companion volume, the \Coq\ Tutorial, is provided
for the beginners. It is advised to read the Tutorial first.
A book~\cite{CoqArt} on practical uses of the \Coq{} system was published in 2004 and is a good support for both the beginner and
the advanced user.
%The system \Coq\ is designed to develop mathematical proofs. It can be
%used by mathematicians to develop mathematical theories and by
%computer scientists to write formal specifications,
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 \textit{Curry-Howard
isomorphism}, programs, properties and proofs are formalized in the
same language called \textit{Calculus of Inductive Constructions},
that is a $\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 \textit{tactics}.
All services of the \Coq\ proof assistant are accessible by
interpretation of a command language called \textit{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.
\begin{itemize}
\item 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 {\tt coqtop} command from the operating system (which we shall
assume to be some variety of UNIX in the rest of this document).
\item 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 {\tt coqc} command from the operating system.
\end{itemize}
These two modes are documented in Chapter~\ref{Addoc-coqc}.
Other modes of interaction with \Coq{} are possible: through an emacs
shell window, an emacs generic user-interface for proof assistant
(ProofGeneral~\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
Chapter~\ref{Addoc-coqide}.
\section*{How to read this book}
This is a Reference Manual, not a User Manual, then it is not made for a
continuous reading. However, it has some structure that is explained
below.
\begin{itemize}
\item The first part describes the specification language,
Gallina. Chapters~\ref{Gallina} and~\ref{Gallina-extension}
describe the concrete syntax as well as the meaning of programs,
theorems and proofs in the Calculus of Inductive
Constructions. Chapter~\ref{Theories} describes the standard library
of \Coq. Chapter~\ref{Cic} is a mathematical description of the
formalism. Chapter~\ref{chapter:Modules} describes the module system.
\item The second part describes the proof engine. It is divided in
five chapters. Chapter~\ref{Vernacular-commands} presents all
commands (we call them \emph{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{Proof-handling}. In
Chapter~\ref{Tactics}, all commands that realize one or more steps
of the proof are presented: we call them \emph{tactics}. The
language to combine these tactics into complex proof strategies is
given in Chapter~\ref{TacticLanguage}. Examples of tactics are
described in Chapter~\ref{Tactics-examples}.
%\item The third part describes how to extend the system in two ways:
% adding parsing and pretty-printing rules
% (Chapter~\ref{Addoc-syntax}) and writing new tactics
% (Chapter~\ref{TacticLanguage}).
\item The third part describes how to extend the syntax of \Coq. It
corresponds to the Chapter~\ref{Addoc-syntax}.
\item In the fourth part more practical tools are documented. First in
Chapter~\ref{Addoc-coqc}, the usage of \texttt{coqc} (batch mode)
and \texttt{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{Addoc-coqide} describes the \Coq{} integrated
development environment.
\end{itemize}
At the end of the document, after the global index, the user can find
specific indexes for tactics, vernacular commands, and error
messages.
\section*{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:
\begin{description}
\item[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 {\tt
RecTutorial.ps}).
\item[Addendum] The fifth part (the Addendum) of the Reference Manual
is distributed as a separate document. It contains more
detailed documentation and examples about some specific aspects of the
system that may interest only certain users. It shares the indexes,
the page numbers and
the bibliography with the Reference Manual. If you see in one of the
indexes a page number that is outside the Reference Manual, it refers
to the Addendum.
\item[Installation] A text file INSTALL that comes with the sources
explains how to install \Coq{}.
\item[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 {\tt Library.ps}.
\end{description}
% $Id: RefMan-int.tex 11307 2008-08-06 08:38:57Z jnarboux $
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "Reference-Manual"
%%% End:
|
