← Back to branch summary

~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to doc/refman/RefMan-int.tex

  • Committer: Bazaar Package Importer
  • Author(s): Stéphane Glondu, Stéphane Glondu, Samuel Mimram
  • Date: 2010-01-07 22:50:39 UTC
  • mfrom: (1.2.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20100107225039-n3cq82589u0qt0s2
Tags: 8.2pl1-1
http://bugs.debian.org/563669
http://bugs.debian.org/543545
[ Stéphane Glondu ]
* New upstream release (Closes: #563669)
  - remove patches
* Packaging overhaul:
  - use git, advertise it in Vcs-* fields of debian/control
  - use debhelper 7 and dh with override
  - use source format 3.0 (quilt)
* debian/control:
  - set Maintainer to d-o-m, set Uploaders to Sam and myself
  - add Homepage field
  - bump Standards-Version to 3.8.3
* Register PDF documentation into doc-base
* Add debian/watch
* Update debian/copyright

[ Samuel Mimram ]
* Change coq-doc's description to mention that it provides documentation in
  pdf format, not postscript, closes: #543545.

Show diffs side-by-side

added added

removed removed

Lines of Context:
doc/refman/RefMan-int.tex
 
1
%BEGIN LATEX
 
2
\setheaders{Introduction}
 
3
%END LATEX
 
4
\chapter*{Introduction}
 
5
 
 
6
This document is the Reference Manual of version \coqversion{} of the \Coq\ 
 
7
proof assistant. A companion volume, the \Coq\ Tutorial, is provided
 
8
for the beginners. It is advised to read the Tutorial first.
 
9
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
 
10
the advanced user.
 
11
 
 
12
%The system \Coq\ is designed to develop mathematical proofs. It can be
 
13
%used by mathematicians to develop mathematical theories and by
 
14
%computer scientists to write formal specifications,
 
15
The \Coq{} system is designed to develop mathematical proofs, and
 
16
especially to write formal specifications, programs and to verify that
 
17
programs are correct with respect to their specification. It provides
 
18
a specification language named \gallina. Terms of \gallina\ can
 
19
represent programs as well as properties of these programs and proofs
 
20
of these properties. Using the so-called \textit{Curry-Howard
 
21
  isomorphism}, programs, properties and proofs are formalized in the
 
22
same language called \textit{Calculus of Inductive Constructions},
 
23
that is a $\lambda$-calculus with a rich type system.  All logical
 
24
judgments in \Coq\ are typing judgments. The very heart of the Coq
 
25
system is the type-checking algorithm that checks the correctness of
 
26
proofs, in other words that checks that a program complies to its
 
27
specification. \Coq\ also provides an interactive proof assistant to
 
28
build proofs using specific programs called \textit{tactics}.
 
29
 
 
30
All services of the \Coq\ proof assistant are accessible by
 
31
interpretation of a command language called \textit{the vernacular}.
 
32
 
 
33
\Coq\ has an interactive mode in which commands are interpreted as the
 
34
user types them in from the keyboard and a compiled mode where
 
35
commands are processed from a file.  
 
36
 
 
37
\begin{itemize}
 
38
\item The interactive mode may be used as a debugging mode in which
 
39
  the user can develop his theories and proofs step by step,
 
40
  backtracking if needed and so on. The interactive mode is run with
 
41
  the {\tt coqtop} command from the operating system (which we shall
 
42
  assume to be some variety of UNIX in the rest of this document).
 
43
\item The compiled mode acts as a proof checker taking a file
 
44
  containing a whole development in order to ensure its correctness.
 
45
  Moreover, \Coq's compiler provides an output file containing a
 
46
  compact representation of its input. The compiled mode is run with
 
47
  the {\tt coqc} command from the operating system. 
 
48
 
 
49
\end{itemize}
 
50
These two modes are documented in Chapter~\ref{Addoc-coqc}.
 
51
 
 
52
Other modes of interaction with \Coq{} are possible: through an emacs
 
53
shell window, an emacs generic user-interface for proof assistant
 
54
(ProofGeneral~\cite{ProofGeneral}) or through a customized interface
 
55
(PCoq~\cite{Pcoq}).  These facilities are not documented here.  There
 
56
is also a \Coq{} Integrated Development Environment described in
 
57
Chapter~\ref{Addoc-coqide}.
 
58
 
 
59
\section*{How to read this book}
 
60
 
 
61
This is a Reference Manual, not a User Manual, then it is not made for a
 
62
continuous reading. However, it has some structure that is explained
 
63
below.
 
64
 
 
65
\begin{itemize}
 
66
\item The first part describes the specification language,
 
67
  Gallina. Chapters~\ref{Gallina} and~\ref{Gallina-extension}
 
68
  describe the concrete syntax as well as the meaning of programs,
 
69
  theorems and proofs in the Calculus of Inductive
 
70
  Constructions. Chapter~\ref{Theories} describes the standard library
 
71
  of \Coq. Chapter~\ref{Cic} is a mathematical description of the
 
72
  formalism. Chapter~\ref{chapter:Modules} describes the module system.
 
73
 
 
74
\item The second part describes the proof engine. It is divided in
 
75
  five chapters. Chapter~\ref{Vernacular-commands} presents all
 
76
  commands (we call them \emph{vernacular commands}) that are not
 
77
  directly related to interactive proving: requests to the
 
78
  environment, complete or partial evaluation, loading and compiling
 
79
  files. How to start and stop proofs, do multiple proofs in parallel
 
80
  is explained in Chapter~\ref{Proof-handling}. In
 
81
  Chapter~\ref{Tactics}, all commands that realize one or more steps
 
82
  of the proof are presented: we call them \emph{tactics}. The
 
83
  language to combine these tactics into complex proof strategies is
 
84
  given in Chapter~\ref{TacticLanguage}. Examples of tactics are
 
85
  described in Chapter~\ref{Tactics-examples}.
 
86
 
 
87
%\item The third part describes how to extend the system in two ways:
 
88
%  adding parsing and pretty-printing rules
 
89
%  (Chapter~\ref{Addoc-syntax}) and writing new tactics
 
90
%  (Chapter~\ref{TacticLanguage}). 
 
91
 
 
92
\item The third part describes how to extend the syntax of \Coq. It
 
93
corresponds to the Chapter~\ref{Addoc-syntax}.
 
94
 
 
95
\item In the fourth part more practical tools are documented. First in
 
96
  Chapter~\ref{Addoc-coqc}, the usage of \texttt{coqc} (batch mode)
 
97
  and \texttt{coqtop} (interactive mode) with their options is
 
98
  described. Then, in Chapter~\ref{Utilities},
 
99
  various utilities that come with the \Coq\ distribution are
 
100
  presented.
 
101
  Finally, Chapter~\ref{Addoc-coqide} describes the \Coq{} integrated
 
102
  development environment. 
 
103
\end{itemize}
 
104
 
 
105
At the end of the document, after the global index, the user can find
 
106
specific indexes for tactics, vernacular commands, and error
 
107
messages. 
 
108
 
 
109
\section*{List of additional documentation}
 
110
 
 
111
This manual does not contain all the documentation the user may need
 
112
about \Coq{}. Various informations can be found in the following
 
113
documents:  
 
114
\begin{description}
 
115
 
 
116
\item[Tutorial] 
 
117
  A companion volume to this reference manual, the \Coq{} Tutorial, is
 
118
  aimed at gently introducing new users to developing proofs in \Coq{}
 
119
  without assuming prior knowledge of type theory. In a second step, the
 
120
  user can read also the tutorial on recursive types (document {\tt
 
121
    RecTutorial.ps}).
 
122
 
 
123
\item[Addendum] The fifth part (the Addendum) of the Reference Manual
 
124
  is distributed as a separate document. It contains more
 
125
  detailed documentation and examples about some specific aspects of the
 
126
  system that may interest only certain users. It shares the indexes,
 
127
  the page numbers and
 
128
  the bibliography with the Reference Manual. If you see in one of the
 
129
  indexes a page number that is outside the Reference Manual, it refers
 
130
  to the Addendum. 
 
131
 
 
132
\item[Installation] A text file INSTALL that comes with the sources
 
133
  explains how to install \Coq{}.
 
134
 
 
135
\item[The \Coq{} standard library]
 
136
A commented version of sources of the \Coq{} standard library
 
137
(including only the specifications, the proofs are removed) 
 
138
is given in the additional document {\tt Library.ps}.
 
139
 
 
140
\end{description}
 
141
 
 
142
 
 
143
% $Id: RefMan-int.tex 11308 2008-08-06 08:40:10Z jnarboux $ 
 
144
 
 
145
%%% Local Variables: 
 
146
%%% mode: latex
 
147
%%% TeX-master: "Reference-Manual"
 
148
%%% End: