diff options
Diffstat (limited to 'doc/refman/RefMan-tac.tex')
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 3096 |
1 files changed, 3096 insertions, 0 deletions
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex new file mode 100644 index 00000000..72df6005 --- /dev/null +++ b/doc/refman/RefMan-tac.tex @@ -0,0 +1,3096 @@ +\chapter{Tactics +\index{Tactics} +\label{Tactics}} + +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}. Indeed, a deduction rule can be read in two ways. The first +one has the shape: {\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 +which proceeds from conclusion to premises. We say that the conclusion +is {\em the goal}\index{goal} to prove and premises are {\em the +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 build 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}. + +There are, at least, three levels of atomic tactics. The simplest one +implements basic rules of the logical framework. The second level is +the one of {\em derived rules} which are built by combination of other +tactics. The third one implements heuristics or decision procedures to +build a complete proof of a goal. + +\section{Invocation of tactics +\label{tactic-syntax} +\index{tactic@{\tac}}} + +A tactic is applied as an ordinary command. If the tactic does not +address the first subgoal, the command may be preceded by the wished +subgoal number as shown below: + +\begin{tabular}{lcl} +{\commandtac} & ::= & {\num} {\tt :} {\tac} {\tt .}\\ + & $|$ & {\tac} {\tt .} +\end{tabular} + +\section{Explicit proof as a term} + +\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} + + +\subsection{\tt refine \term +\tacindex{refine} +\label{refine} +\index{?@{\texttt{?}}}} + +This tactic allows to give an exact proof but still with some +holes. The holes are noted ``\texttt{\_}''. + +\begin{ErrMsgs} +\item \errindex{invalid argument}: + the tactic \texttt{refine} doesn't 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, which 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} + +An example of use is given in section~\ref{refine-example}. + +\section{Basics +\index{Typing rules}} + +Tactics presented in this section implement the basic typing rules of +{\sc Cic} given in Chapter~\ref{Cic}. + +\subsection{{\tt assumption} +\tacindex{assumption}} + +This tactic applies to any goal. It implements the +``Var''\index{Typing rules!Var} rule given in +Section~\ref{Typed-terms}. It 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} + +\subsection{\tt clear {\ident} +\tacindex{clear} +\label{clear}} + +This tactic erases the hypothesis named {\ident} in the local context +of the current goal. Then {\ident} is no more displayed and no more +usable in the proof development. + +\begin{Variants} + +\item {\tt clear {\ident$_1$} {\ldots} {\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. + +\end{Variants} + +\begin{ErrMsgs} +\item \errindex{{\ident} not found} +\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} + +\subsection{\tt move {\ident$_1$} after {\ident$_2$} +\tacindex{move}} + +This moves the hypothesis named {\ident$_1$} in the local context +after the hypothesis named {\ident$_2$}. + +If {\ident$_1$} comes before {\ident$_2$} in the order of dependences, +then all hypotheses between {\ident$_1$} and {\ident$_2$} which +(possibly indirectly) depend on {\ident$_1$} are moved also. + +If {\ident$_1$} comes after {\ident$_2$} in the order of dependences, +then all hypotheses between {\ident$_1$} and {\ident$_2$} which +(possibly indirectly) occur in {\ident$_1$} are moved also. + +\begin{ErrMsgs} + +\item \errindex{{\ident$_i$} not found} + +\item \errindex{Cannot move {\ident$_1$} after {\ident$_2$}: + it occurs in {\ident$_2$}} + +\item \errindex{Cannot move {\ident$_1$} after {\ident$_2$}: + it depends on {\ident$_2$}} + +\end{ErrMsgs} + +\subsection{\tt rename {\ident$_1$} into {\ident$_2$} +\tacindex{rename}} + +This renames hypothesis {\ident$_1$} into {\ident$_2$} in the current +context\footnote{but it does not rename the hypothesis in the + proof-term...} + +\begin{ErrMsgs} + +\item \errindex{{\ident$_2$} not found} + +\item \errindexbis{{\ident$_2$} is already used}{is already used} + +\end{ErrMsgs} + +\subsection{\tt intro +\tacindex{intro} +\label{intro}} + +This tactic applies to a goal which 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 {\tt 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 {\tt $T$ -> $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 red} until the tactic +{\tt intro} can be applied or the goal is not 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} + + Repeats {\tt intro} until it meets the head-constant. It never reduces + head-constants and it never fails. + +\item {\tt intro {\ident}} + + 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$} + + 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} + + 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} + + Repeats {\tt intro} until the {\num}-th non-dependent premise. For + instance, on the subgoal % + \verb+forall x y:nat, x=y -> forall z:nat,z=x->z=y+ the + tactic \texttt{intros until 2} is equivalent to \texttt{intros x y H + z H0} (assuming \texttt{x, y, H, z} and \texttt{H0} do not already + occur in context). + + \ErrMsg \errindex{No such hypothesis in current goal} + + 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} + + Applies {\tt intro} but puts the introduced + hypothesis after the hypothesis \ident{} in the hypotheses. + +\begin{ErrMsgs} +\item \errindex{No product even after head-reduction} +\item \errindex{No such hypothesis} : {\ident} +\end{ErrMsgs} + +\item {\tt intro \ident$_1$ after \ident$_2$} + \tacindex{intro ... after} + + Behaves as previously but \ident$_1$ is the name of the introduced + hypothesis. It is equivalent to {\tt intro \ident$_1$; move + \ident$_1$ after \ident$_2$}. + +\begin{ErrMsgs} +\item \errindex{No product even after head-reduction} +\item \errindex{No such hypothesis} : {\ident} +\end{ErrMsgs} + +\end{Variants} + +\subsection{\tt apply \term +\tacindex{apply} +\label{apply}} + +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}. The tactic {\tt +apply} relies on first-order pattern-matching with dependent +types. See {\tt pattern} in section \ref{pattern} to transform a +second-order pattern-matching problem into a first-order one. + +\begin{ErrMsgs} +\item \errindex{Impossible 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{generated subgoal {\term'} has metavariables in it} + + This occurs when some instantiations of 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} which do not occur in the conclusion + and consequently cannot be found by unification. Notice that + {\term$_1$} \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. But variables are referred by names and non dependent + products by order (see syntax in Section~\ref{Binding-list}). + +\item {\tt eapply \term}\tacindex{eapply}\label{eapply} + + The tactic {\tt eapply} behaves as {\tt apply} but does not fail + when no instantiation are deducible for some variables in the + premises. Rather, it turns these variables into so-called + existential variables which are variables still to instantiate. An + existential variable is identified by a name of the form {\tt ?$n$} + where $n$ is a number. The instantiation is intended to be found + later in the proof. + + An example of use of {\tt eapply} is given in + Section~\ref{eapply-example}. + +\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} + +\subsection{{\tt set ( {\ident} {\tt :=} {\term} \tt )} +\label{tactic:set} +\tacindex{set} +\tacindex{pose}} + +This replaces {\term} by {\ident} in the conclusion or in the +hypotheses of the current goal and adds the new definition {\ident +{\tt :=} \term} to the local context. The default is to make this +replacement only in the conclusion. + +\begin{Variants} + +\item {\tt set ( } {\ident} {\tt :=} {\term} {\tt ) in *}\\ + {\tt set ( } {\ident} {\tt :=} {\term} {\tt ) in * |- *}\\ + + This behaves as above but substitutes {\term} + everywhere in the goal (both in conclusion and hypotheses). + +\item {\tt set ( } {\ident} {\tt :=} {\term} {\tt ) in * |-} + + This behaves the same but substitutes {\term} in + the hypotheses only (not in the conclusion). + +\item {\tt set ( } {\ident} {\tt :=} {\term} {\tt ) in |- *} + + This is equivalent to {\tt set ( } {\ident} {\tt :=} {\term} {\tt + )}, i.e. it substitutes {\term} in the conclusion only. + +\item {\tt set ( {\ident$_0$} {\tt :=} {\term} {\tt ) in} {\ident$_1$}} + + This behaves the same but substitutes {\term} only in + the hypothesis named {\ident$_1$}. + +\item {\tt set (} {\ident$_0$} {\tt :=} {\term} {\tt ) in} + {\ident$_1$} {\tt at} {\num$_1$} \dots\ {\num$_n$} + +This notation allows to specify which occurrences of {\term} have to +be substituted in the hypothesis named {\ident$_1$}. The occurrences +are numbered from left to right and are meaningful on a pure +expression using no implicit argument, notation or coercion. A +negative occurrence number means an occurrence which should not be +substituted. As an exception of 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. + +For expressions using notations, or hiding implicit arguments or +coercions, it is recommended to make explicit all occurrences in +order by using {\tt Set Printing All} (see +section~\ref{SetPrintingAll}). + +\item {\tt set ( } {\ident} {\tt :=} {\term} {\tt ) in |- * at} + {\num$_1$} \dots\ {\num$_n$} + +This allows to specify which occurrences of the conclusion are concerned. + +\item {\tt set (} {\ident$_0$} {\tt :=} {\term} {\tt ) in} + {\ident$_1$} {\tt at} {\num$_1^1$} \dots\ {\num$_{n_1}^1$}, \dots + {\ident$_m$} {\tt at} {\num$_1^m$} \dots {\num$_{n_m}^m$} + + It substitutes {\term} at occurrences {\num$_1^i$} \dots\ + {\num$_{n_i}^i$} of hypothesis {\ident$_i$}. Each {\tt at} part is + optional. + +\item {\tt set (} {\ident$_0$} {\tt :=} {\term} {\tt ) in} + {\ident$_1$} {\tt at} {\num$_1^1$} \dots\ {\num$_{n_1}^1$}, \dots + {\ident$_m$} {\tt at} {\num$_1^m$} \dots {\num$_{n_m}^m$} + {\tt |- *} {\tt at} {\num$'_1$} \dots\ {\num$'_n$} + + This is the more general form which combines all the previous + possibilities. + +\item {\tt set } {\term} + + This behaves as {\tt set (} {\ident} := {\term} {\tt )} but {\ident} + is generated by {\Coq}. This variant is available for the + forms with {\tt in} too. + +\item {\tt pose ( {\ident} {\tt :=} {\term} {\tt )}} + + This adds the local definition {\ident} := {\term} to the current + context without performing any replacement in the goal or in the + hypotheses. + +\item{\tt pose {\term}} + + This behaves as {\tt pose (} {\ident} := {\term} {\tt )} but + {\ident} is generated by {\Coq}. + +\end{Variants} + +\subsection{{\tt assert ( {\ident} : {\form} \tt )} +\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} {\tt )} but + {\ident} is generated by {\Coq}. + +\item{\tt assert (} {\ident} := {\term} {\tt )} + + This behaves as {\tt assert ({\ident} : {\type});[exact + {\term}|idtac]} where {\type} is the type of {\term}. + +\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. + +\end{Variants} + +% PAS CLAIR; +% DEVRAIT AU MOINS FAIRE UN INTRO; +% DEVRAIT ETRE REMPLACE PAR UN LET; +% MESSAGE D'ERREUR STUPIDE +% POURQUOI Specialize trans_equal ECHOUE ? +%\begin{Variants} +%\item {\tt Specialize \term} +% \tacindex{Specialize} \\ +% The argument {\tt t} should be a well-typed +% term of type {\tt T}. This tactics is to make a cut of a +% proposition when you have already the proof of this proposition +% (for example it is a theorem applied to variables of local +% context). It is equivalent to {\tt Assert T. exact t}. +% +%\item {\tt Specialize {\term} with \vref$_1$ := {\term$_1$} \dots +% \vref$_n$ := \term$_n$} +% \tacindex{Specialize \dots\ with} \\ +% It is to provide the tactic with some explicit values to instantiate +% premises of {\term} (see section \ref{Binding-list}). +% Some other premises are inferred using type information and +% unification. The resulting well-formed +% term being {\tt (\term~\term'$_1$\dots\term'$_k$)} +% this tactic behaves as is used as +% {\tt Specialize (\term~\term'$_1$\dots\term'$_k$)} \\ +% +% \ErrMsg {\tt Metavariable wasn't in the metamap} \\ +% Arises when the information provided in the bindings list is not +% sufficient. +%\item {\tt Specialize {\num} {\term} with \vref$_1$ := {\term$_1$} \dots\ +% \vref$_n$:= \term$_n$}\\ +% The behavior is the same as before but only \num\ premises of +% \term\ will be kept. +%\end{Variants} + +\subsection{\tt generalize \term +\tacindex{generalize} +\label{generalize}} + +This tactic applies to any goal. It generalizes the conclusion w.r.t. +one subterm of it. For 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 accordingly +to $T$. + +\begin{Variants} +\item {\tt generalize \term$_1$ \dots\ \term$_n$} + + 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 dependent \term} \tacindex{generalize dependent} + + This generalizes {\term} but also {\em all} hypotheses which depend + on {\term}. It clears the generalized hypotheses. + +\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} + +\subsection{Bindings list +\index{Binding list} +\label{Binding-list}} + +A bindings list is generally used after the keyword {\tt with} in +tactics. The general shape of a bindings list is {\tt (\vref$_1$ := + \term$_1$) \dots\ (\vref$_n$ := \term$_n$)} where {\vref} is either an +{\ident} or a {\num}. It is used to provide a tactic with a list of +values (\term$_1$, \dots, \term$_n$) that have to be substituted +respectively to \vref$_1$, \dots, \vref$_n$. For all $i \in [1\dots\ +n]$, if \vref$_i$ is \ident$_i$ then it references the dependent +product {\tt \ident$_i$:T} (for some type \T); if \vref$_i$ is +\num$_i$ then it references the \num$_i$-th non dependent premise. + +A bindings list can also be a simple list of terms {\tt \term$_1$ + \term$_2$ \dots\term$_n$}. In that case the references to which +these terms correspond are determined by the tactic. In case of {\tt + elim} (see section~\ref{elim}) the terms should correspond to +all the dependent products in the type of \term\ while in the case of +{\tt apply} only the dependent products which are not bound in +the conclusion of the type are given. + + +\section{Negation and contradiction} + +\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}) one +which is equivalent to {\tt False}. It permits to prune irrelevant +cases. This tactic is a macro for the tactics sequence {\tt intros; + elimtype False; assumption}. + +\begin{ErrMsgs} +\item \errindex{No such assumption} +\end{ErrMsgs} + + +\section{Conversion tactics +\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. The specification of such parts are called \emph{clauses}. It +can be either the conclusion, or an hypothesis. In the case of a +defined hypothesis it is possible to specify if the conversion should +occur on the type part, the body part or both (default). + +\index{Clauses} +Clauses are written after a conversion tactic (tactic +\texttt{set}~\ref{tactic:set} also uses clauses) and are introduced by +the keyword \texttt{in}. If no clause is provided, the default is to +perform the conversion only in the conclusion. + +The syntax and description of the various clauses follows: +\begin{description} +\item[\texttt{in H$_1$ $\ldots$ H$_n$ |- }] only in hypotheses $H_1 + $\ldots$ H_n$ +\item[\texttt{in H$_1$ $\ldots$ H$_n$ |- *}] in hypotheses $H_1 \ldots + H_n$ and in the conclusion +\item[\texttt{in * |-}] in every hypothesis +\item[\texttt{in *}] (equivalent to \texttt{in * |- *}) everywhere +\item[\texttt{in (type of H$_1$) (value of H$_2$) $\ldots$ |-}] in + type part of $H_1$, in the value part of $H_2$, etc. +\end{description} + +For backward compatibility, the notation \texttt{in}~$H_1\ldots H_n$ +performs the conversion in hypotheses $H_1\ldots H_n$. + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +%voir reduction__conv_x : histoires d'univers. +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +\subsection{{\tt cbv \flag$_1$ \dots\ \flag$_n$}, {\tt lazy \flag$_1$ +\dots\ \flag$_n$} and {\tt compute} +\tacindex{cbv} +\tacindex{lazy} +\tacindex{compute}} + +These parameterized reduction tactics apply to any goal and perform +the normalization of the goal according to the specified flags. Since +the reduction considered in \Coq\ include $\beta$ (reduction of +functional application), $\delta$ (unfolding of transparent constants, +see \ref{Transparent}), $\iota$ (reduction of {\tt Cases}, {\tt Fix} +and {\tt CoFix} expressions) and $\zeta$ (removal of local +definitions), every flag is one of {\tt beta}, {\tt delta}, {\tt + iota}, {\tt zeta}, {\tt [\qualid$_1$\ldots\qualid$_k$]} and {\tt + -[\qualid$_1$\ldots\qualid$_k$]}. The last two flags give the list +of constants to unfold, or the list of constants not to unfold. These +two flags can occur only after the {\tt delta} flag. +If alone (i.e. not +followed by {\tt [\qualid$_1$\ldots\qualid$_k$]} or {\tt + -[\qualid$_1$\ldots\qualid$_k$]}), the {\tt delta} flag means that all constants must be unfolded. +However, the {\tt delta} flag does not apply to variables bound by a +let-in construction whose unfolding is controlled by the {\tt + zeta} flag only. In addition, there is a flag {\tt Evar} to perform +instantiation of existential variables (``?'') when an instantiation +actually exists. + +The goal may be normalized with 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 partially evaluated only when necessary, but if an +argument is used several times, it is computed only once. This +reduction is efficient for reducing expressions with dead code. For +instance, the proofs of a proposition $\exists_T ~x. P(x)$ reduce to a +pair of a witness $t$, and a proof that $t$ verifies 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 evaluated first, using a weak +reduction (no reduction under the $\lambda$-abstractions). Despite the +lazy strategy always performs fewer reductions than the call-by-value +strategy, the latter should be preferred for evaluating purely +computational expressions (i.e. with few dead code). + +\begin{Variants} +\item {\tt compute} \tacindex{compute} + + This tactic is an alias for {\tt cbv beta delta evar iota zeta}. +\end{Variants} + +\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 which has the form {\tt + forall (x:T1)\dots(xk:Tk), c t1 \dots\ tn} where {\tt c} is 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. +{\tt hnf} does not produce a real head normal form but either a +product or an applicative term in head normal form or a variable. + +\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{\tt simpl +\tacindex{simpl}} + +This tactic applies to any goal. The tactic {\tt simpl} first applies +$\beta\iota$-reduction rule. Then it expands transparent constants +and tries to reduce {\tt T'} according, once more, to $\beta\iota$ +rules. But when the $\iota$ rule is not applicable then possible +$\delta$-reductions are not applied. For instance trying to use {\tt + simpl} on {\tt (plus n O)=n} does change nothing. + +\tacindex{simpl \dots\ in} +\begin{Variants} +\item {\tt simpl {\term}} + + This applies {\tt simpl} only to the occurrences of {\term} in the + current goal. + +\item {\tt simpl {\term} at \num$_1$ \dots\ \num$_i$} + + This applies {\tt simpl} only to the \num$_1$, \dots, \num$_i$ + occurrences of {\term} in the current goal. + + \ErrMsg {\tt Too few occurrences} + +\item {\tt simpl {\ident}} + + This applies {\tt simpl} only to the applicative subterms whose head + occurrence is {\ident}. + +\item {\tt simpl {\ident} at \num$_1$ \dots\ \num$_i$} + + This applies {\tt simpl} only to the \num$_1$, \dots, \num$_i$ +applicative subterms whose head occurrence is {\ident}. + +\end{Variants} + +\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{Simpl-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}$_1$, \dots, \qualid$_n$} + \tacindex{unfold \dots\ in} + + 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} + +\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 +substituted for \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 has $\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} will be + 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$. + +\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{Introductions} + +Introduction tactics address goals which are inductive constants. +They are used when one guesses that the goal can be obtained with one +of its constructors' type. + +\subsection{\tt constructor \num +\label{constructor} +\tacindex{constructor}} + +This tactic applies to a goal such that the head of its conclusion is +an inductive constant (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} if + the number of constructors of the head of the goal. + +\item {\tt constructor \num~with} {\bindinglist} + \tacindex{constructor \dots\ with} + + 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). + +\item {\tt split}\tacindex{split} + + Applies if {\tt I} has only one constructor, typically in the case + of conjunction $A\land B$. Then, it is equivalent to {\tt constructor 1}. + +\item {\tt exists {\bindinglist}}\tacindex{exists} + + Applies if {\tt I} has only one constructor, for instance in the + case of existential quantification $\exists x\cdot P(x)$. + Then, it is equivalent to {\tt intros; constructor 1 with \bindinglist}. + +\item {\tt left}\tacindex{left}, {\tt right}\tacindex{right} + + Apply if {\tt I} has two constructors, for instance in the case of + disjunction $A\lor B$. Then, they are respectively equivalent to {\tt + constructor 1} and {\tt constructor 2}. + +\item {\tt left \bindinglist}, {\tt right \bindinglist}, {\tt split + \bindinglist} + + As soon as the inductive type has the right number of constructors, + these expressions are equivalent to the corresponding {\tt + constructor $i$ with \bindinglist}. + +\end{Variants} + +\section{Eliminations (Induction and Case Analysis)} + +Elimination tactics are useful to prove statements by induction or +case analysis. Indeed, they make use of the elimination (or +induction) principles generated with inductive definitions (see +Section~\ref{Cic-inductive-definitions}). + +\subsection{\tt induction \term +\tacindex{induction}} + +This tactic applies to any goal. The type of the argument {\term} must +be an inductive constant. Then, the tactic {\tt induction} +generates subgoals, one for each possible form of {\term}, i.e. one +for each constructor of the inductive type. + +The tactic {\tt induction} automatically replaces every occurrences +of {\term} in the conclusion and the hypotheses of the goal. It +automatically adds induction hypotheses (using names of the form {\tt + IHn1}) to the local context. If some hypothesis must not be taken +into account in the induction hypothesis, then it needs to be removed +first (you can also use the tactics {\tt elim} or {\tt simple induction}, +see below). + +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}} + +\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. + +\Rem For simple induction on a numeral, use syntax {\tt induction +({\num})} (not very interesting anyway). + +\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{Cannot refine to conclusions with meta-variables} + + As {\tt induction} uses {\tt apply}, see Section~\ref{apply} and + the variant {\tt elim \dots\ with \dots} below. +\end{ErrMsgs} + +\begin{Variants} +\item{\tt induction {\term} as {\intropattern}} + + This behaves as {\tt induction {\term}} but uses the names in + {\intropattern} to names 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 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$'s can be any introduction patterns (see + Section~\ref{intros-pattern}). This provides a concise notation for + nested induction. + +\Rem for an inductive type with one constructor, the pattern notation +{\tt ($p_{1}$,\ldots,$p_{n}$)} can be used instead of +{\tt [} $p_{1}$ \ldots $p_{n}$ {\tt ]}. + +\item {\tt induction {\term} using {\qualid}} + + This behaves as {\tt induction {\term}} but using the induction +scheme of name {\qualid}. It does not expect that the type of +{\term} is inductive. + +\item {\tt induction {\term} using {\qualid} as {\intropattern}} + + This combines {\tt induction {\term} using {\qualid}} +and {\tt induction {\term} as {\intropattern}}. + +\item {\tt elim \term}\label{elim} + + This is a more basic induction tactic. Again, the type of the + argument {\term} must be an inductive constant. Then according to + the type of the goal, the tactic {\tt elim} chooses the right + destructor and applies it (as in the case of the {\tt apply} + tactic). For instance, assume that our proof context contains {\tt + n:nat}, assume that our 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 affect the hypotheses of + the goal, neither introduces the induction loading into the context + of hypotheses. + +\item {\tt elim \term} + + also works when the type of {\term} starts with products and the + head symbol is an inductive definition. In that case the tactic + tries both to find an object in the inductive definition and to use + this inductive definition for elimination. In case of non-dependent + products in the type, subgoals are generated corresponding to the + hypotheses. In the case of dependent products, the tactic will try + to find an instance for which the elimination lemma applies. + +\item {\tt elim {\term} with \term$_1$ \dots\ \term$_n$} + \tacindex{elim \dots\ with} \ + + Allows the user to give explicitly the values for dependent + premises of the elimination schema. All arguments must be given. + + \ErrMsg \errindex{Not the right number of dependent arguments} + +\item{\tt elim {\term} with {\vref$_1$} := {\term$_1$} \dots\ {\vref$_n$} + := {\term$_n$}} + + Provides also {\tt elim} with values for instantiating premises by + associating explicitly variables (or non dependent products) with + their intended instance. + +\item{\tt elim {\term$_1$} using {\term$_2$}} +\tacindex{elim \dots\ using} + +Allows the user to give explicitly an elimination predicate +{\term$_2$} which is not the standard one for the underlying inductive +type of {\term$_1$}. Each of the {\term$_1$} and {\term$_2$} is either +a simple term or a term with a bindings list (see \ref{Binding-list}). + +\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} and which does not occur + in the goal then {\tt elim t} is equivalent to {\tt elimtype I; 2: + exact t.} + + \ErrMsg \errindex{Impossible to unify \dots\ with \dots} + + Arises when {\form} needs to be applied to parameters. + +\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 destruct \term +\tacindex{destruct}} + +The tactic {\tt destruct} is used to perform case analysis without +recursion. Its behavior is similar to {\tt induction} except +that no induction hypothesis is generated. It applies to any goal and +the type of {\term} must be inductively defined. There are particular cases: + +\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}} + +\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. + +\Rem For destruction of a numeral, use syntax {\tt destruct +({\num})} (not very interesting anyway). + +\end{itemize} + +\begin{Variants} +\item{\tt destruct {\term} as {\intropattern}} + + This behaves as {\tt destruct {\term}} but uses the names in + {\intropattern} to names 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$'s can be any introduction patterns (see + Section~\ref{intros-pattern}). This provides a concise notation for + nested destruction. + +% It is recommended to use this variant of {\tt destruct} for +% robust proof scripts. + +\Rem for an inductive type with one constructor, the pattern notation +{\tt ($p_{1}$,\ldots,$p_{n}$)} can be used instead of +{\tt [} $p_{1} $\ldots $p_{n}$ {\tt ]}. + +\item{\tt destruct {\term} using {\qualid}} + + This is a synonym of {\tt induction {\term} using {\qualid}}. + +\item{\tt destruct {\term} as {\intropattern} using {\qualid}} + + This is a synonym of {\tt induction {\term} using {\qualid} as + {\intropattern}}. + +\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 \term$_1$ \dots\ \term$_n$} + \tacindex{case \dots\ with} + + Analogous to {\tt elim \dots\ with} above. + +\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. + +\end{Variants} + +\subsection{\tt intros {\intropattern} {\ldots} {\intropattern} +\label{intros-pattern} +\tacindex{intros \intropattern}} + +The tactic {\tt intros} applied to introduction patterns performs both +introduction of variables and case analysis in order to give names to +components of an hypothesis. + +An introduction pattern is either: +\begin{itemize} +\item the wildcard: {\tt \_} +\item a variable +\item a disjunction of lists of patterns: + {\tt [$p_{11}$ {\ldots} $p_{1m_1}$ | {\ldots} | $p_{11}$ {\ldots} $p_{nm_n}$]} +\item a conjunction of patterns: {\tt (} $p_1$ {\tt ,} {\ldots} {\tt ,} $p_n$ {\tt )} +\end{itemize} + +The behavior of \texttt{intros} is defined inductively over the +structure of the pattern given as argument: +\begin{itemize} +\item introduction on the wildcard do the introduction and then + immediately clear (cf~\ref{clear}) the corresponding hypothesis; +\item introduction on a variable behaves like described in~\ref{intro}; +\item introduction over a +list of patterns $p_1~\ldots~p_n$ is equivalent to the sequence of +introductions over the patterns namely: +\texttt{intros $p_1$;\ldots; intros $p_n$}, the goal should start with +at least $n$ products; +\item introduction over a +disjunction of list of patterns +{\tt [$p_{11}$ {\ldots} $p_{1m_1}$ | {\ldots} | $p_{11}$ {\ldots} $p_{nm_n}$]}. It introduces a new variable $X$, its type should be an inductive +definition with $n$ +constructors, then it performs a case analysis over $X$ +(which generates $n$ subgoals), it +clears $X$ and performs on each generated subgoals the corresponding +\texttt{intros}~$p_{i1}$ {\ldots} $p_{im_i}$ tactic; +\item introduction over a +conjunction of patterns $(p_1,\ldots,p_n)$, it +introduces a new variable $X$, its type should be an inductive +definition with $1$ +constructor with (at least) $n$ arguments, then it performs a case +analysis over $X$ +(which generates $1$ subgoal with at least $n$ products), it +clears $X$ and performs an introduction over the list of patterns $p_1~\ldots~p_n$. +\end{itemize} + +\Rem The pattern {\tt ($p_1$, {\ldots}, $p_n$)} +is a synonym for the pattern {\tt [$p_1$ {\ldots} $p_n$]}, i.e. it +corresponds to the decomposition of an hypothesis typed by an +inductive type with a single constructor. + +\begin{coq_example} +Lemma intros_test : forall A B C:Prop, A \/ B /\ C -> (A -> C) -> C. +intros A B C [a| [_ c]] f. +apply (f a). +Proof c. +\end{coq_example} + +%\subsection{\tt FixPoint \dots}\tacindex{Fixpoint} +%Not yet documented. + +\subsection {\tt double induction \ident$_1$ \ident$_2$ +\tacindex{double induction}} + +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 the case for \verb+(P (S n) (S m))+ with the induction +hypotheses \verb+(P (S n) m)+ and \verb+(m:nat)(P n m)+ (hence +\verb+(P n m)+ and \verb+(P n (S m))+). + +\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 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 an {\num} is valid. + +\end{Variant} + +\subsection{\tt decompose [ {\qualid$_1$} \dots\ {\qualid$_n$} ] \term +\label{decompose} +\tacindex{decompose}} + +This tactic allows to recursively decompose a +complex proposition in order to obtain atomic ones. +Example: + +\begin{coq_eval} +Reset Initial. +\end{coq_eval} +\begin{coq_example} +Lemma ex1 : 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 p.~\pageref{Record}). +\end{Variants} + + +\subsection{\tt functional induction \ident\ \term$_1$ \dots\ \term$_n$. +\tacindex{functional induction} +\label{FunInduction}} + +The \emph{experimental} tactic \texttt{functional induction} +performs case analysis and induction following the definition of +a (not mutually recursive) function. + +\begin{coq_eval} +Reset Initial. +\end{coq_eval} +\begin{coq_example} +Lemma le_minus : forall n m:nat, (n - m <= n). +intros n m. +functional induction minus n m; simpl; auto. +\end{coq_example} +\begin{coq_example*} +Qed. +\end{coq_example*} + +\texttt{functional induction} is a shorthand for the more general +command \texttt{Functional Scheme} which builds induction +principles following the recursive structure of (possibly +mutually recursive) +functions. \SeeAlso{\ref{FunScheme-examples}} for the difference +between using one or the other. + +\Rem \texttt{functional induction} may fail on functions built by +tactics. In particular case analysis of a function are considered +only if they are not inside an application. + +\Rem Arguments of the function must be given, including the +implicit ones. If the function is recursive, arguments must be +variables, otherwise they may be any term. + +\SeeAlso{\ref{FunScheme},\ref{FunScheme-examples}} + +\section{Equality} + +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{(x$_1$:A$_1$) \dots\ (x$_n$:A$_n$)}\term$_1${\tt =}\term$_2$. + +\noindent Then {\tt rewrite \term} replaces every occurrence of +\term$_1$ by \term$_2$ in the goal. Some of the variables x$_1$ 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 {\ident}} + \tacindex{rewrite \dots\ in}\\ + Analogous to {\tt rewrite {\term}} but rewriting is done in the + hypothesis named {\ident}. + +\item {\tt rewrite -> {\term} in {\ident}} + \tacindex{rewrite -> \dots\ in}\\ + Behaves as {\tt rewrite {\term} in {\ident}}. + +\item {\tt rewrite <- {\term} in {\ident}}\\ + \tacindex{rewrite <- \dots\ in} + Uses the equality \term$_1${\tt=}\term$_2$ from right to left to + rewrite in the hypothesis named {\ident}. +\end{Variants} + + +\subsection{\tt cutrewrite -> \term$_1$ = \term$_2$ +\label{cutrewrite} +\tacindex{cutrewrite}} + +This tactic acts like {\tt replace {\term$_1$} with {\term$_2$}} +(see below). + +\subsection{\tt replace {\term$_1$} with {\term$_2$} +\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 amongst 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{Variants} + +\item {\tt replace {\term$_1$} with {\term$_2$} in \ident}\\ + This replaces {\term$_1$} with {\term$_2$} in the hypothesis named + {\ident}, and generates the subgoal {\term$_2$}{\tt =}{\term$_1$}. + + \begin{ErrMsgs} + \item \errindex{No such hypothesis} : {\ident} + \item \errindex{Nothing to rewrite in {\ident}} + \end{ErrMsgs} + +\end{Variants} + +\subsection{\tt reflexivity +\label{reflexivity} +\tacindex{reflexivity}} + +This tactic applies to a goal which 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{Impossible to unify \dots\ with ..} +\end{ErrMsgs} + +\subsection{\tt symmetry +\tacindex{symmetry} +\tacindex{symmetry in}} +This tactic applies to a goal which has the form {\tt t=u} and changes it +into {\tt u=t}. + +\variant {\tt symmetry in {\ident}}\\ +If the statement of the hypothesis {\ident} has the form {\tt t=u}, +the tactic changes it to {\tt u=t}. + +\subsection{\tt transitivity \term +\tacindex{transitivity}} +This tactic applies to a goal which has the form {\tt t=u} +and transforms it into the two subgoals +{\tt t={\term}} and {\tt {\term}=u}. + +\subsection{\tt subst {\ident} +\tacindex{subst}} + +This tactic applies to a goal which has \ident\ in its context and +(at least) one hypothesis, say {\tt H}, of type {\tt + \ident=t} or {\tt t=\ident}. Then it replaces +\ident\ by {\tt t} everywhere in the goal (in the hypotheses +and in the conclusion) and clears \ident\ and {\tt H} from the context. + +\Rem +When several hypotheses have the form {\tt \ident=t} or {\tt + t=\ident}, the first one is used. + +\begin{Variants} + \item {\tt subst \ident$_1$ \dots \ident$_n$} \\ + Is equivalent to {\tt subst \ident$_1$; \dots; subst \ident$_n$}. + \item {\tt subst} \\ + Applies {\tt subst} repeatedly to all identifiers from the context + for which an equality exists. +\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 {\qualid}.} +\end{quote} +where {\qualid} is the name of the lemma. + +The tactic is especially useful for parametric setoids which are not +accepted as regular setoids for {\tt rewrite} and {\tt setoid\_replace} (see chapter \ref{setoid_replace}). + +\tacindex{stepr} +\comindex{Declare Right Step} +\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}}\\ +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 +\begin{quote} +{\tt Declare Right Step {\qualid}.} +\end{quote} +\end{Variants} + +\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. + +\begin{Variants} +\item {\tt decide equality {\term}$_1$ {\term}$_2$ }.\\ + Solves a goal of the form {\tt \{}\term$_1${\tt =}\term$_2${\tt +\}+\{\verb|~|}\term$_1${\tt =}\term$_2${\tt \}}. +\end{Variants} + +\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 discriminate {\ident} +\label{discriminate} +\tacindex{discriminate}} + +This tactic proves any goal from an absurd hypothesis stating that two +structurally different terms of an inductive set are equal. For +example, from the hypothesis {\tt (S (S O))=(S O)} we can derive by +absurdity any proposition. Let {\ident} be a hypothesis of type +{\tt{\term$_1$} = {\term$_2$}} in the local context, {\term$_1$} and +{\term$_2$} being elements of an inductive set. To build the proof, +the tactic traverses the normal forms\footnote{Recall: 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 If {\ident} does not denote an hypothesis in the local context +but refers to an hypothesis quantified in the goal, then the +latter is first introduced in the local context using +\texttt{intros until \ident}. + +\begin{ErrMsgs} +\item {\ident} \errindex{Not a discriminable equality} \\ + occurs when the type of the specified hypothesis is not an equation. +\end{ErrMsgs} + +\begin{Variants} +\item \texttt{discriminate} \num\\ + This does the same thing as \texttt{intros until \num} then +\texttt{discriminate \ident} where {\ident} is the identifier for the last +introduced hypothesis. +\item {\tt discriminate}\tacindex{discriminate} \\ + It applies to a goal of the form {\tt + \verb=~={\term$_1$}={\term$_2$}} and it is equivalent to: + {\tt unfold not; intro {\ident}}; {\tt discriminate + {\ident}}. + + \begin{ErrMsgs} + \item \errindex{No discriminable equalities} \\ + occurs when the goal does not verify the expected preconditions. + \end{ErrMsgs} +\end{Variants} + +\subsection{\tt injection {\ident} +\label{injection} +\tacindex{injection}} + +The {\tt injection} tactic is based on the fact that constructors of +inductive sets are injections. That means that if $c$ is a constructor +of an inductive set, and if $(c~\vec{t_1})$ and $(c~\vec{t_2})$ are two +terms that are equal then $~\vec{t_1}$ and $~\vec{t_2}$ are equal +too. + +If {\ident} is an hypothesis of type {\tt {\term$_1$} = {\term$_2$}}, +then {\tt injection} behaves as applying injection as deep as possible to +derive the equality of all the subterms of {\term$_1$} and {\term$_2$} +placed in the same positions. For example, from the hypothesis {\tt (S + (S n))=(S (S (S m))} we may derive {\tt n=(S m)}. To use this +tactic {\term$_1$} and {\term$_2$} should be elements of an inductive +set and they should be neither explicitly equal, nor structurally +different. We mean by this that, if {\tt n$_1$} and {\tt n$_2$} are +their respective normal forms, then: +\begin{itemize} +\item {\tt n$_1$} and {\tt n$_2$} should not be syntactically equal, +\item there must not exist any couple of subterms {\tt u} and {\tt w}, + {\tt u} subterm of {\tt n$_1$} and {\tt w} subterm of {\tt n$_2$} , + placed in the same positions and having different constructors as + head symbols. +\end{itemize} +If these conditions are satisfied, then, the tactic derives the +equality of all the subterms of {\term$_1$} and {\term$_2$} placed in +the same positions and puts them as antecedents 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 always an equality in a sigma type +whenever the injected object has a dependent type. + +\Rem If {\ident} does not denote an hypothesis in the local context +but refers to an hypothesis quantified in the goal, then the +latter is first introduced in the local context using +\texttt{intros until \ident}. + +\begin{ErrMsgs} +\item {\ident} \errindex{is not a projectable equality} + occurs when the type of + the hypothesis $id$ does not verify the preconditions. +\item \errindex{Not an equation} occurs when the type of the + hypothesis $id$ is not an equation. +\end{ErrMsgs} + +\begin{Variants} +\item \texttt{injection} \num{} + + This does the same thing as \texttt{intros until \num} then +\texttt{injection \ident} where {\ident} is the identifier for the last +introduced hypothesis. + +\item{\tt injection}\tacindex{injection} + + If the current goal is of the form {\term$_1$} {\tt <>} {\term$_2$}, + the tactic computes the head normal form of the goal and then + behaves as the sequence: {\tt unfold not; intro {\ident}; injection + {\ident}}. + + \ErrMsg \errindex{goal does not satisfy the expected preconditions} +\end{Variants} + +\subsection{\tt simplify\_eq {\ident} +\tacindex{simplify\_eq} +\label{simplify-eq}} + +Let {\ident} be the name of an hypothesis of type {\tt + {\term$_1$}={\term$_2$}} in the local context. 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 {\ident}} otherwise it behaves as {\tt injection + {\ident}}. + +\Rem If {\ident} does not denote an hypothesis in the local context +but refers to an hypothesis quantified in the goal, then the +latter is first introduced 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{\tt simplify\_eq} +If the current goal has form $\verb=~=t_1=t_2$, then this tactic does +\texttt{hnf; 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+(existS A B a b)=(existS A 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 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 an hypothesis in the local context +but refers to an hypothesis quantified in the goal, then the +latter is first introduced in the local context using +\texttt{intros until \ident}. + +\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} \texttt{as} {\intropattern} + + This 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 induction} 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}$ + \ldots $p_{ijq}$]} (or, equivalently, {\tt ($p_{ij1}$, + \ldots, $p_{ijq}$)}) where $q$ is the number of subequations + obtained from splitting the original equation. Here is an example. + +\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} {\tt as} {\intropattern} + + This allows to name the hypotheses introduced by + \texttt{inversion} {\num} in the context. + +\item \tacindex{inversion\_cleardots\ as} \texttt{inversion\_clear} + {\ident} {\tt as} {\intropattern} + + This allows to name the hypotheses introduced by + \texttt{inversion\_clear} in the context. + +\item \tacindex{inversion \dots\ in} \texttt{inversion } {\ident} + \texttt{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} {\tt as} {\intropattern} \texttt{in} \ident$_1$ \dots\ + \ident$_n$ + + This allows to name the hypotheses introduced in the context by + \texttt{inversion} {\ident} \texttt{in} \ident$_1$ \dots\ + \ident$_n$. + +\item \tacindex{inversion\_clear \dots\ in} \texttt{inversion\_clear} + {\ident} \texttt{in} \ident$_1$ \ldots \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} \texttt{as} {\intropattern} + \texttt{in} \ident$_1$ \ldots \ident$_n$ + + This allows to name the hypotheses introduced in the context by + \texttt{inversion\_clear} {\ident} \texttt{in} \ident$_1$ \ldots + \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} \texttt{as} {\intropattern} + + This allows to name 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}\texttt{as} {\intropattern} + + This allows to name the hypotheses introduced in the context by + \texttt{dependent inversion\_clear} {\ident} + +\item \tacindex{dependent inversion \dots\ with} \texttt{dependent + inversion } {\ident} \texttt{ with } \term + + This variant allow to give the good 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} \texttt{as} {\intropattern} + \texttt{ with } \term + + This allows to name the hypotheses introduced in the context by + \texttt{dependent inversion } {\ident} \texttt{ with } \term. + +\item \tacindex{dependent inversion\_clear \dots\ with} + \texttt{dependent inversion\_clear } {\ident} \texttt{ 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} \texttt{as} + {\intropattern} \texttt{ with } \term + + This allows to name the hypotheses introduced in the context by + \texttt{dependent inversion\_clear } {\ident} \texttt{ 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} do. + +\item \tacindex{simple inversion \dots\ as} \texttt{simple inversion} + {\ident} \texttt{as} {\intropattern} + + This allows to name the hypotheses introduced in the context by + \texttt{simple inversion}. + +\item \tacindex{inversion \dots\ using} \texttt{inversion} \ident + \texttt{ 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} \texttt{using} \ident$'$ \texttt{in} \ident$_1$\dots\ \ident$_n$ + + This tactic behaves as generalizing \ident$_1$\dots\ \ident$_n$, + then doing \texttt{inversion}{\ident}\texttt{using} \ident$'$. + +\end{Variants} + +\SeeAlso~\ref{inversion-examples} for detailed examples + +\subsection{\tt Derive Inversion {\ident} with + ${\tt forall (}\vec{x}{\tt :}\vec{T}{\tt),} I~\vec{t}$ Sort \sort +\label{Derive-Inversion} +\comindex{Derive Inversion}} + +This command generates an inversion principle for the +\texttt{inversion \dots\ using} tactic. +Let $I$ be an inductive predicate and $\vec{x}$ the variables +occurring in $\vec{t}$. This command generates and stocks the +inversion lemma for the sort \sort~ corresponding to the instance +$forall (\vec{x}:\vec{T}), I~\vec{t}$ with the name {\ident} in the {\bf +global} environment. When applied it is equivalent to have inverted +the instance with the tactic {\tt inversion}. + +\begin{Variants} +\item \texttt{Derive Inversion\_clear} {\ident} \texttt{with} + \comindex{Derive Inversion\_clear} + $forall (\vec{x}:\vec{T}), I~\vec{t}$ \texttt{Sort} \sort~ \\ + \index{Derive Inversion\_clear \dots\ with} + When applied it is equivalent to having + inverted the instance with the tactic \texttt{inversion} + replaced by the tactic \texttt{inversion\_clear}. +\item \texttt{Derive Dependent Inversion} {\ident} \texttt{with} + $forall (\vec{x}:\vec{T}), I~\vec{t}$ \texttt{Sort} \sort~\\ + \comindex{Derive Dependent Inversion} + When applied it is equivalent to having + inverted the instance with the tactic \texttt{dependent inversion}. +\item \texttt{Derive Dependent Inversion\_clear} {\ident} \texttt{with} + $forall (\vec{x}:\vec{T}), I~\vec{t}$ \texttt{Sort} \sort~\\ + \comindex{Derive Dependent Inversion\_clear} + When applied it is equivalent to having + inverted the instance with the tactic \texttt{dependent inversion\_clear}. +\end{Variants} + +\SeeAlso \ref{inversion-examples} for examples + +\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 build 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 build 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{Automatizing +\label{Automatizing}} + +\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 introducing 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. This option can be combined with the previous one. + +\item {\tt auto with *} + + Uses all existing hint databases, minus the special database + {\tt v62}. See Section~\ref{Hints-databases} + +\item {\tt trivial}\tacindex{trivial} + + This tactic is a restriction of {\tt auto} that is not recursive and + tries only hints which cost is 0. Typically it solves trivial + equalities like $X=X$. + +\item \texttt{trivial with \ident$_1$ \dots\ \ident$_n$} + +\item \texttt{trivial with *} + +\end{Variants} + +\Rem {\tt auto} either solves completely the goal or else leave it +intact. \texttt{auto} and \texttt{trivial} never fail. + +\SeeAlso Section~\ref{Hints-databases} + +\subsection{\tt eauto +\tacindex{eauto} +\label{eauto}} + +This tactic generalizes {\tt auto}. In contrast with +the latter, {\tt eauto} uses unification of the goal +against the hints rather than pattern-matching +(in other words, it uses {\tt eapply} instead of +{\tt apply}). +As a consequence, {\tt eauto} can solve such a goal: + +\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 an +hint. + +\SeeAlso Section~\ref{Hints-databases} + +% 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 tauto +\tacindex{tauto} +\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. + +\subsection{\tt intuition {\tac} +\tacindex{intuition} +\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 reengineered by David~Delahaye using mainly the tactic +language (see chapter~\ref{TacticLanguage}). The code is now quite shorter and +a significant increase in performances 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 *}. +\end{Variants} + +% En attente d'un moyen de valoriser les fichiers de demos +%\SeeAlso file \texttt{contrib/Rocq/DEMOS/Demo\_tauto.v} + +\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. + +\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 with \ident$_1$ \dots\ \ident$_n$ } + \tacindex{firstorder with} + + Adds lemmas \ident$_1$ \dots\ \ident$_n$ to the proof-search + environment. + + \item {\tt firstorder using \ident$_1$ \dots\ \ident$_n$ } + \tacindex{firstorder using} + + Adds lemmas in {\tt auto} hints bases \ident$_1$ \dots\ \ident$_n$ + to the proof-search environment. +\end{Variants} + +Proof-search is bounded by a depth parameter which can be set by typing the +{\nobreak \tt Set Firstorder Depth $n$} \comindex{Set Firstorder Depth} +vernacular command. + +%% \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 optionnaly 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}\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 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. + +\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{ErrMsgs} + \item \errindex{I don't know how to handle dependent equality} \\ + The decision procedure managed to find a proof of the goal or of + a discriminable equality but this proof couldn't be built in Coq + because of dependently-typed functions. + \item \errindex{I couldn't solve goal} \\ + The decision procedure didn't managed to find a proof of the goal or of + a discriminable equality. +\end{ErrMsgs} + +\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 and inequalities 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} +(chapter~\ref{OmegaChapter}). + +\subsection{\tt ring \term$_1$ \dots\ \term$_n$ +\tacindex{ring} +\comindex{Add Ring} +\comindex{Add Semi Ring}} + +This tactic, written by Samuel Boutin and Patrick Loiseleur, applies +associative commutative rewriting on every ring. The tactic must be +loaded by \texttt{Require Import Ring}. The ring must be declared in +the \texttt{Add Ring} command (see \ref{ring}). The ring of booleans +is predefined; if one wants to use the tactic on \texttt{nat} one must +first require the module \texttt{ArithRing}; for \texttt{Z}, do +\texttt{Require Import ZArithRing}; for \texttt{N}, do \texttt{Require +Import NArithRing}. + +The terms \term$_1$, \dots, \term$_n$ must be subterms of the goal +conclusion. The tactic \texttt{ring} normalizes these terms +w.r.t. associativity and commutativity and replace them by their +normal form. + +\begin{Variants} +\item \texttt{ring} When the goal is an equality $t_1=t_2$, it + acts like \texttt{ring} $t_1$ $t_2$ and then simplifies or solves + the equality. + +\item \texttt{ring\_nat} is a tactic macro for \texttt{repeat rewrite + S\_to\_plus\_one; ring}. The theorem \texttt{S\_to\_plus\_one} is a + proof that \texttt{forall (n:nat), S n = plus (S O) n}. + +\end{Variants} + +\Example +\begin{coq_eval} +Reset Initial. +Require Import ZArith. +Open Scope Z_scope. +\end{coq_eval} +\begin{coq_example} +Require Import ZArithRing. +Goal forall a b c:Z, + (a + b + c) * (a + b + c) = + a * a + b * b + c * c + 2 * a * b + 2 * a * c + 2 * b * c. +\end{coq_example} +\begin{coq_example} +intros; ring. +\end{coq_example} +\begin{coq_eval} +Reset Initial. +\end{coq_eval} + +You can have a look at the files \texttt{Ring.v}, +\texttt{ArithRing.v}, \texttt{ZArithRing.v} to see examples of the +\texttt{Add Ring} command. + +\SeeAlso Chapter~\ref{ring} for more detailed explanations about this tactic. + +\subsection{\tt field +\tacindex{field}} + +This tactic written by David~Delahaye and Micaela~Mayero solves equalities +using commutative field theory. Denominators have to be non equal to zero and, +as this is not decidable in general, this tactic may generate side conditions +requiring some expressions to be non equal to zero. This tactic must be loaded +by {\tt Require Import Field}. Field theories are declared (as for {\tt ring}) with +the {\tt Add Field} command. + +\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} + +\subsection{\tt Add Field +\comindex{Add Field}} + +This vernacular command adds a commutative field theory to the database for the +tactic {\tt field}. You must provide this theory as follows: +\begin{flushleft} +{\tt Add Field {\it A} {\it Aplus} {\it Amult} {\it Aone} {\it Azero} {\it +Aopp} {\it Aeq} {\it Ainv} {\it Rth} {\it Tinvl}} +\end{flushleft} +where {\tt {\it A}} is a term of type {\tt Type}, {\tt {\it Aplus}} is +a term of type {\tt A->A->A}, {\tt {\it Amult}} is a term of type {\tt + A->A->A}, {\tt {\it Aone}} is a term of type {\tt A}, {\tt {\it + Azero}} is a term of type {\tt A}, {\tt {\it Aopp}} is a term of +type {\tt A->A}, {\tt {\it Aeq}} is a term of type {\tt A->bool}, {\tt + {\it Ainv}} is a term of type {\tt A->A}, {\tt {\it Rth}} is a term +of type {\tt (Ring\_Theory {\it A Aplus Amult Aone Azero Ainv Aeq})}, +and {\tt {\it Tinvl}} is a term of type {\tt forall n:{\it A}, + {\~{}}(n={\it Azero})->({\it Amult} ({\it Ainv} n) n)={\it Aone}}. +To build a ring theory, refer to Chapter~\ref{ring} for more details. + +This command adds also an entry in the ring theory table if this theory is not +already declared. So, it is useless to keep, for a given type, the {\tt Add +Ring} command if you declare a theory with {\tt Add Field}, except if you plan +to use specific features of {\tt ring} (see Chapter~\ref{ring}). However, the +module {\tt ring} is not loaded by {\tt Add Field} and you have to make a {\tt +Require Import Ring} if you want to call the {\tt ring} tactic. + +\begin{Variants} + +\item {\tt Add Field {\it A} {\it Aplus} {\it Amult} {\it Aone} {\it Azero} +{\it Aopp} {\it Aeq} {\it Ainv} {\it Rth} {\it Tinvl}}\\ +{\tt \phantom{Add Field }with minus:={\it Aminus}} + +Adds also the term {\it Aminus} which must be a constant expressed by +means of {\it Aopp}. + +\item {\tt Add Field {\it A} {\it Aplus} {\it Amult} {\it Aone} {\it Azero} +{\it Aopp} {\it Aeq} {\it Ainv} {\it Rth} {\it Tinvl}}\\ +{\tt \phantom{Add Field }with div:={\it Adiv}} + +Adds also the term {\it Adiv} which must be a constant expressed by +means of {\it Ainv}. + +\end{Variants} + +\SeeAlso file {\tt theories/Reals/Rbase.v} for an example of instantiation,\\ +\phantom{\SeeAlso}theory {\tt theories/Reals} for many examples of use of {\tt +field}. + +\SeeAlso \cite{DelMay01} for more details regarding the implementation of {\tt +field}. + +\subsection{\tt fourier +\tacindex{fourier}} + +This tactic written by Lo{\"\i}c Pottier solves linear inequations 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} + +\subsection{\tt autorewrite with \ident$_1$ \dots \ident$_n$. +\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 reengineering of the code, this tactic has also been completely revised +to get a very compact and readable version.} carries out rewritings according +the rewriting rule bases {\tt \ident$_1$ \dots \ident$_n$}. + + Each rewriting rule of a base \ident$_i$ is applied to the main subgoal until +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$ \dots \ident$_n$ using \tac}\\ +Performs, in the same way, all the rewritings of the bases {\tt $ident_1$ $...$ +$ident_n$} applying {\tt \tac} to the main subgoal after each rewriting step. +%\item{\tt autorewrite [ \ident$_1$ \dots \ident$_n$ ]}\\ +%{\tt autorewrite [ \ident$_1$ \dots \ident$_n$ ] using \tac}\\ +%These are deprecated syntactic variants for +%{\tt autorewrite with \ident$_1$ \dots \ident$_n$} +%and +%{\tt autorewrite with \ident$_1$ \dots \ident$_n$ using \tac}. +\end{Variant} + +\subsection{\tt Hint Rewrite \term$_1$ \dots \term$_n$ : \ident +\comindex{Hint Rewrite}} + +This vernacular command adds the terms {\tt \term$_1$ \dots \term$_n$} +(their types must be equalities) in the rewriting base {\tt \ident} +with the default orientation (left to right). Notice that the +rewriting bases are distinct from the {\tt auto} hint bases and that +{\tt auto} does not take them into account. + +This command is synchronous with the section mechanism (see \ref{Section}): +when closing a section, all aliases created by \texttt{Hint Rewrite} in that +section are lost. Conversely, when loading a module, all \texttt{Hint Rewrite} +declarations at the global level of that module are loaded. + +\begin{Variants} +\item {\tt Hint Rewrite -> \term$_1$ \dots \term$_n$ : \ident}\\ +This is strictly equivalent to the command above (we only make explicit the +orientation which otherwise defaults to {\tt ->}). + +\item {\tt Hint Rewrite <- \term$_1$ \dots \term$_n$ : \ident}\\ +Adds the rewriting rules {\tt \term$_1$ \dots \term$_n$} with a right-to-left +orientation in the base {\tt \ident}. + +\item {\tt Hint Rewrite \term$_1$ \dots \term$_n$ using {\tac} : {\ident}}\\ +When the rewriting rules {\tt \term$_1$ \dots \term$_n$} in {\tt \ident} will +be used, the tactic {\tt \tac} will be applied to the generated subgoals, the +main subgoal excluded. + +%% \item +%% {\tt Hint Rewrite [ \term$_1$ \dots \term$_n$ ] in \ident}\\ +%% {\tt Hint Rewrite [ \term$_1$ \dots \term$_n$ ] in {\ident} using {\tac}}\\ +%% These are deprecated syntactic variants for +%% {\tt Hint Rewrite \term$_1$ \dots \term$_n$ : \ident} and +%% {\tt Hint Rewrite \term$_1$ \dots \term$_n$ using {\tac} : {\ident}}. + +\end{Variants} + +\SeeAlso \ref{autorewrite-example} for examples showing the use of +this tactic. + +% En attente d'un moyen de valoriser les fichiers de demos +%\SeeAlso file \texttt{contrib/Rocq/DEMOS/Demo\_AutoRewrite.v} + +\section{The hints databases for {\tt auto} and {\tt eauto} +\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 an nonnegative integer, and a 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. The general +command to add a hint to some database \ident$_1$, \dots, \ident$_n$ is: +\begin{tabbing} + \texttt{Hint} \textsl{hint\_definition} \texttt{:} \ident$_1$ \ldots\ \ident$_n$ +\end{tabbing} +where {\sl hint\_definition} is one of the following expressions: + +\begin{itemize} +\item \texttt{Resolve} {\term} + \comindex{Hint Resolve} + + This command adds {\tt 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 apply {\term}}. + + In case the inferred type of \term\ does not start with a product the + tactic added in the hint list is {\tt exact {\term}}. In case this + type can be reduced to a type starting with a product, the tactic {\tt + apply {\term}} is also stored in the hints list. + + If the inferred type of \term\ does contain a dependent + quantification on a predicate, it is added to the hint list of {\tt + eapply} instead of the hint list of {\tt apply}. In this case, a + warning is printed since the hint is only used by the tactic {\tt + eauto} (see \ref{eauto}). A typical example of hint that is used + only by \texttt{eauto} is a transitivity lemma. + + \begin{ErrMsgs} + \item \errindex{Bound head variable} + + The head symbol of the type of {\term} is a bound variable such + that this tactic cannot be associated to a constant. + + \item \term\ \errindex{cannot be used as a hint} + + The type of \term\ contains products over variables which do not + appear in the conclusion. A typical example is a transitivity axiom. + In that case the {\tt apply} tactic fails, and thus is useless. + + \end{ErrMsgs} + + \begin{Variants} + + \item \texttt{Resolve} {\term$_1$} \dots {\term$_m$} + + Adds each \texttt{Resolve} {\term$_i$}. + + \end{Variants} + +\item \texttt{Immediate {\term}} +\comindex{Hint Immediate} + + This command adds {\tt 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 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 that 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 \texttt{Immediate} {\term$_1$} \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} + + \item {\ident} \errindex{not declared} + + \end{ErrMsgs} + + \begin{Variants} + + \item \texttt{Constructors} {\ident$_1$} \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 \texttt{Unfold} {\ident$_1$} \dots {\ident$_m$} + + Adds each \texttt{Unfold} {\ident$_i$}. + + \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, a 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 succeed 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 ident, 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 auto with eqdec. +\end{coq_example} +\begin{coq_eval} +Abort. +\end{coq_eval} + +\end{itemize} + +\Rem There is currently (in the \coqversion\ release) no way to do +pattern-matching on hypotheses. + +\begin{Variants} +\item \texttt{Hint} \textsl{hint\_definition} + + No database name is given : the hint is registered in the {\tt core} + database. + +\item\texttt{Hint Local} \textsl{hint\_definition} \texttt{:} + \ident$_1$ \ldots\ \ident$_n$ + + This is used to declare hints that must not be exported to the other + modules that require and import the current module. Inside a + section, the option {\tt Local} is useless since hints do not + survive anyway to the closure of sections. + +\item\texttt{Hint Local} \textsl{hint\_definition} + + Idem for the {\tt core} database. + +\end{Variants} + +% 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} and {\tt v62} +databases are non empty and can be used. + +\begin{description} + +\item[\tt core] This special database is automatically used by + \texttt{auto}. It contains only basic lemmas about negation, + 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 proven 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 inequations 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 proven in the \texttt{Lists} subdirectory. + +\item[\tt sets] contains lemmas about sets and relations from the + directories \texttt{Sets} and \texttt{Relations}. +\end{description} + +There is also a special database called {\tt v62}. It collects all +hints that were declared in the versions of {\Coq} prior to version +6.2.4 when the databases {\tt core}, {\tt arith}, and so on were +introduced. The purpose of the database {\tt v62} is to ensure +compatibility with further versions of Coq for developments done in +versions prior to 6.2.4 ({\tt auto} being replaced by {\tt auto with v62}). +The database {\tt v62} is intended not to be extended (!). It is not +included in the hint databases list used in the {\tt auto with *} tactic. + +Furthermore, 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 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, to 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{Hints and sections +\label{Hint-and-Section}} + +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.}). + +\section{Generation of induction principles with {\tt Scheme} +\label{Scheme} +\comindex{Scheme}} + +The {\tt Scheme} command is a high-level tool for generating +automatically (possibly mutual) induction principles for given types +and sorts. Its syntax follows the schema: +\begin{tabbing} +{\tt Scheme {\ident$_1$} := Induction for \ident'$_1$ Sort {\sort$_1$} \\ + with\\ + \mbox{}\hspace{0.1cm} \dots\ \\ + with {\ident$_m$} := Induction for {\ident'$_m$} Sort + {\sort$_m$}} +\end{tabbing} +\ident'$_1$ \dots\ \ident'$_m$ are different inductive type +identifiers belonging to the same package of mutual inductive +definitions. This command generates {\ident$_1$}\dots{} {\ident$_m$} +to be mutually recursive definitions. Each term {\ident$_i$} proves a +general principle of mutual induction for objects in type {\term$_i$}. + +\begin{Variants} +\item {\tt Scheme {\ident$_1$} := Minimality for \ident'$_1$ Sort {\sort$_1$} \\ + with\\ + \mbox{}\hspace{0.1cm} \dots\ \\ + with {\ident$_m$} := Minimality for {\ident'$_m$} Sort + {\sort$_m$}} + + Same as before but defines a non-dependent elimination principle more + natural in case of inductively defined relations. +\end{Variants} + +\SeeAlso \ref{Scheme-examples} + +\SeeAlso Section~\ref{Scheme-examples} + +\section{Generation of induction principles with {\tt Functional Scheme} +\label{FunScheme} +\comindex{Functional Scheme}} + +The {\tt Functional Scheme} command is a high-level experimental +tool for generating automatically induction principles +corresponding to (possibly mutually recursive) functions. Its +syntax follows the schema: +\begin{tabbing} +{\tt Functional Scheme {\ident$_i$} := Induction for + \ident'$_i$ with \ident'$_1$ \dots\ \ident'$_m$.} +\end{tabbing} +\ident'$_1$ \dots\ \ident'$_m$ are the names of mutually recursive +functions (they must be in the same order as when they were defined), +\ident'$_i$ being one of them. This command generates the induction +principle \ident$_i$, following the recursive structure and case +analyses of the functions \ident'$_1$ \dots\ \ident'$_m$, and having +\ident'$_i$ as entry point. + +\begin{Variants} +\item {\tt Functional Scheme {\ident$_1$} := Induction for \ident'$_1$.} + + This command is a shortcut for: + \begin{tabbing} + {\tt Functional Scheme {\ident$_1$} := Induction for + \ident'$_1$ with \ident'$_1$.} +\end{tabbing} + +This variant can be used for non mutually recursive functions only. +\end{Variants} + +\SeeAlso Section~\ref{FunScheme-examples} + + +\section{Simple tactic macros +\index{tactic macros} +\comindex{Tactic Definition} +\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. + +The chapter~\ref{TacticLanguage} gives examples of more complex +user-defined tactics. + + +% $Id: RefMan-tac.tex 8606 2006-02-23 13:58:10Z herbelin $ + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "Reference-Manual" +%%% TeX-master: "Reference-Manual" +%%% End: |