\setheaders{Introduction}
\chapter*{Introduction}

This document is the Reference Manual of version V7.0 of the \Coq\ 
proof assistant. A companion volume, the \Coq\ Tutorial, is provided
for the beginners. It is advised to read the Tutorial first.

The system \Coq\ is designed 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 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.  Other modes of interaction with
\Coq\ are possible, through an emacs shell window, or through a
customized interface with the Centaur environment (CTCoq). These
facilities are not documented here.

\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. Its use is
  documented in chapter \ref{Addoc-coqc}.
\end{itemize}

\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. The 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 Construction. The
  chapter \ref{Theories} describes the standard library of \Coq. The
  chapter \ref{Cic} is a mathematical description of the formalism. 

\item The second part describes the proof engine. It is divided in
  three chapters. Chapter \ref{Vernacular-commands} presents
  all commands (we call them \textit{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 the chapter \ref{Proof-handling}. In chapter \ref{Tactics}, 
  all commands that realize one or more steps of the proof are
  presented: we call them   \textit{tactics}. 

\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 In the fourth part more practical tools are documented. First in
  the 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.
\end{itemize}

At the end of the document, after the global index, the user can find
a tactic index and a vernacular command index.

\section*{List of additionnal documentation}

This manual contains not 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. A file UNINSTALL explains how
  uninstall or move it.

\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$ 

%%% Local Variables: 
%%% mode: latex
%%% TeX-master: "Reference-Manual"
%%% End: