1
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.0 Transitional//EN"
2
"http://www.w3.org/TR/REC-html40/loose.dtd">
6
<META http-equiv="Content-Type" content="text/html; charset=ISO-8859-1">
7
<META name="GENERATOR" content="hevea 1.07">
13
<A HREF="toc.html"><IMG SRC ="contents_motif.gif" ALT="Up"></A>
14
<A HREF="Reference-Manual002.html"><IMG SRC ="next_motif.gif" ALT="Next"></A>
18
This document is the Reference Manual of version 8.0 of the <FONT COLOR=navy>Coq</FONT>
19
proof assistant. A companion volume, the <FONT COLOR=navy>Coq</FONT> Tutorial, is provided
20
for the beginners. It is advised to read the Tutorial first.
21
A new book [<A HREF="biblio.html#CoqArt"><CITE>13</CITE></A>] on practical uses of the <FONT COLOR=navy>Coq</FONT> system will
22
be published in 2004 and is a good support for both the beginner and
23
the advanced user.<BR>
25
The <FONT COLOR=navy>Coq</FONT> system is designed to develop mathematical proofs, and
26
especially to write formal specifications, programs and to verify that
27
programs are correct with respect to their specification. It provides
28
a specification language named <FONT COLOR=navy>Gallina</FONT>. Terms of <FONT COLOR=navy>Gallina</FONT> can
29
represent programs as well as properties of these programs and proofs
30
of these properties. Using the so-called <I>Curry-Howard
31
isomorphism</I>, programs, properties and proofs are formalized in the
32
same language called <I>Calculus of Inductive Constructions</I>,
33
that is a lambda-calculus with a rich type system. All logical
34
judgments in <FONT COLOR=navy>Coq</FONT> are typing judgments. The very heart of the Coq
35
system is the type-checking algorithm that checks the correctness of
36
proofs, in other words that checks that a program complies to its
37
specification. <FONT COLOR=navy>Coq</FONT> also provides an interactive proof assistant to
38
build proofs using specific programs called <I>tactics</I>.<BR>
40
All services of the <FONT COLOR=navy>Coq</FONT> proof assistant are accessible by
41
interpretation of a command language called <I>the vernacular</I>.<BR>
43
<FONT COLOR=navy>Coq</FONT> has an interactive mode in which commands are interpreted as the
44
user types them in from the keyboard and a compiled mode where
45
commands are processed from a file.
47
The interactive mode may be used as a debugging mode in which
48
the user can develop his theories and proofs step by step,
49
backtracking if needed and so on. The interactive mode is run with
50
the <TT>coqtop</TT> command from the operating system (which we shall
51
assume to be some variety of UNIX in the rest of this document).
52
<LI>The compiled mode acts as a proof checker taking a file
53
containing a whole development in order to ensure its correctness.
54
Moreover, <FONT COLOR=navy>Coq</FONT>'s compiler provides an output file containing a
55
compact representation of its input. The compiled mode is run with
56
the <TT>coqc</TT> command from the operating system. </UL>
58
These two modes are documented in chapter <A HREF="Reference-Manual014.html#Addoc-coqc">12</A>.<BR>
60
Other modes of interaction with <FONT COLOR=navy>Coq</FONT> are possible: through an emacs
61
shell window, an emacs generic user-interface for proof assistant
62
(ProofGeneral [<A HREF="biblio.html#ProofGeneral"><CITE>1</CITE></A>]) or through a customized interface
63
(PCoq [<A HREF="biblio.html#Pcoq"><CITE>111</CITE></A>]). These facilities are not documented here. There
64
is also a <FONT COLOR=navy>Coq</FONT> Integrated Development Environment described in
65
Chapter <A HREF="Reference-Manual016.html#Addoc-coqide">14</A>.<BR>
68
<H2>How to read this book</H2>
69
This is a Reference Manual, not a User Manual, then it is not made for a
70
continuous reading. However, it has some structure that is explained
73
The first part describes the specification language,
74
Gallina. Chapters <A HREF="Reference-Manual003.html#Gallina">1</A> and <A HREF="Reference-Manual004.html#Gallina-extension">2</A>
75
describe the concrete syntax as well as the meaning of programs,
76
theorems and proofs in the Calculus of Inductive
77
Constructions. Chapter <A HREF="Reference-Manual005.html#Theories">3</A> describes the standard library
78
of <FONT COLOR=navy>Coq</FONT>. Chapter <A HREF="Reference-Manual006.html#Cic">4</A> is a mathematical description of the
79
formalism. Chapter <A HREF="Reference-Manual007.html#chapter:Modules">5</A> describes the module system.<BR>
81
<LI>The second part describes the proof engine. It is divided in
82
five chapters. Chapter <A HREF="Reference-Manual008.html#Vernacular-commands">6</A> presents all
83
commands (we call them <EM>vernacular commands</EM>) that are not
84
directly related to interactive proving: requests to the
85
environment, complete or partial evaluation, loading and compiling
86
files. How to start and stop proofs, do multiple proofs in parallel
87
is explained in Chapter <A HREF="Reference-Manual009.html#Proof-handling">7</A>. In
88
Chapter <A HREF="Reference-Manual010.html#Tactics">8</A>, all commands that realize one or more steps
89
of the proof are presented: we call them <EM>tactics</EM>. The
90
language to combine these tactics into complex proof strategies is
91
given in Chapter <A HREF="Reference-Manual011.html#TacticLanguage">9</A>. Examples of tactics are
92
described in Chapter <A HREF="Reference-Manual012.html#Tactics-examples">10</A>.<BR>
94
<LI>The third part describes how to extend the syntax of <FONT COLOR=navy>Coq</FONT>. It
95
corresponds to the Chapter <A HREF="Reference-Manual013.html#Addoc-syntax">11</A>.<BR>
97
<LI>In the fourth part more practical tools are documented. First in
98
Chapter <A HREF="Reference-Manual014.html#Addoc-coqc">12</A>, the usage of <TT>coqc</TT> (batch mode)
99
and <TT>coqtop</TT> (interactive mode) with their options is
100
described. Then, in Chapter <A HREF="Reference-Manual015.html#Utilities">13</A>,
101
various utilities that come with the <FONT COLOR=navy>Coq</FONT> distribution are
103
Finally, Chapter <A HREF="Reference-Manual016.html#Addoc-coqide">14</A> describes the <FONT COLOR=navy>Coq</FONT> integrated
104
development environment.
106
At the end of the document, after the global index, the user can find
107
specific indexes for tactics, vernacular commands, and error
111
<H2>List of additional documentation</H2>
112
This manual does not contain all the documentation the user may need
113
about <FONT COLOR=navy>Coq</FONT>. Various informations can be found in the following
115
<DL COMPACT=compact><DT><B>Tutorial</B><DD>
116
A companion volume to this reference manual, the <FONT COLOR=navy>Coq</FONT> Tutorial, is
117
aimed at gently introducing new users to developing proofs in <FONT COLOR=navy>Coq</FONT>
118
without assuming prior knowledge of type theory. In a second step, the
119
user can read also the tutorial on recursive types (document <TT>RecTutorial.ps</TT>).<BR>
121
<DT><B>Addendum</B><DD> The fifth part (the Addendum) of the Reference Manual
122
is distributed as a separate document. It contains more
123
detailed documentation and examples about some specific aspects of the
124
system that may interest only certain users. It shares the indexes,
126
the bibliography with the Reference Manual. If you see in one of the
127
indexes a page number that is outside the Reference Manual, it refers
128
to the Addendum. <BR>
130
<DT><B>Installation</B><DD> A text file INSTALL that comes with the sources
131
explains how to install <FONT COLOR=navy>Coq</FONT>.<BR>
133
<DT><B>The <FONT COLOR=navy>Coq</FONT></B><B> standard library</B><DD>
134
A commented version of sources of the <FONT COLOR=navy>Coq</FONT> standard library
135
(including only the specifications, the proofs are removed)
136
is given in the additional document <TT>Library.ps</TT>.</DL>
139
<A HREF="toc.html"><IMG SRC ="contents_motif.gif" ALT="Up"></A>
140
<A HREF="Reference-Manual002.html"><IMG SRC ="next_motif.gif" ALT="Next"></A>
added
removed
manual/Reference-Manual001.html
