diff options
Diffstat (limited to 'doc/sphinx/proof-engine/tactics.rst')
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 5397 |
1 files changed, 5397 insertions, 0 deletions
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst new file mode 100644 index 000000000..2597e3c37 --- /dev/null +++ b/doc/sphinx/proof-engine/tactics.rst @@ -0,0 +1,5397 @@ +% TODO: unify the use of \form and \type to mean a type +% or use \form specifically for a type of type Prop +\chapter{Tactics +\index{Tactics} +\label{Tactics}} +%HEVEA\cutname{tactics.html} + +A deduction rule is a link between some (unique) formula, that we call +the {\em conclusion} and (several) formulas that we call the {\em +premises}. A deduction rule can be read in two ways. The first +one says: {\it ``if I know this and this then I can deduce +this''}. For instance, if I have a proof of $A$ and a proof of $B$ +then I have a proof of $A \land B$. This is forward reasoning from +premises to conclusion. The other way says: {\it ``to prove this I +have to prove this and this''}. For instance, to prove $A \land B$, I +have to prove $A$ and I have to prove $B$. This is backward reasoning +from conclusion to premises. We say that the conclusion +is the {\em goal}\index{goal} to prove and premises are the {\em +subgoals}\index{subgoal}. The tactics implement {\em backward +reasoning}. When applied to a goal, a tactic replaces this goal with +the subgoals it generates. We say that a tactic reduces a goal to its +subgoal(s). + +Each (sub)goal is denoted with a number. The current goal is numbered +1. By default, a tactic is applied to the current goal, but one can +address a particular goal in the list by writing {\sl n:\tac} which +means {\it ``apply tactic {\tac} to goal number {\sl n}''}. +We can show the list of subgoals by typing {\tt Show} (see +Section~\ref{Show}). + +Since not every rule applies to a given statement, every tactic cannot be +used to reduce any goal. In other words, before applying a tactic to a +given goal, the system checks that some {\em preconditions} are +satisfied. If it is not the case, the tactic raises an error message. + +Tactics are built 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}. + +\section{Invocation of tactics +\label{tactic-syntax} +\index{tactic@{\tac}}} + +A tactic is applied as an ordinary command. It may be preceded by a +goal selector (see Section \ref{ltac:selector}). +If no selector is specified, the default +selector (see Section \ref{default-selector}) is used. + +\newcommand{\toplevelselector}{\nterm{toplevel\_selector}} +\begin{tabular}{lcl} +{\commandtac} & ::= & {\toplevelselector} {\tt :} {\tac} {\tt .}\\ + & $|$ & {\tac} {\tt .} +\end{tabular} +\subsection[\tt Set Default Goal Selector ``\toplevelselector''.] + {\tt Set Default Goal Selector ``\toplevelselector''. + \optindex{Default Goal Selector} + \label{default-selector}} +After using this command, the default selector -- used when no selector +is specified when applying a tactic -- is set to the chosen value. The +initial value is $1$, hence the tactics are, by default, applied to +the first goal. Using {\tt Set Default Goal Selector ``all''} will +make is so that tactics are, by default, applied to every goal +simultaneously. Then, to apply a tactic {\tt tac} to the first goal +only, you can write {\tt 1:tac}. Although more selectors are available, +only {\tt ``all''} or a single natural number are valid default +goal selectors. + +\subsection[\tt Test Default Goal Selector.] + {\tt Test Default Goal Selector.} +This command displays the current default selector. + +\subsection{Bindings list +\index{Binding list} +\label{Binding-list}} + +Tactics that take a term as argument may also support a bindings list, so +as to instantiate some parameters of the term by name or position. +The general form of a term equipped with a bindings list is {\tt +{\term} with {\bindinglist}} where {\bindinglist} may be of two +different forms: + +\begin{itemize} +\item In a bindings list of the form {\tt (\vref$_1$ := \term$_1$) + \dots\ (\vref$_n$ := \term$_n$)}, {\vref} is either an {\ident} or a + {\num}. The references are determined according to the type of + {\term}. If \vref$_i$ is an identifier, this identifier has to be + bound in the type of {\term} and the binding provides the tactic + with an instance for the parameter of this name. If \vref$_i$ is + some number $n$, this number denotes the $n$-th non dependent + premise of the {\term}, as determined by the type of {\term}. + + \ErrMsg \errindex{No such binder} + +\item A bindings list can also be a simple list of terms {\tt + \term$_1$ \dots\ \term$_n$}. In that case the references to + which these terms correspond are determined by the tactic. In case + of {\tt induction}, {\tt destruct}, {\tt elim} and {\tt case} (see + Section~\ref{elim}) the terms have to provide instances for all the + dependent products in the type of \term\ while in the case of {\tt + apply}, or of {\tt constructor} and its variants, only instances for + the dependent products that are not bound in the conclusion of the + type are required. + + \ErrMsg \errindex{Not the right number of missing arguments} +\end{itemize} + +\subsection{Occurrences sets and occurrences clauses} +\label{Occurrences_clauses} +\index{Occurrences clauses} + +An occurrences clause is a modifier to some tactics that obeys the +following syntax: + +\begin{tabular}{lcl} +{\occclause} & ::= & {\tt in} {\occgoalset} \\ +{\occgoalset} & ::= & + \zeroonelax{{\ident$_1$} \zeroone{\atoccurrences} {\tt ,} \\ +& & {\dots} {\tt ,}\\ +& & {\ident$_m$} \zeroone{\atoccurrences}}\\ +& & \zeroone{{\tt |-} \zeroone{{\tt *} \zeroone{\atoccurrences}}}\\ +& | & + {\tt *} {\tt |-} \zeroone{{\tt *} \zeroone{\atoccurrences}}\\ +& | & + {\tt *}\\ +{\atoccurrences} & ::= & {\tt at} {\occlist}\\ +{\occlist} & ::= & \zeroone{{\tt -}} {\num$_1$} \dots\ {\num$_n$} +\end{tabular} + +The role of an occurrence clause is to select a set of occurrences of +a {\term} in a goal. In the first case, the {{\ident$_i$} +\zeroone{{\tt at} {\num$_1^i$} \dots\ {\num$_{n_i}^i$}}} parts +indicate that occurrences have to be selected in the hypotheses named +{\ident$_i$}. If no numbers are given for hypothesis {\ident$_i$}, +then all the occurrences of {\term} in the hypothesis are selected. If +numbers are given, they refer to occurrences of {\term} when the term +is printed using option {\tt Set Printing All} (see +Section~\ref{SetPrintingAll}), counting from left to right. In +particular, occurrences of {\term} in implicit arguments (see +Section~\ref{Implicit Arguments}) or coercions (see +Section~\ref{Coercions}) are counted. + +If a minus sign is given between {\tt at} and the list of occurrences, +it negates the condition so that the clause denotes all the occurrences except +the ones explicitly mentioned after the minus sign. + +As an exception to the left-to-right order, the occurrences in the +{\tt return} subexpression of a {\tt match} are considered {\em +before} the occurrences in the matched term. + +In the second case, the {\tt *} on the left of {\tt |-} means that +all occurrences of {\term} are selected in every hypothesis. + +In the first and second case, if {\tt *} is mentioned on the right of +{\tt |-}, the occurrences of the conclusion of the goal have to be +selected. If some numbers are given, then only the occurrences denoted +by these numbers are selected. In no numbers are given, all +occurrences of {\term} in the goal are selected. + +Finally, the last notation is an abbreviation for {\tt * |- *}. Note +also that {\tt |-} is optional in the first case when no {\tt *} is +given. + +Here are some tactics that understand occurrences clauses: +{\tt set}, {\tt remember}, {\tt induction}, {\tt destruct}. + +\SeeAlso~Sections~\ref{tactic:set}, \ref{Tac-induction}, \ref{SetPrintingAll}. + +\section{Applying theorems} + +\subsection{\tt exact \term} +\tacindex{exact} +\label{exact} + +This tactic applies to any goal. It gives directly the exact proof +term of the goal. Let {\T} be our goal, let {\tt p} be a term of type +{\tt U} then {\tt exact p} succeeds iff {\tt T} and {\tt U} are +convertible (see Section~\ref{conv-rules}). + +\begin{ErrMsgs} +\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 + and goals with meta-variables. + +\end{Variants} + +\subsection{\tt assumption} +\tacindex{assumption} + +This tactic looks in the local context for an +hypothesis which type is equal to the goal. If it is the case, the +subgoal is proved. Otherwise, it fails. + +\begin{ErrMsgs} +\item \errindex{No such assumption} +\end{ErrMsgs} + +\begin{Variants} +\tacindex{eassumption} + \item \texttt{eassumption} + + This tactic behaves like \texttt{assumption} but is able to handle + goals with meta-variables. + +\end{Variants} + +\subsection{\tt refine \term} +\tacindex{refine} +\label{refine} +\label{refine-example} +\index{?@{\texttt{?}}} + +This tactic applies to any goal. It behaves like {\tt exact} with a big +difference: the user can leave some holes (denoted by \texttt{\_} or +{\tt (\_:\type)}) in the term. {\tt refine} will generate as +many subgoals as there are holes in the term. The type of holes must be +either synthesized by the system or declared by an +explicit cast like \verb|(_:nat->Prop)|. Any subgoal that occurs in other +subgoals is automatically shelved, as if calling {\tt shelve\_unifiable} +(see Section~\ref{shelve}). +This low-level tactic can be useful to advanced users. + +\Example + +\begin{coq_example*} +Inductive Option : Set := + | Fail : Option + | Ok : bool -> Option. +\end{coq_example} +\begin{coq_example} +Definition get : forall x:Option, x <> Fail -> bool. +refine + (fun x:Option => + match x return x <> Fail -> bool with + | Fail => _ + | Ok b => fun _ => b + end). +intros; absurd (Fail = Fail); trivial. +\end{coq_example} +\begin{coq_example*} +Defined. +\end{coq_example*} + +\begin{ErrMsgs} +\item \errindex{invalid argument}: + the tactic \texttt{refine} does not know what to do + with the term you gave. +\item \texttt{Refine passed ill-formed term}: the term you gave is not + a valid proof (not easy to debug in general). + This message may also occur in higher-level tactics that call + \texttt{refine} internally. +\item \errindex{Cannot infer a term for this placeholder}: + there is a hole in the term you gave + which type cannot be inferred. Put a cast around it. +\end{ErrMsgs} + +\begin{Variants} +\item {\tt simple refine \term}\tacindex{simple refine} + + This tactic behaves like {\tt refine}, but it does not shelve any + subgoal. It does not perform any beta-reduction either. +\item {\tt notypeclasses refine \term}\tacindex{notypeclasses refine} + + This tactic behaves like {\tt refine} except it performs typechecking + without resolution of typeclasses. + +\item {\tt simple notypeclasses refine \term}\tacindex{simple + notypeclasses refine} + + This tactic behaves like {\tt simple refine} except it performs typechecking + without resolution of typeclasses. +\end{Variants} + +\subsection{\tt apply \term} +\tacindex{apply} +\label{apply} +\label{eapply} + +This tactic applies to any goal. The argument {\term} is a term +well-formed in the local context. The tactic {\tt apply} tries to +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}. 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 each component +of the tuple is recursively matched to the goal in the left-to-right +order. + +The tactic {\tt apply} relies on first-order unification with +dependent types unless the conclusion of the type of {\term} is of the +form {\tt ($P$ $t_1$ \dots\ $t_n$)} with $P$ to be instantiated. In +the latter case, the behavior depends on the form of the goal. If the +goal is of the form {\tt (fun $x$ => $Q$)~$u_1$~\ldots~$u_n$} and the +$t_i$ and $u_i$ unifies, then $P$ is taken to be {\tt (fun $x$ => $Q$)}. +Otherwise, {\tt apply} tries to define $P$ by abstracting over +$t_1$~\ldots ~$t_n$ in the goal. See {\tt pattern} in +Section~\ref{pattern} to transform the goal so that it gets the form +{\tt (fun $x$ => $Q$)~$u_1$~\ldots~$u_n$}. + +\begin{ErrMsgs} +\item \errindex{Unable to unify \dots\ with \dots} + + The {\tt apply} + tactic failed to match the conclusion of {\term} and the current goal. + You can help the {\tt apply} tactic by transforming your + goal with the {\tt change} or {\tt pattern} tactics (see + sections~\ref{pattern},~\ref{change}). + +\item \errindex{Unable to find an instance for the variables +{\ident} \dots\ {\ident}} + + This occurs when some instantiations of the premises of {\term} are not + deducible from the unification. This is the case, for instance, when + you want to apply a transitivity property. In this case, you have to + use one of the variants below: + +\end{ErrMsgs} + +\begin{Variants} + +\item{\tt apply {\term} with {\term$_1$} \dots\ {\term$_n$}} + \tacindex{apply \dots\ with} + + Provides {\tt apply} with explicit instantiations for all dependent + premises of the type of {\term} that do not occur in the conclusion + and consequently cannot be found by unification. Notice that + {\term$_1$} \mbox{\dots} {\term$_n$} must be given according to the order + of these dependent premises of the type of {\term}. + + \ErrMsg \errindex{Not the right number of missing arguments} + +\item{\tt apply {\term} with ({\vref$_1$} := {\term$_1$}) \dots\ ({\vref$_n$} + := {\term$_n$})} + + This also provides {\tt apply} with values for instantiating + premises. Here, variables are referred by names and non-dependent + products by increasing numbers (see syntax in Section~\ref{Binding-list}). + +\item {\tt apply \term$_1$ , \mbox{\dots} , \term$_n$} + + This is a shortcut for {\tt apply} {\term$_1$} {\tt ; [ ..~|} + \ldots~{\tt ; [ ..~| {\tt apply} {\term$_n$} ]} \ldots~{\tt ]}, i.e. for the + successive applications of {\term$_{i+1}$} on the last subgoal + generated by {\tt apply} {\term$_i$}, starting from the application + of {\term$_1$}. + +\item {\tt eapply \term}\tacindex{eapply} + + The tactic {\tt eapply} behaves like {\tt apply} but it does not fail + when no instantiations are deducible for some variables in the + premises. Rather, it turns these variables into + existential variables which are variables still to instantiate (see + Section~\ref{evars}). The instantiation is intended to be found + later in the proof. + +\item {\tt simple apply {\term}} \tacindex{simple apply} + + This behaves like {\tt apply} but it reasons modulo conversion only + on subterms that contain no variables to instantiate. For instance, + the following example does not succeed because it would require the + conversion of {\tt id ?foo} and {\tt O}. + +\begin{coq_eval} +Reset Initial. +\end{coq_eval} +\begin{coq_example*} +Definition id (x : nat) := x. +Hypothesis H : forall y, id y = y. +Goal O = O. +\end{coq_example*} +\begin{coq_example} +Fail simple apply H. +\end{coq_example} + + Because it reasons modulo a limited amount of conversion, {\tt + simple apply} fails quicker than {\tt apply} and it is then + well-suited for uses in used-defined tactics that backtrack often. + Moreover, it does not traverse tuples as {\tt apply} does. + +\item \zeroone{{\tt simple}} {\tt apply} {\term$_1$} \zeroone{{\tt with} + {\bindinglist$_1$}} {\tt ,} \ldots {\tt ,} {\term$_n$} \zeroone{{\tt with} + {\bindinglist$_n$}}\\ + \zeroone{{\tt simple}} {\tt eapply} {\term$_1$} \zeroone{{\tt with} + {\bindinglist$_1$}} {\tt ,} \ldots {\tt ,} {\term$_n$} \zeroone{{\tt with} + {\bindinglist$_n$}} + + This summarizes the different syntaxes for {\tt apply} and {\tt eapply}. + +\item {\tt lapply {\term}} \tacindex{lapply} + + This tactic applies to any goal, say {\tt G}. The argument {\term} + has to be well-formed in the current context, its type being + reducible to a non-dependent product {\tt A -> B} with {\tt B} + possibly containing products. Then it generates two subgoals {\tt + B->G} and {\tt A}. Applying {\tt lapply H} (where {\tt H} has type + {\tt A->B} and {\tt B} does not start with a product) does the same + as giving the sequence {\tt cut B. 2:apply H.} where {\tt cut} is + described below. + + \Warning When {\term} contains more than one non + dependent product the tactic {\tt lapply} only takes into account the + first product. + +\end{Variants} + +\Example +Assume we have a transitive relation {\tt R} on {\tt nat}: +\label{eapply-example} + +\begin{coq_eval} +Reset Initial. +\end{coq_eval} +\begin{coq_example*} +Variable R : nat -> nat -> Prop. +Hypothesis Rtrans : forall x y z:nat, R x y -> R y z -> R x z. +Variables n m p : nat. +Hypothesis Rnm : R n m. +Hypothesis Rmp : R m p. +\end{coq_example*} + +Consider the goal {\tt (R n p)} provable using the transitivity of +{\tt R}: + +\begin{coq_example*} +Goal R n p. +\end{coq_example*} + +The direct application of {\tt Rtrans} with {\tt apply} fails because +no value for {\tt y} in {\tt Rtrans} is found by {\tt apply}: + +%\begin{coq_eval} +%Set Printing Depth 50. +%(********** The following is not correct and should produce **********) +%(**** Error: generated subgoal (R n ?17) has metavariables in it *****) +%\end{coq_eval} +\begin{coq_example} +Fail apply Rtrans. +\end{coq_example} + +A solution is to apply {\tt (Rtrans n m p)} or {\tt (Rtrans n m)}. + +\begin{coq_example} +apply (Rtrans n m p). +\end{coq_example} + +\begin{coq_eval} +Undo. +\end{coq_eval} + +Note that {\tt n} can be inferred from the goal, so the following would +work too. + +\begin{coq_example*} +apply (Rtrans _ m). +\end{coq_example*} +\begin{coq_eval} +Undo. +\end{coq_eval} + +More elegantly, {\tt apply Rtrans with (y:=m)} allows only mentioning +the unknown {\tt m}: + +\begin{coq_example*} +apply Rtrans with (y := m). +\end{coq_example*} +\begin{coq_eval} +Undo. +\end{coq_eval} + +Another solution is to mention the proof of {\tt (R x y)} in {\tt +Rtrans} \ldots + +\begin{coq_example} +apply Rtrans with (1 := Rnm). +\end{coq_example} +\begin{coq_eval} +Undo. +\end{coq_eval} + +\ldots or the proof of {\tt (R y z)}. + +\begin{coq_example} +apply Rtrans with (2 := Rmp). +\end{coq_example} +\begin{coq_eval} +Undo. +\end{coq_eval} + +On the opposite, one can use {\tt eapply} which postpones the problem +of finding {\tt m}. Then one can apply the hypotheses {\tt Rnm} and {\tt +Rmp}. This instantiates the existential variable and completes the proof. + +\begin{coq_example} +eapply Rtrans. +apply Rnm. +apply Rmp. +\end{coq_example} + +\begin{coq_eval} +Reset R. +\end{coq_eval} + +\noindent {\bf Remark: } When the conclusion of the type of the term +to apply is an inductive type isomorphic to a tuple type and {\em apply} +looks recursively whether a component of the tuple matches the goal, +it excludes components whose statement would result in applying an +universal lemma of the form {\tt forall A, ... -> A}. Excluding this +kind of lemma can be avoided by setting the following option: + +\begin{quote} +\optindex{Universal Lemma Under Conjunction} +{\tt Set Universal Lemma Under Conjunction} +\end{quote} + +This option, which preserves compatibility with versions of {\Coq} +prior to 8.4 is also available for {\tt apply {\term} in {\ident}} +(see Section~\ref{apply-in}). + +\subsection{\tt apply {\term} in {\ident}} +\label{apply-in} +\tacindex{apply \dots\ 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 \dots\ 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 {\intropattern}} + +This works as {\tt apply \nelist{{\term} with {\bindinglist}}{,} in +{\ident}} then applies the {\intropattern} to the hypothesis {\ident}. + +\item {\tt eapply \nelist{{\term} with {\bindinglist}}{,} in {\ident} as {\intropattern}} + +This works as {\tt apply \nelist{{\term} with {\bindinglist}}{,} in {\ident} as {\intropattern}} but using {\tt eapply}. + +\item {\tt simple apply {\term} in {\ident}} +\tacindex{simple apply \dots\ in} +\tacindex{simple eapply \dots\ 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 id ?1234} and {\tt O} where {\tt ?1234} 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 {\intropattern}}}\\ +{\tt \zeroone{simple} eapply \nelist{{\term} \zeroone{with {\bindinglist}}}{,} in {\ident} \zeroone{as {\intropattern}}} + +This summarizes the different syntactic variants of {\tt apply {\term} + in {\ident}} and {\tt eapply {\term} in {\ident}}. +\end{Variants} + +\subsection{\tt constructor \num} +\label{constructor} +\tacindex{constructor} + +This tactic applies to a goal such that its conclusion is +an inductive type (say {\tt I}). The argument {\num} must be less +or equal to the numbers of constructor(s) of {\tt I}. Let {\tt ci} be +the {\tt i}-th constructor of {\tt I}, then {\tt constructor i} is +equivalent to {\tt intros; apply ci}. + +\begin{ErrMsgs} +\item \errindex{Not an inductive product} +\item \errindex{Not enough constructors} +\end{ErrMsgs} + +\begin{Variants} +\item \texttt{constructor} + + This tries \texttt{constructor 1} then \texttt{constructor 2}, + \dots\ , then \texttt{constructor} \textit{n} where \textit{n} is + the number of constructors of the head of the goal. + +\item {\tt constructor \num~with} {\bindinglist} + + Let {\tt ci} be the {\tt i}-th constructor of {\tt I}, then {\tt + constructor i with \bindinglist} is equivalent to {\tt intros; + apply ci with \bindinglist}. + + \Warning the terms in the \bindinglist\ are checked + in the context where {\tt constructor} is executed and not in the + context where {\tt apply} is executed (the introductions are not + taken into account). + +% To document? +% \item {\tt constructor {\tactic}} + +\item {\tt split}\tacindex{split} + + This applies only if {\tt I} has a single constructor. It is then + equivalent to {\tt constructor 1}. It is typically used in the case + of a conjunction $A\land B$. + + \ErrMsg \errindex{Not an inductive goal with 1 constructor} + +\item {\tt exists {\bindinglist}}\tacindex{exists} + + This applies only if {\tt I} has a single constructor. It is then + equivalent to {\tt intros; constructor 1 with \bindinglist}. It is + typically used in the case of an existential quantification $\exists + x, P(x)$. + + \ErrMsg \errindex{Not an inductive goal with 1 constructor} + +\item {\tt exists \nelist{\bindinglist}{,}} + + This iteratively applies {\tt exists {\bindinglist}}. + +\item {\tt left}\tacindex{left}\\ + {\tt right}\tacindex{right} + + These tactics apply only if {\tt I} has two constructors, for instance + in the case of a + disjunction $A\lor B$. Then, they are respectively equivalent to {\tt + constructor 1} and {\tt constructor 2}. + + \ErrMsg \errindex{Not an inductive goal with 2 constructors} + +\item {\tt left with \bindinglist}\\ + {\tt right with \bindinglist}\\ + {\tt split with \bindinglist} + + As soon as the inductive type has the right number of constructors, + these expressions are equivalent to calling {\tt + constructor $i$ with \bindinglist} for the appropriate $i$. + +\item \texttt{econstructor}\tacindex{econstructor}\\ + \texttt{eexists}\tacindex{eexists}\\ + \texttt{esplit}\tacindex{esplit}\\ + \texttt{eleft}\tacindex{eleft}\\ + \texttt{eright}\tacindex{eright} + + These tactics and their variants behave like \texttt{constructor}, + \texttt{exists}, \texttt{split}, \texttt{left}, \texttt{right} and + their variants but they introduce existential variables instead of + failing when the instantiation of a variable cannot be found (cf + \texttt{eapply} and Section~\ref{eapply-example}). + +\end{Variants} + +\section{Managing the local context} + +\subsection{\tt intro} +\tacindex{intro} +\label{intro} + +This tactic applies to a goal that is either a product or starts with +a let binder. If the goal is a product, the tactic implements the +``Lam''\index{Typing rules!Lam} rule given in +Section~\ref{Typed-terms}\footnote{Actually, only the second subgoal will be +generated since the other one can be automatically checked.}. If the +goal starts with a let binder, then the tactic implements a mix of the +``Let''\index{Typing rules!Let} and ``Conv''\index{Typing rules!Conv}. + +If the current goal is a dependent product $\forall x:T,~U$ (resp {\tt +let $x$:=$t$ in $U$}) then {\tt intro} puts {\tt $x$:$T$} (resp {\tt $x$:=$t$}) + in the local context. +% Obsolete (quantified names already avoid hypotheses names): +% Otherwise, it puts +% {\tt x}{\it n}{\tt :T} where {\it n} is such that {\tt x}{\it n} is a +%fresh name. +The new subgoal is $U$. +% If the {\tt x} has been renamed {\tt x}{\it n} then it is replaced +% by {\tt x}{\it n} in {\tt U}. + +If the goal is a non-dependent product $T \to U$, then it puts +in the local context either {\tt H}{\it n}{\tt :$T$} (if $T$ is of +type {\tt Set} or {\tt Prop}) or {\tt X}{\it n}{\tt :$T$} (if the type +of $T$ is {\tt Type}). The optional index {\it n} is such that {\tt +H}{\it n} or {\tt X}{\it n} is a fresh identifier. +In both cases, the new subgoal is $U$. + +If the goal is neither a product nor starting with a let definition, +the tactic {\tt intro} applies the tactic {\tt hnf} until the tactic +{\tt intro} can be applied or the goal is not head-reducible. + +\begin{ErrMsgs} +\item \errindex{No product even after head-reduction} +\item \errindexbis{{\ident} is already used}{is already used} +\end{ErrMsgs} + +\begin{Variants} + +\item {\tt intros}\tacindex{intros} + + This repeats {\tt intro} until it meets the head-constant. It never reduces + head-constants and it never fails. + +\item {\tt intro {\ident}} + + This applies {\tt intro} but forces {\ident} to be the name of the + introduced hypothesis. + + \ErrMsg \errindex{name {\ident} is already used} + + \Rem If a name used by {\tt intro} hides the base name of a global + constant then the latter can still be referred to by a qualified name + (see \ref{LongNames}). + +\item {\tt intros \ident$_1$ \dots\ \ident$_n$} + + This is equivalent to the composed tactic {\tt intro \ident$_1$; \dots\ ; + intro \ident$_n$}. + + More generally, the \texttt{intros} tactic takes a pattern as + argument in order to introduce names for components of an inductive + definition or to clear introduced hypotheses. This is explained + in~\ref{intros-pattern}. + +\item {\tt intros until {\ident}} \tacindex{intros until} + + This repeats {\tt intro} until it meets a premise of the goal having form + {\tt (} {\ident}~{\tt :}~{\term} {\tt )} and discharges the variable + named {\ident} of the current goal. + + \ErrMsg \errindex{No such hypothesis in current goal} + +\item {\tt intros until {\num}} \tacindex{intros until} + + This repeats {\tt intro} until the {\num}-th non-dependent product. For + instance, on the subgoal % + \verb+forall x y:nat, x=y -> y=x+ the tactic \texttt{intros until 1} + is equivalent to \texttt{intros x y H}, as \verb+x=y -> y=x+ is the + first non-dependent product. And on the subgoal % + \verb+forall x y z:nat, x=y -> y=x+ the tactic \texttt{intros until 1} + is equivalent to \texttt{intros x y z} as the product on \texttt{z} + can be rewritten as a non-dependent product: % + \verb+forall x y:nat, nat -> x=y -> y=x+ + + + \ErrMsg \errindex{No such hypothesis in current goal} + + This happens when {\num} is 0 or is greater than the number of non-dependent + products of the goal. + +\item {\tt intro after \ident} \tacindex{intro after}\\ + {\tt intro before \ident} \tacindex{intro before}\\ + {\tt intro at top} \tacindex{intro at top}\\ + {\tt intro at bottom} \tacindex{intro at bottom} + + These tactics apply {\tt intro} and move the freshly introduced hypothesis + respectively after the hypothesis \ident{}, before the hypothesis + \ident{}, at the top of the local context, or at the bottom of the + local context. All hypotheses on which the new hypothesis depends + are moved too so as to respect the order of dependencies between + hypotheses. Note that {\tt intro at bottom} is a synonym for {\tt + intro} with no argument. + + \ErrMsg \errindex{No such hypothesis} : {\ident} + +\item {\tt intro \ident$_1$ after \ident$_2$}\\ + {\tt intro \ident$_1$ before \ident$_2$}\\ + {\tt intro \ident$_1$ at top}\\ + {\tt intro \ident$_1$ at bottom} + + These tactics behave as previously but naming the introduced hypothesis + \ident$_1$. It is equivalent to {\tt intro \ident$_1$} followed by + the appropriate call to {\tt move}~(see Section~\ref{move}). + +\end{Variants} + +\subsection{\tt intros {\intropatternlist}} +\label{intros-pattern} +\tacindex{intros \intropattern} +\index{Introduction patterns} +\index{Naming introduction patterns} +\index{Disjunctive/conjunctive introduction patterns} +\index{Disjunctive/conjunctive introduction patterns} +\index{Equality introduction patterns} + +This extension of the tactic {\tt intros} allows to apply tactics on +the fly on the variables or hypotheses which have been introduced. An +{\em introduction pattern list} {\intropatternlist} is a list of +introduction patterns possibly containing the filling introduction +patterns {\tt *} and {\tt **}. An {\em introduction pattern} is +either: +\begin{itemize} +\item a {\em naming introduction pattern}, i.e. either one of: + \begin{itemize} + \item the pattern \texttt{?} + \item the pattern \texttt{?\ident} + \item an identifier + \end{itemize} +\item an {\em action introduction pattern} which itself classifies into: + \begin{itemize} + \item a {\em disjunctive/conjunctive introduction pattern}, i.e. either one of: + \begin{itemize} + \item a disjunction of lists of patterns: + {\tt [$\intropatternlist_1$ | \dots\ | $\intropatternlist_n$]} + \item a conjunction of patterns: {\tt ($p_1$ , \dots\ , $p_n$)} + \item a list of patterns {\tt ($p_1$ \&\ \dots\ \&\ $p_n$)} + for sequence of right-associative binary constructs + \end{itemize} + \item an {\em equality introduction pattern}, i.e. either one of: + \begin{itemize} + \item a pattern for decomposing an equality: {\tt [= $p_1$ \dots\ $p_n$]} + \item the rewriting orientations: {\tt ->} or {\tt <-} + \end{itemize} + \item the on-the-fly application of lemmas: $p${\tt \%{\term$_1$}} + \ldots {\tt \%{\term$_n$}} where $p$ itself is not a pattern for + on-the-fly application of lemmas (note: syntax is in experimental stage) + \end{itemize} +\item the wildcard: {\tt \_} +\end{itemize} + +Assuming a goal of type $Q \to P$ (non-dependent product), or +of type $\forall x:T,~P$ (dependent product), the behavior of +{\tt intros $p$} is defined inductively over the structure of the +introduction pattern~$p$: +\begin{itemize} +\item introduction on \texttt{?} performs the introduction, and lets {\Coq} + choose a fresh name for the variable; +\item introduction on \texttt{?\ident} performs the introduction, and + lets {\Coq} choose a fresh name for the variable based on {\ident}; +\item introduction on \texttt{\ident} behaves as described in + Section~\ref{intro}; +\item introduction over a disjunction of list of patterns {\tt + [$\intropatternlist_{1}$ | \dots\ | $\intropatternlist_n$]} expects + the product to be over an inductive type whose number of + constructors is $n$ (or more generally over a type of conclusion an + inductive type built from $n$ constructors, e.g. {\tt C -> + A\textbackslash/B} with $n=2$ since {\tt A\textbackslash/B} has 2 + constructors): it destructs the introduced hypothesis as {\tt + destruct} (see Section~\ref{destruct}) would and applies on each + generated subgoal the corresponding tactic; + \texttt{intros}~$\intropatternlist_i$. The introduction patterns in + $\intropatternlist_i$ are expected to consume no more than the + number of arguments of the $i^{\mbox{\scriptsize th}}$ + constructor. If it consumes less, then {\Coq} completes the pattern + so that all the arguments of the constructors of the inductive type + are introduced (for instance, the list of patterns {\tt [$\;$|$\;$] + H} applied on goal {\tt forall x:nat, x=0 -> 0=x} behaves the same + as the list of patterns {\tt [$\,$|$\,$?$\,$] H}); +\item introduction over a conjunction of patterns {\tt ($p_1$, \ldots, + $p_n$)} expects the goal to be a product over an inductive type $I$ with a + single constructor that itself has at least $n$ arguments: it + performs a case analysis over the hypothesis, as {\tt destruct} + would, and applies the patterns $p_1$~\ldots~$p_n$ to the arguments + of the constructor of $I$ (observe that {\tt ($p_1$, {\ldots}, + $p_n$)} is an alternative notation for {\tt [$p_1$ {\ldots} + $p_n$]}); +\item introduction via {\tt ($p_1$ \& \dots\ \& $p_n$)} + is a shortcut for introduction via + {\tt ($p_1$,(\ldots,(\dots,$p_n$)\ldots))}; it expects the + hypothesis to be a sequence of right-associative binary inductive + constructors such as {\tt conj} or {\tt ex\_intro}; for instance, an + hypothesis with type {\tt A\verb|/\|(exists x, B\verb|/\|C\verb|/\|D)} can be + introduced via pattern {\tt (a \& x \& b \& c \& d)}; +\item if the product is over an equality type, then a pattern of the + form {\tt [= $p_{1}$ \dots\ $p_n$]} applies either {\tt injection} + (see Section~\ref{injection}) or {\tt discriminate} (see + Section~\ref{discriminate}) instead of {\tt destruct}; if {\tt + injection} is applicable, the patterns $p_1$, \ldots, $p_n$ are + used on the hypotheses generated by {\tt injection}; if the number + of patterns is smaller than the number of hypotheses generated, the + pattern \texttt{?} is used to complete the list; + %TODO! + %if {\tt discriminate} is applicable, the list of patterns $p_{1}$ + %\dots\ $p_n$ is supposed to be empty; +\item introduction over {\tt ->} (respectively {\tt <-}) expects the + hypothesis to be an equality and the right-hand-side (respectively + the left-hand-side) is replaced by the left-hand-side (respectively + the right-hand-side) in the conclusion of the goal; the hypothesis + itself is erased; if the term to substitute is a variable, it is + substituted also in the context of goal and the variable is removed + too; +\item introduction over a pattern $p${\tt \%{\term$_1$}} \ldots {\tt + \%{\term$_n$}} first applies {\term$_1$},\ldots, {\term$_n$} on the + hypothesis to be introduced (as in {\tt apply }{\term}$_1$, \ldots, + {\term}$_n$ {\tt in}) prior to the application of the introduction + pattern $p$; +\item introduction on the wildcard depends on whether the product is + dependent or not: in the non-dependent case, it erases the + corresponding hypothesis (i.e. it behaves as an {\tt intro} followed + by a {\tt clear}, cf Section~\ref{clear}) while in the dependent + case, it succeeds and erases the variable only if the wildcard is + part of a more complex list of introduction patterns that also + erases the hypotheses depending on this variable; +\item introduction over {\tt *} introduces all forthcoming quantified + variables appearing in a row; introduction over {\tt **} introduces + all forthcoming quantified variables or hypotheses until the goal is + not any more a quantification or an implication. +\end{itemize} + +\Example + +\begin{coq_example} +Goal forall A B C:Prop, A \/ B /\ C -> (A -> C) -> C. +intros * [a | (_,c)] f. +\end{coq_example} +\begin{coq_eval} +Abort. +\end{coq_eval} + +\Rem {\tt intros $p_1~\ldots~p_n$} is not equivalent to \texttt{intros + $p_1$;\ldots; intros $p_n$} for the following reason: If one of the +$p_i$ is a wildcard pattern, he might succeed in the first case +because the further hypotheses it depends in are eventually erased too +while it might fail in the second case because of dependencies in +hypotheses which are not yet introduced (and a fortiori not yet +erased). + +\Rem In {\tt intros $\intropatternlist$}, if the last introduction +pattern is a disjunctive or conjunctive pattern {\tt + [$\intropatternlist_1$ | \dots\ | $\intropatternlist_n$]}, the +completion of $\intropatternlist_i$ so that all the arguments of the +$i^{\mbox{\scriptsize th}}$ constructors of the corresponding +inductive type are introduced can be controlled with the +following option: +\optindex{Bracketing Last Introduction Pattern} + +\begin{quote} +{\tt Set Bracketing Last Introduction Pattern} +\end{quote} + +Force completion, if needed, when the last introduction pattern is a +disjunctive or conjunctive pattern (this is the default). + +\begin{quote} +{\tt Unset Bracketing Last Introduction Pattern} +\end{quote} + +Deactivate completion when the last introduction pattern is a disjunctive +or conjunctive pattern. + + + +\subsection{\tt clear \ident} +\tacindex{clear} +\label{clear} + +This tactic erases the hypothesis named {\ident} in the local context +of the current goal. As a consequence, {\ident} is no more displayed and no more +usable in the proof development. + +\begin{ErrMsgs} +\item \errindex{No such hypothesis} +\item \errindexbis{{\ident} is used in the conclusion}{is used in the + conclusion} +\item \errindexbis{{\ident} is used in the hypothesis {\ident'}}{is + used in the hypothesis} +\end{ErrMsgs} + +\begin{Variants} + +\item {\tt clear {\ident$_1$} \dots\ {\ident$_n$}} + + This is equivalent to {\tt clear {\ident$_1$}. {\ldots} clear + {\ident$_n$}.} + +\item {\tt clearbody {\ident}}\tacindex{clearbody} + + This tactic expects {\ident} to be a local definition then clears + its body. Otherwise said, this tactic turns a definition into an + assumption. + + \ErrMsg \errindexbis{{\ident} is not a local definition}{is not a local definition} + +\item \texttt{clear - {\ident$_1$} \dots\ {\ident$_n$}} + + This tactic clears all the hypotheses except the ones depending in + the hypotheses named {\ident$_1$} {\ldots} {\ident$_n$} and in the + goal. + +\item \texttt{clear} + + This tactic clears all the hypotheses except the ones the goal depends on. + +\item {\tt clear dependent \ident \tacindex{clear dependent}} + + This clears the hypothesis \ident\ and all the hypotheses + that depend on it. + +\end{Variants} + +\subsection{\tt revert \ident$_1$ \dots\ \ident$_n$} +\tacindex{revert} +\label{revert} + +This applies to any goal with variables \ident$_1$ \dots\ \ident$_n$. +It moves the hypotheses (possibly defined) to the goal, if this respects +dependencies. This tactic is the inverse of {\tt intro}. + +\begin{ErrMsgs} +\item \errindex{No such hypothesis} +\item \errindexbis{{\ident} is used in the hypothesis {\ident'}}{is + used in the hypothesis} +\end{ErrMsgs} + +\begin{Variants} +\item {\tt revert dependent \ident \tacindex{revert dependent}} + + This moves to the goal the hypothesis {\ident} and all the hypotheses + that depend on it. + +\end{Variants} + +\subsection{\tt move {\ident$_1$} after {\ident$_2$}} +\tacindex{move} +\label{move} + +This moves the hypothesis named {\ident$_1$} in the local context +after the hypothesis named {\ident$_2$}, where ``after'' is in +reference to the direction of the move. The proof term is not changed. + +If {\ident$_1$} comes before {\ident$_2$} in the order of +dependencies, then all the hypotheses between {\ident$_1$} and +{\ident$_2$} that (possibly indirectly) depend on {\ident$_1$} are +moved too, and all of them are thus moved after {\ident$_2$} in the +order of dependencies. + +If {\ident$_1$} comes after {\ident$_2$} in the order of dependencies, +then all the hypotheses between {\ident$_1$} and {\ident$_2$} that +(possibly indirectly) occur in the type of {\ident$_1$} are moved +too, and all of them are thus moved before {\ident$_2$} in the order +of dependencies. + +\begin{Variants} + +\item {\tt move {\ident$_1$} before {\ident$_2$}} + +This moves {\ident$_1$} towards and just before the hypothesis named +{\ident$_2$}. As for {\tt move {\ident$_1$} after {\ident$_2$}}, +dependencies over {\ident$_1$} (when {\ident$_1$} comes before +{\ident$_2$} in the order of dependencies) or in the type of +{\ident$_1$} (when {\ident$_1$} comes after {\ident$_2$} in the order +of dependencies) are moved too. + +\item {\tt move {\ident} at top} + +This moves {\ident} at the top of the local context (at the beginning of the context). + +\item {\tt move {\ident} at bottom} + +This moves {\ident} at the bottom of the local context (at the end of the context). + +\end{Variants} + +\begin{ErrMsgs} + +\item \errindex{No such hypothesis} + +\item \errindex{Cannot move {\ident$_1$} after {\ident$_2$}: + it occurs in the type of {\ident$_2$}} + +\item \errindex{Cannot move {\ident$_1$} after {\ident$_2$}: + it depends on {\ident$_2$}} + +\end{ErrMsgs} + +\Example + +\begin{coq_example} +Goal forall x :nat, x = 0 -> forall z y:nat, y=y-> 0=x. +intros x H z y H0. +move x after H0. +Undo. +move x before H0. +Undo. +move H0 after H. +Undo. +move H0 before H. +\end{coq_example} +\begin{coq_eval} +Abort. +\end{coq_eval} + +\subsection{\tt rename {\ident$_1$} into {\ident$_2$}} +\tacindex{rename} + +This renames hypothesis {\ident$_1$} into {\ident$_2$} in the current +context. The name of the hypothesis in the proof-term, however, is left +unchanged. + +\begin{Variants} + +\item {\tt rename {\ident$_1$} into {\ident$_2$}, \ldots, + {\ident$_{2k-1}$} into {\ident$_{2k}$}} + +This renames the variables {\ident$_1$} \ldots {\ident$_2k-1$} into respectively +{\ident$_2$} \ldots {\ident$_2k$} in parallel. In particular, the target +identifiers may contain identifiers that exist in the source context, as long +as the latter are also renamed by the same tactic. + +\end{Variants} + +\begin{ErrMsgs} +\item \errindex{No such hypothesis} +\item \errindexbis{{\ident$_2$} is already used}{is already used} +\end{ErrMsgs} + +\subsection{\tt set ( {\ident} := {\term} )} +\label{tactic:set} +\tacindex{set} + +This replaces {\term} by {\ident} in the conclusion of the current goal +and adds the new definition {\tt {\ident} := \term} to the local context. + +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{ErrMsgs} +\item \errindex{The variable {\ident} is already defined} +\end{ErrMsgs} + +\begin{Variants} + +\item {\tt set ( {\ident} := {\term} ) in {\occgoalset}} + +This notation allows specifying which occurrences of {\term} have to +be substituted in the context. The {\tt in {\occgoalset}} clause is an +occurrence clause whose syntax and behavior are described in +Section~\ref{Occurrences_clauses}. + +\item {\tt set ( {\ident} \nelistnosep{\binder} := {\term} )} + + This is equivalent to {\tt set ( {\ident} := fun + \nelistnosep{\binder} => {\term} )}. + +\item {\tt set \term} + + This behaves as {\tt set (} {\ident} := {\term} {\tt )} but {\ident} + is generated by {\Coq}. This variant also supports an occurrence clause. + +\item {\tt set ( {\ident$_0$} \nelistnosep{\binder} := {\term} ) in {\occgoalset}}\\ + {\tt set {\term} in {\occgoalset}} + + These are the general forms that combine the previous possibilities. + +\item {\tt eset ( {\ident$_0$} \nelistnosep{\binder} := {\term} ) in {\occgoalset}}\tacindex{eset}\\ + {\tt eset {\term} in {\occgoalset}} + + While the different variants of \texttt{set} expect that no + existential variables are generated by the tactic, \texttt{eset} + removes this constraint. In practice, this is relevant only when + \texttt{eset} is used as a synonym of \texttt{epose}, i.e. when the + term does not occur in the goal. + +\item {\tt remember {\term} as {\ident}}\tacindex{remember} + + This behaves as {\tt set ( {\ident} := {\term} ) in *} and using a + logical (Leibniz's) equality instead of a local definition. + +\item {\tt remember {\term} as {\ident} eqn:{\ident}} + + This behaves as {\tt remember {\term} as {\ident}}, except + that the name of the generated equality is also given. + +\item {\tt remember {\term} as {\ident} in {\occgoalset}} + + This is a more general form of {\tt remember} that remembers the + occurrences of {\term} specified by an occurrences set. + +\item + {\tt eremember {\term} as {\ident}}\tacindex{eremember}\\ + {\tt eremember {\term} as {\ident} in {\occgoalset}}\\ + {\tt eremember {\term} as {\ident} eqn:{\ident}} + + While the different variants of \texttt{remember} expect that no + existential variables are generated by the tactic, \texttt{eremember} + removes this constraint. + +\item {\tt pose ( {\ident} := {\term} )}\tacindex{pose} + + This adds the local definition {\ident} := {\term} to the current + context without performing any replacement in the goal or in the + hypotheses. It is equivalent to {\tt set ( {\ident} {\tt :=} + {\term} {\tt ) in |-}}. + +\item {\tt pose ( {\ident} \nelistnosep{\binder} := {\term} )} + + This is equivalent to {\tt pose (} {\ident} {\tt :=} {\tt fun} + \nelistnosep{\binder} {\tt =>} {\term} {\tt )}. + +\item{\tt pose {\term}} + + This behaves as {\tt pose ( {\ident} := {\term} )} but + {\ident} is generated by {\Coq}. + +\item {\tt epose ( {\ident} := {\term} )}\tacindex{epose}\\ + {\tt epose ( {\ident} \nelistnosep{\binder} := {\term} )}\\ + {\tt epose {\term}} + + While the different variants of \texttt{pose} expect that no + existential variables are generated by the tactic, \texttt{epose} + removes this constraint. + +\end{Variants} + +\subsection{\tt decompose [ {\qualid$_1$} \dots\ {\qualid$_n$} ] \term} +\label{decompose} +\tacindex{decompose} + +This tactic recursively decomposes a +complex proposition in order to obtain atomic ones. + +\Example + +\begin{coq_eval} +Reset Initial. +\end{coq_eval} +\begin{coq_example} +Goal forall A B C:Prop, A /\ B /\ C \/ B /\ C \/ C /\ A -> C. +intros A B C H; decompose [and or] H; assumption. +\end{coq_example} +\begin{coq_example*} +Qed. +\end{coq_example*} + +{\tt decompose} does not work on right-hand sides of implications or products. + +\begin{Variants} + +\item {\tt decompose sum \term}\tacindex{decompose sum} + + This decomposes sum types (like \texttt{or}). + +\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 Section~\ref{Record}). + +\end{Variants} + +\section{Controlling the proof flow} + +\subsection{\tt assert ( {\ident} :\ {\form} )} +\tacindex{assert} + +This tactic applies to any goal. {\tt assert (H : U)} adds a new +hypothesis of name \texttt{H} asserting \texttt{U} to the current goal +and opens a new subgoal \texttt{U}\footnote{This corresponds to the + cut rule of sequent calculus.}. The subgoal {\texttt U} comes first +in the list of subgoals remaining to prove. + +\begin{ErrMsgs} +\item \errindex{Not a proposition or a type} + + Arises when the argument {\form} is neither of type {\tt Prop}, {\tt + Set} nor {\tt Type}. + +\end{ErrMsgs} + +\begin{Variants} + +\item{\tt assert {\form}} + + This behaves as {\tt assert ( {\ident} :\ {\form} )} but + {\ident} is generated by {\Coq}. + +\item \texttt{assert {\form} by {\tac}}\tacindex{assert by} + + This tactic behaves like \texttt{assert} but applies {\tac} + to solve the subgoals generated by \texttt{assert}. + + \ErrMsg \errindex{Proof is not complete} + +\item \texttt{assert {\form} as {\intropattern}\tacindex{assert as}} + + If {\intropattern} is a naming introduction pattern (see + Section~\ref{intros-pattern}), the hypothesis is named after this + introduction pattern (in particular, if {\intropattern} is {\ident}, + the tactic behaves like \texttt{assert ({\ident} :\ {\form})}). + + If {\intropattern} is an action introduction pattern, the tactic + behaves like \texttt{assert {\form}} followed by the action done by + this introduction pattern. + +\item \texttt{assert {\form} as {\intropattern} by {\tac}} + + This combines the two previous variants of {\tt assert}. + +\item{\tt assert ( {\ident} := {\term} )} + + This behaves as {\tt assert ({\ident} :\ {\type}) by exact {\term}} + where {\type} is the type of {\term}. This is deprecated in favor of + {\tt pose proof}. + + If the head of {\term} is {\ident}, the tactic behaves as + {\tt specialize \term}. + + \ErrMsg \errindex{Variable {\ident} is already declared} + +\item \texttt{eassert {\form} as {\intropattern} by {\tac}}\tacindex{eassert}\tacindex{eassert as}\tacindex{eassert by}\\ + {\tt assert ( {\ident} := {\term} )} + + While the different variants of \texttt{assert} expect that no + existential variables are generated by the tactic, \texttt{eassert} + removes this constraint. This allows not to specify the asserted + statement completely before starting to prove it. + +\item \texttt{pose proof {\term} \zeroone{as {\intropattern}}\tacindex{pose proof}} + + This tactic behaves like \texttt{assert T \zeroone{as {\intropattern}} by + exact {\term}} where \texttt{T} is the type of {\term}. + + In particular, \texttt{pose proof {\term} as {\ident}} behaves as + \texttt{assert ({\ident} := {\term})} and \texttt{pose proof {\term} + as {\intropattern}} is the same as applying + the {\intropattern} to {\term}. + +\item \texttt{epose proof {\term} \zeroone{as {\intropattern}}\tacindex{epose proof}} + + While \texttt{pose proof} expects that no existential variables are generated by the tactic, + \texttt{epose proof} removes this constraint. + +\item \texttt{enough ({\ident} :\ {\form})}\tacindex{enough} + + This adds a new hypothesis of name {\ident} asserting {\form} to the + goal the tactic \texttt{enough} is applied to. A new subgoal stating + \texttt{\form} is inserted after the initial goal rather than before + it as \texttt{assert} would do. + +\item \texttt{enough {\form}}\tacindex{enough} + + This behaves like \texttt{enough ({\ident} :\ {\form})} with the name + {\ident} of the hypothesis generated by {\Coq}. + +\item \texttt{enough {\form} as {\intropattern}\tacindex{enough as}} + + This behaves like \texttt{enough} {\form} using {\intropattern} to + name or destruct the new hypothesis. + +\item \texttt{enough ({\ident} :\ {\form}) by {\tac}}\tacindex{enough by}\\ + \texttt{enough {\form} by {\tac}}\tacindex{enough by}\\ + \texttt{enough {\form} as {\intropattern} by {\tac}} + + This behaves as above but with {\tac} expected to solve the initial + goal after the extra assumption {\form} is added and possibly + destructed. If the \texttt{as} {\intropattern} clause generates more + than one subgoal, {\tac} is applied to all of them. + +\item \texttt{eenough ({\ident} :\ {\form}) by {\tac}}\tacindex{eenough}\tacindex{eenough as}\tacindex{eenough by}\\ + \texttt{eenough {\form} by {\tac}}\tacindex{enough by}\\ + \texttt{eenough {\form} as {\intropattern} by {\tac}} + + While the different variants of \texttt{enough} expect that no + existential variables are generated by the tactic, \texttt{eenough} + removes this constraint. + +\item {\tt cut {\form}}\tacindex{cut} + + This tactic applies to any goal. It implements the non-dependent + case of the ``App''\index{Typing rules!App} rule given in + Section~\ref{Typed-terms}. (This is Modus Ponens inference rule.) + {\tt cut U} transforms the current goal \texttt{T} into the two + following subgoals: {\tt U -> T} and \texttt{U}. The subgoal {\tt U + -> T} comes first in the list of remaining subgoal to prove. + +\item {\tt specialize ({\ident} \term$_1$ \dots\ \term$_n$)\tacindex{specialize} \zeroone{as \intropattern}}\\ + {\tt specialize {\ident} with {\bindinglist} \zeroone{as \intropattern}} + + The tactic {\tt specialize} works on local hypothesis \ident. + The premises of this hypothesis (either universal + quantifications or non-dependent implications) are instantiated + by concrete terms coming either from arguments \term$_1$ + $\ldots$ \term$_n$ or from a bindings list (see + Section~\ref{Binding-list} for more about bindings lists). + In the first form the application to \term$_1$ {\ldots} + \term$_n$ can be partial. The first form is equivalent to + {\tt assert ({\ident} := {\ident} {\term$_1$} \dots\ \term$_n$)}. + + In the second form, instantiation elements can also be partial. + In this case the uninstantiated arguments are inferred by + unification if possible or left quantified in the hypothesis + otherwise. + + With the {\tt as} clause, the local hypothesis {\ident} is left + unchanged and instead, the modified hypothesis is introduced as + specified by the {\intropattern}. + + The name {\ident} can also refer to a global lemma or + hypothesis. In this case, for compatibility reasons, the + behavior of {\tt specialize} is close to that of {\tt + generalize}: the instantiated statement becomes an additional + premise of the goal. The {\tt as} clause is especially useful + in this case to immediately introduce the instantiated statement + as a local hypothesis. + + \begin{ErrMsgs} + \item \errindexbis{{\ident} is used in hypothesis \ident'}{is used in hypothesis} + \item \errindexbis{{\ident} is used in conclusion}{is used in conclusion} + \end{ErrMsgs} + +%% Moreover, the old syntax allows the use of a number after {\tt specialize} +%% for controlling the number of premises to instantiate. Giving this +%% number should not be mandatory anymore (automatic detection of how +%% many premises can be eaten without leaving meta-variables). Hence +%% no documentation for this integer optional argument of specialize + +\end{Variants} + +\subsection{\tt generalize \term} +\tacindex{generalize} +\label{generalize} + +This tactic applies to any goal. It generalizes the conclusion with +respect to some term. + +\Example + +\begin{coq_eval} +Goal forall x y:nat, (0 <= x + y + y). +intros. +\end{coq_eval} +\begin{coq_example} +Show. +generalize (x + y + y). +\end{coq_example} + +\begin{coq_eval} +Abort. +\end{coq_eval} + +If the goal is $G$ and $t$ is a subterm of type $T$ in the goal, then +{\tt generalize} \textit{t} replaces the goal by {\tt forall (x:$T$), $G'$} +where $G'$ is obtained from $G$ by replacing all occurrences of $t$ by +{\tt x}. The name of the variable (here {\tt n}) is chosen based on $T$. + +\begin{Variants} +\item {\tt generalize {\term$_1$ , \dots\ , \term$_n$}} + + This is equivalent to {\tt generalize \term$_n$; \dots\ ; generalize + \term$_1$}. Note that the sequence of \term$_i$'s are processed + from $n$ to $1$. + +\item {\tt generalize {\term} at {\num$_1$ \dots\ \num$_i$}} + + This is equivalent to {\tt generalize \term} but it generalizes only over + the specified occurrences of {\term} (counting from left to right on the + expression printed using option {\tt Set Printing All}). + +\item {\tt generalize {\term} as {\ident}} + + This is equivalent to {\tt generalize \term} but it uses {\ident} to name the + generalized hypothesis. + +\item {\tt generalize {\term$_1$} at {\num$_{11}$ \dots\ \num$_{1i_1}$} + as {\ident$_1$} + , {\ldots} , + {\term$_n$} at {\num$_{n1}$ \mbox{\dots} \num$_{ni_n}$} + as {\ident$_2$}} + + This is the most general form of {\tt generalize} that combines the + previous behaviors. + +\item {\tt generalize dependent \term} \tacindex{generalize dependent} + + This generalizes {\term} but also {\em all} hypotheses that depend + on {\term}. It clears the generalized hypotheses. + +\end{Variants} + +\subsection{\tt evar ( {\ident} :\ {\term} )} +\tacindex{evar} +\label{evar} + +The {\tt evar} tactic creates a new local definition named \ident\ with +type \term\ in the context. The body of this binding is a fresh +existential variable. + +\subsection{\tt instantiate ( {\ident} := {\term} )} +\tacindex{instantiate} +\label{instantiate} + +The {\tt instantiate} tactic refines (see Section~\ref{refine}) +an existential variable {\ident} with the term {\term}. +It is equivalent to {\tt only [\ident]: refine \term} (preferred alternative). + +\begin{Remarks} +\item To be able to refer to an existential variable by name, the +user must have given the name explicitly (see~\ref{ExistentialVariables}). + +\item When you are referring to hypotheses which you did not name +explicitly, be aware that Coq may make a different decision on how to +name the variable in the current goal and in the context of the +existential variable. This can lead to surprising behaviors. +\end{Remarks} + +\begin{Variants} + + \item {\tt instantiate ( {\num} := {\term} )} + This variant allows to refer to an existential variable which was not + named by the user. The {\num} argument is the position of the + existential variable from right to left in the goal. + Because this variant is not robust to slight changes in the goal, + its use is strongly discouraged. + + \item {\tt instantiate ( {\num} := {\term} ) in \ident} + + \item {\tt instantiate ( {\num} := {\term} ) in ( Value of {\ident} )} + + \item {\tt instantiate ( {\num} := {\term} ) in ( Type of {\ident} )} + +These allow to refer respectively to existential variables occurring in +a hypothesis or in the body or the type of a local definition. + + \item {\tt instantiate} + + Without argument, the {\tt instantiate} tactic tries to solve as + many existential variables as possible, using information gathered + from other tactics in the same tactical. This is automatically + done after each complete tactic (i.e. after a dot in proof mode), + but not, for example, between each tactic when they are sequenced + by semicolons. + +\end{Variants} + +\subsection{\tt admit} +\tacindex{admit} +\tacindex{give\_up} +\label{admit} + +The {\tt admit} tactic allows temporarily skipping a subgoal so as to +progress further in the rest of the proof. A proof containing +admitted goals cannot be closed with {\tt Qed} but only with +{\tt Admitted}. + +\begin{Variants} + + \item {\tt give\_up} + + Synonym of {\tt admit}. + +\end{Variants} + +\subsection{\tt absurd \term} +\tacindex{absurd} +\label{absurd} + +This tactic applies to any goal. The argument {\term} is any +proposition {\tt P} of type {\tt Prop}. This tactic applies {\tt + False} elimination, that is it deduces the current goal from {\tt + False}, and generates as subgoals {\tt $\sim$P} and {\tt P}. It is +very useful in proofs by cases, where some cases are impossible. In +most cases, \texttt{P} or $\sim$\texttt{P} is one of the hypotheses of +the local context. + +\subsection{\tt contradiction} +\label{contradiction} +\tacindex{contradiction} + +This tactic applies to any goal. The {\tt contradiction} tactic +attempts to find in the current context (after all {\tt intros}) an +hypothesis that is equivalent to an empty inductive type (e.g. {\tt + False}), to the negation of a singleton inductive type (e.g. {\tt + True} or {\tt x=x}), or two contradictory hypotheses. + +\begin{ErrMsgs} +\item \errindex{No such assumption} +\end{ErrMsgs} + +\begin{Variants} +\item {\tt contradiction \ident} + +The proof of {\tt False} is searched in the hypothesis named \ident. +\end{Variants} + +\subsection{\tt contradict \ident} +\label{contradict} +\tacindex{contradict} + +This tactic allows manipulating negated hypothesis and goals. The +name \ident\ should correspond to a hypothesis. With +{\tt contradict H}, the current goal and context is transformed in +the following way: +\begin{itemize} +\item {\tt H:$\neg$A $\vd$ B} \ becomes \ {\tt $\vd$ A} +\item {\tt H:$\neg$A $\vd$ $\neg$B} \ becomes \ {\tt H: B $\vd$ A } +\item {\tt H: A $\vd$ B} \ becomes \ {\tt $\vd$ $\neg$A} +\item {\tt H: A $\vd$ $\neg$B} \ becomes \ {\tt H: B $\vd$ $\neg$A} +\end{itemize} + +\subsection{\tt exfalso} +\label{exfalso} +\tacindex{exfalso} + +This tactic implements the ``ex falso quodlibet'' logical principle: +an elimination of {\tt False} is performed on the current goal, and the +user is then required to prove that {\tt False} is indeed provable in +the current context. This tactic is a macro for {\tt elimtype False}. + +\section{Case analysis and induction} + +The tactics presented in this section implement induction or case +analysis on inductive or co-inductive objects (see +Section~\ref{Cic-inductive-definitions}). + +\subsection{\tt destruct \term} +\tacindex{destruct} +\label{destruct} + +This tactic applies to any goal. The argument {\term} must be of +inductive or co-inductive type and the tactic generates subgoals, one +for each possible form of {\term}, i.e. one for each constructor of +the inductive or co-inductive type. Unlike {\tt induction}, no +induction hypothesis is generated by {\tt destruct}. + +There are special cases: + +\begin{itemize} + +\item If {\term} is an identifier {\ident} denoting a quantified + variable of the conclusion of the goal, then {\tt destruct {\ident}} + behaves as {\tt intros until {\ident}; destruct {\ident}}. If + {\ident} is not anymore dependent in the goal after application of + {\tt destruct}, it is erased (to avoid erasure, use + parentheses, as in {\tt 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. Remark: For destruction of a numeral, use +syntax {\tt destruct ({\num})} (not very interesting anyway). + +\item In case {\term} is an hypothesis {\ident} of the context, + and {\ident} is not anymore dependent in the goal after + application of {\tt destruct}, it is erased (to avoid erasure, use + parentheses, as in {\tt destruct ({\ident})}). + +\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} + +\begin{Variants} +\item{\tt destruct \term$_1$, \ldots, \term$_n$} + + This is a shortcut for {\tt destruct \term$_1$; \ldots; destruct \term$_n$}. + +\item{\tt destruct {\term} as {\disjconjintropattern}} + + This behaves as {\tt destruct {\term}} but uses the names in + {\intropattern} to name the variables introduced in the context. + The {\intropattern} must have the form {\tt [} $p_{11}$ \ldots + $p_{1n_1}$ {\tt |} {\ldots} {\tt |} $p_{m1}$ \ldots $p_{mn_m}$ + {\tt ]} with $m$ being the number of constructors of the type of + {\term}. Each variable introduced by {\tt destruct} in the context + of the $i^{th}$ goal gets its name from the list $p_{i1}$ \ldots + $p_{in_i}$ in order. If there are not enough names, {\tt destruct} + invents names for the remaining variables to introduce. More + generally, the $p_{ij}$ can be any introduction pattern (see + Section~\ref{intros-pattern}). This provides a concise notation for + chaining destruction of an hypothesis. + +% It is recommended to use this variant of {\tt destruct} for +% robust proof scripts. + +\item{\tt destruct {\term} eqn:{\namingintropattern}} + + This behaves as {\tt destruct {\term}} but adds an equation between + {\term} and the value that {\term} takes in each of the possible + cases. The name of the equation is specified by {\namingintropattern} + (see Section~\ref{intros-pattern}), in particular {\tt ?} can be + used to let Coq generate a fresh name. + +\item{\tt destruct {\term} with \bindinglist} + + This behaves like \texttt{destruct {\term}} providing explicit + instances for the dependent premises of the type of {\term} (see + syntax of bindings in Section~\ref{Binding-list}). + +\item{\tt edestruct {\term}\tacindex{edestruct}} + + This tactic behaves like \texttt{destruct {\term}} except that it + does not fail if the instance of a dependent premises of the type of + {\term} is not inferable. Instead, the unresolved instances are left + as existential variables to be inferred later, in the same way as + {\tt eapply} does (see Section~\ref{eapply-example}). + +\item{\tt destruct {\term$_1$} using {\term$_2$}}\\ + {\tt destruct {\term$_1$} using {\term$_2$} with {\bindinglist}} + + These are synonyms of {\tt induction {\term$_1$} using {\term$_2$}} and + {\tt induction {\term$_1$} using {\term$_2$} with {\bindinglist}}. + +\item \texttt{destruct {\term} in {\occgoalset}} + + This syntax is used for selecting which occurrences of {\term} the + case analysis has to be done on. The {\tt in {\occgoalset}} clause is an + occurrence clause whose syntax and behavior is described in + Section~\ref{Occurrences_clauses}. + +\item{\tt destruct {\term$_1$} with {\bindinglist$_1$} + as {\disjconjintropattern} eqn:{\namingintropattern} + using {\term$_2$} with {\bindinglist$_2$} in {\occgoalset}}\\ + {\tt edestruct {\term$_1$} with {\bindinglist$_1$} + as {\disjconjintropattern} eqn:{\namingintropattern} + using {\term$_2$} with {\bindinglist$_2$} in {\occgoalset}} + + These are the general forms of {\tt destruct} and {\tt edestruct}. + They combine the effects of the {\tt with}, {\tt as}, {\tt eqn:}, {\tt using}, + and {\tt in} clauses. + +\item{\tt case \term}\label{case}\tacindex{case} + + The tactic {\tt case} is a more basic tactic to perform case + analysis without recursion. It behaves as {\tt elim \term} but using + a case-analysis elimination principle and not a recursive one. + +\item {\tt case {\term} with {\bindinglist}} + + Analogous to {\tt elim {\term} with {\bindinglist}} above. + +\item{\tt ecase {\term}\tacindex{ecase}}\\ + {\tt ecase {\term} with {\bindinglist}} + + In case the type of {\term} has dependent premises, or dependent + premises whose values are not inferable from the {\tt with + {\bindinglist}} clause, {\tt ecase} turns them into existential + variables to be resolved later on. + +\item {\tt simple destruct \ident}\tacindex{simple destruct} + + This tactic behaves as {\tt intros until + {\ident}; case {\tt {\ident}}} when {\ident} is a quantified + variable of the goal. + +\item {\tt simple destruct {\num}} + + This tactic behaves as {\tt intros until + {\num}; case {\tt {\ident}}} where {\ident} is the name given by + {\tt intros until {\num}} to the {\num}-th non-dependent premise of + the goal. + +\item{\tt case\_eq \term}\label{case_eq}\tacindex{case\_eq} + + The tactic {\tt case\_eq} is a variant of the {\tt case} tactic that + allow to perform case analysis on a term without completely + forgetting its original form. This is done by generating equalities + between the original form of the term and the outcomes of the case + analysis. + +% The effect of this tactic is similar to the effect of {\tt +% destruct {\term} in |- *} with the exception that no new hypotheses +% are introduced in the context. + +\end{Variants} + +\subsection{\tt induction \term} +\tacindex{induction} +\label{Tac-induction} + +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. + +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: + +\begin{itemize} + +\item If {\term} is an identifier {\ident} denoting a quantified + variable of the conclusion of the goal, then {\tt induction + {\ident}} behaves as {\tt intros until {\ident}; induction + {\ident}}. If {\ident} is not anymore dependent in the goal + after application of {\tt induction}, it is erased (to avoid + erasure, use parentheses, as in {\tt 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. Remark: For simple induction on a numeral, +use syntax {\tt induction ({\num})} (not very interesting anyway). + +\item In case {\term} is an hypothesis {\ident} of the context, + and {\ident} is not anymore dependent in the goal after + application of {\tt induction}, it is erased (to avoid erasure, use + parentheses, as in {\tt induction ({\ident})}). + +\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} + +\Example + +\begin{coq_example} +Lemma induction_test : forall n:nat, n = n -> n <= n. +intros n H. +induction n. +\end{coq_example} + +\begin{ErrMsgs} +\item \errindex{Not an inductive product} +\item \errindex{Unable to find an instance for the variables +{\ident} \ldots {\ident}} + + Use in this case + the variant {\tt elim \dots\ with \dots} below. +\end{ErrMsgs} + +\begin{Variants} +\item{\tt induction {\term} as {\disjconjintropattern}} + + This behaves as {\tt induction {\term}} but uses the names in + {\disjconjintropattern} to name the variables introduced in the context. + The {\disjconjintropattern} must typically be of the form + {\tt [} $p_{11}$ {\ldots} + $p_{1n_1}$ {\tt |} {\ldots} {\tt |} $p_{m1}$ {\ldots} $p_{mn_m}$ {\tt + ]} with $m$ being the number of constructors of the type of + {\term}. Each variable introduced by {\tt induction} in the context + of the $i^{th}$ goal gets its name from the list $p_{i1}$ {\ldots} + $p_{in_i}$ in order. If there are not enough names, {\tt induction} + invents names for the remaining variables to introduce. More + generally, the $p_{ij}$ can be any disjunctive/conjunctive + introduction pattern (see Section~\ref{intros-pattern}). For instance, + for an inductive type with one constructor, the pattern notation + {\tt (}$p_{1}$ {\tt ,} {\ldots} {\tt ,} $p_{n}${\tt )} can be used instead of + {\tt [} $p_{1}$ {\ldots} $p_{n}$ {\tt ]}. + +%% \item{\tt induction {\term} eqn:{\namingintropattern}} + +%% This behaves as {\tt induction {\term}} but adds an equation between +%% {\term} and the value that {\term} takes in each of the induction +%% case. The name of the equation is built according to +%% {\namingintropattern} which can be an identifier, a ``?'', etc, as +%% indicated in Section~\ref{intros-pattern}. + +%% \item{\tt induction {\term} as {\disjconjintropattern} eqn:{\namingintropattern}} + +%% This combines the two previous forms. + +\item{\tt induction {\term} with \bindinglist} + + This behaves like \texttt{induction {\term}} providing explicit + instances for the premises of the type of {\term} (see the syntax of + bindings in Section~\ref{Binding-list}). + +\item{\tt einduction {\term}\tacindex{einduction}} + + This tactic behaves like \texttt{induction {\term}} excepts that it + does not fail if some dependent premise of the type of {\term} is + not inferable. Instead, the unresolved premises are posed as + existential variables to be inferred later, in the same way as {\tt + eapply} does (see Section~\ref{eapply-example}). + +\item {\tt induction {\term$_1$} using {\term$_2$}} + + This behaves as {\tt induction {\term$_1$}} but using {\term$_2$} as + induction scheme. It does not expect the conclusion of the type of + {\term$_1$} to be inductive. + +\item {\tt induction {\term$_1$} using {\term$_2$} with {\bindinglist}} + + This behaves as {\tt induction {\term$_1$} using {\term$_2$}} but + also providing instances for the premises of the type of {\term$_2$}. + +\item \texttt{induction {\term}$_1$, {\ldots}, {\term}$_n$ using {\qualid}} + + This syntax is used for the case {\qualid} denotes an induction principle + with complex predicates as the induction principles generated by + {\tt Function} or {\tt Functional Scheme} may be. + +\item \texttt{induction {\term} in {\occgoalset}} + + This syntax is used for selecting which occurrences of {\term} the + induction has to be carried on. The {\tt in \occgoalset} clause is + an occurrence clause whose syntax and behavior is described in + Section~\ref{Occurrences_clauses}. If variables or hypotheses not + mentioning {\term} in their type are listed in {\occgoalset}, those + are generalized as well in the statement to prove. + +\Example + +\begin{coq_example} +Lemma comm x y : x + y = y + x. +induction y in x |- *. +Show 2. +\end{coq_example} + +\item {\tt induction {\term$_1$} with {\bindinglist$_1$} + as {\disjconjintropattern} %% eqn:{\namingintropattern} + using {\term$_2$} with {\bindinglist$_2$} in {\occgoalset}}\\ + {\tt einduction {\term$_1$} with {\bindinglist$_1$} + as {\disjconjintropattern} %% eqn:{\namingintropattern} + using {\term$_2$} with {\bindinglist$_2$} in {\occgoalset}} + + These are the most general forms of {\tt induction} and {\tt + einduction}. It combines the effects of the {\tt with}, {\tt as}, %%{\tt eqn:}, + {\tt using}, and {\tt in} clauses. + +\item {\tt elim \term}\label{elim} + + This is a more basic induction tactic. Again, the type of the + argument {\term} must be an inductive type. Then, according to + the type of the goal, the tactic {\tt elim} chooses the appropriate + destructor and applies it as the tactic {\tt apply} + would do. For instance, if the proof context contains {\tt + n:nat} and the current goal is {\tt T} of type {\tt + Prop}, then {\tt elim n} is equivalent to {\tt apply nat\_ind with + (n:=n)}. The tactic {\tt elim} does not modify the context of + the goal, neither introduces the induction loading into the context + of hypotheses. + + More generally, {\tt elim \term} also works when the type of {\term} + is a statement with premises and whose conclusion is inductive. In + that case the tactic performs induction on the conclusion of the + type of {\term} and leaves the non-dependent premises of the type as + subgoals. In the case of dependent products, the tactic tries to + find an instance for which the elimination lemma applies and fails + otherwise. + +\item {\tt elim {\term} with {\bindinglist}} + + Allows to give explicit instances to the premises of the type + of {\term} (see Section~\ref{Binding-list}). + +\item{\tt eelim {\term}\tacindex{eelim}} + + In case the type of {\term} has dependent premises, this turns them into + existential variables to be resolved later on. + +\item{\tt elim {\term$_1$} using {\term$_2$}}\\ + {\tt elim {\term$_1$} using {\term$_2$} with {\bindinglist}\tacindex{elim \dots\ using}} + +Allows the user to give explicitly an elimination predicate +{\term$_2$} that is not the standard one for the underlying inductive +type of {\term$_1$}. The {\bindinglist} clause allows +instantiating premises of the type of {\term$_2$}. + +\item{\tt elim {\term$_1$} with {\bindinglist$_1$} using {\term$_2$} with {\bindinglist$_2$}}\\ + {\tt eelim {\term$_1$} with {\bindinglist$_1$} using {\term$_2$} with {\bindinglist$_2$}} + + These are the most general forms of {\tt elim} and {\tt eelim}. It + combines the effects of the {\tt using} clause and of the two uses + of the {\tt with} clause. + +\item {\tt elimtype \form}\tacindex{elimtype} + + The argument {\form} must be inductively defined. {\tt elimtype I} + is equivalent to {\tt cut I. intro H{\rm\sl n}; elim H{\rm\sl n}; + clear H{\rm\sl n}}. Therefore the hypothesis {\tt H{\rm\sl n}} will + not appear in the context(s) of the subgoal(s). Conversely, if {\tt + t} is a term of (inductive) type {\tt I} that does not occur + in the goal, then {\tt elim t} is equivalent to {\tt elimtype I; 2: + exact t.} + +\item {\tt simple induction \ident}\tacindex{simple induction} + + This tactic behaves as {\tt intros until + {\ident}; elim {\tt {\ident}}} when {\ident} is a quantified + variable of the goal. + +\item {\tt simple induction {\num}} + + This tactic behaves as {\tt intros until + {\num}; elim {\tt {\ident}}} where {\ident} is the name given by + {\tt intros until {\num}} to the {\num}-th non-dependent premise of + the goal. + +%% \item {\tt simple induction {\term}}\tacindex{simple induction} + +%% If {\term} is an {\ident} corresponding to a quantified variable of +%% the goal then the tactic behaves as {\tt intros until {\ident}; elim +%% {\tt {\ident}}}. If {\term} is a {\num} then the tactic behaves as +%% {\tt intros until {\ident}; elim {\tt {\ident}}}. Otherwise, it is +%% a synonym for {\tt elim {\term}}. + +%% \Rem For simple induction on a numeral, use syntax {\tt simple +%% induction ({\num})}. + +\end{Variants} + +%\subsection[\tt FixPoint \dots]{\tt FixPoint \dots\tacindex{Fixpoint}} +%Not yet documented. + +\subsection{\tt double induction \ident$_1$ \ident$_2$} +\tacindex{double induction} + +This tactic is deprecated and should be replaced by {\tt induction \ident$_1$; induction \ident$_2$} (or {\tt induction \ident$_1$; destruct \ident$_2$} depending on the exact needs). + +%% This tactic applies to any goal. If the variables {\ident$_1$} and +%% {\ident$_2$} of the goal have an inductive type, then this tactic +%% performs double induction on these variables. For instance, if the +%% current goal is \verb+forall n m:nat, P n m+ then, {\tt double induction n +%% m} yields the four cases with their respective inductive hypotheses. + +%% In particular, for proving \verb+(P (S n) (S m))+, the generated induction +%% hypotheses are \verb+(P (S n) m)+ and \verb+(m:nat)(P n m)+ (of the latter, +%% \verb+(P n m)+ and \verb+(P n (S m))+ are derivable). + +%% \Rem When the induction hypothesis \verb+(P (S n) m)+ is not +%% needed, {\tt induction \ident$_1$; destruct \ident$_2$} produces +%% more concise subgoals. + +\begin{Variant} + +\item {\tt double induction \num$_1$ \num$_2$} + +This tactic is deprecated and should be replaced by {\tt induction + \num$_1$; induction \num$_3$} where \num$_3$ is the result of +\num$_2$-\num$_1$. + +%% This applies double induction on the \num$_1^{th}$ and \num$_2^{th}$ {\it +%% non dependent} premises of the goal. More generally, any combination of an +%% {\ident} and a {\num} is valid. + +\end{Variant} + +\subsection{\tt dependent induction \ident} +\tacindex{dependent induction} +\label{DepInduction} + +The \emph{experimental} tactic \texttt{dependent induction} performs +induction-inversion on an instantiated inductive predicate. +One needs to first require the {\tt Coq.Program.Equality} module to use +this tactic. The tactic is based on the BasicElim tactic by Conor +McBride \cite{DBLP:conf/types/McBride00} and the work of Cristina Cornes +around inversion \cite{DBLP:conf/types/CornesT95}. From an instantiated +inductive predicate and a goal, it generates an equivalent goal where the +hypothesis has been generalized over its indexes which are then +constrained by equalities to be the right instances. This permits to +state lemmas without resorting to manually adding these equalities and +still get enough information in the proofs. + +\Example + +\begin{coq_eval} +Reset Initial. +\end{coq_eval} +\begin{coq_example} +Lemma le_minus : forall n:nat, n < 1 -> n = 0. +intros n H ; induction H. +\end{coq_example} + +Here we did not get any information on the indexes to help fulfill this +proof. The problem is that, when we use the \texttt{induction} tactic, +we lose information on the hypothesis instance, notably that the second +argument is \texttt{1} here. Dependent induction solves this problem by +adding the corresponding equality to the context. + +\begin{coq_eval} +Reset Initial. +\end{coq_eval} +\begin{coq_example} +Require Import Coq.Program.Equality. +Lemma le_minus : forall n:nat, n < 1 -> n = 0. +intros n H ; dependent induction H. +\end{coq_example} + +The subgoal is cleaned up as the tactic tries to automatically +simplify the subgoals with respect to the generated equalities. +In this enriched context, it becomes possible to solve this subgoal. +\begin{coq_example} +reflexivity. +\end{coq_example} + +Now we are in a contradictory context and the proof can be solved. +\begin{coq_example} +inversion H. +\end{coq_example} + +This technique works with any inductive predicate. +In fact, the \texttt{dependent induction} tactic is just a wrapper around +the \texttt{induction} tactic. One can make its own variant by just +writing a new tactic based on the definition found in +\texttt{Coq.Program.Equality}. + +\begin{Variants} +\item {\tt dependent induction {\ident} generalizing {\ident$_1$} \dots + {\ident$_n$}}\tacindex{dependent induction \dots\ generalizing} + + This performs dependent induction on the hypothesis {\ident} but first + generalizes the goal by the given variables so that they are + universally quantified in the goal. This is generally what one wants + to do with the variables that are inside some constructors in the + induction hypothesis. The other ones need not be further generalized. + +\item {\tt dependent destruction {\ident}}\tacindex{dependent destruction} + + This performs the generalization of the instance {\ident} but uses {\tt destruct} + instead of {\tt induction} on the generalized hypothesis. This gives + results equivalent to {\tt inversion} or {\tt dependent inversion} if + the hypothesis is dependent. +\end{Variants} + +\SeeAlso \ref{dependent-induction-example} for a larger example of +dependent induction and an explanation of the underlying technique. + +\subsection{\tt functional induction (\qualid\ \term$_1$ \dots\ \term$_n$)} +\tacindex{functional induction} +\label{FunInduction} + +The 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} +(see Section~\ref{Function}) or \texttt{Functional Scheme} +(see Section~\ref{FunScheme}). Note that this tactic is only available +after a {\tt Require Import FunInd}. + +\begin{coq_eval} +Reset Initial. +Import Nat. +\end{coq_eval} +\begin{coq_example} +Require Import FunInd. +Functional Scheme minus_ind := Induction for minus Sort Prop. +Check minus_ind. +Lemma le_minus (n m:nat) : n - m <= n. +functional induction (minus n m) using minus_ind; simpl; auto. +\end{coq_example} +\begin{coq_example*} +Qed. +\end{coq_example*} + +\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 Parentheses over \qualid \dots \term$_n$ are mandatory. + +\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} (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 {\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} (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. + +\SeeAlso{\ref{Function},\ref{FunScheme},\ref{FunScheme-examples}, + \ref{sec:functional-inversion}} + +\begin{ErrMsgs} +\item \errindex{Cannot find induction information on \qualid} +\item \errindex{Not the right number of induction arguments} +\end{ErrMsgs} + +\begin{Variants} +\item {\tt functional induction (\qualid\ \term$_1$ \dots\ \term$_n$) + as {\disjconjintropattern} using \term$_{m+1}$ with \bindinglist} + + Similarly to \texttt{Induction} and \texttt{elim} + (see Section~\ref{Tac-induction}), this allows giving explicitly the + name of the introduced variables, the + induction principle, and the values of dependent premises of the + elimination scheme, including \emph{predicates} for mutual induction + when {\qualid} is part of a mutually recursive definition. + +\end{Variants} + +\subsection{\tt discriminate \term} +\label{discriminate} +\tacindex{discriminate} + + +This tactic proves any goal from an assumption stating that two +structurally different terms of an inductive set are equal. For +example, from {\tt (S (S O))=(S O)} we can derive by absurdity any +proposition. + +The argument {\term} is assumed to be a proof of a statement +of conclusion {\tt{\term$_1$} = {\term$_2$}} with {\term$_1$} and +{\term$_2$} being elements of an inductive set. To build the proof, +the tactic traverses the normal forms\footnote{Reminder: opaque + constants will not be expanded by $\delta$ reductions.} of +{\term$_1$} and {\term$_2$} looking for a couple of subterms {\tt u} +and {\tt w} ({\tt u} subterm of the normal form of {\term$_1$} and +{\tt w} subterm of the normal form of {\term$_2$}), placed at the same +positions and whose head symbols are two different constructors. If +such a couple of subterms exists, then the proof of the current goal +is completed, otherwise the tactic fails. + +\Rem The syntax {\tt discriminate {\ident}} can be used to refer to a +hypothesis quantified in the goal. In this case, the quantified +hypothesis whose name is {\ident} is first introduced in the local +context using \texttt{intros until \ident}. + +\begin{ErrMsgs} +\item \errindex{No primitive equality found} +\item \errindex{Not a discriminable equality} +\end{ErrMsgs} + +\begin{Variants} +\item \texttt{discriminate \num} + + This does the same thing as \texttt{intros until \num} followed by + \texttt{discriminate \ident} where {\ident} is the identifier for + the last introduced hypothesis. + +\item \texttt{discriminate {\term} with \bindinglist} + + This does the same thing as \texttt{discriminate {\term}} but using +the given bindings to instantiate parameters or hypotheses of {\term}. + +\item \texttt{ediscriminate \num}\tacindex{ediscriminate}\\ + \texttt{ediscriminate {\term} \zeroone{with \bindinglist}} + + This works the same as {\tt discriminate} but if the type of {\term}, + or the type of the hypothesis referred to by {\num}, has uninstantiated + parameters, these parameters are left as existential variables. + +\item \texttt{discriminate} + + This behaves like {\tt discriminate {\ident}} if {\ident} is the + name of an hypothesis to which {\tt discriminate} is applicable; if + the current goal is of the form {\term$_1$} {\tt <>} {\term$_2$}, + this behaves as {\tt intro {\ident}; discriminate {\ident}}. + + \ErrMsg \errindex{No discriminable equalities} +\end{Variants} + +\subsection{\tt injection \term} +\label{injection} +\tacindex{injection} + +The {\tt injection} tactic exploits the property that constructors of +inductive types are injective, i.e. that if $c$ is a constructor +of an inductive type and $c~\vec{t_1}$ and $c~\vec{t_2}$ are equal +then $\vec{t_1}$ and $\vec{t_2}$ are equal too. + +If {\term} is a proof of a statement of conclusion + {\tt {\term$_1$} = {\term$_2$}}, +then {\tt injection} applies the injectivity of constructors as deep as possible to +derive the equality of all the subterms of {\term$_1$} and {\term$_2$} at positions +where {\term$_1$} and {\term$_2$} start to differ. +For example, from {\tt (S p, S n) = (q, S (S m)} we may derive {\tt S + p = q} and {\tt n = S m}. For this tactic to work, {\term$_1$} and +{\term$_2$} should be typed with an inductive +type and they should be neither convertible, nor having a different +head constructor. If these conditions are satisfied, the tactic +derives the equality of all the subterms of {\term$_1$} and +{\term$_2$} at positions where they differ and adds them as +antecedents to the conclusion of the current goal. + +\Example Consider the following goal: + +\begin{coq_example*} +Inductive list : Set := + | nil : list + | cons : nat -> list -> list. +Variable P : list -> Prop. +\end{coq_example*} +\begin{coq_eval} +Lemma ex : + forall (l:list) (n:nat), P nil -> cons n l = cons 0 nil -> P l. +intros l n H H0. +\end{coq_eval} +\begin{coq_example} +Show. +injection H0. +\end{coq_example} +\begin{coq_eval} +Abort. +\end{coq_eval} + +Beware that \texttt{injection} yields an equality in a sigma type +whenever the injected object has a dependent type $P$ with its two +instances in different types $(P~t_1~...~t_n)$ and +$(P~u_1~...~u_n)$. If $t_1$ and $u_1$ are the same and have for type +an inductive type for which a decidable equality has been declared +using the command {\tt Scheme Equality} (see \ref{Scheme}), the use of +a sigma type is avoided. + +\Rem If some quantified hypothesis of the goal is named {\ident}, then +{\tt injection {\ident}} first introduces the hypothesis in the local +context using \texttt{intros until \ident}. + +\begin{ErrMsgs} +\item \errindex{Not a projectable equality but a discriminable one} +\item \errindex{Nothing to do, it is an equality between convertible terms} +\item \errindex{Not a primitive equality} +\item \errindex{Nothing to inject} +\end{ErrMsgs} + +\begin{Variants} +\item \texttt{injection \num} + + This does the same thing as \texttt{intros until \num} followed by +\texttt{injection \ident} where {\ident} is the identifier for the last +introduced hypothesis. + +\item \texttt{injection {\term} with \bindinglist} + + This does the same as \texttt{injection {\term}} but using + the given bindings to instantiate parameters or hypotheses of {\term}. + +\item \texttt{einjection \num}\tacindex{einjection}\\ + \texttt{einjection {\term} \zeroone{with \bindinglist}} + + This works the same as {\tt injection} but if the type of {\term}, + or the type of the hypothesis referred to by {\num}, has uninstantiated + parameters, these parameters are left as existential variables. + +\item{\tt injection} + + If the current goal is of the form {\term$_1$} {\tt <>} {\term$_2$}, + this behaves as {\tt intro {\ident}; injection {\ident}}. + + \ErrMsg \errindex{goal does not satisfy the expected preconditions} + +\item \texttt{injection {\term} \zeroone{with \bindinglist} as \nelistnosep{\intropattern}}\\ +\texttt{injection {\num} as {\intropattern} \dots\ \intropattern}\\ +\texttt{injection as {\intropattern} \dots\ \intropattern}\\ +\texttt{einjection {\term} \zeroone{with \bindinglist} as \nelistnosep{\intropattern}}\\ +\texttt{einjection {\num} as {\intropattern} \dots\ \intropattern}\\ +\texttt{einjection as {\intropattern} \dots\ \intropattern} +\tacindex{injection \dots\ as} + +These variants apply \texttt{intros} \nelistnosep{\intropattern} after +the call to \texttt{injection} or \texttt{einjection} so that all +equalities generated are moved in the context of hypotheses. The +number of {\intropattern} must not exceed the number of equalities +newly generated. If it is smaller, fresh names are automatically +generated to adjust the list of {\intropattern} to the number of new +equalities. The original equality is erased if it corresponds to an +hypothesis. + +\end{Variants} + +\optindex{Structural Injection} + +It is possible to ensure that \texttt{injection {\term}} erases the +original hypothesis and leaves the generated equalities in the context +rather than putting them as antecedents of the current goal, as if +giving \texttt{injection {\term} as} (with an empty list of names). To +obtain this behavior, the option {\tt Set Structural Injection} must +be activated. This option is off by default. + +By default, \texttt{injection} only creates new equalities between +terms whose type is in sort \texttt{Type} or \texttt{Set}, thus +implementing a special behavior for objects that are proofs +of a statement in \texttt{Prop}. This behavior can be turned off +by setting the option \texttt{Set Keep Proof Equalities}. +\optindex{Keep Proof Equalities} +\subsection{\tt inversion \ident} +\tacindex{inversion} + +Let the type of {\ident} in the local context be $(I~\vec{t})$, +where $I$ is a (co)inductive predicate. Then, +\texttt{inversion} applied to \ident~ derives for each possible +constructor $c_i$ of $(I~\vec{t})$, {\bf all} the necessary +conditions that should hold for the instance $(I~\vec{t})$ to be +proved by $c_i$. + +\Rem If {\ident} does not denote a hypothesis in the local context +but refers to a hypothesis quantified in the goal, then the +latter is first introduced in the local context using +\texttt{intros until \ident}. + +\Rem As inversion proofs may be large in size, we recommend the user to +stock the lemmas whenever the same instance needs to be inverted +several times. See Section~\ref{Derive-Inversion}. + +\Rem Part of the behavior of the \texttt{inversion} tactic is to generate +equalities between expressions that appeared in the hypothesis that is +being processed. By default, no equalities are generated if they relate +two proofs (i.e. equalities between terms whose type is in +sort \texttt{Prop}). This behavior can be turned off by using the option +\texttt{Set Keep Proof Equalities.} +\optindex{Keep Proof Equalities} + +\begin{Variants} +\item \texttt{inversion \num} + + This does the same thing as \texttt{intros until \num} then + \texttt{inversion \ident} where {\ident} is the identifier for the + last introduced hypothesis. + +\item \tacindex{inversion\_clear} \texttt{inversion\_clear \ident} + + This behaves as \texttt{inversion} and then erases \ident~ from the + context. + +\item \tacindex{inversion \dots\ as} \texttt{inversion {\ident} as \intropattern} + + This generally behaves as \texttt{inversion} but using names in + {\intropattern} for naming hypotheses. The {\intropattern} must have + the form {\tt [} $p_{11} \ldots p_{1n_1}$ {\tt |} {\ldots} {\tt |} + $p_{m1} \ldots p_{mn_m}$ {\tt ]} with $m$ being the number of + constructors of the type of {\ident}. Be careful that the list must + be of length $m$ even if {\tt inversion} discards some cases (which + is precisely one of its roles): for the discarded cases, just use an + empty list (i.e. $n_i=0$). + + The arguments of the $i^{th}$ constructor and the + equalities that {\tt inversion} introduces in the context of the + goal corresponding to the $i^{th}$ constructor, if it exists, get + their names from the list $p_{i1}$ \ldots $p_{in_i}$ in order. If + there are not enough names, {\tt inversion} invents names for the + remaining variables to introduce. In case an equation splits into + several equations (because {\tt inversion} applies {\tt injection} + on the equalities it generates), the corresponding name $p_{ij}$ in + the list must be replaced by a sublist of the form {\tt [$p_{ij1}$ + \mbox{\dots} $p_{ijq}$]} (or, equivalently, {\tt ($p_{ij1}$, + \dots, $p_{ijq}$)}) where $q$ is the number of subequalities + obtained from splitting the original equation. Here is an example. + + The \texttt{inversion \dots\ as} variant of \texttt{inversion} + generally behaves in a slightly more expectable way than + \texttt{inversion} (no artificial duplication of some hypotheses + referring to other hypotheses) To take benefit of these + improvements, it is enough to use \texttt{inversion \dots\ as []}, + letting the names being finally chosen by {\Coq}. + +\begin{coq_eval} +Require Import List. +\end{coq_eval} + +\begin{coq_example} +Inductive contains0 : list nat -> Prop := + | in_hd : forall l, contains0 (0 :: l) + | in_tl : forall l b, contains0 l -> contains0 (b :: l). +Goal forall l:list nat, contains0 (1 :: l) -> contains0 l. +intros l H; inversion H as [ | l' p Hl' [Heqp Heql'] ]. +\end{coq_example} + +\begin{coq_eval} +Abort. +\end{coq_eval} + +\item \texttt{inversion {\num} as \intropattern} + + This allows naming the hypotheses introduced by + \texttt{inversion \num} in the context. + +\item \tacindex{inversion\_clear \dots\ as} \texttt{inversion\_clear + {\ident} as \intropattern} + + This allows naming the hypotheses introduced by + \texttt{inversion\_clear} in the context. Notice that hypothesis + names can be provided as if \texttt{inversion} were called, even + though the \texttt{inversion\_clear} will eventually erase the + hypotheses. + +\item \tacindex{inversion \dots\ in} \texttt{inversion {\ident} + in \ident$_1$ \dots\ \ident$_n$} + + Let \ident$_1$ \dots\ \ident$_n$, be identifiers in the local context. This + tactic behaves as generalizing \ident$_1$ \dots\ \ident$_n$, and + then performing \texttt{inversion}. + +\item \tacindex{inversion \dots\ as \dots\ in} \texttt{inversion + {\ident} as {\intropattern} in \ident$_1$ \dots\ + \ident$_n$} + + This allows naming the hypotheses introduced in the context by + \texttt{inversion {\ident} in \ident$_1$ \dots\ \ident$_n$}. + +\item \tacindex{inversion\_clear \dots\ in} \texttt{inversion\_clear + {\ident} in \ident$_1$ \dots\ \ident$_n$} + + Let \ident$_1$ \dots\ \ident$_n$, be identifiers in the local context. This + tactic behaves as generalizing \ident$_1$ \dots\ \ident$_n$, and + then performing {\tt inversion\_clear}. + +\item \tacindex{inversion\_clear \dots\ as \dots\ in} + \texttt{inversion\_clear {\ident} as {\intropattern} + in \ident$_1$ \dots\ \ident$_n$} + + This allows naming the hypotheses introduced in the context by + \texttt{inversion\_clear {\ident} in \ident$_1$ \dots\ \ident$_n$}. + +\item \tacindex{dependent inversion} \texttt{dependent inversion \ident} + + That must be used when \ident\ appears in the current goal. It acts + like \texttt{inversion} and then substitutes \ident\ for the + corresponding term in the goal. + +\item \tacindex{dependent inversion \dots\ as } \texttt{dependent + inversion {\ident} as \intropattern} + + This allows naming the hypotheses introduced in the context by + \texttt{dependent inversion} {\ident}. + +\item \tacindex{dependent inversion\_clear} \texttt{dependent + inversion\_clear \ident} + + Like \texttt{dependent inversion}, except that {\ident} is cleared + from the local context. + +\item \tacindex{dependent inversion\_clear \dots\ as} + \texttt{dependent inversion\_clear {\ident} as \intropattern} + + This allows naming the hypotheses introduced in the context by + \texttt{dependent inversion\_clear} {\ident}. + +\item \tacindex{dependent inversion \dots\ with} \texttt{dependent + inversion {\ident} with \term} + + This variant allows you to specify the generalization of the goal. It + is useful when the system fails to generalize the goal automatically. If + {\ident} has type $(I~\vec{t})$ and $I$ has type + $\forall (\vec{x}:\vec{T}), s$, then \term~ must be of type + $I:\forall (\vec{x}:\vec{T}), I~\vec{x}\to s'$ where $s'$ is the + type of the goal. + +\item \tacindex{dependent inversion \dots\ as \dots\ with} + \texttt{dependent inversion {\ident} as {\intropattern} + with \term} + + This allows naming the hypotheses introduced in the context by + \texttt{dependent inversion {\ident} with \term}. + +\item \tacindex{dependent inversion\_clear \dots\ with} + \texttt{dependent inversion\_clear {\ident} with \term} + + Like \texttt{dependent inversion \dots\ with} but clears {\ident} from + the local context. + +\item \tacindex{dependent inversion\_clear \dots\ as \dots\ with} + \texttt{dependent inversion\_clear {\ident} as + {\intropattern} with \term} + + This allows naming the hypotheses introduced in the context by + \texttt{dependent inversion\_clear {\ident} with \term}. + +\item \tacindex{simple inversion} \texttt{simple inversion \ident} + + It is a very primitive inversion tactic that derives all the necessary + equalities but it does not simplify the constraints as + \texttt{inversion} does. + +\item \tacindex{simple inversion \dots\ as} \texttt{simple inversion + {\ident} as \intropattern} + + This allows naming the hypotheses introduced in the context by + \texttt{simple inversion}. + +\item \tacindex{inversion \dots\ using} \texttt{inversion {\ident} + using \ident$'$} + + Let {\ident} have type $(I~\vec{t})$ ($I$ an inductive + predicate) in the local context, and \ident$'$ be a (dependent) inversion + lemma. Then, this tactic refines the current goal with the specified + lemma. + +\item \tacindex{inversion \dots\ using \dots\ in} \texttt{inversion + {\ident} using \ident$'$ in \ident$_1$\dots\ \ident$_n$} + + This tactic behaves as generalizing \ident$_1$\dots\ \ident$_n$, + then doing \texttt{inversion {\ident} using \ident$'$}. + +\item \tacindex{inversion\_sigma} \texttt{inversion\_sigma} + + This tactic turns equalities of dependent pairs (e.g., + \texttt{existT P x p = existT P y q}, frequently left over by + \texttt{inversion} on a dependent type family) into pairs of + equalities (e.g., a hypothesis \texttt{H : x = y} and a hypothesis + of type \texttt{rew H in p = q}); these hypotheses can subsequently + be simplified using \texttt{subst}, without ever invoking any kind + of axiom asserting uniqueness of identity proofs. If you want to + explicitly specify the hypothesis to be inverted, or name the + generated hypotheses, you can invoke \texttt{induction H as [H1 H2] + using eq\_sigT\_rect}. This tactic also works for \texttt{sig}, + \texttt{sigT2}, and \texttt{sig2}, and there are similar + \texttt{eq\_sig\emph{*}\_rect} induction lemmas. + +\end{Variants} + +\firstexample +\example{Non-dependent inversion} +\label{inversion-examples} + +Let us consider the relation \texttt{Le} over natural numbers and the +following variables: + +\begin{coq_eval} +Reset Initial. +\end{coq_eval} + +\begin{coq_example*} +Inductive Le : nat -> nat -> Set := + | LeO : forall n:nat, Le 0 n + | LeS : forall n m:nat, Le n m -> Le (S n) (S m). +Variable P : nat -> nat -> Prop. +Variable Q : forall n m:nat, Le n m -> Prop. +\end{coq_example*} + +Let us consider the following goal: + +\begin{coq_eval} +Lemma ex : forall n m:nat, Le (S n) m -> P n m. +intros. +\end{coq_eval} + +\begin{coq_example} +Show. +\end{coq_example} + +To prove the goal, we may need to reason by cases on \texttt{H} and to +derive that \texttt{m} is necessarily of +the form $(S~m_0)$ for certain $m_0$ and that $(Le~n~m_0)$. +Deriving these conditions corresponds to prove that the +only possible constructor of \texttt{(Le (S n) m)} is +\texttt{LeS} and that we can invert the +\texttt{->} in the type of \texttt{LeS}. +This inversion is possible because \texttt{Le} is the smallest set closed by +the constructors \texttt{LeO} and \texttt{LeS}. + +\begin{coq_example} +inversion_clear H. +\end{coq_example} + +Note that \texttt{m} has been substituted in the goal for \texttt{(S m0)} +and that the hypothesis \texttt{(Le n m0)} has been added to the +context. + +Sometimes it is +interesting to have the equality \texttt{m=(S m0)} in the +context to use it after. In that case we can use \texttt{inversion} that +does not clear the equalities: + +\begin{coq_eval} +Undo. +\end{coq_eval} + +\begin{coq_example} +inversion H. +\end{coq_example} + +\begin{coq_eval} +Abort. +\end{coq_eval} + +\example{Dependent inversion} + +Let us consider the following goal: + +\begin{coq_eval} +Lemma ex_dep : forall (n m:nat) (H:Le (S n) m), Q (S n) m H. +intros. +\end{coq_eval} + +\begin{coq_example} +Show. +\end{coq_example} + +As \texttt{H} occurs in the goal, we may want to reason by cases on its +structure and so, we would like inversion tactics to +substitute \texttt{H} by the corresponding term in constructor form. +Neither \texttt{Inversion} nor {\tt Inversion\_clear} make such a +substitution. +To have such a behavior we use the dependent inversion tactics: + +\begin{coq_example} +dependent inversion_clear H. +\end{coq_example} + +Note that \texttt{H} has been substituted by \texttt{(LeS n m0 l)} and +\texttt{m} by \texttt{(S m0)}. + +\example{Using \texorpdfstring{\texttt{inversion\_sigma}}{inversion\_sigma}} + +Let us consider the following inductive type of length-indexed lists, +and a lemma about inverting equality of \texttt{cons}: + +\begin{coq_eval} +Reset Initial. +Set Printing Compact Contexts. +\end{coq_eval} + +\begin{coq_example*} +Require Coq.Logic.Eqdep_dec. + +Inductive vec A : nat -> Type := +| nil : vec A O +| cons {n} (x : A) (xs : vec A n) : vec A (S n). + +Lemma invert_cons : forall A n x xs y ys, + @cons A n x xs = @cons A n y ys + -> xs = ys. +Proof. +\end{coq_example*} + +\begin{coq_example} +intros A n x xs y ys H. +\end{coq_example} + +After performing \texttt{inversion}, we are left with an equality of +\texttt{existT}s: + +\begin{coq_example} +inversion H. +\end{coq_example} + +We can turn this equality into a usable form with +\texttt{inversion\_sigma}: + +\begin{coq_example} +inversion_sigma. +\end{coq_example} + +To finish cleaning up the proof, we will need to use the fact that +that all proofs of \texttt{n = n} for \texttt{n} a \texttt{nat} are +\texttt{eq\_refl}: + +\begin{coq_example} +let H := match goal with H : n = n |- _ => H end in +pose proof (Eqdep_dec.UIP_refl_nat _ H); subst H. +simpl in *. +\end{coq_example} + +Finally, we can finish the proof: + +\begin{coq_example} +assumption. +Qed. +\end{coq_example} + +\subsection{\tt fix {\ident} {\num}} +\tacindex{fix} +\label{tactic:fix} + +This tactic is a primitive tactic to start a proof by induction. In +general, it is easier to rely on higher-level induction tactics such +as the ones described in Section~\ref{Tac-induction}. + +In the syntax of the tactic, the identifier {\ident} is the name given +to the induction hypothesis. The natural number {\num} tells on which +premise of the current goal the induction acts, starting +from 1, counting both dependent and non dependent +products, but skipping local definitions. Especially, the current +lemma must be composed of at least {\num} products. + +Like in a {\tt fix} expression, the induction +hypotheses have to be used on structurally smaller arguments. +The verification that inductive proof arguments are correct is done +only at the time of registering the lemma in the environment. To know +if the use of induction hypotheses is correct at some +time of the interactive development of a proof, use the command {\tt + Guarded} (see Section~\ref{Guarded}). + +\begin{Variants} + \item {\tt fix \ident$_1$ {\num} with ( \ident$_2$ + \nelistnosep{\binder$_2$} \zeroone{\{ struct \ident$'_2$ + \}} :~\type$_2$ ) \dots\ ( \ident$_n$ + \nelistnosep{\binder$_n$} \zeroone{\{ struct \ident$'_n$ \}} :~\type$_n$ )} + +This starts a proof by mutual induction. The statements to be +simultaneously proved are respectively {\tt forall} + \nelistnosep{{\binder}$_2$}{\tt ,} {\type}$_2$, {\ldots}, {\tt forall} + \nelistnosep{{\binder}$_n$}{\tt ,} {\type}$_n$. The identifiers +{\ident}$_1$ {\ldots} {\ident}$_n$ are the names of the induction +hypotheses. The identifiers {\ident}$'_2$ {\ldots} {\ident}$'_n$ are the +respective names of the premises on which the induction is performed +in the statements to be simultaneously proved (if not given, the +system tries to guess itself what they are). + +\end{Variants} + +\subsection{\tt cofix \ident} +\tacindex{cofix} +\label{tactic:cofix} + +This tactic starts a proof by coinduction. The identifier {\ident} is +the name given to the coinduction hypothesis. Like in a {\tt cofix} +expression, the use of induction hypotheses have to guarded by a +constructor. The verification that the use of co-inductive hypotheses +is correct is done only at the time of registering the lemma in the +environment. To know if the use of coinduction hypotheses is correct +at some time of the interactive development of a proof, use the +command {\tt Guarded} (see Section~\ref{Guarded}). + + +\begin{Variants} + \item {\tt cofix \ident$_1$ with ( \ident$_2$ + \nelistnosep{\binder$_2$} :~\type$_2$ ) \dots\ ( + \ident$_n$ \nelistnosep{\binder$_n$} :~\type$_n$ )} + +This starts a proof by mutual coinduction. The statements to be +simultaneously proved are respectively {\tt forall} +\nelistnosep{{\binder}$_2$}{\tt ,} {\type}$_2$, {\ldots}, {\tt forall} + \nelistnosep{{\binder}$_n$}{\tt ,} {\type}$_n$. The identifiers + {\ident}$_1$ {\ldots} {\ident}$_n$ are the names of the + coinduction hypotheses. + +\end{Variants} + +\section{Rewriting expressions} + + +These tactics use the equality {\tt eq:forall A:Type, A->A->Prop} +defined in file {\tt Logic.v} (see Section~\ref{Equality}). The +notation for {\tt eq}~$T~t~u$ is simply {\tt $t$=$u$} dropping the +implicit type of $t$ and $u$. + +\subsection{\tt rewrite \term} +\label{rewrite} +\tacindex{rewrite} + +This tactic applies to any goal. The type of {\term} +must have the form + +\texttt{forall (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} finds the first subterm matching +\term$_1$ in the goal, resulting in instances \term$_1'$ and \term$_2'$ +and then replaces every occurrence of \term$_1'$ by \term$_2'$. +Hence, some of the variables x$_i$ are +solved by unification, and some of the types \texttt{A}$_1$, \dots, +\texttt{A}$_n$ become new subgoals. + +% \Rem In case the type of +% \term$_1$ contains occurrences of variables bound in the +% type of \term, the tactic tries first to find a subterm of the goal +% which matches this term in order to find a closed instance \term$'_1$ +% of \term$_1$, and then all instances of \term$'_1$ will be replaced. + +\begin{ErrMsgs} +\item \errindex{The term provided does not end with an equation} + +\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 ->} + + Is equivalent to {\tt rewrite \term} + +\item {\tt rewrite <- \term}\tacindex{rewrite <-} + + Uses the equality \term$_1${\tt=}\term$_2$ from right to left + +\item {\tt rewrite {\term} in \nterm{clause}} + \tacindex{rewrite \dots\ in} + + Analogous to {\tt rewrite {\term}} but rewriting is done following + \nterm{clause} (similarly to \ref{Conversion-tactics}). For + instance: + \begin{itemize} + \item \texttt{rewrite H in H1} will rewrite \texttt{H} in the hypothesis + \texttt{H1} instead of the current goal. + \item \texttt{rewrite H in H1 at 1, H2 at - 2 |- *} means \texttt{rewrite H; rewrite H in H1 at 1; + rewrite H in H2 at - 2}. In particular a failure will happen if any of + these three simpler tactics fails. + \item \texttt{rewrite H in * |- } will do \texttt{rewrite H in + H$_i$} for all hypotheses \texttt{H$_i$} different from \texttt{H}. A success will happen + as soon as at least one of these simpler 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} + Orientation {\tt ->} or {\tt <-} can be + inserted before the term to rewrite. + +\item {\tt rewrite {\term} at {\occlist}} + \tacindex{rewrite \dots\ at} + + Rewrite only the given occurrences of \term$_1'$. Occurrences are + specified from left to right as for \texttt{pattern} (\S + \ref{pattern}). The rewrite is always performed using setoid + rewriting, even for Leibniz's equality, so one has to + \texttt{Import Setoid} to use this variant. + +\item {\tt rewrite {\term} by {\tac}} + \tacindex{rewrite \dots\ by} + + Use {\tac} to completely solve the side-conditions arising from the + rewrite. + +\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 \nterm{clause} + can be added at the end after the keyword {\tt in}; it will + then affect all rewrite operations. + +\item In all forms of {\tt rewrite} described above, a term to rewrite + can be immediately prefixed by one of the following modifiers: + \begin{itemize} + \item {\tt ?} : the tactic {\tt rewrite ?$\term$} performs the + rewrite of $\term$ as many times as possible (perhaps zero time). + This form never fails. + \item {\tt $n$?} : works similarly, except that it will do at most + $n$ rewrites. + \item {\tt !} : works as {\tt ?}, except that at least one rewrite + should succeed, otherwise the tactic fails. + \item {\tt $n$!} (or simply {\tt $n$}) : precisely $n$ rewrites + of $\term$ will be done, leading to failure if these $n$ rewrites are not possible. + \end{itemize} + +\item {\tt erewrite {\term}\tacindex{erewrite}} + +This tactic works as {\tt rewrite {\term}} but turning unresolved +bindings into existential variables, if any, instead of failing. It has +the same variants as {\tt rewrite} has. + +\end{Variants} + +\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 +{\term$_1$} in the current goal with {\term$_2$} and generates the +equality {\term$_2$}{\tt =}{\term$_1$} as a subgoal. This equality is +automatically solved if it occurs among the assumption, or if its +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$ 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}} + + Replaces {\term} with {\term'} using the + first assumption whose type has the form {\tt \term=\term'} or {\tt + \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}} + + Replaces {\term} with {\term'} using the + first assumption whose type has the form {\tt \term'=\term} + +\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}. + +\item {\tt cutrewrite <- (\term$_1$ = \term$_2$)} +%\label{cutrewrite} +\tacindex{cutrewrite} + +This tactic is deprecated. It acts like {\tt replace {\term$_2$} with + {\term$_1$}}, or, equivalently as {\tt enough} (\term$_1$ = +\term$_2$) {\tt as <-}. + +\item {\tt cutrewrite -> (\term$_1$ = \term$_2$)} +%\label{cutrewrite} +\tacindex{cutrewrite} + +This tactic is deprecated. It can be replaced by {\tt enough} +(\term$_1$ = \term$_2$) {\tt as ->}. + +\end{Variants} + +\subsection{\tt subst \ident} +\tacindex{subst} +\optindex{Regular Subst Tactic} + +This tactic applies to a goal that has \ident\ in its context and (at +least) one hypothesis, say $H$, of type {\tt \ident} = $t$ or $t$ +{\tt = \ident} with {\ident} not occurring in $t$. Then it replaces +{\ident} by $t$ everywhere in the goal (in the hypotheses and in the +conclusion) and clears {\ident} and $H$ from the context. + +If {\ident} is a local definition of the form {\ident} := $t$, it is +also unfolded and cleared. + +\Rem +When several hypotheses have the form {\tt \ident} = $t$ or {\tt + $t$ = \ident}, the first one is used. + +\Rem +If $H$ is itself dependent in the goal, it is replaced by the +proof of reflexivity of equality. + +\begin{Variants} + \item {\tt subst \ident$_1$ {\dots} \ident$_n$} + + This is equivalent to {\tt subst \ident$_1$; \dots; subst \ident$_n$}. + \item {\tt subst} + + This applies {\tt subst} repeatedly from top to bottom to all + identifiers of the context for which an equality of the form {\tt + \ident} = $t$ or $t$ {\tt = \ident} or {\tt \ident} := $t$ exists, with + {\ident} not occurring in $t$. + +\noindent {\bf Remark: } The behavior of {\tt subst} can be controlled +using option {\tt Set Regular Subst Tactic}. When this option is +activated, {\tt subst} also deals with the following corner cases: +\begin{itemize} +\item A context with ordered hypotheses {\tt \ident$_1$ = \ident$_2$} + and {\tt \ident$_1$ = $t$}, or {$t'$ = \ident$_1$} with $t'$ not a + variable, and no other hypotheses of the form {\tt \ident$_2$ = $u$} + or {\tt $u$ = \ident$_2$}; without the option, a second call to {\tt + subst} would be necessary to replace {\ident$_2$} by $t$ or $t'$ + respectively. + +\item The presence of a recursive equation which without the option + would be a cause of failure of {\tt subst}. + +\item A context with cyclic dependencies as with hypotheses {\tt + \ident$_1$ = f~\ident$_2$} and {\tt \ident$_2$ = g~\ident$_1$} which + without the option would be a cause of failure of {\tt subst}. +\end{itemize} +Additionally, it prevents a local definition such as {\tt \ident} := + $t$ to be unfolded which otherwise it would exceptionally unfold in +configurations containing hypotheses of the form {\tt {\ident} = $u$}, +or {\tt $u'$ = \ident} with $u'$ not a variable. + +Finally, it preserves the initial order of hypotheses, which without +the option it may break. + +The option is on by default. + +\end{Variants} + +\subsection{\tt stepl \term} +\tacindex{stepl} + +This tactic is for chaining rewriting steps. It assumes a goal of the +form ``$R$ {\term}$_1$ {\term}$_2$'' where $R$ is a binary relation +and relies on a database of lemmas of the form {\tt forall} $x$ $y$ +$z$, $R$ $x$ $y$ {\tt ->} $eq$ $x$ $z$ {\tt ->} $R$ $z$ $y$ where $eq$ +is typically a setoid equality. The application of {\tt stepl {\term}} +then replaces the goal by ``$R$ {\term} {\term}$_2$'' and adds a new +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 {\term}.} +\end{quote} + +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{setoids}). + +\begin{Variants} +\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}}\tacindex{stepr} + +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$ +$z$, $R$ $x$ $y$ {\tt ->} $eq$ $y$ $z$ {\tt ->} $R$ $x$ $z$'' +and are registered using the command +\comindex{Declare Right Step} +\begin{quote} +{\tt Declare Right Step {\term}.} +\end{quote} +\end{Variants} + +\subsection{\tt change \term} +\tacindex{change} +\label{change} + +This tactic applies to any goal. It implements the rule +``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. + +\begin{ErrMsgs} +\item \errindex{Not convertible} +\end{ErrMsgs} + +\tacindex{change \dots\ in} +\begin{Variants} +\item {\tt change \term$_1$ with \term$_2$} + + This replaces the occurrences of \term$_1$ by \term$_2$ in the + current goal. The terms \term$_1$ and \term$_2$ must be + convertible. + +\item {\tt change \term$_1$ at \num$_1$ \dots\ \num$_i$ with \term$_2$} + + This replaces the occurrences numbered \num$_1$ \dots\ \num$_i$ of + \term$_1$ by \term$_2$ in the current goal. + The terms \term$_1$ and \term$_2$ must be convertible. + + \ErrMsg {\tt Too few occurrences} + +\item {\tt change {\term} in {\ident}} + +\item {\tt change \term$_1$ with \term$_2$ in {\ident}} + +\item {\tt change \term$_1$ at \num$_1$ \dots\ \num$_i$ with \term$_2$ in + {\ident}} + + This applies the {\tt change} tactic not to the goal but to the + hypothesis {\ident}. + +\end{Variants} + +\SeeAlso \ref{Conversion-tactics} + + +\section{Performing computations +\index{Conversion tactics} +\label{Conversion-tactics}} + +This set of tactics implements different specialized usages of the +tactic \texttt{change}. + +All conversion tactics (including \texttt{change}) can be +parameterized by the parts of the goal where the conversion can +occur. This is done using \emph{goal clauses} which consists in a list +of hypotheses and, optionally, of a reference to the conclusion of the +goal. For defined hypothesis it is possible to specify if the +conversion should occur on the type part, the body part or both +(default). + +\index{Clauses} +\index{Goal clauses} +Goal 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 goal clauses) and +are introduced by the keyword \texttt{in}. If no goal clause is provided, +the default is to perform the conversion only in the conclusion. + +The syntax and description of the various goal clauses is the following: +\begin{description} +\item[]\texttt{in {\ident}$_1$ $\ldots$ {\ident}$_n$ |- } only in hypotheses {\ident}$_1$ + \ldots {\ident}$_n$ +\item[]\texttt{in {\ident}$_1$ $\ldots$ {\ident}$_n$ |- *} in hypotheses {\ident}$_1$ \ldots + {\ident}$_n$ and in the conclusion +\item[]\texttt{in * |-} in every hypothesis +\item[]\texttt{in *} (equivalent to \texttt{in * |- *}) everywhere +\item[]\texttt{in (type of {\ident}$_1$) (value of {\ident}$_2$) $\ldots$ |-} in + type part of {\ident}$_1$, in the value part of {\ident}$_2$, etc. +\end{description} + +For backward compatibility, the notation \texttt{in}~{\ident}$_1$\ldots {\ident}$_n$ +performs the conversion in hypotheses {\ident}$_1$\ldots {\ident}$_n$. + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +%voir reduction__conv_x : histoires d'univers. +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +\subsection{{\tt cbv \flag$_1$ \mbox{\dots} \flag$_n$}, {\tt lazy \flag$_1$ +\mbox{\dots} \flag$_n$}, and \tt compute} +\tacindex{cbv} +\tacindex{lazy} +\tacindex{compute} +\tacindex{vm\_compute}\label{vmcompute} +\tacindex{native\_compute}\label{nativecompute} + +These parameterized reduction tactics apply to any goal and perform +the normalization of the goal according to the specified flags. In +correspondence with the kinds of reduction considered in \Coq\, namely +$\beta$ (reduction of functional application), $\delta$ (unfolding of +transparent constants, see \ref{Transparent}), $\iota$ (reduction of +pattern-matching over a constructed term, and unfolding of {\tt fix} +and {\tt cofix} expressions) and $\zeta$ (contraction of local +definitions), the flags are either {\tt beta}, {\tt delta}, +{\tt match}, {\tt fix}, {\tt cofix}, {\tt iota} or {\tt zeta}. +The {\tt iota} flag is a shorthand for {\tt match}, {\tt fix} and {\tt cofix}. +The {\tt delta} flag itself can be refined into {\tt +delta [\qualid$_1$\ldots\qualid$_k$]} or {\tt delta +-[\qualid$_1$\ldots\qualid$_k$]}, restricting in the first case the +constants to unfold to the constants listed, and restricting in the +second case the constant to unfold to all but the ones explicitly +mentioned. Notice that the {\tt delta} flag does not apply to +variables bound by a let-in construction inside the term itself (use +here the {\tt zeta} flag). In any cases, opaque constants are not +unfolded (see Section~\ref{Opaque}). + +Normalization according to the flags is done by first evaluating the +head of the expression into a {\em weak-head} normal form, i.e. until +the evaluation is bloked by a variable (or an opaque constant, or an +axiom), as e.g. in {\tt x\;u$_1$\;...\;u$_n$}, or {\tt match x with + ... end}, or {\tt (fix f x \{struct x\} := ...) x}, or is a +constructed form (a $\lambda$-expression, a constructor, a cofixpoint, +an inductive type, a product type, a sort), or is a redex that the +flags prevent to reduce. Once a weak-head normal form is obtained, +subterms are recursively reduced using the same strategy. + +Reduction to weak-head normal form can be done using two strategies: +{\em lazy} ({\tt lazy} tactic), or {\em call-by-value} ({\tt cbv} +tactic). The lazy strategy is a call-by-need strategy, with sharing of +reductions: the arguments of a function call are weakly evaluated only +when necessary, and if an argument is used several times then it is +weakly computed only once. This reduction is efficient for reducing +expressions with dead code. For instance, the proofs of a proposition +{\tt exists~$x$. $P(x)$} reduce to a pair of a witness $t$, and a +proof that $t$ satisfies the predicate $P$. Most of the time, $t$ may +be computed without computing the proof of $P(t)$, thanks to the lazy +strategy. + +The call-by-value strategy is the one used in ML languages: the +arguments of a function call are systematically weakly evaluated +first. Despite the lazy strategy always performs fewer reductions than +the call-by-value strategy, the latter is generally more efficient for +evaluating purely computational expressions (i.e. with little dead code). + +\begin{Variants} +\item {\tt compute} \tacindex{compute}\\ + {\tt cbv} + + These are synonyms for {\tt cbv beta delta iota zeta}. + +\item {\tt lazy} + + This is a synonym for {\tt lazy beta delta iota zeta}. + +\item {\tt compute [\qualid$_1$\ldots\qualid$_k$]}\\ + {\tt cbv [\qualid$_1$\ldots\qualid$_k$]} + + These are synonyms of {\tt cbv beta delta + [\qualid$_1$\ldots\qualid$_k$] iota zeta}. + +\item {\tt compute -[\qualid$_1$\ldots\qualid$_k$]}\\ + {\tt cbv -[\qualid$_1$\ldots\qualid$_k$]} + + These are synonyms of {\tt cbv beta delta + -[\qualid$_1$\ldots\qualid$_k$] iota zeta}. + +\item {\tt lazy [\qualid$_1$\ldots\qualid$_k$]}\\ + {\tt lazy -[\qualid$_1$\ldots\qualid$_k$]} + + 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} + + This tactic evaluates the goal using the optimized call-by-value evaluation + bytecode-based virtual machine described in + \cite{CompiledStrongReduction}. 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 reflection-based tactics. + +\item {\tt native\_compute} \tacindex{native\_compute} \optindex{NativeCompute Profiling} + + This tactic evaluates the goal by compilation to \ocaml{} as described in + \cite{FullReduction}. If \Coq{} is running in native code, it can be typically + two to five times faster than {\tt vm\_compute}. Note however that the + compilation cost is higher, so it is worth using only for intensive + computations. + + On Linux, if you have the {\tt perf} profiler installed, you can profile {\tt native\_compute} evaluations. + The command + \begin{quote} + {\tt Set Native Compute Profiling} + \end{quote} + enables profiling. Use the command + \begin{quote} + {\tt Set NativeCompute Profile Filename \str} + \end{quote} + to specify the profile output; the default is {\tt native\_compute\_profile.data}. The actual filename used + will contain extra characters to avoid overwriting an existing file; that filename is reported to the user. That means + you can individually profile multiple uses of {\tt native\_compute} in a script. From the Linux command line, run {\tt perf report} on + the profile file to see the results. Consult the {\tt perf} documentation for more details. + +\end{Variants} + +\Rem The following option makes {\tt cbv} (and its derivative {\tt + compute}) print information about the constants it encounters and +the unfolding decisions it makes. +\begin{quote} + \optindex{Debug Cbv} + {\tt Set Debug Cbv} +\end{quote} + +% Obsolete? Anyway not very important message +%\begin{ErrMsgs} +%\item \errindex{Delta must be specified before} +% +% A list of constants appeared before the {\tt delta} flag. +%\end{ErrMsgs} + + +\subsection{\tt red} +\tacindex{red} + +This tactic applies to a goal that has the form {\tt + forall (x:T1)\dots(xk:Tk), t} with {\tt t} +$\beta\iota\zeta$-reducing to {\tt c t1 \dots\ tn} and {\tt c} a +constant. If +{\tt c} is transparent then it replaces {\tt c} with its definition +(say {\tt t}) and then reduces {\tt (t t1 \dots\ tn)} according to +$\beta\iota\zeta$-reduction rules. + +\begin{ErrMsgs} +\item \errindex{Not reducible} +\end{ErrMsgs} + +\subsection{\tt hnf} +\tacindex{hnf} + +This tactic applies to any goal. It replaces the current goal with its +head normal form according to the $\beta\delta\iota\zeta$-reduction +rules, i.e. it reduces the head of the goal until it becomes a +product or an irreducible term. All inner $\beta\iota$-redexes are also +reduced. + +\Example +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). + +\subsection{\texorpdfstring{\texttt{cbn}}{cbn} and \texorpdfstring{\texttt{simpl}}{simpl}} +\tacindex{cbn} \tacindex{simpl} + +These tactics apply to any goal. They try to reduce a term to +something still readable instead of fully normalizing it. They perform +a sort of strong normalization with two key differences: +\begin{itemize} +\item They unfold a constant if and only if it leads to a + $\iota$-reduction, i.e. reducing a match or unfolding a fixpoint. +\item While reducing a constant unfolding to (co)fixpoints, + the tactics use the name of the + constant the (co)fixpoint comes from instead of the (co)fixpoint + definition in recursive calls. +\end{itemize} + +The \texttt{cbn} tactic is claimed to be a more principled, faster and more +predictable replacement for \texttt{simpl}. + +The \texttt{cbn} tactic accepts the same flags as \texttt{cbv} and +\texttt{lazy}. The behavior of both \texttt{simpl} and \texttt{cbn} +can be tuned using the \texttt{Arguments} vernacular command as +follows: \comindex{Arguments} +\begin{itemize} +\item +A constant can be marked to be never unfolded by \texttt{cbn} or +\texttt{simpl}: +\begin{coq_example*} +Arguments minus n m : simpl never. +\end{coq_example*} +After that command an expression like \texttt{(minus (S x) y)} is left +untouched by the tactics \texttt{cbn} and \texttt{simpl}. +\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. +\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 !n !m. +\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 n m : 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} + +In detail, the tactic \texttt{simpl} first applies +$\beta\iota$-reduction. Then, it expands transparent constants and +tries to reduce further using $\beta\iota$-reduction. But, when no +$\iota$ rule is applied after unfolding then $\delta$-reductions are +not applied. For instance trying to use \texttt{simpl} on +\texttt{(plus n O)=n} changes nothing. + +Notice that only transparent constants whose name can be reused in the +recursive calls are possibly unfolded by \texttt{simpl}. For instance +a constant defined by \texttt{plus' := plus} is possibly unfolded and +reused in the recursive calls, but a constant such as \texttt{succ := + plus (S O)} is never unfolded. This is the main difference between +\texttt{simpl} and \texttt{cbn}. The tactic \texttt{cbn} reduces +whenever it will be able to reuse it or not: \texttt{succ t} is +reduced to \texttt{S t}. + +\tacindex{simpl \dots\ in} +\begin{Variants} +\item {\tt cbn [\qualid$_1$\ldots\qualid$_k$]}\\ + {\tt cbn -[\qualid$_1$\ldots\qualid$_k$]} + + These are respectively synonyms of {\tt cbn beta delta + [\qualid$_1$\ldots\qualid$_k$] iota zeta} and {\tt cbn beta delta + -[\qualid$_1$\ldots\qualid$_k$] iota zeta} (see \ref{vmcompute}). + +\item {\tt simpl {\pattern}} + + This applies {\tt simpl} only to the subterms matching {\pattern} in the + current goal. + +\item {\tt simpl {\pattern} at \num$_1$ \dots\ \num$_i$} + + This applies {\tt simpl} only to the \num$_1$, \dots, \num$_i$ + occurrences of the subterms matching {\pattern} in the current goal. + + \ErrMsg {\tt Too few occurrences} + +\item {\tt simpl {\qualid}}\\ + {\tt simpl {\qstring}} + + This applies {\tt simpl} only to the applicative subterms whose head + occurrence is the unfoldable constant {\qualid} (the constant can be + referred to by its notation using {\qstring} if such a notation + exists). + +\item {\tt simpl {\qualid} at \num$_1$ \dots\ \num$_i$}\\ + {\tt simpl {\qstring} at \num$_1$ \dots\ \num$_i$}\\ + + This applies {\tt simpl} only to the \num$_1$, \dots, \num$_i$ + applicative subterms whose head occurrence is {\qualid} (or + {\qstring}). + +\end{Variants} + +\begin{quote} + \optindex{Debug RAKAM} + {\tt Set Debug RAKAM} +\end{quote} +This option makes {\tt cbn} print various debugging information. +{\tt RAKAM} is the Refolding Algebraic Krivine Abstract Machine. + +\subsection{\tt unfold \qualid} +\tacindex{unfold} +\label{unfold} + +This tactic applies to any goal. The argument {\qualid} must denote a +defined transparent constant or local definition (see Sections~\ref{Basic-definitions} and~\ref{Transparent}). The tactic {\tt + unfold} applies the $\delta$ rule to each occurrence of the constant +to which {\qualid} refers in the current goal and then replaces it +with its $\beta\iota$-normal form. + +\begin{ErrMsgs} +\item {\qualid} \errindex{does not denote an evaluable constant} + +\end{ErrMsgs} + +\begin{Variants} +\item {\tt unfold {\qualid} in {\ident}} + \tacindex{unfold \dots in} + + Replaces {\qualid} in hypothesis {\ident} with its definition + and replaces the hypothesis with its $\beta\iota$ normal form. + +\item {\tt unfold {\qualid}$_1$, \dots, \qualid$_n$} + + Replaces {\em simultaneously} {\qualid}$_1$, \dots, {\qualid}$_n$ + with their definitions and replaces the current goal with its + $\beta\iota$ normal form. + +\item {\tt unfold {\qualid}$_1$ at \num$_1^1$, \dots, \num$_i^1$, +\dots,\ \qualid$_n$ at \num$_1^n$ \dots\ \num$_j^n$} + + The lists \num$_1^1$, \dots, \num$_i^1$ and \num$_1^n$, \dots, + \num$_j^n$ specify the occurrences of {\qualid}$_1$, \dots, + \qualid$_n$ to be unfolded. Occurrences are located from left to + right. + + \ErrMsg {\tt bad occurrence number of {\qualid}$_i$} + + \ErrMsg {\qualid}$_i$ {\tt does not occur} + +\item {\tt unfold {\qstring}} + + If {\qstring} denotes the discriminating symbol of a notation (e.g. {\tt + "+"}) or an expression defining a notation (e.g. \verb!"_ + _"!), and + this notation refers to an unfoldable constant, then the tactic + unfolds it. + +\item {\tt unfold {\qstring}\%{\delimkey}} + + This is variant of {\tt unfold {\qstring}} where {\qstring} gets its + interpretation from the scope bound to the delimiting key + {\delimkey} instead of its default interpretation (see + Section~\ref{scopechange}). + +\item {\tt unfold \qualidorstring$_1$ at \num$_1^1$, \dots, \num$_i^1$, +\dots,\ \qualidorstring$_n$ at \num$_1^n$ \dots\ \num$_j^n$} + + This is the most general form, where {\qualidorstring} is either a + {\qualid} or a {\qstring} referring to a notation. + +\end{Variants} + +\subsection{\tt fold \term} +\tacindex{fold} + +This tactic applies to any goal. The term \term\ is reduced using the {\tt red} +tactic. Every occurrence of the resulting term in the goal is then +replaced by \term. + +\begin{Variants} +\item {\tt fold} \term$_1$ \dots\ \term$_n$ + + Equivalent to {\tt fold} \term$_1${\tt;}\ldots{\tt; fold} \term$_n$. +\end{Variants} + +\subsection{\tt pattern \term} +\tacindex{pattern} +\label{pattern} + +This command applies to any goal. The argument {\term} must be a free +subterm of the current goal. The command {\tt pattern} performs +$\beta$-expansion (the inverse of $\bt$-reduction) of the current goal +(say \T) by +\begin{enumerate} +\item replacing all occurrences of {\term} in {\T} with a fresh variable +\item abstracting this variable +\item applying the abstracted goal to {\term} +\end{enumerate} + +For instance, if the current goal $T$ is expressible as $\phi(t)$ +where the notation captures all the instances of $t$ in $\phi(t)$, +then {\tt pattern $t$} transforms it into {\tt (fun x:$A$ => $\phi(${\tt +x}$)$) $t$}. This command can be used, for instance, when the tactic +{\tt apply} fails on matching. + +\begin{Variants} +\item {\tt pattern {\term} at {\num$_1$} \dots\ {\num$_n$}} + + Only the occurrences {\num$_1$} \dots\ {\num$_n$} of {\term} are + considered for $\beta$-expansion. Occurrences are located from left + to right. + +\item {\tt pattern {\term} at - {\num$_1$} \dots\ {\num$_n$}} + + All occurrences except the occurrences of indexes {\num$_1$} \dots\ + {\num$_n$} of {\term} are considered for + $\beta$-expansion. Occurrences are located from left to right. + +\item {\tt pattern {\term$_1$}, \dots, {\term$_m$}} + + 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 + generated types $A_j$ these occurrences will also be considered and + possibly abstracted. + +\item {\tt pattern {\term$_1$} at {\num$_1^1$} \dots\ {\num$_{n_1}^1$}, \dots, + {\term$_m$} at {\num$_1^m$} \dots\ {\num$_{n_m}^m$}} + + This behaves as above but processing only the occurrences \num$_1^1$, + \dots, \num$_i^1$ of \term$_1$, \dots, \num$_1^m$, \dots, \num$_j^m$ + of \term$_m$ starting from \term$_m$. + +\item {\tt pattern} {\term$_1$} \zeroone{{\tt at \zeroone{-}} {\num$_1^1$} \dots\ {\num$_{n_1}^1$}} {\tt ,} \dots {\tt ,} + {\term$_m$} \zeroone{{\tt at \zeroone{-}} {\num$_1^m$} \dots\ {\num$_{n_m}^m$}} + + This is the most general syntax that combines the different variants. + +\end{Variants} + +\subsection{Conversion tactics applied to hypotheses} + +{\convtactic} {\tt in} \ident$_1$ \dots\ \ident$_n$ + +Applies the conversion tactic {\convtactic} to the +hypotheses \ident$_1$, \ldots, \ident$_n$. The tactic {\convtactic} is +any of the conversion tactics listed in this section. + +If \ident$_i$ is a local definition, then \ident$_i$ can be replaced +by (Type of \ident$_i$) to address not the body but the type of the +local definition. Example: {\tt unfold not in (Type of H1) (Type of H3).} + +\begin{ErrMsgs} +\item \errindex{No such hypothesis} : {\ident}. +\end{ErrMsgs} + + +\section{Automation} +\subsection{\tt auto} +\label{auto} +\tacindex{auto} + +This tactic implements a Prolog-like resolution procedure to solve the +current goal. It first tries to solve the goal using the {\tt + assumption} tactic, then it reduces the goal to an atomic one using +{\tt intros} and introduces the newly generated hypotheses as hints. +Then it looks at the list of tactics associated to the head symbol of +the goal and tries to apply one of them (starting from the tactics +with lower cost). This process is recursively applied to the generated +subgoals. + +By default, \texttt{auto} only uses the hypotheses of the current goal and the +hints of the database named {\tt core}. + +\begin{Variants} + +\item {\tt auto \num} + + Forces the search depth to be \num. The maximal search depth is 5 by + default. + +\item {\tt auto with \ident$_1$ \dots\ \ident$_n$} + + Uses the hint databases $\ident_1$ \dots\ $\ident_n$ in addition to + the database {\tt core}. See Section~\ref{Hints-databases} for the + list of pre-defined databases and the way to create or extend a + database. + +\item {\tt auto with *} + + Uses all existing hint databases. See Section~\ref{Hints-databases} + +\item \texttt{auto using} \nterm{lemma}$_1$ {\tt ,} {\ldots} {\tt ,} \nterm{lemma}$_n$ + + Uses \nterm{lemma}$_1$, \ldots, \nterm{lemma}$_n$ in addition to + hints (can be combined with the \texttt{with \ident} option). If + $lemma_i$ is an inductive type, it is the collection of its + constructors which is added as hints. + +\item {\tt info\_auto} + + Behaves like {\tt auto} but shows the tactics it uses to solve the goal. + This variant is very useful for getting a better understanding of automation, + or to know what lemmas/assumptions were used. + +\item {\tt debug auto} Behaves like {\tt auto} but shows the tactics + it tries to solve the goal, including failing paths. + +\item {\tt \zeroone{info\_}auto \zeroone{\num}} \zeroone{{\tt using} \nterm{lemma}$_1$ + {\tt ,} {\ldots} {\tt ,} \nterm{lemma}$_n$} \zeroone{{\tt with} + \ident$_1$ {\ldots} \ident$_n$} + + This is the most general form, combining the various options. + +\item {\tt trivial}\tacindex{trivial} + + This tactic is a restriction of {\tt auto} that is not recursive and + tries only hints that cost 0. Typically it solves trivial + equalities like $X=X$. + +\item \texttt{trivial with \ident$_1$ \dots\ \ident$_n$} + +\item \texttt{trivial with *} + +\item \texttt{trivial using} \nterm{lemma}$_1$ {\tt ,} {\ldots} {\tt ,} \nterm{lemma}$_n$ + +\item {\tt info\_trivial} + +\item {\tt debug trivial} + +\item {\tt \zeroone{info\_}trivial} \zeroone{{\tt using} \nterm{lemma}$_1$ + {\tt ,} {\ldots} {\tt ,} \nterm{lemma}$_n$} \zeroone{{\tt with} + \ident$_1$ {\ldots} \ident$_n$} + +\end{Variants} + +\Rem {\tt auto} either solves completely the goal or else leaves it +intact. \texttt{auto} and \texttt{trivial} never fail. + +\Rem The following options enable printing of informative or debug +information for the {\tt auto} and {\tt trivial} tactics: +\begin{quote} + \optindex{Info Auto} + {\tt Set Info Auto} + \optindex{Debug Auto} + {\tt Set Debug Auto} + \optindex{Info Trivial} + {\tt Set Info Trivial} + \optindex{Debug Trivial} + {\tt Set Debug Trivial} +\end{quote} + +\SeeAlso Section~\ref{Hints-databases} + +\subsection{\tt eauto} +\tacindex{eauto} +\label{eauto} + +This tactic generalizes {\tt auto}. While {\tt auto} does not try +resolution hints which would leave existential variables in the goal, +{\tt eauto} does try them (informally speaking, it uses +{\tt simple eapply} where {\tt auto} uses {\tt simple apply}). +As a consequence, {\tt eauto} can solve such a goal: + +\begin{coq_eval} +Reset Initial. +\end{coq_eval} +\begin{coq_example} +Hint Resolve ex_intro. +Goal forall P:nat -> Prop, P 0 -> exists n, P n. +eauto. +\end{coq_example} +\begin{coq_eval} +Abort. +\end{coq_eval} + +Note that {\tt ex\_intro} should be declared as a hint. + +\begin{Variants} + +\item {\tt \zeroone{info\_}eauto \zeroone{\num}} \zeroone{{\tt using} \nterm{lemma}$_1$ + {\tt ,} {\ldots} {\tt ,} \nterm{lemma}$_n$} \zeroone{{\tt with} + \ident$_1$ {\ldots} \ident$_n$} + + The various options for eauto are the same as for auto. + +\end{Variants} + +\Rem {\tt eauto} obeys the following options: +\begin{quote} + \optindex{Info Eauto} + {\tt Set Info Eauto} + \optindex{Debug Eauto} + {\tt Set Debug Eauto} +\end{quote} + +\SeeAlso Section~\ref{Hints-databases} + +\subsection{\tt autounfold with \ident$_1$ \mbox{\dots} \ident$_n$} +\tacindex{autounfold} +\label{autounfold} + +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 \nterm{clause}} + + Performs the unfolding in the given clause. + +\item {\tt autounfold with *} + + Uses the unfold hints declared in all the hint databases. +\end{Variants} + + +\subsection{\tt autorewrite with \ident$_1$ \mbox{\dots} \ident$_n$} +\label{tactic:autorewrite} +\tacindex{autorewrite} + +This tactic \footnote{The behavior of this tactic has much changed compared to +the versions available in the previous distributions (V6). This may cause +significant changes in your theories to obtain the same result. As a drawback +of the re-engineering 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 +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 +the next base is processed. For the bases, the behavior is exactly similar to +the processing of the rewriting rules. + +The rewriting rule bases are built with the {\tt Hint~Rewrite} vernacular +command. + +\Warning{} This tactic may loop if you build non terminating rewriting systems. + +\begin{Variant} +\item {\tt autorewrite with \ident$_1$ \mbox{\dots} \ident$_n$ using \tac} + +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 {\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 {\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} + +\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 +this tactic. + +% En attente d'un moyen de valoriser les fichiers de demos +%\SeeAlso file \texttt{contrib/Rocq/DEMOS/Demo\_AutoRewrite.v} + +\subsection{\tt easy} +\tacindex{easy} +\label{easy} + +This tactic tries to solve the current goal by a number of standard closing steps. +In particular, it tries to close the current goal using the closing tactics +{\tt trivial}, reflexivity, symmetry, contradiction and inversion of hypothesis. +If this fails, it tries introducing variables and splitting and-hypotheses, +using the closing tactics afterwards, and splitting the goal using {\tt split} and recursing. + +This tactic solves goals that belong to many common classes; in particular, many cases of +unsatisfiable hypotheses, and simple equality goals are usually solved by this tactic. + +\begin{Variant} +\item {\tt now \tac} + \tacindex{now} + + Run \tac\/ followed by easy. This is a notation for {\tt \tac; easy}. +\end{Variant} + +\section{Controlling automation} + +\subsection{The hints databases for {\tt auto} and {\tt eauto}} +\index{Hints databases} +\label{Hints-databases} +\comindex{Hint} + +The hints for \texttt{auto} and \texttt{eauto} are stored in +databases. Each database maps head symbols to a list of hints. One can +use the command \texttt{Print Hint \ident} to display the hints +associated to the head symbol \ident{} (see \ref{PrintHint}). Each +hint has a cost that is a nonnegative integer, and an optional pattern. +The hints with lower cost are tried first. A hint is tried by +\texttt{auto} when the conclusion of the current goal +matches its pattern or when it has no pattern. + +\subsubsection*{Creating Hint databases + \label{CreateHintDb}\comindex{CreateHintDb}} + +One can optionally declare a hint database using the command +\texttt{Create HintDb}. If a hint is added to an unknown database, it +will be automatically created. + +\medskip +\texttt{Create HintDb} {\ident} [\texttt{discriminated}] +\medskip + +This command creates a new database named \ident. +The database is implemented by a Discrimination Tree (DT) that serves as +an index of all the lemmas. The DT can use transparency information to decide +if a constant should be indexed or not (c.f. \ref{HintTransparency}), +making the retrieval more efficient. +The legacy implementation (the default one for new databases) uses the +DT only on goals without existentials (i.e., auto goals), for non-Immediate +hints and do not make use of transparency hints, putting more work on the +unification that is run after retrieval (it keeps a list of the lemmas +in case the DT is not used). The new implementation enabled by +the {\tt discriminated} option makes use of DTs in all cases and takes +transparency information into account. However, the order in which hints +are retrieved from the DT may differ from the order in which they were +inserted, making this implementation observationally different from the +legacy one. + +The general +command to add a hint to some databases \ident$_1$, \dots, \ident$_n$ is +\begin{tabbing} + {\tt Hint {\hintdef} :~\ident$_1$ \mbox{\dots} \ident$_n$} +\end{tabbing} + +\begin{Variants} +\item {\tt Hint \hintdef} + + No database name is given: the hint is registered in the {\tt core} + database. + +\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 {\tt Local Hint \hintdef} + + Idem for the {\tt core} database. + +\end{Variants} + +The {\hintdef} is one of the following expressions: + +\begin{itemize} +\item {\tt Resolve \term {\zeroone{{\tt |} \zeroone{\num} \zeroone{\pattern}}}} + \comindex{Hint Resolve} + + This command adds {\tt simple apply {\term}} to the hint list + with the head symbol of the type of \term. The cost of that hint is + the number of subgoals generated by {\tt simple apply {\term}} or \num + if specified. The associated pattern is inferred from the conclusion + of the type of \term or the given \pattern if specified. +%{\tt auto} actually uses a slightly modified variant of {\tt simple apply} with use_metas_eagerly_in_conv_on_closed_terms set to false + + In case the inferred type of \term\ does not start with a product + the tactic added in the hint list is {\tt exact {\term}}. +% Actually, a slightly restricted version is used (no conversion on the head symbol) + In case + this type can however be reduced to a type starting with a product, + the tactic {\tt simple apply {\term}} is also stored in the hints list. + + If the inferred type of \term\ contains a dependent quantification + on a variable which occurs only in the premisses of the type and not + in its conclusion, no instance could be inferred for the variable by + unification with the goal. In this case, the hint is added to the + hint list of {\tt eauto} (see \ref{eauto}) instead of the hint list + of {\tt auto} and a warning is printed. A typical example of a hint + that is used only by \texttt{eauto} is a transitivity lemma. + + \begin{ErrMsgs} +%% \item \errindex{Bound head variable} + + \item \term\ \errindex{cannot be used as a hint} + + The head symbol of the type of {\term} is a bound variable such + that this tactic cannot be associated to a constant. + + %% The type of {\term} contains products over variables that do not + %% appear in the conclusion. A typical example is a transitivity axiom. + %% In that case the {\tt simple apply} tactic fails, and thus is useless. + + \end{ErrMsgs} + + \begin{Variants} + + \item {\tt Resolve \term$_1$ \mbox{\dots} \term$_m$} + + Adds each \texttt{Resolve} {\term$_i$}. + + \item {\tt Resolve -> \term} + + Adds the left-to-right implication of an equivalence as a hint + (informally the hint will be used as {\tt apply <- \term}, + although as mentionned before, the tactic actually used is + a restricted version of apply). + + \item {\tt Resolve <- \term} + + Adds the right-to-left implication of an equivalence as a hint. + + \end{Variants} + +\item \texttt{Immediate {\term}} +\comindex{Hint Immediate} + + This command adds {\tt simple apply {\term}; trivial} to the hint list + associated with the head symbol of the type of {\ident} in the given + database. This tactic will fail if all the subgoals generated by + {\tt simple apply {\term}} are not solved immediately by the {\tt trivial} + tactic (which only tries tactics with cost $0$). + + This command is useful for theorems such as the symmetry of equality + or $n+1=m+1 \to n=m$ that we may like to introduce with a + limited use in order to avoid useless proof-search. + + The cost of this tactic (which never generates subgoals) is always 1, + so that it is not used by {\tt trivial} itself. + + \begin{ErrMsgs} + +%% \item \errindex{Bound head variable} + + \item \term\ \errindex{cannot be used as a hint} + + \end{ErrMsgs} + + \begin{Variants} + + \item {\tt Immediate \term$_1$ \mbox{\dots} \term$_m$} + + Adds each \texttt{Immediate} {\term$_i$}. + + \end{Variants} + +\item \texttt{Constructors} {\ident} +\comindex{Hint Constructors} + + If {\ident} is an inductive type, this command adds all its + constructors as hints of type \texttt{Resolve}. Then, when the + conclusion of current goal has the form \texttt{({\ident} \dots)}, + \texttt{auto} will try to apply each constructor. + + \begin{ErrMsgs} + + \item {\ident} \errindex{is not an inductive type} + +% No need to have this message here, is is generic to all commands +% referring to globals +%% \item {\ident} \errindex{not declared} + + \end{ErrMsgs} + + \begin{Variants} + + \item {\tt Constructors \ident$_1$ \mbox{\dots} \ident$_m$} + + Adds each \texttt{Constructors} {\ident$_i$}. + + \end{Variants} + +\item \texttt{Unfold} {\qualid} +\comindex{Hint Unfold} + + This adds the tactic {\tt unfold {\qualid}} to the hint list that + will only be used when the head constant of the goal is \ident. Its + cost is 4. + + \begin{Variants} + + \item {\tt Unfold \ident$_1$ \mbox{\dots} \ident$_m$} + + Adds each \texttt{Unfold} {\ident$_i$}. + + \end{Variants} + +\item \texttt{Transparent}, \texttt{Opaque} {\qualid} +\label{HintTransparency} +\comindex{Hint Transparent} +\comindex{Hint Opaque} + + This adds a transparency hint to the database, making {\tt {\qualid}} + a transparent or opaque constant during resolution. This information + is used during unification of the goal with any lemma in the database + and inside the discrimination network to relax or constrain it in the + case of \texttt{discriminated} databases. + + \begin{Variants} + + \item \texttt{Transparent}, \texttt{Opaque} {\ident$_1$} \mbox{\dots} {\ident$_m$} + + Declares each {\ident$_i$} as a transparent or opaque constant. + + \end{Variants} + +\item \texttt{Extern \num\ [\pattern]\ => }\textsl{tactic} +\comindex{Hint Extern} + + This hint type is to extend \texttt{auto} with tactics other than + \texttt{apply} and \texttt{unfold}. For that, we must specify a + cost, an optional pattern and a tactic to execute. Here is an example: + +\begin{quotation} +\begin{verbatim} +Hint Extern 4 (~(_ = _)) => discriminate. +\end{verbatim} +\end{quotation} + + Now, when the head of the goal is a disequality, \texttt{auto} will + try \texttt{discriminate} if it does not manage to solve the goal + with hints with a cost less than 4. + + One can even use some sub-patterns of the pattern in the tactic + script. A sub-pattern is a question mark followed by an identifier, like + \texttt{?X1} or \texttt{?X2}. Here is an example: + +% Require EqDecide. +\begin{coq_example*} +Require Import List. +\end{coq_example*} +\begin{coq_example} +Hint Extern 5 ({?X1 = ?X2} + {?X1 <> ?X2}) => + generalize X1, X2; decide equality : eqdec. +Goal +forall a b:list (nat * nat), {a = b} + {a <> b}. +Info 1 auto with eqdec. +\end{coq_example} +\begin{coq_eval} +Abort. +\end{coq_eval} + +\item \texttt{Cut} {\textit{regexp}} +\label{HintCut} +\comindex{Hint Cut} + + \textit{Warning:} these hints currently only apply to typeclass proof search and + the \texttt{typeclasses eauto} tactic (\ref{typeclasseseauto}). + + This command can be used to cut the proof-search tree according to a + regular expression matching paths to be cut. The grammar for regular + expressions is the following. Beware, there is no operator precedence + during parsing, one can check with \texttt{Print HintDb} to verify the + current cut expression: +\[\begin{array}{lcll} + e & ::= & \ident & \text{ hint or instance identifier } \\ + & & \texttt{\_} & \text{ any hint } \\ + & & e | e' & \text{ disjunction } \\ + & & e e' & \text{ sequence } \\ + & & e * & \text{ Kleene star } \\ + & & \texttt{emp} & \text{ empty } \\ + & & \texttt{eps} & \text{ epsilon } \\ + & & \texttt{(} e \texttt{)} & +\end{array}\] + +The \texttt{emp} regexp does not match any search path while +\texttt{eps} matches the empty path. During proof search, the path of +successive successful hints on a search branch is recorded, as a list of +identifiers for the hints (note \texttt{Hint Extern}'s do not have an +associated identifier). Before applying any hint $\ident$ the current +path $p$ extended with $\ident$ is matched against the current cut +expression $c$ associated to the hint database. If matching succeeds, +the hint is \emph{not} applied. The semantics of \texttt{Hint Cut} $e$ +is to set the cut expression to $c | e$, the initial cut expression +being \texttt{emp}. + + +\item \texttt{Mode} {\qualid} {\tt (+ | ! | -)}$^*$ +\label{HintMode} +\comindex{Hint Mode} + +This sets an optional mode of use of the identifier {\qualid}. When +proof-search faces a goal that ends in an application of {\qualid} to +arguments {\tt \term$_1$ \mbox{\dots} \term$_n$}, the mode tells if the +hints associated to qualid can be applied or not. A mode specification +is a list of $n$ {\tt +}, {\tt !} or {\tt -} items that specify if an +argument of the identifier is to be treated as an input ({\tt +}), if +its head only is an input ({\tt !}) or an output ({\tt -}) of the +identifier. For a mode to match a list of arguments, input terms and +input heads \emph{must not} contain existential variables or be +existential variables respectively, while outputs can be any +term. Multiple modes can be declared for a single identifier, in that +case only one mode needs to match the arguments for the hints to be +applied. + +The head of a term is understood here as the applicative head, or the +match or projection scrutinee's head, recursively, casts being ignored. + +{\tt Hint Mode} is especially useful for typeclasses, when one does not +want to support default instances and avoid ambiguity in +general. Setting a parameter of a class as an input forces proof-search +to be driven by that index of the class, with {\tt !} giving more +flexibility by allowing existentials to still appear deeper in the index +but not at its head. + +\end{itemize} + +\Rem One can use an \texttt{Extern} hint with no pattern to do +pattern-matching on hypotheses using \texttt{match goal with} inside +the tactic. + +% There are shortcuts that allow to define several goal at once: + +% \begin{itemize} +% \item \comindex{Hints Resolve}\texttt{Hints Resolve \ident$_1$ \dots\ \ident$_n$ : \ident.}\\ +% This command is a shortcut for the following ones: +% \begin{quotation} +% \noindent\texttt{Hint \ident$_1$ : \ident\ := Resolve \ident$_1$}\\ +% \dots\\ +% \texttt{Hint \ident$_1$ : \ident := Resolve \ident$_1$} +% \end{quotation} +% Notice that the hint name is the same that the theorem given as +% hint. +% \item \comindex{Hints Immediate}\texttt{Hints Immediate \ident$_1$ \dots\ \ident$_n$ : \ident.}\\ +% \item \comindex{Hints Unfold}\texttt{Hints Unfold \qualid$_1$ \dots\ \qualid$_n$ : \ident.}\\ +% \end{itemize} + +%\begin{Warnings} +% \item \texttt{Overriding hint named \dots\ in database \dots} +%\end{Warnings} + + + +\subsection{Hint databases defined in the \Coq\ standard library} + +Several hint databases are defined in the \Coq\ standard library. The +actual content of a database is the collection of the hints declared +to belong to this database in each of the various modules currently +loaded. Especially, requiring new modules potentially extend a +database. At {\Coq} startup, only the {\tt core} database is non empty +and can be used. + +\begin{description} + +\item[\tt core] This special database is automatically used by + \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. + +\item[\tt arith] This database contains all lemmas about Peano's + arithmetic proved in the directories \texttt{Init} and + \texttt{Arith} + +\item[\tt zarith] contains lemmas about binary signed integers from + the directories \texttt{theories/ZArith}. When required, the module + {\tt Omega} also extends the database {\tt zarith} with a high-cost + hint that calls {\tt omega} on equations and inequalities in {\tt + nat} or {\tt Z}. + +\item[\tt bool] contains lemmas about booleans, mostly from directory + \texttt{theories/Bool}. + +\item[\tt datatypes] is for lemmas about lists, streams and so on that + are mainly proved in the \texttt{Lists} subdirectory. + +\item[\tt sets] contains lemmas about sets and relations from the + directories \texttt{Sets} and \texttt{Relations}. + +\item[\tt typeclass\_instances] contains all the type class instances + declared in the environment, including those used for \texttt{setoid\_rewrite}, + from the \texttt{Classes} directory. +\end{description} + +You are advised not to put your own hints in the {\tt core} database, +but use one or several databases specific to your development. + +\subsection{\tt Remove Hints \term$_1$ \mbox{\dots} \term$_n$ :~ \ident$_1$ + \mbox{\dots} \ident$_m$} +\label{RemoveHints} +\comindex{Remove Hints} + +This command removes the hints associated to terms \term$_1$ \mbox{\dots} +\term$_n$ in databases \ident$_1$ \mbox{\dots} \ident$_m$. + +\subsection{\tt Print Hint} +\label{PrintHint} +\comindex{Print Hint} + +This command displays all hints that apply to the current goal. It +fails if no proof is being edited, while the two variants can be used at +every moment. + +\begin{Variants} + +\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 + command will not fail if no goal is being edited. + +\item {\tt Print Hint *} + + This command displays all declared hints. + +\item {\tt Print HintDb \ident} +\label{PrintHintDb} +\comindex{Print HintDb} + + This command displays all hints from database \ident. + +\end{Variants} + +\subsection{\tt Hint Rewrite \term$_1$ \mbox{\dots} \term$_n$ :~ \ident$_1$ \mbox{\dots} \ident$_m$} +\label{HintRewrite} +\comindex{Hint Rewrite} + +This vernacular command adds the terms {\tt \term$_1$ \mbox{\dots} \term$_n$} +(their types must be equalities) in the rewriting bases \ident$_1$, \dots, \ident$_m$ +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$ \mbox{\dots} \term$_n$ :~\ident$_1$ \mbox{\dots} \ident$_m$} + +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$ \mbox{\dots} \term$_n$ :~\ident$_1$ \mbox{\dots} \ident$_m$} + +Adds the rewriting rules {\tt \term$_1$ \mbox{\dots} \term$_n$} with a right-to-left +orientation in the bases \ident$_1$, \dots, \ident$_m$. + +\item {\tt Hint Rewrite \term$_1$ \mbox{\dots} \term$_n$ using {\tac} :~\ident$_1$ \mbox{\dots} \ident$_m$} + +When the rewriting rules {\tt \term$_1$ \mbox{\dots} \term$_n$} in \ident$_1$, \dots, \ident$_m$ 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{Hint locality +\label{Hint-Locality}} +\optindex{Loose Hint Behavior} + +Hints provided by the \texttt{Hint} commands are erased when closing a +section. Conversely, all hints of a module \texttt{A} that are not +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.}). + +As of today, hints only have a binary behavior regarding locality, as described +above: either they disappear at the end of a section scope, or they remain +global forever. This causes a scalability issue, because hints coming from an +unrelated part of the code may badly influence another development. It can be +mitigated to some extent thanks to the {\tt Remove Hints} command +(see ~\ref{RemoveHints}), but this is a mere workaround and has some +limitations (for instance, external hints cannot be removed). + +A proper way to fix this issue is to bind the hints to their module scope, as +for most of the other objects Coq uses. Hints should only made available when +the module they are defined in is imported, not just required. It is very +difficult to change the historical behavior, as it would break a lot of scripts. +We propose a smooth transitional path by providing the {\tt Loose Hint Behavior} +option which accepts three flags allowing for a fine-grained handling of +non-imported hints. + +\begin{Variants} + +\item {\tt Set Loose Hint Behavior "Lax"} + + This is the default, and corresponds to the historical behavior, that is, + hints defined outside of a section have a global scope. + +\item {\tt Set Loose Hint Behavior "Warn"} + + When set, it outputs a warning when a non-imported hint is used. Note that + this is an over-approximation, because a hint may be triggered by a run that + will eventually fail and backtrack, resulting in the hint not being actually + useful for the proof. + +\item {\tt Set Loose Hint Behavior "Strict"} + + When set, it changes the behavior of an unloaded hint to a immediate fail + tactic, allowing to emulate an import-scoped hint mechanism. + +\end{Variants} + +\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}. + +\begin{Variants} + +\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$ \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}}\label{DeclareImplicit} +\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} +\begin{coq_eval} +Clear Implicit Tactic. +Reset Initial. +\end{coq_eval} + +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{Decision procedures} + +\subsection{\tt tauto} +\tacindex{tauto} +\tacindex{dtauto} +\label{tauto} + +This tactic implements a decision procedure for intuitionistic propositional +calculus based on the contraction-free sequent calculi LJT* of Roy Dyckhoff +\cite{Dyc92}. Note that {\tt tauto} succeeds on any instance of an +intuitionistic tautological proposition. {\tt tauto} unfolds negations +and logical equivalence but does not unfold any other definition. + +The following goal can be proved by {\tt tauto} whereas {\tt auto} +would fail: + +\begin{coq_example} +Goal forall (x:nat) (P:nat -> Prop), x = 0 \/ P x -> x <> 0 -> P x. + intros. + tauto. +\end{coq_example} +\begin{coq_eval} +Abort. +\end{coq_eval} + +Moreover, if it has nothing else to do, {\tt tauto} performs +introductions. Therefore, the use of {\tt intros} in the previous +proof is unnecessary. {\tt tauto} can for instance prove the +following: +\begin{coq_example} +(* auto would fail *) +Goal forall (A:Prop) (P:nat -> Prop), + A \/ (forall x:nat, ~ A -> P x) -> forall x:nat, ~ A -> P x. + + tauto. +\end{coq_example} +\begin{coq_eval} +Abort. +\end{coq_eval} + +\Rem In contrast, {\tt tauto} cannot solve the following goal + +\begin{coq_example*} +Goal forall (A:Prop) (P:nat -> Prop), + A \/ (forall x:nat, ~ A -> P x) -> forall x:nat, ~ ~ (A \/ P x). +\end{coq_example*} +\begin{coq_eval} +Abort. +\end{coq_eval} + +because \verb=(forall x:nat, ~ A -> P x)= cannot be treated as atomic and an +instantiation of \verb=x= is necessary. + +\begin{Variants} + +\item {\tt dtauto} + + While {\tt tauto} recognizes inductively defined connectives + isomorphic to the standard connective {\tt and}, {\tt prod}, {\tt + or}, {\tt sum}, {\tt False}, {\tt Empty\_set}, {\tt unit}, {\tt + True}, {\tt dtauto} recognizes also all inductive types with + one constructors and no indices, i.e. record-style connectives. + +\end{Variants} + +\subsection{\tt intuition \tac} +\tacindex{intuition} +\tacindex{dintuition} +\label{intuition} + +The tactic \texttt{intuition} takes advantage of the search-tree built +by the decision procedure involved in the tactic {\tt tauto}. It uses +this information to generate a set of subgoals equivalent to the +original one (but simpler than it) and applies the tactic +{\tac} to them \cite{Mun94}. If this tactic fails on some goals then +{\tt intuition} fails. In fact, {\tt tauto} is simply {\tt intuition + fail}. + +For instance, the tactic {\tt intuition auto} applied to the goal +\begin{verbatim} +(forall (x:nat), P x)/\B -> (forall (y:nat),P y)/\ P O \/B/\ P O +\end{verbatim} +internally replaces it by the equivalent one: +\begin{verbatim} +(forall (x:nat), P x), B |- P O +\end{verbatim} +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 re-engineered by David~Delahaye using mainly the tactic +language (see Chapter~\ref{TacticLanguage}). The code is now much shorter and +a significant increase in performance 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 +incompatibilities. + +\begin{Variants} +\item {\tt intuition} + + Is equivalent to {\tt intuition auto with *}. + +\item {\tt dintuition} + + While {\tt intuition} recognizes inductively defined connectives + isomorphic to the standard connective {\tt and}, {\tt prod}, {\tt + or}, {\tt sum}, {\tt False}, {\tt Empty\_set}, {\tt unit}, {\tt + True}, {\tt dintuition} recognizes also all inductive types with + one constructors and no indices, i.e. record-style connectives. + +\end{Variants} + +\optindex{Intuition Negation Unfolding} + +Some aspects of the tactic {\tt intuition} can be +controlled using options. To avoid that inner negations which do not +need to be unfolded are unfolded, use: + +\begin{quote} +{\tt Unset Intuition Negation Unfolding} +\end{quote} + +To do that all negations of the goal are unfolded even inner ones +(this is the default), use: + +\begin{quote} +{\tt Set Intuition Negation Unfolding} +\end{quote} + +To avoid that inner occurrence of {\tt iff} which do not need to be +unfolded are unfolded (this is the default), use: + +% 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} + +The tactic \texttt{firstorder} is an {\it experimental} extension of +\texttt{tauto} to +first-order reasoning, written by Pierre Corbineau. +It is not restricted to usual logical connectives but +instead may reason about any first-order class inductive definition. + +The default tactic used by \texttt{firstorder} when no rule applies is {\tt + auto with *}, it can be reset locally or globally using the {\nobreak + {\tt Set Firstorder Solver {\tac}}} \optindex{Firstorder Solver} +vernacular command and printed using {\nobreak {\tt Print Firstorder + Solver}}. + +\begin{Variants} + \item {\tt firstorder {\tac}} + \tacindex{firstorder {\tac}} + + Tries to solve the goal with {\tac} when no logical rule may apply. + + \item {\tt firstorder using {\qualid}$_1$ , \dots\ , {\qualid}$_n$ } + \tacindex{firstorder using} + + Adds lemmas {\qualid}$_1$ \dots\ {\qualid}$_n$ to the proof-search + environment. If {\qualid}$_i$ refers to an inductive type, it is + the collection of its constructors which are added to the + proof-search environment. + + \item {\tt firstorder with \ident$_1$ \dots\ \ident$_n$ } + \tacindex{firstorder with} + + Adds lemmas from {\tt auto} hint bases \ident$_1$ \dots\ \ident$_n$ + to the proof-search environment. + +\item \texttt{firstorder {\tac} using {\qualid}$_1$ , \dots\ , {\qualid}$_n$ with \ident$_1$ \dots\ \ident$_n$} + + This combines the effects of the different variants of \texttt{firstorder}. + +\end{Variants} + +Proof-search is bounded by a depth parameter which can be set by typing the +{\nobreak \tt Set Firstorder Depth $n$} \optindex{Firstorder Depth} +vernacular command. + + +\subsection{\tt congruence} +\tacindex{congruence} +\label{congruence} + +The tactic {\tt congruence}, by Pierre Corbineau, implements the standard Nelson and Oppen +congruence closure algorithm, which is a decision procedure for ground +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. Alternatively, congruence tries to prove that a 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 members 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. +Variables a b:A. +Variable f:A->A. +Variable g:A->A->A. +\end{coq_eval} + +\begin{coq_example} +Theorem T: + a=(f a) -> (g b (f a))=(f (f a)) -> (g a b)=(f (g b a)) -> (g a b)=a. +intros. +congruence. +\end{coq_example} + +\begin{coq_eval} +Reset Initial. +Variable A:Set. +Variables a c d:A. +Variable f:A->A*A. +\end{coq_eval} + +\begin{coq_example} +Theorem inj : f = pair a -> Some (f c) = Some (f d) -> c=d. +intros. +congruence. +\end{coq_example} + +\begin{Variants} + \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. + +\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 could not be built in {\Coq} + because of dependently-typed functions. + + \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 above. +\end{ErrMsgs} + +\noindent {\bf Remark: } {\tt congruence} can be made to print debug +information by setting the following option: + +\begin{quote} +\optindex{Congruence Verbose} +{\tt Set Congruence Verbose} +\end{quote} + +\section{Checking properties of terms} + +Each of the following tactics acts as the identity if the check succeeds, and results in an error otherwise. + +\subsection{\tt constr\_eq \term$_1$ \term$_2$} +\tacindex{constr\_eq} +\label{constreq} + +This tactic checks whether its arguments are equal modulo alpha conversion and casts. + +\ErrMsg \errindex{Not equal} + +\subsection{\tt unify \term$_1$ \term$_2$} +\tacindex{unify} +\label{unify} + +This tactic checks whether its arguments are unifiable, potentially +instantiating existential variables. + +\ErrMsg \errindex{Not unifiable} + +\begin{Variants} +\item {\tt unify \term$_1$ \term$_2$ with \ident} + + Unification takes the transparency information defined in the + hint database {\tt \ident} into account (see Section~\ref{HintTransparency}). +\end{Variants} + +\subsection{\tt is\_evar \term} +\tacindex{is\_evar} +\label{isevar} + +This tactic checks whether its argument is a current existential +variable. Existential variables are uninstantiated variables generated +by {\tt eapply} (see Section~\ref{apply}) and some other tactics. + +\ErrMsg \errindex{Not an evar} + +\subsection{\tt has\_evar \term} +\tacindex{has\_evar} +\label{hasevar} + +This tactic checks whether its argument has an existential variable as +a subterm. Unlike {\tt context} patterns combined with {\tt is\_evar}, +this tactic scans all subterms, including those under binders. + +\ErrMsg \errindex{No evars} + +\subsection{\tt is\_var \term} +\tacindex{is\_var} +\label{isvar} + +This tactic checks whether its argument is a variable or hypothesis in the +current goal context or in the opened sections. + +\ErrMsg \errindex{Not a variable or hypothesis} + +\section{Equality} + +\subsection{\tt f\_equal} +\label{f-equal} +\tacindex{f\_equal} + +This tactic applies to a goal of the form $f\ a_1\ \ldots\ a_n = f'\ +a'_1\ \ldots\ a'_n$. Using {\tt f\_equal} on such a goal leads to +subgoals $f=f'$ and $a_1=a'_1$ and so on up to $a_n=a'_n$. Amongst +these subgoals, the simple ones (e.g. provable by +reflexivity or congruence) are automatically solved by {\tt f\_equal}. + +\subsection{\tt reflexivity} +\label{reflexivity} +\tacindex{reflexivity} + +This tactic applies to a goal that has the form {\tt t=u}. It checks +that {\tt t} and {\tt u} are convertible and then solves the goal. +It is equivalent to {\tt apply refl\_equal}. + +\begin{ErrMsgs} +\item \errindex{The conclusion is not a substitutive equation} +\item \errindex{Unable to unify \dots\ with \dots} +\end{ErrMsgs} + +\subsection{\tt symmetry} +\tacindex{symmetry} + +This tactic applies to a goal that has the form {\tt t=u} and changes it +into {\tt u=t}. + +\begin{Variants} +\item {\tt symmetry in \ident} \tacindex{symmetry in} + +If the statement of the hypothesis {\ident} has the form {\tt t=u}, +the tactic changes it to {\tt u=t}. +\end{Variants} + +\subsection{\tt transitivity \term} +\tacindex{transitivity} + +This tactic applies to a goal that has the form {\tt t=u} +and transforms it into the two subgoals +{\tt t={\term}} and {\tt {\term}=u}. + +\section{Equality and inductive sets} + +We describe in this section some special purpose tactics dealing with +equality and inductive sets or types. These tactics use the equality +{\tt eq:forall (A:Type), A->A->Prop}, simply written with the +infix symbol {\tt =}. + +\subsection{\tt decide equality} +\label{decideequality} +\tacindex{decide equality} + +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. +It solves goals of the form {\tt \{$x$=$y$\}+\{\verb|~|$x$=$y$\}} as well. + +\subsection{\tt compare \term$_1$ \term$_2$} +\tacindex{compare} + +This tactic compares two given objects \term$_1$ and \term$_2$ +of an inductive datatype. If $G$ is the current goal, it leaves the sub-goals +\term$_1${\tt =}\term$_2$ {\tt ->} $G$ and \verb|~|\term$_1${\tt =}\term$_2$ +{\tt ->} $G$. The type +of \term$_1$ and \term$_2$ must satisfy the same restrictions as in the tactic +\texttt{decide equality}. + +\subsection{\tt simplify\_eq \term} +\tacindex{simplify\_eq} +\tacindex{esimplify\_eq} +\label{simplify-eq} + +Let {\term} be the proof of a statement of conclusion {\tt + {\term$_1$}={\term$_2$}}. If {\term$_1$} and +{\term$_2$} are structurally different (in the sense described for the +tactic {\tt discriminate}), then the tactic {\tt simplify\_eq} behaves as {\tt + discriminate {\term}}, otherwise it behaves as {\tt injection + {\term}}. + +\Rem If some quantified hypothesis of the goal is named {\ident}, then +{\tt simplify\_eq {\ident}} first introduces the hypothesis in the local +context using \texttt{intros until \ident}. + +\begin{Variants} +\item \texttt{simplify\_eq} \num + + This does the same thing as \texttt{intros until \num} then +\texttt{simplify\_eq \ident} where {\ident} is the identifier for the last +introduced hypothesis. + +\item \texttt{simplify\_eq} \term{} {\tt with} {\bindinglist} + + This does the same as \texttt{simplify\_eq {\term}} but using + the given bindings to instantiate parameters or hypotheses of {\term}. + +\item \texttt{esimplify\_eq} \num\\ + \texttt{esimplify\_eq} \term{} \zeroone{{\tt with} {\bindinglist}} + + This works the same as {\tt simplify\_eq} but if the type of {\term}, + or the type of the hypothesis referred to by {\num}, has uninstantiated + parameters, these parameters are left as existential variables. + +\item{\tt simplify\_eq} + +If the current goal has form $t_1\verb=<>=t_2$, it behaves as +\texttt{intro {\ident}; simplify\_eq {\ident}}. +\end{Variants} + +\subsection{\tt dependent rewrite -> \ident} +\tacindex{dependent rewrite ->} +\label{dependent-rewrite} + +This tactic applies to any goal. If \ident\ has type +\verb+(existT B a b)=(existT B a' b')+ +in the local context (i.e. each term of the +equality has a sigma type $\{ a:A~ \&~(B~a)\}$) this tactic rewrites +\verb+a+ into \verb+a'+ and \verb+b+ into \verb+b'+ in the current +goal. This tactic works even if $B$ is also a sigma type. This kind +of equalities between dependent pairs may be derived by the injection +and inversion tactics. + +\begin{Variants} +\item{\tt dependent rewrite <- {\ident}} +\tacindex{dependent rewrite <-} + +Analogous to {\tt dependent rewrite ->} but uses the equality from +right to left. +\end{Variants} + +\section{Inversion +\label{inversion}} + +\subsection{\tt functional inversion \ident} +\tacindex{functional inversion} +\label{sec:functional-inversion} + +\texttt{functional inversion} is a tactic +that 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} (see Section~\ref{Function}). +Note that this tactic is only available after a {\tt Require Import FunInd}. + +\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} + + If 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 + choosing which {\qualid} is inverted. +\end{Variants} + + + +\subsection{\tt quote \ident} +\tacindex{quote} +\index{2-level approach} + +This kind of inversion has nothing to do with the tactic +\texttt{inversion} above. This tactic does \texttt{change (\ident\ + t)}, where \texttt{t} is a term built in order to ensure the +convertibility. In other words, it does inversion of the function +\ident. This function must be a fixpoint on a simple recursive +datatype: see~\ref{quote-examples} for the full details. + +\begin{ErrMsgs} +\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$ ]} + + 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} + +% En attente d'un moyen de valoriser les fichiers de demos +% \SeeAlso file \texttt{theories/DEMOS/DemoQuote.v} in the distribution + +\section{Classical tactics} +\label{ClassicalTactics} + +In order to ease the proving process, when the {\tt Classical} module is loaded. A few more tactics are available. Make sure to load the module using the \texttt{Require Import} command. + +\subsection{{\tt classical\_left} and \tt classical\_right} +\tacindex{classical\_left} +\tacindex{classical\_right} + +The tactics \texttt{classical\_left} and \texttt{classical\_right} are the analog of the \texttt{left} and \texttt{right} but using classical logic. They can only be used for disjunctions. +Use \texttt{classical\_left} to prove the left part of the disjunction with the assumption that the negation of right part holds. +Use \texttt{classical\_right} to prove the right part of the disjunction with the assumption that the negation of left part holds. + +\section{Automatizing +\label{Automatizing}} + +% EXISTE ENCORE ? +% +% \subsection{\tt Prolog [ \term$_1$ \dots\ \term$_n$ ] \num} +% \tacindex{Prolog}\label{Prolog} +% This tactic, implemented by Chet Murthy, is based upon the concept of +% existential variables of Gilles Dowek, stating that resolution is a +% kind of unification. It tries to solve the current goal using the {\tt +% Assumption} tactic, the {\tt intro} tactic, and applying hypotheses +% of the local context and terms of the given list {\tt [ \term$_1$ +% \dots\ \term$_n$\ ]}. It is more powerful than {\tt auto} since it +% may apply to any theorem, even those of the form {\tt (x:A)(P x) -> Q} +% where {\tt x} does not appear free in {\tt Q}. The maximal search +% depth is {\tt \num}. + +% \begin{ErrMsgs} +% \item \errindex{Prolog failed}\\ +% The Prolog tactic was not able to prove the subgoal. +% \end{ErrMsgs} + + +%% \subsection{{\tt jp} {\em (Jprover)} +%% \tacindex{jp} +%% \label{jprover}} + +%% The tactic \texttt{jp}, due to Huang Guan-Shieng, is an experimental +%% port of the {\em Jprover}\cite{SLKN01} semi-decision procedure for +%% first-order intuitionistic logic implemented in {\em +%% NuPRL}\cite{Kre02}. + +%% The tactic \texttt{jp}, due to Huang Guan-Shieng, is an {\it +%% experimental} port of the {\em Jprover}\cite{SLKN01} semi-decision +%% procedure for first-order intuitionistic logic implemented in {\em +%% NuPRL}\cite{Kre02}. + +%% Search may optionally be bounded by a multiplicity parameter +%% indicating how many (at most) copies of a formula may be used in +%% the proof process, its absence may lead to non-termination of the tactic. + +%% %\begin{coq_eval} +%% %Variable S:Set. +%% %Variables P Q:S->Prop. +%% %Variable f:S->S. +%% %\end{coq_eval} + +%% %\begin{coq_example*} +%% %Lemma example: (exists x |P x\/Q x)->(exists x |P x)\/(exists x |Q x). +%% %jp. +%% %Qed. + +%% %Lemma example2: (forall x ,P x->P (f x))->forall x,P x->P (f(f x)). +%% %jp. +%% %Qed. +%% %\end{coq_example*} + +%% \begin{Variants} +%% \item {\tt jp $n$}\\ +%% \tacindex{jp $n$} +%% Tries the {\em Jprover} procedure with multiplicities up to $n$, +%% starting from 1. +%% \item {\tt jp}\\ +%% Tries the {\em Jprover} procedure without multiplicity bound, +%% possibly running forever. +%% \end{Variants} + +%% \begin{ErrMsgs} +%% \item \errindex{multiplicity limit reached}\\ +%% The procedure tried all multiplicities below the limit and +%% failed. Goal might be solved by increasing the multiplicity limit. +%% \item \errindex{formula is not provable}\\ +%% The procedure determined that goal was not provable in +%% intuitionistic first-order logic, no matter how big the +%% multiplicity is. +%% \end{ErrMsgs} + + +% \subsection[\tt Linear]{\tt Linear\tacindex{Linear}\label{Linear}} +% The tactic \texttt{Linear}, due to Jean-Christophe Filli{\^a}atre +% \cite{Fil94}, implements a decision procedure for {\em Direct +% Predicate Calculus}, that is first-order Gentzen's Sequent Calculus +% without contraction rules \cite{KeWe84,BeKe92}. Intuitively, a +% first-order goal is provable in Direct Predicate Calculus if it can be +% proved using each hypothesis at most once. + +% Unlike the previous tactics, the \texttt{Linear} tactic does not belong +% to the initial state of the system, and it must be loaded explicitly +% with the command + +% \begin{coq_example*} +% Require Linear. +% \end{coq_example*} + +% For instance, assuming that \texttt{even} and \texttt{odd} are two +% predicates on natural numbers, and \texttt{a} of type \texttt{nat}, the +% tactic \texttt{Linear} solves the following goal + +% \begin{coq_eval} +% Variables even,odd : nat -> Prop. +% Variable a:nat. +% \end{coq_eval} + +% \begin{coq_example*} +% Lemma example : (even a) +% -> ((x:nat)((even x)->(odd (S x)))) +% -> (EX y | (odd y)). +% \end{coq_example*} + +% You can find examples of the use of \texttt{Linear} in +% \texttt{theories/DEMOS/DemoLinear.v}. +% \begin{coq_eval} +% Abort. +% \end{coq_eval} + +% \begin{Variants} +% \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} +% tactic. So one can use axioms, lemmas or hypotheses of the local +% context with \texttt{Linear} in this way. +% \end{Variants} + +% \begin{ErrMsgs} +% \item \errindex{Not provable in Direct Predicate Calculus} +% \item \errindex{Found $n$ classical proof(s) but no intuitionistic one}\\ +% The decision procedure looks actually for classical proofs of the +% goals, and then checks that they are intuitionistic. In that case, +% classical proofs have been found, which do not correspond to +% intuitionistic ones. +% \end{ErrMsgs} + + +\subsection{\tt btauto} +\tacindex{btauto} +\label{btauto} + +The tactic \texttt{btauto} implements a reflexive solver for boolean tautologies. It +solves goals of the form {\tt t = u} where {\tt t} and {\tt u} are constructed +over the following grammar: + +$$\mathtt{t} ::= x \mid \mathtt{true} \mid \mathtt{false}\mid \mathtt{orb\ t_1\ t_2} +\mid \mathtt{andb\ t_1\ t_2} \mid\mathtt{xorb\ t_1\ t_2} \mid\mathtt{negb\ t} +\mid\mathtt{if\ t_1\ then\ t_2\ else\ t_3} +$$ + +Whenever the formula supplied is not a tautology, it also provides a counter-example. + +Internally, it uses a system very similar to the one of the {\tt ring} tactic. + +\subsection{\tt omega} +\tacindex{omega} +\label{omega} + +The tactic \texttt{omega}, due to Pierre Cr{\'e}gut, +is an automatic decision procedure for Presburger +arithmetic. It solves quantifier-free +formulas built with \verb|~|, \verb|\/|, \verb|/\|, +\verb|->| on top of equalities, inequalities and disequalities on +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} +(see Chapter~\ref{OmegaChapter}). + +\subsection{{\tt ring} and \tt ring\_simplify \term$_1$ \mbox{\dots} \term$_n$} +\tacindex{ring} +\tacindex{ring\_simplify} +\comindex{Add Ring} +\comindex{Print Rings} + +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. + +{\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. + +See Chapter~\ref{ring} for more information on the tactic and how to +declare new ring structures. All declared field structures can be +printed with the {\tt Print Rings} command. + +\subsection{{\tt field}, {\tt field\_simplify \term$_1$ \mbox{\dots} + \term$_n$}, and \tt field\_simplify\_eq} +\tacindex{field} +\tacindex{field\_simplify} +\tacindex{field\_simplify\_eq} +\comindex{Add Field} +\comindex{Print Fields} + +The {\tt field} tactic is built on the same ideas as {\tt ring}: this +is a reflexive tactic that solves or simplifies equations in a field +structure. The main idea is to reduce a field expression (which is an +extension of ring expressions with the inverse and division +operations) to a fraction made of two polynomial expressions. + +Tactic {\tt field} is used to solve subgoals, whereas {\tt + field\_simplify \term$_1$\dots\term$_n$} replaces the provided terms +by their reduced fraction. {\tt field\_simplify\_eq} applies when the +conclusion is an equation: it simplifies both hand sides and multiplies +so as to cancel denominators. So it produces an equation without +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 +declare new field structures. All declared field structures can be +printed with the {\tt Print Fields} command. + +\Example +\begin{coq_example*} +Require Import Reals. +Goal forall x y:R, + (x * y > 0)%R -> + (x * (1 / x + x / (x + y)))%R = + ((- 1 / y) * y * (- x * (x / (x + y)) - 1))%R. +\end{coq_example*} + +\begin{coq_example} +intros; field. +\end{coq_example} + +\begin{coq_eval} +Reset Initial. +\end{coq_eval} + +\SeeAlso file {\tt plugins/setoid\_ring/RealField.v} for an example of instantiation,\\ +\phantom{\SeeAlso}theory {\tt theories/Reals} for many examples of use of {\tt +field}. + +\subsection{\tt fourier} +\tacindex{fourier} + +This tactic written by Lo{\"\i}c Pottier solves linear inequalities on +real numbers using Fourier's method~\cite{Fourier}. This tactic must +be loaded by {\tt Require Import Fourier}. + +\Example +\begin{coq_example*} +Require Import Reals. +Require Import Fourier. +Goal forall x y:R, (x < y)%R -> (y + 1 >= x - 1)%R. +\end{coq_example*} + +\begin{coq_example} +intros; fourier. +\end{coq_example} + +\begin{coq_eval} +Reset Initial. +\end{coq_eval} + +\section{Non-logical tactics} + +\subsection[\tt cycle \num]{\tt cycle \num\tacindex{cycle}} + +This tactic puts the {\num} first goals at the end of the list of +goals. If {\num} is negative, it will put the last $\left|\num\right|$ goals at +the beginning of the list. + +\Example +\begin{coq_example*} +Parameter P : nat -> Prop. +Goal P 1 /\ P 2 /\ P 3 /\ P 4 /\ P 5. +\end{coq_example*} +\begin{coq_example} +repeat split. +all: cycle 2. +all: cycle -3. +\end{coq_example} + +\begin{coq_eval} +Reset Initial. +\end{coq_eval} + +\subsection[\tt swap \num$_1$ \num$_2$]{\tt swap \num$_1$ \num$_2$\tacindex{swap}} + +This tactic switches the position of the goals of indices $\num_1$ and $\num_2$. If either $\num_1$ or $\num_2$ is negative then goals are counted from the end of the focused goal list. Goals are indexed from $1$, there is no goal with position $0$. + +\Example +\begin{coq_example*} +Parameter P : nat -> Prop. +Goal P 1 /\ P 2 /\ P 3 /\ P 4 /\ P 5. +\end{coq_example*} +\begin{coq_example} +repeat split. +all: swap 1 3. +all: swap 1 -1. +\end{coq_example} + +\begin{coq_eval} +Reset Initial. +\end{coq_eval} + +\subsection[\tt revgoals]{\tt revgoals\tacindex{revgoals}} + +This tactics reverses the list of the focused goals. + +\Example +\begin{coq_example*} +Parameter P : nat -> Prop. +Goal P 1 /\ P 2 /\ P 3 /\ P 4 /\ P 5. +\end{coq_example*} +\begin{coq_example} +repeat split. +all: revgoals. +\end{coq_example} + +\begin{coq_eval} +Reset Initial. +\end{coq_eval} + + + +\subsection[\tt shelve]{\tt shelve\tacindex{shelve}\label{shelve}} + +This tactic moves all goals under focus to a shelf. While on the shelf, goals +will not be focused on. They can be solved by unification, or they can be called +back into focus with the command {\tt Unshelve} (Section~\ref{unshelve}). + +\begin{Variants} + \item \texttt{shelve\_unifiable}\tacindex{shelve\_unifiable} + + Shelves only the goals under focus that are mentioned in other goals. + Goals that appear in the type of other goals can be solved by unification. + +\Example +\begin{coq_example} +Goal exists n, n=0. +refine (ex_intro _ _ _). +all:shelve_unifiable. +reflexivity. +\end{coq_example} + +\begin{coq_eval} +Reset Initial. +\end{coq_eval} + +\end{Variants} + +\subsection[\tt Unshelve]{\tt Unshelve\comindex{Unshelve}\label{unshelve}} + +This command moves all the goals on the shelf (see Section~\ref{shelve}) from the +shelf into focus, by appending them to the end of the current list of focused goals. + +\subsection[\tt give\_up]{\tt give\_up\tacindex{give\_up}} + +This tactic removes the focused goals from the proof. They are not solved, and cannot +be solved later in the proof. As the goals are not solved, the proof cannot be closed. + +The {\tt give\_up} tactic can be used while editing a proof, to choose to write the +proof script in a non-sequential order. + +\section{Simple tactic macros} +\index{Tactic macros} +\label{TacticDefinition} + +A simple example has more value than a long explanation: + +\begin{coq_example} +Ltac Solve := simpl; intros; auto. +Ltac ElimBoolRewrite b H1 H2 := + elim b; [ intros; rewrite H1; eauto | intros; rewrite H2; eauto ]. +\end{coq_example} + +The tactics macros are synchronous with the \Coq\ section mechanism: +a tactic definition is deleted from the current environment +when you close the section (see also \ref{Section}) +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. + +Chapter~\ref{TacticLanguage} gives examples of more complex +user-defined tactics. + + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "Reference-Manual" +%%% TeX-master: "Reference-Manual" +%%% End: |