diff options
| -rw-r--r-- | doc/RefMan-tac.tex | 19 | ||||
| -rw-r--r-- | doc/RefMan-tacex.tex | 29 |
2 files changed, 34 insertions, 14 deletions
diff --git a/doc/RefMan-tac.tex b/doc/RefMan-tac.tex index 43c6f965b..565c94e6a 100644 --- a/doc/RefMan-tac.tex +++ b/doc/RefMan-tac.tex @@ -1337,8 +1337,9 @@ Qed. \tacindex{functional induction} \label{FunInduction}} -The tactic \texttt{functional induction} performs case analysis -and induction following the definition of a function. +The \emph{experimental} tactic \texttt{functional induction} +performs case analysis and induction following the definition of +a (not mutually recursive) function. \begin{coq_eval} Reset Initial. @@ -1355,11 +1356,17 @@ Qed. \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. +mutually recursive) +functions. \SeeAlso{\ref{FunScheme-examples}} for the difference +between using one or the other. -\Rem \texttt{functional induction} does not work on polymorphic -and dependently typed functions yet. It may also fail on -functions built by certain tactics. +\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 +implicits. If the function is recursive, arguments must be +variables, otherwise they may be any term. \SeeAlso{\ref{FunScheme},\ref{FunScheme-examples}} diff --git a/doc/RefMan-tacex.tex b/doc/RefMan-tacex.tex index a26a18267..98ae9a7db 100644 --- a/doc/RefMan-tacex.tex +++ b/doc/RefMan-tacex.tex @@ -352,14 +352,13 @@ Qed. \end{coq_example*} \paragraph{remark:} \texttt{functional induction} makes no use of -a induction principle, so be warned that each time it is used, a -term mimicking the structure of \texttt{div2} (roughly the size -of {\tt div2\_ind}) is built. Using \texttt{Functional Scheme} is -generally faster and less memory consuming. On the other hand -\texttt{functional induction} performs some extra simplifications -that \texttt{Functional Scheme} does not, and as it is a tactic -it can be used in tactic definitions. - +an induction principle, so be warned that each time it is +applied, a term mimicking the structure of \texttt{div2} (roughly +the size of {\tt div2\_ind}) is built. Using \texttt{Functional + Scheme} is generally faster and less memory consuming. On the +other hand \texttt{functional induction} performs some extra +simplifications that \texttt{Functional Scheme} does not, and as +it is a tactic it can be used in tactic definitions. \example{Induction scheme for \texttt{tree\_size}} @@ -808,6 +807,8 @@ is undecidable in general case, don't expect miracles from it! \SeeAlso the \texttt{ring} tactic (Chapter~\ref{ring}) + + \section{Using the tactical language} \subsection{About the cardinality of the set of natural numbers} @@ -847,6 +848,11 @@ of non-linear matching). \subsection{Permutation on closed lists} +Another more complex example is the problem of permutation on closed lists. The +aim is to show that a closed list is a permutation of another one. + +First, we define the permutation predicate as shown in table~\ref{permutpred}. + \begin{figure} \begin{centerframe} \begin{coq_example*} @@ -932,6 +938,7 @@ With {\tt PermutProve}, we can now prove lemmas as follows: %\begin{figure} %\begin{centerframe} + \begin{coq_example*} Lemma permut_ex1 : permut nat (1 :: 2 :: 3 :: nil) (3 :: 2 :: 1 :: nil). @@ -1051,6 +1058,12 @@ Proof. TautoProp. Qed. \subsection{Deciding type isomorphisms} +A more tricky problem is to decide equalities between types and modulo +isomorphisms. Here, we choose to use the isomorphisms of the simply typed +$\lb{}$-calculus with Cartesian product and $unit$ type (see, for example, +\cite{RC95}). The axioms of this $\lb{}$-calculus are given by +table~\ref{isosax}. + \begin{figure} \begin{centerframe} \begin{coq_eval} |