Initial revision

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8143 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 127 insertions, 0 deletions

diff --git a/doc/RefMan-int.tex b/doc/RefMan-int.tex
new file mode 100755
index 0000000000..d874f7cdb9
--- /dev/null
+++ b/doc/RefMan-int.tex
@@ -0,0 +1,127 @@
+\setheaders{Introduction}
+\chapter*{Introduction}
+
+This document is the Reference Manual of version V6.2.4 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{WritingTactics})
+
+
+\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: