path: root/doc/RefMan-tac.tex

\chapter{Tactics}
\index{Tactics}
\label{Tactics}

A deduction rule is a link between some (unique) formula, that we call
the {\em conclusion} and (several) formul{\ae} 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{There is an unknown subterm I cannot solve}: 
  there is a hole in the term you gave
  which type cannot be inferred. Put a cast around it.
\end{ErrMsgs}

This tactic is currently given as an experiment. 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{No such assumption}
\item \errindex{{\ident} is used in the conclusion}
\item \errindex{{\ident} is used in the hypothesis {\ident'}}
\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{No such assumption: {\ident$_i$}}

\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{No such assumption}

\item \errindex{{\ident$_2$} 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 {\tt U}.
% If the {\tt x} has been renamed {\tt x}{\it n} then it is replaced 
% by {\tt x}{\it n} in {\tt U}. 

If the goal is a non dependent product T -> U, then it puts in the
local context either {\tt H}{\it n}{\tt :T} (if {\tt T} is {\tt Set}
or {\tt Prop}) or {\tt X}{\it n}{\tt :T} (if the type of {\tt T} is
{\tt Type}) {\it n} is such that {\tt H}{\it n} or {\tt X}{\it n}
{\tt l}{\it n} or are fresh identifiers.  In both cases the new
subgoal is {\tt 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 \errindex{\texttt{{\ident} 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 bound }

  \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
instantiations of the premises of the type of {\term}.

\begin{ErrMsgs}
\item \errindex{Impossible to unify \dots\ with \dots} 

  Since higher order unification is undecidable, the {\tt apply}
  tactic may fail when you think it should work.  In this case, if you
  know that the conclusion of {\term} and the current goal are
  unifiable, 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{Cannot refine to conclusions with meta-variables}

  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 the 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 Be careful, 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 )}}
\tacindex{set}

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 *}
  
  This is equivalent to the above form but applies everywhere in the
  goal (both in conclusion and hypotheses).

\item {\tt set ( {\ident$_0$} {\tt :=} {\term} {\tt ) in} {\ident$_1$}}
  
  This behaves the same but substitutes {\term} not in the goal but 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 the hypothesis
named {\ident$_1$} (or the goal if {\ident$_1$} is the word {\tt
  Goal}) should be substituted. The occurrences are numbered from left
to right. A negative occurrence number means an occurrence which
should not be substituted.

\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$}
  
  This is the general form. It substitutes {\term} at occurrences
  {\num$_1^i$} \dots\ {\num$_{n_i}^i$} of hypothesis {\ident$_i$}. One
  of the {\ident}'s may be the word {\tt Goal}.


\item {\tt pose (  {\ident} {\tt :=} {\term} {\tt )}}
\tacindex{pose}

  This is equivalent to the default behavior in {\tt set}.
  
%  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}.

\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 a \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}
\index[tactic]{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 \term} (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 \term} 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}
\index[tactic]{Conversion tactics}
\label{Conversion-tactics}

This set of tactics implements different specialized usages of the
tactic \texttt{change}.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%voir reduction__conv_x : histoires d'univers.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\subsection{{\tt cbv} \flag$_1$ \dots\ \flag$_n$, {\tt Lazy} \flag$_1$
\dots\ \flag$_n$ {\rm and} {\tt compute}}
\tacindex{cbv}\tacindex{lazy}

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.  For these
tactics, the {\tt delta} flag does not apply to variables bound by a
let-in construction of which the 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).

Notice that, for these tactics, the {\tt delta} flag without rest
should be understood as unfolding all 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 have 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$-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$-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 will only be applied to transparent constants
(i.e. which have not been frozen with an {\tt Opaque} command; see
section \ref{Opaque}).

\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} will 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 section
\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}
is printed.

\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 \num$_1^1$ \dots\ \num$_i^1$ {\qualid}$_1$ \dots\  \num$_1^n$
    \dots\ \num$_j^n$ \qualid$_n$}
  
  The lists \num$_1^1$, \dots, \num$_i^1$ and \num$_1^n$, \dots,
  \num$_j^n$ are to specify the occurrences of {\qualid}$_1$, \dots,
  \qualid$_n$ to be unfolded. Occurrences are located from left to
  right in the linear
  notation of terms.

  \ErrMsg {\tt bad occurrence numbers of {\qualid}$_i$}

\end{Variants}

\subsection{{\tt fold} \term}
\tacindex{fold}

This tactic applies to any goal. \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 {\tt (P t)} when {\tt t} does not occur in
{\tt P} then {\tt pattern t} transforms it into {\tt ([x:A](P x) t)}. This
command has to be used, for instance, when an {\tt apply} command
fails on matching.

\begin{Variants}
\item {\tt pattern {\num$_1$} \dots\ {\num$_n$} {\term}}
  
  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 {\num$_1^1$} \dots\ {\num$_{n_1}^1$} {\term$_1$} \dots
    {\num$_1^m$} \dots\ {\num$_{n_m}^m$} {\term$_m$}}
  
  Will process 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$.  Starting from a goal {\tt (P t$_1$\dots\ t$_m$)} with
  the {\tt t$_i$} which do not occur in $P$, the tactic {\tt pattern
    t$_1$\dots\ t$_m$} generates the equivalent goal {\tt
    ([x$_1$:A$_1$]\dots\ [x$_m$:A$_m$](P 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.

\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$. 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)$. 
  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$. They are respectively equivalent to {\tt
    constructor 1} and {\tt constructor 2}.
  
\item {\tt left \bindinglist}, {\tt right \bindinglist}, {\tt split
    \bindinglist}
  
  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}

\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.

  It is recommended to use this variant of {\tt induction} for 
  robust proof scripts.

\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.

\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+(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 [ {\ident$_1$} \dots\ {\ident$_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 tactic \texttt{functional induction} performs case analysis
and induction following the definition of a 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.

\Rem \texttt{functional induction} does not work on polymorphic
and dependently typed functions yet. It may also fail on
functions built by certain tactics.

\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. It is equivalent
to {\tt cut \term$_2$=\term$_1$; intro H{\sl n}; rewrite <- H{\sl n}; 
  clear H{\sl n}}.

%N'existe pas...
%\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}
%  \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 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 have 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 have \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}


\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 {\tt \verb=~={\term$_1$}={\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 \texttt{inversion\_clear} \ident\\
  \tacindex{inversion\_clear}
  This behaves as \texttt{inversion} and then erases \ident~ from the
  context.
\item \texttt{inversion} {\ident} \texttt{as} {\intropattern} \\
  \tacindex{inversion \dots\ as} 
  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 \texttt{inversion\_clear} {\ident} {\tt as} {\intropattern} \\
  \tacindex{inversion\_cleardots\ as}
  This allows to name the hypotheses introduced by
  \texttt{inversion\_clear} in the context.
\item \texttt{inversion } {\ident} \texttt{in} \ident$_1$ \dots\ \ident$_n$\\
  \tacindex{inversion \dots\ in}
  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 \texttt{inversion } {\ident}  {\tt as} {\intropattern}
\texttt{in} \ident$_1$ \dots\ \ident$_n$\\
  \tacindex{inversion \dots\ as \dots\ in}
  This allows to name the hypotheses introduced in the context by
  \texttt{inversion} {\ident} \texttt{in} \ident$_1$ \dots\ \ident$_n$.
\item \texttt{inversion\_clear} {\ident} \texttt{in} \ident$_1$ \ldots
  \ident$_n$\\ 
  \tacindex{inversion\_clear \dots\ in}
  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 \texttt{inversion\_clear} {\ident} \texttt{as} {\intropattern}
  \texttt{in} \ident$_1$ \ldots \ident$_n$\\ 
  \tacindex{inversion\_clear \dots\ as \dots\ in}
  This allows to name the hypotheses introduced in the context by
  \texttt{inversion\_clear} {\ident} \texttt{in} \ident$_1$ \ldots \ident$_n$.
\item \texttt{dependent inversion} {\ident}\\
  \tacindex{dependent inversion}
  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 \texttt{dependent inversion} {\ident} \texttt{as} {\intropattern} \\
  \tacindex{dependent inversion \dots\ as }
  This allows to name the hypotheses introduced in the context by
  \texttt{dependent inversion} {\ident}.
\item \texttt{dependent inversion\_clear} {\ident}\\
  \tacindex{dependent inversion\_clear}
  Like \texttt{dependent inversion}, except that {\ident} is cleared
  from the local context.
\item \texttt{dependent inversion\_clear} {\ident}\texttt{as} {\intropattern}\\
  \tacindex{dependent inversion\_clear \dots\ as}
  This allows to name the hypotheses introduced in the context by
  \texttt{dependent inversion\_clear} {\ident}
\item \texttt{dependent inversion } {\ident} \texttt{ with } \term \\
  \tacindex{dependent inversion \dots\ with}
  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 \texttt{dependent inversion } {\ident} \texttt{as} {\intropattern} \texttt{ with } \term \\
  \tacindex{dependent inversion \dots\ as \dots\ with}
  This allows to name the hypotheses introduced in the context by
  \texttt{dependent inversion } {\ident} \texttt{ with } \term.
\item \texttt{dependent inversion\_clear } {\ident} \texttt{ with } \term\\
  \tacindex{dependent inversion\_clear \dots\ with}
  Like \texttt{dependent inversion \dots\ with} but clears \ident from
  the local context.
\item \texttt{dependent inversion\_clear } {\ident} \texttt{as} {\intropattern} \texttt{ with } \term\\
  \tacindex{dependent inversion\_clear \dots\ as \dots\ with}
  This allows to name the hypotheses introduced in the context by
  \texttt{dependent inversion\_clear } {\ident} \texttt{ with } \term.
\item \texttt{simple inversion} {\ident}\\
  \tacindex{simple inversion}
  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 \texttt{simple inversion} {\ident} \texttt{as} {\intropattern}\\
  \tacindex{simple inversion \dots\ as}
  This allows to name the hypotheses introduced in the context by
  \texttt{simple inversion}.
\item \texttt{inversion} \ident \texttt{ using} \ident$'$ \\
  \tacindex{inversion \dots\ using}
  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 \texttt{inversion} {\ident} \texttt{using} \ident$'$ 
  \texttt{in} \ident$_1$\dots\ \ident$_n$\\
  \tacindex{inversion \dots\ using \dots\ in}
  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
  $forall (\vec{x}:\vec{T}), I~\vec{t}$ Sort \sort}
\label{Derive-Inversion}
\comindex{Derive Inversion}
\index[tactic]{Derive Inversion@{\tt 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 builded
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 reenginered 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{\tt 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{\tt firstorder with}
   Adds lemmata \ident$_1$ \dots\ \ident$_n$ to the proof-search
   environment.
 \item {\tt firstorder using \ident$_1$ \dots\ \ident$_n$ }\\
   \tacindex{\tt firstorder using}
   Adds lemmata 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 {\em (Jprover)}}
\label{jprover}

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 constext. 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 Prestburger
arithmetic. It solves quantifier-free 
formulae build with \verb|~|, \verb|\/|, \verb|/\|,
\verb|->| on top of equations and inequations 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:\\

{\tt Add Field {\it A} {\it Aplus} {\it Amult} {\it Aone} {\it Azero} {\it
Aopp} {\it Aeq} {\it Ainv} {\it Rth} {\it Tinvl}}\\

\noindent 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  [ \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 reenginering 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  [ \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.
\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 precise the
orientation which is the default one).

\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.
\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 auto and eauto}
\index{Hints databases}\label{Hints-databases}\comindex{Hint}
The hints for \texttt{auto} and \texttt{eauto} are stored in databases.
Each databases maps head
symbols to 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 hint is
tried by \texttt{auto} if the conclusion of current goal matches its
pattern, and after hints with a lower cost. The general command to add
a hint to some databases \ident$_1$, \dots, \ident$_n$ is:

\comindex{Hint}
\begin{quotation}
  \texttt{Hint} \textsl{hint\_definition} \texttt{:} \ident$_1$ \ldots\ \ident$_n$
\end{quotation}

\noindent where {\sl hint\_definition} is one of the following expressions:

\begin{itemize}
\item \texttt{Resolve} {\term} \index[command]{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}} \index[command]{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}\index[command]{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}\index[command]{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}\index[command]{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. There is no systematic relation between the directories of the
library and the databases.

\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} and
  \texttt{contrib/omega}. It contains also a hint with a high
  cost that calls {\tt omega}.

\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}
\index[tactic]{Hint!\texttt{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:

\noindent
{\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$}}\\

\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}


\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:\bigskip

\noindent
{\tt Functional Scheme {\ident$_i$} := Induction for
    \ident'$_i$ with \ident'$_1$ \dots\ \ident'$_m$.}\\
  
  \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:
  
  {\tt Functional Scheme {\ident$_1$} := Induction for
    \ident'$_1$ with \ident'$_1$.}

  This variant can be used for non mutually recursive functions only.
\end{Variants}

\SeeAlso \ref{FunScheme-examples}


\section{Simple tactic macros}
\index[tactic]{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$ 

%%% Local Variables: 
%%% mode: latex
%%% TeX-master: "Reference-Manual"
%%% TeX-master: "Reference-Manual"
%%% End: