diff options
-rwxr-xr-x | doc/common/macros.tex | 1 | ||||
-rw-r--r-- | doc/refman/RefMan-tac.tex | 200 |
2 files changed, 122 insertions, 79 deletions
diff --git a/doc/common/macros.tex b/doc/common/macros.tex index b21e0e9e2..2704a28af 100755 --- a/doc/common/macros.tex +++ b/doc/common/macros.tex @@ -140,6 +140,7 @@ \newcommand{\idparams}{\nterm{ident\_with\_params}} \newcommand{\statkwd}{\nterm{assertion\_keyword}} % vernac \newcommand{\termarg}{\nterm{arg}} +\newcommand{\hintdef}{\nterm{hint\_definition}} \newcommand{\typecstr}{\zeroone{{\tt :}~{\term}}} \newcommand{\typecstrwithoutblank}{\zeroone{{\tt :}{\term}}} diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 72b5593e9..dce35c6d9 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -2528,21 +2528,25 @@ solved by unification, and some of the types \texttt{A}$_1$, \dots, \begin{ErrMsgs} \item \errindex{The term provided does not end with an equation} -\item \errindex{Tactic generated a subgoal identical to the original goal}\\ +\item \errindex{Tactic generated a subgoal identical to the original goal} + This happens if \term$_1$ does not occur in the goal. \end{ErrMsgs} \begin{Variants} -\item {\tt rewrite -> {\term}}\tacindex{rewrite ->}\\ +\item {\tt rewrite -> \term}\tacindex{rewrite ->} + Is equivalent to {\tt rewrite \term} -\item {\tt rewrite <- {\term}}\tacindex{rewrite <-}\\ +\item {\tt rewrite <- \term}\tacindex{rewrite <-} + Uses the equality \term$_1${\tt=}\term$_2$ from right to left -\item {\tt rewrite {\term} in \textit{clause}} - \tacindex{rewrite \dots\ in}\\ +\item {\tt rewrite {\term} in \nterm{clause}} + \tacindex{rewrite \dots\ in} + Analogous to {\tt rewrite {\term}} but rewriting is done following - \textit{clause} (similarly to \ref{Conversion-tactics}). For + \nterm{clause} (similarly to \ref{Conversion-tactics}). For instance: \begin{itemize} \item \texttt{rewrite H in H1} will rewrite \texttt{H} in the hypothesis @@ -2575,12 +2579,13 @@ This happens if \term$_1$ does not occur in the goal. Use {\tac} to completely solve the side-conditions arising from the rewrite. -\item {\tt rewrite} $\term_1${\tt ,} {\ldots}{\tt ,} $\term_n$\\ +\item {\tt rewrite \term$_1$ , \mbox{\dots} , \term$_n$} + Is equivalent to the $n$ successive tactics {\tt rewrite $\term_1$} up to {\tt rewrite $\term_n$}, each one working on the first subgoal generated by the previous one. Orientation {\tt ->} or {\tt <-} can be - inserted before each term to rewrite. One unique \textit{clause} + inserted before each term to rewrite. One unique \nterm{clause} can be added at the end after the keyword {\tt in}; it will then affect all rewrite operations. @@ -2631,25 +2636,39 @@ n}| assumption || symmetry; try assumption]}. \end{ErrMsgs} \begin{Variants} -\item {\tt replace {\term$_1$} with {\term$_2$} by \tac}\\ This acts - as {\tt replace {\term$_1$} with {\term$_2$}} but applies {\tt \tac} + +\item {\tt replace \term$_1$ with \term$_2$ by \tac} + + This acts as {\tt replace \term$_1$ with \term$_2$} but applies {\tt \tac} to solve the generated subgoal {\tt \term$_2$=\term$_1$}. -\item {\tt replace {\term}}\\ Replace {\term} with {\term'} using the + +\item {\tt replace {\term}} + + Replaces {\term} with {\term'} using the first assumption whose type has the form {\tt \term=\term'} or {\tt - \term'=\term} -\item {\tt replace -> {\term}}\\ Replace {\term} with {\term'} using the + \term'=\term}. + +\item {\tt replace -> {\term}} + + Replaces {\term} with {\term'} using the first assumption whose type has the form {\tt \term=\term'} -\item {\tt replace <- {\term}}\\ Replace {\term} with {\term'} using the + +\item {\tt replace <- {\term}} + + Replaces {\term} with {\term'} using the first assumption whose type has the form {\tt \term'=\term} -\item {\tt replace {\term$_1$} with {\term$_2$} \textit{clause} }\\ - {\tt replace {\term$_1$} with {\term$_2$} \textit{clause} by \tac }\\ - {\tt replace {\term} \textit{clause}}\\ - {\tt replace -> {\term} \textit{clause}}\\ - {\tt replace <- {\term} \textit{clause}}\\ - Act as before but the replacements take place in - \textit{clause}~(see Section~\ref{Conversion-tactics}) and not only - in the conclusion of the goal.\\ - The \textit{clause} argument must not contain any \texttt{type of} nor \texttt{value of}. + +\item {\tt replace {\term$_1$} with {\term$_2$} in \nterm{clause} }\\ + {\tt replace {\term$_1$} with {\term$_2$} in \nterm{clause} by \tac }\\ + {\tt replace {\term} in \nterm{clause}}\\ + {\tt replace -> {\term} in \nterm{clause}}\\ + {\tt replace <- {\term} in \nterm{clause}} + + Acts as before but the replacements take place in + \nterm{clause}~(see Section~\ref{Conversion-tactics}) and not only + in the conclusion of the goal. + The \nterm{clause} argument must not contain any \texttt{type of} nor \texttt{value of}. + \end{Variants} \subsection{\tt reflexivity} @@ -2668,10 +2687,12 @@ It is equivalent to {\tt apply refl\_equal}. \subsection{\tt symmetry} \tacindex{symmetry} \tacindex{symmetry in} + This tactic applies to a goal which has the form {\tt t=u} and changes it into {\tt u=t}. -\variant {\tt symmetry in {\ident}}\\ +\variant {\tt symmetry in {\ident}} + If the statement of the hypothesis {\ident} has the form {\tt t=u}, the tactic changes it to {\tt u=t}. @@ -2695,9 +2716,11 @@ When several hypotheses have the form {\tt \ident=t} or {\tt t=\ident}, the first one is used. \begin{Variants} - \item {\tt subst \ident$_1$ \dots \ident$_n$} \\ + \item {\tt subst \ident$_1$ \dots \ident$_n$} + Is equivalent to {\tt subst \ident$_1$; \dots; subst \ident$_n$}. - \item {\tt subst} \\ + \item {\tt subst} + Applies {\tt subst} repeatedly to all identifiers from the context for which an equality exists. \end{Variants} @@ -2726,11 +2749,13 @@ accepted as regular setoids for {\tt rewrite} and {\tt \tacindex{stepr} \comindex{Declare Right Step} \begin{Variants} -\item{\tt stepl {\term} by {\tac}}\\ +\item{\tt stepl {\term} by {\tac}} + This applies {\tt stepl {\term}} then applies {\tac} to the second goal. \item{\tt stepr {\term}}\\ - {\tt stepr {\term} by {\tac}}\\ + {\tt stepr {\term} by {\tac}} + This behaves as {\tt stepl} but on the right-hand-side of the binary relation. Lemmas are expected to be of the form ``{\tt forall} $x$ $y$ @@ -3145,7 +3170,7 @@ x}$)$) $t$}. This command can be used, for instance, when the tactic Starting from a goal $\phi(t_1 \dots\ t_m)$, the tactic {\tt pattern $t_1$, \dots,\ $t_m$} generates the equivalent goal {\tt (fun (x$_1$:$A_1$) \dots\ (x$_m$:$A_m$) => $\phi(${\tt x$_1$\dots\ - x$_m$}$)$) $t_1$ \dots\ $t_m$}.\\ If $t_i$ occurs in one of the + x$_m$}$)$) $t_1$ \dots\ $t_m$}. If $t_i$ occurs in one of the generated types $A_j$ these occurrences will also be considered and possibly abstracted. @@ -3277,9 +3302,9 @@ This tactic unfolds constants that were declared through a {\tt Hint Unfold} in the given databases. \begin{Variants} -\item {\tt autounfold with \ident$_1$ \dots\ \ident$_n$ in \textit{clause}} +\item {\tt autounfold with \ident$_1$ \dots\ \ident$_n$ in \nterm{clause}} - Perform the unfolding in the given clause. + Performs the unfolding in the given clause. \item {\tt autounfold with *} @@ -3311,21 +3336,24 @@ command. \Warning{} This tactic may loop if you build non terminating rewriting systems. \begin{Variant} -\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 with \ident$_1$ \mbox{\dots} \ident$_n$ using \tac} -\item \texttt{autorewrite with {\ident$_1$} \dots \ident$_n$ in {\qualid}} +Performs, in the same way, all the rewritings of the bases {\tt \ident$_1$ +\mbox{\dots} \ident$_n$} applying {\tt \tac} to the main subgoal after each +rewriting step. + +\item {\tt autorewrite with \ident$_1$ \mbox{\dots} \ident$_n$ in \qualid} Performs all the rewritings in hypothesis {\qualid}. -\item \texttt{autorewrite with {\ident$_1$} \dots \ident$_n$ in {\qualid} using \tac} +\item {\tt autorewrite with \ident$_1$ \mbox{\dots} \ident$_n$ in {\qualid} using \tac} Performs all the rewritings in hypothesis {\qualid} applying {\tt \tac} to the main subgoal after each rewriting step. -\item \texttt{autorewrite with {\ident$_1$} \dots \ident$_n$ in \textit{clause}} - Performs all the rewritings in the clause \textit{clause}. \\ - The \textit{clause} argument must not contain any \texttt{type of} nor \texttt{value of}. +\item {\tt autorewrite with \ident$_1$ \mbox{\dots} \ident$_n$ in \nterm{clause}} + + Performs all the rewriting in the clause \nterm{clause}. + The \nterm{clause} argument must not contain any \texttt{type of} nor \texttt{value of}. \end{Variant} @@ -3381,35 +3409,34 @@ inserted, making this implementation observationally different from the legacy one. The general -command to add a hint to some database \ident$_1$, \dots, \ident$_n$ is +command to add a hint to some databases \ident$_1$, \dots, \ident$_n$ is \begin{tabbing} - \texttt{Hint} \textsl{hint\_definition} \texttt{:} \ident$_1$ {\ldots} \ident$_n$ + {\tt Hint {\hintdef} :~\ident$_1$ \mbox{\dots} \ident$_n$} \end{tabbing} \begin{Variants} -\item \texttt{Hint} \textsl{hint\_definition} +\item {\tt Hint \hintdef} No database name is given: the hint is registered in the {\tt core} database. -\item\texttt{Local Hint} \textsl{hint\_definition} \texttt{:} - \ident$_1$ \ldots\ \ident$_n$ +\item {\tt Local Hint {\hintdef} :~\ident$_1$ \mbox{\dots} \ident$_n$} This is used to declare hints that must not be exported to the other modules that require and import the current module. Inside a section, the option {\tt Local} is useless since hints do not survive anyway to the closure of sections. -\item\texttt{Local Hint} \textsl{hint\_definition} +\item {\tt Local Hint \hintdef} Idem for the {\tt core} database. \end{Variants} -The \textsl{hint\_definition} is one of the following expressions: +The \hintdef is one of the following expressions: \begin{itemize} -\item \texttt{Resolve} {\term} +\item {\tt Resolve \term} \comindex{Hint Resolve} This command adds {\tt apply {\term}} to the hint list @@ -3444,7 +3471,7 @@ The \textsl{hint\_definition} is one of the following expressions: \begin{Variants} - \item \texttt{Resolve} {\term$_1$} \dots {\term$_m$} + \item {\tt Resolve \term$_1$ \mbox{\dots} \term$_m$} Adds each \texttt{Resolve} {\term$_i$}. @@ -3476,7 +3503,7 @@ The \textsl{hint\_definition} is one of the following expressions: \begin{Variants} - \item \texttt{Immediate} {\term$_1$} \dots {\term$_m$} + \item {\tt Immediate \term$_1$ \mbox{\dots} \term$_m$} Adds each \texttt{Immediate} {\term$_i$}. @@ -3500,7 +3527,7 @@ The \textsl{hint\_definition} is one of the following expressions: \begin{Variants} - \item \texttt{Constructors} {\ident$_1$} \dots {\ident$_m$} + \item {\tt Constructors \ident$_1$ \mbox{\dots} \ident$_m$} Adds each \texttt{Constructors} {\ident$_i$}. @@ -3515,7 +3542,7 @@ The \textsl{hint\_definition} is one of the following expressions: \begin{Variants} - \item \texttt{Unfold} {\ident$_1$} \dots {\ident$_m$} + \item {\tt Unfold \ident$_1$ \mbox{\dots} \ident$_m$} Adds each \texttt{Unfold} {\ident$_i$}. @@ -3534,7 +3561,7 @@ The \textsl{hint\_definition} is one of the following expressions: \begin{Variants} - \item \texttt{Transparent}, \texttt{Opaque} {\ident$_1$} \dots {\ident$_m$} + \item \texttt{Transparent}, \texttt{Opaque} {\ident$_1$} \mbox{\dots} {\ident$_m$} Declares each {\ident$_i$} as a transparent or opaque constant. @@ -3583,20 +3610,19 @@ pattern-matching on hypotheses using \texttt{match goal with} inside the tactic. \begin{Variants} -\item \texttt{Hint} \textsl{hint\_definition} +\item {\tt Hint \hintdef} No database name is given: the hint is registered in the {\tt core} database. -\item\texttt{Hint Local} \textsl{hint\_definition} \texttt{:} - \ident$_1$ \ldots\ \ident$_n$ +\item {\tt Hint Local {\hintdef} : \ident$_1$ \mbox{\dots} \ident$_n$} This is used to declare hints that must not be exported to the other modules that require and import the current module. Inside a section, the option {\tt Local} is useless since hints do not survive anyway to the closure of sections. -\item\texttt{Hint Local} \textsl{hint\_definition} +\item {\tt Hint Local \hintdef} Idem for the {\tt core} database. @@ -3689,7 +3715,7 @@ every moment. \begin{Variants} -\item {\tt Print Hint {\ident} } +\item {\tt Print Hint \ident} This command displays only tactics associated with \ident\ in the hints list. This is independent of the goal being edited, so this @@ -3699,7 +3725,7 @@ every moment. This command displays all declared hints. -\item {\tt Print HintDb {\ident} } +\item {\tt Print HintDb \ident} \label{PrintHintDb} \comindex{Print HintDb} @@ -3707,11 +3733,11 @@ every moment. \end{Variants} -\subsection{\tt Hint Rewrite \term$_1$ \mbox{\dots} \term$_n$ : \ident} +\subsection{\tt Hint Rewrite \term$_1$ \mbox{\dots} \term$_n$ :~\ident} \label{HintRewrite} \comindex{Hint Rewrite} -This vernacular command adds the terms {\tt \term$_1$ \dots \term$_n$} +This vernacular command adds the terms {\tt \term$_1$ \mbox{\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 @@ -3723,16 +3749,19 @@ 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}\\ +\item {\tt Hint Rewrite -> \term$_1$ \mbox{\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 +\item {\tt Hint Rewrite <- \term$_1$ \mbox{\dots} \term$_n$ :~\ident} + +Adds the rewriting rules {\tt \term$_1$ \mbox{\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 +\item {\tt Hint Rewrite \term$_1$ \mbox{\dots} \term$_n$ using {\tac} :~\ident} + +When the rewriting rules {\tt \term$_1$ \mbox{\dots} \term$_n$} in {\tt \ident} will be used, the tactic {\tt \tac} will be applied to the generated subgoals, the main subgoal excluded. @@ -3760,8 +3789,9 @@ e.g. \texttt{Require Import A.}). \subsection{Setting implicit automation tactics} -\subsubsection[\tt Proof with {\tac}.]{\tt Proof with {\tac}.\label{ProofWith} -\comindex{Proof with}} +\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 @@ -3771,16 +3801,17 @@ e.g. \texttt{Require Import A.}). \SeeAlso {\tt Proof.} in Section~\ref{BeginProof}. \begin{Variants} -\item {\tt Proof with {\tac} using {\ident$_1$ \dots {\ident$_n$}}} +\item {\tt Proof with {\tac} using \ident$_1$ \mbox{\dots} \ident$_n$} Combines in a single line {\tt Proof with} and {\tt Proof using}, see~\ref{ProofUsing} -\item {\tt Proof using {\ident$_1$ \dots {\ident$_n$}} with {\tac}} +\item {\tt Proof using \ident$_1$ \mbox{\dots} \ident$_n$ with {\tac}} Combines in a single line {\tt Proof with} and {\tt Proof using}, see~\ref{ProofUsing} \end{Variants} -\subsubsection[\tt Declare Implicit Tactic {\tac}.]{\tt Declare Implicit Tactic {\tac}.\comindex{Declare Implicit Tactic}} +\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 @@ -3885,7 +3916,8 @@ slightly changed to get clearer semantics. This may lead to some incompatibilities. \begin{Variants} -\item {\tt intuition}\\ +\item {\tt intuition} + Is equivalent to {\tt intuition auto with *}. \end{Variants} @@ -3984,26 +4016,33 @@ congruence. \end{coq_example} \begin{Variants} - \item {\tt congruence {\sl n}}\\ + \item {\tt congruence {\sl n}} + Tries to add at most {\tt \sl n} instances of hypotheses stating quantified equalities to the problem in order to solve it. A bigger value of {\tt \sl n} does not make success slower, only failure. You might consider adding some lemmas as hypotheses using {\tt assert} in order for congruence to use them. \end{Variants} \begin{Variants} -\item {\tt congruence with \term$_1$ \dots\ \term$_n$}\\ +\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} \\ + \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} \\ + + \item \errindex{I couldn't solve goal} + 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.} \\ + + \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 @@ -4203,7 +4242,8 @@ and inversion tactics. \begin{Variants} \item{\tt dependent rewrite <- {\ident}} -\tacindex{dependent rewrite <-} \\ +\tacindex{dependent rewrite <-} + Analogous to {\tt dependent rewrite ->} but uses the equality from right to left. \end{Variants} @@ -4257,12 +4297,14 @@ convertibility. In other words, it does inversion of the function datatype: see~\ref{quote-examples} for the full details. \begin{ErrMsgs} -\item \errindex{quote: not a simple fixpoint}\\ +\item \errindex{quote: not a simple fixpoint} + Happens when \texttt{quote} is not able to perform inversion properly. \end{ErrMsgs} \begin{Variants} -\item \texttt{quote {\ident} [ \ident$_1$ \dots \ident$_n$ ]}\\ +\item \texttt{quote {\ident} [ \ident$_1$ \dots \ident$_n$ ]} + All terms that are built only with \ident$_1$ \dots \ident$_n$ will be considered by \texttt{quote} as constants rather than variables. \end{Variants} |