diff options
| author |  Stephane Glondu <steph@glondu.net> | 2012-01-12 16:02:20 +0100 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2012-01-12 16:02:20 +0100 |
| commit | 97fefe1fcca363a1317e066e7f4b99b9c1e9987b (patch) | |
| tree | 97ec6b7d831cc5fb66328b0c63a11db1cbb2f158 /doc | |
| parent | 300293c119981054c95182a90c829058530a6b6f (diff) | |
Imported Upstream version 8.4~betaupstream/8.4_beta
Diffstat (limited to 'doc')
43 files changed, 1026 insertions, 722 deletions
diff --git a/doc/common/macros.tex b/doc/common/macros.tex index d745f34a..f0fb0883 100755 --- a/doc/common/macros.tex +++ b/doc/common/macros.tex @@ -520,8 +520,6 @@ {\begin{center}\begin{rulebox}} {\end{rulebox}\end{center}} -% $Id: macros.tex 13091 2010-06-08 13:56:19Z herbelin $ - %%% Local Variables: %%% mode: latex diff --git a/doc/common/styles/html/coqremote/cover.html b/doc/common/styles/html/coqremote/cover.html index c3091b4e..f4809a48 100644 --- a/doc/common/styles/html/coqremote/cover.html +++ b/doc/common/styles/html/coqremote/cover.html @@ -1,10 +1,9 @@ -<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" - "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd"> -<html xmlns="http://www.w3.org/1999/xhtml" lang="en" xml:lang="en"> +<HTML> -<head> +<HEAD> +<TITLE>Cover Page</TITLE> -<meta http-equiv="Content-Type" content="text/html; charset=ISO-8859-1"/> +<meta http-equiv="Content-Type" content="text/html; charset=ISO-8859-1"> <title>Reference Manual | The Coq Proof Assistant</title> <link rel="shortcut icon" href="favicon.ico" type="image/x-icon" /> @@ -18,9 +17,9 @@ <style type="text/css" media="all">@import "http://coq.inria.fr/sites/all/themes/coq/style.css";</style> <style type="text/css" media="all">@import "http://coq.inria.fr/sites/all/themes/coq/coqdoc.css";</style> -</head> +</HEAD> -<body> +<BODY> <div id="container"> <div id="headertop"> @@ -28,6 +27,7 @@ <ul class="links-menu"> <li><a href="http://coq.inria.fr/" class="active">Home</a></li> + <li><a href="http://coq.inria.fr/about-coq" title="More about coq">About Coq</a></li> <li><a href="http://coq.inria.fr/download">Get Coq</a></li> <li><a href="http://coq.inria.fr/documentation">Documentation</a></li> @@ -54,27 +54,29 @@ <h1 style="text-align: center; font-weight:bold; font-size: 300%; line-height: 2ex">Reference Manual</h1> <h2 style="text-align:center; font-size: 120%"> - Version 8.3<a name="text1"></a><sup><a href="#note1"><span style="font-size: 80%">1</span></a></sup> + Version trunk<a name="text1"></a><a href="#note1"><SUP><span style="font-size: 80%">1</span></SUP></a> <br/><br/><br/><br/><br/><br/> <span style="text-align: center; font-size: 120%; ">The Coq Development Team</span> <br/><br/><br/><br/><br/><br/> -</h2> + <div style="text-align: left; font-size: 80%; text-indent: 0pt"> <ul style="list-style: none; margin-left: 0pt"> <li>V7.x © INRIA 1999-2004</li> - <li>V8.x © INRIA 2004-2010</li> + <li>V8.0 © INRIA 2004-2006</li> + <li>V8.1 © INRIA 2006-2008</li> + <li>V8.2 © INRIA 2008-2009</li> </ul> <p style="text-indent: 0pt">This material may be distributed only subject to the terms and conditions set forth in the Open Publication License, v1.0 or later (the latest version is presently available at <a href="http://www.opencontent.org/openpub">http://www.opencontent.org/openpub</a>). Options A and B are not elected.</p> </div> <br/> -<hr style="width: 75%"/> +<hr width="75%" size=1> <div style="text-align: left; font-size: 80%; text-indent: 0pt"> <dl> - <dt><a name="note1" href="toc.html#text1">1</a></dt> + <dt><a name="note1" href="toc.html#text1">1</a> <dd>This research was partly supported by IST working group ``Types''</dd> </dl> </div> diff --git a/doc/common/styles/html/coqremote/footer.html b/doc/common/styles/html/coqremote/footer.html deleted file mode 100644 index 2b4e0de0..00000000 --- a/doc/common/styles/html/coqremote/footer.html +++ /dev/null @@ -1,43 +0,0 @@ -<div id="sidebarWrapper"> -<div id="sidebar"> - -<div class="block"> -<h2 class="title">Navigation</h2> -<div class="content"> - -<ul class="menu"> - -<li class="leaf">Standard Library - <ul class="menu"> - <li><a href="index.html">Table of contents</a></li> - <li><a href="genindex.html">Index</a></li> - </ul> -</li> - -</ul> - -</div> -</div> - -</div> -</div> - - -</div> - -<div id="footer"> -<div id="nav-footer"> - <ul class="links-menu-footer"> - <li><a href="mailto:www-coq_@_lix.polytechnique.fr">webmaster</a></li> - <li><a href="http://validator.w3.org/check?uri=referer">xhtml valid</a></li> - <li><a href="http://jigsaw.w3.org/css-validator/check/referer">CSS valid</a></li> - </ul> - -</div> -</div> - -</div> - -</body> -</html> - diff --git a/doc/common/styles/html/coqremote/header.html b/doc/common/styles/html/coqremote/header.html deleted file mode 100644 index 025e1d3a..00000000 --- a/doc/common/styles/html/coqremote/header.html +++ /dev/null @@ -1,49 +0,0 @@ -<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd"> -<html xmlns="http://www.w3.org/1999/xhtml" lang="en" xml:lang="en"> - -<head> -<meta http-equiv="Content-Type" content="text/html; charset=utf-8"/> -<title>Standard Library | The Coq Proof Assistant</title> - -<link rel="shortcut icon" href="favicon.ico" type="image/x-icon" /> -<style type="text/css" media="all">@import "http://coq.inria.fr/modules/node/node.css";</style> - -<style type="text/css" media="all">@import "http://coq.inria.fr/modules/system/defaults.css";</style> -<style type="text/css" media="all">@import "http://coq.inria.fr/modules/system/system.css";</style> -<style type="text/css" media="all">@import "http://coq.inria.fr/modules/user/user.css";</style> - -<style type="text/css" media="all">@import "http://coq.inria.fr/sites/all/themes/coq/style.css";</style> -<style type="text/css" media="all">@import "http://coq.inria.fr/sites/all/themes/coq/coqdoc.css";</style> - -</head> - -<body> - -<div id="container"> -<div id="headertop"> -<div id="nav"> - <ul class="links-menu"> - <li><a href="http://coq.inria.fr/" class="active">Home</a></li> - - <li><a href="http://coq.inria.fr/about-coq" title="More about coq">About Coq</a></li> - <li><a href="http://coq.inria.fr/download">Get Coq</a></li> - <li><a href="http://coq.inria.fr/documentation">Documentation</a></li> - <li><a href="http://coq.inria.fr/community">Community</a></li> - </ul> -</div> -</div> - -<div id="header"> - -<div id="logoWrapper"> - -<div id="logo"><a href="http://coq.inria.fr/" title="Home"><img src="http://coq.inria.fr/files/barron_logo.png" alt="Home" /></a> -</div> -<div id="siteName"><a href="http://coq.inria.fr/" title="Home">The Coq Proof Assistant</a> -</div> - -</div> -</div> - -<div id="content"> - diff --git a/doc/common/styles/html/coqremote/styles.hva b/doc/common/styles/html/coqremote/styles.hva index ec14840b..82f18681 100644 --- a/doc/common/styles/html/coqremote/styles.hva +++ b/doc/common/styles/html/coqremote/styles.hva @@ -2,16 +2,16 @@ \begin{rawhtml} <meta http-equiv="Content-Type" content="text/html; charset=ISO-8859-1"> -<LINK rel="shortcut icon" href="favicon.ico" type="image/x-icon"> -<STYLE type="text/css" media="all">@import "http://coq.inria.fr/modules/node/node.css";</STYLE> +<link rel="shortcut icon" href="favicon.ico" type="image/x-icon" /> +<style type="text/css" media="all">@import "http://coq.inria.fr/modules/node/node.css";</style> -<STYLE type="text/css" media="all">@import "http://coq.inria.fr/modules/system/defaults.css";</STYLE> -<STYLE type="text/css" media="all">@import "http://coq.inria.fr/modules/system/system.css";</STYLE> -<STYLE type="text/css" media="all">@import "http://coq.inria.fr/modules/user/user.css";</STYLE> +<style type="text/css" media="all">@import "http://coq.inria.fr/modules/system/defaults.css";</style> +<style type="text/css" media="all">@import "http://coq.inria.fr/modules/system/system.css";</style> +<style type="text/css" media="all">@import "http://coq.inria.fr/modules/user/user.css";</style> -<STYLE type="text/css" media="all">@import "http://coq.inria.fr/sites/all/themes/coq/style.css";</STYLE> -<STYLE type="text/css" media="all">@import "http://coq.inria.fr/sites/all/themes/coq/coqdoc.css";</STYLE> -<STYLE type="text/css" media="all">@import "http://coq.inria.fr/sites/all/themes/coq/hevea.css";</STYLE> +<style type="text/css" media="all">@import "http://coq.inria.fr/sites/all/themes/coq/style.css";</style> +<style type="text/css" media="all">@import "http://coq.inria.fr/sites/all/themes/coq/coqdoc.css";</style> +<style type="text/css" media="all">@import "http://coq.inria.fr/sites/all/themes/coq/hevea.css";</style> \end{rawhtml}} % for HeVeA @@ -35,7 +35,7 @@ <div id="logoWrapper"> -<div id="logo"><a href="http://coq.inria.fr/" title="Home"><img src="http://coq.inria.fr/files/barron_logo.png" alt="Home"></a> +<div id="logo"><a href="http://coq.inria.fr/" title="Home"><img src="http://coq.inria.fr/files/barron_logo.png" alt="Home" /></a> </div> <div id="siteName"><a href="http://coq.inria.fr/" title="Home">The Coq Proof Assistant</a> </div> @@ -79,6 +79,8 @@ </div> +</div> + <div id="footer"> <div id="nav-footer"> <ul class="links-menu-footer"> diff --git a/doc/common/styles/html/simple/cover.html b/doc/common/styles/html/simple/cover.html index b377396d..75b938f9 100644 --- a/doc/common/styles/html/simple/cover.html +++ b/doc/common/styles/html/simple/cover.html @@ -25,7 +25,7 @@ <h1 style="font-weight:bold; font-size: 300%; line-height: 2ex">Reference Manual</h1> <h2 style="font-size: 120%"> - Version 8.3<a name="text1"></a><a href="#note1"><sup><span style="font-size: 80%">1</span></sup></a></h2> + Version 8.2<a name="text1"></a><a href="#note1"><sup><span style="font-size: 80%">1</span></sup></a></h2> <br/><br/><br/><br/><br/><br/> <p><span style="text-align: center; font-size: 120%; ">The Coq Development Team</span></p> @@ -35,7 +35,9 @@ <div style="text-align: left; font-size: 80%; text-indent: 0pt"> <ul style="list-style: none; margin-left: 0pt"> <li>V7.x © INRIA 1999-2004</li> - <li>V8.x © INRIA 2004-2010</li> + <li>V8.0 © INRIA 2004-2006</li> + <li>V8.1 © INRIA 2006-2008</li> + <li>V8.2 © INRIA 2008-2009</li> </ul> <p style="text-indent: 0pt">This material may be distributed only subject to the terms and conditions set forth in the Open Publication License, v1.0 or later (the latest version is presently available at <a href="http://www.opencontent.org/openpub">http://www.opencontent.org/openpub</a>). Options A and B are not elected.</p> diff --git a/doc/common/styles/html/simple/header.html b/doc/common/styles/html/simple/header.html deleted file mode 100644 index 14d2f988..00000000 --- a/doc/common/styles/html/simple/header.html +++ /dev/null @@ -1,13 +0,0 @@ -<!DOCTYPE html - PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" - "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd"> - -<html xmlns="http://www.w3.org/1999/xhtml" xml:lang="en" lang="en"> -<head> -<meta http-equiv="Content-Type" content="text/html; charset=iso-8859-15"/> -<link rel="stylesheet" href="coqdoc.css" type="text/css"/> -<title>The Coq Standard Library</title> -</head> - -<body> - diff --git a/doc/common/styles/html/simple/styles.hva b/doc/common/styles/html/simple/styles.hva index a2d46f3e..76935cb1 100644 --- a/doc/common/styles/html/simple/styles.hva +++ b/doc/common/styles/html/simple/styles.hva @@ -1,7 +1,6 @@ \renewcommand{\@meta}{ \begin{rawhtml} <meta http-equiv="Content-Type" content="text/html; charset=ISO-8859-1"> -<title>Reference Manual | The Coq Proof Assistant</title> <link rel="stylesheet" type="text/css" href="style.css"> <link rel="stylesheet" type="text/css" href="coqdoc.css"> diff --git a/doc/common/title.tex b/doc/common/title.tex index 38ec0e55..1dc52432 100755 --- a/doc/common/title.tex +++ b/doc/common/title.tex @@ -25,12 +25,12 @@ The Coq Proof Assistant\\[12pt] #1\\[20pt] \Large\today\\[20pt] -Version \coqversion%\footnote[1]{This research was partly supported by IST working group ``Types''} +Version \coqversion\footnote[1]{This research was partly supported by IST working group ``Types''} \vspace{0pt plus .5fill} #2 \par\vfill -The Coq Development Team +TypiCal Project (formerly LogiCal) \vspace*{15pt} \end{center} @@ -45,7 +45,7 @@ V\coqversion, \today %END LATEX \copyright INRIA 1999-2004 ({\Coq} versions 7.x) -\copyright INRIA 2004-2011 ({\Coq} versions 8.x) +\copyright INRIA 2004-2009 ({\Coq} versions 8.x) #3 \end{flushleft} @@ -70,4 +70,3 @@ V\coqversion, \today % TeX-master: "" % End: -% $Id: title.tex 14641 2011-11-06 11:59:10Z herbelin $ diff --git a/doc/faq/FAQ.tex b/doc/faq/FAQ.tex index bd6f7dbf..c0f8c087 100644 --- a/doc/faq/FAQ.tex +++ b/doc/faq/FAQ.tex @@ -22,7 +22,6 @@ \usepackage[dvips]{graphicx} \fi -\input{../common/version.tex} %\input{../macros.tex} % Making hevea happy @@ -134,7 +133,7 @@ %%%%%%% Coq pour les nuls %%%%%%% -\title{Coq Version {\coqversion} for the Clueless\\ +\title{Coq Version 8.3 for the Clueless\\ \large(\protect\ref{lastquestion} \ Hints) } @@ -166,7 +165,7 @@ proofs in \Coq. Since we are singularly short-minded, we wrote the answers we found on bits of papers to have them at hand whenever the situation occurs again. This is pretty much the result of that: a collection of tips one can refer to when proofs become intricate. Yes, -this means we won't take the blame for the shortcomings of this +it means we won't take the blame for the shortcomings of this FAQ. But if you want to contribute and send in your own question and answers, feel free to write to us\ldots @@ -372,7 +371,7 @@ downloadable postscripts. \Question{Where can I find this FAQ on the web?} -This FAQ is available online at \ahref{http://coq.inria.fr/faq}{\url{http://coq.inria.fr/faq}}. +This FAQ is available online at \ahref{http://coq.inria.fr/doc/faq.html}{\url{http://coq.inria.fr/doc/faq.html}}. \Question{How can I submit suggestions / improvements / additions for this FAQ?} @@ -380,20 +379,20 @@ This FAQ is unfinished (in the sense that there are some obvious sections that are missing). Please send contributions to Coq-Club. \Question{Is there any mailing list about {\Coq}?} -The main {\Coq} mailing list is \url{coq-club@inria.fr}, which +The main {\Coq} mailing list is \url{coq-club@pauillac.inria.fr}, which broadcasts questions and suggestions about the implementation, the logical formalism or proof developments. See -\ahref{http://coq.inria.fr/mailman/listinfo/coq-club}{\url{https://sympa-roc.inria.fr/wws/info/coq-club}} for +\ahref{http://coq.inria.fr/mailman/listinfo/coq-club}{\url{http://pauillac.inria.fr/mailman/listinfo/coq-club}} for subscription. For bugs reports see question \ref{coqbug}. \Question{Where can I find an archive of the list?} The archives of the {\Coq} mailing list are available at -\ahref{http://pauillac.inria.fr/pipermail/coq-club}{\url{https://sympa-roc.inria.fr/wws/arc/coq-club}}. +\ahref{http://pauillac.inria.fr/pipermail/coq-club}{\url{http://coq.inria.fr/pipermail/coq-club}}. \Question{How can I be kept informed of new releases of {\Coq}?} -New versions of {\Coq} are announced on the coq-club mailing list. +New versions of {\Coq} are announced on the coq-club mailing list. If you only want to receive information about new releases, you can subscribe to {\Coq} on \ahref{http://freshmeat.net/projects/coq/}{\url{http://freshmeat.net/projects/coq/}}. \Question{Is there any book about {\Coq}?} @@ -417,7 +416,7 @@ You can also find large developments using \Question{How can I report a bug?}\label{coqbug} -You can use the web interface accessible at \ahref{http://coq.inria.fr/bugs}{\url{http://coq.inria.fr/bugs}}. +You can use the web interface accessible at \ahref{http://coq.inria.fr}{\url{http://coq.inria.fr}}, link ``contacts''. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @@ -432,7 +431,7 @@ You can use the web interface accessible at \ahref{http://coq.inria.fr/bugs}{\ur The sources of {\Coq} can be found online in the tar.gz'ed packages (\ahref{http://coq.inria.fr}{\url{http://coq.inria.fr}}, link ``download''). Development sources can be accessed at -\ahref{https://gforge.inria.fr/scm/?group_id=269}{\url{https://gforge.inria.fr/scm/?group_id=269}} +\ahref{http://coq.gforge.inria.fr/}{\url{http://coq.gforge.inria.fr/}} \Question{On which platform is {\Coq} available?} Compiled binaries are available for Linux, MacOS X, and Windows. The @@ -666,9 +665,10 @@ where both excluded-middle and the axiom of description are valid (see file \vfile{\LogicClassicalDescription}{ClassicalDescription} for a proof that excluded-middle and description implies the double negation of excluded-middle in {\Set} and file {\tt Hurkens\_Set.v} from the -user contribution {\tt Rocq/PARADOXES} for a proof that -impredicativity of {\Set} implies the simple negation of -excluded-middle in {\Set}). +user contribution {\tt Paradoxes} at +\ahref{http://coq.inria.fr/contribs}{\url{http://coq.inria.fr/contribs}} +for a proof that impredicativity of {\Set} implies the simple negation +of excluded-middle in {\Set}). \Question{Is {\Type} impredicative?} @@ -1509,7 +1509,7 @@ apply the elimination scheme using the \verb=using= option of The short answer : You should use {\texttt le\_lt\_dec n p} instead.\\ -That's right, you can't. +The long answer: That's right, you can't. If you type for instance the following ``definition'': \begin{coq_eval} Reset Initial. @@ -1627,7 +1627,7 @@ certified programs which need to compare natural numbers, and is not designed to compare quickly two numbers. Nevertheless, the \emph{extraction} of \texttt{le\_lt\_dec} towards -\emph{Ocaml} or \emph{Haskell}, is a reasonable program for comparing two +\emph{OCaml} or \emph{Haskell}, is a reasonable program for comparing two natural numbers in Peano form in linear time. It is also possible to keep your boolean function as a decision procedure, @@ -1700,7 +1700,7 @@ Lemma Rwf : well_founded R. \item Define the step function (which needs proofs that recursive calls are on smaller arguments). -\begin{coq_example*} +\begin{verbatim} Definition split (l : list nat) : {l1: list nat | R l1 l} * {l2 : list nat | R l2 l} := (* ... *) . @@ -1710,7 +1710,7 @@ Definition merge_step (l : list nat) (f: forall l':list nat, R l' l -> list nat) let (l1,H1) := lH1 in let (l2,H2) := lH2 in concat (f l1 H1) (f l2 H2). -\end{coq_example*} +\end{verbatim} \item Define the recursive function by fixpoint on the step function. @@ -1890,13 +1890,15 @@ because ``$^2$'' is an iso-latin character. If you really want this kind of nota \Question{Why ``no associativity'' and ``left associativity'' at the same level does not work?} -Because we relie on camlp4 for syntactical analysis and camlp4 does not really implement no associativity. By default, non associative operators are defined as right associative. +Because we relie on Camlp4 for syntactical analysis and Camlp4 does not really +implement no associativity. By default, non associative operators are defined +as right associative. \Question{How can I know the associativity associated with a level?} -You can do ``Print Grammar constr'', and decode the output from camlp4, good luck ! +You can do ``Print Grammar constr'', and decode the output from Camlp4, good luck ! \section{Modules} @@ -1991,13 +1993,81 @@ todo \Question{How can I define static and dynamic code?} \fi -\section{Tactics written in Ocaml} +\section{Tactics written in OCaml} \Question{Can you show me an example of a tactic written in OCaml?} -You have some examples of tactics written in Ocaml in the ``plugins'' directory of {\Coq} sources. - - +Have a look at the skeleton ``Hello World'' tactic from the next question. +You also have some examples of tactics written in OCaml in the ``plugins'' directory of {\Coq} sources. + +\Question{Is there a skeleton of OCaml tactic I can reuse somewhere?} + +The following steps describe how to write a simplistic ``Hello world'' OCaml +tactic. This takes the form of a dynamically loadable OCaml module, which will +be invoked from the Coq toplevel. +\begin{enumerate} +\item In the \verb+plugins+ directory of the Coq source location, create a +directory \verb+hello+. Proceed to create a grammar and OCaml file, respectively +\verb+plugins/hello/g_hello.ml4+ and \verb+plugins/hello/coq_hello.ml+, +containing: + \begin{itemize} + \item in \verb+g_hello.ml4+: +\begin{verbatim} +(*i camlp4deps: "parsing/grammar.cma" i*) +TACTIC EXTEND Hello +| [ "hello" ] -> [ Coq_hello.printHello ] +END +\end{verbatim} + \item in \verb+coq_hello.ml+: +\begin{verbatim} +let printHello gl = +Tacticals.tclIDTAC_MESSAGE (Pp.str "Hello world") gl + \end{verbatim} + \end{itemize} +\item Create a file \verb+plugins/hello/hello_plugin.mllib+, containing the +names of the OCaml modules bundled in the dynamic library: +\begin{verbatim} +Coq_hello +G_hello +\end{verbatim} +\item Append the following lines in \verb+plugins/plugins{byte,opt}.itarget+: +\begin{itemize} + \item in \verb+pluginsopt.itarget+: +\begin{verbatim} +hello/hello_plugin.cmxa +\end{verbatim} + \item in \verb+pluginsbyte.itarget+: +\begin{verbatim} +hello/hello_plugin.cma +\end{verbatim} +\end{itemize} +\item In the root directory of the Coq source location, modify the file +\verb+Makefile.common+: + \begin{itemize} + \item add \verb+hello+ to the \verb+SRCDIR+ definition (second argument of the + \verb+addprefix+ function); + \item in the section ``Object and Source files'', add \verb+HELLOCMA:=plugins/hello/hello_plugin.cma+; + \item add \verb+$(HELLOCMA)+ to the \verb+PLUGINSCMA+ definition. + \end{itemize} +\item Modify the file \verb+Makefile.build+, adding in section ``3) plugins'' the +line: +\begin{verbatim} +hello: $(HELLOCMA) +\end{verbatim} +\item From the command line, run \verb+make hello+, then \verb+make plugins/hello/hello_plugin.cmxs+. +\end{enumerate} +The call to the tactic \verb+hello+ from a Coq script has to be preceded by +\verb+Declare ML Module "hello_plugin"+, which will load the dynamic object +\verb+hello_plugin.cmxs+. For instance: +\begin{verbatim} +Declare ML Module "hello_plugin". +Variable A:Prop. +Goal A-> A. +Proof. +hello. +auto. +Qed. +\end{verbatim} \section{Case studies} @@ -2238,7 +2308,8 @@ You can use this bibtex entry: @Manual{Coq:manual, title = {The Coq proof assistant reference manual}, author = {\mbox{The Coq development team}}, - note = {Version 8.3}, + organization = {LogiCal Project}, + note = {Version 8.2}, year = {2009}, url = "http://coq.inria.fr" } @@ -2276,8 +2347,8 @@ Depending on your configuration, use either one of these two methods \begin{itemize} \item Insert \texttt{gtk-key-theme-name = "Emacs"} - in your \texttt{.coqide-gtk2rc} file. It may be in the current dir - or in \verb#$HOME# dir. This is done by default. + in your \texttt{coqide-gtk2rc} file. It should be in + \verb#$XDG_CONFIG_DIRS/coq# dir. This is done by default. \item If in Gnome, run the gnome configuration editor (\texttt{gconf-editor}) and set key \texttt{gtk-key-theme} to \texttt{Emacs} in the category @@ -2323,21 +2394,32 @@ pretty simple notations. 2200 is the hexadecimal code for forall in unicode charts and is encoded as in UTF-8. 2203 is for exists. See \ahref{http://www.unicode.org}{\url{http://www.unicode.org}} for more codes. -\item Second solution: rebind \verb#<AltGr>a# to forall and \verb#<AltGr>e# to exists. - Under X11, you need to use something like +\item Second solution: rebind \verb#<AltGr>a# to forall and \verb#<AltGr>e# to exists. + + Under X11, one can add those lines in the file ~/.xmodmaprc : + \begin{verbatim} - xmodmap -e "keycode 24 = a A F13 F13" - xmodmap -e "keycode 26 = e E F14 F14" +! forall +keycode 24 = a A a A U2200 NoSymbol U2200 NoSymbol +! exists +keycode 26 = e E e E U2203 NoSymbol U2203 NoSymbol \end{verbatim} - and then to add +and then run xmodmap ~/.xmodmaprc. + + Alternatively, if your version of \verb=xmodmap= does not support unicode, you need to use something like \begin{verbatim} - bind "F13" {"insert-at-cursor" ("")} - bind "F14" {"insert-at-cursor" ("")} +xmodmap -e "keycode 24 = a A F13 F13" +xmodmap -e "keycode 26 = e E F14 F14" \end{verbatim} - to your "binding "text"" section in \verb#.coqiderc-gtk2rc.# - The strange ("") argument is the UTF-8 encoding for - 0x2200. - You can compute these encodings using the lablgtk2 toplevel with + and then to add + +\verb=bind "F13" {"insert-at-cursor" ("=$\forall$\verb=")}=\\ +\verb=bind "F14" {"insert-at-cursor" ("=$\exists$\verb=")}= + + to your "binding "text"" section in \verb#coqiderc-gtk2rc#. + The last arguments to {\tt bind} between "" are + the UTF-8 encodings for 0x2200 and 0x2203. + You can compute these encodings using the lablgtk2 toplevel with \begin{verbatim} Glib.Utf8.from_unichar 0x2200;; \end{verbatim} @@ -2345,17 +2427,11 @@ Glib.Utf8.from_unichar 0x2200;; do not need . \end{itemize} -\Question{How to build a custom {\CoqIde} with user ml code?} - Use - coqmktop -ide -byte m1.cmo...mi.cmo - or - coqmktop -ide -opt m1.cmx...mi.cmx - \Question{How to customize the shortcuts for menus?} Two solutions are offered: \begin{itemize} -\item Edit \$HOME/.coqide.keys by hand or -\item Add "gtk-can-change-accels = 1" in your .coqide-gtk2rc file. Then +\item Edit \verb+$XDG_CONFIG_HOME/coq/coqide.keys+ (which is usually \verb+$HOME/.config/coq/coqide.keys+) by hand or +\item Add "gtk-can-change-accels = 1" in your coqide-gtk2rc file. Then from \CoqIde, you may select a menu entry and press the desired shortcut. \end{itemize} @@ -2375,9 +2451,9 @@ Glib.Utf8.from_unichar 0x2200;; Some users may experiment problems with unwanted automatic templates while using Coqide. This is due to a change in the modifiers keys available through GTK. The straightest way to get -rid of the problem is to edit by hand your .coqiderc (either -\verb|/home/<user>/.coqiderc| under Linux, or \\ -\verb|C:\Documents and Settings\<user>\.coqiderc| under Windows) +rid of the problem is to edit by hand your coqiderc (either +\verb|/home/<user>/.config/coq/coqiderc| under Linux, or \\ +\verb|C:\Documents and Settings\<user>\.config\coq\coqiderc| under Windows) and replace any occurence of \texttt{MOD4} by \texttt{MOD1}. diff --git a/doc/faq/fk.bib b/doc/faq/fk.bib index 976b36b0..d41ab7f0 100644 --- a/doc/faq/fk.bib +++ b/doc/faq/fk.bib @@ -1117,9 +1117,10 @@ cedures.}, @Manual{Coq:manual, title = {The Coq proof assistant reference manual}, author = {\mbox{The Coq development team}}, - note = {Version 8.3}, - year = {2010}, - url = "http://coq.inria.fr/doc" + organization = {LogiCal Project}, + note = {Version 8.0}, + year = {2004}, + url = "http://coq.inria.fr" } @string{jfp = "Journal of Functional Programming"} diff --git a/doc/refman/Classes.tex b/doc/refman/Classes.tex index f427609f..20ff649a 100644 --- a/doc/refman/Classes.tex +++ b/doc/refman/Classes.tex @@ -10,7 +10,7 @@ \label{typeclasses} \begin{flushleft} - \em The status of Type Classes is experimental. + \em The status of Type Classes is (extremely) experimental. \end{flushleft} This chapter presents a quick reference of the commands related to type @@ -128,7 +128,9 @@ particular support for type classes: methods. In the example above, \texttt{A} and \texttt{eqa} should be set maximally implicit. \item They support implicit quantification on partialy applied type - classes. + classes (\S \ref{implicit-generalization}). + Any argument not given as part of a type class binder will be + automatically generalized. \item They also support implicit quantification on superclasses (\S \ref{classes:superclasses}) \end{itemize} @@ -141,19 +143,6 @@ Definition neqb_impl `{eqa : EqDec A} (x y : A) := negb (eqb x y). Here \texttt{A} is implicitly generalized, and the resulting function is equivalent to the one above. -The parsing of generalized type-class binders is different from regular -binders: -\begin{itemize} -\item Implicit arguments of the class type are ignored. -\item Superclasses arguments are automatically generalized. -\item Any remaining arguments not given as part of a type class binder - will be automatically generalized. In other words, the rightmost - parameters are automatically generalized if not mentionned. -\end{itemize} - -One can switch off this special treatment using the $!$ mark in front of -the class name (see example below). - \asection{Parameterized Instances} One can declare parameterized instances as in \Haskell simply by giving @@ -242,9 +231,9 @@ Definition le_eqb `{Ord A} (x y : A) := andb (le x y) (le y x). \end{coq_example*} In some cases, to be able to specify sharing of structures, one may want to give -explicitly the superclasses. It is possible to do it directly in regular -generalized binders, and using the \texttt{!} modifier in class -binders. For example: +explicitly the superclasses. It is is possible to do it directly in regular +binders, and using the \texttt{!} modifier in class binders. For +example: \begin{coq_example*} Definition lt `{eqa : EqDec A, ! Ord eqa} (x y : A) := andb (le x y) (neqb x y). @@ -378,6 +367,12 @@ instances at the end of sections, or declaring structure projections as instances. This is almost equivalent to {\tt Hint Resolve {\ident} : typeclass\_instances}. +\begin{Variants} +\item {\tt Existing Instances {\ident}$_1$ \ldots {\ident}$_n$} + \comindex{Existing Instances} + With this command, several existing instances can be declared at once. +\end{Variants} + \subsection{\tt Context {\binder$_1$ \ldots \binder$_n$}} \comindex{Context} \label{Context} diff --git a/doc/refman/Extraction.tex b/doc/refman/Extraction.tex index cc9cf5c8..ee289ee7 100644 --- a/doc/refman/Extraction.tex +++ b/doc/refman/Extraction.tex @@ -469,9 +469,9 @@ mandatory. It only enhances readability of extracted code. You can then copy-paste the output to a file {\tt euclid.ml} or let \Coq\ do it for you with the following command: -\begin{coq_example} +\begin{verbatim} Extraction "euclid" eucl_dev. -\end{coq_example} +\end{verbatim} Let us play the resulting program: @@ -543,8 +543,6 @@ Some pathological examples of extraction are grouped in the file After compilation those two examples run nonetheless, thanks to the correction of the extraction~\cite{Let02}. -% $Id: Extraction.tex 14575 2011-10-18 15:49:01Z letouzey $ - %%% Local Variables: %%% mode: latex %%% TeX-master: "Reference-Manual" diff --git a/doc/refman/Micromega.tex b/doc/refman/Micromega.tex index 2fe7c2f7..5f9ed443 100644 --- a/doc/refman/Micromega.tex +++ b/doc/refman/Micromega.tex @@ -1,33 +1,24 @@ -\achapter{Micromega : tactics for solving arithmetics goals over ordered rings} +\achapter{Micromega : tactics for solving arithmetic goals over ordered rings} \aauthor{Frédéric Besson and Evgeny Makarov} \newtheorem{theorem}{Theorem} -For using the tactics out-of-the-box, read Section~\ref{sec:psatz-hurry}. -% -Section~\ref{sec:psatz-back} presents some background explaining the proof principle for solving polynomials goals. -% -Section~\ref{sec:lia} explains how to get a complete procedure for linear integer arithmetic. - -\asection{The {\tt psatz} tactic in a hurry} -\tacindex{psatz} + +\asection{Short description of the tactics} +\tacindex{psatz} \tacindex{lra} \label{sec:psatz-hurry} -Load the {\tt Psatz} module ({\tt Require Psatz}.). This module defines the tactics: -{\tt lia}, {\tt psatzl D}, %{\tt sos D} -and {\tt psatz D n} where {\tt D} is {\tt Z}, {\tt Q} or {\tt R} and {\tt n} is an optional integer limiting the proof search depth. - % - \begin{itemize} - \item The {\tt psatzl} tactic solves linear goals using an embedded (naive) linear programming prover \emph{i.e.}, - fourier elimination. - \item The {\tt psatz} tactic solves polynomial goals using John Harrison's Hol light driver to the external prover {\tt cspd}\footnote{Sources and binaries can be found at \url{https://projects.coin-or.org/Csdp}}. Note that the {\tt csdp} driver is generating - a \emph{proof cache} thus allowing to rerun scripts even without {\tt csdp}. - \item The {\tt lia} (linear integer arithmetic) tactic is specialised to solve linear goals over $\mathbb{Z}$. - It extends {\tt psatzl Z} and exploits the discreetness of $\mathbb{Z}$. -%% \item The {\tt sos} tactic is another Hol light driver to the {\tt csdp} prover. In theory, it is less general than -%% {\tt psatz}. In practice, even when {\tt psatz} fails, it can be worth a try -- see -%% Section~\ref{sec:psatz-back} for details. - \end{itemize} - -These tactics solve propositional formulas parameterised by atomic arithmetics expressions +The {\tt Psatz} module ({\tt Require Psatz.}) gives access to several tactics for solving arithmetic goals over + {\tt Z}\footnote{Support for {\tt nat} and {\tt N} is obtained by pre-processing the goal with the {\tt zify} tactic.}, {\tt Q} and {\tt R}: +\begin{itemize} +\item {\tt lia} is a decision procedure for linear integer arithmetic (see Section~\ref{sec:lia}); +\item {\tt nia} is an incomplete proof procedure for integer non-linear arithmetic (see Section~\ref{sec:nia}); +\item {\tt lra} is a decision procedure for linear (real or rational) arithmetic goals (see Section~\ref{sec:lra}); +\item {\tt psatz D n} where {\tt D} is {\tt Z}, {\tt Q} or {\tt R} and {\tt n} is an optional integer limiting the proof search depth is +is an incomplete proof procedure for non-linear arithmetic. It is based on John Harrison's Hol light driver to the external prover {\tt cspd}\footnote{Sources and binaries can be found at \url{https://projects.coin-or.org/Csdp}}. + Note that the {\tt csdp} driver is generating + a \emph{proof cache} thus allowing to rerun scripts even without {\tt csdp} (see Section~\ref{sec:psatz}). +\end{itemize} + +The tactics solve propositional formulas parameterised by atomic arithmetics expressions interpreted over a domain $D \in \{\mathbb{Z}, \mathbb{Q}, \mathbb{R} \}$. The syntax of the formulas is the following: \[ @@ -39,21 +30,29 @@ The syntax of the formulas is the following: \] where $c$ is a numeric constant, $x\in D$ is a numeric variable and the operators $-$, $+$, $\times$, are respectively subtraction, addition, product, $p \verb!^!n $ is exponentiation by a constant $n$, $P$ is an - arbitrary proposition. %that is mostly ignored. -%% -%% Over $\mathbb{Z}$, $c$ is an integer ($c \in \mathtt{Z}$), over $\mathbb{Q}$, $c$ is -The following table details for each domain $D \in \{\mathbb{Z},\mathbb{Q},\mathbb{R}\}$ the range of constants $c$ and exponent $n$. -\[ -\begin{array}{|c|c|c|c|} - \hline - &\mathbb{Z} & \mathbb{Q} & \mathbb{R} \\ - \hline - c &\mathtt{Z} & \mathtt{Q} & \{R1, R0\} \\ - \hline - n &\mathtt{Z} & \mathtt{Z} & \mathtt{nat}\\ - \hline -\end{array} -\] + arbitrary proposition. + % + For {\tt Q}, equality is not leibnitz equality {\tt =} but the equality of rationals {\tt ==}. + +For {\tt Z} (resp. {\tt Q} ), $c$ ranges over integer constants (resp. rational constants). +%% The following table details for each domain $D \in \{\mathbb{Z},\mathbb{Q},\mathbb{R}\}$ the range of constants $c$ and exponent $n$. +%% \[ +%% \begin{array}{|c|c|c|c|} +%% \hline +%% &\mathbb{Z} & \mathbb{Q} & \mathbb{R} \\ +%% \hline +%% c &\mathtt{Z} & \mathtt{Q} & (see below) \\ +%% \hline +%% n &\mathtt{Z} & \mathtt{Z} & \mathtt{nat}\\ +%% \hline +%% \end{array} +%% \] +For {\tt R}, the tactic recognises as real constants the following expressions: +\begin{verbatim} +c ::= R0 | R1 | Rmul(c,c) | Rplus(c,c) | Rminus(c,c) | IZR z | IQR q | Rdiv(c,c) | Rinv c +\end{verbatim} +where ${\tt z}$ is a constant in {\tt Z} and {\tt q} is a constant in {\tt Q}. +This includes integer constants written using the decimal notation \emph{i.e.,} {\tt c\%R}. \asection{\emph{Positivstellensatz} refutations} \label{sec:psatz-back} @@ -87,6 +86,26 @@ For each conjunct $C_i$, the tactic calls a oracle which searches for $-1$ withi Upon success, the oracle returns a \emph{cone expression} that is normalised by the {\tt ring} tactic (see chapter~\ref{ring}) and checked to be $-1$. + +\asection{{\tt lra} : a decision procedure for linear real and rational arithmetic} +\label{sec:lra} +The {\tt lra} tactic is searching for \emph{linear} refutations using +Fourier elimination\footnote{More efficient linear programming techniques could equally be employed}. As a +result, this tactic explores a subset of the $Cone$ defined as: +\[ +LinCone(S) =\left\{ \left. \sum_{p \in S} \alpha_p \times p\ \right|\ \alpha_p \mbox{ are positive constants} \right\} +\] +The deductive power of {\tt lra} is the combined deductive power of {\tt ring\_simplify} and {\tt fourier}. +% +There is also an overlap with the {\tt field} tactic {\emph e.g.}, {\tt x = 10 * x / 10} is solved by {\tt lra}. + +\asection{ {\tt psatz} : a proof procedure for non-linear arithmetic} +\label{sec:psatz} +The {\tt psatz} tactic explores the $Cone$ by increasing degrees -- hence the depth parameter $n$. +In theory, such a proof search is complete -- if the goal is provable the search eventually stops. +Unfortunately, the external oracle is using numeric (approximate) optimisation techniques that might miss a +refutation. + To illustrate the working of the tactic, consider we wish to prove the following Coq goal.\\ \begin{coq_eval} Require Import ZArith Psatz. @@ -104,30 +123,21 @@ expression belongs to $Cone(\{-x^2, x -1\})$. Moreover, by running {\tt ring} w Theorem~\ref{thm:psatz}, the goal is valid. % -\paragraph{The {\tt psatzl} tactic} is searching for \emph{linear} refutations using a fourier -elimination\footnote{More efficient linear programming techniques could equally be employed}. -As a result, this tactic explore a subset of the $Cone$ defined as: -\[ -LinCone(S) =\left\{ \left. \sum_{p \in S} \alpha_p \times p\ \right|\ \alpha_p \mbox{ are positive constants} \right\} -\] -Basically, the deductive power of {\tt psatzl} is the combined deductive power of {\tt ring\_simplify} and {\tt fourier}. - -\paragraph{The {\tt psatz} tactic} explores the $Cone$ by increasing degrees -- hence the depth parameter $n$. -In theory, such a proof search is complete -- if the goal is provable the search eventually stops. -Unfortunately, the external oracle is using numeric (approximate) optimisation techniques that might miss a -refutation. - %% \paragraph{The {\tt sos} tactic} -- where {\tt sos} stands for \emph{sum of squares} -- tries to prove that a %% single polynomial $p$ is positive by expressing it as a sum of squares \emph{i.e.,} $\sum_{i\in S} p_i^2$. %% This amounts to searching for $p$ in the cone without generators \emph{i.e.}, $Cone(\{\})$. % -\asection{ {\tt lia} : the linear integer arithmetic tactic } +\asection{ {\tt lia} : a tactic for linear integer arithmetic } \tacindex{lia} \label{sec:lia} The tactic {\tt lia} offers an alternative to the {\tt omega} and {\tt romega} tactic (see -Chapter~\ref{OmegaChapter}). It solves goals that {\tt omega} and {\tt romega} do not solve, such as the +Chapter~\ref{OmegaChapter}). +% +Rougthly speaking, the deductive power of {\tt lia} is the combined deductive power of {\tt ring\_simplify} and {\tt omega}. +% +However, it solves linear goals that {\tt omega} and {\tt romega} do not solve, such as the following so-called \emph{omega nightmare}~\cite{TheOmegaPaper}. \begin{coq_example*} Goal forall x y, @@ -153,7 +163,7 @@ The canonical exemple is {\tt 2 * x = 1 -> False} which is a theorem of $\mathbb To remedy this weakness, the {\tt lia} tactic is using recursively a combination of: % \begin{itemize} -\item linear \emph{positivstellensatz} refutations \emph{i.e.}, {\tt psatzl Z}; +\item linear \emph{positivstellensatz} refutations; \item cutting plane proofs; \item case split. \end{itemize} @@ -189,7 +199,21 @@ Our current oracle tries to find an expression $e$ with a small range $[c_1,c_2] We generate $c_2 - c_1$ subgoals which contexts are enriched with an equation $e = i$ for $i \in [c_1,c_2]$ and recursively search for a proof. -% This technique is used to solve so-called \emph{Omega nightmare} +\asection{ {\tt nia} : a proof procedure for non-linear integer arithmetic} +\tacindex{nia} +\label{sec:nia} +The {\tt nia} tactic is an {\emph experimental} proof procedure for non-linear integer arithmetic. +% +The tactic performs a limited amount of non-linear reasoning before running the +linear prover of {\tt lia}. +This pre-processing does the following: +\begin{itemize} +\item If the context contains an arithmetic expression of the form $e[x^2]$ where $x$ is a + monomial, the context is enriched with $x^2\ge 0$; +\item For all pairs of hypotheses $e_1\ge 0$, $e_2 \ge 0$, the context is enriched with $e_1 \times e_2 \ge 0$. +\end{itemize} +After pre-processing, the linear prover of {\tt lia} is searching for a proof by abstracting monomials by variables. + %%% Local Variables: diff --git a/doc/refman/Nsatz.tex b/doc/refman/Nsatz.tex index 794e461f..3ecc7e65 100644 --- a/doc/refman/Nsatz.tex +++ b/doc/refman/Nsatz.tex @@ -54,19 +54,17 @@ performed using {\em Type Classes} (see \ref{typeclasses}) . -The \texttt{Nsatz} module defines the generic tactic -\texttt{nsatz}, which uses the low-level tactic \texttt{nsatz\_domainpv}: \\ +The \texttt{Nsatz} module defines the tactic +\texttt{nsatz}, which can be used without arguments: \\ \vspace*{3mm} -\texttt{nsatz\_domainpv pretac rmax strategy lparam lvar simpltac domain} - +\texttt{nsatz}\\ +or with the syntax: \\ +\vspace*{3mm} +\texttt{nsatz with radicalmax:={\em number}\%N strategy:={\em number}\%Z parameters:={\em list of variables} variables:={\em list of variables}}\\ where: \begin{itemize} - \item \texttt{pretac} is a tactic depending on the ring A; its goal is to -make apparent the generic operations of a domain (ring\_eq, ring\_plus, etc), -both in the goal and the hypotheses; it is executed first. By default it is \texttt{ltac:idtac}. - - \item \texttt{rmax} is a bound when for searching r s.t.$c (P-Q)^r = + \item \texttt{radicalmax} is a bound when for searching r s.t.$c (P-Q)^r = \sum_{i=1..s} S_i (P_i - Q_i)$ \item \texttt{strategy} gives the order on variables $X_1,...X_n$ and @@ -80,7 +78,7 @@ the strategy used in Buchberger algorithm (see \item strategy = 3: pure lexicographic order and sugar strategy. \end{itemize} - \item \texttt{lparam} is the list of variables + \item \texttt{parameters} is the list of variables $X_{i_1},\ldots,X_{i_k}$ among $X_1,...,X_n$ which are considered as parameters: computation will be performed with rational fractions in these variables, i.e. polynomials are considered with coefficients in @@ -88,21 +86,14 @@ $R(X_{i_1},\ldots,X_{i_k})$. In this case, the coefficient $c$ can be a non constant polynomial in $X_{i_1},\ldots,X_{i_k}$, and the tactic produces a goal which states that $c$ is not zero. - \item \texttt{lvar} is the list of the variables -in the decreasing order in which they will be used in Buchberger algorithm. If \texttt{lvar} = {(@nil + \item \texttt{variables} is the list of the variables +in the decreasing order in which they will be used in Buchberger algorithm. If \texttt{variables} = {(@nil R)}, then \texttt{lvar} is replaced by all the variables which are not in -lparam. - - \item \texttt{simpltac} is a tactic depending on the ring A; its goal is to -simplify goals and make apparent the generic operations of a domain after -simplifications. By default it is \texttt{ltac:simpl}. - - \item \texttt{domain} is the object of type Domain representing A, its -operations and properties of integral domain. +parameters. \end{itemize} -See file \texttt{Nsatz.v} for examples. +See file \texttt{Nsatz.v} for many examples, specially in geometry. %%% Local Variables: %%% mode: latex diff --git a/doc/refman/Program.tex b/doc/refman/Program.tex index b41014ab..96073d71 100644 --- a/doc/refman/Program.tex +++ b/doc/refman/Program.tex @@ -3,11 +3,7 @@ \aauthor{Matthieu Sozeau} \index{Program} -\begin{flushleft} - \em The status of \Program\ is experimental. -\end{flushleft} - -We present here the new \Program\ tactic commands, used to build certified +We present here the \Program\ tactic commands, used to build certified \Coq\ programs, elaborating them from their algorithmic skeleton and a rich specification \cite{Sozeau06}. It can be sought of as a dual of extraction (see Chapter~\ref{Extraction}). The goal of \Program~is to program as in a regular @@ -73,6 +69,8 @@ will be first rewrote to: works with the previous mechanism. \end{itemize} +\subsection{Syntactic control over equalities} +\label{ProgramSyntax} To give more control over the generation of equalities, the typechecker will fall back directly to \Coq's usual typing of dependent pattern-matching if a {\tt return} or {\tt in} clause is specified. Likewise, @@ -89,9 +87,18 @@ Program Definition id (n : nat) : { x : nat | x = n } := else S (pred n). \end{coq_example} -Finally, the let tupling construct {\tt let (x1, ..., xn) := t in b} +The let tupling construct {\tt let (x1, ..., xn) := t in b} does not produce an equality, contrary to the let pattern construct {\tt let '(x1, ..., xn) := t in b}. +Also, {\tt {\term}:>} explicitly asks the system to coerce {\tt \term} to its +support type. It can be useful in notations, for example: +\begin{coq_example} +Notation " x `= y " := (@eq _ (x :>) (y :>)) (only parsing). +\end{coq_example} + +This notation denotes equality on subset types using equality on their +support types, avoiding uses of proof-irrelevance that would come up +when reasoning with equality on the subset types themselves. The next two commands are similar to their standard counterparts Definition (see Section~\ref{Basic-definitions}) and Fixpoint (see Section~\ref{Fixpoint}) in that diff --git a/doc/refman/RefMan-add.tex b/doc/refman/RefMan-add.tex index 9d7ca7b1..2094c9d2 100644 --- a/doc/refman/RefMan-add.tex +++ b/doc/refman/RefMan-add.tex @@ -51,8 +51,6 @@ can be found in the document {\tt Polynom.dvi} %anomalous behavior, please check first whether it has been already %reported in this document. -% $Id: RefMan-add.tex 10061 2007-08-08 13:14:05Z msozeau $ - %%% Local Variables: %%% mode: latex diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex index dab164e7..9660a04b 100644 --- a/doc/refman/RefMan-cic.tex +++ b/doc/refman/RefMan-cic.tex @@ -1706,8 +1706,6 @@ impredicative system for sort \Set{} become~: -% $Id: RefMan-cic.tex 13029 2010-05-28 11:49:12Z herbelin $ - %%% Local Variables: %%% mode: latex %%% TeX-master: "Reference-Manual" diff --git a/doc/refman/RefMan-coi.tex b/doc/refman/RefMan-coi.tex index b0f0212e..619a8ee1 100644 --- a/doc/refman/RefMan-coi.tex +++ b/doc/refman/RefMan-coi.tex @@ -403,4 +403,3 @@ See \cite{Gimenez95b} for a complete description about this development. %\end{document} -% $Id: RefMan-coi.tex 10421 2008-01-05 14:06:51Z herbelin $ diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex index 13a4219a..a40c210e 100644 --- a/doc/refman/RefMan-com.tex +++ b/doc/refman/RefMan-com.tex @@ -34,11 +34,6 @@ toplevel (to allow the dynamic link of tactics). You can switch to the Caml toplevel with the command \verb!Drop.!, and come back to the \Coq~toplevel with the command \verb!Toplevel.loop();;!. -% The command \verb!coqtop -searchisos! runs the search tool {\sf -% Coq\_SearchIsos} (see Section~\ref{coqsearchisos}, -% page~\pageref{coqsearchisos}) and, as the \Coq~system, can be combined -% with the option \verb!-opt!. - \section{Batch compilation ({\tt coqc})} The {\tt coqc} command takes a name {\em file} as argument. Then it looks for a vernacular file named {\em file}{\tt .v}, and tries to @@ -58,12 +53,15 @@ native-code versions of the system. \section[Resource file]{Resource file\index{Resource file}} When \Coq\ is launched, with either {\tt coqtop} or {\tt coqc}, the -resource file \verb:$HOME/.coqrc.7.0: is loaded, where \verb:$HOME: is -the home directory of the user. If this file is not found, then the -file \verb:$HOME/.coqrc: is searched. You can also specify an +resource file \verb:$XDG_CONFIG_HOME/coq/coqrc.xxx: is loaded, where +\verb:$XDG_CONFIG_HOME: is the configuration directory of the user (by +default its home directory \verb!/.config! and \verb:xxx: is the version +number (e.g. 8.3). If this file is not found, then the file +\verb:$XDG_CONFIG_HOME/coqrc: is searched. You can also specify an arbitrary name for the resource file (see option \verb:-init-file: -below), or the name of another user to load the resource file of -someone else (see option \verb:-user:). +below), or the name of another user to load the resource file of someone +else (see option \verb:-user:). + This file may contain, for instance, \verb:Add LoadPath: commands to add directories to the load path of \Coq. @@ -73,9 +71,11 @@ option \verb:-q:. \section[Environment variables]{Environment variables\label{EnvVariables} \index{Environment variables}} -There are three environment variables used by the \Coq\ system. +There are four environment variables used by the \Coq\ system. \verb:$COQBIN: for the directory where the binaries are, -\verb:$COQLIB: for the directory where the standard library is, and +\verb:$COQLIB: for the directory where the standard library is, +\verb:$COQPATH: for a list of directories seperated by \verb|:| +(\verb|;| on windows) to add to the load path, and \verb:$COQTOP: for the directory of the sources. The latter is useful only for developers that are writing their own tactics and are using \texttt{coq\_makefile} (see \ref{Makefile}). If \verb:$COQBIN: or @@ -83,6 +83,11 @@ only for developers that are writing their own tactics and are using (defined at installation time). So these variables are useful only if you move the \Coq\ binaries and library after installation. +Coq will also honor \verb:$XDG_DATA_HOME: and \verb:$XDG_DATA_DIRS: (see +\url{http://standards.freedesktop.org/basedir-spec/basedir-spec-latest.html}). +Coq adds \verb:${XDG_DATA_HOME}/coq: and \verb:${XDG_DATA_DIRS}/coq: to its +search path. + \section[Options]{Options\index{Options of the command line} \label{vmoption} \label{coqoptions}} @@ -173,11 +178,6 @@ The following command-line options are recognized by the commands {\tt Cause \Coq~not to load the resource file. -\item[{\tt -user} {\em username}]\ - - Take resource file of user {\em username} (that is - \verb+~+{\em username}{\tt /.coqrc.7.0}) instead of yours. - \item[{\tt -load-ml-source} {\em file}]\ Load the Caml source file {\em file}. @@ -263,9 +263,25 @@ The following command-line options are recognized by the commands {\tt \item[{\tt -dont-load-proofs}]\ - This avoids loading in memory the proofs of opaque theorems - resulting in a smaller memory requirement and faster compilation; - warning: this invalidates some features such as the extraction tool. + Warning: this is an unsafe mode. + Instead of loading in memory the proofs of opaque theorems, they are + treated as axioms. This results in smaller memory requirement and + faster compilation, but the behavior of the system might slightly change + (for instance during module subtyping), and some features won't be + available (for example {\tt Print Assumptions}). + +\item[{\tt -lazy-load-proofs}]\ + + This is the default behavior. Proofs of opaque theorems aren't + loaded immediately in memory, but only when necessary, for instance + during some module subtyping or {\tt Print Assumptions}. This should be + almost as fast and efficient as {\tt -dont-load-proofs}, with none + of its drawbacks. + +\item[{\tt -force-load-proofs}]\ + + Proofs of opaque theorems are loaded in memory as soon as the + corresponding {\tt Require} is done. This used to be Coq's default behavior. \item[{\tt -vm}]\ @@ -376,8 +392,6 @@ makes more disk access. It is also less secure since an attacker might have replaced the compiled library $A$ after it has been read by the first command, but before it has been read by the second command. -% $Id: RefMan-com.tex 12443 2009-10-29 16:17:29Z gmelquio $ - %%% Local Variables: %%% mode: latex %%% TeX-master: "Reference-Manual" diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex index c0e578fe..2da5bec1 100644 --- a/doc/refman/RefMan-ext.tex +++ b/doc/refman/RefMan-ext.tex @@ -200,6 +200,20 @@ Definition b := {| x := 5; y := 3 |}. Definition c := {| y := 3; x := 5 |}. \end{coq_example} +This syntax can be disabled globally for printing by +\begin{quote} +{\tt Unset Printing Records.} +\end{quote} +For a given type, one can override this using either +\begin{quote} +{\tt Add Printing Record {\ident}.} +\end{quote} +to get record syntax or +\begin{quote} +{\tt Add Printing Constructor {\ident}.} +\end{quote} +to get constructor syntax. + This syntax can also be used for pattern matching. \begin{coq_example} @@ -675,7 +689,15 @@ Function plus (n m : nat) {struct n} : nat := \paragraph[Limitations]{Limitations\label{sec:Function-limitations}} \term$_0$ must be build as a \emph{pure pattern-matching tree} (\texttt{match...with}) with applications only \emph{at the end} of -each branch. For now dependent cases are not treated. +each branch. + +Function does not support partial application of the function being defined. Thus, the following example cannot be accepted due to the presence of partial application of \ident{wrong} into the body of \ident{wrong}~: +\begin{coq_example*} + Function wrong (C:nat) {\ldots} : nat := + List.hd(List.map wrong (C::nil)). +\end{coq_example*} + +For now dependent cases are not treated for non structurally terminating functions. @@ -1119,14 +1141,14 @@ possible, the correct argument will be automatically generated. \end{ErrMsgs} \subsection{Declaration of implicit arguments for a constant -\comindex{Implicit Arguments}} +\comindex{Arguments}} \label{ImplicitArguments} In case one wants that some arguments of a given object (constant, inductive types, constructors, assumptions, local or not) are always inferred by Coq, one may declare once and for all which are the expected implicit arguments of this object. There are two ways to do this, -a-priori and a-posteriori. +a priori and a posteriori. \subsubsection{Implicit Argument Binders} @@ -1166,44 +1188,44 @@ Print list. One can always specify the parameter if it is not uniform using the usual implicit arguments disambiguation syntax. -\subsubsection{The Implicit Arguments Vernacular Command} +\subsubsection{Declaring Implicit Arguments} -To set implicit arguments for a constant a-posteriori, one can use the +To set implicit arguments for a constant a posteriori, one can use the command: \begin{quote} -\tt Implicit Arguments {\qualid} [ \nelist{\possiblybracketedident}{} ] +\tt Arguments {\qualid} \nelist{\possiblybracketedident}{} \end{quote} -where the list of {\possiblybracketedident} is the list of parameters -to be declared implicit, each of the identifier of the list being -optionally surrounded by square brackets, then meaning that this -parameter has to be maximally inserted. +where the list of {\possiblybracketedident} is the list of all arguments of +{\qualid} where the ones to be declared implicit are surrounded by +square brackets and the ones to be declared as maximally inserted implicits +are surrounded by curly braces. After the above declaration is issued, implicit arguments can just (and have to) be skipped in any expression involving an application of {\qualid}. \begin{Variants} -\item {\tt Global Implicit Arguments {\qualid} [ \nelist{\possiblybracketedident}{} ] -\comindex{Global Implicit Arguments}} +\item {\tt Global Arguments {\qualid} \nelist{\possiblybracketedident}{} +\comindex{Global Arguments}} -Tells to recompute the implicit arguments of {\qualid} after ending of +Tell to recompute the implicit arguments of {\qualid} after ending of the current section if any, enforcing the implicit arguments known from inside the section to be the ones declared by the command. -\item {\tt Local Implicit Arguments {\qualid} [ \nelist{\possiblybracketedident}{} ] -\comindex{Local Implicit Arguments}} +\item {\tt Local Arguments {\qualid} \nelist{\possiblybracketedident}{} +\comindex{Local Arguments}} -When in a module, tells not to activate the implicit arguments of -{\qualid} declared by this commands to contexts that requires the +When in a module, tell not to activate the implicit arguments of +{\qualid} declared by this command to contexts that require the module. -\item {\tt \zeroone{Global {\sl |} Local} Implicit Arguments {\qualid} \sequence{[ \nelist{\possiblybracketedident}{} ]}{}} +\item {\tt \zeroone{Global {\sl |} Local} Arguments {\qualid} \sequence{\nelist{\possiblybracketedident}{}}{,}} For names of constants, inductive types, constructors, lemmas which can only be applied to a fixed number of arguments (this excludes for -instance constants whose type is polymorphic), multiple lists -of implicit arguments can be given. These lists must be of different -length, and, depending on the number of arguments {\qualid} is applied +instance constants whose type is polymorphic), multiple +implicit arguments decflarations can be given. +Depending on the number of arguments {\qualid} is applied to in practice, the longest applicable list of implicit arguments is used to select which implicit arguments are inserted. @@ -1223,17 +1245,17 @@ Inductive list (A:Type) : Type := \end{coq_example*} \begin{coq_example} Check (cons nat 3 (nil nat)). -Implicit Arguments cons [A]. -Implicit Arguments nil [A]. +Arguments cons [A] _ _. +Arguments nil [A]. Check (cons 3 nil). Fixpoint map (A B:Type) (f:A->B) (l:list A) : list B := match l with nil => nil | cons a t => cons (f a) (map A B f t) end. Fixpoint length (A:Type) (l:list A) : nat := match l with nil => 0 | cons _ m => S (length A m) end. -Implicit Arguments map [A B]. -Implicit Arguments length [[A]]. (* A has to be maximally inserted *) +Arguments map [A B] f l. +Arguments length {A} l. (* A has to be maximally inserted *) Check (fun l:list (list nat) => map length l). -Implicit Arguments map [A B] [A] []. +Arguments map [A B] f l, [A] B f l, A B f l. Check (fun l => map length l = map (list nat) nat length l). \end{coq_example} @@ -1248,8 +1270,8 @@ implicit arguments of {\qualid}. {\Coq} can also automatically detect what are the implicit arguments of a defined object. The command is just \begin{quote} -{\tt Implicit Arguments {\qualid} -\comindex{Implicit Arguments}} +{\tt Arguments {\qualid} : default implicits +\comindex{Arguments}} \end{quote} The auto-detection is governed by options telling if strict, contextual, or reversible-pattern implicit arguments must be @@ -1258,16 +1280,16 @@ Sections~\ref{SetStrictImplicit},~\ref{SetContextualImplicit},~\ref{SetReversibl and also~\ref{SetMaximalImplicitInsertion}). \begin{Variants} -\item {\tt Global Implicit Arguments {\qualid} -\comindex{Global Implicit Arguments}} +\item {\tt Global Arguments {\qualid} : default implicits +\comindex{Global Arguments}} -Tells to recompute the implicit arguments of {\qualid} after ending of +Tell to recompute the implicit arguments of {\qualid} after ending of the current section if any. -\item {\tt Local Implicit Arguments {\qualid} -\comindex{Local Implicit Arguments}} +\item {\tt Local Arguments {\qualid} : default implicits +\comindex{Local Arguments}} -When in a module, tells not to activate the implicit arguments of +When in a module, tell not to activate the implicit arguments of {\qualid} computed by this declaration to contexts that requires the module. @@ -1283,12 +1305,12 @@ Inductive list (A:Set) : Set := | cons : A -> list A -> list A. \end{coq_example*} \begin{coq_example} -Implicit Arguments cons. +Arguments cons : default implicits. Print Implicit cons. -Implicit Arguments nil. +Arguments nil : default implicits. Print Implicit nil. Set Contextual Implicit. -Implicit Arguments nil. +Arguments nil : default implicits. Print Implicit nil. \end{coq_example} @@ -1304,7 +1326,7 @@ Definition Relation := X -> X -> Prop. Definition Transitivity (R:Relation) := forall x y:X, R x y -> forall z:X, R y z -> R x z. Variables (R : Relation) (p : Transitivity R). -Implicit Arguments p. +Arguments p : default implicits. \end{coq_example*} \begin{coq_example} Print p. @@ -1317,6 +1339,21 @@ Variables (a b c : X) (r1 : R a b) (r2 : R b c). Check (p r1 r2). \end{coq_example} +Implicit arguments can be cleared with the following syntax: + +\begin{quote} +{\tt Arguments {\qualid} : clear implicits +\comindex{Arguments}} +\end{quote} + +In the following example implict arguments declarations for the {\tt nil} +constant are cleared: +\begin{coq_example} +Arguments cons : clear implicits. +Print Implicit cons. +\end{coq_example} + + \subsection{Mode for automatic declaration of implicit arguments \label{Auto-implicit} \comindex{Set Implicit Arguments} @@ -1410,7 +1447,7 @@ Implicit Insertion}. \subsection{Explicit applications \index{Explicitly given implicit arguments} \label{Implicits-explicitation} -\index{qualid@{\qualid}}} +\index{qualid@{\qualid}} \index{\symbol{64}}} In presence of non strict or contextual argument, or in presence of partial applications, the synthesis of implicit arguments may fail, so @@ -1442,6 +1479,28 @@ Check (p r1 (z:=c)). Check (p (x:=a) (y:=b) r1 (z:=c) r2). \end{coq_example} +\subsection{Renaming implicit arguments +\comindex{Arguments} +} + +Implicit arguments names can be redefined using the following syntax: +\begin{quote} +{\tt Arguments {\qualid} \nelist{\name}{} : rename} +\end{quote} + +Without the {\tt rename} flag, {\tt Arguments} can be used to assert +that a given constant has the expected number of arguments and that +these arguments are named as expected. + +\noindent {\bf Example (continued): } +\begin{coq_example} +Arguments p [s t] _ [u] _: rename. +Check (p r1 (u:=c)). +Check (p (s:=a) (t:=b) r1 (u:=c) r2). +Fail Arguments p [s t] _ [w] _. +\end{coq_example} + + \subsection{Displaying what the implicit arguments are \comindex{Print Implicit} \label{PrintImplicit}} @@ -1622,7 +1681,7 @@ the generalized variables. Inside implicit generalization delimiters, free variables in the current context are automatically quantified using a product or a lambda abstraction to generate a closed term. In the following statement for example, the variables \texttt{n} -and \texttt{m} are automatically generalized and become explicit +and \texttt{m} are autamatically generalized and become explicit arguments of the lemma as we are using \verb|`( )|: \begin{coq_example} @@ -1638,7 +1697,7 @@ generalizations when mistyping identifiers. There are three variants of the command: \begin{quote} -{\tt (Global)? Generalizable (All|No) Variable(s)? ({\ident$_1$ \ident$_n$})?.} +{\tt Generalizable (All|No) Variable(s)? ({\ident$_1$ \ident$_n$})?.} \end{quote} \begin{Variants} @@ -1742,13 +1801,25 @@ of the occurrences of {\Type}, use \end{quote} \comindex{Print Universes} +\comindex{Print Sorted Universes} The constraints on the internal level of the occurrences of {\Type} (see Section~\ref{Sorts}) can be printed using the command \begin{quote} -{\tt Print Universes.} +{\tt Print \zeroone{Sorted} Universes.} \end{quote} +If the optional {\tt Sorted} option is given, each universe will be +made equivalent to a numbered label reflecting its level (with a +linear ordering) in the universe hierarchy. +This command also accepts an optional output filename: +\begin{quote} +\tt Print \zeroone{Sorted} Universes {\str}. +\end{quote} +If {\str} ends in \texttt{.dot} or \texttt{.gv}, the constraints are +printed in the DOT language, and can be processed by Graphviz +tools. The format is unspecified if {\str} doesn't end in +\texttt{.dot} or \texttt{.gv}. %%% Local Variables: %%% mode: latex diff --git a/doc/refman/RefMan-gal.tex b/doc/refman/RefMan-gal.tex index d1489591..204fa90d 100644 --- a/doc/refman/RefMan-gal.tex +++ b/doc/refman/RefMan-gal.tex @@ -217,12 +217,12 @@ possible one (among all tokens defined at this moment), and so on. \subsection{Syntax of terms} -Figures \ref{term-syntax} and \ref{term-syntax-aux} describe the basic -set of terms which form the {\em Calculus of Inductive Constructions} -(also called \CIC). The formal presentation of {\CIC} is given in -Chapter \ref{Cic}. Extensions of this syntax are given in chapter -\ref{Gallina-extension}. How to customize the syntax is described in -Chapter \ref{Addoc-syntax}. +Figures \ref{term-syntax} and \ref{term-syntax-aux} describe the basic syntax of +the terms of the {\em Calculus of Inductive Constructions} (also +called \CIC). The formal presentation of {\CIC} is given in Chapter +\ref{Cic}. Extensions of this syntax are given in chapter +\ref{Gallina-extension}. How to customize the syntax is described in Chapter +\ref{Addoc-syntax}. \begin{figure}[htbp] \begin{centerframe} @@ -240,9 +240,13 @@ Chapter \ref{Addoc-syntax}. & $|$ & {\tt let} {\tt (} \sequence{\name}{,} {\tt )} \zeroone{\ifitem} {\tt :=} {\term} {\tt in} {\term} &(\ref{caseanalysis}, \ref{Mult-match})\\ + & $|$ & {\tt let '} {\pattern} \zeroone{{\tt in} {\term}} {\tt :=} {\term} + \zeroone{\returntype} {\tt in} {\term} & (\ref{caseanalysis}, \ref{Mult-match})\\ & $|$ & {\tt if} {\term} \zeroone{\ifitem} {\tt then} {\term} {\tt else} {\term} &(\ref{caseanalysis}, \ref{Mult-match})\\ & $|$ & {\term} {\tt :} {\term} &(\ref{typecast})\\ + & $|$ & {\term} {\tt <:} {\term} &(\ref{typecast})\\ + & $|$ & {\term} {\tt :>} &(\ref{ProgramSyntax})\\ & $|$ & {\term} {\tt ->} {\term} &(\ref{products})\\ & $|$ & {\term} \nelist{\termarg}{}&(\ref{applications})\\ & $|$ & {\tt @} {\qualid} \sequence{\term}{} @@ -256,6 +260,7 @@ Chapter \ref{Addoc-syntax}. & $|$ & {\sort} &(\ref{Gallina-sorts})\\ & $|$ & {\num} &(\ref{numerals})\\ & $|$ & {\_} &(\ref{hole})\\ + & $|$ & {\tt (} {\term} {\tt )} & \\ & & &\\ {\termarg} & ::= & {\term} &\\ & $|$ & {\tt (} {\ident} {\tt :=} {\term} {\tt )} @@ -496,6 +501,10 @@ arguments is used for making explicit the value of implicit arguments The expression ``{\term}~{\tt :}~{\type}'' is a type cast expression. It enforces the type of {\term} to be {\type}. +``{\term}~{\tt <:}~{\type}'' locally sets up the virtual machine (as if option +{\tt Virtual Machine} were on, see \ref{SetVirtualMachine}) for checking that +{\term} has type {\type}. + \subsection{Inferable subterms \label{hole} \index{\_}} diff --git a/doc/refman/RefMan-ide.tex b/doc/refman/RefMan-ide.tex index 5d9c8c16..f061ef18 100644 --- a/doc/refman/RefMan-ide.tex +++ b/doc/refman/RefMan-ide.tex @@ -261,32 +261,26 @@ CONTROL and the SHIFT keys, and type the hexadecimal code of the symbol required, for example \verb|2200| for the $\forall$ symbol. A list of symbol codes is available at \url{http://www.unicode.org}. -This method obviously doesn't scale, that's why the preferred -alternative is to use an Input Method Editor. On POSIX systems (Linux -distributions, BSD variants and MacOS X), you can use \texttt{uim} to -support \LaTeX{}-style edition and, if using X Windows, you can also use -the XCompose method (XIM). How to use \texttt{uim} is documented below. - -If you have \texttt{uim} 1.5.x, first manually copy the files located -in directory {\tt ide/uim} of the Coq source distribution to the -{\tt uim} directory of input methods which typically is {\tt - /usr/share/uim}. Execute {\tt uim-module-manager -{-}register - coqide}. Then, execute \texttt{uim-pref-gtk} as regular user and set -the default Input Method to "CoqIDE" in the "Global Settings" group -(don't forget to tick the checkbox "Specify default IM"; you may also -have to first edit the set of "Enabled input method" to add CoqIDE to -the set). You can now execute CoqIDE with the following commands -(assuming you use a Bourne-style shell): +This method obviously doesn't scale, that's why the preferred alternative is to +use an Input Method Editor. On POSIX systems (Linux distros, BSD variants and +MacOS X), you can use \texttt{uim} version 1.6 or later which provides a \LaTeX{}-style +input method. + +To configure \texttt{uim}, execute \texttt{uim-pref-gtk} as your regular user. +In the "Global Settings" group set the default Input Method to "ELatin" (don't +forget to tick the checkbox "Specify default IM"). In the "ELatin" group set the +layout to "TeX", and remember the content of the "[ELatin] on" field (by default +"<Control>\textbackslash"). You can now execute CoqIDE with the following commands (assuming +you use a Bourne-style shell): \begin{verbatim} $ export GTK_IM_MODULE=uim $ coqide \end{verbatim} -If you then type the sequence "\verb=\Gamma=", you will see the sequence being -replaced by $\Gamma$ as soon as you type the second "a". - -If you have \texttt{uim} 1.6.x, the \LaTeX{} input method is built-in. You just have to execute \texttt{uim-pref-gtk} and choose "ELatin" as default Input Method in the "Global Settings". Then, in the "ELatin" group set the layout to "TeX", and remember the content of the "[ELatin] on" field (by default "<Control>$\backslash$"). Proceed then as above. +Activate the ELatin Input Method with Ctrl-\textbackslash, then type the +sequence "\verb=\Gamma=". You will see the sequence being +replaced by $\Gamma$ as soon as you type the second "a". \subsection[Character encoding for saved files]{Character encoding for saved files\label{sec:coqidecharencoding}} @@ -305,23 +299,6 @@ each dot is an hexadecimal digit: the number between braces is the hexadecimal UNICODE index for the missing character. -\section{Building a custom \CoqIDE{} with user \textsc{ML} code} - -You can do this as described in Section~\ref{Coqmktop} for a -custom coq text toplevel, simply by adding -option \verb|-ide| to \verb|coqmktop|, that is something like -\begin{quote} -\texttt{coqmktop -ide -byte $m_1$.cmo \ldots{} $m_n$.cmo} -\end{quote} -or -\begin{quote} -\texttt{coqmktop -ide -opt $m_1$.cmx \ldots{} $m_n$.cmx} -\end{quote} - - - -% $Id: RefMan-ide.tex 13701 2010-12-10 07:48:30Z herbelin $ - %%% Local Variables: %%% mode: latex %%% TeX-master: "Reference-Manual" diff --git a/doc/refman/RefMan-ind.tex b/doc/refman/RefMan-ind.tex index af4257ca..95944240 100644 --- a/doc/refman/RefMan-ind.tex +++ b/doc/refman/RefMan-ind.tex @@ -508,4 +508,3 @@ Check tree_forest_mutind. %\end{document} -% $Id: RefMan-ind.tex 10421 2008-01-05 14:06:51Z herbelin $ diff --git a/doc/refman/RefMan-int.tex b/doc/refman/RefMan-int.tex index 7b531409..6d2c37f7 100644 --- a/doc/refman/RefMan-int.tex +++ b/doc/refman/RefMan-int.tex @@ -140,8 +140,6 @@ 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" diff --git a/doc/refman/RefMan-lib.tex b/doc/refman/RefMan-lib.tex index 2c8abc88..31c6fef4 100644 --- a/doc/refman/RefMan-lib.tex +++ b/doc/refman/RefMan-lib.tex @@ -809,7 +809,8 @@ subdirectories: \begin{tabular}{lp{12cm}} {\bf Logic} & Classical logic and dependent equality \\ {\bf Arith} & Basic Peano arithmetic \\ - {\bf NArith} & Basic positive integer arithmetic \\ + {\bf PArith} & Basic positive integer arithmetic \\ + {\bf NArith} & Basic binary natural number arithmetic \\ {\bf ZArith} & Basic relative integer arithmetic \\ {\bf Numbers} & Various approaches to natural, integer and cyclic numbers (currently axiomatically and on top of 2$^{31}$ binary words) \\ {\bf Bool} & Booleans (basic functions and results) \\ @@ -996,7 +997,7 @@ Abort. \end{coq_eval} \item {\tt split\_Rabs} allows to unfold {\tt Rabs} constant and splits -corresponding conjonctions. +corresponding conjunctions. \tacindex{split\_Rabs} \begin{coq_example*} @@ -1094,8 +1095,6 @@ description, etc.) and the possibility to download them one by one. You will also find informations on how to submit a new contribution. -% $Id: RefMan-lib.tex 13091 2010-06-08 13:56:19Z herbelin $ - %%% Local Variables: %%% mode: latex %%% TeX-master: "Reference-Manual" diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex index d8747254..38ad9aa8 100644 --- a/doc/refman/RefMan-ltac.tex +++ b/doc/refman/RefMan-ltac.tex @@ -100,6 +100,7 @@ is understood as & | & {\tt progress} {\tacexprpref}\\ & | & {\tt repeat} {\tacexprpref}\\ & | & {\tt try} {\tacexprpref}\\ +& | & {\tt timeout} {\it (}{\naturalnumber} {\it |} {\ident}{\it )} {\tacexprpref}\\ & | & {\tacexprinf} \\ \\ {\tacexprinf} & ::= & @@ -446,6 +447,28 @@ This is a combination of the previous variants. \ErrMsg \errindex{Tactic Failure {\it message} (level $n$)}. +\subsubsection[Timeout]{Timeout\tacindex{timeout} +\index{Tacticals!timeout@{\tt timeout}}} + +We can force a tactic to stop if it has not finished after a certain +amount of time: +\begin{quote} +{\tt timeout} {\num} {\tacexpr} +\end{quote} +{\tacexpr} is evaluated to $v$. $v$ must be a tactic value. $v$ is +normally applied, except that it is interrupted after ${\num}$ seconds +if it is still running. In this case the outcome is a failure. + +Warning: For the moment, {\tt timeout} is based on elapsed time in +seconds, which is very +machine-dependent: a script that works on a quick machine may fail +on a slow one. The converse is even possible if you combine a +{\tt timeout} with some other tacticals. This tactical is hence +proposed only for convenience during debug or other development +phases, we strongly advise you to not leave any {\tt timeout} in +final scripts. Note also that this tactical isn't available on +the native Windows port of Coq. + \subsubsection[Local definitions]{Local definitions\index{Ltac!let} \index{Ltac!let rec} \index{let!in Ltac} @@ -568,11 +591,10 @@ pattern: \begin{quote} {\tt context} {\ident} {\tt [} {\cpattern} {\tt ]} \end{quote} -It matches any term which one subterm matches {\cpattern}. If there is -a match, the optional {\ident} is assign the ``matched context'', that -is the initial term where the matched subterm is replaced by a -hole. The definition of {\tt context} in expressions below will show -how to use such term contexts. +It matches any term with a subterm matching {\cpattern}. If there is +a match, the optional {\ident} is assigned the ``matched context'', i.e. +the initial term where the matched subterm is replaced by a +hole. The example below will show how to use such term contexts. If the evaluation of the right-hand-side of a valid match fails, the next matching subterm is tried. If no further subterm matches, the @@ -606,7 +628,7 @@ Alternatively, one may now use the following variant of {\tt context}: The behavior of {\tt appcontext} is the same as the one of {\tt context}, except that a matching subterm could be a partial part of a longer application. For instance, in {\tt (f 1 2)}, -an {\tt appcontext [f ?x]} will find the matching subterm {\tt (f 1)}. +an {\tt appcontext [f ?x]} will find the matching subterm {\tt (f 1)}. \end{Variants} diff --git a/doc/refman/RefMan-modr.tex b/doc/refman/RefMan-modr.tex index b2ea232c..9ab8aded 100644 --- a/doc/refman/RefMan-modr.tex +++ b/doc/refman/RefMan-modr.tex @@ -556,8 +556,6 @@ In the rules below we assume $\Gamma_P$ is $[p_1:P_1;\ldots;p_r:P_r]$, % \end{itemize} -% $Id: RefMan-modr.tex 11197 2008-07-01 13:05:41Z soubiran $ - %%% Local Variables: %%% mode: latex %%% TeX-master: "Reference-Manual" diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex index 025788f5..5b1ad198 100644 --- a/doc/refman/RefMan-oth.tex +++ b/doc/refman/RefMan-oth.tex @@ -225,8 +225,7 @@ a subterm that matches the pattern {\termpattern} (holes of the pattern are either denoted by ``{\texttt \_}'' or by ``{\texttt ?{\ident}}'' when non linear patterns are expected). -\item {\tt SearchAbout [ \nelist{\zeroone{-}{\termpatternorstr}}{} -].}\\ +\item {\tt SearchAbout \nelist{\zeroone{-}{\termpatternorstr}}{}.}\\ \noindent where {\termpatternorstr} is a {\termpattern} or a {\str}, or a {\str} followed by a scope @@ -241,25 +240,24 @@ search excludes the objects that mention that {\termpattern} or that {\str}. \item -\begin{tabular}[t]{@{}l} - {\tt SearchAbout {\termpatternorstr} inside {\module$_1$} \ldots{} {\module$_n$}.} \\ - {\tt SearchAbout [ \nelist{{\termpatternorstr}}{} ] + {\tt SearchAbout \nelist{{\termpatternorstr}}{} inside {\module$_1$} \ldots{} {\module$_n$}.} -\end{tabular} This restricts the search to constructions defined in modules {\module$_1$} \ldots{} {\module$_n$}. \item -\begin{tabular}[t]{@{}l} - {\tt SearchAbout {\termpatternorstr} outside {\module$_1$}...{\module$_n$}.} \\ - {\tt SearchAbout [ \nelist{{\termpatternorstr}}{} ] + {\tt SearchAbout \nelist{{\termpatternorstr}}{} outside {\module$_1$}...{\module$_n$}.} -\end{tabular} This restricts the search to constructions not defined in modules {\module$_1$} \ldots{} {\module$_n$}. +\item {\tt SearchAbout [ ... ]. } + +For compatibility with older versions, the list of objects to search +may be enclosed by optional {\tt [ ]} delimiters. + \end{Variants} \examples @@ -268,8 +266,8 @@ This restricts the search to constructions not defined in modules Require Import ZArith. \end{coq_example*} \begin{coq_example} -SearchAbout [ Zmult Zplus "distr" ]. -SearchAbout [ "+"%Z "*"%Z "distr" -positive -Prop]. +SearchAbout Zmult Zplus "distr". +SearchAbout "+"%Z "*"%Z "distr" -positive -Prop. SearchAbout (?x * _ + ?x * _)%Z outside OmegaLemmas. \end{coq_example} @@ -338,16 +336,6 @@ This restricts the search to constructions not defined in modules \end{Variants} -% \subsection[\tt SearchIsos {\term}.]{\tt SearchIsos {\term}.\comindex{SearchIsos}} -% \label{searchisos} -% \texttt{SearchIsos} searches terms by their type modulo isomorphism. -% This command displays the full name of all constants, variables, -% inductive types, and inductive constructors of the current -% context whose type is isomorphic to {\term} modulo the contextual part of the -% following axiomatization (the mutual inductive types with one constructor, -% without implicit arguments, and for which projections exist, are regarded as a -% sequence of $\sa{}$): - % \begin{tabbing} % \ \ \ \ \=11.\ \=\kill @@ -632,6 +620,12 @@ files is only possible under the bytecode version of {\tt coqtop} \ref{Addoc-coqc}), or when Coq has been compiled with a version of Objective Caml that supports native {\tt Dynlink} ($\ge$ 3.11). +\begin{Variants} +\item {\tt Local Declare ML Module {\str$_1$} .. {\str$_n$}.}\\ + This variant is not exported to the modules that import the module + where they occur, even if outside a section. +\end{Variants} + \begin{ErrMsgs} \item \errindex{File not found on loadpath : \str} \item \errindex{Loading of ML object file forbidden in a native Coq} @@ -938,7 +932,7 @@ a {\tt Timeout} are unaffected. \subsection[\tt Unset Default Timeout.]{\tt Unset Default Timeout.\comindex{Unset Default Timeout}} -This command turns off the use of a defaut timeout. +This command turns off the use of a default timeout. \subsection[\tt Test Default Timeout.]{\tt Test Default Timeout.\comindex{Test Default Timeout}} @@ -978,12 +972,6 @@ time of writing this documentation, the default value is 50). \subsection[\tt Test Printing Depth.]{\tt Test Printing Depth.\comindex{Test Printing Depth}} This command displays the current nesting depth used for display. -%\subsection{\tt Explain ...} -%Not yet documented. - -%\subsection{\tt Go ...} -%Not yet documented. - %\subsection{\tt Abstraction ...} %Not yet documented. @@ -997,7 +985,7 @@ compares applicative terms while the other is a brute-force but efficient algorithm that first normalizes the terms before comparing them. The second algorithm is based on a bytecode representation of terms similar to the bytecode representation used in the ZINC virtual -machine~\cite{Leroy90}. It is specially useful for intensive +machine~\cite{Leroy90}. It is especially useful for intensive computation of algebraic values, such as numbers, and for reflexion-based tactics. The commands to fine-tune the reduction strategies and the lazy conversion algorithm are described first. @@ -1188,8 +1176,6 @@ control the scope of their effect. There are four kinds of commands: \end{itemize} -% $Id: RefMan-oth.tex 13923 2011-03-21 16:25:20Z letouzey $ - %%% Local Variables: %%% mode: latex %%% TeX-master: "Reference-Manual" diff --git a/doc/refman/RefMan-pre.tex b/doc/refman/RefMan-pre.tex index a2cdb5ec..29de89d8 100644 --- a/doc/refman/RefMan-pre.tex +++ b/doc/refman/RefMan-pre.tex @@ -673,7 +673,7 @@ Yves Bertot, Jean-Christophe Filliâtre, Pierre Courtieu and Julien Forest acted as maintainers of features they implemented in previous versions of Coq. -Julien Narboux contributed to CoqIDE. +Julien Narboux contributed to {\CoqIDE}. Nicolas Tabareau made the adaptation of the interface of the old ``setoid rewrite'' tactic to the new version. Lionel Mamane worked on the interaction between Coq and its external interfaces. With Samuel @@ -750,7 +750,7 @@ standard and more robust basis. Though invisible from outside, Arnaud Spiwack improved the general process of management of existential variables. Pierre Letouzey and Stéphane Glondu improved the compilation scheme of the Coq archive. -Vincent Gross provided support to CoqIDE. Jean-Marc Notin provided +Vincent Gross provided support to {\CoqIDE}. Jean-Marc Notin provided support for benchmarking and archiving. Many users helped by reporting problems, providing patches, suggesting @@ -768,6 +768,150 @@ Paris, April 2010\\ Hugo Herbelin\\ \end{flushright} +\section*{Credits: version 8.4} + +{\Coq} version 8.4 contains the result of three long-term projects: a +new modular library of arithmetic by Pierre Letouzey, a new proof +engine by Arnaud Spiwack and a new communication protocol for {\CoqIDE} +by Vincent Gross. + +The new modular library of arithmetic extends, generalizes and +unifies the existing libraries on Peano arithmetic (types {\tt nat}, +{\tt N} and {\tt BigN}), positive arithmetic (type {\tt positive}), +integer arithmetic ({\tt Z} and {\tt BigZ}) and machine word +arithmetic (type {\tt Int31}). It provides with unified notations +(e.g. systematic use of {\tt add} and {\tt mul} for denoting the +addition and multiplication operators), systematic and generic +development of operators and properties of these operators for all the +types mentioned above, including gcd, pcm, power, square root, base 2 +logarithm, division, modulo, bitwise operations, logical shifts, +comparisons, iterators, ... + +The most visible feature of the new proof engine is the support for +structured scripts (bullets and proof brackets) but, even if yet not +user-available, the new engine also provides the basis for refining +existential variables using tactics, for applying tactics to several +goals simultaneously, for reordering goals, all features which are +planned for the next release. + +Before version 8.4, {\CoqIDE} was linked to {\Coq} with the graphical +interface living in a separate thread. From version 8.4, {\CoqIDE} is a +separate process communicating with {\Coq} through a textual +channel. This allows for a more robust interfacing, the ability to +interrupt {\Coq} without interrupting the interface, and the ability to +manage several sessions in parallel. Relying on the infrastructure +work made by Vincent Gross, Pierre Letouzey, Pierre Boutillier and +Pierre-Marie P\'edrot contributed many various refinements of {\CoqIDE}. + +{\Coq} 8.4 also comes with a bunch of many various smaller-scale changes +and improvements regarding the different components of the system. + +The underlying logic has been extended with $\eta$-conversion thanks +to Hugo Herbelin, St\'ephane Glondu and Benjamin Gr\'egoire. The +addition of $\eta$-conversion is justified by the confidence that the +formulation of the Calculus of Inductive Constructions based on typed +equality (such as the one considered in Lee and Werner to build a +set-theoretic model of CIC~\cite{LeeWerner11}) is applicable to the +concrete implementation of {\Coq}. + +The underlying logic benefited also from a refinement of the guard +condition for fixpoints by Pierre Boutillier, the point being that it +is safe to propagate the information about structurally smaller +arguments through $\beta$-redexes that are blocked by the +``match'' construction (blocked commutative cuts). + +Relying on the added permissiveness of the guard condition, Hugo +Herbelin could extend the pattern-matching compilation algorithm +so that matching over a sequence of terms involving +dependencies of a term or of the indices of the type of a term in the +type of other terms is systematically supported. + +Regarding the high-level specification language, Pierre Boutillier +introduced the ability to give implicit arguments to anonymous +functions, Hugo Herbelin introduced the ability to define notations +with several binders (e.g. \verb=exists x y z, P=), Matthieu Sozeau +made the type classes inference mechanism more robust and predictable, +Enrico Tassi introduced a command {\tt Arguments} that generalizes +{\tt Implicit Arguments} and {\tt Arguments Scope} for assigning +various properties to arguments of constants. Various improvements in +the type inference algorithm were provided by Matthieu Sozeau and Hugo +Herbelin with contributions from Enrico Tassi. + +Regarding tactics, Hugo Herbelin introduced support for referring to +expressions occurring in the goal by pattern in tactics such as {\tt + set} or {\tt destruct}. Hugo Herbelin also relied on ideas from +Chung-Kil Hur's {\tt Heq} plugin to introduce automatic computation of +occurrences to generalize when using {\tt destruct} and {\tt + induction} on types with indices. St\'ephane Glondu introduced new +tactics {\tt constr\_eq}, {\tt is\_evar} and {\tt has\_evar} to be +used when writing complex tactics. Enrico Tassi added support to +fine-tuning the behavior of {\tt simpl}. Enrico Tassi added the +ability to specify over which variables of a section a lemma has +to be exactly generalized. Pierre Letouzey added a tactic {\tt + timeout} and the interruptibility of {\tt vm\_compute}. Bug fixes +and miscellaneous improvements of the tactic language came from Hugo +Herbelin, Pierre Letouzey and Matthieu Sozeau. + +Regarding decision tactics, Lo\"ic Pottier maintained {\tt Nsatz}, +moving in particular to a type-class based reification of goals while +Fr\'ed\'eric Besson maintained {\tt Micromega}, adding in particular +support for division. + +Regarding vernacular commands, St\'ephane Glondu provided new commands +to analyze the structure of type universes. + +Regarding libraries, a new library about lists of a given length +(called vectors) has been provided by Pierre Boutillier. + +Pierre Corbineau maintained the C-zar proof mode. + +Bruno Barras and Benjamin Gr\'egoire maintained the call-by-value +reduction machines. + +The extraction mechanism benefited from several improvements provided by +Pierre Letouzey. + +Pierre Letouzey maintained the module system, with contributions from +\'Elie Soubiran. + +Julien Forest maintained the {\tt Function} command. + +Matthieu Sozeau maintained the setoid rewriting mechanism. + +{\Coq} related tools have been upgraded too. In particular, {\tt + coq\_makefile} has been largely revised by Pierre Boutillier. + +Bruno Barras and Pierre Letouzey maintained the {\tt coqchk} checker. + +Pierre Courtieu and Arnaud Spiwack contributed new features for using +{\Coq} through Proof General. + +Under the hood, the {\Coq} architecture benefited from improvements in +terms of efficiency and robustness thanks to Pierre Letouzey and Yann +R\'egis-Gianas with contributions from St\'ephane Glondu and Matthias +Puech. The build system is maintained by Pierre Letouzey with +contributions from St\'ephane Glondu and Pierre Boutillier. + +The general maintenance was done by Hugo Herbelin, Pierre Letouzey, +Pierre Boutillier and St\'ephane Glondu with local contributions from +Guillaume Melquiond and Julien Narboux. + +Packaging tools were provided by Pierre Letouzey (Windows), Pierre +Boutillier (MacOS), St\'ephane Glondu (Debian). Releasing, testing and +benchmarking support was provided by Jean-Marc Notin. + +Many suggestions for improvements were motivated by feedback from +users, on either the bug tracker or the coq-club mailing list. Special +thanks are going to the users who contributed patches, starting with +Tom Prince. Other patch contributors include C\'edric Auger, David +Baelde, Dan Grayson, Paolo Herms, Robbert Krebbers, Marc Lasson, +Hendrik Tews and Eelis van der Weegen. + +\begin{flushright} +Paris, December 2011\\ +Hugo Herbelin\\ +\end{flushright} + %new Makefile %\newpage @@ -775,7 +919,7 @@ Hugo Herbelin\\ % Integration of ZArith lemmas from Sophia and Nijmegen. -% $Id: RefMan-pre.tex 13271 2010-07-08 18:10:54Z herbelin $ +% $Id: RefMan-pre.tex 14853 2011-12-23 19:59:48Z herbelin $ %%% Local Variables: %%% mode: latex diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex index 3a8936eb..e5dc669d 100644 --- a/doc/refman/RefMan-pro.tex +++ b/doc/refman/RefMan-pro.tex @@ -133,6 +133,24 @@ one gulp, as a proof term (see Section~\ref{exact}). \SeeAlso {\tt Proof with {\tac}.} in Section~\ref{ProofWith}. +\subsection[\tt Proof using {\ident$_1$ \dots {\ident$_n$}}.] +{\tt Proof using {\ident$_1$ \dots {\ident$_n$}}. +\comindex{Proof using} \label{ProofUsing}} + +This command applies in proof editing mode. +It declares the set of section variables (see~\ref{Variable}) +used by the proof. At {\tt Qed} time, the system will assert that +the set of section variables actually used in the proof is a subset of +the declared one. + +The set of declared variables is closed under type dependency. +For example if {\tt T} is variable and {\tt a} is a variable of +type {\tt T}, the commands {\tt Proof using a} and +{\tt Proof using T a} are actually equivalent. + +\variant {\tt Proof using {\ident$_1$ \dots {\ident$_n$}} with {\tac}.} +in Section~\ref{ProofWith}. + \subsection[\tt Abort.]{\tt Abort.\comindex{Abort}} This command cancels the current proof development, switching back to @@ -211,7 +229,6 @@ backtracks one step. \begin{ErrMsgs} \item \errindex{No focused proof (No proof-editing in progress)} -\item \errindex{Undo stack would be exhausted} \end{ErrMsgs} \begin{Variants} @@ -222,18 +239,6 @@ backtracks one step. \end{Variants} -\subsection[\tt Set Undo {\num}.]{\tt Set Undo {\num}.\comindex{Set Undo}} - -This command changes the maximum number of {\tt Undo}'s that will be -possible when doing a proof. It only affects proofs started after -this command, such that if you want to change the current undo limit -inside a proof, you should first restart this proof. - -\subsection[\tt Unset Undo.]{\tt Unset Undo.\comindex{Unset Undo}} - -This command resets the default number of possible {\tt Undo} commands -(which is currently 12). - \subsection[\tt Restart.]{\tt Restart.\comindex{Restart}} This command restores the proof editing process to the original goal. @@ -362,8 +367,6 @@ All the hypotheses remains usable in the proof development. This command goes back to the default mode which is to print all available hypotheses. -% $Id: RefMan-pro.tex 13091 2010-06-08 13:56:19Z herbelin $ - \subsection[\tt Set Automatic Introduction.]{\tt Set Automatic Introduction.\comindex{Set Automatic Introduction}\comindex{Unset Automatic Introduction}\label{Set Automatic Introduction}} diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex index 2b0d636e..ea3d55f2 100644 --- a/doc/refman/RefMan-syn.tex +++ b/doc/refman/RefMan-syn.tex @@ -345,7 +345,7 @@ Infix "/\" := and (at level 80, right associativity). \subsection{Reserving notations \label{ReservedNotation} -\comindex{ReservedNotation}} +\comindex{Reserved Notation}} A given notation may be used in different contexts. {\Coq} expects all uses of the notation to be defined at the same precedence and with the @@ -774,32 +774,57 @@ To bind a delimiting key to a scope, use the command \end{quote} \subsubsection{Binding arguments of a constant to an interpretation scope -\comindex{Arguments Scope}} +\comindex{Arguments}} It is possible to set in advance that some arguments of a given constant have to be interpreted in a given scope. The command is \begin{quote} -{\tt Arguments Scope} {\qualid} {\tt [ \nelist{\optscope}{} ]} +{\tt Arguments} {\qualid} \nelist{\name {\tt \%}\scope}{} \end{quote} -where the list is a list made either of {\tt \_} or of a scope name. -Each scope in the list is bound to the corresponding parameter of -{\qualid} in order. When interpreting a term, if some of the +where the list is the list of the arguments of {\qualid} eventually +annotated with their {\scope}. Grouping round parentheses can +be used to decorate multiple arguments with the same scope. +{\scope} can be either a scope name or its delimiting key. For example +the following command puts the first two arguments of {\tt plus\_fct} +in the scope delimited by the key {\tt F} ({\tt Rfun\_scope}) and the +last argument in the scope delimited by the key {\tt R} ({\tt R\_scope}). + +\begin{coq_example*} +Arguments plus_fct (f1 f2)%F x%R. +\end{coq_example*} + +The {\tt Arguments} command accepts scopes decoration to all grouping +parentheses. In the following example arguments {\tt A} and {\tt B} +are marked as maximally inserted implicit arguments and are +put into the {\tt type\_scope} scope. + +\begin{coq_example*} +Arguments respectful {A B}%type (R R')%signature _ _. +\end{coq_example*} + +When interpreting a term, if some of the arguments of {\qualid} are built from a notation, then this notation is interpreted in the scope stack extended by the scopes bound (if any) to these arguments. +Arguments scopes can be cleared with the following command: + +\begin{quote} +{\tt Arguments {\qualid} : clear scopes} +\end{quote} + \begin{Variants} -\item {\tt Global Arguments Scope} {\qualid} {\tt [ \nelist{\optscope}{} ]} +\item {\tt Global Arguments} {\qualid} \nelist{\name {\tt \%}\scope}{} -This behaves like {\tt Arguments Scope} {\qualid} {\tt [ -\nelist{\optscope}{} ]} but survives when a section is closed instead +This behaves like {\tt Arguments} {\qualid} \nelist{\name {\tt \%}\scope}{} +but survives when a section is closed instead of stopping working at section closing. Without the {\tt Global} modifier, the effect of the command stops when the section it belongs to ends. -\item {\tt Local Arguments Scope} {\qualid} {\tt [ \nelist{\optscope}{} ]} +\item {\tt Local Arguments} {\qualid} \nelist{\name {\tt \%}\scope}{} -This behaves like {\tt Arguments Scope} {\qualid} {\tt [ - \nelist{\optscope}{} ]} but does not survive modules and files. +This behaves like {\tt Arguments} {\qualid} \nelist{\name {\tt \%}\scope}{} +but does not survive modules and files. Without the {\tt Local} modifier, the effect of the command is visible from within other modules or files. @@ -861,7 +886,7 @@ declared or defined constant. We give an overview of the scopes used in the standard library of {\Coq}. For a complete list of notations in each scope, use the -commands {\tt Print Scopes} or {\tt Print Scopes {\scope}}. +commands {\tt Print Scopes} or {\tt Print Scope {\scope}}. \subsubsection{\tt type\_scope} @@ -1047,7 +1072,8 @@ at the time of use of the abbreviation. %except that abbreviations are used for printing (unless the modifier %\verb=(only parsing)= is given) while syntactic definitions were not. -\section{Tactic Notations} +\section{Tactic Notations +\comindex{Tactic Notation}} Tactic notations allow to customize the syntax of the tactics of the tactic language\footnote{Tactic notations are just a simplification of @@ -1140,8 +1166,6 @@ places where a list of the underlying entry can be used: {\nterm{entry}} is either {\tt\small constr}, {\tt\small hyp}, {\tt\small integer} or {\tt\small int\_or\_var}. -% $Id: RefMan-syn.tex 13329 2010-07-26 11:05:39Z herbelin $ - %%% Local Variables: %%% mode: latex %%% TeX-master: "Reference-Manual" diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 14d95ab8..198f8f30 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -497,6 +497,89 @@ Section~\ref{pattern} to transform the goal so that it gets the form \end{Variants} +\subsection{{\tt apply {\term} in {\ident}} +\tacindex{apply \ldots\ in}} + +This tactic applies to any goal. The argument {\term} is a term +well-formed in the local context and the argument {\ident} is an +hypothesis of the context. The tactic {\tt apply {\term} in {\ident}} +tries to match the conclusion of the type of {\ident} against a non +dependent premise of the type of {\term}, trying them from right to +left. If it succeeds, the statement of hypothesis {\ident} is +replaced by the conclusion of the type of {\term}. The tactic also +returns as many subgoals as the number of other non dependent premises +in the type of {\term} and of the non dependent premises of the type +of {\ident}. If the conclusion of the type of {\term} does not match +the goal {\em and} the conclusion is an inductive type isomorphic to a +tuple type, then the tuple is (recursively) decomposed and the first +component of the tuple of which a non dependent premise matches the +conclusion of the type of {\ident}. Tuples are decomposed in a +width-first left-to-right order (for instance if the type of {\tt H1} +is a \verb=A <-> B= statement, and the type of {\tt H2} is \verb=A= +then {\tt apply H1 in H2} transforms the type of {\tt H2} into {\tt + B}). The tactic {\tt apply} relies on first-order pattern-matching +with dependent types. + +\begin{ErrMsgs} +\item \errindex{Statement without assumptions} + +This happens if the type of {\term} has no non dependent premise. + +\item \errindex{Unable to apply} + +This happens if the conclusion of {\ident} does not match any of the +non dependent premises of the type of {\term}. +\end{ErrMsgs} + +\begin{Variants} +\item {\tt apply \nelist{\term}{,} in {\ident}} + +This applies each of {\term} in sequence in {\ident}. + +\item {\tt apply \nelist{{\term} with {\bindinglist}}{,} in {\ident}} + +This does the same but uses the bindings in each {\bindinglist} to +instantiate the parameters of the corresponding type of {\term} +(see syntax of bindings in Section~\ref{Binding-list}). + +\item {\tt eapply \nelist{{\term} with {\bindinglist}}{,} in {\ident}} +\tacindex{eapply {\ldots} in} + +This works as {\tt apply \nelist{{\term} with {\bindinglist}}{,} in +{\ident}} but turns unresolved bindings into existential variables, if +any, instead of failing. + +\item {\tt apply \nelist{{\term}{,} with {\bindinglist}}{,} in {\ident} as {\disjconjintropattern}} + +This works as {\tt apply \nelist{{\term}{,} with {\bindinglist}}{,} in +{\ident}} then destructs the hypothesis {\ident} along +{\disjconjintropattern} as {\tt destruct {\ident} as +{\disjconjintropattern}} would. + +\item {\tt eapply \nelist{{\term}{,} with {\bindinglist}}{,} in {\ident} as {\disjconjintropattern}} + +This works as {\tt apply \nelist{{\term}{,} with {\bindinglist}}{,} in {\ident} as {\disjconjintropattern}} but using {\tt eapply}. + +\item {\tt simple apply {\term} in {\ident}} +\tacindex{simple apply {\ldots} in} +\tacindex{simple eapply {\ldots} in} + +This behaves like {\tt apply {\term} in {\ident}} but it reasons +modulo conversion only on subterms that contain no variables to +instantiate. For instance, if {\tt id := fun x:nat => x} and {\tt H : + forall y, id y = y -> True} and {\tt H0 : O = O} then {\tt simple + apply H in H0} does not succeed because it would require the +conversion of {\tt f ?y} and {\tt O} where {\tt ?y} is a variable to +instantiate. Tactic {\tt simple apply {\term} in {\ident}} does not +either traverse tuples as {\tt apply {\term} in {\ident}} does. + +\item {\tt \zeroone{simple} apply \nelist{{\term} \zeroone{with {\bindinglist}}}{,} in {\ident} \zeroone{as {\disjconjintropattern}}}\\ +{\tt \zeroone{simple} eapply \nelist{{\term} \zeroone{with {\bindinglist}}}{,} in {\ident} \zeroone{as {\disjconjintropattern}}} + +This summarizes the different syntactic variants of {\tt apply {\term} + in {\ident}} and {\tt eapply {\term} in {\ident}}. +\end{Variants} + \subsection{{\tt set ( {\ident} {\tt :=} {\term} \tt )} \label{tactic:set} \tacindex{set} @@ -508,6 +591,11 @@ hypotheses of the current goal and adds the new definition {\ident {\tt :=} \term} to the local context. The default is to make this replacement only in the conclusion. +If {\term} has holes (i.e. subexpressions of the form ``\_''), the +tactic first checks that all subterms matching the pattern are +compatible before doing the replacement using the leftmost subterm +matching the pattern. + \begin{Variants} \item {\tt set (} {\ident} {\tt :=} {\term} {\tt ) in {\occgoalset}} @@ -543,7 +631,7 @@ Section~\ref{Occurrences clauses}. This is a more general form of {\tt remember} that remembers the occurrences of {\term} specified by an occurrences set. -\item {\tt pose ( {\ident} {\tt :=} {\term} {\tt )}} +\item {\tt pose ( {\ident} := {\term} )} This adds the local definition {\ident} := {\term} to the current context without performing any replacement in the goal or in the @@ -660,89 +748,6 @@ in the list of subgoals remaining to prove. \end{Variants} -\subsection{{\tt apply {\term} in {\ident}} -\tacindex{apply \ldots\ in}} - -This tactic applies to any goal. The argument {\term} is a term -well-formed in the local context and the argument {\ident} is an -hypothesis of the context. The tactic {\tt apply {\term} in {\ident}} -tries to match the conclusion of the type of {\ident} against a non -dependent premise of the type of {\term}, trying them from right to -left. If it succeeds, the statement of hypothesis {\ident} is -replaced by the conclusion of the type of {\term}. The tactic also -returns as many subgoals as the number of other non dependent premises -in the type of {\term} and of the non dependent premises of the type -of {\ident}. If the conclusion of the type of {\term} does not match -the goal {\em and} the conclusion is an inductive type isomorphic to a -tuple type, then the tuple is (recursively) decomposed and the first -component of the tuple of which a non dependent premise matches the -conclusion of the type of {\ident}. Tuples are decomposed in a -width-first left-to-right order (for instance if the type of {\tt H1} -is a \verb=A <-> B= statement, and the type of {\tt H2} is \verb=A= -then {\tt apply H1 in H2} transforms the type of {\tt H2} into {\tt - B}). The tactic {\tt apply} relies on first-order pattern-matching -with dependent types. - -\begin{ErrMsgs} -\item \errindex{Statement without assumptions} - -This happens if the type of {\term} has no non dependent premise. - -\item \errindex{Unable to apply} - -This happens if the conclusion of {\ident} does not match any of the -non dependent premises of the type of {\term}. -\end{ErrMsgs} - -\begin{Variants} -\item {\tt apply \nelist{\term}{,} in {\ident}} - -This applies each of {\term} in sequence in {\ident}. - -\item {\tt apply \nelist{{\term} with {\bindinglist}}{,} in {\ident}} - -This does the same but uses the bindings in each {\bindinglist} to -instantiate the parameters of the corresponding type of {\term} -(see syntax of bindings in Section~\ref{Binding-list}). - -\item {\tt eapply \nelist{{\term} with {\bindinglist}}{,} in {\ident}} -\tacindex{eapply {\ldots} in} - -This works as {\tt apply \nelist{{\term} with {\bindinglist}}{,} in -{\ident}} but turns unresolved bindings into existential variables, if -any, instead of failing. - -\item {\tt apply \nelist{{\term}{,} with {\bindinglist}}{,} in {\ident} as {\disjconjintropattern}} - -This works as {\tt apply \nelist{{\term}{,} with {\bindinglist}}{,} in -{\ident}} then destructs the hypothesis {\ident} along -{\disjconjintropattern} as {\tt destruct {\ident} as -{\disjconjintropattern}} would. - -\item {\tt eapply \nelist{{\term}{,} with {\bindinglist}}{,} in {\ident} as {\disjconjintropattern}} - -This works as {\tt apply \nelist{{\term}{,} with {\bindinglist}}{,} in {\ident} as {\disjconjintropattern}} but using {\tt eapply}. - -\item {\tt simple apply {\term} in {\ident}} -\tacindex{simple apply {\ldots} in} -\tacindex{simple eapply {\ldots} in} - -This behaves like {\tt apply {\term} in {\ident}} but it reasons -modulo conversion only on subterms that contain no variables to -instantiate. For instance, if {\tt id := fun x:nat => x} and {\tt H : - forall y, id y = y -> True} and {\tt H0 : O = O} then {\tt simple - apply H in H0} does not succeed because it would require the -conversion of {\tt f ?y} and {\tt O} where {\tt ?y} is a variable to -instantiate. Tactic {\tt simple apply {\term} in {\ident}} does not -either traverse tuples as {\tt apply {\term} in {\ident}} does. - -\item {\tt \zeroone{simple} apply \nelist{{\term} \zeroone{with {\bindinglist}}}{,} in {\ident} \zeroone{as {\disjconjintropattern}}}\\ -{\tt \zeroone{simple} eapply \nelist{{\term} \zeroone{with {\bindinglist}}}{,} in {\ident} \zeroone{as {\disjconjintropattern}}} - -This summarizes the different syntactic variants of {\tt apply {\term} - in {\ident}} and {\tt eapply {\term} in {\ident}}. -\end{Variants} - \subsection{\tt generalize \term \tacindex{generalize} \label{generalize}} @@ -950,7 +955,8 @@ existential variable. \tacindex{instantiate} \label{instantiate}} -The {\tt instantiate} tactic allows to solve an existential variable +The {\tt instantiate} tactic allows to refine (see Section~\ref{refine}) +an existential variable with the term \term. The \num\ argument is the position of the existential variable from right to left in the conclusion. This cannot be the number of the existential variable since this number is different @@ -1296,8 +1302,8 @@ computational expressions (i.e. with few dead code). \item {\tt lazy [\qualid$_1$\ldots\qualid$_k$]}\\ {\tt lazy -[\qualid$_1$\ldots\qualid$_k$]} - These are respectively synonyms of {\tt cbv beta delta - [\qualid$_1$\ldots\qualid$_k$] iota zeta} and {\tt cbv beta delta + These are respectively synonyms of {\tt lazy beta delta + [\qualid$_1$\ldots\qualid$_k$] iota zeta} and {\tt lazy beta delta -[\qualid$_1$\ldots\qualid$_k$] iota zeta}. \item {\tt vm\_compute} \tacindex{vm\_compute} @@ -1361,6 +1367,55 @@ by {\tt plus' := plus} is possibly unfolded and reused in the recursive calls, but a constant such as {\tt succ := plus (S O)} is never unfolded. +The behaviour of {\tt simpl} can be tuned using the {\tt Arguments} vernacular +command as follows: +\begin{itemize} +\item +A constant can be marked to be never unfolded by {\tt simpl}: +\begin{coq_example*} +Arguments minus x y : simpl never +\end{coq_example*} +After that command an expression like {\tt (minus (S x) y)} is left untouched by +the {\tt simpl} tactic. +\item +A constant can be marked to be unfolded only if applied to enough arguments. +The number of arguments required can be specified using +the {\tt /} symbol in the arguments list of the {\tt Arguments} vernacular +command. +\begin{coq_example*} +Definition fcomp A B C f (g : A -> B) (x : A) : C := f (g x). +Notation "f \o g" := (fcomp f g) (at level 50). +Arguments fcomp {A B C} f g x /. +\end{coq_example*} +After that command the expression {\tt (f \verb+\+o g)} is left untouched by +{\tt simpl} while {\tt ((f \verb+\+o g) t)} is reduced to {\tt (f (g t))}. +The same mechanism can be used to make a constant volatile, i.e. always +unfolded by {\tt simpl}. +\begin{coq_example*} +Definition volatile := fun x : nat => x. +Arguments volatile / x. +\end{coq_example*} +\item +A constant can be marked to be unfolded only if an entire set of arguments +evaluates to a constructor. The {\tt !} symbol can be used to mark such +arguments. +\begin{coq_example*} +Arguments minus !x !y. +\end{coq_example*} +After that command, the expression {\tt (minus (S x) y)} is left untouched by +{\tt simpl}, while {\tt (minus (S x) (S y))} is reduced to {\tt (minus x y)}. +\item +A special heuristic to determine if a constant has to be unfolded can be +activated with the following command: +\begin{coq_example*} +Arguments minus x y : simpl nomatch +\end{coq_example*} +The heuristic avoids to perform a simplification step that would +expose a {\tt match} construct in head position. For example the +expression {\tt (minus (S (S x)) (S y))} is simplified to +{\tt (minus (S x) y)} even if an extra simplification is possible. +\end{itemize} + \tacindex{simpl \dots\ in} \begin{Variants} \item {\tt simpl {\term}} @@ -1626,18 +1681,16 @@ Section~\ref{Cic-inductive-definitions}). \subsection{\tt induction \term \tacindex{induction}} -This tactic applies to any goal. The type of the argument {\term} must -be an inductive constant. Then, the tactic {\tt induction} -generates subgoals, one for each possible form of {\term}, i.e. one -for each constructor of the inductive type. +This tactic applies to any goal. The argument {\term} must be of +inductive type and the tactic {\tt induction} generates subgoals, +one for each possible form of {\term}, i.e. one for each constructor +of the inductive type. -The tactic {\tt induction} automatically replaces every occurrences -of {\term} in the conclusion and the hypotheses of the goal. It -automatically adds induction hypotheses (using names of the form {\tt - IHn1}) to the local context. If some hypothesis must not be taken -into account in the induction hypothesis, then it needs to be removed -first (you can also use the tactics {\tt elim} or {\tt simple induction}, -see below). +If the argument is dependent in either the conclusion or some +hypotheses of the goal, the argument is replaced by the appropriate +constructor form in each of the resulting subgoals and induction +hypotheses are added to the local context using names whose prefix is +{\tt IH}. There are particular cases: @@ -1649,10 +1702,13 @@ behaves as {\tt intros until {\ident}; induction {\ident}}. \item If {\term} is a {\num}, then {\tt induction {\num}} behaves as {\tt intros until {\num}} followed by {\tt induction} applied to the -last introduced hypothesis. +last introduced hypothesis. Remark: For simple induction on a numeral, +use syntax {\tt induction ({\num})} (not very interesting anyway). -\Rem For simple induction on a numeral, use syntax {\tt induction -({\num})} (not very interesting anyway). +\item The argument {\term} can also be a pattern of which holes are + denoted by ``\_''. In this case, the tactic checks that all subterms + matching the pattern in the conclusion and the hypotheses are + compatible and performs induction using this subterm. \end{itemize} @@ -1840,10 +1896,19 @@ instantiate premises of the type of {\term$_2$}. \tacindex{destruct}} \label{destruct} -The tactic {\tt destruct} is used to perform case analysis without -recursion. Its behavior is similar to {\tt induction} except -that no induction hypothesis is generated. It applies to any goal and -the type of {\term} must be inductively defined. There are particular cases: +This tactic applies to any goal. The argument {\term} must be of +inductive or coinductive type and the tactic generates subgoals, one +for each possible form of {\term}, i.e. one for each constructor of +the inductive or coinductive type. Unlike {\tt induction}, no +induction hypothesis is generated by {\tt destruct}. + +If the argument is dependent in either the conclusion or some +hypotheses of the goal, the argument is replaced by the appropriate +constructor form in each of the resulting subgoals, thus performing +case analysis. If non dependent, the tactic simply exposes the +inductive or coinductive structure of the argument. + +There are special cases: \begin{itemize} @@ -1853,10 +1918,13 @@ behaves as {\tt intros until {\ident}; destruct {\ident}}. \item If {\term} is a {\num}, then {\tt destruct {\num}} behaves as {\tt intros until {\num}} followed by {\tt destruct} applied to the -last introduced hypothesis. +last introduced hypothesis. Remark: For destruction of a numeral, use +syntax {\tt destruct ({\num})} (not very interesting anyway). -\Rem For destruction of a numeral, use syntax {\tt destruct -({\num})} (not very interesting anyway). +\item The argument {\term} can also be a pattern of which holes are + denoted by ``\_''. In this case, the tactic checks that all subterms + matching the pattern in the conclusion and the hypotheses are + compatible and performs case analysis using this subterm. \end{itemize} @@ -2599,12 +2667,7 @@ This tactic solves a goal of the form {\tt forall $x$ $y$:$R$, \{$x$=$y$\}+\{\verb|~|$x$=$y$\}}, where $R$ is an inductive type such that its constructors do not take proofs or functions as arguments, nor objects in dependent types. - -\begin{Variants} -\item {\tt decide equality {\term}$_1$ {\term}$_2$ }.\\ - Solves a goal of the form {\tt \{}\term$_1${\tt =}\term$_2${\tt -\}+\{\verb|~|}\term$_1${\tt =}\term$_2${\tt \}}. -\end{Variants} +It solves goals of the form {\tt \{$x$=$y$\}+\{\verb|~|$x$=$y$\}} as well. \subsection{\tt compare \term$_1$ \term$_2$ \tacindex{compare}} @@ -2696,7 +2759,7 @@ If {\term} is a proof of a statement of conclusion then {\tt injection} applies injectivity as deep as possible to derive the equality of all the subterms of {\term$_1$} and {\term$_2$} placed in the same positions. For example, from {\tt (S - (S n))=(S (S (S m))} we may derive {\tt n=(S m)}. To use this + (S n))=(S (S (S m)))} we may derive {\tt n=(S m)}. To use this tactic {\term$_1$} and {\term$_2$} should be elements of an inductive set and they should be neither explicitly equal, nor structurally different. We mean by this that, if {\tt n$_1$} and {\tt n$_2$} are @@ -4042,7 +4105,9 @@ databases are non empty and can be used. \begin{description} \item[\tt core] This special database is automatically used by - \texttt{auto}. It contains only basic lemmas about negation, + \texttt{auto}, except when pseudo-database \texttt{nocore} is + given to \texttt{auto}. The \texttt{core} database contains + only basic lemmas about negation, conjunction, and so on from. Most of the hints in this database come from the \texttt{Init} and \texttt{Logic} directories. @@ -4174,6 +4239,16 @@ e.g. \texttt{Require Import A.}). \SeeAlso {\tt Proof.} in Section~\ref{BeginProof}. +\begin{Variants} +\item {\tt Proof with {\tac} using {\ident$_1$ \dots {\ident$_n$}}} + Combines in a single line {\tt Proof with} and {\tt Proof using}, + see~\ref{ProofUsing} +\item {\tt Proof using {\ident$_1$ \dots {\ident$_n$}} with {\tac}} + Combines in a single line {\tt Proof with} and {\tt Proof using}, + see~\ref{ProofUsing} + +\end{Variants} + \subsubsection[\tt Declare Implicit Tactic {\tac}.]{\tt Declare Implicit Tactic {\tac}.\comindex{Declare Implicit Tactic}} This command declares a tactic to be used to solve implicit arguments @@ -4230,7 +4305,8 @@ general principle of mutual induction for objects in type {\term$_i$}. \item {\tt Scheme Equality for \ident$_1$\comindex{Scheme Equality}} Tries to generate a boolean equality and a proof of the - decidability of the usual equality. + decidability of the usual equality. If \ident$_i$ involves + some other inductive types, their equality has to be defined first. \item {\tt Scheme Induction for \ident$_1$ Sort {\sort$_1$} \\ with\\ @@ -4332,8 +4408,6 @@ Chapter~\ref{TacticLanguage} gives examples of more complex user-defined tactics. -% $Id: RefMan-tac.tex 14762 2011-12-04 20:48:36Z herbelin $ - %%% Local Variables: %%% mode: latex %%% TeX-master: "Reference-Manual" diff --git a/doc/refman/RefMan-uti.tex b/doc/refman/RefMan-uti.tex index 5f201b67..bda4cff9 100644 --- a/doc/refman/RefMan-uti.tex +++ b/doc/refman/RefMan-uti.tex @@ -84,85 +84,42 @@ modules. The writing of a generic and complete {\tt Makefile} may be a tedious work and that's why \Coq\ provides a tool to automate its creation, -{\tt coq\_makefile}. Given the files to compile, the command {\tt -coq\_makefile} prints a -{\tt Makefile} on the standard output. So one has just to run the -command: +{\tt coq\_makefile}. -\begin{quotation} -\texttt{\% coq\_makefile} {\em file$_1$.v \dots\ file$_n$.v} \texttt{> Makefile} -\end{quotation} - -The resulted {\tt Makefile} has a target {\tt depend} which computes the -dependencies and puts them in a separate file {\tt .depend}, which is -included by the {\tt Makefile}. -Therefore, you should create such a file before the first invocation -of make. You can for instance use the command - -\begin{quotation} -\texttt{\% touch .depend} -\end{quotation} - -Then, to initialize or update the modules dependencies, type in: +Arguments are explain by \texttt{\% coq\_makefile --help}. They can be directly +written in the command line but it is recommended to write them in a file (called +for example {\tt Make}) and then call {\tt coq\_makefile -f Make -o + Makefile}. That means options are in {\tt Make} file and output is {\tt + Makefile} This way, {\tt Makefile} will be automatically regenerated if +something changes in {\tt Make}. +The first time you use this tool, you may be happy with: \begin{quotation} -\texttt{\% make depend} +\texttt{\% \{ echo '-R .} {\em MyFancyLib} \texttt{' ; find -name '*.v' -print \} > + Make \&\& coq\_makefile -f Make -o Makefile} \end{quotation} -There is a target {\tt all} to compile all the files {\em file$_1$ -\dots\ file$_n$}, and a generic target to produce a {\tt .vo} file from -the corresponding {\tt .v} file (so you can do {\tt make} {\em file}{\tt.vo} -to compile the file {\em file}{\tt.v}). - -{\tt coq\_makefile} can also handle the case of ML files and -subdirectories. For more options type - -\begin{quotation} -\texttt{\% coq\_makefile --help} -\end{quotation} +To customize things afterwards, remember: +\begin{itemize} +\item Coq files must end in {\tt .v}, caml modules in {\tt .ml4} if they + require camlp preproccessing (and in {\tt .ml} otherwise), and caml module signatures in {\tt + .mli}. +\item If you give a directory directly as argument, it is because you provide a + Makefile for it in it. +\item {\tt -R} option is for Coq, {\tt -I} for caml. The same directory can + ``included'' by both. + Using {\tt -R} option gives a right logical path and a correct installation + emplacement to your coq files. +\item If your files depend on an external library that isn't install somewhere + looked by coqc, use {\tt OTHERFLAGS = '-R path/to/lib lib\_name'} option in your {\tt + Make} but don't do {\tt -R \dots} directly, the {\em make clean} command would + erase it! +\end{itemize} \Warning To compile a project containing \ocaml{} files you must keep the sources of \Coq{} somewhere and have an environment variable named \texttt{COQTOP} that points to that directory. -% \section{{\sf Coq\_SearchIsos}: information retrieval in a \Coq\ proofs -% library} -% \label{coqsearchisos} -% \index{Coq\_SearchIsos@{\sf Coq\_SearchIsos}} - -% In the \Coq\ distribution, there is also a separated and independent tool, -% called {\sf Coq\_SearchIsos}, which allows the search in accordance with {\tt -% SearchIsos}\index{SearchIsos@{\tt SearchIsos}} (see Section~\ref{searchisos}) -% in a \Coq\ proofs library. More precisely, this program begins, once launched -% by {\tt coqtop -searchisos}\index{coqtopsearchisos@{\tt -% coqtop -searchisos}}, loading lightly (by using specifications functions) -% all the \Coq\ objects files ({\tt .vo}) accessible by the {\tt LoadPath} (see -% Section~\ref{loadpath}). Next, a prompt appears and four commands are then -% available: - -% \begin{description} -% \item [{\tt SearchIsos}]\ \\ -% Scans the fixed context. -% \item [{\tt Time}]\index{Time@{\tt Time}}\ \\ -% Turns on the Time Search Display mode (see Section~\ref{time}). -% \item [{\tt Untime}]\index{Untime@{\tt Untime}}\ \\ -% Turns off the Time Search Display mode (see Section~\ref{time}). -% \item [{\tt Quit}]\index{Quit@{\tt Quit}}\ \\ -% Ends the {\tt coqtop -searchisos} session. -% \end{description} - -% When running {\tt coqtop -searchisos} you can use the two options: - -% \begin{description} -% \item[{\tt -opt}]\ \\ -% Runs the native-code version of {\sf Coq\_SearchIsos}. - -% \item[{\tt -image} {\em file}]\ \\ -% This option sets the binary image to be used to be {\em file} -% instead of the standard one. Not of general use. -% \end{description} - - \section[Documenting \Coq\ files with coqdoc]{Documenting \Coq\ files with coqdoc\label{coqdoc} \index{Coqdoc@{\sf coqdoc}}} @@ -200,8 +157,8 @@ have been completely produced with {\tt coq-tex}. \subsection{The \Coq\ Emacs mode} \Coq\ comes with a Major mode for \emacs, {\tt coq.el}. This mode provides -syntax highlighting (assuming your \emacs\ library provides -{\tt hilit19.el}) and also a rudimentary indentation facility +syntax highlighting +and also a rudimentary indentation facility in the style of the Caml \emacs\ mode. Add the following lines to your \verb!.emacs! file: @@ -232,7 +189,7 @@ Instructions to use it are contained in this file. \subsection[Proof General]{Proof General\index{Proof General}} Proof General is a generic interface for proof assistants based on -Emacs (or XEmacs). The main idea is that the \Coq\ commands you are +Emacs. The main idea is that the \Coq\ commands you are editing are sent to a \Coq\ toplevel running behind Emacs and the answers of the system automatically inserted into other Emacs buffers. Thus you don't need to copy-paste the \Coq\ material from your files @@ -264,8 +221,6 @@ There are man pages for the commands {\tt coqdep}, {\tt gallina} and \RefManCutCommand{ENDREFMAN=\thepage} %END LATEX -% $Id: RefMan-uti.tex 11975 2009-03-14 11:29:36Z letouzey $ - %%% Local Variables: %%% mode: latex %%% TeX-master: t diff --git a/doc/refman/Reference-Manual.tex b/doc/refman/Reference-Manual.tex index b0ada528..cc42c2ef 100644 --- a/doc/refman/Reference-Manual.tex +++ b/doc/refman/Reference-Manual.tex @@ -148,4 +148,3 @@ Options A and B of the licence are {\em not} elected.} \end{document} -% $Id: Reference-Manual.tex 14090 2011-05-03 13:34:16Z pboutill $ diff --git a/doc/refman/Setoid.tex b/doc/refman/Setoid.tex index 20c8c02b..8e1bb10c 100644 --- a/doc/refman/Setoid.tex +++ b/doc/refman/Setoid.tex @@ -710,5 +710,4 @@ using the command \texttt{Typeclasses Opaque} (see \S \ref{TypeclassesTransparen %%% Local Variables: %%% mode: latex %%% TeX-master: "Reference-Manual" -%%% compile-command: "make -C ../.. -f Makefile.stage3 doc/refman/Reference-Manual.pdf" %%% End: diff --git a/doc/refman/biblio.bib b/doc/refman/biblio.bib index f93b66f9..192a9699 100644 --- a/doc/refman/biblio.bib +++ b/doc/refman/biblio.bib @@ -1246,6 +1246,19 @@ Languages}, publisher = {} } +@article{LeeWerner11, + author = {Gyesik Lee and + Benjamin Werner}, + title = {Proof-irrelevant model of {CC} with predicative induction + and judgmental equality}, + journal = {Logical Methods in Computer Science}, + volume = {7}, + number = {4}, + year = {2011}, + ee = {http://dx.doi.org/10.2168/LMCS-7(4:5)2011}, + bibsource = {DBLP, http://dblp.uni-trier.de} +} + @Comment{cross-references, must be at end} @Book{Bastad92, diff --git a/doc/stdlib/Library.tex b/doc/stdlib/Library.tex index bfd7f3f2..cb32adfc 100755 --- a/doc/stdlib/Library.tex +++ b/doc/stdlib/Library.tex @@ -3,6 +3,7 @@ \usepackage[utf8x]{inputenc} \usepackage[T1]{fontenc} \usepackage{fullpage} +\usepackage{amsfonts} \usepackage[color]{../../coqdoc} \input{../common/version} @@ -61,4 +62,3 @@ you can access from the \Coq\ home page at \end{document} -% $Id: Library.tex 12363 2009-09-28 15:04:07Z letouzey $ diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index 541fa1b9..35c13f3b 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -1,5 +1,17 @@ +<!DOCTYPE html + PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" + "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd"> -<h1>The Coq Standard Library</h1> +<html xmlns="http://www.w3.org/1999/xhtml" xml:lang="en" lang="en"> +<head> +<meta http-equiv="Content-Type" content="text/html; charset=iso-8859-15"/> +<link rel="stylesheet" href="css/context.css" type="text/css"/> +<title>The Coq Standard Library</title> +</head> + +<body> + +<H1>The Coq Standard Library</H1> <p>Here is a short description of the Coq standard library, which is distributed with the system. @@ -109,7 +121,6 @@ through the <tt>Require Import</tt> command.</p> (theories/Arith/Arith.v) theories/Arith/Min.v theories/Arith/Max.v - theories/Arith/MinMax.v theories/Arith/Compare.v theories/Arith/Div2.v theories/Arith/EqNat.v @@ -118,31 +129,40 @@ through the <tt>Require Import</tt> command.</p> theories/Arith/Bool_nat.v theories/Arith/Factorial.v theories/Arith/Wf_nat.v - theories/Arith/NatOrderedType.v </dd> - - <dt> <b>NArith</b>: + + <dt> <b>PArith</b>: Binary positive integers </dt> - <dd> - theories/NArith/BinPos.v + <dd> + theories/PArith/BinPosDef.v + theories/PArith/BinPos.v + theories/PArith/Pnat.v + theories/PArith/POrderedType.v + (theories/PArith/PArith.v) + </dd> + + <dt> <b>NArith</b>: + Binary natural numbers + </dt> + <dd> + theories/NArith/BinNatDef.v theories/NArith/BinNat.v - (theories/NArith/NArith.v) - theories/NArith/Pnat.v theories/NArith/Nnat.v theories/NArith/Ndigits.v theories/NArith/Ndist.v theories/NArith/Ndec.v - theories/NArith/NOrderedType.v - theories/NArith/Nminmax.v - theories/NArith/POrderedType.v - theories/NArith/Pminmax.v + theories/NArith/Ndiv_def.v + theories/NArith/Ngcd_def.v + theories/NArith/Nsqrt_def.v + (theories/NArith/NArith.v) </dd> <dt> <b>ZArith</b>: Binary integers </dt> - <dd> + <dd> + theories/ZArith/BinIntDef.v theories/ZArith/BinInt.v theories/ZArith/Zorder.v theories/ZArith/Zcompare.v @@ -160,20 +180,20 @@ through the <tt>Require Import</tt> command.</p> theories/ZArith/Zhints.v (theories/ZArith/ZArith_base.v) theories/ZArith/Zcomplements.v - theories/ZArith/Zsqrt.v + theories/ZArith/Zsqrt_compat.v theories/ZArith/Zpow_def.v + theories/ZArith/Zpow_alt.v theories/ZArith/Zpower.v theories/ZArith/Zdiv.v + theories/ZArith/Zquot.v + theories/ZArith/Zeuclid.v theories/ZArith/Zlogarithm.v (theories/ZArith/ZArith.v) theories/ZArith/Zgcd_alt.v theories/ZArith/Zwf.v theories/ZArith/Znumtheory.v theories/ZArith/Int.v - theories/ZArith/ZOdiv_def.v - theories/ZArith/ZOdiv.v theories/ZArith/Zpow_facts.v - theories/ZArith/ZOrderedType.v theories/ZArith/Zdigits.v </dd> @@ -198,10 +218,9 @@ through the <tt>Require Import</tt> command.</p> <dt> <b>Numbers</b>: An experimental modular architecture for arithmetic </dt> - <dd> - <dl> - <dt> <b> Prelude</b>:</dt> + <dt> <b> Prelude</b>: <dd> + theories/Numbers/BinNums.v theories/Numbers/NumPrelude.v theories/Numbers/BigNumPrelude.v theories/Numbers/NaryFunctions.v @@ -209,7 +228,6 @@ through the <tt>Require Import</tt> command.</p> <dt> <b> NatInt</b>: Abstract mixed natural/integer/cyclic arithmetic - </dt> <dd> theories/Numbers/NatInt/NZAdd.v theories/Numbers/NatInt/NZAddOrder.v @@ -221,11 +239,17 @@ through the <tt>Require Import</tt> command.</p> theories/Numbers/NatInt/NZOrder.v theories/Numbers/NatInt/NZDomain.v theories/Numbers/NatInt/NZProperties.v + theories/Numbers/NatInt/NZParity.v + theories/Numbers/NatInt/NZPow.v + theories/Numbers/NatInt/NZSqrt.v + theories/Numbers/NatInt/NZLog.v + theories/Numbers/NatInt/NZGcd.v + theories/Numbers/NatInt/NZBits.v </dd> + </dt> - <dt> <b> Cyclic</b>: + <dt> <b> Cyclic</b>: Abstract and 31-bits-based cyclic arithmetic - </dt> <dd> theories/Numbers/Cyclic/Abstract/CyclicAxioms.v theories/Numbers/Cyclic/Abstract/NZCyclic.v @@ -244,10 +268,10 @@ through the <tt>Require Import</tt> command.</p> theories/Numbers/Cyclic/Int31/Int31.v theories/Numbers/Cyclic/ZModulo/ZModulo.v </dd> + </dt> - <dt> <b> Natural</b>: + <dt> <b> Natural</b>: Abstract and 31-bits-words-based natural arithmetic - </dt> <dd> theories/Numbers/Natural/Abstract/NAdd.v theories/Numbers/Natural/Abstract/NAddOrder.v @@ -260,6 +284,14 @@ through the <tt>Require Import</tt> command.</p> theories/Numbers/Natural/Abstract/NStrongRec.v theories/Numbers/Natural/Abstract/NSub.v theories/Numbers/Natural/Abstract/NDiv.v + theories/Numbers/Natural/Abstract/NMaxMin.v + theories/Numbers/Natural/Abstract/NParity.v + theories/Numbers/Natural/Abstract/NPow.v + theories/Numbers/Natural/Abstract/NSqrt.v + theories/Numbers/Natural/Abstract/NLog.v + theories/Numbers/Natural/Abstract/NGcd.v + theories/Numbers/Natural/Abstract/NLcm.v + theories/Numbers/Natural/Abstract/NBits.v theories/Numbers/Natural/Abstract/NProperties.v theories/Numbers/Natural/Binary/NBinary.v theories/Numbers/Natural/Peano/NPeano.v @@ -270,10 +302,10 @@ through the <tt>Require Import</tt> command.</p> theories/Numbers/Natural/BigN/NMake.v theories/Numbers/Natural/BigN/NMake_gen.v </dd> + </dt> <dt> <b> Integer</b>: Abstract and concrete (especially 31-bits-words-based) integer arithmetic - </dt> <dd> theories/Numbers/Integer/Abstract/ZAdd.v theories/Numbers/Integer/Abstract/ZAddOrder.v @@ -282,11 +314,17 @@ through the <tt>Require Import</tt> command.</p> theories/Numbers/Integer/Abstract/ZLt.v theories/Numbers/Integer/Abstract/ZMul.v theories/Numbers/Integer/Abstract/ZMulOrder.v + theories/Numbers/Integer/Abstract/ZSgnAbs.v + theories/Numbers/Integer/Abstract/ZMaxMin.v + theories/Numbers/Integer/Abstract/ZParity.v + theories/Numbers/Integer/Abstract/ZPow.v + theories/Numbers/Integer/Abstract/ZGcd.v + theories/Numbers/Integer/Abstract/ZLcm.v + theories/Numbers/Integer/Abstract/ZBits.v + theories/Numbers/Integer/Abstract/ZProperties.v theories/Numbers/Integer/Abstract/ZDivEucl.v theories/Numbers/Integer/Abstract/ZDivFloor.v theories/Numbers/Integer/Abstract/ZDivTrunc.v - theories/Numbers/Integer/Abstract/ZProperties.v - theories/Numbers/Integer/Abstract/ZSgnAbs.v theories/Numbers/Integer/Binary/ZBinary.v theories/Numbers/Integer/NatPairs/ZNatPairs.v theories/Numbers/Integer/SpecViaZ/ZSig.v @@ -294,17 +332,17 @@ through the <tt>Require Import</tt> command.</p> theories/Numbers/Integer/BigZ/BigZ.v theories/Numbers/Integer/BigZ/ZMake.v </dd> + </dt> <dt><b> Rational</b>: Abstract and 31-bits-words-based rational arithmetic - </dt> <dd> theories/Numbers/Rational/SpecViaQ/QSig.v theories/Numbers/Rational/BigQ/BigQ.v theories/Numbers/Rational/BigQ/QMake.v </dd> - </dl> - </dd> + </dt> + </dt> <dt> <b>Relations</b>: Relations (definitions and basic results) @@ -344,7 +382,7 @@ through the <tt>Require Import</tt> command.</p> theories/Sets/Uniset.v </dd> - <dt> <b>Classes</b>:</dt> + <dt> <b>Classes</b>: <dd> theories/Classes/Init.v theories/Classes/RelationClasses.v @@ -359,7 +397,7 @@ through the <tt>Require Import</tt> command.</p> theories/Classes/RelationPairs.v </dd> - <dt> <b>Setoids</b>:</dt> + <dt> <b>Setoids</b>: <dd> theories/Setoids/Setoid.v </dd> @@ -373,7 +411,6 @@ through the <tt>Require Import</tt> command.</p> theories/Lists/SetoidList.v theories/Lists/Streams.v theories/Lists/StreamMemo.v - theories/Lists/TheoryList.v theories/Lists/ListTactics.v </dd> diff --git a/doc/common/styles/html/simple/footer.html b/doc/stdlib/index-trailer.html index 308b1d01..308b1d01 100644 --- a/doc/common/styles/html/simple/footer.html +++ b/doc/stdlib/index-trailer.html diff --git a/doc/stdlib/make-library-files b/doc/stdlib/make-library-files index 39cedbec..c071c4a2 100755 --- a/doc/stdlib/make-library-files +++ b/doc/stdlib/make-library-files @@ -10,7 +10,7 @@ # En supposant que make fait son boulot, ca fait un tri topologique du # graphe des dépendances -LIBDIRS="Arith NArith ZArith Reals Logic Bool Lists Relations Sets Sorting Wellfounded Setoids Program Classes Numbers" +LIBDIRS="Arith PArith NArith ZArith Reals Logic Bool Lists Relations Sets Sorting Wellfounded Setoids Program Classes Numbers" rm -f library.files.ls.tmp (cd $COQSRC/theories; find $LIBDIR -name "*.v" -ls) > library.files.ls.tmp diff --git a/doc/stdlib/make-library-index b/doc/stdlib/make-library-index index c8782e93..8e496fdd 100755 --- a/doc/stdlib/make-library-index +++ b/doc/stdlib/make-library-index @@ -7,7 +7,7 @@ FILE=$1 cp -f $FILE.template tmp echo -n Building file index-list.prehtml ... -LIBDIRS="Init Logic Structures Bool Arith NArith ZArith QArith Relations Sets Classes Setoids Lists Sorting Wellfounded MSets FSets Reals Program Numbers Numbers/Natural/Abstract Numbers/Natural/Peano Numbers/Natural/Binary Numbers/Natural/BigN Numbers/Natural/SpecViaZ Numbers/Integer/Abstract Numbers/Integer/NatPairs Numbers/Integer/Binary Numbers/Integer/SpecViaZ Numbers/Integer/BigZ Numbers/NatInt Numbers/Cyclic/Abstract Numbers/Cyclic/Int31 Numbers/Cyclic/ZModulo Numbers/Cyclic/DoubleCyclic Numbers/Rational/BigQ Numbers/Rational/SpecViaQ Strings" +LIBDIRS="Init Logic Structures Bool Arith PArith NArith ZArith QArith Relations Sets Classes Setoids Lists Sorting Wellfounded MSets FSets Reals Program Numbers Numbers/Natural/Abstract Numbers/Natural/Peano Numbers/Natural/Binary Numbers/Natural/BigN Numbers/Natural/SpecViaZ Numbers/Integer/Abstract Numbers/Integer/NatPairs Numbers/Integer/Binary Numbers/Integer/SpecViaZ Numbers/Integer/BigZ Numbers/NatInt Numbers/Cyclic/Abstract Numbers/Cyclic/Int31 Numbers/Cyclic/ZModulo Numbers/Cyclic/DoubleCyclic Numbers/Rational/BigQ Numbers/Rational/SpecViaQ Strings" for k in $LIBDIRS; do i=theories/$k diff --git a/doc/tutorial/Tutorial.tex b/doc/tutorial/Tutorial.tex index 723295bf..43c8bf62 100755 --- a/doc/tutorial/Tutorial.tex +++ b/doc/tutorial/Tutorial.tex @@ -59,7 +59,7 @@ invocation of \Coq\ delivers a message such as: \begin{flushleft} \begin{verbatim} unix:~> coqtop -Welcome to Coq 8.3 (October 2010) +Welcome to Coq 8.2 (January 2009) Coq < \end{verbatim} @@ -69,7 +69,7 @@ Coq < The first line gives a banner stating the precise version of \Coq~ used. You should always return this banner when you report an anomaly to our bug-tracking system -\verb|http://coq.inria.fr/bugs| +\verb|http://logical.futurs.inria.fr/coq-bugs| \chapter{Basic Predicate Calculus} @@ -1574,4 +1574,3 @@ with \Coq, in order to acquaint yourself with various proof techniques. \end{document} -% $Id: Tutorial.tex 13547 2010-10-14 12:35:00Z notin $ |