diff options
Diffstat (limited to 'doc/refman/RefMan-tacex.tex')
-rw-r--r-- | doc/refman/RefMan-tacex.tex | 44 |
1 files changed, 19 insertions, 25 deletions
diff --git a/doc/refman/RefMan-tacex.tex b/doc/refman/RefMan-tacex.tex index ecd54f44..57155d21 100644 --- a/doc/refman/RefMan-tacex.tex +++ b/doc/refman/RefMan-tacex.tex @@ -289,10 +289,8 @@ Require Import Arith. Fixpoint div2 (n:nat) : nat := match n with | O => 0 - | S n0 => match n0 with - | O => 0 - | S n' => S (div2 n') - end + | S O => 0 + | S (S n') => S (div2 n') end. \end{coq_example*} @@ -300,7 +298,7 @@ The definition of a principle of induction corresponding to the recursive structure of \texttt{div2} is defined by the command: \begin{coq_example} -Functional Scheme div2_ind := Induction for div2. +Functional Scheme div2_ind := Induction for div2 Sort Prop. \end{coq_example} You may now look at the type of {\tt div2\_ind}: @@ -315,7 +313,7 @@ We can now prove the following lemma using this principle: \begin{coq_example*} Lemma div2_le' : forall n:nat, div2 n <= n. intro n. - pattern n. + pattern n , (div2 n). \end{coq_example*} @@ -330,18 +328,17 @@ simpl; auto with arith. Qed. \end{coq_example*} -Since \texttt{div2} is not mutually recursive, we can use -directly the \texttt{functional induction} tactic instead of -building the principle: +We can use directly the \texttt{functional induction} +(\ref{FunInduction}) tactic instead of the pattern/apply trick: \begin{coq_example*} -Reset div2_ind. +Reset div2_le'. Lemma div2_le : forall n:nat, div2 n <= n. intro n. \end{coq_example*} \begin{coq_example} -functional induction div2 n. +functional induction (div2 n). \end{coq_example} \begin{coq_example*} @@ -351,14 +348,11 @@ auto with arith. Qed. \end{coq_example*} -\paragraph{remark:} \texttt{functional induction} makes no use of -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. +\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. \example{Induction scheme for \texttt{tree\_size}} @@ -398,14 +392,14 @@ recursive structure of \texttt{tree\_size} is defined by the command: \begin{coq_example*} -Functional Scheme treeInd := Induction for tree_size - with tree_size forest_size. +Functional Scheme tree_size_ind := Induction for tree_size Sort Prop +with forest_size_ind := Induction for forest_size Sort Prop. \end{coq_example*} -You may now look at the type of {\tt treeInd}: +You may now look at the type of {\tt tree\_size\_ind}: \begin{coq_example} -Check treeInd. +Check tree_size_ind. \end{coq_example} @@ -706,7 +700,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 +718,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} |