aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
diff options
context:
space:
mode:
Diffstat (limited to 'doc')
-rwxr-xr-xdoc/common/macros.tex4
-rw-r--r--doc/refman/RefMan-syn.tex31
-rw-r--r--doc/refman/RefMan-tac.tex355
3 files changed, 244 insertions, 146 deletions
diff --git a/doc/common/macros.tex b/doc/common/macros.tex
index 6b6c158b5..1c4fa7e1f 100755
--- a/doc/common/macros.tex
+++ b/doc/common/macros.tex
@@ -125,7 +125,9 @@
\newcommand{\caseitem}{\nterm{match\_item}}
\newcommand{\eqn}{\nterm{equation}}
\newcommand{\ifitem}{\nterm{dep\_ret\_type}}
-\newcommand{\letclauses}{\nterm{letclauses}}
+\newcommand{\convclause}{\nterm{conversion\_clause}}
+\newcommand{\occclause}{\nterm{occurrence\_clause}}
+\newcommand{\occset}{\nterm{occurrence\_set}}
\newcommand{\params}{\nterm{params}} % vernac
\newcommand{\returntype}{\nterm{return\_type}}
\newcommand{\idparams}{\nterm{ident\_with\_params}}
diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex
index 71e87b3f3..e319bdbb1 100644
--- a/doc/refman/RefMan-syn.tex
+++ b/doc/refman/RefMan-syn.tex
@@ -1002,14 +1002,23 @@ syntax
%{\tt preident} $|$
{\tt ident} $|$
{\tt simple\_intropattern} $|$
-{\tt hyp} \\ & $|$ &
-% {\tt quantified\_hypothesis} $|$
-{\tt reference} $|$
-{\tt constr} \\ & $|$ &
+{\tt reference} \\ & $|$ &
+{\tt hyp} $|$
+{\tt hyp\_list} $|$
+{\tt ne\_hyp\_list} \\ & $|$ &
+% {\tt quantified\_hypothesis} \\ & $|$ &
+{\tt constr} $|$
+{\tt constr\_list} $|$
+{\tt ne\_constr\_list} \\ & $|$ &
%{\tt castedopenconstr} $|$
{\tt integer} $|$
-{\tt int\_or\_var} \\ & $|$ &
+{\tt integer\_list} $|$
+{\tt ne\_integer\_list} \\ & $|$ &
+{\tt int\_or\_var} $|$
+{\tt int\_or\_var\_list} $|$
+{\tt ne\_int\_or\_var\_list} \\ & $|$ &
{\tt tactic} $|$ {\tt tactic$n$} \qquad\mbox{(for $0\leq n\leq 5$)}
+
\end{tabular}
\medskip
@@ -1034,7 +1043,7 @@ use the corresponding kind of argument.
\noindent
\begin{tabular}{l|l|l|l}
Tactic argument type & parsed as & interpreted as & as in tactic \\
-\hline \\
+\hline & & & \\
{\tt\small ident} & identifier & a user-given name & {\tt intro} \\
{\tt\small simple\_intropattern} & intro\_pattern & an intro\_pattern & {\tt intros}\\
{\tt\small hyp} & identifier & an hypothesis defined in context & {\tt clear}\\
@@ -1046,8 +1055,10 @@ Tactic argument type & parsed as & interpreted as & as in tactic \\
%%{\tt\small castedopenconstr} & term & a term with its sign. of exist. var. & {\tt refine}\\
{\tt\small integer} & integer & an integer & \\
{\tt\small int\_or\_var} & identifier or integer & an integer & {\tt do} \\
-{\tt\small tactic} & tactic at level 5 & a tactic & \\
+{\tt\small tactic} & tactic at level 5 & a tactic & \\
{\tt\small tactic$n$} & tactic at level $n$ & a tactic & \\
+{\tt\small {\nterm{entry}}\_list} & list of {\nterm{entry}} & a list of how {\nterm{entry}} is interpreted & \\
+{\tt\small ne\_{\nterm{entry}}\_list} & non-empty list of {\nterm{entry}} & a list of how {\nterm{entry}} is interpreted& \\
\end{tabular}
\Rem In order to be bound in tactic definitions, each syntactic entry
@@ -1059,6 +1070,12 @@ for {\tt integer}. This is the reason for introducing a special entry
syntactically includes identifiers in order to be usable in tactic
definitions.
+\Rem The {\tt {\nterm{entry}}\_list} and {\tt ne\_{\nterm{entry}}\_list}
+entries can be used in primitive tactics or in other notations at
+places where a list of the underlying entry can be used: {\nterm{entry}} is
+either {\tt\small constr}, {\tt\small hyp}, {\tt\small integer} or
+{\tt\small int\_or\_var}.
+
% $Id$
%%% Local Variables:
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.