From e978da8c41d8a3c19a29036d9c569fbe2a4616b0 Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Fri, 16 Jun 2006 14:41:51 +0000 Subject: Imported Upstream version 8.0pl3+8.1beta --- doc/refman/RefMan-tac.tex | 92 ++++++++++++++++++++++++++++++++++++----------- 1 file changed, 72 insertions(+), 20 deletions(-) (limited to 'doc/refman/RefMan-tac.tex') diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 72df6005..f034df41 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -1015,7 +1015,7 @@ equivalent to {\tt intros; apply ci}. \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 @@ -1387,42 +1387,83 @@ Qed. \end{Variants} -\subsection{\tt functional induction \ident\ \term$_1$ \dots\ \term$_n$. +\subsection{\tt functional induction (\ident\ \term$_1$ \dots\ \term$_n$). \tacindex{functional induction} \label{FunInduction}} -The \emph{experimental} tactic \texttt{functional induction} -performs case analysis and induction following the definition of -a (not mutually recursive) function. +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}). This principle is named \ident\_ind by +default but you can give it explicitly, see variants below. \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. +functional induction (minus n m); simpl; auto. \end{coq_example} \begin{coq_example*} Qed. \end{coq_example*} -\texttt{functional induction} is a shorthand for the more general -command \texttt{Functional Scheme} which builds induction -principles following the recursive structure of (possibly -mutually recursive) -functions. \SeeAlso{\ref{FunScheme-examples}} for the difference -between using one or the other. +\Rem \texttt{(\ident\ \term$_1$ \dots\ \term$_n$)} must be a correct +full application of \ident. In particular, the rules for implicit +arguments are the same as usual. For example use \texttt{@\ident} if +you want to write implicit arguments explicitly. + +\Rem Parenthesis over \ident \dots \term$_n$ are not mandatory, but if +there are not written then implicit arguments must be given. + +\Rem \texttt{functional induction (f x1 x2 x3)} is actually a +shorthand for \texttt{induction x1 x2 x3 (f x1 x2 x3) using f\_ind}. +\texttt{f\_ind} being an induction scheme computed by the +\texttt{Function} (section~\ref{Function}) or \texttt{Functional + Scheme} (section~\ref{FunScheme}) command . Therefore +\texttt{functional induction} may fail if the induction scheme +(\texttt{f\_ind}) 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}} + +\ErrMsg + +\errindex{The reference \ident\_ind was not found in the current +environment} + +~ -\Rem \texttt{functional induction} may fail on functions built by -tactics. In particular case analysis of a function are considered -only if they are not inside an application. +\errindex{Not the right number of induction arguments} + + +\begin{Variants} +\item {\tt functional induction (\ident\ \term$_1$ \dots\ \term$_n$) + using \term$_{m+1}$ with {\term$_{n+1}$} \dots {\term$_m$}} -\Rem Arguments of the function must be given, including the -implicit ones. If the function is recursive, arguments must be -variables, otherwise they may be any term. + 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 \ident is mutually recursive. -\SeeAlso{\ref{FunScheme},\ref{FunScheme-examples}} +\item {\tt functional induction (\ident\ \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}). +\end{Variants} \section{Equality} @@ -2067,6 +2108,17 @@ datatype: see~\ref{quote-examples} for the full details. % 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}} @@ -3087,7 +3139,7 @@ The chapter~\ref{TacticLanguage} gives examples of more complex user-defined tactics. -% $Id: RefMan-tac.tex 8606 2006-02-23 13:58:10Z herbelin $ +% $Id: RefMan-tac.tex 8938 2006-06-09 16:29:01Z jnarboux $ %%% Local Variables: %%% mode: latex -- cgit v1.2.3