From 3e96002677226c0cdaa8f355938a76cfb37a722a Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Thu, 14 Oct 2010 17:51:11 +0200 Subject: Imported Upstream version 8.3 --- doc/refman/RefMan-int.tex | 148 ++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 148 insertions(+) create mode 100644 doc/refman/RefMan-int.tex (limited to 'doc/refman/RefMan-int.tex') diff --git a/doc/refman/RefMan-int.tex b/doc/refman/RefMan-int.tex new file mode 100644 index 00000000..7b531409 --- /dev/null +++ b/doc/refman/RefMan-int.tex @@ -0,0 +1,148 @@ +%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: -- cgit v1.2.3