diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 52 |
1 files changed, 37 insertions, 15 deletions
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index d9e600784..93a7406eb 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -149,6 +149,10 @@ usable in the proof development. its body. Otherwise said, this tactic turns a definition into an assumption. +\item \texttt{clear - {\ident}.} + + This tactic clears all hypotheses except the ones depending in {\ident}. + \end{Variants} \begin{ErrMsgs} @@ -527,6 +531,10 @@ in the list of subgoals remaining to prove. This tactic behaves like \texttt{assert} but tries to apply {\tac} to any subgoals generated by \texttt{assert}. +\item \texttt{assert {\form} as {\ident}\tacindex{assert as}} + + This tactic behaves like \texttt{assert ({\ident} : {\form})}. + \end{Variants} % PAS CLAIR; @@ -1125,6 +1133,11 @@ induction n. scheme of name {\qualid}. It does not expect that the type of {\term} is inductive. +\item \texttt{induction {\term}$_1$ $\ldots$ {\term}$_n$ using {\qualid}} + + where {\qualid} is an induction principle with complex predicates + (like the ones generated by function induction). + \item {\tt induction {\term} using {\qualid} as {\intropattern}} This combines {\tt induction {\term} using {\qualid}} @@ -1308,6 +1321,7 @@ components of an hypothesis. An introduction pattern is either: \begin{itemize} \item the wildcard: {\tt \_} +\item the pattern \texttt{?} \item a variable \item a disjunction of lists of patterns: {\tt [$p_{11}$ {\ldots} $p_{1m_1}$ | {\ldots} | $p_{11}$ {\ldots} $p_{nm_n}$]} @@ -1319,6 +1333,8 @@ structure of the pattern given as argument: \begin{itemize} \item introduction on the wildcard do the introduction and then immediately clear (cf~\ref{clear}) the corresponding hypothesis; +\item introduction on \texttt{?} do the introduction, and let Coq + choose a fresh name for the variable; \item introduction on a variable behaves like described in~\ref{intro}; \item introduction over a list of patterns $p_1~\ldots~p_n$ is equivalent to the sequence of @@ -1509,7 +1525,10 @@ implicit type of $t$ and $u$. This tactic applies to any goal. The type of {\term} must have the form -\texttt{(x$_1$:A$_1$) \dots\ (x$_n$:A$_n$)}\term$_1${\tt =}\term$_2$. +\texttt{(x$_1$:A$_1$) \dots\ (x$_n$:A$_n$)}\texttt{eq}\term$_1$ \term$_2$. + +\noindent where \texttt{eq} is the Leibniz equality or a registered +setoid equality. \noindent Then {\tt rewrite \term} replaces every occurrence of \term$_1$ by \term$_2$ in the goal. Some of the variables x$_1$ are @@ -1536,10 +1555,14 @@ This happens if \term$_1$ does not occur in the goal. \item {\tt rewrite <- {\term}}\tacindex{rewrite <-}\\ Uses the equality \term$_1${\tt=}\term$_2$ from right to left -\item {\tt rewrite {\term} in {\ident}} +\item {\tt rewrite {\term} in {\clause}} \tacindex{rewrite \dots\ in}\\ - Analogous to {\tt rewrite {\term}} but rewriting is done in the - hypothesis named {\ident}. + Analogous to {\tt rewrite {\term}} but rewriting is done following + {\clause} (similarly to \ref{Conversion-tactic}). For instance: + \texttt{rewrite H in H1,H2 |- *} means \texttt{rewrite H in H1; + rewrite H in H2; rewrite H} and \texttt{rewrite H in * |-} will do + \texttt{try rewrite H in H$_i$} for all hypothesis \texttt{H$_i$ <> + H}. \item {\tt rewrite -> {\term} in {\ident}} \tacindex{rewrite -> \dots\ in}\\ @@ -1656,12 +1679,12 @@ goal stating ``$eq$ {\term} {\term}$_1$''. Lemmas are added to the database using the command \comindex{Declare Left Step} \begin{quote} -{\tt Declare Left Step {\qualid}.} +{\tt Declare Left Step {\term}.} \end{quote} -where {\qualid} is the name of the lemma. The tactic is especially useful for parametric setoids which are not -accepted as regular setoids for {\tt rewrite} and {\tt setoid\_replace} (see chapter \ref{setoid_replace}). +accepted as regular setoids for {\tt rewrite} and {\tt + setoid\_replace} (see chapter \ref{setoid_replace}). \tacindex{stepr} \comindex{Declare Right Step} @@ -1677,7 +1700,7 @@ Lemmas are expected to be of the form $z$, $R$ $x$ $y$ {\tt ->} $eq$ $y$ $z$ {\tt ->} $R$ $x$ $z$'' and are registered using the command \begin{quote} -{\tt Declare Right Step {\qualid}.} +{\tt Declare Right Step {\term}.} \end{quote} \end{Variants} @@ -2746,7 +2769,7 @@ of the reengineering of the code, this tactic has also been completely revised to get a very compact and readable version.} carries out rewritings according the rewriting rule bases {\tt \ident$_1$ \dots \ident$_n$}. - Each rewriting rule of a base \ident$_i$ is applied to the main subgoal until +Each rewriting rule of a base \ident$_i$ is applied to the main subgoal until it fails. Once all the rules have been processed, if the main subgoal has progressed (e.g., if it is distinct from the initial main goal) then the rules of this base are processed again. If the main subgoal has not progressed then @@ -2762,12 +2785,11 @@ command. \item {\tt autorewrite with \ident$_1$ \dots \ident$_n$ using \tac}\\ Performs, in the same way, all the rewritings of the bases {\tt $ident_1$ $...$ $ident_n$} applying {\tt \tac} to the main subgoal after each rewriting step. -%\item{\tt autorewrite [ \ident$_1$ \dots \ident$_n$ ]}\\ -%{\tt autorewrite [ \ident$_1$ \dots \ident$_n$ ] using \tac}\\ -%These are deprecated syntactic variants for -%{\tt autorewrite with \ident$_1$ \dots \ident$_n$} -%and -%{\tt autorewrite with \ident$_1$ \dots \ident$_n$ using \tac}. + +\item \texttt{autorewrite with {\ident} in {\qualid}} + + Performs all the rewritings in hypothesis {\qualid}. + \end{Variant} \subsection{\tt Hint Rewrite \term$_1$ \dots \term$_n$ : \ident |