diff options
Diffstat (limited to 'doc/refman/RefMan-tac.tex')
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 389 |
1 files changed, 238 insertions, 151 deletions
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 24699873..24ea78c0 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -120,6 +120,7 @@ subgoal is proved. Otherwise, it fails. \end{ErrMsgs} \begin{Variants} +\tacindex{eassumption} \item \texttt{eassumption} This tactic behaves like \texttt{assumption} but is able to handle @@ -576,6 +577,45 @@ in the list of subgoals remaining to prove. % \term\ will be kept. %\end{Variants} +\subsection{{\tt apply {\term} in {\ident}} +\tacindex{apply {\ldots} in}} + +This tactic applies to any goal. The argument {\term} is a term +well-formed in the local context and the argument {\ident} is an +hypothesis of the context. The tactic {\tt apply {\term} in {\ident}} +tries to match the conclusion of the type of {\ident} against a non +dependent premisses of the type of {\term}, trying them from right to +left. If it succeeds, the statement of hypothesis {\ident} is +replaced by the conclusion of the type of {\ident}. The tactic also +returns as many subgoals as the number of other non dependent premises +in the type of {\term} and of the non dependent premises of the type +of {\ident}. The tactic {\tt apply} relies on first-order +pattern-matching with dependent types. + +\begin{ErrMsgs} +\item \errindex{Statement without assumptions} + +This happens if the type of {\term} has no non dependent premise. + +\item \errindex{Unable to apply} + +This happens if the conclusion of {\ident} does not match any of the +non dependent premises of the type of {\term}. +\end{ErrMsgs} + +\begin{Variants} +\item {\tt apply \nelist{\term}{,} in {\ident}} + +This applies each of {\term} in sequence in {\ident}. + +\item {\tt apply \nelist{{\term} {\bindinglist}}{,} in {\ident}} + +This does the same but uses the bindings in each {\bindinglist} to +instanciate the parameters of the corresponding type of {\term} +(see syntax of bindings in Section~\ref{Binding-list}). + +\end{Variants} + \subsection{\tt generalize \term \tacindex{generalize} \label{generalize}} @@ -725,11 +765,12 @@ can be either the conclusion, or an hypothesis. In the case of a defined hypothesis it is possible to specify if the conversion should occur on the type part, the body part or both (default). -\index{Clauses} -Clauses are written after a conversion tactic (tactic -\texttt{set}~\ref{tactic:set} also uses clauses) and are introduced by -the keyword \texttt{in}. If no clause is provided, the default is to -perform the conversion only in the conclusion. +\index{Clauses} Clauses are written after a conversion tactic (tactics +\texttt{set}~\ref{tactic:set}, \texttt{rewrite}~\ref{rewrite}, +\texttt{replace}~\ref{tactic:replace} and +\texttt{autorewrite}~\ref{tactic:autorewrite} also use clauses) and +are introduced by the keyword \texttt{in}. If no clause is provided, +the default is to perform the conversion only in the conclusion. The syntax and description of the various clauses follows: \begin{description} @@ -754,7 +795,8 @@ performs the conversion in hypotheses $H_1\ldots H_n$. \dots\ \flag$_n$} and {\tt compute} \tacindex{cbv} \tacindex{lazy} -\tacindex{compute}} +\tacindex{compute} +\tacindex{vm\_compute}} \label{vmcompute} These parameterized reduction tactics apply to any goal and perform @@ -773,9 +815,7 @@ followed by {\tt [\qualid$_1$\ldots\qualid$_k$]} or {\tt -[\qualid$_1$\ldots\qualid$_k$]}), the {\tt delta} flag means that all constants must be unfolded. However, the {\tt delta} flag does not apply to variables bound by a let-in construction whose unfolding is controlled by the {\tt - zeta} flag only. In addition, there is a flag {\tt Evar} to perform -instantiation of existential variables (``?'') when an instantiation -actually exists. + zeta} flag only. The goal may be normalized with two strategies: {\em lazy} ({\tt lazy} tactic), or {\em call-by-value} ({\tt cbv} tactic). The lazy strategy @@ -798,7 +838,7 @@ computational expressions (i.e. with few dead code). \begin{Variants} \item {\tt compute} \tacindex{compute} - This tactic is an alias for {\tt cbv beta delta evar iota zeta}. + This tactic is an alias for {\tt cbv beta delta iota zeta}. \item {\tt vm\_compute} \tacindex{vm\_compute} @@ -1453,7 +1493,7 @@ Qed. \end{Variants} -\subsection{\tt functional induction (\ident\ \term$_1$ \dots\ \term$_n$). +\subsection{\tt functional induction (\qualid\ \term$_1$ \dots\ \term$_n$). \tacindex{functional induction} \label{FunInduction}} @@ -1461,8 +1501,7 @@ 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}). This principle is named \ident\_ind by -default but you can give it explicitly, see variants below. +(section~\ref{FunScheme}). \begin{coq_eval} Reset Initial. @@ -1478,22 +1517,22 @@ functional induction (minus n m); simpl; auto. Qed. \end{coq_example*} -\Rem \texttt{(\ident\ \term$_1$ \dots\ \term$_n$)} must be a correct -full application of \ident. In particular, the rules for implicit -arguments are the same as usual. For example use \texttt{@\ident} if +\Rem \texttt{(\qualid\ \term$_1$ \dots\ \term$_n$)} must be a correct +full application of \qualid. In particular, the rules for implicit +arguments are the same as usual. For example use \texttt{@\qualid} if you want to write implicit arguments explicitly. -\Rem Parenthesis over \ident \dots \term$_n$ are not mandatory, but if -there are not written then implicit arguments must be given. +\Rem Parenthesis over \qualid \dots \term$_n$ are mandatory. -\Rem \texttt{functional induction (f x1 x2 x3)} is actually a -shorthand for \texttt{induction x1 x2 x3 (f x1 x2 x3) using f\_ind}. -\texttt{f\_ind} being an induction scheme computed by the -\texttt{Function} (section~\ref{Function}) or \texttt{Functional - Scheme} (section~\ref{FunScheme}) command . Therefore -\texttt{functional induction} may fail if the induction scheme -(\texttt{f\_ind}) is not defined. See also section~\ref{Function} for -the function terms accepted by \texttt{Function}. +\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) +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 +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 @@ -1501,36 +1540,42 @@ using \texttt{Functional Scheme} after a normal definition using \texttt{Fixpoint} or \texttt{Definition}. See \ref{Function} for details. -\SeeAlso{\ref{Function},\ref{FunScheme},\ref{FunScheme-examples}} +\SeeAlso{\ref{Function},\ref{FunScheme},\ref{FunScheme-examples}, + \ref{sec:functional-inversion}} -\ErrMsg - -\errindex{The reference \ident\_ind was not found in the current -environment} +\begin{ErrMsgs} +\item \errindex{Cannot find induction information on \qualid} -~ + ~ -\errindex{Not the right number of induction arguments} - +\item \errindex{Not the right number of induction arguments} +\end{ErrMsgs} \begin{Variants} -\item {\tt functional induction (\ident\ \term$_1$ \dots\ \term$_n$) +\item {\tt functional induction (\qualid\ \term$_1$ \dots\ \term$_n$) 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 induction principle and the values of dependent premises of the elimination scheme, including \emph{predicates} for mutual induction - when \ident is mutually recursive. + when \qualid is mutually recursive. -\item {\tt functional induction (\ident\ \term$_1$ \dots\ \term$_n$) +\item {\tt functional induction (\qualid\ \term$_1$ \dots\ \term$_n$) using \term$_{m+1}$ with {\vref$_1$} := {\term$_{n+1}$} \dots\ {\vref$_m$} := {\term$_n$}} Similar to \texttt{induction} and \texttt{elim} (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}). + \end{Variants} + + \section{Equality} These tactics use the equality {\tt eq:forall A:Type, A->A->Prop} @@ -1578,20 +1623,30 @@ This happens if \term$_1$ does not occur in the goal. \item {\tt rewrite {\term} in \textit{clause}} \tacindex{rewrite \dots\ in}\\ 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}} + \textit{clause} (similarly to \ref{Conversion-tactics}). For + instance: + \begin{itemize} + \item \texttt{rewrite H in H1} will rewrites \texttt{H} in the hypothesis + \texttt{H1} instead of the current goal. + \item \texttt{rewrite H in H1,H2 |- *} means \texttt{rewrite H; rewrite H in H1; + rewrite H in H2}. In particular a failure will happen if any of + these three simplier tactics fails. + \item \texttt{rewrite H in * |- } will do \texttt{rewrite H in + H$_i$} for all hypothesis \texttt{H$_i$ <> H}. A success will happen + as soon as at least one of these simplier tactics succeeds. + \item \texttt{rewrite H in *} is a combination of \texttt{rewrite H} + and \texttt{rewrite H in * |-} that succeeds if at + least one of these two tactics succeeds. + \end{itemize} + +\item {\tt rewrite -> {\term} in \textit{clause}} \tacindex{rewrite -> \dots\ in}\\ - Behaves as {\tt rewrite {\term} in {\ident}}. + Behaves as {\tt rewrite {\term} in \textit{clause}}. -\item {\tt rewrite <- {\term} in {\ident}}\\ +\item {\tt rewrite <- {\term} in \textit{clause}}\\ \tacindex{rewrite <- \dots\ in} Uses the equality \term$_1${\tt=}\term$_2$ from right to left to - rewrite in the hypothesis named {\ident}. + rewrite in \textit{clause} as explained above. \end{Variants} @@ -1603,6 +1658,7 @@ This tactic acts like {\tt replace {\term$_1$} with {\term$_2$}} (see below). \subsection{\tt replace {\term$_1$} with {\term$_2$} +\label{tactic:replace} \tacindex{replace \dots\ with}} This tactic applies to any goal. It replaces all free occurrences of @@ -1618,21 +1674,23 @@ n}| assumption || symmetry; try assumption]}. \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} - -\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 +\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}. +\item {\tt replace {\term}}\\ Replace {\term} with {\term'} using the + first assumption which type has the form {\tt \term=\term'} or {\tt + \term'=\term} +\item {\tt replace -> {\term}}\\ Replace {\term} with {\term'} using the + first assumption which type has the form {\tt \term=\term'} +\item {\tt replace <- {\term}}\\ Replace {\term} with {\term'} using the + first assumption which 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}~\ref{Conversion-tactics} an not only in the conclusion of the goal.\\ + The \textit{clause} arg must not contain any \texttt{type of} nor \texttt{value of}. \end{Variants} \subsection{\tt reflexivity @@ -1709,7 +1767,7 @@ 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}{\sl n} by {\tac}}\\ This applies {\tt stepl {\term}} then applies {\tac} to the second goal. \item{\tt stepr {\term}}\\ @@ -1884,6 +1942,14 @@ introduced hypothesis. {\ident}}. \ErrMsg \errindex{goal does not satisfy the expected preconditions} + +\item \texttt{injection} \ident{} \texttt{as} \nelist{\intropattern}{}\\ +\texttt{injection} \num{} \texttt{as} {\intropattern} {\ldots} {\intropattern}\\ +\texttt{injection} \texttt{as} {\intropattern} {\ldots} {\intropattern}\\ +\tacindex{injection \ldots{} as} + +These variants apply \texttt{intros} \nelist{\intropattern}{} after the call to \texttt{injection}. + \end{Variants} \subsection{\tt simplify\_eq {\ident} @@ -2165,6 +2231,42 @@ the instance with the tactic {\tt inversion}. \SeeAlso \ref{inversion-examples} for examples + + +\subsection{\tt functional inversion \ident} +\label{sec:functional-inversion} + +\texttt{functional inversion} is a \emph{highly} experimental tactic +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}). + +\begin{ErrMsgs} +\item \errindex{Hypothesis \ident must contain at least one Function} +\item \errindex{Cannot find inversion information for hypothesis \ident} + This error may be raised when some inversion lemma failed to be + generated by Function. +\end{ErrMsgs} + +\begin{Variants} +\item {\tt functional inversion \num} + + This does the same thing as \texttt{intros until \num} then + \texttt{functional inversion \ident} where {\ident} is the + identifier for the last introduced hypothesis. +\item {\tt functional inversion \ident\ \qualid}\\ + {\tt functional inversion \num\ \qualid} + + In case the hypothesis \ident (or \num) has a type of the form + \texttt{\qualid$_1$\ \term$_1$\dots\term$_n$\ =\qualid$_2$\ + \term$_{n+1}$\dots\term$_{n+m}$} where \qualid$_1$ and \qualid$_2$ + are valid candidates to functional inversion, this variant allows to + chose which must be inverted. +\end{Variants} + + + \subsection{\tt quote \ident \tacindex{quote} \index{2-level approach}} @@ -2557,6 +2659,8 @@ 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. Alternatively, congruence tries to prove that an hypothesis is equal to the goal or to the negation of another hypothesis. +{\tt congruence} is also able to take advantage of hypotheses stating quantified equalities, you have to provide a bound for the number of extra equalities generated that way. Please note that one of the memebers of the equality must contain all the quantified variables in order for {\tt congruence} to match against it. + \begin{coq_eval} Reset Initial. Variable A:Set. @@ -2586,6 +2690,12 @@ congruence. \end{coq_example} \begin{Variants} + \item {\tt congruence {\sl n}}\\ + Tries to add at most {\tt \sl n} instances of hypotheses satting quantifiesd 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 lemmata 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$}\\ Adds {\tt \term$_1$ \dots\ \term$_n$} to the pool of terms used by {\tt congruence}. This helps in case you have partially applied @@ -2623,70 +2733,29 @@ integers. This tactic must be loaded by the command \texttt{Require Import Omega}. See the additional documentation about \texttt{omega} (chapter~\ref{OmegaChapter}). -\subsection{\tt ring \term$_1$ \dots\ \term$_n$ +\subsection{{\tt ring} and {\tt ring\_simplify \term$_1$ \dots\ \term$_n$} \tacindex{ring} -\comindex{Add Ring} -\comindex{Add Semi Ring}} - -This tactic, written by Samuel Boutin and Patrick Loiseleur, applies -associative commutative rewriting on every ring. The tactic must be -loaded by \texttt{Require Import Ring}. The ring must be declared in -the \texttt{Add Ring} command (see \ref{ring}). The ring of booleans -is predefined; if one wants to use the tactic on \texttt{nat} one must -first require the module \texttt{ArithRing}; for \texttt{Z}, do -\texttt{Require Import ZArithRing}; for \texttt{N}, do \texttt{Require -Import NArithRing}. - -The terms \term$_1$, \dots, \term$_n$ must be subterms of the goal -conclusion. The tactic \texttt{ring} normalizes these terms -w.r.t. associativity and commutativity and replace them by their -normal form. +\tacindex{ring\_simplify} +\comindex{Add Ring}} -\begin{Variants} -\item \texttt{ring} When the goal is an equality $t_1=t_2$, it - acts like \texttt{ring} $t_1$ $t_2$ and then simplifies or solves - the equality. +The {\tt ring} tactic solves equations upon polynomial expressions of +a ring (or semi-ring) structure. It proceeds by normalizing both hand +sides of the equation (w.r.t. associativity, commutativity and +distributivity, constant propagation) and comparing syntactically the +results. -\item \texttt{ring\_nat} is a tactic macro for \texttt{repeat rewrite - S\_to\_plus\_one; ring}. The theorem \texttt{S\_to\_plus\_one} is a - proof that \texttt{forall (n:nat), S n = plus (S O) n}. +{\tt ring\_simplify} applies the normalization procedure described +above to the terms given. The tactic then replaces all occurrences of +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. -\end{Variants} - -\Example -\begin{coq_eval} -Reset Initial. -Require Import ZArith. -Open Scope Z_scope. -\end{coq_eval} -\begin{coq_example} -Require Import ZArithRing. -Goal forall a b c:Z, - (a + b + c) * (a + b + c) = - a * a + b * b + c * c + 2 * a * b + 2 * a * c + 2 * b * c. -\end{coq_example} -\begin{coq_example} -intros; ring. -\end{coq_example} -\begin{coq_eval} -Reset Initial. -\end{coq_eval} - -You can have a look at the files \texttt{Ring.v}, -\texttt{ArithRing.v}, \texttt{ZArithRing.v} to see examples of the -\texttt{Add Ring} command. - -\SeeAlso Chapter~\ref{ring} for more detailed explanations about this tactic. +See chapter~\ref{ring} for more information on the tactic and how to +declare new ring structures. \subsection{\tt field -\tacindex{field}} - -This tactic written by David~Delahaye and Micaela~Mayero solves equalities -using commutative field theory. Denominators have to be non equal to zero and, -as this is not decidable in general, this tactic may generate side conditions -requiring some expressions to be non equal to zero. This tactic must be loaded -by {\tt Require Import Field}. Field theories are declared (as for {\tt ring}) with -the {\tt Add Field} command. +\tacindex{field} +\comindex{Add Field}} \Example \begin{coq_example*} @@ -2705,13 +2774,28 @@ intros; field. Reset Initial. \end{coq_eval} -\subsection{\tt Add Field -\comindex{Add Field}} +\SeeAlso file {\tt theories/Reals/Rbase.v} for an example of instantiation,\\ +\phantom{\SeeAlso}theory {\tt theories/Reals} for many examples of use of {\tt +field}. + +\subsection{\tt legacy field +\tacindex{legacy field}} + +This tactic written by David~Delahaye and Micaela~Mayero solves equalities +using commutative field theory. Denominators have to be non equal to zero and, +as this is not decidable in general, this tactic may generate side conditions +requiring some expressions to be non equal to zero. This tactic must be loaded +by {\tt Require Import LegacyField}. Field theories are declared (as for +{\tt legacy ring}) with +the {\tt Add Legacy Field} command. + +\subsection{\tt Add Legacy Field +\comindex{Add Legacy Field}} This vernacular command adds a commutative field theory to the database for the tactic {\tt field}. You must provide this theory as follows: \begin{flushleft} -{\tt Add Field {\it A} {\it Aplus} {\it Amult} {\it Aone} {\it Azero} {\it +{\tt Add Legacy Field {\it A} {\it Aplus} {\it Amult} {\it Aone} {\it Azero} {\it Aopp} {\it Aeq} {\it Ainv} {\it Rth} {\it Tinvl}} \end{flushleft} where {\tt {\it A}} is a term of type {\tt Type}, {\tt {\it Aplus}} is @@ -2734,28 +2818,24 @@ Require Import Ring} if you want to call the {\tt ring} tactic. \begin{Variants} -\item {\tt Add Field {\it A} {\it Aplus} {\it Amult} {\it Aone} {\it Azero} +\item {\tt Add Legacy Field {\it A} {\it Aplus} {\it Amult} {\it Aone} {\it Azero} {\it Aopp} {\it Aeq} {\it Ainv} {\it Rth} {\it Tinvl}}\\ {\tt \phantom{Add Field }with minus:={\it Aminus}} Adds also the term {\it Aminus} which must be a constant expressed by means of {\it Aopp}. -\item {\tt Add Field {\it A} {\it Aplus} {\it Amult} {\it Aone} {\it Azero} +\item {\tt Add Legacy Field {\it A} {\it Aplus} {\it Amult} {\it Aone} {\it Azero} {\it Aopp} {\it Aeq} {\it Ainv} {\it Rth} {\it Tinvl}}\\ -{\tt \phantom{Add Field }with div:={\it Adiv}} +{\tt \phantom{Add Legacy Field }with div:={\it Adiv}} Adds also the term {\it Adiv} which must be a constant expressed by means of {\it Ainv}. \end{Variants} -\SeeAlso file {\tt theories/Reals/Rbase.v} for an example of instantiation,\\ -\phantom{\SeeAlso}theory {\tt theories/Reals} for many examples of use of {\tt -field}. - \SeeAlso \cite{DelMay01} for more details regarding the implementation of {\tt -field}. +legacy field}. \subsection{\tt fourier \tacindex{fourier}} @@ -2780,6 +2860,7 @@ Reset Initial. \end{coq_eval} \subsection{\tt autorewrite with \ident$_1$ \dots \ident$_n$. +\label{tactic:autorewrite} \tacindex{autorewrite}} This tactic \footnote{The behavior of this tactic has much changed compared to @@ -2806,9 +2887,17 @@ command. 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 \texttt{autorewrite with {\ident} in {\qualid}} +\item \texttt{autorewrite with {\ident$_1$} \dots \ident$_n$ in {\qualid}} Performs all the rewritings in hypothesis {\qualid}. +\item \texttt{autorewrite with {\ident$_1$} \dots \ident$_n$ in {\qualid}} + + 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} arg must not contain any \texttt{type of} nor \texttt{value of}. \end{Variant} @@ -3243,27 +3332,25 @@ tool for generating automatically induction principles corresponding to (possibly mutually recursive) functions. Its syntax follows the schema: \begin{tabbing} -{\tt Functional Scheme {\ident$_i$} := Induction for - \ident'$_i$ with \ident'$_1$ \dots\ \ident'$_m$.} +{\tt Functional Scheme {\ident$_1$} := Induction for \ident'$_1$ Sort {\sort$_1$} \\ + with\\ + \mbox{}\hspace{0.1cm} \dots\ \\ + with {\ident$_m$} := Induction for {\ident'$_m$} Sort + {\sort$_m$}} \end{tabbing} -\ident'$_1$ \dots\ \ident'$_m$ are the names of mutually recursive -functions (they must be in the same order as when they were defined), -\ident'$_i$ being one of them. This command generates the induction -principle \ident$_i$, following the recursive structure and case -analyses of the functions \ident'$_1$ \dots\ \ident'$_m$, and having -\ident'$_i$ as entry point. +\ident'$_1$ \dots\ \ident'$_m$ are different mutually defined function +names (they must be in the same order as when they were defined). +This command generates the induction principles +\ident$_1$\dots\ident$_m$, following the recursive structure and case +analyses of the functions \ident'$_1$ \dots\ \ident'$_m$. -\begin{Variants} -\item {\tt Functional Scheme {\ident$_1$} := Induction for \ident'$_1$.} - - This command is a shortcut for: - \begin{tabbing} - {\tt Functional Scheme {\ident$_1$} := Induction for - \ident'$_1$ with \ident'$_1$.} -\end{tabbing} -This variant can be used for non mutually recursive functions only. -\end{Variants} +\paragraph{\texttt{Functional Scheme}} +There is a difference between obtaining an induction scheme by using +\texttt{Functional Scheme} on a function defined by \texttt{Function} +or not. Indeed \texttt{Function} generally produces smaller +principles, closer to the definition written by the user. + \SeeAlso Section~\ref{FunScheme-examples} @@ -3292,7 +3379,7 @@ The chapter~\ref{TacticLanguage} gives examples of more complex user-defined tactics. -% $Id: RefMan-tac.tex 9044 2006-07-12 13:22:17Z herbelin $ +% $Id: RefMan-tac.tex 9283 2006-10-26 08:13:51Z herbelin $ %%% Local Variables: %%% mode: latex |