diff options
Diffstat (limited to 'doc/refman/RefMan-tac.tex')
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 273 |
1 files changed, 213 insertions, 60 deletions
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 |