1 files changed, 147 insertions, 0 deletions
diff --git a/doc/refman/RefMan-int.tex b/doc/refman/RefMan-int.tex
new file mode 100644
index 00000000..258d0ca0
--- /dev/null
+++ b/doc/refman/RefMan-int.tex
@@ -0,0 +1,147 @@
+\setheaders{Introduction}
+\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 new book~\cite{CoqArt} on practical uses of the \Coq{} system will
+be 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 8609 2006-02-24 13:32:57Z notin,no-port-forwarding,no-agent-forwarding,no-X11-forwarding,no-pty $ 
+
+%%% Local Variables: 
+%%% mode: latex
+%%% TeX-master: "Reference-Manual"
+%%% End: