Imported Upstream version 8.1+dfsgupstream/8.1+dfsg

1 files changed, 0 insertions, 3388 deletions

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
deleted file mode 100644
index 24ea78c0..00000000
--- a/doc/refman/RefMan-tac.tex
+++ /dev/null
@@ -1,3388 +0,0 @@
-\chapter{Tactics
-\index{Tactics}
-\label{Tactics}}
-
-A deduction rule is a link between some (unique) formula, that we call
-the {\em conclusion} and (several) formulas that we call the {\em
-premises}. Indeed, a deduction rule can be read in two ways. The first
-one has the shape: {\it ``if I know this and this then I can deduce
-this''}. For instance, if I have a proof of $A$ and a proof of $B$
-then I have a proof of $A \land B$. This is forward reasoning from
-premises to conclusion. The other way says: {\it ``to prove this I
-have to prove this and this''}. For instance, to prove $A \land B$, I
-have to prove $A$ and I have to prove $B$. This is backward reasoning
-which proceeds from conclusion to premises. We say that the conclusion
-is {\em the goal}\index{goal} to prove and premises are {\em the
-subgoals}\index{subgoal}.  The tactics implement {\em backward
-reasoning}. When applied to a goal, a tactic replaces this goal with
-the subgoals it generates. We say that a tactic reduces a goal to its
-subgoal(s).
-
-Each (sub)goal is denoted with a number. The current goal is numbered
-1. By default, a tactic is applied to the current goal, but one can
-address a particular goal in the list by writing {\sl n:\tac} which
-means {\it ``apply tactic {\tac} to goal number {\sl n}''}.
-We can show the list of subgoals by typing {\tt Show} (see
-Section~\ref{Show}). 
-
-Since not every rule applies to a given statement, every tactic cannot be
-used to reduce any goal. In other words, before applying a tactic to a
-given goal, the system checks that some {\em preconditions} are
-satisfied. If it is not the case, the tactic raises an error message.
-
-Tactics are build from atomic tactics and tactic expressions (which
-extends the folklore notion of tactical) to combine those atomic
-tactics. This chapter is devoted to atomic tactics. The tactic
-language will be described in chapter~\ref{TacticLanguage}.
-
-There are, at least, three levels of atomic tactics. The simplest one
-implements basic rules of the logical framework. The second level is
-the one of {\em derived rules} which are built by combination of other
-tactics. The third one implements heuristics or decision procedures to
-build a complete proof of a goal.
-
-\section{Invocation of tactics
-\label{tactic-syntax}
-\index{tactic@{\tac}}}
-
-A tactic is applied as an ordinary command. If the tactic does not
-address the first subgoal, the command may be preceded by the wished
-subgoal number as shown below:
-
-\begin{tabular}{lcl}
-{\commandtac} & ::= & {\num} {\tt :} {\tac} {\tt .}\\
- & $|$ & {\tac} {\tt .}
-\end{tabular}
-
-\section{Explicit proof as a term}
-
-\subsection{\tt exact \term
-\tacindex{exact}
-\label{exact}}
-
-This tactic applies to any goal. It gives directly the exact proof
-term of the goal. Let {\T} be our goal, let {\tt p} be a term of type
-{\tt U} then {\tt exact p} succeeds iff {\tt T} and {\tt U} are
-convertible (see Section~\ref{conv-rules}).
-
-\begin{ErrMsgs}
-\item \errindex{Not an exact proof}
-\end{ErrMsgs}
-
-\begin{Variants}
-  \item \texttt{eexact \term}\tacindex{eexact} 
-    
-    This tactic behaves like \texttt{exact} but is able to handle terms with meta-variables. 
-
-\end{Variants}
-
-
-\subsection{\tt refine \term
-\tacindex{refine}
-\label{refine}
-\index{?@{\texttt{?}}}}
-
-This tactic allows to give an exact proof but still with some
-holes. The holes are noted ``\texttt{\_}''.
-
-\begin{ErrMsgs}
-\item \errindex{invalid argument}: 
-  the tactic \texttt{refine} doesn't know what to do
-  with the term you gave.
-\item \texttt{Refine passed ill-formed term}: the term you gave is not
-  a valid proof (not easy to debug in general).
-  This message may also occur in higher-level tactics, which call 
-  \texttt{refine} internally.
-\item \errindex{Cannot infer a term for this placeholder}
-  there is a hole in the term you gave
-  which type cannot be inferred. Put a cast around it.
-\end{ErrMsgs}
-
-An example of use is given in section~\ref{refine-example}.
-
-\section{Basics
-\index{Typing rules}}
-
-Tactics presented in this section implement the basic typing rules of
-{\sc Cic} given in Chapter~\ref{Cic}.
-
-\subsection{{\tt assumption}
-\tacindex{assumption}}
-
-This tactic applies to any goal. It implements the
-``Var''\index{Typing rules!Var} rule given in
-Section~\ref{Typed-terms}. It looks in the local context for an
-hypothesis which type is equal to the goal.  If it is the case, the
-subgoal is proved. Otherwise, it fails.
-
-\begin{ErrMsgs}
-\item  \errindex{No such assumption}
-\end{ErrMsgs}
-
-\begin{Variants}
-\tacindex{eassumption}
-  \item \texttt{eassumption}
-
-    This tactic behaves like \texttt{assumption} but is able to handle
-    goals with meta-variables.
-
-\end{Variants}
-
-
-\subsection{\tt 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.
-
-\item \texttt{clear - {\ident}.} 
-
-  This tactic clears all hypotheses except the ones depending in {\ident}.
-
-\end{Variants}
-
-\begin{ErrMsgs}
-\item \errindex{{\ident} not found}
-\item \errindexbis{{\ident} is used in the conclusion}{is used in the
-    conclusion} 
-\item \errindexbis{{\ident} is used in the hypothesis {\ident'}}{is
-    used in the hypothesis} 
-\end{ErrMsgs}
-
-\subsection{\tt move {\ident$_1$} after {\ident$_2$}
-\tacindex{move}}
-
-This moves the hypothesis named {\ident$_1$} in the local context
-after the hypothesis named {\ident$_2$}.
-
-If {\ident$_1$} comes before {\ident$_2$} in the order of dependences,
-then all hypotheses between {\ident$_1$} and {\ident$_2$} which
-(possibly indirectly) depend on {\ident$_1$} are moved also.
-
-If {\ident$_1$} comes after {\ident$_2$} in the order of dependences,
-then all hypotheses between {\ident$_1$} and {\ident$_2$} which 
-(possibly indirectly) occur in {\ident$_1$} are moved also.
-
-\begin{ErrMsgs}
-
-\item \errindex{{\ident$_i$} not found}
-
-\item \errindex{Cannot move {\ident$_1$} after {\ident$_2$}:
-                   it occurs in {\ident$_2$}}
-
-\item \errindex{Cannot move {\ident$_1$} after {\ident$_2$}:
-                   it depends on {\ident$_2$}}
-
-\end{ErrMsgs}
-
-\subsection{\tt rename {\ident$_1$} into {\ident$_2$}
-\tacindex{rename}}
-
-This renames hypothesis {\ident$_1$} into {\ident$_2$} in the current
-context\footnote{but it does not rename the hypothesis in the
-  proof-term...}
-
-\begin{ErrMsgs}
-
-\item \errindex{{\ident$_2$} not found}
-
-\item \errindexbis{{\ident$_2$} is already used}{is already used}
-
-\end{ErrMsgs}
-
-\subsection{\tt intro
-\tacindex{intro}
-\label{intro}}
-
-This tactic applies to a goal which is either a product or starts with
-a let binder. If the goal is a product, the tactic implements the
-``Lam''\index{Typing rules!Lam} rule given in
-Section~\ref{Typed-terms}\footnote{Actually, only the second subgoal will be
-generated since the other one can be automatically checked.}.  If the
-goal starts with a let binder then the tactic implements a mix of the
-``Let''\index{Typing rules!Let} and ``Conv''\index{Typing rules!Conv}.
-
-If the current goal is a dependent product {\tt forall $x$:$T$, $U$} (resp {\tt
-let $x$:=$t$ in $U$}) then {\tt intro} puts {\tt $x$:$T$} (resp {\tt $x$:=$t$})
- in the local context.
-% Obsolete (quantified names already avoid hypotheses names):
-% Otherwise, it puts
-% {\tt x}{\it n}{\tt :T} where {\it n} is such that {\tt x}{\it n} is a
-%fresh name.
-The new subgoal is $U$.
-% If the {\tt x} has been renamed {\tt x}{\it n} then it is replaced 
-% by {\tt x}{\it n} in {\tt U}. 
-
-If the goal is a non dependent product {\tt $T$ -> $U$}, then it puts
-in the local context either {\tt H}{\it n}{\tt :$T$} (if $T$ is of
-type {\tt Set} or {\tt Prop}) or {\tt X}{\it n}{\tt :$T$} (if the type
-of $T$ is {\tt Type}). The optional index {\it n} is such that {\tt
-H}{\it n} or {\tt X}{\it n} is a fresh identifier.
-In both cases the new subgoal is $U$.
-
-If the goal is neither a product nor starting with a let definition,
-the tactic {\tt intro} applies the tactic {\tt red} until the tactic
-{\tt intro} can be applied or the goal is not reducible.
-
-\begin{ErrMsgs}
-\item \errindex{No product even after head-reduction}
-\item \errindexbis{{\ident} is already used}{is already used}
-\end{ErrMsgs}
-
-\begin{Variants}
-
-\item {\tt intros}\tacindex{intros}
-
-  Repeats {\tt intro} until it meets the head-constant. It never reduces
-  head-constants and it never fails.
-
-\item {\tt intro {\ident}}
-
-  Applies {\tt intro} but forces {\ident} to be the name of the
-  introduced hypothesis.
-
-  \ErrMsg \errindex{name {\ident} is already used}
-
-  \Rem If a name used by {\tt intro} hides the base name of a global
-  constant then the latter can still be referred to by a qualified name
-  (see \ref{LongNames}).
-
-\item {\tt intros \ident$_1$ \dots\ \ident$_n$} 
-  
-  Is equivalent to the composed tactic {\tt intro \ident$_1$; \dots\ ;
-    intro \ident$_n$}.
-
-  More generally, the \texttt{intros} tactic takes a pattern as
-  argument in order to introduce names for components of an inductive
-  definition or to clear introduced hypotheses; This is explained
-  in~\ref{intros-pattern}.
-
-\item {\tt intros until {\ident}} \tacindex{intros until}
-  
-  Repeats {\tt intro} until it meets a premise of the goal having form
-  {\tt (} {\ident}~{\tt :}~{\term} {\tt )} and discharges the variable
-  named {\ident} of the current goal.
-
-  \ErrMsg \errindex{No such hypothesis in current goal}
-  
-\item {\tt intros until {\num}}  \tacindex{intros until}
-  
-  Repeats {\tt intro} until the {\num}-th non-dependent premise. For
-  instance, on the subgoal %
-  \verb+forall x y:nat, x=y -> forall z:nat,z=x->z=y+ the
-  tactic \texttt{intros until 2} is equivalent to \texttt{intros x y H
-    z H0} (assuming \texttt{x, y, H, z} and \texttt{H0} do not already
-  occur in context).
-
-  \ErrMsg \errindex{No such hypothesis in current goal}
-
-  Happens when {\num} is 0 or is greater than the number of non-dependent
-  products of the goal.
-
-\item {\tt intro after \ident} \tacindex{intro after}
-
-  Applies {\tt intro} but puts the introduced
-  hypothesis after the hypothesis \ident{} in the hypotheses.
-
-\begin{ErrMsgs}
-\item \errindex{No product even after head-reduction}
-\item \errindex{No such hypothesis} : {\ident}
-\end{ErrMsgs}
-
-\item {\tt intro \ident$_1$ after \ident$_2$}
-  \tacindex{intro ... after}
-  
-  Behaves as previously but \ident$_1$ is the name of the introduced
-  hypothesis.  It is equivalent to {\tt intro \ident$_1$; move
-    \ident$_1$ after \ident$_2$}.
-
-\begin{ErrMsgs}
-\item \errindex{No product even after head-reduction}
-\item \errindex{No such hypothesis} : {\ident}
-\end{ErrMsgs}
-
-\end{Variants}
-
-\subsection{\tt apply \term
-\tacindex{apply}
-\label{apply}}
-
-This tactic applies to any goal.  The argument {\term} is a term
-well-formed in the local context.  The tactic {\tt apply} tries to
-match the current goal against the conclusion of the type of {\term}.
-If it succeeds, then the tactic returns as many subgoals as the number
-of non dependent premises of the type of {\term}.  The tactic {\tt
-apply} relies on first-order pattern-matching with dependent
-types. See {\tt pattern} in section \ref{pattern} to transform a
-second-order pattern-matching problem into a first-order one.
-
-\begin{ErrMsgs}
-\item \errindex{Impossible to unify \dots\ with \dots} 
-
-  The {\tt apply}
-  tactic failed to match the conclusion of {\term} and the current goal.
-  You can help the {\tt apply} tactic by transforming your
-  goal with the {\tt change} or {\tt pattern} tactics (see 
-  sections~\ref{pattern},~\ref{change}).
-
-\item \errindex{generated subgoal {\term'} has metavariables in it}
-
-  This occurs when some instantiations of premises of {\term} are not
-  deducible from the unification. This is the case, for instance, when
-  you want to apply a transitivity property. In this case, you have to
-  use one of the variants below:
-
-\end{ErrMsgs}
-
-\begin{Variants}
-
-\item{\tt apply {\term} with {\term$_1$} \dots\ {\term$_n$}} 
-  \tacindex{apply \dots\ with}
-  
-  Provides {\tt apply} with explicit instantiations for all dependent
-  premises of the type of {\term} which do not occur in the conclusion
-  and consequently cannot be found by unification. Notice that
-  {\term$_1$} \dots\ {\term$_n$} must be given according to the order
-  of these dependent premises of the type of {\term}.
-
-  \ErrMsg \errindex{Not the right number of missing arguments}
-
-\item{\tt apply {\term} with ({\vref$_1$} := {\term$_1$}) \dots\ ({\vref$_n$}
-    := {\term$_n$})} 
-  
-  This also provides {\tt apply} with values for instantiating
-  premises. But variables are referred by names and non dependent
-  products by order (see syntax in Section~\ref{Binding-list}).
-
-\item {\tt eapply \term}\tacindex{eapply}\label{eapply}
-  
-  The tactic {\tt eapply} behaves as {\tt apply} but does not fail
-  when no instantiation are deducible for some variables in the
-  premises.  Rather, it turns these variables into so-called
-  existential variables which are variables still to instantiate. An
-  existential variable is identified by a name of the form {\tt ?$n$}
-  where $n$ is a number.  The instantiation is intended to be found
-  later in the proof.
-
-  An example of use of {\tt eapply} is given in
-  Section~\ref{eapply-example}. 
-
-\item {\tt lapply {\term}} \tacindex{lapply} 
-
-  This tactic applies to any goal, say {\tt G}.  The argument {\term}
-  has to be well-formed in the current context, its type being
-  reducible to a non-dependent product {\tt A -> B} with {\tt B}
-  possibly containing products. Then it generates two subgoals {\tt
-  B->G} and {\tt A}. Applying {\tt lapply H} (where {\tt H} has type
-  {\tt A->B} and {\tt B} does not start with a product) does the same
-  as giving the sequence {\tt cut B. 2:apply H.} where {\tt cut} is
-  described below.
-
-  \Warning When {\term} contains more than one non
-  dependent product the tactic {\tt lapply} only takes into account the
-  first product.
-
-\end{Variants}
-
-\subsection{{\tt set ( {\ident} {\tt :=} {\term} \tt )}
-\label{tactic:set}
-\tacindex{set}
-\tacindex{pose}}
-
-This replaces {\term} by {\ident} in the conclusion or in the
-hypotheses of the current goal and adds the new definition {\ident
-{\tt :=} \term} to the local context. The default is to make this
-replacement only in the conclusion.
-
-\begin{Variants}
-
-\item {\tt set ( } {\ident} {\tt :=} {\term} {\tt ) in *}\\
-  {\tt set ( } {\ident} {\tt :=} {\term} {\tt ) in * |- *}\\
-  
-  This behaves as above but substitutes {\term}
-  everywhere in the goal (both in conclusion and hypotheses).
-
-\item {\tt set ( } {\ident} {\tt :=} {\term} {\tt ) in * |-}
-  
-  This behaves the same but substitutes {\term} in
-  the hypotheses only (not in the conclusion).
-
-\item {\tt set ( } {\ident} {\tt :=} {\term} {\tt ) in |- *}
-  
-  This is equivalent to {\tt set ( } {\ident} {\tt :=} {\term} {\tt
-  )}, i.e. it substitutes {\term} in the conclusion only.
-
-\item {\tt set ( {\ident$_0$} {\tt :=} {\term} {\tt ) in} {\ident$_1$}}
-  
-  This behaves the same but substitutes {\term} only in
-  the hypothesis named {\ident$_1$}.
-  
-\item {\tt set (} {\ident$_0$} {\tt :=} {\term} {\tt ) in}
-    {\ident$_1$} {\tt at} {\num$_1$} \dots\ {\num$_n$}
-
-This notation allows to specify which occurrences of {\term} have to
-be substituted in the hypothesis named {\ident$_1$}. The occurrences
-are numbered from left to right and are meaningful on a pure
-expression using no implicit argument, notation or coercion. A
-negative occurrence number means an occurrence which should not be
-substituted. As an exception of the left-to-right order, the
-occurrences in the {\tt return} subexpression of a {\tt match} are
-considered {\em before} the occurrences in the matched term.
-
-For expressions using notations, or hiding implicit arguments or
-coercions, it is recommended to make explicit all occurrences in 
-order by using {\tt Set Printing All} (see
-section~\ref{SetPrintingAll}).
-
-\item {\tt set ( } {\ident} {\tt :=} {\term} {\tt ) in |- * at}
-      {\num$_1$} \dots\ {\num$_n$}
-  
-This allows to specify which occurrences of the conclusion are concerned.
-
-\item {\tt set (} {\ident$_0$} {\tt :=} {\term} {\tt ) in}
-    {\ident$_1$} {\tt at} {\num$_1^1$} \dots\ {\num$_{n_1}^1$}, \dots
-    {\ident$_m$} {\tt at} {\num$_1^m$} \dots {\num$_{n_m}^m$}
-  
-  It substitutes {\term} at occurrences {\num$_1^i$} \dots\
-  {\num$_{n_i}^i$} of hypothesis {\ident$_i$}. Each {\tt at} part is
-  optional.
-
-\item {\tt set (} {\ident$_0$} {\tt :=} {\term} {\tt ) in}
-    {\ident$_1$} {\tt at} {\num$_1^1$} \dots\ {\num$_{n_1}^1$}, \dots
-    {\ident$_m$} {\tt at} {\num$_1^m$} \dots {\num$_{n_m}^m$}
-    {\tt |- *} {\tt at} {\num$'_1$} \dots\ {\num$'_n$}
-
-  This is the more general form which combines all the previous
-  possibilities.
-
-\item {\tt set } {\term}
-
-  This behaves as {\tt set (} {\ident} := {\term} {\tt )} but {\ident}
-    is generated by {\Coq}. This variant is available for the 
-    forms with {\tt in} too.
-
-\item {\tt pose (  {\ident} {\tt :=} {\term} {\tt )}}
-  
-  This adds the local definition {\ident} := {\term} to the current
-  context without performing any replacement in the goal or in the
-  hypotheses.
-
-\item{\tt pose {\term}}
-  
-  This behaves as {\tt pose (} {\ident} := {\term} {\tt )} but
-  {\ident} is generated by {\Coq}.
-
-\end{Variants}
-
-\subsection{{\tt assert ( {\ident} : {\form} \tt )}
-\tacindex{assert}}
-
-This tactic applies to any goal. {\tt assert (H : U)} adds a new
-hypothesis of name \texttt{H} asserting \texttt{U} to the current goal
-and opens a new subgoal \texttt{U}\footnote{This corresponds to the
-  cut rule of sequent calculus.}. The subgoal {\texttt U} comes first
-in the list of subgoals remaining to prove.
-
-\begin{ErrMsgs}
-\item \errindex{Not a proposition or a type}
-  
-  Arises when the argument {\form} is neither of type {\tt Prop}, {\tt
-    Set} nor {\tt Type}.
-
-\end{ErrMsgs}
-
-\begin{Variants}
-
-\item{\tt assert {\form}}
-  
-  This behaves as {\tt assert (} {\ident} : {\form} {\tt )} but
-  {\ident} is generated by {\Coq}.
-
-\item{\tt assert (} {\ident} := {\term} {\tt )}
-  
-  This behaves as {\tt assert ({\ident} : {\type});[exact
-    {\term}|idtac]} where {\type} is the type of {\term}.
-
-\item {\tt cut {\form}}\tacindex{cut} 
-  
-  This tactic applies to any goal. It implements the non dependent
-  case of the ``App''\index{Typing rules!App} rule given in
-  Section~\ref{Typed-terms}. (This is Modus Ponens inference rule.)
-  {\tt cut U} transforms the current goal \texttt{T} into the two
-  following subgoals: {\tt U -> T} and \texttt{U}.  The subgoal {\tt U
-    -> T} comes first in the list of remaining subgoal to prove.
-
-\item \texttt{assert {\form} by {\tac}}\tacindex{assert by}
-  
-  This tactic behaves like \texttt{assert} but tries to apply {\tac}
-  to any subgoals generated by \texttt{assert}.
-
-\item \texttt{assert {\form} as {\ident}\tacindex{assert as}}
-
-   This tactic behaves like \texttt{assert ({\ident} : {\form})}.
-
-\item \texttt{pose proof {\term} as {\ident}}
-
-  This tactic behaves like \texttt{assert ({\ident:T} by exact {\term}} where
-  \texttt{T} is the type of {\term}. 
-
-\end{Variants}
-
-% PAS CLAIR;
-% 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 apply {\term} in {\ident}}
-\tacindex{apply {\ldots} in}}
-
-This tactic applies to any goal.  The argument {\term} is a term
-well-formed in the local context and the argument {\ident} is an
-hypothesis of the context.  The tactic {\tt apply {\term} in {\ident}}
-tries to match the conclusion of the type of {\ident} against a non
-dependent premisses of the type of {\term}, trying them from right to
-left.  If it succeeds, the statement of hypothesis {\ident} is
-replaced by the conclusion of the type of {\ident}. The tactic also
-returns as many subgoals as the number of other non dependent premises
-in the type of {\term} and of the non dependent premises of the type
-of {\ident}.  The tactic {\tt apply} relies on first-order
-pattern-matching with dependent types.
-
-\begin{ErrMsgs}
-\item \errindex{Statement without assumptions}
-
-This happens if the type of {\term} has no non dependent premise.
-
-\item \errindex{Unable to apply}
-
-This happens if the conclusion of {\ident} does not match any of the
-non dependent premises of the type of {\term}.
-\end{ErrMsgs}
-
-\begin{Variants}
-\item {\tt apply \nelist{\term}{,} in {\ident}}
-
-This applies each of {\term} in sequence in {\ident}.
-
-\item {\tt apply \nelist{{\term} {\bindinglist}}{,} in {\ident}}
-
-This does the same but uses the bindings in each {\bindinglist} to 
-instanciate the parameters of the corresponding type of {\term}
-(see syntax of bindings in Section~\ref{Binding-list}).
-
-\end{Variants}
-
-\subsection{\tt generalize \term
-\tacindex{generalize}
-\label{generalize}}
-
-This tactic applies to any goal. It generalizes the conclusion w.r.t.
-one subterm of it. For example:
-
-\begin{coq_eval}
-Goal forall x y:nat, (0 <= x + y + y).
-intros.
-\end{coq_eval}
-\begin{coq_example}
-Show.
-generalize (x + y + y).
-\end{coq_example}
-
-\begin{coq_eval}
-Abort.
-\end{coq_eval}
-
-If the goal is $G$ and $t$ is a subterm of type $T$ in the goal, then
-{\tt generalize} \textit{t} replaces the goal by {\tt forall (x:$T$), $G'$}
-where $G'$ is obtained from $G$ by replacing all occurrences of $t$ by
-{\tt x}. The name of the variable (here {\tt n}) is chosen accordingly
-to $T$.
-
-\begin{Variants}
-\item {\tt generalize \term$_1$ \dots\ \term$_n$} 
-  
-  Is equivalent to {\tt generalize \term$_n$; \dots\ ; generalize
-    \term$_1$}. Note that the sequence of \term$_i$'s are processed
-  from $n$ to $1$.
-  
-\item {\tt generalize dependent \term} \tacindex{generalize dependent}
-  
-  This generalizes {\term} but also {\em all} hypotheses which depend
-  on {\term}. It clears the generalized hypotheses.
-
-\end{Variants}
-
-\subsection{\tt change \term
-\tacindex{change}
-\label{change}}
-
-This tactic applies to any goal. It implements the rule
-``Conv''\index{Typing rules!Conv} given in section~\ref{Conv}.  {\tt
-  change U} replaces the current goal \T\ with \U\ providing that
-\U\ is well-formed and that \T\ and \U\ are convertible.
-
-\begin{ErrMsgs}
-\item \errindex{Not convertible}
-\end{ErrMsgs}
-
-\tacindex{change \dots\ in}
-\begin{Variants}
-\item {\tt change \term$_1$ with \term$_2$} 
-  
-  This replaces the occurrences of \term$_1$ by \term$_2$ in the
-  current goal.  The terms \term$_1$ and \term$_2$ must be
-  convertible.
-
-\item {\tt change \term$_1$ at \num$_1$ \dots\ \num$_i$ with \term$_2$} 
-  
-  This replaces the occurrences numbered \num$_1$ \dots\ \num$_i$ of
-  \term$_1$ by \term$_2$ in the current goal.
-  The terms \term$_1$ and \term$_2$ must be convertible.
-
-  \ErrMsg {\tt Too few occurrences}
-
-\item {\tt change {\term} in {\ident}}
-
-\item {\tt change \term$_1$ with \term$_2$ in {\ident}}
-  
-\item {\tt change \term$_1$ at  \num$_1$ \dots\ \num$_i$ with \term$_2$ in
-    {\ident}}
-  
-  This applies the {\tt change} tactic not to the goal but to the
-  hypothesis {\ident}.
-
-\end{Variants}
-
-\SeeAlso \ref{Conversion-tactics}
-
-\subsection{Bindings list
-\index{Binding list}
-\label{Binding-list}}
-
-A bindings list is generally used after the keyword {\tt with} in
-tactics.  The general shape of a bindings list is {\tt (\vref$_1$ :=
-  \term$_1$) \dots\ (\vref$_n$ := \term$_n$)} where {\vref} is either an
-{\ident} or a {\num}. It is used to provide a tactic with a list of
-values (\term$_1$, \dots, \term$_n$) that have to be substituted
-respectively to \vref$_1$, \dots, \vref$_n$. For all $i \in [1\dots\ 
-n]$, if \vref$_i$ is \ident$_i$ then it references the dependent
-product {\tt \ident$_i$:T} (for some type \T); if \vref$_i$ is
-\num$_i$ then it references the \num$_i$-th non dependent premise.
-
-A bindings list can also be a simple list of terms {\tt \term$_1$
-  \term$_2$ \dots\term$_n$}. In that case the references to which
-these terms correspond are determined by the tactic. In case of {\tt
-  elim} (see section~\ref{elim}) the terms should correspond to
-all the dependent products in the type of \term\ while in the case of
-{\tt apply} only the dependent products which are not bound in
-the conclusion of the type are given.
-
-
-\section{Negation and contradiction}
-
-\subsection{\tt absurd \term
-\tacindex{absurd}
-\label{absurd}}
-
-This tactic applies to any goal. The argument {\term} is any
-proposition {\tt P} of type {\tt Prop}. This tactic applies {\tt
-  False} elimination, that is it deduces the current goal from {\tt
-  False}, and generates as subgoals {\tt $\sim$P} and {\tt P}. It is
-very useful in proofs by cases, where some cases are impossible. In
-most cases, \texttt{P} or $\sim$\texttt{P} is one of the hypotheses of
-the local context.
-
-\subsection{\tt contradiction
-\label{contradiction}
-\tacindex{contradiction}}
-
-This tactic applies to any goal. The {\tt contradiction} tactic
-attempts to find in the current context (after all {\tt intros}) one
-which is equivalent to {\tt False}. It permits to prune irrelevant
-cases.  This tactic is a macro for the tactics sequence {\tt intros;
-  elimtype False; assumption}.
-
-\begin{ErrMsgs}
-\item \errindex{No such assumption}
-\end{ErrMsgs}
-
-
-\section{Conversion tactics
-\index{Conversion tactics}
-\label{Conversion-tactics}}
-
-This set of tactics implements different specialized usages of the
-tactic \texttt{change}.
-
-All conversion tactics (including \texttt{change}) can be
-parameterized by the parts of the goal where the conversion can
-occur. The specification of such parts are called \emph{clauses}. It
-can be either the conclusion, or an hypothesis. In the case of a
-defined hypothesis it is possible to specify if the conversion should
-occur on the type part, the body part or both (default).
-
-\index{Clauses} Clauses are written after a conversion tactic (tactics
-\texttt{set}~\ref{tactic:set},          \texttt{rewrite}~\ref{rewrite},
-\texttt{replace}~\ref{tactic:replace}                               and
-\texttt{autorewrite}~\ref{tactic:autorewrite}  also  use clauses)  and
-are introduced by  the keyword \texttt{in}. If no  clause is provided,
-the default is to perform the conversion only in the conclusion.
-
-The syntax and description of the various clauses follows:
-\begin{description}
-\item[\texttt{in H$_1$ $\ldots$ H$_n$ |- }] only in hypotheses $H_1
-  $\ldots$ H_n$
-\item[\texttt{in H$_1$ $\ldots$ H$_n$ |- *}] in hypotheses $H_1 \ldots
-  H_n$ and in the conclusion
-\item[\texttt{in * |-}] in every hypothesis
-\item[\texttt{in *}] (equivalent to \texttt{in * |- *}) everywhere
-\item[\texttt{in (type of H$_1$) (value of H$_2$) $\ldots$ |-}] in
-  type part of $H_1$, in the value part of $H_2$, etc. 
-\end{description}
-
-For backward compatibility, the notation \texttt{in}~$H_1\ldots H_n$
-performs the conversion in hypotheses $H_1\ldots H_n$.
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%voir reduction__conv_x : histoires d'univers.
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-\subsection{{\tt cbv \flag$_1$ \dots\ \flag$_n$}, {\tt lazy \flag$_1$
-\dots\ \flag$_n$} and {\tt compute}
-\tacindex{cbv}
-\tacindex{lazy}
-\tacindex{compute}
-\tacindex{vm\_compute}}
-\label{vmcompute}
-
-These parameterized reduction tactics apply to any goal and perform
-the normalization of the goal according to the specified flags. Since
-the reduction considered in \Coq\ include $\beta$ (reduction of
-functional application), $\delta$ (unfolding of transparent constants,
-see \ref{Transparent}), $\iota$ (reduction of {\tt Cases}, {\tt Fix}
-and {\tt CoFix} expressions) and $\zeta$ (removal of local
-definitions), every flag is one of {\tt beta}, {\tt delta}, {\tt
-  iota}, {\tt zeta}, {\tt [\qualid$_1$\ldots\qualid$_k$]} and {\tt
-  -[\qualid$_1$\ldots\qualid$_k$]}.  The last two flags give the list
-of constants to unfold, or the list of constants not to unfold. These
-two flags can occur only after the {\tt delta} flag. 
-If alone (i.e. not
-followed by {\tt [\qualid$_1$\ldots\qualid$_k$]} or {\tt
-  -[\qualid$_1$\ldots\qualid$_k$]}), the {\tt delta} flag means that all constants must be unfolded.
-However, the {\tt delta} flag does not apply to variables bound by a
-let-in construction whose unfolding is controlled by the {\tt
-  zeta} flag only.
-
-The goal may be normalized with two strategies: {\em lazy} ({\tt lazy}
-tactic), or {\em call-by-value} ({\tt cbv} tactic). The lazy strategy
-is a call-by-need strategy, with sharing of reductions: the arguments of a
-function call are partially evaluated only when necessary, but if an
-argument is used several times, it is computed only once. This
-reduction is efficient for reducing expressions with dead code. For
-instance, the proofs of a proposition $\exists_T ~x. P(x)$ reduce to a
-pair of a witness $t$, and a proof that $t$ verifies the predicate
-$P$. Most of the time, $t$ may be computed without computing the proof
-of $P(t)$, thanks to the lazy strategy.
-
-The call-by-value strategy is the one used in ML languages: the
-arguments of a function call are evaluated first, using a weak
-reduction (no reduction under the $\lambda$-abstractions). Despite the
-lazy strategy always performs fewer reductions than the call-by-value
-strategy, the latter should be preferred for evaluating purely
-computational expressions (i.e. with few dead code).
-
-\begin{Variants}
-\item {\tt compute} \tacindex{compute} 
-  
-  This tactic is an alias for {\tt cbv beta delta iota zeta}.
-
-\item {\tt vm\_compute} \tacindex{vm\_compute}
-
-  This tactic evaluates the goal using the optimized call-by-value
-  evaluation bytecode-based virtual machine. This algorithm is
-  dramatically more efficient than the algorithm used for the {\tt
-  cbv} tactic, but it cannot be fine-tuned. It is specially
-  interesting for full evaluation of algebraic objects. This includes
-  the case of reflexion-based tactics.
-
-\end{Variants}
-
-\begin{ErrMsgs}
-\item \errindex{Delta must be specified before}
-  
-  A list of constants appeared before the {\tt delta} flag.
-\end{ErrMsgs}
-
-
-\subsection{{\tt red}
-\tacindex{red}}
-
-This tactic applies to a goal which has the form {\tt
-  forall (x:T1)\dots(xk:Tk), c t1 \dots\ tn} where {\tt c} is a constant.  If
-{\tt c} is transparent then it replaces {\tt c} with its definition
-(say {\tt t}) and then reduces {\tt (t t1 \dots\ tn)} according to
-$\beta\iota\zeta$-reduction rules.
-
-\begin{ErrMsgs}
-\item \errindex{Not reducible}
-\end{ErrMsgs}
-
-\subsection{{\tt hnf}
-\tacindex{hnf}}
-
-This tactic applies to any goal. It replaces the current goal with its
-head normal form according to the $\beta\delta\iota\zeta$-reduction rules.
-{\tt hnf} does not produce a real head normal form but either a
-product or an applicative term in head normal form or a variable.
-
-\Example
-The term \verb+forall n:nat, (plus (S n) (S n))+ is not reduced by {\tt hnf}.
-
-\Rem The $\delta$ rule only applies to transparent constants
-(see section~\ref{Opaque} on transparency and opacity).
-
-\subsection{\tt simpl
-\tacindex{simpl}}
-
-This tactic applies to any goal. The tactic {\tt simpl} first applies
-$\beta\iota$-reduction rule.  Then it expands transparent constants
-and tries to reduce {\tt T'} according, once more, to $\beta\iota$
-rules. But when the $\iota$ rule is not applicable then possible
-$\delta$-reductions are not applied.  For instance trying to use {\tt
-  simpl} on {\tt (plus n O)=n} does change nothing.
-
-\tacindex{simpl \dots\ in}
-\begin{Variants}
-\item {\tt simpl {\term}}
-  
-  This applies {\tt simpl} only to the occurrences of {\term} in the
-  current goal.
-
-\item {\tt simpl {\term} at \num$_1$ \dots\ \num$_i$}
-  
-  This applies {\tt simpl} only to the \num$_1$, \dots, \num$_i$
-  occurrences of {\term} in the current goal.
-
-  \ErrMsg {\tt Too few occurrences}
-
-\item {\tt simpl {\ident}}
-  
-  This applies {\tt simpl} only to the applicative subterms whose head
-  occurrence is {\ident}.
-
-\item {\tt simpl {\ident} at \num$_1$ \dots\ \num$_i$}
-  
-  This applies {\tt simpl} only to the \num$_1$, \dots, \num$_i$
-applicative subterms whose head occurrence is {\ident}.
-
-\end{Variants}
-
-\subsection{\tt unfold \qualid
-\tacindex{unfold}
-\label{unfold}}
-
-This tactic applies to any goal. The argument {\qualid} must denote a
-defined transparent constant or local definition (see Sections~\ref{Simpl-definitions} and~\ref{Transparent}).  The tactic {\tt
-  unfold} applies the $\delta$ rule to each occurrence of the constant
-to which {\qualid} refers in the current goal and then replaces it
-with its $\beta\iota$-normal form.
-
-\begin{ErrMsgs}
-\item {\qualid} \errindex{does not denote an evaluable constant}
-
-\end{ErrMsgs}
-
-\begin{Variants}
-\item {\tt unfold {\qualid}$_1$, \dots, \qualid$_n$}
-  \tacindex{unfold \dots\ in}
-  
-  Replaces {\em simultaneously} {\qualid}$_1$, \dots, {\qualid}$_n$
-  with their definitions and replaces the current goal with its
-  $\beta\iota$ normal form.
-
-\item {\tt unfold {\qualid}$_1$ at \num$_1^1$, \dots, \num$_i^1$,
-\dots,\ \qualid$_n$ at \num$_1^n$ \dots\ \num$_j^n$}
-  
-  The lists \num$_1^1$, \dots, \num$_i^1$ and \num$_1^n$, \dots,
-  \num$_j^n$ specify the occurrences of {\qualid}$_1$, \dots,
-  \qualid$_n$ to be unfolded. Occurrences are located from left to
-  right.
-
-  \ErrMsg {\tt bad occurrence number of {\qualid}$_i$}
-
-  \ErrMsg {\qualid}$_i$ {\tt does not occur}
-
-\end{Variants}
-
-\subsection{{\tt fold} \term
-\tacindex{fold}}
-
-This tactic applies to any goal. The term \term\ is reduced using the {\tt red}
-tactic. Every occurrence of the resulting term in the goal is then
-substituted for \term.
-
-\begin{Variants}
-\item {\tt fold} \term$_1$ \dots\ \term$_n$ 
-  
-  Equivalent to {\tt fold} \term$_1${\tt;}\ldots{\tt; fold} \term$_n$.
-\end{Variants}
-
-\subsection{{\tt pattern {\term}}
-\tacindex{pattern}
-\label{pattern}}
-
-This command applies to any goal. The argument {\term} must be a free
-subterm of the current goal.  The command {\tt pattern} performs
-$\beta$-expansion (the inverse of $\bt$-reduction) of the current goal
-(say \T) by
-\begin{enumerate}
-\item replacing all occurrences of {\term} in {\T} with a fresh variable
-\item abstracting this variable
-\item applying the abstracted goal to {\term}
-\end{enumerate}
-
-For instance, if the current goal $T$ is expressible has $\phi(t)$
-where the notation captures all the instances of $t$ in $\phi(t)$,
-then {\tt pattern $t$} transforms it into {\tt (fun x:$A$ => $\phi(${\tt
-x}$)$) $t$}.  This command can be used, for instance, when the tactic
-{\tt apply} fails on matching.
-
-\begin{Variants}
-\item {\tt pattern {\term} at {\num$_1$} \dots\ {\num$_n$}}
-  
-  Only the occurrences {\num$_1$} \dots\ {\num$_n$} of {\term} will be
-  considered for $\beta$-expansion. Occurrences are located from left
-  to right.
-
-\item {\tt pattern {\term$_1$}, \dots, {\term$_m$}}
-  
-  Starting from a goal $\phi(t_1 \dots\ t_m)$, the tactic
-   {\tt pattern $t_1$, \dots,\ $t_m$} generates the equivalent goal {\tt
-   (fun (x$_1$:$A_1$) \dots\ (x$_m$:$A_m$) => $\phi(${\tt x$_1$\dots\
-   x$_m$}$)$) $t_1$ \dots\ $t_m$}.\\ If $t_i$ occurs in one of the
-   generated types $A_j$ these occurrences will also be considered and
-   possibly abstracted.
-
-\item {\tt pattern {\term$_1$} at {\num$_1^1$} \dots\ {\num$_{n_1}^1$}, \dots,
-    {\term$_m$} at {\num$_1^m$} \dots\ {\num$_{n_m}^m$}}
-  
-  This behaves as above but processing only the occurrences \num$_1^1$,
-  \dots, \num$_i^1$ of \term$_1$, \dots, \num$_1^m$, \dots, \num$_j^m$
-  of \term$_m$ starting from \term$_m$.
-
-\end{Variants}
-
-\subsection{Conversion tactics applied to hypotheses}
-
-{\convtactic} {\tt in} \ident$_1$ \dots\ \ident$_n$ 
-
-Applies the conversion tactic {\convtactic} to the
-hypotheses \ident$_1$, \ldots, \ident$_n$. The tactic {\convtactic} is
-any of the conversion tactics listed in this section. 
-
-If \ident$_i$ is a local definition, then \ident$_i$ can be replaced
-by (Type of \ident$_i$) to address not the body but the type of the
-local definition. Example: {\tt unfold not in (Type of H1) (Type of H3).}
-
-\begin{ErrMsgs}
-\item \errindex{No such hypothesis} : {\ident}.
-\end{ErrMsgs}
-
-
-\section{Introductions}
-
-Introduction tactics address goals which are inductive constants.
-They are used when one guesses that the goal can be obtained with one
-of its constructors' type.
-
-\subsection{\tt constructor \num
-\label{constructor}
-\tacindex{constructor}}
-
-This tactic applies to a goal such that the head of its conclusion is
-an inductive constant (say {\tt I}).  The argument {\num} must be less
-or equal to the numbers of constructor(s) of {\tt I}. Let {\tt ci} be
-the {\tt i}-th constructor of {\tt I}, then {\tt constructor i} is
-equivalent to {\tt intros; apply ci}.
-
-\begin{ErrMsgs}
-\item \errindex{Not an inductive product}
-\item \errindex{Not enough constructors}
-\end{ErrMsgs}
-
-\begin{Variants}
-\item \texttt{constructor} 
-  
-  This tries \texttt{constructor 1} then \texttt{constructor 2},
-  \dots\ , then \texttt{constructor} \textit{n} where \textit{n} if
-  the number of constructors of the head of the goal.
-
-\item {\tt constructor \num~with} {\bindinglist}
-  \tacindex{constructor \dots\  with}
-  
-  Let {\tt ci} be the {\tt i}-th constructor of {\tt I}, then {\tt
-    constructor i with \bindinglist} is equivalent to {\tt intros;
-    apply ci with \bindinglist}.
-
-  \Warning the terms in the \bindinglist\ are checked
-  in the context where {\tt constructor} is executed and not in the
-  context where {\tt apply} is executed (the introductions are not
-  taken into account).
-
-\item {\tt split}\tacindex{split}
-
-  Applies if {\tt I} has only one constructor, typically in the case
-  of conjunction $A\land B$. Then, it is equivalent to {\tt constructor 1}.
-
-\item {\tt exists {\bindinglist}}\tacindex{exists} 
-
-  Applies if {\tt I} has only one constructor, for instance in the
-  case of existential quantification $\exists x\cdot P(x)$. 
-  Then, it is equivalent to {\tt intros; constructor 1 with \bindinglist}.
-
-\item {\tt left}\tacindex{left},  {\tt right}\tacindex{right}
-
-  Apply if {\tt I} has two constructors, for instance in the case of
-  disjunction $A\lor B$. Then, they are respectively equivalent to {\tt
-    constructor 1} and {\tt constructor 2}.
-  
-\item {\tt left \bindinglist}, {\tt right \bindinglist}, {\tt split
-    \bindinglist}
-  
-  As soon as the inductive type has the right number of constructors,
-    these expressions are equivalent to the corresponding {\tt
-    constructor $i$ with \bindinglist}.
-
-\item \texttt{econstructor}
-
-  This tactic behaves like \texttt{constructor} but is able to
-  introduce existential variables if an instanciation for a variable
-  cannot be found (cf \texttt{eapply}). The tactics \texttt{eexists},
-  \texttt{esplit}, \texttt{eleft} and \texttt{eright} follows the same
-  behaviour.
-
-\end{Variants}
-
-\section{Eliminations (Induction and Case Analysis)}
-\label{Tac-induction}
-Elimination tactics are useful to prove statements by induction or
-case analysis.  Indeed, they make use of the elimination (or
-induction) principles generated with inductive definitions (see
-Section~\ref{Cic-inductive-definitions}).
-
-\subsection{\tt induction \term
-\tacindex{induction}}
-
-This tactic applies to any goal. The type of the argument {\term} must
-be an inductive constant. Then, the tactic {\tt induction}
-generates subgoals, one for each possible form of {\term}, i.e. one
-for each constructor of the inductive type.
-
-The tactic {\tt induction} automatically replaces every occurrences
-of {\term} in the conclusion and the hypotheses of the goal.  It
-automatically adds induction hypotheses (using names of the form {\tt
-  IHn1}) to the local context. If some hypothesis must not be taken
-into account in the induction hypothesis, then it needs to be removed
-first (you can also use the tactics {\tt elim} or {\tt simple induction},
-see below).
-
-There are particular cases:
-
-\begin{itemize}
-
-\item If {\term} is an identifier {\ident} denoting a quantified
-variable of the conclusion of the goal, then {\tt induction {\ident}}
-behaves as {\tt intros until {\ident}; induction {\ident}}
-
-\item If {\term} is a {\num}, then {\tt induction {\num}} behaves as
-{\tt intros until {\num}} followed by {\tt induction} applied to the
-last introduced hypothesis.
-
-\Rem For simple induction on a numeral, use syntax {\tt induction
-({\num})} (not very interesting anyway).
-
-\end{itemize}
-
-\Example
-
-\begin{coq_example}
-Lemma induction_test : forall n:nat, n = n -> n <= n.
-intros n H.
-induction n.
-\end{coq_example}
-
-\begin{ErrMsgs}
-\item \errindex{Not an inductive product}
-\item \errindex{Cannot refine to conclusions with meta-variables}
-  
-  As {\tt induction} uses {\tt apply}, see Section~\ref{apply} and
-  the variant {\tt elim \dots\ with \dots} below.
-\end{ErrMsgs}
-
-\begin{Variants}
-\item{\tt induction {\term} as {\intropattern}}
-  
-  This behaves as {\tt induction {\term}} but uses the names in
-  {\intropattern} to names the variables introduced in the context.
-  The {\intropattern} must have the form {\tt [} $p_{11}$ \ldots
-  $p_{1n_1}$ {\tt |} {\ldots} {\tt |} $p_{m1}$ \ldots $p_{mn_m}$ {\tt
-    ]} with $m$ being the number of constructors of the type of
-  {\term}. Each variable introduced by {\tt induction} in the context
-  of the $i^{th}$ goal gets its name from the list $p_{i1}$ \ldots
-  $p_{in_i}$ in order. If there are not enough names, {\tt induction}
-  invents names for the remaining variables to introduce. More
-  generally, the $p$'s can be any introduction patterns (see
-  Section~\ref{intros-pattern}). This provides a concise notation for
-  nested induction.
-
-\Rem for an inductive type with one constructor, the pattern notation
-{\tt ($p_{1}$,\ldots,$p_{n}$)} can be used instead of
-{\tt [} $p_{1}$ \ldots $p_{n}$ {\tt ]}.
-
-\item {\tt induction {\term} using {\qualid}}
-
-  This behaves as {\tt induction {\term}} but using the induction
-scheme of name {\qualid}. It does not expect that the type of
-{\term} is inductive.
-
-\item \texttt{induction {\term}$_1$ $\ldots$ {\term}$_n$ using {\qualid}}
-
-  where {\qualid} is an induction principle with complex predicates
-  (like the ones generated by function induction).
-
-\item {\tt induction {\term} using {\qualid} as {\intropattern}}
-
-  This combines {\tt induction {\term} using {\qualid}}
-and {\tt induction {\term} as {\intropattern}}.
-
-\item {\tt elim \term}\label{elim}
-  
-  This is a more basic induction tactic.  Again, the type of the
-  argument {\term} must be an inductive constant. Then according to
-  the type of the goal, the tactic {\tt elim} chooses the right
-  destructor and applies it (as in the case of the {\tt apply}
-  tactic). For instance, assume that our proof context contains {\tt
-    n:nat}, assume that our current goal is {\tt T} of type {\tt
-    Prop}, then {\tt elim n} is equivalent to {\tt apply nat\_ind with
-    (n:=n)}.  The tactic {\tt elim} does not affect the hypotheses of
-  the goal, neither introduces the induction loading into the context
-  of hypotheses.
-
-\item {\tt elim \term} 
-  
-  also works when the type of {\term} starts with products and the
-  head symbol is an inductive definition. In that case the tactic
-  tries both to find an object in the inductive definition and to use
-  this inductive definition for elimination.  In case of non-dependent
-  products in the type, subgoals are generated corresponding to the
-  hypotheses. In the case of dependent products, the tactic will try
-  to find an instance for which the elimination lemma applies.
-
-\item {\tt elim {\term} with \term$_1$ \dots\ \term$_n$}
-  \tacindex{elim \dots\ with} \
-  
-  Allows the user to give explicitly the values for dependent
-  premises of the elimination schema. All arguments must be given.
-
-  \ErrMsg \errindex{Not the right number of dependent arguments}
-
-\item{\tt elim {\term} with {\vref$_1$} := {\term$_1$} \dots\ {\vref$_n$}
-    := {\term$_n$}} 
-  
-  Provides also {\tt elim} with values for instantiating premises by
-  associating explicitly variables (or non dependent products) with
-  their intended instance.
-
-\item{\tt elim {\term$_1$} using {\term$_2$}}
-\tacindex{elim \dots\ using} 
-
-Allows the user to give explicitly an elimination predicate
-{\term$_2$} which is not the standard one for the underlying inductive
-type of {\term$_1$}. Each of the {\term$_1$} and {\term$_2$} is either
-a simple term or a term with a bindings list (see \ref{Binding-list}).
-
-\item {\tt elimtype \form}\tacindex{elimtype}
-  
-  The argument {\form} must be inductively defined. {\tt elimtype I}
-  is equivalent to {\tt cut I. intro H{\rm\sl n}; elim H{\rm\sl n};
-    clear H{\rm\sl n}}. Therefore the hypothesis {\tt H{\rm\sl n}} will
-  not appear in the context(s) of the subgoal(s).  Conversely, if {\tt
-    t} is a term of (inductive) type {\tt I} and which does not occur
-  in the goal then {\tt elim t} is equivalent to {\tt elimtype I; 2:
-    exact t.}
-
-  \ErrMsg \errindex{Impossible to unify \dots\ with \dots} 
-  
-  Arises when {\form} needs to be applied to parameters.
-
-\item {\tt simple induction \ident}\tacindex{simple induction}
-  
-  This tactic behaves as {\tt intros until
-    {\ident}; elim {\tt {\ident}}} when {\ident} is a quantified
-  variable of the goal.
-
-\item {\tt simple induction {\num}}
-  
-  This tactic behaves as {\tt intros until
-    {\num}; elim {\tt {\ident}}} where {\ident} is the name given by
-  {\tt intros until {\num}} to the {\num}-th non-dependent premise of
-  the goal.
-
-%% \item {\tt simple induction {\term}}\tacindex{simple induction}
-  
-%%   If {\term} is an {\ident} corresponding to a quantified variable of
-%%   the goal then the tactic behaves as {\tt intros until {\ident}; elim
-%%   {\tt {\ident}}}.  If {\term} is a {\num} then the tactic behaves as
-%%   {\tt intros until {\ident}; elim {\tt {\ident}}}.  Otherwise, it is
-%%   a synonym for {\tt elim {\term}}.
-
-%%   \Rem For simple induction on a numeral, use syntax {\tt simple
-%%   induction ({\num})}.
-
-\end{Variants}
-
-\subsection{\tt destruct \term
-\tacindex{destruct}}
-
-The tactic {\tt destruct} is used to perform case analysis without
-recursion. Its behavior is similar to {\tt induction} except
-that no induction hypothesis is generated.  It applies to any goal and
-the type of {\term} must be inductively defined. There are particular cases:
-
-\begin{itemize}
-
-\item If {\term} is an identifier {\ident} denoting a quantified
-variable of the conclusion of the goal, then {\tt destruct {\ident}}
-behaves as {\tt intros until {\ident}; destruct {\ident}}
-
-\item If {\term} is a {\num}, then {\tt destruct {\num}} behaves as
-{\tt intros until {\num}} followed by {\tt destruct} applied to the
-last introduced hypothesis.
-
-\Rem For destruction of a numeral, use syntax {\tt destruct
-({\num})} (not very interesting anyway).
-
-\end{itemize}
-
-\begin{Variants}
-\item{\tt destruct {\term} as {\intropattern}}
-  
-  This behaves as {\tt destruct {\term}} but uses the names in
-  {\intropattern} to names the variables introduced in the context.
-  The {\intropattern} must have the form {\tt [} $p_{11}$ \ldots
-  $p_{1n_1}$ {\tt |} {\ldots} {\tt |} $p_{m1}$ \ldots $p_{mn_m}$ {\tt
-    ]} with $m$ being the number of constructors of the type of
-  {\term}. Each variable introduced by {\tt destruct} in the context
-  of the $i^{th}$ goal gets its name from the list $p_{i1}$ \ldots
-  $p_{in_i}$ in order. If there are not enough names, {\tt destruct}
-  invents names for the remaining variables to introduce. More
-  generally, the $p$'s can be any introduction patterns (see
-  Section~\ref{intros-pattern}). This provides a concise notation for
-  nested destruction.
-
-%  It is recommended to use this variant of {\tt destruct} for 
-%  robust proof scripts.
-
-\Rem for an inductive type with one constructor, the pattern notation
-{\tt ($p_{1}$,\ldots,$p_{n}$)} can be used instead of
-{\tt [} $p_{1} $\ldots $p_{n}$ {\tt ]}.
-
-\item \texttt{pose proof {\term} as {\intropattern}}
-
-  This tactic behaves like \texttt{destruct {\term} as {\intropattern}}.
-
-\item{\tt destruct {\term} using {\qualid}}
-
-  This is a synonym of {\tt induction {\term} using {\qualid}}.
-
-\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 the pattern \texttt{?}
-\item a variable
-\item a disjunction of lists of patterns:
-  {\tt [$p_{11}$ {\ldots} $p_{1m_1}$ | {\ldots} | $p_{11}$ {\ldots} $p_{nm_n}$]}
-\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 \texttt{?} do the introduction, and let Coq
-  choose a fresh name for the variable;
-\item introduction on a variable behaves like described in~\ref{intro}; 
-\item introduction over a
-list of patterns $p_1~\ldots~p_n$ is equivalent to the sequence of
-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).
-exact c.
-Qed.
-\end{coq_example}
-
-%\subsection{\tt FixPoint \dots}\tacindex{Fixpoint}
-%Not yet documented.
-
-\subsection {\tt double induction \ident$_1$ \ident$_2$
-\tacindex{double induction}}
-
-This tactic applies to any goal. If the variables {\ident$_1$} and
-{\ident$_2$} of the goal have an inductive type, then this tactic
-performs double induction on these variables.  For instance, if the
-current goal is \verb+forall n m:nat, P n m+ then, {\tt double induction n
-  m} yields the four cases with their respective inductive hypotheses.
-In particular the case for \verb+(P (S n) (S m))+ with the induction
-hypotheses \verb+(P (S n) m)+ and \verb+(m:nat)(P n m)+ (hence
-\verb+(P n m)+ and \verb+(P n (S m))+).
-
-\Rem When the induction hypothesis \verb+(P (S n) m)+ is not
-needed, {\tt induction \ident$_1$; destruct \ident$_2$} produces
-more concise subgoals.
-
-\begin{Variant}
-
-\item {\tt double induction \num$_1$ \num$_2$}
-
-This applies double induction on the \num$_1^{th}$ and \num$_2^{th}$ {\it
-non dependent} premises of the goal. More generally, any combination of an
-{\ident} and an {\num} is valid.
-
-\end{Variant}
-
-\subsection{\tt decompose [ {\qualid$_1$} \dots\ {\qualid$_n$} ] \term
-\label{decompose}
-\tacindex{decompose}}
-
-This tactic allows to recursively decompose a
-complex proposition in order to obtain atomic ones.
-Example: 
-
-\begin{coq_eval}
-Reset Initial.
-\end{coq_eval}
-\begin{coq_example}
-Lemma ex1 : forall A B C:Prop, A /\ B /\ C \/ B /\ C \/ C /\ A -> C.
-intros A B C H; decompose [and or] H; assumption.
-\end{coq_example}
-\begin{coq_example*}
-Qed.
-\end{coq_example*}
-
-{\tt decompose} does not work on right-hand sides of implications or products.
-
-\begin{Variants}
-  
-\item {\tt decompose sum \term}\tacindex{decompose sum}
-  This decomposes sum types (like \texttt{or}).
-\item {\tt decompose record \term}\tacindex{decompose record}
-  This decomposes record types (inductive types with one constructor,
-  like \texttt{and} and \texttt{exists} and those defined with the
-  \texttt{Record} macro, see p.~\pageref{Record}).
-\end{Variants}
-
-
-\subsection{\tt functional induction (\qualid\ \term$_1$ \dots\ \term$_n$).
-\tacindex{functional induction}
-\label{FunInduction}}
-
-The \emph{experimental} tactic \texttt{functional induction} performs
-case analysis and induction following the definition of a function. It
-makes use of a principle generated by \texttt{Function}
-(section~\ref{Function}) or \texttt{Functional Scheme}
-(section~\ref{FunScheme}).
-
-\begin{coq_eval}
-Reset Initial.
-\end{coq_eval}
-\begin{coq_example}
-Functional Scheme minus_ind := Induction for minus Sort Prop.
-
-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*}
-
-\Rem \texttt{(\qualid\ \term$_1$ \dots\ \term$_n$)} must be a correct
-full application of \qualid. In particular, the rules for implicit
-arguments are the same as usual. For example use \texttt{@\qualid} if
-you want to write implicit arguments explicitly.
-
-\Rem Parenthesis over \qualid \dots \term$_n$ are mandatory.
-
-\Rem \texttt{functional induction (f x1 x2 x3)} is actually a wrapper
-for \texttt{induction x1 x2 x3 (f x1 x2 x3) using \qualid} followed by
-a cleaning phase, where $\qualid$ is the induction principle
-registered for $f$ (by the \texttt{Function} (section~\ref{Function})
-or \texttt{Functional Scheme} (section~\ref{FunScheme}) command)
-corresponding to the sort of the goal.  Therefore \texttt{functional
-  induction} may fail if the induction scheme (\texttt{\qualid}) is
-not defined. See also section~\ref{Function} for the function terms
-accepted by \texttt{Function}.
-
-\Rem There is a difference between obtaining an induction scheme for a
-function by using \texttt{Function} (section~\ref{Function}) and by
-using \texttt{Functional Scheme} after a normal definition using
-\texttt{Fixpoint} or \texttt{Definition}. See \ref{Function} for
-details.
-
-\SeeAlso{\ref{Function},\ref{FunScheme},\ref{FunScheme-examples},
-  \ref{sec:functional-inversion}}
-
-\begin{ErrMsgs}
-\item \errindex{Cannot find induction information on \qualid}
-
-  ~
-
-\item \errindex{Not the right number of induction arguments}
-\end{ErrMsgs}
-
-\begin{Variants}
-\item {\tt functional induction (\qualid\ \term$_1$ \dots\ \term$_n$)
-   using \term$_{m+1}$ with {\term$_{n+1}$} \dots {\term$_m$}}
-
- Similar to \texttt{Induction} and \texttt{elim}
- (section~\ref{Tac-induction}), allows to give explicitly the
- induction principle and the values of dependent premises of the
- elimination scheme, including \emph{predicates} for mutual induction
- when \qualid is mutually recursive.
-
-\item {\tt functional induction (\qualid\ \term$_1$ \dots\ \term$_n$)
-    using \term$_{m+1}$ with {\vref$_1$} := {\term$_{n+1}$} \dots\
-    {\vref$_m$} := {\term$_n$}}
-
-  Similar to \texttt{induction} and \texttt{elim}
-  (section~\ref{Tac-induction}).
-
-\item All previous variants can be extended by the usual \texttt{as
-    \intropattern} construction, similarly for example to
-  \texttt{induction} and \texttt{elim} (section~\ref{Tac-induction}).
-    
-\end{Variants}
-
-
-
-\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$)}\texttt{eq}\term$_1$ \term$_2$. 
-
-\noindent where \texttt{eq} is the Leibniz equality or a registered
-setoid equality.
-
-\noindent Then {\tt rewrite \term} replaces every occurrence of 
-\term$_1$ by \term$_2$ in the goal. Some of the variables x$_1$ are
-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 \textit{clause}}
-  \tacindex{rewrite \dots\ in}\\
-  Analogous to {\tt rewrite {\term}} but rewriting is done following
-  \textit{clause} (similarly to \ref{Conversion-tactics}). For
-  instance:
-  \begin{itemize}
-  \item \texttt{rewrite H in H1} will rewrites \texttt{H} in the hypothesis
-    \texttt{H1} instead of the current goal.
-  \item \texttt{rewrite H in H1,H2 |- *} means \texttt{rewrite H; rewrite H in H1;
-      rewrite H in H2}. In particular a failure will happen if any of
-    these three simplier tactics fails. 
-  \item \texttt{rewrite H in * |- } will do \texttt{rewrite H in
-      H$_i$} for all hypothesis \texttt{H$_i$ <> H}. A success will happen
-    as soon as at least one of these simplier tactics succeeds.
-  \item \texttt{rewrite H in *} is a combination of \texttt{rewrite H} 
-    and \texttt{rewrite H in * |-} that succeeds if at
-    least one of these two tactics succeeds. 
-  \end{itemize}
-
-\item {\tt rewrite -> {\term} in \textit{clause}}
-  \tacindex{rewrite -> \dots\ in}\\
-  Behaves as {\tt rewrite {\term} in \textit{clause}}.
- 
-\item {\tt rewrite <- {\term} in \textit{clause}}\\
-  \tacindex{rewrite <- \dots\ in}
-  Uses the equality \term$_1${\tt=}\term$_2$ from right to left to
-  rewrite in \textit{clause} as explained above.
-\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$}
-\label{tactic:replace}
-\tacindex{replace \dots\ with}}
-
-This tactic applies to any goal. It replaces all free occurrences of
-{\term$_1$} in the current goal with {\term$_2$} and generates the
-equality {\term$_2$}{\tt =}{\term$_1$} as a subgoal. This equality is
-automatically solved if it occurs amongst the assumption, or if its
-symmetric form occurs.  It is equivalent to {\tt cut
-\term$_2$=\term$_1$; [intro H{\sl n}; rewrite <- H{\sl n}; clear H{\sl
-n}| assumption || symmetry; try assumption]}.
-
-\begin{ErrMsgs}
-\item \errindex{terms do not have convertible types}
-\end{ErrMsgs}
-
-\begin{Variants}
-\item {\tt replace {\term$_1$} with {\term$_2$} by \tac}\\ This acts
-  as {\tt replace {\term$_1$} with {\term$_2$}} but try to solve the
-  generated subgoal {\tt \term$_2$=\term$_1$} using {\tt \tac}.
-\item {\tt replace {\term}}\\ Replace {\term} with {\term'} using the
-  first assumption which type has the form {\tt \term=\term'} or {\tt
-    \term'=\term}
-\item {\tt replace -> {\term}}\\ Replace {\term} with {\term'} using the
-  first assumption which type has the form {\tt \term=\term'}
-\item {\tt replace <- {\term}}\\ Replace {\term} with {\term'} using the
-  first assumption which type has the form {\tt \term'=\term}
-\item {\tt replace {\term$_1$} with {\term$_2$} \textit{clause} }\\
-    {\tt replace {\term$_1$} with {\term$_2$} \textit{clause} by \tac }\\ 
-    {\tt replace {\term} \textit{clause}}\\ 
-    {\tt replace -> {\term} \textit{clause}}\\ 
-    {\tt replace -> {\term} \textit{clause}}\\ 
-    Act as before but the replacements take place in \textit{clause}~\ref{Conversion-tactics} an not only in the conclusion of the goal.\\
-    The  \textit{clause} arg must  not contain  any \texttt{type  of} nor  \texttt{value  of}.
-\end{Variants}
-
-\subsection{\tt reflexivity
-\label{reflexivity}
-\tacindex{reflexivity}}
-
-This tactic applies to a goal which has the form {\tt t=u}. It checks
-that {\tt t} and {\tt u} are convertible and then solves the goal.
-It is equivalent to {\tt apply refl\_equal}.
-
-\begin{ErrMsgs}
-\item \errindex{The conclusion is not a substitutive equation}
-\item \errindex{Impossible to unify \dots\ with ..}
-\end{ErrMsgs}
-
-\subsection{\tt symmetry
-\tacindex{symmetry}
-\tacindex{symmetry in}}
-This tactic applies to a goal which has the form {\tt t=u} and changes it
-into {\tt u=t}.
-
-\variant {\tt symmetry in {\ident}}\\
-If the statement of the hypothesis {\ident} has the form {\tt t=u},
-the tactic changes it to {\tt u=t}.
-
-\subsection{\tt transitivity \term
-\tacindex{transitivity}}
-This tactic applies to a goal which has the form {\tt t=u}
-and transforms it into the two subgoals 
-{\tt t={\term}} and {\tt {\term}=u}.
-
-\subsection{\tt subst {\ident}
-\tacindex{subst}}
-
-This tactic applies to a goal which has \ident\ in its context and
-(at least) one hypothesis, say {\tt H}, of type {\tt
-  \ident=t} or {\tt t=\ident}. Then it replaces 
-\ident\ by {\tt t} everywhere in the goal (in the hypotheses 
-and in the conclusion) and clears \ident\ and {\tt H} from the context.
-
-\Rem 
-When several hypotheses have the form {\tt \ident=t} or {\tt
-  t=\ident}, the first one is used. 
-
-\begin{Variants}
-  \item {\tt subst \ident$_1$ \dots \ident$_n$} \\
-    Is equivalent to {\tt subst \ident$_1$; \dots; subst \ident$_n$}.
-  \item {\tt subst} \\
-    Applies {\tt subst} repeatedly to all identifiers from the context
-    for which an equality exists.
-\end{Variants}
-
-\subsection{{\tt stepl {\term}}}
-\tacindex{stepl}
-
-This tactic is for chaining rewriting steps. It assumes a goal of the
-form ``$R$ {\term}$_1$ {\term}$_2$'' where $R$ is a binary relation
-and relies on a database of lemmas of the form {\tt forall} $x$ $y$
-$z$, $R$ $x$ $y$ {\tt ->} $eq$ $x$ $z$ {\tt ->} $R$ $z$ $y$ where $eq$
-is typically a setoid equality. The application of {\tt stepl {\term}}
-then replaces the goal by ``$R$ {\term} {\term}$_2$'' and adds a new
-goal stating ``$eq$ {\term} {\term}$_1$''.
-
-Lemmas are added to the database using the command 
-\comindex{Declare Left Step}
-\begin{quote}
-{\tt Declare Left Step {\term}.}
-\end{quote}
-
-The tactic is especially useful for parametric setoids which are not
-accepted as regular setoids for {\tt rewrite} and {\tt
-  setoid\_replace} (see chapter \ref{setoid_replace}).
-
-\tacindex{stepr}
-\comindex{Declare Right Step}
-\begin{Variants}
-\item{\tt stepl {\term}{\sl n} by {\tac}}\\
-This applies {\tt stepl {\term}} then applies {\tac} to the second goal.
-
-\item{\tt stepr {\term}}\\
-     {\tt stepr {\term} by {\tac}}\\
-This behaves as {\tt stepl} but on the right-hand-side of the binary relation.
-Lemmas are expected to be of the form
-``{\tt forall} $x$ $y$
-$z$, $R$ $x$ $y$ {\tt ->} $eq$ $y$ $z$ {\tt ->} $R$ $x$ $z$''
-and are registered using the command
-\begin{quote}
-{\tt Declare Right Step {\term}.}
-\end{quote}
-\end{Variants}
-
-\section{Equality and inductive sets}
-
-We describe in this section some special purpose tactics dealing with
-equality and inductive sets or types. These tactics use the equality
-{\tt eq:forall (A:Type), A->A->Prop}, simply written with the
-infix symbol {\tt =}.
-
-\subsection{\tt decide equality
-\label{decideequality}
-\tacindex{decide equality}}
-
-This tactic solves a goal of the form
-{\tt forall $x$ $y$:$R$, \{$x$=$y$\}+\{\verb|~|$x$=$y$\}}, where $R$
-is an inductive type such that its constructors do not take proofs or
-functions as arguments, nor objects in dependent types.
-
-\begin{Variants}
-\item {\tt decide equality {\term}$_1$ {\term}$_2$ }.\\
- Solves a goal of the form {\tt \{}\term$_1${\tt =}\term$_2${\tt
-\}+\{\verb|~|}\term$_1${\tt =}\term$_2${\tt \}}.
-\end{Variants}
-
-\subsection{\tt compare \term$_1$ \term$_2$
-\tacindex{compare}}
-
-This tactic compares two given objects \term$_1$ and \term$_2$ 
-of an inductive datatype. If $G$ is the current goal, it leaves the sub-goals
-\term$_1${\tt =}\term$_2$ {\tt ->} $G$ and \verb|~|\term$_1${\tt =}\term$_2$
-{\tt ->} $G$. The type
-of \term$_1$ and \term$_2$ must satisfy the same restrictions as in the tactic
-\texttt{decide equality}.
-
-\subsection {\tt discriminate {\ident}
-\label{discriminate}
-\tacindex{discriminate}}
-
-This tactic proves any goal from an absurd hypothesis stating that two
-structurally different terms of an inductive set are equal. For
-example, from the hypothesis {\tt (S (S O))=(S O)} we can derive by
-absurdity any proposition.  Let {\ident} be a hypothesis of type
-{\tt{\term$_1$} = {\term$_2$}} in the local context, {\term$_1$} and
-{\term$_2$} being elements of an inductive set.  To build the proof,
-the tactic traverses the normal forms\footnote{Recall: opaque
-  constants will not be expanded by $\delta$ reductions} of
-{\term$_1$} and {\term$_2$} looking for a couple of subterms {\tt u}
-and {\tt w} ({\tt u} subterm of the normal form of {\term$_1$} and
-{\tt w} subterm of the normal form of {\term$_2$}), placed at the same
-positions and whose head symbols are two different constructors. If
-such a couple of subterms exists, then the proof of the current goal
-is completed, otherwise the tactic fails.
-
-\Rem If {\ident} does not denote an hypothesis in the local context
-but refers to an hypothesis quantified in the goal, then the
-latter is first introduced in the local context using
-\texttt{intros until \ident}.
-
-\begin{ErrMsgs}
-\item {\ident} \errindex{Not a discriminable equality} \\
-  occurs when the type of the specified hypothesis is not an equation.
-\end{ErrMsgs}  
-
-\begin{Variants}
-\item \texttt{discriminate} \num\\
-  This does the same thing as \texttt{intros until \num} then
-\texttt{discriminate \ident} where {\ident} is the identifier for the last
-introduced hypothesis.
-\item {\tt discriminate}\tacindex{discriminate} \\
-  It applies to a goal of the form {\tt
-    \verb=~={\term$_1$}={\term$_2$}} and it is equivalent to: 
-  {\tt unfold not; intro {\ident}}; {\tt discriminate
-    {\ident}}.
-
-  \begin{ErrMsgs}
-  \item \errindex{No discriminable equalities} \\
-  occurs when the goal does not verify the expected preconditions.
-  \end{ErrMsgs}
-\end{Variants}
-
-\subsection{\tt injection {\ident}
-\label{injection}
-\tacindex{injection}}
-
-The {\tt injection} tactic is based on the fact that constructors of
-inductive sets are injections. That means that if $c$ is a constructor
-of an inductive set, and if $(c~\vec{t_1})$ and $(c~\vec{t_2})$ are two
-terms that are equal then $~\vec{t_1}$ and $~\vec{t_2}$ are equal
-too.
-
-If {\ident} is an hypothesis of type {\tt {\term$_1$} = {\term$_2$}},
-then {\tt injection} behaves as applying injection as deep as possible to
-derive the equality of all the subterms of {\term$_1$} and {\term$_2$}
-placed in the same positions. For example, from the hypothesis {\tt (S
-  (S n))=(S (S (S m))} we may derive {\tt n=(S m)}.  To use this
-tactic {\term$_1$} and {\term$_2$} should be elements of an inductive
-set and they should be neither explicitly equal, nor structurally
-different. We mean by this that, if {\tt n$_1$} and {\tt n$_2$} are
-their respective normal forms, then:
-\begin{itemize}
-\item {\tt n$_1$} and {\tt n$_2$} should not be syntactically equal,
-\item there must not exist any couple of subterms {\tt u} and {\tt w},
-  {\tt u} subterm of {\tt n$_1$} and {\tt w} subterm of {\tt n$_2$} ,
-  placed in the same positions and having different constructors as
-  head symbols.
-\end{itemize}
-If these conditions are satisfied, then, the tactic derives the
-equality of all the subterms of {\term$_1$} and {\term$_2$} placed in
-the same positions and puts them as antecedents of the current goal.
-
-\Example Consider the following goal:
-
-\begin{coq_example*}
-Inductive list : Set :=
-  | nil : list
-  | cons : nat -> list -> list.
-Variable P : list -> Prop.
-\end{coq_example*}
-\begin{coq_eval}
-Lemma ex :
- forall (l:list) (n:nat), P nil -> cons n l = cons 0 nil -> P l.
-intros l n H H0.
-\end{coq_eval}
-\begin{coq_example}
-Show.
-injection H0.
-\end{coq_example}
-\begin{coq_eval}
-Abort.
-\end{coq_eval}
-
-Beware that \texttt{injection} yields always an equality in a sigma type
-whenever the injected object has a dependent type.
-
-\Rem If {\ident} does not denote an hypothesis in the local context
-but refers to an hypothesis quantified in the goal, then the
-latter is first introduced in the local context using
-\texttt{intros until \ident}.
-
-\begin{ErrMsgs}
-\item {\ident} \errindex{is not a projectable equality} 
-  occurs when the type of
-  the hypothesis $id$ does not verify the preconditions.
-\item \errindex{Not an equation} occurs when the type of the
-  hypothesis $id$ is not an equation.
-\end{ErrMsgs}
-
-\begin{Variants}
-\item \texttt{injection} \num{}
-
-  This does the same thing as \texttt{intros until \num} then
-\texttt{injection \ident} where {\ident} is the identifier for the last
-introduced hypothesis.
-
-\item{\tt injection}\tacindex{injection} 
-  
-  If the current goal is of the form {\term$_1$} {\tt <>} {\term$_2$},
-  the tactic computes the head normal form of the goal and then
-  behaves as the sequence: {\tt unfold not; intro {\ident}; injection
-  {\ident}}.
-  
-  \ErrMsg \errindex{goal does not satisfy the expected preconditions}
-
-\item \texttt{injection} \ident{} \texttt{as} \nelist{\intropattern}{}\\
-\texttt{injection} \num{} \texttt{as} {\intropattern} {\ldots} {\intropattern}\\
-\texttt{injection} \texttt{as} {\intropattern} {\ldots} {\intropattern}\\
-\tacindex{injection \ldots{} as}
- 
-These variants apply \texttt{intros} \nelist{\intropattern}{} after the call to \texttt{injection}.
-
-\end{Variants}
-
-\subsection{\tt simplify\_eq {\ident}
-\tacindex{simplify\_eq}
-\label{simplify-eq}}
-
-Let {\ident} be the name of an hypothesis of type {\tt
-  {\term$_1$}={\term$_2$}} in the local context. If {\term$_1$} and
-{\term$_2$} are structurally different (in the sense described for the
-tactic {\tt discriminate}), then the tactic {\tt simplify\_eq} behaves as {\tt
-  discriminate {\ident}} otherwise it behaves as {\tt injection
-  {\ident}}.
-
-\Rem If {\ident} does not denote an hypothesis in the local context
-but refers to an hypothesis quantified in the goal, then the
-latter is first introduced in the local context using
-\texttt{intros until \ident}.
-
-\begin{Variants}
-\item \texttt{simplify\_eq} \num
-
-  This does the same thing as \texttt{intros until \num} then
-\texttt{simplify\_eq \ident} where {\ident} is the identifier for the last
-introduced hypothesis.
-\item{\tt simplify\_eq}
-If the current goal has form $\verb=~=t_1=t_2$, then this tactic does 
-\texttt{hnf; intro {\ident}; simplify\_eq {\ident}}.
-\end{Variants}
-
-\subsection{\tt dependent rewrite -> {\ident}
-\tacindex{dependent rewrite ->}
-\label{dependent-rewrite}}
-
-This tactic applies to any goal.  If \ident\ has type 
-\verb+(existS A B a b)=(existS A B a' b')+ 
-in the local context (i.e. each term of the
-equality has a sigma type $\{ a:A~ \&~(B~a)\}$) this tactic rewrites
-\verb+a+ into \verb+a'+ and \verb+b+ into \verb+b'+ in the current
-goal. This tactic works even if $B$ is also a sigma type.  This kind
-of equalities between dependent pairs may be derived by the injection
-and inversion tactics.
-
-\begin{Variants}
-\item{\tt dependent rewrite <- {\ident}}
-\tacindex{dependent rewrite <-} \\
-Analogous to {\tt dependent rewrite ->} but uses the equality from
-right to left.
-\end{Variants}
-
-\section{Inversion
-\label{inversion}}
-
-\subsection{\tt inversion {\ident}
-\tacindex{inversion}}
-
-Let the type of \ident~ in the local context be $(I~\vec{t})$,
-where $I$ is a (co)inductive predicate. Then,
-\texttt{inversion} applied to \ident~ derives for each possible
-constructor $c_i$ of $(I~\vec{t})$, {\bf all} the necessary
-conditions that should hold for the instance $(I~\vec{t})$ to be
-proved by $c_i$.
-
-\Rem If {\ident} does not denote an hypothesis in the local context
-but refers to an hypothesis quantified in the goal, then the
-latter is first introduced in the local context using
-\texttt{intros until \ident}.
-
-\begin{Variants}
-\item \texttt{inversion} \num
-  
-  This does the same thing as \texttt{intros until \num} then
-  \texttt{inversion \ident} where {\ident} is the identifier for the
-  last introduced hypothesis.
-
-\item \tacindex{inversion\_clear} \texttt{inversion\_clear} \ident
-
-  This behaves as \texttt{inversion} and then erases \ident~ from the
-  context.
-
-\item \tacindex{inversion \dots\ as} \texttt{inversion} {\ident} \texttt{as} {\intropattern}
-  
-  This behaves as \texttt{inversion} but using names in
-  {\intropattern} for naming hypotheses. The {\intropattern} must have
-  the form {\tt [} $p_{11}$ \ldots $p_{1n_1}$ {\tt |} {\ldots} {\tt |}
-  $p_{m1}$ \ldots $p_{mn_m}$ {\tt ]} with $m$ being the number of
-  constructors of the type of {\ident}. Be careful that the list must
-  be of length $m$ even if {\tt inversion} discards some cases (which
-  is precisely one of its roles): for the discarded cases, just use an
-  empty list (i.e. $n_i=0$).
-
-  The arguments of the $i^{th}$ constructor and the
-  equalities that {\tt inversion} introduces in the context of the
-  goal corresponding to the $i^{th}$ constructor, if it exists, get
-  their names from the list $p_{i1}$ \ldots $p_{in_i}$ in order. If
-  there are not enough names, {\tt induction} invents names for the
-  remaining variables to introduce. In case an equation splits into
-  several equations (because {\tt inversion} applies {\tt injection}
-  on the equalities it generates), the corresponding name $p_{ij}$ in
-  the list must be replaced by a sublist of the form {\tt [$p_{ij1}$
-  \ldots $p_{ijq}$]} (or, equivalently, {\tt ($p_{ij1}$,
-  \ldots, $p_{ijq}$)}) where $q$ is the number of subequations
-  obtained from splitting the original equation. Here is an example.
-
-\begin{coq_eval}
-Require Import List.
-\end{coq_eval}
-
-\begin{coq_example}
-Inductive contains0 : list nat -> Prop :=
-  | in_hd : forall l, contains0 (0 :: l)
-  | in_tl : forall l b, contains0 l -> contains0 (b :: l).
-Goal forall l:list nat, contains0 (1 :: l) -> contains0 l.
-intros l H; inversion H as [ | l' p Hl' [Heqp Heql'] ].
-\end{coq_example}
-
-\begin{coq_eval}
-Abort.
-\end{coq_eval}
-
-\item \texttt{inversion} {\num} {\tt as} {\intropattern} 
-
-  This allows to name the hypotheses introduced by
-  \texttt{inversion} {\num} in the context.
-
-\item \tacindex{inversion\_cleardots\ as} \texttt{inversion\_clear}
-  {\ident} {\tt as} {\intropattern}  
-
-  This allows to name the hypotheses introduced by
-  \texttt{inversion\_clear} in the context.
-  
-\item \tacindex{inversion \dots\ in} \texttt{inversion } {\ident}
-  \texttt{in} \ident$_1$ \dots\ \ident$_n$
-
-  Let \ident$_1$ \dots\ \ident$_n$, be identifiers in the local context. This
-  tactic behaves as generalizing \ident$_1$ \dots\ \ident$_n$, and
-  then performing \texttt{inversion}.
-  
-\item \tacindex{inversion \dots\ as \dots\ in} \texttt{inversion }
-  {\ident} {\tt as} {\intropattern} \texttt{in} \ident$_1$ \dots\ 
-  \ident$_n$
-  
-  This allows to name the hypotheses introduced in the context by
-  \texttt{inversion} {\ident} \texttt{in} \ident$_1$ \dots\ 
-  \ident$_n$.
-  
-\item \tacindex{inversion\_clear \dots\ in} \texttt{inversion\_clear}
-  {\ident} \texttt{in} \ident$_1$ \ldots \ident$_n$
- 
-  Let \ident$_1$ \dots\ \ident$_n$, be identifiers in the local context. This
-  tactic behaves as generalizing \ident$_1$ \dots\ \ident$_n$, and
-  then performing {\tt inversion\_clear}.
-  
-\item \tacindex{inversion\_clear \dots\ as \dots\ in}
-  \texttt{inversion\_clear} {\ident} \texttt{as} {\intropattern}
-  \texttt{in} \ident$_1$ \ldots \ident$_n$
-
-  This allows to name the hypotheses introduced in the context by
-  \texttt{inversion\_clear} {\ident} \texttt{in} \ident$_1$ \ldots
-  \ident$_n$.
-
-\item \tacindex{dependent inversion} \texttt{dependent inversion}
-  {\ident}  
-  
-  That must be used when \ident\ appears in the current goal.  It acts
-  like \texttt{inversion} and then substitutes \ident\ for the
-  corresponding term in the goal.
-  
-\item \tacindex{dependent inversion \dots\ as } \texttt{dependent
-    inversion} {\ident} \texttt{as} {\intropattern} 
-  
-  This allows to name the hypotheses introduced in the context by
-  \texttt{dependent inversion} {\ident}.
-
-\item \tacindex{dependent inversion\_clear} \texttt{dependent
-    inversion\_clear} {\ident} 
-  
-  Like \texttt{dependent inversion}, except that {\ident} is cleared
-  from the local context.
-
-\item \tacindex{dependent inversion\_clear \dots\ as}
-  \texttt{dependent inversion\_clear} {\ident}\texttt{as} {\intropattern}
-  
-  This allows to name the hypotheses introduced in the context by
-  \texttt{dependent inversion\_clear} {\ident}
-
-\item \tacindex{dependent inversion \dots\ with} \texttt{dependent
-    inversion } {\ident} \texttt{ with } \term  
-  
-  This variant allow to give the good generalization of the goal. It
-  is useful when the system fails to generalize the goal automatically. If
-  {\ident} has type $(I~\vec{t})$ and $I$ has type
-  $forall (\vec{x}:\vec{T}), s$,   then \term~  must be of type
-  $I:forall (\vec{x}:\vec{T}), I~\vec{x}\to s'$ where $s'$ is the
-  type of the goal.
-
-\item \tacindex{dependent inversion \dots\ as \dots\ with}
-  \texttt{dependent inversion } {\ident} \texttt{as} {\intropattern}
-  \texttt{ with } \term  
-  
-  This allows to name the hypotheses introduced in the context by
-  \texttt{dependent inversion } {\ident} \texttt{ with } \term.
-
-\item \tacindex{dependent inversion\_clear \dots\ with}
-  \texttt{dependent inversion\_clear } {\ident} \texttt{ with } \term 
-  
-  Like \texttt{dependent inversion \dots\ with} but clears \ident from
-  the local context.
-
-\item \tacindex{dependent inversion\_clear \dots\ as \dots\ with}
-  \texttt{dependent inversion\_clear } {\ident} \texttt{as}
-  {\intropattern} \texttt{ with } \term 
-  
-  This allows to name the hypotheses introduced in the context by
-  \texttt{dependent inversion\_clear } {\ident} \texttt{ with } \term.
-
-\item \tacindex{simple inversion} \texttt{simple inversion} {\ident}
-  
-  It is a very primitive inversion tactic that derives all the necessary
-  equalities  but it does not simplify the  constraints as
-  \texttt{inversion} do.
-
-\item \tacindex{simple inversion \dots\ as} \texttt{simple inversion}
-  {\ident} \texttt{as} {\intropattern} 
-  
-  This allows to name the hypotheses introduced in the context by
-  \texttt{simple inversion}.
-
-\item \tacindex{inversion \dots\ using} \texttt{inversion} \ident
-  \texttt{ using} \ident$'$  
-  
-  Let {\ident} have type $(I~\vec{t})$ ($I$ an inductive
-  predicate) in the local context, and \ident$'$ be a (dependent) inversion
-  lemma. Then, this tactic refines the current goal with the specified
-  lemma.
-
-\item \tacindex{inversion \dots\ using \dots\ in} \texttt{inversion}
-  {\ident} \texttt{using} \ident$'$ \texttt{in} \ident$_1$\dots\ \ident$_n$
-  
-  This tactic behaves as generalizing \ident$_1$\dots\ \ident$_n$,
-  then doing \texttt{inversion}{\ident}\texttt{using} \ident$'$.
-
-\end{Variants}
-
-\SeeAlso~\ref{inversion-examples} for detailed examples
-
-\subsection{\tt Derive Inversion {\ident} with
-  ${\tt forall (}\vec{x}{\tt :}\vec{T}{\tt),} I~\vec{t}$ Sort \sort
-\label{Derive-Inversion}
-\comindex{Derive Inversion}}
-
-This command generates an inversion principle for the
-\texttt{inversion \dots\ using} tactic.
-Let $I$ be an inductive predicate and $\vec{x}$ the variables
-occurring in $\vec{t}$. This command generates and stocks the
-inversion lemma for the sort \sort~ corresponding to the instance
-$forall (\vec{x}:\vec{T}), I~\vec{t}$ with the name {\ident} in the {\bf
-global} environment. When applied it is equivalent to have inverted
-the instance with the tactic {\tt inversion}.
-
-\begin{Variants}
-\item \texttt{Derive Inversion\_clear} {\ident} \texttt{with}
-  \comindex{Derive Inversion\_clear}
-  $forall (\vec{x}:\vec{T}), I~\vec{t}$ \texttt{Sort} \sort~ \\ 
-  \index{Derive Inversion\_clear \dots\ with}
-  When applied it is equivalent to having
-  inverted the instance with the tactic \texttt{inversion}
-  replaced by the tactic \texttt{inversion\_clear}.
-\item \texttt{Derive Dependent Inversion} {\ident} \texttt{with}
-  $forall (\vec{x}:\vec{T}), I~\vec{t}$ \texttt{Sort} \sort~\\
-  \comindex{Derive Dependent Inversion}
-  When applied it is equivalent to having
-  inverted the instance with the tactic \texttt{dependent inversion}.
-\item \texttt{Derive Dependent Inversion\_clear} {\ident} \texttt{with}
-  $forall (\vec{x}:\vec{T}), I~\vec{t}$ \texttt{Sort} \sort~\\
-  \comindex{Derive Dependent Inversion\_clear}
-  When applied it is equivalent to having
-  inverted the instance with the tactic \texttt{dependent inversion\_clear}.
-\end{Variants}
-
-\SeeAlso \ref{inversion-examples} for examples
-
-
-
-\subsection{\tt functional inversion \ident}
-\label{sec:functional-inversion}
-
-\texttt{functional inversion} is a \emph{highly} experimental tactic
-which performs inversion on hypothesis \ident\ of the form
-\texttt{\qualid\ \term$_1$\dots\term$_n$\ = \term} or \texttt{\term\ =
-  \qualid\ \term$_1$\dots\term$_n$} where \qualid\ must have been
-defined using \texttt{Function} (section~\ref{Function}).
-
-\begin{ErrMsgs}
-\item \errindex{Hypothesis \ident must contain at least one Function}
-\item \errindex{Cannot find inversion information for hypothesis \ident}
-  This error may be raised when  some inversion lemma failed to be
-  generated by Function.
-\end{ErrMsgs}
-
-\begin{Variants}
-\item {\tt functional inversion \num}
-
-  This does the same thing as \texttt{intros until \num} then
-  \texttt{functional inversion \ident} where {\ident} is the
-  identifier for the last introduced hypothesis.
-\item {\tt functional inversion \ident\ \qualid}\\
-  {\tt functional inversion \num\ \qualid}
-
-  In case the hypothesis \ident (or \num) has a type of the form
-  \texttt{\qualid$_1$\ \term$_1$\dots\term$_n$\ =\qualid$_2$\
-    \term$_{n+1}$\dots\term$_{n+m}$} where \qualid$_1$ and \qualid$_2$
-  are valid candidates to functional inversion, this variant allows to
-  chose which must be inverted.
-\end{Variants}
-
-
-
-\subsection{\tt quote \ident
-\tacindex{quote}
-\index{2-level approach}}
-
-This kind of inversion has nothing to do with the tactic
-\texttt{inversion} above. This tactic does \texttt{change (\ident\
-  t)}, where \texttt{t} is a term 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{Classical tactics}
-\label{ClassicalTactics}
-
-In order to ease the proving process, when the {\tt Classical} module is loaded. A few more tactics are available. Make sure to load the module using the \texttt{Require Import} command.
-
-\subsection{{\tt classical\_left, classical\_right} \tacindex{classical\_left} \tacindex{classical\_right}}
-
-The tactics \texttt{classical\_left} and \texttt{classical\_right} are the analog of the \texttt{left} and \texttt{right} but using classical logic. They can only be used for disjunctions.
-Use  \texttt{classical\_left} to prove the left part of the disjunction with the assumption that the negation of right part holds. 
-Use \texttt{classical\_left} to prove the right part of the disjunction with the assumption that the negation of left part holds. 
-
-\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 \texttt{auto using $lemma_1, \ldots, lemma_n$}
-
-  Uses $lemma_1, \ldots, lemma_n$ in addition to hints (can be conbined
-  with the \texttt{with \ident} option).
-
-\item {\tt trivial}\tacindex{trivial}
-
-  This tactic is a restriction of {\tt auto} that is not recursive and 
-  tries only hints which cost is 0. Typically it solves trivial
-  equalities like $X=X$.
-
-\item \texttt{trivial with \ident$_1$ \dots\ \ident$_n$}
-
-\item \texttt{trivial with *}
-
-\end{Variants}
-
-\Rem {\tt auto} either solves completely the goal or else leave it
-intact. \texttt{auto} and \texttt{trivial} never fail.
-
-\SeeAlso Section~\ref{Hints-databases}
-
-\subsection{\tt eauto
-\tacindex{eauto}
-\label{eauto}}
-
-This tactic generalizes {\tt auto}. In contrast with 
-the latter, {\tt eauto} uses unification of the goal
-against the hints rather than pattern-matching
-(in other words, it uses {\tt eapply} instead of
-{\tt apply}).
-As a consequence, {\tt eauto} can solve such a goal:
-
-\begin{coq_example}
-Hint Resolve ex_intro.
-Goal forall P:nat -> Prop, P 0 ->  exists n, P n.
-eauto.
-\end{coq_example}
-\begin{coq_eval}
-Abort.
-\end{coq_eval}
-
-Note that {\tt ex\_intro} should be declared as an
-hint.
-
-\SeeAlso Section~\ref{Hints-databases}
-
-% EXISTE ENCORE ?
-% 
-% \subsection{\tt Prolog [ \term$_1$ \dots\ \term$_n$ ] \num}
-% \tacindex{Prolog}\label{Prolog}
-% This tactic, implemented by Chet Murthy, is based upon the concept of
-% existential variables of Gilles Dowek, stating that resolution is a
-% kind of unification. It tries to solve the current goal using the {\tt
-%   Assumption} tactic, the {\tt intro} tactic, and applying hypotheses
-% of the local context and terms of the given list {\tt [ \term$_1$
-%   \dots\ \term$_n$\ ]}.  It is more powerful than {\tt auto} since it
-% may apply to any theorem, even those of the form {\tt (x:A)(P x) -> Q}
-% where {\tt x} does not appear free in {\tt Q}.  The maximal search
-% depth is {\tt \num}.
-
-% \begin{ErrMsgs}
-% \item \errindex{Prolog failed}\\
-%   The Prolog tactic was not able to prove the subgoal.
-% \end{ErrMsgs}
-
-\subsection{\tt tauto
-\tacindex{tauto}
-\label{tauto}}
-
-This tactic implements a decision procedure for intuitionistic propositional
-calculus based on the contraction-free sequent calculi LJT* of Roy Dyckhoff
-\cite{Dyc92}. Note that {\tt tauto} succeeds on any instance of an
-intuitionistic tautological proposition. {\tt tauto} unfolds negations
-and logical equivalence but does not unfold any other definition.
-
-The following goal can be proved by {\tt tauto} whereas {\tt auto}
-would fail:
-
-\begin{coq_example}
-Goal forall (x:nat) (P:nat -> Prop), x = 0 \/ P x -> x <> 0 -> P x.
-  intros.
-  tauto.
-\end{coq_example}
-\begin{coq_eval}
-Abort.
-\end{coq_eval}
-
-Moreover, if it has nothing else to do, {\tt tauto} performs
-introductions. Therefore, the use of {\tt intros} in the previous
-proof is unnecessary. {\tt tauto} can for instance prove the
-following:
-\begin{coq_example}
-(* auto would fail *)
-Goal forall (A:Prop) (P:nat -> Prop),
-    A \/ (forall x:nat, ~ A -> P x) -> forall x:nat, ~ A -> P x.
-
-  tauto.
-\end{coq_example}
-\begin{coq_eval}
-Abort.
-\end{coq_eval}
-
-\Rem In contrast, {\tt tauto} cannot solve the following goal
-
-\begin{coq_example*}
-Goal forall (A:Prop) (P:nat -> Prop),
-    A \/ (forall x:nat, ~ A -> P x) -> forall x:nat, ~ ~ (A \/ P x).
-\end{coq_example*}
-\begin{coq_eval}
-Abort.
-\end{coq_eval}
-
-because \verb=(forall x:nat, ~ A -> P x)= cannot be treated as atomic and an
-instantiation of \verb=x= is necessary.
-
-\subsection{\tt intuition {\tac}
-\tacindex{intuition}
-\label{intuition}}
-
-The tactic \texttt{intuition} takes advantage of the search-tree built
-by the decision procedure involved in the tactic {\tt tauto}. It uses
-this information to generate a set of subgoals equivalent to the
-original one (but simpler than it) and applies the tactic 
-{\tac} to them \cite{Mun94}. If this tactic fails on some goals then
-{\tt intuition} fails. In fact, {\tt tauto} is simply {\tt intuition
-  fail}.
-
-For instance, the tactic {\tt intuition auto} applied to the goal
-\begin{verbatim}
-(forall (x:nat), P x)/\B -> (forall (y:nat),P y)/\ P O \/B/\ P O
-\end{verbatim}
-internally replaces it by the equivalent one:
-\begin{verbatim}
-(forall (x:nat), P x), B |- P O
-\end{verbatim}
-and then uses {\tt auto} which completes the proof.
-
-Originally due to C{\'e}sar~Mu{\~n}oz, these tactics ({\tt tauto} and {\tt intuition})
-have been completely reengineered by David~Delahaye using mainly the tactic
-language (see chapter~\ref{TacticLanguage}). The code is now quite shorter and
-a significant increase in performances has been noticed. The general behavior
-with respect to dependent types, unfolding and introductions has
-slightly changed to get clearer semantics. This may lead to some
-incompatibilities.
-
-\begin{Variants}
-\item {\tt intuition}\\
-  Is equivalent to {\tt intuition auto with *}.
-\end{Variants}
-
-% En attente d'un moyen de valoriser les fichiers de demos
-%\SeeAlso file \texttt{contrib/Rocq/DEMOS/Demo\_tauto.v}
-
-
-\subsection{\tt rtauto
-\tacindex{rtauto}
-\label{rtauto}}
-
-The {\tt rtauto} tactic solves propositional tautologies similarly to what {\tt tauto} does. The main difference is that the proof term is built using a reflection scheme applied to a sequent calculus proof of the goal. The search procedure is also implemented using a different technique. 
-
-Users should be aware that this difference may result in faster proof-search but  slower proof-checking, and {\tt rtauto} might not solve goals that {\tt tauto} would be able to solve (e.g. goals involving universal quantifiers). 
-
-\subsection{{\tt firstorder}
-\tacindex{firstorder}
-\label{firstorder}}
-
-The tactic \texttt{firstorder} is an {\it experimental} extension of
-\texttt{tauto} to  
-first-order reasoning, written by Pierre Corbineau. 
-It is not restricted to usual logical connectives but
-instead may reason about any first-order class inductive definition.
-
-\begin{Variants}
- \item {\tt firstorder {\tac}}
-   \tacindex{firstorder {\tac}}
-
-   Tries to solve the goal with {\tac} when no logical rule may apply.
-
- \item {\tt firstorder with \ident$_1$ \dots\ \ident$_n$ }
-   \tacindex{firstorder with}
-
-   Adds lemmas \ident$_1$ \dots\ \ident$_n$ to the proof-search
-   environment.
-
- \item {\tt firstorder using \ident$_1$ \dots\ \ident$_n$ }
-   \tacindex{firstorder using}
-
-   Adds lemmas in {\tt auto} hints bases \ident$_1$ \dots\ \ident$_n$
-   to the proof-search environment.
-\end{Variants}
-
-Proof-search is bounded by a depth parameter which can be set by typing the
-{\nobreak \tt Set Firstorder Depth $n$} \comindex{Set Firstorder Depth} 
-vernacular command.
-
-%% \subsection{{\tt jp} {\em (Jprover)}
-%% \tacindex{jp}
-%% \label{jprover}}
-
-%% The tactic \texttt{jp}, due to Huang Guan-Shieng, is an experimental
-%% port of the {\em Jprover}\cite{SLKN01} semi-decision procedure for
-%% first-order intuitionistic logic implemented in {\em
-%%   NuPRL}\cite{Kre02}.
-
-%% The tactic \texttt{jp}, due to Huang Guan-Shieng, is an {\it
-%%   experimental} port of the {\em Jprover}\cite{SLKN01} semi-decision 
-%% procedure for first-order intuitionistic logic implemented in {\em
-%%   NuPRL}\cite{Kre02}. 
-
-%% Search may optionnaly be bounded by a multiplicity parameter
-%% indicating how many (at most) copies of a formula may be used in 
-%% the proof process, its absence may lead to non-termination of the tactic.
-
-%% %\begin{coq_eval}
-%% %Variable S:Set.
-%% %Variables P Q:S->Prop.
-%% %Variable f:S->S.
-%% %\end{coq_eval}
-
-%% %\begin{coq_example*}
-%% %Lemma example: (exists x |P x\/Q x)->(exists x |P x)\/(exists x |Q x).
-%% %jp.
-%% %Qed.
-
-%% %Lemma example2: (forall x ,P x->P (f x))->forall x,P x->P (f(f x)).
-%% %jp.
-%% %Qed.
-%% %\end{coq_example*}
-
-%% \begin{Variants}
-%%  \item {\tt jp $n$}\\
-%%    \tacindex{jp $n$} 
-%%    Tries the {\em Jprover} procedure with multiplicities up to $n$,
-%%    starting from 1.
-%%  \item {\tt jp}\\
-%%    Tries the {\em Jprover} procedure without multiplicity bound, 
-%%    possibly running forever.
-%% \end{Variants}
-
-%% \begin{ErrMsgs}
-%%  \item \errindex{multiplicity limit reached}\\
-%%    The procedure tried all multiplicities below the limit and
-%%    failed. Goal might be solved by increasing the multiplicity limit. 
-%%  \item \errindex{formula is not provable}\\
-%%    The procedure determined that goal was not provable in
-%%    intuitionistic first-order logic, no matter how big the
-%%    multiplicity is.
-%% \end{ErrMsgs}
-
-
-% \subsection{\tt Linear}\tacindex{Linear}\label{Linear}
-% The tactic \texttt{Linear}, due to Jean-Christophe Filli{\^a}atre
-% \cite{Fil94}, implements a decision procedure for {\em Direct
-%   Predicate Calculus}, that is first-order Gentzen's Sequent Calculus
-% without contraction rules \cite{KeWe84,BeKe92}.  Intuitively, a
-% first-order goal is provable in Direct Predicate Calculus if it can be
-% proved using each hypothesis at most once.
-
-% Unlike the previous tactics, the \texttt{Linear} tactic does not belong
-% to the initial state of the system, and it must be loaded explicitly
-% with the command
-
-% \begin{coq_example*}
-% Require Linear.
-% \end{coq_example*}
-
-% For instance, assuming that \texttt{even} and \texttt{odd} are two
-% predicates on natural numbers, and \texttt{a} of type \texttt{nat}, the
-% tactic \texttt{Linear} solves the following goal
-
-% \begin{coq_eval}
-% Variables even,odd : nat -> Prop.
-% Variable a:nat.
-% \end{coq_eval}
-
-% \begin{coq_example*}
-% Lemma example : (even a) 
-%               -> ((x:nat)((even x)->(odd (S x))))
-%               -> (EX y | (odd y)).
-% \end{coq_example*}
-
-% You can find examples of the use of \texttt{Linear} in
-% \texttt{theories/DEMOS/DemoLinear.v}.
-% \begin{coq_eval}
-% Abort.
-% \end{coq_eval}
-
-% \begin{Variants}
-% \item {\tt Linear with \ident$_1$ \dots\ \ident$_n$}\\
-%   \tacindex{Linear with} 
-%   Is equivalent to apply first {\tt generalize \ident$_1$ \dots
-%     \ident$_n$} (see section \ref{generalize}) then the \texttt{Linear}
-%   tactic.  So one can use axioms, lemmas or hypotheses of the local
-%   context with \texttt{Linear} in this way.
-% \end{Variants}
-
-% \begin{ErrMsgs}
-% \item \errindex{Not provable in Direct Predicate Calculus}
-% \item \errindex{Found $n$ classical proof(s) but no intuitionistic one}\\ 
-%   The decision procedure looks actually for classical proofs of the
-%   goals, and then checks that they are intuitionistic.  In that case,
-%   classical proofs have been found, which do not correspond to
-%   intuitionistic ones.
-% \end{ErrMsgs}
-
-\subsection{\tt congruence
-\tacindex{congruence}
-\label{congruence}}
-
-The tactic {\tt congruence}, by Pierre Corbineau, implements the standard Nelson and Oppen
-congruence closure algorithm, which is a decision procedure for ground
-equalities with uninterpreted symbols. It also include the constructor theory
-(see \ref{injection} and \ref{discriminate}).
-If the goal is a non-quantified equality, {\tt congruence} tries to
-prove it with non-quantified equalities in the context. Otherwise it
-tries to infer a discriminable equality from those in the context. Alternatively, congruence tries to prove that an hypothesis is equal to the goal or to the negation of another hypothesis.
-
-{\tt congruence} is also able to take advantage of hypotheses stating quantified equalities, you have to provide a bound for the number of extra equalities generated that way. Please note that one of the memebers of the equality must contain all the quantified variables in order for {\tt congruence} to match against it. 
-
-\begin{coq_eval}
-Reset Initial.
-Variable A:Set.
-Variables a b:A.
-Variable f:A->A.
-Variable g:A->A->A.
-\end{coq_eval}
-
-\begin{coq_example}
-Theorem T: 
-  a=(f a) -> (g b (f a))=(f (f a)) -> (g a b)=(f (g b a)) -> (g a b)=a.
-intros.
-congruence.
-\end{coq_example}
-
-\begin{coq_eval}
-Reset Initial.
-Variable A:Set.
-Variables a c d:A.
-Variable f:A->A*A.
-\end{coq_eval}
-
-\begin{coq_example}
-Theorem inj : f = pair a -> Some (f c) = Some (f d) -> c=d.
-intros.
-congruence.
-\end{coq_example}
-
-\begin{Variants}
- \item {\tt congruence {\sl n}}\\
-  Tries to add at most {\tt \sl n} instances of hypotheses satting quantifiesd equalities to the problem in order to solve it. A bigger value of {\tt \sl n} does not make success slower, only failure. You might consider adding some lemmata as hypotheses using {\tt assert} in order for congruence to use them.
-
-\end{Variants}
-
-\begin{Variants}
-\item {\tt congruence with \term$_1$ \dots\ \term$_n$}\\
-  Adds {\tt \term$_1$ \dots\ \term$_n$} to the pool of terms used by
-  {\tt congruence}. This helps in case you have partially applied
-  constructors in your goal.
-\end{Variants}
-
-\begin{ErrMsgs}
-  \item \errindex{I don't know how to handle dependent equality} \\
-    The decision procedure managed to find a proof of the goal or of
-    a discriminable equality but this proof couldn't be built in Coq
-    because of dependently-typed functions.
-  \item \errindex{I couldn't solve goal} \\
-    The decision procedure didn't find any way to solve the goal.
-  \item \errindex{Goal is solvable by congruence but some arguments are missing. Try "congruence with \dots", replacing metavariables by arbitrary terms.} \\
-    The decision procedure could solve the goal with the provision
-    that additional arguments are supplied for some partially applied
-    constructors. Any term of an appropriate type will allow the
-    tactic to successfully solve the goal. Those additional arguments
-    can be given to {\tt congruence} by filling in the holes in the
-    terms given in the error message, using the {\tt with} variant
-    described below.
-\end{ErrMsgs}
-
-\subsection{\tt omega
-\tacindex{omega}
-\label{omega}}
-
-The tactic \texttt{omega}, due to Pierre Cr{\'e}gut,
-is an automatic decision procedure for Presburger
-arithmetic. It solves quantifier-free 
-formulas built with \verb|~|, \verb|\/|, \verb|/\|,
-\verb|->| on top of equalities and inequalities on
-both the type \texttt{nat} of natural numbers and \texttt{Z} of binary
-integers. This tactic must be loaded by the command \texttt{Require Import
-  Omega}. See the additional documentation about \texttt{omega}
-(chapter~\ref{OmegaChapter}).
-
-\subsection{{\tt ring} and {\tt ring\_simplify \term$_1$ \dots\ \term$_n$}
-\tacindex{ring}
-\tacindex{ring\_simplify}
-\comindex{Add Ring}}
-
-The {\tt ring} tactic solves equations upon polynomial expressions of
-a ring (or semi-ring) structure. It proceeds by normalizing both hand
-sides of the equation (w.r.t. associativity, commutativity and
-distributivity, constant propagation) and comparing syntactically the
-results.
-
-{\tt ring\_simplify} applies the normalization procedure described
-above to the terms given. The tactic then replaces all occurrences of
-the terms given in the conclusion of the goal by their normal
-forms. If no term is given, then the conclusion should be an equation
-and both hand sides are normalized.
-
-See chapter~\ref{ring} for more information on the tactic and how to
-declare new ring structures.
-
-\subsection{\tt field
-\tacindex{field}
-\comindex{Add Field}}
-
-\Example
-\begin{coq_example*}
-Require Import Reals.
-Goal forall x y:R,
-    (x * y > 0)%R ->
-    (x * (1 / x + x / (x + y)))%R =
-    ((- 1 / y) * y * (- x * (x / (x + y)) - 1))%R.
-\end{coq_example*}
-
-\begin{coq_example}
-intros; field.
-\end{coq_example}
-
-\begin{coq_eval}
-Reset Initial.
-\end{coq_eval}
-
-\SeeAlso file {\tt theories/Reals/Rbase.v} for an example of instantiation,\\
-\phantom{\SeeAlso}theory {\tt theories/Reals} for many examples of use of {\tt
-field}.
-
-\subsection{\tt legacy field
-\tacindex{legacy 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 LegacyField}. Field theories are declared (as for
-{\tt legacy ring}) with
-the {\tt Add Legacy Field} command.
-
-\subsection{\tt Add Legacy Field
-\comindex{Add Legacy Field}}
-
-This vernacular command adds a commutative field theory to the database for the
-tactic {\tt field}. You must provide this theory as follows:
-\begin{flushleft}
-{\tt Add Legacy Field {\it A} {\it Aplus} {\it Amult} {\it Aone} {\it Azero} {\it
-Aopp} {\it Aeq} {\it Ainv} {\it Rth} {\it Tinvl}}
-\end{flushleft}
-where {\tt {\it A}} is a term of type {\tt Type}, {\tt {\it Aplus}} is
-a term of type {\tt A->A->A}, {\tt {\it Amult}} is a term of type {\tt
-  A->A->A}, {\tt {\it Aone}} is a term of type {\tt A}, {\tt {\it
-    Azero}} is a term of type {\tt A}, {\tt {\it Aopp}} is a term of
-type {\tt A->A}, {\tt {\it Aeq}} is a term of type {\tt A->bool}, {\tt
-  {\it Ainv}} is a term of type {\tt A->A}, {\tt {\it Rth}} is a term
-of type {\tt (Ring\_Theory {\it A Aplus Amult Aone Azero Ainv Aeq})},
-and {\tt {\it Tinvl}} is a term of type {\tt forall n:{\it A},
-  {\~{}}(n={\it Azero})->({\it Amult} ({\it Ainv} n) n)={\it Aone}}.
-To build a ring theory, refer to Chapter~\ref{ring} for more details.
-
-This command adds also an entry in the ring theory table if this theory is not
-already declared. So, it is useless to keep, for a given type, the {\tt Add
-Ring} command if you declare a theory with {\tt Add Field}, except if you plan
-to use specific features of {\tt ring} (see Chapter~\ref{ring}). However, the
-module {\tt ring} is not loaded by {\tt Add Field} and you have to make a {\tt
-Require Import Ring} if you want to call the {\tt ring} tactic.
-
-\begin{Variants}
-
-\item {\tt Add Legacy 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 Legacy Field {\it A} {\it Aplus} {\it Amult} {\it Aone} {\it Azero}
-{\it Aopp} {\it Aeq} {\it Ainv} {\it Rth} {\it Tinvl}}\\
-{\tt \phantom{Add Legacy 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 \cite{DelMay01} for more details regarding the implementation of {\tt
-legacy field}.
-
-\subsection{\tt fourier
-\tacindex{fourier}}
-
-This tactic written by Lo{\"\i}c Pottier solves linear inequations on
-real numbers using Fourier's method~\cite{Fourier}. This tactic must
-be loaded by {\tt Require Import Fourier}.
-
-\Example
-\begin{coq_example*}
-Require Import Reals.
-Require Import Fourier.
-Goal forall x y:R, (x < y)%R -> (y + 1 >= x - 1)%R.
-\end{coq_example*}
-
-\begin{coq_example}
-intros; fourier.
-\end{coq_example}
-
-\begin{coq_eval}
-Reset Initial.
-\end{coq_eval}
-
-\subsection{\tt autorewrite with \ident$_1$ \dots \ident$_n$.
-\label{tactic:autorewrite}
-\tacindex{autorewrite}}
-
-This tactic \footnote{The behavior of this tactic has much changed compared to
-the versions available in the previous distributions (V6). This may cause
-significant changes in your theories to obtain the same result. As a drawback
-of the reengineering of the code, this tactic has also been completely revised
-to get a very compact and readable version.} carries out rewritings according
-the rewriting rule bases {\tt \ident$_1$ \dots \ident$_n$}.
-
-Each rewriting rule of a base \ident$_i$ is applied to the main subgoal until
-it fails. Once all the rules have been processed, if the main subgoal has
-progressed (e.g., if it is distinct from the initial main goal) then the rules
-of this base are processed again. If the main subgoal has not progressed then
-the next base is processed. For the bases, the behavior is exactly similar to
-the processing of the rewriting rules.
-
-The rewriting rule bases are built with the {\tt Hint~Rewrite} vernacular
-command.
-
-\Warning{} This tactic may loop if you build non terminating rewriting systems.
-
-\begin{Variant}
-\item {\tt autorewrite with \ident$_1$ \dots \ident$_n$ using \tac}\\
-Performs, in the same way, all the rewritings of the bases {\tt $ident_1$ $...$
-$ident_n$} applying {\tt \tac} to the main subgoal after each rewriting step.
-
-\item \texttt{autorewrite with {\ident$_1$} \dots \ident$_n$ in {\qualid}}
-
-  Performs all the rewritings in hypothesis {\qualid}.
-\item \texttt{autorewrite with {\ident$_1$} \dots \ident$_n$ in {\qualid}}
-
-  Performs all  the rewritings  in hypothesis {\qualid}  applying {\tt
-    \tac} to the main subgoal after each rewriting step.
-
-\item \texttt{autorewrite with {\ident$_1$} \dots \ident$_n$ in \textit{clause}}
-  Performs all  the rewritings  in the clause \textit{clause}. \\
-  The  \textit{clause} arg must  not contain  any \texttt{type  of} nor  \texttt{value  of}.
-
-\end{Variant}
-
-\SeeAlso section \ref{HintRewrite} for feeding the database of lemmas used by {\tt autorewrite}.
-
-\SeeAlso section \ref{autorewrite-example} for examples showing the use of
-this tactic. 
-
-% En attente d'un moyen de valoriser les fichiers de demos
-%\SeeAlso file \texttt{contrib/Rocq/DEMOS/Demo\_AutoRewrite.v}
-
-\section{Controlling automation}
-
-\subsection{The hints databases for {\tt auto} and {\tt eauto}
-\index{Hints databases}
-\label{Hints-databases}
-\comindex{Hint}}
-
-The hints for \texttt{auto} and \texttt{eauto} are stored in
-databases.  Each database maps head symbols to a list of hints. One can
-use the command \texttt{Print Hint \ident} to display the hints
-associated to the head symbol \ident{} (see \ref{PrintHint}). Each
-hint has a cost that is an nonnegative integer, and a pattern. 
-The hints with lower cost are tried first. A hint is tried by 
-\texttt{auto} when the conclusion of the current goal
-matches its pattern. The general
-command to add a hint to some database \ident$_1$, \dots, \ident$_n$ is:
-\begin{tabbing}
-  \texttt{Hint} \textsl{hint\_definition} \texttt{:} \ident$_1$ \ldots\ \ident$_n$
-\end{tabbing}
-where {\sl hint\_definition} is one of the following expressions:
-
-\begin{itemize}
-\item \texttt{Resolve} {\term} 
-  \comindex{Hint Resolve}
-  
-  This command adds {\tt apply {\term}} to the hint list
-  with the head symbol of the type of \term. The cost of that hint is
-  the number of subgoals generated by {\tt apply {\term}}.
-  
-  In case the inferred type of \term\ does not start with a product the
-  tactic added in the hint list is {\tt exact {\term}}. In case this
-  type can be reduced to a type starting with a product, the tactic {\tt
-    apply {\term}} is also stored in the hints list.
-  
-  If the inferred type of \term\ does contain a dependent
-  quantification on a predicate, it is added to the hint list of {\tt
-    eapply} instead of the hint list of {\tt apply}. In this case, a
-  warning is printed since the hint is only used by the tactic {\tt
-    eauto} (see \ref{eauto}). A typical example of hint that is used
-  only by \texttt{eauto} is a transitivity lemma.
-
-  \begin{ErrMsgs}
-  \item \errindex{Bound head variable}
-
-    The head symbol of the type of {\term} is a bound variable such
-    that this tactic cannot be associated to a constant.
-
-  \item \term\ \errindex{cannot be used as a hint}
-
-    The type of \term\ contains products over variables which do not
-    appear in the conclusion. A typical example is a transitivity axiom.
-    In that case the {\tt apply} tactic fails, and thus is useless.
-
-  \end{ErrMsgs}
-
-  \begin{Variants}
-
-  \item \texttt{Resolve} {\term$_1$} \dots {\term$_m$}
-
-    Adds each \texttt{Resolve} {\term$_i$}.
-
-  \end{Variants}
-
-\item \texttt{Immediate {\term}} 
-\comindex{Hint Immediate}
-  
-  This command adds {\tt apply {\term}; trivial} to the hint list
-  associated with the head symbol of the type of \ident in the given
-  database. This tactic will fail if all the subgoals generated by
-  {\tt apply {\term}} are not solved immediately by the {\tt trivial}
-  tactic which only tries tactics with cost $0$.
-  
-  This command is useful for theorems such that the symmetry of equality
-  or $n+1=m+1 \to n=m$ that we may like to introduce with a
-  limited use in order to avoid useless proof-search.
-  
-  The cost of this tactic (which never generates subgoals) is always 1,
-  so that it is not used by {\tt trivial} itself.
-
-  \begin{ErrMsgs}
-
-  \item \errindex{Bound head variable}
-
-  \item \term\ \errindex{cannot be used as a hint} 
-
-  \end{ErrMsgs}
-
-  \begin{Variants}
-
-    \item \texttt{Immediate} {\term$_1$} \dots {\term$_m$} 
-
-      Adds each \texttt{Immediate} {\term$_i$}.
-
-  \end{Variants}
-
-\item \texttt{Constructors} {\ident}
-\comindex{Hint Constructors}
-  
-  If {\ident} is an inductive type, this command adds all its
-  constructors as hints of type \texttt{Resolve}. Then, when the
-  conclusion of current goal has the form \texttt{({\ident} \dots)},
-  \texttt{auto} will try to apply each constructor.
-
-  \begin{ErrMsgs}
-
-    \item {\ident} \errindex{is not an inductive type}
-
-    \item {\ident} \errindex{not declared}
-
-  \end{ErrMsgs}
-
-  \begin{Variants}
-
-    \item \texttt{Constructors} {\ident$_1$} \dots {\ident$_m$} 
-
-      Adds each \texttt{Constructors} {\ident$_i$}.
-
-  \end{Variants}
-
-\item \texttt{Unfold} {\qualid}
-\comindex{Hint Unfold}
-  
-  This adds the tactic {\tt unfold {\qualid}} to the hint list that
-  will only be used when the head constant of the goal is \ident.  Its
-  cost is 4.
-
-  \begin{Variants}
-
-    \item \texttt{Unfold} {\ident$_1$} \dots {\ident$_m$} 
-
-      Adds each \texttt{Unfold} {\ident$_i$}.
-
-  \end{Variants}
-
-\item \texttt{Extern \num\ \pattern\ => }\textsl{tactic}
-\comindex{Hint Extern}
-
-  This hint type is to extend \texttt{auto} with tactics other than
-  \texttt{apply} and \texttt{unfold}. For that, we must specify a
-  cost, a pattern and a tactic to execute. Here is an example:
-
-\begin{quotation}
-\begin{verbatim}
-Hint Extern 4 ~(?=?) => discriminate.
-\end{verbatim}
-\end{quotation}
-
-  Now, when the head of the goal is a disequality, \texttt{auto} will
-  try \texttt{discriminate} if it does not succeed to solve the goal
-  with hints with a cost less than 4.
-
-  One can even use some sub-patterns of the pattern in the tactic
-  script. A sub-pattern is a question mark followed by an ident, like
-  \texttt{?X1} or \texttt{?X2}. Here is an example:
-
-% Require EqDecide.
-\begin{coq_example*}
-Require Import List.
-\end{coq_example*}
-\begin{coq_example}
-Hint Extern 5   ({?X1 = ?X2} + {?X1 <> ?X2}) =>
- generalize X1 X2; decide equality : eqdec.
-Goal 
-forall a b:list (nat * nat), {a = b} + {a <> b}.
-info auto with eqdec.
-\end{coq_example}
-\begin{coq_eval}
-Abort.
-\end{coq_eval}
-
-\end{itemize}
-
-\Rem There is currently (in the \coqversion\ release) no way to do
-pattern-matching on hypotheses.
-
-\begin{Variants}
-\item \texttt{Hint} \textsl{hint\_definition} 
-  
-  No database name is given : the hint is registered in the {\tt core} 
-    database. 
-
-\item\texttt{Hint Local} \textsl{hint\_definition} \texttt{:}
-   \ident$_1$ \ldots\ \ident$_n$
-
-  This is used to declare hints that must not be exported to the other
-  modules that require and import the current module. Inside a
-  section, the option {\tt Local} is useless since hints do not
-  survive anyway to the closure of sections.
-
-\item\texttt{Hint Local} \textsl{hint\_definition} 
-
-  Idem for the {\tt core} database.
-    
-\end{Variants}
-
-% There are shortcuts that allow to define several goal at once:
-
-% \begin{itemize}
-% \item \comindex{Hints Resolve}\texttt{Hints Resolve \ident$_1$ \dots\ \ident$_n$ : \ident.}\\
-%   This command is a shortcut for the following ones:
-%   \begin{quotation}
-%    \noindent\texttt{Hint \ident$_1$ : \ident\ := Resolve \ident$_1$}\\
-%    \dots\\
-%    \texttt{Hint \ident$_1$ : \ident := Resolve \ident$_1$}
-%   \end{quotation}
-%   Notice that the hint name is the same that the theorem given as
-%   hint.
-% \item \comindex{Hints Immediate}\texttt{Hints Immediate \ident$_1$ \dots\ \ident$_n$ : \ident.}\\
-% \item \comindex{Hints Unfold}\texttt{Hints Unfold \qualid$_1$ \dots\ \qualid$_n$ : \ident.}\\
-% \end{itemize}
-
-%\begin{Warnings}
-%  \item \texttt{Overriding hint named \dots\ in database \dots}
-%\end{Warnings}
-
-\subsection{Hint databases defined in the \Coq\ standard library}
-
-Several hint databases are defined in the \Coq\ standard library.  The
-actual content of a database is the collection of the hints declared
-to belong to this database in each of the various modules currently
-loaded.  Especially, requiring new modules potentially extend a
-database. At {\Coq} startup, only the {\tt core} and {\tt v62}
-databases are non empty and can be used.
-
-\begin{description}
-
-\item[\tt core] This special database is automatically used by
-  \texttt{auto}. It contains only basic lemmas about negation,
-  conjunction, and so on from. Most of the hints in this database come 
-  from the \texttt{Init} and \texttt{Logic} directories.
-
-\item[\tt arith] This database contains all lemmas about Peano's
-  arithmetic proven in the directories \texttt{Init} and
-  \texttt{Arith}
-
-\item[\tt zarith] contains lemmas about binary signed integers from
-  the directories \texttt{theories/ZArith}. When required, the module
-  {\tt Omega} also extends the database {\tt zarith} with a high-cost
-  hint that calls {\tt omega} on equations and inequations in {\tt
-  nat} or {\tt Z}.
-
-\item[\tt bool] contains lemmas about booleans, mostly from directory
-  \texttt{theories/Bool}.
-
-\item[\tt datatypes] is for lemmas about lists, streams and so on that 
-  are mainly proven in the \texttt{Lists} subdirectory.
-
-\item[\tt sets] contains lemmas about sets and relations from the 
-  directories \texttt{Sets} and \texttt{Relations}.
-\end{description}
-
-There is also a special database called {\tt v62}. It collects all
-hints that were declared in the versions of {\Coq} prior to version
-6.2.4 when the databases {\tt core}, {\tt arith}, and so on were
-introduced.  The purpose of the database {\tt v62} is to ensure
-compatibility with further versions of Coq for developments done in
-versions prior to 6.2.4 ({\tt auto} being replaced by {\tt auto with v62}).
-The database {\tt v62} is intended not to be extended (!). It is not
-included in the hint databases list used in the {\tt auto with *} tactic.
-
-Furthermore, you are advised not to put your own hints in the
-{\tt core} database, but use one or several databases specific to your
-development.
-
-\subsection{\tt Print Hint
-\label{PrintHint}
-\comindex{Print Hint}}
-
-This command displays all hints that apply to the current goal. It
-fails if no proof is being edited, while the two variants can be used at
-every moment.
-
-\begin{Variants}
-
-\item {\tt  Print Hint {\ident} }
-
- This command displays only tactics associated with \ident\ in the
- hints list. This is independent of the goal being edited, to this
- command will not fail if no goal is being edited.
-
-\item {\tt Print Hint *}
-
-  This command displays all declared hints. 
-
-\item {\tt  Print HintDb {\ident} }
-\label{PrintHintDb}
-\comindex{Print HintDb}
-
- This command displays all hints from database \ident.
-
-\end{Variants}
-
-\subsection{\tt Hint Rewrite \term$_1$ \dots \term$_n$ : \ident
-\label{HintRewrite}
-\comindex{Hint Rewrite}}
-
-This vernacular command adds the terms {\tt \term$_1$ \dots \term$_n$}
-(their types must be equalities) in the rewriting base {\tt \ident}
-with the default orientation (left to right). Notice that the
-rewriting bases are distinct from the {\tt auto} hint bases and that
-{\tt auto} does not take them into account.
-
-This command is synchronous with the section mechanism (see \ref{Section}):
-when closing a section, all aliases created by \texttt{Hint Rewrite} in that
-section are lost. Conversely, when loading a module, all \texttt{Hint Rewrite}
-declarations at the global level of that module are loaded.
-
-\begin{Variants}
-\item {\tt Hint Rewrite -> \term$_1$ \dots \term$_n$ : \ident}\\
-This is strictly equivalent to the command above (we only make explicit the
-orientation which otherwise defaults to {\tt ->}).
-
-\item {\tt Hint Rewrite <- \term$_1$ \dots \term$_n$ : \ident}\\
-Adds the rewriting rules {\tt \term$_1$ \dots \term$_n$} with a right-to-left
-orientation in the base {\tt \ident}.
-
-\item {\tt Hint Rewrite \term$_1$ \dots \term$_n$ using {\tac} : {\ident}}\\
-When the rewriting rules {\tt \term$_1$ \dots \term$_n$} in {\tt \ident} will
-be used, the tactic {\tt \tac} will be applied to the generated subgoals, the
-main subgoal excluded.
-
-%% \item 
-%% {\tt Hint Rewrite [ \term$_1$ \dots \term$_n$ ] in \ident}\\
-%% {\tt Hint Rewrite [ \term$_1$ \dots \term$_n$ ] in {\ident} using {\tac}}\\
-%% These are deprecated syntactic variants for
-%% {\tt Hint Rewrite \term$_1$ \dots \term$_n$ : \ident} and
-%% {\tt Hint Rewrite \term$_1$ \dots \term$_n$ using {\tac} : {\ident}}.
-
-\item \texttt{Print Rewrite HintDb {\ident}}
-
-  This command displays all rewrite hints contained in {\ident}.
-
-\end{Variants}
-
-\subsection{Hints and sections
-\label{Hint-and-Section}}
-
-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.}).
-
-\subsection{Setting implicit automation tactics}
-
-\subsubsection{\tt Proof with {\tac}.}
-\label{ProofWith}
-\comindex{Proof with}
-
-  This command may be used to start a proof. It defines a default
-  tactic to be used each time a tactic command {\tac$_1$} is ended by
-  ``\verb#...#''. In this case the tactic command typed by the user is
-  equivalent to \tac$_1$;{\tac}.
-
-\SeeAlso {\tt Proof.} in section~\ref{BeginProof}.
-
-\subsubsection{\tt Declare Implicit Tactic {\tac}.}
-\comindex{Declare Implicit Tactic}
-
-This command declares a tactic to be used to solve implicit arguments
-that {\Coq} does not know how to solve by unification. It is used
-every time the term argument of a tactic has one of its holes not
-fully resolved.
-
-Here is an example:
-
-\begin{coq_example}
-Parameter quo : nat -> forall n:nat, n<>0 -> nat.
-Notation "x // y" := (quo x y _) (at level 40).
-
-Declare Implicit Tactic assumption.
-Goal forall n m, m<>0 -> { q:nat & { r | q * m + r = n } }.
-intros.
-exists (n // m).
-\end{coq_example}
-
-The tactic {\tt exists (n // m)} did not fail. The hole was solved by
-{\tt assumption} so that it behaved as {\tt exists (quo n m H)}.
-
-\section{Generation of induction principles with {\tt Scheme}
-\label{Scheme}
-\comindex{Scheme}}
-
-The {\tt Scheme} command is a high-level tool for generating
-automatically (possibly mutual) induction principles for given types
-and sorts.  Its syntax follows the schema:
-\begin{tabbing}
-{\tt Scheme {\ident$_1$} := Induction for \ident'$_1$ Sort {\sort$_1$} \\
-  with\\
-  \mbox{}\hspace{0.1cm} \dots\ \\
-        with {\ident$_m$} := Induction for {\ident'$_m$} Sort
-        {\sort$_m$}}
-\end{tabbing}
-\ident'$_1$ \dots\ \ident'$_m$ are different inductive type
-identifiers belonging to the same package of mutual inductive
-definitions. This command generates {\ident$_1$}\dots{} {\ident$_m$}
-to be mutually recursive definitions. Each term {\ident$_i$} proves a
-general principle of mutual induction for objects in type {\term$_i$}.
-
-\begin{Variants}
-\item {\tt Scheme {\ident$_1$} := Minimality for \ident'$_1$ Sort {\sort$_1$} \\
-    with\\
-    \mbox{}\hspace{0.1cm} \dots\ \\
-    with {\ident$_m$} := Minimality for {\ident'$_m$} Sort
-    {\sort$_m$}}
-
-  Same as before but defines a non-dependent elimination principle more
-  natural in case of inductively defined relations. 
-\end{Variants}
-
-\SeeAlso \ref{Scheme-examples}
-
-\SeeAlso Section~\ref{Scheme-examples}
-
-\section{Generation of induction principles with {\tt Functional Scheme}
-\label{FunScheme}
-\comindex{Functional Scheme}}
-
-The {\tt Functional Scheme} command is a high-level experimental
-tool for generating automatically induction principles
-corresponding to (possibly mutually recursive) functions.  Its
-syntax follows the schema:
-\begin{tabbing}
-{\tt Functional Scheme {\ident$_1$} := Induction for \ident'$_1$ Sort {\sort$_1$} \\
-  with\\
-  \mbox{}\hspace{0.1cm} \dots\ \\
-        with {\ident$_m$} := Induction for {\ident'$_m$} Sort
-        {\sort$_m$}}
-\end{tabbing}  
-\ident'$_1$ \dots\ \ident'$_m$ are different mutually defined function
-names (they must be in the same order as when they were defined).
-This command generates the induction principles
-\ident$_1$\dots\ident$_m$, following the recursive structure and case
-analyses of the functions \ident'$_1$ \dots\ \ident'$_m$.
-
-
-\paragraph{\texttt{Functional Scheme}} 
-There is a difference between obtaining an induction scheme by using
-\texttt{Functional Scheme} on a function defined by \texttt{Function}
-or not. Indeed \texttt{Function} generally produces smaller
-principles, closer to the definition written by the user.
-
-
-\SeeAlso Section~\ref{FunScheme-examples}
-
-
-\section{Simple tactic macros
-\index{tactic macros}
-\comindex{Tactic Definition}
-\label{TacticDefinition}}
-
-A simple example has more value than a long explanation: 
-
-\begin{coq_example}
-Ltac Solve := simpl; intros; auto.
-Ltac ElimBoolRewrite b H1 H2 :=
-  elim b; [ intros; rewrite H1; eauto | intros; rewrite H2; eauto ].
-\end{coq_example}
-
-The tactics macros are synchronous with the \Coq\ section mechanism:
-a tactic definition is deleted from the current environment
-when you close the section (see also \ref{Section}) 
-where it was defined. If you want that a
-tactic macro defined in a module is usable in the modules that
-require it, you should put it outside of any section.
-
-The chapter~\ref{TacticLanguage} gives examples of more complex
-user-defined tactics.
-
-
-% $Id: RefMan-tac.tex 9283 2006-10-26 08:13:51Z herbelin $ 
-
-%%% Local Variables: 
-%%% mode: latex
-%%% TeX-master: "Reference-Manual"
-%%% TeX-master: "Reference-Manual"
-%%% End: