diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/Makefile | 12 | ||||
| -rwxr-xr-x | doc/common/macros.tex | 5 | ||||
| -rw-r--r-- | doc/refman/Cases.tex | 93 | ||||
| -rw-r--r-- | doc/refman/RefMan-cic.tex | 185 | ||||
| -rw-r--r-- | doc/refman/RefMan-com.tex | 8 | ||||
| -rw-r--r-- | doc/refman/RefMan-ext.tex | 56 | ||||
| -rw-r--r-- | doc/refman/RefMan-gal.tex | 234 | ||||
| -rw-r--r-- | doc/refman/RefMan-ide.tex | 9 | ||||
| -rw-r--r-- | doc/refman/RefMan-ltac.tex | 262 | ||||
| -rw-r--r-- | doc/refman/RefMan-mod.tex | 46 | ||||
| -rw-r--r-- | doc/refman/RefMan-oth.tex | 100 | ||||
| -rw-r--r-- | doc/refman/RefMan-pre.tex | 16 | ||||
| -rw-r--r-- | doc/refman/RefMan-pro.tex | 19 | ||||
| -rw-r--r-- | doc/refman/RefMan-syn.tex | 74 | ||||
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 273 | ||||
| -rw-r--r-- | doc/refman/Reference-Manual.tex | 4 | ||||
| -rw-r--r-- | doc/refman/cover.html | 3 | ||||
| -rw-r--r-- | doc/refman/index.html | 31 | ||||
| -rw-r--r-- | doc/refman/menu.html | 29 | ||||
| -rwxr-xr-x | doc/tutorial/Tutorial.tex | 31 |
20 files changed, 1125 insertions, 365 deletions
diff --git a/doc/Makefile b/doc/Makefile index fd508e07..6209b0c8 100644 --- a/doc/Makefile +++ b/doc/Makefile @@ -110,7 +110,7 @@ REFMANCOQTEXFILES=\ refman/RefMan-mod.v.tex refman/RefMan-tac.v.tex \ refman/RefMan-cic.v.tex refman/RefMan-lib.v.tex \ refman/RefMan-tacex.v.tex refman/RefMan-syn.v.tex \ - refman/RefMan-oth.v.tex \ + refman/RefMan-oth.v.tex refman/RefMan-ltac.v.tex \ refman/Cases.v.tex refman/Coercion.v.tex refman/Extraction.v.tex \ refman/Program.v.tex refman/Omega.v.tex refman/Polynom.v.tex \ refman/Setoid.v.tex refman/Helm.tex # refman/Natural.v.tex @@ -119,7 +119,7 @@ REFMANTEXFILES=\ refman/headers.tex \ refman/Reference-Manual.tex refman/RefMan-pre.tex \ refman/RefMan-int.tex refman/RefMan-pro.tex \ - refman/RefMan-com.tex refman/RefMan-ltac.tex \ + refman/RefMan-com.tex \ refman/RefMan-uti.tex refman/RefMan-ide.tex \ refman/RefMan-add.tex refman/RefMan-modr.tex \ $(REFMANCOQTEXFILES) \ @@ -161,9 +161,15 @@ refman/html/index.html: refman/Reference-Manual.html $(REFMANPNGFILES) \ mkdir refman/html cp $(REFMANPNGFILES) refman/html (cd refman/html; hacha -o toc.html ../Reference-Manual.html) - cp refman/cover.html refman/html + cp refman/cover.html refman/menu.html refman/html cp refman/index.html refman/html +refman-quick: + (cd refman; \ + $(PDFLATEX) Reference-Manual.tex; \ + hevea -fix -exec xxdate.exe ./Reference-Manual.tex) + + ###################################################################### # Tutorial ###################################################################### diff --git a/doc/common/macros.tex b/doc/common/macros.tex index 393b8547..2465d70f 100755 --- a/doc/common/macros.tex +++ b/doc/common/macros.tex @@ -161,6 +161,7 @@ \newcommand{\form}{\textrm{\textsl{form}}} \newcommand{\entry}{\textrm{\textsl{entry}}} \newcommand{\proditem}{\textrm{\textsl{production\_item}}} +\newcommand{\taclevel}{\textrm{\textsl{tactic\_level}}} \newcommand{\tacargtype}{\textrm{\textsl{tactic\_argument\_type}}} \newcommand{\scope}{\textrm{\textsl{scope}}} \newcommand{\optscope}{\textrm{\textsl{opt\_scope}}} @@ -182,6 +183,7 @@ \newcommand{\name}{\textrm{\textsl{name}}} \newcommand{\num}{\textrm{\textsl{num}}} \newcommand{\pattern}{\textrm{\textsl{pattern}}} +\newcommand{\orpattern}{\textrm{\textsl{or\_pattern}}} \newcommand{\intropattern}{\textrm{\textsl{intro\_pattern}}} \newcommand{\pat}{\textrm{\textsl{pat}}} \newcommand{\pgs}{\textrm{\textsl{pgms}}} @@ -200,6 +202,7 @@ \newcommand{\str}{\textrm{\textsl{string}}} \newcommand{\subsequentletter}{\textrm{\textsl{subsequent\_letter}}} \newcommand{\switch}{\textrm{\textsl{switch}}} +\newcommand{\messagetoken}{\textrm{\textsl{message\_token}}} \newcommand{\tac}{\textrm{\textsl{tactic}}} \newcommand{\terms}{\textrm{\textsl{terms}}} \newcommand{\term}{\textrm{\textsl{term}}} @@ -488,7 +491,7 @@ {\begin{center}\begin{rulebox}} {\end{rulebox}\end{center}} -% $Id: macros.tex 8606 2006-02-23 13:58:10Z herbelin $ +% $Id: macros.tex 9038 2006-07-11 13:53:53Z herbelin $ %%% Local Variables: diff --git a/doc/refman/Cases.tex b/doc/refman/Cases.tex index a05231cd..dfe9e94c 100644 --- a/doc/refman/Cases.tex +++ b/doc/refman/Cases.tex @@ -1,5 +1,5 @@ \achapter{Extended pattern-matching}\defaultheaders -\aauthor{Cristina Cornes} +\aauthor{Cristina Cornes and Hugo Herbelin} \label{Mult-match-full} \ttindex{Cases} @@ -17,32 +17,38 @@ pattern. It is recommended to start variable names by a lowercase letter. If a pattern has the form $(c~\vec{x})$ where $c$ is a constructor -symbol and $\vec{x}$ is a linear vector of variables, it is called -{\em simple}: it is the kind of pattern recognized by the basic -version of {\tt match}. If a pattern is -not simple we call it {\em nested}. +symbol and $\vec{x}$ is a linear vector of (distinct) variables, it is +called {\em simple}: it is the kind of pattern recognized by the basic +version of {\tt match}. On the opposite, if it is a variable $x$ or +has the form $(c~\vec{p})$ with $p$ not only made of variables, the +pattern is called {\em nested}. A variable pattern matches any value, and the identifier is bound to that value. The pattern ``\texttt{\_}'' (called ``don't care'' or -``wildcard'' symbol) also matches any value, but does not bind anything. It -may occur an arbitrary number of times in a pattern. Alias patterns -written \texttt{(}{\sl pattern} \texttt{as} {\sl identifier}\texttt{)} are -also accepted. This pattern matches the same values as {\sl pattern} -does and {\sl identifier} is bound to the matched value. A list of -patterns separated with commas -is also considered as a pattern and is called {\em multiple -pattern}. +``wildcard'' symbol) also matches any value, but does not bind +anything. It may occur an arbitrary number of times in a +pattern. Alias patterns written \texttt{(}{\sl pattern} \texttt{as} +{\sl identifier}\texttt{)} are also accepted. This pattern matches the +same values as {\sl pattern} does and {\sl identifier} is bound to the +matched value. +A pattern of the form {\pattern}{\tt |}{\pattern} is called +disjunctive. A list of patterns separated with commas is also +considered as a pattern and is called {\em multiple pattern}. However +multiple patterns can only occur at the root of pattern-matching +equations. Disjunctions of {\em multiple pattern} are allowed though. Since extended {\tt match} expressions are compiled into the primitive ones, the expressiveness of the theory remains the same. Once the -stage of parsing has finished only simple patterns remain. An easy way -to see the result of the expansion is by printing the term with -\texttt{Print} if the term is a constant, or using the command +stage of parsing has finished only simple patterns remain. Re-nesting +of pattern is performed at printing time. An easy way to see the +result of the expansion is to toggle off the nesting performed at +printing (use here {\tt Set Printing Matching}), then by printing the term +with \texttt{Print} if the term is a constant, or using the command \texttt{Check}. The extended \texttt{match} still accepts an optional {\em elimination predicate} given after the keyword \texttt{return}. Given a pattern -matching expression, if all the right hand sides of \texttt{=>} ({\em +matching expression, if all the right-hand-sides of \texttt{=>} ({\em rhs} in short) have the same type, then this type can be sometimes synthesized, and so we can omit the \texttt{return} part. Otherwise the predicate after \texttt{return} has to be provided, like for the basic @@ -64,7 +70,9 @@ Fixpoint max (n m:nat) {struct m} : nat := end. \end{coq_example} -Using multiple patterns in the definition allows to write: +\paragraph{Multiple patterns} + +Using multiple patterns in the definition of {\tt max} allows to write: \begin{coq_example} Reset max. @@ -89,7 +97,9 @@ Check (fun x:nat => match x return nat with end). \end{coq_example} -We can also use ``\texttt{as} patterns'' to associate a name to a +\paragraph{Aliasing subpatterns} + +We can also use ``\texttt{as} {\ident}'' to associate a name to a sub-pattern: \begin{coq_example} @@ -102,6 +112,8 @@ Fixpoint max (n m:nat) {struct n} : nat := end. \end{coq_example} +\paragraph{Nested patterns} + Here is now an example of nested patterns: \begin{coq_example} @@ -157,7 +169,6 @@ Fixpoint lef (n m:nat) {struct m} : bool := end. \end{coq_example} - Here the last pattern superposes with the first two. Because of the priority rule, the last pattern will be used only for values that do not match neither the first nor @@ -180,12 +191,50 @@ Check (fun x:nat => end). \end{coq_example} +\paragraph{Disjunctive patterns} + +Multiple patterns that share the same right-hand-side can be +factorized using the notation \nelist{\multpattern}{\tt |}. For instance, +{\tt max} can be rewritten as follows: + +\begin{coq_eval} +Reset max. +\end{coq_eval} +\begin{coq_example} +Fixpoint max (n m:nat) {struct m} : nat := + match n, m with + | S n', S m' => S (max n' m') + | 0, p | p, 0 => p + end. +\end{coq_example} + +Similarly, factorization of (non necessary multiple) patterns +that share the same variables is possible by using the notation +\nelist{\pattern}{\tt |}. Here is an example: + +\begin{coq_example} +Definition filter_2_4 (n:nat) : nat := + match n with + | 2 as m | 4 as m => m + | _ => 0 + end. +\end{coq_example} + +Here is another example using disjunctive subpatterns. + +\begin{coq_example} +Definition filter_some_square_corners (p:nat*nat) : nat*nat := + match p with + | ((2 as m | 4 as m), (3 as n | 5 as n)) => (m,n) + | _ => (0,0) + end. +\end{coq_example} + \asection{About patterns of parametric types} When matching objects of a parametric type, constructors in patterns {\em do not expect} the parameter arguments. Their value is deduced during expansion. - -Consider for example the polymorphic lists: +Consider for example the type of polymorphic lists: \begin{coq_example} Inductive List (A:Set) : Set := diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex index e288cdfb..0a2f5904 100644 --- a/doc/refman/RefMan-cic.tex +++ b/doc/refman/RefMan-cic.tex @@ -218,10 +218,10 @@ either an assumption, written $x:T$ ($T$ is a type) or a definition, written $x:=t:T$. We use brackets to write contexts. A typical example is $[x:T;y:=u:U;z:V]$. Notice that the variables declared in a context must be distinct. If $\Gamma$ declares some $x$, -we write $x \in\Gamma$. By writing $(x:T)\in\Gamma$ we mean that +we write $x \in \Gamma$. By writing $(x:T) \in \Gamma$ we mean that either $x:T$ is an assumption in $\Gamma$ or that there exists some $t$ such that $x:=t:T$ is a definition in $\Gamma$. If $\Gamma$ defines some -$x:=t:T$, we also write $(x:=t:T)\in\Gamma$. Contexts must be +$x:=t:T$, we also write $(x:=t:T) \in \Gamma$. Contexts must be themselves {\em well formed}. For the rest of the chapter, the notation $\Gamma::(y:T)$ (resp. $\Gamma::(y:=t:T)$) denotes the context $\Gamma$ enriched with the declaration $y:T$ (resp. $y:=t:T$). The @@ -233,8 +233,8 @@ notation $[]$ denotes the empty context. \index{Context} We define the inclusion of two contexts $\Gamma$ and $\Delta$ (written as $\Gamma \subset \Delta$) as the property, for all variable $x$, -type $T$ and term $t$, if $(x:T) \in \Gamma$ then $(x:T)\in \Delta$ -and if $(x:=t:T) \in \Gamma$ then $(x:=t:T)\in \Delta$. +type $T$ and term $t$, if $(x:T) \in \Gamma$ then $(x:T) \in \Delta$ +and if $(x:=t:T) \in \Gamma$ then $(x:=t:T) \in \Delta$. %We write % $|\Delta|$ for the length of the context $\Delta$, that is for the number % of declarations (assumptions or definitions) in $\Delta$. @@ -288,28 +288,30 @@ be derived from the following rules. \begin{description} \item[W-E] \inference{\WF{[]}{[]}} \item[W-S] % Ce n'est pas vrai : x peut apparaitre plusieurs fois dans Gamma -\inference{\frac{\WTEG{T}{s}~~~~s\in \Sort~~~~x \not\in +\inference{\frac{\WTEG{T}{s}~~~~s \in \Sort~~~~x \not\in \Gamma % \cup E } {\WFE{\Gamma::(x:T)}}~~~~~ \frac{\WTEG{t}{T}~~~~x \not\in \Gamma % \cup E }{\WFE{\Gamma::(x:=t:T)}}} -\item[Def] \inference{\frac{\WTEG{t}{T}~~~c \notin E\cup \Gamma} +\item[Def] \inference{\frac{\WTEG{t}{T}~~~c \notin E \cup \Gamma} {\WF{E;\Def{\Gamma}{c}{t}{T}}{\Gamma}}} +\item[Assum] \inference{\frac{\WTEG{T}{s}~~~~s \in \Sort~~~~c \notin E \cup \Gamma} + {\WF{E;\Assum{\Gamma}{c}{T}}{\Gamma}}} \item[Ax] \index{Typing rules!Ax} \inference{\frac{\WFE{\Gamma}}{\WTEG{\Prop}{\Type(p)}}~~~~~ \frac{\WFE{\Gamma}}{\WTEG{\Set}{\Type(q)}}} \inference{\frac{\WFE{\Gamma}~~~~i<j}{\WTEG{\Type(i)}{\Type(j)}}} \item[Var]\index{Typing rules!Var} - \inference{\frac{ \WFE{\Gamma}~~~~~(x:T)\in\Gamma~~\mbox{or}~~(x:=t:T)\in\Gamma~\mbox{for some $t$}}{\WTEG{x}{T}}} + \inference{\frac{ \WFE{\Gamma}~~~~~(x:T) \in \Gamma~~\mbox{or}~~(x:=t:T) \in \Gamma~\mbox{for some $t$}}{\WTEG{x}{T}}} \item[Const] \index{Typing rules!Const} -\inference{\frac{\WFE{\Gamma}~~~~(c:T) \in E}{\WTEG{c}{T}}} +\inference{\frac{\WFE{\Gamma}~~~~(c:T) \in E~~\mbox{or}~~(c:=t:T) \in E~\mbox{for some $t$} }{\WTEG{c}{T}}} \item[Prod] \index{Typing rules!Prod} \inference{\frac{\WTEG{T}{s}~~~~s \in \Sort~~~ \WTE{\Gamma::(x:T)}{U}{\Prop}} { \WTEG{\forall~x:T,U}{\Prop}}} -\inference{\frac{\WTEG{T}{s}~~~~s\in\{\Prop, \Set\}~~~~~~ +\inference{\frac{\WTEG{T}{s}~~~~s \in\{\Prop, \Set\}~~~~~~ \WTE{\Gamma::(x:T)}{U}{\Set}} { \WTEG{\forall~x:T,U}{\Set}}} \inference{\frac{\WTEG{T}{\Type(i)}~~~~i\leq k~~~ @@ -373,7 +375,7 @@ environment. It is legal to identify such a reference with its value, that is to expand (or unfold) it into its value. This reduction is called $\delta$-reduction and shows as follows. -$$\WTEGRED{x}{\triangleright_{\delta}}{t}~~~~~\mbox{if $(x:=t:T)\in\Gamma$}~~~~~~~~~\WTEGRED{c}{\triangleright_{\delta}}{t}~~~~~\mbox{if $(c:=t:T)\in E$}$$ +$$\WTEGRED{x}{\triangleright_{\delta}}{t}~~~~~\mbox{if $(x:=t:T) \in \Gamma$}~~~~~~~~~\WTEGRED{c}{\triangleright_{\delta}}{t}~~~~~\mbox{if $(c:=t:T) \in E$}$$ \paragraph{$\zeta$-reduction.} @@ -553,15 +555,13 @@ represented by: \List}\] Assuming $\Gamma_I$ is $[I_1:A_1;\ldots;I_k:A_k]$, and $\Gamma_C$ is - $[c_1:C_1;\ldots;c_n:C_n]$, the general typing rules are: + $[c_1:C_1;\ldots;c_n:C_n]$, the general typing rules are, + for $1\leq j\leq k$ and $1\leq i\leq n$: \bigskip -\inference{\frac{\NInd{\Gamma}{\Gamma_I}{\Gamma_C} \in E - ~~j=1\ldots k}{(I_j:A_j) \in E}} +\inference{\frac{\NInd{\Gamma}{\Gamma_I}{\Gamma_C} \in E}{(I_j:A_j) \in E}} -\inference{\frac{\NInd{\Gamma}{\Gamma_I}{\Gamma_C} \in E - ~~~~i=1.. n} - {(c_i:C_i)\in E}} +\inference{\frac{\NInd{\Gamma}{\Gamma_I}{\Gamma_C} \in E}{(c_i:C_i) \in E}} \subsubsection{Inductive definitions with parameters} @@ -593,11 +593,11 @@ p_1:P_1,\ldots,\forall p_r:P_r,\forall a_1:A_1, \ldots \forall a_n:A_n, with $I$ one of the inductive definitions in $\Gamma_I$. We say that $n$ is the number of real arguments of the constructor $c$. -\paragraph{Context of parameters} +\paragraph{Context of parameters.} If an inductive definition $\NInd{\Gamma}{\Gamma_I}{\Gamma_C}$ admits $r$ inductive parameters, then there exists a context $\Gamma_P$ of -size $r$, such that $\Gamma_P=p_1:P_1;\ldots;\forall p_r:P_r$ and -if $(t:A)\in\Gamma_I,\Gamma_C$ then $A$ can be written as +size $r$, such that $\Gamma_P=p_1:P_1;\ldots;p_r:P_r$ and +if $(t:A) \in \Gamma_I,\Gamma_C$ then $A$ can be written as $\forall p_1:P_1,\ldots \forall p_r:P_r,A'$. We call $\Gamma_P$ the context of parameters of the inductive definition and use the notation $\forall \Gamma_P,A'$ for the term $A$. @@ -741,7 +741,7 @@ contains an inductive declaration. \inference{\frac{\Ind{\Gamma}{p}{\Gamma_I}{\Gamma_C} \in E ~~~~i=1.. n} - {(c_i:C_i)\in E}} + {(c_i:C_i) \in E}} \end{description} \paragraph{Example.} @@ -848,16 +848,16 @@ inductive definition. \begin{description} \item[W-Ind] Let $E$ be an environment and $\Gamma,\Gamma_P,\Gamma_I,\Gamma_C$ are contexts such that - $\Gamma_I$ is $[I_1:\forall \Gamma_p,A_1;\ldots;I_k:\forall + $\Gamma_I$ is $[I_1:\forall \Gamma_P,A_1;\ldots;I_k:\forall \Gamma_P,A_k]$ and $\Gamma_C$ is - $[c_1:\forall \Gamma_p,C_1;\ldots;c_n:\forall \Gamma_p,C_n]$. + $[c_1:\forall \Gamma_P,C_1;\ldots;c_n:\forall \Gamma_P,C_n]$. \inference{ \frac{ (\WTE{\Gamma;\Gamma_P}{A_j}{s'_j})_{j=1\ldots k} ~~ (\WTE{\Gamma;\Gamma_I;\Gamma_P}{C_i}{s_{p_i}})_{i=1\ldots n} } {\WF{E;\Ind{\Gamma}{p}{\Gamma_I}{\Gamma_C}}{\Gamma}}} -providing the following side conditions hold: +provided that the following side conditions hold: \begin{itemize} \item $k>0$, $I_j$, $c_i$ are different names for $j=1\ldots k$ and $i=1\ldots n$, \item $p$ is the number of parameters of \NInd{\Gamma}{\Gamma_I}{\Gamma_C} @@ -874,7 +874,7 @@ arity of the inductive type and the sort of the type of its constructors which will always be satisfied for the impredicative sort (\Prop) but may fail to define inductive definition on sort \Set{} and generate constraints between universes for -inductive definitions in types. +inductive definitions in the {\Type} hierarchy. \paragraph{Examples.} It is well known that existential quantifier can be encoded as an @@ -907,6 +907,135 @@ Inductive exType (P:Type->Prop) : Type %is recursive or not. We shall write the type $(x:_R T)C$ if it is %a recursive argument and $(x:_P T)C$ if the argument is not recursive. +\paragraph{Sort-polymorphism of inductive families.} +\index{Sort-polymorphism of inductive families} + +From {\Coq} version 8.1, inductive families declared in {\Type} are +polymorphic over their arguments in {\Type}. + +If $A$ is an arity and $s$ a sort, we write $A_{/s}$ for the arity +obtained from $A$ by replacing its sort with $s$. Especially, if $A$ +is well-typed in some environment and context, then $A_{/s}$ is typable +by typability of all products in the Calculus of Inductive Constructions. +The following typing rule is added to the theory. + +\begin{description} +\item[Ind-Family] Let $\Gamma_P$ be a context of parameters +$[p_1:P_1;\ldots;p_{m'}:P_{m'}]$ and $m\leq m'$ be the length of the +initial prefix of parameters that occur unchanged in the recursive +occurrences of the constructor types. Assume that $\Gamma_I$ is +$[I_1:\forall \Gamma_P,A_1;\ldots;I_k:\forall \Gamma_P,A_k]$ and +$\Gamma_C$ is $[c_1:\forall \Gamma_P,C_1;\ldots;c_n:\forall +\Gamma_P,C_n]$. + +Let $q_1$, \ldots, $q_r$, with $0\leq r\leq m$, be a possibly partial +instantiation of the parameters in $\Gamma_P$. We have: + +\inference{\frac +{\left\{\begin{array}{l} +\Ind{\Gamma}{p}{\Gamma_I}{\Gamma_C} \in E\\ +(E[\Gamma] \vdash q_s : P'_s)_{s=1\ldots r}\\ +(E[\Gamma] \vdash \WTEGLECONV{P'_s}{\subst{P_s}{x_u}{q_u}_{u=1\ldots s-1}})_{s=1\ldots r}\\ +1 \leq j \leq k +\end{array} +\right.} +{(I_j\,q_1\,\ldots\,q_r:\forall \Gamma^{r+1}_p, (A_j)_{/s})} +} + +provided that the following side conditions hold: + +\begin{itemize} +\item $\Gamma_{P'}$ is the context obtained from $\Gamma_P$ by +replacing, each $P_s$ that is an arity with the +sort of $P'_s$, as soon as $1\leq s \leq r$ (notice that +$P_s$ arity implies $P'_s$ arity since $E[\Gamma] +\vdash \WTEGLECONV{P'_s}{ \subst{P_s}{x_u}{q_u}_{u=1\ldots s-1}}$); +\item there are sorts $s_i$, for $1 \leq i \leq k$ such that, for + $\Gamma_{I'}$ obtained from $\Gamma_I$ by changing each $A_i$ by $(A_i)_{/s_i}$, +we have $(\WTE{\Gamma;\Gamma_{I'};\Gamma_{P'}}{C_i}{s_{p_i}})_{i=1\ldots n}$; +\item the sorts are such that all elimination are allowed (see +section~\ref{elimdep}). +\end{itemize} +\end{description} + +Notice that if $I_j\,q_1\,\ldots\,q_r$ is typable using the rules {\bf +Ind-Const} and {\bf App}, then it is typable using the rule {\bf +Ind-Family}. Conversely, the extended theory is not stronger than the +theory without {\bf Ind-Family}. We get an equiconsistency result by +mapping each $\Ind{\Gamma}{p}{\Gamma_I}{\Gamma_C}$ occurring into a +given derivation into as many fresh inductive types and constructors +as the number of different (partial) replacements of sorts, needed for +this derivation, in the parameters that are arities. That is, the +changes in the types of each partial instance $q_1\,\ldots\,q_r$ can +be characterized by the ordered sets of arity sorts among the types of +parameters, and to each signature is associated a new inductive +definition with fresh names. Conversion is preserved as any (partial) +instance $I_j\,q_1\,\ldots\,q_r$ or $C_i\,q_1\,\ldots\,q_r$ is mapped +to the names chosen in the specific instance of +$\Ind{\Gamma}{p}{\Gamma_I}{\Gamma_C}$. + +\newcommand{\Single}{\mbox{\textsf{Set}}} + +In practice, the rule is used by {\Coq} only with in case the +inductive type is declared with an arity of a sort in the $\Type$ +hierarchy, and, then, the polymorphism is over the parameters whose +type is an arity in the {\Type} hierarchy. The sort $s_j$ are then +chosen canonically so that each $s_j$ is minimal with respect to the +hierarchy ${\Prop_u}\subset{\Set_p}\subset\Type$ where $\Set_p$ is +predicative {\Set}, and ${\Prop_u}$ is the sort of small singleton +inductive types (i.e. of inductive types with one single constructor +and that contains either proofs or inhabitants of singleton types +only). More precisely, a small singleton inductive family is set in +{\Prop}, a small non singleton inductive family is set in {\Set} (even +in case {\Set} is impredicative -- see section~\ref{impredicativity}), +and otherwise in the {\Type} hierarchy. +% TODO: clarify the case of a partial application ?? + +Note that the side-condition about allowed elimination sorts in the +rule~{\bf Ind-Family} is just to avoid to recompute the allowed +elimination sorts at each instance of a pattern-matching (see +section~\ref{elimdep}). + +As an example, let us consider the following definition: +\begin{coq_example*} +Inductive option (A:Type) : Type := +| None : option A +| Some : A -> option A. +\end{coq_example*} + +As the definition is set in the {\Type} hierarchy, it is used +polymorphically over its parameters whose types are arities of a sort +in the {\Type} hierarchy. Here, the parameter $A$ has this property, +hence, if \texttt{option} is applied to a type in {\Set}, the result is +in {\Set}. Note that if \texttt{option} is applied to a type in {\Prop}, +then, the result is not set in \texttt{Prop} but in \texttt{Set} +still. This is because \texttt{option} is not a singleton type (see +section~\ref{singleton}) and it would loose the elimination to {\Set} and +{\Type} if set in {\Prop}. + +\begin{coq_example} +Check (fun A:Set => option A). +Check (fun A:Prop => option A). +\end{coq_example} + +Here is another example. + +\begin{coq_example*} +Inductive prod (A B:Type) : Type := pair : A -> B -> prod A B. +\end{coq_example*} + +As \texttt{prod} is a singleton type, it will be in {\Prop} if applied +twice to propositions, in {\Set} if applied twice to at least one type +in {\Set} and none in {\Type}, and in {\Type} otherwise. In all cases, +the three kind of eliminations schemes are allowed. + +\begin{coq_example} +Check (fun A:Set => prod A). +Check (fun A:Prop => prod A A). +Check (fun (A:Prop) (B:Set) => prod A B). +Check (fun (A:Type) (B:Prop) => prod A B). +\end{coq_example} + \subsection{Destructors} The specification of inductive definitions with arities and constructors is quite natural. But we still have to say how to use an @@ -1049,6 +1178,7 @@ compact notation~: % \mbox{\tt =>}~ \false} \paragraph{Allowed elimination sorts.} + \index{Elimination sorts} An important question for building the typing rule for \kw{match} is @@ -1158,6 +1288,7 @@ the two projections on this type. %{\tt Program} tactic or when extracting ML programs. \paragraph{Empty and singleton elimination} +\label{singleton} \index{Elimination!Singleton elimination} \index{Elimination!Empty elimination} @@ -1167,7 +1298,7 @@ eliminations are allowed. \item[\Prop-extended] \inference{ \frac{I \mbox{~is an empty or singleton - definition}~~~s\in\Sort}{\compat{I:\Prop}{I\ra s}} + definition}~~~s \in \Sort}{\compat{I:\Prop}{I\ra s}} } \end{description} @@ -1530,7 +1661,7 @@ The major change in the theory concerns the rule for product formation in the sort \Set, which is extended to a domain in any sort~: \begin{description} \item [Prod] \index{Typing rules!Prod (impredicative Set)} -\inference{\frac{\WTEG{T}{s}~~~~s\in\Sort~~~~~~ +\inference{\frac{\WTEG{T}{s}~~~~s \in \Sort~~~~~~ \WTE{\Gamma::(x:T)}{U}{\Set}} { \WTEG{\forall~x:T,U}{\Set}}} \end{description} @@ -1553,7 +1684,7 @@ impredicative system for sort \Set{} become~: -% $Id: RefMan-cic.tex 8914 2006-06-07 14:57:22Z cpaulin $ +% $Id: RefMan-cic.tex 9001 2006-07-04 13:50:15Z herbelin $ %%% Local Variables: %%% mode: latex diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex index f8a7546f..8c54e0ed 100644 --- a/doc/refman/RefMan-com.tex +++ b/doc/refman/RefMan-com.tex @@ -86,6 +86,7 @@ you move the \Coq\ binaries and library after installation. \section{Options} \index{Options of the command line} +\label{vmoption} The following command-line options are recognized by the commands {\tt coqc} and {\tt coqtop}, unless stated otherwise: @@ -239,6 +240,11 @@ The following command-line options are recognized by the commands {\tt resulting in a smaller memory requirement and faster compilation; warning: this invalidates some features such as the extraction tool. +\item[{\tt -vm}]\ + + This activates the use of the bytecode-based conversion algorithm + for the current session (see section~\ref{SetVirtualMachine}). + \item[{\tt -image} {\em file}]\ This option sets the binary image to be used to be {\em file} @@ -272,7 +278,7 @@ The following command-line options are recognized by the commands {\tt % (see section~\ref{coqsearchisos}, page~\pageref{coqsearchisos}). % \end{description} -% $Id: RefMan-com.tex 8609 2006-02-24 13:32:57Z notin,no-port-forwarding,no-agent-forwarding,no-X11-forwarding,no-pty $ +% $Id: RefMan-com.tex 9044 2006-07-12 13:22:17Z herbelin $ %%% Local Variables: %%% mode: latex diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex index 503d7571..37660aa3 100644 --- a/doc/refman/RefMan-ext.tex +++ b/doc/refman/RefMan-ext.tex @@ -223,13 +223,14 @@ To deactivate the printing of projections, use \label{Mult-match}} The basic version of \verb+match+ allows pattern-matching on simple -patterns. As an extension, multiple and nested patterns are -allowed, as in ML-like languages. +patterns. As an extension, multiple nested patterns or disjunction of +patterns are allowed, as in ML-like languages. The extension just acts as a macro that is expanded during parsing into a sequence of {\tt match} on simple patterns. Especially, a -construction defined using the extended {\tt match} is printed under -its expanded form. +construction defined using the extended {\tt match} is generally +printed under its expanded form (see~\texttt{Set Printing Matching} in +section~\ref{SetPrintingMatching}). \SeeAlso chapter \ref{Mult-match-full}. @@ -330,11 +331,40 @@ The general equivalence for an inductive type with one constructors {\tt C} is $\equiv$~ {\tt match {\term} \zeroone{\ifitem} with C {\ident}$_1$ {\ldots} {\ident}$_n$ \verb!=>! {\term}' end} -\subsection{Options for pretty-printing of {\tt match} +\subsection{Controlling pretty-printing of {\tt match} expressions \label{printing-options}} -There are three options controlling the pretty-printing of {\tt match} -expressions. +The following commands give some control over the pretty-printing of +{\tt match} expressions. + +\subsubsection{Printing nested patterns +\label{SetPrintingMatching} +\comindex{Set Printing Matching} +\comindex{Unset Printing Matching} +\comindex{Test Printing Matching}} + +The Calculus of Inductive Constructions knows pattern-matching only +over simple patterns. It is however convenient to re-factorize nested +pattern-matching into a single pattern-matching over a nested pattern. +{\Coq}'s printer try to do such limited re-factorization. + +\begin{quote} +{\tt Set Printing Matching.} +\end{quote} +This tells {\Coq} to try to use nested patterns. This is the default +behavior. + +\begin{quote} +{\tt Unset Printing Matching.} +\end{quote} +This tells {\Coq} to print only simple pattern-matching problems in +the same way as the {\Coq} kernel handles them. + +\begin{quote} +{\tt Test Printing Matching.} +\end{quote} +This tells if the printing matching mode is on or off. The default is +on. \subsubsection{Printing of wildcard pattern \comindex{Set Printing Wildcard} @@ -1088,6 +1118,18 @@ the declaration \SeeAlso more examples in user contribution \texttt{category} (\texttt{Rocq/ALGEBRA}). +\subsubsection{Print Canonical Projections. +\comindex{Print Canonical Projections}} + +This displays the list of global names that are components of some +canonical structure. For each of them, the canonical structure of +which it is a projection is indicated. For instance, the above example +gives the following output: + +\begin{coq_example} +Print Canonical Projections. +\end{coq_example} + \subsection{Implicit types of variables} It is possible to bind variable names to a given type (e.g. in a diff --git a/doc/refman/RefMan-gal.tex b/doc/refman/RefMan-gal.tex index 2214864a..e7b825d7 100644 --- a/doc/refman/RefMan-gal.tex +++ b/doc/refman/RefMan-gal.tex @@ -64,15 +64,24 @@ That is, they are recognized by the following lexical class: \begin{center} \begin{tabular}{rcl} {\firstletter} & ::= & {\tt a..z} $\mid$ {\tt A..Z} $\mid$ {\tt \_} -% $\mid$ {\tt unicode-letter} +$\mid$ {\tt unicode-letter} \\ {\subsequentletter} & ::= & {\tt a..z} $\mid$ {\tt A..Z} $\mid$ {\tt 0..9} $\mid$ {\tt \_} % $\mid$ {\tt \$} -$\mid$ {\tt '} \\ +$\mid$ {\tt '} +$\mid$ {\tt unicode-letter} +$\mid$ {\tt unicode-id-part} \\ {\ident} & ::= & {\firstletter} \sequencewithoutblank{\subsequentletter}{} \end{tabular} \end{center} -All characters are meaningful. In particular, identifiers are case-sensitive. +All characters are meaningful. In particular, identifiers are +case-sensitive. The entry {\tt unicode-letter} non-exhaustively +includes Latin, Greek, Gothic, Cyrillic, Arabic, Hebrew, Georgian, +Hangul, Hiragana and Katakana characters, CJK ideographs, mathematical +letter-like symbols, hyphens, non-breaking space, {\ldots} The entry +{\tt unicode-id-part} non-exhaustively includes symbols for prime +letters and subscripts. + Access identifiers, written {\accessident}, are identifiers prefixed by \verb!.! (dot) without blank. They are used in the syntax of qualified identifiers. @@ -308,7 +317,9 @@ chapter \ref{Addoc-syntax}. &&\\ {\returntype} & ::= & {\tt return} {\term} \\ &&\\ -{\eqn} & ::= & \nelist{\pattern}{\tt ,} {\tt =>} {\term}\\ +{\eqn} & ::= & \nelist{\multpattern}{\tt |} {\tt =>} {\term}\\ +&&\\ +{\multpattern} & ::= & \nelist{\pattern}{\tt ,}\\ &&\\ {\pattern} & ::= & {\qualid} \nelist{\pattern}{} \\ & $|$ & {\pattern} {\tt as} {\ident} \\ @@ -316,7 +327,9 @@ chapter \ref{Addoc-syntax}. & $|$ & {\qualid} \\ & $|$ & {\tt \_} \\ & $|$ & {\num} \\ - & $|$ & {\tt (} \nelist{\pattern}{,} {\tt )} + & $|$ & {\tt (} \nelist{\orpattern}{,} {\tt )} \\ +\\ +{\orpattern} & ::= & \nelist{\pattern}{\tt |}\\ \end{tabular} \end{centerframe} \caption{Syntax of terms (continued)} @@ -515,10 +528,11 @@ The expression {\tt match} {\term$_0$} {\returntype} {\tt with} {\pattern$_1$} {\tt =>} {\term$_1$} {\tt $|$} {\ldots} {\tt $|$} {\pattern$_n$} {\tt =>} {\term$_n$} {\tt end}, denotes a {\em pattern-matching} over the term {\term$_0$} (expected to be of an -inductive type $I$). {\term$_1$}\ldots{\term$_n$} are called branches. In +inductive type $I$). +The terms {\term$_1$}\ldots{\term$_n$} are called branches. In a simple pattern \qualid~\nelist{\ident}{}, the qualified identifier {\qualid} is intended to -be a constructor. There should be a branch for every constructor of +be a constructor. There should be one branch for every constructor of $I$. The {\returntype} is used to compute the resulting type of the whole @@ -530,9 +544,8 @@ annotation has to be given when the resulting type of the whole {\tt match} depends on the actual {\term$_0$} matched. There are specific notations for case analysis on types with one or -two constructors: {\tt if / then / else} and -{\tt let (}\ldots{\tt ) :=} \ldots {\tt in}\ldots. \SeeAlso -section~\ref{Mult-match} for details and examples. +two constructors: {\tt if {\ldots} then {\ldots} else {\ldots}} and +{\tt let (}\nelist{\ldots}{,}{\tt ) :=} {\ldots} {\tt in} {\ldots}. \SeeAlso Section~\ref{Mult-match} for details and examples. @@ -761,12 +774,17 @@ environment, provided that {\term} is well-typed. {\binder$_1$}\ldots{\binder$_n$}{\tt ,}\,\term$_1$\,{\tt :=}}\,% {\tt fun}\,{\binder$_1$}\ldots{\binder$_n$}\,{\tt =>}\,{\term$_2$}\,% {\tt .} + +\item {\tt Example {\ident} := {\term}.}\\ +{\tt Example {\ident} {\tt :}{\term$_1$} := {\term$_2$}.}\\ +{\tt Example {\ident} {\binder$_1$}\ldots{\binder$_n$} + {\tt :}\term$_1$ {\tt :=} {\term$_2$}.}\\ +\comindex{Example} +These are synonyms of the {\tt Definition} forms. \end{Variants} \begin{ErrMsgs} -\item \errindex{In environment {\dots} the term: {\term$_2$} does not have type - {\term$_1$}}.\\ - \texttt{Actually, it has type {\term$_3$}}. +\item \errindex{Error: The term ``{\term}'' has type "{\type}" while it is expected to have type ``{\type}''} \end{ErrMsgs} \SeeAlso Sections \ref{Opaque}, \ref{Transparent}, \ref{unfold} @@ -1062,17 +1080,23 @@ inductive types The extended syntax is: \medskip {\tt -Inductive {{\ident$_1$} {\params} : {\type$_1$} := \\ -\mbox{}\hspace{0.4cm} {\ident$_1^1$} : {\type$_1^1$} \\ -\mbox{}\hspace{0.1cm}| .. \\ -\mbox{}\hspace{0.1cm}| {\ident$_{n_1}^1$} : {\type$_{n_1}^1$} \\ +\begin{tabular}{l} +Inductive {\ident$_1$} {\params} : {\type$_1$} := \\ +\begin{tabular}{clcl} + & {\ident$_1^1$} &:& {\type$_1^1$} \\ + | & {\ldots} && \\ + | & {\ident$_{n_1}^1$} &:& {\type$_{n_1}^1$} +\end{tabular} \\ with\\ -\mbox{}\hspace{0.1cm} .. \\ +~{\ldots} \\ with {\ident$_m$} {\params} : {\type$_m$} := \\ -\mbox{}\hspace{0.4cm}{\ident$_1^m$} : {\type$_1^m$} \\ -\mbox{}\hspace{0.1cm}| .. \\ -\mbox{}\hspace{0.1cm}| {\ident$_{n_m}^m$} : {\type$_{n_m}^m$}. -}} +\begin{tabular}{clcl} + & {\ident$_1^m$} &:& {\type$_1^m$} \\ + | & {\ldots} \\ + | & {\ident$_{n_m}^m$} &:& {\type$_{n_m}^m$}. +\end{tabular} +\end{tabular} +} \medskip \Example @@ -1184,20 +1208,22 @@ how to introduce infinite objects in Section~\ref{CoFixpoint}. %% \subsection{Definition of recursive functions} -\subsubsection{\tt Fixpoint {\ident} {\params} {\tt \{struct} +\subsubsection{Recursive functions over a inductive type} + +The command: +\begin{center} + \texttt{Fixpoint {\ident} {\params} {\tt \{struct} \ident$_0$ {\tt \}} : type$_0$ := \term$_0$ -\comindex{Fixpoint} -\label{Fixpoint}} - -This command allows to define inductive objects using a fixed point -construction. The meaning of this declaration is to define {\it ident} -a recursive function with arguments specified by the binders in -\params{} % {\binder$_1$}\ldots{\binder$_n$} -such that {\it ident} applied to -arguments corresponding to these binders has type \type$_0$, and is -equivalent to the expression \term$_0$. The type of the {\ident} is -consequently {\tt forall {\params} {\tt,} \type$_0$} -and the value is equivalent to {\tt fun {\params} {\tt =>} \term$_0$}. + \comindex{Fixpoint}\label{Fixpoint}} +\end{center} +allows to define inductive objects using a fixed point construction. +The meaning of this declaration is to define {\it ident} a recursive +function with arguments specified by the binders in {\params} such +that {\it ident} applied to arguments corresponding to these binders +has type \type$_0$, and is equivalent to the expression \term$_0$. The +type of the {\ident} is consequently {\tt forall {\params} {\tt,} + \type$_0$} and the value is equivalent to {\tt fun {\params} {\tt + =>} \term$_0$}. To be accepted, a {\tt Fixpoint} definition has to satisfy some syntactical constraints on a special argument called the decreasing @@ -1205,8 +1231,8 @@ argument. They are needed to ensure that the {\tt Fixpoint} definition always terminates. The point of the {\tt \{struct \ident {\tt \}}} annotation is to let the user tell the system which argument decreases along the recursive calls. This annotation may be left implicit for -fixpoints with one argument. For instance, one can define the addition -function as : +fixpoints where only one argument has an inductive type. For instance, +one can define the addition function as : \begin{coq_example} Fixpoint add (n m:nat) {struct n} : nat := @@ -1323,23 +1349,25 @@ Fixpoint tree_size (t:tree) : nat := A generic command {\tt Scheme} is useful to build automatically various mutual induction principles. It is described in Section~\ref{Scheme}. -\subsubsection{\tt Function {\ident} {\binder$_1$}\ldots{\binder$_n$} - {\tt \{}decrease\_annot{\tt\}} : type$_0$ := \term$_0$. -} -\comindex{Function} -\label{Function} - -This \emph{experimental} command can be seen as a generalization of -{\tt Fixpoint}. It is actually a wrapper for several ways of defining -a function \emph{and other useful related objects}, namely: an -induction principle that reflects the recursive structure of the -function (see \ref{FunInduction}), and its fixpoint equality (not -always, see below). The meaning of this declaration is to define a -function {\it ident}, similarly to {\tt Fixpoint}. Like in {\tt -Fixpoint}, the decreasing argument must be given (unless the function -is not recursive), but it must not necessary be \emph{structurally} -decreasing. The point of the {\tt -\{\}} annotation is to name the decreasing argument \emph{and} to +\subsubsection{A more complex definition of recursive functions} + +The \emph{experimental} command +\begin{center} + \texttt{Function {\ident} {\binder$_1$}\ldots{\binder$_n$} + \{decrease\_annot\} : type$_0$ := \term$_0$} + \comindex{Function} + \label{Function} +\end{center} +can be seen as a generalization of {\tt Fixpoint}. It is actually a +wrapper for several ways of defining a function \emph{and other useful + related objects}, namely: an induction principle that reflects the +recursive structure of the function (see \ref{FunInduction}), and its +fixpoint equality (not always, see below). The meaning of this +declaration is to define a function {\it ident}, similarly to {\tt + Fixpoint}. Like in {\tt Fixpoint}, the decreasing argument must be +given (unless the function is not recursive), but it must not +necessary be \emph{structurally} decreasing. The point of the {\tt + \{\}} annotation is to name the decreasing argument \emph{and} to describe which kind of decreasing criteria must be used to ensure termination of recursive calls. @@ -1416,43 +1444,35 @@ This error happens generally when: \SeeAlso{\ref{FunScheme},\ref{FunScheme-examples},\ref{FunInduction}} -Depending on the {\tt \{\}} annotation, different definition +Depending on the {\tt \{$\ldots$\}} annotation, different definition mechanisms are used by {\tt Function}. More precise description given below. - - -\subsubsection{\tt Function {\ident} {\binder$_1$}\ldots{\binder$_n$} - : type$_0$ := \term$_0$. -\comindex{Function} -} - -Defines the not recursive function \ident\ as if declared with -\texttt{Definition}. Three elimination schemes {\tt\ident\_rect}, -{\tt\ident\_rec} and {\tt\ident\_ind} are generated (see the -documentation of {\tt Inductive} \ref{Inductive}), which reflect the -pattern matching structure of \term$_0$. - - -\subsubsection{\tt Function {\ident} {\binder$_1$}\ldots{\binder$_n$} - {\tt \{}{\tt struct} \ident$_0${\tt\}} : type$_0$ := \term$_0$. -\comindex{Function} -} - -Defines the structural recursive function \ident\ as if declared with -\texttt{Fixpoint} . Three induction schemes {\tt\ident\_rect}, -{\tt\ident\_rec} and {\tt\ident\_ind} are generated (see the -documentation of {\tt Inductive} \ref{Inductive}), which reflect the -recursive structure of \term$_0$. When there is only one parameter, -{\tt \{struct} \ident$_0${\tt\}} can be omitted. - -\subsubsection{\tt Function {\ident} {\binder$_1$}\ldots{\binder$_n$} - {\tt \{}{\tt measure \term$_1$} \ident$_0${\tt\}} : type$_0$ := \term$_0$. -\comindex{Function}} - -\subsubsection{\tt Function {\ident} {\binder$_1$}\ldots{\binder$_n$} - {\tt \{}{\tt wf \term$_1$} \ident$_0${\tt\}} : type$_0$ := \term$_0$. -\comindex{Function}} +\begin{Variants} +\item \texttt{ Function {\ident} {\binder$_1$}\ldots{\binder$_n$} + : type$_0$ := \term$_0$} + + Defines the not recursive function \ident\ as if declared with + \texttt{Definition}. Three elimination schemes {\tt\ident\_rect}, + {\tt\ident\_rec} and {\tt\ident\_ind} are generated (see the + documentation of {\tt Inductive} \ref{Inductive}), which reflect the + pattern matching structure of \term$_0$. + +\item \texttt{Function {\ident} {\binder$_1$}\ldots{\binder$_n$} + {\tt \{}{\tt struct} \ident$_0${\tt\}} : type$_0$ := \term$_0$} + + Defines the structural recursive function \ident\ as if declared + with \texttt{Fixpoint}. Three induction schemes {\tt\ident\_rect}, + {\tt\ident\_rec} and {\tt\ident\_ind} are generated (see the + documentation of {\tt Inductive} \ref{Inductive}), which reflect the + recursive structure of \term$_0$. When there is only one parameter, + {\tt \{struct} \ident$_0${\tt\}} can be omitted. + +\item \texttt{Function {\ident} {\binder$_1$}\ldots{\binder$_n$} {\tt + \{}{\tt measure \term$_1$} \ident$_0${\tt\}} : type$_0$ := + \term$_0$} +\item \texttt{Function {\ident} {\binder$_1$}\ldots{\binder$_n$} + {\tt \{}{\tt wf \term$_1$} \ident$_0${\tt\}} : type$_0$ := \term$_0$} Defines a recursive function by well founded recursion. \textbf{The module \texttt{Recdef} of the standard library must be loaded for this @@ -1508,21 +1528,21 @@ subgoals belonging to a Lemma {\ident}{\tt\_tcc}. % These subgoals are independe %The decreasing argument cannot be dependent of another?? %Exemples faux ici +\end{Variants} +\subsubsection{Recursive functions over co-indcutive types} - - -\subsubsection{\tt CoFixpoint {\ident} : \type$_0$ := \term$_0$. -\comindex{CoFixpoint} -\label{CoFixpoint}} - -The {\tt CoFixpoint} command introduces a method for constructing an -infinite object of a coinduc\-tive type. For example, the stream -containing all natural numbers can be introduced applying the -following method to the number \texttt{O} (see -Section~\ref{CoInductiveTypes} for the definition of {\tt Stream}, -{\tt hd} and {\tt tl}): +The command: +\begin{center} + \texttt{CoFixpoint {\ident} : \type$_0$ := \term$_0$} + \comindex{CoFixpoint}\label{CoFixpoint} +\end{center} +introduces a method for constructing an infinite object of a +coinduc\-tive type. For example, the stream containing all natural +numbers can be introduced applying the following method to the number +\texttt{O} (see Section~\ref{CoInductiveTypes} for the definition of +{\tt Stream}, {\tt hd} and {\tt tl}): \begin{coq_eval} Reset Initial. CoInductive Stream : Set := @@ -1606,9 +1626,13 @@ After a statement, {\Coq} needs a proof. \begin{Variants} \item {\tt Lemma {\ident} : {\type}.}\\ -It is a synonymous of \texttt{Theorem} -\item {\tt Remark {\ident} : {\type}.}\\ -It is a synonymous of \texttt{Theorem} + {\tt Remark {\ident} : {\type}.}\\ + {\tt Fact {\ident} : {\type}.}\\ + {\tt Corollary {\ident} : {\type}.}\\ + {\tt Proposition {\ident} : {\type}.}\\ +\comindex{Proposition} +\comindex{Corollary} +All these commands are synonymous of \texttt{Theorem} % Same as {\tt Theorem} except % that if this statement is in one or more levels of sections then the % name {\ident} will be accessible only prefixed by the sections names @@ -1616,8 +1640,6 @@ It is a synonymous of \texttt{Theorem} % closed. % %All proofs of persistent objects (such as theorems) referring to {\ident} % %within the section will be replaced by the proof of {\ident}. - \item {\tt Fact {\ident} : {\type}.}\\ -It is a synonymous of \texttt{Theorem} % Same as {\tt Remark} except % that the innermost section name is dropped from the full name. \item {\tt Definition {\ident} : {\type}.} \\ @@ -1684,4 +1706,4 @@ To be able to unfold a proof, you should end the proof by {\tt Defined} % TeX-master: "Reference-Manual" % End: -% $Id: RefMan-gal.tex 8915 2006-06-07 15:17:13Z courtieu $ +% $Id: RefMan-gal.tex 9040 2006-07-11 18:06:49Z notin $ diff --git a/doc/refman/RefMan-ide.tex b/doc/refman/RefMan-ide.tex index 3c73c141..104338ea 100644 --- a/doc/refman/RefMan-ide.tex +++ b/doc/refman/RefMan-ide.tex @@ -11,9 +11,10 @@ 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 buffer'', and with a file name as argument, another buffer displaying -the contents of that file. Additionally, coqide accepts the same -options as coqtop, given in Chapter~\ref{Addoc-coqc}, the ones having -obviously no meaning for \CoqIDE{} being ignored. +the contents of that file. Additionally, \verb|coqide| accepts the same +options as \verb|coqtop|, given in Chapter~\ref{Addoc-coqc}, the ones having +obviously no meaning for \CoqIDE{} being ignored. Additionally, \verb|coqide| accepts the option \verb|-enable-geoproof| to enable the support for \emph{GeoProof} \footnote{\emph{GeoProof} is dynamic geometry software which can be used in conjunction with \CoqIDE{} to interactively build a Coq statement corresponding to a geometric figure. More information about \emph{GeoProof} can be found here: \url{http://home.gna.org/geoproof/} }. + \begin{figure}[t] \begin{center} @@ -319,7 +320,7 @@ or -% $Id: RefMan-ide.tex 8626 2006-03-14 15:01:00Z notin $ +% $Id: RefMan-ide.tex 8945 2006-06-10 12:04:14Z jnarboux $ %%% Local Variables: %%% mode: latex diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex index de9897c4..e7400232 100644 --- a/doc/refman/RefMan-ltac.tex +++ b/doc/refman/RefMan-ltac.tex @@ -103,16 +103,23 @@ is understood as {\tt match reverse goal with} \nelist{\contextrule}{\tt |} {\tt end}\\ & | & {\tt match} {\tacexpr} {\tt with} \nelist{\matchrule}{\tt |} {\tt end}\\ +& | & +{\tt lazymatch goal with} \nelist{\contextrule}{\tt |} {\tt end}\\ +& | & +{\tt lazymatch reverse goal with} \nelist{\contextrule}{\tt |} {\tt end}\\ +& | & +{\tt lazymatch} {\tacexpr} {\tt with} \nelist{\matchrule}{\tt |} {\tt end}\\ & | & {\tt abstract} {\atom}\\ & | & {\tt abstract} {\atom} {\tt using} {\ident} \\ & | & {\tt first [} \nelist{\tacexpr}{\tt |} {\tt ]}\\ & | & {\tt solve [} \nelist{\tacexpr}{\tt |} {\tt ]}\\ -& | & {\tt idtac} ~|~ {\tt idtac} {\qstring}\\ -& | & {\tt fail} ~|~ {\tt fail} {\naturalnumber} {\qstring}\\ +& | & {\tt idtac} \sequence{\messagetoken}{}\\ +& | & {\tt fail} \zeroone{\naturalnumber} \sequence{\messagetoken}{}\\ & | & {\tt fresh} ~|~ {\tt fresh} {\qstring}\\ & | & {\tt context} {\ident} {\tt [} {\term} {\tt ]}\\ & | & {\tt eval} {\nterm{redexpr}} {\tt in} {\term}\\ & | & {\tt type of} {\term}\\ +& | & {\tt external} {\qstring} {\qstring} \nelist{\tacarg}{}\\ & | & {\tt constr :} {\term}\\ & | & \atomictac\\ & | & {\qualid} \nelist{\tacarg}{}\\ @@ -122,6 +129,8 @@ is understood as {\qualid} \\ & | & ()\\ & | & {\tt (} {\tacexpr} {\tt )}\\ +\\ +{\messagetoken}\!\!\!\!\!\! & ::= & {\qstring} ~|~ {\term} ~|~ {\integer} \\ \end{tabular} \end{centerframe} \caption{Syntax of the tactic language} @@ -266,6 +275,12 @@ 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 $v_0$ does not generate exactly $n$ subgoals. +\variant If no tactic is given for the $i$-th generated subgoal, it +behaves as if the tactic {\tt idtac} were given. For instance, {\tt +split ; [ | auto ]} is a shortcut for +{\tt split ; [ idtac | auto ]}. + + \subsubsection{For loop} \tacindex{do} \index{Tacticals!do@{\tt do}} @@ -369,10 +384,13 @@ 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{quote} -{\tt idtac} and {\tt idtac "message"} -\end{quote} -The latter variant prints the string on the standard output. + +\variant {\tt idtac \nelist{\messagetoken}{}} + +This prints the given tokens. Strings and integers are printed +literally. If a term is given, it is printed, its variables being +interpreted in the current environment. In particular, if a variable +is given, its value is printed. \subsubsection{Failing} @@ -381,17 +399,24 @@ 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{quote} -{\tt fail $n$}, {\tt fail "message"} and {\tt fail $n$ "message"} -\end{quote} +catched by {\tt try} or {\tt match goal}. + +\begin{Variants} +\item {\tt fail $n$}\\ 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 (backtracking). If non zero, the current {\tt match goal} block or {\tt try} command is aborted and the level is decremented. -\ErrMsg \errindex{Tactic Failure "message" (level $n$)}. +\item {\tt fail \nelist{\messagetoken}{}}\\ +The given tokens are used for printing the failure message. + +\item {\tt fail $n$ \nelist{\messagetoken}{}}\\ +This is a combination of the previous variants. +\end{Variants} + +\ErrMsg \errindex{Tactic Failure {\it message} (level $n$)}. \subsubsection{Local definitions} \index{Ltac!let} @@ -464,10 +489,13 @@ The {\tacexpr} is evaluated and should yield a term which is matched pattern matching instantiations to the metavariables. If the matching with {\cpattern}$_1$ fails, {\cpattern}$_2$ is used and so on. The pattern {\_} matches any term and shunts all remaining patterns if -any. If {\tacexpr}$_1$ evaluates to a tactic, this tactic is not -immediately applied to the current goal (in contrast with {\tt match -goal}). If all clauses fail (in particular, there is no pattern {\_}) -then a no-matching error is raised. +any. If {\tacexpr}$_1$ evaluates to a tactic and the {\tt match} +expression is in position to be applied to a goal (e.g. it is not +bound to a variable by a {\tt let in}, then this tactic is applied. If +the tactic succeeds, the list of resulting subgoals is the result of +the {\tt match} expression. On the opposite, if it fails, the next +pattern is tried. If all clauses fail (in particular, there is no +pattern {\_}) then a no-matching error is raised. \begin{ErrMsgs} @@ -481,7 +509,8 @@ then a no-matching error is raised. \end{ErrMsgs} -\index{context!in pattern} +\begin{Variants} +\item \index{context!in pattern} There is a special form of patterns to match a subterm against the pattern: \begin{quote} @@ -493,11 +522,36 @@ is the initial term where the matched subterm is replaced by a hole. The definition of {\tt context} in expressions below will show how to use such term contexts. -This operator never makes backtracking. If there are several subterms -matching the pattern, only the first match is considered. Note that -the order of matching is left unspecified. -%% TODO: clarify this point! It *should* be specified +If the evaluation of the right-hand-side of a valid match fails, the +next matching subterm is tried. If no further subterm matches, the +next clause is tried. Matching subterms are considered top-bottom and +from left to right (with respect to the raw printing obtained by +setting option {\tt Printing All}, see section~\ref{SetPrintingAll}). + +\begin{coq_example} +Ltac f x := + match x with + context f [S ?X] => + idtac X; (* To display the evaluation order *) + assert (p := refl_equal 1 : X=1); (* To filter the case X=1 *) + let x:= context f[O] in assert (x=O) (* To observe the context *) + end. +Goal True. +f (3+4). +\end{coq_example} + +\item \index{lazymatch!in Ltac} +\index{Ltac!lazymatch} +Using {\tt lazymatch} instead of {\tt match} has an effect if the +right-hand-side of a clause returns a tactic. With {\tt match}, the +tactic is applied to the current goal (and the next clause is tried if +it fails). With {\tt lazymatch}, the tactic is directly returned as +the result of the whole {\tt lazymatch} block without being first +tried to be applied to the goal. Typically, if the {\tt lazymatch} +block is bound to some variable $x$ in a {\tt let in}, then tactic +expression gets bound to the variable $x$. +\end{Variants} \subsubsection{Pattern matching on goals} \index{Ltac!match goal} @@ -521,8 +575,6 @@ We can make pattern matching on goals using the following expression: \end{tabbing} \end{quote} -% TODO: specify order of hypothesis and explain reverse... - If each hypothesis pattern $hyp_{1,i}$, with $i=1,...,m_1$ is matched (non-linear first order unification) by an hypothesis of the goal and if {\cpattern}$_1$ is matched by the conclusion of the @@ -535,7 +587,9 @@ hypotheses is tried with the same proof context pattern. If there is no other combination of hypotheses then the second proof context pattern is tried and so on. If the next to last proof context pattern fails then {\tacexpr}$_{n+1}$ is evaluated to $v_{n+1}$ and $v_{n+1}$ -is applied. +is applied. Note also that matching against subterms (using the {\tt +context} {\ident} {\tt [} {\cpattern} {\tt ]}) is available and may +itself induce extra backtrackings. \ErrMsg \errindex{No matching clauses for match goal} @@ -552,6 +606,36 @@ pattern, the goal hypothesis are matched in order (fresher hypothesis first), but it possible to reverse this order (older first) with the {\tt match reverse goal with} variant. +\variant +\index{lazymatch goal!in Ltac} +\index{Ltac!lazymatch goal} +\index{lazymatch reverse goal!in Ltac} +\index{Ltac!lazymatch reverse goal} +Using {\tt lazymatch} instead of {\tt match} has an effect if the +right-hand-side of a clause returns a tactic. With {\tt match}, the +tactic is applied to the current goal (and the next clause is tried if +it fails). With {\tt lazymatch}, the tactic is directly returned as +the result of the whole {\tt lazymatch} block without being first +tried to be applied to the goal. Typically, if the {\tt lazymatch} +block is bound to some variable $x$ in a {\tt let in}, then tactic +expression gets bound to the variable $x$. + +\begin{coq_example} +Ltac test_lazy := + lazymatch goal with + | _ => idtac "here"; fail + | _ => idtac "wasn't lazy"; trivial + end. +Ltac test_eager := + match goal with + | _ => idtac "here"; fail + | _ => idtac "wasn't lazy"; trivial + end. +Goal True. +test_lazy || idtac "was lazy". +test_eager || idtac "was lazy". +\end{coq_example} + \subsubsection{Filling a term context} \index{context!in expression} @@ -585,13 +669,6 @@ 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} -\index{Ltac!type of} -\index{type of!in Ltac} - -This tactic computes the type of {\term}. - \subsubsection{Computing in a constr} \index{Ltac!eval} \index{eval!in Ltac} @@ -604,6 +681,16 @@ 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}. +\subsubsection{Type-checking a term} +%\tacindex{type of} +\index{Ltac!type of} +\index{type of!in Ltac} + +The following returns the type of {\term}: + +\begin{quote} +{\tt type of} {\term} +\end{quote} \subsubsection{Accessing tactic decomposition} \tacindex{info} @@ -635,10 +722,76 @@ without having to cut manually the proof in smaller lemmas. \ErrMsg \errindex{Proof is not complete} +\subsubsection{Calling an external tactic} +\index{Ltac!external} + +The tactic {\tt external} allows to run an executable outside the +{\Coq} executable. The communication is done via an XML encoding of +constructions. The syntax of the command is + +\begin{quote} +{\tt external} "\textsl{command}" "\textsl{request}" \nelist{\tacarg}{} +\end{quote} + +The string \textsl{command}, to be interpreted in the default +execution path of the operating system, is the name of the external +command. The string \textsl{request} is the name of a request to be +sent to the external command. Finally the list of tactic arguments +have to evaluate to terms. An XML tree of the following form is sent +to the standard input of the external command. +\medskip + +\begin{tabular}{l} +\texttt{<REQUEST req="}\textsl{request}\texttt{">}\\ +the XML tree of the first argument\\ +{\ldots}\\ +the XML tree of the last argument\\ +\texttt{</REQUEST>}\\ +\end{tabular} +\medskip + +Conversely, the external command must send on its standard output an +XML tree of the following forms: + +\medskip +\begin{tabular}{l} +\texttt{<TERM>}\\ +the XML tree of a term\\ +\texttt{</TERM>}\\ +\end{tabular} +\medskip + +\noindent or + +\medskip +\begin{tabular}{l} +\texttt{<CALL uri="}\textsl{ltac\_qualified\_ident}\texttt{">}\\ +the XML tree of a first argument\\ +{\ldots}\\ +the XML tree of a last argument\\ +\texttt{</CALL>}\\ +\end{tabular} + +\medskip +\noindent where \textsl{ltac\_qualified\_ident} is the name of a +defined {\ltac} function and each subsequent XML tree is recursively a +\texttt{CALL} or a \texttt{TERM} node. + +The Document Type Definition (DTD) for terms of the Calculus of +Inductive Constructions is the one developed as part of the MoWGLI +European project. It can be found in the file {\tt dev/doc/cic.dtd} of +the {\Coq} source archive. + +An example of parser for this DTD, written in the Objective Caml - +Camlp4 language, can be found in the file {\tt parsing/g\_xml.ml4} of +the {\Coq} source archive. + \section{Tactic toplevel definitions} \comindex{Ltac} -Basically, tactics toplevel definitions are made as follows: +\subsection{Defining {\ltac} functions} + +Basically, {\ltac} toplevel definitions are made as follows: %{\tt Tactic Definition} {\ident} {\tt :=} {\tacexpr}\\ % %{\tacexpr} is evaluated to $v$ and $v$ is associated to {\ident}. Next, every @@ -649,8 +802,8 @@ Basically, tactics toplevel definitions are made as follows: {\tt Ltac} {\ident} {\ident}$_1$ ... {\ident}$_n$ {\tt :=} {\tacexpr} \end{quote} -This defines a new tactic that can be used in any tactic script or new -tactic toplevel definition. +This defines a new {\ltac} function that can be used in any tactic +script or new {\ltac} toplevel definition. \Rem The preceding definition can equivalently be written: \begin{quote} @@ -674,8 +827,49 @@ possible with the syntax: %usual except that the substitutions are lazily carried out (when an identifier %to be evaluated is the name of a recursive definition). -\endinput +\subsection{Printing {\ltac} tactics} +\comindex{Print Ltac} + +Defined {\ltac} functions can be displayed using the command + +\begin{quote} +{\tt Print Ltac {\qualid}.} +\end{quote} + +\section{Debugging {\ltac} tactics} +\comindex{Set Ltac Debug} +\comindex{Unset Ltac Debug} +\comindex{Test Ltac Debug} + +The {\ltac} interpreter comes with a step-by-step debugger. The +debugger can be activated using the command + +\begin{quote} +{\tt Set Ltac Debug.} +\end{quote} + +\noindent and deactivated using the command + +\begin{quote} +{\tt Unset Ltac Debug.} +\end{quote} + +To know if the debugger is on, use the command \texttt{Test Ltac Debug}. +When the debugger is activated, it stops at every step of the +evaluation of the current {\ltac} expression and it prints information +on what it is doing. The debugger stops, prompting for a command which +can be one of the following: + +\medskip +\begin{tabular}{ll} +simple newline: & go to the next step\\ +h: & get help\\ +x: & exit current evaluation\\ +s: & continue current evaluation without stopping\\ +r$n$: & advance $n$ steps further\\ +\end{tabular} +\endinput \subsection{Permutation on closed lists} diff --git a/doc/refman/RefMan-mod.tex b/doc/refman/RefMan-mod.tex index 9f6f2abc..44a88034 100644 --- a/doc/refman/RefMan-mod.tex +++ b/doc/refman/RefMan-mod.tex @@ -55,6 +55,11 @@ This command is used to start an interactive module named {\ident}. {\modbindings}. The output module type is verified against the module type {\modtype}. +\item\texttt{Module [Import|Export]} + + Behaves like \texttt{Module}, but automatically imports or exports + the module. + \end{Variants} \subsection{\tt End {\ident} @@ -139,38 +144,9 @@ Defines a module type {\ident} equal to {\modtype}. {\modbindings} and returning {\modtype}. \end{Variants} -\subsection{\tt Declare Module {\ident}} - -Starts an interactive module declaration. This command is available -only in module types. - -\begin{Variants} - -\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}} -% -% Starts an interactive declaration of a module satisfying {\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 +Declares a module {\ident} of type {\modtype}. This command is available only in module types. \begin{Variants} @@ -189,6 +165,11 @@ only in module types. Declares a module equal to the module {\qualid}, verifying that the module type of the latter is a subtype of {\modtype}. +\item\texttt{Declare Module [Import|Export] {\ident} := {\qualid}} + + Declares a modules {\ident} of type {\modtype}, and imports or + exports it directly. + \end{Variants} @@ -389,6 +370,11 @@ Prints the module type and (optionally) the body of the module {\ident}. Prints the module type corresponding to {\ident}. +\subsection{\texttt{Locate Module {\qualid}} +\comindex{Locate Module}} + +Prints the full name of the module {\qualid}. + %%% Local Variables: %%% mode: latex diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex index e92cde74..1d2057a9 100644 --- a/doc/refman/RefMan-oth.tex +++ b/doc/refman/RefMan-oth.tex @@ -334,6 +334,72 @@ Locate I.Dont.Exist. \SeeAlso Section \ref{LocateSymbol} +\subsection{The {\sc Whelp} searching tool +\label{Whelp}} + +{\sc Whelp} is an experimental searching and browsing tool for the +whole {\Coq} library and the whole set of {\Coq} user contributions. +{\sc Whelp} requires a browser to work. {\sc Whelp} has been developed +at the University of Bologna as part of the HELM\footnote{Hypertextual +Electronic Library of Mathematics} and MoWGLI\footnote{Mathematics on +the Web, Get it by Logics and Interfaces} projects. It can be invoked +directly from the {\Coq} toplevel or from {\CoqIDE}, assuming a +graphical environment is also running. The browser to use can be +selected by setting the environment variable {\tt +COQREMOTEBROWSER}. If not explicitly set, it defaults to +\verb!netscape -remote "OpenURL(%s)"! or +\verb!C:\\PROGRA~1\\INTERN~1\\IEXPLORE %s!, depending on the +underlying operating system (in the command, the string \verb!%s! +serves as metavariable for the url to open). + +The {\sc Whelp} commands are: + +\subsubsection{\tt Whelp Locate "{\sl reg\_expr}". +\comindex{Whelp Locate}} + +This command opens a browser window and displays the result of seeking +for all names that match the regular expression {\sl reg\_expr} in the +{\Coq} library and user contributions. The regular expression can +contain the special operators are * and ? that respectively stand for +an arbitrary substring and for exactly one character. + +\variant {\tt Whelp Locate {\ident}.}\\ +This is equivalent to {\tt Whelp Locate "{\ident}"}. + +\subsubsection{\tt Whelp Match {\pattern}. +\comindex{Whelp Match}} + +This command opens a browser window and displays the result of seeking +for all statements that match the pattern {\pattern}. Holes in the +pattern are represented by the wildcard character ``\_''. + +\subsubsection{\tt Whelp Instance {\pattern}.} +\comindex{Whelp Instance} + +This command opens a browser window and displays the result of seeking +for all statements that are instances of the pattern {\pattern}. The +pattern is here assumed to be an universally quantified expression. + +\subsubsection{\tt Whelp Elim {\qualid}.} +\comindex{Whelp Elim} + +This command opens a browser window and displays the result of seeking +for all statements that have the ``form'' of an elimination scheme +over the type denoted by {\qualid}. + +\subsubsection{\tt Whelp Hint {\term}.} +\comindex{Whelp Hint} + +This command opens a browser window and displays the result of seeking +for all statements that can be instantiated so that to prove the +statement {\term}. + +\variant {\tt Whelp Hint.}\\ This is equivalent to {\tt Whelp Hint +{\sl goal}} where {\sl goal} is the current goal to prove. Notice that +{\Coq} does not send the local environment of definitions to the {\sc +Whelp} tool so that it only works on requests strictly based on, only, +definitions of the standard library and user contributions. + \section{Loading files} \Coq\ offers the possibility of loading different @@ -765,7 +831,39 @@ This command displays the current nesting depth used for display. %\subsection{\tt Abstraction ...} %Not yet documented. -% $Id: RefMan-oth.tex 8606 2006-02-23 13:58:10Z herbelin $ +\section{Controlling the conversion algorithm} + +{\Coq} comes with two algorithms to check the convertibility of types +(see section~\ref{convertibility}). The first algorithm lazily +compares applicative terms while the other is a brute-force but efficient +algorithm that first normalizes the terms before comparing them. The +second algorithm is based on a bytecode representation of terms +similar to the bytecode representation used in the ZINC virtual +machine~\cite{Leroy90}. It is specially useful for intensive +computation of algebraic values, such as numbers, and for reflexion-based +tactics. + +\subsection{\tt Set Virtual Machine +\label{SetVirtualMachine} +\comindex{Set Virtual Machine}} + +This activates the bytecode-based conversion algorithm. + +\subsection{\tt Unset Virtual Machine +\comindex{Unset Virtual Machine}} + +This deactivates the bytecode-based conversion algorithm. + +\subsection{\tt Test Virtual Machine +\comindex{Test Virtual Machine}} + +This tells if the bytecode-based conversion algorithm is +activated. The default behavior is to have the bytecode-based +conversion algorithm deactivated. + +\SeeAlso sections~\ref{vmcompute} and~\ref{vmoption}. + +% $Id: RefMan-oth.tex 9044 2006-07-12 13:22:17Z herbelin $ %%% Local Variables: %%% mode: latex diff --git a/doc/refman/RefMan-pre.tex b/doc/refman/RefMan-pre.tex index 2f79e5f0..43216ed0 100644 --- a/doc/refman/RefMan-pre.tex +++ b/doc/refman/RefMan-pre.tex @@ -556,19 +556,19 @@ unresolved implicit has been implemented by Hugo Herbelin. Laurent Théry's contribution on strings and Pierre Letouzey and Jean-Christophe Filliâtre's contribution on finite maps have been integrated to the {\Coq} standard library. Pierre Letouzey developed a -library about finite sets ``à la Objective Caml'' and extended the -lists library. Pierre Letouzey's contribution on rational numbers -has been integrated too. +library about finite sets ``à la Objective Caml''. With Jean-Marc +Notin, he extended the library on lists. Pierre Letouzey's +contribution on rational numbers has been integrated and extended.. Pierre Corbineau extended his tactic for solving first-order -statements. He wrote a reflexion-based intuitionistic tautology +statements. He wrote a reflection-based intuitionistic tautology solver. -Jean-Marc Notin took care of {\textsf{coqdoc}} and of the general -maintenance of the system. +Jean-Marc Notin significantly contributed to the general maintenance +of the system. He also took care of {\textsf{coqdoc}}. \begin{flushright} -Palaiseau, Apr. 2006\\ +Palaiseau, July 2006\\ Hugo Herbelin \end{flushright} @@ -577,7 +577,7 @@ Hugo Herbelin % Integration of ZArith lemmas from Sophia and Nijmegen. -% $Id: RefMan-pre.tex 8941 2006-06-09 16:43:42Z herbelin $ +% $Id: RefMan-pre.tex 9030 2006-07-07 15:37:23Z herbelin $ %%% Local Variables: %%% mode: latex diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex index 739ca6b5..8c1a7824 100644 --- a/doc/refman/RefMan-pro.tex +++ b/doc/refman/RefMan-pro.tex @@ -163,28 +163,21 @@ as a {\tt Theorem}, the name {\ident} is known at all section levels: current section. \end{Variants} -\subsection{\tt Proof {\term}.}\comindex{Proof} +\subsection{\tt Proof {\term}.} +\comindex{Proof} +\label{BeginProof} This command applies in proof editing mode. It is equivalent to {\tt exact {\term}; Save.} That is, you have to give the full proof in one gulp, as a proof term (see section \ref{exact}). -\begin{Variants} - -\item{\tt Proof.} +\variant {\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} +\SeeAlso {\tt Proof with {\tac}.} in section~\ref{ProofWith}. \subsection{\tt Abort.} \comindex{Abort} @@ -381,7 +374,7 @@ All the hypotheses remains usable in the proof development. This command goes back to the default mode which is to print all available hypotheses. -% $Id: RefMan-pro.tex 8609 2006-02-24 13:32:57Z notin,no-port-forwarding,no-agent-forwarding,no-X11-forwarding,no-pty $ +% $Id: RefMan-pro.tex 9030 2006-07-07 15:37:23Z herbelin $ %%% Local Variables: %%% mode: latex diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex index 341e766e..e41983dc 100644 --- a/doc/refman/RefMan-syn.tex +++ b/doc/refman/RefMan-syn.tex @@ -221,6 +221,14 @@ The command to display the current state of the {\Coq} term parser is \tt Print Grammar constr. \end{quote} +\variant + +\comindex{Print Grammar pattern} +{\tt Print Grammar pattern.}\\ + +This displays the state of the subparser of patterns (the parser +used in the grammar of the {\tt match} {\tt with} constructions). + \subsection{Displaying symbolic notations} The command \texttt{Notation} has an effect both on the {\Coq} parser and @@ -436,9 +444,10 @@ Locate "'exists' _ , _". \SeeAlso Section \ref{Locate}. \begin{figure} +\begin{small} \begin{centerframe} \begin{tabular}{lcl} -{\sentence} & ::= & +{\sentence} & ::= & \texttt{Notation} \zeroone{\tt Local} {\str} \texttt{:=} {\term} \zeroone{\modifiers} \zeroone{:{\scope}} .\\ & $|$ & @@ -474,6 +483,7 @@ Locate "'exists' _ , _". & $|$ & {\tt format} {\str} \end{tabular} \end{centerframe} +\end{small} \caption{Syntax of the variants of {\tt Notation}} \label{notation-syntax} \end{figure} @@ -633,7 +643,8 @@ instance the infix symbol \verb=+= can be used to denote distinct definitions of an additive operator. Depending on which interpretation scopes is currently open, the interpretation is different. Interpretation scopes can include an interpretation for -numerals. However, this is only made possible at the {\ocaml} level. +numerals and strings. However, this is only made possible at the +{\ocaml} level. See Figure \ref{notation-syntax} for the syntax of notations including the possibility to declare them in a given scope. Here is a typical @@ -824,6 +835,21 @@ type {\tt positive} (binary strictly positive numbers). It is delimited by key {\tt positive} and comes with an interpretation for numerals as closed term of type {\tt positive}. +\subsubsection{\tt Q\_scope} + +This includes the standard arithmetical operators and relations on +type {\tt Q} (rational numbers defined as fractions of an integer and +a strictly positive integer modulo the equality of the +numerator-denominator cross-product). As for numerals, only $0$ and +$1$ have an interpretation in scope {\tt Q\_scope} (their +interpretations are $\frac{0}{1}$ and $\frac{1}{1}$ respectively). + +\subsubsection{\tt Qc\_scope} + +This includes the standard arithmetical operators and relations on the +type {\tt Qc} of rational numbers defined as the type of irreducible +fractions of an integer and a strictly positive integer. + \subsubsection{\tt real\_scope} This includes the standard arithmetical operators and relations on @@ -853,6 +879,25 @@ delimited by key {\tt list}. This includes the notation for pairs. It is delimited by key {\tt core}. +\subsubsection{\tt string\_scope} + +This includes notation for strings as elements of the type {\tt +string}. Special characters and escaping follow {\Coq} conventions +on strings (see page~\pageref{strings}). Especially, there is no +convention to visualize non printable characters of a string. The +file {\tt String.v} shows an example that contains quotes, a newline +and a beep (i.e. the ascii character of code 7). + +\subsubsection{\tt char\_scope} + +This includes interpretation for all strings of the form +\verb!"!$c$\verb!"! where $c$ is an ascii character, or of the form +\verb!"!$nnn$\verb!"! where $nnn$ is a three-digits number (possibly +with leading 0's), or of the form \verb!""""!. Their respective +denotations are the ascii code of $c$, the decimal ascii code $nnn$, +or the ascii code of the character \verb!"! (i.e. the ascii code +34), all of them being represented in the type {\tt ascii}. + \subsection{Displaying informations about scopes} \subsubsection{\tt Print Visibility} @@ -948,11 +993,14 @@ tactic language\footnote{Tactic notations are just a simplification of the {\tt Grammar tactic simple\_tactic} command that existed in versions prior to version 8.0.}. Tactic notations obey the following syntax +\medskip +\noindent \begin{tabular}{lcl} -{\sentence} & ::= & \texttt{Tactic Notation} {\str} \sequence{\proditem}{} \\ +{\sentence} & ::= & \texttt{Tactic Notation} {\taclevel} \sequence{\proditem}{} \\ & & \texttt{:= {\tac} .}\\ {\proditem} & ::= & {\str} $|$ {\tacargtype}{\tt ({\ident})} \\ +{\taclevel} & ::= & $|$ {\tt (at level} {\naturalnumber}{\tt )} \\ {\tacargtype} & ::= & %{\tt preident} $|$ {\tt ident} $|$ @@ -966,14 +1014,18 @@ syntax {\tt int\_or\_var} $|$ {\tt tactic} $|$ \end{tabular} +\medskip -A tactic notation {\tt Tactic Notation {\str} {\sequence{\proditem}{}} -:= {\tac}} extends the parser and pretty-printer of tactics with a -new rule made of the juxtaposition of the head name of the tactic -{\str} and the list of its production items (in the syntax of -production items, {\str} stands for a terminal symbol and {\tt -\tacargtype({\ident}) for non terminal entries}. It then evaluates -into the tactic expression {\tac}. +A tactic notation {\tt Tactic Notation {\taclevel} +{\sequence{\proditem}{}} := {\tac}} extends the parser and +pretty-printer of tactics with a new rule made of the list of +production items. It then evaluates into the tactic expression +{\tac}. For simple tactics, it is recommended to use a terminal +symbol, i.e. a {\str}, for the first production item. The tactic +level indicates the parsing precedence of the tactic notation. This +information is particularly relevant for notations of tacticals. +Levels 0 to 5 are available. To know the parsing precedences of the +existing tacticals, use the command {\tt Print Grammar tactic.} Each type of tactic argument has a specific semantic regarding how it is parsed and how it is interpreted. The semantic is described in the @@ -1008,7 +1060,7 @@ for {\tt integer}. This is the reason for introducing a special entry syntactically includes identifiers in order to be usable in tactic definitions. -% $Id: RefMan-syn.tex 8609 2006-02-24 13:32:57Z notin,no-port-forwarding,no-agent-forwarding,no-X11-forwarding,no-pty $ +% $Id: RefMan-syn.tex 9012 2006-07-05 16:03:16Z herbelin $ %%% Local Variables: %%% mode: latex diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index f034df41..24699873 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -69,6 +69,13 @@ convertible (see Section~\ref{conv-rules}). \item \errindex{Not an exact proof} \end{ErrMsgs} +\begin{Variants} + \item \texttt{eexact \term}\tacindex{eexact} + + This tactic behaves like \texttt{exact} but is able to handle terms with meta-variables. + +\end{Variants} + \subsection{\tt refine \term \tacindex{refine} @@ -112,6 +119,15 @@ subgoal is proved. Otherwise, it fails. \item \errindex{No such assumption} \end{ErrMsgs} +\begin{Variants} + \item \texttt{eassumption} + + This tactic behaves like \texttt{assumption} but is able to handle + goals with meta-variables. + +\end{Variants} + + \subsection{\tt clear {\ident} \tacindex{clear} \label{clear}} @@ -133,6 +149,10 @@ usable in the proof development. its body. Otherwise said, this tactic turns a definition into an assumption. +\item \texttt{clear - {\ident}.} + + This tactic clears all hypotheses except the ones depending in {\ident}. + \end{Variants} \begin{ErrMsgs} @@ -506,6 +526,20 @@ in the list of subgoals remaining to prove. following subgoals: {\tt U -> T} and \texttt{U}. The subgoal {\tt U -> T} comes first in the list of remaining subgoal to prove. +\item \texttt{assert {\form} by {\tac}}\tacindex{assert by} + + This tactic behaves like \texttt{assert} but tries to apply {\tac} + to any subgoals generated by \texttt{assert}. + +\item \texttt{assert {\form} as {\ident}\tacindex{assert as}} + + This tactic behaves like \texttt{assert ({\ident} : {\form})}. + +\item \texttt{pose proof {\term} as {\ident}} + + This tactic behaves like \texttt{assert ({\ident:T} by exact {\term}} where + \texttt{T} is the type of {\term}. + \end{Variants} % PAS CLAIR; @@ -721,6 +755,7 @@ performs the conversion in hypotheses $H_1\ldots H_n$. \tacindex{cbv} \tacindex{lazy} \tacindex{compute}} +\label{vmcompute} These parameterized reduction tactics apply to any goal and perform the normalization of the goal according to the specified flags. Since @@ -764,6 +799,16 @@ computational expressions (i.e. with few dead code). \item {\tt compute} \tacindex{compute} This tactic is an alias for {\tt cbv beta delta evar iota zeta}. + +\item {\tt vm\_compute} \tacindex{vm\_compute} + + This tactic evaluates the goal using the optimized call-by-value + evaluation bytecode-based virtual machine. This algorithm is + dramatically more efficient than the algorithm used for the {\tt + cbv} tactic, but it cannot be fine-tuned. It is specially + interesting for full evaluation of algebraic objects. This includes + the case of reflexion-based tactics. + \end{Variants} \begin{ErrMsgs} @@ -1012,6 +1057,14 @@ equivalent to {\tt intros; apply ci}. these expressions are equivalent to the corresponding {\tt constructor $i$ with \bindinglist}. +\item \texttt{econstructor} + + This tactic behaves like \texttt{constructor} but is able to + introduce existential variables if an instanciation for a variable + cannot be found (cf \texttt{eapply}). The tactics \texttt{eexists}, + \texttt{esplit}, \texttt{eleft} and \texttt{eright} follows the same + behaviour. + \end{Variants} \section{Eliminations (Induction and Case Analysis)} @@ -1096,6 +1149,11 @@ induction n. scheme of name {\qualid}. It does not expect that the type of {\term} is inductive. +\item \texttt{induction {\term}$_1$ $\ldots$ {\term}$_n$ using {\qualid}} + + where {\qualid} is an induction principle with complex predicates + (like the ones generated by function induction). + \item {\tt induction {\term} using {\qualid} as {\intropattern}} This combines {\tt induction {\term} using {\qualid}} @@ -1233,6 +1291,10 @@ last introduced hypothesis. {\tt ($p_{1}$,\ldots,$p_{n}$)} can be used instead of {\tt [} $p_{1} $\ldots $p_{n}$ {\tt ]}. +\item \texttt{pose proof {\term} as {\intropattern}} + + This tactic behaves like \texttt{destruct {\term} as {\intropattern}}. + \item{\tt destruct {\term} using {\qualid}} This is a synonym of {\tt induction {\term} using {\qualid}}. @@ -1279,6 +1341,7 @@ components of an hypothesis. An introduction pattern is either: \begin{itemize} \item the wildcard: {\tt \_} +\item the pattern \texttt{?} \item a variable \item a disjunction of lists of patterns: {\tt [$p_{11}$ {\ldots} $p_{1m_1}$ | {\ldots} | $p_{11}$ {\ldots} $p_{nm_n}$]} @@ -1290,6 +1353,8 @@ structure of the pattern given as argument: \begin{itemize} \item introduction on the wildcard do the introduction and then immediately clear (cf~\ref{clear}) the corresponding hypothesis; +\item introduction on \texttt{?} do the introduction, and let Coq + choose a fresh name for the variable; \item introduction on a variable behaves like described in~\ref{intro}; \item introduction over a list of patterns $p_1~\ldots~p_n$ is equivalent to the sequence of @@ -1323,7 +1388,8 @@ inductive type with a single constructor. Lemma intros_test : forall A B C:Prop, A \/ B /\ C -> (A -> C) -> C. intros A B C [a| [_ c]] f. apply (f a). -Proof c. +exact c. +Qed. \end{coq_example} %\subsection{\tt FixPoint \dots}\tacindex{Fixpoint} @@ -1479,7 +1545,10 @@ implicit type of $t$ and $u$. This tactic applies to any goal. The type of {\term} must have the form -\texttt{(x$_1$:A$_1$) \dots\ (x$_n$:A$_n$)}\term$_1${\tt =}\term$_2$. +\texttt{(x$_1$:A$_1$) \dots\ (x$_n$:A$_n$)}\texttt{eq}\term$_1$ \term$_2$. + +\noindent where \texttt{eq} is the Leibniz equality or a registered +setoid equality. \noindent Then {\tt rewrite \term} replaces every occurrence of \term$_1$ by \term$_2$ in the goal. Some of the variables x$_1$ are @@ -1506,10 +1575,14 @@ This happens if \term$_1$ does not occur in the goal. \item {\tt rewrite <- {\term}}\tacindex{rewrite <-}\\ Uses the equality \term$_1${\tt=}\term$_2$ from right to left -\item {\tt rewrite {\term} in {\ident}} +\item {\tt rewrite {\term} in \textit{clause}} \tacindex{rewrite \dots\ in}\\ - Analogous to {\tt rewrite {\term}} but rewriting is done in the - hypothesis named {\ident}. + Analogous to {\tt rewrite {\term}} but rewriting is done following + \textit{clause} (similarly to \ref{Conversion-tactics}). For instance: + \texttt{rewrite H in H1,H2 |- *} means \texttt{rewrite H in H1; + rewrite H in H2; rewrite H} and \texttt{rewrite H in * |-} will do + \texttt{try rewrite H in H$_i$} for all hypothesis \texttt{H$_i$ <> + H}. \item {\tt rewrite -> {\term} in {\ident}} \tacindex{rewrite -> \dots\ in}\\ @@ -1540,17 +1613,26 @@ symmetric form occurs. It is equivalent to {\tt cut \term$_2$=\term$_1$; [intro H{\sl n}; rewrite <- H{\sl n}; clear H{\sl n}| assumption || symmetry; try assumption]}. +\begin{ErrMsgs} +\item \errindex{terms do not have convertible types} +\end{ErrMsgs} + \begin{Variants} \item {\tt replace {\term$_1$} with {\term$_2$} in \ident}\\ This replaces {\term$_1$} with {\term$_2$} in the hypothesis named {\ident}, and generates the subgoal {\term$_2$}{\tt =}{\term$_1$}. - \begin{ErrMsgs} - \item \errindex{No such hypothesis} : {\ident} - \item \errindex{Nothing to rewrite in {\ident}} - \end{ErrMsgs} +% \begin{ErrMsgs} +% \item \errindex{No such hypothesis} : {\ident} +% \item \errindex{Nothing to rewrite in {\ident}} +% \end{ErrMsgs} +\item {\tt replace {\term$_1$} with {\term$_2$} by \tac}\\ This acts as + {\tt replace {\term$_1$} with {\term$_2$}} but try to solve the + generated subgoal {\tt \term$_2$=\term$_1$} using {\tt \tac}. +\item {\tt replace {\term$_1$} with {\term$_2$} in \ident by \tac}\\ + This acts as {\tt replace {\term$_1$} with {\term$_2$} in \ident} but try to solve the generated subgoal {\tt \term$_2$=\term$_1$} using {\tt \tac}. \end{Variants} \subsection{\tt reflexivity @@ -1617,12 +1699,12 @@ goal stating ``$eq$ {\term} {\term}$_1$''. Lemmas are added to the database using the command \comindex{Declare Left Step} \begin{quote} -{\tt Declare Left Step {\qualid}.} +{\tt Declare Left Step {\term}.} \end{quote} -where {\qualid} is the name of the lemma. The tactic is especially useful for parametric setoids which are not -accepted as regular setoids for {\tt rewrite} and {\tt setoid\_replace} (see chapter \ref{setoid_replace}). +accepted as regular setoids for {\tt rewrite} and {\tt + setoid\_replace} (see chapter \ref{setoid_replace}). \tacindex{stepr} \comindex{Declare Right Step} @@ -1638,7 +1720,7 @@ Lemmas are expected to be of the form $z$, $R$ $x$ $y$ {\tt ->} $eq$ $y$ $z$ {\tt ->} $R$ $x$ $z$'' and are registered using the command \begin{quote} -{\tt Declare Right Step {\qualid}.} +{\tt Declare Right Step {\term}.} \end{quote} \end{Variants} @@ -2157,6 +2239,11 @@ hints of the database named {\tt core}. Uses all existing hint databases, minus the special database {\tt v62}. See Section~\ref{Hints-databases} +\item \texttt{auto using $lemma_1, \ldots, lemma_n$} + + Uses $lemma_1, \ldots, lemma_n$ in addition to hints (can be conbined + with the \texttt{with \ident} option). + \item {\tt trivial}\tacindex{trivial} This tactic is a restriction of {\tt auto} that is not recursive and @@ -2306,6 +2393,15 @@ incompatibilities. % En attente d'un moyen de valoriser les fichiers de demos %\SeeAlso file \texttt{contrib/Rocq/DEMOS/Demo\_tauto.v} + +\subsection{\tt rtauto +\tacindex{rtauto} +\label{rtauto}} + +The {\tt rtauto} tactic solves propositional tautologies similarly to what {\tt tauto} does. The main difference is that the proof term is built using a reflection scheme applied to a sequent calculus proof of the goal. The search procedure is also implemented using a different technique. + +Users should be aware that this difference may result in faster proof-search but slower proof-checking, and {\tt rtauto} might not solve goals that {\tt tauto} would be able to solve (e.g. goals involving universal quantifiers). + \subsection{{\tt firstorder} \tacindex{firstorder} \label{firstorder}} @@ -2459,7 +2555,7 @@ equalities with uninterpreted symbols. It also include the constructor theory (see \ref{injection} and \ref{discriminate}). If the goal is a non-quantified equality, {\tt congruence} tries to prove it with non-quantified equalities in the context. Otherwise it -tries to infer a discriminable equality from those in the context. +tries to infer a discriminable equality from those in the context. Alternatively, congruence tries to prove that an hypothesis is equal to the goal or to the negation of another hypothesis. \begin{coq_eval} Reset Initial. @@ -2489,14 +2585,28 @@ intros. congruence. \end{coq_example} +\begin{Variants} +\item {\tt congruence with \term$_1$ \dots\ \term$_n$}\\ + Adds {\tt \term$_1$ \dots\ \term$_n$} to the pool of terms used by + {\tt congruence}. This helps in case you have partially applied + constructors in your goal. +\end{Variants} + \begin{ErrMsgs} \item \errindex{I don't know how to handle dependent equality} \\ The decision procedure managed to find a proof of the goal or of a discriminable equality but this proof couldn't be built in Coq because of dependently-typed functions. \item \errindex{I couldn't solve goal} \\ - The decision procedure didn't managed to find a proof of the goal or of - a discriminable equality. + The decision procedure didn't find any way to solve the goal. + \item \errindex{Goal is solvable by congruence but some arguments are missing. Try "congruence with \dots", replacing metavariables by arbitrary terms.} \\ + The decision procedure could solve the goal with the provision + that additional arguments are supplied for some partially applied + constructors. Any term of an appropriate type will allow the + tactic to successfully solve the goal. Those additional arguments + can be given to {\tt congruence} by filling in the holes in the + terms given in the error message, using the {\tt with} variant + described below. \end{ErrMsgs} \subsection{\tt omega @@ -2679,7 +2789,7 @@ of the reengineering of the code, this tactic has also been completely revised to get a very compact and readable version.} carries out rewritings according the rewriting rule bases {\tt \ident$_1$ \dots \ident$_n$}. - Each rewriting rule of a base \ident$_i$ is applied to the main subgoal until +Each rewriting rule of a base \ident$_i$ is applied to the main subgoal until it fails. Once all the rules have been processed, if the main subgoal has progressed (e.g., if it is distinct from the initial main goal) then the rules of this base are processed again. If the main subgoal has not progressed then @@ -2695,58 +2805,24 @@ command. \item {\tt autorewrite with \ident$_1$ \dots \ident$_n$ using \tac}\\ Performs, in the same way, all the rewritings of the bases {\tt $ident_1$ $...$ $ident_n$} applying {\tt \tac} to the main subgoal after each rewriting step. -%\item{\tt autorewrite [ \ident$_1$ \dots \ident$_n$ ]}\\ -%{\tt autorewrite [ \ident$_1$ \dots \ident$_n$ ] using \tac}\\ -%These are deprecated syntactic variants for -%{\tt autorewrite with \ident$_1$ \dots \ident$_n$} -%and -%{\tt autorewrite with \ident$_1$ \dots \ident$_n$ using \tac}. -\end{Variant} -\subsection{\tt Hint Rewrite \term$_1$ \dots \term$_n$ : \ident -\comindex{Hint Rewrite}} +\item \texttt{autorewrite with {\ident} in {\qualid}} -This vernacular command adds the terms {\tt \term$_1$ \dots \term$_n$} -(their types must be equalities) in the rewriting base {\tt \ident} -with the default orientation (left to right). Notice that the -rewriting bases are distinct from the {\tt auto} hint bases and that -{\tt auto} does not take them into account. - -This command is synchronous with the section mechanism (see \ref{Section}): -when closing a section, all aliases created by \texttt{Hint Rewrite} in that -section are lost. Conversely, when loading a module, all \texttt{Hint Rewrite} -declarations at the global level of that module are loaded. - -\begin{Variants} -\item {\tt Hint Rewrite -> \term$_1$ \dots \term$_n$ : \ident}\\ -This is strictly equivalent to the command above (we only make explicit the -orientation which otherwise defaults to {\tt ->}). - -\item {\tt Hint Rewrite <- \term$_1$ \dots \term$_n$ : \ident}\\ -Adds the rewriting rules {\tt \term$_1$ \dots \term$_n$} with a right-to-left -orientation in the base {\tt \ident}. + Performs all the rewritings in hypothesis {\qualid}. -\item {\tt Hint Rewrite \term$_1$ \dots \term$_n$ using {\tac} : {\ident}}\\ -When the rewriting rules {\tt \term$_1$ \dots \term$_n$} in {\tt \ident} will -be used, the tactic {\tt \tac} will be applied to the generated subgoals, the -main subgoal excluded. - -%% \item -%% {\tt Hint Rewrite [ \term$_1$ \dots \term$_n$ ] in \ident}\\ -%% {\tt Hint Rewrite [ \term$_1$ \dots \term$_n$ ] in {\ident} using {\tac}}\\ -%% These are deprecated syntactic variants for -%% {\tt Hint Rewrite \term$_1$ \dots \term$_n$ : \ident} and -%% {\tt Hint Rewrite \term$_1$ \dots \term$_n$ using {\tac} : {\ident}}. +\end{Variant} -\end{Variants} +\SeeAlso section \ref{HintRewrite} for feeding the database of lemmas used by {\tt autorewrite}. -\SeeAlso \ref{autorewrite-example} for examples showing the use of +\SeeAlso section \ref{autorewrite-example} for examples showing the use of this tactic. % En attente d'un moyen de valoriser les fichiers de demos %\SeeAlso file \texttt{contrib/Rocq/DEMOS/Demo\_AutoRewrite.v} -\section{The hints databases for {\tt auto} and {\tt eauto} +\section{Controlling automation} + +\subsection{The hints databases for {\tt auto} and {\tt eauto} \index{Hints databases} \label{Hints-databases} \comindex{Hint}} @@ -3036,6 +3112,47 @@ every moment. \end{Variants} +\subsection{\tt Hint Rewrite \term$_1$ \dots \term$_n$ : \ident +\label{HintRewrite} +\comindex{Hint Rewrite}} + +This vernacular command adds the terms {\tt \term$_1$ \dots \term$_n$} +(their types must be equalities) in the rewriting base {\tt \ident} +with the default orientation (left to right). Notice that the +rewriting bases are distinct from the {\tt auto} hint bases and that +{\tt auto} does not take them into account. + +This command is synchronous with the section mechanism (see \ref{Section}): +when closing a section, all aliases created by \texttt{Hint Rewrite} in that +section are lost. Conversely, when loading a module, all \texttt{Hint Rewrite} +declarations at the global level of that module are loaded. + +\begin{Variants} +\item {\tt Hint Rewrite -> \term$_1$ \dots \term$_n$ : \ident}\\ +This is strictly equivalent to the command above (we only make explicit the +orientation which otherwise defaults to {\tt ->}). + +\item {\tt Hint Rewrite <- \term$_1$ \dots \term$_n$ : \ident}\\ +Adds the rewriting rules {\tt \term$_1$ \dots \term$_n$} with a right-to-left +orientation in the base {\tt \ident}. + +\item {\tt Hint Rewrite \term$_1$ \dots \term$_n$ using {\tac} : {\ident}}\\ +When the rewriting rules {\tt \term$_1$ \dots \term$_n$} in {\tt \ident} will +be used, the tactic {\tt \tac} will be applied to the generated subgoals, the +main subgoal excluded. + +%% \item +%% {\tt Hint Rewrite [ \term$_1$ \dots \term$_n$ ] in \ident}\\ +%% {\tt Hint Rewrite [ \term$_1$ \dots \term$_n$ ] in {\ident} using {\tac}}\\ +%% These are deprecated syntactic variants for +%% {\tt Hint Rewrite \term$_1$ \dots \term$_n$ : \ident} and +%% {\tt Hint Rewrite \term$_1$ \dots \term$_n$ using {\tac} : {\ident}}. + +\item \texttt{Print Rewrite HintDb {\ident}} + + This command displays all rewrite hints contained in {\ident}. + +\end{Variants} \subsection{Hints and sections \label{Hint-and-Section}} @@ -3046,6 +3163,42 @@ 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{Setting implicit automation tactics} + +\subsubsection{\tt Proof with {\tac}.} +\label{ProofWith} +\comindex{Proof with} + + This command may be used to start a proof. It defines a default + tactic to be used each time a tactic command {\tac$_1$} is ended by + ``\verb#...#''. In this case the tactic command typed by the user is + equivalent to \tac$_1$;{\tac}. + +\SeeAlso {\tt Proof.} in section~\ref{BeginProof}. + +\subsubsection{\tt Declare Implicit Tactic {\tac}.} +\comindex{Declare Implicit Tactic} + +This command declares a tactic to be used to solve implicit arguments +that {\Coq} does not know how to solve by unification. It is used +every time the term argument of a tactic has one of its holes not +fully resolved. + +Here is an example: + +\begin{coq_example} +Parameter quo : nat -> forall n:nat, n<>0 -> nat. +Notation "x // y" := (quo x y _) (at level 40). + +Declare Implicit Tactic assumption. +Goal forall n m, m<>0 -> { q:nat & { r | q * m + r = n } }. +intros. +exists (n // m). +\end{coq_example} + +The tactic {\tt exists (n // m)} did not fail. The hole was solved by +{\tt assumption} so that it behaved as {\tt exists (quo n m H)}. + \section{Generation of induction principles with {\tt Scheme} \label{Scheme} \comindex{Scheme}} @@ -3139,7 +3292,7 @@ The chapter~\ref{TacticLanguage} gives examples of more complex user-defined tactics. -% $Id: RefMan-tac.tex 8938 2006-06-09 16:29:01Z jnarboux $ +% $Id: RefMan-tac.tex 9044 2006-07-12 13:22:17Z herbelin $ %%% Local Variables: %%% mode: latex diff --git a/doc/refman/Reference-Manual.tex b/doc/refman/Reference-Manual.tex index 4542e730..14fbff47 100644 --- a/doc/refman/Reference-Manual.tex +++ b/doc/refman/Reference-Manual.tex @@ -68,7 +68,7 @@ \include{RefMan-oth.v}% Vernacular commands \include{RefMan-pro}% Proof handling \include{RefMan-tac.v}% Tactics and tacticals -\include{RefMan-ltac}% Writing tactics +\include{RefMan-ltac.v}% Writing tactics \include{RefMan-tacex.v}% Detailed Examples of tactics \part{User extensions} @@ -122,4 +122,4 @@ \end{document} -% $Id: Reference-Manual.tex 8688 2006-04-07 15:08:12Z msozeau $ +% $Id: Reference-Manual.tex 9038 2006-07-11 13:53:53Z herbelin $ diff --git a/doc/refman/cover.html b/doc/refman/cover.html index 1d2700b1..a3ec2516 100644 --- a/doc/refman/cover.html +++ b/doc/refman/cover.html @@ -13,7 +13,7 @@ The Coq Proof Assistant<BR> Reference Manual<BR></B></FONT><FONT SIZE=7> </FONT> -<BR><BR><FONT SIZE=5><B><BR></B></FONT><FONT SIZE=5><B>Version 8.0</B></FONT><FONT SIZE=5><B> +<BR><BR><FONT SIZE=5><B><BR></B></FONT><FONT SIZE=5><B>Version 8.1</B></FONT><FONT SIZE=5><B> </B></FONT><A NAME="text1"></A><A HREF="#note1"><SUP><FONT SIZE=2>1</FONT></SUP></A><FONT SIZE=5><B><BR><BR><BR><BR><BR><BR> </B></FONT><FONT SIZE=5><B>The Coq Development Team</B></FONT><FONT SIZE=5><B><BR></B></FONT><FONT SIZE=5><B>LogiCal Project</B></FONT><FONT SIZE=5><B><BR><BR><BR> </B></FONT></DIV><BR> @@ -22,6 +22,7 @@ The Coq Proof Assistant<BR> <DIV ALIGN=left> <FONT SIZE=4>V7.x © INRIA 1999-2004</FONT><BR> <FONT SIZE=4>V8.0 © INRIA 2004-2006</FONT><BR> +<FONT SIZE=4>V8.1 © INRIA 2006</FONT><BR> This material may be distributed only subject to the terms and conditions set forth in the Open Publication License, v1.0 or later (the latest version is presently available at <A HREF="http://www.opencontent.org/openpub">http://www.opencontent.org/openpub</A>). Options A and B are not elected. </DIV> <BR> diff --git a/doc/refman/index.html b/doc/refman/index.html index db19678f..9b5250ab 100644 --- a/doc/refman/index.html +++ b/doc/refman/index.html @@ -1,29 +1,14 @@ <HTML> -<BODY> +<HEAD> -<CENTER> +<TITLE>The Coq Proof Assistant Reference Manual</TITLE> -<TABLE BORDER="0" CELLPADDING=10> -<TR> -<TD><CENTER><A HREF="cover.html" TARGET="UP"><FONT SIZE=2>Cover page</FONT></A></CENTER></TD> -<TD><CENTER><A HREF="toc.html" TARGET="UP"><FONT SIZE=2>Table of contents</FONT></A></CENTER></TD> -<TD><CENTER><A HREF="biblio.html" TARGET="UP"><FONT SIZE=2> -Bibliography</FONT></A></CENTER></TD> -<TD><CENTER><A HREF="general-index.html" TARGET="UP"><FONT SIZE=2> -Global Index -</FONT></A></CENTER></TD> -<TD><CENTER><A HREF="tactic-index.html" TARGET="UP"><FONT SIZE=2> -Tactics Index -</FONT></A></CENTER></TD> -<TD><CENTER><A HREF="command-index.html" TARGET="UP"><FONT SIZE=2> -Vernacular Commands Index -</FONT></A></CENTER></TD> -<TD><CENTER><A HREF="error-index.html" TARGET="UP"><FONT SIZE=2> -Index of Error Messages -</FONT></A></CENTER></TD> -</TABLE> +</HEAD> -</CENTER> +<FRAMESET ROWS=90%,*> + <FRAME SRC="cover.html" NAME="UP"> + <FRAME SRC="menu.html"> +</FRAMESET> -</BODY></HTML>
\ No newline at end of file +</HTML>
\ No newline at end of file diff --git a/doc/refman/menu.html b/doc/refman/menu.html new file mode 100644 index 00000000..db19678f --- /dev/null +++ b/doc/refman/menu.html @@ -0,0 +1,29 @@ +<HTML> + +<BODY> + +<CENTER> + +<TABLE BORDER="0" CELLPADDING=10> +<TR> +<TD><CENTER><A HREF="cover.html" TARGET="UP"><FONT SIZE=2>Cover page</FONT></A></CENTER></TD> +<TD><CENTER><A HREF="toc.html" TARGET="UP"><FONT SIZE=2>Table of contents</FONT></A></CENTER></TD> +<TD><CENTER><A HREF="biblio.html" TARGET="UP"><FONT SIZE=2> +Bibliography</FONT></A></CENTER></TD> +<TD><CENTER><A HREF="general-index.html" TARGET="UP"><FONT SIZE=2> +Global Index +</FONT></A></CENTER></TD> +<TD><CENTER><A HREF="tactic-index.html" TARGET="UP"><FONT SIZE=2> +Tactics Index +</FONT></A></CENTER></TD> +<TD><CENTER><A HREF="command-index.html" TARGET="UP"><FONT SIZE=2> +Vernacular Commands Index +</FONT></A></CENTER></TD> +<TD><CENTER><A HREF="error-index.html" TARGET="UP"><FONT SIZE=2> +Index of Error Messages +</FONT></A></CENTER></TD> +</TABLE> + +</CENTER> + +</BODY></HTML>
\ No newline at end of file diff --git a/doc/tutorial/Tutorial.tex b/doc/tutorial/Tutorial.tex index 73d833c4..d5523f1f 100755 --- a/doc/tutorial/Tutorial.tex +++ b/doc/tutorial/Tutorial.tex @@ -31,20 +31,29 @@ proof tools. For more advanced information, the reader could refer to the \Coq{} Reference Manual or the \textit{Coq'Art}, a new book by Y. Bertot and P. Castéran on practical uses of the \Coq{} system. -We assume here that the potential user has installed \Coq~ on his workstation, -that he calls \Coq~ from a standard teletype-like shell window, and that -he does not use any special interface. +Coq can be used from a standard teletype-like shell window but +preferably through the graphical user interface +CoqIde\footnote{Alternative graphical interfaces exist: Proof General +and Pcoq.}. + Instructions on installation procedures, as well as more comprehensive documentation, may be found in the standard distribution of \Coq, which may be obtained from \Coq{} web site \texttt{http://coq.inria.fr}. -In the following, all examples preceded by the prompting sequence -\verb:Coq < : represent user input, terminated by a period. The -following lines usually show \Coq's answer as it appears on the users -screen. The sequence of such examples is a valid \Coq~ session, unless -otherwise specified. This version of the tutorial has been prepared -on a PC workstation running Linux. -The standard invocation of \Coq\ delivers a message such as: +In the following, we assume that \Coq~ is called from a standard +teletype-like shell window. All examples preceded by the prompting +sequence \verb:Coq < : represent user input, terminated by a +period. + +The following lines usually show \Coq's answer as it appears on the +users screen. When used from a graphical user interface such as +CoqIde, the prompt is not displayed: user input is given in one window +and \Coq's answers are displayed in a different window. + +The sequence of such examples is a valid \Coq~ +session, unless otherwise specified. This version of the tutorial has +been prepared on a PC workstation running Linux. The standard +invocation of \Coq\ delivers a message such as: \begin{small} \begin{flushleft} @@ -1552,4 +1561,4 @@ with \Coq, in order to acquaint yourself with various proof techniques. \end{document} -% $Id: Tutorial.tex 8715 2006-04-14 12:43:23Z cpaulin $ +% $Id: Tutorial.tex 8978 2006-06-23 10:15:57Z herbelin $ |