diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-02-23 13:58:10 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-02-23 13:58:10 +0000 |
commit | 6cf8d80ac0a9869d97373d6813441eabebce8980 (patch) | |
tree | 0bd1913284ed77113594ac47298410add66d10c1 /doc | |
parent | 2da65b20770536729fbff86ec67429d0fe74e145 (diff) |
Nettoyage de l'archive doc et restructuration avant intégration à l'archive
principale de Coq et publication des sources (HH)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8606 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc')
-rwxr-xr-x | doc/Anomalies.tex | 34 | ||||
-rw-r--r-- | doc/Changes.html | 126 | ||||
-rwxr-xr-x | doc/Changes.tex | 24 | ||||
-rwxr-xr-x | doc/ChangesV6-2.tex | 921 | ||||
-rw-r--r-- | doc/ChangesV6-3-1.tex | 160 | ||||
-rw-r--r-- | doc/ChangesV6-3.tex | 302 | ||||
-rwxr-xr-x | doc/ChangesV7-0.tex | 757 | ||||
-rw-r--r-- | doc/Correctness.tex | 930 | ||||
-rw-r--r-- | doc/INSTALL | 65 | ||||
-rw-r--r-- | doc/LICENCE | 606 | ||||
-rw-r--r-- | doc/Makefile.rt | 43 | ||||
-rw-r--r-- | doc/Program.tex | 850 | ||||
-rwxr-xr-x | doc/Recursive-Definition.tex | 251 | ||||
-rw-r--r-- | doc/RefMan.txt | 74 | ||||
-rw-r--r-- | doc/book-html.sty | 133 | ||||
-rwxr-xr-x | doc/common/macros.tex (renamed from doc/macros.tex) | 0 | ||||
-rwxr-xr-x | doc/common/title.tex (renamed from doc/title.tex) | 0 | ||||
-rw-r--r-- | doc/coq-html.sty | 6 | ||||
-rw-r--r-- | doc/discussion-syntaxe.txt | 349 | ||||
-rw-r--r-- | doc/faq.tex | 800 | ||||
-rw-r--r-- | doc/faq/FAQ.tex (renamed from doc/newfaq/main.tex) | 0 | ||||
-rw-r--r-- | doc/faq/axioms.eps (renamed from doc/newfaq/axioms.eps) | 0 | ||||
-rw-r--r-- | doc/faq/axioms.fig (renamed from doc/newfaq/axioms.fig) | 0 | ||||
-rw-r--r-- | doc/faq/axioms.png | bin | 0 -> 10075 bytes | |||
-rw-r--r-- | doc/faq/fk.bib (renamed from doc/newfaq/fk.bib) | 0 | ||||
-rw-r--r-- | doc/faq/hevea.sty | 78 | ||||
-rw-r--r-- | doc/faq/interval_discr.v (renamed from doc/newfaq/interval_discr.v) | 0 | ||||
-rw-r--r-- | doc/main.html | 13 | ||||
-rw-r--r-- | doc/newfaq/faq.cls | 70 | ||||
-rw-r--r-- | doc/newfaq/faq.sty | 883 | ||||
-rw-r--r-- | doc/newfaq/main.v001.gif | 0 | ||||
-rwxr-xr-x | doc/newfaq/run.sh | 6 | ||||
-rw-r--r-- | doc/refman/AddRefMan-pre.tex (renamed from doc/AddRefMan-pre.tex) | 0 | ||||
-rw-r--r-- | doc/refman/Cases.tex (renamed from doc/Cases.tex) | 0 | ||||
-rw-r--r-- | doc/refman/Coercion.tex (renamed from doc/Coercion.tex) | 0 | ||||
-rwxr-xr-x | doc/refman/Extraction.tex (renamed from doc/Extraction.tex) | 0 | ||||
-rw-r--r-- | doc/refman/Helm.tex (renamed from doc/Helm.tex) | 0 | ||||
-rwxr-xr-x | doc/refman/Natural.tex (renamed from doc/Natural.tex) | 0 | ||||
-rwxr-xr-x | doc/refman/Omega.tex (renamed from doc/Omega.tex) | 0 | ||||
-rw-r--r-- | doc/refman/Polynom.tex (renamed from doc/Polynom.tex) | 0 | ||||
-rwxr-xr-x | doc/refman/RefMan-add.tex (renamed from doc/RefMan-add.tex) | 0 | ||||
-rwxr-xr-x | doc/refman/RefMan-cas.tex (renamed from doc/RefMan-cas.tex) | 0 | ||||
-rwxr-xr-x | doc/refman/RefMan-cic.tex (renamed from doc/RefMan-cic.tex) | 0 | ||||
-rwxr-xr-x | doc/refman/RefMan-coi.tex (renamed from doc/RefMan-coi.tex) | 0 | ||||
-rwxr-xr-x | doc/refman/RefMan-com.tex (renamed from doc/RefMan-com.tex) | 0 | ||||
-rw-r--r-- | doc/refman/RefMan-ext.tex (renamed from doc/RefMan-ext.tex) | 0 | ||||
-rw-r--r-- | doc/refman/RefMan-gal.tex (renamed from doc/RefMan-gal.tex) | 0 | ||||
-rw-r--r-- | doc/refman/RefMan-ide.tex (renamed from doc/RefMan-ide.tex) | 0 | ||||
-rwxr-xr-x | doc/refman/RefMan-ind.tex (renamed from doc/RefMan-ind.tex) | 0 | ||||
-rwxr-xr-x | doc/refman/RefMan-int.tex (renamed from doc/RefMan-int.tex) | 0 | ||||
-rwxr-xr-x | doc/refman/RefMan-lib.tex (renamed from doc/RefMan-lib.tex) | 0 | ||||
-rw-r--r-- | doc/refman/RefMan-ltac.tex (renamed from doc/RefMan-ltac.tex) | 0 | ||||
-rw-r--r-- | doc/refman/RefMan-mod.tex (renamed from doc/RefMan-mod.tex) | 0 | ||||
-rw-r--r-- | doc/refman/RefMan-modr.tex (renamed from doc/RefMan-modr.tex) | 0 | ||||
-rw-r--r-- | doc/refman/RefMan-oth.tex (renamed from doc/RefMan-oth.tex) | 0 | ||||
-rwxr-xr-x | doc/refman/RefMan-pre.tex (renamed from doc/RefMan-pre.tex) | 0 | ||||
-rwxr-xr-x | doc/refman/RefMan-pro.tex (renamed from doc/RefMan-pro.tex) | 0 | ||||
-rwxr-xr-x | doc/refman/RefMan-syn.tex (renamed from doc/RefMan-syn.tex) | 0 | ||||
-rw-r--r-- | doc/refman/RefMan-tac.tex (renamed from doc/RefMan-tac.tex) | 0 | ||||
-rw-r--r-- | doc/refman/RefMan-tacex.tex (renamed from doc/RefMan-tacex.tex) | 0 | ||||
-rwxr-xr-x | doc/refman/RefMan-tus.tex (renamed from doc/RefMan-tus.tex) | 0 | ||||
-rwxr-xr-x | doc/refman/RefMan-uti.tex (renamed from doc/RefMan-uti.tex) | 0 | ||||
-rw-r--r-- | doc/refman/Reference-Manual.tex (renamed from doc/Reference-Manual.tex) | 0 | ||||
-rw-r--r-- | doc/refman/Setoid.tex (renamed from doc/Setoid.tex) | 0 | ||||
-rwxr-xr-x | doc/refman/biblio.bib (renamed from doc/biblio.bib) | 0 | ||||
-rw-r--r-- | doc/refman/coqdoc.tex (renamed from doc/coqdoc.tex) | 0 | ||||
-rw-r--r-- | doc/refman/coqide-queries.png (renamed from doc/coqide-queries.png) | bin | 27316 -> 27316 bytes | |||
-rw-r--r-- | doc/refman/coqide.png (renamed from doc/coqide.png) | bin | 20953 -> 20953 bytes | |||
-rw-r--r-- | doc/refman/cover.html (renamed from doc/cover.html) | 0 | ||||
-rw-r--r-- | doc/refman/headers.tex (renamed from doc/headers.tex) | 0 | ||||
-rw-r--r-- | doc/refman/hevea.sty | 78 | ||||
-rw-r--r-- | doc/refman/index.html (renamed from doc/main-0.html) | 0 | ||||
-rw-r--r-- | doc/rt/RefMan-cover.tex (renamed from doc/RefMan-cover.tex) | 0 | ||||
-rw-r--r-- | doc/rt/Tutorial-cover.tex (renamed from doc/Tutorial-cover.tex) | 0 | ||||
-rwxr-xr-x | doc/stdlib/Library.tex (renamed from doc/Library.tex) | 0 | ||||
-rw-r--r-- | doc/syntax.txt | 68 | ||||
-rw-r--r-- | doc/tools/Translator.tex (renamed from doc/Translator.tex) | 0 | ||||
-rwxr-xr-x | doc/tov8 | 5 | ||||
-rw-r--r-- | doc/tradv8.ml4 | 105 | ||||
-rwxr-xr-x | doc/tutorial/Tutorial.tex (renamed from doc/Tutorial.tex) | 0 | ||||
-rw-r--r-- | doc/v8.txt | 50 |
81 files changed, 870 insertions, 6917 deletions
diff --git a/doc/Anomalies.tex b/doc/Anomalies.tex deleted file mode 100755 index a21577db0..000000000 --- a/doc/Anomalies.tex +++ /dev/null @@ -1,34 +0,0 @@ -\documentclass[11pt]{article} - -\input{./title} - -\title{Known bugs of \Coq{} V6.2} -\author{\ } -\begin{document} -\maketitle - -\begin{itemize} - -\item {\tt Program} may fail to build pattern in {\tt Cases} -expressions. Instead an old style {\tt Case} expression without -patterns is generated. - -\item The option {\tt Set Printing Synth} sometimes fails to decide if -a elimination predicates is synthetisable. If a term printed without -the elimination predicate is not correctly re-interpreted by Coq, then -turn off the {\tt Printing Synth} mode. - -\item {\tt Unfold} and {\tt Pattern} may incorrectly number the -occurrences of constants or subterms when {\tt Cases} expression are involved. - -\item \texttt{Transparent} and \texttt{Opaque} are not synchronous - with the \texttt{Reset} mecanism. If a constant was transparent at - point \texttt{A}, if you set it opaque and do \texttt{Reset A}, it - is still opaque and that may cause problems if you try to replay - tactic scripts between \texttt{A} and the current point. - -\end{itemize} - -\end{document} - -% $Id$ diff --git a/doc/Changes.html b/doc/Changes.html deleted file mode 100644 index 87082c6b8..000000000 --- a/doc/Changes.html +++ /dev/null @@ -1,126 +0,0 @@ -<HTML> -<body bgcolor=white> -<BR> -<b><font size=18>Changes from V7.3 to V7.3.1</font></b> -<BR> - -<H3>Bug fixes</H3> -<UL> -<LI> Corrupted Field tactic and Match Context tactic construction fixed -<LI> Checking of names already existing in Assert added (PR#182) -<LI> Invalid argument bug in Exact tactic solved (PR#183) -<LI> Colliding bound names bug fixed (PR#202) -<LI> Wrong non-recursivity test for Record fixed (PR#189) -<LI> Out of memory/seg fault bug related to parametric inductive fixed (PR#195) -<LI> Setoid_replace/Setoid_rewrite bug wrt "==" fixed -</UL> - -<H3>Miscellaneous</H3> -<UL> -<LI> Ocaml version >= 3.06 is needed to compile Coq from sources -<LI> Simplification of fresh names creation strategy for Assert, Pose and - LetTac (PR#192) -</UL> - -<BR> -<b><font size=18>Changes from V7.2 to V7.3</font></b> -<BR> - -<H3>Language</H3> -<UL> -<LI> Slightly improved compilation of pattern-matching (slight source of - incompatibilities) -<LI> Record's now accept anonymous fields "_" which does not build projections -<LI> Changes in the allowed elimination sorts for certain class of inductive - definitions : an inductive definition without constructors - of Sort Prop can be eliminated on sorts Set and Type A "singleton" - inductive definition (one constructor with arguments in the sort Prop - like conjunction of two propositions or equality) can be eliminated - directly on sort Type (In V7.2, only the sorts Prop and Set were allowed) -</UL> - -<H3>Tactics</H3> -<UL> -<LI> New tactic "Rename x into y" for renaming hypotheses -<LI> New tactics "Pose x:=u" and "Pose u" to add definitions to local context -<LI> Pattern now working on partially applied subterms -<LI> Ring no longer applies irreversible congruence laws of mult but - better applies congruence laws of plus (slight source of incompatibilities). -<LI> Intuition does no longer unfold constants except "<->" and "~". It - can be parameterized by a tactic. It also can introduce dependent - product if needed (source of incompatibilities) -<LI> "Match Context" now matching more recent hypotheses first and failing only - on user errors and Fail tactic (possible source of incompatibilities) -<LI> Tactic Definition's without arguments now allowed in Coq states -<LI> Better simplification and discrimination made by Inversion (source - of incompatibilities) -</UL> - -<H3>Bugs</H3> -<UL> -<LI> "Intros H" now working like "Intro H" trying first to reduce if not a product -<LI> Forward dependencies in Cases now taken into account -<LI> Known bugs related to Inversion and let-in's fixed -<LI> Bug unexpected Delta with let-in now fixed -</UL> - -<H3>Extraction (details in contrib/extraction/CHANGES or documentation)</H3> -<UL> -<LI> Signatures of extracted terms are now mostly expunged from dummy arguments. -<LI> Haskell extraction is now operational (tested & debugged). -</UL> - -<H3>Standard library</H3> -<UL> -<LI> Some additions in [ZArith]: three files (Zcomplements.v, Zpower.v - and Zlogarithms.v) moved from contrib/omega in order to be more - visible, one Zsgn function, more induction principles (Wf_Z.v and - tail of Zcomplements.v), one more general Euclid theorem -<LI> Peano_dec.v and Compare_dec.v now part of Arith.v -</UL> - -<H3>Tools</H3> -<UL> -<LI> new option -dump-glob to coqtop to dump globalizations (to be used by the - new documentation tool coqdoc; see http://www.lri.fr/~filliatr/coqdoc) -</UL> - -<H3>User Contributions</H3> -<UL> -<LI> CongruenceClosure (congruence closure decision procedure) -<LI> MapleMode (an interface to embed Maple simplification procedures in Coq) -<LI> Presburger (a formalization of Presburger's algorithm as stated in the initial paper by Presburger) -<LI> Chinese has been rewritten using Z from ZArith as datatype - ZChinese is the new version, Chinese the obsolete one -</UL> - -<H3>Incompatibilities</H3> -<UL> -<LI> Ring: exceptional incompatibilities (1 above 650 in submitted user - contribs, leading to a simplification) -<LI> Intuition: does not unfold any definition except "<->" and "~" -<LI> Cases: removal of some extra Cases in configurations of the form - "Cases ... of C _ => ... | _ D => ..." (effects on 2 definitions of - submitted user contributions necessitating the removal of now superfluous - proof steps in 3 different proofs) -<LI> Match Context, in case of incompatibilities because of a now non - trapped error (e.g. Not_found or Failure), use instead tactic Fail - to force Match Context trying the next clause -<LI> Inversion: better simplification and discrimination may occasionally - lead to less subgoals and/or hypotheses and different naming of hypotheses -<LI> Unification done by Apply/Elim has been changed and may exceptionally lead - to incompatible instantiations -<LI> Peano_dec.v and Compare_dec.v parts of Arith.v make Auto more - powerful if these files were not already required (1 occurrence of - this in submitted user contribs) -</UL> - -<BR><BR> -<HR> -<BR> - -<a href="ftp://ftp.inria.fr/INRIA/coq/V7.2/doc/Changes.html">Previous changes (from Coq V7.1 to V7.2)</a> -<BR> - -</BODY> -</HTML> diff --git a/doc/Changes.tex b/doc/Changes.tex deleted file mode 100755 index dec509651..000000000 --- a/doc/Changes.tex +++ /dev/null @@ -1,24 +0,0 @@ -\documentclass[11pt]{article} -\usepackage[latin1]{inputenc} -\usepackage[T1]{fontenc} - -\input{./title} -\input{./macros} - -\begin{document} - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% Changes 6.3.1 ===> 7.0 & 7.1 -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\shorttitle{Changes from {\Coq} V6.3.1 to {\Coq} V7.0 and V7.1} - -\end{document} - -% Local Variables: -% mode: LaTeX -% TeX-master: t -% End: - - -% $Id$ - diff --git a/doc/ChangesV6-2.tex b/doc/ChangesV6-2.tex deleted file mode 100755 index 3a0f7ef17..000000000 --- a/doc/ChangesV6-2.tex +++ /dev/null @@ -1,921 +0,0 @@ -\documentclass[11pt]{article} -\usepackage[latin1]{inputenc} -\usepackage[T1]{fontenc} - -\input{./title} -\input{./macros} - -\begin{document} - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% Changes 6.1 ===> 6.2 -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\coverpage{Changes from {\Coq} V6.1 to {\Coq} V6.2}{\ } - -This document describes the main differences between Coq V6.1 and -V6.2. This new version of Coq is characterized by an acceleration of -parsing, loading and reduction, by a more user-friendly syntax, and by -new tactics and management tools. -We refer to the reference manual -for a more precise description of the new features. - -See the ASCII file \texttt{CHANGES} available by FTP with \Coq\ for -the minor changes of the bug-fix releases 6.2.1 and 6.2.2. - - -\section{Changes overview} - -\begin{itemize} - -\item \textbf{Syntax} - -\begin{description} - - \item[New syntax for defining parsing and pretty-printing rules.]{\ - - The \texttt{Grammar} and - \texttt{Syntax} declarations are more readable and more symmetric.} - - \item[\texttt{Cases} vs \texttt{Case}]{\ - - The constructions defined by cases are - now printed with the ML-style \texttt{Cases} syntax. The - \texttt{Case} syntax should no longer be used.} - - \item[New syntax for the existential and universal quantifiers.]{\ - - \texttt{(EX x:A | P)}, \texttt{(EX x| P)}, \texttt{(EX x:A | P \& - Q)}, \texttt{(EX x | P \& Q)}, - \texttt{(ALL x:A | P)} and - \texttt{(ALL x | P)} are alternative - syntax for \texttt{(Ex [x:A]P)}, \texttt{(Ex2 [x:A]P [x:A]Q)} - and \texttt{(All [x:A]P)}, the syntax \texttt{<A>Ex(P), - <A>Ex(P,Q)} and \texttt{<A>All(P)} are no longer supported.} - - \item[Natural syntax for the ... naturals.]{\ - - With the {\tt Arith} theory, you can - now type \texttt{(3)} for \texttt{(S (S (S O)))}}. - - \item[Natural syntax for expressions of integer arithmetic.]{\ - - With the {\tt ZArith} theory, you can - type e.g. \texttt{`3 <= x - 4 < 7`}.} - -\end{description} - -\item \textbf{Tactics} - - \begin{itemize} - - \item New mechanism to define parameterized tactics (see - section~\ref{parameterised}). - - \item New tactic \texttt{Decompose} to decompose a - complex proposition in atomic ones (see - section~\ref{decompose}). - - \item New tactics \texttt{Decide Equality} and - \texttt{Compare} for deciding the equality of two - inductive objects. - - \item \texttt{Intros} has been extended such that it takes arguments - denoting patterns and accordingly to this patterns, performs decomposition of arguments ranging - over inductive definitions as well as introduction (see section~\ref{intros}). - - \item \texttt{Tauto} is extended to - work also on connectives defined by the user and on informative - types (see section~\ref{tauto}). - - \item The {\bf equality} tactics, especially \texttt{Rewrite}, - \texttt{Transitivity}, \texttt{Symmetry} and \texttt{Reflexivity}, - works now independently of the universe that the equality - inhabits (see section~\ref{equality}). - - \item New experimental tactic \texttt{Refine}: a kind of - \texttt{exact} with typed holes that are transformed into - subgoals (see - section~\ref{refine}). - - \item The tactical \texttt{Abstract} allow to automatically - divide a big proof into smaller lemmas. It may improve the - efficiency of the \texttt{Save} procedure (see section~\ref{abstract}). - - \item The tactics \texttt{Rewrite} and \texttt{Rewrite in} now - accept bindings as tactics \texttt{Apply} and \texttt{Elim}. - - \item The tactic \texttt{Rewrite} now fails when no rewriting can be - done. So you must use \texttt{Try Rewrite} to get the old behavior. - - \end{itemize} - -\item \textbf{New toplevel commands.} - - \begin{description} - - \item[Precise location of errors.]{\ - - At toplevel, when possible, \Coq\ - underlines the portion of erroneous vernac source. When compiling, - it tells the line and characters where the error took place. The - output is compatible with the \texttt{next-error} mechanism of GNU - Emacs.} - - \item[New reduction functions.]{\ - A more precise control on what is reduced is now - possible in tactics. All toplevel reductions are performed through the - \texttt{Eval} command. The commands \texttt{Compute} and - \texttt{Simplify} do not exist any longer, they are replaced by - the commands \texttt{Eval Compute in} and \texttt{Eval Simpl in}. - In addition, - \texttt{Eval} now takes into consideration the hypotheses of the - current goal in order to type-check the term to be reduced - (see section~\ref{reductions}).} - - \end{description} - -\item \textbf{Libraries} - - \begin{description} - - \item[Arithmetic on Z.]{\ - - Pierre Cr\'egut's arithmetical library on integers (the set Z) is now - integrated to the standard library. - \texttt{ZArith} contains basic - definitions, theorems, and syntax rules that allow users of \texttt{ZArith} - to write formulas such as $3+(x*y) < z \le 3+(x*y+1)$ in the - natural way~(see section~\ref{zarith}). - } - - \item[\texttt{SearchIsos} : a tool to search through the standard library]{ - - The \texttt{SearchIsos} tool se\-arches terms by their - types and modulo type isomorphisms. There are two ways to use - \texttt{SearchIsos}: - - \begin{itemize} - \item Search a theorem in the current environment with the new - \texttt{SearchIsos} command in an interactive session - \item Search a theorem in the whole Library using the external tool - \texttt{coqtop -searchisos} - \end{itemize} } - - \item The \texttt{Locate} vernac command can now locate the - module in which a term is defined in a \texttt{coqtop} session. You can - also ask for the exact location of a file or a module that lies - somewhere in the load path. - -\end{description} - -\item \textbf{Extraction} - - \begin{description} - - \item Extraction to Haskell available - - \end{description} - -\item \textbf{Improved Coq efficiency} - - \begin{description} - - \item[Parsing] - - Thanks to a new grammar implementation based on Daniel de - Rauglaudre's Camlp4 system, parsing is now several times faster. The - report of syntax errors is more precise. - - \item[Cleaning up the tactics source]{\ - - Source code of the tactics has been revisited, so that the user can - implement his/her own tactics more easily. The internal ML names - for tactics have been normalized, and they are organized in - different files. See chapter ``Writing your own tactics'' in the - Coq reference manual.} - - \end{description} - -\item \textbf{Incompatibilities} - - You could have to modify your vernacular source for the following - reasons: - - \begin{itemize} - - \item You use the name \texttt{Sum} which is now a keyword. - \item You use the syntax \texttt{<A>Ex(P)}, \texttt{<A>Ex2(P,Q)} or - \texttt{<A>All(P)}. - - \item You use Coq \texttt{Grammar} or \texttt{Syntax} commands. - In this case, see section - \ref{parsing-printing} to know how to modify your parsing or printing - rules. - - \item You use Coq \texttt{Call} to apply a tactic abbreviation - declared using \texttt{Tactic Definition}. These tactics can be - directly called, just remove the \texttt{Call} prefix. - - \item \texttt{Require} semantics. The Coq V6.1 \texttt{Require} - command did not behave as described in the reference manual. - It has been corrected.\\ - The Coq V6.2 behavior is now the following. - Assume a file \texttt{A} containing a - command \texttt{Require B} is compiled. Then the command - \texttt{Require A} loads the module \texttt{B} but the definitions - in \texttt{B} are not visible. In order to see theses definitions, - a further \texttt{Require B} is - needed or you should write \texttt{Require Export B} instead of - \texttt{Require B} inside the file \texttt{A}. \\ - The Coq V6.1 behavior of \texttt{Require} was equivalent to the - Coq V6.2 \texttt{Require Export} command. - \item \texttt{Print Hint} now works only in proof mode and displays - the hints that apply to the current goal. \texttt{Print Hint *} - works as the old \texttt{Print Hint} command and displays the complete - hints table. - - \end{itemize} - - In addition, it is strongly recommended to use now the {\tt Cases} - pattern-matching operator rather than the intended to disappear {\tt - Case} operator. - -\item \textbf{Documentation} - The Reference Manual has been rearranged and - updated. The chapters on syntactic extensions, and user-defined - tactics have been completely rewritten. - - \begin{itemize} - \item We made a big effort to make the Reference Manual better and - more precise. The paper documentation is now divided in three - parts: - \begin{enumerate} - \item The Reference Manual, that documents the language (part I), - a brief explanation of each command and tactic (part II), the - users extensions for syntax and tactics (part III), the tools - (part IV); - - \item The Addendum to Reference Manual (part V), that contains - more detailed explanations about extraction, printing proofs in - natural language, tactics such as Omega, Ring and Program, - coercions and Cases compilation. - - \item The Tutorial, an introduction to Coq for the new user, that - has not much changed - \end{enumerate} - - \item The Hyper-Text documentation has been much improved. Please - check our web page \verb!http://pauillac.inria.fr/coq!. It is - possible to perform searches in the standard Library by name or by - type (with SearchIsos), and of course to read the HTML version - of the documentation. - \end{itemize} - -\end{itemize} - -\section{New tactics} - - -\subsection{Proof of imperative programs} - -A new tactic to establish correctness and termination of imperative -(and functional) programs is now available, in the \Coq\ module -\texttt{Programs}. This tactic, called \texttt{Correctness}, is -described in the chapter 18 of the \Coq\ Reference Manual. - - -\subsection{Defining parameterized tactics} -\label{parameterised} -It is possible to define tactics macros, taking terms as arguments -using the \texttt{Tactic Definition} command. - -These macros can be called directly (in Coq V6.1, a prefix -\texttt{Call} was used). -Example: - -\begin{coq_example*} -Tactic Definition DecideEq [$a $b] := - [<:tactic:< - Destruct $a; - Destruct $b; - Auto; - (Left;Discriminate) Orelse (Right;Discriminate)>>]. -Inductive Set Color := Blue:Color | White:Color | Red:Color | Black:Color. -\end{coq_example*} - -\begin{coq_example} -Theorem eqColor: (c1,c2:Color){c1=c2}+{~c1=c2}. -DecideEq c1 c2. -\end{coq_example} -\begin{coq_example*} -Qed. -\end{coq_example*} - -\subsection{Intros}\label{intros} -The tactic \texttt{Intros} can now take a pattern as argument. A -pattern is either -\begin{itemize} -\item a variable -\item a list of patterns : $p_1~\ldots~p_n$ -\item a disjunction of patterns : $[p_1~|~~\ldots~|~p_n]$ -\item a conjunction of patterns : $(p_1,\ldots,p_n)$ -\end{itemize} - -The behavior of \texttt{Intros} is defined inductively over the -structure of the pattern given as argument: -\begin{itemize} -\item introduction on a variable behaves like before; -\item introduction over a -list of patterns $p_1~\ldots~p_n$ is equivalent to the sequence of -introductions over the patterns namely : -\texttt{Intros $p_1$;\ldots; Intros $p_n$}, the goal should start with -at least $n$ products; -\item introduction over a -disjunction of patterns $[p_1~|~~\ldots~|~p_n]$, it -introduces a new variable $X$, its type should be an inductive definition with $n$ -constructors, then it performs a case analysis over $X$ -(which generates $n$ subgoals), it -clears $X$ and performs on each generated subgoals the corresponding -\texttt{Intros}~$p_i$ tactic; -\item introduction over a -conjunction of patterns $(p_1,\ldots,p_n)$, it -introduces a new variable $X$, its type should be an inductive definition with $1$ -constructor with (at least) $n$ arguments, then it performs a case analysis over $X$ -(which generates $1$ subgoal with at least $n$ products), it -clears $X$ and performs an introduction over the list of patterns $p_1~\ldots~p_n$. -\end{itemize} -\begin{coq_example} -Lemma intros_test : (A,B,C:Prop)(A\/(B/\C))->(A->C)->C. -Intros A B C [a|(b,c)] f. -Apply (f a). -Proof c. -\end{coq_example} -\subsection{Refine}\label{refine} -This tactics takes a term with holes as argument. - -It is still experimental and not automatically loaded. It can -be dynamically loaded if you use the byte-code version of Coq; -with the version in native code, you have to use the \texttt{-full} option. - -\Example -\begin{coq_example*} -Require Refine. -Inductive Option: Set := Fail : Option | Ok : bool->Option. -\end{coq_example} -\begin{coq_example} -Definition get: (x:Option)~x=Fail->bool. -Refine - [x:Option]<[x:Option]~x=Fail->bool>Cases x of - Fail => ? - | (Ok b) => [_:?]b end. -Intros;Absurd Fail=Fail;Trivial. -\end{coq_example} -\begin{coq_example*} -Defined. -\end{coq_example*} - -\subsection{Decompose}\label{decompose} -This tactic allows to recursively decompose a -complex proposition in order to obtain atomic ones. -Example: - -\begin{coq_eval} -Reset Initial. -\end{coq_eval} -\begin{coq_example} -Lemma ex1: (A,B,C:Prop)(A/\B/\C \/ B/\C \/ C/\A) -> C. -Intros A B C H; Decompose [and or] H; Assumption. -\end{coq_example} -\begin{coq_example*} -Qed. -\end{coq_example*} - - -\subsection{Tauto}\label{tauto} -This tactic has been extended to work also on -connectives defined by the user as well as on informative types. -Example: - -\begin{coq_example*} -Inductive AND4 [A:Set;B,C,D:Prop] : Set := - tuple4 : A->B->C->D->(AND4 A B C D). -\end{coq_example*} -\begin{coq_example} -Lemma ex2: (B,C,D:Prop)(AND4 nat B C D)->(AND4 nat C D B). -Tauto. -\end{coq_example} -\begin{coq_example*} -Qed. -\end{coq_example*} - -\subsection{Tactics about Equality}\label{equality} -\texttt{Rewrite}, \texttt{Transitivity}, \texttt{Symmetry}, -\texttt{Reflexivity} and other tactics associated to equality predicates work -now independently of the universe that the equality inhabits. -Example: - -\begin{coq_example*} -Inductive EQ [A:Type] : Type->Prop := reflEQ : (EQ A A). -\end{coq_example*} -\begin{coq_example} -Lemma sym_EQ: (A,B:Type)(EQ A B)->(EQ B A). -Intros;Symmetry;Assumption. -\end{coq_example} -\begin{coq_example*} -Qed. -\end{coq_example*} - -\begin{coq_example} -Lemma trans_idT: (A,B:Type)(A===Set)->(B===Set)->A===B. -Intros A B X Y;Rewrite X;Symmetry;Assumption. -\end{coq_example} -\begin{coq_example*} -Qed. -\end{coq_example*} - - -\subsection{The tactical \texttt{Abstract}}~\label{abstract} -From outside, typing \texttt{Abstract \tac} is the same that -typing \tac. If \tac{} completely solves the current goal, it saves an auxiliary lemma called -{\ident}\texttt{\_subproof}\textit{n} where {\ident} is the name of the -current goal and \textit{n} is chosen so that this is a fresh -name. This lemma is a proof of the current goal, generalized over the -local hypotheses. - -This tactical is useful with tactics such that \texttt{Omega} and -\texttt{Discriminate} that generate big proof terms. With that tool -the user can avoid the explosion at time of the \texttt{Save} command -without having to cut ``by hand'' the proof in smaller lemmas. - -\begin{Variants} -\item \texttt{Abstract {\tac} using {\ident}}. Gives explicitly the - name of the auxiliary lemma. -\end{Variants} -\begin{coq_example*} -Lemma abstract_test : (A,B:Prop)A/\B -> A\/B. -\end{coq_example*} -\begin{coq_example} -Intros. -Abstract Tauto using sub_proof. -Check sub_proof. -\end{coq_example} -\begin{coq_example*} -Qed. -\end{coq_example*} -\begin{coq_example} -Print abstract_test. -\end{coq_example} - - -\subsection{Conditional $tac$ Rewrite $c$} -This tactics acts as \texttt{Rewrite} and applies a given tactic on the -subgoals corresponding to conditions of the rewriting. -See the Reference Manual for more details. - - -\section{Changes in concrete syntax} - -\subsection{The natural grammar for arithmetic} -\label{zarith} -There is a new syntax of signed integer arithmetic. However the -syntax delimiters were \verb=[|= and \verb=|]= in the beta-version. In -the final release of 6.2, it's two back-quotes \texttt{`} and \texttt{`}. - -Here is an example: -\begin{coq_eval} -Reset Initial. -\end{coq_eval} - -\begin{coq_example*} -Require ZArith. -Variables x,y,z:Z. -Variables f,g:Z->Z. -\end{coq_example*} -\begin{coq_example} -Check ` 23 + (f x)*45 - 34 `. -Check Zplus_sym. -Check ` x < (g y) <= z+3 `. -Check ` 3+ [if true then ` 4 ` else (f x)] `. -SearchIsos (x,y,z:Z) ` x+(y+z) = (x+y)+z `. -\end{coq_example} - -\begin{coq_eval} -Reset x. -\end{coq_eval} - -Arithmetic expressions are enclosed between \verb=`= and \verb=`=. It can -be: -\begin{itemize} -\item integers -\item any of the operators \verb|+|, \verb|-| and \verb|*| -\item functional application -\item any of the relations \verb|<|, \verb|<=|, \verb|>=|, \verb|>|, -\verb|=| and \verb|<>| -\end{itemize} - -Inside an arithmetic expression, you can type an arbitrary Coq -expression provided it is escaped with \verb|[ ]|. There is also -shortcuts such as $x < y \le z$ which means $x<y \wedge y \le z$. - -\begin{coq_example} -Lemma ex3 : (x:Z)` x>0 ` -> ` x <= 2*x <= 4*x `. -Split. -\end{coq_example} -\begin{coq_eval} -Abort. -\end{coq_eval} -\subsection{The new \texttt{Grammar} and \texttt{Syntax}} -\label{parsing-printing} - -The leading idea in the {\tt Grammar} and {\tt Syntax} command syntax -changes is to unify and simplify them. - -\subsubsection{Syntax changes for \texttt{Grammar} declarations (parsing rules)} - -Each \texttt{Grammar} rule now needs to be named, as \texttt{Syntax} -rules do. Although they are just comments, it is advised to use distinct -names for rules. - -The syntax of an ordinary grammar rule is now: - -\[ -\texttt{Grammar}~\textit{GrammarName}~\textit{EntryName}~\texttt{:=}~ - \textit{RuleName}~ \texttt{[} \textit{Pattern} \texttt{] -> [} \textit{Action} -\texttt{]}. -\] -\paragraph{Parametric rules} - -Parametric grammars does not exist any longer. Their main use was to -write left associative rules. For that, there is a simplest way based -on a new grammar builder \texttt{LEFTA} (and grammar builder -\texttt{RIGHTA} and \texttt{NONA} as well). - -For instance, the grammar in V6.1 style - -\begin{verbatim} -Grammar natural fact := - [ final($c) factprod[[$c]]($r) ] -> [$r]. - -Grammar natural factprod[$p] := - [ ] -> [$p] -| [ "*" final($c) factprod[[<<(mult $p $c)>>]]($r)] -> [$r]. -\end{verbatim} -should now be written -\begin{verbatim} -Grammar natural fact := - LEFTA - fact_final [ final($c) ] -> [$c] - | fact_prod [ final($p) "*" final($c) ] -> [ <<(mult $p $c)>> ]. -\end{verbatim} - -\subsubsection{Internal abstract syntax tree (ast) changes} - -The syntax of internal abstract syntax tree (ast) has also been -modified. Most users, which only uses \verb|<<| ... \verb|>>| in the -right-hand side of the grammar rules are not concerned with that. -For the others, it should be noted that now there are two kinds of -production for grammar rules: ast and lists of asts. - -A rule that produces a list of asts should be declared of this type by -inserting ``\texttt{:List}'' just after the grammar name. - -The ast constructors \verb!$CONS!, \verb!$NIL!, \verb!$APPEND!, -\verb!$PRIM!, \verb!SOME! and \verb!$OPER! do not -exist any longer. A simple juxtaposition is used to build ast lists. -For an empty -list, just put nothing. The old \verb!($OPER{Foo} ($CONS $c1 $c2))! -becomes \verb!(Foo $c1 $c2)!. The old \verb!$SLAML! is now \verb!$SLAM!. - -The constructor \verb!$LIST! has a new meaning. It serves to cast an -ast list variable into an ast. - -For instance, the following grammar rules in V6.1 style: -\begin{verbatim} -Grammar vernac eqns := - [ "|" ne_command_list($ts) "=>" command($u) eqns($es) ] - -> [($CONS ($OPER{COMMANDLIST} ($CONS $u $ts)) $es)]. -| [ ] -> [($LIST)] - -with vernac := - [ "Foo" "Definition" identarg($idf) command($c) ":=" eqns($eqs) "." ] - -> [($OPER{FooDefinition} ($CONS $idf ($CONS $c $eqs)))] -\end{verbatim} -can be written like this in V6.2 -\begin{verbatim} -Grammar vernac eqns : List := - eqns_cons [ "|" ne_command_list($ts) "=>" command($u) eqns($es) ] - -> [ (COMMANDLIST $u ($LIST $ts)) ($LIST $es)] -| eqns_nil [ ] -> [ ]. - -with vernac := - rec_def [ "Foo" "Definition" identarg($idf) command($c) ":=" eqns($eqs) "." ] - -> [(FooDefinition $idf $c ($LIST $eqs))]. -\end{verbatim} - - -\subsubsection{Syntax changes for \texttt{Syntax} declarations - (printing rules)} - -The new syntax for printing rules follows the one for parsing rules. In -addition, there are indications of associativity, precedences and -formatting. - -Rules are classified by strength: the keyword is \verb-level-. The -non-terminal items are written in a simplest way: a non-terminal -\verb!<$t:dummy-name:*>! is now just written \verb!$t!. For left or -right associativity, the modifiers \verb!:L! or - \verb!:E! have to be given as in \verb!$t:E!. The expression \verb!$t:L! prints the -ast \verb!$t! with a level strictly lower than the current one. -The expression \verb!$t:E! calls the printer with the same level. Thus, for left -associative operators, the left term must be called with \verb!:E!, and the -right one with \verb!:L!. It is the opposite for the right associative -operators. Non associative operators use \verb!:L! for both sub-terms. - -For instance, the following rules in V6.1 syntax - -\begin{verbatim} -Syntax constr Zplus <<(Zplus $n1 $n2)>> 8 - [<hov 0> "`" <$nn1:"dummy":E> "+" <$n2:"dummy":L> "`" ] - with $nn1 := (ZEXPR $n1) $nn2 := (ZEXPR $n2). - -Syntax constr Zminus <<(Zminus $n1 $n2)>> 8 - [<hov 0> "`" <$nn1:"dummy":E> "-" <$n2:"dummy":L> "`" ] - with $nn1 := (ZEXPR $n1) $nn2 := (ZEXPR $n2). - -Syntax constr Zmult <<(Zmult $n1 $n2)>> 7 - [<hov 0> "`" <$nn1:"dummy":E> "*" <$n2:"dummy":L> "`" ] - with $nn1 := (ZEXPR $n1) $nn2 := (ZEXPR $n2). -\end{verbatim} -are now written -\begin{verbatim} -Syntax constr - - level 8: - Zplus [<<(Zplus $n1 $n2)>>] - -> [ [<hov 0> "`"(ZEXPR $n1):E "+"(ZEXPR $n2):L "`"] ] - | Zminus [<<(Zminus $n1 $n2)>>] - -> [ [<hov 0> "`"(ZEXPR $n1):E "-"(ZEXPR $n2):L "`"] ] - ; - - level 7: - Zmult [<<(Zmult $n1 $n2)>>] - -> [ [<hov 0> "`"(ZEXPR $n1):E "*"(ZEXPR $n2):L "`"] ] - . -\end{verbatim} - -\section{How to use \texttt{SearchIsos}} - -As shown in the overview, \texttt{SearchIsos} is made up of two tools: new -commands integrated in Coq and a separated program. - -\subsection{In the {\Coq} toplevel} - -Under \Coq, \texttt{SearchIsos} is called upon with the following command: - -\begin{tabbing} -\ \ \ \ \=\kill -\>{\tt SearchIsos} {\it term}. -\end{tabbing} - -This command displays the full name (modules, sections and identifiers) of all -the constants, variables, inductive types and constructors of inductive types -of the current context (not necessarily in the specialized -buffers) whose type is equal to {\it term} up to isomorphisms. These -isomorphisms of types are characterized by the contextual part of a theory -which is a generalization of the axiomatization for the typed lambda-calculus -associated with the Closed Cartesian Categories taking into account -polymorphism and dependent types. - -\texttt{SearchIsos} is twined with two other commands which allow to have some -informations about the search time: - -\begin{tabbing} -\ \ \ \ \=\kill -\>{\tt Time}.\\ -\>{\tt UnTime}. -\end{tabbing} - -As expected, these two commands respectively sets and disconnects the Time -Search Display mode. - -The following example shows a possibility of use: - -\begin{coq_eval} -Reset Initial. -\end{coq_eval} -\begin{coq_example} -Time. -Variables A,B:Set. -Hypothesis H0:(x:A)(y:B)(x=x/\y=y). -SearchIsos (b:B)(a:A)(b=b/\a=a). -\end{coq_example} - -For more informations, see the sections 5.6.7, 5.6.8 and 5.6.9 in the Reference -Manual. - -\subsection{In the whole library hierarchy} - -To extend the search to a {\Coq} library, you must use \textsf{Coq\_SearchIsos} -which is an independent tool compared to {\Coq} and can be invoked by the shell -command as follows: - -\begin{tabbing} -\ \ \ \ \=\kill -\>{\tt coqtop -searchisos} -\end{tabbing} - -Under this new toplevel (which contains your {\Coq} library), the three -commands {\tt SearchIsos}, {\tt Time} and {\tt UnTime} (described previously) -are then available and have always the same behavior. - -Likewise, this little sample (about the Euclidean division) shows a possible -request to the standard library of {\Coq}: - -\begin{verbatim} -Coq_SearchIsos < Time. - -Coq_SearchIsos < SearchIsos (b,a:nat)(gt b O) -Coq_SearchIsos < ->{q:nat&{r:nat|a=(plus (mult q b) r)/\(gt b r)}}. -#Div#--* [div1 : (b:nat)(gt b (0))->(a:nat)(diveucl a b)] -#Div#--* [div2 : (b:nat)(gt b (0))->(a:nat)(diveucl a b)] -#Euclid_proof#--* [eucl_dev : (b:nat)(gt b (0))->(a:nat)(diveucl a b)] -#Euclid_proof#--* [quotient : -(b:nat) - (gt b (0)) - ->(a:nat){q:nat | (EX r:nat | a=(plus (mult q b) r)/\(gt b r))}] -#Euclid_proof#--* [modulo : -(b:nat) - (gt b (0)) - ->(a:nat){r:nat | (EX q:nat | a=(plus (mult q b) r)/\(gt b r))}] -Finished transaction in 4 secs (2.27u,0s) -\end{verbatim} - -For more informations about \textsf{Coq\_SearchIsos}, see the section 15.4 in -the Reference Manual. - -\section{The new reduction functions} \label{reductions} - -\subsection{\texttt{Cbv}, \texttt{Lazy}} -The usual reduction or conversion tactics are \verb!Red!, \verb!Hnf!, -\verb!Simpl!, \verb!Unfold!, \verb!Change! and \verb!Pattern!. It is -now possible to normalize a goal with a parametric reduction function, -by specifying which of $\beta$,$\delta$ and $\iota$ must be -performed. In the case of $\delta$, a list of identifiers to unfold, -or a list of identifiers not to unfold, may follow. Moreover, two -strategies are available: a call-by-value reduction, efficient for -computations, and a lazy reduction, i.e. a call-by-name strategy with -sharing of reductions. - -To apply a reduction tactic, use one of the two strategies -\texttt{Cbv} for call-by value or \texttt{Lazy} for lazy reduction -applied to one or more ``flags'' designing which reduction to perform -\texttt{Beta} for $\beta$-reduction, \texttt{Iota} for -$\iota$-reduction (reduction of \texttt{Cases}) and \texttt{Delta} for -$\delta$-reduction (expansion of constants). - -The function \verb!Compute! is simply an alias for -\verb!Cbv Beta Delta Iota!. - -The following tactic applies on the current goal, -the $\beta\iota$-reduction, and -$\delta$-reduction of any constants except \verb!minus!, using the -call-by-value strategy. -\begin{verbatim} -Cbv Beta Iota Delta - [ minus ] -\end{verbatim} - -\subsection{\texttt{Fold}} -A specific function \verb!Fold! was designed: -\verb!Fold! takes as argument a list of -terms. These terms are reduced using \verb!Red!, and the result is -replaced by the expanded term. For example, -\begin{coq_example*} -Require Arith. -Lemma ex4 : (n:nat)(le (S O) n)->(le (S n) (plus n n)). -Intros. -\end{coq_example*} -\begin{coq_example} -Fold (plus (1) n). -\end{coq_example} -\begin{coq_eval} -Abort. -\end{coq_eval} - -\subsection{\texttt{Eval}} - -The reduction may be applied to a given term (not only the goal) with -the vernac command \verb!Eval!. -The syntax is: -\[\texttt{Eval}~ \textit{ReductionFunction}~ \texttt{in}~ -\textit{term}.\] -To compute the reduced value of $t$ using the reduction strategy -\textit{ReductionFunction}. - -It may happen that the term to be -reduced depends on hypothesis introduced in a goal. The default -behavior is that the term is interpreted in the current goal (if -any). \texttt{Eval} can take an extra argument specifying an -alternative goal. - -Here are a few examples of reduction commands: -\begin{coq_example} -Eval Simpl in [n:nat]n=(plus O n). -\end{coq_example} -Simplifies the expression. -\begin{coq_example*} -Lemma ex5 : O=O /\ (x:nat)x=x. -Split; Intros. -\end{coq_example*} -\begin{coq_example} -Eval 2 Lazy Beta Delta [ mult ] Iota in ([n:nat](mult n (plus n x)) (3)). -\end{coq_example} - -$\beta\iota$-reduces the given term and $\delta$-reduces \verb+mult+ in the -context of the second goal. - -\begin{coq_example} -Eval Compute in `18446744073709551616 * 18446744073709551616`. -\end{coq_example} - -Computes $2^{128}$. - -\section{Installation procedure} - -\subsection{Uninstalling Coq} - -\paragraph{Warning} -It is strongly recommended to clean-up the V6.1 Coq library directory -by hand, before you install the new version. -\paragraph{Uninstalling Coq V6.2} -There is a new option to coqtop \texttt{-uninstall} that will remove -the the binaries and the library files of Coq V6.2 on a Unix system. - - -\subsection{OS Issues -- Requirements} - -\subsubsection{Unix users} -You need Objective Caml version 1.06 or 1.07, and Camlp4 version 1.07.2 -to compile the system. Both are available by anonymous ftp -at: - -\bigskip -\verb|ftp://ftp.inria.fr/Projects/Cristal|. -\bigskip - -\noindent -Binary distributions are available for the following architectures: - -\bigskip -\begin{tabular}{l|c|r} -{\bf OS } & {\bf Processor} & {name of the package}\\ -\hline -Linux & 80386 and higher & coq-6.2-linux-i386.tar.gz \\ -Solaris & Sparc & coq-6.2-solaris-sparc.tar.gz\\ -Digital & Alpha & coq-6.2-OSF1.tar.gz\\ -\end{tabular} -\bigskip - -If your configuration is in the above list, you don't need to install -Caml and Camlp4 and to compile the system: -just download the package and install the binaries in the right place. - -\subsubsection{MS Windows users} - -The MS Windows version will be soon available. - -%users will get the 6.2 version at the same time than -%Unix users ! -%A binary distribution is available for Windows 95/NT. Windows 3.1 -%users may run the binaries if they install the Win32s module, freely -%available at \verb|ftp.inria.fr|. - -\section{Credits} - -The new parsing mechanism and the new syntax for extensible grammars -and pretty-printing rules are from Bruno Barras and Daniel de -Rauglaudre. - -The rearrangement of tactics, the extension of \texttt{Tauto}, \texttt{Intros} and -equality tactics, and the tactic definition mechanism are from Eduardo -Gim\'enez. Jean-Christophe Filli\^atre designed and implemented the -tactic \texttt{Refine} and the tactic \texttt{Correctness}. - -Bruno Barras improved the reduction functions and introduced new -uniform commands for reducing a goal or an expression. David Delahaye -designed and implemented {\tt SearchIsos}. - -Patrick Loiseleur introduced syntax rules to -manipulate natural numbers and binary integers expression. -Hugo Herbelin improved the loading mechanism and contributed to a more -user-friendly syntax. - -\end{document} - -% Local Variables: -% mode: LaTeX -% TeX-master: t -% End: - - -% $Id$ - diff --git a/doc/ChangesV6-3-1.tex b/doc/ChangesV6-3-1.tex deleted file mode 100644 index 4eac45633..000000000 --- a/doc/ChangesV6-3-1.tex +++ /dev/null @@ -1,160 +0,0 @@ -\documentclass[11pt]{article} -\usepackage[latin1]{inputenc} -\usepackage[T1]{fontenc} - -\input{./title} -\input{./macros} - -\begin{document} - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% Changes 6.3 ===> 6.3.1 -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\shorttitle{Changes from {\Coq} V6.3 to {\Coq} V6.3.1} - -This document describes the main differences between Coq V6.3 and -V6.3.1. This new version of Coq is characterized by fixed bugs, and -improvement of implicit arguments synthesis and speed in tactic -applications. - -\section{Changes overview} - -\subsection{Tactics} - - \begin{itemize} - - \item \texttt {Tauto} has been unable for a time to deal with -hypotheses with 2 imbricated implications. Now it should work. -\texttt {Intuition} now removes true, and therefore useless, -hypotheses.\\ - - \item Several bugs of the {\texttt Program} are fixed (but some - automatically generated names have changed and may lead to - incompatibilities). - - \item Bug with negative index in bindings fixed. - - \item Speed improvement: redondant checks when applying a tactic - have been turned off. For some tactics that don't make themselves - the expected verifications, it may result in incorrect proofs - detected only at Qed/Save time. In this last case, you can turn on - the -tac-debug flag to coqtop. - - \item The ``?'' in goals are now instantiated as soon as an instance - is known for them. - - \end{itemize} - -\subsection{Toplevel commands} - -\begin{description} - -\item Bug in \texttt{Time} fixed. - -\end{description} - -\subsection{Language} - - \begin{description} \item[Type reconstruction] The algorithm to - solve incomplete information in terms has been improved - furthermore. In particular question marks can be put in in place of - the type of abstracted variables and in Cases expressions. - - \item[Guarded cofixpoints] A weakness in the guardness condition - when a cofixpoint refers to another one has been corrected. - WARNING: the new criterion may refuse some olderly accepted - Cofixpoint definitions which actually are valid but for a reason - difficult to detect automatically. - - \item[Extraction] A bug was limiting the number of propositional - singleton inductive types (such has ``eq'') for which elimination - towards Set is valid. - - \end{description} - -\subsection{Incompatibilities} - - You could have to modify your vernacular source for the following - reasons: - - \begin{itemize} - - \item Some names of variables generated by the \texttt{Program} have - changed. - - \item {\texttt Intuition} now remove trye hypotheses. - - \item In all cases, the ``.vo'' files are not compatible and should - be recompiled. - - \end{itemize} - -\section{New users contributions} - - \begin{description} - - \item[Binary Decision Diagrams] provided by Kumar Verma (Dyade) - - \item[A distributed reference counter] (part of a - garbage collector) provided by Jean Duprat (ENS-Lyon) - -\end{description} - -\section{Installation procedure} - -\subsection{Uninstalling Coq} - -\paragraph{Warning} -It is strongly recommended to clean-up the V6.3 Coq library directory -before you install the new version. -Use the option to coqtop \texttt{-uninstall} that will remove -the binaries and the library files of Coq V6.3 on a Unix system. - -\subsection{OS Issues -- Requirements} - -\subsubsection{Unix users} -You need Objective Caml version 2.01 or later, and the corresponding -Camlp4 version to compile the system. Both are available by anonymous ftp -at: \\ -\verb|ftp://ftp.inria.fr/Projects/Cristal|. -\bigskip - -\noindent -Binary distributions are available for the following architectures: - -\bigskip -\begin{tabular}{l|c|r} -{\bf OS } & {\bf Processor} & {name of the package}\\ -\hline -Linux & 80386 and higher & coq-6.3.1-Linux-i386.tar.gz \\ -Solaris & Sparc & coq-6.3.1-solaris-sparc.tar.gz\\ -Digital & Alpha & coq-6.3.1-OSF1-alpha.tar.gz\\ -\end{tabular} -\bigskip - -There is also rpm packages for Linux. - -\bigskip - -If your configuration is in the above list, you don't need to install -Caml and Camlp4 and to compile the system: -just download the package and install the binaries in the right place. - -\subsubsection{MS Windows users} - -A binary distribution is available for PC under MS Windows 95/98/NT. -The package is named coq-6.3.1-win.zip. - -For installation information see the -files INSTALL.win and README.win. - -\end{document} - -% Local Variables: -% mode: LaTeX -% TeX-master: t -% End: - - -% $Id$ - diff --git a/doc/ChangesV6-3.tex b/doc/ChangesV6-3.tex deleted file mode 100644 index 8e43a258c..000000000 --- a/doc/ChangesV6-3.tex +++ /dev/null @@ -1,302 +0,0 @@ -\documentclass[11pt]{article} -\usepackage[latin1]{inputenc} -\usepackage[T1]{fontenc} - -\input{./title} -\input{./macros} - -\begin{document} - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% Changes 6.2 ===> 6.3 -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\shorttitle{Changes from {\Coq} V6.2 to {\Coq} V6.3} - -This document describes the main differences between Coq V6.2 and -V6.3. This new version of Coq is characterized by new tactics and a -more flexible guard condition in fixpoints definitions. -We refer to the reference manual -for a more precise description of the new features. - -%See the ASCII file \texttt{CHANGES} available by FTP with \Coq\ for -%the minor changes of the bug-fix releases 6.2.1 and 6.2.2. - - -\section{Changes overview} - -\subsection{New Tactics} - - \begin{itemize} - - \item The \texttt{AutoRewrite} tactic uses a set of theorems - as rewrite rules that are applied sequentially in order to - solve the goal. This tactic is still experimental and subject to changes. - - \item \texttt{First} and \texttt{Solve} are two tacticals which - apply to a sequence of - tactics written \texttt{[ \textit{tac}$_1$ | ... | - \textit{tac}$_n$ ]}. - \texttt{First} applies the first tactic in the given list - which does not fail while - \texttt{Solve} applies the first tactic in the list - which completely solves the goal. - - \item \texttt{Quote} this new tactic does automatic inversion of - interpretation function for people using Barengregt's so-called - `2-level approach'. See examples in \texttt{theories/DEMOS/DemoQuote.v}. - - \item \texttt{Change} \textit{term} \texttt{in} \textit{hyp} is now - available. - - \item \texttt{Move} \textit{hyp} \texttt{after} \textit{hyp} allows - to reorder the hypotheses of the local context. - - \end{itemize} - -\subsection{Changes in existing tactics} - - \begin{itemize} - - \item \texttt{Intro} or \texttt{Intros} with explicit names - will force an head reduction of the goal in case it does not start - with a product. \\ - -\texttt{Intro} or \texttt{Intros} without explicit names - generate automatically names for the hypothesis or - variable to be introduced. The algorithm to generate these names - has been slightly changed, this may be a source of incompatibility in the - proofs script. - - The new variant \texttt{Intro \textit{ident} after \textit{hyp}} allows to - tell the place where an hypothesis is introduced in the context. - - \item \texttt{Auto} the structure of the hints databases for the Auto - tactic was changed in version V6.2.3. - In version V6.3, the following new features were added to Auto~: - \begin{itemize} - \item \texttt{Print} \textit{HintDbname} prints out the contents of - a the hint database \textit{HintDbname}; - \item \texttt{Constructors} \textit{Indname} is a new hint - tactic which is equivalent to introduce the \texttt{Resolve} - hint tactic for each - constructor of the \textit{Indname} inductive definition. - \end{itemize} - - \item \texttt{Induction} \textit{var} now also performs induction on - a variable \textit{var} of the local context. This extension is - more ``user-friendly'' in the sense it generalizes automatically - above the other hypotheses dependent on the original variable. It - does not duplicate any longer the name of the variable to which it - applies. It should avantageously replaces "Elim" on an - hypothesis/variable or a typical sequence "Generalize" followed by - "Induction" on the generalized variable. But this extension is - experimental and susceptible of change in next releases. - - \item \texttt{Let} \textit{ident} \texttt{:=} \textit{term} - \texttt{in} \textit{occurlist} \textit{hyps} replaces the given - occurrences of \texttt{term} in the hypotheses \textit{hyps} (or in - the goal) by the variable \textit{ident} and keep the equality - \textit{ident=term} in the context. This is actually a variant of - \texttt{Generalize} which keeps track of the original term. As the - new \texttt{Induction} to which it can be combined, it is susceptible - of change in next releases. - - \item The \texttt{Ring} tactic has been extended and - works now also when the ring is in the \Type{} sort. - - \item The tactic \texttt{Correctness} has been improved. - \end{itemize} - -\subsection{New toplevel commands} - -\begin{description} - -\item[\texttt{Time}] Any vernacular command (including invocation of - tactics) can be prefixed by the word \texttt{Time}; then the time - spent is printed after having executed the command. For example : - \texttt{Time Save.} or \texttt{Time Omega.} - -\item[\texttt{Focus} $n$] It is now possible to focus on a specific - goal using the command \texttt{Focus} $n$, with $n$ being the - range of the selected subgoal. All the tactics will be applied to - this goal and only the subgoals inherited from the selected goal - are displayed. When the subgoal is completed, the message - \texttt{"Subtree proved"} is printed out then the focus goes back - to the initial goal and the corresponding remaining subgoals are - printed out. The focus commands are reseted by the - \texttt{Undo} command or \texttt{Unfocus}. \texttt{Focus} - without argument keeps its old meaning to only disply the first - subgoal. - -\item[Evaluation in Definition] It is now possible to apply a - reduction function to a term inside a definition. Just replace the - term to be defined by - \[ \texttt{Eval}~ \textit{reduction-function}~ \texttt{in}~ - \textit{term}\] - at the right hand side of the \texttt{:=} sign in a definition. - - \end{description} - -\subsection{Language extensions} - \begin{description} - \item[Type reconstruction] The algorithm to solve incomplete - information in terms has been improved. In particular - question marks can be put - in place of the type of universally quantified variables. - \item[Guarded fixpoints] The condition for well-formed - fixpoints has been extended, it is now possible to define - structural fixpoints for positive inductive definitions with - nested recursion (like \texttt{Inductive term : Set := cons : (list term)->term}) - \end{description} - -\subsection{Libraries} - - \begin{description} - - \item[Reals] The library of real numbers has been extended and - obeys to the same naming convention than - ARITH and ZARITH: addition is \texttt{Rplus}, theorems stating commutativity are - postfixed by \texttt{\_sym} like \texttt{plus\_sym}, - \texttt{Rmult\_sym}, etc. The tactic \texttt{Ring} has been - instantiated on the reals; one can use it to normalize polynomial - expressions over the reals. - -The library \texttt{Reals} - has been completed by a definition of limit, derivative - and by others properties and functions. -\end{description} - - -\subsection{Documentation} - -The documentation includes now an index of errors. - -\section{Incompatibilities} - - You could have to modify your vernacular source for the following - reasons: - - \begin{itemize} - - \item Some names of variables have changed. Typically, a sequence - "Generalize n; Induction n" should become a "Generalize n; Induction n0", - or better, simply "Induction n" since Induction now works with - hypotheses of the context and generalizes automatically. - - \item In the library ZArith, "Zinv" has been renamed as "Zopp", in - order to be coherent with the Reals library. Theorems whose name - includes "Zinv" have been renamed too. A global search-and-replace - of "Zinv" by "Zopp" should be sufficient to update user's - developments. - - \item In the library Reals, some names has been changed. - In the file README of the library, there is a script which can be - used to update user's developments. - - \item The definition of Exists has changed in LISTS/Streams. - - \end{itemize} - -\section{New contributions} -We integrated new contributions : -\begin{description} -\item[Finite sets and graphs] -This contribution is due to J. Goubault-Larrecq from Dyade - (INRIA-Bull). It contains a -development of finite sets implemented efficiently -as trees indexed by binary numbers. This representation is used to -implement graphs corresponding to arithmetic formulas and prove the -correctness of a decision procedure testing the satisfiability of -formula by detecting cycles of positive weigth in the graph -\item[$\pi$-calculus] A development of $\pi$-calculus due to -I. Scagnetto from University of Udine. -\item[The three gap theorem] A Proof of the Three Gap Theorem - (Steinhaus Conjecture) by M. Mayero from INRIA Rocquencourt. -\item[Floating point numbers] An axiomatisation of the IEEE 754 -norm for Floating point numbers done by P. Loiseleur fron LRI Orsay. -\item[Algebra] Basic notions of algebra designed by L. Pottier from - INRIA Sophia-Antipolis. -\item[Heapsort] A proof of an imperative version of the - Heapsort sorting algorithm developed by J-C. Filli\^atre from -LRI Orsay. - -\end{description} - -\section{Installation procedure} - -\subsection{Uninstalling Coq} - -\paragraph{Warning} -It is strongly recommended to clean-up the V6.2 Coq library directory -before you install the new version. -Use the option to coqtop \texttt{-uninstall} that will remove -the binaries and the library files of Coq V6.2 on a Unix system. - -\subsection{OS Issues -- Requirements} - -\subsubsection{Unix users} -You need Objective Caml version 2.01 or 2.02, and the corresponding -Camlp4 version to compile the system. Both are available by anonymous ftp -at: \\ -\verb|ftp://ftp.inria.fr/Projects/Cristal|. -\bigskip - -\noindent -Binary distributions are available for the following architectures: - -\bigskip -\begin{tabular}{l|c|r} -{\bf OS } & {\bf Processor} & {name of the package}\\ -\hline -Linux & 80386 and higher & coq-6.3-linux-i386.tar.gz \\ -Solaris & Sparc & coq-6.3-solaris-sparc.tar.gz\\ -Digital & Alpha & coq-6.3-OSF1.tar.gz\\ -\end{tabular} -\bigskip - -If your configuration is in the above list, you don't need to install -Caml and Camlp4 and to compile the system: -just download the package and install the binaries in the right place. - -\subsubsection{MS Windows users} - -A binary distribution is available for PC under MS Windows 95/98/NT. -The package is named coq-6.3-win.zip. - -For installation information see the -files INSTALL.win and README.win. - - -%users will get the 6.2 version at the same time than -%Unix users ! -%A binary distribution is available for Windows 95/NT. Windows 3.1 -%users may run the binaries if they install the Win32s module, freely -%available at \verb|ftp.inria.fr|. - -\section{Credits} -B. Barras extended the unification algorithm to complete partial terms -and solved various tricky bugs related to universes.\\ -D. Delahaye developed the \texttt{AutoRewrite} tactic. He also designed the new -behavior of \texttt{Intro} and provided the tacticals \texttt{First} and -\texttt{Solve}.\\ -J.-C. Filli\^atre developed the \texttt{Correctness} tactic.\\ -E. Gim\'enez extended the guard condition in fixpoints.\\ -H. Herbelin designed the new syntax for definitions and extended the -\texttt{Induction} tactic.\\ -P. Loiseleur developed the \texttt{Quote} tactic and -the new design of the \texttt{Auto} -tactic, he also introduced the index of -errors in the documentation.\\ -C. Paulin wrote the \texttt{Focus} command and introduced -the reduction functions in definitions, this last feature -was proposed by J.-F. Monin from CNET Lannion. -\end{document} - -% Local Variables: -% mode: LaTeX -% TeX-master: t -% End: - - -% $Id$ - diff --git a/doc/ChangesV7-0.tex b/doc/ChangesV7-0.tex deleted file mode 100755 index b593b9dc8..000000000 --- a/doc/ChangesV7-0.tex +++ /dev/null @@ -1,757 +0,0 @@ -\documentclass[11pt]{article} -\usepackage[latin1]{inputenc} -\usepackage[T1]{fontenc} - -\input{./title} -\input{./macros} - -\begin{document} - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% Changes 6.3.1 ===> 7.0 -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\shorttitle{Changes from {\Coq} V6.3.1 to {\Coq} V7} - - -%This document describes the main differences between {\Coq} V6.3.1 and -%V7. This new version of {\Coq} is characterized by fixed bugs, and -%improvement of implicit arguments synthesis and speed in tactic -%applications. - -\def\ltac{{\cal L}_{tac}} - -\section*{Overview} - -The new major version number is justified by a deep restructuration of -the implementation code of \Coq. For the end-user, {\Coq} -V7 provides the following novelties: - -\begin{itemize} -\item A more high-level tactic language called $\ltac$ (see -section~\ref{Tactics}) -\item A primitive let-in construction (see section \ref{Letin}) -which can also be used in \texttt{Record} definitions - (as suggested by Randy Pollack) -\item Structuration of the developments in libraries and use of the -dot notation to access names (see section \ref{Names}) -\item A search facilities by pattern -provided by Yves Bertot (see section \ref{Search}) -\item A ``natural'' syntax for real numbers (see section -\ref{SyntaxExtensions}) -\item New tactics (and developments) for real numbers -(see section~\ref{NewTactics}) -\item The tactic {\tt Field} which solves equalities using commutative field -theory (see section~\ref{NewTactics}) -\item The tactic {\tt Fourier} to solve inequalities, developed by - Loïc Pottier has been integrated -\item A command to export theories to XML to -be used with Helm's publishing and rendering tools (see section -\ref{XML}) -\item A new implementation of extraction (see section \ref{Extraction}) -%\item As usual, several bugs fixed and a lot of new ones introduced -\end{itemize} - -Incompatibilities are described in section -\ref{Incompatibilities}. Please notice that -{\tt Program/Realizer} is no more available in {\Coq} V7. - -Developers of tactics in ML are invited to read section -\ref{Developers}. - -\paragraph{Changes between \Coq{} V7beta and \Coq{} V7} -Some functionalities of \Coq{} V6.3 that were not available in \Coq{} -V7beta has been restored~: -\begin{itemize} -\item A new mechanism for extraction of ML programs has been introduced. -\item \texttt{Correctness} is now supported. -\item Syntax for user-defined tactics calls does not require extra - parenthesis. -\item \texttt{Elim} can be called even for non-inductive objects - when the apropriate elimination lemma exists. -\item User defined tokens with arbitrary combination of letters and - symbols have been reintroduced. -\end{itemize} -\section{Language} -\label{Language} -\subsection{Primitive {\tt let ... in ...} construction} -\label{Letin} -The {\tt let ... in ...} syntax in V6.3.1 was implemented as a -macro. It is now a first-class construction. - -\begin{coq_example} -Require ZArith. -Definition eight := [two:=`1 + 1`][four:=`two + two`]`four + four`. -Print eight. -\end{coq_example} - -{\tt Local} definitions and {\tt Remark} inside a section now behaves -as local definitions outside the section. - -\begin{coq_example} -Section A. -Local two := `1 + 1`. -Definition four := `two + two`. -End A. -Print four. -\end{coq_example} - -The unfolding of a reference with respect to a definition local to a section -is performed by $\delta$ rule. But a ``{\tt let ... in ...}'' inside a term -is not concerned by $\delta$ reduction. Commands to finely reduce this -kind of expression remain to be provided. -\medskip - -\paragraph{Alternative syntax} - A less symbolic but equivalent syntax is available as~:\\ {\tt let -two = `1 + 1` in `two + two`}. - -\paragraph{Local definitions in records} -{\tt Local} definitions can be used inside record definitions as -suggested by Randy Pollack~: -\begin{coq_example} -Record local_record : Set := {x:nat; y:=O; H:x=y}. -Print local_record. -Print x. -Print y. -Check H. -\end{coq_example} - -\subsection{Libraries and qualified names} -\label{Names} - -\paragraph{Identifiers} An identifier is any string beginning by a -letter and followed by letters, digits or simple quotes. The bug -with identifiers ended by a number greater than $2^{30}$ is fixed! - -\paragraph{Libraries} - -The theories developed in {\Coq} are now stored in {\it libraries}. A -library is characterized by a name called {\it root} of the -library. By default, two libraries are defined at the beginning of a -{\Coq} session. The first library has root name {\tt Coq} and contains the -standard library of \Coq. The second has root name {\tt Scratch} and -contains all definitions and theorems not explicitly put in a specific -library. - -Libraries have a tree structure. Typically, the {\tt Coq} library -contains the (sub-)libraries {\tt Init}, {\tt Logic}, {\tt Arith}, -{\tt Lists}, ... The ``dot notation'' is used to write -(sub-)libraries. Typically, the {\tt Arith} library of {\Coq} standard -library is written ``{\tt Coq.Arith}''. - -\smallskip -Remark: no space is allowed -between the dot and the following identifier, otherwise the dot is -interpreted as the final dot of the command! -\smallskip - -Libraries and sublibraries can be mapped to physical directories of the -operating system using the command - -\begin{quote} -{\tt Add LoadPath {\it physical\_dir} as {\it (sub-)library}}. -\end{quote} - -Incidentally, if a {\it (sub-)library} does not already -exists, it is created by the command. This allows users to define new -root libraries. - -A library can inherit the tree structure of a physical directory by -using the command - -\begin{quote} -{\tt Add Rec LoadPath {\it physical\_dir} as {\it (sub-)library}}. -\end{quote} - -At some point, (sub-)libraries contain {\it modules} which coincides -with files at the physical level. Modules themselves may contain -sections, subsections, ... and eventually definitions and theorems. - -As for sublibraries, the dot notation is used to denote a specific -module, section, definition or theorem of a library. Typically, {\tt -Coq.Init.Logic.Equality.eq} denotes the Leibniz' equality defined in -section {\tt Equality} of the module {\tt Logic} in the -sublibrary {\tt Init} of the standard library of \Coq. By -this way, a module, section, definition or theorem name is now unique -in \Coq. - -\paragraph{Absolute and short names} - -The full name of a library, module, section, definition or theorem is -called {\it absolute}. The final identifier {\tt eq} is called the -{\it base name}. We call {\it short name} a name reduced to a single -identifier. {\Coq} maintains a {\it name table} mapping short names -to absolute names. This greatly simplifies the notations and preserves -compatibility with the previous versions of \Coq. - -\paragraph{Visibility and qualified names} -An absolute path is called {\it visible} when its base name suffices -to denote it. This means the base name is mapped to the absolute name -in {\Coq} name table. - -All the base names of sublibraries, modules, sections, definitions and -theorems are automatically put in the {\Coq} name table. But sometimes, -names used in a module can hide names defined in another module. -Instead of just distinguishing the clashing names by using the -absolute names, it is enough to prefix the base name just by the name -of its containing section (or module or library). -% CP : L'exemple avec Equality.eq ne semble pas fonctionner -% E.g. if {\tt eq} -% above is hidden by another definition of same base name, it is enough -% to write {\tt Equality.eq} to access it... unless section {\tt -% Equality} itself has been hidden in which case, it is necessary to -% write {\tt Logic.Equality.eq} and so on. -Such a name built from -single identifiers separated by dots is called a {\it qualified} -name. Especially, both absolute names and short names are qualified -names. Root names cannot be hidden in such a way fully qualified -(i.e. absolute names) cannot be hidden. - -Examples: - -\begin{coq_eval} -Reset Initial. -\end{coq_eval} - -\begin{coq_example} -Check O. -Definition nat := bool. -Check O. -Check Datatypes.nat. -\end{coq_example} - -\paragraph{Requiring a file} - -When a ``.vo'' file is required in a physical directory mapped to some -(sub-)library, it is adequately mapped in the whole library structure -known by \Coq. However, no consistency check is currently done to -ensure the required module has actually been compiled with the same -absolute name (e.g. a module can be compiled with absolute name -{\tt Mycontrib.Arith.Plus} but required with absolute name -{\tt HisContrib.ZArith.Plus}). - -The command {\tt Add Rec LoadPath} is also available from {\tt coqtop} -and {\tt coqc} by using option \verb=-R= (see section \ref{Tools}). - -\subsection{Syntax extensions} -\label{SyntaxExtensions} - -\paragraph{``Natural'' syntax for real numbers} -A ``natural'' syntax for real numbers and operations on reals is now -available by putting expressions inside pairs of backquotes. - -\begin{coq_example} -Require Reals. -Check ``2*3/(4+2)``. -\end{coq_example} -Remark: A constant, say \verb:``4``:, is equivalent to -\verb:``(1+(1+(1+1)))``:. - -\paragraph{{\tt Infix}} was inactive on pretty-printer. Now it works. - -\paragraph{Consecutive symbols} are now considered as an unique token. -Exceptions have been coded in the lexer to separate tokens we do not want to -separate (for example \verb:A->~B:), but this is not exhaustive and some spaces -may have to be inserted in some cases which have not been treated -(e.g. \verb:~<nat>O=O: should now be written \verb:~ <nat>O=O:). - -%should now be separated (e.g. by a -%space). Typically, the string \verb:A->~<nat>O=O: is no longer -%recognized. It should be written \verb:A-> ~ <nat>O=O:... or simply -%\verb:A->~ <nat>O=O: because of a special treatment for \verb:->:! - -\paragraph{The {\tt command} syntactic class for {\tt Grammar}} has -been renamed {\tt constr} consistently with the usage for {\tt Syntax} -extensions. Entries {\tt command1}, {\tt command2}, ... are renamed -accordingly. The type {\tt List} in {\tt Grammar} rules has been -renamed {\tt ast list}. - -\paragraph{Default parser in {\tt Grammar} and {\tt Syntax}} -\label{GrammarSyntax} - -The default parser for right-hand-side of {\tt Grammar} rules and for -left-hand-side of {\tt Syntax} rule was the {\tt ast} parser. Now it -is the one of same name as the syntactic class extended (i.e. {\tt -constr}, {\tt tactic} or {\tt vernac}). As a consequence, -{\verb:<< ... >>:} should be removed. - -On the opposite, in rules expecting the {\tt ast} parser, -{\verb:<< ... >>:} should be added in the left-hand-side of {\tt Syntax} rule. -As for {\tt Grammar} rule, a typing constraint, {\tt ast} or {\tt ast -list} needs to be explicitly given to force the use of the {\tt ast} -parser. For {\tt Grammar} rule building a new syntactic class, -different from {\tt constr}, {\tt tactic}, {\tt vernac} or {\tt ast}, -any of the previous keyword can be used as type (and therefore as -parser). - -See examples in appendix. - -\paragraph{Syntax overloading} - - Binding of constructions in Grammar rules is now done with absolute - paths. This means overloading of syntax for different constructions - having the same base name is no longer possible. - -\paragraph{Timing or abbreviating a sequence of commands} - -The syntax {\tt [ {\it phrase$_1$} ... {\it phrase$_n$} ].} is now -available to group several commands into a single one (useful for -{\tt Time} or for grammar extensions abbreviating sequence of commands). - -\subsection{Miscellaneous} - -\paragraph{Pattern aliases} of dependent type in \verb=Cases= -expressions are currently not supported. - -\subsection{Libraries} -The names of directories in \texttt{theories} has been changed. The -directory \texttt{theories/Zarith} has been renamed -\texttt{theories/ZArith} between \Coq{} V7.0beta and V7.0. - -A new directory \texttt{theories/IntMap} has been added which -contains an efficient representation of finite sets -as maps indexed by binary integers. This development has been -developed by J. Goubault and was previously an external contribution. - -Some definitions, lemmas and theorems have been added or reorganised, -see the Library documentation for more information. - -\section{Tactics} -\label{Tactics} -\def\oc{\textsc{Objective~Caml}} - -\subsection{A tactic language: $\ltac$} - -$\ltac$ is a new layer of metalanguage to write tactics and especially to deal -with small automations for which the use of the full programmable metalanguage -(\oc{}) would be excessive. $\ltac$ is mainly a small functional core with -recursors and elaborated matching operators for terms but also for proof -contexts. This language can be directly used in proof scripts or in toplevel -definitions ({\tt Tactic~Definition}). It has been noticed that non-trivial -tactics can be written with $\ltac$ and to provide a Turing-complete -programming framework, a quotation has been built to use $\ltac$ in \oc{}. -$\ltac$ has been contributed by David Delahaye and, for more details, see the -Reference Manual. Regarding the foundations of this language, the author page -can be visited at the following URL:\\ - -\url{http://logical.inria.fr/~delahaye/} - -\paragraph{Tactic debugger} - - \paragraph{{\tt Debug $($ On $|$ Off $)$}} turns on/off the tactic - debugger for $\ltac$. - This is still very experimental and no documentation is provided yet. - - -\subsection{New tactics} -\label{NewTactics} -\def\ml{\textsc{ML}} - - \paragraph{{\tt Field}} written by David~Delahaye and Micaela~Mayero solves -equalities using commutative field theory. This tactic is reflexive and has -been implemented using essentially the new tactic language $\ltac$. Only the -table of field theories (as for the tactic {\tt Ring}) is dealt by means of an -\ml{} part. This tactic is currently used in the real number theory. For more -details, see the Reference Manual. - - \paragraph{{\tt Fourier}} written by Loïc Pottier solves linear inequations. - - \paragraph{Other tactics and developments} has been included in the real -numbers library: {\tt DiscrR} proves that a real integer constant $c_1$ is non -equal to another real integer constant $c_2$; {\tt SplitAbsolu} allows us to -unfold {\tt Rabsolu} contants and split corresponding conjonctions; -{\tt SplitRmult} allows us to split a condition that a product is non equal to -zero into subgoals corresponding to the condition on each subterm of the -product. All these tactics have been written with the tactic language -$\ltac$.\\ -A development on Cauchy series, power series,... has been also added.\\ -For more details, see the Reference Manual. - -\subsection{Changes in pre-existing tactics} -\label{TacticChanges} - - \paragraph{{\tt Tauto} and {\tt Intuition}} have been rewritten using the - new tactic language $\ltac$. The code is now quite shorter and a significant - increase in performances has been noticed. {\tt Tauto} has exactly the same - behavior. {\tt Intuition} is slightly less powerful (w.r.t. to dependent - types which are now considered as atomic formulas) but it has clearer - semantics. This may lead to some incompatibilities. - - \paragraph{{\tt Simpl}} now simplifies mutually defined fixpoints - as expected (i.e. it does not introduce {\tt Fix id - \{...\}} expressions). - - \paragraph{{\tt AutoRewrite}} now applies only on main goal and the remaining - subgoals are handled by\break{}{\tt Hint~Rewrite}. The syntax is now:\\ - - {\tt Hint Rewrite $($ -> $|$ <- $)*$ [ $term_1$ $...$ $term_n$ ] in - $ident$ using $tac$}\\ - - Adds the terms $term_1$ $...$ $term_n$ (their types must be equalities) in - the rewriting database $ident$ with the corresponding orientation (given by - the arrows; default is left to right) and the tactic $tac$ which is applied - to the subgoals generated by a rewriting, the main subgoal excluded.\\ - - {\tt AutoRewrite [ $ident_1$ $...$ $ident_n$ ] using $tac$}\\ - - Performs all the rewritings given by the databases $ident_1$ $...$ $ident_n$ - applying $tac$ to the main subgoal after each rewriting step.\\ - - See the contribution \texttt{contrib/Rocq/DEMOS/Demo\_AutoRewrite.v} for - examples. - - \paragraph{{\tt Intro $hyp$} and {\bf \tt Intros $hyp_1$ ... $hyp_n$}} - now fail if the hypothesis/variable name provided already exists. - - \paragraph{{\tt Prolog}} is now part of the core - system. Don't use {\tt Require Prolog}. - - \paragraph{{\tt Unfold}} now fails when its argument is not an - unfoldable constant. - - \paragraph{Tactic {\tt Let}} has been renamed into {\tt LetTac} - and it now relies on the primitive {\tt let-in} constructions - - \paragraph{{\tt Apply ... with ...}} when instantiations are - redundant or incompatible now behaves smoothly. - - \paragraph{{\tt Decompose}} has now less bugs. Also hypotheses - are now numbered in order. - - \paragraph{{\tt Linear}} seems to be very rarely used. It has not - been ported in {\Coq} V7. - - \paragraph{{\tt Program/Realizer}} has not been ported in {\Coq} V7. - -\section{Toplevel commands} - -\subsection{Searching the environment} -\label{Search} -A new searching mechanism by pattern has been contributed by Yves Bertot. - - -\paragraph{{\tt SearchPattern {\term}}} -displays the name and type of all theorems of the current -context whose statement's conclusion matches the expression {\term} -where holes in the latter are denoted by ``{\tt ?}''. - -\begin{coq_eval} -Reset Initial. -\end{coq_eval} -\begin{coq_example} -Require Arith. -SearchPattern (plus ? ?)=?. -\end{coq_example} - -Patterns need not be linear: you can express that the same -expression must occur in two places by using indexed ``{\tt ?}''. - -\begin{coq_example} -Require Arith. -SearchPattern (plus ? ?1)=(mult ?1 ?). -\end{coq_example} - -\paragraph{{\tt SearchRewrite {\term}}} -displays the name and type of all theorems of the current -context whose statement's conclusion is an equality of which one side matches -the expression {\term}. Holes in {\term} are denoted by ``{\tt ?}''. - -\begin{coq_example} -Require Arith. -SearchRewrite (plus ? (plus ? ?)). -\end{coq_example} - -\begin{Variants} - -\item {\tt SearchPattern {\term} inside {\module$_1$}...{\module$_n$}}\\ -{\tt SearchRewrite {\term} inside -{\module$_1$}...{\module$_n$}.} - - This restricts the search to constructions defined in modules {\module$_1$}...{\module$_n$}. - -\item {\tt SearchPattern {\term} outside {\module}.}\\ -{\tt SearchRewrite {\term} outside {\module$_1$}...{\module$_n$}.} - - This restricts the search to constructions not defined in modules {\module$_1$}...{\module$_n$}. - -\end{Variants} - -\paragraph{{\tt Search {\ident}.}} has been extended to accept qualified -identifiers and the {\tt inside} and {\tt outside} restrictions as -{\tt SearchPattern} and {\tt SearchRewrite}. - -\paragraph{{\tt SearchIsos {\term}.}} has not been ported yet. - -\subsection{XML output} -\label{XML} - -A printer of {\Coq} theories into XML syntax has been contributed by -Claudio Sacerdoti Coen. Various printing commands (such as {\tt Print -XML Module {\ident}}) allow to produce XML files from -``.vo'' files. In order to experiment these possibilities, you need to -require the \Coq{} \texttt{Xml} module first. - -These XML files can be published on the Web, retrieved -and rendered by tools developed in the HELM project (see -http://www.cs.unibo.it/helm). - -\subsection{Other new commands} - - - \paragraph{{\tt Implicits {\ident}}} associate to \ident{} - implicit arguments as if the implicit arguments mode was on. - - \paragraph{{\tt Implicits {\ident} [{\num} \ldots {\num}]}} - allows to explicitly give what arguments - have to be considered as implicit in {\ident}. - -\begin{coq_example} -Parameter exists : (A:Set)(P:A->Prop)(x:A)(P x)->(EX x:A |(P x)). -Implicits exists. -Print exists. -Implicits exists [1]. -Print exists. -\end{coq_example} - -\subsection{Syntax standardisation} - -The commands on the left are now equivalent to (old) commands on -the right. - -\medskip - -\begin{tt} -\begin{tabular}{ll} -Set Implicit Arguments & Implicit Arguments On \\ -Unset Implicit Arguments ~~~~~ & Implicit Arguments Off \\ -Add LoadPath & AddPath \\ -Add Rec LoadPath & AddRecPath \\ -Remove LoadPath & DelPath \\ -Set Silent & Begin Silent \\ -Unset Silent & End Silent \\ -Print Coercion Paths & Print Path\\ -\end{tabular} -\end{tt} - -\medskip - -Commands on the right remains available for compatibility reasons (except for -{\tt Begin Silent} and {\tt End Silent} which interfere with -section closing, and for the misunderstandable {\tt Print Path}). - -\subsection{Other Changes} - - -\paragraph{Final dot} Commands should now be ended by a final dot ``.'' followed by a blank -(space, return, line feed or tabulation). This is to distinguish from -the dot notation for qualified names where the dot must immediately be -followed by a letter (see section \ref{Names}). - -\paragraph{Eval Cbv Delta ... in ...} The {\tt [- {\it -const}]}, if any, should now immediately follow the {\tt Delta} keyword. - - -\section{Tools} -\label{Tools} - -\paragraph{Consistency check for {\tt .vo} files} A check-sum test -avoids to require inconsistent {\tt .vo} files. - -\paragraph{Optimal compiler} If your architecture supports it, the native -version of {\tt coqtop} and {\tt coqc} is used by default. - -\paragraph{Option -R} The {\tt -R} option to {\tt coqtop} and {\tt -coqc} now serves to link physical path to logical paths (see -\ref{Names}). It expects two arguments, the first being the physical -path and the second its logical alias. It still recursively scans -subdirectories. - -\paragraph{Makefile automatic generation} {\tt coq\_makefile} is the -new name for {\tt do\_Makefile}. - -\paragraph{Error localisation} Several kind of typing errors are now -located in the source file. - -\section{Extraction}\label{Extraction} -Extraction code has been completely rewritten by J.-C. Filliâtre and -P. Letouzey since version V6.3. -This work is still not finished, but most parts of it are already -usable. It was successfully tested on the \Coq{} theories. - -The new mechanism is able to extract programs from any \Coq{} term -(including terms at the Type level). -A new mechanism to extract Ocaml modules from Coq files has been -added. - -However, the resulting ML term is not guaranteed to be typable in ML -(the next version should incorporate automatically appropriate conversions). - -Only extraction towards Ocaml programs is currently available. -The \verb=ML import= command is not available anymore, the command -\verb=Extract Constant= can be used to realize a \Coq{} axiom by -an ML program. - -More -information can be found in \verb=$COQTOP/contrib/extraction/README=. -The syntax of commands is described in the Reference Manual. - - -\section{Developers} -\label{Developers} -The internals of {\Coq} has changed a lot and will continue to change -significantly in the next months. We recommend tactic developers to -take contact with us for adapting their code. A document describing -the interfaces of the ML modules constituting {\Coq} is available -thanks to J.-C. Filliatre's ocamlweb -documentation tool (see the ``doc'' directory in {\Coq} source). - -\section{Incompatibilities} -\label{Incompatibilities} - - You could have to modify your vernacular source for the following - reasons: - - \begin{itemize} - - \item Any of the tactic changes mentioned in section \ref{TacticChanges}. - - \item The ``.vo'' files are not compatible and all ``.v'' files should - be recompiled. - - \item Consecutive symbols may have to be separated in some cases (see - section~\ref{SyntaxExtensions}). - - \item Default parsers in {\tt Grammar} and {\tt Syntax} are - different (see section \ref{GrammarSyntax}). - - \item Definition of {\tt D\_in} (Rderiv.v) is now with Rdiv and not - with Rmult and Rinv as before. - - \item Pattern aliases of dependent type in \verb=Cases= - expressions are currently not supported. - - \end{itemize} - -A shell script \verb=translate_V6-3-1_to_V7= is available in the archive to -automatically translate V6.3.1 ``.v'' files to V7.0 syntax -(incompatibilities due to changes in tactics semantics are not -treated). - -%\section{New users contributions} - -\section{Installation procedure} - -%\subsection{Operating System Issues -- Requirements} - -{\Coq} is available as a source package at - -\begin{quote} -\verb|ftp://ftp.inria.fr/INRIA/coq/V7|\\ -\verb|http://coq.inria.fr| -\end{quote} - -You need Objective Caml version 3.00 or later, and the corresponding -Camlp4 version to compile the system. Both are available by anonymous ftp -at: - -\begin{quote} -\verb|ftp://ftp.inria.fr/Projects/Cristal|\\ -\verb|http://caml.inria.fr| -\end{quote} - -\noindent -%Binary distributions are available for the following architectures: -% -%\bigskip -%\begin{tabular}{l|c|r} -%{\bf OS } & {\bf Processor} & {name of the package}\\ -%\hline -%Linux & 80386 and higher & coq-6.3.1-Linux-i386.tar.gz \\ -%Solaris & Sparc & coq-6.3.1-solaris-sparc.tar.gz\\ -%Digital & Alpha & coq-6.3.1-OSF1-alpha.tar.gz\\ -%\end{tabular} -%\bigskip - -%A rpm package is available for i386 Linux users. No other binary -%package is available for this beta release. - -%\bigskip -% -%If your configuration is in the above list, you don't need to install -%Caml and Camlp4 and to compile the system: -%just download the package and install the binaries in the right place. - -%\paragraph{MS Windows users} -% -%A binary distribution is available for PC under MS Windows 95/98/NT. -%The package is named coq-6.3.1-win.zip. -% -%For installation information see the -%files INSTALL.win and README.win. - -\section*{Appendix} -\label{Appendix} -We detail the differences between {\Coq} V6.3.1 and V7.0 for the {\tt -Syntax} and {\tt Grammar} default parsers. - -\medskip - -{\bf Examples in V6.3.1} - -\begin{verbatim} -Grammar command command0 := - pair [ "(" lcommand($lc1) "," lcommand($lc2) ")" ] -> - [<<(pair ? ? $lc1 $lc2)>>]. - -Syntax constr - level 1: - pair [<<(pair $_ $_ $t3 $t4)>>] -> [[<hov 0> "(" $t3:E ","[0 1] $t4:E ")" ]]. - -Grammar znatural formula := - form_expr [ expr($p) ] -> [$p] -| form_eq [ expr($p) "=" expr($c) ] -> [<<(eq Z $p $c)>>]. - -Syntax constr - level 0: - Zeq [<<(eq Z $n1 $n2)>>] -> - [[<hov 0> "`" (ZEXPR $n1) [1 0] "= "(ZEXPR $n2)"`"]]. - -Grammar tactic simple_tactic := - tauto [ "Tauto" ] -> [(Tauto)]. -\end{verbatim} - -\medskip - -{\bf New form in V7.0beta} - -\begin{verbatim} -Grammar constr constr0 := - pair [ "(" lconstr($lc1) "," lconstr($lc2) ")" ] -> [ (pair ? ? $lc1 $lc2) ]. - -Syntax constr - level 1: - pair [ (pair $_ $_ $t3 $t4) ] -> [[<hov 0> "(" $t3:E ","[0 1] $t4:E ")" ]]. - -Grammar znatural formula : constr := - form_expr [ expr($p) ] -> [ $p ] -| form_eq [ expr($p) "=" expr($c) ] -> [ (eq Z $p $c) ]. - -Syntax constr - level 0: - Zeq [ (eq Z $n1 $n2) ] -> - [<hov 0> "`" (ZEXPR $n1) [1 0] "= "(ZEXPR $n2)"`"]]. - -Grammar tactic simple_tactic: ast := - tauto [ "Tauto" ] -> [(Tauto)]. -\end{verbatim} - -\end{document} - -% Local Variables: -% mode: LaTeX -% TeX-master: t -% End: - - -% $Id$ - diff --git a/doc/Correctness.tex b/doc/Correctness.tex deleted file mode 100644 index 2b770a877..000000000 --- a/doc/Correctness.tex +++ /dev/null @@ -1,930 +0,0 @@ -\achapter{Proof of imperative programs} -\aauthor{Jean-Christophe Filliâtre} -\label{Addoc-programs} -\index{Imperative programs!proof of} -\comindex{Correctness} - -%%%%%%%%%%%%%%%% -% Introduction % -%%%%%%%%%%%%%%%% - -\noindent\framebox{Warning:} The tactic presented in this chapter was a -prototype implementation, now deprecated and no more maintained. It is -subsumed by a much more powerful tool, developped and distributed -independently of the system \Coq, called \textsc{Why} (see -\url{http://why.lri.fr/}). - -\bigskip - -This chapter describes a tactic -to prove the correctness and termination of imperative -programs annotated in a Floyd-Hoare logic style. -The theoretical fundations of this tactic are described -in~\cite{Filliatre99,Filliatre03jfp}. -This tactic is provided in the \Coq\ module \texttt{Correctness}, -which does not belong to the initial state of \Coq. So you must import -it when necessary, with the following command: -$$ -\mbox{\texttt{Require Correctness.}} -$$ - - -%%%%%%%%%%%%%%%%%%%%% -% comment ça marche % -%%%%%%%%%%%%%%%%%%%%% - -\asection{How it works} - -Before going on into details and syntax, let us give a quick overview -of how that tactic works. -Its behavior is the following: you give a -program annotated with logical assertions and the tactic will generate -a bundle of subgoals, called \emph{proof obligations}. Then, if you -prove all those proof obligations, you will establish the correctness and the -termination of the program. -The implementation currently supports traditional imperative programs -with references and arrays on arbitrary purely functional datatypes, -local variables, functions with call-by-value and call-by-variable -arguments, and recursive functions. - -Although it behaves as an implementation of Floyd-Hoare logic, it is not. -The idea of the underlying mechanism is to translate the imperative -program into a partial proof of a proposition of the kind -$$ -\forall \vec{x}. P(\vec{x}) - \Rightarrow \exists(\vec{y},v). Q(\vec{x},\vec{y},v) -$$ -where $P$ and $Q$ stand for the pre- and post-conditions of the -program, $\vec{x}$ and $\vec{y}$ the variables used and modified by -the program and $v$ its result. -Then this partial proof is given to the tactic \texttt{Refine} -(see~\ref{refine}, page~\pageref{refine}), which effect is to generate as many -subgoals as holes in the partial proof term. - -\medskip - -The syntax to invoke the tactic is the following: -$$ -\mbox{\tt Correctness} ~~ ident ~~ annotated\_program. -$$ -Notice that this is not exactly a \emph{tactic}, since it does not -apply to a goal. To be more rigorous, it is the combination of a -vernacular command (which creates the goal from the annotated program) -and a tactic (which partially solves it, leaving some proof -obligations to the user). - -Although \texttt{Correctness} is not a tactic, the following syntax is -available: -$$ -\mbox{\tt Correctness} ~~ ident ~~ annotated\_program ~ ; ~ tactic. -$$ -In that case, the given tactic is applied on any proof -obligation generated by the first command. - - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% Syntaxe de programmes annotes % -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -\asection{Syntax of annotated programs} - -\asubsection{Programs} - -The syntax of programs is given in figure~\ref{fig:ProgramsSyntax}. -Basically, the programming language is a purely functional kernel -with an addition of references and arrays on purely functional values. -If you do not consider the logical assertions, the syntax coincide -with \ocaml\ syntax, except for elements of arrays which are written -$t[i]$. In particular, the dereference of a mutable variable $x$ is -written $!x$ and assignment is written \verb!:=! -(for instance, the increment of the variable $x$ will -be written \verb@x := !x + 1@). -Actually, that syntax does not really matters, since it would -be extracted later to real concrete syntax, in different programming -languages. - -\begin{figure}[htbp] - \begin{center} - \leavevmode -$$ -\begin{array}{lrl} - prog & ::= & \verb!{! ~ predicate ~ \verb!}! * - ~ statement ~ [ \verb!{! ~ predicate ~ \verb!}! ] \\ - - & & \\[0.1em] - - statement - & ::= & expression \\ - & | & identifier ~ \verb!:=! ~ prog \\ - & | & identifier ~ \verb![! ~ expression ~ \verb!]! - ~ \verb!:=! ~ prog \\ - & | & \verb!let! ~ identifier ~ \verb!=! ~ \verb!ref! ~ - prog ~ \verb!in! ~ prog \\ - & | & \verb!if! ~ prog ~ \verb!then! ~ prog - ~ [ \verb!else! ~ prog ] \\ - & | & \verb!while! ~ prog ~ \verb!do! - ~ loop\_annot ~ block ~ \verb!done! \\ - & | & \verb!begin! ~ block ~ \verb!end! \\ - & | & \verb!let! ~ identifier ~ \verb!=! ~ prog ~ - \verb!in! ~ prog \\ - & | & \verb!fun! ~ binders ~ \verb!->! ~ prog \\ - & | & \verb!let! ~ \verb!rec! ~ identifier ~ binder ~ \verb!:! - ~ value\_type \\ - & & ~~ \verb!{! ~ \verb!variant! ~ wf\_arg ~ \verb!}! - ~ \verb!=! ~ prog ~ [ \verb!in! ~ prog ] \\ - & | & \verb!(! ~ prog ~~ prog ~ \verb!)! \\ - - & & \\[1em] - - expression - & ::= & identifier \\ - & | & \verb@!@ ~ identifier \\ - & | & identifier ~ \verb![! ~ expression ~ \verb!]! \\ - & | & integer \\ - & | & \verb!(! ~ expression+ \verb!)! \\ - - & & \\[1em] - - block & ::= & block\_statement ~ [ ~ \verb!;! ~ block ~ ] \\ - - & & \\[0.1em] - - block\_statement - & ::= & prog \\ - & | & \verb!label! ~ identifier \\ - & | & \verb!assert! ~ \verb!{! ~ predicate ~ \verb!}! \\ - - & & \\[1em] - - binders & ::= & \verb!(! ~ identifier,\dots,identifier ~ \verb!:! - ~ value\_type ~ \verb!)! + \\ - - & & \\[1em] - - loop\_annot - & ::= & \verb!{! ~ \verb!invariant! ~ predicate ~ - \verb!variant! ~ wf\_arg ~ \verb!}! \\ - & & \\[0.1em] - - wf\_arg & ::= & cic\_term ~ [ \verb!for! ~ cic\_term ] \\ - - & & \\[0.1em] - - predicate & ::= & cci\_term ~ [ \verb!as! ~ identifier ] \\ - - \end{array} -$$ - \caption{Syntax of annotated programs} - \label{fig:ProgramsSyntax} - \end{center} -\end{figure} - - -\paragraph{Syntactic sugar.} - -\begin{itemize} - \item \textbf{Boolean expressions:} - - Boolean expressions appearing in programs (and in particular in - \kw{if} and \kw{while} tests) are arbitrary programs of type \texttt{bool}. - In order to make programs more readable, some syntactic sugar is - provided for the usual logical connectives and the usual order - relations over type \texttt{Z}, with the following syntax: - $$ - \begin{array}{lrl} - prog - & ::= & prog ~ \verb!and! ~ prog \\ - & | & prog ~ \verb!or! ~ prog \\ - & | & \verb!not! ~ prog \\ - & | & expression ~ order\_relation ~ expression \\[1em] - order\_relation - & ::= & \verb!>! ~|~ \verb!>=! ~|~ \verb!<! ~|~ \verb!<=! - ~|~ \verb!=! ~|~ \verb!<>! \\ - \end{array} - $$ - where the order relations have the strongest precedences, - \verb!not! has a stronger precedence than \verb!and!, - and \verb!and! a stronger precedence than \verb!or!. - - Order relations in other types, like \texttt{lt}, \texttt{le}, \dots in - type \texttt{nat}, should be explicited as described in the - paragraph about \emph{Boolean expressions}, page~\pageref{prog:booleans}. - - \item \textbf{Arithmetical expressions:} - - Some syntactic sugar is provided for the usual arithmetic operator - over type \texttt{Z}, with the following syntax: - $$ - \begin{array}{lrl} - prog - & ::= & prog ~ \verb!*! ~ prog \\ - & | & prog ~ \verb!+! ~ prog \\ - & | & prog ~ \verb!-! ~ prog \\ - & | & \verb!-! ~ prog - \end{array} - $$ - where the unary operator \texttt{-} has the strongest precedence, - and \texttt{*} a stronger precedence than \texttt{+} and \texttt{-}. - - Operations in other arithmetical types (such as type \texttt{nat}) - must be explicitly written as applications, like - \texttt{(plus~a~b)}, \texttt{(pred~a)}, etc. - - \item \texttt{if $b$ then $p$} is a shortcut for - \texttt{if $b$ then $p$ else tt}, where \texttt{tt} is the - constant of type \texttt{unit}; - - \item Values in type \texttt{Z} - may be directly written as integers : 0,1,12546,\dots - Negative integers are not recognized and must be written - as \texttt{(Zinv $x$)}; - - \item Multiple application may be written $(f~a_1~\dots~a_n)$, - which must be understood as left-associa\-tive - i.e. as $(\dots((f~a_1)~a_2)\dots~a_n)$. -\end{itemize} - - -\paragraph{Restrictions.} - -You can notice some restrictions with respect to real ML programs: -\begin{enumerate} - \item Binders in functions (recursive or not) are explicitly typed, - and the type of the result of a recursive function is also given. - This is due to the lack of type inference. - - \item Full expressions are not allowed on left-hand side of assignment, but - only variables. Therefore, you can not write -\begin{verbatim} - (if b then x else y) := 0 -\end{verbatim} - But, in most cases, you can rewrite - them into acceptable programs. For instance, the previous program - may be rewritten into the following one: -\begin{verbatim} - if b then x := 0 else y := 0 -\end{verbatim} -\end{enumerate} - - - -%%%%%%%%%%%%%%% -% Type system % -%%%%%%%%%%%%%%% - -\asubsection{Typing} - -The types of annotated programs are split into two kinds: the types of -\emph{values} and the types of \emph{computations}. Those two types -families are recursively mutually defined with the following concrete syntax: -$$ -\begin{array}{lrl} - value\_type - & ::= & cic\_term \\ - & | & {cic\_term} ~ \verb!ref! \\ - & | & \verb!array! ~ cic\_term ~ \verb!of! ~ cic\_term \\ - & | & \verb!fun! ~ \verb!(! ~ x \verb!:! value\_type ~ \verb!)!\!+ - ~ computation\_type \\ - & & \\ - computation\_type - & ::= & \verb!returns! ~ identifier \verb!:! value\_type \\ - & & [\verb!reads! ~ identifier,\ldots,identifier] - ~ [\verb!writes! ~ identifier,\ldots,identifier] \\ - & & [\verb!pre! ~ predicate] ~ [\verb!post! ~ predicate] \\ - & & \verb!end! \\ - & & \\ - predicate - & ::= & cic\_term \\ - & & \\ -\end{array} -$$ - -The typing is mostly the one of ML, without polymorphism. -The user should notice that: -\begin{itemize} - \item Arrays are indexed over the type \texttt{Z} of binary integers - (defined in the module \texttt{ZArith}); - - \item Expressions must have purely functional types, and can not be - references or arrays (but, of course, you can pass mutables to - functions as call-by-variable arguments); - - \item There is no partial application. -\end{itemize} - - -%%%%%%%%%%%%%%%%%% -% Specifications % -%%%%%%%%%%%%%%%%%% - -\asubsection{Specification} - -The specification part of programs is made of different kind of -annotations, which are terms of sort \Prop\ in the Calculus of Inductive -Constructions. - -Those annotations can refer to the values of the variables -directly by their names. \emph{There is no dereference operator ``!'' in -annotations}. Annotations are read with the \Coq\ parser, so you can -use all the \Coq\ syntax to write annotations. For instance, if $x$ -and $y$ are references over integers (in type \texttt{Z}), you can write the -following annotation -$$ -\mbox{\texttt{\{ 0 < x <= x+y \}}} -$$ -In a post-condition, if necessary, you can refer to the value of the variable -$x$ \emph{before} the evaluation with the notation $x'at'$. -Actually, it is possible to refer to the value of a variable at any -moment of the evaluation with the notation $x'at'l$, -provided that $l$ is a \emph{label} previously inserted in your program -(see below the paragraph about labels). - -You have the possibility to give some names to the annotations, with -the syntax -$$ -\texttt{\{ \emph{annotation} as \emph{identifier} \}} -$$ -and then the annotation will be given this name in the proof -obligations. -Otherwise, fresh names are given automatically, of the kind -\texttt{Post3}, \texttt{Pre12}, \texttt{Test4}, etc. -You are encouraged to give explicit names, in order not to have to -modify your proof script when your proof obligations change (for -instance, if you modify a part of the program). - - -\asubsubsection{Pre- and post-conditions} - -Each program, and each of its sub-programs, may be annotated by a -pre-condition and/or a post-condition. -The pre-condition is an annotation about the values of variables -\emph{before} the evaluation, and the post-condition is an annotation -about the values of variables \emph{before} and \emph{after} the -evaluation. Example: -$$ -\mbox{\texttt{\{ 0 < x \} x := (Zplus !x !x) \{ x'at' < x \}}} -$$ -Moreover, you can assert some properties of the result of the evaluation -in the post-condition, by referring to it through the name \emph{result}. -Example: -$$ -\mbox{\texttt{(Zs (Zplus !x !x)) \{ (Zodd result) \}}} -$$ - - -\asubsubsection{Loops invariants and variants} - -Loop invariants and variants are introduced just after the \kw{do} -keyword, with the following syntax: -$$ -\begin{array}{l} - \kw{while} ~ B ~ \kw{do} \\ - ~~~ \{ ~ \kw{invariant} ~ I ~~~ \kw{variant} ~ \phi ~ \kw{for} ~ R ~ - \} \\ - ~~~ block \\ - \kw{done} -\end{array} -$$ - -The invariant $I$ is an annotation about the values of variables -when the loop is entered, since $B$ has no side effects ($B$ is a -purely functional expression). Of course, $I$ may refer to values of -variables at any moment before the entering of the loop. - -The variant $\phi$ must be given in order to establish the termination of -the loop. The relation $R$ must be a term of type $A\rightarrow -A\rightarrow\Prop$, where $\phi$ is of type $A$. -When $R$ is not specified, then $\phi$ is assumed to be of type -\texttt{Z} and the usual order relation on natural number is used. - - -\asubsubsection{Recursive functions} - -The termination of a recursive function is justified in the same way as -loops, using a variant. This variant is introduced with the following syntax -$$ -\kw{let} ~ \kw{rec} ~ f ~ (x_1:V_1)\dots(x_n:V_n) : V - ~ \{ ~ \kw{variant} ~ \phi ~ \kw{for} ~ R ~ \} = prog -$$ -and is interpreted as for loops. Of course, the variant may refer to -the bound variables $x_i$. -The specification of a recursive function is the one of its body, $prog$. -Example: -$$ -\kw{let} ~ \kw{rec} ~ fact ~ (x:Z) : Z ~ \{ ~ \kw{variant} ~ x \} = - \{ ~ x\ge0 ~ \} ~ \dots ~ \{ ~ result=x! ~ \} -$$ - - -\asubsubsection{Assertions inside blocks} - -Assertions may be inserted inside blocks, with the following syntax -$$ -\kw{begin} ~ block\_statements \dots; ~ \kw{assert} ~ \{ ~ P ~ \}; - ~ block\_statements \dots ~ \kw{end} -$$ -The annotation $P$ may refer to the values of variables at any labels -known at this moment of evaluation. - - -\asubsubsection{Inserting labels in your program} - -In order to refer to the values of variables at any moment of -evaluation of the program, you may put some \emph{labels} inside your -programs. Actually, it is only necessary to insert them inside blocks, -since this is the only place where side effects can appear. The syntax -to insert a label is the following: -$$ -\kw{begin} ~ block\_statements \dots; ~ \kw{label} ~ L; - ~ block\_statements \dots ~ \kw{end} -$$ -Then it is possible to refer to the value of the variable $x$ at step -$L$ with the notation $x'at'L$. - -There is a special label $0$ which is automatically inserted at the -beginning of the program. Therefore, $x'at'0$ will always refer to the -initial value of the variable $x$. - -\medskip - -Notice that this mechanism allows the user to get rid of the so-called -\emph{auxiliary variables}, which are usually widely used in -traditional frameworks to refer to previous values of variables. - - -%%%%%%%%%%%% -% booléens % -%%%%%%%%%%%% - -\asubsubsection{Boolean expressions}\label{prog:booleans} - -As explained above, boolean expressions appearing in \kw{if} and -\kw{while} tests are arbitrary programs of type \texttt{bool}. -Actually, there is a little restriction: a test can not do some side -effects. -Usually, a test if annotated in such a way: -$$ - B ~ \{ \myifthenelse{result}{T}{F} \} -$$ -(The \textsf{if then else} construction in the annotation is the one -of \Coq\ !) -Here $T$ and $F$ are the two propositions you want to get in the two -branches of the test. -If you do not annotate a test, then $T$ and $F$ automatically become -$B=\kw{true}$ and $B=\kw{false}$, which is the usual annotation in -Floyd-Hoare logic. - -But you should take advantages of the fact that $T$ and $F$ may be -arbitrary propositions, or you can even annotate $B$ with any other -kind of proposition (usually depending on $result$). - -As explained in the paragraph about the syntax of boolean expression, -some syntactic sugar is provided for usual order relations over type -\texttt{Z}. When you write $\kw{if} ~ x<y ~ \dots$ in your program, -it is only a shortcut for $\kw{if} ~ (\texttt{Z\_lt\_ge\_bool}~x~y) ~ \dots$, -where \texttt{Z\_lt\_ge\_bool} is the proof of -$\forall x,y:\texttt{Z}. \exists b:\texttt{bool}. - (\myifthenelse{b}{x<y}{x\ge y})$ -i.e. of a program returning a boolean with the expected post-condition. -But you can use any other functional expression of such a type. -In particular, the \texttt{Correctness} standard library comes -with a bunch of decidability theorems on type \texttt{nat}: -$$ -\begin{array}{ll} - zerop\_bool & : \forall n:\kw{nat}.\exists b:\texttt{bool}. - \myifthenelse{b}{n=0}{0<n} \\ - nat\_eq\_bool & : \forall n,m:\kw{nat}.\exists b:\texttt{bool}. - \myifthenelse{b}{n=m}{n\not=m} \\ - le\_lt\_bool & : \forall n,m:\kw{nat}.\exists b:\texttt{bool}. - \myifthenelse{b}{n\le m}{m<n} \\ - lt\_le\_bool & : \forall n,m:\kw{nat}.\exists b:\texttt{bool}. - \myifthenelse{b}{n<m}{m\le n} \\ -\end{array} -$$ -which you can combine with the logical connectives. - -It is often the case that you have a decidability theorem over some -type, as for instance a theorem of decidability of equality over some -type $S$: -$$ -S\_dec : (x,y:S)\sumbool{x=y}{\neg x=y} -$$ -Then you can build a test function corresponding to $S\_dec$ using the -operator \texttt{bool\_of\_sumbool} provided with the -\texttt{Prorgams} module, in such a way: -$$ -\texttt{Definition} ~ S\_bool ~ \texttt{:=} - [x,y:S](\texttt{bool\_of\_sumbool} ~ ? ~ ? ~ (S\_dec ~ x ~ y)) -$$ -Then you can use the test function $S\_bool$ in your programs, -and you will get the hypothesis $x=y$ and $\neg x=y$ in the corresponding -branches. -Of course, you can do the same for any function returning some result -in the constructive sum $\sumbool{A}{B}$. - - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% variables locales et globales % -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -\asection{Local and global variables} - -\asubsection{Global variables} -\comindex{Global Variable} - -You can declare a new global variable with the following command -$$ -\mbox{\texttt{Global Variable}} ~~ x ~ : ~ value\_type. -$$ -where $x$ may be a reference, an array or a function. -\Example -\begin{verbatim} -Parameter N : Z. -Global Variable x : Z ref. -Correctness foo { x < N } begin x := (Zmult 2 !x) end { x < 2*N }. -\end{verbatim} - -\comindex{Show Programs} -Each time you complete a correctness proof, the corresponding program is -added to the programs environment. You can list the current programs -environment with the command -$$ -\mbox{\texttt{Show Programs.}} -$$ - - -\asubsection{Local variables} - -Local variables are introduced with the following syntax -$$ -\mbox{\texttt{let}} ~ x ~ = ~ \mbox{\texttt{ref}} ~ e_1 -~ \mbox{\texttt{in}} ~ e_2 -$$ -where the scope of $x$ is exactly the program $e_2$. -Notice that, as usual in ML, local variables must be -initialized (here with $e_1$). - -When specifying a program including local variables, you have to take -care about their scopes. Indeed, the following two programs are not -annotated in the same way: -\begin{itemize} - \item $\kw{let} ~ x = e_1 ~ \kw{in} ~ e_2 ~ \spec{Q}$ \\ - The post-condition $Q$ applies to $e_2$, and therefore $x$ may - appear in $Q$; - - \item $(\kw{let} ~ x = e_1 ~ \kw{in} ~ e_2) ~ \spec{Q}$ \\ - The post-condition $Q$ applies to the whole program, and therefore - the local variable $x$ may \emph{not} appear in $Q$ (it is beyond - its scope). -\end{itemize} - - -%%%%%%%%%%%%%%%%% -% Function call % -%%%%%%%%%%%%%%%%% - -\asection{Function call} - -Still following the syntax of ML, the function application is written -$(f ~ a_1 ~ \ldots ~ a_n)$, where $f$ is a function and the $a_i$'s -its arguments. Notice that $f$ and the $a_i$'s may be annotated -programs themselves. - -In the general case, $f$ is a function already specified (either with -\texttt{Global Variable} or with a proof of correctness) and has a -pre-condition $P_f$ and a post-condition $Q_f$. - -As expected, a proof obligation is generated, which correspond to -$P_f$ applied to the values of the arguments, once they are evaluated. - -Regarding the post-condition of $f$, there are different possible cases: -\begin{itemize} - \item either you did not annotate the function call, writing directly - $$(f ~ a_1 ~ \ldots ~ a_n)$$ - and then the post-condition of $f$ is added automatically - \emph{if possible}: indeed, if some arguments of $f$ make side-effects - this is not always possible. In that case, you have to put a - post-condition to the function call by yourself; - - \item or you annotated it with a post-condition, say $Q$: - $$(f ~ a_1 ~ \ldots ~ a_n) ~ \spec{Q}$$ - then you will have to prove that $Q$ holds under the hypothesis that - the post-condition $Q_f$ holds (where both are - instantiated by the results of the evaluation of the $a_i$). - Of course, if $Q$ is exactly the post-condition of $f$ then - the corresponding proof obligation will be automatically - discharged. -\end{itemize} - - -%%%%%%%%%%%% -% Libraries % -%%%%%%%%%%%% - -\asection{Libraries} -\index{Imperative programs!libraries} - -The tactic comes with some libraries, useful to write programs and -specifications. -The first set of libraries is automatically loaded with the module -\texttt{Correctness}. Among them, you can find the modules: -\begin{description} - \item[ProgWf]: this module defines a family of relations $Zwf$ on type - \texttt{Z} by - $$(Zwf ~ c) = \lambda x,y. c\le x \land c \le y \land x < y$$ - and establishes that this relation is well-founded for all $c$ - (lemma \texttt{Zwf\_well\_founded}). This lemma is automatically - used by the tactic \texttt{Correctness} when necessary. - When no relation is given for the variant of a loop or a recursive - function, then $(Zwf~0)$ is used \emph{i.e.} the usual order - relation on positive integers. - - \item[Arrays]: this module defines an abstract type \texttt{array} - for arrays, with the corresponding operations \texttt{new}, - \texttt{access} and \texttt{store}. Access in a array $t$ at index - $i$ may be written \texttt{\#$t$[$i$]} in \Coq, and in particular - inside specifications. - This module also provides some axioms to manipulate arrays - expression, among which \texttt{store\_def\_1} and - \texttt{store\_def\_2} allow you to simplify expressions of the - kind \texttt{(access (store $t$ $i$ $v$) $j$)}. -\end{description} - -\noindent Other useful modules, which are not automatically loaded, are the -following: -\begin{description} - \item[Exchange]: this module defines a predicate \texttt{(exchange - $t$ $t'$ $i$ $j$)} which means that elements of indexes $i$ and - $j$ are swapped in arrays $t$ and $t'$, and other left unchanged. - This modules also provides some lemmas to establish this property - or conversely to get some consequences of this property. - - \item[Permut]: this module defines the notion of permutation between - two arrays, on a segment of the arrays (\texttt{sub\_permut}) or - on the whole array (\texttt{permut}). - Permutations are inductively defined as the smallest equivalence - relation containing the transpositions (defined in the module - \texttt{Exchange}). - - \item[Sorted]: this module defines the property for an array to be - sorted, either on the whole array (\texttt{sorted\_array}) or on a segment - (\texttt{sub\_sorted\_array}). It also provides a few lemmas to - establish this property. -\end{description} - - - -%%%%%%%%%%%%%% -% Extraction % -%%%%%%%%%%%%%% - -% \asection{Extraction} -% \index{Imperative programs!extraction of} - -% Once a program is proved, one usually wants to run it, and that's why -% this implementation comes with an extraction mechanism. -% For the moment, there is only extraction to \ocaml\ code. -% This functionality is provided by the following module: -% $$ -% \mbox{\texttt{Require ProgramsExtraction.}} -% $$ -% This extraction facility extends the extraction of functional programs -% (see chapter~\ref{Extraction}), on which it is based. -% Indeed, the extraction of functional terms (\Coq\ objects) is first -% performed by the module \texttt{Extraction}, and the extraction of -% imperative programs comes after. -% Therefore, we have kept the same syntax as for functional terms: -% $$ -% \mbox{\tt Write Caml File "\str" [ \ident$_1$ \dots\ \ident$_n$ ].} -% $$ -% where \str\ is the name given to the file to be produced (the suffix -% {\tt .ml} is added if necessary), and \ident$_1$ \dots\ \ident$_n$ the -% names of the objects to be extracted. -% That list may contain functional and imperative objects, and does not need -% to be exhaustive. - -% Of course, you can use the extraction facilities described in -% chapter~\ref{Extraction}, namely the \texttt{ML Import}, -% \texttt{Link} and \texttt{Extract} commands. - - -% \paragraph{The case of integers} -% There is no use of the \ocaml\ native integers: indeed, it would not be safe -% to use the machine integers while the correctness proof is done -% with unbounded integers (\texttt{nat}, \texttt{Z} or whatever type). -% But since \ocaml\ arrays are indexed over the type \texttt{int} -% (the machine integers) arrays indexes are converted from \texttt{Z} -% to \texttt{int} when necessary (the conversion is very fast: due -% to the binary representation of integers in type \texttt{Z}, it -% will never exceed thirty elementary steps). - -% And it is also safe, since the size of a \ocaml\ array can not be greater -% than the maximum integer ($2^{30}-1$) and since the correctness proof -% establishes that indexes are always within the bounds of arrays -% (Therefore, indexes will never be greater than the maximum integer, -% and the conversion will never produce an overflow). - - -%%%%%%%%%%%% -% Examples % -%%%%%%%%%%%% - -\asection{Examples}\label{prog:examples} - -\asubsection{Computation of $X^n$} - -As a first example, we prove the correctness of a program computing -$X^n$ using the following equations: -$$ -\left\{ -\begin{array}{lcl} -X^{2n} & = & (X^n)^2 \\ -X^{2n+1} & = & X \times (X^n)^2 -\end{array} -\right. -$$ -If $x$ and $n$ are variables containing the input and $y$ a variable that will -contain the result ($x^n$), such a program may be the following one: -\begin{center} - \begin{minipage}{8cm} - \begin{tabbing} - AA\=\kill - $m$ := $!x$ ; $y$ := $1$ ; \\ - \kw{while} $!n \not= 0$ \kw{do} \\ - \> \kw{if} $(odd ~ !n)$ \kw{then} $y$ := $!y \times !m$ ;\\ - \> $m$ := $!m \times !m$ ; \\ - \> $n$ := $!n / 2$ \\ - \kw{done} \\ - \end{tabbing} - \end{minipage} -\end{center} - - -\paragraph{Specification part.} - -Here we choose to use the binary integers of \texttt{ZArith}. -The exponentiation $X^n$ is defined, for $n \ge 0$, in the module -\texttt{Zpower}: -\begin{coq_example*} -Require Import ZArith. -Require Import Zpower. -\end{coq_example*} - -In particular, the module \texttt{ZArith} loads a module \texttt{Zmisc} -which contains the definitions of the predicate \texttt{Zeven} and -\texttt{Zodd}, and the function \texttt{Zdiv2}. -This module \texttt{ProgBool} also contains a test function -\texttt{Zeven\_odd\_bool} of type -$\forall n. \exists b. \myifthenelse{b}{(Zeven~n)}{(Zodd~n)}$ -derived from the proof \texttt{Zeven\_odd\_dec}, -as explained in section~\ref{prog:booleans}: - -\begin{coq_eval} -Require Import Ring. -\end{coq_eval} - - -\paragraph{Correctness part.} - -Then we come to the correctness proof. We first import the \Coq\ -module \texttt{Correctness}: -\begin{coq_example*} -Require Import Correctness. -Open Scope Z_scope. -\end{coq_example*} -\begin{coq_eval} -Definition Zsquare (n:Z) := n * n. -Definition Zdouble (n:Z) := 2 * n. -\end{coq_eval} - -Then we introduce all the variables needed by the program: -\begin{coq_example*} -Parameter x : Z. -Global Variable n, m, y :Z ref. -\end{coq_example*} - -At last, we can give the annotated program: -\begin{coq_example} -Correctness i_exp - {n >= 0} - begin - m := x; - y := 1; - while (!n>0) do - { invariant (Zpower x n'at'0 = y * Zpower m n /\ n >= 0) variant n } - (if (not (Zeven_odd_bool !n)) then y := (Zmult !y !m) else tt) - {Zpower x n'at'0 = y * Zpower m (Zdouble (Zdiv2 n))}; m := (Zsquare !m); - n := (Zdiv2 !n) - done - end - {y = Zpower x n'at'0}. -\end{coq_example} - -The proof obligations require some lemmas involving \texttt{Zpower} and -\texttt{Zdiv2}. You can find the whole proof in the \Coq\ standard -library (see below). -Let us make some quick remarks about this program and the way it was -written: -\begin{itemize} - \item The name \verb!n'at'0! is used to refer to the initial value of - the variable \verb!n!, as well inside the loop invariant as in - the post-condition; - - \item Purely functional expressions are allowed anywhere in the - program and they can use any purely informative \Coq\ constants; - That is why we can use \texttt{Zmult}, \texttt{Zsquare} and - \texttt{Zdiv2} in the programs even if they are not other functions - previously introduced as programs. -\end{itemize} - - -\asubsection{A recursive program} - -To give an example of a recursive program, let us rewrite the previous -program into a recursive one. We obtain the following program: -\begin{center} - \begin{minipage}{8cm} - \begin{tabbing} - AA\=AA\=AA\=\kill - \kw{let} \kw{rec} $exp$ $x$ $n$ = \\ - \> \kw{if} $n = 0$ \kw{then} \\ - \> \> 1 \\ - \> \kw{else} \\ - \> \> \kw{let} $y$ = $(exp ~ x ~ (n/2))$ \kw{in} \\ - \> \> \kw{if} $(even ~ n)$ \kw{then} $y\times y$ - \kw{else} $x\times (y\times y)$ \\ - \end{tabbing} - \end{minipage} -\end{center} - -This recursive program, once it is annotated, is given to the -tactic \texttt{Correctness}: -\begin{coq_eval} -Reset n. -\end{coq_eval} -\begin{coq_example} -Correctness r_exp - let rec exp (x:Z)(n:Z) :Z { variant n } = - {n >= 0} - (if (n=0) then 1 - else - let y = (exp x (Zdiv2 n)) in - (if (Zeven_odd_bool n) then (Zmult y y) else (Zmult x (Zmult y y))) - {result = Zpower x n}) - {result = Zpower x n}. -\end{coq_example} - -You can notice that the specification is simpler in the recursive case: -we only have to give the pre- and post-conditions --- which are the same -as for the imperative version --- but there is no annotation -corresponding to the loop invariant. -The other two annotations in the recursive program are added for the -recursive call and for the test inside the \textsf{let in} construct -(it can not be done automatically in general, -so the user has to add it by himself). - - -\asubsection{Other examples} - -You will find some other examples with the distribution of the system -\Coq, in the sub-directory \verb!contrib/correctness! of the -\Coq\ standard library. Those examples are mostly programs to compute -the factorial and the exponentiation in various ways (on types \texttt{nat} -or \texttt{Z}, in imperative way or recursively, with global -variables or as functions, \dots). - -There are also some bigger correctness developments in the -\Coq\ contributions, which are available on the web page -\verb!coq.inria.fr/contribs!. -for the moment, you can find: -\begin{itemize} - \item A proof of \emph{insertion sort} by Nicolas Magaud, ENS Lyon; - \item Proofs of \emph{quicksort}, \emph{heapsort} and \emph{find} by - the author. -\end{itemize} -These examples are fully detailed in~\cite{FilliatreMagaud99,Filliatre99c}. - - -%%%%%%%%%%%%%%% -% BUG REPORTS % -%%%%%%%%%%%%%%% - -\asection{Bugs} - -\begin{itemize} - \item There is no discharge mechanism for programs; so you - \emph{cannot} do a program's proof inside a section (actually, - you can do it, but your program will not exist anymore after having - closed the section). -\end{itemize} - -Surely there are still many bugs in this implementation. -Please send bug reports to \textsf{Jean-Christophe.Filliatre$@$lri.fr}. -Don't forget to send the version of \Coq\ used (given by -\texttt{coqtop -v}) and a script producing the bug. - - -%%% Local Variables: -%%% mode: latex -%%% TeX-master: "Reference-Manual" -%%% End: diff --git a/doc/INSTALL b/doc/INSTALL new file mode 100644 index 000000000..9223a41bd --- /dev/null +++ b/doc/INSTALL @@ -0,0 +1,65 @@ + The Coq documentation + ===================== + +The Coq documentation includes + +- A Reference Manual +- A Tutorial +- A document presenting the Coq standard library +- A list of questions/answers in the FAQ style + +The sources of the documents are mainly made of LaTeX code from which +user-readable PostScript or PDF files, or a user-browsable bunch of +html files are generated. + +Prerequisite +------------ + +To produce the documents, you need the coqtop, coq-tex, coqdoc and +gallina tools, with same version number as the current +documentation. These four tools normally come with any basic Coq +installation. + +In addition, to produce the PostScript documents, the following tools +are needed: + + - latex (latex2e) + - dvips + - bibtex + - makeindex + - pngtopnm and pnmtops (for the Reference Manual and the FAQ) + +To produce the PDF documents, the following tools are needed: + + - pdflatex + - bibtex + +To produce the html documents, the following tools are needed: + + - hevea (e.g. 1.07 works) + +To produce the documentation of the standard library, a source copy of +the coq distribution is needed. + +Compilation +----------- + +To produce all PostScript documents, do: make all-ps +To produce all PDF documents, do: make all-pdf +To produce all html documents, do: make all-html +To produce all formats of the Reference Manual, do: make refman +To produce all formats of the Tutorial, do: make tutorial +To produce all formats of the Coq Standard Library, do: make stdlib +To produce all formats of the FAQ, do: make faq + +Installation +------------ + +To install all produced documents, do: + + make DOCDIR=/some/directory/for/documentation install + +DOCDIR defauts to /usr/share/doc/coq-x.y were x.y is the version number + + + diff --git a/doc/LICENCE b/doc/LICENCE new file mode 100644 index 000000000..bb4e190a0 --- /dev/null +++ b/doc/LICENCE @@ -0,0 +1,606 @@ +The Coq Reference Manual is a collective work from the Coq Development +Team whose members are listed in the file CREDITS of the Coq source +package. All related documents (the LaTeX source and the PostScript, +PDF and html outputs) are copyright (c) INRIA 1999-2006. The material +connected to the Reference Manual 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 +http://www.opencontent.org/openpub/). Notice that options A and B are +*not* elected. + +The Coq Tutorial is a work by GŽérard Huet, Gilles Kahn and Christine +Paulin-Mohring. All documents (the LaTeX source and the PostScript, +PDF and html outputs) are copyright (c) INRIA 1999-2006 and come with +no license. + +The Coq Standard Library is a collective work from the Coq Development +Team whose members are listed in the file CREDITS of the Coq source +package. All related documents (the Coq vernacular source files and +the PostScript, PDF and html outputs) are copyright (c) INRIA +1999-2006. The material connected to the Standard Library is +distributed under the terms of the Lesser General Public License +version 2.1 or later. + +---------------------------------------------------------------------- + + *Open Publication License* + v1.0, 8 June 1999 + + +*I. REQUIREMENTS ON BOTH UNMODIFIED AND MODIFIED VERSIONS* + +The Open Publication works may be reproduced and distributed in whole or +in part, in any medium physical or electronic, provided that the terms +of this license are adhered to, and that this license or an +incorporation of it by reference (with any options elected by the +author(s) and/or publisher) is displayed in the reproduction. + +Proper form for an incorporation by reference is as follows: + + Copyright (c) <year> by <author's name or designee>. This material + may be distributed only subject to the terms and conditions set + forth in the Open Publication License, vX.Y or later (the latest + version is presently available at http://www.opencontent.org/openpub/). + +The reference must be immediately followed with any options elected by +the author(s) and/or publisher of the document (see section VI). + +Commercial redistribution of Open Publication-licensed material is +permitted. + +Any publication in standard (paper) book form shall require the citation +of the original publisher and author. The publisher and author's names +shall appear on all outer surfaces of the book. On all outer surfaces of +the book the original publisher's name shall be as large as the title of +the work and cited as possessive with respect to the title. + + +*II. COPYRIGHT* + +The copyright to each Open Publication is owned by its author(s) or +designee. + + +*III. SCOPE OF LICENSE* + +The following license terms apply to all Open Publication works, unless +otherwise explicitly stated in the document. + +Mere aggregation of Open Publication works or a portion of an Open +Publication work with other works or programs on the same media shall +not cause this license to apply to those other works. The aggregate work +shall contain a notice specifying the inclusion of the Open Publication +material and appropriate copyright notice. + +SEVERABILITY. If any part of this license is found to be unenforceable +in any jurisdiction, the remaining portions of the license remain in force. + +NO WARRANTY. Open Publication works are licensed and provided "as is" +without warranty of any kind, express or implied, including, but not +limited to, the implied warranties of merchantability and fitness for a +particular purpose or a warranty of non-infringement. + + +*IV. REQUIREMENTS ON MODIFIED WORKS* + +All modified versions of documents covered by this license, including +translations, anthologies, compilations and partial documents, must meet +the following requirements: + + 1. The modified version must be labeled as such. + 2. The person making the modifications must be identified and the + modifications dated. + 3. Acknowledgement of the original author and publisher if applicable + must be retained according to normal academic citation practices. + 4. The location of the original unmodified document must be identified. + 5. The original author's (or authors') name(s) may not be used to + assert or imply endorsement of the resulting document without the + original author's (or authors') permission. + + +*V. GOOD-PRACTICE RECOMMENDATIONS * + +In addition to the requirements of this license, it is requested from +and strongly recommended of redistributors that: + + 1. If you are distributing Open Publication works on hardcopy or + CD-ROM, you provide email notification to the authors of your + intent to redistribute at least thirty days before your manuscript + or media freeze, to give the authors time to provide updated + documents. This notification should describe modifications, if + any, made to the document. + 2. All substantive modifications (including deletions) be either + clearly marked up in the document or else described in an + attachment to the document. + 3. Finally, while it is not mandatory under this license, it is + considered good form to offer a free copy of any hardcopy and + CD-ROM expression of an Open Publication-licensed work to its + author(s). + + +*VI. LICENSE OPTIONS* + +The author(s) and/or publisher of an Open Publication-licensed document +may elect certain options by appending language to the reference to or +copy of the license. These options are considered part of the license +instance and must be included with the license (or its incorporation by +reference) in derived works. + +A. To prohibit distribution of substantively modified versions without +the explicit permission of the author(s). "Substantive modification" is +defined as a change to the semantic content of the document, and +excludes mere changes in format or typographical corrections. + +To accomplish this, add the phrase `Distribution of substantively +modified versions of this document is prohibited without the explicit +permission of the copyright holder.' to the license reference or copy. + +B. To prohibit any publication of this work or derivative works in whole +or in part in standard (paper) book form for commercial purposes is +prohibited unless prior permission is obtained from the copyright holder. + +To accomplish this, add the phrase 'Distribution of the work or +derivative of the work in any standard (paper) book form is prohibited +unless prior permission is obtained from the copyright holder.' to the +license reference or copy. + +---------------------------------------------------------------------- + + GNU LESSER GENERAL PUBLIC LICENSE + Version 2.1, February 1999 + + Copyright (C) 1991, 1999 Free Software Foundation, Inc. + 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA + Everyone is permitted to copy and distribute verbatim copies + of this license document, but changing it is not allowed. + +[This is the first released version of the Lesser GPL. It also counts + as the successor of the GNU Library Public License, version 2, hence + the version number 2.1.] + + Preamble + + The licenses for most software are designed to take away your +freedom to share and change it. By contrast, the GNU General Public +Licenses are intended to guarantee your freedom to share and change +free software--to make sure the software is free for all its users. + + This license, the Lesser General Public License, applies to some +specially designated software packages--typically libraries--of the +Free Software Foundation and other authors who decide to use it. You +can use it too, but we suggest you first think carefully about whether +this license or the ordinary General Public License is the better +strategy to use in any particular case, based on the explanations below. + + When we speak of free software, we are referring to freedom of use, +not price. Our General Public Licenses are designed to make sure that +you have the freedom to distribute copies of free software (and charge +for this service if you wish); that you receive source code or can get +it if you want it; that you can change the software and use pieces of +it in new free programs; and that you are informed that you can do +these things. + + To protect your rights, we need to make restrictions that forbid +distributors to deny you these rights or to ask you to surrender these +rights. These restrictions translate to certain responsibilities for +you if you distribute copies of the library or if you modify it. + + For example, if you distribute copies of the library, whether gratis +or for a fee, you must give the recipients all the rights that we gave +you. You must make sure that they, too, receive or can get the source +code. If you link other code with the library, you must provide +complete object files to the recipients, so that they can relink them +with the library after making changes to the library and recompiling +it. And you must show them these terms so they know their rights. + + We protect your rights with a two-step method: (1) we copyright the +library, and (2) we offer you this license, which gives you legal +permission to copy, distribute and/or modify the library. + + To protect each distributor, we want to make it very clear that +there is no warranty for the free library. Also, if the library is +modified by someone else and passed on, the recipients should know +that what they have is not the original version, so that the original +author's reputation will not be affected by problems that might be +introduced by others. + + Finally, software patents pose a constant threat to the existence of +any free program. We wish to make sure that a company cannot +effectively restrict the users of a free program by obtaining a +restrictive license from a patent holder. Therefore, we insist that +any patent license obtained for a version of the library must be +consistent with the full freedom of use specified in this license. + + Most GNU software, including some libraries, is covered by the +ordinary GNU General Public License. This license, the GNU Lesser +General Public License, applies to certain designated libraries, and +is quite different from the ordinary General Public License. We use +this license for certain libraries in order to permit linking those +libraries into non-free programs. + + When a program is linked with a library, whether statically or using +a shared library, the combination of the two is legally speaking a +combined work, a derivative of the original library. The ordinary +General Public License therefore permits such linking only if the +entire combination fits its criteria of freedom. The Lesser General +Public License permits more lax criteria for linking other code with +the library. + + We call this license the "Lesser" General Public License because it +does Less to protect the user's freedom than the ordinary General +Public License. It also provides other free software developers Less +of an advantage over competing non-free programs. These disadvantages +are the reason we use the ordinary General Public License for many +libraries. However, the Lesser license provides advantages in certain +special circumstances. + + For example, on rare occasions, there may be a special need to +encourage the widest possible use of a certain library, so that it becomes +a de-facto standard. To achieve this, non-free programs must be +allowed to use the library. A more frequent case is that a free +library does the same job as widely used non-free libraries. In this +case, there is little to gain by limiting the free library to free +software only, so we use the Lesser General Public License. + + In other cases, permission to use a particular library in non-free +programs enables a greater number of people to use a large body of +free software. For example, permission to use the GNU C Library in +non-free programs enables many more people to use the whole GNU +operating system, as well as its variant, the GNU/Linux operating +system. + + Although the Lesser General Public License is Less protective of the +users' freedom, it does ensure that the user of a program that is +linked with the Library has the freedom and the wherewithal to run +that program using a modified version of the Library. + + The precise terms and conditions for copying, distribution and +modification follow. Pay close attention to the difference between a +"work based on the library" and a "work that uses the library". The +former contains code derived from the library, whereas the latter must +be combined with the library in order to run. + + GNU LESSER GENERAL PUBLIC LICENSE + TERMS AND CONDITIONS FOR COPYING, DISTRIBUTION AND MODIFICATION + + 0. This License Agreement applies to any software library or other +program which contains a notice placed by the copyright holder or +other authorized party saying it may be distributed under the terms of +this Lesser General Public License (also called "this License"). +Each licensee is addressed as "you". + + A "library" means a collection of software functions and/or data +prepared so as to be conveniently linked with application programs +(which use some of those functions and data) to form executables. + + The "Library", below, refers to any such software library or work +which has been distributed under these terms. A "work based on the +Library" means either the Library or any derivative work under +copyright law: that is to say, a work containing the Library or a +portion of it, either verbatim or with modifications and/or translated +straightforwardly into another language. (Hereinafter, translation is +included without limitation in the term "modification".) + + "Source code" for a work means the preferred form of the work for +making modifications to it. For a library, complete source code means +all the source code for all modules it contains, plus any associated +interface definition files, plus the scripts used to control compilation +and installation of the library. + + Activities other than copying, distribution and modification are not +covered by this License; they are outside its scope. The act of +running a program using the Library is not restricted, and output from +such a program is covered only if its contents constitute a work based +on the Library (independent of the use of the Library in a tool for +writing it). Whether that is true depends on what the Library does +and what the program that uses the Library does. + + 1. You may copy and distribute verbatim copies of the Library's +complete source code as you receive it, in any medium, provided that +you conspicuously and appropriately publish on each copy an +appropriate copyright notice and disclaimer of warranty; keep intact +all the notices that refer to this License and to the absence of any +warranty; and distribute a copy of this License along with the +Library. + + You may charge a fee for the physical act of transferring a copy, +and you may at your option offer warranty protection in exchange for a +fee. + + 2. You may modify your copy or copies of the Library or any portion +of it, thus forming a work based on the Library, and copy and +distribute such modifications or work under the terms of Section 1 +above, provided that you also meet all of these conditions: + + a) The modified work must itself be a software library. + + b) You must cause the files modified to carry prominent notices + stating that you changed the files and the date of any change. + + c) You must cause the whole of the work to be licensed at no + charge to all third parties under the terms of this License. + + d) If a facility in the modified Library refers to a function or a + table of data to be supplied by an application program that uses + the facility, other than as an argument passed when the facility + is invoked, then you must make a good faith effort to ensure that, + in the event an application does not supply such function or + table, the facility still operates, and performs whatever part of + its purpose remains meaningful. + + (For example, a function in a library to compute square roots has + a purpose that is entirely well-defined independent of the + application. Therefore, Subsection 2d requires that any + application-supplied function or table used by this function must + be optional: if the application does not supply it, the square + root function must still compute square roots.) + +These requirements apply to the modified work as a whole. If +identifiable sections of that work are not derived from the Library, +and can be reasonably considered independent and separate works in +themselves, then this License, and its terms, do not apply to those +sections when you distribute them as separate works. But when you +distribute the same sections as part of a whole which is a work based +on the Library, the distribution of the whole must be on the terms of +this License, whose permissions for other licensees extend to the +entire whole, and thus to each and every part regardless of who wrote +it. + +Thus, it is not the intent of this section to claim rights or contest +your rights to work written entirely by you; rather, the intent is to +exercise the right to control the distribution of derivative or +collective works based on the Library. + +In addition, mere aggregation of another work not based on the Library +with the Library (or with a work based on the Library) on a volume of +a storage or distribution medium does not bring the other work under +the scope of this License. + + 3. You may opt to apply the terms of the ordinary GNU General Public +License instead of this License to a given copy of the Library. To do +this, you must alter all the notices that refer to this License, so +that they refer to the ordinary GNU General Public License, version 2, +instead of to this License. (If a newer version than version 2 of the +ordinary GNU General Public License has appeared, then you can specify +that version instead if you wish.) Do not make any other change in +these notices. + + Once this change is made in a given copy, it is irreversible for +that copy, so the ordinary GNU General Public License applies to all +subsequent copies and derivative works made from that copy. + + This option is useful when you wish to copy part of the code of +the Library into a program that is not a library. + + 4. You may copy and distribute the Library (or a portion or +derivative of it, under Section 2) in object code or executable form +under the terms of Sections 1 and 2 above provided that you accompany +it with the complete corresponding machine-readable source code, which +must be distributed under the terms of Sections 1 and 2 above on a +medium customarily used for software interchange. + + If distribution of object code is made by offering access to copy +from a designated place, then offering equivalent access to copy the +source code from the same place satisfies the requirement to +distribute the source code, even though third parties are not +compelled to copy the source along with the object code. + + 5. A program that contains no derivative of any portion of the +Library, but is designed to work with the Library by being compiled or +linked with it, is called a "work that uses the Library". Such a +work, in isolation, is not a derivative work of the Library, and +therefore falls outside the scope of this License. + + However, linking a "work that uses the Library" with the Library +creates an executable that is a derivative of the Library (because it +contains portions of the Library), rather than a "work that uses the +library". The executable is therefore covered by this License. +Section 6 states terms for distribution of such executables. + + When a "work that uses the Library" uses material from a header file +that is part of the Library, the object code for the work may be a +derivative work of the Library even though the source code is not. +Whether this is true is especially significant if the work can be +linked without the Library, or if the work is itself a library. The +threshold for this to be true is not precisely defined by law. + + If such an object file uses only numerical parameters, data +structure layouts and accessors, and small macros and small inline +functions (ten lines or less in length), then the use of the object +file is unrestricted, regardless of whether it is legally a derivative +work. (Executables containing this object code plus portions of the +Library will still fall under Section 6.) + + Otherwise, if the work is a derivative of the Library, you may +distribute the object code for the work under the terms of Section 6. +Any executables containing that work also fall under Section 6, +whether or not they are linked directly with the Library itself. + + 6. As an exception to the Sections above, you may also combine or +link a "work that uses the Library" with the Library to produce a +work containing portions of the Library, and distribute that work +under terms of your choice, provided that the terms permit +modification of the work for the customer's own use and reverse +engineering for debugging such modifications. + + You must give prominent notice with each copy of the work that the +Library is used in it and that the Library and its use are covered by +this License. You must supply a copy of this License. If the work +during execution displays copyright notices, you must include the +copyright notice for the Library among them, as well as a reference +directing the user to the copy of this License. Also, you must do one +of these things: + + a) Accompany the work with the complete corresponding + machine-readable source code for the Library including whatever + changes were used in the work (which must be distributed under + Sections 1 and 2 above); and, if the work is an executable linked + with the Library, with the complete machine-readable "work that + uses the Library", as object code and/or source code, so that the + user can modify the Library and then relink to produce a modified + executable containing the modified Library. (It is understood + that the user who changes the contents of definitions files in the + Library will not necessarily be able to recompile the application + to use the modified definitions.) + + b) Use a suitable shared library mechanism for linking with the + Library. A suitable mechanism is one that (1) uses at run time a + copy of the library already present on the user's computer system, + rather than copying library functions into the executable, and (2) + will operate properly with a modified version of the library, if + the user installs one, as long as the modified version is + interface-compatible with the version that the work was made with. + + c) Accompany the work with a written offer, valid for at + least three years, to give the same user the materials + specified in Subsection 6a, above, for a charge no more + than the cost of performing this distribution. + + d) If distribution of the work is made by offering access to copy + from a designated place, offer equivalent access to copy the above + specified materials from the same place. + + e) Verify that the user has already received a copy of these + materials or that you have already sent this user a copy. + + For an executable, the required form of the "work that uses the +Library" must include any data and utility programs needed for +reproducing the executable from it. However, as a special exception, +the materials to be distributed need not include anything that is +normally distributed (in either source or binary form) with the major +components (compiler, kernel, and so on) of the operating system on +which the executable runs, unless that component itself accompanies +the executable. + + It may happen that this requirement contradicts the license +restrictions of other proprietary libraries that do not normally +accompany the operating system. Such a contradiction means you cannot +use both them and the Library together in an executable that you +distribute. + + 7. You may place library facilities that are a work based on the +Library side-by-side in a single library together with other library +facilities not covered by this License, and distribute such a combined +library, provided that the separate distribution of the work based on +the Library and of the other library facilities is otherwise +permitted, and provided that you do these two things: + + a) Accompany the combined library with a copy of the same work + based on the Library, uncombined with any other library + facilities. This must be distributed under the terms of the + Sections above. + + b) Give prominent notice with the combined library of the fact + that part of it is a work based on the Library, and explaining + where to find the accompanying uncombined form of the same work. + + 8. You may not copy, modify, sublicense, link with, or distribute +the Library except as expressly provided under this License. Any +attempt otherwise to copy, modify, sublicense, link with, or +distribute the Library is void, and will automatically terminate your +rights under this License. However, parties who have received copies, +or rights, from you under this License will not have their licenses +terminated so long as such parties remain in full compliance. + + 9. You are not required to accept this License, since you have not +signed it. However, nothing else grants you permission to modify or +distribute the Library or its derivative works. These actions are +prohibited by law if you do not accept this License. Therefore, by +modifying or distributing the Library (or any work based on the +Library), you indicate your acceptance of this License to do so, and +all its terms and conditions for copying, distributing or modifying +the Library or works based on it. + + 10. Each time you redistribute the Library (or any work based on the +Library), the recipient automatically receives a license from the +original licensor to copy, distribute, link with or modify the Library +subject to these terms and conditions. You may not impose any further +restrictions on the recipients' exercise of the rights granted herein. +You are not responsible for enforcing compliance by third parties with +this License. + + 11. If, as a consequence of a court judgment or allegation of patent +infringement or for any other reason (not limited to patent issues), +conditions are imposed on you (whether by court order, agreement or +otherwise) that contradict the conditions of this License, they do not +excuse you from the conditions of this License. If you cannot +distribute so as to satisfy simultaneously your obligations under this +License and any other pertinent obligations, then as a consequence you +may not distribute the Library at all. For example, if a patent +license would not permit royalty-free redistribution of the Library by +all those who receive copies directly or indirectly through you, then +the only way you could satisfy both it and this License would be to +refrain entirely from distribution of the Library. + +If any portion of this section is held invalid or unenforceable under any +particular circumstance, the balance of the section is intended to apply, +and the section as a whole is intended to apply in other circumstances. + +It is not the purpose of this section to induce you to infringe any +patents or other property right claims or to contest validity of any +such claims; this section has the sole purpose of protecting the +integrity of the free software distribution system which is +implemented by public license practices. Many people have made +generous contributions to the wide range of software distributed +through that system in reliance on consistent application of that +system; it is up to the author/donor to decide if he or she is willing +to distribute software through any other system and a licensee cannot +impose that choice. + +This section is intended to make thoroughly clear what is believed to +be a consequence of the rest of this License. + + 12. If the distribution and/or use of the Library is restricted in +certain countries either by patents or by copyrighted interfaces, the +original copyright holder who places the Library under this License may add +an explicit geographical distribution limitation excluding those countries, +so that distribution is permitted only in or among countries not thus +excluded. In such case, this License incorporates the limitation as if +written in the body of this License. + + 13. The Free Software Foundation may publish revised and/or new +versions of the Lesser General Public License from time to time. +Such new versions will be similar in spirit to the present version, +but may differ in detail to address new problems or concerns. + +Each version is given a distinguishing version number. If the Library +specifies a version number of this License which applies to it and +"any later version", you have the option of following the terms and +conditions either of that version or of any later version published by +the Free Software Foundation. If the Library does not specify a +license version number, you may choose any version ever published by +the Free Software Foundation. + + 14. If you wish to incorporate parts of the Library into other free +programs whose distribution conditions are incompatible with these, +write to the author to ask for permission. For software which is +copyrighted by the Free Software Foundation, write to the Free +Software Foundation; we sometimes make exceptions for this. Our +decision will be guided by the two goals of preserving the free status +of all derivatives of our free software and of promoting the sharing +and reuse of software generally. + + NO WARRANTY + + 15. BECAUSE THE LIBRARY IS LICENSED FREE OF CHARGE, THERE IS NO +WARRANTY FOR THE LIBRARY, TO THE EXTENT PERMITTED BY APPLICABLE LAW. +EXCEPT WHEN OTHERWISE STATED IN WRITING THE COPYRIGHT HOLDERS AND/OR +OTHER PARTIES PROVIDE THE LIBRARY "AS IS" WITHOUT WARRANTY OF ANY +KIND, EITHER EXPRESSED OR IMPLIED, INCLUDING, BUT NOT LIMITED TO, THE +IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR +PURPOSE. THE ENTIRE RISK AS TO THE QUALITY AND PERFORMANCE OF THE +LIBRARY IS WITH YOU. SHOULD THE LIBRARY PROVE DEFECTIVE, YOU ASSUME +THE COST OF ALL NECESSARY SERVICING, REPAIR OR CORRECTION. + + 16. IN NO EVENT UNLESS REQUIRED BY APPLICABLE LAW OR AGREED TO IN +WRITING WILL ANY COPYRIGHT HOLDER, OR ANY OTHER PARTY WHO MAY MODIFY +AND/OR REDISTRIBUTE THE LIBRARY AS PERMITTED ABOVE, BE LIABLE TO YOU +FOR DAMAGES, INCLUDING ANY GENERAL, SPECIAL, INCIDENTAL OR +CONSEQUENTIAL DAMAGES ARISING OUT OF THE USE OR INABILITY TO USE THE +LIBRARY (INCLUDING BUT NOT LIMITED TO LOSS OF DATA OR DATA BEING +RENDERED INACCURATE OR LOSSES SUSTAINED BY YOU OR THIRD PARTIES OR A +FAILURE OF THE LIBRARY TO OPERATE WITH ANY OTHER SOFTWARE), EVEN IF +SUCH HOLDER OR OTHER PARTY HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH +DAMAGES. + + END OF TERMS AND CONDITIONS diff --git a/doc/Makefile.rt b/doc/Makefile.rt new file mode 100644 index 000000000..6c3281346 --- /dev/null +++ b/doc/Makefile.rt @@ -0,0 +1,43 @@ +# Makefile for building Coq Technical Reports + +# if coqc,coqtop,coq-tex are not in your PATH, you need the environment +# variable COQBIN to be correctly set +# (COQTOP is autodetected) +# (some files are preprocessed using Coq and some part of the documentation +# is automatically built from the theories sources) + +# To compile documentation, you need the following tools: +# Dvi: latex (latex2e), bibtex, makeindex, dviselect (package RPM dviutils) +# Ps: dvips, psutils (ftp://ftp.dcs.ed.ac.uk/pub/ajcd/psutils.tar.gz) +# Pdf: pdflatex +# Html: +# - hevea: http://para.inria.fr/~maranget/hevea/ +# - htmlSplit: http://coq.inria.fr/~delahaye +# Rapports INRIA: dviselect, rrkit (par Michel Mauny) + +include ./Makefile + +################### +# RT +################### +# Fabrication d'un RT INRIA (utilise rrkit de Michel Mauny) +rt/Reference-Manual-RT.dvi: refman/Reference-Manual.dvi rt/RefMan-cover.tex + dviselect -i refman/Reference-Manual.dvi -o rt/RefMan-body.dvi 3: + (cd rt; $(LATEX) RefMan-cover.tex) + set a=`tail -1 refman/Reference-Manual.log`;\ + set a=expr \("$$a" : '.*(\(.*\) pages.*'\) % 2;\ + (cd rt; if $(TEST) "$$a = 0";\ + then rrkit RefMan-cover.dvi RefMan-body.dvi Reference-Manual-RT.dvi;\ + else rrkit -odd RefMan-cover.dvi RefMan-body.dvi Reference-Manual-RT.dvi;\ + fi) + +# Fabrication d'un RT INRIA (utilise rrkit de Michel Mauny) +rt/Tutorial-RT.dvi : tutorial/Tutorial.v.dvi rt/Tutorial-cover.tex + dviselect -i rt/Tutorial.v.dvi -o rt/Tutorial-body.dvi 3: + (cd rt; $(LATEX) Tutorial-cover.tex) + set a=`tail -1 tutorial/Tutorial.v.log`;\ + set a=expr \("$$a" : '.*(\(.*\) pages.*'\) % 2;\ + (cd rt; if $(TEST) "$$a = 0";\ + then rrkit Tutorial-cover.dvi Tutorial-body.dvi Tutorial-RT.dvi;\ + else rrkit -odd Tutorial-cover.dvi Tutorial-body.dvi Tutorial-RT.dvi;\ + fi) diff --git a/doc/Program.tex b/doc/Program.tex deleted file mode 100644 index aa900ecb9..000000000 --- a/doc/Program.tex +++ /dev/null @@ -1,850 +0,0 @@ -\achapter{The Program Tactic} -\aauthor{Catherine Parent} -\label{Addoc-program} - -The facilities described in this document pertain to a special aspect of -the \Coq\ system: how to associate to a functional program, whose -specification is written in \gallina, a proof of its correctness. - -This methodology is based on the Curry-Howard isomorphism between -functional programs and constructive proofs. This isomorphism allows -the synthesis of a functional program from the constructive part of its -proof of correctness. That is, it is possible to analyze a \Coq\ proof, -to erase all its non-informative parts (roughly speaking, removing the -parts pertaining to sort \Prop, considered as comments, to keep only the -parts pertaining to sort \Set). - -This {\sl realizability interpretation} -was defined by Christine Paulin-Mohring in her PhD dissertation -\cite{Moh89b}, and -implemented as a {\sl program extraction} facility in previous versions of -\Coq~ by Benjamin Werner (see \cite{COQ93}). -However, the corresponding certified program -development methodology was very awkward: the user had to understand very -precisely the extraction mechanism in order to guide the proof construction -towards the desired algorithm. The facilities described in this chapter -attempt to do the reverse: i.e. to try and generate the proof of correctness -from the program itself, given as argument to a specialized tactic. -This work is based on the PhD dissertation of -Catherine Parent (see \cite{CPar95}) - -\asection{Developing certified programs: Motivations} -\label{program_proving} - -We want to develop certified programs automatically proved by the -system. That is to say, instead of giving a specification, an -interactive proof and then extracting a program, the user gives the -program he wants to prove and the corresponding specification. Using -this information, an automatic proof is developed which solves the -``informative'' goals without the help of the user. When the proof is -finished, the extracted program is guaranteed to be correct and -corresponds to the one given by the user. The tactic uses the fact -that the extracted program is a skeleton of its corresponding proof. - -\asection{Using {\tt Program}} -The user has to give two things: the specification (given as usual by -a goal) and the program (see section \ref{program-syntax}). Then, this program -is associated to the current goal (to know which specification it -corresponds to) and the user can use different tactics to develop an -automatic proof. - -\asubsection{\tt Realizer \term.} -\tacindex{Realizer} -\label{Realizer} -This command attaches a program {\term} to the current goal. This is a -necessary step before applying the first time the tactic {\tt -Program}. The syntax of programs is given in section \ref{program-syntax}. -If a program is already attached to the current subgoal, {\tt -Realizer} can be also used to change it. - -\asubsection{\tt Show Program.} -\comindex{Show Program}\label{Show Program} -The command \verb=Show Program= shows the program associated to the -current goal. The variant \verb=Show Program n= shows the program associated to -the nth subgoal. - -\asubsection{\tt Program.} -\tacindex{Program}\label{Program} -This tactics tries to build a proof of the current subgoal from the -program associated to the current goal. This tactic performs -\verb=Intros= then either one \verb=Apply= or one \verb=Elim= -depending on the syntax of the program. The \verb=Program= tactic -generates a list of subgoals which can be either logical or -informative. Subprograms are automatically attached to the informative -subgoals. - -When attached program are not automatically generated, an initial program -has to be given by {\tt Realizer}. - -\begin{ErrMsgs} -\item \errindex{No program associated to this subgoal}\\ -You need to attach a program to the current goal by using {\tt Realizer}. -Perhaps, you already attached a program but a {\tt Restart} or an -{\tt Undo} has removed it. -\item \errindex{Type of program and informative extraction of goal do not coincide} -\item \errindex{Cannot attach a realizer to a logical goal}\\ -The current goal is non informative (it lives in the world {\tt Prop} -of propositions or {\tt Type} of abstract sets) while it should lives -in the world {\tt Set} of computational objects. -\item \errindex{Perhaps a term of the Realizer is not an FW - term}\texttt{ and you then have to replace it by its extraction}\\ -Your program contains non informative subterms. -\end{ErrMsgs} - -\begin{Variants} -\item{\tt Program\_all.} - \tacindex{Program\_all}\label{Program_all}\\ - This tactic is equivalent to the composed tactic - \verb=Repeat (Program OrElse Auto)=. It repeats the \verb=Program= - tactic on every informative subgoal and tries the \verb=Auto= tactic - on the logical subgoals. Note that the work of the \verb=Program= - tactic is considered to be finished when all the informative subgoals - have been solved. This implies that logical lemmas can stay at the end - of the automatic proof which have to be solved by the user. -\item {\tt Program\_Expand} - \tacindex{Program\_Expand}\label{Program_Expand}\\ - The \verb=Program_Expand= tactic transforms the current program into - the same program with the head constant expanded. This tactic - particularly allows the user to force a program to be reduced before - each application of the \verb=Program= tactic. - - \begin{ErrMsgs} - \item \errindex{Not reducible}\\ - The head of the program is not a constant or is an opaque constant. - need to attach a program to the current goal by using {\tt Realizer}. - Perhaps, you already attached a program but a {\tt Restart} or an - {\tt Undo} has removed it. - \end{ErrMsgs} -\end{Variants} - -\asubsection{Hints for {\tt Program}} - -\begin{description} -\item[Mutual inductive types] The \verb=Program= tactic can deal with - mutual inductive types. But, this needs the use of - annotations. Indeed, when associating a mutual fixpoint program to a - specification, the specification is associated to the first (the - outermost) function defined by the fixpoint. But, the specifications - to be associated to the other functions cannot be automatically - derived. They have to be explicitly given by the user as - annotations. See section \ref{program-ex-mutual} for an example. - -\item[Constants] The \verb=Program= tactic is very sensitive to the - status of constants. Constants can be either opaque (their body - cannot be viewed) or transparent. The best of way of doing is to - leave constants opaque (this is the default). If it is needed after, - it is best to use the \verb=Transparent= command {\bf after} having - used the \verb=Program= tactic. -\end{description} - -\asection{Syntax for programs} -\label{program-syntax} -\asubsection{Pure programs} -The language to express programs is called \real\footnote{It - corresponds to \FW\ plus inductive definitions}. Programs are -explicitly typed\footnote{This information is not strictly needed but - was useful for type checking in a first experiment.} like terms -extracted from proofs. Some extra expressions have been added to have -a simpler syntax. - -This is the raw form of what we call pure programs. But, in fact, it -appeared that this simple type of programs is not sufficient. Indeed, -all the logical part useful for the proof is not contained in these -programs. That is why annotated programs are introduced. - -\asubsection{Annotated programs} -The notion of annotation introduces in a program a logical assertion -that will be used for the proof. The aim of the \verb=Program= tactic -is to start from a specification and a program and to generate -subgoals either logical or associated with programs. However, to find -the good specification for subprograms is not at all trivial in -general. For instance, if we have to find an invariant for a loop, or -a well founded order in a recursive call. - -So, annotations add in a program the logical part which is needed for -the proof and which cannot be automatically retrieved. This allows the -system to do proofs it could not do otherwise. - -For this, a particular syntax is needed which is the following: since -they are specifications, annotations follow the same internal syntax -as \Coq~terms. We indicate they are annotations by putting them -between \verb={= and \verb=}= and preceding them with \verb=:: ::=. -Since annotations are \Coq~terms, they can involve abstractions over -logical propositions that have to be declared. Annotated-$\lambda$ -have to be written between \verb=[{= and \verb=}]=. -Annotated-$\lambda$ can be seen like usual $\lambda$-bindings but -concerning just annotations and not \Coq~programs. - -\asubsection{Recursive Programs} -Programs can be recursively defined using the following syntax: \verb=<={\it - type-of-the-result}\verb=> rec= \index{rec@{\tt rec}} {\it - name-of-the-induction-hypothesis} \verb=:: :: {= {\it - well-founded-order-of-the-recursion} \verb=}= and then the body of -the program (see section \ref{program-examples}) which must always begin with -an abstraction [x:A] where A is the type of the arguments of the -function (also on which the ordering relation acts). - -\asubsection{Implicit arguments} - -A synthesis of implicit arguments has been added in order to -allow the user to write a minimum of types in a program. Then, it is -possible not to write a type inside a program term. This type has then -to be automatically synthesized. For this, it is necessary to indicate -where the implicit type to be synthesized appears. The syntax is the -current one of implicit arguments in \Coq: the question mark -\verb+?+. - -This synthesis of implicit arguments is not possible everywhere in a -program. In fact, the synthesis is only available inside a -\verb+Match+, a \verb+Cases+ or a \verb+Fix+ construction (where -\verb+Fix+ is a syntax for defining fixpoints). - -\asubsection{Grammar} -The grammar for programs is described in figure \ref{pgm-syntax}. - -\begin{figure} -\begin{tabular}{lcl} -{\pg} & ::= & {\ident}\\ - & $|$ & {\tt ?} \\ - & $|$ & {\tt [} {\ident} {\tt :} {\pg} {\tt ]} {\pg} \\ - & $|$ & {\tt [} {\ident} {\tt ]} {\pg} \\ - & $|$ & {\tt (} {\ident} {\tt :} {\pg} {\tt )} {\pg} \\ - & $|$ & {\tt (} {\pgs} {\tt )} \\ - & $|$ & {\tt Match} {\pg} {\tt with} {\pgs} {\tt end} \\ - & $|$ & \verb=<={\pg}\verb=>={\tt Match} {\pg} {\tt with} {\pgs} {\tt end} \\ - & $|$ & {\tt Cases} {\pg} {\tt of} \sequence{\eqn} {|} {\tt end} \\ - & $|$ & \verb=<={\pg}\verb=>={\tt Cases} {\pg} {\tt of} - \sequence{\eqn} {|} {\tt end} \\ - & $|$ & {\tt Fix} {\ident} \verb.{.\nelist{\fixpg}{with} \verb.}. \\ - & $|$ & {\tt Cofix} {\ident} \{{\ident} {\tt :} {\pg} {\tt :=} {\pg} - {\tt with} {\ldots} {\tt with} {\ident} {\tt :} {\pg} {\tt :=} {\pg}\} \\ - & $|$ & {\pg} {\tt ::} {\tt ::} \{ {\term} \} \\ - & $|$ & {\tt [\{} {\ident} {\tt :} {\term} {\tt \}]} {\pg} \\ - & $|$ & {\tt let} - {\tt (} {\ident} {\tt ,} {\ldots} {\tt ,} {\ident} {\tt ,} {\dots} - {\tt ,} {\ident} {\tt )} {\tt =} {\pg} {\tt in} {\pg} \\ -% & $|$ & \verb=<={\pg}\verb=>={\tt let} {\tt (} {\ident} {\tt ,} {\ldots} {\tt -% ,} {\ident} {\tt :} {\pg} {\tt ;} {\ldots} {\tt ;} {\ident} {\tt ,} -% {\ldots} {\tt ,} {\ident} {\tt :} {\pg} {\tt )} {\tt =} {\pg} {\tt -% in} {\pg} \\ - & $|$ & \verb=<={\pg}\verb=>={\tt let} {\tt (} {\ident} {\tt ,} - {\ldots} {\tt ,} {\ldots} {\tt ,} {\ident} {\tt )} {\tt =} {\pg} {\tt - in} {\pg} \\ - & $|$ & {\tt if} {\pg} {\tt then} {\pg} {\tt else} {\pg} \\ - & $|$ & \verb=<={\pg}\verb=>={\tt if} {\pg} {\tt then} {\pg} {\tt - else} {\pg} \\ - & $|$ & \verb=<={\pg}\verb=>={\tt rec} {\ident} {\tt ::} {\tt ::} \{ \term \} - {\tt [} {\ident} {\tt :} {\pg} {\tt ]} {\pg} \\ - {\pgs} & ::= & \pg \\ - & $|$ & {\pg} {\pgs}\\ -{\fixpg} & ::= & {\ident} {\tt [} \nelist{\typedidents}{;} {\tt ]} {\tt :} {\pg} {\tt :=} {\pg} \\ - & $|$ & {\ident} {\tt /} {\num} {\tt :} {\pg} {\tt :=} {\pg} {\tt ::} {\tt ::} \{ {\term} \} \\ -{\simplepattern} & ::= & {\ident} \\ - & $|$ & \verb!(! \nelist{\ident}{} \verb!)! \\ -{\eqn} & ::= & {\simplepattern} ~\verb!=>! ~\pg \\ -\end{tabular} -\caption{Syntax of annotated programs} -\label{pgm-syntax} -\end{figure} - -As for {\Coq} terms (see section \ref{term}), {\tt (}{\pgs}{\tt )} -associates to the left. The syntax of {\term} is the one in section. -The infix annotation operator \verb!:: ::! binds more than the -abstraction and product constructions. -\ref{term}. - -The reference to an identifier of the \Coq\ context (in particular a -constant) inside a program of the -language \real\ is a reference to its extracted contents. - -\asection{Examples} -\label{program-examples} -\asubsection{Ackermann Function} -Let us give the specification of Ackermann's function. We want to -prove that for every $n$ and $m$, there exists a $p$ such that -$ack(n,m)=p$ with: - -\begin{eqnarray*} -ack(0,n) & = & n+1 \\ -ack(n+1,0) & = & ack(n,1) \\ -ack(n+1,m+1) & = & ack(n,ack(n+1,m)) -\end{eqnarray*} - -An ML program following this specification can be: - -\begin{verbatim} -let rec ack = function - 0 -> (function m -> Sm) - | Sn -> (function 0 -> ack n 1 - | Sm -> ack n (ack Sn m)) -\end{verbatim} - -Suppose we give the following definition in \Coq~of a ternary relation -\verb=(Ack n m p)= in a Prolog like form representing $p=ack(n,m)$: - -\begin{coq_example*} -Inductive Ack : nat->nat->nat->Prop := - AckO : (n:nat)(Ack O n (S n)) - | AcknO : (n,p:nat)(Ack n (S O) p)->(Ack (S n) O p) - | AckSS : (n,m,p,q:nat)(Ack (S n) m q)->(Ack n q p) - ->(Ack (S n) (S m) p). -\end{coq_example*} -Then the goal is to prove that $\forall n,m .\exists p.(Ack~n~m~p)$, so -the specification is: - -\verb!(n,m:nat){p:nat|(Ack n m p)}!. -The associated {\real} program corresponding to the above ML program can be defined as a fixpoint: -\begin{coq_example*} -Fixpoint ack_func [n:nat] : nat -> nat := - Cases n of - O => [m:nat](S m) - | (S n') => Fix ack_func2 {ack_func2 [m:nat] : nat := - Cases m of - O => (ack_func n' (S O)) - | (S m') => (ack_func n' (ack_func2 m')) - end} - end. -\end{coq_example*} -The program is associated by using \verb=Realizer ack_func=. The -program is automatically expanded. Each realizer which is a constant -is automatically expanded. Then, by repeating the \verb=Program= -tactic, three logical lemmas are generated and are easily solved by -using the property Ack0, Ackn0 and AckSS. -\begin{coq_eval} -Goal (n,m:nat){p:nat|(Ack n m p)}. -Realizer ack_func. -\end{coq_eval} -\begin{coq_example} -Repeat Program. -\end{coq_example} - - -\asubsection{Euclidean Division} -This example shows the use of {\bf recursive programs}. Let us -give the specification of the euclidean division algorithm. We want to -prove that for $a$ and $b$ ($b>0$), there exist $q$ and $r$ such that -$a=b*q+r$ and $b>r$. - -An ML program following this specification can be: -\begin{verbatim} -let div b a = divrec a where rec divrec = function - if (b<=a) then let (q,r) = divrec (a-b) in (Sq,r) - else (0,a) -\end{verbatim} -Suppose we give the following definition in \Coq~which describes what -has to be proved, ie, $\exists q \exists r.~(a=b*q+r \wedge ~b>r)$: -\begin{coq_eval} -Abort. -Require Arith. -\end{coq_eval} -\begin{coq_example*} -Inductive diveucl [a,b:nat] : Set - := divex : (q,r:nat)(a=(plus (mult q b) r))->(gt b r) - ->(diveucl a b). -\end{coq_example*} -The decidability of the ordering relation has to be proved first, by -giving the associated function of type \verb!nat->nat->bool!: -\begin{coq_example*} -Theorem le_gt_dec : (n,m:nat){(le n m)}+{(gt n m)}. -Realizer Fix le_gt_bool {le_gt_bool [n:nat] : nat -> bool := - Cases n of - | O => [m:nat]true - | (S n') => [m:nat]Cases m of - | O => false - | (S m') => (le_gt_bool n' m') - end - end}. -Program_all. -Save. -\end{coq_example*} -Then the specification is \verb!(b:nat)(gt b O)->(a:nat)(diveucl a b)!. -The associated program corresponding to the ML program will be: -\begin{coq_eval} -Definition lt := [n,m:nat](gt m n). -Theorem eucl_dev : (b:nat)(gt b O)->(a:nat)(diveucl a b). -\end{coq_eval} -\begin{coq_example*} -Realizer - [b:nat](<nat*nat>rec div :: :: { lt } - [a:nat]if (le_gt_dec b a) - then let (q,r) = (div (minus a b)) - in ((S q),r) - else (O,a)). -\end{coq_example*} -Where \verb=lt= is the well-founded ordering relation defined by: -\begin{coq_example} -Print lt. -\end{coq_example} -Note the syntax for recursive programs as explained before. The -\verb=rec= construction needs 4 arguments: the type result of the -function (\verb=nat*nat= because it returns two natural numbers) -between \verb=<= and \verb=>=, the name of the induction hypothesis -(which can be used for recursive calls), the ordering relation -\verb=lt= (as an annotation because it is a specification), and the -program itself which must begin with a $\lambda$-abstraction. The -specification of \verb=le_gt_dec= is known because it is a previous -lemma. -The term \verb!(le_gt_dec b a)! is seen by the \verb!Program! tactic -as a term of type \verb!bool! which satisfies the specification -\verb!{(le a b)}+{(gt a b)}!. -The tactics \verb=Program_all= or \verb=Program= can be used, and the -following logical lemmas are obtained: -\begin{coq_example} -Repeat Program. -\end{coq_example} -The subgoals 4, 5 and 6 are resolved by \verb=Auto= (if you use -\verb=Program_all= they don't appear, because \verb=Program_all= tries -to apply \verb=Auto=). The other ones have to be solved by the user. - - -\asubsection{Insertion sort} -This example shows the use of {\bf annotations}. Let us give the -specification of a sorting algorithm. We want to prove that for a -sorted list of natural numbers $l$ and a natural number $a$, we can -build another sorted list $l'$, containing all the elements of $l$ -plus $a$. - -An ML program implementing the insertion sort and following this -specification can be: -\begin{verbatim} -let sort a l = sortrec l where rec sortrec = function - [] -> [a] - | b::l' -> if a<b then a::b::l' else b::(sortrec l') -\end{verbatim} -Suppose we give the following definitions in \Coq: - -First, the decidability of the ordering relation: -\begin{coq_eval} -Reset Initial. -Require Le. -Require Gt. -\end{coq_eval} -\begin{coq_example*} -Fixpoint inf_dec [n:nat] : nat -> bool := -[m:nat]Cases n of - O => true - | (S n') => Cases m of - O => false - | (S m') => (inf_dec n' m') - end - end. -\end{coq_example*} - -The definition of the type \verb=list=: -\begin{coq_example*} -Inductive list : Set := nil : list | cons : nat -> list -> list. -\end{coq_example*} - -We define the property for an element \verb=x= to be {\bf in} a list -\verb=l= as the smallest relation such that: $\forall a \forall -l~(In~x~l) \Ra (In~x~(a::l))$ and $\forall l~(In~x~(x::l))$. -\begin{coq_example*} -Inductive In [x:nat] : list->Prop - := Inl : (a:nat)(l:list)(In x l) -> (In x (cons a l)) - | Ineq : (l:list)(In x (cons x l)). -\end{coq_example*} - -A list \verb=t'= is equivalent to a list \verb=t= with one added -element \verb=y= iff: $(\forall x~(In~x~t) \Ra (In~x~t'))$ and -$(In~y~t')$ and $\forall x~(In~x~t') \Ra ((In~x~t) \vee y=x)$. The -following definition implements this ternary conjunction. -\begin{coq_example*} -Inductive equiv [y:nat;t,t':list]: Prop := - equiv_cons : - ((x:nat)(In x t)->(In x t')) - -> (In y t') - ->((x:nat)(In x t')->((In x t)\/y=x)) - -> (equiv y t t'). -\end{coq_example*} - -Definition of the property of list to be sorted, still defined -inductively: -\begin{coq_example*} -Inductive sorted : list->Prop - := sorted_nil : (sorted nil) - | sorted_trans : (a:nat)(sorted (cons a nil)) - | sorted_cons : (a,b:nat)(l:list)(sorted (cons b l)) -> (le a b) - -> (sorted (cons a (cons b l))). -\end{coq_example*} -Then the specification is:\\ -\verb!(a:nat)(l:list)(sorted l)->{l':list|(equiv a l l')&(sorted l')}!. - -The associated \real\ program corresponding to the ML program will be: -\begin{coq_eval} -Lemma toto : (a:nat)(l:list)(sorted l)->{l':list|(equiv a l l')&(sorted l')}. -\end{coq_eval} -\begin{coq_example*} -Realizer - Fix list_insert{list_insert [a:nat; l:list] : list := - Cases l of - | nil => (cons a nil) - | (cons b m) => - if (inf_dec b a) :: :: { {(le b a)}+{(gt b a)} } - then (cons b (list_insert a m)) - else (cons a (cons b m)) - end}. -\end{coq_example*} -% Realizer [a:nat][l:list] -% Match l with -% (cons a nil) -% [b,m,H]if (inf_dec b a) :: :: { {(le b a)}+{(gt b a)} } -% then (cons b H) -% else (cons a (cons b m)) -% end. -Note that we have defined \verb=inf_dec= as the program realizing the -decidability of the ordering relation on natural numbers. But, it has -no specification, so an annotation is needed to give this -specification. This specification is used and then the decidability of -the ordering relation on natural numbers has to be proved using the -index program. - -Suppose \verb=Program_all= is used, a few logical -lemmas are obtained (which have to be solved by the user): -\begin{coq_example} -Program_all. -\end{coq_example} - - -\asubsection{Quicksort} -This example shows the use of {\bf programs using previous -programs}. Let us give the specification of Quicksort. We want to -prove that for a list of natural numbers $l$, we can build a sorted -list $l'$, which is a permutation of the previous one. - -An ML program following this specification can be: -\begin{verbatim} -let rec quicksort l = function - [] -> [] - | a::m -> let (l1,l2) = splitting a m in - let m1 = quicksort l1 and - let m2 = quicksort l2 in m1@[a]@m2 -\end{verbatim} -Where \verb=splitting= is defined by: -\begin{verbatim} -let rec splitting a l = function - [] -> ([],[]) - | b::m -> let (l1,l2) = splitting a m in - if a<b then (l1,b::l2) - else (b::l1,l2) -\end{verbatim} -Suppose we give the following definitions in \Coq: - -Declaration of the ordering relation: -\begin{coq_eval} -Reset Initial. -Require List. -Require Gt. -\end{coq_eval} -\begin{coq_example*} -Variable inf : A -> A -> Prop. -Definition sup := [x,y:A]~(inf x y). -Hypothesis inf_sup : (x,y:A){(inf x y)}+{(sup x y)}. -\end{coq_example*} -Definition of the concatenation of two lists: -\begin{coq_eval} -Write State toto. -\end{coq_eval} -\begin{coq_example*} -Fixpoint app [l:list] : list -> list - := [m:list]Cases l of - nil => m - | (cons a l1) => (cons a (app l1 m)) end. -\end{coq_example*} -\begin{coq_eval} -Restore State toto. -\end{coq_eval} -Definition of the permutation of two lists: -\begin{coq_eval} -Definition mil := [a:A][l,m:list](app l (cons a m)) : A->list->list->list. -Lemma mil_app : (a:A)(l,m,n:list)(mil a l (app m n))=(app (mil a l m) n). - Intros. - Unfold mil. - Elim (ass_app l (cons a m) n). - Auto. -Save. -\end{coq_eval} -\begin{coq_example*} -Inductive permut : list->list->Prop := - permut_nil : (permut nil nil) - |permut_tran : (l,m,n:list)(permut l m)->(permut m n)->(permut l n) - |permut_cmil : (a:A)(l,m,n:list) - (permut l (app m n))->(permut (cons a l) (mil a m n)) - |permut_milc : (a:A)(l,m,n:list) - (permut (app m n) l)->(permut (mil a m n) (cons a l)). -\end{coq_example*} -\begin{coq_eval} -Hints Resolve permut_nil permut_cmil permut_milc. -Lemma permut_cons : (a:A)(l,m:list)(permut l m)->(permut (cons a l) (cons a m)). - Intros. - Change (permut (cons a l) (mil a nil m)). - Auto. -Save. -Hints Resolve permut_cons. -Lemma permut_refl : (l:list)(permut l l). - Induction l ; Auto. -Save. -Hints Resolve permut_refl. -Lemma permut_sym : (l,m:list)(permut l m)->(permut m l). - Intros l m h1 ; Elim h1 ; Auto. - Intros l0 m0 n h2 h3 h4 h5. - Apply permut_tran with m0 ; Auto. -Save. -Hints Immediate permut_sym. -Lemma permut_app1 : (m1,n1,l:list)(permut m1 n1)->(permut (app l m1) (app l n1)). - Intros ; Elim l ; Simpl ; Auto. -Save. -Hints Resolve permut_app1. -Lemma permut_app_mil : (a:A)(l1,m1,l2,m2,n2:list) - (permut (app l1 m1) (app (app l2 m2) n2)) - -> (permut (app (cons a l1) m1) (app (mil a l2 m2) n2)). - Intros ; Simpl. - Elim (mil_app a l2 m2 n2). - Apply permut_cmil. - Elim (app_ass l2 m2 n2) ; Auto. -Save. -Hints Resolve permut_app_mil. -Lemma permut_app_app : (m1,m2,n1,n2 :list) - (permut m1 n1)->(permut m2 n2)->(permut (app m1 m2) (app n1 n2)). - Intros m1 m2 n1 n2 h1 h2. - Elim h1 ; Intros. - exact h2. - Apply permut_tran with (app m n2) ; Auto. - Apply permut_tran with (app m m2) ; Auto. - Auto. - Apply permut_sym ; Auto. -Save. -Hints Resolve permut_app_app. -Lemma permut_app : (m,m1,m2,n1,n2 :list)(permut m1 n1)->(permut m2 n2)-> - (permut m (app m1 m2))->(permut m (app n1 n2)). - Intros. - Apply permut_tran with (app m1 m2) ; Auto. -Save. -\end{coq_eval} -The definitions \verb=inf_list= and \verb=sup_list= allow to know if -an element is lower or greater than all the elements of a list: -\begin{coq_example*} -Section Rlist_. -Variable R : A->Prop. -Inductive Rlist : list -> Prop := - Rnil : (Rlist nil) - | Rcons : (x:A)(l:list)(R x)->(Rlist l)->(Rlist (cons x l)). -\end{coq_example*} -\begin{coq_eval} -Hints Resolve Rnil Rcons. -Lemma Rlist_app : (m,n:list)(Rlist m)->(Rlist n)->(Rlist (app m n)). - Intros m n h1 h2 ; Elim h1 ; Simpl ; Auto. -Save. -Hints Resolve Rlist_app. -Section Rlist_cons_. -Variable a : A. -Variable l : list. -Hypothesis Rc : (Rlist (cons a l)). -Lemma Rlist_cons : (R a)/\(Rlist l). - Inversion_clear Rc; Auto. -Save. -End Rlist_cons_. -Section Rlist_append. -Variable n,m : list. -Lemma Rlist_appd : (Rlist (app n m))->((Rlist n)/\(Rlist m)). -Elim n ; Simpl; Auto. -Intros a y h1 h2. -Elim (Rlist_cons a (app y m)) ; Auto. -Intros h3 h4; Elim h1 ; Auto. -Save. -End Rlist_append. -Hints Resolve Rlist_appd. -Lemma Rpermut : (m,n:list)(permut m n)->(Rlist m)->(Rlist n). - Intros m n h1 ; Elim h1 ; Unfold mil ; Auto. - Intros a l m0 n0 h2 h3 h4. - Elim (Rlist_cons a l); Auto. - Intros h5 h6; Elim (Rlist_appd m0 n0); Auto. - Intros a l m0 n0 h2 h3 h4. - Elim (Rlist_appd m0 (cons a n0)) ; Auto. - Intros h5 h6; Elim (Rlist_cons a n0) ; Auto. -Save. -\end{coq_eval} -\begin{coq_example*} -End Rlist_. -Hints Resolve Rnil Rcons. -\end{coq_example*} -\begin{coq_eval} -Hints Resolve Rlist_app. -\end{coq_eval} -\begin{coq_example*} -Section Inf_Sup. -Hypothesis x : A. -Hypothesis l : list. -Definition inf_list := (Rlist (inf x) l). -Definition sup_list := (Rlist (sup x) l). -End Inf_Sup. -\end{coq_example*} -\begin{coq_eval} -Hints Unfold inf_list sup_list. -\end{coq_eval} -Definition of the property of a list to be sorted: -\begin{coq_example*} -Inductive sort : list->Prop := - sort_nil : (sort nil) - | sort_mil : (a:A)(l,m:list)(sup_list a l)->(inf_list a m) - ->(sort l)->(sort m)->(sort (mil a l m)). -\end{coq_example*} -\begin{coq_eval} -Hints Resolve sort_nil sort_mil. -Lemma permutapp : (a0:A)(y,l1,l2:list)(permut y (app l1 l2))->(permut (cons a0 y) (app l1 (cons a0 l2))). -Intros. -exact (permut_cmil a0 y l1 l2 H). -Save. -Hints Resolve permutapp. -Lemma sortmil : (a:A)(x,x0,l1,l2:list)(sup_list a l1)->(inf_list a l2)->(sort x)->(sort x0)->(permut l1 x)->(permut l2 x0)->(sort (mil a x x0)). -Intros. -Apply sort_mil ; Auto. -Unfold sup_list ; Apply Rpermut with l1 ; Auto. -Unfold inf_list ; Apply Rpermut with l2 ; Auto. -Save. -\end{coq_eval} - -\noindent Then the goal to prove is -$\forall l~\exists m~(sort~m) \wedge (permut~l~m)$ and the specification is - -\verb!(l:list){m:list|(sort m)&(permut l m)!. - -\noindent Let us first prove a preliminary lemma. Let us define \verb=ltl= a -well-founded ordering relation. - -\begin{coq_example*} -Definition ltl := [l,m:list](gt (length m) (length l)). -\end{coq_example*} -\begin{coq_eval} -Hints Unfold ltl. -Lemma ltl_cons : (a,a0:A)(l1,y:list)(ltl l1 (cons a y))->(ltl l1 (cons a (cons a0 y))). -Unfold ltl; Simpl; Auto. -Save. -Hints Resolve ltl_cons. -Lemma ltl_cons_cons : (a,a0:A)(l2,y:list)(ltl l2 (cons a y))->(ltl (cons a0 l2) (cons a (cons a0 y))). -Unfold ltl; Simpl; Auto with arith.. -Save. -Hints Resolve ltl_cons_cons. -Require Wf_nat. -\end{coq_eval} -Let us then give a definition of \verb=Splitting_spec= corresponding -to\\ -$\exists l_1 \exists l_2.~(sup\_list~a~l_1) \wedge (inf\_list~a~l_2) -\wedge (l \equiv l_1@l_2) \wedge (ltl~l_1~(a::l)) \wedge -(ltl~l2~(a::l))$ and a theorem on this definition. -\begin{coq_example*} -Inductive Splitting_spec [a:A; l:list] : Set := - Split_intro : (l1,l2:list)(sup_list a l1)->(inf_list a l2) - ->(permut l (app l1 l2)) - ->(ltl l1 (cons a l))->(ltl l2 (cons a l)) - ->(Splitting_spec a l). -\end{coq_example*} -\begin{coq_example*} -Theorem Splitting : (a:A)(l:list)(Splitting_spec a l). -Realizer - Fix split {split [a:A;l:list] : list*list := - Cases l of - | nil => (nil,nil) - | (cons b m) => let (l1,l2) = (split a m) in - if (inf_sup a b) - then (* inf a b *) (l1,(cons b l2)) - else (* sup a b *) ((cons b l1),l2) - end}. -Program_all. -Simpl; Auto. -Save. -\end{coq_example*} -% Realizer [a:A][l:list] -% Match l with -% (* nil *) (nil,nil) -% (* cons *) [b,m,ll]let (l1,l2) = ll in -% if (inf_sup a b) -% then (* inf a b *) (l1,(cons b l2)) -% else (* sup a b *) ((cons b l1),l2) -% end. - -The associated {\real} program to the specification we wanted to first -prove and corresponding to the ML program will be: -\begin{coq_example*} -Lemma Quicksort: (l:list){m:list|(sort m)&(permut l m)}. -Realizer <list>rec quick :: :: { ltl } - [l:list]Cases l of - nil => nil - | (cons a m) => let (l1,l2) = (Splitting a m) in - (mil a (quick l1) (quick l2)) - end. -\end{coq_example*} -Then \verb=Program_all= gives the following logical lemmas (they have -to be resolved by the user): -\begin{coq_example} -Program_all. -\end{coq_example} -\begin{coq_eval} -Abort. -\end{coq_eval} - -\asubsection{Mutual Inductive Types} -\label{program-ex-mutual} -This example shows the use of {\bf mutual inductive types} with -\verb=Program=. Let us give the specification of trees and forest, and -two predicate to say if a natural number is the size of a tree or a -forest. - -\begin{coq_example*} -Section TreeForest. - -Variable A : Set. - -Mutual Inductive - tree : Set := node : A -> forest -> tree -with forest : Set := empty : forest - | cons : tree -> forest -> forest. - -Mutual Inductive Tree_Size : tree -> nat -> Prop := - Node_Size : (n:nat)(a:A)(f:forest)(Forest_Size f n) - ->(Tree_Size (node a f) (S n)) -with Forest_Size : forest -> nat -> Prop := - Empty_Size : (Forest_Size empty O) -| Cons_Size : (n,m:nat)(t:tree)(f:forest) - (Tree_Size t n) - ->(Forest_Size f m) - ->(Forest_Size (cons t f) (plus n m)). - -Hints Resolve Node_Size Empty_Size Cons_Size. -\end{coq_example*} - -Then, let us associate the two mutually dependent functions to compute -the size of a forest and a tree to the the following specification: - -\begin{coq_example*} -Theorem tree_size_prog : (t:tree){n:nat | (Tree_Size t n)}. - -Realizer [t:tree] -(Fix tree_size{ - tree_size [t:tree] : nat := let (a,f) = t in (S (forest_size f)) - with forest_size /1 : forest -> nat - := ([f:forest]Cases f of - empty => O - | (cons t f') => (plus (tree_size t) (forest_size f')) - end) - :: :: {(f:forest) {n:nat | (Forest_Size f n)}}} - t). -\end{coq_example*} - -It is necessary to add an annotation for the \verb=forest_size= -function. Indeed, the global specification corresponds to the -specification of the \verb=tree_size= function and the specification -of \verb=forest_size= cannot be automatically inferred from the -initial one. - -Then, the \verb=Program_all= tactic can be applied: -\begin{coq_example} -Program_all. -Save. -\end{coq_example} - -% $Id$ - -%%% Local Variables: -%%% mode: latex -%%% TeX-master: "Reference-Manual" -%%% End: diff --git a/doc/Recursive-Definition.tex b/doc/Recursive-Definition.tex deleted file mode 100755 index ba9423409..000000000 --- a/doc/Recursive-Definition.tex +++ /dev/null @@ -1,251 +0,0 @@ -\documentstyle[]{article} -\input{title} - -\newcommand{\xx}{\noindent} -\newcommand{\Coq}{\textsc{Coq}} - -\begin{document} - -\coverpage{Users friendly {\tt Recursive Definition}}{Pascal MANOURY} - -This command allows to define functions in -the following syntax : -\begin{verbatim} -Recursive Definition f [X1:U1;..;Xk:Uk] : T1-> .. -> Tn -> T := - p11 .. p1n => t1 -... -|pm1 .. pmn => tm. -\end{verbatim} -This definition schema must be understood as : -\begin{itemize} -\item {\tt f} is the name of the constant we want -to define; -\item {\tt (X1:U1)..(Xk:Uk) T1-> .. -> Tn -> T} -is its intended type; -\item {\tt p11 .. p1n => t1 | ... |pm1 .. pmn => tm.} -describe its beha\-viour in terms of patterns. -We -call the {\sl patterns clauses} this part of the {\tt Recursive Definition}. -\end{itemize} -The semantics of the {\tt Recursive Definition} -is to -define the new constant {\tt f} as a term (say {\tt F}) of -the intended type providing that {\tt F} has the intended -computational behavior expressed in the {\sl patterns -clauses}. Moreover, a {\tt Recursive Definition} states and -proves all equational theorems corresponding to {\sl -patterns clauses}. In other words, a {\tt Recursive Definition} is -equivalent to : -\begin{verbatim} -Definition f : (X1:U1)..(Xk:Uk) T1-> .. -> Tn -> T := F. -Theorem f_eq1 : (X1:U1)..(Xk:Uk)(x11:V11)..(x1l:V1l)(F X1 .. Xk p11 .. p1n)=t1. -Intros; Unfold F; Simpl; Trivial. Save. -... -Theorem f_eqm : (X1:U1)..(Xk:Uk)(xm1:Vm1)..(xml:Vml)(F X1 .. Xk pm1 .. pmn)=tm. -Intros; Unfold F; Simpl; Trivial. Save. -\end{verbatim} -For instance, one can write : -\begin{coq_example} -Recursive Definition Ack : nat -> nat -> nat := - O m => (S m) - |(S n) O => (Ack n (S O)) - |(S n) (S m) => (Ack n (Ack (S n) m)). -\end{coq_example} - -Unfortunately, the problem of finding a term (of \Coq) -satisfying a set of {\sl patterns clauses} does not always have a -solution, as shown by the following example~:\\ -\centerline {\tt Recursive Definition fix : -nat -> nat := n => (fix n).} -The point is that, in \Coq, any term {\tt F} of type {\tt -nat -> nat} represents a function which always terminates -and it is easy to see that the function {\tt fix} never -terminates. This general property of \Coq's terms is called -{\it strong normalization}. - -\xx -The fact that a syntactically correct {\tt Recursive -Definition} as the one of {\tt fix} does not correspond to any -term in \Coq~ points out that we cannot content with the {\it -syntactical level} of the declaration to obtain a term, but we -have to lift up onto the {\it logical level} to ensure that -the aimed function satisfies such a strong property as -termination. And here comes the difficulty, since the termination -problem is known to be undecidable in general. - -\xx -In fact, termination is the main logical property we -have to face with. Then the main job of the {\tt Recursive -Definition} is to build a proof of {\tt (X1:U1)..(Xk:Uk) -T1-> .. -> Tn -> T} understood as a termination proof of the -aimed function.\\ -Let's see how it works on the Ackermann's function example -: -\begin{coq_eval} -Restore State Initial. -\end{coq_eval} -\begin{coq_example} -Theorem Ack : nat -> nat -> nat. -Intro n; Elim n. -Intro m; exact (S m). -Intros p Ack_n m; Elim m. -exact (Ack_n (S O)). -Intros q Ack_Sn_m; exact (Ack_n Ack_Sn_m). -Save. -\end{coq_example} -One can check that the term {\tt Ack} ({\it eg} : the above -proof of {\tt nat -> nat -> nat}) actually satisfies -the intended {\sl patterns clauses} of Ackermann's -function. - -\xx -Such a proof is {\em automatically} synthesized by a -{specialized strategy} which was originally designed for the -\textsc{ProPre} programming language. It has been adapted for -the \Coq's framework. For a short description of the \textsc{ProPre} -programming language, we refer the reader to -\cite{MPSI}. For details -concerning the original proof search strategy, we refer the -reader to \cite{MSAR}. For theoretical settings of the -method involved in \textsc{ProPre}, we refer the reader to -\cite{KRPA} and \cite{PARI}. - -\xx -We list bellow some correct and incorrect usages of -the {\tt Recursive Definition} feature. - -\subsection*{Correct {\tt Recursive Definition}'s} -\begin{coq_example*} -Recursive Definition IfSet [X:Set] : bool -> X -> X -> X := - true x y => x - |false x y => y. -Recursive Definition equal_nat : nat -> nat -> bool := - O O => true - |O (S m) => false - |(S n) O => false - |(S n) (S m) => (equal_nat n m). -Recursive Definition less_equal : nat -> nat -> bool := - O m => true - |(S n) O => false - |(S n) (S m) => (less_equal n m). -Inductive Set bintree := - Le : bintree - |Br : nat -> bintree -> bintree -> bintree. -Recursive Definition ins_bsr [n:nat] : bintree -> bintree := - Le => (Br n Le Le) - |(Br m a1 a2) - => (IfSet bintree (less_equal n m) (Br m (ins_bsr n a1) a2) - (Br m a1 (ins_bsr n a2))). -Inductive list [X:Set] : Set := - Nil : (list X) - |Cons : X -> (list X) -> (list X). -Recursive Definition append [X:Set;ys:(list X)] : (list X) -> (list X) := - (Nil X) => ys - |(Cons X x xs) => (Cons X x (append X ys xs)). -Recursive Definition soml : (list nat) -> nat := - (Nil nat) => O - |(Cons nat O x) => (soml x) - |(Cons nat (S n) x) => (S (soml (Cons nat n x))). -Recursive Definition sorted_list : (list nat) -> Prop := - (Nil nat) => True - |(Cons nat n (Nil nat)) => True -|(Cons nat n (Cons nat m x)) - => (<bool>(less_equal n m)=true) /\ (sorted_list (Cons nat m x)). -\end{coq_example*} - -\subsection*{Incorrect {\tt Recursive Definition}'s} -\begin{coq_example} -Recursive Definition equal_list : (list nat) -> (list nat) -> bool := - (Nil nat) (Nil nat) => true - |(Nil nat) (Cons nat n y) => false - |(Cons nat n x) (Nil nat) => false - |(Cons nat n x) (Cons nat n y) => (equal_list x y). -\end{coq_example} -As explains the error message, a same pattern variable can't be used -more than one time. -\begin{coq_example} -Recursive Definition min : nat -> nat -> nat := - O m => m - |n O => n - |(S n) (S m) => (S (min n m)). -\end{coq_example} -We do not allow the various left members of {\sl patterns clauses} to -overlap. -\begin{coq_example} -Recursive Definition wrong_equal : nat -> nat -> bool := - O O => true - |(S n) (S m) => (wrong_equal n m). -\end{coq_example} -As we need to prove that the function is totally defined, we need an -exhaustive pattern matching of the inputs. -\begin{coq_example} -Recursive Definition div2 : nat -> nat := - O => O - |(S O) => O - |(S (S n)) => (S (div2 n)). -\end{coq_example} -The strategy makes use of structural induction to search a proof of -{\tt nat -> nat}, then it can only accept arguments decreasing in one -step ({\it eg} from {\tt (S n)} to {\tt n}) which is not the case -here. -\begin{coq_example} -Recursive Definition wrong_fact : nat -> nat := - n => (IfSet nat (equal_nat n O) (S O) (mult n (wrong_fact (pred n)))). -\end{coq_example} -This error comes from the fact that the strategy doesn't recognize -that the {\tt IfSet} is used as matching on naturals and that, when -{\tt n} is not {\tt O}, {\tt (pred n)} is less than {\tt n}. Indeed, -matching must be explicit and decreasing too. -\begin{coq_example} -Recursive Definition heap_merge : bintree -> bintree -> bintree := - Le b => b - |(Br n a1 a2) Le => (Br n a1 a2) - |(Br n a1 a2) (Br m b1 b2) - => (IfSet bintree - (less_equal n m) - (Br n (heap_merge a1 a2) (Br m b1 b2)) - (Br m (Br n a1 a2) (heap_merge b1 b2))). -\end{coq_example} -This failure of the strategy is due to the fact than with simple -structural induction one can't get any induction hypothesis for both -inductive calls {\tt (heap\_merge a1 a2)} and {\tt (heap\_merge b1 - b2)}. - - -\begin{thebibliography}{9999} -\bibitem{KRPA} J.L Krivine, M. Parigot - {\it Programming with proofs} ; in SCT 87 (1987), -Wendish-Rietz ; in EIK 26 (1990) pp 146-167. - -\bibitem{MPSI} P. Manoury, M. Parigot, M. Simonot {\it {\sf -ProPre} : a programming language with proofs} ; in -proceedings LPAR 92, LNAI 624. - -\bibitem{MSTH} P. Manoury and M. Simonot {\it Des preuves -de totalit\'e de fonctions comme synth\`ese de -programmes} ; Phd Thesis, Universit\'e Paris 7, December -1992. - -\bibitem{MSAR} P. Manoury and M. Simonot {\it -Automatizing termination proof of recursively defined -functions} ; to appear in TCS. - -\bibitem{PARI} M. Parigot {\it Recursive programming with -proofs} ; in TCS 94 (1992) pp 335-356. - -\bibitem{PAUL} C. Paulin-Mohring {\it Inductive -Definitions in the System Coq - Rules and properties} ; -proceedings TLCA 93, LNCS 664 (1993). - -\bibitem{WERN} B. Werner {\it Une th\'eorie des -constructions inductives} ; Phd Thesis, Universit\'e Paris -7, May 1994. - -\end{thebibliography} - -\end{document} - - - - -% $Id$ diff --git a/doc/RefMan.txt b/doc/RefMan.txt deleted file mode 100644 index 446ad1284..000000000 --- a/doc/RefMan.txt +++ /dev/null @@ -1,74 +0,0 @@ -TUTORIAL N. Oury - -GUIDE PASSAGE V7-V8 BB - -MANUEL DE REFERENCE -\include{RefMan-int}% Introduction HH - relu CP -\include{RefMan-pre}% Credits HH - relu CP - -\tableofcontents - -\part{The language} -\defaultheaders -\include{RefMan-gal.v}% Gallina BB -\include{RefMan-ext.v}% Gallina extensions HH -fait -\include{RefMan-lib.v}% The coq library BB -\include{RefMan-cic.v}% The Calculus of Constructions CP -fait - -\include{RefMan-modr}% The module system Jacek - - -\part{The proof engine} -\include{RefMan-oth.v}% Vernacular commands JCF -fait -\include{RefMan-pro}% Proof handling Clement -\include{RefMan-tac.v}% Tactics and tacticals JCF - fait -%% ajouter JProver/Ground/CC Pierre C -fait -\include{RefMan-tacex.v}% Detailed Examples of tactics JCF - fait - -\part{User extensions} -\include{RefMan-syn.v}% The Syntax and the Grammar commands HH -%%SUPPRIME \include{RefMan-tus.v}% Writing tactics -%%REMPLACE PAR -\include{RefMan-ltac.v}% Writing tactics BB -fait - -\part{Practical tools} -\include{RefMan-com}% The coq commands (coqc coqtop) HH -fait -%%ajouter nouvelles options -v7 -translate au document de passage -\include{RefMan-uti}% utilities (gallina, do_Makefile, etc) JCF -fait -\include{RefMan-ide}%CoqIde CM - -\include{AddRefMan-pre}% CP - -\include{Cases.v}% CP -fait -\include{Coercion.v}% HH -fait -%%SUPPRIME \include{Natural.v}% -\include{Omega.v}% JCF - fait -%%Nouvelle version ROmega Pierre Cregut -%%SUPPRIME \include{Program.v}% -%% A SUPPRIMER -%% \include{Correctness.v}% = preuve de pgms imperatifs -\include{Extraction.v}% Pierre L -\include{Polynom.v}% = Ring Julien N -\include{Setoid.v}% Tactique pour les setoides Clement -\addtocontents{sh}{ENDADDENDUM=\thepage} - -\nocite{*} -\bibliographystyle{plain} -\bibliography{biblio} -\addtocontents{sh}{psselect -q -p-$ENDREFMAN,$BEGINBIBLIO- Reference-Manual.ps Reference-Manual-base.ps} -\addtocontents{sh}{psselect -q -p$BEGINADDENDUM-$ENDADDENDUM Reference-Manual.ps Reference-Manual-addendum.ps} -\addtocontents{sh}{dviselect -i Reference-Manual.dvi -o Reference-Manual-base.dvi 1-$ENDREFMAN $BEGINBIBLIO-} -\addtocontents{sh}{dviselect -i Reference-Manual.dvi -o Reference-Manual-addendum.dvi $BEGINADDENDUM-$ENDADDENDUM} - -\printindex - -\printindex[tactic] - -\printindex[command] - -\printindex[error] - -\end{document} - - -% $Id$ diff --git a/doc/book-html.sty b/doc/book-html.sty deleted file mode 100644 index 27eaeefa8..000000000 --- a/doc/book-html.sty +++ /dev/null @@ -1,133 +0,0 @@ -\newcounter {part} -\newcounter {chapter} -\newcounter {section}[chapter] -\newcounter {subsection}[section] -\newcounter {subsubsection}[subsection] -\newcounter {paragraph}[subsubsection] -\newcounter {subparagraph}[paragraph] -\renewcommand \thepart {\Roman{part}} -\renewcommand \thesection {\thechapter.\arabic{section}} -\renewcommand\thesubsection {\thesection.\arabic{subsection}} -\renewcommand\thesubsubsection{\thesubsection .\arabic{subsubsection}} -\renewcommand\theparagraph {\thesubsubsection.\arabic{paragraph}} -\renewcommand\thesubparagraph {\theparagraph.\arabic{subparagraph}} -\newcommand{\partname}{Part} -\newcommand{\chaptername}{Chapter} -%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\newcommand{\appendix}{% -\renewcommand{\chaptername}{Appendix}% -\setcounter{chapter}{0}% -\renewcommand{\thechapter}{\Alph{chapter}}% -} -\newcounter{figure}[chapter] -\renewcommand{\thefigure}{\thechapter.\arabic{figure}} - -\newcommand{\part}[1]{% -\@print{<!--CUT PART-->} -\@open{H1}{ALIGN=center} -\refstepcounter{part} -\partname:~\thepart\\ -#1 -\@close{H1} -} -\newcommand{\part*}[1]{% -\@print{<!--CUT CHAPTER-->} -\@open{H1}{ALIGN=center} -#1 -\@close{H1} -} - -\newcommand{\chapter}[1]{% -\@print{<!--CUT CHAPTER-->} -\@open{H1}{} -\refstepcounter{chapter} -\chaptername~\thechapter: #1 -\@close{H1} -} -\newcommand{\chapter*}[1]{% -\@print{<!--CUT CHAPTER-->} -\@open{H1}{} -#1 -\@close{H1} -} - -\newcommand{\section}[1]{% -\@print{<!--CUT SECTION-->} -\@open{H2}{} -\refstepcounter{section} -\thesection~#1 -\@close{H2} -} -\newcommand{\section*}[1]{% -\@print{<!--CUT SECTION-->} -\@open{H2}{} -#1 -\@close{H2} -} - - -\newcommand{\subsection}[1]{% -\@open{H3}{} -\refstepcounter{subsection} -\thesubsection~#1 -\@close{H3} -} -\newcommand{\subsection*}[1]{% -\@open{H3}{} -#1 -\@close{H3} -} - - -\newcommand{\subsubsection}[1]{% -\@open{H4}{} -% \refstepcounter{subsubsection} -% \thesubsubsection~ -#1 -\@close{H4} -} -\newcommand{\subsubsection*}[1]{% -\@open{H4}{} -#1 -\@close{H4} -} - -\newcommand{\paragraph}[1]{% -\@open{H5}{} -% \refstepcounter{paragraph} -% \theparagraph~ -#1 -\@close{H5} -} -\newcommand{\paragraph*}[1]{% -\@open{H5}{} -#1 -\@close{H5} -} - -\renewenvironment{thebibliography}[1]{% -\@print{ -<!--CUT BIBLIOGRAPHY--> -} -\@open{H1}{} -\bibname\@close{H1}\@open{DL}{}}{% - -\@close{DL} -} -\renewcommand{\bibitem}[1]{\item[{\purple[\@bibref{#1}]\label{#1}}]} -% \renewcommand{\index}[2][default]{\@index[#1]{#2}} -\renewcommand{\printindex}[1][default]{% -\@print{ -<!--CUT INDEX--> -} -\@printindex[#1] -} - -\renewcommand{\addtocontents}[2]{} - -\newcommand{\tophtml}{% -\@print{ -<!--CUT TOP--> -}} - -\newcommand{\atableofcontents}{} diff --git a/doc/macros.tex b/doc/common/macros.tex index 8a6ac82ff..8a6ac82ff 100755 --- a/doc/macros.tex +++ b/doc/common/macros.tex diff --git a/doc/title.tex b/doc/common/title.tex index 8e1d1c9c9..8e1d1c9c9 100755 --- a/doc/title.tex +++ b/doc/common/title.tex diff --git a/doc/coq-html.sty b/doc/coq-html.sty deleted file mode 100644 index 2793fdc2a..000000000 --- a/doc/coq-html.sty +++ /dev/null @@ -1,6 +0,0 @@ -\def\sf{\purple} -\def\textsf#1{{\sf #1}} -\newcommand{\inference}[1]{$${#1}$$} -\newcommand{\NInd}[3]{\mbox{{\sf Ind}$(#1)(#2:=#3\,)$}} -\newcommand{\Ind}[4]{\mbox{{\sf Ind}$(#1)[#2](#3:=#4\,)$}} -\renewcommand{\medskip}{\\} diff --git a/doc/discussion-syntaxe.txt b/doc/discussion-syntaxe.txt deleted file mode 100644 index 658c67c72..000000000 --- a/doc/discussion-syntaxe.txt +++ /dev/null @@ -1,349 +0,0 @@ - - Synthèse des différentes propositions de "rénovation" de la syntaxe de Coq - -------------------------------------------------------------------------- - -I) Constructions - - Éléments de doctrine : - - - choix de mots-clés en minuscule - - proche de ml - -A) Produit - - Consensus apparent pour remplacer la syntaxe actuelle à base de -parenthèses par quelque chose de plus "simple". Les options retenues -sont "! x . P x", "Forall x . P x" ou "forall x . P x". - - A1) Choix du symbole de tête - - "!" est court et expressif mais sans doute moins que "forall" - surtout pour un débutant. "!", c'est le choix d'HOL, "forall" (en - majuscule), celui de PVS. Un inconvénient de "forall" est qu'il - n'est pas très approprié pour le produit fonctionnel dépendant (ou - alors, on propose à la fois "pi" et "forall" comme synonymes) - - Rem: Quelque soit le choix du symbole de tête, un parseur/printeur - unicode pourra substituer le symbole de tête par le "\forall" (et le - "\pi" dans l'option ou "pi" et "forall" coexistent) - - - A2) Quantification sur plusieurs variables - - A2a) "! x y1 z. P x" - - Avantages : analogie avec la juxtaposition des arguments pour l'application, - réminiscent de la juxtaposition en math "\forall xyz.P(x)", c'est le - choix d'HOL. - - A2b) "! x, y1, z. P x" - - Avantages : plus standard ? - - - A3) Mention des types - - A3a) On a séparé par des espaces - - A3a1) "! ( x x1 : A ) ( y1 y2 : f a ( g b ) ) z. P x" - A3a2) "! x x1 : A, y1 y2 : f a ( g b ), z. P x" - A3a3) "! x x1 : A; y1 y2 : f a ( g b ); z. P x" - A3a4) "! x x1 : A. ! y1 y2 : f a ( g b ). ! z. P x" - Rem: ici, un seul type explicite par quantificateur; mais incohérence - avec "! x y. P x" où x et y peuvent avoir des types différente; en - revanche, se comporte bien à l'écriture sur plusieurs lignes - - A3b) On a séparé par des virgules - - A3b1) "! ( x, x1 : A ), ( y1, y2 : f a ( g b ) ), z. P x" - A3b2) "! x, x1 : A, y1 y2 : f a ( g b ), z. P x" - A3b3) "! x, x1 : A; y1 y2 : f a ( g b ); z. P x" - A3b4) "! x, x1 : A. ! y1 y2 : f a ( g b ) . ! z. P x" - - Rem: si ";" voir section terminateur de phrase - - -B) Application - - Pas d'apparence de consensus - - B1) Principe que les parenthèses font partie de la notation - (appliqué par une partie de la communauté \-calcul et dans Lisp), - - B2) Principe que les parenthèses ne servent qu'à grouper - (appliqué par une partie de la communauté \-calcul et dans ML) - - Argument : notations plus légères, cohérence avec ML - - Ce choix implique-t-il de donner la plus grande précédence à l'application ? - Exemple : comment comprendre ces expressions ? - - f 4 + x - P A -> B - ! x : f a = b c . h y - - -C) Abstraction - - Tant qu'à faire, renoncement à la notation crochet pour obtenir une -meilleure cohérence avec le reste. - - C1) "\ x. g y" ou "fun x. g y" (analogie avec "!" ou "forall") - C2) "fun x => g y" ou "Fun x => g y" (analogie avec caml et le filtrage) - C3) "\ x => g y" (réminiscent de Haskell) - - -D) Arithmétique - - Consensus pour réserver 0, 1, 2, ... ainsi que +, -, *, /, < et > à -l'arithmétique. Tant qu'à faire, >=, <= et <> aussi (l'usage en est -standard). - - Trois approches ont été proposées pour distinguer l'algèbre -concernée (N, Z, R, ...). - - D1) Qualification des opérateurs, qui obéissent alors aux mêmes règles -que des identificateurs concernant la surcharge (càd le dernier module -"importé" ("ouvert" au sens ML) impose ses noms et symboles. Ex: - - Require Arith. (* + est l'addition sur les naturels *) - Require ZArith. (* + devient l'addition sur les entiers relatifs mais - l'addition sur N reste accessible par Arith.+ *) - - Contraintes : - - - les expressions style Arith.+ doivent être reconnues par - l'analyseur lexicale (sinon la grammaire n'est plus LL1). Pour - garder le "." dans le pour tout, on pourrait adopter ce principe: un - "." immédiatement suivi d'une lettre doit être compris comme un - accès qualifié et le "." se différencie par le fait qu'il serait - suivi d'un blanc, ce qui est conforme à la typographie usuelle. - - cf aussi E - - D2) Chaque module exporte 2 notations, "+" et une autre (typiquement - "+_N" pour les naturels, "+_Z" pour les entiers relatifs, ...). - Le dernier module "ouvert" impose son "+" mais les autres restent - accessibles par le symbole indexé. - - Cette option requiert des symboles mixtes (cf H) - - D3) ... - - Remarque supplémentaire sur les constantes numériques: si on ne - choisit pas l'option D1 (qualification style N.1), on doit pouvoir les - mettre dans "positive" par défaut et jouer avec les coercions pour - qu'elles atterissent dans le type attendu (N, Z, ...). - - -E) Constructeurs de type de données - - Propositions: utilisation de ** pour prod et ++ pour sum, rien pour -sumor et sumbool (qui pourrait être renommé "dec" ou "decidable"). - - Quid de sig ? - - -F) Egalité et existentielle - - Consensus pour fusionner = et ==, càd que = dénote eqT (càd l'actuel ==) -et que la notation == disparaisse. La cumulativité assure la compatibilité. - - Mieux, idée à explorer que = dénote l'égalité de John Major. Tenants -et aboutissants ??? - - Consensus pour avoir une existentielle unique (donc au niveau type -en jouant sur la cumulativité). La notation serait naturellement -"? x. P x", "exists x. P x" ou "Exists x. P x". - - -G) Autres connecteurs - - Les choix actuels semblent convenir... (->, /\, \/ et ~) - - -H) Extensibilité de la syntaxe (tokens) - - H1) Une famille de token non extensible limitée à l'avance, - typiquement constituée des suites de symboles spéciaux (comme en Caml) - - Avantage : le lexeur peut être "camllex" (est-ce important ?) - - Inconvénients : - - Comment gérer les tokens style "=_S" (cf D2) - Dans l'option qualification des symboles (cf D1), cela pourrait - être "S.=", sinon... any ideas ? - - Obligation de séparer, comme dans ~~A, etc - - Rem: Les tokens composés uniquement de lettres, tel que "U" pour - l'union pourrait être autorisés à condition de les quoter par des « ' - », « ` » ou « " », ce qui d'ailleurs améliore leur lisibilité. - - H2) Famille de token extensible (comme en V6) - - Avantage : grande souplesse de choix de nouveaux symboles ce que -l'usage mathématique apprécie - - -J) Extensibilité de la syntaxe (règles) - - Consensus apparent pour limiter l'usage de Grammar et Syntax. Comme -de toutes façons se sont essentiellement des infixes, ainsi que quelques -préfixes, postfixes et distfixes dont on a besoin ! - - Prendre soin des combinaisons précédence/associativité pour les -symboles à la fois préfixe/postfixe et infixe comme le "-". - - -K) Variables existentielles - - Si "?" est pris pour l'existentielle, "_", "_1", ... pourrait convenir. - - -L) Arguments implicites - - L1) Proposition (HH) d'unifier la notation "1!a" des arguments -implicites avec celle du "with" de Apply, et celle de "Intros Until", -sous une forme "f a b c with x:=d, 2:=H". - - Les index désigneraient alors les arguments non nommés (qu'ils -soient implicites ou non). - - L2) Si "!" est pris pour le produit, "1!c" pourrait devenir "@1:=c" - ou quelque chose comme cela. - - -M) Point fixe - - Quelques idées... sachant que le cas est rare et que l'effort doit -porter d'abord sur Fixpoint. - - M1) "(let f a (b:B) c = ... and g d e f : A = ... in f) u v" - M2) "(fun f a (b:B) c = ... and {h} x y = ... and g d e f = ...) u v" - (ici, accolades pour dire que c'est h qui est projeté) - M3) "(fix f where f a (b:B) c := ... and ... g d e f : A = ...) u v" - - + détection automatique des arguments gardés et mention optionnelle - du type résultat. - - -N) Filtrage - - N1) sans contrainte : - - "match t with p1 => t1 | ... | pn => tn end" - - et pas de parenthèses autour des pattern si pas autour de l'application - - N2) avec contrainte : - - "match t as x : I p1 .. pn y1 .. yq => T with - p1 => t1 - | ... - | pn => tn - end" - - N3) multiple - - "match t1, .., tq with - p11, .., p1q => t1 - | .. - | pn1, .., pnq => tn - end" - - Problème avec le choix de la virgule : conflit avec la notation - primitive des n-uplets si ceux-ci ne sont pas entourées par des - parenthèses. - - Alternative : séparation avec un "&" (pas d'ambiguïté avec les - paires) mais réquisitionne le symbole, et pas très standard (sauf - latex...), quoique le symbole est intuitif. - - N4) multiple avec contrainte - - "match t1 as x : I p1 .. pn y1 .. yq, .., tq as ... => T with - p11, .., p1q => t1 - | .. - | pn1, .., pnq => tn - end" - - Alternatives: case, cases, ... - - -II) Gallina - -A) Terminateur de phrase - - Le "." étant apprécié pour le pour tout, il conviendrait d'en -changer (pour la qualification on peut vivre avec en suivant le -principe mentionné en I-D1). - - A1) ";;" - - Deux symboles donc peu d'interférence avec le reste, cohérence avec - caml, mais assez lourd - - A2) ";" - - Léger, comme en SML, mais oblige à changer la syntaxe du THEN - (alternatives "," ou "THEN"), des records (alternative ",") et - interdit dans le ";" dans les lieurs (I-A3a3 et I-A3b3). - -B) Records - -C) Point fixe (cf I-M) - - C1) "Fixpoint f a (b:B) c := ... and g d e f : A := ... ." - C2) "Fixpoint f a (b:B) c := ... with g d e f : A := ... ." - - - -III) Tactiques - -Questions ouvertes : - -- Incompatibilité de prendre en compte dans ltad des arguments - numériques en conflit avec des ident, comme dans "Unfold 1 3 plus". - - Suggestion : "Unfold [1 3] plus". - -- La syntaxe "Pattern -2 -1 x" est-elle claire ? Le "-" voulant dire - sauf et non en partant de la fin. - - Suggestion de CP : on réécrit le but avec des _ à la place des occurrences - souhaitées. - -IV) Vernac - -Mots-cles Variables/Hypotheses/Parameters ? Si oui, pourquoi pas Axioms ? - -Intégrer Eval In à Constr ? Oui, mais avec une syntax plus légère -Ou alors standardiser -Definition_kind id params := red_expr c : t. - -Intégrer "with_binding" à Constr ! - -Faut-il séparer command/gallina/gallina_ext/syntax, sachant que si -l'on sépare, alors il ne faut plus partager de premier mot-clé (ex: -Add et Print seront réservé pour command) ? - -Virer theorem_body_line ? - -Virer le Mutual old syntax ! Et même implanter le future style de -Christine avec paramètres engendrés automatiquement et propre à chaque inductif - -Scheme est-il Gallina ou pas ? -Require est-il gallina_ext ou commande ? Et faut-il garder specif ? -Utilite de RequireFrom ? - -Faire des qualid un token ? - -EVAL et CONTEXT dans constr: partout ou seulement en tete ? -Supprimer Specialize, supprimer with c (sans nom) - -Ltac impose que "?" soit utilisable là où un identificateur ou un nom -long est attendu (p.ex. dans Clear). Accepte-t-on le principe ? - -V) Bibliothèque standard - -Zcompare_EGAL -> Zcompare_EQUAL diff --git a/doc/faq.tex b/doc/faq.tex deleted file mode 100644 index 29d7802b9..000000000 --- a/doc/faq.tex +++ /dev/null @@ -1,800 +0,0 @@ -\documentclass{article} -\usepackage{fullpage} -\usepackage{hevea} -\usepackage{url} - -\input{./macros.tex} - -\newcommand{\coqtt}[1]{{\tt #1}} -\newcommand{\coqimp}{{\mbox{\tt ->}}} -\newcommand{\coqequiv}{{\mbox{\tt <->}}} - -\newcommand{\question}[1]{ - \subsection*{\aname{no:number}{Question:~\sf{#1}}} - \addcontentsline{toc}{subsection}{\ahrefloc{no:number}{#1}} - \addcontentsline{htoc}{subsection}{\ahrefloc{no:number}{#1}}} -%{\subsubsection{Question:~\sf{#1}}}} -\newcommand{\answer}{{\bf Answer:~}} - - -\newcommand\vfile[2]{\ahref{#1}{\tt {#2}.v}} - -\begin{document} -\urldef{\refman}{\url}{http://coq.inria.fr/doc/main.html} -\urldef{\InitWf}{\url} - {http://coq.inria.fr/library/Coq.Init.Wf.html} -\urldef{\LogicBerardi}{\url} - {http://coq.inria.fr/library/Coq.Logic.Berardi.html} -\urldef{\LogicClassical}{\url} - {http://coq.inria.fr/library/Coq.Logic.Classical.html} -\urldef{\LogicClassicalFacts}{\url} - {http://coq.inria.fr/library/Coq.Logic.ClassicalFacts.html} -\urldef{\LogicProofIrrelevance}{\url} - {http://coq.inria.fr/library/Coq.Logic.ProofIrrelevance.html} -\urldef{\LogicEqdep}{\url} - {http://coq.inria.fr/library/Coq.Logic.Eqdep.html} -\urldef{\LogicEqdepDec}{\url} - {http://coq.inria.fr/library/Coq.Logic.Eqdep_dec.html} - -\begin{center} -\begin{Large} -Frequently Asked Questions -\end{Large} - -\medskip -{\Coq} version 8 -\end{center} - -\tableofcontents - -\section{General} - -\question{What is {\Coq}?} - -\answer {\Coq} is a proof assistant with two main application fields: -proving program correctness and formalising mathematical -theories. {\Coq} offers also automatic extraction of zero-defect -programs from a proof of their specification. - -\question{How to use {\Coq}?} - -\answer{{\Coq} offers a development environment in which you can -alternatively define predicates, functions or sets and state claims to -be interactively proved. {\Coq} comes with a large library of -predefined notions both from the standard mathematical background -(natural, integer and real numbers, sets and relations, ...) and from -the standard computer science background (lists, binary numbers, -finite sets, dictionaries, ...). {\Coq} comes with a -graphical interface. - -\question{What are the main applications done in {\Coq}?} - -\answer Largest developments are Java certification, safety of -cryptographic protocols, advanced constructive and classical analysis, -algebraic topology, ... - -\question{What is the logic of {\Coq}?} - -\answer {\Coq} is based on an axiom-free type theory called -the Calculus of Inductive Constructions (see Coquand \cite{CoHu86} -and Coquand--Paulin-Mohring \cite{CoPa89}). It includes higher-order -functions and predicates, inductive and co-inductive datatypes and -predicates, and a stratified hierarchy of sets. - -\question{Is {\Coq}'s logic intuitionistic or classical?} - -\answer {\Coq} theory is basically intuitionistic -(i.e. excluded-middle $A\lor\neg A$ is not granted by default) with -the possibility to reason classically on demand by requiring an -optional module stating $A\lor\neg A$. - -\question{What's the status of proofs in {\Coq}} - -\answer {\Coq} proofs are build with tactics allowing both forward -reasoning (stating - -cannot be accepted without a proof expressed in the Calculus of -Inductive Constructions. The correctness of a proof relies on a -relatively small proof-checker at the kernel of {\Coq} (8000 lines of ML -code). Even {\Coq} decision procedures are producing proofs which are -double-checked by the kernel. - -\question{Can I define non-terminating programs in {\Coq}?} - -\answer No, all programs in {\Coq} are terminating. Especially, loops -must come with an evidence of their termination. - -\question{Is {\Coq} a theorem prover?} - -\answer {\Coq} comes with a few decision procedures (on propositional -calculus, Presburger arithmetic, ring and field simplification, -resolution, ...) but the main style for proving theorems is -interactively by using LCF-style tactics. - -\question{How is equational reasoning working in {\Coq}?} - -\answer {\Coq} comes with an internal notion of computation called -{\em conversion} (e.g. $(x+1)+y$ is internally equivalent to -$(x+y)+1$; similarly applying argument $a$ to a function mapping $x$ -to some expression $t$ converts to the expression $t$ where $x$ is -replaced by $a$). This notion of conversion (which is decidable -because {\Coq} programs are terminating) covers a certain part of -equational reasoning but is limited to sequential evaluation of -expressions of (not necessarily closed) programs. Besides conversion, -equations have to be treated by hand or using specialised tactics. - -\question{What are the high-level tactics of {\Coq}} - -\begin{itemize} -\item Decision of quantifier-free Presburger's Arithmetic -\item Simplification of expressions on rings and fields -\item Decision of closed systems of equations -\item Semi-decision of first-order logic -\item Prolog-style proof search, possibly involving equalities -\end{itemize} - -\question{What are the main libraries of {\Coq}} - -\begin{itemize} -\item Basic Peano's arithmetic -\item Binary integer numbers -\item Real analysis -\item Libraries for lists, boolean, maps. -\item Libraries for relations, sets -\end{itemize} - -\section{Equality} - -%\subsection{Equality on Terms} - -\question{How can I prove that 2 terms in an inductive set are equal? Or different?} - -\answer Cf "Decide Equality" and "Discriminate" in the \ahref{\refman}{Reference Manual}. - -\question{Why is the proof of \coqtt{0+n=n} on natural numbers -trivial but the proof of \coqtt{n+0=n} is not?} - -\answer Since \coqtt{+} (\coqtt{plus}) on natural numbers is defined by analysis on its first argument - -\begin{coq_example} -Print plus. -\end{coq_example} - -\noindent the expression \coqtt{0+n} evaluates to \coqtt{n}. As {\Coq} reasons -modulo evaluation of expressions, \coqtt{0+n} and \coqtt{n} are -considered equal and the theorem \coqtt{0+n=n} is an instance of the -reflexivity of equality. On the other side, \coqtt{n+0} does not -evaluate to \coqtt{n} and a proof by induction on \coqtt{n} is -necessary to trigger the evaluation of \coqtt{+}. - -àéè\question{I have two proofs of the same proposition. Can I prove they are equal?} -\label{proof-irrelevance} - -\answer In the base {\Coq} system, the answer is no. However, if -classical logic is set, the answer is yes for propositions in {\Prop}. - -More precisely, the equality of all proofs of a given proposition is called -{\em proof-irrelevance}. Proof-irrelevance (in {\Prop}) can be assumed - without leading to contradiction in {\Coq}. - - That classical logic (what can be assumed in {\Coq} by requiring the file - \vfile{\LogicClassical}{Classical}) implies proof-irrelevance is shown in files - \vfile{\LogicProofIrrelevance}{ProofIrrelevance} and \vfile{\LogicBerardi}{Berardi}. - - Alternatively, propositional extensionality (i.e. \coqtt{(A - \coqequiv B) \coqimp A=B}, defined in \vfile{\LogicClassicalFacts}{ClassicalFacts}), - also implies proof-irrelevance. - -% It is an ongoing work of research to natively include proof -% irrelevance in {\Coq}. - -\question{Can I prove that the second components of equal dependent -pairs are equal?} - -\answer The answer is the same as for proofs of equality -statements. It is provable if equality on the domain of the first -component is decidable (look at \verb=inj_right_pair= from file -\vfile{\LogicEqdepDec}{Eqdep\_dec}), but not provable in the general -case. However, it is consistent (with the Calculus of Constructions) -to assume it is true. The file \vfile{\LogicEqdep}{Eqdep} actually -provides an axiom (equivalent to Streicher's axiom $K$) which entails -the result (look at \verb=inj_pair2= in \vfile{\LogicEqdep}{Eqdep}). - -\question{I have two proofs of an equality statement. Can I prove they are -equal?} - -\answer Yes, if equality is decidable on the domain considered (which -is the case for {\tt nat}, {\tt bool}, etc): see {\Coq} file -\verb=Eqdep_dec.v=). No otherwise, unless -assuming Streicher's axiom $K$ (see \cite{HofStr98}) or a more general -assumption such as proof-irrelevance (see \ref{proof-irrelevance}) or -classical logic. - -\question{What is Streicher's axiom $K$} -\label{Streicher} - -\answer Streicher's axiom $K$ \cite{HofStr98} asserts dependent -elimination of reflexive equality proofs. - -\begin{coq_example*} -Axiom Streicher_K : - forall (A:Type) (x:A) (P: x=x -> Prop), - P (refl_equal x) -> forall p: x=x, P p. -\end{coq_example*} - -In the general case, axiom $K$ is an independent statement of the -Calculus of Inductive Constructions. However, it is true on decidable -domains (see file \vfile{\LogicEqdepDec}{Eqdep\_dec}). It is also -trivially a consequence of proof-irrelevance (see -\ref{proof-irrelevance}) hence of classical logic. - -Axiom $K$ is equivalent to {\em Uniqueness of Identity Proofs} \cite{HofStr98} -which states that - -\begin{coq_example*} -Axiom UIP : forall (A:Set) (x y:A) (p1 p2: x=y), p1 = p2. -\end{coq_example*} - -Axiom $K$ is also equivalent to {\em Uniqueness of Reflexive Identity Proofs} \cite{HofStr98} - -\begin{coq_example*} -Axiom UIP_refl : forall (A:Set) (x:A) (p: x=x), p = refl_equal x. -\end{coq_example*} - -Axiom $K$ is also equivalent to - -\begin{coq_example*} -Axiom - eq_rec_eq : - forall (A:Set) (x:A) (P: A->Set) (p:P x) (h: x=x), - p = eq_rect x P p x h. -\end{coq_example*} - -It is also equivalent to the injectivity of dependent equality (dependent equality is itself equivalent to equality of dependent pairs). - -\begin{coq_example*} -Inductive eq_dep (U:Set) (P:U -> Set) (p:U) (x:P p) : -forall q:U, P q -> Prop := - eq_dep_intro : eq_dep U P p x p x. -Axiom - eq_dep_eq : - forall (U:Set) (u:U) (P:U -> Set) (p1 p2:P u), - eq_dep U P u p1 u p2 -> p1 = p2. -\end{coq_example*} - -All of these statements can be found in file \vfile{\LogicEqdep}{Eqdep}. - -% \subsection{Equality on types} - -\question{How to prove that 2 sets are differents?} - -\answer You need to find a property true on one set and false on the -other one. As an example we show how to prove that {\tt bool} and {\tt -nat} are discriminable. As discrimination property we take the -property to have no more than 2 elements. - -\begin{coq_example*} -Theorem nat_bool_discr : bool <> nat. -Proof. - pose (discr := - fun X:Set => - ~ (forall a b:X, ~ (forall x:X, x <> a -> x <> b -> False))). - intro Heq; assert (H: discr bool). - intro H; apply (H true false); destruct x; auto. - rewrite Heq in H; apply H; clear H. - destruct a; destruct b as [|n]; intro H0; eauto. - destruct n; [ apply (H0 2); discriminate | eauto ]. -Qed. -\end{coq_example*} - -\question{How to exploit equalities on sets} - -\answer To extract information from an equality on sets, you need to -find a predicate of sets satisfied by the elements of the sets. As an -example, let's consider the following theorem. - -\begin{coq_example*} -Theorem le_le : - forall m n:nat, - {x : nat | x <= m} = {x : nat | x <= n} -> m = n. -\end{coq_example*} - -A typical property is to have cardinality $n$. - -\section{Axioms} - -\question{Can I identify two functions that have the same behaviour (extensionality)?} - -\answer Extensionality of functions is an axiom in, say set theory, -but from a programming point of view, extensionality cannot be {\em a -priori} accepted since it would identify, say programs as mergesort -and quicksort. - -%\begin{coq_example*} -% Axiom extensionality : (A,B:Set)(f,g:(A->B))(x:A)(f x)=(g x)->f=g. -%\end{coq_example*} - -Let {\tt A}, {\tt B} be types. To deal with extensionality on -\verb=A->B=, the recommended approach is to define his -own extensional equality on \verb=A->B=. - -\begin{coq_eval} -Variables A B : Set. -\end{coq_eval} - -\begin{coq_example*} -Definition ext_eq (f g: A->B) := forall x:A, f x = g x. -\end{coq_example*} - -and to reason on \verb=A->B= as a setoid (see the Chapter on -Setoids in the Reference Manual). - -\question{Is {\Type} impredicative (that is, letting -\coqtt{T:=(X:Type)X->X}, can I apply an expression \coqtt{t} of type \coqtt{T} to \coqtt{T} itself)?} - -\answer No, {\Type} is stratified. This is hidden for the -user, but {\Coq} internally maintains a set of constraints ensuring -stratification. - - If {\Type} were impredicative then Girard's systems $U-$ and $U$ -could be encoded in {\Coq} and it is known from Girard, Coquand, -Hurkens and Miquel that systems $U-$ and $U$ are inconsistent [Girard -1972, Coquand 1991, Hurkens 1993, Miquel 2001]. This encoding can be -found in file {\tt Logic/Hurkens.v} of {\Coq} standard library. - - For instance, when the user see {\tt forall (X:Type), X->X : Type}, each -occurrence of {\Type} is implicitly bound to a different level, say -$\alpha$ and $\beta$ and the actual statement is {\tt -forall X:Type($\alpha$), X->X : Type($\beta$)} with the constraint -$\alpha<\beta$. - - When a statement violates a constraint, the message {\tt Universe -inconsistency} appears. Example: {\tt fun (x:Type) (y:forall X:Type, X \coqimp X) => z x x}. - -\section{Inductive types} - -\question{What is a "large inductive definition"?} - -\answer An inductive definition in {\Prop} pr {\Set} is called large -if its constructors embed sets or propositions. As an example, here is -a large inductive type: - -\begin{coq_example*} -Inductive sigST (P:Set -> Set) : Type := - existST : forall X:Set, P X -> sigST P. -\end{coq_example*} - -In the {\tt Set} impredicative variant of {\Coq}, large inductive -definitions in {\tt Set} have restricted elimination schemes to -prevent inconsistencies. Especially, projecting the set or the -proposition content of a large inductive definition is forbidden. If -it were allowed, it would be possible to encode e.g. Burali-Forti -paradox \cite{Gir70,Coq85}. - -\question{Why Injection does not work on impredicative {\tt Set}?} - - E.g. in this case (this occurs only in the {\tt Set}-impredicative - variant of {\Coq}}: - -\begin{coq_eval} -Reset Initial. -\end{coq_eval} - -\begin{coq_example*} -Inductive I : Type := - intro : forall k:Set, k -> I. -Lemma eq_jdef : - forall x y:nat, intro _ x = intro _ y -> x = y. -Proof. - intros x y H; injection H. -\end{coq_example*} - -\answer Injectivity of constructors is restricted to predicative types. If -injectivity on large inductive types were not restricted, we would be -allowed to derive an inconsistency (e.g. following the lines of -Burali-Forti paradox). The question remains open whether injectivity -is consistent on some large inductive types not expressive enough to -encode known paradoxes (such as type I above). - -\section{Recursion} - -\question{Why can't I define a non terminating program?} - -\answer Because otherwise the decidability of the type-checking -algorithm (which involves evaluation of programs) is not ensured. On -another side, if non terminating proofs were allowed, we could get a -proof of {\tt False}: - -\begin{coq_example*} -(* This is fortunately not allowed! *) -Fixpoint InfiniteProof (n:nat) : False := InfiniteProof n. -Theorem Paradox : False. -Proof (InfiniteProof O). -\end{coq_example*} - -\question{Why only structurally well-founded loops are allowed?} - -\answer The structural order on inductive types is a simple and -powerful notion of termination. The consistency of the Calculus of -Inductive Constructions relies on it and another consistency proof -would have to be made for stronger termination arguments (such -as the termination of the evaluation of CIC programs themselves!). - -In spite of this, all non-pathological termination orders can be mapped -to a structural order. Tools to do this are provided in the file -\vfile{\InitWf}{Wf} of the standard library of {\Coq}. - -\question{How to define loops based on non structurally smaller -recursive calls?} - -\answer The procedure is as follows (we consider the definition of {\tt -mergesort} as an example). - -\begin{itemize} - -\item Define the termination order, say {\tt R} on the type {\tt A} of -the arguments of the loop. - -\begin{coq_eval} -Open Scope R_scope. -Require Import List. -\end{coq_eval} - -\begin{coq_example*} -Definition R (a b:list nat) := length a < length b. -\end{coq_example*} - -\item Prove that this order is well-founded (in fact that all elements in {\tt A} are accessible along {\tt R}). - -\begin{coq_example*} -Lemma Rwf : well_founded (A:=R). -\end{coq_example*} - -\item Define the step function (which needs proofs that recursive -calls are on smaller arguments). - -\begin{coq_example*} -Definition split (l : list nat) - : {l1: list nat | R l1 l} * {l2 : list nat | R l2 l} - := (* ... *) . -Definition concat (l1 l2 : list nat) : list nat := (* ... *) . -Definition merge_step (l : list nat) (f: forall l':list nat, R l' l -> list nat) := - let (lH1,lH2) := (split l) in - let (l1,H1) := lH1 in - let (l2,H2) := lH2 in - concat (f l1 H1) (f l2 H2). -\end{coq_example*} - -\item Define the recursive function by fixpoint on the step function. - -\begin{coq_example*} -Definition merge := Fix Rwf (fun _ => list nat) merge_step. -\end{coq_example*} - -\end{itemize} - -\question{What is behind these accessibility and well-foundedness proofs?} - -\answer Well-foundedness of some relation {\tt R} on some type {\tt A} -is defined as the accessibility of all elements of {\tt A} along {\tt R}. - -\begin{coq_example} -Print well_founded. -Print Acc. -\end{coq_example} - -The structure of the accessibility predicate is a well-founded tree -branching at each node {\tt x} in {\tt A} along all the nodes {\tt x'} -less than {\tt x} along {\tt R}. Any sequence of elements of {\tt A} -decreasing along the order {\tt R} are branches in the accessibility -tree. Hence any decreasing along {\tt R} is mapped into a structural -decreasing in the accessibility tree of {\tt R}. This is emphasised in -the definition of {\tt fix} which recurs not on its argument {\tt x:A} -but on the accessibility of this argument along {\tt R}. - -See file \vfile{\InitWf}{Wf}. - -\section{Elimination, Case Analysis and Induction} - -%\subsection{Parametric elimination} - -\question{What is parametric elimination?} - -\answer {\em Parametric} elimination is a generalisation of the -substitutivity of equality. Only inductive types with non-constant -parameters are concerned with this kind of dependent -elimination. Typical examples of inductive types enjoying parametric -elimination in {\Coq} standard library are the equality predicate -\verb=eq= and the less than predicate on natural numbers \verb=le=. - -\begin{coq_example} -Print eq. -Print eq_ind. -Print le. -\end{coq_example} - -%\subsection{Dependent elimination} - -\question{What means dependent elimination?} - -\answer Dependent elimination is a generalisation of the -standard Peano's induction principle on natural numbers. This -elimination asserts that to prove a property P on say the set {\tt nat} of -natural numbers, it is enough to prove the property on O and to prove -it on successor numbers. Combined with fixpoints, this directly -provides with usual Peano's induction scheme. - -Non dependent elimination is when elimination is used to build an -object whose type does not depend on the eliminated object. An example -of non dependent elimination is recursion, or the simpler form of -{\coqtt if $\ldots$ then $\ldots$ else}. - -The relevant tactics to deal with this kind of elimination are {\tt -elim}, {\tt induction}, {\tt nestruct} and {\tt case}, {\tt -simple induction} and {\tt simple destruct}. - - -% \question{Does the elimination in Prop follows a -% different rule than the elimination in Set?} - -% \answer There are two kinds of dependent case analysis. The result type of a -% case analysis may depend on the matched object (this is what is -% usually intended by dependent) but may also depend on the non-constant -% arguments of the type of the matched object without being dependent of -% the object itself. - -% This is typically what happens in a proof using equality. The result -% does not depend on the proof of the equality itself but crucially -% depends on the second compared argument of the equality. - -% It happens that proofs using elimination (i.e. case analysis or -% induction) on objects at the Set level are usually dependent on the -% matched term. This is because propositions precisely depend on the -% object on which an induction or case analysis is applied. Conversely, -% it happens that proofs using elimination on objects at the Prop level -% (typically elimination on equality proofs) are usually not dependent -% on the matched object. This is because proofs usually stay at the -% proof level and a few developments are stating things about proofs. -% But, again, to be not dependent on the matched objet does not mean not -% dependent at all. For equality, dependency on the second compared -% argument is precisely what provides with the substitutivity schema of -% equality. - -\question{Why is dependent elimination in Prop not -available by default?} - -\answer -This is just because most of the time it is not needed. To derive a -dependent elimination principle in {\tt Prop}, use the command {\tt Scheme} and -apply the elimination scheme using the \verb=using= option of -\verb=elim=, \verb=destruct= or \verb=induction=. - -\question{How to eliminate impossible cases of an inductive definition} - -\answer -Use {\tt inversion}. - -%\subsection{Induction} - -\question{How to perform double induction?} - -\answer In general a double induction is simply solved by an induction on the -first hypothesis followed by an inversion over the second -hypothesis. Here is an example - -\begin{coq_eval} -Reset Initial. -\end{coq_eval} - -\begin{coq_example} -Inductive even : nat -> Prop := - | even_O : even 0 - | even_S : forall n:nat, even n -> even (S (S n)). - -Inductive odd : nat -> Prop := - | odd_SO : odd 1 - | odd_S : forall n:nat, odd n -> odd (S (S n)). - -Goal forall n:nat, even n -> odd n -> False. -induction 1. - inversion 1. - inversion 1. apply IHeven; trivial. -Qed. -\end{coq_example} - -\Rem In case the type of the second induction hypothesis is not -dependent, {\tt inversion} can just be replaced by {\tt destruct}. - -\question{How to define a function by double recursion?} - -\answer The same trick applies, you can even use the pattern-matching -compilation algorithm to do the work for you. Here is an example: - -\begin{coq_example} -Fixpoint minus (n m:nat) {struct n} : nat := - match n, m with - | O, _ => 0 - | S k, O => S k - | S k, S l => minus k l - end. -Print minus. -\end{coq_example} - -\Rem In case of dependencies in the type of the induction objects -$t_1$ and $t_2$, an extra argument stating $t_1=t_2$ must be given to -the fixpoint definition - -\question{How to perform nested induction?} - -\answer To reason by nested induction, just reason by induction on the -successive components. - -\begin{coq_eval} -Require Import Arith. -\end{coq_eval} - -\begin{coq_example} -Infix "<" := lt (at level 50, no associativity). -Infix "<=" := le (at level 50, no associativity). -Lemma le_or_lt : forall n n0:nat, n0 < n \/ n <= n0. -induction n; destruct n0; auto with arith. -destruct (IHn n0); auto with arith. -\end{coq_example} - -\question{How to define a function by nested recursion?} - -\answer The same trick applies. Here is the example of Ackermann -function. - -\begin{coq_example} -Fixpoint ack (n:nat) : nat -> nat := - match n with - | O => S - | S n' => - (fix ack' (m:nat) : nat := - match m with - | O => ack n' 1 - | S m' => ack n' (ack' m') - end) - end. -\end{coq_example} - -\section{Coinductive types} - -\question{I have a cofixpoint t:=F(t) and I want to prove t=F(t). What is -the simplest way?} - -\answer Just case-expand F(t) then complete by a trivial case analysis. -Here is what it gives on e.g. the type of streams on naturals - -\begin{coq_example} -CoInductive Stream (A:Set) : Set := - Cons : A -> Stream A -> Stream A. -CoFixpoint nats (n:nat) : Stream nat := Cons n (nats (S n)). -Lemma Stream_unfold : - forall n:nat, nats n = Cons n (nats (S n)). -Proof. - intro; - change (nats n = match nats n with - | Cons x s => Cons x s - end). - case (nats n); reflexivity. -Qed. -\end{coq_example} - -\section{Miscellaneous} - -\question{I copy-paste a term and {\Coq} says it is not convertible - to the original term. Sometimes it even says the copied term is not -well-typed.} - -\answer This is probably due to invisible implicit information (implicit -arguments, coercions and Cases annotations) in the printed term, which -is not re-synthetised from the copied-pasted term in the same way as -it is in the original term. - - Consider for instance {\tt (@eq Type True True)}. This term is -printed as {\tt True=True} and re-parsed as {\tt (@eq Prop True -True)}. The two terms are not convertible (hence they fool tactics -like {\tt pattern}). - - There is currently no satisfactory answer to the problem. - - Due to coercions, one may even face type-checking errors. In some -rare cases, the criterion to hide coercions is a bit too loosy, which -may result in a typing error message if the parser is not able to find -again the missing coercion. - -\question{I have a problem of dependent elimination on -proofs, how to solve it?} - -\begin{coq_eval} -Reset Initial. -\end{coq_eval} - -\begin{coq_example*} -Inductive Def1 : Set := c1 : Def1. -Inductive DefProp : Def1 -> Set := - c2 : forall d:Def1, DefProp d. -Inductive Comb : Set := - c3 : forall d:Def1, DefProp d -> Comb. -Lemma eq_comb : - forall (d1 d1':Def1) (d2:DefProp d1) (d2':DefProp d1'), - d1 = d1' -> c3 d1 d2 = c3 d1' d2'. -\end{coq_example*} - -\answer You need to derive the dependent elimination -scheme for DefProp by hand using {\coqtt Scheme}. - -\begin{coq_eval} -Abort. -\end{coq_eval} - -\begin{coq_example*} -Scheme DefProp_elim := Induction for DefProp Sort Prop. -Lemma eq_comb : - forall d1 d1':Def1, - d1 = d1' -> - forall (d2:DefProp d1) (d2':DefProp d1'), c3 d1 d2 = c3 d1' d2'. -intros. -destruct H. -destruct d2 using DefProp_elim. -destruct d2' using DefProp_elim. -reflexivity. -Qed. -\end{coq_example*} - -\question{And what if I want to prove the following?} - -\begin{coq_example*} -Inductive natProp : nat -> Prop := - | p0 : natProp 0 - | pS : forall n:nat, natProp n -> natProp (S n). -Inductive package : Set := - pack : forall n:nat, natProp n -> package. -Lemma eq_pack : - forall n n':nat, - n = n' -> - forall (np:natProp n) (np':natProp n'), pack n np = pack n' np'. -\end{coq_example*} - -\answer - -\begin{coq_eval} -Abort. -\end{coq_eval} -\begin{coq_example*} -Scheme natProp_elim := Induction for natProp Sort Prop. -Definition pack_S : package -> package. -destruct 1. -apply (pack (S n)). -apply pS; assumption. -Defined. -Lemma eq_pack : - forall n n':nat, - n = n' -> - forall (np:natProp n) (np':natProp n'), pack n np = pack n' np'. -intros n n' Heq np np'. -generalize dependent n'. -induction np using natProp_elim. -induction np' using natProp_elim; intros; auto. - discriminate Heq. -induction np' using natProp_elim; intros; auto. - discriminate Heq. -change (pack_S (pack n np) = pack_S (pack n0 np')). -apply (f_equal (A:=package)). -apply IHnp. -auto. -Qed. -\end{coq_example*} - -\question{Why does {\Coq} tell me that \texttt{\{x:A|(P x)\}} is not convertible with \texttt{(sig A P)}?} - -\answer This is because \texttt{\{x:A|P x\}} is a notation for -\texttt{sig (fun x:A => P x)}. Since {\Coq} does not reason up to -$\eta$-conversion, this is different from \texttt{sig P}. - -\bibliographystyle{plain} -\bibliography{biblio} - -\end{document} diff --git a/doc/newfaq/main.tex b/doc/faq/FAQ.tex index 7b8ed6d10..7b8ed6d10 100644 --- a/doc/newfaq/main.tex +++ b/doc/faq/FAQ.tex diff --git a/doc/newfaq/axioms.eps b/doc/faq/axioms.eps index 3f3c01c43..3f3c01c43 100644 --- a/doc/newfaq/axioms.eps +++ b/doc/faq/axioms.eps diff --git a/doc/newfaq/axioms.fig b/doc/faq/axioms.fig index f07759302..f07759302 100644 --- a/doc/newfaq/axioms.fig +++ b/doc/faq/axioms.fig diff --git a/doc/faq/axioms.png b/doc/faq/axioms.png Binary files differnew file mode 100644 index 000000000..2aee09166 --- /dev/null +++ b/doc/faq/axioms.png diff --git a/doc/newfaq/fk.bib b/doc/faq/fk.bib index 392e401fc..392e401fc 100644 --- a/doc/newfaq/fk.bib +++ b/doc/faq/fk.bib diff --git a/doc/faq/hevea.sty b/doc/faq/hevea.sty new file mode 100644 index 000000000..6d49aa8ce --- /dev/null +++ b/doc/faq/hevea.sty @@ -0,0 +1,78 @@ +% hevea : hevea.sty +% This is a very basic style file for latex document to be processed +% with hevea. It contains definitions of LaTeX environment which are +% processed in a special way by the translator. +% Mostly : +% - latexonly, not processed by hevea, processed by latex. +% - htmlonly , the reverse. +% - rawhtml, to include raw HTML in hevea output. +% - toimage, to send text to the image file. +% The package also provides hevea logos, html related commands (ahref +% etc.), void cutting and image commands. +\NeedsTeXFormat{LaTeX2e} +\ProvidesPackage{hevea}[2002/01/11] +\RequirePackage{comment} +\newif\ifhevea\heveafalse +\@ifundefined{ifimagen}{\newif\ifimagen\imagenfalse} +\makeatletter% +\newcommand{\heveasmup}[2]{% +\raise #1\hbox{$\m@th$% + \csname S@\f@size\endcsname + \fontsize\sf@size 0% + \math@fontsfalse\selectfont +#2% +}}% +\DeclareRobustCommand{\hevea}{H\kern-.15em\heveasmup{.2ex}{E}\kern-.15emV\kern-.15em\heveasmup{.2ex}{E}\kern-.15emA}% +\DeclareRobustCommand{\hacha}{H\kern-.15em\heveasmup{.2ex}{A}\kern-.15emC\kern-.1em\heveasmup{.2ex}{H}\kern-.15emA}% +\DeclareRobustCommand{\html}{\protect\heveasmup{0.ex}{HTML}} +%%%%%%%%% Hyperlinks hevea style +\newcommand{\ahref}[2]{{#2}} +\newcommand{\ahrefloc}[2]{{#2}} +\newcommand{\aname}[2]{{#2}} +\newcommand{\ahrefurl}[1]{\texttt{#1}} +\newcommand{\footahref}[2]{#2\footnote{\texttt{#1}}} +\newcommand{\mailto}[1]{\texttt{#1}} +\newcommand{\imgsrc}[2][]{} +\newcommand{\home}[1]{\protect\raisebox{-.75ex}{\char126}#1} +\AtBeginDocument +{\@ifundefined{url} +{%url package is not loaded +\let\url\ahref\let\oneurl\ahrefurl\let\footurl\footahref} +{}} +%% Void cutting instructions +\newcounter{cuttingdepth} +\newcommand{\tocnumber}{} +\newcommand{\notocnumber}{} +\newcommand{\cuttingunit}{} +\newcommand{\cutdef}[2][]{} +\newcommand{\cuthere}[2]{} +\newcommand{\cutend}{} +\newcommand{\htmlhead}[1]{} +\newcommand{\htmlfoot}[1]{} +\newcommand{\htmlprefix}[1]{} +\newenvironment{cutflow}[1]{}{} +\newcommand{\cutname}[1]{} +\newcommand{\toplinks}[3]{} +%%%% Html only +\excludecomment{rawhtml} +\newcommand{\rawhtmlinput}[1]{} +\excludecomment{htmlonly} +%%%% Latex only +\newenvironment{latexonly}{}{} +\newenvironment{verblatex}{}{} +%%%% Image file stuff +\def\toimage{\endgroup} +\def\endtoimage{\begingroup\def\@currenvir{toimage}} +\def\verbimage{\endgroup} +\def\endverbimage{\begingroup\def\@currenvir{verbimage}} +\newcommand{\imageflush}[1][]{} +%%% Bgcolor definition +\newsavebox{\@bgcolorbin} +\newenvironment{bgcolor}[2][] + {\newcommand{\@mycolor}{#2}\begin{lrbox}{\@bgcolorbin}\vbox\bgroup} + {\egroup\end{lrbox}% + \begin{flushleft}% + \colorbox{\@mycolor}{\usebox{\@bgcolorbin}}% + \end{flushleft}} +%%% Postlude +\makeatother diff --git a/doc/newfaq/interval_discr.v b/doc/faq/interval_discr.v index 972300dac..972300dac 100644 --- a/doc/newfaq/interval_discr.v +++ b/doc/faq/interval_discr.v diff --git a/doc/main.html b/doc/main.html deleted file mode 100644 index 1b5898298..000000000 --- a/doc/main.html +++ /dev/null @@ -1,13 +0,0 @@ -<HTML> - -<HEAD> - -<TITLE>The Coq Proof Assistant Reference Manual</TITLE> - -</HEAD> - -<FRAMESET ROWS=90%,*><FRAME SRC="cover.html" NAME="UP"> -<FRAME SRC="main-0.html"> -</FRAMESET> - -</HTML>
\ No newline at end of file diff --git a/doc/newfaq/faq.cls b/doc/newfaq/faq.cls deleted file mode 100644 index 304260996..000000000 --- a/doc/newfaq/faq.cls +++ /dev/null @@ -1,70 +0,0 @@ -% simple class to format the UK TeX FAQ in two columns - -\ProvidesClass{faq}[2002/03/11 v2.0 UK TeX FAQ] - -\NeedsTeXFormat{LaTeX2e}[1995/12/01] - -\DeclareOption*{\PassOptionsToClass{\CurrentOption}{article}} -\ProcessOptions - -\LoadClass{article} - -\RequirePackage[hyphens,obeyspaces]{url} -\RequirePackage{multicol,faq} - -% now, hack at page layout, taking account of whether we're in a -% single-column version... - -% **************************************** -% * PAGE LAYOUT * -% **************************************** -% -% (This stuff is hacked from SPQR (et al) in baskerv.cls) -% -% SIDE MARGINS: (as is for single column) -\ifsinglecolumn\else -\oddsidemargin -2.5pc \evensidemargin -2.5pc -\marginparwidth 4pc % don't use marginal notes... -\marginparsep 0.5pc % ...in the UK TUG newsletter -\fi - -% VERTICAL SPACING: -\topmargin -0.5in % allow half an inch border -\headheight 0\p@ % we don't bother with headers here ... -\headsep 0\p@ % ... this ain't a publication -\topskip 10\p@ -\footskip 15\p@ - -% DIMENSION OF TEXT: - -% vertical dimension -\textheight \paperheight -\advance\textheight -1.5in -%\textheight 250mm % height of text on a page (A4 paper) - -% horizontal dimension: pro tem, as is for singlcolumn -\ifsinglecolumn\else -\textwidth \paperwidth -\advance\textwidth -1in -%\textwidth 180mm % total width of a page (A4 paper) - -\columnseprule 0.5\p@ % width of line in the inter-column gutter -\columnsep 10mm % space between columns -\tolerance 9999 % make those columns justify -\fi - -% FOOTNOTES: -\footnotesep 6\p@ -\skip\footins 19.5\p@ plus 12\p@ \@minus \p@ - -% little patch generated in investigating a request from a user here -% in cambridge -\let\FAQ@@tableofcontents\tableofcontents -\renewcommand\tableofcontents{{% - \let\FAQ@@addvspace\addvspace - \def\addvspace##1{% - \@tempskipa##1\relax - \FAQ@@addvspace{0.1\@tempskipa}% - }% - \FAQ@@tableofcontents -}} diff --git a/doc/newfaq/faq.sty b/doc/newfaq/faq.sty deleted file mode 100644 index 0c8f23bf7..000000000 --- a/doc/newfaq/faq.sty +++ /dev/null @@ -1,883 +0,0 @@ -% This is a LaTeX2e package for the UKTUG FAQ document. -% -% uses production LaTeX 2e commands -\NeedsTeXFormat{LaTeX2e}[1994/06/01]% at least! -\ProvidesPackage{faq}[2002/10/01 v2.3 English TeX FAQ macros] -% -% something affecting fonts: do we use only freely available fonts -% (i.e., are we going to make the postscript of this publicly -% available?); the config file could change this setting if -% necessary. things affected herein are the definition of \MP (for -% metapost), which isn't currently doable with free fonts, and -% suppression of boldface versions of the logo fonts. -\newif\ifpublicversion \publicversiontrue - -% -% what fonts are we going to typeset in? -\newif\ifusePSfont -\InputIfFileExists{faqfont.cfg}% must set \ifusePSfont if necessary - {\typeout{FAQ -- loading font configuration file faqfont.cfg}} - {\RequirePackage{times}% - \usePSfonttrue - \usepackage[T1,OT1]{fontenc}% - \usepackage{textcomp}% - \DeclareRobustCommand{\$}{\char`\$}% otherwise tries to load tctt.... - % use cmtt for typewriter rather than Cou-beastly-rier - \renewcommand{\ttdefault}{cmtt}% - \@ifundefined{Dings}{\RequirePackage{pifont}% - \def\Dings{\nopagebreak{\footnotesize - \dingline{167}}}% - }% - {}% - } - -% -% switches (potentially) to be set according to status -\newif\ifpdf -\newif\ifsinglecolumn - -% -% Status values -\providecommand{\Status}{0} -\ifcase\Status\relax - % 0: default case is do nothing -% \typeout{faq.sty: default output using \ifprivate private\else -% public\fi\space fonts} - \singlecolumnfalse - \pdffalse -\or - % 1: pdf output using public fonts - \typeout{faq.sty: 1-col pdf output using public fonts} - \singlecolumntrue - \pdftrue - \let\multicols\@gobble - \let\endmulticols\relax -\or - % 2: pdf output using public fonts, two columns - \typeout{faq.sty: 2-col pdf output using public fonts} - \singlecolumnfalse - \pdftrue -\fi - -% -% if we're doing pdf, set up hyperref package and backdoors that avoid -% its sillier byproducts... -\ifpdf - \pdfavoidoverfull=1 - \let\@faq@@url\url - \urldef\DebianSocialContract\@faq@@url - {http://www.debian.org/social_contract#guidelines} - \RequirePackage[pdftex% - ,colorlinks% - ,pdftitle=The\ UK\ TUG\ FAQ% - ,linkcolor=blue% - ,pdfpagemode=None% - ,pdfstartview=FitBH% -% ,bookmarks=false% - ,bookmarksnumbered% - ]{hyperref} - \usepackage{thumbpdf} - \pdfstringdefDisableCommands{% - \let\cs\psd@cs - \def\csx#1{\textbackslash#1}% - \let\acro\@firstofone - \let\ProgName\@firstofone - \let\Package\@firstofone - \def\meta#1{<#1>}% - % - \def\twee{2e}% - \def\AllTeX{(La)TeX}% - \def\WYSIWYG{WYSIWYG}% - \def\AMSTeX{AmSTeX}% - \def\BibTeX{BibTeX}% - \def\PiCTeX{PiCTeX}% - \def\CDROM{CD-ROM}% - \def\TeXXeT{TeXXeT}% - \def\MLTeX{ML-TeX}% - \def\MP{MetaPost}% - \def\NTS{NTS}% - \def\dots{...}% - \def\obracesymbol{\{}% - \def\cbracesymbol{\}}% - }% - \begingroup - \lccode`\~=`\|% - \lowercase{\endgroup - \def\psd@cs~#1~{\textbackslash#1}% - }% - % adding table of contents to bookmarks - \let\Orig@tableofcontents\tableofcontents - \def\tableofcontents{% - \pdfbookmark[1]{\contentsname}{contents}% - \Orig@tableofcontents - }% - % adding \subsection*{Finding the Files} - \AtBeginDocument{% - \let\Orig@subsection\subsection - \def\subsection{% - \@ifstar{\bookmark@subsectionstar}{\Orig@subsection}% - }% - }% - \def\bookmark@subsectionstar#1{% - \advance\Hy@linkcounter by 1\relax - \pdfbookmark[2]{#1}{subsectionstar.\the\Hy@linkcounter}% - \Orig@subsection*{#1}% - }% -\fi - -% -% general support -%\RequirePackage{calc} -% -% code for handling logo font -\RequirePackage{mflogo} -\ifpublicversion - \renewcommand{\MP}{Meta\-Post} - \let\faq@@MF\MF - \def\faq@bx{bx} - \DeclareRobustCommand{\MF}{{% - \ifx\f@series\faq@bx - \expandafter\textmd% - \fi - {\faq@@MF}% - }% - } -\fi -% -% get texnames package (as amended) -\RequirePackage{texnames} -% -% ifthenelse for the undefined references -\RequirePackage{ifthen} -% -% we define html only stuff using Eijkhout's package -\RequirePackage{comment} -\excludecomment{htmlversion} -\ifpdf -\includecomment{pdfversion} -\excludecomment{dviversion} -\includecomment{wideversion} -\excludecomment{narrowversion} -\else -\excludecomment{pdfversion} -\includecomment{dviversion} -\includecomment{narrowversion} -\excludecomment{wideversion} -\fi -% -% but we also want a `short' version, like LaTeX2HTML's -\let\htmlonly\@gobble -% -% the Baskerville and other logos and abbreviations -\providecommand\BV{\emph{Baskerville}} -\providecommand\DANTE{\acro{DANTE}\@} -\providecommand\MSDOS{\acro{MS-DOS}\@} -\providecommand\CDROM{\acro{CD-ROM}\@} -\providecommand\TeXXeT{\TeX-{}-X\lower.5ex\hbox{E}\kern-.1667emT\@} -\providecommand\MLTeX{ML-\TeX} -% -% provided for consistency's sake -\newcommand\PS{PostScript} -% -\def\careof{\leavevmode\hbox{\raise.75ex\hbox{c}\kern-.15em - /\kern-.125em\smash{\lower.3ex\hbox{o}}}} -% -% \cs{SMC} \emph{isn't} small caps~--- Barbara Beeton says she thinks -% of it as ``big small caps''. She says (modulo capitalisation of -% things\dots): -% \begin{quote} -% For the things it's used for, regular small caps are not -% appropriate~--- they're too small. Real small caps are -% appropriate for author names (and are so used in continental -% bibliographies), section headings, running heads, and, on -% occasion, words to which some emphasis is to be given. \cs{SMC} -% was designed to be used for acronyms and all-caps abbreviations, -% which look terrible in small caps, but nearly as bad in all caps -% in the regular text size. The principle of using ``one size -% smaller'' than the text size is similar to the design of caps in -% German~--- where they are smaller relative to lowercase than are -% caps in fonts intended for English, to improve the appearance of -% regular text in which caps are used at the heads of all nouns, not -% just at the beginnings of sentences. -% \end{quote} -% -% We define this in terms of the memory of the size currently selected -% that's maintained in \cs{@currsize}: if the user does something -% silly re.~selecting fonts, we'll get the wrong results. The -% following code is adapted from |relsize.sty| by Donald Arseneau and -% Matt Swift, from a 2.09 original by Bernie Cosell. (Note that the -% order of examination of \cs{@currsize} is to get the commonest cases -% out of the way first.) -% \begin{macrocode} -%<!latex2e>\def\SMC{\small} -%<*latex2e> -\DeclareRobustCommand\SMC{% - \ifx\@currsize\normalsize\small\else - \ifx\@currsize\small\footnotesize\else - \ifx\@currsize\footnotesize\scriptsize\else - \ifx\@currsize\large\normalsize\else - \ifx\@currsize\Large\large\else - \ifx\@currsize\LARGE\Large\else - \ifx\@currsize\scriptsize\tiny\else - \ifx\@currsize\tiny\tiny\else - \ifx\@currsize\huge\LARGE\else - \ifx\@currsize\Huge\huge\else - \small\SMC@unknown@warning - \fi\fi\fi\fi\fi\fi\fi\fi\fi\fi -} -\newcommand\SMC@unknown@warning{\PackageWarning{faq}{Unknown text font - size command -- using \string\small}} -\DeclareRobustCommand\textSMC[1]{{\SMC #1}} -% \end{macrocode} -% -% The \cs{acro} command uses \cs{SMC} as it was originally intended. -% Note that, since most of these things are uppercase-only names, it -% fiddles with the spacefactor after inserting its text. -% -% \begin{macrocode} -\DeclareRobustCommand\acro[1]{\textSMC{#1}\@} -%</latex2e> -%<!latex>\def\acro#1{{\SMC #1}\spacefactor\@m} -%<!latex2e>\def\acro#1{{\SMC #1}\@} -% \end{macrocode} -% -%\TUGboat (effectively) takes arguments {<empty>}vol(issue) -\DeclareRobustCommand\TUGboat[1]{\expandafter\@TUGboat\ignorespaces} -\def\@TUGboat#1(#2){\textsl{TUGboat} \textbf{#1}(#2)} -% -% The NTS and eTeX (and for consistency Eplain) logos -\DeclareRobustCommand\NTS{$\mathcal{N}$\lower.5ex\hbox - {$\mathcal{T}$}$\mathcal{S}$\@} -\DeclareRobustCommand\eTeX{{$\varepsilon$}-\TeX} -\DeclareRobustCommand\Eplain{Eplain} -\DeclareRobustCommand\PDFTeX{\acro{PDF}\TeX} -\DeclareRobustCommand\PDFLaTeX{\acro{PDF}\LaTeX} -\DeclareRobustCommand\CONTeXT{Con\TeX{}t} -\DeclareRobustCommand\TeXsis{\TeX{}sis} -\DeclareRobustCommand\YandY{\acro{Y}\&\acro{Y}} -% -% Other odds and ends (appear differently in TeX and http or plain -% text -% -% wysiwyg gets capitalised at the beginning of a sentence. not -% entirely reliably... -\DeclareRobustCommand\WYSIWYG{% - \ifvmode - \let\faq@tempa\MakeUppercase - \else - \ifnum\spacefactor>2000 - \let\faq@tempa\MakeUppercase - \else - \let\faq@tempa\relax - \fi - \fi - \textsc{\faq@tempa wysiwyg}% -} -% -% Command for doing `square one' :-} -\newcommand\sqfbox[1]{\framebox{\makebox[\totalheight]{#1\/}}} -% -% an arrow used as a hyphen... -\newcommand\arrowhyph{\ensuremath{\rightarrow}\penalty0\hskip0pt\relax} -% -% Here's a \fullline macro that works in lists and so on -\newcommand\fullline[1]{\@tempdima\hsize\relax - \advance\@tempdima-\leftmargin\relax - \advance\@tempdima-\rightmargin\relax - \hb@xt@\@tempdima{#1}} -% -% for tidy expression of things with parentheses around them: -\newcommand\parens[1]{(#1)} -\newcommand\oparen{(}%)( [footling around to match brackety things in emacs] -\newcommand\cparen{)} -% -% make the tex logo robust -\edef\@tempa{\noexpand\DeclareRobustCommand\noexpand\TeX{\TeX}} -\@tempa -% -% this piece of fantasy was let loose on an unsuspecting world by -% christina thiele, but i bet she didn't write it ;-) -\edef\diatop{\noexpand\protect\csname diatop \endcsname} -\expandafter\def\csname diatop \endcsname[#1|#2]{% - \leavevmode - {% - \setbox1=\hbox{{#1{}}}\setbox2=\hbox{{#2{}}}% - \dimen0=\ifdim\wd1>\wd2\wd1\else\wd2\fi% - \dimen1=\ht2\advance\dimen1by-1ex% - \setbox1=\hbox to1\dimen0{\hss#1\hss}% - \rlap{\raise1\dimen1\box1}% - \hbox to1\dimen0{\hss#2\hss}% - }% -}% -% -% for han the thanh (who knows whether i've actually got this right; i -% can't use the T5 fonts, which aren't even really publicly available -% yet) -\DeclareRobustCommand{\The}{Th\diatop[\'|\^e]} -% -% 2e's LaTeX logo sets the A in scripstyle jammed up to the top of the T; it -% also has the advantage that it's set in the same font as the -% surrounding text. However, the esteemed bbeeton says the logo looks -% "squidge awful" in italic text (I agree; and the same is true of its -% behaviour in slanted text) -% -% So here's a version that allows for the slant of the leading L -\DeclareRobustCommand{\LaTeX}{L% - {\setbox0\hbox{T}% - \setbox\@tempboxa\hbox{$\m@th$% - \csname S@\f@size\endcsname - \fontsize\sf@size\z@ - \math@fontsfalse\selectfont - A}% - \@tempdima\ht0 - \advance\@tempdima-\ht\@tempboxa - \@tempdima\strip@pt\fontdimen1\font\@tempdima - \advance\@tempdima-.36em - \kern\@tempdima - \vbox to\ht0{\box\@tempboxa - \vss}% - }% - \kern-.15em - \TeX} -% -% Ditto for \AllTeX (as used in TUGboat) -\DeclareRobustCommand{\AllTeX}{(L% - {\setbox0\hbox{T}% - \setbox\@tempboxa\hbox{$\m@th$% - \csname S@\f@size\endcsname - \fontsize\sf@size\z@ - \math@fontsfalse\selectfont - A}% - \@tempdima\ht0 - \advance\@tempdima-\ht\@tempboxa - \@tempdima\strip@pt\fontdimen1\font\@tempdima - \advance\@tempdima-.36em - \kern\@tempdima - \vbox to\ht0{\box\@tempboxa - \vss}% - }\kern-.075em)% - \kern-.075em\TeX} -% -% A similar game is used in defining an `all LaTeX' sort of thing: -\DeclareRobustCommand\twee{2$_{\textstyle\varepsilon}$} -% -% it proves that, for Alan's stuff, the following needs to have been -% done _before_ we define the macros -\RequirePackage{shortvrb} -\MakeShortVerb{\|} -% -% A command which sets some text in typewriter, with the hyphenchar -% temporarily set to its first argument \FAQverb\HYPHEN{TEXT}. -% NB: This requires no catcode hackery, so should work inside moving -% arguments. It will, however, produce spurious spaces after CSs, and -% won't allow brace-unmatched input. It also won't survive going into a -% moving argument if \HYPHEN won't. -% -\let\FAQverbFamily\ttfamily -\DeclareRobustCommand{\FAQverb}[2]{{% - \ifvmode\leavevmode\fi - \lefthyphenmin=256\setlanguage\language - \FAQverbFamily\hyphenchar\the\font`#1\relax - \def\@tempa{#2}% - \expandafter\@faq@strip\meaning\@tempa\@faq@strip - \hyphenchar\the\font\m@ne -}\setlanguage\language} -\def\@faq@strip#1->#2\@faq@strip{#2} -% -% Document markup: -% -% (new method, using url.sty -- old version using FAQverb stuff -% deleted from comments 2000/03/24) -\newcommand\Email{\begingroup \urlstyle{tt}\Url} % email address -\ifpdf -\def\mailto|#1|{\href{mailto:#1}{\Email|#1|}} % url to mail somewhere -\else -\newcommand\mailto{\begingroup \urlstyle{tt}\Url} % mailable address -\fi -\let\Emaildot\Email % only needed for hysterical raisins -\DeclareRobustCommand\FTP{\begingroup \urlstyle{tt}\Url} % FTP site address -\DeclareRobustCommand\File{\begingroup \urlstyle{tt}\Url} % File name -\DeclareRobustCommand\@ctan@path{\begingroup \urlstyle{tt}\Url} % CTAN path - % (argument in braces) -\ifpdf -\newcommand\@CTAN[3]{\href{#1#2#3}{\@ctan@path{#2}}} % relay via hyperreference -\else -\newcommand\@CTAN[3]{\@ctan@path{#2}} % text-only reference -\fi -\newcommand\Newsgroup{\begingroup \urlstyle{tt}\Url} % newsgroup -\let\URL\url % just a URL -% url.sty defines \path, etc. hyperref may redefine... -\ifpdf - % hyperref has defined \href -\else - \newcommand\href{\begingroup - \@makeother\\% - \@makeother\_% - \@makeother\%% - \@makeother\~% - \@makeother\#% - \@href - } - \newcommand\@href[1]{\endgroup\urldef\@faq@tempurl\url{#1}% - \@href@text - } - \newcommand\@href@text[1]{#1 (see \@faq@tempurl)} -\fi - -\DeclareRobustCommand\ProgName{% - \begingroup - \def\UrlFont{\rmfamily\itshape}\Url@do - \Url -} -\let\Package\ProgName % pro tem -\let\Class\Package % ... -\let\FontName\Package % ... - -% another little oddity (from doc.sty originally, iirc) -\newcommand\meta[1]{\ensuremath{\langle}\emph{#1}\ensuremath{\rangle}} - -% -% ISBN references -\def\ISBN#1{\mbox{\acro{ISBN}}~#1} -% -% Alan's code for CTAN references (now hacked to be capable of urls -% for use in pdf output): -% -% define a location for a package on CTAN -% ignores a leading * (which has meaning for html version only) -% #1 is the package name -% #2 is the CTAN path to the thing -% a package in a directory -\ifpdf - \newcommand{\CTANdirectory}{\@ifstar\@sCTANdirectory\@CTANdirectory} -\else - \newcommand{\CTANdirectory}{\@ifstar\@CTANdirectory\@CTANdirectory} -\fi -\newcommand{\@CTANdirectory}[2]{\@ifundefined{ctan-#1}{% - \expandafter\gdef\csname ctan-#1\endcsname{\@CTAN\LocalCTAN{#2}\CTANDirFmt}% -}{% - \PackageWarningNoLine{faq}{Repeated definition of label: #1}% - \stepcounter{CTAN@replabs}% -}} -\ifpdf - \newcommand{\@sCTANdirectory}[2]{\@ifundefined{ctan-#1}{% - \expandafter\gdef\csname ctan-#1\endcsname{\@CTAN\LocalCTAN{#2}/}% - }{% - \PackageWarningNoLine{faq}{Repeated definition of label: #1}% - \stepcounter{CTAN@replabs}% - }} -\fi -% -% a package in a single file (the same appearance, but the WWW -- and -% ultimately the pdf -- versions are different). -\ifpdf -\newcommand{\CTANfile}[2]{\@ifundefined{ctan-#1}{% - \expandafter\gdef\csname ctan-#1\endcsname{\@CTAN\LocalCTAN{#2}{}}% -}{% - \PackageWarningNoLine{faq}{Repeated definition of label: #1}% - \stepcounter{CTAN@replabs}% -}} -\else -\let\CTANfile\CTANdirectory -\fi -% -% Make reference to a CTAN package -% -% counters for the undefined references and repeated labels -\newcounter{CTAN@unrefs} -\newcounter{CTAN@replabs}% -% -% the command itself -\DeclareRobustCommand{\CTANref}[1]{\@ifundefined{ctan-#1}{% - \PackageWarning{CTAN}{Undefined reference: #1}% - \stepcounter{CTAN@unrefs}% -}{% -% \edef\@tempa{\noexpand\CTAN{\csname ctan-#1\endcsname}}\@tempa - \csname ctan-#1\endcsname -}} -% -% hook for diagnosing undefined references at the end -\AtEndDocument{\ifthenelse{\theCTAN@unrefs > 0}{% - \PackageWarningNoLine{ctan}{There were \arabic{CTAN@unrefs} undefined - references to CTAN}% - }% - {}% - \ifthenelse{\theCTAN@replabs > 0}{% - \PackageWarningNoLine{ctan}{There were \arabic{CTAN@replabs} - multiply defined references to CTAN}% - }% - {}% -} -% -% a slight variation of description for lists of book titles -\newcommand{\booklabel}[1]{\hspace\labelsep\normalfont\itshape #1} -\newenvironment{booklist}{% - \begin{list}{}% - {% - \labelwidth\z@ - \itemindent-\leftmargin - \let\makelabel\booklabel - \parskip \z@ - \itemsep \z@ - }% - }% - {\end{list}} -% -% proglist is the same as booklist if we're using italics for program -% names, but will need hacking otherwise -\newenvironment{proglist}{\begin{booklist}}{\end{booklist}} -% -% similarly for ctanrefs environment -\newcommand{\ctanreference}[1]{\hspace\labelsep\normalfont\ttfamily\itshape#1% - \/\normalfont:} -\newenvironment{ctanrefs}{% - \par\noindent\leavevmode - \begin{list}{}% - {% - \labelwidth\z@ - \itemindent-\leftmargin - \let\makelabel\ctanreference - \topsep 4\p@ - \parskip \z@ - \itemsep \z@ - \@rightskip=\z@\@plus1in\relax - \spaceskip=.3333em\relax - \xspaceskip=.5em\relax - }% - }% - {\end{list}} -% -% compact the itemize, enumerate and description environments -\let\FAQ@@itemize\itemize -\renewcommand\itemize{% - \topsep 0.25\topsep - \FAQ@@itemize - \parskip \z@ - \itemsep \z@ -} -\let\FAQ@@enumerate\enumerate -\renewcommand\enumerate{% - \topsep 0.25\topsep - \FAQ@@enumerate - \parskip \z@ - \itemsep \z@ -} -\let\FAQ@@description\description -\renewcommand\description{% - \topsep 0.25\topsep - \FAQ@@description - \parskip \z@ - \itemsep \z@ -} -% -% and similarly close up verbatim's separation from what surrounds it -\let\FAQ@@verbatim\verbatim -\renewcommand\verbatim{% - \topsep 0.25\topsep - \FAQ@@verbatim -} -% -% \raggedwithindent is useful when we've got an URL or something -% overrunning the end of the line (and this line is terminated with -% \\) -% -% Typical usage is within the argument of a \nothtml command -\newcommand\raggedwithindent{% - \rightskip=\z@\@plus5em\relax - \spaceskip=.3333em\relax - \xspaceskip=.5em\relax - \hangindent=1pc\relax} -% -% the little bit(s) of code that's(re) going to be ignored when the -% html is generated are enclosed by the following two commands -\let\htmlignore\relax -\let\endhtmlignore\relax -% -% or it's the argument to \nothtml -\newcommand\nothtml[1]{#1} -% -% a trivium that appears differently in the two modes -\newcommand\latexhtml[2]{#1} -% -% things needed for the benefit of texfaq2html's `sanitise_line' -\let\textpercent\% -\let\faq@@textbar\textbar -\chardef\faq@vertbar`\| -\renewcommand\textbar{\def\@tempa{cmtt}% - \ifx\@tempa\f@family - \faq@vertbar - \else - \faq@@textbar - \fi -} -% -% redefine \cs{l@section} to require space for itself at the bottom -% of a column -\renewcommand\l@section[2]{% - \ifnum \c@tocdepth >\z@ - \addpenalty\@secpenalty - \addvspace{1.0em \@plus\p@}% -% "needspace" element here (doesn't work) -% \vskip \z@ \@plus 3\baselineskip -% \penalty -\@highpenalty -% \vskip \z@ \@plus -3\baselineskip - \setlength\@tempdima{1.5em}% - \begingroup - \parindent \z@ \rightskip \@pnumwidth - \parfillskip -\@pnumwidth - \leavevmode \bfseries - \advance\leftskip\@tempdima - \hskip -\leftskip - #1\nobreak\hfil \nobreak\hb@xt@\@pnumwidth{\hss #2}\par - \endgroup - \fi -} -% -% subsections: these are a curious half-breed between latex sections -% and subsections -- as designed, i'm not intending there ever to be -% more than 9 per section (hahaha) -\renewcommand\subsection{\@startsection{subsection}% - \tw@ - \z@ - {-1.5ex \@plus-1ex \@minus-.3ex}% - {1ex \@plus.2ex}% - {\normalfont\large\bfseries - \raggedright}% - } -\renewcommand*\l@subsection[2]{% - \ifnum \c@tocdepth >\@ne - \addpenalty\@secpenalty - \addvspace{0.5em \@plus\p@}% -% "needspace" element here (doesn't work) -% \vskip \z@ \@plus 3\baselineskip -% \penalty -\@highpenalty -% \vskip \z@ \@plus -3\baselineskip - \setlength\@tempdima{2.0em}% - \begingroup - \parindent \z@ \rightskip \@pnumwidth - \parfillskip -\@pnumwidth - \leavevmode \bfseries - \advance\leftskip\@tempdima - \hskip -\leftskip - #1\nobreak\hfil \nobreak\hb@xt@\@pnumwidth{\hss #2}\par - \endgroup - \fi} -% -% -% the question structure -% \Question[label name]{question asked} -% if [label name] present, the named label is assigned with \Qlabel -\newcounter{question} -\newcommand\Question[2][]{% - \ifpdf - \def\annot@label{#1}% - \def\annot@question{#2}% - \fi - \qu@stion{#2}% - \def\reserved@a{#1}% - \ifx\reserved@a\@empty - \PackageWarning{faq}{Question "#2" has no label}% - \else - \Qlabel{#1}% -% \addtocontents{lab}{\protect\QuestionLabel{#1}{#2}{\thepage}}% - \fi -} -\newcommand\qu@stion{\@startsection{question}% - \thr@@ - \z@ - {-1.25ex \@plus -1ex \@minus -.2ex}% - {0.75ex \@plus .2ex}% - {% - \normalfont - \normalsize - \bfseries - \raggedright - \protected@edef\@svsec{\protect\annot@set\@svsec}% - }% -} -\newcommand*\questionmark[1]{} -\newcommand*\l@question{\@dottedtocline{2}{2.0em}{2.3em}} -% -\long\def\@ReturnAfterFi#1\fi{\fi#1}% -\ifpdf - \newcommand*\toclevel@question{3}% - \let\orig@section\section - \let\orig@subsection\subsection - \let\orig@subsubsection\subsubsection - \def\section{% - \def\toclevel@question{2}% - \orig@section - } - \def\subsection{% - \def\toclevel@question{3}% - \orig@subsection - } - \def\subsubsection{% - \def\toclevel@question{4}% - \orig@subsubsection - } - % - \def\annot@set{% - \ifx\annot@label\@empty - \else - \begingroup - \def\x##1-##2\@nil{\def\annot@label{##2}}% - \expandafter\x\annot@label\@nil - \def\x##1_##2\@nil{% - ##1% - \ifx\\##2\\% - \else - \noexpand\textunderscore - \@ReturnAfterFi{\x##2\@nil}% - \fi - }% - \edef\annot@label{\expandafter\x\annot@label_\@nil}% - \edef\NL{\string\n}% - \pdfstringdef\annot@text{% - http://www.tex.ac.uk/cgi-bin/texfaq2html?label=\annot@label\NL - \annot@question - }% - \rlap{% - \kern-10mm\relax - \settoheight{\dimen@}{X}% - \pdfannotlink - width 200mm - height \dimen@ - depth 25mm - user {% - /Subtype/Text% - /T(Question \thequestion: \annot@label)% - /Contents(\annot@text)% - }% - \pdfendlink - }% - \endgroup - \fi - }% - \@ifundefined{pdfannotlink}{% - \let\pdfannotlink\pdfstartlink - }{} -\else - \let\annot@set\relax -\fi -% -% \QuestionLabel starts out as a null command (so that inputting a -% .lab file at s.o.d has no effect), but it's then reset to -% \@questionLabel in case the file is going to be read again later -% (e.g., as an appendix), but we don't have a sensible definition of -% _that_ yet, either... -\newcommand{\labellist}{% - \newcommand{\QuestionLabel}[3]{}% -% \@starttoc{lab}% - \let\QuestionLabel\@questionLabel -} -\newcommand{\@questionLabel}[3]{} -% -% \afterquestion is used when the \Question command itself has to be -% inside a group for some reason (e.g., to have it in \boldmath) -\newcommand\afterquestion{% - \global\toks@\expandafter{\the\everypar}% - \edef\@tempa{% - \noexpand\@afterindentfalse - \noexpand\everypar{\the\toks@}% - }% - \expandafter\endgroup\@tempa -} -% -% \cs{Destination} is used immediately after a \cs{Question} command -% in the various add-* files to signify where the question is supposed -% to go -\newcommand\Destination[1]{\begin{center} - \itshape#1 - \end{center} -} -% -% we `number' our sections alphabetically -\renewcommand{\thesection}{\Alph{section}} -% -% keywords for questions. these get translated into comments in web -% versions -\newcommand\keywords{\begingroup - \@makeother\\% - \@makeother\^% - \@makeother\_% - \@makeother\%% - \expandafter\endgroup - \@gobble -} -% -% \Qlabel and \Qref: define and refer to labels -\ifpdf -% hyperref version of \label doesn't get set until begin document - \AtBeginDocument{\let\Qlabel\label} -\else - \let\Qlabel\label -\fi -\newcommand\Qref{\@ifstar\@QrefA\@QrefB} -\newcommand\@QrefA[3][see question]{#2 (#1~\ref{#3})} -\newcommand\@QrefB[3][see question]{#1~\ref{#3}} -% -% from doc package, then hacked about by yours truly -\DeclareRobustCommand\csx[1]{\def\@tempa{#1}{\FAQverbFamily\char`\\% - \expandafter\@faq@strip\meaning\@tempa\@faq@strip}} -\def\cs|#1|{\csx{#1}} -% -% fancier versions of the above -% -% \cmdinvoke\cs<argument sequence> -% \cs typeset as above -% <argument sequence> may consist of optional or mandatory arguments; -% so far only "one mandatory" and "one optional, one mandatory" -% are supported by texfaq2html -% -% the `arguments' are simply typesett \texttt, as yet -- if something -% fancier is needed, there's a bunch of code needs rewriting here... -\DeclareRobustCommand\cmdinvoke{\@ifstar - {\let\@tempa\emph\@scmdinvoke}% - {\let\@tempa\relax\@scmdinvoke}% -} -\def\@scmdinvoke#1{\texttt{\symbol{92}#1}% - \futurelet\@let@token\@cmdinvoke -} -\def\@cmdinvoke{\ifx\@let@token\bgroup - \expandafter\@cmdinvoke@lbrace - \else - \ifx\@let@token[% ] - \expandafter\expandafter\expandafter\@cmdinvoke@lbrack - \fi - \fi -} -\def\@cmdinvoke@lbrace#1{\penalty-150\hskip0pt\relax - \texttt{\symbol{123}\@tempa{#1}\symbol{125}}% - \futurelet\@let@token\@cmdinvoke -} -\def\@cmdinvoke@lbrack[#1]{\penalty-150\hskip0pt\relax - \texttt{[\@tempa{#1}]}% - \futurelet\@let@token\@cmdinvoke -} - -% minuscule bit more structured markup... -\def\environment#1{\texttt{#1}} -\def\pkgoption#1{\texttt{#1}} - -% -% symbols for the braces (which can confuse perl sumfink rotten -\def\obracesymbol{\symbol{123}} -\def\cbracesymbol{\symbol{125}} -% -% for comments during maintenance -\def\Q#1{\footnote{{\ttfamily QUERY: #1}}} -%\def\Q#1{\marginpar{{\ttfamily QUERY: #1}}} -% -% Checking structure (null for now) -\newcommand\checked[2]{} -% -% for Alan's benefit -\newbox\@footnoteenvbox -\newenvironment{footnoteenv} - {\begin{lrbox}\@footnoteenvbox\reset@font\footnotesize\ignorespaces} - {\end{lrbox}% - \footnote{\unhbox\@footnoteenvbox}} -% -% end of package -\endinput diff --git a/doc/newfaq/main.v001.gif b/doc/newfaq/main.v001.gif deleted file mode 100644 index e69de29bb..000000000 --- a/doc/newfaq/main.v001.gif +++ /dev/null diff --git a/doc/newfaq/run.sh b/doc/newfaq/run.sh deleted file mode 100755 index 808d59b36..000000000 --- a/doc/newfaq/run.sh +++ /dev/null @@ -1,6 +0,0 @@ -#/bin/sh -coq-tex -n 72 -v -sl -small main.tex && latex main.v.tex && bibtex main.v && latex main.v.tex && latex main.v.tex && hevea -fix -nosymb main.v.tex - -# Commands for installation on pauillac -# scp main.v001.gif interval_discr.v pauillac.inria.fr:/net/pauillac/infosystems/www/coq/doc -# scp main.v.html pauillac.inria.fr:/net/pauillac/infosystems/www/coq/doc/faq.html diff --git a/doc/AddRefMan-pre.tex b/doc/refman/AddRefMan-pre.tex index 5312b8fc2..5312b8fc2 100644 --- a/doc/AddRefMan-pre.tex +++ b/doc/refman/AddRefMan-pre.tex diff --git a/doc/Cases.tex b/doc/refman/Cases.tex index 95411afae..95411afae 100644 --- a/doc/Cases.tex +++ b/doc/refman/Cases.tex diff --git a/doc/Coercion.tex b/doc/refman/Coercion.tex index 5445224b0..5445224b0 100644 --- a/doc/Coercion.tex +++ b/doc/refman/Coercion.tex diff --git a/doc/Extraction.tex b/doc/refman/Extraction.tex index a68969c38..a68969c38 100755 --- a/doc/Extraction.tex +++ b/doc/refman/Extraction.tex diff --git a/doc/Helm.tex b/doc/refman/Helm.tex index 262c3315d..262c3315d 100644 --- a/doc/Helm.tex +++ b/doc/refman/Helm.tex diff --git a/doc/Natural.tex b/doc/refman/Natural.tex index 69dfab87c..69dfab87c 100755 --- a/doc/Natural.tex +++ b/doc/refman/Natural.tex diff --git a/doc/Omega.tex b/doc/refman/Omega.tex index bbf17f630..bbf17f630 100755 --- a/doc/Omega.tex +++ b/doc/refman/Omega.tex diff --git a/doc/Polynom.tex b/doc/refman/Polynom.tex index 70889c9d4..70889c9d4 100644 --- a/doc/Polynom.tex +++ b/doc/refman/Polynom.tex diff --git a/doc/RefMan-add.tex b/doc/refman/RefMan-add.tex index d04d1468f..d04d1468f 100755 --- a/doc/RefMan-add.tex +++ b/doc/refman/RefMan-add.tex diff --git a/doc/RefMan-cas.tex b/doc/refman/RefMan-cas.tex index c79c14e9b..c79c14e9b 100755 --- a/doc/RefMan-cas.tex +++ b/doc/refman/RefMan-cas.tex diff --git a/doc/RefMan-cic.tex b/doc/refman/RefMan-cic.tex index 52745b7a9..52745b7a9 100755 --- a/doc/RefMan-cic.tex +++ b/doc/refman/RefMan-cic.tex diff --git a/doc/RefMan-coi.tex b/doc/refman/RefMan-coi.tex index 120c1201e..120c1201e 100755 --- a/doc/RefMan-coi.tex +++ b/doc/refman/RefMan-coi.tex diff --git a/doc/RefMan-com.tex b/doc/refman/RefMan-com.tex index 730100eed..730100eed 100755 --- a/doc/RefMan-com.tex +++ b/doc/refman/RefMan-com.tex diff --git a/doc/RefMan-ext.tex b/doc/refman/RefMan-ext.tex index 503d7571d..503d7571d 100644 --- a/doc/RefMan-ext.tex +++ b/doc/refman/RefMan-ext.tex diff --git a/doc/RefMan-gal.tex b/doc/refman/RefMan-gal.tex index 543b3fb82..543b3fb82 100644 --- a/doc/RefMan-gal.tex +++ b/doc/refman/RefMan-gal.tex diff --git a/doc/RefMan-ide.tex b/doc/refman/RefMan-ide.tex index d1497f162..d1497f162 100644 --- a/doc/RefMan-ide.tex +++ b/doc/refman/RefMan-ide.tex diff --git a/doc/RefMan-ind.tex b/doc/refman/RefMan-ind.tex index 3389382af..3389382af 100755 --- a/doc/RefMan-ind.tex +++ b/doc/refman/RefMan-ind.tex diff --git a/doc/RefMan-int.tex b/doc/refman/RefMan-int.tex index b1f4b26b8..b1f4b26b8 100755 --- a/doc/RefMan-int.tex +++ b/doc/refman/RefMan-int.tex diff --git a/doc/RefMan-lib.tex b/doc/refman/RefMan-lib.tex index 5a022c74e..5a022c74e 100755 --- a/doc/RefMan-lib.tex +++ b/doc/refman/RefMan-lib.tex diff --git a/doc/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex index eced8099a..eced8099a 100644 --- a/doc/RefMan-ltac.tex +++ b/doc/refman/RefMan-ltac.tex diff --git a/doc/RefMan-mod.tex b/doc/refman/RefMan-mod.tex index 9f6f2abce..9f6f2abce 100644 --- a/doc/RefMan-mod.tex +++ b/doc/refman/RefMan-mod.tex diff --git a/doc/RefMan-modr.tex b/doc/refman/RefMan-modr.tex index e08c7c401..e08c7c401 100644 --- a/doc/RefMan-modr.tex +++ b/doc/refman/RefMan-modr.tex diff --git a/doc/RefMan-oth.tex b/doc/refman/RefMan-oth.tex index 35c55e07b..35c55e07b 100644 --- a/doc/RefMan-oth.tex +++ b/doc/refman/RefMan-oth.tex diff --git a/doc/RefMan-pre.tex b/doc/refman/RefMan-pre.tex index 4559aaf47..4559aaf47 100755 --- a/doc/RefMan-pre.tex +++ b/doc/refman/RefMan-pre.tex diff --git a/doc/RefMan-pro.tex b/doc/refman/RefMan-pro.tex index 7565612d1..7565612d1 100755 --- a/doc/RefMan-pro.tex +++ b/doc/refman/RefMan-pro.tex diff --git a/doc/RefMan-syn.tex b/doc/refman/RefMan-syn.tex index 95f3d806b..95f3d806b 100755 --- a/doc/RefMan-syn.tex +++ b/doc/refman/RefMan-syn.tex diff --git a/doc/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index cb4abb22e..cb4abb22e 100644 --- a/doc/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex diff --git a/doc/RefMan-tacex.tex b/doc/refman/RefMan-tacex.tex index ecd54f449..ecd54f449 100644 --- a/doc/RefMan-tacex.tex +++ b/doc/refman/RefMan-tacex.tex diff --git a/doc/RefMan-tus.tex b/doc/refman/RefMan-tus.tex index 8be5c9635..8be5c9635 100755 --- a/doc/RefMan-tus.tex +++ b/doc/refman/RefMan-tus.tex diff --git a/doc/RefMan-uti.tex b/doc/refman/RefMan-uti.tex index 8c4c5edb8..8c4c5edb8 100755 --- a/doc/RefMan-uti.tex +++ b/doc/refman/RefMan-uti.tex diff --git a/doc/Reference-Manual.tex b/doc/refman/Reference-Manual.tex index fa909b607..fa909b607 100644 --- a/doc/Reference-Manual.tex +++ b/doc/refman/Reference-Manual.tex diff --git a/doc/Setoid.tex b/doc/refman/Setoid.tex index 867d60366..867d60366 100644 --- a/doc/Setoid.tex +++ b/doc/refman/Setoid.tex diff --git a/doc/biblio.bib b/doc/refman/biblio.bib index 378936d9a..378936d9a 100755 --- a/doc/biblio.bib +++ b/doc/refman/biblio.bib diff --git a/doc/coqdoc.tex b/doc/refman/coqdoc.tex index 7862c5c38..7862c5c38 100644 --- a/doc/coqdoc.tex +++ b/doc/refman/coqdoc.tex diff --git a/doc/coqide-queries.png b/doc/refman/coqide-queries.png Binary files differindex dea5626f8..dea5626f8 100644 --- a/doc/coqide-queries.png +++ b/doc/refman/coqide-queries.png diff --git a/doc/coqide.png b/doc/refman/coqide.png Binary files differindex a6a0f5850..a6a0f5850 100644 --- a/doc/coqide.png +++ b/doc/refman/coqide.png diff --git a/doc/cover.html b/doc/refman/cover.html index 2a09ea231..2a09ea231 100644 --- a/doc/cover.html +++ b/doc/refman/cover.html diff --git a/doc/headers.tex b/doc/refman/headers.tex index 21b3b6e85..21b3b6e85 100644 --- a/doc/headers.tex +++ b/doc/refman/headers.tex diff --git a/doc/refman/hevea.sty b/doc/refman/hevea.sty new file mode 100644 index 000000000..6d49aa8ce --- /dev/null +++ b/doc/refman/hevea.sty @@ -0,0 +1,78 @@ +% hevea : hevea.sty +% This is a very basic style file for latex document to be processed +% with hevea. It contains definitions of LaTeX environment which are +% processed in a special way by the translator. +% Mostly : +% - latexonly, not processed by hevea, processed by latex. +% - htmlonly , the reverse. +% - rawhtml, to include raw HTML in hevea output. +% - toimage, to send text to the image file. +% The package also provides hevea logos, html related commands (ahref +% etc.), void cutting and image commands. +\NeedsTeXFormat{LaTeX2e} +\ProvidesPackage{hevea}[2002/01/11] +\RequirePackage{comment} +\newif\ifhevea\heveafalse +\@ifundefined{ifimagen}{\newif\ifimagen\imagenfalse} +\makeatletter% +\newcommand{\heveasmup}[2]{% +\raise #1\hbox{$\m@th$% + \csname S@\f@size\endcsname + \fontsize\sf@size 0% + \math@fontsfalse\selectfont +#2% +}}% +\DeclareRobustCommand{\hevea}{H\kern-.15em\heveasmup{.2ex}{E}\kern-.15emV\kern-.15em\heveasmup{.2ex}{E}\kern-.15emA}% +\DeclareRobustCommand{\hacha}{H\kern-.15em\heveasmup{.2ex}{A}\kern-.15emC\kern-.1em\heveasmup{.2ex}{H}\kern-.15emA}% +\DeclareRobustCommand{\html}{\protect\heveasmup{0.ex}{HTML}} +%%%%%%%%% Hyperlinks hevea style +\newcommand{\ahref}[2]{{#2}} +\newcommand{\ahrefloc}[2]{{#2}} +\newcommand{\aname}[2]{{#2}} +\newcommand{\ahrefurl}[1]{\texttt{#1}} +\newcommand{\footahref}[2]{#2\footnote{\texttt{#1}}} +\newcommand{\mailto}[1]{\texttt{#1}} +\newcommand{\imgsrc}[2][]{} +\newcommand{\home}[1]{\protect\raisebox{-.75ex}{\char126}#1} +\AtBeginDocument +{\@ifundefined{url} +{%url package is not loaded +\let\url\ahref\let\oneurl\ahrefurl\let\footurl\footahref} +{}} +%% Void cutting instructions +\newcounter{cuttingdepth} +\newcommand{\tocnumber}{} +\newcommand{\notocnumber}{} +\newcommand{\cuttingunit}{} +\newcommand{\cutdef}[2][]{} +\newcommand{\cuthere}[2]{} +\newcommand{\cutend}{} +\newcommand{\htmlhead}[1]{} +\newcommand{\htmlfoot}[1]{} +\newcommand{\htmlprefix}[1]{} +\newenvironment{cutflow}[1]{}{} +\newcommand{\cutname}[1]{} +\newcommand{\toplinks}[3]{} +%%%% Html only +\excludecomment{rawhtml} +\newcommand{\rawhtmlinput}[1]{} +\excludecomment{htmlonly} +%%%% Latex only +\newenvironment{latexonly}{}{} +\newenvironment{verblatex}{}{} +%%%% Image file stuff +\def\toimage{\endgroup} +\def\endtoimage{\begingroup\def\@currenvir{toimage}} +\def\verbimage{\endgroup} +\def\endverbimage{\begingroup\def\@currenvir{verbimage}} +\newcommand{\imageflush}[1][]{} +%%% Bgcolor definition +\newsavebox{\@bgcolorbin} +\newenvironment{bgcolor}[2][] + {\newcommand{\@mycolor}{#2}\begin{lrbox}{\@bgcolorbin}\vbox\bgroup} + {\egroup\end{lrbox}% + \begin{flushleft}% + \colorbox{\@mycolor}{\usebox{\@bgcolorbin}}% + \end{flushleft}} +%%% Postlude +\makeatother diff --git a/doc/main-0.html b/doc/refman/index.html index db19678f3..db19678f3 100644 --- a/doc/main-0.html +++ b/doc/refman/index.html diff --git a/doc/RefMan-cover.tex b/doc/rt/RefMan-cover.tex index d881329a6..d881329a6 100644 --- a/doc/RefMan-cover.tex +++ b/doc/rt/RefMan-cover.tex diff --git a/doc/Tutorial-cover.tex b/doc/rt/Tutorial-cover.tex index b747b812e..b747b812e 100644 --- a/doc/Tutorial-cover.tex +++ b/doc/rt/Tutorial-cover.tex diff --git a/doc/Library.tex b/doc/stdlib/Library.tex index 58b2dc6df..58b2dc6df 100755 --- a/doc/Library.tex +++ b/doc/stdlib/Library.tex diff --git a/doc/syntax.txt b/doc/syntax.txt deleted file mode 100644 index 044ba8ee5..000000000 --- a/doc/syntax.txt +++ /dev/null @@ -1,68 +0,0 @@ - -====================================================================== -Conventions lexicales -====================================================================== - - INFIX = suites de symboles speciaux, repartis en plusieurs - categories correspondant a des precedences differentes - (comme en ocaml) - - si `s' est un infix, alors `@s' est un IDENT correspondant au - symbole (prefixe) correspondant - - d'ou definition $+ := plus; - check O + O; - -====================================================================== -Constr -====================================================================== - -simple_constr - ::= qident - | "\" binders "." constr \\ lambda - | "!" binders "." constr \\ produit - | constr "->" constr \\ assoc droite - | "(" simple_constr+ ")" - | "cases" constr "of" OPT "|" LIST0 equation SEP "|" "end" - | "fix" ident "where" LIST1 recursive SEP "and" - | "Set" - | "Prop" - | "Type" - | "?" - | constr infix constr \\ =, +, -, *, /, **, ++, etc. - \\ /\ and ? \/ or ? - | "~" constr \\ not ? - -constr - ::= simple_constr+ - -binders - ::= LIST1 ident SEP "," - | LIST1 binder SEP "," - -binder - ::= LIST1 ident SEP "," ":" constr - -equation - ::= pattern "=>" constr - -pattern - ::= - -recursive - ::= ident binders "{" "struct" ident "}" ":" constr ":=" constr - - -====================================================================== -Tactic -====================================================================== - - -====================================================================== -Vernac -====================================================================== - -vernac - ::= "definition" ... - | "fixpoint" LIST1 recursive SEP "and" - diff --git a/doc/Translator.tex b/doc/tools/Translator.tex index 005ca9c0c..005ca9c0c 100644 --- a/doc/Translator.tex +++ b/doc/tools/Translator.tex diff --git a/doc/tov8 b/doc/tov8 deleted file mode 100755 index b47f482e8..000000000 --- a/doc/tov8 +++ /dev/null @@ -1,5 +0,0 @@ -#!/bin/sh - -./tradv8 $1 -mv $1 $1.save -mv $1.v8 $1 diff --git a/doc/tradv8.ml4 b/doc/tradv8.ml4 deleted file mode 100644 index f050f7537..000000000 --- a/doc/tradv8.ml4 +++ /dev/null @@ -1,105 +0,0 @@ - -open Printf - -let file = Sys.argv.(1) - -let cin = open_in file -let cout = open_out (file ^ ".v8") - -let (coq_out, coq_in) as chan = Unix.open_process "coqtop -translate" - -let begin_coq = - Str.regexp - "\\\\begin{coq_\\(example\\|example\\*\\|example\\#\\|eval\\)}[ \t]*$" - -let end_coq = - Str.regexp - "\\\\end{coq_\\(example\\|example\\*\\|example\\#\\|eval\\)}[ \t]*$" - -let new_syntax = - Str.regexp "New Syntax:[ \t]*$" - -(* on envoie un Check O et on saute les 2 premiers New Syntax *) -let _ = - output_string coq_in "Check O.\n"; - flush coq_in; - while not (Str.string_match new_syntax (input_line coq_out) 0) do () done; - while not (Str.string_match new_syntax (input_line coq_out) 0) do () done; - printf "** init terminée\n"; flush stdout - -let iter_char_until_dot cin f = - printf "** entrée dans iter_char\n"; flush stdout; - let last_c = ref ' ' in - let rec loop () = - let c = input_char cin in - printf "[%c]" c; flush stdout; - f c; - if !last_c = '.' && (c = ' ' || c = '\t' || c = '\n') then - () - else begin - last_c := c; - loop () - end - in - loop () - -let trad_commands () = - (* on copie toutes les commandes dans un fichier temporaire *) - let tmp = Filename.temp_file "trad" ".v" in - let tmp_in, end_s = - let tmp_out = open_out tmp in - let rec loop () = - let s = input_line cin in - if Str.string_match end_coq s 0 then begin - close_out tmp_out; - open_in tmp, s - end else begin - output_string tmp_out (s ^ "\n"); - loop () - end - in - loop () - in - ignore (Sys.command (Printf.sprintf "cat %s" tmp)); - let one_command () = - (* on envoie toute la commande a Coq *) - iter_char_until_dot tmp_in (fun c -> output_char coq_in c); - (* on flush *) - flush coq_in; - (* on lit la réponse *) - try - (* 1. on cherche la ligne "New Syntax:" *) - while true do - let s = input_line coq_out in - if Str.string_match new_syntax s 0 then raise Exit - done - with Exit -> - (* 2. on copie tout jusqu'au point *) - printf "** New Syntax trouvé\n"; flush stdout; - iter_char_until_dot coq_out (fun c -> output_char cout c); - printf "** copie terminée\n"; flush stdout; - flush cout - in - try - while true do one_command () done; assert false - with End_of_file -> - printf "** End_of_file\n"; flush stdout; - Sys.remove tmp; - end_s - -let trad () = - while true do - let s = input_line cin in - output_string cout (s ^ "\n"); - if Str.string_match begin_coq s 0 then - let s = trad_commands () in - output_string cout (s ^ "\n"); - done - -let _ = - try - trad () - with End_of_file -> - close_out cout; - printf "** close_out cout\n"; flush stdout; - ignore (Unix.close_process chan) diff --git a/doc/Tutorial.tex b/doc/tutorial/Tutorial.tex index c5b977628..c5b977628 100755 --- a/doc/Tutorial.tex +++ b/doc/tutorial/Tutorial.tex diff --git a/doc/v8.txt b/doc/v8.txt deleted file mode 100644 index 24efe89b6..000000000 --- a/doc/v8.txt +++ /dev/null @@ -1,50 +0,0 @@ - -Anomalies.tex - -faq.tex - -Changes.tex -ChangesV6-2.tex -ChangesV6-3-1.tex -ChangesV6-3.tex -ChangesV7-0.tex - -macros.tex -title.tex - -Tutorial-cover.tex -Tutorial.tex - -Reference-Manual.tex -RefMan-add.tex -RefMan-cas.tex -RefMan-cic.tex -RefMan-coi.tex -RefMan-com.tex -RefMan-cover.tex -RefMan-ext.tex -RefMan-gal.tex -RefMan-ind.tex -RefMan-int.tex -RefMan-lib.tex -RefMan-ltac.tex -RefMan-mod.tex -RefMan-modr.tex -RefMan-oth.tex -RefMan-pre.tex -RefMan-pro.tex -RefMan-syn.tex -RefMan-tac.tex -RefMan-tacex.tex -RefMan-tus.tex -RefMan-uti.tex -AddRefMan-pre.tex -Cases.tex -Coercion.tex -Correctness.tex -Extraction.tex -Library.tex -Omega.tex -Polynom.tex -Setoid.tex - |