diff options
Diffstat (limited to 'doc')
-rw-r--r-- | doc/refman/RefMan-gal.tex | 34 | ||||
-rw-r--r-- | doc/refman/RefMan-tac.tex | 71 | ||||
-rw-r--r-- | doc/refman/RefMan-tacex.tex | 4 |
3 files changed, 84 insertions, 25 deletions
diff --git a/doc/refman/RefMan-gal.tex b/doc/refman/RefMan-gal.tex index cd5c2b3c4..be80e7eb7 100644 --- a/doc/refman/RefMan-gal.tex +++ b/doc/refman/RefMan-gal.tex @@ -1325,8 +1325,9 @@ mutual induction principles. It is described in Section~\ref{Scheme}. \subsubsection{\tt Function {\ident} {\binder$_1$}\ldots{\binder$_n$} {\tt \{}decrease\_annot{\tt\}} : type$_0$ := \term$_0$. +} \comindex{Function} -\label{Function}} +\label{Function} This \emph{experimental} command can be seen as a generalization of {\tt Fixpoint}. It is actually a wrapper for several ways of defining @@ -1376,10 +1377,31 @@ Function plus (n m : nat) {struct n} : nat := \paragraph{Limitations} \label{sec:Function-limitations} -\term$_0$ must be build as an imbrication of pattern matchings +\term$_0$ must be build as a \emph{pure pattern-matching tree} (\texttt{match...with}) with $\lambda$-abstraction and applications only -\emph{at the end} of each branch. -For now dependent cases are not treated. +\emph{at the end} of each branch. For now dependent cases are not +treated. + + +\ErrMsg + +\errindex{while trying to define Inductive R\_\ident ...} + +The generation of the graph relation \texttt{(R\_\ident)} used to +compute the induction scheme of \ident raised a typing error, the +definition of \ident was aborted. You can use \texttt{Fixpoint} +instead of \texttt{Function}, but the scheme will not be generated. + +This error happens generally when: + +\begin{itemize} +\item the definition uses pattern matching on dependent types, which + \texttt{Function} cannot deal with yet. +\item the definition is not a \emph{pattern-matching tree} as + explained above. +\end{itemize} + + \SeeAlso{\ref{FunScheme},\ref{FunScheme-examples},\ref{FunInduction}} @@ -1387,6 +1409,8 @@ Depending on the {\tt \{\}} annotation, different definition mechanisms are used by {\tt Function}. More precise description given below. + + \subsubsection{\tt Function {\ident} {\binder$_1$}\ldots{\binder$_n$} : type$_0$ := \term$_0$. \comindex{Function} @@ -1433,7 +1457,7 @@ the following: \item {\tt \{wf} \term$_1$ \ident$_0${\tt\}} with \ident$_0$ being the decreasing argument and \term$_1$ an ordering relation on the type of \ident$_0$ (i.e. of type T$_{\ident_0}$ - $\rightarrow$ T$_{\ident_0}$ $\rightarrow$ {\tt Prop}) for which + $\to$ T$_{\ident_0}$ $\to$ {\tt Prop}) for which the decreasing argument decreases at each recursive call of \term$_0$. The order must be well founded. parameters of the function are bound in \term$_0$. diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index b689a8f2d..cf1099169 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -1387,19 +1387,29 @@ 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. It makes use of principle -generated by \texttt{Function}\ref{Function}. +The \emph{experimental} tactic \texttt{functional induction} performs +case analysis and induction following the definition of a function. It +makes use of the principle \ident\_ind 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} +Function minus (n m : nat) {struct n} : nat := +match n with + | 0 => 0 + | S k => match m with + | 0 => S k + | S l => minus k l + end + end. + Lemma le_minus : forall n m:nat, (n - m <= n). intros n m. functional induction minus n m; simpl; auto. @@ -1408,22 +1418,47 @@ functional induction minus n m; simpl; auto. 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 Arguments of the function must be given, including the implicit +ones. + +\Rem Parenthesis over \ident \dots \term$_n$ are mandatory. + +\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} command +(section~\ref{Function}). 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}. + +\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. +~ -\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. +\errindex{Not the right number of induction arguments} + + +\begin{Variants} +\item {\tt functional induction (\ident\ \term$_1$ \dots\ \term$_n$) + with {\term$_1$} \dots {\term$_n$}} -\SeeAlso{\ref{FunScheme},\ref{FunScheme-examples}} + Similar to \texttt{Induction} and \texttt{elim} + (section~\ref{Tac-induction}), allows to give explicitly the values + of dependent premises of the elimination scheme, including + \emph{predicates} for mutual induction when \ident is mutually + recursive. + +\item {\tt functional induction (\ident\ \term$_1$ \dots\ \term$_n$) + with {\vref$_1$} := {\term$_1$} \dots\ {\vref$_n$} := {\term$_n$}} + + Similar to \texttt{induction} and \texttt{elim} + (section~\ref{Tac-induction}). +\end{Variants} \section{Equality} diff --git a/doc/refman/RefMan-tacex.tex b/doc/refman/RefMan-tacex.tex index ecd54f449..c25c275d6 100644 --- a/doc/refman/RefMan-tacex.tex +++ b/doc/refman/RefMan-tacex.tex @@ -706,7 +706,7 @@ theorem \texttt{simplify\_ok: (f:formula)(interp\_f (simplify f)) -> \end{verbatim} But there is a problem with leafs: in the example above one cannot write a function that implements, for example, the logical simplifications -$A \wedge A \ra A$ or $A \wedge \neg A \ra \texttt{False}$. This is +$A \land A \ra A$ or $A \land \lnot A \ra \texttt{False}$. This is because the \Prop{} is impredicative. It is better to use that type of formulas: @@ -724,7 +724,7 @@ Inductive formula : Set := \end{coq_example*} \texttt{index} is defined in module \texttt{quote}. Equality on that -type is decidable so we are able to simplify $A \wedge A$ into $A$ at +type is decidable so we are able to simplify $A \land A$ into $A$ at the abstract level. When there are variables, there are bindings, and \texttt{quote} |