diff options
Diffstat (limited to 'doc/RefMan-tacex.tex')
| -rw-r--r-- | doc/RefMan-tacex.tex | 29 |
1 files changed, 21 insertions, 8 deletions
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} |