diff options
Diffstat (limited to 'doc/refman')
40 files changed, 892 insertions, 2801 deletions
diff --git a/doc/refman/AddRefMan-pre.tex b/doc/refman/AddRefMan-pre.tex index eee41a6798..856a823de0 100644 --- a/doc/refman/AddRefMan-pre.tex +++ b/doc/refman/AddRefMan-pre.tex @@ -4,6 +4,7 @@ \setheaders{Presentation of the Addendum} %END LATEX \chapter*{Presentation of the Addendum} +%HEVEA\cutname{addendum.html} Here you will find several pieces of additional documentation for the \Coq\ Reference Manual. Each of this chapters is concentrated on a diff --git a/doc/refman/AsyncProofs.tex b/doc/refman/AsyncProofs.tex index 1609e4a041..8f9d876cb8 100644 --- a/doc/refman/AsyncProofs.tex +++ b/doc/refman/AsyncProofs.tex @@ -1,4 +1,5 @@ -\achapter{Asynchronous and Parallel Proof Processing} +\achapter{Asynchronous and Parallel Proof Processing\label{Asyncprocessing}} +%HEVEA\cutname{async-proofs.html} \aauthor{Enrico Tassi} \label{pralitp} diff --git a/doc/refman/CanonicalStructures.tex b/doc/refman/CanonicalStructures.tex index 275e1c2d55..8961b00964 100644 --- a/doc/refman/CanonicalStructures.tex +++ b/doc/refman/CanonicalStructures.tex @@ -1,4 +1,5 @@ \achapter{Canonical Structures} +%HEVEA\cutname{canonical-structures.html} \aauthor{Assia Mahboubi and Enrico Tassi} \label{CS-full} diff --git a/doc/refman/Cases.tex b/doc/refman/Cases.tex index a95d8114ff..376ef031db 100644 --- a/doc/refman/Cases.tex +++ b/doc/refman/Cases.tex @@ -1,4 +1,5 @@ \achapter{Extended pattern-matching} +%HEVEA\cutname{cases.html} %BEGIN LATEX \defaultheaders %END LATEX @@ -279,6 +280,18 @@ Fail Check end). \end{coq_example} +The option {\tt Set Asymmetric Patterns} \optindex{Asymmetric Patterns} +(off by default) removes parameters from constructors in patterns: +\begin{coq_example} + Set Asymmetric Patterns. + Check (fun l:List nat => + match l with + | nil => nil + | cons _ l' => l' + end) + Unset Asymmetric Patterns. +\end{coq_example} + \paragraph{Implicit arguments in patterns} By default, implicit arguments are omitted in patterns. So we write: diff --git a/doc/refman/Classes.tex b/doc/refman/Classes.tex index 7e07868a38..6e76d04e77 100644 --- a/doc/refman/Classes.tex +++ b/doc/refman/Classes.tex @@ -6,6 +6,7 @@ \newcommand\tele[1]{\overrightarrow{#1}} \achapter{\protect{Type Classes}} +%HEVEA\cutname{type-classes.html} \aauthor{Matthieu Sozeau} \label{typeclasses} @@ -461,11 +462,18 @@ abbreviate a type, like {\tt relation A := A -> A -> Prop}. This is equivalent to {\tt Hint Transparent,Opaque} {\ident} {\tt: typeclass\_instances}. +\subsection{\tt Set Typeclasses Axioms Are Instances} +\optindex{Typeclasses Axioms Are Instances} + +This option (off by default since 8.8) automatically declares axioms +whose type is a typeclass at declaration time as instances of that +class. + \subsection{\tt Set Typeclasses Dependency Order} \optindex{Typeclasses Dependency Order} This option (on by default since 8.6) respects the dependency order between -subgoals, meaning that subgoals which are depended on by other subgoals +subgoals, meaning that subgoals which are depended on by other subgoals come first, while the non-dependent subgoals were put before the dependent ones previously (Coq v8.5 and below). This can result in quite different performance behaviors of proof search. @@ -518,14 +526,14 @@ potentially more expensive proof-search (i.e. more useless backtracking). \subsection{\tt Set Typeclass Resolution After Apply} -\optindex{Typeclasses Resolution After Apply} +\optindex{Typeclass Resolution After Apply} \emph{Deprecated since 8.6} This option (off by default in Coq 8.6 and 8.5) controls the resolution of typeclass subgoals generated by the {\tt apply} tactic. \subsection{\tt Set Typeclass Resolution For Conversion} -\optindex{Typeclasses Resolution For Conversion} +\optindex{Typeclass Resolution For Conversion} This option (on by default) controls the use of typeclass resolution when a unification problem cannot be solved during diff --git a/doc/refman/Coercion.tex b/doc/refman/Coercion.tex index 16006a6adf..ec46e1eb58 100644 --- a/doc/refman/Coercion.tex +++ b/doc/refman/Coercion.tex @@ -1,4 +1,5 @@ \achapter{Implicit Coercions} +%HEVEA\cutname{coercions.html} \aauthor{Amokrane Saïbi} \label{Coercions-full} diff --git a/doc/refman/Extraction.tex b/doc/refman/Extraction.tex index 499239b6f3..cff7be3e96 100644 --- a/doc/refman/Extraction.tex +++ b/doc/refman/Extraction.tex @@ -1,4 +1,5 @@ -\achapter{Extraction of programs in Objective Caml and Haskell} +\achapter{Extraction of programs in OCaml and Haskell} +%HEVEA\cutname{extraction.html} \label{Extraction} \aauthor{Jean-Christophe Filliâtre and Pierre Letouzey} \index{Extraction} @@ -94,12 +95,12 @@ one monolithic file or one file per \Coq\ library. \begin{description} \item {\tt Extraction TestCompile} \qualid$_1$ \dots\ \qualid$_n$. ~\par All the globals (or modules) \qualid$_1$ \dots\ \qualid$_n$ and all - their dependencies are extracted to a temporary Ocaml file, just as in + their dependencies are extracted to a temporary {\ocaml} file, just as in {\tt Extraction "{\em file}"}. Then this temporary file and its - signature are compiled with the same Ocaml compiler used to built - \Coq. This command succeeds only if the extraction and the Ocaml + signature are compiled with the same {\ocaml} compiler used to built + \Coq. This command succeeds only if the extraction and the {\ocaml} compilation succeed (and it fails if the current target language - of the extraction is not Ocaml). + of the extraction is not {\ocaml}). \end{description} \asection{Extraction options} @@ -108,26 +109,26 @@ one monolithic file or one file per \Coq\ library. \comindex{Extraction Language} The ability to fix target language is the first and more important -of the extraction options. Default is Ocaml. +of the extraction options. Default is {\ocaml}. \begin{description} -\item {\tt Extraction Language Ocaml}. +\item {\tt Extraction Language OCaml}. \item {\tt Extraction Language Haskell}. \item {\tt Extraction Language Scheme}. \end{description} \asubsection{Inlining and optimizations} -Since Objective Caml is a strict language, the extracted code has to +Since {\ocaml} is a strict language, the extracted code has to be optimized in order to be efficient (for instance, when using induction principles we do not want to compute all the recursive calls but only the needed ones). So the extraction mechanism provides an automatic optimization routine that will be called each time the user -want to generate Ocaml programs. The optimizations can be split in two +want to generate {\ocaml} programs. The optimizations can be split in two groups: the type-preserving ones -- essentially constant inlining and reductions -- and the non type-preserving ones -- some function abstractions of dummy types are removed when it is deemed safe in order to have more elegant types. Therefore some constants may not appear in the -resulting monolithic Ocaml program. In the case of modular extraction, +resulting monolithic {\ocaml} program. In the case of modular extraction, even if some inlining is done, the inlined constant are nevertheless printed, to ensure session-independent programs. @@ -366,15 +367,15 @@ As for {\tt Extract Inductive}, this command should be used with care: \item Extracting an inductive type to a pre-existing ML inductive type is quite sound. But extracting to a general type (by providing an ad-hoc pattern-matching) will often \emph{not} be fully rigorously -correct. For instance, when extracting {\tt nat} to Ocaml's {\tt +correct. For instance, when extracting {\tt nat} to {\ocaml}'s {\tt int}, it is theoretically possible to build {\tt nat} values that are -larger than Ocaml's {\tt max\_int}. It is the user's responsibility to +larger than {\ocaml}'s {\tt max\_int}. It is the user's responsibility to be sure that no overflow or other bad events occur in practice. \item Translating an inductive type to an ML type does \emph{not} magically improve the asymptotic complexity of functions, even if the ML type is an efficient representation. For instance, when extracting -{\tt nat} to Ocaml's {\tt int}, the function {\tt mult} stays +{\tt nat} to {\ocaml}'s {\tt int}, the function {\tt mult} stays quadratic. It might be interesting to associate this translation with some specific {\tt Extract Constant} when primitive counterparts exist. \end{itemize} @@ -390,16 +391,18 @@ Extract Inductive bool => "bool" [ "true" "false" ]. Extract Inductive sumbool => "bool" [ "true" "false" ]. \end{coq_example} -\noindent If an inductive constructor or type has arity 2 and the corresponding -string is enclosed by parenthesis, then the rest of the string is used -as infix constructor or type. +\noindent When extracting to {\ocaml}, if an inductive constructor or type +has arity 2 and the corresponding string is enclosed by parentheses, +and the string meets {\ocaml}'s lexical criteria for an infix symbol, +then the rest of the string is used as infix constructor or type. + \begin{coq_example} Extract Inductive list => "list" [ "[]" "(::)" ]. Extract Inductive prod => "(*)" [ "(,)" ]. \end{coq_example} \noindent As an example of translation to a non-inductive datatype, let's turn -{\tt nat} into Ocaml's {\tt int} (see caveat above): +{\tt nat} into {\ocaml}'s {\tt int} (see caveat above): \begin{coq_example} Extract Inductive nat => int [ "0" "succ" ] "(fun fO fS n -> if n=0 then fO () else fS (n-1))". @@ -414,7 +417,7 @@ directly depends from the names of the \Coq\ files. It may happen that these filenames are in conflict with already existing files, either in the standard library of the target language or in other code that is meant to be linked with the extracted code. -For instance the module {\tt List} exists both in \Coq\ and in Ocaml. +For instance the module {\tt List} exists both in \Coq\ and in {\ocaml}. It is possible to instruct the extraction not to use particular filenames. \begin{description} @@ -427,7 +430,7 @@ It is possible to instruct the extraction not to use particular filenames. Allow the extraction to use any filename. \end{description} -\noindent For Ocaml, a typical use of these commands is +\noindent For {\ocaml}, a typical use of these commands is {\tt Extraction Blacklist String List}. \asection{Differences between \Coq\ and ML type systems} @@ -435,7 +438,7 @@ It is possible to instruct the extraction not to use particular filenames. Due to differences between \Coq\ and ML type systems, some extracted programs are not directly typable in ML. -We now solve this problem (at least in Ocaml) by adding +We now solve this problem (at least in {\ocaml}) by adding when needed some unsafe casting {\tt Obj.magic}, which give a generic type {\tt 'a} to any term. @@ -452,7 +455,7 @@ Definition dp := fun (A B:Set)(x:A)(y:B)(f:forall C:Set, C->C) => (f A x, f B y). \end{verbatim} -In Ocaml, for instance, the direct extracted term would be +In {\ocaml}, for instance, the direct extracted term would be \begin{verbatim} let dp x y f = Pair((f () x),(f () y)) \end{verbatim} @@ -477,13 +480,13 @@ Inductive anything : Type := dummy : forall A:Set, A -> anything. \end{verbatim} which corresponds to the definition of an ML dynamic type. -In Ocaml, we must cast any argument of the constructor dummy. +In {\ocaml}, we must cast any argument of the constructor dummy. \end{itemize} \noindent Even with those unsafe castings, you should never get error like ``segmentation fault''. In fact even if your program may seem -ill-typed to the Ocaml type-checker, it can't go wrong: it comes +ill-typed to the {\ocaml} type-checker, it can't go wrong: it comes from a Coq well-typed terms, so for example inductives will always have the correct number of arguments, etc. diff --git a/doc/refman/Micromega.tex b/doc/refman/Micromega.tex index 4daf98f87a..2617142f5a 100644 --- a/doc/refman/Micromega.tex +++ b/doc/refman/Micromega.tex @@ -1,4 +1,5 @@ \achapter{Micromega: tactics for solving arithmetic goals over ordered rings} +%HEVEA\cutname{micromega.html} \aauthor{Frédéric Besson and Evgeny Makarov} \newtheorem{theorem}{Theorem} diff --git a/doc/refman/Misc.tex b/doc/refman/Misc.tex index e953d2f709..ab00fbfe37 100644 --- a/doc/refman/Misc.tex +++ b/doc/refman/Misc.tex @@ -1,4 +1,5 @@ \achapter{\protect{Miscellaneous extensions}} +%HEVEA\cutname{miscellaneous.html} \asection{Program derivation} diff --git a/doc/refman/Nsatz.tex b/doc/refman/Nsatz.tex index 70e36a5ee9..1401af10f6 100644 --- a/doc/refman/Nsatz.tex +++ b/doc/refman/Nsatz.tex @@ -1,4 +1,5 @@ \achapter{Nsatz: tactics for proving equalities in integral domains} +%HEVEA\cutname{nsatz.html} \aauthor{Loïc Pottier} The tactic \texttt{nsatz} proves goals of the form diff --git a/doc/refman/Omega.tex b/doc/refman/Omega.tex index 1610305e75..82765da6ed 100644 --- a/doc/refman/Omega.tex +++ b/doc/refman/Omega.tex @@ -1,5 +1,6 @@ \achapter{Omega: a solver of quantifier-free problems in Presburger Arithmetic} +%HEVEA\cutname{omega.html} \aauthor{Pierre Crégut} \label{OmegaChapter} @@ -148,6 +149,32 @@ intro; omega. % Other examples can be found in \verb+$COQLIB/theories/DEMOS/OMEGA+. +\section{Options} + +\begin{quote} + \optindex{Stable Omega} + {\tt Unset Stable Omega} +\end{quote} +This deprecated option (on by default) is for compatibility with Coq +pre 8.5. It resets internal name counters to make executions of +{\tt omega} independent. + +\begin{quote} + \optindex{Omega UseLocalDefs} + {\tt Unset Omega UseLocalDefs} +\end{quote} +This option (on by default) allows {\tt omega} to use the bodies of +local variables. + +\begin{quote} + \optindex{Omega System} + {\tt Set Omega System} + \optindex{Omega Action} + {\tt Set Omega Action} +\end{quote} +These two options (off by default) activate the printing of debug +information. + \asection{Technical data} \label{technical} diff --git a/doc/refman/Polynom.tex b/doc/refman/Polynom.tex index 77d5928345..d9b8b8c522 100644 --- a/doc/refman/Polynom.tex +++ b/doc/refman/Polynom.tex @@ -1,4 +1,5 @@ \achapter{The \texttt{ring} and \texttt{field} tactic families} +%HEVEA\cutname{ring.html} \aauthor{Bruno Barras, Benjamin Gr\'egoire, Assia Mahboubi, Laurent Th\'ery\footnote{based on previous work from Patrick Loiseleur and Samuel Boutin}} diff --git a/doc/refman/Program.tex b/doc/refman/Program.tex index f60908da6c..1e204dc83d 100644 --- a/doc/refman/Program.tex +++ b/doc/refman/Program.tex @@ -1,4 +1,5 @@ \achapter{\Program{}} +%HEVEA\cutname{program.html} \label{Program} \aauthor{Matthieu Sozeau} \index{Program} diff --git a/doc/refman/RefMan-add.tex b/doc/refman/RefMan-add.tex deleted file mode 100644 index 2094c9d2d5..0000000000 --- a/doc/refman/RefMan-add.tex +++ /dev/null @@ -1,58 +0,0 @@ -\chapter[List of additional documentation]{List of additional documentation\label{Addoc}} - -\section[Tutorials]{Tutorials\label{Tutorial}} -A companion volume to this reference manual, the \Coq\ Tutorial, is -aimed at gently introducing new users to developing proofs in \Coq\ -without assuming prior knowledge of type theory. In a second step, the -user can read also the tutorial on recursive types (document {\tt -RecTutorial.ps}). - -\section[The \Coq\ standard library]{The \Coq\ standard library\label{Addoc-library}} -A brief description of the \Coq\ standard library is given in the additional -document {\tt Library.dvi}. - -\section[Installation and un-installation procedures]{Installation and un-installation procedures\label{Addoc-install}} -A \verb!INSTALL! file in the distribution explains how to install -\Coq. - -\section[{\tt Extraction} of programs]{{\tt Extraction} of programs\label{Addoc-extract}} -{\tt Extraction} is a package offering some special facilities to -extract ML program files. It is described in the separate document -{\tt Extraction.dvi} -\index{Extraction of programs} - -\section[{\tt Program}]{A tool for {\tt Program}-ing\label{Addoc-program}} -{\tt Program} is a package offering some special facilities to -extract ML program files. It is described in the separate document -{\tt Program.dvi} -\index{Program-ing} - -\section[Proof printing in {\tt Natural} language]{Proof printing in {\tt Natural} language\label{Addoc-natural}} -{\tt Natural} is a tool to print proofs in natural language. -It is described in the separate document {\tt Natural.dvi}. -\index{Natural@{\tt Print Natural}} -\index{Printing in natural language} - -\section[The {\tt Omega} decision tactic]{The {\tt Omega} decision tactic\label{Addoc-omega}} -{\bf Omega} is a tactic to automatically solve arithmetical goals in -Presburger arithmetic (i.e. arithmetic without multiplication). -It is described in the separate document {\tt Omega.dvi}. -\index{Omega@{\tt Omega}} - -\section[Simplification on rings]{Simplification on rings\label{Addoc-polynom}} -A documentation of the package {\tt polynom} (simplification on rings) -can be found in the document {\tt Polynom.dvi} -\index{Polynom@{\tt Polynom}} -\index{Simplification on rings} - -%\section[Anomalies]{Anomalies\label{Addoc-anomalies}} -%The separate document {\tt Anomalies.*} gives a list of known -%anomalies and bugs of the system. Before communicating us an -%anomalous behavior, please check first whether it has been already -%reported in this document. - - -%%% Local Variables: -%%% mode: latex -%%% TeX-master: "Reference-Manual" -%%% End: diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex index ad795d4064..2695c5eee4 100644 --- a/doc/refman/RefMan-cic.tex +++ b/doc/refman/RefMan-cic.tex @@ -2,6 +2,7 @@ \label{Cic} \index{Cic@\textsc{CIC}} \index{Calculus of Inductive Constructions}} +%HEVEA\cutname{cic.html} The underlying formal language of {\Coq} is a {\em Calculus of Inductive Constructions} (\CIC) whose inference rules are presented in @@ -882,56 +883,60 @@ the type $V$ satisfies the nested positivity condition for $X$ \settowidth\framecharacterwidth{\hh} \newcommand\ws{\hbox{}\hskip\the\framecharacterwidth} \newcommand\ruleref[1]{\hskip.25em\dots\hskip.2em{\em (bullet #1)}} +\newcommand{\NatTree}{\mbox{\textsf{nattree}}} +\newcommand{\NatTreeA}{\mbox{\textsf{nattree}}~\ensuremath{A}} +\newcommand{\cnode}{\mbox{\textsf{node}}} +\newcommand{\cleaf}{\mbox{\textsf{leaf}}} -\noindent For instance, if one considers the type +\noindent For instance, if one considers the following variant of a tree type branching over the natural numbers \begin{verbatim} -Inductive tree (A:Type) : Type := - | leaf : list A - | node : A -> (nat -> tree A) -> tree A +Inductive nattree (A:Type) : Type := + | leaf : nattree A + | node : A -> (nat -> nattree A) -> nattree A \end{verbatim} \begin{latexonly} -\noindent Then every instantiated constructor of $\ListA$ satisfies the nested positivity condition for $\List$\\ +\noindent Then every instantiated constructor of $\NatTreeA$ satisfies the nested positivity condition for $\NatTree$\\ \noindent \ws\ws\vv\\ -\ws\ws\vh\hh\ws concerning type $\ListA$ of constructor $\Nil$:\\ -\ws\ws\vv\ws\ws\ws\ws Type $\ListA$ of constructor $\Nil$ satisfies the positivity condition for $\List$\\ -\ws\ws\vv\ws\ws\ws\ws because $\List$ does not appear in any (real) arguments of the type of that constructor\\ -\ws\ws\vv\ws\ws\ws\ws (primarily because $\List$ does not have any (real) arguments)\ruleref1\\ +\ws\ws\vh\hh\ws concerning type $\NatTreeA$ of constructor $\cleaf$:\\ +\ws\ws\vv\ws\ws\ws\ws Type $\NatTreeA$ of constructor $\cleaf$ satisfies the positivity condition for $\NatTree$\\ +\ws\ws\vv\ws\ws\ws\ws because $\NatTree$ does not appear in any (real) arguments of the type of that constructor\\ +\ws\ws\vv\ws\ws\ws\ws (primarily because $\NatTree$ does not have any (real) arguments)\ruleref1\\ \ws\ws\vv\\ -\ws\ws\hv\hh\ws concerning type $\forall~A\ra\ListA\ra\ListA$ of constructor $\cons$:\\ -\ws\ws\ws\ws\ws\ws\ws Type $\forall~A:\Type,A\ra\ListA\ra\ListA$ of constructor $\cons$\\ -\ws\ws\ws\ws\ws\ws\ws satisfies the positivity condition for $\List$ because:\\ +\ws\ws\hv\hh\ws concerning type $\forall~A\ra(\NN\ra\NatTreeA)\ra\NatTreeA$ of constructor $\cnode$:\\ + \ws\ws\ws\ws\ws\ws\ws Type $\forall~A:\Type,A\ra(\NN\ra\NatTreeA)\ra\NatTreeA$ of constructor $\cnode$\\ +\ws\ws\ws\ws\ws\ws\ws satisfies the positivity condition for $\NatTree$ because:\\ \ws\ws\ws\ws\ws\ws\ws\vv\\ -\ws\ws\ws\ws\ws\ws\ws\vh\hh\ws $\List$ occurs only strictly positively in $\Type$\ruleref3\\ +\ws\ws\ws\ws\ws\ws\ws\vh\hh\ws $\NatTree$ occurs only strictly positively in $\Type$\ruleref1\\ \ws\ws\ws\ws\ws\ws\ws\vv\\ -\ws\ws\ws\ws\ws\ws\ws\vh\hh\ws $\List$ occurs only strictly positively in $A$\ruleref3\\ +\ws\ws\ws\ws\ws\ws\ws\vh\hh\ws $\NatTree$ occurs only strictly positively in $A$\ruleref1\\ \ws\ws\ws\ws\ws\ws\ws\vv\\ -\ws\ws\ws\ws\ws\ws\ws\vh\hh\ws $\List$ occurs only strictly positively in $\ListA$\ruleref4\\ + \ws\ws\ws\ws\ws\ws\ws\vh\hh\ws $\NatTree$ occurs only strictly positively in $\NN\ra\NatTreeA$\ruleref{3+2}\\ \ws\ws\ws\ws\ws\ws\ws\vv\\ -\ws\ws\ws\ws\ws\ws\ws\hv\hh\ws $\List$ satisfies the positivity condition for $\ListA$\ruleref1 +\ws\ws\ws\ws\ws\ws\ws\hv\hh\ws $\NatTree$ satisfies the positivity condition for $\NatTreeA$\ruleref1 \end{latexonly} \begin{rawhtml} <pre> -<span style="font-family:serif">Then every instantiated constructor of <span style="font-family:monospace">list A</span> satisfies the nested positivity condition for <span style="font-family:monospace">list</span></span> +<span style="font-family:serif">Then every instantiated constructor of <span style="font-family:monospace">nattree A</span> satisfies the nested positivity condition for <span style="font-family:monospace">nattree</span></span> │ - ├─ <span style="font-family:serif">concerning type <span style="font-family:monospace">list A</span> of constructor <span style="font-family:monospace">nil</span>:</span> - │ <span style="font-family:serif">Type <span style="font-family:monospace">list A</span> of constructor <span style="font-family:monospace">nil</span> satisfies the positivity condition for <span style="font-family:monospace">list</span></span> - │ <span style="font-family:serif">because <span style="font-family:monospace">list</span> does not appear in any (real) arguments of the type of that constructor</span> - │ <span style="font-family:serif">(primarily because list does not have any (real) arguments) ... <span style="font-style:italic">(bullet 1)</span></span> + ├─ <span style="font-family:serif">concerning type <span style="font-family:monospace">nattree A</span> of constructor <span style="font-family:monospace">nil</span>:</span> + │ <span style="font-family:serif">Type <span style="font-family:monospace">nattree A</span> of constructor <span style="font-family:monospace">nil</span> satisfies the positivity condition for <span style="font-family:monospace">nattree</span></span> + │ <span style="font-family:serif">because <span style="font-family:monospace">nattree</span> does not appear in any (real) arguments of the type of that constructor</span> + │ <span style="font-family:serif">(primarily because nattree does not have any (real) arguments) ... <span style="font-style:italic">(bullet 1)</span></span> │ - ╰─ <span style="font-family:serif">concerning type <span style="font-family:monospace">∀ A → list A → list A</span> of constructor <span style="font-family:monospace">cons</span>:</span> - <span style="font-family:serif">Type <span style="font-family:monospace">∀ A : Type, A → list A → list A</span> of constructor <span style="font-family:monospace">cons</span></span> - <span style="font-family:serif">satisfies the positivity condition for <span style="font-family:monospace">list</span> because:</span> + ╰─ <span style="font-family:serif">concerning type <span style="font-family:monospace">∀ A → (nat → nattree A) → nattree A</span> of constructor <span style="font-family:monospace">cons</span>:</span> + <span style="font-family:serif">Type <span style="font-family:monospace">∀ A : Type, A → (nat → nattree A) → nattree A</span> of constructor <span style="font-family:monospace">cons</span></span> + <span style="font-family:serif">satisfies the positivity condition for <span style="font-family:monospace">nattree</span> because:</span> │ - ├─ <span style="font-family:serif"><span style="font-family:monospace">list</span> occurs only strictly positively in <span style="font-family:monospace">Type</span> ... <span style="font-style:italic">(bullet 3)</span></span> + ├─ <span style="font-family:serif"><span style="font-family:monospace">nattree</span> occurs only strictly positively in <span style="font-family:monospace">Type</span> ... <span style="font-style:italic">(bullet 1)</span></span> │ - ├─ <span style="font-family:serif"><span style="font-family:monospace">list</span> occurs only strictly positively in <span style="font-family:monospace">A</span> ... <span style="font-style:italic">(bullet 3)</span></span> + ├─ <span style="font-family:serif"><span style="font-family:monospace">nattree</span> occurs only strictly positively in <span style="font-family:monospace">A</span> ... <span style="font-style:italic">(bullet 1)</span></span> │ - ├─ <span style="font-family:serif"><span style="font-family:monospace">list</span> occurs only strictly positively in <span style="font-family:monospace">list A</span> ... <span style="font-style:italic">(bullet 4)</span></span> + ├─ <span style="font-family:serif"><span style="font-family:monospace">nattree</span> occurs only strictly positively in <span style="font-family:monospace">nat → nattree A</span> ... <span style="font-style:italic">(bullet 3+2)</span></span> │ - ╰─ <span style="font-family:serif"><span style="font-family:monospace">list</span> satisfies the positivity condition for <span style="font-family:monospace">list A</span> ... <span style="font-style:italic">(bullet 1)</span></span> + ╰─ <span style="font-family:serif"><span style="font-family:monospace">nattree</span> satisfies the positivity condition for <span style="font-family:monospace">nattree A</span> ... <span style="font-style:italic">(bullet 1)</span></span> </pre> \end{rawhtml} diff --git a/doc/refman/RefMan-coi.tex b/doc/refman/RefMan-coi.tex deleted file mode 100644 index dac3c60bd6..0000000000 --- a/doc/refman/RefMan-coi.tex +++ /dev/null @@ -1,405 +0,0 @@ -%\documentstyle[11pt,../tools/coq-tex/coq]{article} -%\input{title} - -%\include{macros} -%\begin{document} - -%\coverpage{Co-inductive types in Coq}{Eduardo Gim\'enez} -\chapter[Co-inductive types in Coq]{Co-inductive types in Coq\label{Co-inductives}} - -%\begin{abstract} -{\it Co-inductive} types are types whose elements may not be well-founded. -A formal study of the Calculus of Constructions extended by -co-inductive types has been presented -in \cite{Gim94}. It is based on the notion of -{\it guarded definitions} introduced by Th. Coquand -in \cite{Coquand93}. The implementation is by E. Gim\'enez. -%\end{abstract} - -\section{A short introduction to co-inductive types} - -We assume that the reader is rather familiar with inductive types. -These types are characterized by their {\it constructors}, which can be -regarded as the basic methods from which the elements -of the type can be built up. It is implicit in the definition -of an inductive type that -its elements are the result of a {\it finite} number of -applications of its constructors. Co-inductive types arise from -relaxing this implicit condition and admitting that an element of -the type can also be introduced by a non-ending (but effective) process -of construction defined in terms of the basic methods which characterize the -type. So we could think in the wider notion of types defined by -constructors (let us call them {\it recursive types}) and classify -them into inductive and co-inductive ones, depending on whether or not -we consider non-ending methods as admissible for constructing elements -of the type. Note that in both cases we obtain a ``closed type'', all whose -elements are pre-determined in advance (by the constructors). When we -know that $a$ is an element of a recursive type (no matter if it is -inductive or co-inductive) what we know is that it is the result of applying -one of the basic forms of construction allowed for the type. -So the more primitive way of eliminating an element of a recursive type is -by case analysis, i.e. by considering through which constructor it could have -been introduced. In the case of inductive sets, the additional knowledge that -constructors can be applied only a finite number of times provide -us with a more powerful way of eliminating their elements, say, -the principle of -induction. This principle is obviously not valid for co-inductive types, -since it is just the expression of this extra knowledge attached to inductive -types. - - -An example of a co-inductive type is the type of infinite sequences formed with -elements of type $A$, or streams for shorter. In Coq, -it can be introduced using the \verb!CoInductive! command~: -\begin{coq_example} -CoInductive Stream (A:Set) : Set := - cons : A -> Stream A -> Stream A. -\end{coq_example} - -The syntax of this command is the same as the -command \verb!Inductive! (cf. section -\ref{gal_Inductive_Definitions}). -Definition of mutually co-inductive types are possible. - -As was already said, there are not principles of -induction for co-inductive sets, the only way of eliminating these -elements is by case analysis. -In the example of streams, this elimination principle can be -used for instance to define the well known -destructors on streams $\hd : (\Str\;A)\rightarrow A$ -and $\tl: (\Str\;A)\rightarrow (\Str\;A)$ : -\begin{coq_example} -Section Destructors. -Variable A : Set. -Definition hd (x:Stream A) := match x with - | cons a s => a - end. -Definition tl (x:Stream A) := match x with - | cons a s => s - end. -\end{coq_example} -\begin{coq_example*} -End Destructors. -\end{coq_example*} - -\subsection{Non-ending methods of construction} - -At this point the reader should have realized that we have left unexplained -what is a ``non-ending but effective process of -construction'' of a stream. In the widest sense, a -method is a non-ending process of construction if we can eliminate the -stream that it introduces, in other words, if we can reduce -any case analysis on it. In this sense, the following ways of -introducing a stream are not acceptable. -\begin{center} -$\zeros = (\cons\;\nat\;\nO\;(\tl\;\zeros))\;\;:\;\;(\Str\;\nat)$\\[12pt] -$\filter\;(\cons\;A\;a\;s) = \si\;\;(P\;a)\;\;\alors\;\;(\cons\;A\;a\;(\filter\;s))\;\;\sinon\;\;(\filter\;s) )\;\;:\;\;(\Str\;A)$ -\end{center} -\noindent The former it is not valid since the stream can not be eliminated -to obtain its tail. In the latter, a stream is naively defined as -the result of erasing from another (arbitrary) stream -all the elements which does not verify a certain property $P$. This -does not always makes sense, for example it does not when all the elements -of the stream verify $P$, in which case we can not eliminate it to -obtain its head\footnote{Note that there is no notion of ``the empty -stream'', a stream is always infinite and build by a \texttt{cons}.}. -On the contrary, the following definitions are acceptable methods for -constructing a stream~: -\begin{center} -$\zeros = (\cons\;\nat\;\nO\;\zeros)\;\;:\;\;(\Str\;\nat)\;\;\;(*)$\\[12pt] -$(\from\;n) = (\cons\;\nat\;n\;(\from\;(\nS\;n)))\;:\;(\Str\;\nat)$\\[12pt] -$\alter = (\cons\;\bool\;\true\;(\cons\;\bool\;\false\;\alter))\;:\;(\Str\;\bool)$. -\end{center} -\noindent The first one introduces a stream containing all the natural numbers -greater than a given one, and the second the stream which infinitely -alternates the booleans true and false. - -In general it is not evident to realise when a definition can -be accepted or not. However, there is a class of definitions that -can be easily recognised as being valid : those -where (1) all the recursive calls of the method are done -after having explicitly mentioned which is (at least) the first constructor -to start building the element, and (2) no other -functions apart from constructors are applied to recursive calls. -This class of definitions is usually -referred as {\it guarded-by-constructors} -definitions \cite{Coquand93,Gim94}. -The methods $\from$ -and $\alter$ are examples of definitions which are guarded by constructors. -The definition of function $\filter$ is not, because there is no -constructor to guard -the recursive call in the {\it else} branch. Neither is the one of -$\zeros$, since there is function applied to the recursive call -which is not a constructor. However, there is a difference between -the definition of $\zeros$ and $\filter$. The former may be seen as a -wrong way of characterising an object which makes sense, and it can -be reformulated in an admissible way using the equation (*). On the contrary, -the definition of -$\filter$ can not be patched, since is the idea itself -of traversing an infinite -construction searching for an element whose existence is not ensured -which does not make sense. - - - -Guarded definitions are exactly the kind of non-ending process of -construction which are allowed in Coq. The way of introducing -a guarded definition in Coq is using the special command -{\tt CoFixpoint}. This command verifies that the definition introduces an -element of a co-inductive type, and checks if it is guarded by constructors. -If we try to -introduce the definitions above, $\from$ and $\alter$ will be accepted, -while $\zeros$ and $\filter$ will be rejected giving some explanation -about why. -\begin{coq_example} -CoFixpoint zeros : Stream nat := cons nat 0%N (tl nat zeros). -CoFixpoint zeros : Stream nat := cons nat 0%N zeros. -CoFixpoint from (n:nat) : Stream nat := cons nat n (from (S n)). -\end{coq_example} - -As in the \verb!Fixpoint! command (see Section~\ref{Fixpoint}), it is possible -to introduce a block of mutually dependent methods. The general syntax -for this case is : - -{\tt CoFixpoint {\ident$_1$} :{\term$_1$} := {\term$_1'$}\\ - with\\ - \mbox{}\hspace{0.1cm} $\ldots$ \\ - with {\ident$_m$} : {\term$_m$} := {\term$_m'$}} - - -\subsection{Non-ending methods and reduction} - -The elimination of a stream introduced by a \verb!CoFixpoint! definition -is done lazily, i.e. its definition can be expanded only when it occurs -at the head of an application which is the argument of a case expression. -Isolately it is considered as a canonical expression which -is completely evaluated. We can test this using the command \verb!compute! -to calculate the normal forms of some terms~: -\begin{coq_example} -Eval compute in (from 0). -Eval compute in (hd nat (from 0)). -Eval compute in (tl nat (from 0)). -\end{coq_example} -\noindent Thus, the equality -$(\from\;n)\equiv(\cons\;\nat\;n\;(\from \; (\S\;n)))$ -does not hold as definitional one. Nevertheless, it can be proved -as a propositional equality, in the sense of Leibniz's equality. -The version {\it à la Leibniz} of the equality above follows from -a general lemma stating that eliminating and then re-introducing a stream -yields the same stream. -\begin{coq_example} -Lemma unfold_Stream : - forall x:Stream nat, x = match x with - | cons a s => cons nat a s - end. -\end{coq_example} - -\noindent The proof is immediate from the analysis of -the possible cases for $x$, which transforms -the equality in a trivial one. - -\begin{coq_example} -olddestruct x. -trivial. -\end{coq_example} -\begin{coq_eval} -Qed. -\end{coq_eval} -The application of this lemma to $(\from\;n)$ puts this -constant at the head of an application which is an argument -of a case analysis, forcing its expansion. -We can test the type of this application using Coq's command \verb!Check!, -which infers the type of a given term. -\begin{coq_example} -Check (fun n:nat => unfold_Stream (from n)). -\end{coq_example} - \noindent Actually, The elimination of $(\from\;n)$ has actually -no effect, because it is followed by a re-introduction, -so the type of this application is in fact -definitionally equal to the -desired proposition. We can test this computing -the normal form of the application above to see its type. -\begin{coq_example} -Transparent unfold_Stream. -Eval compute in (fun n:nat => unfold_Stream (from n)). -\end{coq_example} - - -\section{Reasoning about infinite objects} - -At a first sight, it might seem that -case analysis does not provide a very powerful way -of reasoning about infinite objects. In fact, what we can prove about -an infinite object using -only case analysis is just what we can prove unfolding its method -of construction a finite number of times, which is not always -enough. Consider for example the following method for appending -two streams~: -\begin{coq_example} -Variable A : Set. -CoFixpoint conc (s1 s2:Stream A) : Stream A := - cons A (hd A s1) (conc (tl A s1) s2). -\end{coq_example} - -Informally speaking, we expect that for all pair of streams $s_1$ and $s_2$, -$(\conc\;s_1\;s_2)$ -defines the ``the same'' stream as $s_1$, -in the sense that if we would be able to unfold the definition -``up to the infinite'', we would obtain definitionally equal normal forms. -However, no finite unfolding of the definitions gives definitionally -equal terms. Their equality can not be proved just using case analysis. - - -The weakness of the elimination principle proposed for infinite objects -contrast with the power provided by the inductive -elimination principles, but it is not actually surprising. It just means -that we can not expect to prove very interesting things about infinite -objects doing finite proofs. To take advantage of infinite objects we -have to consider infinite proofs as well. For example, -if we want to catch up the equality between $(\conc\;s_1\;s_2)$ and -$s_1$ we have to introduce first the type of the infinite proofs -of equality between streams. This is a -co-inductive type, whose elements are build up from a -unique constructor, requiring a proof of the equality of the -heads of the streams, and an (infinite) proof of the equality -of their tails. - -\begin{coq_example} -CoInductive EqSt : Stream A -> Stream A -> Prop := - eqst : - forall s1 s2:Stream A, - hd A s1 = hd A s2 -> EqSt (tl A s1) (tl A s2) -> EqSt s1 s2. -\end{coq_example} -\noindent Now the equality of both streams can be proved introducing -an infinite object of type - -\noindent $(\EqSt\;s_1\;(\conc\;s_1\;s_2))$ by a \verb!CoFixpoint! -definition. -\begin{coq_example} -CoFixpoint eqproof (s1 s2:Stream A) : EqSt s1 (conc s1 s2) := - eqst s1 (conc s1 s2) (eq_refl (hd A (conc s1 s2))) - (eqproof (tl A s1) s2). -\end{coq_example} -\begin{coq_eval} -Reset eqproof. -\end{coq_eval} -\noindent Instead of giving an explicit definition, -we can use the proof editor of Coq to help us in -the construction of the proof. -A tactic \verb!Cofix! allows placing a \verb!CoFixpoint! definition -inside a proof. -This tactic introduces a variable in the context which has -the same type as the current goal, and its application stands -for a recursive call in the construction of the proof. If no name is -specified for this variable, the name of the lemma is chosen by -default. -%\pagebreak - -\begin{coq_example} -Lemma eqproof : forall s1 s2:Stream A, EqSt s1 (conc s1 s2). -cofix. -\end{coq_example} - -\noindent An easy (and wrong!) way of finishing the proof is just to apply the -variable \verb!eqproof!, which has the same type as the goal. - -\begin{coq_example} -intros. -apply eqproof. -\end{coq_example} - -\noindent The ``proof'' constructed in this way -would correspond to the \verb!CoFixpoint! definition -\begin{coq_example*} -CoFixpoint eqproof : forall s1 s2:Stream A, EqSt s1 (conc s1 s2) := - eqproof. -\end{coq_example*} - -\noindent which is obviously non-guarded. This means that -we can use the proof editor to -define a method of construction which does not make sense. However, -the system will never accept to include it as part of the theory, -because the guard condition is always verified before saving the proof. - -\begin{coq_example} -Qed. -\end{coq_example} - -\noindent Thus, the user must be careful in the -construction of infinite proofs -with the tactic \verb!Cofix!. Remark that once it has been used -the application of tactics performing automatic proof search in -the environment (like for example \verb!Auto!) -could introduce unguarded recursive calls in the proof. -The command \verb!Guarded! verifies -that the guarded condition has been not violated -during the construction of the proof. This command can be -applied even if the proof term is not complete. - - - -\begin{coq_example} -Restart. -cofix. -auto. -Guarded. -Undo. -Guarded. -\end{coq_example} - -\noindent To finish with this example, let us restart from the -beginning and show how to construct an admissible proof~: - -\begin{coq_example} -Restart. - cofix. -\end{coq_example} - -%\pagebreak - -\begin{coq_example} -intros. -apply eqst. -trivial. -simpl. -apply eqproof. -Qed. -\end{coq_example} - - -\section{Experiments with co-inductive types} - -Some examples involving co-inductive types are available with -the distributed system, in the theories library and in the contributions -of the Lyon site. Here we present a short description of their contents~: -\begin{itemize} -\item Directory \verb!theories/LISTS! : - \begin{itemize} - \item File \verb!Streams.v! : The type of streams and the -extensional equality between streams. - \end{itemize} - -\item Directory \verb!contrib/Lyon/COINDUCTIVES! : - \begin{itemize} - \item Directory \verb!ARITH! : An arithmetic where $\infty$ -is an explicit constant of the language instead of a metatheoretical notion. - \item Directory \verb!STREAM! : - \begin{itemize} - \item File \verb!Examples! : -Several examples of guarded definitions, as well as -of frequent errors in the introduction of a stream. A different -way of defining the extensional equality of two streams, -and the proofs showing that it is equivalent to the one in \verb!theories!. - \item File \verb!Alter.v! : An example showing how -an infinite proof introduced by a guarded definition can be also described -using an operator of co-recursion \cite{Gimenez95b}. - \end{itemize} -\item Directory \verb!PROCESSES! : A proof of the alternating -bit protocol based on Pra\-sad's Calculus of Broadcasting Systems \cite{Prasad93}, -and the verification of an interpreter for this calculus. -See \cite{Gimenez95b} for a complete description about this development. - \end{itemize} -\end{itemize} - -%\end{document} - diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex index 45230fb6e5..04a8a25c12 100644 --- a/doc/refman/RefMan-com.tex +++ b/doc/refman/RefMan-com.tex @@ -2,6 +2,7 @@ \ttindex{coqtop} \ttindex{coqc} \ttindex{coqchk}} +%HEVEA\cutname{commands.html} There are three \Coq~commands: \begin{itemize} @@ -106,6 +107,15 @@ The following command-line options are recognized by the commands {\tt recursively available from {\Coq} using absolute names (extending the {\dirpath} prefix) (see Section~\ref{LongNames}). + Note that only those subdirectories and files which obey the lexical + conventions of what is an {\ident} (see Section~\ref{lexical}) + are taken into account. Conversely, the underlying file systems or + operating systems may be more restrictive than {\Coq}. While Linux's + ext4 file system supports any {\Coq} recursive layout + (within the limit of 255 bytes per file name), the default on NTFS + (Windows) or HFS+ (MacOS X) file systems is on the contrary to + disallow two files differing only in the case in the same directory. + \SeeAlso Section~\ref{Libraries}. \item[{\tt -R} {\em directory} {\dirpath}]\ % @@ -204,11 +214,6 @@ The following command-line options are recognized by the commands {\tt % % Switch on the debug flag. -\item[{\tt -with-geoproof} (yes|no)]\ % - - Enable or not special functions for Geoproof within {\CoqIDE} (default - is yes). - \item[{\tt -color} (on|off|auto)]\ % Enable or not the coloring of output of {\tt coqtop}. Default is auto, @@ -294,8 +299,9 @@ The following command-line options are recognized by the commands {\tt \section{Compiled libraries checker ({\tt coqchk})} -The {\tt coqchk} command takes a list of library paths as argument. -The corresponding compiled libraries (.vo files) are searched in the +The {\tt coqchk} command takes a list of library paths as argument, described +either by their logical name or by their physical filename, which must end in +{\tt .vo}. The corresponding compiled libraries (.vo files) are searched in the path, recursively processing the libraries they depend on. The content of all these libraries is then type-checked. The effect of {\tt coqchk} is only to return with normal exit code in case of success, @@ -325,9 +331,12 @@ code, it cannot be guaranteed that the produced compiled libraries are correct. {\tt coqchk} is a standalone verifier, and thus it cannot be tainted by such malicious code. -Command-line options {\tt -I}, {\tt -R}, {\tt -where} and +Command-line options {\tt -Q}, {\tt -R}, {\tt -where} and {\tt -impredicative-set} are supported by {\tt coqchk} and have the -same meaning as for {\tt coqtop}. Extra options are: +same meaning as for {\tt coqtop}. As there is no notion of relative paths in +object files {\tt -Q} and {\tt -R} have exactly the same meaning. + +Extra options are: \begin{description} \item[{\tt -norec} {\em module}]\ % diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex index 713f344cbe..a1950d136e 100644 --- a/doc/refman/RefMan-ext.tex +++ b/doc/refman/RefMan-ext.tex @@ -1,4 +1,5 @@ \chapter[Extensions of \Gallina{}]{Extensions of \Gallina{}\label{Gallina-extension}\index{Gallina}} +%HEVEA\cutname{gallina-ext.html} {\gallina} is the kernel language of {\Coq}. We describe here extensions of the Gallina's syntax. @@ -279,15 +280,78 @@ of the chapter devoted to coercions. \label{prim-proj} The option {\tt Set Primitive Projections} turns on the use of primitive -projections when defining subsequent records. Primitive projections +projections when defining subsequent records (even through the {\tt + Inductive} and {\tt CoInductive} commands). Primitive projections extended the Calculus of Inductive Constructions with a new binary term constructor {\tt r.(p)} representing a primitive projection p applied to a record object {\tt r} (i.e., primitive projections are always applied). Even if the record type has parameters, these do not appear at applications of the projection, considerably reducing the sizes of terms when manipulating parameterized records and typechecking time. On the -user level, primitive projections are a transparent replacement -for the usual defined ones. +user level, primitive projections can be used as a replacement for the +usual defined ones, although there are a few notable differences. + +The internally omitted parameters can be reconstructed at printing time +even though they are absent in the actual AST manipulated by the kernel. This +can be obtained by setting the {\tt Printing Primitive Projection Parameters} +flag. Another compatibility printing can be activated thanks to the +{\tt Printing Primitive Projection Compatibility} option which governs the +printing of pattern-matching over primitive records. + +\subsubsection{Primitive Record Types} +When the {\tt Set Primitive Projections} option is on, definitions of +record types change meaning. When a type is declared with primitive +projections, its {\tt match} construct is disabled (see +\ref{primproj:compat} though). To eliminate the (co-)inductive type, one +must use its defined primitive projections. + +There are currently two ways to introduce primitive records types: +\begin{itemize} +\item Through the {\tt Record} command, in which case the type has to be + non-recursive. The defined type enjoys eta-conversion definitionally, + that is the generalized form of surjective pairing for records: + {\tt $r$ = Build\_R ($r$.($p_1$) .. $r$.($p_n$))}. Eta-conversion allows to define + dependent elimination for these types as well. +\item Through the {\tt Inductive} and {\tt CoInductive} commands, when + the body of the definition is a record declaration of the form {\tt + Build\_R \{ $p_1$ : $t_1$; .. ; $p_n$ : $t_n$ \}}. In this case the types can be + recursive and eta-conversion is disallowed. These kind of record types + differ from their traditional versions in the sense that dependent + elimination is not available for them and only non-dependent case analysis + can be defined. +\end{itemize} + +\subsubsection{Reduction} + +The basic reduction rule of a primitive projection is {\tt $p_i$ + (Build\_R $t_1$ .. $t_n$) $\rightarrow_{\iota}$ $t_i$}. However, to take the $\delta$ flag into +account, projections can be in two states: folded or unfolded. An +unfolded primitive projection application obeys the rule above, while +the folded version delta-reduces to the unfolded version. This allows to +precisely mimic the usual unfolding rules of constants. Projections +obey the usual {\tt simpl} flags of the {\tt Arguments} command in particular. + +There is currently no way to input unfolded primitive projections at the +user-level, and one must use the {\tt Printing Primitive Projection + Compatibility} to display unfolded primitive projections as matches +and distinguish them from folded ones. + +\subsubsection{Compatibility Projections and {\tt match}} +\label{primproj:compat} +To ease compatibility with ordinary record types, each primitive +projection is also defined as a ordinary constant taking parameters and +an object of the record type as arguments, and whose body is an +application of the unfolded primitive projection of the same name. These +constants are used when elaborating partial applications of the +projection. One can distinguish them from applications of the primitive +projection if the {\tt Printing Primitive Projection Parameters} option +is off: for a primitive projection application, parameters are printed +as underscores while for the compatibility projections they are printed +as usual. + +Additionally, user-written {\tt match} constructs on primitive records +are desugared into substitution of the projections, they cannot be +printed back as {\tt match} constructs. % - r.(p) and (p r) elaborate to native projection application, and % the parameters cannot be mentioned. The following arguments are @@ -305,13 +369,6 @@ for the usual defined ones. % - [pattern x at n], [rewrite x at n] and in general abstraction and selection % of occurrences may fail due to the disappearance of parameters. -The internally omitted parameters can be reconstructed at printing time -even though they are absent in the actual AST manipulated by the kernel. This -can be obtained by setting the {\tt Printing Primitive Projection Parameters} -flag. Another compatibility printing can be activated thanks to the -{\tt Printing Primitive Projection Compatibility} option which governs the -printing of pattern-matching over primitive records. - \section{Variants and extensions of {\mbox{\tt match}} \label{Extensions-of-match} \index{match@{\tt match\ldots with\ldots end}}} @@ -493,6 +550,60 @@ the same way as the {\Coq} kernel handles them. This tells if the printing matching mode is on or off. The default is on. +\subsubsection{Factorization of clauses with same right-hand side} +\label{SetPrintingFactorizableMatchPatterns} +\optindex{Printing Factorizable Match Patterns} + +When several patterns share the same right-hand side, it is +additionally possible to share the clauses using disjunctive patterns. +Assuming that the printing matching mode is on, whether {\Coq}'s +printer shall try to do this kind of factorization is governed by the +following commands: + +\begin{quote} +{\tt Set Printing Factorizable Match Patterns.} +\end{quote} +This tells {\Coq}'s printer to try to use disjunctive patterns. This is the default +behavior. + +\begin{quote} +{\tt Unset Printing Factorizable Match Patterns.} +\end{quote} +This tells {\Coq}'s printer not to try to use disjunctive patterns. + +\begin{quote} +{\tt Test Printing Factorizable Match Patterns.} +\end{quote} +This tells if the factorization of clauses with same right-hand side is +on or off. + +\subsubsection{Use of a default clause} +\label{SetPrintingAllowDefaultClause} +\optindex{Printing Allow Default Clause} + +When several patterns share the same right-hand side which do not +depend on the arguments of the patterns, yet an extra factorization is +possible: the disjunction of patterns can be replaced with a ``{\tt + \_}'' default clause. Assuming that the printing matching mode and +the factorization mode are on, whether {\Coq}'s printer shall try to +use a default clause is governed by the following commands: + +\begin{quote} +{\tt Set Printing Allow Default Clause.} +\end{quote} +This tells {\Coq}'s printer to use a default clause when relevant. This is the default +behavior. + +\begin{quote} +{\tt Unset Printing Allow Default Clause.} +\end{quote} +This tells {\Coq}'s printer not to use a default clause. + +\begin{quote} +{\tt Test Printing Allow Default Clause.} +\end{quote} +This tells if the use of a default clause is allowed. + \subsubsection{Printing of wildcard pattern \optindex{Printing Wildcard}} @@ -1664,7 +1775,7 @@ to be given as if none arguments were implicit. By symmetry, this also affects printing. To restore parsing and normal printing of implicit arguments, use: \begin{quote} -{\tt Set Parsing Explicit.} +{\tt Unset Parsing Explicit.} \end{quote} \subsection{Canonical structures @@ -1783,6 +1894,9 @@ This is useful for declaring the implicit type of a single variable. \subsection{Implicit generalization \label{implicit-generalization} \comindex{Generalizable Variables}} +% \textquoteleft since \` doesn't do what we want +\index{0genimpl@{\textquoteleft\{\ldots\}}} +\index{0genexpl@{\textquoteleft(\ldots)}} Implicit generalization is an automatic elaboration of a statement with free variables into a closed statement where these variables are diff --git a/doc/refman/RefMan-gal.tex b/doc/refman/RefMan-gal.tex index ef12fe416a..41ea0a5dcd 100644 --- a/doc/refman/RefMan-gal.tex +++ b/doc/refman/RefMan-gal.tex @@ -1,5 +1,6 @@ \chapter{The \gallina{} specification language \label{Gallina}\index{Gallina}} +%HEVEA\cutname{gallina.html} \label{BNF-syntax} % Used referred to as a chapter label This chapter describes \gallina, the specification language of {\Coq}. @@ -433,6 +434,7 @@ be shortened in {\tt fun~x~y~z~:~A~=>~t}). \subsection{Abstractions \label{abstractions} \index{abstractions}} +\index{fun@{{\tt fun \ldots => \ldots}}} The expression ``{\tt fun} {\ident} {\tt :} {\type} {\tt =>}~{\term}'' defines the {\em abstraction} of the variable {\ident}, of type @@ -454,6 +456,7 @@ occurs in the list of binders, it is expanded to a let-in definition \subsection{Products \label{products} \index{products}} +\index{forall@{{\tt forall \ldots, \ldots}}} The expression ``{\tt forall}~{\ident}~{\tt :}~{\type}{\tt ,}~{\term}'' denotes the {\em product} of the variable {\ident} of @@ -494,6 +497,7 @@ arguments is used for making explicit the value of implicit arguments \subsection{Type cast \label{typecast} \index{Cast}} +\index{cast@{{\tt(\ldots: \ldots)}}} The expression ``{\term}~{\tt :}~{\type}'' is a type cast expression. It enforces the type of {\term} to be {\type}. @@ -513,6 +517,7 @@ symbol ``\_'' and {\Coq} will guess the missing piece of information. \label{let-in} \index{Let-in definitions} \index{let-in}} +\index{let@{{\tt let \ldots := \ldots in \ldots}}} {\tt let}~{\ident}~{\tt :=}~{\term$_1$}~{\tt in}~{\term$_2$} denotes diff --git a/doc/refman/RefMan-ide.tex b/doc/refman/RefMan-ide.tex index c6fbd1c538..2d98534307 100644 --- a/doc/refman/RefMan-ide.tex +++ b/doc/refman/RefMan-ide.tex @@ -1,5 +1,6 @@ \chapter[\Coq{} Integrated Development Environment]{\Coq{} Integrated Development Environment\label{Addoc-coqide} \ttindex{coqide}} +%HEVEA\cutname{coqide.html} The \Coq{} Integrated Development Environment is a graphical tool, to be used as a user-friendly replacement to \texttt{coqtop}. Its main @@ -12,8 +13,7 @@ line. Without argument, the main screen is displayed with an ``unnamed buffer'', and with a file name as argument, another buffer displaying the contents of that file. Additionally, \verb|coqide| accepts the same options as \verb|coqtop|, given in Chapter~\ref{Addoc-coqc}, the ones having -obviously no meaning for \CoqIDE{} being ignored. Additionally, \verb|coqide| accepts the option \verb|-enable-geoproof| to enable the support for \emph{GeoProof} \footnote{\emph{GeoProof} is dynamic geometry software which can be used in conjunction with \CoqIDE{} to interactively build a Coq statement corresponding to a geometric figure. More information about \emph{GeoProof} can be found here: \url{http://home.gna.org/geoproof/} }. - +obviously no meaning for \CoqIDE{} being ignored. \begin{figure}[t] \begin{center} @@ -44,9 +44,10 @@ bottom is the status bar. In the script window, you may open arbitrarily many buffers to edit. The \emph{File} menu allows you to open files or create some, save them, print or export them into various formats. Among all these -buffers, there is always one which is the current \emph{running - buffer}, whose name is displayed on a green background, which is the -one where Coq commands are currently executed. +buffers, there is always one which is the current +\emph{running buffer}, whose name is displayed on a background in the +\emph{processed} color (green by default), which is the one where Coq commands +are currently executed. Buffers may be edited as in any text editor, and classical basic editing commands (Copy/Paste, \ldots) are available in the \emph{Edit} @@ -58,12 +59,13 @@ menu. \section{Interactive navigation into \Coq{} scripts} The running buffer is the one where navigation takes place. The -toolbar proposes five basic commands for this. The first one, +toolbar offers five basic navigation commands. The first one, represented by a down arrow icon, is for going forward executing one command. If that command is successful, the part of the script that -has been executed is displayed on a green background. If that command -fails, the error message is displayed in the message window, and the -location of the error is emphasized by a red underline. +has been executed is displayed on a background with the +processed color. If that command fails, the error message is +displayed in the message window, and the location of the error is +emphasized by an underline in the error foreground color (red by default). On Figure~\ref{fig:coqide}, the running buffer is \verb|Fermat.v|, all commands until the \verb|Theorem| have been already executed, and the @@ -71,23 +73,41 @@ user tried to go forward executing \verb|Induction n|. That command failed because no such tactic exist (tactics are now in lowercase\ldots), and the wrong word is underlined. -Notice that the green part of the running buffer is not editable. If +Notice that the processed part of the running buffer is not editable. If you ever want to modify something you have to go backward using the up arrow tool, or even better, put the cursor where you want to go back and use the \textsf{goto} button. Unlike with \verb|coqtop|, you should never use \verb|Undo| to go backward. -Two additional tool buttons exist, one to go directly to the end and -one to go back to the beginning. If you try to go to the end, or in -general to run several commands using the \textsf{goto} button, the - execution will stop whenever an error is found. +There are two additional buttons for navigation within the running buffer. +The ``down'' button with a line goes directly to the end; the ``up'' button +with a line goes back to the beginning. The handling of errors when using the +go-to-the-end button depends on whether \Coq{} is running in asynchronous mode or not +(see Chapter~\ref{Asyncprocessing}). If it is not running in that mode, execution stops +as soon as an error is found. Otherwise, execution continues, and the +error is marked with an underline in the error foreground color, with a background in +the error background color (pink by default). The same characterization of +error-handling applies when running several commands using the \textsf{goto} button. If you ever try to execute a command which happens to run during a long time, and would like to abort it before its termination, you may use the interrupt button (the white cross on a red circle). -Finally, notice that these navigation buttons are also available in -the menu, where their keyboard shortcuts are given. +There are other buttons on the \CoqIDE{} toolbar: a button to save the running +buffer; a button to close the current buffer (an ``X''); buttons to switch among +buffers (left and right arrows); an ``information'' button; and a ``gears'' button. + +The ``information'' button is described in Section~\ref{sec:trytactics}. + +The ``gears'' button submits proof terms to the \Coq{} kernel for type-checking. +When \Coq{} uses asynchronous processing (see Chapter~\ref{Asyncprocessing}), proofs may +have been completed without kernel-checking of generated proof terms. The presence of +unchecked proof terms is indicated by \texttt{Qed} statements +that have a subdued \emph{being-processed} color (light blue by default), +rather than the processed color, though their preceding proofs have the processed color. + +Notice that for all these buttons, except for the ``gears'' button, their operations +are also available in the menu, where their keyboard shortcuts are given. \section[Try tactics automatically]{Try tactics automatically\label{sec:trytactics}} @@ -96,8 +116,8 @@ trying to solve the current goal using simple tactics. If such a tactic succeeds in solving the goal, then its text is automatically inserted into the script. There is finally a combination of these tactics, called the \emph{proof wizard} which will try each of them in -turn. This wizard is also available as a tool button (the light -bulb). The set of tactics tried by the wizard is customizable in +turn. This wizard is also available as a tool button (the ``information'' +button). The set of tactics tried by the wizard is customizable in the preferences. These tactics are general ones, in particular they do not refer to @@ -132,7 +152,7 @@ arguments. \begin{figure}[t] \begin{center} -%HEVEA\imgsrc[alt="coqide query window"]{coqide-queries.png} +%HEVEA\imgsrc[alt="coqide query"]{coqide-queries.png} %BEGIN LATEX \ifpdf % si on est en pdflatex \includegraphics[width=1.0\textwidth]{coqide-queries.png} @@ -141,27 +161,21 @@ arguments. \fi %END LATEX \end{center} -\caption{\CoqIDE{}: the query window} -\label{fig:querywindow} +\caption{\CoqIDE{}: a Print query on a selected phrase} +\label{fig:queryselected} \end{figure} - -We call \emph{query} any vernacular command that do not change the -current state, such as \verb|Check|, \verb|Search|, etc. Those -commands are of course useless during compilation of a file, hence -should not be included in scripts. To run such commands without -writing them in the script, \CoqIDE{} offers another input window -called the \emph{query window}. This window can be displayed on -demand, either by using the \texttt{Window} menu, or directly using -shortcuts given in the \texttt{Queries} menu. Indeed, with \CoqIDE{} -the simplest way to perform a \texttt{Search} on some identifier -is to select it using the mouse, and pressing \verb|F2|. This will -both make appear the query window and run the \texttt{Search} in -it, displaying the result. Shortcuts \verb|F3| and \verb|F4| are for -\verb|Check| and \verb|Print| respectively. -Figure~\ref{fig:querywindow} displays the query window after selection -of the word ``mult'' in the script windows, and pressing \verb|F4| to -print its definition. +We call \emph{query} any vernacular command that does not change the +current state, such as \verb|Check|, \verb|Search|, etc. +To run such commands interactively, without writing them in scripts, +\CoqIDE{} offers a \emph{query pane}. +The query pane can be displayed on demand by using the \texttt{View} menu, +or using the shortcut \verb|F1|. Queries can also be performed by +selecting a particular phrase, then choosing an item from the +\texttt{Queries} menu. The response then appears in the message window. +Figure~\ref{fig:queryselected} shows the result after selecting +of the phrase \verb|Nat.mul| in the script window, and choosing \verb|Print| +from the \texttt{Queries} menu. \section{Compilation} diff --git a/doc/refman/RefMan-int.tex b/doc/refman/RefMan-int.tex index 2b9e4e6051..f802a35950 100644 --- a/doc/refman/RefMan-int.tex +++ b/doc/refman/RefMan-int.tex @@ -2,6 +2,7 @@ \setheaders{Introduction} %END LATEX \chapter*{Introduction} +%HEVEA\cutname{introduction.html} This document is the Reference Manual of version \coqversion{} of the \Coq\ proof assistant. A companion volume, the \Coq\ Tutorial, is provided diff --git a/doc/refman/RefMan-lib.tex b/doc/refman/RefMan-lib.tex index 4ebb484e7c..89f5be8438 100644 --- a/doc/refman/RefMan-lib.tex +++ b/doc/refman/RefMan-lib.tex @@ -1,4 +1,5 @@ \chapter[The {\Coq} library]{The {\Coq} library\index{Theories}\label{Theories}} +%HEVEA\cutname{stdlib.html} The \Coq\ library is structured into two parts: @@ -54,6 +55,7 @@ Figure~\ref{init-notations}. \hline Notation & Precedence & Associativity \\ \hline +\verb!_ -> _! & 99 & right \\ \verb!_ <-> _! & 95 & no \\ \verb!_ \/ _! & 85 & right \\ \verb!_ /\ _! & 80 & right \\ diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex index 3ce1d4ecd8..c4c0435c5f 100644 --- a/doc/refman/RefMan-ltac.tex +++ b/doc/refman/RefMan-ltac.tex @@ -1,4 +1,5 @@ \chapter[The tactic language]{The tactic language\label{TacticLanguage}} +%HEVEA\cutname{ltac.html} %\geometry{a4paper,body={5in,8in}} @@ -197,8 +198,6 @@ is understood as {\cpattern} {\tt =>} {\tacexpr}\\ & $|$ & {\tt context} {\zeroone{\ident}} {\tt [} {\cpattern} {\tt ]} {\tt =>} {\tacexpr}\\ -& $|$ & {\tt appcontext} {\zeroone{\ident}} {\tt [} {\cpattern} {\tt ]} - {\tt =>} {\tacexpr}\\ & $|$ & {\tt \_ =>} {\tacexpr}\\ \\ {\it test} & ::= & @@ -310,10 +309,11 @@ A sequence is an expression of the following form: \begin{quote} {\tacexpr}$_1$ {\tt ;} {\tacexpr}$_2$ \end{quote} -The expressions {\tacexpr}$_1$ and {\tacexpr}$_2$ are evaluated -to $v_1$ and $v_2$ which have to be tactic values. The tactic $v_1$ is -then applied and $v_2$ is applied to the goals generated by the -application of $v_1$. Sequence is left-associative. +The expression {\tacexpr}$_1$ is evaluated to $v_1$, which must be +a tactic value. The tactic $v_1$ is applied to the current goal, +possibly producing more goals. Then {\tacexpr}$_2$ is evaluated to +produce $v_2$, which must be a tactic value. The tactic $v_2$ is applied to +all the goals produced by the prior application. Sequence is associative. \subsubsection[Local application of tactics]{Local application of tactics\tacindex{[>\ldots$\mid$\ldots$\mid$\ldots]}\tacindex{;[\ldots$\mid$\ldots$\mid$\ldots]}\index{Tacticals![> \mid ]@{\tt {\tac$_0$};[{\tac$_1$}$\mid$\ldots$\mid$\tac$_n$]}}\index{Tacticals!; [ \mid ]@{\tt {\tac$_0$};[{\tac$_1$}$\mid$\ldots$\mid$\tac$_n$]}}} %\tacindex{; [ | ]} @@ -546,7 +546,7 @@ Yet another way of branching without backtracking is the following structure: $v_2$ which must be tactic values. The tactic value $v_1$ is applied in each subgoal independently and if it fails \emph{to progress} then $v_2$ is applied. {\tacexpr}$_1$ {\tt ||} {\tacexpr}$_2$ is equivalent to {\tt - first [} {\tt progress} {\tacexpr}$_1$ {\tt |} {\tt progress} + first [} {\tt progress} {\tacexpr}$_1$ {\tt |} {\tacexpr}$_2$ {\tt ]} (except that if it fails, it fails like $v_2$). Branching is left-associative. @@ -560,7 +560,7 @@ The tactic is a generalization of the biased-branching tactics above. The expression {\tacexpr}$_1$ is evaluated to $v_1$, which is then applied to each subgoal independently. For each goal where $v_1$ succeeds at -least once, {tacexpr}$_2$ is evaluated to $v_2$ which is then applied +least once, {\tacexpr}$_2$ is evaluated to $v_2$ which is then applied collectively to the generated subgoals. The $v_2$ tactic can trigger backtracking points in $v_1$: where $v_1$ succeeds at least once, {\tt tryif {\tacexpr}$_1$ then {\tacexpr}$_2$ else {\tacexpr}$_3$} is @@ -709,6 +709,55 @@ runs is displayed. Time is in seconds and is machine-dependent. The {\qstring} argument is optional. When provided, it is used to identify this particular occurrence of {\tt time}. +\subsubsection{Timing a tactic that evaluates to a term\tacindex{time\_constr}\tacindex{restart\_timer}\tacindex{finish\_timing} +\index{Tacticals!time\_constr@{\tt time\_constr}}} +\index{Tacticals!restart\_timer@{\tt restart\_timer}} +\index{Tacticals!finish\_timing@{\tt finish\_timing}} + +Tactic expressions that produce terms can be timed with the experimental tactic +\begin{quote} + {\tt time\_constr} {\tacexpr} +\end{quote} +which evaluates {\tacexpr\tt{ ()}} +and displays the time the tactic expression evaluated, assuming successful evaluation. +Time is in seconds and is machine-dependent. + +This tactic currently does not support nesting, and will report times based on the innermost execution. +This is due to the fact that it is implemented using the tactics +\begin{quote} + {\tt restart\_timer} {\qstring} +\end{quote} +and +\begin{quote} + {\tt finish\_timing} ({\qstring}) {\qstring} +\end{quote} +which (re)set and display an optionally named timer, respectively. +The parenthesized {\qstring} argument to {\tt finish\_timing} is also +optional, and determines the label associated with the timer for +printing. + +By copying the definition of {\tt time\_constr} from the standard +library, users can achive support for a fixed pattern of nesting by +passing different {\qstring} parameters to {\tt restart\_timer} and +{\tt finish\_timing} at each level of nesting. For example: + +\begin{coq_example} +Ltac time_constr1 tac := + let eval_early := match goal with _ => restart_timer "(depth 1)" end in + let ret := tac () in + let eval_early := match goal with _ => finish_timing ( "Tactic evaluation" ) "(depth 1)" end in + ret. + +Goal True. + let v := time_constr + ltac:(fun _ => + let x := time_constr1 ltac:(fun _ => constr:(10 * 10)) in + let y := time_constr1 ltac:(fun _ => eval compute in x) in + y) in + pose v. +Abort. +\end{coq_example} + \subsubsection[Local definitions]{Local definitions\index{Ltac!let@\texttt{let}} \index{Ltac!let rec@\texttt{let rec}} \index{let@\texttt{let}!in Ltac} @@ -874,21 +923,6 @@ Goal True. f (3+4). \end{coq_example} -\item \index{appcontext@\texttt{appcontext}!in pattern} - \optindex{Tactic Compat Context} -For historical reasons, {\tt context} used to consider $n$-ary applications -such as {\tt (f 1 2)} as a whole, and not as a sequence of unary -applications {\tt ((f 1) 2)}. Hence {\tt context [f ?x]} would fail -to find a matching subterm in {\tt (f 1 2)}: if the pattern was a partial -application, the matched subterms would have necessarily been -applications with exactly the same number of arguments. -As a workaround, one could use the following variant of {\tt context}: -\begin{quote} -{\tt appcontext} {\ident} {\tt [} {\cpattern} {\tt ]} -\end{quote} -This syntax is now deprecated, as {\tt context} behaves as intended. The former -behavior can be retrieved with the {\tt Tactic Compat Context} flag. - \end{Variants} \subsubsection[Pattern matching on goals]{Pattern matching on goals\index{Ltac!match goal@\texttt{match goal}}\label{ltac-match-goal} @@ -1105,19 +1139,14 @@ Fail all:let n:= numgoals in guard n=2. Reset Initial. \end{coq_eval} -\subsubsection[Proving a subgoal as a separate lemma]{Proving a subgoal as a separate lemma\tacindex{abstract}\tacindex{transparent\_abstract}\comindex{Qed exporting} +\subsubsection[Proving a subgoal as a separate lemma]{Proving a subgoal as a separate lemma\tacindex{abstract}\tacindex{transparent\_abstract} \index{Tacticals!abstract@{\tt abstract}}\index{Tacticals!transparent\_abstract@{\tt transparent\_abstract}}} From the outside ``\texttt{abstract \tacexpr}'' is the same as {\tt solve \tacexpr}. Internally 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. -Such auxiliary lemma is inlined in the final proof term -unless the proof is ended with ``\texttt{Qed exporting}''. In such -case the lemma is preserved. The syntax -``\texttt{Qed exporting }\ident$_1$\texttt{, ..., }\ident$_n$'' -is also supported. In such case the system checks that the names given by the -user actually exist when the proof is ended. +Such an auxiliary lemma is inlined in the final proof term. This tactical is useful with tactics such as \texttt{omega} or \texttt{discriminate} that generate huge proof terms. With that tool @@ -1378,10 +1407,35 @@ The following two tactics behave like {\tt idtac} but enable and disable the pro {\tt stop ltac profiling}. \end{quote} +\tacindex{reset ltac profile}\tacindex{show ltac profile} +The following tactics behave like the corresponding vernacular commands and allow displaying and resetting the profile from tactic scripts for benchmarking purposes. + +\begin{quote} +{\tt reset ltac profile}. +\end{quote} + +\begin{quote} +{\tt show ltac profile}. +\end{quote} + +\begin{quote} +{\tt show ltac profile} {\qstring}. +\end{quote} + You can also pass the {\tt -profile-ltac} command line option to {\tt coqc}, which performs a {\tt Set Ltac Profiling} at the beginning of each document, and a {\tt Show Ltac Profile} at the end. Note that the profiler currently does not handle backtracking into multi-success tactics, and issues a warning to this effect in many cases when such backtracking occurs. +\subsection[Run-time optimization tactic]{Run-time optimization tactic\label{tactic-optimizeheap}}. + +The following tactic behaves like {\tt idtac}, and running it compacts the heap in the +OCaml run-time system. It is analogous to the Vernacular command {\tt Optimize Heap} (see~\ref{vernac-optimizeheap}). + +\tacindex{optimize\_heap} +\begin{quote} +{\tt optimize\_heap}. +\end{quote} + \endinput \subsection{Permutation on closed lists} diff --git a/doc/refman/RefMan-mod.tex b/doc/refman/RefMan-mod.tex index e56c8fa7fe..b4e270e6c3 100644 --- a/doc/refman/RefMan-mod.tex +++ b/doc/refman/RefMan-mod.tex @@ -403,10 +403,14 @@ Fail Check B.T. \end{Warnings} \subsection{\tt Print Module {\ident} -\comindex{Print Module}} +\comindex{Print Module} \optindex{Short Module Printing}} Prints the module type and (optionally) the body of the module {\ident}. +For this command and {\tt Print Module Type}, the option {\tt Short + Module Printing} (off by default) disables the printing of the types of fields, +leaving only their names. + \subsection{\tt Print Module Type {\ident} \comindex{Print Module Type}} diff --git a/doc/refman/RefMan-modr.tex b/doc/refman/RefMan-modr.tex index 2019a529fe..7c672cf422 100644 --- a/doc/refman/RefMan-modr.tex +++ b/doc/refman/RefMan-modr.tex @@ -1,4 +1,5 @@ \chapter[The Module System]{The Module System\label{chapter:Modules}} +%HEVEA\cutname{modules.html} The module system extends the Calculus of Inductive Constructions providing a convenient way to structure large developments as well as diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex index 8f43ebcfbc..1cd23c9297 100644 --- a/doc/refman/RefMan-oth.tex +++ b/doc/refman/RefMan-oth.tex @@ -1,5 +1,6 @@ \chapter[Vernacular commands]{Vernacular commands\label{Vernacular-commands} \label{Other-commands}} +%HEVEA\cutname{vernacular.html} \section{Displaying} @@ -9,6 +10,8 @@ defined object referred by {\qualid}. \begin{ErrMsgs} \item {\qualid} \errindex{not a defined object} +\item \errindex{Universe instance should have length} $n$. +\item \errindex{This object does not support universe names.} \end{ErrMsgs} \begin{Variants} @@ -26,6 +29,11 @@ constructor, abbreviation, \ldots), long name, type, implicit arguments and argument scopes. It does not print the body of definitions or proofs. +\item {\tt Print {\qualid}@\{names\}.}\\ +This locally renames the polymorphic universes of {\qualid}. +An underscore means the raw universe is printed. +This form can be used with {\tt Print Term} and {\tt About}. + %\item {\tt Print Proof {\qualid}.}\comindex{Print Proof}\\ %In case \qualid\ denotes an opaque theorem defined in a section, %it is stored on a special unprintable form and displayed as @@ -904,6 +912,15 @@ This command turns off the use of a default timeout. This command displays whether some default timeout has be set or not. +\subsection[\tt Fail \textrm{\textsl{command-or-tactic}}.]{\tt Fail \textrm{\textsl{command-or-tactic}}.\comindex{Fail}\label{Fail}} + +For debugging {\Coq} scripts, sometimes it is desirable to know +whether a command or a tactic fails. If the given command or tactic +fails, the {\tt Fail} statement succeeds, without changing the proof +state, and in interactive mode, {\Coq} prints a message confirming the failure. +If the command or tactic succeeds, the statement is an error, and +{\Coq} prints a message indicating that the failure did not occur. + \section{Controlling display} \subsection[\tt Set Silent.]{\tt Set Silent.\optindex{Silent} diff --git a/doc/refman/RefMan-pre.tex b/doc/refman/RefMan-pre.tex index 0c2a18eb2e..05775bfbe5 100644 --- a/doc/refman/RefMan-pre.tex +++ b/doc/refman/RefMan-pre.tex @@ -2,6 +2,7 @@ \setheaders{Credits} %END LATEX \chapter*{Credits} +%HEVEA\cutname{credits.html} %\addcontentsline{toc}{section}{Credits} \Coq{}~ is a proof assistant for higher-order logic, allowing the @@ -498,7 +499,7 @@ Claude Marché coordinated the edition of the Reference Manual for Pierre Letouzey and Jacek Chrz\k{a}szcz respectively maintained the extraction tool and module system of {\Coq}. -Jean-Christophe Filliâtre, Pierre Letouzey, Hugo Herbelin ando +Jean-Christophe Filliâtre, Pierre Letouzey, Hugo Herbelin and other contributors from Sophia-Antipolis and Nijmegen participated to the extension of the library. @@ -658,7 +659,7 @@ Matthieu Sozeau extended the \textsc{Russell} language, ending in an convenient way to write programs of given specifications, Pierre Corbineau extended the Mathematical Proof Language and the automatization tools that accompany it, Pierre Letouzey supervised and -extended various parts the standard library, Stéphane Glondu +extended various parts of the standard library, Stéphane Glondu contributed a few tactics and improvements, Jean-Marc Notin provided help in debugging, general maintenance and {\tt coqdoc} support, Vincent Siles contributed extensions of the {\tt Scheme} command and @@ -679,7 +680,7 @@ Nicolas Tabareau made the adaptation of the interface of the old the interaction between Coq and its external interfaces. With Samuel Mimram, he also helped making Coq compatible with recent software tools. Russell O'Connor, Cezary Kaliscyk, Milad Niqui contributed to -improved the libraries of integers, rational, and real numbers. We +improve the libraries of integers, rational, and real numbers. We also thank many users and partners for suggestions and feedback, in particular Pierre Castéran and Arthur Charguéraud, the INRIA Marelle team, Georges Gonthier and the INRIA-Microsoft Mathematical Components team, @@ -713,7 +714,7 @@ implementation of $\mathbb{N}$, $\mathbb{Z}$ or $\mathbb{Z}/n\mathbb{Z}$. The main other evolutions of the library are due to Hugo Herbelin who -made a revision of the sorting library (includingh a certified +made a revision of the sorting library (including a certified merge-sort) and to Guillaume Melquiond who slightly revised and cleaned up the library of reals. @@ -722,7 +723,7 @@ some efficiency issues and a more flexible construction of module types, Élie Soubiran brought a new model of name equivalence, the $\Delta$-equivalence, which respects as much as possible the names given by the users. He also designed with Pierre Letouzey a new -convenient operator \verb!<+! for nesting functor application, what +convenient operator \verb!<+! for nesting functor application, that provides a light notation for inheriting the properties of cascading modules. diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex index eb59ca584e..6b24fdde79 100644 --- a/doc/refman/RefMan-pro.tex +++ b/doc/refman/RefMan-pro.tex @@ -1,5 +1,6 @@ \chapter[Proof handling]{Proof handling\index{Proof editing} \label{Proof-handling}} +%HEVEA\cutname{proof-handling.html} In \Coq's proof editing mode all top-level commands documented in Chapter~\ref{Vernacular-commands} remain available @@ -319,10 +320,19 @@ Note that when a focused goal is proved a message is displayed together with a suggestion about the right bullet or {\tt \}} to unfocus it or focus the next one. +\begin{Variants} + +\item {\tt {\num}: \{}\\ +This focuses on the $\num^{th}$ subgoal to prove. + +\end{Variants} + \begin{ErrMsgs} \item \errindex{This proof is focused, but cannot be unfocused this way} You are trying to use {\tt \}} but the current subproof has not been fully solved. +\item \errindex{No such goal} +\item \errindex{Brackets only support the single numbered goal selector} \item see also error message about bullets below. \end{ErrMsgs} @@ -394,6 +404,8 @@ Proof. \end{ErrMsgs} +\subsection[\tt Set Bullet Behavior.]{\tt Set Bullet Behavior.\optindex{Bullet Behavior}} + The bullet behavior can be controlled by the following commands. \begin{quote} @@ -552,12 +564,12 @@ used to force Coq to optimize some of its internal data structures. This command forces Coq to shrink the data structure used to represent the ongoing proof. -\subsection[\tt Optimize Heap.]{\tt Optimize Heap.} +\subsection[\tt Optimize Heap.]{\tt Optimize Heap.\label{vernac-optimizeheap}} This command forces the OCaml runtime to perform a heap compaction. -This is in general an expensive operation. See: - \url{http://caml.inria.fr/pub/docs/manual-ocaml/libref/Gc.html#VALcompact} - +This is in general an expensive operation. See: \\ +\ \url{http://caml.inria.fr/pub/docs/manual-ocaml/libref/Gc.html#VALcompact} \\ +There is also an analogous tactic {\tt optimize\_heap} (see~\ref{tactic-optimizeheap}). %%% Local Variables: %%% mode: latex diff --git a/doc/refman/RefMan-sch.tex b/doc/refman/RefMan-sch.tex index 23a1c9b029..30724759d2 100644 --- a/doc/refman/RefMan-sch.tex +++ b/doc/refman/RefMan-sch.tex @@ -1,4 +1,5 @@ \chapter{Proof schemes} +%HEVEA\cutname{schemes.html} \section{Generation of induction principles with {\tt Scheme}} \label{Scheme} @@ -126,8 +127,10 @@ conclusion is {\tt (n:nat)(even n)->(Q n)}. \optindex{Boolean Equality Schemes} \optindex{Elimination Schemes} \optindex{Nonrecursive Elimination Schemes} +\optindex{Record Elimination Schemes} \optindex{Case Analysis Schemes} \optindex{Decidable Equality Schemes} +\optindex{Rewriting Schemes} \label{set-nonrecursive-elimination-schemes} } @@ -141,6 +144,7 @@ and {\tt Record} (see~\ref{Record}) do not have an automatic declaration of the induction principles. It can be activated with the command {\tt Set Nonrecursive Elimination Schemes}. It can be deactivated again with {\tt Unset Nonrecursive Elimination Schemes}. +{\tt Record Elimination Schemes} is a deprecated alias of {\tt Nonrecursive Elimination Schemes}. In addition, the {\tt Case Analysis Schemes} flag governs the generation of case analysis lemmas for inductive types, i.e. corresponding to the @@ -155,6 +159,9 @@ However you have to be careful with this option since \Coq~ may now reject well-defined inductive types because it cannot compute a Boolean equality for them. +The {\tt Rewriting Schemes} flag governs generation of equality +related schemes such as congruence. + \subsection{\tt Combined Scheme} \label{CombinedScheme} \comindex{Combined Scheme} diff --git a/doc/refman/RefMan-ssr.tex b/doc/refman/RefMan-ssr.tex index 61f7421c44..31dabcdd4e 100644 --- a/doc/refman/RefMan-ssr.tex +++ b/doc/refman/RefMan-ssr.tex @@ -1,4 +1,5 @@ \achapter{The SSReflect proof language} +%HEVEA\cutname{ssreflect.html} \aauthor{Georges Gonthier, Assia Mahboubi, Enrico Tassi} \newcommand{\ssr}{{\sc SSReflect}} @@ -42,7 +43,7 @@ Proofs written in \ssr{} typically look quite different from the ones written using only tactics as per Chapter~\ref{Tactics}. We try to summarise here the most ``visible'' ones in order to help the reader already accustomed to the tactics described in -Chapter~\ref{Tactics}to read this chapter. +Chapter~\ref{Tactics} to read this chapter. The first difference between the tactics described in this chapter and the tactics described in Chapter~\ref{Tactics} is the way @@ -79,19 +80,19 @@ expansion and partial evaluation participate all to a same concept of rewriting a goal in a larger sense. As such, all these functionalities are provided by the \ssrC{rewrite} tactic. -\ssrC{} includes a little language of patterns to select subterms in tactics +\ssr{} includes a little language of patterns to select subterms in tactics or tacticals where it matters. Its most notable application is in the \ssrC{rewrite} tactic, where patterns are used to specify where the rewriting step has to take place. -Finally, \ssr{} supports the so-called reflection steps, typically +Finally, \ssr{} supports so-called reflection steps, typically allowing to switch back and forth between the computational view and logical view of a concept. To conclude it is worth mentioning that \ssr{} tactics can be mixed with non \ssr{} tactics in the same proof, -or in the same LTac expression. The few exceptions -to this statement are described in section~\label{sec:compat}. +or in the same Ltac expression. The few exceptions +to this statement are described in section~\ref{sec:compat}. \iffalse %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @@ -130,7 +131,7 @@ ProofGeneral provided in the distribution: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \subsection*{Acknowledgments} -The authors would like to thank Fr\'ed\'eric Blanqui, Fran\,cois Pottier +The authors would like to thank Frédéric Blanqui, François Pottier and Laurence Rideau for their comments and suggestions. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @@ -3095,10 +3096,10 @@ the tactic \ssrC{rewrite (=~ multi1)} is equivalent to \end{lstlisting} except that the constants \ssrC{eqba, eqab, mult1_rev} have not been created. -Rewriting with multirules -is useful to implement simplification or transformation -procedures, to be applied on terms of small to medium size. For -instance the library \ssrL{ssrnat} provides two implementations for +Rewriting with multirules is useful to implement simplification or +transformation procedures, to be applied on terms of small to medium +size. For instance, the library \ssrL{ssrnat} --- available in the +external math-comp library --- provides two implementations for arithmetic operations on natural numbers: an elementary one and a tail recursive version, less inefficient but also less convenient for reasoning purposes. The library also provides one lemma per such diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex index d8a353300f..836753db16 100644 --- a/doc/refman/RefMan-syn.tex +++ b/doc/refman/RefMan-syn.tex @@ -1,26 +1,34 @@ \chapter[Syntax extensions and interpretation scopes]{Syntax extensions and interpretation scopes\label{Addoc-syntax}} +%HEVEA\cutname{syntax-extensions.html} In this chapter, we introduce advanced commands to modify the way {\Coq} parses and prints objects, i.e. the translations between the -concrete and internal representations of terms and commands. The main -commands are {\tt Notation} and {\tt Infix} which are described in -section \ref{Notation}. It also happens that the same symbolic -notation is expected in different contexts. To achieve this form of -overloading, {\Coq} offers a notion of interpretation scope. This is -described in Section~\ref{scopes}. - -\Rem The commands {\tt Grammar}, {\tt Syntax} and {\tt Distfix} which -were present for a while in {\Coq} are no longer available from {\Coq} -version 8.0. The underlying AST structure is also no longer available. -The functionalities of the command {\tt Syntactic Definition} are -still available; see Section~\ref{Abbreviations}. +concrete and internal representations of terms and commands. + +The main commands to provide custom symbolic notations for terms are +{\tt Notation} and {\tt Infix}. They are described in Section +\ref{Notation}. There is also a variant of {\tt Notation} which does +not modify the parser. This provides with a form of abbreviation and +it is described in Section~\ref{Abbreviations}. It is sometimes +expected that the same symbolic notation has different meanings in +different contexts. To achieve this form of overloading, {\Coq} offers +a notion of interpretation scope. This is described in +Section~\ref{scopes}. + +The main command to provide custom notations for tactics is {\tt + Tactic Notation}. It is described in Section~\ref{Tactic-Notation}. + +% No need any more to remind this +%% \Rem The commands {\tt Grammar}, {\tt Syntax} and {\tt Distfix} which +%% were present for a while in {\Coq} are no longer available from {\Coq} +%% version 8.0. The underlying AST structure is also no longer available. \section[Notations]{Notations\label{Notation} \comindex{Notation}} \subsection{Basic notations} -A {\em notation} is a symbolic abbreviation denoting some term +A {\em notation} is a symbolic expression denoting some term or term pattern. A typical notation is the use of the infix symbol \verb=/\= to denote @@ -36,7 +44,7 @@ string \verb="A /\ B"= (called a {\em notation}) tells how it is symbolically written. A notation is always surrounded by double quotes (except when the -abbreviation is a single identifier; see \ref{Abbreviations}). The +abbreviation has the form of an ordinary applicative expression; see \ref{Abbreviations}). The notation is composed of {\em tokens} separated by spaces. Identifiers in the string (such as \texttt{A} and \texttt{B}) are the {\em parameters} of the notation. They must occur at least once each in the @@ -60,7 +68,7 @@ syntactic expression (see \ref{ReservedNotation}), explicit precedences and associativity rules have to be given. \Rem The right-hand side of a notation is interpreted at the time the -notation is given. In particular, implicit arguments (see +notation is given. In particular, disambiguation of constants, implicit arguments (see Section~\ref{Implicit Arguments}), coercions (see Section~\ref{Coercions}), etc. are resolved at the time of the declaration of the notation. @@ -104,8 +112,8 @@ parentheses are mandatory (this is a ``no associativity'')\footnote{ which {\Coq} is built, namely {\camlpppp}, currently does not implement the no-associativity and replaces it by a left associativity; hence it is the same for {\Coq}: no-associativity is in fact left associativity}. -We don't know of a special convention of the associativity of -disjunction and conjunction, so let's apply for instance a right +We do not know of a special convention of the associativity of +disjunction and conjunction, so let us apply for instance a right associativity (which is the choice of {\Coq}). Precedence levels and associativity rules of notations have to be @@ -141,7 +149,8 @@ Notation "x = y" := (@eq _ x y) (at level 70, no associativity). \end{coq_example*} One can define {\em closed} notations whose both sides are symbols. In -this case, the default precedence level for inner subexpression is 200. +this case, the default precedence level for inner subexpression is +200, and the default level for the notation itself is 0. \begin{coq_eval} Set Printing Depth 50. @@ -149,7 +158,7 @@ Set Printing Depth 50. (**** an incompatibility with the reserved notation ********) \end{coq_eval} \begin{coq_example*} -Notation "( x , y )" := (@pair _ _ x y) (at level 0). +Notation "( x , y )" := (@pair _ _ x y). \end{coq_example*} One can also define notations for binders. @@ -160,17 +169,17 @@ Set Printing Depth 50. (**** an incompatibility with the reserved notation ********) \end{coq_eval} \begin{coq_example*} -Notation "{ x : A | P }" := (sig A (fun x => P)) (at level 0). +Notation "{ x : A | P }" := (sig A (fun x => P)). \end{coq_example*} In the last case though, there is a conflict with the notation for -type casts. This last notation, as shown by the command {\tt Print Grammar +type casts. The notation for type casts, as shown by the command {\tt Print Grammar constr} is at level 100. To avoid \verb=x : A= being parsed as a type cast, it is necessary to put {\tt x} at a level below 100, typically 99. Hence, a -correct definition is +correct definition is the following. \begin{coq_example*} -Notation "{ x : A | P }" := (sig A (fun x => P)) (at level 0, x at level 99). +Notation "{ x : A | P }" := (sig A (fun x => P)) (x at level 99). \end{coq_example*} %This change has retrospectively an effect on the notation for notation @@ -181,14 +190,17 @@ Notation "{ x : A | P }" := (sig A (fun x => P)) (at level 0, x at level 99). %Notation "{ A } + { B }" := (sumbool A B) (at level 0, A at level 99). %\end{coq_example*} -See the next section for more about factorization. +More generally, it is required that notations are explicitly +factorized on the left. See the next section for more about +factorization. \subsection{Simple factorization rules} -{\Coq} extensible parsing is performed by Camlp5 which is essentially a -LL1 parser. Hence, some care has to be taken not to hide already -existing rules by new rules. Some simple left factorization work has -to be done. Here is an example. +{\Coq} extensible parsing is performed by {\camlpppp} which is +essentially a LL1 parser: it decides which notation to parse by +looking tokens from left to right. Hence, some care has to be taken +not to hide already existing rules by new rules. Some simple left +factorization work has to be done. Here is an example. \begin{coq_eval} (********** The next rule for notation _ < _ < _ produces **********) @@ -241,17 +253,19 @@ on the {\Coq} printer. For example: Check (and True True). \end{coq_example} -However, printing, especially pretty-printing, requires -more care than parsing. We may want specific indentations, -line breaks, alignment if on several lines, etc. +However, printing, especially pretty-printing, also requires some +care. We may want specific indentations, line breaks, alignment if on +several lines, etc. For pretty-printing, {\Coq} relies on {\ocaml} +formatting library, which provides indentation and automatic line +breaks depending on page width by means of {\em formatting boxes}. -The default printing of notations is very rudimentary. For printing a -notation, a {\em formatting box} is opened in such a way that if the +The default printing of notations is rudimentary. For printing a +notation, a formatting box is opened in such a way that if the notation and its arguments cannot fit on a single line, a line break is inserted before the symbols of the notation and the arguments on the next lines are aligned with the argument on the first line. -A first, simple control that a user can have on the printing of a +A first simple control that a user can have on the printing of a notation is the insertion of spaces at some places of the notation. This is performed by adding extra spaces between the symbols and parameters: each extra space (other than the single space needed @@ -276,6 +290,13 @@ Notation "'If' c1 'then' c2 'else' c3" := (IF_then_else c1 c2 c3) \end{coq_example} \end{small} +\begin{coq_example} +Check + (IF_then_else (IF_then_else True False True) + (IF_then_else True False True) + (IF_then_else True False True)). +\end{coq_example} + A {\em format} is an extension of the string denoting the notation with the possible following elements delimited by single quotes: @@ -312,22 +333,15 @@ Notations do not survive the end of sections. No typing of the denoted expression is performed at definition time. Type-checking is done only at the time of use of the notation. -\begin{coq_example} -Check - (IF_then_else (IF_then_else True False True) - (IF_then_else True False True) - (IF_then_else True False True)). -\end{coq_example} - \Rem Sometimes, a notation is expected only for the parser. %(e.g. because %the underlying parser of {\Coq}, namely {\camlpppp}, is LL1 and some extra %rules are needed to circumvent the absence of factorization). -To do so, the option {\em only parsing} is allowed in the list of modifiers of +To do so, the option {\tt only parsing} is allowed in the list of modifiers of \texttt{Notation}. -Conversely, the {\em only printing} can be used to declare +Conversely, the {\tt only printing} can be used to declare that a notation should only be used for printing and should not declare a parsing rule. In particular, such notations do not modify the parser. @@ -338,16 +352,16 @@ The \texttt{Infix} command is a shortening for declaring notations of infix symbols. Its syntax is \begin{quote} -\noindent\texttt{Infix "{\symbolentry}" :=} {\qualid} {\tt (} \nelist{\em modifier}{,} {\tt )}. +\noindent\texttt{Infix "{\symbolentry}" :=} {\term} {\tt (} \nelist{\em modifier}{,} {\tt )}. \end{quote} and it is equivalent to \begin{quote} -\noindent\texttt{Notation "x {\symbolentry} y" := ({\qualid} x y) (} \nelist{\em modifier}{,} {\tt )}. +\noindent\texttt{Notation "x {\symbolentry} y" := ({\term} x y) (} \nelist{\em modifier}{,} {\tt )}. \end{quote} -where {\tt x} and {\tt y} are fresh names distinct from {\qualid}. Here is an example. +where {\tt x} and {\tt y} are fresh names. Here is an example. \begin{coq_example*} Infix "/\" := and (at level 80, right associativity). @@ -379,12 +393,14 @@ reserved. Hence their precedence and associativity cannot be changed. \comindex{CoFixpoint {\ldots} where {\ldots}} \comindex{Inductive {\ldots} where {\ldots}}} -Thanks to reserved notations, the inductive, co-inductive, recursive -and corecursive definitions can benefit of customized notations. To do -this, insert a {\tt where} notation clause after the definition of the -(co)inductive type or (co)recursive term (or after the definition of -each of them in case of mutual definitions). The exact syntax is given -on Figure~\ref{notation-syntax}. Here are examples: +Thanks to reserved notations, the inductive, co-inductive, record, +recursive and corecursive definitions can benefit of customized +notations. To do this, insert a {\tt where} notation clause after the +definition of the (co)inductive type or (co)recursive term (or after +the definition of each of them in case of mutual definitions). The +exact syntax is given on Figure~\ref{notation-syntax} for inductive, +co-inductive, recursive and corecursive definitions and on +Figure~\ref{record-syntax} for records. Here are examples: \begin{coq_eval} Set Printing Depth 50. @@ -478,20 +494,28 @@ Locate "exists _ .. _ , _". \\ \\ {\modifiers} - & ::= & \nelist{\ident}{,} {\tt at level} {\naturalnumber} \\ - & $|$ & \nelist{\ident}{,} {\tt at next level} \\ - & $|$ & {\tt at level} {\naturalnumber} \\ - & $|$ & {\tt left associativity} \\ - & $|$ & {\tt right associativity} \\ - & $|$ & {\tt no associativity} \\ + & ::= & {\tt at level} {\naturalnumber} \\ + & $|$ & \nelist{\ident}{,} {\tt at level} {\naturalnumber} \zeroone{\binderinterp}\\ + & $|$ & \nelist{\ident}{,} {\tt at next level} \zeroone{\binderinterp}\\ + & $|$ & {\ident} {\binderinterp} \\ & $|$ & {\ident} {\tt ident} \\ - & $|$ & {\ident} {\tt binder} \\ - & $|$ & {\ident} {\tt closed binder} \\ & $|$ & {\ident} {\tt global} \\ & $|$ & {\ident} {\tt bigint} \\ + & $|$ & {\ident} \zeroone{{\tt strict}} {\tt pattern} \zeroone{{\tt at level} {\naturalnumber}}\\ + & $|$ & {\ident} {\tt binder} \\ + & $|$ & {\ident} {\tt closed binder} \\ + & $|$ & {\tt left associativity} \\ + & $|$ & {\tt right associativity} \\ + & $|$ & {\tt no associativity} \\ & $|$ & {\tt only parsing} \\ & $|$ & {\tt only printing} \\ - & $|$ & {\tt format} {\str} + & $|$ & {\tt format} {\str} \\ +\\ +\\ +{\binderinterp} + & ::= & {\tt as ident} \\ + & $|$ & {\tt as pattern} \\ + & $|$ & {\tt as strict pattern} \\ \end{tabular} \end{centerframe} \end{small} @@ -499,9 +523,93 @@ Locate "exists _ .. _ , _". \label{notation-syntax} \end{figure} -\subsection{Notations and simple binders} +\subsection{Notations and binders} + +Notations can include binders. This section lists +different ways to deal with binders. For further examples, see also +Section~\ref{RecursiveNotationsWithBinders}. + +\subsubsection{Binders bound in the notation and parsed as identifiers} -Notations can be defined for binders as in the example: +Here is the basic example of a notation using a binder: + +\begin{coq_example*} +Notation "'sigma' x : A , B" := (sigT (fun x : A => B)) + (at level 200, x ident, A at level 200, right associativity). +\end{coq_example*} + +The binding variables in the right-hand side that occur as a parameter +of the notation (here {\tt x}) dynamically bind all the occurrences +in their respective binding scope after instantiation of the +parameters of the notation. This means that the term bound to {\tt B} can +refer to the variable name bound to {\tt x} as shown in the following +application of the notation: + +\begin{coq_example} +Check sigma z : nat, z = 0. +\end{coq_example} + +Notice the modifier {\tt x ident} in the declaration of the +notation. It tells to parse {\tt x} as a single identifier. + +\subsubsection{Binders bound in the notation and parsed as patterns} + +In the same way as patterns can be used as binders, as in {\tt fun + '(x,y) => x+y} or {\tt fun '(existT \_ x \_) => x}, notations can be +defined so that any pattern (in the sense of the entry {\pattern} of +Figure~\ref{term-syntax-aux}) can be used in place of the +binder. Here is an example: + +\begin{coq_eval} +Reset Initial. +\end{coq_eval} + +\begin{coq_example*} +Notation "'subset' ' p , P " := (sig (fun p => P)) + (at level 200, p pattern, format "'subset' ' p , P"). +\end{coq_example*} + +\begin{coq_example} +Check subset '(x,y), x+y=0. +\end{coq_example} + +The modifier {\tt p pattern} in the declaration of the notation +tells to parse $p$ as a pattern. Note that a single +variable is both an identifier and a pattern, so, e.g., the following +also works: + +% Note: we rely on the notation of the standard library which does not +% print the expected output, so we hide the output. +\begin{coq_example} +Check subset 'x, x=0. +\end{coq_example} + +If one wants to prevent such a notation to be used for printing when the +pattern is reduced to a single identifier, one has to use instead +the modifier {\tt p strict pattern}. For parsing, however, a {\tt + strict pattern} will continue to include the case of a +variable. Here is an example showing the difference: + +\begin{coq_example*} +Notation "'subset_bis' ' p , P" := (sig (fun p => P)) + (at level 200, p strict pattern). +Notation "'subset_bis' p , P " := (sig (fun p => P)) + (at level 200, p ident). +\end{coq_example*} + +\begin{coq_example} +Check subset_bis 'x, x=0. +\end{coq_example} + +The default level for a {\tt pattern} is 0. One can use a different level by +using {\tt pattern at level} $n$ where the scale is the same as the one for +terms (Figure~\ref{init-notations}). + +\subsubsection{Binders bound in the notation and parsed as terms} + +Sometimes, for the sake of factorization of rules, a binder has to be +parsed as a term. This is typically the case for a notation such as +the following: \begin{coq_eval} Set Printing Depth 50. @@ -509,18 +617,53 @@ Set Printing Depth 50. (**** an incompatibility with the reserved notation ********) \end{coq_eval} \begin{coq_example*} -Notation "{ x : A | P }" := (sig (fun x : A => P)) (at level 0). +Notation "{ x : A | P }" := (sig (fun x : A => P)) + (at level 0, x at level 99 as ident). +\end{coq_example*} + +This is so because the grammar also contains rules starting with +{\tt \{} and followed by a term, such as the rule for the notation + {\tt \{ A \} + \{ B \}} for the constant {\tt + sumbool}~(see Section~\ref{sumbool}). + +Then, in the rule, {\tt x ident} is replaced by {\tt x at level 99 as + ident} meaning that {\tt x} is parsed as a term at level 99 (as done +in the notation for {\tt sumbool}), but that this term has actually to +be an identifier. + +The notation {\tt \{ x | P \}} is already defined in the standard +library with the {\tt as ident} modifier. We cannot redefine it but +one can define an alternative notation, say {\tt \{ p such that P }\}, +using instead {\tt as pattern}. + +% Note, this conflicts with the default rule in the standard library, so +% we don't show the +\begin{coq_example*} +Notation "{ p 'such' 'that' P }" := (sig (fun p => P)) + (at level 0, p at level 99 as pattern). \end{coq_example*} -The binding variables in the left-hand-side that occur as a parameter -of the notation naturally bind all their occurrences appearing in -their respective scope after instantiation of the parameters of the -notation. +Then, the following works: +\begin{coq_example} +Check {(x,y) such that x+y=0}. +\end{coq_example} + +To enforce that the pattern should not be used for printing when it +is just an identifier, one could have said {\tt p at level + 99 as strict pattern}. + +Note also that in the absence of a {\tt as ident}, {\tt as strict + pattern} or {\tt as pattern} modifiers, the default is to consider +subexpressions occurring in binding position and parsed as terms to be +{\tt as ident}. + +\subsubsection{Binders not bound in the notation} +\label{NotationsWithBinders} -Contrastingly, the binding variables that are not a parameter of the -notation do not capture the variables of same name that -could appear in their scope after instantiation of the -notation. E.g., for the notation +We can also have binders in the right-hand side of a notation which +are not themselves bound in the notation. In this case, the binders +are considered up to renaming of the internal binder. E.g., for the +notation \begin{coq_example*} Notation "'exists_different' n" := (exists p:nat, p<>n) (at level 200). @@ -536,14 +679,6 @@ Set Printing Depth 50. Fail Check (exists_different p). \end{coq_example} -\Rem Binding variables must not necessarily be parsed using the -{\tt ident} entry. For factorization purposes, they can be said to be -parsed at another level (e.g. {\tt x} in \verb="{ x : A | P }"= must be -parsed at level 99 to be factorized with the notation -\verb="{ A } + { B }"= for which {\tt A} can be any term). -However, even if parsed as a term, this term must at the end be effectively -a single identifier. - \subsection{Notations with recursive patterns} \label{RecursiveNotations} @@ -564,24 +699,22 @@ notation parses any number of time (but at least one time) a sequence of expressions separated by the sequence of tokens $s$ (in the example, $s$ is just ``{\tt ;}''). -In the right-hand side, the term enclosed within {\tt ..} must be a -pattern with two holes of the form $\phi([~]_E,[~]_I)$ where the first -hole is occupied either by $x$ or by $y$ and the second hole is -occupied by an arbitrary term $t$ called the {\it terminating} -expression of the recursive notation. The subterm {\tt ..} $\phi(x,t)$ -{\tt ..} (or {\tt ..} $\phi(y,t)$ {\tt ..}) must itself occur at -second position of the same pattern where the first hole is occupied -by the other variable, $y$ or $x$. Otherwise said, the right-hand side -must contain a subterm of the form either $\phi(x,${\tt ..} -$\phi(y,t)$ {\tt ..}$)$ or $\phi(y,${\tt ..} $\phi(x,t)$ {\tt ..}$)$. -The pattern $\phi$ is the {\em iterator} of the recursive notation -and, of course, the name $x$ and $y$ can be chosen arbitrarily. - -The parsing phase produces a list of expressions which are used to -fill in order the first hole of the iterating pattern which is +The right-hand side must contain a subterm of the form either +$\phi(x,${\tt ..} $\phi(y,t)$ {\tt ..}$)$ or $\phi(y,${\tt ..} +$\phi(x,t)$ {\tt ..}$)$ where $\phi([~]_E,[~]_I)$, called the {\em + iterator} of the recursive notation is an arbitrary expression with +distinguished placeholders and +where $t$ is called the {\tt terminating expression} of the recursive +notation. In the example, we choose the name s$x$ and $y$ but in +practice they can of course be chosen arbitrarily. Note that the +placeholder $[~]_I$ has to occur only once but the $[~]_E$ can occur +several times. + +Parsing the notation produces a list of expressions which are used to +fill the first placeholder of the iterating pattern which itself is repeatedly nested as many times as the length of the list, the second -hole being the nesting point. In the innermost occurrence of the -nested iterating pattern, the second hole is finally filled with the +placeholder being the nesting point. In the innermost occurrence of the +nested iterating pattern, the second placeholder is finally filled with the terminating expression. In the example above, the iterator $\phi([~]_E,[~]_I)$ is {\tt cons @@ -608,24 +741,26 @@ notations, they can also be declared within interpretation scopes (see section \ref{scopes}). \subsection{Notations with recursive patterns involving binders} +\label{RecursiveNotationsWithBinders} Recursive notations can also be used with binders. The basic example is: \begin{coq_example*} -Notation "'exists' x .. y , p" := (ex (fun x => .. (ex (fun y => p)) ..)) +Notation "'exists' x .. y , p" := + (ex (fun x => .. (ex (fun y => p)) ..)) (at level 200, x binder, y binder, right associativity). \end{coq_example*} The principle is the same as in Section~\ref{RecursiveNotations} -except that in the iterator $\phi([~]_E,[~]_I)$, the first hole is a -placeholder occurring at the position of the binding variable of a {\tt +except that in the iterator $\phi([~]_E,[~]_I)$, the placeholder $[~]_E$ can +also occur in position of the binding variable of a {\tt fun} or a {\tt forall}. To specify that the part ``$x$ {\tt ..} $y$'' of the notation parses a sequence of binders, $x$ and $y$ must be marked as {\tt - binder} in the list of modifiers of the notation. Then, the list of -binders produced at the parsing phase are used to fill in the first -hole of the iterating pattern which is repeatedly nested as many times + binder} in the list of modifiers of the notation. The +binders of the parsed sequence are used to fill the occurrences of the first +placeholder of the iterating pattern which is repeatedly nested as many times as the number of binders generated. If ever the generalization operator {\tt `} (see Section~\ref{implicit-generalization}) is used in the binding list, the added binders are taken into account too. @@ -634,14 +769,14 @@ Binders parsing exist in two flavors. If $x$ and $y$ are marked as {\tt binder}, then a sequence such as {\tt a b c : T} will be accepted and interpreted as the sequence of binders {\tt (a:T) (b:T) (c:T)}. For instance, in the notation above, the syntax {\tt exists - a b : nat, a = b} is provided. + a b : nat, a = b} is valid. The variables $x$ and $y$ can also be marked as {\tt closed binder} in which case only well-bracketed binders of the form {\tt (a b c:T)} or {\tt \{a b c:T\}} etc. are accepted. With closed binders, the recursive sequence in the left-hand side can -be of the general form $x$ $s$ {\tt ..} $s$ $y$ where $s$ is an +be of the more general form $x$ $s$ {\tt ..} $s$ $y$ where $s$ is an arbitrary sequence of tokens. With open binders though, $s$ has to be empty. Here is an example of recursive notation with closed binders: @@ -660,6 +795,40 @@ Notation "'FUNAPP' x .. y , f" := (at level 200, x binder, y binder, right associativity). \end{coq_example*} +If an occurrence of the $[~]_E$ is not in position of a binding +variable but of a term, it is the name used in the binding which is +used. Here is an example: + +\begin{coq_example*} +Notation "'exists_non_null' x .. y , P" := + (ex (fun x => x <> 0 /\ .. (ex (fun y => y <> 0 /\ P)) ..)) + (at level 200, x binder). +\end{coq_example*} + +\subsection{Predefined entries} + +By default, sub-expressions are parsed as terms and the corresponding +grammar entry is called {\tt constr}. However, one may sometimes want +to restrict the syntax of terms in a notation. For instance, the +following notation will accept to parse only global reference in +position of {\tt x}: + +\begin{coq_example*} +Notation "'apply' f a1 .. an" := (.. (f a1) .. an) + (at level 10, f global, a1, an at level 9). +\end{coq_example*} + +In addition to {\tt global}, one can restrict the syntax of a +sub-expression by using the entry names {\tt ident} or {\tt pattern} +already seen in Section~\ref{NotationsWithBinders}, even when the +corresponding expression is not used as a binder in the right-hand +side. E.g.: + +\begin{coq_example*} +Notation "'apply_id' f a1 .. an" := (.. (f a1) .. an) + (at level 10, f ident, a1, an at level 9). +\end{coq_example*} + \subsection{Summary} \paragraph{Syntax of notations} @@ -753,7 +922,7 @@ stack by using the command {\tt Close Scope} {\scope}. \end{quote} Notice that this command does not only cancel the last {\tt Open Scope -{\scope}} but all the invocation of it. +{\scope}} but all the invocations of it. \Rem {\tt Open Scope} and {\tt Close Scope} do not survive the end of sections where they occur. When defined outside of a section, they are @@ -852,6 +1021,14 @@ Arguments scopes can be cleared with the following command: {\tt Arguments {\qualid} : clear scopes} \end{quote} +Extra argument scopes, to be used in case of coercion to Funclass +(see Chapter~\ref{Coercions-full}) or with a computed type, +can be given with + +\begin{quote} +{\tt Arguments} {\qualid} \nelist{\textunderscore {\tt \%} \scope}{} {\tt : extra scopes.} +\end{quote} + \begin{Variants} \item {\tt Global Arguments} {\qualid} \nelist{\name {\tt \%}\scope}{} @@ -1107,7 +1284,7 @@ Check reflexive iff. \end{coq_example} An abbreviation expects no precedence nor associativity, since it -follows the usual syntax of application. Abbreviations are used as +is parsed as usual application. Abbreviations are used as much as possible by the {\Coq} printers unless the modifier \verb=(only parsing)= is given. @@ -1120,7 +1297,7 @@ abbreviation but at the time it is used. Especially, abbreviations can be bound to terms with holes (i.e. with ``\_''). The general syntax for abbreviations is \begin{quote} -\zeroone{{\tt Local}} \texttt{Notation} {\ident} \sequence{\ident} {\ident} \texttt{:=} {\term} +\zeroone{{\tt Local}} \texttt{Notation} {\ident} \sequence{\ident}{} \texttt{:=} {\term} \zeroone{{\tt (only parsing)}}~\verb=.= \end{quote} @@ -1146,13 +1323,15 @@ at the time of use of the abbreviation. %\verb=(only parsing)= is given) while syntactic definitions were not. \section{Tactic Notations +\label{Tactic-Notation} \comindex{Tactic Notation}} Tactic notations allow to customize the syntax of the tactics of the -tactic language\footnote{Tactic notations are just a simplification of -the {\tt Grammar tactic simple\_tactic} command that existed in -versions prior to version 8.0.}. Tactic notations obey the following -syntax +tactic language. +%% \footnote{Tactic notations are just a simplification of +%% the {\tt Grammar tactic simple\_tactic} command that existed in +%% versions prior to version 8.0.} +Tactic notations obey the following syntax: \medskip \noindent @@ -1195,7 +1374,9 @@ level indicates the parsing precedence of the tactic notation. This information is particularly relevant for notations of tacticals. Levels 0 to 5 are available (default is 0). To know the parsing precedences of the -existing tacticals, use the command {\tt Print Grammar tactic.} +existing tacticals, use the command +\comindex{Print Grammar tactic} + {\tt Print Grammar tactic.} Each type of tactic argument has a specific semantic regarding how it is parsed and how it is interpreted. The semantic is described in the diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 6e27357008..66a5f107a5 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -3,6 +3,7 @@ \chapter{Tactics \index{Tactics} \label{Tactics}} +%HEVEA\cutname{tactics.html} A deduction rule is a link between some (unique) formula, that we call the {\em conclusion} and (several) formulas that we call the {\em @@ -3309,7 +3310,7 @@ evaluating purely computational expressions (i.e. with little dead code). fine-tuned. It is specially interesting for full evaluation of algebraic objects. This includes the case of reflection-based tactics. -\item {\tt native\_compute} \tacindex{native\_compute} +\item {\tt native\_compute} \tacindex{native\_compute} \optindex{NativeCompute Profiling} This tactic evaluates the goal by compilation to \ocaml{} as described in \cite{FullReduction}. If \Coq{} is running in native code, it can be typically @@ -3333,6 +3334,14 @@ evaluating purely computational expressions (i.e. with little dead code). \end{Variants} +\Rem The following option makes {\tt cbv} (and its derivative {\tt + compute}) print information about the constants it encounters and +the unfolding decisions it makes. +\begin{quote} + \optindex{Debug Cbv} + {\tt Set Debug Cbv} +\end{quote} + % Obsolete? Anyway not very important message %\begin{ErrMsgs} %\item \errindex{Delta must be specified before} @@ -3506,6 +3515,13 @@ of {\tt cbn} while doing reductions in unification, type inference and tactic applications. It can result in expensive unifications, as refolding currently uses a potentially exponential heuristic. +\begin{quote} + \optindex{Debug RAKAM} + {\tt Set Debug RAKAM} +\end{quote} +This option makes {\tt cbn} print various debugging information. +{\tt RAKAM} is the Refolding Algebraic Krivine Abstract Machine. + \subsection{\tt unfold \qualid} \tacindex{unfold} \label{unfold} @@ -3522,8 +3538,13 @@ with its $\beta\iota$-normal form. \end{ErrMsgs} \begin{Variants} +\item {\tt unfold {\qualid} in {\ident}} + \tacindex{unfold \dots in} + + Replaces {\qualid} in hypothesis {\ident} with its definition + and replaces the hypothesis with its $\beta\iota$ normal form. + \item {\tt unfold {\qualid}$_1$, \dots, \qualid$_n$} - \tacindex{unfold \dots\ in} Replaces {\em simultaneously} {\qualid}$_1$, \dots, {\qualid}$_n$ with their definitions and replaces the current goal with its @@ -3697,6 +3718,9 @@ hints of the database named {\tt core}. This variant is very useful for getting a better understanding of automation, or to know what lemmas/assumptions were used. +\item {\tt debug auto} Behaves like {\tt auto} but shows the tactics + it tries to solve the goal, including failing paths. + \item {\tt \zeroone{info\_}auto \zeroone{\num}} \zeroone{{\tt using} \nterm{lemma}$_1$ {\tt ,} {\ldots} {\tt ,} \nterm{lemma}$_n$} \zeroone{{\tt with} \ident$_1$ {\ldots} \ident$_n$} @@ -3717,6 +3741,8 @@ hints of the database named {\tt core}. \item {\tt info\_trivial} +\item {\tt debug trivial} + \item {\tt \zeroone{info\_}trivial} \zeroone{{\tt using} \nterm{lemma}$_1$ {\tt ,} {\ldots} {\tt ,} \nterm{lemma}$_n$} \zeroone{{\tt with} \ident$_1$ {\ldots} \ident$_n$} @@ -3726,6 +3752,19 @@ hints of the database named {\tt core}. \Rem {\tt auto} either solves completely the goal or else leaves it intact. \texttt{auto} and \texttt{trivial} never fail. +\Rem The following options enable printing of informative or debug +information for the {\tt auto} and {\tt trivial} tactics: +\begin{quote} + \optindex{Info Auto} + {\tt Set Info Auto} + \optindex{Debug Auto} + {\tt Set Debug Auto} + \optindex{Info Trivial} + {\tt Set Info Trivial} + \optindex{Debug Trivial} + {\tt Set Debug Trivial} +\end{quote} + \SeeAlso Section~\ref{Hints-databases} \subsection{\tt eauto} @@ -3762,6 +3801,14 @@ Note that {\tt ex\_intro} should be declared as a hint. \end{Variants} +\Rem {\tt eauto} obeys the following options: +\begin{quote} + \optindex{Info Eauto} + {\tt Set Info Eauto} + \optindex{Debug Eauto} + {\tt Set Debug Eauto} +\end{quote} + \SeeAlso Section~\ref{Hints-databases} \subsection{\tt autounfold with \ident$_1$ \mbox{\dots} \ident$_n$} @@ -3835,6 +3882,26 @@ this tactic. % En attente d'un moyen de valoriser les fichiers de demos %\SeeAlso file \texttt{contrib/Rocq/DEMOS/Demo\_AutoRewrite.v} +\subsection{\tt easy} +\tacindex{easy} +\label{easy} + +This tactic tries to solve the current goal by a number of standard closing steps. +In particular, it tries to close the current goal using the closing tactics +{\tt trivial}, reflexivity, symmetry, contradiction and inversion of hypothesis. +If this fails, it tries introducing variables and splitting and-hypotheses, +using the closing tactics afterwards, and splitting the goal using {\tt split} and recursing. + +This tactic solves goals that belong to many common classes; in particular, many cases of +unsatisfiable hypotheses, and simple equality goals are usually solved by this tactic. + +\begin{Variant} +\item {\tt now \tac} + \tacindex{now} + + Run \tac\/ followed by easy. This is a notation for {\tt \tac; easy}. +\end{Variant} + \section{Controlling automation} \subsection{The hints databases for {\tt auto} and {\tt eauto}} @@ -4684,6 +4751,13 @@ congruence. described above. \end{ErrMsgs} +\noindent {\bf Remark: } {\tt congruence} can be made to print debug +information by setting the following option: + +\begin{quote} +\optindex{Congruence Verbose} +{\tt Set Congruence Verbose} +\end{quote} \section{Checking properties of terms} diff --git a/doc/refman/RefMan-tacex.tex b/doc/refman/RefMan-tacex.tex index cb8f916f13..7cdb1a5274 100644 --- a/doc/refman/RefMan-tacex.tex +++ b/doc/refman/RefMan-tacex.tex @@ -1,4 +1,5 @@ \chapter[Detailed examples of tactics]{Detailed examples of tactics\label{Tactics-examples}} +%HEVEA\cutname{tactic-examples.html} This chapter presents detailed examples of certain tactics, to illustrate their behavior. diff --git a/doc/refman/RefMan-tus.tex b/doc/refman/RefMan-tus.tex deleted file mode 100644 index 7e5bb81a90..0000000000 --- a/doc/refman/RefMan-tus.tex +++ /dev/null @@ -1,2001 +0,0 @@ -%\documentclass[11pt]{article} -%\usepackage{fullpage,euler} -%\usepackage[latin1]{inputenc} -%\begin{document} -%\title{Writing ad-hoc Tactics in Coq} -%\author{} -%\date{} -%\maketitle -%\tableofcontents -%\clearpage - -\chapter[Writing ad-hoc Tactics in Coq]{Writing ad-hoc Tactics in Coq\label{WritingTactics}} - -\section{Introduction} - -\Coq\ is an open proof environment, in the sense that the collection of -proof strategies offered by the system can be extended by the user. -This feature has two important advantages. First, the user can develop -his/her own ad-hoc proof procedures, customizing the system for a -particular domain of application. Second, the repetitive and tedious -aspects of the proofs can be abstracted away implementing new tactics -for dealing with them. For example, this may be useful when a theorem -needs several lemmas which are all proven in a similar but not exactly -the same way. Let us illustrate this with an example. - -Consider the problem of deciding the equality of two booleans. The -theorem establishing that this is always possible is state by -the following theorem: - -\begin{coq_example*} -Theorem decideBool : (x,y:bool){x=y}+{~x=y}. -\end{coq_example*} - -The proof proceeds by case analysis on both $x$ and $y$. This yields -four cases to solve. The cases $x=y=\textsl{true}$ and -$x=y=\textsl{false}$ are immediate by the reflexivity of equality. - -The other two cases follow by discrimination. The following script -describes the proof: - -\begin{coq_example*} -Destruct x. - Destruct y. - Left ; Reflexivity. - Right; Discriminate. - Destruct y. - Right; Discriminate. - Left ; Reflexivity. -\end{coq_example*} -\begin{coq_eval} -Abort. -\end{coq_eval} - -Now, consider the theorem stating the same property but for the -following enumerated type: - -\begin{coq_example*} -Inductive Set Color := Blue:Color | White:Color | Red:Color. -Theorem decideColor : (c1,c2:Color){c1=c2}+{~c1=c2}. -\end{coq_example*} - -This theorem can be proven in a very similar way, reasoning by case -analysis on $c_1$ and $c_2$. Once more, each of the (now six) cases is -solved either by reflexivity or by discrimination: - -\begin{coq_example*} -Destruct c1. - Destruct c2. - Left ; Reflexivity. - Right ; Discriminate. - Right ; Discriminate. - Destruct c2. - Right ; Discriminate. - Left ; Reflexivity. - Right ; Discriminate. - Destruct c2. - Right ; Discriminate. - Right ; Discriminate. - Left ; Reflexivity. -\end{coq_example*} -\begin{coq_eval} -Abort. -\end{coq_eval} - -If we face the same theorem for an enumerated datatype corresponding -to the days of the week, it would still follow a similar pattern. In -general, the general pattern for proving the property -$(x,y:R)\{x=y\}+\{\neg x =y\}$ for an enumerated type $R$ proceeds as -follow: -\begin{enumerate} -\item Analyze the cases for $x$. -\item For each of the sub-goals generated by the first step, analyze -the cases for $y$. -\item The remaining subgoals follow either by reflexivity or -by discrimination. -\end{enumerate} - -Let us describe how this general proof procedure can be introduced in -\Coq. - -\section{Tactic Macros} - -The simplest way to introduce it is to define it as new a -\textsl{tactic macro}, as follows: - -\begin{coq_example*} -Tactic Definition DecideEq [$a $b] := - [<:tactic:<Destruct $a; - Destruct $b; - (Left;Reflexivity) Orelse (Right;Discriminate)>>]. -\end{coq_example*} - -The general pattern of the proof is abstracted away using the -tacticals ``\texttt{;}'' and \texttt{Orelse}, and introducing two -parameters for the names of the arguments to be analyzed. - -Once defined, this tactic can be called like any other tactic, just -supplying the list of terms corresponding to its real arguments. Let us -revisit the proof of the former theorems using the new tactic -\texttt{DecideEq}: - -\begin{coq_example*} -Theorem decideBool : (x,y:bool){x=y}+{~x=y}. -DecideEq x y. -Defined. -\end{coq_example*} -\begin{coq_example*} -Theorem decideColor : (c1,c2:Color){c1=c2}+{~c1=c2}. -DecideEq c1 c2. -Defined. -\end{coq_example*} - -In general, the command \texttt{Tactic Definition} associates a name -to a parameterized tactic expression, built up from the tactics and -tacticals that are already available. The general syntax rule for this -command is the following: - -\begin{tabbing} -\texttt{Tactic Definition} \textit{tactic-name} \= -\texttt{[}\$$id_1\ldots \$id_n$\texttt{]}\\ -\> := \texttt{[<:tactic:<} \textit{tactic-expression} \verb+>>]+ -\end{tabbing} - -This command provides a quick but also very primitive mechanism for -introducing new tactics. It does not support recursive definitions, -and the arguments of a tactic macro are restricted to term -expressions. Moreover, there is no static checking of the definition -other than the syntactical one. Any error in the definition of the -tactic ---for instance, a call to an undefined tactic--- will not be -noticed until the tactic is called. - -%This command provides a very primitive mechanism for introducing new -%tactics. The arguments of a tactic macro are restricted to term -%expressions. Hence, it is not possible to define higher order tactics -%with this command. Also, there is no static checking of the definition -%other than syntactical. If the tactic contain errors in its definition -%--for instance, a call to an undefined tactic-- this will be noticed -%during the tactic call. - -Let us illustrate the weakness of this way of introducing new tactics -trying to extend our proof procedure to work on a larger class of -inductive types. Consider for example the decidability of equality -for pairs of booleans and colors: - -\begin{coq_example*} -Theorem decideBoolXColor : (p1,p2:bool*Color){p1=p2}+{~p1=p2}. -\end{coq_example*} - -The proof still proceeds by a double case analysis, but now the -constructors of the type take two arguments. Therefore, the sub-goals -that can not be solved by discrimination need further considerations -about the equality of such arguments: - -\begin{coq_example} - Destruct p1; - Destruct p2; Try (Right;Discriminate);Intros. -\end{coq_example} - -The half of the disjunction to be chosen depends on whether or not -$b=b_0$ and $c=c_0$. These equalities can be decided automatically -using the previous lemmas about booleans and colors. If both -equalities are satisfied, then it is sufficient to rewrite $b$ into -$b_0$ and $c$ into $c_0$, so that the left half of the goal follows by -reflexivity. Otherwise, the right half follows by first contraposing -the disequality, and then applying the invectiveness of the pairing -constructor. - -As the cases associated to each argument of the pair are very similar, -a tactic macro can be introduced to abstract this part of the proof: - -\begin{coq_example*} -Hints Resolve decideBool decideColor. -Tactic Definition SolveArg [$t1 $t2] := - [<:tactic:< - ElimType {$t1=$t2}+{~$t1=$t2}; - [(Intro equality;Rewrite equality;Clear equality) | - (Intro diseq; Right; Red; Intro absurd; - Apply diseq;Injection absurd;Trivial) | - Auto]>>]. -\end{coq_example*} - -This tactic is applied to each corresponding pair of arguments of the -arguments, until the goal can be solved by reflexivity: - -\begin{coq_example*} -SolveArg b b0; - SolveArg c c0; - Left; Reflexivity. -Defined. -\end{coq_example*} - -Therefore, a more general strategy for deciding the property -$(x,y:R)\{x=y\}+\{\neg x =y\}$ on $R$ can be sketched as follows: -\begin{enumerate} -\item Eliminate $x$ and then $y$. -\item Try discrimination to solve those goals where $x$ and $y$ has -been introduced by different constructors. -\item If $x$ and $y$ have been introduced by the same constructor, -then iterate the tactic \textsl{SolveArg} for each pair of -arguments. -\item Finally, solve the left half of the goal by reflexivity. -\end{enumerate} - -The implementation of this stronger proof strategy needs to perform a -term decomposition, in order to extract the list of arguments of each -constructor. It also requires the introduction of recursively defined -tactics, so that the \textsl{SolveArg} can be iterated on the lists of -arguments. These features are not supported by the \texttt{Tactic -Definition} command. One possibility could be extended this command in -order to introduce recursion, general parameter passing, -pattern-matching, etc, but this would quickly lead us to introduce the -whole \ocaml{} into \Coq\footnote{This is historically true. In fact, -\ocaml{} is a direct descendent of ML, a functional programming language -conceived language for programming the tactics of the theorem prover -LCF.}. Instead of doing this, we prefer to give to the user the -possibility of writing his/her own tactics directly in \ocaml{}, and then -to link them dynamically with \Coq's code. This requires a minimal -knowledge about \Coq's implementation. The next section provides an -overview of \Coq's architecture. - -%It is important to point out that the introduction of a new tactic -%never endangers the correction of the theorems proven in the extended -%system. In order to understand why, let us introduce briefly the system -%architecture. - -\section{An Overview of \Coq's Architecture} - -The implementation of \Coq\ is based on eight \textsl{logical -modules}. By ``module'' we mean here a logical piece of code having a -conceptual unity, that may concern several \ocaml{} files. By the sake of -organization, all the \ocaml{} files concerning a logical module are -grouped altogether into the same sub-directory. The eight modules -are: - -\begin{tabular}{lll} -1. & The logical framework & (directory \texttt{src/generic})\\ -2. & The language of constructions & (directory \texttt{src/constr})\\ -3. & The type-checker & (directory \texttt{src/typing})\\ -4. & The proof engine & (directory \texttt{src/proofs})\\ -5. & The language of basic tactics & (directory \texttt{src/tactics})\\ -6. & The vernacular interpreter & (directory \texttt{src/env})\\ -7. & The parser and the pretty-printer & (directory \texttt{src/parsing})\\ -8. & The standard library & (directory \texttt{src/lib}) -\end{tabular} - -\vspace{1em} - -The following sections briefly present each of the modules above. -This presentation is not intended to be a complete description of \Coq's -implementation, but rather a guideline to be read before taking a look -at the sources. For each of the modules, we also present some of its -most important functions, which are sufficient to implement a large -class of tactics. - - -\subsection[The Logical Framework]{The Logical Framework\label{LogicalFramework}} - -At the very heart of \Coq there is a generic untyped language for -expressing abstractions, applications and global constants. This -language is used as a meta-language for expressing the terms of the -Calculus of Inductive Constructions. General operations on terms like -collecting the free variables of an expression, substituting a term for -a free variable, etc, are expressed in this language. - -The meta-language \texttt{'op term} of terms has seven main -constructors: -\begin{itemize} -\item $(\texttt{VAR}\;id)$, a reference to a global identifier called $id$; -\item $(\texttt{Rel}\;n)$, a bound variable, whose binder is the $nth$ - binder up in the term; -\item $\texttt{DLAM}\;(x,t)$, a de Bruijn's binder on the term $t$; -\item $\texttt{DLAMV}\;(x,vt)$, a de Bruijn's binder on all the terms of - the vector $vt$; -\item $(\texttt{DOP0}\;op)$, a unary operator $op$; -\item $\texttt{DOP2}\;(op,t_1,t_2)$, the application of a binary -operator $op$ to the terms $t_1$ and $t_2$; -\item $\texttt{DOPN} (op,vt)$, the application of an n-ary operator $op$ to the -vector of terms $vt$. -\end{itemize} - -In this meta-language, bound variables are represented using the -so-called de Bruijn's indexes. In this representation, an occurrence of -a bound variable is denoted by an integer, meaning the number of -binders that must be traversed to reach its own -binder\footnote{Actually, $(\texttt{Rel}\;n)$ means that $(n-1)$ binders -have to be traversed, since indexes are represented by strictly -positive integers.}. On the other hand, constants are referred by its -name, as usual. For example, if $A$ is a variable of the current -section, then the lambda abstraction $[x:A]x$ of the Calculus of -Constructions is represented in the meta-language by the term: - -\begin{displaymath} -(DOP2 (Lambda,(Var\;A),DLAM (x,(Rel\;1))) -\end{displaymath} - -In this term, $Lambda$ is a binary operator. Its first argument -correspond to the type $A$ of the bound variable, while the second is -a body of the abstraction, where $x$ is bound. The name $x$ is just kept -to pretty-print the occurrences of the bound variable. - -%Similarly, the product -%$(A:Prop)A$ of the Calculus of Constructions is represented by the -%term: -%\begin{displaumath} -%DOP2 (Prod, DOP0 (Sort (Prop Null)), DLAM (Name \#A, Rel 1)) -%\end{displaymath} - -The following functions perform some of the most frequent operations -on the terms of the meta-language: -\begin{description} -\fun{val Generic.subst1 : 'op term -> 'op term -> 'op term} - {$(\texttt{subst1}\;t_1\;t_2)$ substitutes $t_1$ for - $\texttt{(Rel}\;1)$ in $t_2$.} -\fun{val Generic.occur\_var : identifier -> 'op term -> bool} - {Returns true when the given identifier appears in the term, - and false otherwise.} -\fun{val Generic.eq\_term : 'op term -> 'op term -> bool} - {Implements $\alpha$-equality for terms.} -\fun{val Generic.dependent : 'op term -> 'op term -> bool} - {Returns true if the first term is a sub-term of the second.} -%\fun{val Generic.subst\_var : identifier -> 'op term -> 'op term} -% { $(\texttt{subst\_var}\;id\;t)$ substitutes the de Bruijn's index -% associated to $id$ to every occurrence of the term -% $(\texttt{VAR}\;id)$ in $t$.} -\end{description} - -\subsubsection{Identifiers, names and sections paths.} - -Three different kinds of names are used in the meta-language. They are -all defined in the \ocaml{} file \texttt{Names}. - -\paragraph{Identifiers.} The simplest kind of names are -\textsl{identifiers}. An identifier is a string possibly indexed by an -integer. They are used to represent names that are not unique, like -for example the name of a variable in the scope of a section. The -following operations can be used for handling identifiers: - -\begin{description} -\fun{val Names.make\_ident : string -> int -> identifier} - {The value $(\texttt{make\_ident}\;x\;i)$ creates the - identifier $x_i$. If $i=-1$, then the identifier has - is created with no index at all.} -\fun{val Names.repr\_ident : identifier -> string * int} - {The inverse operation of \texttt{make\_ident}: - it yields the string and the index of the identifier.} -\fun{val Names.lift\_ident : identifier -> identifier} - {Increases the index of the identifier by one.} -\fun{val Names.next\_ident\_away : \\ -\qquad identifier -> identifier list -> identifier} - {\\ Generates a new identifier with the same root string than the - given one, but with a new index, different from all the indexes of - a given list of identifiers.} -\fun{val Names.id\_of\_string : string -> - identifier} - {Creates an identifier from a string.} -\fun{val Names.string\_of\_id : identifier -> string} - {The inverse operation: transforms an identifier into a string} -\end{description} - -\paragraph{Names.} A \textsl{name} is either an identifier or the -special name \texttt{Anonymous}. Names are used as arguments of -binders, in order to pretty print bound variables. -The following operations can be used for handling names: - -\begin{description} -\fun{val Names.Name: identifier -> Name} - {Constructs a name from an identifier.} -\fun{val Names.Anonymous : Name} - {Constructs a special, anonymous identifier, like the variable abstracted - in the term $[\_:A]0$.} -\fun{val - Names.next\_name\_away\_with\_default : \\ \qquad - string->name->identifier list->identifier} -{\\ If the name is not anonymous, then this function generates a new - identifier different from all the ones in a given list. Otherwise, it - generates an identifier from the given string.} -\end{description} - -\paragraph[Section paths.]{Section paths.\label{SectionPaths}} -A \textsl{section-path} is a global name to refer to an object without -ambiguity. It can be seen as a sort of filename, where open sections -play the role of directories. Each section path is formed by three -components: a \textsl{directory} (the list of open sections); a -\textsl{basename} (the identifier for the object); and a \textsl{kind} -(either CCI for the terms of the Calculus of Constructions, FW for the -the terms of $F_\omega$, or OBJ for other objects). For example, the -name of the following constant: -\begin{verbatim} - Section A. - Section B. - Section C. - Definition zero := O. -\end{verbatim} - -is internally represented by the section path: - -$$\underbrace{\mathtt{\#A\#B\#C}}_{\mbox{dirpath}} -\underbrace{\mathtt{\tt \#zero}}_{\mbox{basename}} -\underbrace{\mathtt{\tt .cci}_{\;}}_{\mbox{kind}}$$ - -When one of the sections is closed, a new constant is created with an -updated section-path,a nd the old one is no longer reachable. In our -example, after closing the section \texttt{C}, the new section-path -for the constant {\tt zero} becomes: -\begin{center} -\texttt{ \#A\#B\#zero.cci} -\end{center} - -The following operations can be used to handle section paths: - -\begin{description} -\fun{val Names.string\_of\_path : section\_path -> string} - {Transforms the section path into a string.} -\fun{val Names.path\_of\_string : string -> section\_path} - {Parses a string an returns the corresponding section path.} -\fun{val Names.basename : section\_path -> identifier} - {Provides the basename of a section path} -\fun{val Names.dirpath : section\_path -> string list} - {Provides the directory of a section path} -\fun{val Names.kind\_of\_path : section\_path -> path\_kind} - {Provides the kind of a section path} -\end{description} - -\subsubsection{Signatures} - -A \textsl{signature} is a mapping associating different informations -to identifiers (for example, its type, its definition, etc). The -following operations could be useful for working with signatures: - -\begin{description} -\fun{val Names.ids\_of\_sign : 'a signature -> identifier list} - {Gets the list of identifiers of the signature.} -\fun{val Names.vals\_of\_sign : 'a signature -> 'a list} - {Gets the list of values associated to the identifiers of the signature.} -\fun{val Names.lookup\_glob1 : \\ \qquad -identifier -> 'a signature -> (identifier * - 'a)} - {\\ Gets the value associated to a given identifier of the signature.} -\end{description} - - -\subsection{The Terms of the Calculus of Constructions} - -The language of the Calculus of Inductive Constructions described in -Chapter \ref{Cic} is implemented on the top of the logical framework, -instantiating the parameter $op$ of the meta-language with a -particular set of operators. In the implementation this language is -called \texttt{constr}, the language of constructions. - -% The only difference -%with respect to the one described in Section \ref{} is that the terms -%of \texttt{constr} may contain \textsl{existential variables}. An -%existential variable is a place holder representing a part of the term -%that is still to be constructed. Such ``open terms'' are necessary -%when building proofs interactively. - -\subsubsection{Building Constructions} - -The user does not need to know the choices made to represent -\texttt{constr} in the meta-language. They are abstracted away by the -following constructor functions: - -\begin{description} -\fun{val Term.mkRel : int -> constr} - {$(\texttt{mkRel}\;n)$ represents de Bruijn's index $n$.} - -\fun{val Term.mkVar : identifier -> constr} - {$(\texttt{mkVar}\;id)$ - represents a global identifier named $id$, like a variable - inside the scope of a section, or a hypothesis in a proof}. - -\fun{val Term.mkExistential : constr} - {\texttt{mkExistential} represents an implicit sub-term, like the question - marks in the term \texttt{(pair ? ? O true)}.} - -%\fun{val Term.mkMeta : int -> constr} -% {$(\texttt{mkMeta}\;n)$ represents an existential variable, whose -% name is the integer $n$.} - -\fun{val Term.mkProp : constr} - {$\texttt{mkProp}$ represents the sort \textsl{Prop}.} - -\fun{val Term.mkSet : constr} - {$\texttt{mkSet}$ represents the sort \textsl{Set}.} - -\fun{val Term.mkType : Impuniv.universe -> constr} - {$(\texttt{mkType}\;u)$ represents the term - $\textsl{Type}(u)$. The universe $u$ is represented as a - section path indexed by an integer. } - -\fun{val Term.mkConst : section\_path -> constr array -> constr} - {$(\texttt{mkConst}\;c\;v)$ represents a constant whose name is - $c$. The body of the constant is stored in a global table, - accessible through the name of the constant. The array of terms - $v$ corresponds to the variables of the environment appearing in - the body of the constant when it was defined. For instance, a - constant defined in the section \textsl{Foo} containing the - variable $A$, and whose body is $[x:Prop\ra Prop](x\;A)$ is - represented inside the scope of the section by - $(\texttt{mkConst}\;\texttt{\#foo\#f.cci}\;[| \texttt{mkVAR}\;A - |])$. Once the section is closed, the constant is represented by - the term $(\texttt{mkConst}\;\#f.cci\;[| |])$, and its body - becomes $[A:Prop][x:Prop\ra Prop](x\;A)$}. - -\fun{val Term.mkMutInd : section\_path -> int -> constr array ->constr} - {$(\texttt{mkMutInd}\;c\;i)$ represents the $ith$ type - (starting from zero) of the block of mutually dependent - (co)inductive types, whose first type is $c$. Similarly to the - case of constants, the array of terms represents the current - environment of the (co)inductive type. The definition of the type - (its arity, its constructors, whether it is inductive or co-inductive, etc.) - is stored in a global hash table, accessible through the name of - the type.} - -\fun{val Term.mkMutConstruct : \\ \qquad section\_path -> int -> int -> constr array - ->constr} {\\ $(\texttt{mkMutConstruct}\;c\;i\;j)$ represents the - $jth$ constructor of the $ith$ type of the block of mutually - dependent (co)inductive types whose first type is $c$. The array - of terms represents the current environment of the (co)inductive - type.} - -\fun{val Term.mkCast : constr -> constr -> constr} - {$(\texttt{mkCast}\;t\;T)$ represents the annotated term $t::T$ in - \Coq's syntax.} - -\fun{val Term.mkProd : name ->constr ->constr -> constr} - {$(\texttt{mkProd}\;x\;A\;B)$ represents the product $(x:A)B$. - The free ocurrences of $x$ in $B$ are represented by de Bruijn's - indexes.} - -\fun{val Term.mkNamedProd : identifier -> constr -> constr -> constr} - {$(\texttt{produit}\;x\;A\;B)$ represents the product $(x:A)B$, - but the bound occurrences of $x$ in $B$ are denoted by - the identifier $(\texttt{mkVar}\;x)$. The function automatically - changes each occurrences of this identifier into the corresponding - de Bruijn's index.} - -\fun{val Term.mkArrow : constr -> constr -> constr} - {$(\texttt{arrow}\;A\;B)$ represents the type $(A\rightarrow B)$.} - -\fun{val Term.mkLambda : name -> constr -> constr -> constr} - {$(\texttt{mkLambda}\;x\;A\;b)$ represents the lambda abstraction - $[x:A]b$. The free ocurrences of $x$ in $B$ are represented by de Bruijn's - indexes.} - -\fun{val Term.mkNamedLambda : identifier -> constr -> constr -> constr} - {$(\texttt{lambda}\;x\;A\;b)$ represents the lambda abstraction - $[x:A]b$, but the bound occurrences of $x$ in $B$ are denoted by - the identifier $(\texttt{mkVar}\;x)$. } - -\fun{val Term.mkAppLA : constr array -> constr} - {$(\texttt{mkAppLA}\;t\;[|t_1\ldots t_n|])$ represents the application - $(t\;t_1\;\ldots t_n)$.} - -\fun{val Term.mkMutCaseA : \\ \qquad - case\_info -> constr ->constr - ->constr array -> constr} - {\\ $(\texttt{mkMutCaseA}\;r\;P\;m\;[|f_1\ldots f_n|])$ - represents the term \Case{P}{m}{f_1\ldots f_n}. The first argument - $r$ is either \texttt{None} or $\texttt{Some}\;(c,i)$, where the - pair $(c,i)$ refers to the inductive type that $m$ belongs to.} - -\fun{val Term.mkFix : \\ \qquad -int array->int->constr array->name - list->constr array->constr} - {\\ $(\texttt{mkFix}\;[|k_1\ldots k_n |]\;i\;[|A_1\ldots - A_n|]\;[|f_1\ldots f_n|]\;[|t_1\ldots t_n|])$ represents the term - $\Fix{f_i}{f_1/k_1:A_1:=t_1 \ldots f_n/k_n:A_n:=t_n}$} - -\fun{val Term.mkCoFix : \\ \qquad - int -> constr array -> name list -> - constr array -> constr} - {\\ $(\texttt{mkCoFix}\;i\;[|A_1\ldots - A_n|]\;[|f_1\ldots f_n|]\;[|t_1\ldots t_n|])$ represents the term - $\CoFix{f_i}{f_1:A_1:=t_1 \ldots f_n:A_n:=t_n}$. There are no - decreasing indexes in this case.} -\end{description} - -\subsubsection{Decomposing Constructions} - -Each of the construction functions above has its corresponding -(partial) destruction function, whose name is obtained changing the -prefix \texttt{mk} by \texttt{dest}. In addition to these functions, a -concrete datatype \texttt{kindOfTerm} can be used to do pattern -matching on terms without dealing with their internal representation -in the meta-language. This concrete datatype is described in the \ocaml{} -file \texttt{term.mli}. The following function transforms a construction -into an element of type \texttt{kindOfTerm}: - -\begin{description} -\fun{val Term.kind\_of\_term : constr -> kindOfTerm} - {Destructs a term of the language \texttt{constr}, -yielding the direct components of the term. Hence, in order to do -pattern matching on an object $c$ of \texttt{constr}, it is sufficient -to do pattern matching on the value $(\texttt{kind\_of\_term}\;c)$.} -\end{description} - -Part of the information associated to the constants is stored in -global tables. The following functions give access to such -information: - -\begin{description} -\fun{val Termenv.constant\_value : constr -> constr} - {If the term denotes a constant, projects the body of a constant} -\fun{Termenv.constant\_type : constr -> constr} - {If the term denotes a constant, projects the type of the constant} -\fun{val mind\_arity : constr -> constr} - {If the term denotes an inductive type, projects its arity (i.e., - the type of the inductive type).} -\fun{val Termenv.mis\_is\_finite : mind\_specif -> bool} - {Determines whether a recursive type is inductive or co-inductive.} -\fun{val Termenv.mind\_nparams : constr -> int} - {If the term denotes an inductive type, projects the number of - its general parameters.} -\fun{val Termenv.mind\_is\_recursive : constr -> bool} - {If the term denotes an inductive type, - determines if the type has at least one recursive constructor. } -\fun{val Termenv.mind\_recargs : constr -> recarg list array array} - {If the term denotes an inductive type, returns an array $v$ such - that the nth element of $v.(i).(j)$ is - \texttt{Mrec} if the $nth$ argument of the $jth$ constructor of - the $ith$ type is recursive, and \texttt{Norec} if it is not.}. -\end{description} - -\subsection[The Type Checker]{The Type Checker\label{TypeChecker}} - -The third logical module is the type checker. It concentrates two main -tasks concerning the language of constructions. - -On one hand, it contains the type inference and type-checking -functions. The type inference function takes a term -$a$ and a signature $\Gamma$, and yields a term $A$ such that -$\Gamma \vdash a:A$. The type-checking function takes two terms $a$ -and $A$ and a signature $\Gamma$, and determines whether or not -$\Gamma \vdash a:A$. - -On the other hand, this module is in charge of the compilation of -\Coq's abstract syntax trees into the language \texttt{constr} of -constructions. This compilation seeks to eliminate all the ambiguities -contained in \Coq's abstract syntax, restoring the information -necessary to type-check it. It concerns at least the following steps: -\begin{enumerate} -\item Compiling the pattern-matching expressions containing -constructor patterns, wild-cards, etc, into terms that only -use the primitive \textsl{Case} described in Chapter \ref{Cic} -\item Restoring type coercions and synthesizing the implicit arguments -(the one denoted by question marks in -{\Coq} syntax: see Section~\ref{Coercions}). -\item Transforming the named bound variables into de Bruijn's indexes. -\item Classifying the global names into the different classes of -constants (defined constants, constructors, inductive types, etc). -\end{enumerate} - -\subsection{The Proof Engine} - -The fourth stage of \Coq's implementation is the \textsl{proof engine}: -the interactive machine for constructing proofs. The aim of the proof -engine is to construct a top-down derivation or \textsl{proof tree}, -by the application of \textsl{tactics}. A proof tree has the following -general structure:\\ - -\begin{displaymath} -\frac{\Gamma \vdash ? = t(?_1,\ldots?_n) : G} - {\hspace{3ex}\frac{\displaystyle \Gamma_1 \vdash ?_1 = t_1(\ldots) : G_1} - {\stackrel{\vdots}{\displaystyle {\Gamma_{i_1} \vdash ?_{i_1} - : G_{i_1}}}}(tac_1) - \;\;\;\;\;\;\;\;\; - \frac{\displaystyle \Gamma_n \vdash ?_n = t_n(\ldots) : G_n} - {\displaystyle \stackrel{\vdots}{\displaystyle {\Gamma_{i_m} \vdash ?_{i_m} : - G_{i_m}}}}(tac_n)} (tac) -\end{displaymath} - - -\noindent Each node of the tree is called a \textsl{goal}. A goal -is a record type containing the following three fields: -\begin{enumerate} -\item the conclusion $G$ to be proven; -\item a typing signature $\Gamma$ for the free variables in $G$; -\item if the goal is an internal node of the proof tree, the -definition $t(?_1,\ldots?_n)$ of an \textsl{existential variable} -(i.e. a possible undefined constant) $?$ of type $G$ in terms of the -existential variables of the children sub-goals. If the node is a -leaf, the existential variable maybe still undefined. -\end{enumerate} - -Once all the existential variables have been defined the derivation is -completed, and a construction can be generated from the proof tree, -replacing each of the existential variables by its definition. This -is exactly what happens when one of the commands -\texttt{Qed} or \texttt{Defined} is invoked -(see Section~\ref{Qed}). The saved theorem becomes a defined constant, -whose body is the proof object generated. - -\paragraph{Important:} Before being added to the -context, the proof object is type-checked, in order to verify that it is -actually an object of the expected type $G$. Hence, the correctness -of the proof actually does not depend on the tactics applied to -generate it or the machinery of the proof engine, but only on the -type-checker. In other words, extending the system with a potentially -bugged new tactic never endangers the consistency of the system. - -\subsubsection[What is a Tactic?]{What is a Tactic?\label{WhatIsATactic}} -%Let us now explain what is a tactic, and how the user can introduce -%new ones. - -From an operational point of view, the current state of the proof -engine is given by the mapping $emap$ from existential variables into -goals, plus a pointer to one of the leaf goals $g$. Such a pointer -indicates where the proof tree will be refined by the application of a -\textsl{tactic}. A tactic is a function from the current state -$(g,emap)$ of the proof engine into a pair $(l,val)$. The first -component of this pair is the list of children sub-goals $g_1,\ldots -g_n$ of $g$ to be yielded by the tactic. The second one is a -\textsl{validation function}. Once the proof trees $\pi_1,\ldots -\pi_n$ for $g_1,\ldots g_n$ have been completed, this validation -function must yield a proof tree $(val\;\pi_1,\ldots \pi_n)$ deriving -$g$. - -Tactics can be classified into \textsl{primitive} ones and -\textsl{defined} ones. Primitive tactics correspond to the five basic -operations of the proof engine: - -\begin{enumerate} -\item Introducing a universally quantified variable into the local -context of the goal. -\item Defining an undefined existential variable -\item Changing the conclusion of the goal for another ---definitionally equal-- term. -\item Changing the type of a variable in the local context for another -definitionally equal term. -\item Erasing a variable from the local context. -\end{enumerate} - -\textsl{Defined} tactics are tactics constructed by combining these -primitive operations. Defined tactics are registered in a hash table, -so that they can be introduced dynamically. In order to define such a -tactic table, it is necessary to fix what a \textsl{possible argument} -of a tactic may be. The type \texttt{tactic\_arg} of the possible -arguments for tactics is a union type including: -\begin{itemize} -\item quoted strings; -\item integers; -\item identifiers; -\item lists of identifiers; -\item plain terms, represented by its abstract syntax tree; -\item well-typed terms, represented by a construction; -\item a substitution for bound variables, like the -substitution in the tactic \\$\texttt{Apply}\;t\;\texttt{with}\;x:=t_1\ldots -x_n:=t_n$, (see Section~\ref{apply}); -\item a reduction expression, denoting the reduction strategy to be -followed. -\end{itemize} -Therefore, for each function $tac:a \rightarrow tactic$ implementing a -defined tactic, an associated dynamic tactic $tacargs\_tac: -\texttt{tactic\_arg}\;list \rightarrow tactic$ calling $tac$ must be -written. The aim of the auxiliary function $tacargs\_tac$ is to inject -the arguments of the tactic $tac$ into the type of possible arguments -for a tactic. - -The following function can be used for registering and calling a -defined tactic: - -\begin{description} -\fun{val Tacmach.add\_tactic : \\ \qquad -string -> (tactic\_arg list ->tactic) -> unit} - {\\ Registers a dynamic tactic with the given string as access index.} -\fun{val Tacinterp.vernac\_tactic : string*tactic\_arg list -> tactic} - {Interprets a defined tactic given by its entry in the - tactics table with a particular list of possible arguments.} -\fun{val Tacinterp.vernac\_interp : CoqAst.t -> tactic} - {Interprets a tactic expression formed combining \Coq's tactics and - tacticals, and described by its abstract syntax tree.} -\end{description} - -When programming a new tactic that calls an already defined tactic -$tac$, we have the choice between using the \ocaml{} function -implementing $tac$, or calling the tactic interpreter with the name -and arguments for interpreting $tac$. In the first case, a tactic call -will left the trace of the whole implementation of $tac$ in the proof -tree. In the second, the implementation of $tac$ will be hidden, and -only an invocation of $tac$ will be recalled (cf. the example of -Section \ref{ACompleteExample}. The following combinators can be used -to hide the implementation of a tactic: - -\begin{verbatim} -type 'a hiding_combinator = string -> ('a -> tactic) -> ('a -> tactic) -val Tacmach.hide_atomic_tactic : string -> tactic -> tactic -val Tacmach.hide_constr_tactic : constr hiding_combinator -val Tacmach.hide_constrl_tactic : (constr list) hiding_combinator -val Tacmach.hide_numarg_tactic : int hiding_combinator -val Tacmach.hide_ident_tactic : identifier hiding_combinator -val Tacmach.hide_identl_tactic : identifier hiding_combinator -val Tacmach.hide_string_tactic : string hiding_combinator -val Tacmach.hide_bindl_tactic : substitution hiding_combinator -val Tacmach.hide_cbindl_tactic : - (constr * substitution) hiding_combinator -\end{verbatim} - -These functions first register the tactic by a side effect, and then -yield a function calling the interpreter with the registered name and -the right injection into the type of possible arguments. - -\subsection{Tactics and Tacticals Provided by \Coq} - -The fifth logical module is the library of tacticals and basic tactics -provided by \Coq. This library is distributed into the directories -\texttt{tactics} and \texttt{src/tactics}. The former contains those -basic tactics that make use of the types contained in the basic state -of \Coq. For example, inversion or rewriting tactics are in the -directory \texttt{tactics}, since they make use of the propositional -equality type. Those tactics which are independent from the context ---like for example \texttt{Cut}, \texttt{Intros}, etc-- are defined in -the directory \texttt{src/tactics}. This latter directory also -contains some useful tools for programming new tactics, referred in -Section \ref{SomeUsefulToolsforWrittingTactics}. - -In practice, it is very unusual that the list of sub-goals and the -validation function of the tactic must be explicitly constructed by -the user. In most of the cases, the implementation of a new tactic -consists in supplying the appropriate arguments to the basic tactics -and tacticals. - -\subsubsection{Basic Tactics} - -The file \texttt{Tactics} contain the implementation of the basic -tactics provided by \Coq. The following tactics are some of the most -used ones: - -\begin{verbatim} -val Tactics.intro : tactic -val Tactics.assumption : tactic -val Tactics.clear : identifier list -> tactic -val Tactics.apply : constr -> constr substitution -> tactic -val Tactics.one_constructor : int -> constr substitution -> tactic -val Tactics.simplest_elim : constr -> tactic -val Tactics.elimType : constr -> tactic -val Tactics.simplest_case : constr -> tactic -val Tactics.caseType : constr -> tactic -val Tactics.cut : constr -> tactic -val Tactics.reduce : redexpr -> tactic -val Tactics.exact : constr -> tactic -val Auto.auto : int option -> tactic -val Auto.trivial : tactic -\end{verbatim} - -The functions hiding the implementation of these tactics are defined -in the module \texttt{Hiddentac}. Their names are prefixed by ``h\_''. - -\subsubsection[Tacticals]{Tacticals\label{OcamlTacticals}} - -The following tacticals can be used to combine already existing -tactics: - -\begin{description} -\fun{val Tacticals.tclIDTAC : tactic} - {The identity tactic: it leaves the goal as it is.} - -\fun{val Tacticals.tclORELSE : tactic -> tactic -> tactic} - {Tries the first tactic and in case of failure applies the second one.} - -\fun{val Tacticals.tclTHEN : tactic -> tactic -> tactic} - {Applies the first tactic and then the second one to each generated subgoal.} - -\fun{val Tacticals.tclTHENS : tactic -> tactic list -> tactic} - {Applies a tactic, and then applies each tactic of the tactic list to the - corresponding generated subgoal.} - -\fun{val Tacticals.tclTHENL : tactic -> tactic -> tactic} - {Applies the first tactic, and then applies the second one to the last - generated subgoal.} - -\fun{val Tacticals.tclREPEAT : tactic -> tactic} - {If the given tactic succeeds in producing a subgoal, then it - is recursively applied to each generated subgoal, - and so on until it fails. } - -\fun{val Tacticals.tclFIRST : tactic list -> tactic} - {Tries the tactics of the given list one by one, until one of them - succeeds.} - -\fun{val Tacticals.tclTRY : tactic -> tactic} - {Tries the given tactic and in case of failure applies the {\tt - tclIDTAC} tactical to the original goal.} - -\fun{val Tacticals.tclDO : int -> tactic -> tactic} - {Applies the tactic a given number of times.} - -\fun{val Tacticals.tclFAIL : tactic} - {The always failing tactic: it raises a {\tt UserError} exception.} - -\fun{val Tacticals.tclPROGRESS : tactic -> tactic} - {Applies the given tactic to the current goal and fails if the - tactic leaves the goal unchanged} - -\fun{val Tacticals.tclNTH\_HYP : int -> (constr -> tactic) -> tactic} - {Applies a tactic to the nth hypothesis of the local context. - The last hypothesis introduced correspond to the integer 1.} - -\fun{val Tacticals.tclLAST\_HYP : (constr -> tactic) -> tactic} - {Applies a tactic to the last hypothesis introduced.} - -\fun{val Tacticals.tclCOMPLETE : tactic -> tactic} - {Applies a tactic and fails if the tactic did not solve completely the - goal} - -\fun{val Tacticals.tclMAP : ('a -> tactic) -> 'a list -> tactic} - {Applied to the function \texttt{f} and the list \texttt{[x\_1; - ... ; x\_n]}, this tactical applies the tactic - \texttt{tclTHEN (f x1) (tclTHEN (f x2) ... ))))}} - -\fun{val Tacicals.tclIF : (goal sigma -> bool) -> tactic -> tactic -> tactic} - {If the condition holds, apply the first tactic; otherwise, - apply the second one} - -\end{description} - - -\subsection{The Vernacular Interpreter} - -The sixth logical module of the implementation corresponds to the -interpreter of the vernacular phrases of \Coq. These phrases may be -expressions from the \gallina{} language (definitions), general -directives (setting commands) or tactics to be applied by the proof -engine. - -\subsection[The Parser and the Pretty-Printer]{The Parser and the Pretty-Printer\label{PrettyPrinter}} - -The last logical module is the parser and pretty printer of \Coq, -which is the interface between the vernacular interpreter and the -user. They translate the chains of characters entered at the input -into abstract syntax trees, and vice versa. Abstract syntax trees are -represented by labeled n-ary trees, and its type is called -\texttt{CoqAst.t}. For instance, the abstract syntax tree associated -to the term $[x:A]x$ is: - -\begin{displaymath} -\texttt{Node} - ((0,6), "LAMBDA", - [\texttt{Nvar}~((3, 4),"A");~\texttt{Slam}~((0,6),~Some~"x",~\texttt{Nvar}~((5,6),"x"))]) -\end{displaymath} - -The numbers correspond to \textsl{locations}, used to point to some -input line and character positions in the error messages. As it was -already explained in Section \ref{TypeChecker}, this term is then -translated into a construction term in order to be typed. - -The parser of \Coq\ is implemented using \camlpppp. The lexer and the data -used by \camlpppp\ to generate the parser lay in the directory -\texttt{src/parsing}. This directory also contains \Coq's -pretty-printer. The printing rules lay in the directory -\texttt{src/syntax}. The different entries of the grammar are -described in the module \texttt{Pcoq.Entry}. Let us present here two -important functions of this logical module: - -\begin{description} -\fun{val Pcoq.parse\_string : 'a Grammar.Entry.e -> string -> 'a} - {Parses a given string, trying to recognize a phrase - corresponding to some entry in the grammar. If it succeeds, - it yields a value associated to the grammar entry. For example, - applied to the entry \texttt{Pcoq.Command.command}, this function - parses a term of \Coq's language, and yields a value of type - \texttt{CoqAst.t}. When applied to the entry - \texttt{Pcoq.Vernac.vernac}, it parses a vernacular command and - returns the corresponding Ast.} -\fun{val gentermpr : \\ \qquad -path\_kind -> constr assumptions -> constr -> std\_ppcmds} - {\\ Pretty-prints a well-typed term of certain kind (cf. Section - \ref{SectionPaths}) under its context of typing assumption.} -\fun{val gentacpr : CoqAst.t -> std\_ppcmds} - {Pretty-prints a given abstract syntax tree representing a tactic - expression.} -\end{description} - -\subsection{The General Library} - -In addition to the ones laying in the standard library of \ocaml{}, -several useful modules about lists, arrays, sets, mappings, balanced -trees, and other frequently used data structures can be found in the -directory \texttt{lib}. Before writing a new one, check if it is not -already there! - -\subsubsection{The module \texttt{Std}} -This module in the directory \texttt{src/lib/util} is opened by almost -all modules of \Coq{}. Among other things, it contains a definition of -the different kinds of errors used in \Coq{} : - -\begin{description} -\fun{exception UserError of string * std\_ppcmds} - {This is the class of ``users exceptions''. Such errors arise when - the user attempts to do something illegal, for example \texttt{Intro} - when the current goal conclusion is not a product.} - -\fun{val Std.error : string -> 'a} - {For simple error messages} -\fun{val Std.user_err : ?loc:Loc.t -> string -> std\_ppcmds -> 'a} - {See Section~\ref{PrettyPrinter} : this can be used if the user - want to display a term or build a complex error message} - -\fun{exception Anomaly of string * std\_ppcmds} - {This for reporting bugs or things that should not - happen. The tacticals \texttt{tclTRY} and - \texttt{tclTRY} described in Section~\ref{OcamlTacticals} catch the - exceptions of type \texttt{UserError}, but they don't catch the - anomalies. So, in your code, don't raise any anomaly, unless you - know what you are doing. We also recommend to avoid constructs - such as \texttt{try ... with \_ -> ...} : such constructs can trap - an anomaly and make the debugging process harder.} - -\fun{val Std.anomaly : string -> 'a}{} -\fun{val Std.anomalylabstrm : string -> std\_ppcmds -> 'a}{} -\end{description} - -\section{The tactic writer mini-HOWTO} - -\subsection{How to add a vernacular command} - -The command to register a vernacular command can be found -in module \texttt{Vernacinterp}: - -\begin{verbatim} -val vinterp_add : string * (vernac_arg list -> unit -> unit) -> unit;; -\end{verbatim} - -The first argument is the name, the second argument is a function that -parses the arguments and returns a function of type -\texttt{unit}$\rightarrow$\texttt{unit} that do the job. - -In this section we will show how to add a vernacular command -\texttt{CheckCheck} that print a type of a term and the type of its -type. - -File \texttt{dcheck.ml}: - -\begin{verbatim} -open Vernacinterp;; -open Trad;; -let _ = - vinterp_add - ("DblCheck", - function [VARG_COMMAND com] -> - (fun () -> - let evmap = Evd.mt_evd () - and sign = Termenv.initial_sign () in - let {vAL=c;tYP=t;kIND=k} = - fconstruct_with_univ evmap sign com in - Pp.mSGNL [< Printer.prterm c; 'sTR ":"; - Printer.prterm t; 'sTR ":"; - Printer.prterm k >] ) - | _ -> bad_vernac_args "DblCheck") -;; -\end{verbatim} - -Like for a new tactic, a new syntax entry must be created. - -File \texttt{DCheck.v}: - -\begin{verbatim} -Declare ML Module "dcheck.ml". - -Grammar vernac vernac := - dblcheck [ "CheckCheck" comarg($c) ] -> [(DblCheck $c)]. -\end{verbatim} - -We are now able to test our new command: - -\begin{verbatim} -Coq < Require DCheck. -Coq < CheckCheck O. -O:nat:Set -\end{verbatim} - -Most Coq vernacular commands are registered in the module - \verb+src/env/vernacentries.ml+. One can see more examples here. - -\subsection{How to keep a hashtable synchronous with the reset mechanism} - -This is far more tricky. Some vernacular commands modify some -sort of state (for example by adding something in a hashtable). One -wants that \texttt{Reset} has the expected behavior with this -commands. - -\Coq{} provides a general mechanism to do that. \Coq{} environments -contains objects of three kinds: CCI, FW and OBJ. CCI and FW are for -constants of the calculus. OBJ is a dynamically extensible datatype -that contains sections, tactic definitions, hints for auto, and so -on. - -The simplest example of use of such a mechanism is in file -\verb+src/proofs/macros.ml+ (which implements the \texttt{Tactic - Definition} command). Tactic macros are stored in the imperative -hashtable \texttt{mactab}. There are two functions freeze and unfreeze -to make a copy of the table and to restore the state of table from the -copy. Then this table is declared using \texttt{Library.declare\_summary}. - -What does \Coq{} with that ? \Coq{} defines synchronization points. -At each synchronisation point, the declared tables are frozen (that -is, a copy of this tables is stored). - -When \texttt{Reset }$i$ is called, \Coq{} goes back to the first -synchronisation point that is above $i$ and ``replays'' all objects -between that point -and $i$. It will re-declare constants, re-open section, etc. - -So we need to declare a new type of objects, TACTIC-MACRO-DATA. To -``replay'' on object of that type is to add the corresponding tactic -macro to \texttt{mactab} - -So, now, we can say that \texttt{mactab} is synchronous with the Reset -mechanism$^{\mathrm{TM}}$. - -Notice that this works for hash tables but also for a single integer -(the Undo stack size, modified by the \texttt{Set Undo} command, for -example). - -\subsection{The right way to access to Coq constants from your ML code} - -With their long names, Coq constants are stored using: - -\begin{itemize} -\item a section path -\item an identifier -\end{itemize} - -The identifier is exactly the identifier that is used in \Coq{} to -denote the constant; the section path can be known using the -\texttt{Locate} command: - -\begin{coq_example} - Locate S. - Locate nat. - Locate eq. -\end{coq_example} - -Now it is easy to get a constant by its name and section path: - - -\begin{verbatim} -let constant sp id = - Machops.global_reference (Names.gLOB (Termenv.initial_sign ())) - (Names.path_of_string sp) (Names.id_of_string id);; -\end{verbatim} - - -The only issue is that if one cannot put: - - -\begin{verbatim} -let coq_S = constant "#Datatypes#nat.cci" "S";; -\end{verbatim} - - -in his tactic's code. That is because this sentence is evaluated -\emph{before} the module \texttt{Datatypes} is loaded. The solution is -to use the lazy evaluation of \ocaml{}: - - -\begin{verbatim} -let coq_S = lazy (constant "#Datatypes#nat.cci" "S");; - -... (Lazy.force coq_S) ... -\end{verbatim} - - -Be sure to call always Lazy.force behind a closure -- i.e. inside a -function body or behind the \texttt{lazy} keyword. - -One can see examples of that technique in the source code of \Coq{}, -for example -\verb+plugins/omega/coq_omega.ml+. - -\section[Some Useful Tools for Writing Tactics]{Some Useful Tools for Writing Tactics\label{SomeUsefulToolsforWrittingTactics}} -When the implementation of a tactic is not a straightforward -combination of tactics and tacticals, the module \texttt{Tacmach} -provides several useful functions for handling goals, calling the -type-checker, parsing terms, etc. This module is intended to be -the interface of the proof engine for the user. - -\begin{description} -\fun{val Tacmach.pf\_hyps : goal sigma -> constr signature} - {Projects the local typing context $\Gamma$ from a given goal $\Gamma\vdash ?:G$.} -\fun{val pf\_concl : goal sigma -> constr} - {Projects the conclusion $G$ from a given goal $\Gamma\vdash ?:G$.} -\fun{val Tacmach.pf\_nth\_hyp : goal sigma -> int -> identifier * - constr} - {Projects the $ith$ typing constraint $x_i:A_i$ from the local - context of the given goal.} -\fun{val Tacmach.pf\_fexecute : goal sigma -> constr -> judgement} - {Given a goal whose local context is $\Gamma$ and a term $a$, this - function infers a type $A$ and a kind $K$ such that the judgement - $a:A:K$ is valid under $\Gamma$, or raises an exception if there - is no such judgement. A judgement is just a record type containing - the three terms $a$, $A$ and $K$.} -\fun{val Tacmach.pf\_infexecute : \\ - \qquad -goal sigma -> constr -> judgement * information} - {\\ In addition to the typing judgement, this function also extracts - the $F_{\omega}$ program underlying the term.} -\fun{val Tacmach.pf\_type\_of : goal sigma -> constr -> constr} - {Infers a term $A$ such that $\Gamma\vdash a:A$ for a given term - $a$, where $\Gamma$ is the local typing context of the goal.} -\fun{val Tacmach.pf\_check\_type : goal sigma -> constr -> constr -> bool} - {This function yields a type $A$ if the two given terms $a$ and $A$ verify $\Gamma\vdash - a:A$ in the local typing context $\Gamma$ of the goal. Otherwise, - it raises an exception.} -\fun{val Tacmach.pf\_constr\_of\_com : goal sigma -> CoqAst.t -> constr} - {Transforms an abstract syntax tree into a well-typed term of the - language of constructions. Raises an exception if the term cannot - be typed.} -\fun{val Tacmach.pf\_constr\_of\_com\_sort : goal sigma -> CoqAst.t -> constr} - {Transforms an abstract syntax tree representing a type into - a well-typed term of the language of constructions. Raises an - exception if the term cannot be typed.} -\fun{val Tacmach.pf\_parse\_const : goal sigma -> string -> constr} - {Constructs the constant whose name is the given string.} -\fun{val -Tacmach.pf\_reduction\_of\_redexp : \\ - \qquad goal sigma -> red\_expr -> constr -> constr} - {\\ Applies a certain kind of reduction function, specified by an - element of the type red\_expr.} -\fun{val Tacmach.pf\_conv\_x : goal sigma -> constr -> constr -> bool} - {Test whether two given terms are definitionally equal.} -\end{description} - -\subsection[Patterns]{Patterns\label{Patterns}} - -The \ocaml{} file \texttt{Pattern} provides a quick way for describing a -term pattern and performing second-order, binding-preserving, matching -on it. Patterns are described using an extension of \Coq's concrete -syntax, where the second-order meta-variables of the pattern are -denoted by indexed question marks. - -Patterns may depend on constants, and therefore only to make have -sense when certain theories have been loaded. For this reason, they -are stored with a \textsl{module-marker}, telling us which modules -have to be open in order to use the pattern. The following functions -can be used to store and retrieve patterns form the pattern table: - -\begin{description} -\fun{val Pattern.make\_module\_marker : string list -> module\_mark} - {Constructs a module marker from a list of module names.} -\fun{val Pattern.put\_pat : module\_mark -> string -> marked\_term} - {Constructs a pattern from a parseable string containing holes - and a module marker.} -\fun{val Pattern.somatches : constr -> marked\_term-> bool} - {Tests if a term matches a pattern.} -\fun{val dest\_somatch : constr -> marked\_term -> constr list} - {If the term matches the pattern, yields the list of sub-terms - matching the occurrences of the pattern variables (ordered from - left to right). Raises a \texttt{UserError} exception if the term - does not match the pattern.} -\fun{val Pattern.soinstance : marked\_term -> constr list -> constr} - {Substitutes each hole in the pattern - by the corresponding term of the given the list.} -\end{description} - -\paragraph{Warning:} Sometimes, a \Coq\ term may have invisible -sub-terms that the matching functions are nevertheless sensible to. -For example, the \Coq\ term $(?_1,?_2)$ is actually a shorthand for -the expression $(\texttt{pair}\;?\;?\;?_1\;?_2)$. -Hence, matching this term pattern -with the term $(\texttt{true},\texttt{O})$ actually yields the list -$[?;?;\texttt{true};\texttt{O}]$ as result (and \textbf{not} -$[\texttt{true};\texttt{O}]$, as could be expected). - -\subsection{Patterns on Inductive Definitions} - -The module \texttt{Pattern} also includes some functions for testing -if the definition of an inductive type satisfies certain -properties. Such functions may be used to perform pattern matching -independently from the name given to the inductive type and the -universe it inhabits. They yield the value $(\texttt{Some}\;r::l)$ if -the input term reduces into an application of an inductive type $r$ to -a list of terms $l$, and the definition of $r$ satisfies certain -conditions. Otherwise, they yield the value \texttt{None}. - -\begin{description} -\fun{val Pattern.match\_with\_non\_recursive\_type : constr list option} - {Tests if the inductive type $r$ has no recursive constructors} -\fun{val Pattern.match\_with\_disjunction : constr list option} - {Tests if the inductive type $r$ is a non-recursive type - such that all its constructors have a single argument.} -\fun{val Pattern.match\_with\_conjunction : constr list option} - {Tests if the inductive type $r$ is a non-recursive type - with a unique constructor.} -\fun{val Pattern.match\_with\_empty\_type : constr list option} - {Tests if the inductive type $r$ has no constructors at all} -\fun{val Pattern.match\_with\_equation : constr list option} - {Tests if the inductive type $r$ has a single constructor - expressing the property of reflexivity for some type. For - example, the types $a=b$, $A\mbox{==}B$ and $A\mbox{===}B$ satisfy - this predicate.} -\end{description} - -\subsection{Elimination Tacticals} - -It is frequently the case that the subgoals generated by an -elimination can all be solved in a similar way, possibly parametrized -on some information about each case, like for example: -\begin{itemize} -\item the inductive type of the object being eliminated; -\item its arguments (if it is an inductive predicate); -\item the branch number; -\item the predicate to be proven; -\item the number of assumptions to be introduced by the case -\item the signature of the branch, i.e., for each argument of -the branch whether it is recursive or not. -\end{itemize} - -The following tacticals can be useful to deal with such situations. -They - -\begin{description} -\fun{val Elim.simple\_elimination\_then : \\ \qquad -(branch\_args -> tactic) -> constr -> tactic} - {\\ Performs the default elimination on the last argument, and then - tries to solve the generated subgoals using a given parametrized - tactic. The type branch\_args is a record type containing all - information mentioned above.} -\fun{val Elim.simple\_case\_then : \\ \qquad -(branch\_args -> tactic) -> constr -> tactic} - {\\ Similarly, but it performs case analysis instead of induction.} -\end{description} - -\section[A Complete Example]{A Complete Example\label{ACompleteExample}} - -In order to illustrate the implementation of a new tactic, let us come -back to the problem of deciding the equality of two elements of an -inductive type. - -\subsection{Preliminaries} - -Let us call \texttt{newtactic} the directory that will contain the -implementation of the new tactic. In this directory will lay two -files: a file \texttt{eqdecide.ml}, containing the \ocaml{} sources that -implements the tactic, and a \Coq\ file \texttt{Eqdecide.v}, containing -its associated grammar rules and the commands to generate a module -that can be loaded dynamically from \Coq's toplevel. - -To compile our project, we will create a \texttt{Makefile} with the -command \texttt{do\_Makefile} (see Section~\ref{Makefile}) : - -\begin{quotation} - \texttt{do\_Makefile eqdecide.ml EqDecide.v > Makefile}\\ - \texttt{touch .depend}\\ - \texttt{make depend} -\end{quotation} - -We must have kept the sources of \Coq{} somewhere and to set an -environment variable \texttt{COQTOP} that points to that directory. - -\subsection{Implementing the Tactic} - -The file \texttt{eqdecide.ml} contains the implementation of the -tactic in \ocaml{}. Let us recall the main steps of the proof strategy -for deciding the proposition $(x,y:R)\{x=y\}+\{\neg x=y\}$ on the -inductive type $R$: -\begin{enumerate} -\item Eliminate $x$ and then $y$. -\item Try discrimination to solve those goals where $x$ and $y$ has -been introduced by different constructors. -\item If $x$ and $y$ have been introduced by the same constructor, - then analyze one by one the corresponding pairs of arguments. - If they are equal, rewrite one into the other. If they are - not, derive a contradiction from the invectiveness of the - constructor. -\item Once all the arguments have been rewritten, solve the left half -of the goal by reflexivity. -\end{enumerate} - -In the sequel we implement these steps one by one. We start opening -the modules necessary for the implementation of the tactic: - -\begin{verbatim} -open Names -open Term -open Tactics -open Tacticals -open Hiddentac -open Equality -open Auto -open Pattern -open Names -open Termenv -open Std -open Proof_trees -open Tacmach -\end{verbatim} - -The first step of the procedure can be straightforwardly implemented as -follows: - -\begin{verbatim} -let clear_last = (tclLAST_HYP (fun c -> (clear_one (destVar c))));; -\end{verbatim} - -\begin{verbatim} -let mkBranches = - (tclTHEN intro - (tclTHEN (tclLAST_HYP h_simplest_elim) - (tclTHEN clear_last - (tclTHEN intros - (tclTHEN (tclLAST_HYP h_simplest_case) - (tclTHEN clear_last - intros))))));; -\end{verbatim} - -Notice the use of the tactical \texttt{tclLAST\_HYP}, which avoids to -give a (potentially clashing) name to the quantified variables of the -goal when they are introduced. - -The second step of the procedure is implemented by the following -tactic: - -\begin{verbatim} -let solveRightBranch = (tclTHEN simplest_right discrConcl);; -\end{verbatim} - -In order to illustrate how the implementation of a tactic can be -hidden, let us do it with the tactic above: - -\begin{verbatim} -let h_solveRightBranch = - hide_atomic_tactic "solveRightBranch" solveRightBranch -;; -\end{verbatim} - -As it was already mentioned in Section \ref{WhatIsATactic}, the -combinator \texttt{hide\_atomic\_tactic} first registers the tactic -\texttt{solveRightBranch} in the table, and returns a tactic which -calls the interpreter with the used to register it. Hence, when the -tactical \texttt{Info} is used, our tactic will just inform that -\texttt{solveRightBranch} was applied, omitting all the details -corresponding to \texttt{simplest\_right} and \texttt{discrConcl}. - - - -The third step requires some auxiliary functions for constructing the -type $\{c_1=c_2\}+\{\neg c_1=c_2\}$ for a given inductive type $R$ and -two constructions $c_1$ and $c_2$, and for generalizing this type over -$c_1$ and $c_2$: - -\begin{verbatim} -let mmk = make_module_marker ["#Logic.obj";"#Specif.obj"];; -let eqpat = put_pat mmk "eq";; -let sumboolpat = put_pat mmk "sumbool";; -let notpat = put_pat mmk "not";; -let eq = get_pat eqpat;; -let sumbool = get_pat sumboolpat;; -let not = get_pat notpat;; - -let mkDecideEqGoal rectype c1 c2 g = - let equality = mkAppL [eq;rectype;c1;c2] in - let disequality = mkAppL [not;equality] - in mkAppL [sumbool;equality;disequality] -;; -let mkGenDecideEqGoal rectype g = - let hypnames = ids_of_sign (pf_hyps g) in - let xname = next_ident_away (id_of_string "x") hypnames - and yname = next_ident_away (id_of_string "y") hypnames - in (mkNamedProd xname rectype - (mkNamedProd yname rectype - (mkDecideEqGoal rectype (mkVar xname) (mkVar yname) g))) -;; -\end{verbatim} - -The tactic will depend on the \Coq modules \texttt{Logic} and -\texttt{Specif}, since we use the constants corresponding to -propositional equality (\texttt{eq}), computational disjunction -(\texttt{sumbool}), and logical negation (\texttt{not}), defined in -that modules. This is specified creating the module maker -\texttt{mmk} (see Section~\ref{Patterns}). - -The third step of the procedure can be divided into three sub-steps. -Assume that both $x$ and $y$ have been introduced by the same -constructor. For each corresponding pair of arguments of that -constructor, we have to consider whether they are equal or not. If -they are equal, the following tactic is applied to rewrite one into -the other: - -\begin{verbatim} -let eqCase tac = - (tclTHEN intro - (tclTHEN (tclLAST_HYP h_rewriteLR) - (tclTHEN clear_last - tac))) -;; -\end{verbatim} - - -If they are not equal, then the goal is contraposed and a -contradiction is reached form the invectiveness of the constructor: - -\begin{verbatim} -let diseqCase = - let diseq = (id_of_string "diseq") in - let absurd = (id_of_string "absurd") - in (tclTHEN (intro_using diseq) - (tclTHEN h_simplest_right - (tclTHEN red_in_concl - (tclTHEN (intro_using absurd) - (tclTHEN (h_simplest_apply (mkVar diseq)) - (tclTHEN (h_injHyp absurd) - trivial )))))) -;; -\end{verbatim} - -In the tactic above we have chosen to name the hypotheses because -they have to be applied later on. This introduces a potential risk -of name clashing if the context already contains other hypotheses -also named ``diseq'' or ``absurd''. - -We are now ready to implement the tactic \textsl{SolveArg}. Given the -two arguments $a_1$ and $a_2$ of the constructor, this tactic cuts the -goal with the proposition $\{a_1=a_2\}+\{\neg a_1=a_2\}$, and then -applies the tactics above to each of the generated cases. If the -disjunction cannot be solved automatically, it remains as a sub-goal -to be proven. - -\begin{verbatim} -let solveArg a1 a2 tac g = - let rectype = pf_type_of g a1 in - let decide = mkDecideEqGoal rectype a1 a2 g - in (tclTHENS (h_elimType decide) - [(eqCase tac);diseqCase;default_auto]) g -;; -\end{verbatim} - -The following tactic implements the third and fourth steps of the -proof procedure: - -\begin{verbatim} -let conclpatt = put_pat mmk "{<?1>?2=?3}+{?4}" -;; -let solveLeftBranch rectype g = - let (_::(lhs::(rhs::_))) = - try (dest_somatch (pf_concl g) conclpatt) - with UserError ("somatch",_)-> error "Unexpected conclusion!" in - let nparams = mind_nparams rectype in - let getargs l = snd (chop_list nparams (snd (decomp_app l))) in - let rargs = getargs rhs - and largs = getargs lhs - in List.fold_right2 - solveArg largs rargs (tclTHEN h_simplest_left h_reflexivity) g -;; -\end{verbatim} - -Notice the use of a pattern to decompose the goal and obtain the -inductive type and the left and right hand sides of the equality. A -certain number of arguments correspond to the general parameters of -the type, and must be skipped over. Once the corresponding list of -arguments \texttt{rargs} and \texttt{largs} have been obtained, the -tactic \texttt{solveArg} is iterated on them, leaving a disjunction -whose left half can be solved by reflexivity. - -The following tactic joints together the three steps of the -proof procedure: - -\begin{verbatim} -let initialpatt = put_pat mmk "(x,y:?1){<?1>x=y}+{~(<?1>x=y)}" -;; -let decideGralEquality g = - let (typ::_) = try (dest_somatch (pf_concl g) initialpatt) - with UserError ("somatch",_) -> - error "The goal does not have the expected form" in - let headtyp = hd_app (pf_compute g typ) in - let rectype = match (kind_of_term headtyp) with - IsMutInd _ -> headtyp - | _ -> error ("This decision procedure only" - " works for inductive objects") - in (tclTHEN mkBranches - (tclORELSE h_solveRightBranch (solveLeftBranch rectype))) g -;; -;; -\end{verbatim} - -The tactic above can be specialized in two different ways: either to -decide a particular instance $\{c_1=c_2\}+\{\neg c_1=c_2\}$ of the -universal quantification; or to eliminate this property and obtain two -subgoals containing the hypotheses $c_1=c_2$ and $\neg c_1=c_2$ -respectively. - -\begin{verbatim} -let decideGralEquality = - (tclTHEN mkBranches (tclORELSE h_solveRightBranch solveLeftBranch)) -;; -let decideEquality c1 c2 g = - let rectype = pf_type_of g c1 in - let decide = mkGenDecideEqGoal rectype g - in (tclTHENS (cut decide) [default_auto;decideGralEquality]) g -;; -let compare c1 c2 g = - let rectype = pf_type_of g c1 in - let decide = mkDecideEqGoal rectype c1 c2 g - in (tclTHENS (cut decide) - [(tclTHEN intro - (tclTHEN (tclLAST_HYP simplest_case) - clear_last)); - decideEquality c1 c2]) g -;; -\end{verbatim} - -Next, for each of the tactics that will have an entry in the grammar -we construct the associated dynamic one to be registered in the table -of tactics. This function can be used to overload a tactic name with -several similar tactics. For example, the tactic proving the general -decidability property and the one proving a particular instance for -two terms can be grouped together with the following convention: if -the user provides two terms as arguments, then the specialized tactic -is used; if no argument is provided then the general tactic is invoked. - -\begin{verbatim} -let dyn_decideEquality args g = - match args with - [(COMMAND com1);(COMMAND com2)] -> - let c1 = pf_constr_of_com g com1 - and c2 = pf_constr_of_com g com2 - in decideEquality c1 c2 g - | [] -> decideGralEquality g - | _ -> error "Invalid arguments for dynamic tactic" -;; -add_tactic "DecideEquality" dyn_decideEquality -;; - -let dyn_compare args g = - match args with - [(COMMAND com1);(COMMAND com2)] -> - let c1 = pf_constr_of_com g com1 - and c2 = pf_constr_of_com g com2 - in compare c1 c2 g - | _ -> error "Invalid arguments for dynamic tactic" -;; -add_tactic "Compare" tacargs_compare -;; -\end{verbatim} - -This completes the implementation of the tactic. We turn now to the -\Coq file \texttt{Eqdecide.v}. - - -\subsection{The Grammar Rules} - -Associated to the implementation of the tactic there is a \Coq\ file -containing the grammar and pretty-printing rules for the new tactic, -and the commands to generate an object module that can be then loaded -dynamically during a \Coq\ session. In order to generate an ML module, -the \Coq\ file must contain a -\texttt{Declare ML module} command for all the \ocaml{} files concerning -the implementation of the tactic --in our case there is only one file, -the file \texttt{eqdecide.ml}: - -\begin{verbatim} -Declare ML Module "eqdecide". -\end{verbatim} - -The following grammar and pretty-printing rules are -self-explanatory. We refer the reader to the Section \ref{Grammar} for -the details: - -\begin{verbatim} -Grammar tactic simple_tactic := - EqDecideRuleG1 - [ "Decide" "Equality" comarg($com1) comarg($com2)] -> - [(DecideEquality $com1 $com2)] -| EqDecideRuleG2 - [ "Decide" "Equality" ] -> - [(DecideEquality)] -| CompareRule - [ "Compare" comarg($com1) comarg($com2)] -> - [(Compare $com1 $com2)]. - -Syntax tactic level 0: - EqDecideRulePP1 - [(DecideEquality)] -> - ["Decide" "Equality"] -| EqDecideRulePP2 - [(DecideEquality $com1 $com2)] -> - ["Decide" "Equality" $com1 $com2] -| ComparePP - [(Compare $com1 $com2)] -> - ["Compare" $com1 $com2]. -\end{verbatim} - - -\paragraph{Important:} The names used to label the abstract syntax tree -in the grammar rules ---in this case ``DecideEquality'' and -``Compare''--- must be the same as the name used to register the -tactic in the tactics table. This is what makes the links between the -input entered by the user and the tactic executed by the interpreter. - -\subsection{Loading the Tactic} - -Once the module \texttt{EqDecide.v} has been compiled, the tactic can -be dynamically loaded using the \texttt{Require} command. - -\begin{coq_example} -Require EqDecide. -Goal (x,y:nat){x=y}+{~x=y}. -Decide Equality. -\end{coq_example} - -The implementation of the tactic can be accessed through the -tactical \texttt{Info}: -\begin{coq_example} -Undo. -Info Decide Equality. -\end{coq_example} -\begin{coq_eval} -Abort. -\end{coq_eval} - -Remark that the task performed by the tactic \texttt{solveRightBranch} -is not displayed, since we have chosen to hide its implementation. - -\section[Testing and Debugging your Tactic]{Testing and Debugging your Tactic\label{test-and-debug}} - -When your tactic does not behave as expected, it is possible to trace -it dynamically from \Coq. In order to do this, you have first to leave -the toplevel of \Coq, and come back to the \ocaml{} interpreter. This can -be done using the command \texttt{Drop} (see Section~\ref{Drop}). Once -in the \ocaml{} toplevel, load the file \texttt{tactics/include.ml}. -This file installs several pretty printers for proof trees, goals, -terms, abstract syntax trees, names, etc. It also contains the -function \texttt{go:unit -> unit} that enables to go back to \Coq's -toplevel. - -The modules \texttt{Tacmach} and \texttt{Pfedit} contain some basic -functions for extracting information from the state of the proof -engine. Such functions can be used to debug your tactic if -necessary. Let us mention here some of them: - -\begin{description} -\fun{val get\_pftreestate : unit -> pftreestate} - {Projects the current state of the proof engine.} -\fun{val proof\_of\_pftreestate : pftreestate -> proof} - {Projects the current state of the proof tree. A pretty-printer - displays it in a readable form. } -\fun{val top\_goal\_of\_pftreestate : pftreestate -> goal sigma} - {Projects the goal and the existential variables mapping from - the current state of the proof engine.} -\fun{val nth\_goal\_of\_pftreestate : int -> pftreestate -> goal sigma} - {Projects the goal and mapping corresponding to the $nth$ subgoal - that remains to be proven} -\fun{val traverse : int -> pftreestate -> pftreestate} - {Yields the children of the node that the current state of the - proof engine points to.} -\fun{val solve\_nth\_pftreestate : \\ \qquad -int -> tactic -> pftreestate -> pftreestate} - {\\ Provides the new state of the proof engine obtained applying - a given tactic to some unproven sub-goal.} -\end{description} - -Finally, the traditional \ocaml{} debugging tools like the directives -\texttt{trace} and \texttt{untrace} can be used to follow the -execution of your functions. Frequently, a better solution is to use -the \ocaml{} debugger, see Chapter \ref{Utilities}. - -\section[Concrete syntax for ML tactic and vernacular command]{Concrete syntax for ML tactic and vernacular command\label{Notations-for-ML-command}} - -\subsection{The general case} - -The standard way to bind an ML-written tactic or vernacular command to -a concrete {\Coq} syntax is to use the -\verb=TACTIC EXTEND= and \verb=VERNAC COMMAND EXTEND= macros. - -These macros can be used in any {\ocaml} file defining a (new) ML tactic -or vernacular command. They are expanded into pure {\ocaml} code by -the {\camlpppp} preprocessor of {\ocaml}. Concretely, files that use -these macros need to be compiled by giving to {\tt ocamlc} the option - -\verb=-pp "camlp4o -I $(COQTOP)/parsing grammar.cma pa_extend.cmo"= - -\noindent which is the default for every file compiled by means of a Makefile -generated by {\tt coq\_makefile} (see Chapter~\ref{Addoc-coqc}). So, -just do \verb=make= in this latter case. - -The syntax of the macros is given on figure -\ref{EXTEND-syntax}. They can be used at any place of an {\ocaml} -files where an ML sentence (called \verb=str_item= in the {\tt ocamlc} -parser) is expected. For each rule, the left-hand-side describes the -grammar production and the right-hand-side its interpretation which -must be an {\ocaml} expression. Each grammar production starts with -the concrete name of the tactic or command in {\Coq} and is followed -by arguments, possibly separated by terminal symbols or words. -Here is an example: - -\begin{verbatim} -TACTIC EXTEND Replace - [ "replace" constr(c1) "with" constr(c2) ] -> [ replace c1 c2 ] -END -\end{verbatim} - -\newcommand{\grule}{\textrm{\textsl{rule}}} -\newcommand{\stritem}{\textrm{\textsl{ocaml\_str\_item}}} -\newcommand{\camlexpr}{\textrm{\textsl{ocaml\_expr}}} -\newcommand{\arginfo}{\textrm{\textsl{argument\_infos}}} -\newcommand{\lident}{\textrm{\textsl{lower\_ident}}} -\newcommand{\argument}{\textrm{\textsl{argument}}} -\newcommand{\entry}{\textrm{\textsl{entry}}} -\newcommand{\argtype}{\textrm{\textsl{argtype}}} - -\begin{figure} -\begin{tabular}{|lcll|} -\hline -{\stritem} - & ::= & -\multicolumn{2}{l|}{{\tt TACTIC EXTEND} {\ident} \nelist{\grule}{$|$} {\tt END}}\\ - & $|$ & \multicolumn{2}{l|}{{\tt VERNAC COMMAND EXTEND} {\ident} \nelist{\grule}{$|$} {\tt END}}\\ -&&\multicolumn{2}{l|}{}\\ -{\grule} & ::= & -\multicolumn{2}{l|}{{\tt [} {\str} \sequence{\argument}{} {\tt ] -> [} {\camlexpr} {\tt ]}}\\ -&&\multicolumn{2}{l|}{}\\ -{\argument} & ::= & {\str} &\mbox{(terminal)}\\ - & $|$ & {\entry} {\tt (} {\lident} {\tt )} &\mbox{(non-terminal)}\\ -&&\multicolumn{2}{l|}{}\\ -{\entry} - & ::= & {\tt string} & (a string)\\ - & $|$ & {\tt preident} & (an identifier typed as a {\tt string})\\ - & $|$ & {\tt ident} & (an identifier of type {\tt identifier})\\ - & $|$ & {\tt global} & (a qualified identifier)\\ - & $|$ & {\tt constr} & (a {\Coq} term)\\ - & $|$ & {\tt openconstr} & (a {\Coq} term with holes)\\ - & $|$ & {\tt sort} & (a {\Coq} sort)\\ - & $|$ & {\tt tactic} & (an ${\cal L}_{tac}$ expression)\\ - & $|$ & {\tt constr\_with\_bindings} & (a {\Coq} term with a list of bindings\footnote{as for the tactics {\tt apply} and {\tt elim}})\\ - & $|$ & {\tt int\_or\_var} & (an integer or an identifier denoting an integer)\\ - & $|$ & {\tt quantified\_hypothesis} & (a quantified hypothesis\footnote{as for the tactics {\tt intros until}})\\ - & $|$ & {\tt {\entry}\_opt} & (an optional {\entry} )\\ - & $|$ & {\tt ne\_{\entry}\_list} & (a non empty list of {\entry})\\ - & $|$ & {\tt {\entry}\_list} & (a list of {\entry})\\ - & $|$ & {\tt bool} & (a boolean: no grammar rule, just for typing)\\ - & $|$ & {\lident} & (a user-defined entry)\\ -\hline -\end{tabular} -\caption{Syntax of the macros binding {\ocaml} tactics or commands to a {\Coq} syntax} -\label{EXTEND-syntax} -\end{figure} - -There is a set of predefined non-terminal entries which are -automatically translated into an {\ocaml} object of a given type. The -type is not the same for tactics and for vernacular commands. It is -given in the following table: - -\begin{small} -\noindent \begin{tabular}{|l|l|l|} -\hline -{\entry} & {\it type for tactics} & {\it type for commands} \\ -{\tt string} & {\tt string} & {\tt string}\\ -{\tt preident} & {\tt string} & {\tt string}\\ -{\tt ident} & {\tt identifier} & {\tt identifier}\\ -{\tt global} & {\tt global\_reference} & {\tt qualid}\\ -{\tt constr} & {\tt constr} & {\tt constr\_expr}\\ -{\tt openconstr} & {\tt open\_constr} & {\tt constr\_expr}\\ -{\tt sort} & {\tt sorts} & {\tt rawsort}\\ -{\tt tactic} & {\tt glob\_tactic\_expr * tactic} & {\tt raw\_tactic\_expr}\\ -{\tt constr\_with\_bindings} & {\tt constr with\_bindings} & {\tt constr\_expr with\_bindings}\\\\ -{\tt int\_or\_var} & {\tt int or\_var} & {\tt int or\_var}\\ -{\tt quantified\_hypothesis} & {\tt quantified\_hypothesis} & {\tt quantified\_hypothesis}\\ -{\tt {\entry}\_opt} & {\it the type of entry} {\tt option} & {\it the type of entry} {\tt option}\\ -{\tt ne\_{\entry}\_list} & {\it the type of entry} {\tt list} & {\it the type of entry} {\tt list}\\ -{\tt {\entry}\_list} & {\it the type of entry} {\tt list} & {\it the type of entry} {\tt list}\\ -{\tt bool} & {\tt bool} & {\tt bool}\\ -{\lident} & {user-provided, cf next section} & {user-provided, cf next section}\\ -\hline -\end{tabular} -\end{small} - -\bigskip - -Notice that {\entry} consists in a single identifier and that the {\tt -\_opt}, {\tt \_list}, ... modifiers are part of the identifier. -Here is now another example of a tactic which takes either a non empty -list of identifiers and executes the {\ocaml} function {\tt subst} or -takes no arguments and executes the{\ocaml} function {\tt subst\_all}. - -\begin{verbatim} -TACTIC EXTEND Subst -| [ "subst" ne_ident_list(l) ] -> [ subst l ] -| [ "subst" ] -> [ subst_all ] -END -\end{verbatim} - -\subsection{Adding grammar entries for tactic or command arguments} - -In case parsing the arguments of the tactic or the vernacular command -involves grammar entries other than the predefined entries listed -above, you have to declare a new entry using the macros -\verb=ARGUMENT EXTEND= or \verb=VERNAC ARGUMENT EXTEND=. The syntax is -given on Figure~\ref{ARGUMENT-EXTEND-syntax}. Notice that arguments -declared by \verb=ARGUMENT EXTEND= can be used for arguments of both -tactics and vernacular commands while arguments declared by -\verb=VERNAC ARGUMENT EXTEND= can only be used by vernacular commands. - -For \verb=VERNAC ARGUMENT EXTEND=, the identifier is the name of the -entry and it must be a valid {\ocaml} identifier (especially it must -be lowercase). The grammar rules works as before except that they do -not have to start by a terminal symbol or word. As an example, here -is how the {\Coq} {\tt Extraction Language {\it language}} parses its -argument: - -\begin{verbatim} -VERNAC ARGUMENT EXTEND language -| [ "Ocaml" ] -> [ Ocaml ] -| [ "Haskell" ] -> [ Haskell ] -| [ "Scheme" ] -> [ Scheme ] -END -\end{verbatim} - -For tactic arguments, and especially for \verb=ARGUMENT EXTEND=, the -procedure is more subtle because tactics are objects of the {\Coq} -environment which can be printed and interpreted. Then the syntax -requires extra information providing a printer and a type telling how -the argument behaves. Here is an example of entry parsing a pair of -optional {\Coq} terms. - -\begin{verbatim} -let pp_minus_div_arg pr_constr pr_tactic (omin,odiv) = - if omin=None && odiv=None then mt() else - spc() ++ str "with" ++ - pr_opt (fun c -> str "minus := " ++ pr_constr c) omin ++ - pr_opt (fun c -> str "div := " ++ pr_constr c) odiv - -ARGUMENT EXTEND minus_div_arg - TYPED AS constr_opt * constr_opt - PRINTED BY pp_minus_div_arg -| [ "with" minusarg(m) divarg_opt(d) ] -> [ Some m, d ] -| [ "with" divarg(d) minusarg_opt(m) ] -> [ m, Some d ] -| [ ] -> [ None, None ] -END -\end{verbatim} - -Notice that the type {\tt constr\_opt * constr\_opt} tells that the -object behaves as a pair of optional {\Coq} terms, i.e. as an object -of {\ocaml} type {\tt constr option * constr option} if in a -\verb=TACTIC EXTEND= macro and of type {\tt constr\_expr option * -constr\_expr option} if in a \verb=VERNAC COMMAND EXTEND= macro. - -As for the printer, it must be a function expecting a printer for -terms, a printer for tactics and returning a printer for the created -argument. Especially, each sub-{\term} and each sub-{\tac} in the -argument must be typed by the corresponding printers. Otherwise, the -{\ocaml} code will not be well-typed. - -\Rem The entry {\tt bool} is bound to no syntax but it can be used to -give the type of an argument as in the following example: - -\begin{verbatim} -let pr_orient _prc _prt = function - | true -> mt () - | false -> str " <-" - -ARGUMENT EXTEND orient TYPED AS bool PRINTED BY pr_orient -| [ "->" ] -> [ true ] -| [ "<-" ] -> [ false ] -| [ ] -> [ true ] -END -\end{verbatim} - -\begin{figure} -\begin{tabular}{|lcl|} -\hline -{\stritem} & ::= & - {\tt ARGUMENT EXTEND} {\ident} {\arginfo} {\nelist{\grule}{$|$}} {\tt END}\\ -& $|$ & {\tt VERNAC ARGUMENT EXTEND} {\ident} {\nelist{\grule}{$|$}} {\tt END}\\ -\\ -{\arginfo} & ::= & {\tt TYPED AS} {\argtype} \\ -&& {\tt PRINTED BY} {\lident} \\ -%&& \zeroone{{\tt INTERPRETED BY} {\lident}}\\ -%&& \zeroone{{\tt GLOBALIZED BY} {\lident}}\\ -%&& \zeroone{{\tt SUBSTITUTED BY} {\lident}}\\ -%&& \zeroone{{\tt RAW\_TYPED AS} {\lident} {\tt RAW\_PRINTED BY} {\lident}}\\ -%&& \zeroone{{\tt GLOB\_TYPED AS} {\lident} {\tt GLOB\_PRINTED BY} {\lident}}\\ -\\ -{\argtype} & ::= & {\argtype} {\tt *} {\argtype} \\ -& $|$ & {\entry} \\ -\hline -\end{tabular} -\caption{Syntax of the macros binding {\ocaml} tactics or commands to a {\Coq} syntax} -\label{ARGUMENT-EXTEND-syntax} -\end{figure} - -%\end{document} diff --git a/doc/refman/RefMan-uti.tex b/doc/refman/RefMan-uti.tex index f6371f8e5c..962aa98b68 100644 --- a/doc/refman/RefMan-uti.tex +++ b/doc/refman/RefMan-uti.tex @@ -1,55 +1,27 @@ \chapter[Utilities]{Utilities\label{Utilities}} +%HEVEA\cutname{tools.html} The distribution provides utilities to simplify some tedious works beside proof development, tactics writing or documentation. -\section[Building a toplevel extended with user tactics]{Building a toplevel extended with user tactics\label{Coqmktop}\ttindex{coqmktop}} +\section[Using Coq as a library]{Using Coq as a library} -The native-code version of \Coq\ cannot dynamically load user tactics -using {\ocaml} code. It is possible to build a toplevel of \Coq, -with {\ocaml} code statically linked, with the tool {\tt - coqmktop}. - -For example, one can build a native-code \Coq\ toplevel extended with a tactic -which source is in {\tt tactic.ml} with the command -\begin{verbatim} - % coqmktop -opt -o mytop.out tactic.cmx -\end{verbatim} -where {\tt tactic.ml} has been compiled with the native-code -compiler {\tt ocamlopt}. This command generates an executable -called {\tt mytop.out}. To use this executable to compile your \Coq\ -files, use {\tt coqc -image mytop.out}. - -A basic example is the native-code version of \Coq\ ({\tt coqtop.opt}), -which can be generated by {\tt coqmktop -opt -o coqopt.opt}. - - -\paragraph[Application: how to use the {\ocaml} debugger with Coq.]{Application: how to use the {\ocaml} debugger with Coq.\index{Debugger}} - -One useful application of \texttt{coqmktop} is to build a \Coq\ toplevel in -order to debug your tactics with the {\ocaml} debugger. -You need to have configured and compiled \Coq\ for debugging -(see the file \texttt{INSTALL} included in the distribution). -Then, you must compile the Caml modules of your tactic with the -option \texttt{-g} (with the bytecode compiler) and build a stand-alone -bytecode toplevel with the following command: +In previous versions, \texttt{coqmktop} was used to build custom +toplevels --- for example for better debugging or custom static +linking. Nowadays, the preferred method is to use \texttt{ocamlfind}. +The most basic custom toplevel is built using: \begin{quotation} -\texttt{\% coqmktop -g -o coq-debug}~\emph{<your \texttt{.cmo} files>} +\texttt{\% ocamlfind ocamlopt -thread -rectypes -linkall -linkpkg + -package coq.toplevel toplevel/coqtop\_bin.ml -o my\_toplevel.native} \end{quotation} - -To launch the \ocaml\ debugger with the image you need to execute it in -an environment which correctly sets the \texttt{COQLIB} variable. -Moreover, you have to indicate the directories in which -\texttt{ocamldebug} should search for Caml modules. - -A possible solution is to use a wrapper around \texttt{ocamldebug} -which detects the executables containing the word \texttt{coq}. In -this case, the debugger is called with the required additional -arguments. In other cases, the debugger is simply called without additional -arguments. Such a wrapper can be found in the \texttt{dev/} -subdirectory of the sources. +For example, to statically link LTAC, you can just do: +\begin{quotation} +\texttt{\% ocamlfind ocamlopt -thread -rectypes -linkall -linkpkg + -package coq.toplevel -package coq.ltac toplevel/coqtop\_bin.ml -o my\_toplevel.native} +\end{quotation} +and similarly for other plugins. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @@ -133,6 +105,7 @@ The optional file {\tt CoqMakefile.local} is included by the generated file compiler, like {\tt -bin-annot} or {\tt -w...}. \item[COQC, COQDEP, COQDOC] can be set in order to use alternative binaries (e.g. wrappers) + \item[COQ\_SRC\_SUBDIRS] can be extended by including other paths in which {\tt *.cm*} files are searched. For example {\tt COQ\_SRC\_SUBDIRS+=user-contrib/Unicoq} lets you build a plugin containing OCaml code that depends on the OCaml code of {\tt Unicoq}. \end{description} \item[Rule extension] The following makefile rules can be extended. For example @@ -465,7 +438,7 @@ the \Coq\ language, and also a rudimentary indentation facility: \end{itemize} An inferior mode to run \Coq\ under Emacs, by Marco Maggesi, is also -included in the distribution, in file \texttt{coq-inferior.el}. +included in the distribution, in file \texttt{inferior-coq.el}. Instructions to use it are contained in this file. \subsection[{\ProofGeneral}]{{\ProofGeneral}\index{Proof General@{\ProofGeneral}}} diff --git a/doc/refman/Setoid.tex b/doc/refman/Setoid.tex index 6c79284389..b7b343112f 100644 --- a/doc/refman/Setoid.tex +++ b/doc/refman/Setoid.tex @@ -1,6 +1,7 @@ \newtheorem{cscexample}{Example} \achapter{\protect{Generalized rewriting}} +%HEVEA\cutname{setoid.html} \aauthor{Matthieu Sozeau} \label{setoids} @@ -223,7 +224,7 @@ the following command. \comindex{Add Parametric Morphism} \begin{quote} - \texttt{Add Parametric Morphism} ($x_1 : \T_!$) \ldots ($x_k : \T_k$)\\ + \texttt{Add Parametric Morphism} ($x_1 : \T_1$) \ldots ($x_k : \T_k$) : (\textit{f $t_1$ \ldots $t_n$})\\ \texttt{~with signature} \textit{sig}\\ \texttt{~as id}.\\ diff --git a/doc/refman/Universes.tex b/doc/refman/Universes.tex index 6ea2537399..6c84a1818c 100644 --- a/doc/refman/Universes.tex +++ b/doc/refman/Universes.tex @@ -1,4 +1,5 @@ \achapter{Polymorphic Universes} +%HEVEA\cutname{universes.html} \aauthor{Matthieu Sozeau} \label{Universes-full} @@ -67,6 +68,13 @@ is only valid as long as \texttt{Top.4} is strictly smaller than monomorphic (not universe polymorphic), so the two universes (in this case \texttt{Top.3} and \texttt{Top.4}) are actually global levels. +When printing \texttt{pidentity}, we can see the universes it binds in +the annotation \texttt{@\{Top.2\}}. Additionally, when \texttt{Set + Printing Universes} is on we print the ``universe context'' of +\texttt{pidentity} consisting of the bound universes and the +constraints they must verify (for \texttt{pidentity} there are no +constraints). + Inductive types can also be declared universes polymorphic on universes appearing in their parameters or fields. A typical example is given by monoids: @@ -137,7 +145,7 @@ producing global universe constraints, one can use the \optindex{Polymorphic Inductive Cumulativity} Polymorphic inductive types, coinductive types, variants and records can be -declared cumulative using the \texttt{Cumulative}. Alternatively, +declared cumulative using the \texttt{Cumulative} prefix. Alternatively, there is an option \texttt{Set Polymorphic Inductive Cumulativity} which when set, makes all subsequent \emph{polymorphic} inductive definitions cumulative. When set, inductive types and the like can be enforced to be @@ -150,15 +158,22 @@ Polymorphic Cumulative Inductive list {A : Type} := \begin{coq_example} Print list. \end{coq_example} -When printing \texttt{list}, the part of the output of the form -\texttt{$\mathtt{\sim}$@\{i\} <= $\mathtt{\sim}$@\{j\} iff } -indicates the universe constraints in order to have the subtyping -$\WTEGLECONV{\mathtt{list@\{i\}} A}{\mathtt{list@\{j\}} B}$ -(for fully applied instances of \texttt{list}) whenever $\WTEGCONV{A}{B}$. -In the case of \texttt{list} there is no constraint! -This also means that any two instances of \texttt{list} are convertible: -$\WTEGCONV{\mathtt{list@\{i\}} A}{\mathtt{list@\{j\}} B}$ whenever $\WTEGCONV{A}{B}$ and -furthermore their corresponding (when fully applied to convertible arguments) constructors. +When printing \texttt{list}, the universe context indicates the +subtyping constraints by prefixing the level names with symbols. + +Because inductive subtypings are only produced by comparing inductives +to themselves with universes changed, they amount to variance +information: each universe is either invariant, covariant or +irrelevant (there are no contravariant subtypings in Coq), +respectively represented by the symbols \texttt{=}, \texttt{+} and +\texttt{*}. + +Here we see that \texttt{list} binds an irrelevant universe, so any +two instances of \texttt{list} are convertible: +$\WTEGCONV{\mathtt{list@\{i\}} A}{\mathtt{list@\{j\}} B}$ whenever +$\WTEGCONV{A}{B}$ and furthermore their corresponding (when fully +applied to convertible arguments) constructors. + See Chapter~\ref{Cic} for more details on convertibility and subtyping. The following is an example of a record with non-trivial subtyping relation: \begin{coq_example*} @@ -167,8 +182,9 @@ Polymorphic Cumulative Record packType := {pk : Type}. \begin{coq_example} Print packType. \end{coq_example} -Notice that as expected, \texttt{packType@\{i\}} and \texttt{packType@\{j\}} are -convertible if and only if \texttt{i $=$ j}. +\texttt{packType} binds a covariant universe, i.e. +$\WTEGCONV{\mathtt{packType@\{i\}}}{\mathtt{packType@\{j\}}}$ whenever +\texttt{i $\leq$ j}. Cumulative inductive types, coninductive types, variants and records only make sense when they are universe polymorphic. Therefore, an @@ -284,8 +300,10 @@ universes and explicitly instantiate polymorphic definitions. \label{UniverseCmd}} In the monorphic case, this command declares a new global universe named -{\ident}. It supports the polymorphic flag only in sections, meaning the -universe quantification will be discharged on each section definition +{\ident}, which can be referred to using its qualified name as +well. Global universe names live in a separate namespace. The command +supports the polymorphic flag only in sections, meaning the universe +quantification will be discharged on each section definition independently. One cannot mix polymorphic and monomorphic declarations in the same section. diff --git a/doc/refman/coqide-queries.png b/doc/refman/coqide-queries.png Binary files differindex dea5626f8e..7a46ac4e68 100644 --- a/doc/refman/coqide-queries.png +++ b/doc/refman/coqide-queries.png diff --git a/doc/refman/coqide.png b/doc/refman/coqide.png Binary files differindex a6a0f5850e..e300401c9f 100644 --- a/doc/refman/coqide.png +++ b/doc/refman/coqide.png diff --git a/doc/refman/index.html b/doc/refman/index.html index 9b5250abcb..b937350e6e 100644 --- a/doc/refman/index.html +++ b/doc/refman/index.html @@ -11,4 +11,4 @@ <FRAME SRC="menu.html"> </FRAMESET> -</HTML>
\ No newline at end of file +</HTML> |
