diff options
Diffstat (limited to 'doc/refman/RefMan-tac.tex')
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 355 |
1 files changed, 217 insertions, 138 deletions
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 3a8f6ca52..45993dd23 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -437,7 +437,8 @@ Section~\ref{pattern} to transform the goal so that it gets the form \subsection{{\tt set ( {\ident} {\tt :=} {\term} \tt )} \label{tactic:set} \tacindex{set} -\tacindex{pose}} +\tacindex{pose} +\tacindex{remember}} This replaces {\term} by {\ident} in the conclusion or in the hypotheses of the current goal and adds the new definition {\ident @@ -446,81 +447,45 @@ replacement only in the conclusion. \begin{Variants} -\item {\tt set ( } {\ident} {\tt :=} {\term} {\tt ) in *}\\ - {\tt set ( } {\ident} {\tt :=} {\term} {\tt ) in * |- *}\\ - - This behaves as above but substitutes {\term} - everywhere in the goal (both in conclusion and hypotheses). - -\item {\tt set ( } {\ident} {\tt :=} {\term} {\tt ) in * |-} - - This behaves the same but substitutes {\term} in - the hypotheses only (not in the conclusion). - -\item {\tt set ( } {\ident} {\tt :=} {\term} {\tt ) in |- *} - - This is equivalent to {\tt set ( } {\ident} {\tt :=} {\term} {\tt - )}, i.e. it substitutes {\term} in the conclusion only. - -\item {\tt set ( {\ident$_0$} {\tt :=} {\term} {\tt ) in} {\ident$_1$}} - - This behaves the same but substitutes {\term} only in - the hypothesis named {\ident$_1$}. - -\item {\tt set (} {\ident$_0$} {\tt :=} {\term} {\tt ) in} - {\ident$_1$} {\tt at} {\num$_1$} \dots\ {\num$_n$} +\item {\tt set (} {\ident} {\tt :=} {\term} {\tt ) in {\occset}} This notation allows to specify which occurrences of {\term} have to -be substituted in the hypothesis named {\ident$_1$}. The occurrences -are numbered from left to right and are meaningful on a pure -expression using no implicit argument, notation or coercion. A -negative occurrence number means an occurrence which should not be -substituted. As an exception of the left-to-right order, the -occurrences in the {\tt return} subexpression of a {\tt match} are -considered {\em before} the occurrences in the matched term. - -For expressions using notations, or hiding implicit arguments or -coercions, it is recommended to make explicit all occurrences in -order by using {\tt Set Printing All} (see -section~\ref{SetPrintingAll}). - -\item {\tt set ( } {\ident} {\tt :=} {\term} {\tt ) in |- * at} - {\num$_1$} \dots\ {\num$_n$} - -This allows to specify which occurrences of the conclusion are concerned. - -\item {\tt set (} {\ident$_0$} {\tt :=} {\term} {\tt ) in} - {\ident$_1$} {\tt at} {\num$_1^1$} \dots\ {\num$_{n_1}^1$}, \dots - {\ident$_m$} {\tt at} {\num$_1^m$} \dots {\num$_{n_m}^m$} - - It substitutes {\term} at occurrences {\num$_1^i$} \dots\ - {\num$_{n_i}^i$} of hypothesis {\ident$_i$}. Each {\tt at} part is - optional. +be substituted in the context. The {\tt in {\occset}} clause is an +occurrence clause whose syntax and behavior is described in +Section~\ref{Occurrences clauses}. \item {\tt set (} {\ident} \nelist{\binder}{} {\tt :=} {\term} {\tt )} This is equivalent to {\tt set (} {\ident} {\tt :=} {\tt fun} \nelist{\binder}{} {\tt =>} {\term} {\tt )}. -\item {\tt set (} {\ident$_0$} \nelist{\binder}{} {\tt :=} {\term} {\tt ) in} - {\ident$_1$} {\tt at} {\num$_1^1$} \dots\ {\num$_{n_1}^1$}, \dots - {\ident$_m$} {\tt at} {\num$_1^m$} \dots {\num$_{n_m}^m$} - {\tt |- *} {\tt at} {\num$'_1$} \dots\ {\num$'_n$} - - This is the more general form which combines all the previous - possibilities. - \item {\tt set } {\term} This behaves as {\tt set (} {\ident} := {\term} {\tt )} but {\ident} - is generated by {\Coq}. This variant is available for the - forms with {\tt in} too. + is generated by {\Coq}. This variant also supports an occurrence clause. + +\item {\tt set (} {\ident$_0$} \nelist{\binder}{} {\tt :=} {\term} + {\tt ) in {\occset}}\\ + {\tt set {\term} in {\occset}} + + These are the general forms which combine the previous possibilities. + +\item {\tt remember {\term} {\tt as} {\ident}} + + This behaves as {\tt set (} {\ident} := {\term} {\tt ) in *} and using a + logical (Leibniz's) equality instead of a local definition. + +\item {\tt remember {\term} {\tt as} {\ident} in {\occset}} + + This is a more general form of {\tt remember} that remembers the + occurrences of {\term} specified by an occurrences set. \item {\tt pose ( {\ident} {\tt :=} {\term} {\tt )}} This adds the local definition {\ident} := {\term} to the current context without performing any replacement in the goal or in the - hypotheses. + hypotheses. It is equivalent to {\tt set ( {\ident} {\tt :=} + {\term} {\tt ) in |-}}. \item {\tt pose (} {\ident} \nelist{\binder}{} {\tt :=} {\term} {\tt )} @@ -528,7 +493,7 @@ This allows to specify which occurrences of the conclusion are concerned. \nelist{\binder}{} {\tt =>} {\term} {\tt )}. \item{\tt pose {\term}} - + This behaves as {\tt pose (} {\ident} := {\term} {\tt )} but {\ident} is generated by {\Coq}. @@ -687,11 +652,31 @@ where $G'$ is obtained from $G$ by replacing all occurrences of $t$ by to $T$. \begin{Variants} -\item {\tt generalize \term$_1$ \dots\ \term$_n$} +\item {\tt generalize {\term$_1$ , \dots\ , \term$_n$}} Is equivalent to {\tt generalize \term$_n$; \dots\ ; generalize \term$_1$}. Note that the sequence of \term$_i$'s are processed from $n$ to $1$. + +\item {\tt generalize {\term} at {\num$_1$ \dots\ \num$_i$}} + + Is equivalent to {\tt generalize \term} but generalizing only over + the specified occurrences of {\term} (counting from left to right on the + expression printed using option {\tt Set Printing All}). + +\item {\tt generalize {\term} as {\ident}} + + Is equivalent to {\tt generalize \term} but use {\ident} to name the + generalized hypothesis. + +\item {\tt generalize {\term$_1$} at {\num$_{11}$ \dots\ \num$_{1i_1}$} + as {\ident$_1$} + , {\ldots} , + {\term$_n$} at {\num$_{n1}$ \dots\ \num$_{ni_n}$} + as {\ident$_2$}} + + This is the most general form of {\tt generalize} that combines the + previous behaviors. \item {\tt generalize dependent \term} \tacindex{generalize dependent} @@ -701,7 +686,7 @@ to $T$. \item {\tt revert \ident$_1$ \dots\ \ident$_n$}\tacindex{revert} This is equivalent to a {\tt generalize} followed by a {\tt clear} - on the given hypotheses. This tactic can be seem as reciprocal to + on the given hypotheses. This tactic can be seen as reciprocal to {\tt intros}. \end{Variants} @@ -748,44 +733,6 @@ This tactic applies to any goal. It implements the rule \end{Variants} \SeeAlso \ref{Conversion-tactics} -\subsection{Bindings list -\index{Binding list} -\label{Binding-list}} - -Tactics that take a term as argument may also support bindings list so -as to instantiate some parameters of the term by name or position. -The general form of a term equipped with a bindings list is {\tt -{\term} with {\bindinglist}} where {\bindinglist} may be of two -different forms: - -\begin{itemize} -\item In a bindings list of the form {\tt (\vref$_1$ := \term$_1$) - \dots\ (\vref$_n$ := \term$_n$)}, {\vref} is either an {\ident} or a - {\num}. The references are determined according to the type of - {\term}. If \vref$_i$ is an identifier, this identifier has to be - bound in the type of {\term} and the binding provides the tactic - with an instance for the parameter of this name. If \vref$_i$ is - some number $n$, this number denotes the $n$-th non dependent - premise of the {\term}, as determined by the type of {\term}. - - \ErrMsg \errindex{No such binder} - -\item A bindings list can also be a simple list of terms {\tt - \term$_1$ \term$_2$ \dots\term$_n$}. In that case the references to - which these terms correspond are determined by the tactic. In case - of {\tt induction}, {\tt destruct}, {\tt elim} and {\tt case} (see - Section~\ref{elim}) the terms have to provide instances for all the - dependent products in the type of \term\ while in the case of {\tt - apply}, or of {\tt constructor} and its variants, only instances for - the dependent products which are not bound in the conclusion of the - type are required. - - \ErrMsg \errindex{Not the right number of missing arguments} - -\end{itemize} - - - \subsection{\tt evar (\ident:\term) \tacindex{evar} \label{evar}} @@ -887,6 +834,101 @@ simultaneously proved are respectively {\tt forall} \end{Variants} +\subsection{Bindings list +\index{Binding list} +\label{Binding-list}} + +Tactics that take a term as argument may also support bindings list so +as to instantiate some parameters of the term by name or position. +The general form of a term equipped with a bindings list is {\tt +{\term} with {\bindinglist}} where {\bindinglist} may be of two +different forms: + +\begin{itemize} +\item In a bindings list of the form {\tt (\vref$_1$ := \term$_1$) + \dots\ (\vref$_n$ := \term$_n$)}, {\vref} is either an {\ident} or a + {\num}. The references are determined according to the type of + {\term}. If \vref$_i$ is an identifier, this identifier has to be + bound in the type of {\term} and the binding provides the tactic + with an instance for the parameter of this name. If \vref$_i$ is + some number $n$, this number denotes the $n$-th non dependent + premise of the {\term}, as determined by the type of {\term}. + + \ErrMsg \errindex{No such binder} + +\item A bindings list can also be a simple list of terms {\tt + \term$_1$ \dots\term$_n$}. In that case the references to + which these terms correspond are determined by the tactic. In case + of {\tt induction}, {\tt destruct}, {\tt elim} and {\tt case} (see + Section~\ref{elim}) the terms have to provide instances for all the + dependent products in the type of \term\ while in the case of {\tt + apply}, or of {\tt constructor} and its variants, only instances for + the dependent products which are not bound in the conclusion of the + type are required. + + \ErrMsg \errindex{Not the right number of missing arguments} + +\end{itemize} + +\subsection{Occurrences sets and occurrences clauses} +\label{Occurrences clauses} +\index{Occurrences clauses} + +An occurrences clause is a modifier to some tactics that obeys the +following syntax: + +$\!\!\!$\begin{tabular}{lcl} +{\occclause} & ::= & {\tt in} {\occset} \\ +{\occset} & ::= & + \zeroone{{\ident$_1$} \zeroone{{\tt at} {\num$_1^1$} \dots\ {\num$_{n_1}^1$}} {\tt ,} {\dots} {\tt ,} + {\ident$_m$} \zeroone{{\tt at} {\num$_1^m$} \dots {\num$_{n_m}^m$}}}\\ +& & + \zeroone{{\tt |-} + \zeroone{{\tt *} \zeroone{{\tt at} {\num$'_1$} \dots\ {\num$'_n$}}}}\\ +& | & + {\tt *} {\tt |-} + \zeroone{{\tt *} \zeroone{{\tt at} {\num$'_1$} \dots\ {\num$'_n$}}}\\ +& | & + {\tt *}\\ +\end{tabular} + +The role of an occurrence clause is to select a set of occurrences of +a {\term} in a goal. In the first case, the {{\ident$_i$} +\zeroone{{\tt at} {\num$_1^i$} \dots\ {\num$_{n_i}^i$}}} parts +indicate that occurrences have to be selected in the hypotheses named +{\ident$_i$}. If no numbers are given for hypothesis {\ident$_i$}, +then all occurrences of {\term} in the hypothesis are selected. If +numbers are given, they refer to occurrences of {\term} when the term +is printed using option {\tt Set Printing All} (see +Section~\ref{SetPrintingAll}), counting from left to right. In +particular, occurrences of {\term} in implicit arguments (see +Section~\ref{Implicit Arguments}) or coercions (see +Section~\ref{Coercions}) are counted. + +A negative occurrence number means an occurrence which should not be +substituted. As an exception to the left-to-right order, the +occurrences in the {\tt return} subexpression of a {\tt match} are +considered {\em before} the occurrences in the matched term. + +In the second case, the {\tt *} on the left of {\tt |-} means that +all occurrences of {\term} are selected in every hypothesis. + +In the first and second case, if {\tt *} is mentioned on the right of +{\tt |-}, the occurrences of the conclusion of the goal have to be +selected. If some numbers are given, then only the occurrences denoted +by these numbers are selected. In no numbers are given, all +occurrences of {\term} in the goal are selected. + +Finally, the last notation is an abbreviation for {\tt * |- *}. Note +also that {\tt |-} is optional in the first case when no {\tt *} is +given. + +Here are some tactics that understand occurrences clauses: +{\tt set}, {\tt remember}, {\tt induction}, {\tt destruct}. + +\SeeAlso~Sections~\ref{tactic:set}, \ref{Tac-induction}, \ref{SetPrintingAll}. + + \section{Negation and contradiction} \subsection{\tt absurd \term @@ -945,32 +987,35 @@ tactic \texttt{change}. All conversion tactics (including \texttt{change}) can be parameterized by the parts of the goal where the conversion can -occur. The specification of such parts are called \emph{clauses}. It -can be either the conclusion, or an hypothesis. In the case of a -defined hypothesis it is possible to specify if the conversion should -occur on the type part, the body part or both (default). - -\index{Clauses} Clauses are written after a conversion tactic (tactics +occur. This is done using \emph{goal clauses} which consists in a list +of hypotheses and, optionally, of a reference to the conclusion of the +goal. For defined hypothesis it is possible to specify if the +conversion should occur on the type part, the body part or both +(default). + +\index{Clauses} +\index{Goal clauses} +Goal clauses are written after a conversion tactic (tactics \texttt{set}~\ref{tactic:set}, \texttt{rewrite}~\ref{rewrite}, \texttt{replace}~\ref{tactic:replace} and \texttt{autorewrite}~\ref{tactic:autorewrite} also use clauses) and -are introduced by the keyword \texttt{in}. If no clause is provided, +are introduced by the keyword \texttt{in}. If no goal clause is provided, the default is to perform the conversion only in the conclusion. -The syntax and description of the various clauses follows: +The syntax and description of the various goal clauses is the following: \begin{description} -\item[\texttt{in H$_1$ $\ldots$ H$_n$ |- }] only in hypotheses $H_1 - $\ldots$ H_n$ -\item[\texttt{in H$_1$ $\ldots$ H$_n$ |- *}] in hypotheses $H_1 \ldots - H_n$ and in the conclusion -\item[\texttt{in * |-}] in every hypothesis -\item[\texttt{in *}] (equivalent to \texttt{in * |- *}) everywhere -\item[\texttt{in (type of H$_1$) (value of H$_2$) $\ldots$ |-}] in - type part of $H_1$, in the value part of $H_2$, etc. +\item[]\texttt{in {\ident}$_1$ $\ldots$ {\ident}$_n$ |- } only in hypotheses {\ident}$_1$ + \ldots {\ident}$_n$ +\item[]\texttt{in {\ident}$_1$ $\ldots$ {\ident}$_n$ |- *} in hypotheses {\ident}$_1$ \ldots + {\ident}$_n$ and in the conclusion +\item[]\texttt{in * |-} in every hypothesis +\item[]\texttt{in *} (equivalent to \texttt{in * |- *}) everywhere +\item[]\texttt{in (type of {\ident}$_1$) (value of {\ident}$_2$) $\ldots$ |-} in + type part of {\ident}$_1$, in the value part of {\ident}$_2$, etc. \end{description} -For backward compatibility, the notation \texttt{in}~$H_1\ldots H_n$ -performs the conversion in hypotheses $H_1\ldots H_n$. +For backward compatibility, the notation \texttt{in}~{\ident}$_1$\ldots {\ident}$_n$ +performs the conversion in hypotheses {\ident}$_1$\ldots {\ident}$_n$. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %voir reduction__conv_x : histoires d'univers. @@ -1451,12 +1496,28 @@ induction n. with complex predicates as the induction principles generated by {\tt Function} or {\tt Functional Scheme} may be. -\item{\tt induction {\term$_1$} with {\bindinglist$_1$} as {\intropattern} using {\term$_2$} with {\bindinglist$_2$}}\\ - {\tt einduction {\term$_1$} with {\bindinglist$_1$} as {\intropattern} using {\term$_2$} with {\bindinglist$_2$}} +\item \texttt{induction {\term} in *} + + This syntax tells to keep an equation between {\term} and the value + it gets in each case of the induction. + +\item \texttt{induction {\term} in {\occset}} + + This syntax is used for selecting which occurrences of {\term} the + induction has to be carried on. The {\tt in {\occset}} clause is an + occurrence clause whose syntax and behavior is described in + Section~\ref{Occurrences clause}. - This is the most general form of {\tt induction} and {\tt einduction}. - It combines the effects of the {\tt with}, {\tt as}, and {\tt - using} clauses. + When an occurrence clause is given, an equation between {\term} and + the value it gets in each case of the induction is added to the + context of the subgoals corresponding to the induction cases. + +\item{\tt induction {\term$_1$} with {\bindinglist$_1$} as {\intropattern} using {\term$_2$} with {\bindinglist$_2$} in {\occset}}\\ + {\tt einduction {\term$_1$} with {\bindinglist$_1$} as {\intropattern} using {\term$_2$} with {\bindinglist$_2$} in {\occset}} + + This is the most general form of {\tt induction} and {\tt + einduction}. It combines the effects of the {\tt with}, {\tt as}, + {\tt using}, and {\tt in} clauses. \item {\tt elim \term}\label{elim} @@ -1611,12 +1672,28 @@ last introduced hypothesis. These are synonyms of {\tt induction {\term$_1$} using {\term$_2$}} and {\tt induction {\term$_1$} using {\term$_2$} with {\bindinglist}}. -\item{\tt destruct {\term$_1$} with {\bindinglist$_1$} as {\intropattern} using {\term$_2$} with {\bindinglist$_2$}}\\ - {\tt edestruct {\term$_1$} with {\bindinglist$_1$} as {\intropattern} using {\term$_2$} with {\bindinglist$_2$}}\\ +\item \texttt{destruct {\term} in *} + + This syntax tells to keep an equation between {\term} and the value + it gets in each cases of the analysis. + +\item \texttt{destruct {\term} in {\occset}} + + This syntax is used for selecting which occurrences of {\term} the + case analysis has to be done on. The {\tt in {\occset}} clause is an + occurrence clause whose syntax and behavior is described in + Section~\ref{Occurrences clauses}. + + When an occurrence clause is given, an equation between {\term} and + the value it gets in each cases of the analysis is added to the + context of the subgoals corresponding to the cases. + +\item{\tt destruct {\term$_1$} with {\bindinglist$_1$} as {\intropattern} using {\term$_2$} with {\bindinglist$_2$} in {\occset}}\\ + {\tt edestruct {\term$_1$} with {\bindinglist$_1$} as {\intropattern} using {\term$_2$} with {\bindinglist$_2$} in {\occset}} This is the most general form of {\tt destruct} and {\tt edestruct}. - It combines the effects of the {\tt with}, {\tt as}, and {\tt - using} clauses. + It combines the effects of the {\tt with}, {\tt as}, {\tt using}, + and {\tt in} clauses. \item{\tt case \term}\label{case}\tacindex{case} @@ -1627,10 +1704,12 @@ last introduced hypothesis. \item{\tt case\_eq \term}\label{case_eq}\tacindex{case\_eq} The tactic {\tt case\_eq} is a variant of the {\tt case} tactic that - allow to perform case analysis on a term without completely - forgetting its original form. This is done by generating - equalities between the original form of the term and the outcomes of - the case analysis. + allow to perform case analysis on a term without completely + forgetting its original form. This is done by generating equalities + between the original form of the term and the outcomes of the case + analysis. The effect of this tactic is similar to the effect of {\tt + destruct {\term} in |- *} to the exception that no new hypotheses + is introduced in the context. \item {\tt case {\term} with {\bindinglist}} @@ -2063,7 +2142,7 @@ This happens if \term$_1$ does not occur in the goal. Rewrite only the given occurrences of \term$_1'$. Occurrences are specified from left to right as for \texttt{pattern} (\S \ref{pattern}). The rewrite is always performed using setoid - rewriting, even for leibniz equality, so one has to + rewriting, even for Leibniz's equality, so one has to \texttt{Import Setoid} to use this variant. \item {\tt rewrite {\term} by {\tac}} @@ -2379,7 +2458,7 @@ Abort. Beware that \texttt{injection} yields always an equality in a sigma type whenever the injected object has a dependent type. -\Rem There is a special case for dependant pairs. If we have a decidable +\Rem There is a special case for dependent pairs. If we have a decidable equality over the type of the first argument, then it is safe to do the projection on the second one, and so {\tt injection} will work fine. To define such an equality, you have to use the {\tt Scheme} command @@ -2521,7 +2600,7 @@ latter is first introduced in the local context using on the equalities it generates), the corresponding name $p_{ij}$ in the list must be replaced by a sublist of the form {\tt [$p_{ij1}$ \ldots $p_{ijq}$]} (or, equivalently, {\tt ($p_{ij1}$, - \ldots, $p_{ijq}$)}) where $q$ is the number of subequations + \ldots, $p_{ijq}$)}) where $q$ is the number of subequalities obtained from splitting the original equation. Here is an example. \begin{coq_eval} @@ -3502,7 +3581,7 @@ Require Import List. \end{coq_example*} \begin{coq_example} Hint Extern 5 ({?X1 = ?X2} + {?X1 <> ?X2}) => - generalize X1 X2; decide equality : eqdec. + generalize X1, X2; decide equality : eqdec. Goal forall a b:list (nat * nat), {a = b} + {a <> b}. info auto with eqdec. @@ -3774,7 +3853,7 @@ general principle of mutual induction for objects in type {\term$_i$}. \subsection{Automatic declaration of schemes} \comindex{Set Equality Scheme} \comindex{Set Elimination Schemes} -It is possible to desactive the automatic declaration of the induction +It is possible to deactivate the automatic declaration of the induction principles when defining a new inductive type with the {\tt UnSet Elimination Schemes} command. It may be reactivated at any time with {\tt Set Elimination Schemes}. @@ -3782,7 +3861,7 @@ reactivated at any time with {\tt Set Elimination Schemes}. You can also activate the automatic declaration of those boolean equalities (see the second variant of {\tt Scheme}) with the {\tt Set Equality Scheme} - command. However you have to be carefull with this option since + command. However you have to be careful with this option since \Coq~ may now reject well-defined inductive types because it cannot compute a boolean equality for them. |