summaryrefslogtreecommitdiff
path: root/doc/refman/RefMan-int.tex
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2011-12-25 13:22:26 +0100
committerGravatar Stephane Glondu <steph@glondu.net>2011-12-25 13:22:26 +0100
commit5fe4ac437bed43547b3695664974f492b55cb553 (patch)
treebd16d3110326d9cacf9cd20b6606e32428f4012e /doc/refman/RefMan-int.tex
parent300293c119981054c95182a90c829058530a6b6f (diff)
parentaa33547c764a229e22d323ca213d46ea221b903e (diff)
Remove non-DFSG contentsupstream/8.3.pl3+dfsg
Diffstat (limited to 'doc/refman/RefMan-int.tex')
-rw-r--r--doc/refman/RefMan-int.tex148
1 files changed, 0 insertions, 148 deletions
diff --git a/doc/refman/RefMan-int.tex b/doc/refman/RefMan-int.tex
deleted file mode 100644
index 7b531409..00000000
--- a/doc/refman/RefMan-int.tex
+++ /dev/null
@@ -1,148 +0,0 @@
-%BEGIN LATEX
-\setheaders{Introduction}
-%END LATEX
-\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 book~\cite{CoqArt} on practical uses of the \Coq{} system was 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 11307 2008-08-06 08:38:57Z jnarboux $
-
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "Reference-Manual"
-%%% End: