diff options
Diffstat (limited to 'doc/refman/RefMan-tac.tex')
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 56 |
1 files changed, 28 insertions, 28 deletions
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 335cc3f15..6276b547b 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -33,7 +33,7 @@ satisfied. If it is not the case, the tactic raises an error message. Tactics are build from atomic tactics and tactic expressions (which extends the folklore notion of tactical) to combine those atomic tactics. This chapter is devoted to atomic tactics. The tactic -language will be described in chapter~\ref{TacticLanguage}. +language will be described in Chapter~\ref{TacticLanguage}. There are, at least, three levels of atomic tactics. The simplest one implements basic rules of the logical framework. The second level is @@ -98,7 +98,7 @@ holes. The holes are noted ``\texttt{\_}''. which type cannot be inferred. Put a cast around it. \end{ErrMsgs} -An example of use is given in section~\ref{refine-example}. +An example of use is given in Section~\ref{refine-example}. \section{Basics \index{Typing rules}} @@ -348,7 +348,7 @@ match the current goal against the conclusion of the type of {\term}. If it succeeds, then the tactic returns as many subgoals as the number of non dependent premises of the type of {\term}. The tactic {\tt apply} relies on first-order pattern-matching with dependent -types. See {\tt pattern} in section \ref{pattern} to transform a +types. See {\tt pattern} in Section~\ref{pattern} to transform a second-order pattern-matching problem into a first-order one. \begin{ErrMsgs} @@ -581,7 +581,7 @@ in the list of subgoals remaining to prove. % \vref$_n$ := \term$_n$} % \tacindex{Specialize \dots\ with} \\ % It is to provide the tactic with some explicit values to instantiate -% premises of {\term} (see section \ref{Binding-list}). +% premises of {\term} (see Section~\ref{Binding-list}). % Some other premises are inferred using type information and % unification. The resulting well-formed % term being {\tt (\term~\term'$_1$\dots\term'$_k$)} @@ -685,7 +685,7 @@ to $T$. \label{change}} This tactic applies to any goal. It implements the rule -``Conv''\index{Typing rules!Conv} given in section~\ref{Conv}. {\tt +``Conv''\index{Typing rules!Conv} given in Section~\ref{Conv}. {\tt change U} replaces the current goal \T\ with \U\ providing that \U\ is well-formed and that \T\ and \U\ are convertible. @@ -739,7 +739,7 @@ product {\tt \ident$_i$:T} (for some type \T); if \vref$_i$ is A bindings list can also be a simple list of terms {\tt \term$_1$ \term$_2$ \dots\term$_n$}. In that case the references to which these terms correspond are determined by the tactic. In case of {\tt - elim} (see section~\ref{elim}) the terms should correspond to + elim} (see Section~\ref{elim}) the terms should correspond to all the dependent products in the type of \term\ while in the case of {\tt apply} only the dependent products which are not bound in the conclusion of the type are given. @@ -943,7 +943,7 @@ product or an applicative term in head normal form or a variable. The term \verb+forall n:nat, (plus (S n) (S n))+ is not reduced by {\tt hnf}. \Rem The $\delta$ rule only applies to transparent constants -(see section~\ref{Opaque} on transparency and opacity). +(see Section~\ref{Opaque} on transparency and opacity). \subsection{\tt simpl \tacindex{simpl}} @@ -1575,7 +1575,7 @@ Qed. \item {\tt decompose record \term}\tacindex{decompose record} This decomposes record types (inductive types with one constructor, like \texttt{and} and \texttt{exists} and those defined with the - \texttt{Record} macro, see p.~\pageref{Record}). + \texttt{Record} macro, see Section~\ref{Record}). \end{Variants} @@ -1586,8 +1586,8 @@ Qed. The \emph{experimental} tactic \texttt{functional induction} performs case analysis and induction following the definition of a function. It makes use of a principle generated by \texttt{Function} -(section~\ref{Function}) or \texttt{Functional Scheme} -(section~\ref{FunScheme}). +(see Section~\ref{Function}) or \texttt{Functional Scheme} +(see Section~\ref{FunScheme}). \begin{coq_eval} Reset Initial. @@ -1613,15 +1613,15 @@ you want to write implicit arguments explicitly. \Rem \texttt{functional induction (f x1 x2 x3)} is actually a wrapper for \texttt{induction x1 x2 x3 (f x1 x2 x3) using \qualid} followed by a cleaning phase, where $\qualid$ is the induction principle -registered for $f$ (by the \texttt{Function} (section~\ref{Function}) -or \texttt{Functional Scheme} (section~\ref{FunScheme}) command) +registered for $f$ (by the \texttt{Function} (see Section~\ref{Function}) +or \texttt{Functional Scheme} (see Section~\ref{FunScheme}) command) corresponding to the sort of the goal. Therefore \texttt{functional induction} may fail if the induction scheme (\texttt{\qualid}) is -not defined. See also section~\ref{Function} for the function terms +not defined. See also Section~\ref{Function} for the function terms accepted by \texttt{Function}. \Rem There is a difference between obtaining an induction scheme for a -function by using \texttt{Function} (section~\ref{Function}) and by +function by using \texttt{Function} (see Section~\ref{Function}) and by using \texttt{Functional Scheme} after a normal definition using \texttt{Fixpoint} or \texttt{Definition}. See \ref{Function} for details. @@ -1642,7 +1642,7 @@ details. using \term$_{m+1}$ with {\term$_{n+1}$} \dots {\term$_m$}} Similar to \texttt{Induction} and \texttt{elim} - (section~\ref{Tac-induction}), allows to give explicitly the + (see Section~\ref{Tac-induction}), allows to give explicitly the induction principle and the values of dependent premises of the elimination scheme, including \emph{predicates} for mutual induction when \qualid is mutually recursive. @@ -1652,11 +1652,11 @@ details. {\vref$_m$} := {\term$_n$}} Similar to \texttt{induction} and \texttt{elim} - (section~\ref{Tac-induction}). + (see Section~\ref{Tac-induction}). \item All previous variants can be extended by the usual \texttt{as \intropattern} construction, similarly for example to - \texttt{induction} and \texttt{elim} (section~\ref{Tac-induction}). + \texttt{induction} and \texttt{elim} (see Section~\ref{Tac-induction}). \end{Variants} @@ -1857,7 +1857,7 @@ Lemmas are added to the database using the command 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}). + setoid\_replace} (see Chapter~\ref{setoid_replace}). \tacindex{stepr} \comindex{Declare Right Step} @@ -2350,7 +2350,7 @@ the instance with the tactic {\tt inversion}. which performs inversion on hypothesis \ident\ of the form \texttt{\qualid\ \term$_1$\dots\term$_n$\ = \term} or \texttt{\term\ = \qualid\ \term$_1$\dots\term$_n$} where \qualid\ must have been -defined using \texttt{Function} (section~\ref{Function}). +defined using \texttt{Function} (see Section~\ref{Function}). \begin{ErrMsgs} \item \errindex{Hypothesis \ident must contain at least one Function} @@ -2590,7 +2590,7 @@ and then uses {\tt auto} which completes the proof. Originally due to C{\'e}sar~Mu{\~n}oz, these tactics ({\tt tauto} and {\tt intuition}) have been completely reengineered by David~Delahaye using mainly the tactic -language (see chapter~\ref{TacticLanguage}). The code is now quite shorter and +language (see Chapter~\ref{TacticLanguage}). The code is now quite shorter and a significant increase in performances has been noticed. The general behavior with respect to dependent types, unfolding and introductions has slightly changed to get clearer semantics. This may lead to some @@ -2742,7 +2742,7 @@ vernacular command. % \item {\tt Linear with \ident$_1$ \dots\ \ident$_n$}\\ % \tacindex{Linear with} % Is equivalent to apply first {\tt generalize \ident$_1$ \dots -% \ident$_n$} (see section \ref{generalize}) then the \texttt{Linear} +% \ident$_n$} (see Section~\ref{generalize}) then the \texttt{Linear} % tactic. So one can use axioms, lemmas or hypotheses of the local % context with \texttt{Linear} in this way. % \end{Variants} @@ -2840,7 +2840,7 @@ formulas built with \verb|~|, \verb|\/|, \verb|/\|, both the type \texttt{nat} of natural numbers and \texttt{Z} of binary integers. This tactic must be loaded by the command \texttt{Require Import Omega}. See the additional documentation about \texttt{omega} -(chapter~\ref{OmegaChapter}). +(see Chapter~\ref{OmegaChapter}). \subsection{{\tt ring} and {\tt ring\_simplify \term$_1$ \dots\ \term$_n$} \tacindex{ring} @@ -2859,7 +2859,7 @@ the terms given in the conclusion of the goal by their normal forms. If no term is given, then the conclusion should be an equation and both hand sides are normalized. -See chapter~\ref{ring} for more information on the tactic and how to +See Chapter~\ref{ring} for more information on the tactic and how to declare new ring structures. \subsection{{\tt field}, {\tt field\_simplify \term$_1$\dots\ \term$_n$} @@ -2885,7 +2885,7 @@ division nor inverse. All of these 3 tactics may generate a subgoal in order to prove that denominators are different from zero. -See chapter~\ref{ring} for more information on the tactic and how to +See Chapter~\ref{ring} for more information on the tactic and how to declare new field structures. \Example @@ -2973,9 +2973,9 @@ $ident_n$} applying {\tt \tac} to the main subgoal after each rewriting step. \end{Variant} -\SeeAlso section \ref{HintRewrite} for feeding the database of lemmas used by {\tt autorewrite}. +\SeeAlso Section~\ref{HintRewrite} for feeding the database of lemmas used by {\tt autorewrite}. -\SeeAlso section \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 @@ -3336,7 +3336,7 @@ e.g. \texttt{Require Import A.}). ``\verb#...#''. In this case the tactic command typed by the user is equivalent to \tac$_1$;{\tac}. -\SeeAlso {\tt Proof.} in section~\ref{BeginProof}. +\SeeAlso {\tt Proof.} in Section~\ref{BeginProof}. \subsubsection[\tt Declare Implicit Tactic {\tac}.]{\tt Declare Implicit Tactic {\tac}.\comindex{Declare Implicit Tactic}} @@ -3480,7 +3480,7 @@ where it was defined. If you want that a tactic macro defined in a module is usable in the modules that require it, you should put it outside of any section. -The chapter~\ref{TacticLanguage} gives examples of more complex +Chapter~\ref{TacticLanguage} gives examples of more complex user-defined tactics. |