diff options
Diffstat (limited to 'doc/refman/RefMan-tac.tex')
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 312 |
1 files changed, 193 insertions, 119 deletions
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 14d95ab8..198f8f30 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -497,6 +497,89 @@ Section~\ref{pattern} to transform the goal so that it gets the form \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 premise 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 {\term}. 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}. If the conclusion of the type of {\term} does not match +the goal {\em and} the conclusion is an inductive type isomorphic to a +tuple type, then the tuple is (recursively) decomposed and the first +component of the tuple of which a non dependent premise matches the +conclusion of the type of {\ident}. Tuples are decomposed in a +width-first left-to-right order (for instance if the type of {\tt H1} +is a \verb=A <-> B= statement, and the type of {\tt H2} is \verb=A= +then {\tt apply H1 in H2} transforms the type of {\tt H2} into {\tt + B}). 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} with {\bindinglist}}{,} in {\ident}} + +This does the same but uses the bindings in each {\bindinglist} to +instantiate the parameters of the corresponding type of {\term} +(see syntax of bindings in Section~\ref{Binding-list}). + +\item {\tt eapply \nelist{{\term} with {\bindinglist}}{,} in {\ident}} +\tacindex{eapply {\ldots} in} + +This works as {\tt apply \nelist{{\term} with {\bindinglist}}{,} in +{\ident}} but turns unresolved bindings into existential variables, if +any, instead of failing. + +\item {\tt apply \nelist{{\term}{,} with {\bindinglist}}{,} in {\ident} as {\disjconjintropattern}} + +This works as {\tt apply \nelist{{\term}{,} with {\bindinglist}}{,} in +{\ident}} then destructs the hypothesis {\ident} along +{\disjconjintropattern} as {\tt destruct {\ident} as +{\disjconjintropattern}} would. + +\item {\tt eapply \nelist{{\term}{,} with {\bindinglist}}{,} in {\ident} as {\disjconjintropattern}} + +This works as {\tt apply \nelist{{\term}{,} with {\bindinglist}}{,} in {\ident} as {\disjconjintropattern}} but using {\tt eapply}. + +\item {\tt simple apply {\term} in {\ident}} +\tacindex{simple apply {\ldots} in} +\tacindex{simple eapply {\ldots} in} + +This behaves like {\tt apply {\term} in {\ident}} but it reasons +modulo conversion only on subterms that contain no variables to +instantiate. For instance, if {\tt id := fun x:nat => x} and {\tt H : + forall y, id y = y -> True} and {\tt H0 : O = O} then {\tt simple + apply H in H0} does not succeed because it would require the +conversion of {\tt f ?y} and {\tt O} where {\tt ?y} is a variable to +instantiate. Tactic {\tt simple apply {\term} in {\ident}} does not +either traverse tuples as {\tt apply {\term} in {\ident}} does. + +\item {\tt \zeroone{simple} apply \nelist{{\term} \zeroone{with {\bindinglist}}}{,} in {\ident} \zeroone{as {\disjconjintropattern}}}\\ +{\tt \zeroone{simple} eapply \nelist{{\term} \zeroone{with {\bindinglist}}}{,} in {\ident} \zeroone{as {\disjconjintropattern}}} + +This summarizes the different syntactic variants of {\tt apply {\term} + in {\ident}} and {\tt eapply {\term} in {\ident}}. +\end{Variants} + \subsection{{\tt set ( {\ident} {\tt :=} {\term} \tt )} \label{tactic:set} \tacindex{set} @@ -508,6 +591,11 @@ hypotheses of the current goal and adds the new definition {\ident {\tt :=} \term} to the local context. The default is to make this replacement only in the conclusion. +If {\term} has holes (i.e. subexpressions of the form ``\_''), the +tactic first checks that all subterms matching the pattern are +compatible before doing the replacement using the leftmost subterm +matching the pattern. + \begin{Variants} \item {\tt set (} {\ident} {\tt :=} {\term} {\tt ) in {\occgoalset}} @@ -543,7 +631,7 @@ Section~\ref{Occurrences clauses}. This is a more general form of {\tt remember} that remembers the occurrences of {\term} specified by an occurrences set. -\item {\tt pose ( {\ident} {\tt :=} {\term} {\tt )}} +\item {\tt pose ( {\ident} := {\term} )} This adds the local definition {\ident} := {\term} to the current context without performing any replacement in the goal or in the @@ -660,89 +748,6 @@ in the list of subgoals remaining to prove. \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 premise 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 {\term}. 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}. If the conclusion of the type of {\term} does not match -the goal {\em and} the conclusion is an inductive type isomorphic to a -tuple type, then the tuple is (recursively) decomposed and the first -component of the tuple of which a non dependent premise matches the -conclusion of the type of {\ident}. Tuples are decomposed in a -width-first left-to-right order (for instance if the type of {\tt H1} -is a \verb=A <-> B= statement, and the type of {\tt H2} is \verb=A= -then {\tt apply H1 in H2} transforms the type of {\tt H2} into {\tt - B}). 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} with {\bindinglist}}{,} in {\ident}} - -This does the same but uses the bindings in each {\bindinglist} to -instantiate the parameters of the corresponding type of {\term} -(see syntax of bindings in Section~\ref{Binding-list}). - -\item {\tt eapply \nelist{{\term} with {\bindinglist}}{,} in {\ident}} -\tacindex{eapply {\ldots} in} - -This works as {\tt apply \nelist{{\term} with {\bindinglist}}{,} in -{\ident}} but turns unresolved bindings into existential variables, if -any, instead of failing. - -\item {\tt apply \nelist{{\term}{,} with {\bindinglist}}{,} in {\ident} as {\disjconjintropattern}} - -This works as {\tt apply \nelist{{\term}{,} with {\bindinglist}}{,} in -{\ident}} then destructs the hypothesis {\ident} along -{\disjconjintropattern} as {\tt destruct {\ident} as -{\disjconjintropattern}} would. - -\item {\tt eapply \nelist{{\term}{,} with {\bindinglist}}{,} in {\ident} as {\disjconjintropattern}} - -This works as {\tt apply \nelist{{\term}{,} with {\bindinglist}}{,} in {\ident} as {\disjconjintropattern}} but using {\tt eapply}. - -\item {\tt simple apply {\term} in {\ident}} -\tacindex{simple apply {\ldots} in} -\tacindex{simple eapply {\ldots} in} - -This behaves like {\tt apply {\term} in {\ident}} but it reasons -modulo conversion only on subterms that contain no variables to -instantiate. For instance, if {\tt id := fun x:nat => x} and {\tt H : - forall y, id y = y -> True} and {\tt H0 : O = O} then {\tt simple - apply H in H0} does not succeed because it would require the -conversion of {\tt f ?y} and {\tt O} where {\tt ?y} is a variable to -instantiate. Tactic {\tt simple apply {\term} in {\ident}} does not -either traverse tuples as {\tt apply {\term} in {\ident}} does. - -\item {\tt \zeroone{simple} apply \nelist{{\term} \zeroone{with {\bindinglist}}}{,} in {\ident} \zeroone{as {\disjconjintropattern}}}\\ -{\tt \zeroone{simple} eapply \nelist{{\term} \zeroone{with {\bindinglist}}}{,} in {\ident} \zeroone{as {\disjconjintropattern}}} - -This summarizes the different syntactic variants of {\tt apply {\term} - in {\ident}} and {\tt eapply {\term} in {\ident}}. -\end{Variants} - \subsection{\tt generalize \term \tacindex{generalize} \label{generalize}} @@ -950,7 +955,8 @@ existential variable. \tacindex{instantiate} \label{instantiate}} -The {\tt instantiate} tactic allows to solve an existential variable +The {\tt instantiate} tactic allows to refine (see Section~\ref{refine}) +an existential variable with the term \term. The \num\ argument is the position of the existential variable from right to left in the conclusion. This cannot be the number of the existential variable since this number is different @@ -1296,8 +1302,8 @@ computational expressions (i.e. with few dead code). \item {\tt lazy [\qualid$_1$\ldots\qualid$_k$]}\\ {\tt lazy -[\qualid$_1$\ldots\qualid$_k$]} - These are respectively synonyms of {\tt cbv beta delta - [\qualid$_1$\ldots\qualid$_k$] iota zeta} and {\tt cbv beta delta + These are respectively synonyms of {\tt lazy beta delta + [\qualid$_1$\ldots\qualid$_k$] iota zeta} and {\tt lazy beta delta -[\qualid$_1$\ldots\qualid$_k$] iota zeta}. \item {\tt vm\_compute} \tacindex{vm\_compute} @@ -1361,6 +1367,55 @@ by {\tt plus' := plus} is possibly unfolded and reused in the recursive calls, but a constant such as {\tt succ := plus (S O)} is never unfolded. +The behaviour of {\tt simpl} can be tuned using the {\tt Arguments} vernacular +command as follows: +\begin{itemize} +\item +A constant can be marked to be never unfolded by {\tt simpl}: +\begin{coq_example*} +Arguments minus x y : simpl never +\end{coq_example*} +After that command an expression like {\tt (minus (S x) y)} is left untouched by +the {\tt simpl} tactic. +\item +A constant can be marked to be unfolded only if applied to enough arguments. +The number of arguments required can be specified using +the {\tt /} symbol in the arguments list of the {\tt Arguments} vernacular +command. +\begin{coq_example*} +Definition fcomp A B C f (g : A -> B) (x : A) : C := f (g x). +Notation "f \o g" := (fcomp f g) (at level 50). +Arguments fcomp {A B C} f g x /. +\end{coq_example*} +After that command the expression {\tt (f \verb+\+o g)} is left untouched by +{\tt simpl} while {\tt ((f \verb+\+o g) t)} is reduced to {\tt (f (g t))}. +The same mechanism can be used to make a constant volatile, i.e. always +unfolded by {\tt simpl}. +\begin{coq_example*} +Definition volatile := fun x : nat => x. +Arguments volatile / x. +\end{coq_example*} +\item +A constant can be marked to be unfolded only if an entire set of arguments +evaluates to a constructor. The {\tt !} symbol can be used to mark such +arguments. +\begin{coq_example*} +Arguments minus !x !y. +\end{coq_example*} +After that command, the expression {\tt (minus (S x) y)} is left untouched by +{\tt simpl}, while {\tt (minus (S x) (S y))} is reduced to {\tt (minus x y)}. +\item +A special heuristic to determine if a constant has to be unfolded can be +activated with the following command: +\begin{coq_example*} +Arguments minus x y : simpl nomatch +\end{coq_example*} +The heuristic avoids to perform a simplification step that would +expose a {\tt match} construct in head position. For example the +expression {\tt (minus (S (S x)) (S y))} is simplified to +{\tt (minus (S x) y)} even if an extra simplification is possible. +\end{itemize} + \tacindex{simpl \dots\ in} \begin{Variants} \item {\tt simpl {\term}} @@ -1626,18 +1681,16 @@ Section~\ref{Cic-inductive-definitions}). \subsection{\tt induction \term \tacindex{induction}} -This tactic applies to any goal. The type of the argument {\term} must -be an inductive constant. Then, the tactic {\tt induction} -generates subgoals, one for each possible form of {\term}, i.e. one -for each constructor of the inductive type. +This tactic applies to any goal. The argument {\term} must be of +inductive type and the tactic {\tt induction} generates subgoals, +one for each possible form of {\term}, i.e. one for each constructor +of the inductive type. -The tactic {\tt induction} automatically replaces every occurrences -of {\term} in the conclusion and the hypotheses of the goal. It -automatically adds induction hypotheses (using names of the form {\tt - IHn1}) to the local context. If some hypothesis must not be taken -into account in the induction hypothesis, then it needs to be removed -first (you can also use the tactics {\tt elim} or {\tt simple induction}, -see below). +If the argument is dependent in either the conclusion or some +hypotheses of the goal, the argument is replaced by the appropriate +constructor form in each of the resulting subgoals and induction +hypotheses are added to the local context using names whose prefix is +{\tt IH}. There are particular cases: @@ -1649,10 +1702,13 @@ behaves as {\tt intros until {\ident}; induction {\ident}}. \item If {\term} is a {\num}, then {\tt induction {\num}} behaves as {\tt intros until {\num}} followed by {\tt induction} applied to the -last introduced hypothesis. +last introduced hypothesis. Remark: For simple induction on a numeral, +use syntax {\tt induction ({\num})} (not very interesting anyway). -\Rem For simple induction on a numeral, use syntax {\tt induction -({\num})} (not very interesting anyway). +\item The argument {\term} can also be a pattern of which holes are + denoted by ``\_''. In this case, the tactic checks that all subterms + matching the pattern in the conclusion and the hypotheses are + compatible and performs induction using this subterm. \end{itemize} @@ -1840,10 +1896,19 @@ instantiate premises of the type of {\term$_2$}. \tacindex{destruct}} \label{destruct} -The tactic {\tt destruct} is used to perform case analysis without -recursion. Its behavior is similar to {\tt induction} except -that no induction hypothesis is generated. It applies to any goal and -the type of {\term} must be inductively defined. There are particular cases: +This tactic applies to any goal. The argument {\term} must be of +inductive or coinductive type and the tactic generates subgoals, one +for each possible form of {\term}, i.e. one for each constructor of +the inductive or coinductive type. Unlike {\tt induction}, no +induction hypothesis is generated by {\tt destruct}. + +If the argument is dependent in either the conclusion or some +hypotheses of the goal, the argument is replaced by the appropriate +constructor form in each of the resulting subgoals, thus performing +case analysis. If non dependent, the tactic simply exposes the +inductive or coinductive structure of the argument. + +There are special cases: \begin{itemize} @@ -1853,10 +1918,13 @@ behaves as {\tt intros until {\ident}; destruct {\ident}}. \item If {\term} is a {\num}, then {\tt destruct {\num}} behaves as {\tt intros until {\num}} followed by {\tt destruct} applied to the -last introduced hypothesis. +last introduced hypothesis. Remark: For destruction of a numeral, use +syntax {\tt destruct ({\num})} (not very interesting anyway). -\Rem For destruction of a numeral, use syntax {\tt destruct -({\num})} (not very interesting anyway). +\item The argument {\term} can also be a pattern of which holes are + denoted by ``\_''. In this case, the tactic checks that all subterms + matching the pattern in the conclusion and the hypotheses are + compatible and performs case analysis using this subterm. \end{itemize} @@ -2599,12 +2667,7 @@ This tactic solves a goal of the form {\tt forall $x$ $y$:$R$, \{$x$=$y$\}+\{\verb|~|$x$=$y$\}}, where $R$ is an inductive type such that its constructors do not take proofs or functions as arguments, nor objects in dependent types. - -\begin{Variants} -\item {\tt decide equality {\term}$_1$ {\term}$_2$ }.\\ - Solves a goal of the form {\tt \{}\term$_1${\tt =}\term$_2${\tt -\}+\{\verb|~|}\term$_1${\tt =}\term$_2${\tt \}}. -\end{Variants} +It solves goals of the form {\tt \{$x$=$y$\}+\{\verb|~|$x$=$y$\}} as well. \subsection{\tt compare \term$_1$ \term$_2$ \tacindex{compare}} @@ -2696,7 +2759,7 @@ If {\term} is a proof of a statement of conclusion then {\tt injection} applies injectivity as deep as possible to derive the equality of all the subterms of {\term$_1$} and {\term$_2$} placed in the same positions. For example, from {\tt (S - (S n))=(S (S (S m))} we may derive {\tt n=(S m)}. To use this + (S n))=(S (S (S m)))} we may derive {\tt n=(S m)}. To use this tactic {\term$_1$} and {\term$_2$} should be elements of an inductive set and they should be neither explicitly equal, nor structurally different. We mean by this that, if {\tt n$_1$} and {\tt n$_2$} are @@ -4042,7 +4105,9 @@ databases are non empty and can be used. \begin{description} \item[\tt core] This special database is automatically used by - \texttt{auto}. It contains only basic lemmas about negation, + \texttt{auto}, except when pseudo-database \texttt{nocore} is + given to \texttt{auto}. The \texttt{core} database contains + only basic lemmas about negation, conjunction, and so on from. Most of the hints in this database come from the \texttt{Init} and \texttt{Logic} directories. @@ -4174,6 +4239,16 @@ 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$}}} + 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}} + 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}} This command declares a tactic to be used to solve implicit arguments @@ -4230,7 +4305,8 @@ general principle of mutual induction for objects in type {\term$_i$}. \item {\tt Scheme Equality for \ident$_1$\comindex{Scheme Equality}} Tries to generate a boolean equality and a proof of the - decidability of the usual equality. + decidability of the usual equality. If \ident$_i$ involves + some other inductive types, their equality has to be defined first. \item {\tt Scheme Induction for \ident$_1$ Sort {\sort$_1$} \\ with\\ @@ -4332,8 +4408,6 @@ Chapter~\ref{TacticLanguage} gives examples of more complex user-defined tactics. -% $Id: RefMan-tac.tex 14762 2011-12-04 20:48:36Z herbelin $ - %%% Local Variables: %%% mode: latex %%% TeX-master: "Reference-Manual" |