diff options
author | 2003-12-30 09:53:31 +0000 | |
---|---|---|
committer | 2003-12-30 09:53:31 +0000 | |
commit | bb6e15cb3d64f2902f98d01b8fe12948a7191095 (patch) | |
tree | cbc0a0f8e740505fb14d13daa47a30070ff258ea | |
parent | c15a7826ecaa05bb36e934237b479c7ab2136037 (diff) |
modif generales claude
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8455 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | doc/AddRefMan-pre.tex | 4 | ||||
-rw-r--r-- | doc/Cases.tex | 3 | ||||
-rw-r--r-- | doc/Coercion.tex | 3 | ||||
-rwxr-xr-x | doc/Extraction.tex | 24 | ||||
-rwxr-xr-x | doc/Omega.tex | 103 | ||||
-rw-r--r-- | doc/Polynom.tex | 59 | ||||
-rwxr-xr-x | doc/RefMan-coi.tex | 2 | ||||
-rwxr-xr-x | doc/RefMan-com.tex | 90 | ||||
-rw-r--r-- | doc/RefMan-ext.tex | 35 | ||||
-rw-r--r-- | doc/RefMan-gal.tex | 47 | ||||
-rw-r--r-- | doc/RefMan-ide.tex | 69 | ||||
-rwxr-xr-x | doc/RefMan-int.tex | 40 | ||||
-rwxr-xr-x | doc/RefMan-lib.tex | 77 | ||||
-rw-r--r-- | doc/RefMan-ltac.tex | 674 | ||||
-rw-r--r-- | doc/RefMan-mod.tex | 144 | ||||
-rw-r--r-- | doc/RefMan-modr.tex | 2 | ||||
-rw-r--r-- | doc/RefMan-oth.tex | 44 | ||||
-rwxr-xr-x | doc/RefMan-pro.tex | 116 | ||||
-rw-r--r-- | doc/RefMan-tac.tex | 484 | ||||
-rw-r--r-- | doc/RefMan-tacex.tex | 2 | ||||
-rw-r--r-- | doc/Reference-Manual.tex | 18 | ||||
-rw-r--r-- | doc/Setoid.tex | 42 | ||||
-rw-r--r-- | doc/Translator.tex | 56 | ||||
-rw-r--r-- | doc/headers.tex | 1 | ||||
-rwxr-xr-x | doc/macros.tex | 9 |
25 files changed, 1494 insertions, 654 deletions
diff --git a/doc/AddRefMan-pre.tex b/doc/AddRefMan-pre.tex index bd661aeef..29632d67f 100644 --- a/doc/AddRefMan-pre.tex +++ b/doc/AddRefMan-pre.tex @@ -33,7 +33,7 @@ Manual. % manual of the tools he wrote for printing proofs in natural % language. At this time, French and English languages are supported. -\item[Omega] \texttt{Omega}, written by Pierre Crégut, solves a whole +\item[omega] \texttt{omega}, written by Pierre Crégut, solves a whole class of arithmetic problems. %\item[Program] The \texttt{Program} technology intends to inverse the @@ -41,7 +41,7 @@ Manual. % programs in \Coq. This chapter is due to Catherine Parent. {\bf This % feature is not available in {\Coq} version 7.} -\item[The {\tt Ring} tactic] This is a tactic to do AC rewriting. This +\item[The {\tt ring} tactic] This is a tactic to do AC rewriting. This chapter explains how to use it and how it works. The chapter is contributed by Patrick Loiseleur. diff --git a/doc/Cases.tex b/doc/Cases.tex index aacdd0c80..a8ab494c7 100644 --- a/doc/Cases.tex +++ b/doc/Cases.tex @@ -409,7 +409,8 @@ Set Printing Depth 50. \begin{coq_example} Fixpoint concat - (n: nat) (l:listn n) (m:nat) (l':listn m) {struct l} : listn (n + m) := + (n:nat) (l:listn n) (m:nat) + (l':listn m) {struct l} : listn (n + m) := match l, l' with | niln, x => x | consn n' a y, x => consn (n' + m) a (concat n' y m x) diff --git a/doc/Coercion.tex b/doc/Coercion.tex index 7a248f47f..be496adb2 100644 --- a/doc/Coercion.tex +++ b/doc/Coercion.tex @@ -358,7 +358,8 @@ We give an example of coercion between classes with parameters. %\begin{\small} \begin{coq_example} -Parameters (C : nat -> Set) (D : nat -> bool -> Set) (E : bool -> Set). +Parameters + (C : nat -> Set) (D : nat -> bool -> Set) (E : bool -> Set). Parameter f : forall n:nat, C n -> D (S n) true. Coercion f : C >-> D. Parameter g : forall (n:nat) (b:bool), D n b -> E b. diff --git a/doc/Extraction.tex b/doc/Extraction.tex index 12a9616e2..19be94560 100755 --- a/doc/Extraction.tex +++ b/doc/Extraction.tex @@ -538,19 +538,23 @@ let treesort leA_dec eqA_dec l = \end{verbatim} Let's test it: - +% Format.set_margin 72;; \begin{verbatim} # #use "heapsort.ml";; type sumbool = Left | Right type nat = O | S of nat type 'a tree = Tree_Leaf | Tree_Node of 'a * 'a tree * 'a tree type 'a list = Nil | Cons of 'a * 'a list -val merge : ('a -> 'a -> sumbool) -> 'b -> 'a list -> 'a list -> 'a list = - <fun> -val heap_to_list : ('a -> 'a -> sumbool) -> 'b -> 'a tree -> 'a list = <fun> -val insert : ('a -> 'a -> sumbool) -> 'b -> 'a tree -> 'a -> 'a tree = <fun> -val list_to_heap : ('a -> 'a -> sumbool) -> 'b -> 'a list -> 'a tree = <fun> -val treesort : ('a -> 'a -> sumbool) -> 'b -> 'a list -> 'a list = <fun> +val merge : + ('a -> 'a -> sumbool) -> 'b -> 'a list -> 'a list -> 'a list = <fun> +val heap_to_list : + ('a -> 'a -> sumbool) -> 'b -> 'a tree -> 'a list = <fun> +val insert : + ('a -> 'a -> sumbool) -> 'b -> 'a tree -> 'a -> 'a tree = <fun> +val list_to_heap : + ('a -> 'a -> sumbool) -> 'b -> 'a list -> 'a tree = <fun> +val treesort : + ('a -> 'a -> sumbool) -> 'b -> 'a list -> 'a list = <fun> \end{verbatim} One can remark that the argument of {\tt treesort} corresponding to @@ -566,9 +570,9 @@ val leAdec : 'a -> 'a -> sumbool = <fun> # let rec listn = function 0 -> Nil | n -> Cons(Random.int 10000,listn (n-1));; val listn : int -> int list = <fun> -# treesort leAdec () (listn 10);; -- : int list = Cons (136, Cons (760, Cons (1512, Cons (2776, Cons (3064, -Cons (4536, Cons (5768, Cons (7560, Cons (8856, Cons (8952, Nil)))))))))) +# treesort leAdec () (listn 9);; +- : int list = Cons (160, Cons (883, Cons (1874, Cons (3275, Cons + (5392, Cons (7320, Cons (8512, Cons (9632, Cons (9876, Nil))))))))) \end{verbatim} Some tests on longer lists (10000 elements) show that the program is diff --git a/doc/Omega.tex b/doc/Omega.tex index 69764336d..bbf17f630 100755 --- a/doc/Omega.tex +++ b/doc/Omega.tex @@ -1,29 +1,29 @@ -\achapter{\texttt{Omega}: a solver of quantifier-free problems in +\achapter{Omega: a solver of quantifier-free problems in Presburger Arithmetic} \aauthor{Pierre Crégut} \label{OmegaChapter} -\asection{Description of {\tt Omega}} -\tacindex{Omega} +\asection{Description of {\tt omega}} +\tacindex{omega} \label{description} -{\tt Omega}~solves a goal in Presburger arithmetic, ie a universally +{\tt omega} solves a goal in Presburger arithmetic, i.e. a universally quantified formula made of equations and inequations. Equations may be specified either on the type \verb=nat= of natural numbers or on the type \verb=Z= of binary-encoded integer numbers. Formulas on \verb=nat= are automatically injected into \verb=Z=. The procedure may use any hypothesis of the current proof session to solve the goal. -Multiplication is handled by {\tt Omega}~but only goals where at +Multiplication is handled by {\tt omega} but only goals where at least one of the two multiplicands of products is a constant are solvable. This is the restriction meaned by ``Presburger arithmetic''. If the tactic cannot solve the goal, it fails with an error message. In any case, the computation eventually stops. -\asubsection{Arithmetical goals recognized by {\tt Omega}} +\asubsection{Arithmetical goals recognized by {\tt omega}} -{\tt Omega}~applied only to quantifier-free formulas built from the +{\tt omega} applied only to quantifier-free formulas built from the connectors \begin{quote} @@ -42,13 +42,13 @@ on atomic formulas. Atomic formulas are built from the predicates \verb!=, <, <=, >, >=! \end{quote} - on \verb=Z=. In expressions of type \verb=nat=, {\tt Omega}~recognizes + on \verb=Z=. In expressions of type \verb=nat=, {\tt omega} recognizes \begin{quote} \verb!plus, minus, mult, pred, S, O! \end{quote} -and in expressions of type \verb=Z=, {\tt Omega}~recognizes +and in expressions of type \verb=Z=, {\tt omega} recognizes \begin{quote} \verb!+, -, *, Zsucc!, and constants. @@ -58,36 +58,39 @@ All expressions of type \verb=nat= or \verb=Z= not built on these operators are considered abstractly as if they were arbitrary variables of type \verb=nat= or \verb=Z=. -\asubsection{Messages from {\tt Omega}} +\asubsection{Messages from {\tt omega}} \label{errors} -When {\tt Omega}~does not solve the goal, one of the following errors +When {\tt omega} does not solve the goal, one of the following errors is generated: \begin{ErrMsgs} -\item \errindex{Omega can't solve this system}\\ + +\item \errindex{omega can't solve this system} + This may happen if your goal is not quantifier-free (if it is - universally quantified, try {\tt Intros} first; if it contains - existentials quantifiers too, {\tt Omega}\ is not strong enough to solve your + universally quantified, try {\tt intros} first; if it contains + existentials quantifiers too, {\tt omega} is not strong enough to solve your goal). This may happen also if your goal contains arithmetical - operators unknown from {\tt Omega}. Finally, your goal may be really - wrong ! + operators unknown from {\tt omega}. Finally, your goal may be really + wrong! -\item \errindex{Omega: Not a quantifier-free goal}\\ +\item \errindex{omega: Not a quantifier-free goal} + If your goal is universally quantified, you should first apply {\tt - Intro} as many time as needed. + intro} as many time as needed. -\item \errindex{Omega: Unrecognized predicate or connective:{\rm\sl ident}} +\item \errindex{omega: Unrecognized predicate or connective: {\sl ident}} -\item \errindex{Omega: Unrecognized atomic proposition:{\rm\sl prop}} +\item \errindex{omega: Unrecognized atomic proposition: {\sl prop}} -\item \errindex{Omega: Can't solve a goal with proposition variables} +\item \errindex{omega: Can't solve a goal with proposition variables} -\item \errindex{Omega: Unrecognized proposition} +\item \errindex{omega: Unrecognized proposition} -\item \errindex{Omega: Can't solve a goal with non-linear products} +\item \errindex{omega: Can't solve a goal with non-linear products} -\item \errindex{Omega: Can't solve a goal with equality on {\rm\sl type}} +\item \errindex{omega: Can't solve a goal with equality on {\sl type}} \end{ErrMsgs} @@ -103,25 +106,24 @@ is generated: % procedure (see \ref{technical}). % \end{itemize} -% \comindex{Set Omega Time} -% \comindex{UnSet Omega Time} -% \comindex{Switch Omega Time} -% \comindex{Set Omega System} -% \comindex{UnSet Omega System} -% \comindex{Switch Omega System} -% \comindex{Set Omega Action} -% \comindex{UnSet Omega Action} -% \comindex{Switch Omega Action} +% \comindex{Set omega Time} +% \comindex{UnSet omega Time} +% \comindex{Switch omega Time} +% \comindex{Set omega System} +% \comindex{UnSet omega System} +% \comindex{Switch omega System} +% \comindex{Set omega Action} +% \comindex{UnSet omega Action} +% \comindex{Switch omega Action} - Use {\tt Set Omega {\rm\sl flag}} to set the flag - {\rm\sl flag}. Use {\tt Unset Omega {\rm\sl flag}} to unset it and -{\tt Switch Omega {\rm\sl flag}} to toggle it. +% Use {\tt Set omega {\rm\sl flag}} to set the flag +% {\rm\sl flag}. Use {\tt Unset omega {\rm\sl flag}} to unset it and +% {\tt Switch omega {\rm\sl flag}} to toggle it. -\section{Using {\tt Omega}} +\section{Using {\tt omega}} -The tactic {\tt Omega}~does not belong to the core system. It should be +The {\tt omega} tactic does not belong to the core system. It should be loaded by - \begin{coq_example*} Require Import Omega. Open Scope Z_scope. @@ -167,7 +169,7 @@ intro; omega. \asubsection{Overview of the {\it OMEGA} decision procedure} -The {\it OMEGA} decision procedure involved in the {\tt Omega}~tactic uses +The {\it OMEGA} decision procedure involved in the {\tt omega} tactic uses a small subset of the decision procedure presented in \begin{quote} @@ -176,8 +178,7 @@ algorithm for dependence analysis", William Pugh, Communication of the ACM , 1992, p 102-114. \end{quote} -Here is an overview. -The reader is refered to the original paper for more information. +Here is an overview, look at the original paper for more information. \begin{itemize} @@ -187,13 +188,13 @@ The reader is refered to the original paper for more information. equal to one. \item Note that each inequation defines a half space in the space of real value of the variables. -\item Inequations are solved by projecting on the hyperspace defined by - cancelling one of the variable. - They are partitioned according to the sign of - the coefficient of the eliminated variable. Pairs of inequations from - different classes define a new edge in the projection. -\item Redundant inequations are eliminated or merged in new equations that can - be eliminated by the Banerjee test. + \item Inequations are solved by projecting on the hyperspace + defined by cancelling one of the variable. They are partitioned + according to the sign of the coefficient of the eliminated + variable. Pairs of inequations from different classes define a + new edge in the projection. + \item Redundant inequations are eliminated or merged in new + equations that can be eliminated by the Banerjee test. \item The last two steps are iterated until a contradiction is reached (success) or there is no more variable to eliminate (failure). @@ -211,10 +212,10 @@ decision procedure is only partial. \item Much too slow. -\item Certainely other bugs! You can report them to +\item Certainly other bugs! You can report them to \begin{quote} - \verb=Pierre.Cregut@cnet.francetelecom.fr= + \url{Pierre.Cregut@cnet.francetelecom.fr} \end{quote} \end{itemize} diff --git a/doc/Polynom.tex b/doc/Polynom.tex index 02c49577b..37633d199 100644 --- a/doc/Polynom.tex +++ b/doc/Polynom.tex @@ -3,11 +3,11 @@ \label{ring} \tacindex{ring} -This chapter presents the \texttt{Ring} tactic. +This chapter presents the \texttt{ring} tactic. \asection{What does this tactic?} -\texttt{Ring} does associative-commutative rewriting in ring and semi-ring +\texttt{ring} does associative-commutative rewriting in ring and semi-ring structures. Assume you have two binary functions $\oplus$ and $\otimes$ that are associative and commutative, with $\oplus$ distributive on $\otimes$, and two constants 0 and 1 that are unities for $\oplus$ and @@ -24,9 +24,9 @@ different, i.e. each monomial in the sum is strictly less than the following monomial according to the lexicographic order. It is an easy theorem to show that every polynomial is equivalent (modulo the ring properties) to exactly one canonical sum. This canonical sum is called -the \textit{normal form} of the polynomial. So what does \texttt{Ring}? It +the \textit{normal form} of the polynomial. So what does \texttt{ring}? It normalizes polynomials over any ring or semi-ring structure. The basic -utility of \texttt{Ring} is to simplify ring expressions, so that the user +use of \texttt{ring} is to simplify ring expressions, so that the user does not have to deal manually with the theorems of associativity and commutativity. @@ -91,7 +91,7 @@ this paragraph and use the tactic according to your intuition. \asection{Concrete usage in \Coq} Under a session launched by \texttt{coqtop} or \texttt{coqtop -full}, -load the \texttt{Ring} files with the command: +load the \texttt{ring} files with the command: \begin{quotation} \begin{verbatim} @@ -103,23 +103,23 @@ It does not work under \texttt{coqtop -opt} because the compiled ML objects used by the tactic are not linked in this binary image, and dynamic loading of native code is not possible in \ocaml. -In order to use \texttt{Ring} on naturals, load \texttt{ArithRing} +In order to use \texttt{ring} on naturals, load \texttt{ArithRing} instead; for binary integers, load the module \texttt{ZArithRing}. Then, to normalize the terms $term_1$, \dots, $term_n$ in the current subgoal, use the tactic: \begin{quotation} -\texttt{Ring} $term_1$ \dots{} $term_n$ +\texttt{ring} $term_1$ \dots{} $term_n$ \end{quotation} -\tacindex{Ring} +\tacindex{ring} Then the tactic guesses the type of given terms, the ring theory to use, the variables map, and replace each term with its normal form. The variables map is common to all terms -\Warning \texttt{Ring $term_1$; Ring $term_2$} is not equivalent to -\texttt{Ring $term_1$ $term_2$}. In the latter case the variables map +\Warning \texttt{ring $term_1$; ring $term_2$} is not equivalent to +\texttt{ring $term_1$ $term_2$}. In the latter case the variables map is shared between the two terms, and common subterm $t$ of $term_1$ and $term_2$ will have the same associated variable number. @@ -135,7 +135,7 @@ and $term_2$ will have the same associated variable number. \end{ErrMsgs} \begin{Variants} -\item \texttt{Ring} +\item \texttt{ring} That works if the current goal is an equality between two polynomials. It will normalize both sides of the @@ -150,7 +150,7 @@ and $term_2$ will have the same associated variable number. \asection{Add a ring structure} It can be done in the \Coq toplevel (No ML file to edit and to link -with \Coq). First, \texttt{Ring} can handle two kinds of structure: +with \Coq). First, \texttt{ring} can handle two kinds of structure: rings and semi-rings. Semi-rings are like rings without an opposite to addition. Their precise specification (in \gallina) can be found in the file @@ -303,8 +303,8 @@ This allows automatic detection of the theory used to achieve the normalization. On popular demand, we can change that and allow several ring structures on the same set. -The table of theories of \texttt{Ring} is compatible with the \Coq\ -sectioning mechanism. If you declare a Ring inside a section, the +The table of ring theories is compatible with the \Coq\ +sectioning mechanism. If you declare a ring inside a section, the declaration will be thrown away when closing the section. And when you load a compiled file, all the \texttt{Add Ring} commands of this file that are not inside a section will be loaded. @@ -321,15 +321,14 @@ load the module \texttt{ZArithRing}. \asection{How does it work?} -The code of \texttt{Ring} a good example of tactic written using -\textit{reflection} (or \textit{internalization}, it is -synonymous). What is reflection? Basically, it is writing \Coq\ tactics -in \Coq, rather than in \ocaml. From the philosophical point of view, -it is using the ability of the Calculus of Constructions to speak and -reason about itself. -For the \texttt{Ring} tactic we used -\Coq\ as a programming language and also as a proof environment to build a -tactic and to prove it correctness. +The code of \texttt{ring} is a good example of tactic written using +\textit{reflection} (or \textit{internalization}, it is synonymous). +What is reflection? Basically, it is writing \Coq{} tactics in \Coq, +rather than in \ocaml. From the philosophical point of view, it is +using the ability of the Calculus of Constructions to speak and reason +about itself. For the \texttt{ring} tactic we used \Coq\ as a +programming language and also as a proof environment to build a tactic +and to prove it correctness. The interested reader is strongly advised to have a look at the file \texttt{Ring\_normalize.v}. Here a type for polynomials is defined: @@ -366,9 +365,9 @@ its correctness w.r.t interpretation, that is: \begin{small} \begin{flushleft} \begin{verbatim} -Theorem polynomial_simplify_correct : (v:(varmap A))(p:polynomial) +Theorem polynomial_simplify_correct : forall (v:(varmap A))(p:polynomial) (interp v (polynomial_simplify p)) - ==(interp v p). + =(interp v p). \end{verbatim} \end{flushleft} \end{small} @@ -405,7 +404,7 @@ $\beta\delta\iota$ simplification extended with AC rewriting rules. Basically, the proof is only the application of the main correctness theorem to well-chosen arguments. -\asection{History of \texttt{Ring}} +\asection{History of \texttt{ring}} First Samuel Boutin designed the tactic \texttt{ACDSimpl}. This tactic did lot of rewriting. But the proofs @@ -439,7 +438,7 @@ reasoning (see \ref{DiscussReflection}). He also wrote a few ML code for the \texttt{Add Ring} command, that allow to register new rings dynamically. -Proofs terms generated by \texttt{Ring} are quite small, they are +Proofs terms generated by \texttt{ring} are quite small, they are linear in the number of $\oplus$ and $\otimes$ operations in the normalized terms. Type-checking those terms requires some time because it makes a large use of the conversion rule, but @@ -449,7 +448,7 @@ memory requirements are much smaller. \label{DiscussReflection} Efficiency is not the only motivation to use reflection -here. \texttt{Ring} also deals with constants, it rewrites for example the +here. \texttt{ring} also deals with constants, it rewrites for example the expression $34 + 2*x -x + 12$ to the expected result $x + 46$. For the tactic \texttt{ACDSimpl}, the only constants were 0 and 1. So the expression $34 + 2*(x - 1) + 12$ is interpreted as @@ -461,12 +460,12 @@ result. Here rewriting is not sufficient: you have to do some kind of reduction (some kind of \textit{computation}) to achieve the normalization. -The tactic \texttt{Ring} is not only faster than a classical one: +The tactic \texttt{ring} is not only faster than a classical one: using reflection, we get for free integration of computation and reasoning that would be very complex to implement in the classic fashion. Is it the ultimate way to write tactics? -The answer is: yes and no. The \texttt{Ring} tactic +The answer is: yes and no. The \texttt{ring} tactic uses intensively the conversion rule of \CIC, that is replaces proof by computation the most as it is possible. It can be useful in all situations where a classical tactic diff --git a/doc/RefMan-coi.tex b/doc/RefMan-coi.tex index ef5907016..120c1201e 100755 --- a/doc/RefMan-coi.tex +++ b/doc/RefMan-coi.tex @@ -173,7 +173,7 @@ 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! +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). diff --git a/doc/RefMan-com.tex b/doc/RefMan-com.tex index 4f88f600d..da21ec467 100755 --- a/doc/RefMan-com.tex +++ b/doc/RefMan-com.tex @@ -94,121 +94,151 @@ The following command-line options are recognized by the commands {\tt coqc} and {\tt coqtop}: \begin{description} -\item[{\tt -byte}]\ \\ +\item[{\tt -byte}]\ + Run the byte-code version of \Coq{}. -\item[{\tt -opt}]\ \\ +\item[{\tt -opt}]\ + Run the native-code version of \Coq{}. -\item[{\tt -I} {\em directory}, {\tt -include} {\em directory}]\ \\ +\item[{\tt -I} {\em directory}, {\tt -include} {\em directory}]\ + Add {\em directory} to the searched directories when looking for a file. -\item[{\tt -R} {\em directory} {\dirpath}]\ \\ +\item[{\tt -R} {\em directory} {\dirpath}]\ + This maps the subdirectory structure of physical {\em directory} to logical {\dirpath} and adds {\em directory} and its subdirectories to the searched directories when looking for a file. -\item[{\tt -is} {\em file}, {\tt -inputstate} {\em file}]\ \\ +\item[{\tt -is} {\em file}, {\tt -inputstate} {\em file}]\ + Cause \Coq~to use the state put in the file {\em file} as its input state. The default state is {\em initial.coq}. Mainly useful to build the standard input state. -\item[{\tt -nois}]\ \\ +\item[{\tt -nois}]\ + Cause \Coq~to begin with an empty state. Mainly useful to build the standard input state. -\item[{\tt -notactics}]\ \\ +\item[{\tt -notactics}]\ + Forbid the dynamic loading of tactics. -\item[{\tt -init-file} {\em file}]\ \\ +\item[{\tt -init-file} {\em file}]\ + Take {\em file} as the resource file. -\item[{\tt -q}]\ \\ +\item[{\tt -q}]\ + Cause \Coq~not to load the resource file. -\item[{\tt -user} {\em username}]\ \\ +\item[{\tt -user} {\em username}]\ + Take resource file of user {\em username} (that is \verb+~+{\em username}{\tt /.coqrc.7.0}) instead of yours. -\item[{\tt -load-ml-source} {\em file}]\ \\ +\item[{\tt -load-ml-source} {\em file}]\ + Load the Caml source file {\em file}. -\item[{\tt -load-ml-object} {\em file}]\ \\ +\item[{\tt -load-ml-object} {\em file}]\ + Load the Caml object file {\em file}. -\item[{\tt -load-vernac-source} {\em file}]\ \\ +\item[{\tt -load-vernac-source} {\em file}]\ + Load \Coq~file {\em file}{\tt .v} -\item[{\tt -load-vernac-object} {\em file}]\ \\ +\item[{\tt -load-vernac-object} {\em file}]\ + Load \Coq~compiled file {\em file}{\tt .vo} %\item[{\tt -preload} {\em file}]\ \\ %Add {\em file}{\tt .vo} to the files to be loaded and opened %before making the initial state. % -\item[{\tt -require} {\em file}]\ \\ +\item[{\tt -require} {\em file}]\ + Load \Coq~compiled file {\em file}{\tt .vo} and import it ({\tt Require} {\em file}). -\item[{\tt -compile} {\em file}]\ \\ +\item[{\tt -compile} {\em file}]\ + This compiles file {\em file}{\tt .v} into {\em file}{\tt .vo}. This option implies options {\tt -batch} and {\tt -silent}. It is only available for {\tt coqtop}. -%\item[{\tt -compile-verbose} {\em file}]\ \\ +%\item[{\tt -compile-verbose} {\em file}]\ +@ % This compiles file {\em file}{\tt .v} into {\em file}{\tt .vo} with % a copy of the contents of the file on standard input. % This option implies options {\tt -batch} and {\tt -silent}. It is % only available for {\tt coqtop}. -\item[{\tt -batch}]\ \\ +\item[{\tt -batch}]\ + Batch mode : exit just after arguments parsing. This option is only used by {\tt coqc}. -\item[{\tt -debug}]\ \\ +\item[{\tt -debug}]\ + Switch on the debug flag. -\item[{\tt -emacs}]\ \\ +\item[{\tt -emacs}]\ + Tells \Coq\ it is executed under Emacs. -\item[{\tt -db}]\ \\ +\item[{\tt -db}]\ + Launch \Coq\ under the Objective Caml debugger (provided that \Coq\ has been compiled for debugging; see next chapter). -\item[{\tt -impredicative-set}]\ \\ +\item[{\tt -impredicative-set}]\ + Change the logical theory of {\Coq} by declaring the sort {\tt Set} impredicative; warning: this is known to be inconsistent with some standard axioms of classical mathematics such as the functional - axiom of choice or the principle of description\\ + axiom of choice or the principle of description + +\item[{\tt -dont-load-proofs}]\ -\item[{\tt -dont-load-proofs}]\ \\ This avoids loading in memory the proofs of opaque theorems resulting in a smaller memory requirement and faster compilation; warning: this invalidates some features such as the extraction tool. -\item[{\tt -image} {\em file}]\ \\ +\item[{\tt -image} {\em file}]\ + This option sets the binary image to be used to be {\em file} instead of the standard one. Not of general use. -\item[{\tt -bindir} {\em directory}]\ \\ +\item[{\tt -bindir} {\em directory}]\ + Set the directory containing \Coq\ binaries. It is equivalent to do \texttt{export COQBIN=}{\em directory} before lauching \Coq. -\item[{\tt -libdir} {\em file}]\ \\ +\item[{\tt -libdir} {\em file}]\ + Set the directory containing \Coq\ libraries. It is equivalent to do \texttt{export COQLIB=}{\em directory} before lauching \Coq. -\item[{\tt -where}]\ \\ +\item[{\tt -where}]\ + Print the \Coq's standard library location and exit. -\item[{\tt -v}]\ \\ +\item[{\tt -v}]\ + Print the \Coq's version and exit. -\item[{\tt -h}, {\tt --help}]\ \\ +\item[{\tt -h}, {\tt --help}]\ + Print a short usage and exit. + \end{description} % {\tt coqtop} owns an additional option: diff --git a/doc/RefMan-ext.tex b/doc/RefMan-ext.tex index a5cc9f7e4..568f8713b 100644 --- a/doc/RefMan-ext.tex +++ b/doc/RefMan-ext.tex @@ -14,20 +14,21 @@ macro is more general than the usual record types, since it allows also for ``manifest'' expressions. In this sense, the \verb+Record+ construction allows to define ``signatures''. -\begin{figure} -\begin{tabular}{|lcl|} -\hline +\begin{figure}[h] +\begin{center} +\fbox{\begin{minipage}{0.95\textwidth} +\begin{tabular}{lcl} {\sentence} & ++= & {\record}\\ & & \\ -{\record} & ::= & {\tt Record} {\ident} \sequence{\binderlet}{} {\tt :} {\sort} - \verb.:=. \zeroone{\ident} \verb!{! - \zeroone{\nelist{\field}{;}} - \verb!}! \verb:.:\\ +{\record} & ::= & {\tt Record} {\ident} \sequence{\binderlet}{} : + {\sort} := \zeroone{\ident} \{ \zeroone{\nelist{\field}{;}} + \} . \\ & & \\ -{\field} & ::= & {\name} \verb.:. {\type} \\ - & $|$ & {\name} {\typecstr} \verb.:=. {\term} \\ -\hline +{\field} & ::= & {\name} : {\type} \\ + & $|$ & {\name} {\typecstr} := {\term} \end{tabular} +\end{minipage}} +\end{center} \caption{Syntax for the definition of {\tt Record}} \label{record-syntax} \end{figure} @@ -79,18 +80,24 @@ Record Rat : Set := mkRat Remark here that the field \verb+Rat_cond+ depends on the field \verb+bottom+. -Let us now see the work done by the {\tt Record} macro. First the -macro generates an inductive definition with just one constructor: +Let us now see the work done by the {\tt Record} macro. +First the macro generates an inductive definition +with just one constructor: \medskip \noindent +{\tt Inductive {\ident} {\binderlet} : {\sort} := \\ +\mbox{}\hspace{0.4cm} {\ident$_0$} : forall ({\ident$_1$}:{\term$_1$}) .. +({\ident$_n$}:{\term$_n$}), {\ident} {\rm\sl params}.} +\medskip + +Let us now see the work done by the {\tt Record} macro. First the +macro generates an inductive definition with just one constructor: \begin{tabular}{l} {\tt Inductive {\ident} {\params} :{\sort} :=} \\ ~~~~{\tt {\ident$_0$} ({\ident$_1$}:{\term$_1$}) .. ({\ident$_n$}:{\term$_n$}).} \end{tabular} -\medskip - To build an object of type {\ident}, one should provide the constructor {\ident$_0$} with $n$ terms filling the fields of diff --git a/doc/RefMan-gal.tex b/doc/RefMan-gal.tex index 264987c50..93045fae6 100644 --- a/doc/RefMan-gal.tex +++ b/doc/RefMan-gal.tex @@ -212,10 +212,10 @@ chapter \ref{Cic}. Extensions of this syntax are given in chapter \ref{Gallina-extension}. How to customize the syntax is described in chapter \ref{Addoc-syntax}. +\begin{figure}[htbp] \begin{center} -\begin{figure}[htb] -\begin{tabular}{|lcl@{~~~~~}r|} -\hline +\fbox{\begin{minipage}{0.95\textwidth} +\begin{tabular}{lcl@{~~~~~}r} {\term} & ::= & {\tt forall} {\binderlist} {\tt ,} {\term} &(\ref{products})\\ & $|$ & {\tt fun} {\binderlist} {\tt =>} {\term} &(\ref{abstractions})\\ @@ -270,19 +270,20 @@ chapter \ref{Addoc-syntax}. {\sort} & ::= & {\tt Prop} ~$|$~ {\tt Set} ~$|$~ {\tt Type} &\\ \hline \end{tabular} +\end{minipage}} +\end{center} \caption{Syntax of terms} \label{term-syntax} \index{term@{\term}} \index{sort@{\sort}} \end{figure} -\end{center} -\begin{center} \begin{figure}[htb] -\begin{tabular}{|lcl|} -\hline +\begin{center} +\fbox{\begin{minipage}{0.95\textwidth} +\begin{tabular}{lcl} {\idparams} & ::= & {\ident} \sequence{\binderlet}{} {\typecstr} \\ &&\\ {\fixpointbodies} & ::= & @@ -316,13 +317,14 @@ chapter \ref{Addoc-syntax}. & $|$ & {\qualid} \\ & $|$ & {\tt \_} \\ & $|$ & {\num} \\ - & $|$ & {\tt (} \nelist{\pattern}{,} {\tt )} \\ -\hline + & $|$ & {\tt (} \nelist{\pattern}{,} {\tt )} \end{tabular} +\end{minipage}} +\end{center} \caption{Syntax of terms (continued)} \label{term-syntax-aux} \end{figure} -\end{center} + %%%%%%% @@ -408,6 +410,11 @@ of let-binders (the first one not being a variable with value), or {\ident$_1$}\ldots{\ident$_n$}\,{\tt :}\,{\type} if all variables share the same type. +{\Coq} terms are typed. {\Coq} types are recognized by the same +syntactic class as {\term}. We denote by {\type} the semantic subclass +of types inside the syntactic class {\term}. +\index{type@{\type}} + \subsection{Abstractions} \label{abstractions} \index{abstractions} @@ -560,14 +567,10 @@ definition have a special syntax: ``{\tt let fix}~$f$~{\ldots}~{\tt \section{The Vernacular} \label{Vernacular} -Figure \ref{sentences-syntax} describes {\em The Vernacular} which is the -language of commands of \gallina. A sentence of the vernacular -language, like in many natural languages, begins with a capital letter -and ends with a dot. -\begin{figure} -\label{sentences-syntax} -\begin{tabular}{|lcl|} -\hline +\begin{figure}[tbp] +\begin{center} +\fbox{\begin{minipage}{0.95\textwidth} +\begin{tabular}{lcl} {\sentence} & ::= & {\declaration} \\ & $|$ & {\definition} \\ & $|$ & {\inductive} \\ @@ -611,13 +614,13 @@ and ends with a dot. &&\\ {\proof} & ::= & {\tt Proof} {\tt .} {\dots} {\tt Qed} {\tt .}\\ & $|$ & {\tt Proof} {\tt .} {\dots} {\tt Defined} {\tt .}\\ - & $|$ & {\tt Proof} {\tt .} {\dots} {\tt Admitted} {\tt .}\\ -\hline + & $|$ & {\tt Proof} {\tt .} {\dots} {\tt Admitted} {\tt .} \end{tabular} +\end{minipage}} +\end{center} \caption{Syntax of sentences} +\label{sentences-syntax} \end{figure} -The different kinds of command are described hereafter. They all suppose -that the terms occurring in the sentences are well-typed. %% %% Axioms and Parameters diff --git a/doc/RefMan-ide.tex b/doc/RefMan-ide.tex index 686e60e7d..d0d9b1ee3 100644 --- a/doc/RefMan-ide.tex +++ b/doc/RefMan-ide.tex @@ -6,7 +6,7 @@ The \Coq{} Integrated Development Environment is a graphical tool, to be used as a user-friendly replacement to \texttt{coqtop}. Its main purpose is to allow the user to navigate forward and backward into a \Coq{} vernacular file, executing corresponding commands or undoing -them respectively. CREDITS ? Proof general, lablgtk, ... +them respectively. % CREDITS ? Proof general, lablgtk, ... \coqide{} is run by typing the command \verb|coqide| on the command line. Without argument, the main screen is displayed with an ``unnamed @@ -26,7 +26,7 @@ obviously no meaning for \coqide{} being ignored. \fi %END LATEX \end{center} -\caption{Coqide main screen} +\caption{\coqide{} main screen} \label{fig:coqide} \end{figure} @@ -39,7 +39,7 @@ prove are displayed. The lower right window is the \emph{message window}, where various messages resulting from commands are displayed. At the bottom is the status bar. -\section{Managing files and buffers} +\section{Managing files and buffers, basic edition} In the script window, you may open arbitrarily many buffers to edit. The \emph{File} menu allows you to open files or create some, @@ -48,6 +48,13 @@ 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 may be edited as in any text editor, and classical basic +editing commands (Copy/Paste, \ldots) are available in the \emph{Edit} +menu. \coqide{} offers only basic editing commands, so if you need +more complex editing commands, you may launch your favorite text +editor on the current buffer, using the \emph{Edit/External Editor} +menu. + \section{Interactive navigation into \Coq{} scripts} The running buffer is the one where navigation takes place. The @@ -61,8 +68,8 @@ location of the error is emphasized by a red underline. On Figure~\ref{fig:coqide}, the running buffer is \verb|Fermat.v|, all commands until the \verb|Theorem| have been already executed, and the user tried to go forward executing \verb|Induction n|. That command -failed because no such tactic exist (you remember that tactics in V8.0 -are lowercase, right ?), and the wrong word is underlined. +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 you ever want to modify something you have to go backward using the up @@ -75,9 +82,9 @@ 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. -If you ever try to execute a long-running command, such as an -\verb|intuition eauto with *|, and would like to abort it before its -end, you may use the interrupt button, the red cross-like. +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. @@ -87,11 +94,11 @@ the menu, where their keyboard shortcuts are given. The menu \texttt{Try Tactics} provides some features for automatically trying to solve the current goal using simple tactics. If such a -tactics succeeds in solving the goal, then its text is automatically +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, with a light -bulb shape. The set of tactics tried by the wizard is customizable 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 the preferences. These tactics are general ones, in particular they do not refer to @@ -104,8 +111,8 @@ preferences if undesirable. \section{Vernacular commands, templates} The \texttt{Templates} menu allows to use shortcuts to insert -vernacular commands. This is a nice menu to use if you are not sure of -the spelling of the command you want. +vernacular commands. This is a nice way to proceed if you are not sure +of the spelling of the command you want. Moreover, this menu offers some \emph{templates} which will automatic insert a complex command like Fixpoint with a convenient shape for its @@ -124,7 +131,7 @@ arguments. \fi %END LATEX \end{center} -\caption{Coqide main screen} +\caption{\coqide{}: the query window} \label{fig:querywindow} \end{figure} @@ -139,7 +146,7 @@ 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{SearchAbout} on some identifier is to select it using the mouse, and pressing \verb|F2|. This will -both make appear the query window ans run the \texttt{SearchAbout} in +both make appear the query window and run the \texttt{SearchAbout} 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 @@ -148,11 +155,13 @@ print its definition. \section{Compilation} -The \verb|Compile| menu offers direct commands to compile the current -buffer, compile a set of files using \verb|make|, and creating a -\verb|makefile| using \verb|coq_makefile|. - -TODO: \verb|Next error| ! +The \verb|Compile| menu offers direct commands to: +\begin{itemize} +\item compile the current buffer +\item run a compilation using \verb|make| +\item go to the last compilation error +\item create a \verb|makefile| using \verb|coq_makefile|. +\end{itemize} \section{Customizations} @@ -160,7 +169,7 @@ You may customize your environment using menu \texttt{Edit/Preferences}. A new window will be displayed, with several customization sections presented as a notebook. -The first section is the select the text font used for scripts, goal +The first section is for selecting the text font used for scripts, goal and message windows. The second section is devoted to file management: you may @@ -183,6 +192,24 @@ The last section is for miscellaneous boolean settings, such as the ``contextual menu on goals'' feature presented in Section~\ref{sec:trytactics}. +Notice that these settings are saved in the file \verb|.coqiderc| of +your home directory. + +A gtk2 accelerator keymap is saved under the name \verb|.coqide.keys|. +This file should not be edited manually: to modify a given menu +shortcut, go to the corresponding menu item without releasing the +mouse button, press the key you want for the new shortcut, and release +the mouse button afterwards. + +For experts: it is also possible to set up a specific gtk resource +file, under the name \verb|.coqide-gtk2rc|, following the gtk2 +resources syntax +\url{http://developer.gnome.org/doc/API/2.0/gtk/gtk-Resource-Files.html}. +Such a default resource file exists in the \Coq{} library, you may +copy this file into your home directory, and edit it using any text +editor, \coqide{} itself for example. + + % $Id$ %%% Local Variables: diff --git a/doc/RefMan-int.tex b/doc/RefMan-int.tex index 1595dccf5..2331b6226 100755 --- a/doc/RefMan-int.tex +++ b/doc/RefMan-int.tex @@ -11,17 +11,16 @@ the advanced user. %The system \Coq\ is designed to develop mathematical proofs. It can be %used by mathematicians to develop mathematical theories and by %computer scientists to write formal specifications, -The system \Coq\ is designed to develop mathematical proofs, and -especially to write formal specifications, -programs and to verify that programs are correct with respect to their -specification. It provides a specification language named \gallina. Terms of -\gallina\ can represent programs as well as properties of these -programs and proofs of these properties. Using the so-called -\textit{Curry-Howard isomorphism}, programs, properties and proofs are -formalized in the same -language called \textit{Calculus of Inductive Constructions}, that is -a $\lambda$-calculus with a rich type system. -All logical judgments in \Coq\ are typing judgments. The very heart of the Coq +The \Coq{} system is designed to develop mathematical proofs, and +especially to write formal specifications, programs and to verify that +programs are correct with respect to their specification. It provides +a specification language named \gallina. Terms of \gallina\ can +represent programs as well as properties of these programs and proofs +of these properties. Using the so-called \textit{Curry-Howard + isomorphism}, programs, properties and proofs are formalized in the +same language called \textit{Calculus of Inductive Constructions}, +that is a $\lambda$-calculus with a rich type system. All logical +judgments in \Coq\ are typing judgments. The very heart of the Coq system is the type-checking algorithm that checks the correctness of proofs, in other words that checks that a program complies to its specification. \Coq\ also provides an interactive proof assistant to @@ -32,12 +31,7 @@ interpretation of a command language called \textit{the vernacular}. \Coq\ has an interactive mode in which commands are interpreted as the user types them in from the keyboard and a compiled mode where -commands are processed from a file. Other modes of interaction with -\Coq\ are possible, through an emacs shell window, an emacs generic -user-interface for proof assistant (ProofGeneral~\cite{ProofGeneral}) -or through a customized interface (PCoq~\cite{Pcoq}). -These facilities are not documented here. -There is also a \Coq{} Integrated Development Environment described in chapter~\ref{Addoc-coqide} +commands are processed from a file. \begin{itemize} \item The interactive mode may be used as a debugging mode in which @@ -54,6 +48,13 @@ There is also a \Coq{} Integrated Development Environment described in chapter~\ \end{itemize} These two modes are documented in chapter \ref{Addoc-coqc}. +Other modes of interaction with \Coq{} are possible: through an emacs +shell window, an emacs generic user-interface for proof assistant +(ProofGeneral~\cite{ProofGeneral}) or through a customized interface +(PCoq~\cite{Pcoq}). These facilities are not documented here. There +is also a \Coq{} Integrated Development Environment described in +Chapter~\ref{Addoc-coqide}. + \section*{How to read this book} This is a Reference Manual, not a User Manual, then it is not made for a @@ -67,7 +68,7 @@ below. theorems and proofs in the Calculus of Inductive Constructions. Chapter~\ref{Theories} describes the standard library of \Coq. Chapter~\ref{Cic} is a mathematical description of the - formalism. Chapter~\ref{Mod} describes the module system. + formalism. Chapter~\ref{chapter:Modules} describes the module system. \item The second part describes the proof engine. It is divided in five chapters. Chapter~\ref{Vernacular-commands} presents all @@ -101,7 +102,8 @@ corresponds to the Chapter~\ref{Addoc-syntax}. \end{itemize} At the end of the document, after the global index, the user can find -a tactic index and a vernacular command index. +a tactic index and a vernacular command index, and an index of error +messages. \section*{List of additional documentation} diff --git a/doc/RefMan-lib.tex b/doc/RefMan-lib.tex index 13f9bd64f..f9b4d2ae0 100755 --- a/doc/RefMan-lib.tex +++ b/doc/RefMan-lib.tex @@ -93,13 +93,12 @@ constructions). They are equipped with an appealing syntax enriching the extension is shown on figure \ref{formulas-syntax}. \begin{figure} -\label{formulas-syntax} \begin{center} -\begin{tabular}{|lclr|} -\hline +\fbox{\begin{minipage}{0.95\textwidth} +\begin{tabular}{rclr} {\form} & ::= & {\tt True} & ({\tt True})\\ & $|$ & {\tt False} & ({\tt False})\\ - & $|$ & {\verb|~|} {\form} & ({\tt not})\\ + & $|$ & {\tt\char'176} {\form} & ({\tt not})\\ & $|$ & {\form} {\tt /$\backslash$} {\form} & ({\tt and})\\ & $|$ & {\form} {\tt $\backslash$/} {\form} & ({\tt or})\\ & $|$ & {\form} {\tt ->} {\form} & (\em{primitive implication})\\ @@ -111,21 +110,28 @@ extension is shown on figure \ref{formulas-syntax}. & $|$ & {\tt exists2} {\ident} \zeroone{{\tt :} {\specif}} {\tt ,} {\form} {\tt \&} {\form} & ({\tt ex2})\\ & $|$ & {\term} {\tt =} {\term} & ({\tt eq})\\ - & $|$ & {\term} {\tt =} {\term} {\tt :>} {\specif} & ({\tt eq})\\ -\hline + & $|$ & {\term} {\tt =} {\term} {\tt :>} {\specif} & ({\tt eq}) \end{tabular} +\end{minipage}} \end{center} +\caption{Syntax of formulas} +\label{formulas-syntax} +\end{figure} -\medskip +The basic library of {\Coq} comes with the definitions of standard +(intuitionistic) logical connectives (they are defined as inductive +constructions). They are equipped with an appealing syntax enriching the +(subclass {\form}) of the syntactic class {\term}. The syntax +extension +\footnote{This syntax is defined in module {\tt LogicSyntax}} + is shown on figure \ref{formulas-syntax}. -\Rem The implication is not defined but primitive +\Rem Implication is not defined but primitive (it is a non-dependent product of a proposition over another proposition). There is also a primitive universal quantification (it is a dependent product over a proposition). The primitive universal quantification allows both first-order and higher-order quantification. -\caption{Syntax of formulas} -\end{figure} \subsubsection{Propositional Connectives} \label{Connectives} \index{Connectives} @@ -297,11 +303,9 @@ Abort. \subsection{Datatypes} \label{Datatypes} In the basic library, we find the definition\footnote{They are in {\tt -Datatypes.v}} -of the basic data-types of programming, -again defined as inductive constructions over the sort -\verb:Set:. Some of them come with a special syntax shown on figure -\ref{specif-syntax}. + Datatypes.v}} of the basic data-types of programming, again +defined as inductive constructions over the sort \verb:Set:. Some of +them come with a special syntax shown on Figure~\ref{specif-syntax}. \subsubsection{Programming} \label{Programming} \index{Programming} @@ -371,7 +375,7 @@ End projections. The following notions\footnote{They are defined in module {\tt Specif.v}} allows to build new datatypes and specifications. They are available with the syntax shown on -figure \ref{specif-syntax}\footnote{This syntax can be found in the module +Figure~\ref{specif-syntax}\footnote{This syntax can be found in the module {\tt SpecifSyntax.v}}. For instance, given \verb|A:Set| and \verb|P:A->Prop|, the construct @@ -454,10 +458,9 @@ Inductive sumor (A:Set) (B:Prop) : Set := inleft (_:A) | inright (_:B). \end{coq_example*} \begin{figure} -\label{specif-syntax} \begin{center} -\begin{tabular}{|lclr|} -\hline +\fbox{\begin{minipage}{0.95\textwidth} +\begin{tabular}{rclr} {\specif} & ::= & {\specif} {\tt *} {\specif} & ({\tt prod})\\ & $|$ & {\specif} {\tt +} {\specif} & ({\tt sum})\\ & $|$ & {\specif} {\tt + \{} {\specif} {\tt \}} & ({\tt sumor})\\ @@ -472,11 +475,12 @@ Inductive sumor (A:Set) (B:Prop) : Set := inleft (_:A) | inright (_:B). & $|$ & {\tt \{} {\ident} {\tt :} {\specif} {\tt \&} {\specif} {\tt \&} {\specif} {\tt \}} & ({\tt sigS2})\\ & & & \\ -{\term} & ::= & {\tt (} {\term} {\tt ,} {\term} {\tt )} & ({\tt pair})\\ -\hline +{\term} & ::= & {\tt (} {\term} {\tt ,} {\term} {\tt )} & ({\tt pair}) \end{tabular} -\caption{Syntax of datatypes and specifications} +\end{minipage}} \end{center} +\caption{Syntax of datatypes and specifications} +\label{specif-syntax} \end{figure} We may define variants of the axiom of choice, like in Martin-Löf's @@ -965,12 +969,13 @@ Check 2 + 3. \subsubsection{Some tactics} -In addition to the Ring, Field and Fourier tactics (see chapter \ref{Tactics}) -there are: - -{\tt DiscrR} prove that a real integer constante c1 is non equal to -another real integer constante c2. -\tacindex{DiscrR} +In addition to the \verb|ring|, \verb|field| and \verb|fourier| +tactics (see Chapter~\ref{Tactics}) there are: +\begin{itemize} +\item {\tt discrR} \tacindex{discrR} + + Proves that a real integer constant $c_1$ is different from another + real integer constant $c_2$. \begin{coq_example*} Require Import DiscrR. @@ -985,9 +990,9 @@ discrR. Abort. \end{coq_eval} -{\tt SplitAbsolu} allows us to unfold {\tt Rabsolu} contants and split +\item {\tt split\_Rabs} allows to unfold {\tt Rabs} constant and splits corresponding conjonctions. -\tacindex{SplitAbsolu} +\tacindex{split\_Rabs} \begin{coq_example*} Require Import SplitAbsolu. @@ -1002,10 +1007,10 @@ intro; split_Rabs. Abort. \end{coq_eval} -{\tt SplitRmult} allows us to split a condition that a product is non equal to -zero into subgoals corresponding to the condition on each subterm of the -product. -\tacindex{SplitRmult} +\item {\tt split\_Rmult} allows to split a condition that a product is + non null into subgoals corresponding to the condition on each + operand of the product. +\tacindex{split\_Rmult} \begin{coq_example*} Require Import SplitRmult. @@ -1016,8 +1021,10 @@ Goal forall x y z:R, x * y * z <> 0. intros; split_Rmult. \end{coq_example} +\end{itemize} + All this tactics has been written with the tactic language Ltac -described in chapter~\ref{TacticLanguage}. More details are available +described in Chapter~\ref{TacticLanguage}. More details are available in document \url{http://coq.inria.fr/~desmettr/Reals.ps}. \begin{coq_eval} diff --git a/doc/RefMan-ltac.tex b/doc/RefMan-ltac.tex index a252a1fd9..3e3a93e7f 100644 --- a/doc/RefMan-ltac.tex +++ b/doc/RefMan-ltac.tex @@ -45,6 +45,7 @@ side, they are used without the question mark. The main entry of the grammar is {\tacexpr}. This language is used in proof mode but it can also be used in toplevel definitions as shown in table~\ref{ltactop}. + \begin{Remarks} \item The infix tacticals ``\dots\ {\tt ||} \dots'' and ``\dots\ {\tt ;} \dots'' are associative. @@ -68,41 +69,40 @@ is understood as \end{Remarks} -\begin{table}[htbp] -\noindent{}\framebox[6in][l] -{\parbox{6in} -{\begin{center} +\begin{figure}[htbp] +\begin{center} +\fbox{\begin{minipage}{0.95\textwidth} \begin{tabular}{lcl} -{\tacexpr} & \cn{}::= & +{\tacexpr} & ::= & {\tacexpr} {\tt ;} {\tacexpr}\\ -& \cn{}| & {\tacexpr} {\tt ; [} \nelist{\tacexpr}{|} {\tt ]}\\ -& \cn{}| & {\tacexprpref}\\ +& | & {\tacexpr} {\tt ; [} \nelist{\tacexpr}{|} {\tt ]}\\ +& | & {\tacexprpref}\\ \\ -{\tacexprpref} & \cn{}::= & +{\tacexprpref} & ::= & {\tt do} {\it (}{\naturalnumber} {\it |} {\ident}{\it )} {\tacexprpref}\\ -& \cn{}| & {\tt info} {\tacexprpref}\\ -& \cn{}| & {\tt progress} {\tacexprpref}\\ -& \cn{}| & {\tt repeat} {\tacexprpref}\\ -& \cn{}| & {\tt try} {\tacexprpref}\\ -& \cn{}| & {\tacexprinf} \\ +& | & {\tt info} {\tacexprpref}\\ +& | & {\tt progress} {\tacexprpref}\\ +& | & {\tt repeat} {\tacexprpref}\\ +& | & {\tt try} {\tacexprpref}\\ +& | & {\tacexprinf} \\ \\ -{\tacexprinf} & \cn{}::= & +{\tacexprinf} & ::= & {\tacexprlow} {\tt ||} {\tacexprpref}\\ -& \cn{}| & {\tacexprlow}\\ +& | & {\tacexprlow}\\ \\ -{\tacexprlow} & \cn{}::= & +{\tacexprlow} & ::= & {\tt fun} \nelist{\name}{} {\tt =>} {\atom}\\ -& \cn{}| & +& | & {\tt let} \nelist{\letclause}{\tt with} {\tt in} {\atom}\\ -& \cn{}| & +& | & {\tt let rec} \nelist{\recclause}{\tt with} {\tt in} {\tacexpr}\\ -& \cn{}| & +& | & {\tt match goal with} \nelist{\contextrule}{\tt |} {\tt end}\\ -& \cn{}| & +& | & {\tt match reverse goal with} \nelist{\contextrule}{\tt |} {\tt end}\\ -& \cn{}| & +& | & {\tt match} {\tacexpr} {\tt with} \nelist{\matchrule}{\tt |} {\tt end}\\ & \cn{}| & {\tt abstract} {\atom}\\ & \cn{}| & {\tt abstract} {\atom} {\tt using} {\ident} \\ @@ -119,22 +119,22 @@ is understood as & \cn{}| & {\qualid} \nelist{\tacarg}{}\\ & \cn{}| & {\atom}\\ \\ -{\atom} & \cn{}::= & +{\atom} & ::= & {\qualid} \\ -& \cn{}| & ()\\ -& \cn{}| & {\tt (} {\tacexpr} {\tt )}\\ +& | & ()\\ +& | & {\tt (} {\tacexpr} {\tt )}\\ \end{tabular} -\end{center}}} +\end{minipage}} +\end{center} \caption{Syntax of the tactic language} \label{ltac} -\end{table} +\end{figure} -\begin{table}[htbp] -\noindent{}\framebox[6in][l] -{\parbox{6in} -{\begin{center} +\begin{figure}[htbp] +\begin{center} +\fbox{\begin{minipage}{0.95\textwidth} \begin{tabular}{lcl} \tacarg & ::= & {\qualid}\\ @@ -158,24 +158,25 @@ is understood as & $|$ & {\tt context} {\zeroone{\ident}} {\tt [} {\cpattern} {\tt ]} {\tt =>} {\tacexpr}\\ & $|$ & {\tt \_ =>} {\tacexpr}\\ \end{tabular} -\end{center}}} +\end{minipage}} +\end{center} \caption{Syntax of the tactic language (continued)} \label{ltac_aux} -\end{table} +\end{figure} -\begin{table}[ht] -\noindent{}\framebox[6in][l] -{\parbox{6in} -{\begin{center} +\begin{figure}[ht] +\begin{center} +\fbox{\begin{minipage}{0.95\textwidth} \begin{tabular}{lcl} \nterm{top} & ::= & {\tt Ltac} \nelist{\nterm{ltac\_def}} {\tt with} \\ \\ \nterm{ltac\_def} & ::= & {\ident} \sequence{\ident}{} {\tt :=} {\tacexpr} \end{tabular} -\end{center}}} +\end{minipage}} +\end{center} \caption{Tactic toplevel definitions} \label{ltactop} -\end{table} +\end{figure} %% @@ -203,7 +204,7 @@ of Ltac. %% Values are given by table~\ref{ltacval}. All these values are tactic values, %% i.e. to be applied to a goal, except {\tt Fun}, {\tt Rec} and $arg$ values. -%% \begin{table}[ht] +%% \begin{figure}[ht] %% \noindent{}\framebox[6in][l] %% {\parbox{6in} %% {\begin{center} @@ -236,7 +237,7 @@ of Ltac. %% \end{center}}} %% \caption{Values of ${\cal L}_{tac}$} %% \label{ltacval} -%% \end{table} +%% \end{figure} %% \subsection{Evaluation} @@ -245,25 +246,27 @@ of Ltac. \index{;@{\tt ;}} \index{Tacticals!;@{\tt {\tac$_1$};\tac$_2$}} -A sequence is an expression of the following form: -\begin{center} +\begin{tabbing} {\tacexpr}$_1$ {\tt ;} {\tacexpr}$_2$ -\end{center} +\end{tabbing} {\tacexpr}$_1$ and {\tacexpr}$_2$ are evaluated to $v_1$ and $v_2$. $v_1$ and $v_2$ must be tactic values. $v_1$ is then applied and $v_2$ is applied to every subgoal generated by the application of $v_1$. Sequence is left associating. \subsubsection{General sequence} + +\tacindex{;[\ldots$\mid$\ldots$\mid$\ldots]} \tacindex{; [ | ]} \index{; [ | ]@{\tt ;[\ldots$\mid$\ldots$\mid$\ldots]}} \index{Tacticals!; [ | ]@{\tt {\tac$_0$};[{\tac$_1$}$\mid$\ldots$\mid$\tac$_n$]}} -We can generalize the previous sequence operator by: -\begin{center} + +We can generalize the previous sequence operator as +\begin{tabbing} {\tacexpr}$_0$ {\tt ; [} {\tacexpr}$_1$ {\tt |} $...$ {\tt |} {\tacexpr}$_n$ {\tt ]} -\end{center} +\end{tabbing} {\tacexpr}$_i$ is evaluated to $v_i$, for $i=0,...,n$. $v_0$ is applied and $v_i$ is applied to the $i$-th generated subgoal by the application of $v_0$, for $=1,...,n$. It fails if the application of @@ -274,9 +277,9 @@ $v_0$ does not generate exactly $n$ subgoals. \index{Tacticals!do@{\tt do}} There is a for loop that repeats a tactic {\num} times: -\begin{center} +\begin{tabbing} {\tt do} {\num} {\tacexpr} -\end{center} +\end{tabbing} {\tacexpr} is evaluated to $v$. $v$ must be a tactic value. $v$ is applied {\num} times. Supposing ${\num}>1$, after the first application of $v$, $v$ is applied, at least once, to the generated @@ -288,9 +291,9 @@ the {\num} applications have been completed. \index{Tacticals!repeat@{\tt repeat}} We have a repeat loop with: -\begin{center} +\begin{tabbing} {\tt repeat} {\tacexpr} -\end{center} +\end{tabbing} {\tacexpr} is evaluated to $v$. $v$ must be a tactic value. $v$ is applied until it fails. Supposing $n>1$, after the first application of $v$, $v$ is applied, at least once, to the generated subgoals and @@ -302,9 +305,9 @@ fails. \index{Tacticals!try@{\tt try}} We can catch the tactic errors with: -\begin{center} +\begin{tabbing} {\tt try} {\tacexpr} -\end{center} +\end{tabbing} {\tacexpr} is evaluated to $v$. $v$ must be a tactic value. $v$ is applied. If the application of $v$ fails, it catches the error and leaves the goal unchanged. If the level of the exception is positive, @@ -314,9 +317,9 @@ then the exception is re-raised with its level decremented. \tacindex{progress} We can check if a tactic made progress with: -\begin{center} +\begin{tabbing} {\tt progress} {\tacexpr} -\end{center} +\end{tabbing} {\tacexpr} is evaluated to $v$. $v$ must be a tactic value. $v$ is applied. If the application of $v$ produced one subgoal equal to the initial goal (up to syntactical equality), then an error of level 0 is @@ -324,15 +327,14 @@ raised. \ErrMsg \errindex{Failed to progress} - \subsubsection{Branching} \tacindex{||} \index{Tacticals!orelse@{\tt ||}} We can easily branch with the following structure: -\begin{center} +\begin{tabbing} {\tacexpr}$_1$ {\tt ||} {\tacexpr}$_2$ -\end{center} +\end{tabbing} {\tacexpr}$_1$ and {\tacexpr}$_2$ are evaluated to $v_1$ and $v_2$. $v_1$ and $v_2$ must be tactic values. $v_1$ is applied and if it fails then $v_2$ is applied. Branching is left associating. @@ -343,9 +345,9 @@ it fails then $v_2$ is applied. Branching is left associating. We may consider the first tactic to work (i.e. which does not fail) among a panel of tactics: -\begin{center} +\begin{tabbing} {\tt first [} {\tacexpr}$_1$ {\tt |} $...$ {\tt |} {\tacexpr}$_n$ {\tt ]} -\end{center} +\end{tabbing} {\tacexpr}$_i$ are evaluated to $v_i$ and $v_i$ must be tactic values, for $i=1,...,n$. Supposing $n>1$, it applies $v_1$, if it works, it stops else it tries to apply $v_2$ and so on. It fails when there is no applicable tactic. @@ -358,9 +360,9 @@ tries to apply $v_2$ and so on. It fails when there is no applicable tactic. We may consider the first to solve (i.e. which generates no subgoal) among a panel of tactics: -\begin{center} +\begin{tabbing} {\tt solve [} {\tacexpr}$_1$ {\tt |} $...$ {\tt |} {\tacexpr}$_n$ {\tt ]} -\end{center} +\end{tabbing} {\tacexpr}$_i$ are evaluated to $v_i$ and $v_i$ must be tactic values, for $i=1,...,n$. Supposing $n>1$, it applies $v_1$, if it solves, it stops else it tries to apply $v_2$ and so on. It fails if there is no solving tactic. @@ -373,11 +375,12 @@ tries to apply $v_2$ and so on. It fails if there is no solving tactic. The constant {\tt idtac} is the identity tactic: it leaves any goal unchanged but it appears in the proof script. -\begin{center} +\begin{tabbing} {\tt idtac} and {\tt idtac "message"} -\end{center} +\end{tabbing} The latter variant prints the string on the standard output. + \subsubsection{Failing} \tacindex{fail} \index{Tacticals!fail@{\tt fail}} @@ -385,9 +388,9 @@ The latter variant prints the string on the standard output. The tactic {\tt fail} is the always-failing tactic: it does not solve any goal. It is useful for defining other tacticals since it can be catched by {\tt try} or {\tt match goal}. There are three variants: -\begin{center} +\begin{tabbing} {\tt fail $n$}, {\tt fail "message"} and {\tt fail $n$ "message"} -\end{center} +\end{tabbing} The number $n$ is the failure level. If no level is specified, it defaults to $0$. The level is used by {\tt try} and {\tt match goal}. If $0$, it makes {\tt match goal} considering the next clause @@ -397,24 +400,19 @@ If $0$, it makes {\tt match goal} considering the next clause \ErrMsg \errindex{Tactic Failure "message" (level $n$)}. \subsubsection{Local definitions} -\tacindex{let} -\tacindex{let rec} +\index{Ltac!let} +\index{Ltac!let rec} +\index{let!in Ltac} +\index{let rec!in Ltac} Local definitions can be done as follows: - -%\newpage{} - -%\phantom{} -%\vfill{} - -\begin{tabular}{l} +\begin{tabbing} {\tt let} {\ident}$_1$ {\tt :=} {\tacexpr}$_1$\\ {\tt with} {\ident}$_2$ {\tt :=} {\tacexpr}$_2$\\ ...\\ {\tt with} {\ident}$_n$ {\tt :=} {\tacexpr}$_n$ {\tt in}\\ {\tacexpr} -\end{tabular} - +\end{tabbing} each {\tacexpr}$_i$ is evaluated to $v_i$, then, {\tacexpr} is evaluated by substituting $v_i$ to each occurrence of {\ident}$_i$, for $i=1,...,n$. There is no dependencies between the {\tacexpr}$_i$ @@ -427,9 +425,9 @@ argument is required. \subsubsection{Application} An application is an expression of the following form: -\begin{center} +\begin{tabbing} {\qualid} {\tacarg}$_1$ ... {\tacarg}$_n$ -\end{center} +\end{tabbing} The reference {\qualid} must be bound to some defined tactic definition expecting at least $n$ arguments. The expressions {\tacexpr}$_i$ are evaluated to $v_i$, for $i=1,...,n$. @@ -441,22 +439,23 @@ definition expecting at least $n$ arguments. The expressions %\subsection{Application of tactic values} \subsubsection{Function construction} -\tacindex{fun} +\index{fun!in Ltac} +\index{Ltac!fun} A parameterized tactic can be built anonymously (without resorting to local definitions) with: -\begin{center} +\begin{tabbing} {\tt fun} {\ident${}_1$} ... {\ident${}_n$} {\tt =>} {\tacexpr} -\end{center} +\end{tabbing} Indeed, local definitions of functions are a syntactic sugar for binding a {\tt fun} tactic to an identifier. \subsubsection{Pattern matching on terms} -\tacindex{match} +\index{Ltac!match} +\index{match!in Ltac} We can carry out pattern matching on terms with: - -\begin{tabular}{l} +\begin{tabbing} {\tt match} {\tacexpr} {\tt with}\\ ~~~{\cpattern}$_1$ {\tt =>} {\tacexpr}$_1$\\ ~{\tt |} {\cpattern}$_2$ {\tt =>} {\tacexpr}$_2$\\ @@ -464,8 +463,7 @@ We can carry out pattern matching on terms with: ~{\tt |} {\cpattern}$_n$ {\tt =>} {\tacexpr}$_n$\\ ~{\tt |} {\tt \_} {\tt =>} {\tacexpr}$_{n+1}$\\ {\tt end} -\end{tabular} - +\end{tabbing} The {\tacexpr} is evaluated and should yield a term which is matched (non-linear first order unification) against {\cpattern}$_1$ then {\tacexpr}$_1$ is evaluated into some value by substituting the @@ -478,18 +476,23 @@ goal}). If all clauses fail (in particular, there is no pattern {\_}) then a no-matching error is raised. \begin{ErrMsgs} -\item \errindex{No matching clauses for match}\\ -No pattern can be used and, in particular, there is no {\tt \_} pattern. -\item \errindex{Argument of match does not evaluate to a term}\\ -This happens when {\tacexpr} does not denote a term. + +\item \errindex{No matching clauses for match} + + No pattern can be used and, in particular, there is no {\tt \_} pattern. + +\item \errindex{Argument of match does not evaluate to a term} + + This happens when {\tacexpr} does not denote a term. + \end{ErrMsgs} -\tacindex{context (in pattern)} +\index{context!in pattern} There is a special form of patterns to match a subterm against the pattern: -\begin{center} +\begin{tabbing} {\tt context} {\ident} {\tt [} {\cpattern} {\tt ]} -\end{center} +\end{tabbing} It matches any term which one subterm matches {\cpattern}. If there is a match, the optional {\ident} is assign the ``matched context'', that is the initial term where the matched subterm is replaced by a @@ -503,23 +506,25 @@ the order of matching is left unspecified. \subsubsection{Pattern matching on goals} -\tacindex{match goal} -\tacindex{match reverse goal} +\index{Ltac!match goal} +\index{Ltac!match reverse goal} +\index{match goal!in Ltac} +\index{match reverse goal!in Ltac} We can make pattern matching on goals using the following expression: - -\begin{tabular}{l} +\begin{tabbing} {\tt match goal with}\\ -~~~$hyp_{1,1}${\tt ,}...{\tt ,}$hyp_{1,m_1}$ +~~\={\tt |} $hyp_{1,1}${\tt ,}...{\tt ,}$hyp_{1,m_1}$ ~~{\tt |-}{\cpattern}$_1${\tt =>} {\tacexpr}$_1$\\ -~~{\tt |}$hyps_{2,1}${\tt ,}...{\tt ,}$hyp_{2,m_2}$ + \>{\tt |} $hyp_{2,1}${\tt ,}...{\tt ,}$hyp_{2,m_2}$ ~~{\tt |-}{\cpattern}$_2${\tt =>} {\tacexpr}$_2$\\ ~~...\\ -~~{\tt |}$hyp_{n,1}${\tt ,}...{\tt ,}$hyp_{n,m_n}$ + \>{\tt |} $hyp_{n,1}${\tt ,}...{\tt ,}$hyp_{n,m_n}$ ~~{\tt |-}{\cpattern}$_n${\tt =>} {\tacexpr}$_n$\\ -~~{\tt |\_}~~~~{\tt =>} {\tacexpr}$_{n+1}$\\ + \>{\tt |\_}~~~~{\tt =>} {\tacexpr}$_{n+1}$\\ {\tt end} -\end{tabular} +\end{tabbing} + % TODO: specify order of hypothesis and explain reverse... @@ -539,8 +544,9 @@ is applied. \ErrMsg \errindex{No matching clauses for match goal} -No goal pattern can be used and, in particular, there is no {\tt -\_} goal pattern. + No goal pattern can be used and, in particular, there is no {\tt + \_} goal pattern. + \medskip It is important to know that each hypothesis of the goal can be @@ -552,14 +558,14 @@ first), but it possible to reverse this order (older first) with the {\tt match reverse goal with} variant. \subsubsection{Filling a term context} -\tacindex{context (in expressions)} +\index{context!in expression} The following expression is not a tactic in the sense that it does not produce subgoals but generates a term to be used in tactic expressions: -\begin{center} +\begin{tabbing} {\tt context} {\ident} {\tt [} {\tacexpr} {\tt ]} -\end{center} +\end{tabbing} {\ident} must denote a context variable bound by a {\tt context} pattern of a {\tt match} expression. This expression evaluates replaces the hole of the value of {\ident} by the value of @@ -567,34 +573,38 @@ replaces the hole of the value of {\ident} by the value of \ErrMsg \errindex{not a context variable} + \subsubsection{Generating fresh hypothesis names} -\tacindex{fresh} +\index{Ltac!fresh} +\index{fresh!in Ltac} Tactics sometimes have to generate new names for hypothesis. Letting the system decide a name with the {\tt intro} tactic is not so good since it is very awkward to retrieve the name the system gave. As before, the following expression returns a term: -\begin{center} +\begin{tabbing} {\tt fresh} {\qstring} -\end{center} +\end{tabbing} It evaluates to an identifier unbound in the goal, which is obtained by padding {\qstring} with a number if necessary. If no name is given, the prefix is {\tt H}. \subsubsection{{\tt type of} {\term}} -\tacindex{type of} +%\tacindex{type of} +\index{Ltac!type of} +\index{type of!in Ltac} This tactic computes the type of {\term}. - \subsubsection{Computing in a constr} -\tacindex{eval} +\index{Ltac!eval} +\index{eval!in Ltac} Evaluation of a term can be performed with: -\begin{center} +\begin{tabbing} {\tt eval} {\nterm{redexpr}} {\tt in} {\term} -\end{center} +\end{tabbing} where \nterm{redexpr} is a reduction tactic among {\tt red}, {\tt hnf}, {\tt compute}, {\tt simpl}, {\tt cbv}, {\tt lazy}, {\tt unfold}, {\tt fold}, {\tt pattern}. @@ -609,10 +619,10 @@ elementary tactics, this is equivalent to \tacexpr. For complex tactic like \texttt{auto}, it displays the operations performed by the tactic. - \subsubsection{Proving a subgoal as a separate lemma} \tacindex{abstract} \index{Tacticals!abstract@{\tt 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 @@ -640,22 +650,21 @@ Basically, tactics toplevel definitions are made as follows: %script is evaluated by substituting $v$ to {\ident}. % %We can define functional definitions by:\\ -\begin{center} +\begin{tabbing} {\tt Ltac} {\ident} {\ident}$_1$ ... {\ident}$_n$ {\tt :=} {\tacexpr} -\end{center} +\end{tabbing} This defines a new tactic that can be used in any tactic script or new tactic toplevel definition. \Rem The preceding definition can equivalently be written: -\begin{center} +\begin{tabbing} {\tt Ltac} {\ident} {\tt := fun} {\ident}$_1$ ... {\ident}$_n$ {\tt =>} {\tacexpr} -\end{center} +\end{tabbing} Recursive and mutual recursive function definitions are also possible with the syntax: -\begin{center} -\begin{tabular}{l} +\begin{tabbing} {\tt Ltac} {\ident}$_1$ {\ident}$_{1,1}$ ... {\ident}$_{1,m_1}$~~{\tt :=} {\tacexpr}$_1$\\ {\tt with} {\ident}$_2$ {\ident}$_{2,1}$ ... {\ident}$_{2,m_2}$~~{\tt :=} @@ -663,12 +672,429 @@ possible with the syntax: ...\\ {\tt with} {\ident}$_n$ {\ident}$_{n,1}$ ... {\ident}$_{n,m_n}$~~{\tt :=} {\tacexpr}$_n$ -\end{tabular} -\end{center} +\end{tabbing} %This definition bloc is a set of definitions (use of %the same previous syntactical sugar) and the other scripts are evaluated as %usual except that the substitutions are lazily carried out (when an identifier %to be evaluated is the name of a recursive definition). +\endinput + +\section{Examples} +\subsection{About the cardinality of the natural number set} + +\begin{figure} +\begin{center} +\fbox{\begin{minipage}{0.95\textwidth} +\begin{coq_eval} +Reset Initial. +Require Import Arith. +Require Import List. +\end{coq_eval} +\begin{coq_example*} +Lemma card_nat : + ~ (exists x : nat, exists y : nat, forall z:nat, x = z \/ y = z). +Proof. +red; intros (x, (y, Hy)). +elim (Hy 0); elim (Hy 1); elim (Hy 2); intros; + match goal with + | [_:(?a = ?b),_:(?a = ?c) |- _ ] => + cut (b = c); [ discriminate | apply trans_equal with a; auto ] + end. +Qed. +\end{coq_example*} +\end{minipage}} +\end{center} +\caption{A proof on cardinality of natural numbers} +\label{cnatltac} +\end{figure} + +A first example which shows how to use the pattern matching over the proof +contexts is the proof that natural numbers have more than two elements. The +proof of such a lemma can be done as shown in table~\ref{cnatltac}. + +We can notice that all the (very similar) cases coming from the three +eliminations (with three distinct natural numbers) are successfully solved by +a {\tt match goal} structure and, in particular, with only one pattern (use +of non-linear matching). + +\subsection{Permutation on closed lists} + +\begin{figure}[b] +\begin{center} +\fbox{\begin{minipage}{0.95\textwidth} +\begin{coq_example*} +Section Sort. +Variable A : Set. +Inductive permut : list A -> list A -> Prop := + | permut_refl : forall l, permut l l + | permut_cons : + forall a l0 l1, permut l0 l1 -> permut (a :: l0) (a :: l1) + | permut_append : forall a l, permut (a :: l) (l ++ a :: nil) + | permut_trans : + forall l0 l1 l2, permut l0 l1 -> permut l1 l2 -> permut l0 l2. +End Sort. +\end{coq_example*} +\end{minipage}} +\end{center} +\caption{Definition of the permutation predicate} +\label{permutpred} +\end{figure} + + +Another more complex example is the problem of permutation on closed +lists. The aim is to show that a closed list is a permutation of +another one. First, we define the permutation predicate as shown in +table~\ref{permutpred}. + +\begin{figure}[p] +\begin{center} +\fbox{\begin{minipage}{0.95\textwidth} +\begin{coq_example} +Ltac Permut n := + match goal with + | |- (permut _ ?l ?l) => apply permut_refl + | |- (permut _ (?a :: ?l1) (?a :: ?l2)) => + let newn := eval compute in (length l1) in + (apply permut_cons; Permut newn) + | |- (permut ?A (?a :: ?l1) ?l2) => + match eval compute in n with + | 1 => fail + | _ => + let l1' := constr:(l1 ++ a :: nil) in + (apply (permut_trans A (a :: l1) l1' l2); + [ apply permut_append | compute; Permut (pred n) ]) + end + end. +Ltac PermutProve := + match goal with + | |- (permut _ ?l1 ?l2) => + match eval compute in (length l1 = length l2) with + | (?n = ?n) => Permut n + end + end. +\end{coq_example} +\end{minipage}} +\end{center} +\caption{Permutation tactic} +\label{permutltac} +\end{figure} + +\begin{figure}[p] +\begin{center} +\fbox{\begin{minipage}{0.95\textwidth} +\begin{coq_example*} +Lemma permut_ex1 : + permut nat (1 :: 2 :: 3 :: nil) (3 :: 2 :: 1 :: nil). +Proof. +PermutProve. +Qed. + +Lemma permut_ex2 : + permut nat + (0 :: 1 :: 2 :: 3 :: 4 :: 5 :: 6 :: 7 :: 8 :: 9 :: nil) + (0 :: 2 :: 4 :: 6 :: 8 :: 9 :: 7 :: 5 :: 3 :: 1 :: nil). +Proof. +PermutProve. +Qed. +\end{coq_example*} +\end{minipage}} +\end{center} +\caption{Examples of {\tt PermutProve} use} +\label{permutlem} +\end{figure} + +Next, we can write naturally the tactic and the result can be seen in +table~\ref{permutltac}. We can notice that we use two toplevel +definitions {\tt PermutProve} and {\tt Permut}. The function to be +called is {\tt PermutProve} which computes the lengths of the two +lists and calls {\tt Permut} with the length if the two lists have the +same length. {\tt Permut} works as expected. If the two lists are +equal, it concludes. Otherwise, if the lists have identical first +elements, it applies {\tt Permut} on the tail of the lists. Finally, +if the lists have different first elements, it puts the first element +of one of the lists (here the second one which appears in the {\tt + permut} predicate) at the end if that is possible, i.e., if the new +first element has been at this place previously. To verify that all +rotations have been done for a list, we use the length of the list as +an argument for {\tt Permut} and this length is decremented for each +rotation down to, but not including, 1 because for a list of length +$n$, we can make exactly $n-1$ rotations to generate at most $n$ +distinct lists. Here, it must be noticed that we use the natural +numbers of {\Coq} for the rotation counter. In table~\ref{ltac}, we +can see that it is possible to use usual natural numbers but they are +only used as arguments for primitive tactics and they cannot be +handled, in particular, we cannot make computations with them. So, a +natural choice is to use {\Coq} data structures so that {\Coq} makes +the computations (reductions) by {\tt eval compute in} and we can get +the terms back by {\tt match}. + +With {\tt PermutProve}, we can now prove lemmas such those shown in +table~\ref{permutlem}. + + +\subsection{Deciding intuitionistic propositional logic} + +\begin{figure}[b] +\begin{center} +\fbox{\begin{minipage}{0.95\textwidth} +\begin{coq_example} +Ltac Axioms := + match goal with + | |- True => trivial + | _:False |- _ => elimtype False; assumption + | _:?A |- ?A => auto + end. +Ltac DSimplif := + repeat + (intros; + match goal with + | id:(~ _) |- _ => red in id + | id:(_ /\ _) |- _ => + elim id; do 2 intro; clear id + | id:(_ \/ _) |- _ => + elim id; intro; clear id + | id:(?A /\ ?B -> ?C) |- _ => + cut (A -> B -> C); + [ intro | intros; apply id; split; assumption ] + | id:(?A \/ ?B -> ?C) |- _ => + cut (B -> C); + [ cut (A -> C); + [ intros; clear id + | intro; apply id; left; assumption ] + | intro; apply id; right; assumption ] + | id0:(?A -> ?B),id1:?A |- _ => + cut B; [ intro; clear id0 | apply id0; assumption ] + | |- (_ /\ _) => split + | |- (~ _) => red + end). +\end{coq_example} +\end{minipage}} +\end{center} +\caption{Deciding intuitionistic propositions (1)} +\label{tautoltaca} +\end{figure} + +\begin{figure} +\begin{center} +\fbox{\begin{minipage}{0.95\textwidth} +\begin{coq_example} +Ltac TautoProp := + DSimplif; + Axioms || + match goal with + | id:((?A -> ?B) -> ?C) |- _ => + cut (B -> C); + [ intro; cut (A -> B); + [ intro; cut C; + [ intro; clear id | apply id; assumption ] + | clear id ] + | intro; apply id; intro; assumption ]; TautoProp + | id:(~ ?A -> ?B) |- _ => + cut (False -> B); + [ intro; cut (A -> False); + [ intro; cut B; + [ intro; clear id | apply id; assumption ] + | clear id ] + | intro; apply id; red; intro; assumption ]; TautoProp + | |- (_ \/ _) => (left; TautoProp) || (right; TautoProp) + end. +\end{coq_example} +\end{minipage}} +\end{center} +\caption{Deciding intuitionistic propositions (2)} +\label{tautoltacb} +\end{figure} + +The pattern matching on goals allows a complete and so a powerful +backtracking when returning tactic values. An interesting application +is the problem of deciding intuitionistic propositional logic. +Considering the contraction-free sequent calculi {\tt LJT*} of +Roy~Dyckhoff (\cite{Dyc92}), it is quite natural to code such a tactic +using the tactic language. In Table~\ref{tautoltaca}, the tactic {\tt + Axioms} tries to conclude using usual axioms. The {\tt DSimplif} +tactic applies all the reversible rules of Dyckhoff's system. +Finally, in Table~\ref{tautoltacb}, the {\tt TautoProp} tactic (the +main tactic to be called) simplifies with {\tt DSimplif}, tries to +conclude with {\tt Axioms} and tries several paths using the +backtracking rules (one of the four Dyckhoff's rules for the left +implication to get rid of the contraction and the right or). + +\begin{figure}[tb] +\begin{center} +\fbox{\begin{minipage}{0.95\textwidth} +\begin{coq_example*} +Lemma tauto_ex1 : forall A B:Prop, A /\ B -> A \/ B. +Proof. +TautoProp. +Qed. + +Lemma tauto_ex2 : + forall A B:Prop, (~ ~ B -> B) -> (A -> B) -> ~ ~ A -> B. +Proof. +TautoProp. +Qed. +\end{coq_example*} +\end{minipage}} +\end{center} +\caption{Proofs of tautologies with {\tt TautoProp}} +\label{tautolem} +\end{figure} + +For example, with {\tt TautoProp}, we can prove tautologies like those in +table~\ref{tautolem}. + + +\subsection{Deciding type isomorphisms} + +A more tricky problem is to decide equalities between types and modulo +isomorphisms. Here, we choose to use the isomorphisms of the simply typed +$\lb{}$-calculus with Cartesian product and $unit$ type (see, for example, +\cite{RC95}). The axioms of this $\lb{}$-calculus are given by +table~\ref{isosax}. + +\begin{figure} +\begin{center} +\fbox{\begin{minipage}{0.95\textwidth} +\begin{coq_eval} +Reset Initial. +\end{coq_eval} +\begin{coq_example*} +Open Scope type_scope. +Section Iso_axioms. +Variables A B C : Set. +Axiom Com : A * B = B * A. +Axiom Ass : A * (B * C) = A * B * C. +Axiom Cur : (A * B -> C) = (A -> B -> C). +Axiom Dis : (A -> B * C) = (A -> B) * (A -> C). +Axiom P_unit : A * unit = A. +Axiom AR_unit : (A -> unit) = unit. +Axiom AL_unit : (unit -> A) = A. +Lemma Cons : B = C -> A * B = A * C. +Proof. +intro Heq; rewrite Heq; apply refl_equal. +Qed. +End Iso_axioms. +\end{coq_example*} +\end{minipage}} +\end{center} +\caption{Type isomorphism axioms} +\label{isosax} +\end{figure} + +The tactic to judge equalities modulo this axiomatization can be written as +shown in tables~\ref{isosltac1} and~\ref{isosltac2}. The algorithm is quite +simple. Types are reduced using axioms that can be oriented (this done by {\tt +MainSimplif}). The normal forms are sequences of Cartesian +products without Cartesian product in the left component. These normal forms +are then compared modulo permutation of the components (this is done by {\tt +CompareStruct}). The main tactic to be called and realizing this algorithm is +{\tt IsoProve}. + +\begin{figure} +\begin{center} +\fbox{\begin{minipage}{0.95\textwidth} +\begin{coq_example} +Ltac DSimplif trm := + match trm with + | (?A * ?B * ?C) => + rewrite <- (Ass A B C); try MainSimplif + | (?A * ?B -> ?C) => + rewrite (Cur A B C); try MainSimplif + | (?A -> ?B * ?C) => + rewrite (Dis A B C); try MainSimplif + | (?A * unit) => + rewrite (P_unit A); try MainSimplif + | (unit * ?B) => + rewrite (Com unit B); try MainSimplif + | (?A -> unit) => + rewrite (AR_unit A); try MainSimplif + | (unit -> ?B) => + rewrite (AL_unit B); try MainSimplif + | (?A * ?B) => + (DSimplif A; try MainSimplif) || (DSimplif B; try MainSimplif) + | (?A -> ?B) => + (DSimplif A; try MainSimplif) || (DSimplif B; try MainSimplif) + end + with MainSimplif := + match goal with + | |- (?A = ?B) => try DSimplif A; try DSimplif B + end. +Ltac Length trm := + match trm with + | (_ * ?B) => let succ := Length B in constr:(S succ) + | _ => constr:1 + end. +Ltac assoc := repeat rewrite <- Ass. +\end{coq_example} +\end{minipage}} +\end{center} +\caption{Type isomorphism tactic (1)} +\label{isosltac1} +\end{figure} + +\begin{figure} +\begin{center} +\fbox{\begin{minipage}{0.95\textwidth} +\begin{coq_example} +Ltac DoCompare n := + match goal with + | [ |- (?A = ?A) ] => apply refl_equal + | [ |- (?A * ?B = ?A * ?C) ] => + apply Cons; let newn := Length B in DoCompare newn + | [ |- (?A * ?B = ?C) ] => + match eval compute in n with + | 1 => fail + | _ => + pattern (A * B) at 1; rewrite Com; assoc; DoCompare (pred n) + end + end. +Ltac CompareStruct := + match goal with + | [ |- (?A = ?B) ] => + let l1 := Length A + with l2 := Length B in + match eval compute in (l1 = l2) with + | (?n = ?n) => DoCompare n + end + end. +Ltac IsoProve := MainSimplif; CompareStruct. +\end{coq_example} +\end{minipage}} +\end{center} +\caption{Type isomorphism tactic (2)} +\label{isosltac2} +\end{figure} + +Table~\ref{isoslem} gives examples of what can be solved by {\tt IsoProve}. + +\begin{figure} +\begin{center} +\fbox{\begin{minipage}{0.95\textwidth} +\begin{coq_example*} +Lemma isos_ex1 : + forall A B:Set, A * unit * B = B * (unit * A). +Proof. +intros; IsoProve. +Qed. + +Lemma isos_ex2 : + forall A B C:Set, + (A * unit -> B * (C * unit)) = + (A * unit -> (C -> unit) * C) * (unit -> A -> B). +Proof. +intros; IsoProve. +Qed. +\end{coq_example*} +\end{minipage}} +\end{center} +\caption{Type equalities solved by {\tt IsoProve}} +\label{isoslem} +\end{figure} + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "Reference-Manual" +%%% End: diff --git a/doc/RefMan-mod.tex b/doc/RefMan-mod.tex index de4f14fa5..1999d47dd 100644 --- a/doc/RefMan-mod.tex +++ b/doc/RefMan-mod.tex @@ -1,48 +1,67 @@ -\section{Module system}\index{Modules}\label{Modules} +\section{Module system} +\index{Modules} +\label{section:Modules} The module system provides a way of packaging related elements together, as well as a mean of massive abstraction. \begin{figure}[t] -\begin{tabular}{|rcl|} -\hline +\begin{center} +\fbox{\begin{minipage}{0.95\textwidth} +\begin{tabular}{rcl} {\modtype} & ::= & {\ident} \\ - & $|$ & {\modtype} \texttt{ with Definition }{\ident} \verb.:=. {\term} \\ - & $|$ & {\modtype} \texttt{ with Module }{\ident} \verb.:=. {\qualid} \\ + & $|$ & {\modtype} \texttt{ with Definition }{\ident} := {\term} \\ + & $|$ & {\modtype} \texttt{ with Module }{\ident} := {\qualid} \\ &&\\ -{\onemodbinding} & ::= & {\tt ( \nelist{\ident}{} \verb.:. {\modtype} )}\\ +{\onemodbinding} & ::= & {\tt ( \nelist{\ident}{} : {\modtype} )}\\ &&\\ {\modbindings} & ::= & \nelist{\onemodbinding}{}\\ &&\\ -{\modexpr} & ::= & \nelist{\qualid}{} \\ -\hline +{\modexpr} & ::= & \nelist{\qualid}{} \end{tabular} +\end{minipage}} +\end{center} \caption{Syntax of modules.} \end{figure} -\subsection{\tt Module {\ident}}\comindex{Module} +\subsection{\tt Module {\ident}} +\comindex{Module} + This command is used to start an interactive module named {\ident}. \begin{Variants} -\item{\tt Module {\ident} {\modbindings}}\\ + +\item{\tt Module {\ident} {\modbindings}} + Starts an interactive functor with parameters given by {\modbindings}. -\item{\tt Module {\ident} \verb.:. {\modtype}}\\ + +\item{\tt Module {\ident} \verb.:. {\modtype}} + Starts an interactive module specifying its module type. -\item{\tt Module {\ident} {\modbindings} \verb.:. {\modtype}}\\ + +\item{\tt Module {\ident} {\modbindings} \verb.:. {\modtype}} + Starts an interactive functor with parameters given by {\modbindings}, and output module type {\modtype}. -\item{\tt Module {\ident} \verb.<:. {\modtype}}\\ + +\item{\tt Module {\ident} \verb.<:. {\modtype}} + Starts an interactive module satisfying {\modtype}. -\item{\tt Module {\ident} {\modbindings} \verb.<:. {\modtype}}\\ + +\item{\tt Module {\ident} {\modbindings} \verb.<:. {\modtype}} + Starts an interactive functor with parameters given by {\modbindings}. The output module type is verified against the module type {\modtype}. + \end{Variants} -\subsection{\tt End {\ident}}\comindex{End} +\subsection{\tt End {\ident}} +\comindex{End} + This command closes the interactive module {\ident}. If the module type was given the content of the module is matched against it and an error is signaled if the matching fails. If the module is basic (is not a @@ -56,34 +75,54 @@ now available through the dot notation. \end{ErrMsgs} -\subsection{\tt Module {\ident} := {\modexpr}}\comindex{Module} -This command defines the module identifier {\ident} to be equal to {\modexpr}. +\subsection{\tt Module {\ident} := {\modexpr}} +\comindex{Module} + +This command defines the module identifier {\ident} to be equal to +{\modexpr}. \begin{Variants} -\item{\tt Module {\ident} {\modbindings} := {\modexpr}}\\ +\item{\tt Module {\ident} {\modbindings} := {\modexpr}} + Defines a functor with parameters given by {\modbindings} and body {\modexpr}. + % Particular cases of the next 2 items -%\item{\tt Module {\ident} \verb.:. {\modtype} := {\modexpr}}\\ +%\item{\tt Module {\ident} \verb.:. {\modtype} := {\modexpr}} +% % Defines a module with body {\modexpr} and interface {\modtype}. -%\item{\tt Module {\ident} \verb.<:. {\modtype} := {\modexpr}}\\ +%\item{\tt Module {\ident} \verb.<:. {\modtype} := {\modexpr}} +% % Defines a module with body {\modexpr}, satisfying {\modtype}. -\item{\tt Module {\ident} {\modbindings} \verb.:. {\modtype} := {\modexpr}}\\ + +\item{\tt Module {\ident} {\modbindings} \verb.:. {\modtype} := + {\modexpr}} + Defines a functor with parameters given by {\modbindings} (possibly none), and output module type {\modtype}, with body {\modexpr}. -\item{\tt Module {\ident} {\modbindings} \verb.<:. {\modtype} := {\modexpr}}\\ + +\item{\tt Module {\ident} {\modbindings} \verb.<:. {\modtype} := + {\modexpr}} + Defines a functor with parameters given by {\modbindings} (possibly none) with body {\modexpr}. The body is checked against {\modtype}. + \end{Variants} \subsection{\tt Module Type {\ident}}\comindex{Module Type} + This command is used to start an interactive module type {\ident}. \begin{Variants} -\item{\tt Module Type {\ident} {\modbindings}}\\ + +\item{\tt Module Type {\ident} {\modbindings}} + Starts an interactive functor type with parameters given by {\modbindings}. + \end{Variants} -\subsection{\tt End {\ident}}\comindex{End} +\subsection{\tt End {\ident}} +\comindex{End} + This command closes the interactive module type {\ident}. \begin{ErrMsgs} @@ -91,11 +130,13 @@ This command closes the interactive module type {\ident}. \end{ErrMsgs} \subsection{\tt Module Type {\ident} := {\modtype}} -Define a module type {\ident} equal to {\modtype}. + +Defines a module type {\ident} equal to {\modtype}. \begin{Variants} -\item {\tt Module Type {\ident} {\modbindings} := {\modtype}} \\ - Define a functor type {\ident} specifying functors taking arguments +\item {\tt Module Type {\ident} {\modbindings} := {\modtype}} + + Defines a functor type {\ident} specifying functors taking arguments {\modbindings} and returning {\modtype}. \end{Variants} @@ -104,34 +145,50 @@ Starts an interactive module declaration. This command is available only in module types. \begin{Variants} -\item{\tt Declare Module {\ident} {\modbindings}}\\ + +\item{\tt Declare Module {\ident} {\modbindings}} + Starts an interactive declaration of a functor with parameters given by {\modbindings}. + % Particular case of the next item -%\item{\tt Declare Module {\ident} \verb.<:. {\modtype}}\\ +%\item{\tt Declare Module {\ident} \verb.<:. {\modtype}} +% % Starts an interactive declaration of a module satisfying {\modtype}. -\item{\tt Declare Module {\ident} {\modbindings} \verb.<:. {\modtype}}\\ + +\item{\tt Declare Module {\ident} {\modbindings} \verb.<:. {\modtype}} + Starts an interactive declaration of a functor with parameters given by {\modbindings} (possibly none). The declared output module type is verified against the module type {\modtype}. + \end{Variants} \subsection{\tt End {\ident}} + This command closes the interactive declaration of module {\ident}. \subsection{\tt Declare Module {\ident} : {\modtype}} + Declares a module of {\ident} of type {\modtype}. This command is available only in module types. \begin{Variants} -\item{\tt Declare Module {\ident} {\modbindings} \verb.:. {\modtype}}\\ + +\item{\tt Declare Module {\ident} {\modbindings} \verb.:. {\modtype}} + Declares a functor with parameters {\modbindings} and output module type {\modtype}. -\item{\tt Declare Module {\ident} := {\qualid}}\\ + +\item{\tt Declare Module {\ident} := {\qualid}} + Declares a module equal to the module {\qualid}. -\item{\tt Declare Module {\ident} \verb.<:. {\modtype} := {\qualid}}\\ + +\item{\tt Declare Module {\ident} \verb.<:. {\modtype} := {\qualid}} + Declares a module equal to the module {\qualid}, verifying that the module type of the latter is a subtype of {\modtype}. + \end{Variants} @@ -147,12 +204,9 @@ Module M. Defined. End M. \end{coq_example} - -\noindent Inside a module one can define constants, prove theorems and do any other things that can be done in the toplevel. Components of a closed module can be accessed using the dot notation: - \begin{coq_example} Print M.x. \end{coq_example} @@ -163,8 +217,6 @@ Module Type SIG. Parameter x : T. End SIG. \end{coq_example} - -\noindent Inside a module type the proof editing mode is not available. Consequently commands like \texttt{Definition}\ without body, \texttt{Lemma}, \texttt{Theorem} are not allowed. In order to declare @@ -203,7 +255,7 @@ transparent constraint Module P <: SIG := M. Print P.y. \end{coq_example} -Now let us create a functor, i.e.\ a parametric module +Now let us create a functor, i.e. a parametric module \begin{coq_example} Module Two (X Y: SIG). \end{coq_example} @@ -303,24 +355,30 @@ Reset Mod. \begin{Variants} -\item{\tt Export {\qualid}}\comindex{Export}\\ +\item{\tt Export {\qualid}}\comindex{Export} + When the module containing the command {\tt Export {\qualid}} is imported, {\qualid} is imported as well. \end{Variants} \begin{ErrMsgs} - \item \errindex{{\qualid} is not a module} + \item \errindexbis{{\qualid} is not a module}{is not a module} % this error is impossible in the import command % \item \errindex{Cannot mask the absolute name {\qualid} !} \end{ErrMsgs} + \begin{Warnings} \item Warning: Trying to mask the absolute name {\qualid} ! \end{Warnings} -\subsection{\tt Print Module {\ident}}\comindex{Print Module} +\subsection{\tt Print Module {\ident}} +\comindex{Print Module} + Prints the module type and (optionally) the body of the module {\ident}. -\subsection{\tt Print Module Type {\ident}}\comindex{Print Module Type} +\subsection{\tt Print Module Type {\ident}} +\comindex{Print Module Type} + Prints the module type corresponding to {\ident}. diff --git a/doc/RefMan-modr.tex b/doc/RefMan-modr.tex index f9a251fdc..055e2313f 100644 --- a/doc/RefMan-modr.tex +++ b/doc/RefMan-modr.tex @@ -1,5 +1,5 @@ \chapter{The Module System} -\label{Mod} +\label{chapter:Modules} 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-oth.tex b/doc/RefMan-oth.tex index e065d54ed..392d68658 100644 --- a/doc/RefMan-oth.tex +++ b/doc/RefMan-oth.tex @@ -23,7 +23,7 @@ global constant. \comindex{About}\\ This displays various informations about the object denoted by {\qualid}: its kind (module, constant, assumption, inductive, -constructor, abbreviation, ...), long name, type, implicit +constructor, abbreviation\ldots), long name, type, implicit arguments and argument scopes. %\item {\tt Print Proof {\qualid}.}\comindex{Print Proof}\\ @@ -79,9 +79,9 @@ displayed in Objective Caml syntax, where global identifiers are still displayed as in \Coq\ terms. \begin{Variants} -\item \texttt{Recursive Extraction {\qualid$_1$} ... {\qualid$_n$}.}\\ +\item \texttt{Recursive Extraction {\qualid$_1$} \ldots{} {\qualid$_n$}.}\\ Recursively extracts all the material needed for the extraction of - globals {\qualid$_1$} ... {\qualid$_n$}. + globals {\qualid$_1$} \ldots{} {\qualid$_n$}. \end{Variants} \SeeAlso chapter~\ref{Extraction}. @@ -154,14 +154,15 @@ environment}\\ \begin{Variants} \item -{\tt Search {\qualid} inside {\module$_1$}...{\module$_n$}.} +{\tt Search {\qualid} inside {\module$_1$} \ldots{} {\module$_n$}.} -This restricts the search to constructions defined in modules {\module$_1$}...{\module$_n$}. +This restricts the search to constructions defined in modules +{\module$_1$} \ldots{} {\module$_n$}. -\item {\tt Search {\qualid} outside {\module$_1$}...{\module$_n$}.} +\item {\tt Search {\qualid} outside {\module$_1$} \ldots{} {\module$_n$}.} This restricts the search to constructions not defined in modules -{\module$_1$}...{\module$_n$}. +{\module$_1$} \ldots{} {\module$_n$}. \begin{ErrMsgs} \item \errindex{Module/section \module{} not found} @@ -202,13 +203,14 @@ SearchAbout [ Zmult Zplus "distr" ]. inside {\module$_1$} \ldots{} {\module$_n$}.} This restricts the search to constructions defined in modules -{\module$_1$}...{\module$_n$}. +{\module$_1$} \ldots{} {\module$_n$}. -\item {\tt SearchAbout {\term} outside {\module$_1$}...{\module$_n$}.}\\ -{\tt SearchAbout [ \nelist{\textrm{\textsl{qualid-or-string}}}{} ] outside {\module$_1$}...{\module$_n$}.} +\item {\tt SearchAbout {\term} outside {\module$_1$} \ldots{} {\module$_n$}.}\\ +{\tt SearchAbout [ \nelist{\textrm{\textsl{qualid-or-string}}}{} ] + outside {\module$_1$} \ldots{} {\module$_n$}.} This restricts the search to constructions not defined in modules -{\module$_1$}...{\module$_n$}. +{\module$_1$} \ldots{} {\module$_n$}. \end{Variants} @@ -234,15 +236,16 @@ SearchPattern (?X1 + _ = _ + ?X1). \begin{Variants} \item {\tt SearchPattern {\term} inside -{\module$_1$}...{\module$_n$}.}\comindex{SearchPattern ... inside -...} +{\module$_1$} \ldots{} {\module$_n$}.}\comindex{SearchPattern \ldots{} inside +\ldots{}} -This restricts the search to constructions defined in modules {\module$_1$}...{\module$_n$}. +This restricts the search to constructions defined in modules +{\module$_1$} \ldots{} {\module$_n$}. -\item {\tt SearchPattern {\term} outside {\module$_1$}...{\module$_n$}.}\comindex{SearchPattern ... outside ...} +\item {\tt SearchPattern {\term} outside {\module$_1$} \ldots{} {\module$_n$}.}\comindex{SearchPattern \ldots{} outside \ldots{}} This restricts the search to constructions not defined in modules -{\module$_1$}...{\module$_n$}. +{\module$_1$} \ldots{} {\module$_n$}. \end{Variants} @@ -259,14 +262,15 @@ SearchRewrite (_ + _ + _). \begin{Variants} \item {\tt SearchRewrite {\term} inside -{\module$_1$}...{\module$_n$}.} +{\module$_1$} \ldots{} {\module$_n$}.} -This restricts the search to constructions defined in modules {\module$_1$}...{\module$_n$}. +This restricts the search to constructions defined in modules +{\module$_1$} \ldots{} {\module$_n$}. -\item {\tt SearchRewrite {\term} outside {\module$_1$}...{\module$_n$}.} +\item {\tt SearchRewrite {\term} outside {\module$_1$} \ldots{} {\module$_n$}.} This restricts the search to constructions not defined in modules -{\module$_1$}...{\module$_n$}. +{\module$_1$} \ldots{} {\module$_n$}. \end{Variants} diff --git a/doc/RefMan-pro.tex b/doc/RefMan-pro.tex index b84d1b38a..1411d9afb 100755 --- a/doc/RefMan-pro.tex +++ b/doc/RefMan-pro.tex @@ -81,17 +81,29 @@ memory overflow. \end{ErrMsgs} \begin{Variants} -\item {\tt Defined.}\comindex{Defined} \label{Defined} \\ + +\item {\tt Defined.} +\comindex{Defined} +\label{Defined} + Defines the proved term as a transparent constant. -\item {\tt Save.}\comindex{Save}\\ + +\item {\tt Save.} +\comindex{Save} + Is equivalent to {\tt Qed}. -\item {\tt Save {\ident}.}\\ Forces the name of the original goal to -be {\ident}. This command (and the following ones) can only be used -if the original goal has been opened using the {\tt Goal} command. + +\item {\tt Save {\ident}.} + + Forces the name of the original goal to be {\ident}. This command + (and the following ones) can only be used if the original goal has + been opened using the {\tt Goal} command. + \item {\tt Save Theorem {\ident}.} \\ {\tt Save Lemma {\ident}.} \\ {\tt Save Remark {\ident}.}\\ - {\tt Save Fact {\ident}.}\\ + {\tt Save Fact {\ident}.} + Are equivalent to {\tt Save {\ident}.} \end{Variants} @@ -99,36 +111,53 @@ if the original goal has been opened using the {\tt Goal} command. This command is available in interactive editing proof mode to give up the current proof and declare the initial goal as an axiom. -\subsection{\tt Theorem {\ident} : {\form}.}\comindex{Theorem}\label{Theorem} +\subsection{\tt Theorem {\ident} : {\form}.} +\comindex{Theorem} +\label{Theorem} + This command switches to interactive editing proof mode and declares {\ident} as being the name of the original goal {\form}. When declared as a {\tt Theorem}, the name {\ident} is known at all section levels: {\tt Theorem} is a {\sl global} lemma. %\ErrMsg (see section \ref{Goal}) + \begin{ErrMsgs} + \item \errindex{the term \form\ has type \ldots{} which should be Set, Prop or Type} -\item \ident\ \errindex{already exists}\\ + +\item \errindexbis{\ident already exists}{already exists} + The name you provided already defined. You have then to choose another name. + \end{ErrMsgs} \begin{Variants} -\item {\tt Lemma {\ident} : {\form}.}\comindex{Lemma}\\ + +\item {\tt Lemma {\ident} : {\form}.} +\comindex{Lemma} + It is equivalent to {\tt Theorem {\ident} : {\form}.} + \item {\tt Remark {\ident} : {\form}.}\comindex{Remark}\\ - {\tt Fact {\ident} : {\form}.}\comindex{Fact}\\ + {\tt Fact {\ident} : {\form}.}\comindex{Fact} + Used to have a different meaning, but are now equivalent to {\tt Theorem {\ident} : {\form}.} They are kept for compatibility. + \item {\tt Definition {\ident} : {\form}.} -\comindex{Definition}\\ +\comindex{Definition} + Analogous to {\tt Theorem}, intended to be used in conjunction with {\tt Defined} (see \ref{Defined}) in order to define a transparent constant. + \item {\tt Local {\ident} : {\form}.} -\comindex{Local}\\ +\comindex{Local} + Analogous to {\tt Definition} except that the definition is turned into a local definition on objects depending on it after closing the current section. @@ -140,38 +169,55 @@ This command applies in proof editing mode. It is equivalent to {\tt one gulp, as a proof term (see section \ref{exact}). \begin{Variants} -\item{\tt Proof.}\\ -Is a noop which is useful to delimit the sequence of -tactic commands which start a proof, after a {\tt Theorem} command. -It is a good practice to use {\tt Proof.} as an opening parenthesis, -closed in the script with a closing {\tt Qed.} -\item{\tt Proof with {\tac}.}\\ -This command may be used to start a proof. It defines a default tactic to be used each time a tactic command is ended by ``\verb#...#''. In this case the tactic command typed by the user is equivalent to \emph{command};{\tac}. + +\item{\tt Proof.} + + Is a noop which is useful to delimit the sequence of tactic commands + which start a proof, after a {\tt Theorem} command. It is a good + practice to use {\tt Proof.} as an opening parenthesis, closed in + the script with a closing {\tt Qed.} + +\item{\tt Proof with {\tac}.} + + This command may be used to start a proof. It defines a default + tactic to be used each time a tactic command is ended by + ``\verb#...#''. In this case the tactic command typed by the user is + equivalent to \emph{command};{\tac}. \end{Variants} -\subsection{\tt Abort.}\comindex{Abort} +\subsection{\tt Abort.} +\comindex{Abort} + This command cancels the current proof development, switching back to the previous proof development, or to the \Coq\ toplevel if no other proof was edited. \begin{ErrMsgs} -\item \errindex{No focused proof}\texttt{ (No proof-editing in progress)} +\item \errindex{No focused proof (No proof-editing in progress)} \end{ErrMsgs} \begin{Variants} -\item {\tt Abort {\ident}.}\\ + +\item {\tt Abort {\ident}.} + Aborts the editing of the proof named {\ident}. -\item {\tt Abort All.}\\ + +\item {\tt Abort All.} + Aborts all current goals, switching back to the \Coq\ toplevel. + \end{Variants} -\subsection{\tt Suspend.}\comindex{Suspend} +\subsection{\tt Suspend.} +\comindex{Suspend} + This command applies in proof editing mode. It switches back to the \Coq\ toplevel, but without canceling the current proofs. \subsection{\tt Resume.} \comindex{Resume}\label{Resume} + This commands switches back to the editing of the last edited proof. \begin{ErrMsgs} @@ -179,9 +225,12 @@ This commands switches back to the editing of the last edited proof. \end{ErrMsgs} \begin{Variants} -\item {\tt Resume {\ident}.}\\ + +\item {\tt Resume {\ident}.} + Restarts the editing of the proof named {\ident}. This can be used to navigate between currently edited proofs. + \end{Variants} \begin{ErrMsgs} @@ -190,7 +239,9 @@ This commands switches back to the editing of the last edited proof. \section{Navigation in the proof tree} -\subsection{\tt Undo.}\comindex{Undo} +\subsection{\tt Undo.} +\comindex{Undo} + This command cancels the effect of the last tactic command. Thus, it backtracks one step. @@ -200,17 +251,24 @@ backtracks one step. \end{ErrMsgs} \begin{Variants} -\item {\tt Undo {\num}.}\\ + +\item {\tt Undo {\num}.} + Repeats {\tt Undo} {\num} times. + \end{Variants} -\subsection{\tt Set Undo {\num}.}\comindex{Set Undo} +\subsection{\tt Set Undo {\num}.} +\comindex{Set Undo} + This command changes the maximum number of {\tt Undo}'s that will be possible when doing a proof. It only affects proofs started after this command, such that if you want to change the current undo limit inside a proof, you should first restart this proof. -\subsection{\tt Unset Undo.}\comindex{Unset Undo} +\subsection{\tt Unset Undo.} +\comindex{Unset Undo} + This command resets the default number of possible {\tt Undo} commands (which is currently 12). diff --git a/doc/RefMan-tac.tex b/doc/RefMan-tac.tex index 886457466..21479ca4b 100644 --- a/doc/RefMan-tac.tex +++ b/doc/RefMan-tac.tex @@ -110,28 +110,40 @@ proved. Otherwise, it fails. \item \errindex{No such assumption} \end{ErrMsgs} -\subsection{\tt clear {\ident}}\tacindex{clear}\label{clear} +\subsection{\tt clear {\ident}} +\tacindex{clear} +\label{clear} + This tactic erases the hypothesis named {\ident} in the local context of the current goal. Then {\ident} is no more displayed and no more usable in the proof development. \begin{Variants} -\item {\tt clear {\ident$_1$} {\ldots} {\ident$_n$}.}\\ -This is equivalent to {\tt clear {\ident$_1$}. {\ldots} clear {\ident$_n$}.} -\item {\tt clearbody {\ident}.}\tacindex{clearbody}\\ -This tactic expects {\ident} to be a local definition then clears its -body. Otherwise said, this tactic turns a definition into an assumption. +\item {\tt clear {\ident$_1$} {\ldots} {\ident$_n$}.} + + This is equivalent to {\tt clear {\ident$_1$}. {\ldots} clear + {\ident$_n$}.} + +\item {\tt clearbody {\ident}.}\tacindex{clearbody} + + This tactic expects {\ident} to be a local definition then clears + its body. Otherwise said, this tactic turns a definition into an + assumption. + \end{Variants} \begin{ErrMsgs} \item \errindex{No such assumption} -\item \errindex{{\ident} is used in the conclusion} -\item \errindex{{\ident} is used in the hypothesis {\ident'}} +\item \errindexbis{{\ident} is used in the conclusion}{is used in the + conclusion} +\item \errindexbis{{\ident} is used in the hypothesis {\ident'}}{is + used in the hypothesis} \end{ErrMsgs} \subsection{\tt move {\ident$_1$} after {\ident$_2$}} -\tacindex{Move} +\tacindex{move} + This moves the hypothesis named {\ident$_1$} in the local context after the hypothesis named {\ident$_2$}. @@ -144,36 +156,44 @@ then all hypotheses between {\ident$_1$} and {\ident$_2$} which (possibly indirectly) occur in {\ident$_1$} are moved also. \begin{ErrMsgs} + \item \errindex{No such assumption: {\ident$_i$}} \item \errindex{Cannot move {\ident$_1$} after {\ident$_2$}: it occurs in {\ident$_2$}} + \item \errindex{Cannot move {\ident$_1$} after {\ident$_2$}: it depends on {\ident$_2$}} + \end{ErrMsgs} \subsection{\tt rename {\ident$_1$} into {\ident$_2$}} -\tacindex{Rename} +\tacindex{rename} + This renames hypothesis {\ident$_1$} into {\ident$_2$} in the current context\footnote{but it does not rename the hypothesis in the -proof-term...} + proof-term...} \begin{ErrMsgs} + \item \errindex{No such assumption} -\item \errindex{{\ident$_2$} is already used} +\item \errindexbis{{\ident$_2$} is already used}{is already used} + \end{ErrMsgs} \subsection{\tt intro} \tacindex{intro} \label{intro} + This tactic applies to a goal which is either a product or starts with a let binder. If the goal is a product, the tactic implements the -``Lam''\index{Typing rules!Lam} rule given in section -\ref{Typed-terms}\footnote{Actually, only the second subgoal will be -generated since the other one can be automatically checked.}. If the -goal starts with a let binder then the tactic implements a mix of the -``Let''\index{Typing rules!Let} and ``Conv''\index{Typing rules!Conv}. +``Lam''\index{Typing rules!Lam} rule given in +Section~\ref{Typed-terms}\footnote{Actually, only the second subgoal + will be generated since the other one can be automatically + checked.}. If the goal starts with a let binder then the tactic +implements a mix of the ``Let''\index{Typing rules!Let} and +``Conv''\index{Typing rules!Conv}. If the current goal is a dependent product {\tt forall (x:T), U} (resp {\tt let x:=t in U}) then {\tt intro} puts {\tt x:T} (resp {\tt x:=t}) in the @@ -199,7 +219,7 @@ the tactic {\tt intro} applies the tactic {\tt red} until the tactic \begin{ErrMsgs} \item \errindex{No product even after head-reduction} -\item \errindex{\texttt{{\ident} is already used}} +\item \errindexbis{{\ident} is already used}{is already used} \end{ErrMsgs} \begin{Variants} @@ -241,7 +261,8 @@ the tactic {\tt intro} applies the tactic {\tt red} until the tactic \item {\tt intros until {\num}} \tacindex{intros until} Repeats {\tt intro} until the {\num}-th non-dependent premise. For - instance, on the subgoal \verb+forall x y:nat, x=y -> forall z:nat,z=x->z=y+ the + instance, on the subgoal % + \verb+forall x y:nat, x=y -> forall z:nat,z=x->z=y+ the tactic \texttt{intros until 2} is equivalent to \texttt{intros x y H z H0} (assuming \texttt{x, y, H, z} and \texttt{H0} do not already occur in context). @@ -400,17 +421,16 @@ should not be substituted. {\num$_{n_i}^i$} of hypothesis {\ident$_i$}. One of the {\ident}'s may be the word {\tt Goal}. - \item {\tt pose ( {\ident} {\tt :=} {\term} {\tt )}} -This adds the local definition {\ident} := {\term} to the current -context without performing any replacement in the goal or in the -hypotheses. + This adds the local definition {\ident} := {\term} to the current + context without performing any replacement in the goal or in the + hypotheses. \item{\tt pose {\term}} -This behaves as {\tt pose (} {\ident} := {\term} {\tt )} but -{\ident} is generated by {\Coq}. + This behaves as {\tt pose (} {\ident} := {\term} {\tt )} but + {\ident} is generated by {\Coq}. \end{Variants} @@ -432,6 +452,7 @@ in the list of subgoals remaining to prove. \end{ErrMsgs} \begin{Variants} + \item{\tt assert {\form}} This behaves as {\tt assert (} {\ident} : {\form} {\tt )} but @@ -570,7 +591,6 @@ This tactic applies to any goal. It implements the rule \subsection{Bindings list} \index{Binding list}\label{Binding-list} -\index[tactic]{Binding list} A bindings list is generally used after the keyword {\tt with} in tactics. The general shape of a bindings list is {\tt (\vref$_1$ := @@ -621,7 +641,6 @@ cases. This tactic is a macro for the tactics sequence {\tt intros; \section{Conversion tactics} \index{Conversion tactics} -\index[tactic]{Conversion tactics} \label{Conversion-tactics} This set of tactics implements different specialized usages of the @@ -631,8 +650,8 @@ tactic \texttt{change}. %voir reduction__conv_x : histoires d'univers. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\subsection{{\tt cbv} \flag$_1$ \dots\ \flag$_n$, {\tt lazy} \flag$_1$ -\dots\ \flag$_n$ {\rm and} {\tt compute}} +\subsection{{\tt cbv \flag$_1$ \dots\ \flag$_n$}, {\tt lazy \flag$_1$ +\dots\ \flag$_n$} and {\tt compute}} \tacindex{cbv}\tacindex{lazy} These parameterized reduction tactics apply to any goal and perform @@ -673,7 +692,7 @@ strategy, the latter should be preferred for evaluating purely computational expressions (i.e. with few dead code). \begin{Variants} -\item {\tt compute} \tacindex{Compute} +\item {\tt compute} \tacindex{compute} This tactic is an alias for {\tt cbv beta delta evar iota zeta}. \end{Variants} @@ -1590,15 +1609,18 @@ latter is first introduced in the local context using \end{ErrMsgs} \begin{Variants} -\item \texttt{injection} \num\\ +\item \texttt{injection} \num{} + This does the same thing as \texttt{intros until \num} then \texttt{injection \ident} where {\ident} is the identifier for the last introduced hypothesis. -\item{\tt injection}\tacindex{injection} \\ - If the current goal is of the form {\tt \verb=~={\term$_1$}={\term$_2$}}, - the tactic computes the head normal form - of the goal and then behaves as the sequence: {\tt unfold not; intro - {\ident}; injection {\ident}}. \\ + +\item{\tt injection}\tacindex{injection} + + If the current goal is of the form {\tt + \verb=~={\term$_1$}={\term$_2$}}, the tactic computes the head + normal form of the goal and then behaves as the sequence: {\tt + unfold not; intro {\ident}; injection {\ident}}. \ErrMsg \errindex{goal does not satisfy the expected preconditions} \end{Variants} @@ -1806,7 +1828,6 @@ Abort. ${\tt forall (}\vec{x}{\tt :}\vec{T}{\tt),} I~\vec{t}$ Sort \sort} \label{Derive-Inversion} \comindex{Derive Inversion} -\index[tactic]{Derive Inversion@{\tt Derive Inversion}} This command generates an inversion principle for the \texttt{inversion \dots\ using} tactic. @@ -1881,22 +1902,34 @@ By default, \texttt{auto} only uses the hypotheses of the current goal and the hints of the database named {\tt core}. \begin{Variants} -\item {\tt auto \num}\\ - Forces the search depth to be \num. The maximal search depth is 5 by default. -\item {\tt auto with \ident$_1$ \dots\ \ident$_n$}\\ + +\item {\tt auto \num} + + Forces the search depth to be \num. The maximal search depth is 5 by + default. + +\item {\tt auto with \ident$_1$ \dots\ \ident$_n$} + Uses the hint databases $\ident_1$ \dots\ $\ident_n$ in addition to the database {\tt core}. See section \ref{Hints-databases} for the list of pre-defined databases and the way to create or extend a database. This option can be combined with the previous one. -\item {\tt auto with *}\\ + +\item {\tt auto with *} + Uses all existing hint databases, minus the special database - {\tt v62}. See section \ref{Hints-databases} -\item {\tt trivial}\tacindex{trivial}\\ + {\tt v62}. See Section~\ref{Hints-databases} + +\item {\tt trivial}\tacindex{trivial} + This tactic is a restriction of {\tt auto} that is not recursive and tries only hints which cost is 0. Typically it solves trivial equalities like $X=X$. -\item \texttt{trivial with \ident$_1$ \dots\ \ident$_n$}\\ -\item \texttt{trivial with *}\\ + +\item \texttt{trivial with \ident$_1$ \dots\ \ident$_n$} + +\item \texttt{trivial with *} + \end{Variants} \Rem {\tt auto} either solves completely the goal or else leave it @@ -2032,7 +2065,8 @@ incompatibilities. % En attente d'un moyen de valoriser les fichiers de demos %\SeeAlso file \texttt{contrib/Rocq/DEMOS/Demo\_tauto.v} -\subsection{{\tt firstorder}\tacindex{firstorder}} +\subsection{{\tt firstorder}} +\tacindex{firstorder} \label{firstorder} The tactic \texttt{firstorder} is an {\it experimental} extension of @@ -2042,15 +2076,20 @@ It is not restricted to usual logical connectives but instead may reason about any first-order class inductive definition. \begin{Variants} - \item {\tt firstorder {\tac}}\\ - \tacindex{\tt firstorder {\tac}} + \item {\tt firstorder {\tac}} + \tacindex{firstorder {\tac}} + Tries to solve the goal with {\tac} when no logical rule may apply. - \item {\tt firstorder with \ident$_1$ \dots\ \ident$_n$ }\\ - \tacindex{\tt firstorder with} + + \item {\tt firstorder with \ident$_1$ \dots\ \ident$_n$ } + \tacindex{firstorder with} + Adds lemmata \ident$_1$ \dots\ \ident$_n$ to the proof-search environment. - \item {\tt firstorder using \ident$_1$ \dots\ \ident$_n$ }\\ - \tacindex{\tt firstorder using} + + \item {\tt firstorder using \ident$_1$ \dots\ \ident$_n$ } + \tacindex{firstorder using} + Adds lemmata in {\tt auto} hints bases \ident$_1$ \dots\ \ident$_n$ to the proof-search environment. \end{Variants} @@ -2059,13 +2098,14 @@ Proof-search is bounded by a depth parameter which can be set by typing the {\nobreak \tt Set Firstorder Depth $n$} \comindex{Set Firstorder Depth} vernacular command. -\subsection{{\tt jp} {\em (Jprover)}}\tacindex{jp {\em (Jprover)}} +\subsection{{\tt jp} {\em (Jprover)}} +\tacindex{jp} \label{jprover} -The tactic \texttt{jp}, due to Huang Guan-Shieng, is an {\it - experimental} port of the {\em Jprover}\cite{SLKN01} semi-decision -procedure for first-order intuitionistic logic implemented in {\em - NuPRL}\cite{Kre02}. +The tactic \texttt{jp}, due to Huang Guan-Shieng, is an experimental +port of the {\em Jprover}\cite{SLKN01} semi-decision procedure for +first-order intuitionistic logic implemented in {\em + NuPRL}\cite{Kre02}. Search may optionnaly be bounded by a multiplicity parameter indicating how many (at most) copies of a formula may be used in @@ -2313,40 +2353,45 @@ Reset Initial. \comindex{Add Field} This vernacular command adds a commutative field theory to the database for the -tactic {\tt field}. You must provide this theory as follows:\\ - +tactic {\tt field}. You must provide this theory as follows: +\begin{flushleft} {\tt Add Field {\it A} {\it Aplus} {\it Amult} {\it Aone} {\it Azero} {\it -Aopp} {\it Aeq} {\it Ainv} {\it Rth} {\it Tinvl}}\\ - -\noindent where {\tt {\it A}} is a term of type {\tt Type}, {\tt {\it Aplus}} -is a term of type {\tt A->A->A}, {\tt {\it Amult}} is a term of type {\tt -A->A->A}, {\tt {\it Aone}} is a term of type {\tt A}, {\tt {\it Azero}} is a -term of type {\tt A}, {\tt {\it Aopp}} is a term of type {\tt A->A}, {\tt {\it -Aeq}} is a term of type {\tt A->bool}, {\tt {\it Ainv}} is a term of type {\tt -A->A}, {\tt {\it Rth}} is a term of type {\tt (Ring\_Theory {\it A Aplus Amult -Aone Azero Ainv Aeq})}, and {\tt {\it Tinvl}} is a term of type {\tt -forall n:{\it A}, {\~{}}(n={\it Azero})->({\it Amult} ({\it Ainv} n) n)={\it Aone}}. -To build a ring theory, refer to chapter~\ref{ring} for more details. +Aopp} {\it Aeq} {\it Ainv} {\it Rth} {\it Tinvl}} +\end{flushleft} +where {\tt {\it A}} is a term of type {\tt Type}, {\tt {\it Aplus}} is +a term of type {\tt A->A->A}, {\tt {\it Amult}} is a term of type {\tt + A->A->A}, {\tt {\it Aone}} is a term of type {\tt A}, {\tt {\it + Azero}} is a term of type {\tt A}, {\tt {\it Aopp}} is a term of +type {\tt A->A}, {\tt {\it Aeq}} is a term of type {\tt A->bool}, {\tt + {\it Ainv}} is a term of type {\tt A->A}, {\tt {\it Rth}} is a term +of type {\tt (Ring\_Theory {\it A Aplus Amult Aone Azero Ainv Aeq})}, +and {\tt {\it Tinvl}} is a term of type {\tt forall n:{\it A}, + {\~{}}(n={\it Azero})->({\it Amult} ({\it Ainv} n) n)={\it Aone}}. +To build a ring theory, refer to Chapter~\ref{ring} for more details. This command adds also an entry in the ring theory table if this theory is not already declared. So, it is useless to keep, for a given type, the {\tt Add Ring} command if you declare a theory with {\tt Add Field}, except if you plan -to use specific features of {\tt ring} (see chapter~\ref{ring}). However, the +to use specific features of {\tt ring} (see Chapter~\ref{ring}). However, the module {\tt ring} is not loaded by {\tt Add Field} and you have to make a {\tt Require Import Ring} if you want to call the {\tt ring} tactic. \begin{Variants} + \item {\tt Add Field {\it A} {\it Aplus} {\it Amult} {\it Aone} {\it Azero} {\it Aopp} {\it Aeq} {\it Ainv} {\it Rth} {\it Tinvl}}\\ -{\tt \phantom{Add Field }with minus:={\it Aminus}}\\ -Adds also the term {\it Aminus} which must be a constant expressed by means of -{\it Aopp}. +{\tt \phantom{Add Field }with minus:={\it Aminus}} + +Adds also the term {\it Aminus} which must be a constant expressed by +means of {\it Aopp}. \item {\tt Add Field {\it A} {\it Aplus} {\it Amult} {\it Aone} {\it Azero} {\it Aopp} {\it Aeq} {\it Ainv} {\it Rth} {\it Tinvl}}\\ -{\tt \phantom{Add Field }with div:={\it Adiv}}\\ -Adds also the term {\it Adiv} which must be a constant expressed by means of -{\it Ainv}. +{\tt \phantom{Add Field }with div:={\it Adiv}} + +Adds also the term {\it Adiv} which must be a constant expressed by +means of {\it Ainv}. + \end{Variants} \SeeAlso file {\tt theories/Reals/Rbase.v} for an example of instantiation,\\ @@ -2359,9 +2404,9 @@ field}. \subsection{\tt fourier} \tacindex{fourier} -This tactic written by Lo{\"\i}c Pottier solves linear inequations on real numbers -using Fourier's method (\cite{Fourier}). This tactic must be loaded by -{\tt Require Import Fourier}. +This tactic written by Lo{\"\i}c Pottier solves linear inequations on +real numbers using Fourier's method~\cite{Fourier}. This tactic must +be loaded by {\tt Require Import Fourier}. \Example \begin{coq_example*} @@ -2442,6 +2487,7 @@ main subgoal excluded. \section{The hints databases for {\tt auto} and {\tt eauto}ê} \index{Hints databases}\label{Hints-databases}\comindex{Hint} + The hints for \texttt{auto} and \texttt{eauto} are stored in databases. Each databases maps head symbols to list of hints. One can use the command \texttt{Print Hint \ident} @@ -2452,7 +2498,16 @@ tried by \texttt{auto} if the conclusion of current goal matches its pattern, and after hints with a lower cost. The general command to add a hint to some databases \ident$_1$, \dots, \ident$_n$ is: -\comindex{Hint} +The hints for \texttt{auto} and \texttt{eauto} have been reorganized +since \Coq{} 6.2.3. They are stored in several databases. Each +databases maps head symbols to list of hints. One can use the command +\texttt{Print Hint \ident} to display the hints associated to the head +symbol \ident{} (see \ref{PrintHint}). Each hint has a cost that is an +nonnegative integer, and a pattern. The hint is tried by \texttt{auto} +if the conclusion of current goal matches its pattern, and after hints +with a lower cost. The general command to add a hint to some databases +\ident$_1$, \dots, \ident$_n$ is: + \begin{quotation} \texttt{Hint} \textsl{hint\_definition} \texttt{:} \ident$_1$ \ldots\ \ident$_n$ \end{quotation} @@ -2460,8 +2515,9 @@ a hint to some databases \ident$_1$, \dots, \ident$_n$ is: \noindent where {\sl hint\_definition} is one of the following expressions: \begin{itemize} -\item \texttt{Resolve} {\term} \index[command]{Hint!Resolve} - +\item \texttt{Resolve} {\term} + \comindex{Hint Resolve} + This command adds {\tt apply {\term}} to the hint list with the head symbol of the type of \term. The cost of that hint is the number of subgoals generated by {\tt apply {\term}}. @@ -2483,27 +2539,31 @@ a hint to some databases \ident$_1$, \dots, \ident$_n$ is: The head symbol of the type of {\term} is a bound variable such that this tactic cannot be associated to a constant. + \item \term\ \errindex{cannot be used as a hint} The type of \term\ contains products over variables which do not appear in the conclusion. A typical example is a transitivity axiom. In that case the {\tt apply} tactic fails, and thus is useless. + \end{ErrMsgs} \begin{Variants} - \item \texttt{Resolve} {\term$_1$} \dots {\term$_m$} - Adds each \texttt{Resolve} {\term$_i$}. + \item \texttt{Resolve} {\term$_1$} \dots {\term$_m$} + + Adds each \texttt{Resolve} {\term$_i$}. + \end{Variants} -\item \texttt{Immediate {\term}} \index[command]{Hint!Immediate}\\ +\item \texttt{Immediate {\term}} +\comindex{Hint Immediate} This command adds {\tt apply {\term}; trivial} to the hint list associated with the head symbol of the type of \ident in the given database. This tactic will fail if all the subgoals generated by - {\tt apply {\term}} are - not solved immediately by the {\tt trivial} tactic which only tries - tactics with cost $0$. + {\tt apply {\term}} are not solved immediately by the {\tt trivial} + tactic which only tries tactics with cost $0$. This command is useful for theorems such that the symmetry of equality or $n+1=m+1 \to n=m$ that we may like to introduce with a @@ -2513,17 +2573,23 @@ a hint to some databases \ident$_1$, \dots, \ident$_n$ is: so that it is not used by {\tt trivial} itself. \begin{ErrMsgs} + \item \errindex{Bound head variable} - \item \term\ \errindex{cannot be used as a hint} + + \item \term\ \errindex{cannot be used as a hint} + \end{ErrMsgs} \begin{Variants} - \item \texttt{Immediate} {\term$_1$} \dots {\term$_m$} + + \item \texttt{Immediate} {\term$_1$} \dots {\term$_m$} Adds each \texttt{Immediate} {\term$_i$}. + \end{Variants} -\item \texttt{Constructors} {\ident}\index[command]{Hint!Constructors}\\ +\item \texttt{Constructors} {\ident} +\comindex{Hint Constructors} If {\ident} is an inductive type, this command adds all its constructors as hints of type \texttt{Resolve}. Then, when the @@ -2531,26 +2597,39 @@ a hint to some databases \ident$_1$, \dots, \ident$_n$ is: \texttt{auto} will try to apply each constructor. \begin{ErrMsgs} + \item {\ident} \errindex{is not an inductive type} + \item {\ident} \errindex{not declared} + \end{ErrMsgs} \begin{Variants} - \item \texttt{Constructors} {\ident$_1$} \dots {\ident$_m$} \\ + + \item \texttt{Constructors} {\ident$_1$} \dots {\ident$_m$} + Adds each \texttt{Constructors} {\ident$_i$}. + \end{Variants} -\item \texttt{Unfold} {\qualid}\index[command]{Hint!unfold}\\ - This adds the tactic {\tt unfold {\qualid}} to the hint list - that will only be used when the head constant of the goal is \ident. - Its cost is 4. +\item \texttt{Unfold} {\qualid} +\comindex{Hint Unfold} + + This adds the tactic {\tt unfold {\qualid}} to the hint list that + will only be used when the head constant of the goal is \ident. Its + cost is 4. \begin{Variants} - \item \texttt{Unfold} {\ident$_1$} \dots {\ident$_m$} \\ + + \item \texttt{Unfold} {\ident$_1$} \dots {\ident$_m$} + Adds each \texttt{Unfold} {\ident$_i$}. + \end{Variants} -\item \texttt{Extern \num\ \pattern\ => }\textsl{tactic}\index[command]{Hint!Extern}\\ +\item \texttt{Extern \num\ \pattern\ => }\textsl{tactic} +\comindex{Hint Extern} + This hint type is to extend \texttt{auto} with tactics other than \texttt{apply} and \texttt{unfold}. For that, we must specify a cost, a pattern and a tactic to execute. Here is an example: @@ -2590,18 +2669,21 @@ Abort. pattern-matching on hypotheses. \begin{Variants} -\item \texttt{Hint} \textsl{hint\_definition} \\ +\item \texttt{Hint} \textsl{hint\_definition} + No database name is given : the hint is registered in the {\tt core} database. \item\texttt{Hint Local} \textsl{hint\_definition} \texttt{:} - \ident$_1$ \ldots\ \ident$_n$\\ + \ident$_1$ \ldots\ \ident$_n$ + This is used to declare hints that must not be exported to the other modules that require and import the current module. Inside a section, the option {\tt Local} is useless since hints do not survive anyway to the closure of sections. -\item\texttt{Hint Local} \textsl{hint\_definition} \\ +\item\texttt{Hint Local} \textsl{hint\_definition} + Idem for the {\tt core} database. \end{Variants} @@ -2633,6 +2715,7 @@ library. There is no systematic relation between the directories of the library and the databases. \begin{description} + \item[\tt core] This special database is automatically used by \texttt{auto}. It contains only basic lemmas about negation, conjunction, and so on from. Most of the hints in this database come @@ -2673,36 +2756,170 @@ development. \subsection{\tt Print Hint} \label{PrintHint} \comindex{Print Hint} -\index[tactic]{Hint!\texttt{Print Hint}} +%\index[tactic]{Hint!\texttt{Print Hint}} + This command displays all hints that apply to the current goal. It fails if no proof is being edited, while the two variants can be used at every moment. \begin{Variants} -\item {\tt Print Hint {\ident} }\\ + +\item {\tt Print Hint {\ident} } + This command displays only tactics associated with \ident\ in the hints list. This is independent of the goal being edited, to this command will not fail if no goal is being edited. -\item {\tt Print Hint *}\\ +\item {\tt Print Hint *} + This command displays all declared hints. -\item {\tt Print HintDb {\ident} }\\ +\item {\tt Print HintDb {\ident} } \label{PrintHintDb} \comindex{Print HintDb} + This command displays all hints from database \ident. + \end{Variants} \subsection{Hints and sections} \label{Hint-and-Section} +Like grammar rules and structures for the \texttt{ring} tactic, things +added by the \texttt{Hint} command will be erased when closing a +section. + +Conversely, when the user does \texttt{Require A.}, all hints +of the module \texttt{A} that are not defined inside a section are +loaded. + +\section{Tacticals} +\label{Tacticals} +\index{Tacticals} + +We describe in this section how to combine the tactics provided by the +system to write synthetic proof scripts called {\em tacticals}. The +tacticals are built using tactic operators we present below. + +\subsection{\tt idtac} +\tacindex{idtac} +\index{Tacticals!idtac@{\tt idtac}} + +The constant {\tt idtac} is the identity tactic: it leaves any goal +unchanged. + +\subsection{\tt fail} +\tacindex{fail} +\index{Tacticals!fail@{\tt fail}} + +The tactic {\tt fail} is the always-failing tactic: it does not solve +any goal. It is useful for defining other tacticals. + +\subsection{\tt do {\num} {\tac}} +\tacindex{do} +\index{Tacticals!do@{\tt do}} + Hints provided by the \texttt{Hint} commands are erased when closing a section. Conversely, all hints of a module \texttt{A} that are not defined inside a section (and not defined with option {\tt Local}) become available when the module {\tt A} is imported (using e.g. \texttt{Require Import A.}). +\subsection{\tt \tac$_1$ {\tt ||} \tac$_2$} +\tacindex{||} +\index{Tacticals!orelse@{\tt ||}} + +The tactical \tac$_1$ {\tt ||} \tac$_2$ tries to apply \tac$_1$ +and, in case of a failure, applies \tac$_2$. It associates to the +left. + +\subsection{\tt repeat {\tac}} +\tacindex{repeat} +\index{Tacticals!repeat@{\tt repeat}} + +This tactic operator repeats {\tac} as long as it does not fail. + +\subsection{\tt {\tac}$_1$ {\tt ;} \tac$_2$} +\tacindex{;} +\index{Tacticals!yy@{\tt {\tac$_1$};\tac$_2$}} + +This tactic operator is a generalized composition for sequencing. The +tactical {\tac}$_1$ {\tt ;} \tac$_2$ first applies \tac$_1$ and then +applies \tac$_2$ to any subgoal generated by \tac$_1$. {\tt ;} +associates to the left. + +\subsection{\tt \tac$_0$; [ \tac$_1$ | \dots\ | \tac$_n$ ]} +\tacindex{;[\ldots$\mid$\ldots$\mid$\ldots]} +\index{Tacticals!zz@{\tt {\tac$_0$};[{\tac$_1$}$\mid$\ldots$\mid$\tac$_n$]}} + +This tactic operator is a generalization of the precedent tactics +operator. The tactical {\tt \tac$_0$ ; [ \tac$_1$ | \dots\ | \tac$_n$ + ]} first applies \tac$_0$ and then applies \tac$_i$ to the i-th +subgoal generated by \tac$_0$. It fails if $n$ is not the exact number +of remaining subgoals. + +\subsection{\tt try {\tac}} +\tacindex{try} +\index{Tacticals!try@{\tt try}} + +This tactic operator applies tactic \tac, and catches the possible +failure of \tac. It never fails. + +\subsection{\tt first [ \tac$_0$ | \dots\ | \tac$_n$ ]} +\tacindex{first} +\index{Tacticals!first@{\tt first}} + +This tactic operator tries to apply the tactics \tac$_i$ with $i=0\ldots{}n$, +starting from $i=0$, until one of them does not fail. It fails if all the +tactics fail. + +\begin{ErrMsgs} +\item \errindex{No applicable tactic.} +\end{ErrMsgs} + +\subsection{\tt solve [ \tac$_0$ | \dots\ | \tac$_n$ ]} +\tacindex{solve} +\index{Tacticals!solve@{\tt solve}} + +This tactic operator tries to solve the current goal with the tactics \tac$_i$ +with $i=0\ldots{}n$, starting from $i=0$, until one of them solves. It fails if +no tactic can solve. + +\begin{ErrMsgs} +\item \errindex{Cannot solve the goal.} +\end{ErrMsgs} + +\subsection{\tt info {\tac}} +\tacindex{info} +\index{Tacticals!info@{\tt info}} + +This is not really a tactical. For elementary tactics, this is +equivalent to \tac. For complex tactic like \texttt{auto}, it displays +the operations performed by the tactic. + +\subsection{\tt abstract {\tac}} +\tacindex{abstract} +\index{Tacticals!abstract@{\tt abstract}} + +From outside, typing \texttt{abstract \tac} is the same that +typing \tac. 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. + +This tactical is useful with tactics such \texttt{omega} or +\texttt{discriminate} that generate big proof terms. With that tool +the user can avoid the explosion at time of the \texttt{Save} command +without having to cut ``by hand'' the proof in smaller lemmas. + +\begin{Variants} + +\item \texttt{abstract {\tac} using {\ident}}. + + Give explicitly the name of the auxiliary lemma. + +\end{Variants} + \section{Generation of induction principles with {\tt Scheme}} \label{Scheme} \comindex{Scheme} @@ -2710,34 +2927,31 @@ e.g. \texttt{Require Import A.}). The {\tt Scheme} command is a high-level tool for generating automatically (possibly mutual) induction principles for given types and sorts. Its syntax follows the schema: - -\noindent +\begin{tabbing} {\tt Scheme {\ident$_1$} := Induction for \ident'$_1$ Sort {\sort$_1$} \\ with\\ \mbox{}\hspace{0.1cm} \dots\ \\ with {\ident$_m$} := Induction for {\ident'$_m$} Sort - {\sort$_m$}}\\ - + {\sort$_m$}} +\end{tabbing} \ident'$_1$ \dots\ \ident'$_m$ are different inductive type -identifiers belonging to -the same package of mutual inductive definitions. This command -generates {\ident$_1$}\dots{} {\ident$_m$} to be mutually recursive -definitions. Each term {\ident$_i$} proves a general principle -of mutual induction for objects in type {\term$_i$}. - +identifiers belonging to the same package of mutual inductive +definitions. This command generates {\ident$_1$}\dots{} {\ident$_m$} +to be mutually recursive definitions. Each term {\ident$_i$} proves a +general principle of mutual induction for objects in type {\term$_i$}. \begin{Variants} \item {\tt Scheme {\ident$_1$} := Minimality for \ident'$_1$ Sort {\sort$_1$} \\ with\\ \mbox{}\hspace{0.1cm} \dots\ \\ with {\ident$_m$} := Minimality for {\ident'$_m$} Sort - {\sort$_m$}}\\ + {\sort$_m$}} + Same as before but defines a non-dependent elimination principle more natural in case of inductively defined relations. \end{Variants} -\SeeAlso \ref{Scheme-examples} - +\SeeAlso Section~\ref{Scheme-examples} \section{Generation of induction principles with {\tt Functional Scheme}} \label{FunScheme} @@ -2746,36 +2960,34 @@ of mutual induction for objects in type {\term$_i$}. The {\tt Functional Scheme} command is a high-level experimental tool for generating automatically induction principles corresponding to (possibly mutually recursive) functions. Its -syntax follows the schema:\bigskip - -\noindent +syntax follows the schema: +\begin{tabbing} {\tt Functional Scheme {\ident$_i$} := Induction for - \ident'$_i$ with \ident'$_1$ \dots\ \ident'$_m$.}\\ - - \ident'$_1$ \dots\ \ident'$_m$ are the names of mutually - recursive functions (they must be in the same order as when - they were defined), \ident'$_i$ being one of them. This command - generates the induction principle \ident$_i$, following the - recursive structure and case analyses of the functions - \ident'$_1$ \dots\ \ident'$_m$, and having \ident'$_i$ as entry - point. + \ident'$_i$ with \ident'$_1$ \dots\ \ident'$_m$.} +\end{tabbing} +\ident'$_1$ \dots\ \ident'$_m$ are the names of mutually recursive +functions (they must be in the same order as when they were defined), +\ident'$_i$ being one of them. This command generates the induction +principle \ident$_i$, following the recursive structure and case +analyses of the functions \ident'$_1$ \dots\ \ident'$_m$, and having +\ident'$_i$ as entry point. \begin{Variants} -\item {\tt Functional Scheme {\ident$_1$} := Induction for \ident'$_1$.}\\ +\item {\tt Functional Scheme {\ident$_1$} := Induction for \ident'$_1$.} This command is a shortcut for: - + \begin{tabbing} {\tt Functional Scheme {\ident$_1$} := Induction for \ident'$_1$ with \ident'$_1$.} +\end{tabbing} - This variant can be used for non mutually recursive functions only. +This variant can be used for non mutually recursive functions only. \end{Variants} -\SeeAlso \ref{FunScheme-examples} +\SeeAlso Section~\ref{FunScheme-examples} \section{Simple tactic macros} -\index[tactic]{tactic macros} \index{tactic macros} \comindex{Tactic Definition} \label{TacticDefinition} diff --git a/doc/RefMan-tacex.tex b/doc/RefMan-tacex.tex index 7a411e822..def17e717 100644 --- a/doc/RefMan-tacex.tex +++ b/doc/RefMan-tacex.tex @@ -807,7 +807,7 @@ is undecidable in general case, don't expect miracles from it! \SeeAlso comments of source file \texttt{tactics/contrib/polynom/quote.ml} -\SeeAlso the tactic \texttt{ring} (chapter \ref{ring}) +\SeeAlso the \texttt{ring} tactic (Chapter~\ref{ring}) \section{Using the tactical language} diff --git a/doc/Reference-Manual.tex b/doc/Reference-Manual.tex index 853189c6f..4d876f71e 100644 --- a/doc/Reference-Manual.tex +++ b/doc/Reference-Manual.tex @@ -79,13 +79,6 @@ \nocite{*} \bibliographystyle{plain} \bibliography{biblio} -%BEGIN LATEX -\RefManCutCommand{psselect -q -p-$ENDREFMAN,$BEGINBIBLIO- Reference-Manual.ps Reference-Manual-base.ps} -\RefManCutCommand{psselect -q -p$BEGINADDENDUM-$ENDADDENDUM Reference-Manual.ps Reference-Manual-addendum.ps} -\RefManCutCommand{dviselect -i Reference-Manual.dvi -o Reference-Manual-base.dvi 1-$ENDREFMAN $BEGINBIBLIO-} -\RefManCutCommand{dviselect -i Reference-Manual.dvi -o Reference-Manual-addendum.dvi $BEGINADDENDUM-$ENDADDENDUM} -\RefManCutClose -%END LATEX \printindex @@ -95,6 +88,17 @@ \printindex[error] +\listoffigures +%\listoftables + +%BEGIN LATEX +\RefManCutCommand{psselect -q -p-$ENDREFMAN,$BEGINBIBLIO- Reference-Manual.ps Reference-Manual-base.ps} +\RefManCutCommand{psselect -q -p$BEGINADDENDUM-$ENDADDENDUM Reference-Manual.ps Reference-Manual-addendum.ps} +\RefManCutCommand{dviselect -i Reference-Manual.dvi -o Reference-Manual-base.dvi 1-$ENDREFMAN $BEGINBIBLIO-} +\RefManCutCommand{dviselect -i Reference-Manual.dvi -o Reference-Manual-addendum.dvi $BEGINADDENDUM-$ENDADDENDUM} +\RefManCutClose +%END LATEX + \end{document} diff --git a/doc/Setoid.tex b/doc/Setoid.tex index 68260e085..6d45411c3 100644 --- a/doc/Setoid.tex +++ b/doc/Setoid.tex @@ -1,18 +1,18 @@ -\achapter{The \texttt{Setoid\_replace} tactic} +\achapter{The \texttt{setoid\_replace} tactic} \aauthor{Cl\'ement Renard} -\label{Setoid_replace} -\tacindex{Setoid\_replace} +\label{setoid_replace} +\tacindex{setoid\_replace} -This chapter presents the \texttt{Setoid\_replace} tactic. +This chapter presents the \texttt{setoid\_replace} tactic. -\asection{Description of \texttt{Setoid\_replace}} +\asection{Description of \texttt{setoid\_replace}} Working on user-defined structures in \Coq\ is not very easy if Leibniz equality does not denote the intended equality. For example using lists to denote finite sets drive to difficulties since two non convertible terms can denote the same set. -We present here a \Coq\ module, {\tt Setoid\_replace}, which allow to +We present here a \Coq\ module, {\tt setoid\_replace}, which allow to structure and automate some parts of the work. In particular, if everything has been registered a simple tactic can do replacement just as if the two terms were equal. @@ -20,17 +20,11 @@ tactic can do replacement just as if the two terms were equal. \asection{Adding new setoid or morphisms} Under the toplevel -load the \texttt{Setoid\_replace} files with the command: +load the \texttt{setoid\_replace} files with the command: -\begin{coq_eval} +\begin{coq_example*} Require Setoid. -\end{coq_eval} - -\begin{quotation} -\begin{verbatim} -Require Setoid. -\end{verbatim} -\end{quotation} +\end{coq_example*} A setoid is just a type \verb+A+ and an equivalence relation on \verb+A+. @@ -96,7 +90,7 @@ And when you load a compiled file, all the \texttt{Add Setoid} commands of this file that are not inside a section will be loaded. \Warning Only the setoid on \texttt{Prop} is loaded by default with the -\texttt{Setoid\_replace} module. The equivalence relation used is +\texttt{setoid\_replace} module. The equivalence relation used is \texttt{iff} {\it i.e.} the logical equivalence. \asection{Adding new morphisms} @@ -129,28 +123,28 @@ The compatibility lemma genereted depends on the setoids already declared. \asection{The tactic itself} -\tacindex{Setoid\_replace} -\tacindex{Setoid\_rewrite} +\tacindex{setoid\_replace} +\tacindex{setoid\_rewrite} After having registered all the setoids and morphisms you need, you can -use the tactic called \texttt{Setoid\_replace}. The syntax is +use the tactic called \texttt{setoid\_replace}. The syntax is \begin{quotation} -\texttt{Setoid\_replace} $ term_1$ with $term_2$ +\texttt{setoid\_replace} $ term_1$ with $term_2$ \end{quotation} The effect is similar to the one of \texttt{Replace}. -You also have a tactic called \texttt{Setoid\_rewrite} which is the +You also have a tactic called \texttt{setoid\_rewrite} which is the equivalent of \texttt{Rewrite} for setoids. The syntax is \begin{quotation} -\texttt{Setoid\_rewrite} \term +\texttt{setoid\_rewrite} \term \end{quotation} \begin{Variants} - \item \texttt{Setoid\_rewrite ->} \term - \item \texttt{Setoid\_rewrite <-} \term + \item \texttt{setoid\_rewrite ->} \term + \item \texttt{setoid\_rewrite <-} \term \end{Variants} The arrow tells the systems in which direction the rewriting has to be diff --git a/doc/Translator.tex b/doc/Translator.tex index 5ebee7fdf..423e22755 100644 --- a/doc/Translator.tex +++ b/doc/Translator.tex @@ -23,7 +23,8 @@ \def\NT#1{\langle\textit{#1}\rangle} \def\NTL#1#2{\langle\textit{#1}\rangle_{#2}} -\def\TERM#1{\textsf{\bf #1}} +%\def\TERM#1{\textsf{\bf #1}} +\def\TERM#1{\texttt{#1}} \newenvironment{transbox} {\begin{center}\tt\begin{tabular}{l|ll} \hfil\textrm{V7} & \hfil\textrm{V8} \\ \hline} {\end{tabular}\end{center}} @@ -79,8 +80,8 @@ the eager user who wants to start with the new syntax quickly. The toplevel has an option {\tt -translate} which allows to interactively translate commands. This toplevel translator accepts a -command, prints the translation on standard output (after a \verb+New -syntax:+ balise), executes the command, and waits for another +command, prints the translation on standard output (after a % +\verb+New syntax:+ balise), executes the command, and waits for another command. The only requirements is that they should be syntactically correct, but they do not have to be well-typed. @@ -103,6 +104,7 @@ syntax that changed and how they were translated. All the examples below can be tested by entering the V7 commands in the toplevel translator. + %% \subsection{Changes in lexical conventions w.r.t. V7} @@ -113,7 +115,7 @@ The lexical conventions changed: \TERM{_} is not a regular identifier anymore. It is used in terms as a placeholder for subterms to be inferred at type-checking, and in patterns as a non-binding variable. -Furthermore, only letters (unicode letters), digits, single quotes and +Furthermore, only letters (Unicode letters), digits, single quotes and _ are allowed after the first character. \subsubsection{Quoted string} @@ -121,7 +123,7 @@ _ are allowed after the first character. Quoted strings are used typically to give a filename (which may not be a regular identifier). As before they are written between double quotes ("). Unlike for V7, there is no escape character: characters -are written normaly but the double quote which is doubled. +are written normally except the double quote which is doubled. \begin{transbox} \TRANS{"abcd$\backslash\backslash$efg"}{"abcd$\backslash$efg"} @@ -171,7 +173,7 @@ to be used when notations of several scopes appear in the same expression. In examples below, scope changes are not needed if the appropriate scope -has been opened. Scope nat_scope is opened in the initial state of Coq. +has been opened. Scope \verb|nat_scope| is opened in the initial state of Coq. \begin{transbox} \TRANSCOM{`0+x=x+0`}{0+x=x+0}{\textrm{Z_scope}} \TRANSCOM{``0 + [if b then ``1`` else ``2``]``}{0 + if b then 1 else 2}{\textrm{R_scope}} @@ -182,23 +184,21 @@ Below is a table that tells which notation is available in which scope. The relative precedences and associativity of operators is the same as in usual mathematics. See the reference manual for more details. However, it is important to remember that unlike V7, the type -operators for product and sum are left associative, in order not to +operators for product and sum are left-associative, in order not to clash with arithmetic operators. \begin{center} \begin{tabular}{l|l} scope & notations \\ \hline -nat_scope & $+ ~- ~* ~< ~\leq ~> ~\geq$ \\ -Z_scope & $+ ~- ~* ~/ ~\TERM{mod} ~< ~\leq ~> ~\geq ~?=$ \\ -R_scope & $+ ~- ~* ~/ ~< ~\leq ~> ~\geq$ \\ -type_scope & $* ~+$ \\ -bool_scope & $\TERM{\&\&} ~\TERM{$||$} ~\TERM{-}$ \\ -list_scope & $\TERM{::} ~\TERM{++}$ +nat_scope & \texttt{+ - * < <= > >=} \\ +Z_scope & \texttt{+ - * / mod < <= > >= ?=} \\ +R_scope & \texttt{+ - * / < <= > >=} \\ +type_scope & \texttt{* +} \\ +bool_scope & \texttt{\&\& || -} \\ +list_scope & \texttt{:: ++} \end{tabular} \end{center} -(Note: $\leq$ stands for \TERM{$<=$}) - \subsubsection{Notation for implicit arguments} @@ -206,7 +206,7 @@ list_scope & $\TERM{::} ~\TERM{++}$ The explicitation of arguments is closer to the \emph{bindings} notation in tactics. Argument positions follow the argument names of the head constant. The example below assumes \verb+f+ is a function -with 2 dependent arguments named \verb+x+ and \verb+y+, and a third +with two dependent arguments named \verb+x+ and \verb+y+, and a third non-dependent argument. \begin{transbox} \TRANS{f 1!t1 2!t2 3!t3}{f (x:=t1) (y:=t2) (1:=t3)} @@ -226,14 +226,14 @@ written {\tt _} \subsubsection{Universal quantification} The universal quantification and dependent product types are now -materialized with the \TERM{forall} keyword before the binders and a +introduced by the \texttt{forall} keyword before the binders and a comma after the binders. The syntax of binders also changed significantly. A binder can simply be a name when its type can be inferred. In other cases, the name and the type of the variable are put between parentheses. When several consecutive variables have the same type, they can be grouped. Finally, if all variables -have the same type parentheses can be omitted. +have the same type, parentheses can be omitted. \begin{transbox} \TRANS{(x:A)B}{forall (x:~A), B ~~\textrm{or}~~ forall x:~A, B} @@ -246,8 +246,8 @@ have the same type parentheses can be omitted. \subsubsection{Abstraction} The notation for $\lambda$-abstraction follows that of universal -quantification. The binders are surrounded by keyword \TERM{fun} -and $\Rightarrow$ (\verb+=>+ in ascii). +quantification. The binders are surrounded by keyword \texttt{fun} +and \verb+=>+. \begin{transbox} \TRANS{[x,y:nat; z](f a b c)}{fun (x y:nat) z => f a b c} @@ -301,7 +301,7 @@ dependent case analysis. \subsubsection{Fixpoints and cofixpoints} -An easier syntax for non-mutual fixpoints is provided, making it very close +An simpler syntax for non-mutual fixpoints is provided, making it very close to the usual notation for non-recursive functions. The decreasing argument is now indicated by an annotation between curly braces, regardless of the binders grouping. The annotation can be omitted if the binders introduce only @@ -389,8 +389,8 @@ Ltac by default. \subsubsection{Occurrences} -To avoid ambiguity between a numeric literal and the optionnal -occurence numbers of this term, the occurence numbers are put after +To avoid ambiguity between a numeric literal and the optional +occurrence numbers of this term, the occurrence numbers are put after the term itself and after keyword \TERM{as}. \begin{transbox} \TRANS{Pattern 1 2 (f x) 3 4 d y z}{pattern f x at 1 2, d at 3 4, y, z} @@ -605,7 +605,7 @@ try and make the translation. \subsubsection{The general case} The preferred way is to use script {\tt translate-v8} if your development -is compiled by a Makfile with the following constraints: +is compiled by a Makefile with the following constraints: \begin{itemize} \item compilation is achievd by invoke make without specifying a target \item options are passed to Coq with make variable COQFLAGS that @@ -683,6 +683,8 @@ If the choices made by translation or in the following cases: the user should change his development prior to translation. +\subsubsection{Syntax extensions} + \subsubsection{{\tt Case} and {\tt Match}} These very low-level case analysis are no longer supported. The @@ -693,20 +695,19 @@ to determine the context in which terms appearing in tactics live.}. If this happens, it is preferable to transform it manually before translation. - \subsubsection{Syntax extensions with {\tt Grammar} and {\tt Syntax}} {\tt Grammar} and {\tt Syntax} are no longer supported. They should be replaced by an equivalent {\tt Notation} command and be -processed as decribed above. Before attempting translation, users +processed as described above. Before attempting translation, users should verify that compilation with option {\tt -v7} succeeds. In the cases where {\tt Grammar} and {\tt Syntax} cannot be emulated by {\tt Notation}, users have to change manually they development as they wish to avoid the use of {\tt Grammar}. If this is not done, the translator will simply expand the notations and the output of the -translator will use the reuglar Coq syntax. +translator will use the regular Coq syntax. \subsubsection{Syntax extensions with {\tt Notation} and {\tt Infix}} @@ -891,5 +892,6 @@ In the case you want to adopt the new semantics of {\tt Set Implicit Warning: changing the number of implicit arguments can break the notations. Then use the {\tt V8only} modifier of {\tt Notation}. +>>>>>>> 1.4 \end{document} diff --git a/doc/headers.tex b/doc/headers.tex index c10dca58e..277b62021 100644 --- a/doc/headers.tex +++ b/doc/headers.tex @@ -82,6 +82,7 @@ Vernacular Commands Index} \newcommand{\comindex}[1]{% \index{#1@\texttt{#1}}\index[command]{#1@\texttt{#1}}} \newcommand{\errindex}[1]{\texttt{#1}\index[error]{#1}} +\newcommand{\errindexbis}[2]{\texttt{#1}\index[error]{#2}} \newcommand{\ttindex}[1]{\index{#1@\texttt{#1}}} \makeatother diff --git a/doc/macros.tex b/doc/macros.tex index 8084d8f94..71f223ad6 100755 --- a/doc/macros.tex +++ b/doc/macros.tex @@ -405,11 +405,10 @@ % placement of figures -\renewcommand{\topfraction}{.95} -\renewcommand{\bottomfraction}{.95} -\renewcommand{\textfraction}{.05} -\renewcommand{\floatpagefraction}{.8} - +\renewcommand{\topfraction}{.99} +\renewcommand{\bottomfraction}{.99} +\renewcommand{\textfraction}{.01} +\renewcommand{\floatpagefraction}{.9} % Macros Bruno pour description de la syntaxe |