diff options
Diffstat (limited to 'doc/refman')
| -rw-r--r-- | doc/refman/Program.tex | 2 | ||||
| -rw-r--r-- | doc/refman/RefMan-ltac.tex | 14 | ||||
| -rw-r--r-- | doc/refman/RefMan-oth.tex | 8 | ||||
| -rw-r--r-- | doc/refman/RefMan-syn.tex | 10 | ||||
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 182 |
5 files changed, 115 insertions, 101 deletions
diff --git a/doc/refman/Program.tex b/doc/refman/Program.tex index 3a99bfdd4f..11dd3a0517 100644 --- a/doc/refman/Program.tex +++ b/doc/refman/Program.tex @@ -261,7 +261,7 @@ tactic is replaced by the default one if not specified. as implicit arguments of the special constant \texttt{Program.Tactics.obligation}. \item {\tt Set Shrink Obligations}\optindex{Shrink Obligations} - Control whether obligations defined by tactics should have their + Control whether obligations should have their context minimized to the set of variables used in the proof of the obligation, to avoid unnecessary dependencies. \end{itemize} diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex index 5880487f71..cc7e6b53bf 100644 --- a/doc/refman/RefMan-ltac.tex +++ b/doc/refman/RefMan-ltac.tex @@ -1041,6 +1041,18 @@ This tactical is useful with tactics such as \texttt{omega} or the user can avoid the explosion at time of the \texttt{Save} command without having to cut manually the proof in smaller lemmas. +It may be useful to generate lemmas minimal w.r.t. the assumptions they depend +on. This can be obtained thanks to the option below. + +\begin{quote} +\optindex{Shrink Abstract} +{\tt Set Shrink Abstract} +\end{quote} + +When set, all lemmas generated through \texttt{abstract {\tacexpr}} are +quantified only over the variables that appear in the term constructed by +\texttt{\tacexpr}. + \begin{Variants} \item \texttt{abstract {\tacexpr} using {\ident}}.\\ Give explicitly the name of the auxiliary lemma. @@ -1089,7 +1101,7 @@ using the syntax: {\tt Ltac} {\qualid} {\ident}$_1$ ... {\ident}$_n$ {\tt ::=} {\tacexpr} \end{quote} -A previous definition of \qualid must exist in the environment. +A previous definition of {\qualid} must exist in the environment. The new definition will always be used instead of the old one and it goes accross module boundaries. diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex index 0a243308d5..aea2bae38d 100644 --- a/doc/refman/RefMan-oth.tex +++ b/doc/refman/RefMan-oth.tex @@ -914,6 +914,14 @@ This command turns off the normal displaying. \subsection[\tt Unset Silent.]{\tt Unset Silent.\optindex{Silent}} This command turns the normal display on. +\subsection[\tt Set Search Output Name Only.]{\tt Set Search Output Name Only.\optindex{Search Output Name Only} +\label{Search-Output-Name-Only} +\index{Search Output Name Only mode}} +This command restricts the output of search commands to identifier names; turning it on causes invocations of {\tt Search}, {\tt SearchHead}, {\tt SearchPattern}, {\tt SearchRewrite} etc. to omit types from their output, printing only identifiers. + +\subsection[\tt Unset Search Output Name Only.]{\tt Unset Search Output Name Only.\optindex{Search Output Name Only}} +This command turns type display in search results back on. + \subsection[\tt Set Printing Width {\integer}.]{\tt Set Printing Width {\integer}.\optindex{Printing Width}} \label{SetPrintingWidth} This command sets which left-aligned part of the width of the screen diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex index aabc8a8995..1f08b6a2f1 100644 --- a/doc/refman/RefMan-syn.tex +++ b/doc/refman/RefMan-syn.tex @@ -358,7 +358,7 @@ state of {\Coq}. Reserved Notation "x = y" (at level 70, no associativity). \end{coq_example} -Reserving a notation is also useful for simultaneously defined an +Reserving a notation is also useful for simultaneously defining an inductive type or a recursive constant and a notation for it. \Rem The notations mentioned on Figure~\ref{init-notations} are @@ -860,11 +860,11 @@ statically. For instance, if {\tt f} is a polymorphic function of type {\scope}, then {\tt a} of type {\tt t} in {\tt f~t~a} is not recognized as an argument to be interpreted in scope {\scope}. -\comindex{Bind Scope} -Any global reference can be bound by default to an -interpretation scope. The command to do it is +\comindex{Bind Scope} +More generally, any {\class} (see Chapter~\ref{Coercions-full}) can be +bound to an interpretation scope. The command to do it is \begin{quote} -{\tt Bind Scope} {\scope} \texttt{with} {\qualid} +{\tt Bind Scope} {\scope} \texttt{with} {\class} \end{quote} \Example diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 903e2e19af..54450fe7dc 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -802,7 +802,7 @@ the tactic {\tt intro} applies the tactic {\tt hnf} until the tactic \end{Variants} -\subsection{\tt intros {\intropattern} \mbox{\dots} \intropattern} +\subsection{\tt intros {\intropatternlist}} \label{intros-pattern} \tacindex{intros \intropattern} \index{Introduction patterns} @@ -811,9 +811,11 @@ the tactic {\tt intro} applies the tactic {\tt hnf} until the tactic \index{Disjunctive/conjunctive introduction patterns} \index{Equality introduction patterns} - -This extension of the tactic {\tt intros} combines introduction of -variables or hypotheses and case analysis. An {\em introduction pattern} is +This extension of the tactic {\tt intros} allows to apply tactics on +the fly on the variables or hypotheses which have been introduced. An +{\em introduction pattern list} {\intropatternlist} is a list of +introduction patterns possibly containing the filling introduction +patterns {\tt *} and {\tt **}. An {\em introduction pattern} is either: \begin{itemize} \item a {\em naming introduction pattern}, i.e. either one of: @@ -827,7 +829,7 @@ either: \item a {\em disjunctive/conjunctive introduction pattern}, i.e. either one of: \begin{itemize} \item a disjunction of lists of patterns: - {\tt [$p_{11}$ \dots\ $p_{1m_1}$ | \dots\ | $p_{11}$ \dots\ $p_{nm_n}$]} + {\tt [$\intropatternlist_1$ | \dots\ | $\intropatternlist_n$]} \item a conjunction of patterns: {\tt ($p_1$ , \dots\ , $p_n$)} \item a list of patterns {\tt ($p_1$ \&\ \dots\ \&\ $p_n$)} for sequence of right-associative binary constructs @@ -844,10 +846,6 @@ either: \item the wildcard: {\tt \_} \end{itemize} -Introduction patterns can be combined into lists. An {\em introduction - pattern list} is a list of introduction patterns possibly containing -the filling introduction patterns {\tt *} and {\tt **}. - Assuming a goal of type $Q \to P$ (non-dependent product), or of type $\forall x:T,~P$ (dependent product), the behavior of {\tt intros $p$} is defined inductively over the structure of the @@ -860,21 +858,22 @@ introduction pattern~$p$: \item introduction on \texttt{\ident} behaves as described in Section~\ref{intro}; \item introduction over a disjunction of list of patterns {\tt - [$p_{11}$ \dots\ $p_{1m_1}$ | \dots\ | $p_{11}$ \dots\ $p_{nm_n}$]} - expects the product to be over an inductive type - whose number of constructors is $n$ (or more generally over a type - of conclusion an inductive type built from $n$ constructors, - e.g. {\tt C -> A\textbackslash/B} with $n=2$ since {\tt - A\textbackslash/B} has 2 constructors): it destructs the introduced - hypothesis as {\tt destruct} (see Section~\ref{destruct}) would and - applies on each generated subgoal the corresponding tactic; - \texttt{intros}~$p_{i1}$ {\ldots} $p_{im_i}$; if the disjunctive - pattern is part of a sequence of patterns, then {\Coq} completes the - pattern so that all the arguments of the constructors of the - inductive type are introduced (for instance, the list of patterns - {\tt [$\;$|$\;$] H} applied on goal {\tt forall x:nat, x=0 -> 0=x} - behaves the same as the list of patterns {\tt [$\,$|$\,$?$\,$] H}, - up to one exception explained in the Remark below); + [$\intropatternlist_{1}$ | \dots\ | $\intropatternlist_n$]} expects + the product to be over an inductive type whose number of + constructors is $n$ (or more generally over a type of conclusion an + inductive type built from $n$ constructors, e.g. {\tt C -> + A\textbackslash/B} with $n=2$ since {\tt A\textbackslash/B} has 2 + constructors): it destructs the introduced hypothesis as {\tt + destruct} (see Section~\ref{destruct}) would and applies on each + generated subgoal the corresponding tactic; + \texttt{intros}~$\intropatternlist_i$. The introduction patterns in + $\intropatternlist_i$ are expected to consume no more than the + number of arguments of the $i^{\mbox{\scriptsize th}}$ + constructor. If it consumes less, then {\Coq} completes the pattern + so that all the arguments of the constructors of the inductive type + are introduced (for instance, the list of patterns {\tt [$\;$|$\;$] + H} applied on goal {\tt forall x:nat, x=0 -> 0=x} behaves the same + as the list of patterns {\tt [$\,$|$\,$?$\,$] H}); \item introduction over a conjunction of patterns {\tt ($p_1$, \ldots, $p_n$)} expects the goal to be a product over an inductive type $I$ with a single constructor that itself has at least $n$ arguments: it @@ -926,19 +925,6 @@ introduction pattern~$p$: not any more a quantification or an implication. \end{itemize} -Then, if $p_1$ ... $p_n$ is a list of introduction patterns possibly -containing {\tt *} or {\tt **}, {\tt intros $p_1$ ... $p_n$} -\begin{itemize} -\item introduction over {\tt *} introduces all forthcoming quantified - variables appearing in a row; -\item introduction over {\tt **} introduces all forthcoming quantified - variables or hypotheses until the goal is not any more a - quantification or an implication; -\item introduction over an introduction pattern $p$ introduces the - forthcoming quantified variables or premise of the goal and applies - the introduction pattern $p$ to it. -\end{itemize} - \Example \begin{coq_example} @@ -949,37 +935,39 @@ intros * [a | (_,c)] f. Abort. \end{coq_eval} -\Rem {\tt intros $p_1~\ldots~p_n$} is not fully equivalent to -\texttt{intros $p_1$;\ldots; intros $p_n$} for the following reasons: -\label{bracketing-last} -\begin{itemize} -\item A wildcard pattern never succeeds when applied isolated on a - dependent product, while it succeeds as part of a list of - introduction patterns if the hypotheses that depends on it are - erased too. -\item A disjunctive or conjunctive pattern followed by an introduction - pattern forces the introduction in the context of all arguments of - the constructors before applying the next pattern while a terminal - disjunctive or conjunctive pattern does not. Here is an example - -\begin{coq_example} -Goal forall n:nat, n = 0 -> n = 0. -intros [ | ] H. -Show 2. -Undo. -intros [ | ]; intros H. -Show 2. -\end{coq_example} +\Rem {\tt intros $p_1~\ldots~p_n$} is not equivalent to \texttt{intros + $p_1$;\ldots; intros $p_n$} for the following reason: If one of the +$p_i$ is a wildcard pattern, he might succeed in the first case +because the further hypotheses it depends in are eventually erased too +while it might fail in the second case because of dependencies in +hypotheses which are not yet introduced (and a fortiori not yet +erased). + +\Rem In {\tt intros $\intropatternlist$}, if the last introduction +pattern is a disjunctive or conjunctive pattern {\tt + [$\intropatternlist_1$ | \dots\ | $\intropatternlist_n$]}, the +completion of $\intropatternlist_i$ so that all the arguments of the +$i^{\mbox{\scriptsize th}}$ constructors of the corresponding +inductive type are introduced can be controlled with the +following option: +\optindex{Bracketing Last Introduction Pattern} -\end{itemize} +\begin{quote} +{\tt Set Bracketing Last Introduction Pattern} +\end{quote} -This later behavior can be avoided by setting the following option: +Force completion, if needed, when the last introduction pattern is a +disjunctive or conjunctive pattern (this is the default). \begin{quote} -\optindex{Bracketing Last Introduction Pattern} -{\tt Set Bracketing Last Introduction Pattern} +{\tt Unset Bracketing Last Introduction Pattern} \end{quote} +Deactivate completion when the last introduction pattern is a disjunctive +or conjunctive pattern. + + + \subsection{\tt clear \ident} \tacindex{clear} \label{clear} @@ -1267,18 +1255,9 @@ in the list of subgoals remaining to prove. introduction pattern (in particular, if {\intropattern} is {\ident}, the tactic behaves like \texttt{assert ({\ident} :\ {\form})}). - If {\intropattern} is a disjunctive/conjunctive - introduction pattern, the tactic behaves like \texttt{assert - {\form}} followed by a {\tt destruct} using this introduction pattern. - - If {\intropattern} is a rewriting intropattern pattern, the tactic - behaves like \texttt{assert {\form}} followed by a call to {\tt - subst} on the resulting hypothesis, if applicable, or to {\tt - rewrite} otherwise. - - If {\intropattern} is an injection intropattern pattern, the tactic - behaves like \texttt{assert {\form}} followed by {\tt injection} - using this introduction pattern. + If {\intropattern} is an action introduction pattern, the tactic + behaves like \texttt{assert {\form}} followed by the action done by + this introduction pattern. \item \texttt{assert {\form} as {\intropattern} by {\tac}} @@ -2854,43 +2833,58 @@ This tactic is deprecated. It can be replaced by {\tt enough} \tacindex{subst} \optindex{Regular Subst Tactic} -This tactic applies to a goal that has \ident\ in its context and -(at least) one hypothesis, say {\tt H}, of type {\tt - \ident=t} or {\tt t=\ident}. Then it replaces -\ident\ by {\tt t} everywhere in the goal (in the hypotheses -and in the conclusion) and clears \ident\ and {\tt H} from the context. +This tactic applies to a goal that has \ident\ in its context and (at +least) one hypothesis, say $H$, of type {\tt \ident} = $t$ or $t$ +{\tt = \ident} with {\ident} not occurring in $t$. Then it replaces +{\ident} by $t$ everywhere in the goal (in the hypotheses and in the +conclusion) and clears {\ident} and $H$ from the context. + +If {\ident} is a local definition of the form {\ident} := $t$, it is +also unfolded and cleared. \Rem -When several hypotheses have the form {\tt \ident=t} or {\tt - t=\ident}, the first one is used. +When several hypotheses have the form {\tt \ident} = $t$ or {\tt + $t$ = \ident}, the first one is used. + +\Rem +If $H$ is itself dependent in the goal, it is replaced by the +proof of reflexivity of equality. \begin{Variants} - \item {\tt subst \ident$_1$ \dots \ident$_n$} + \item {\tt subst \ident$_1$ {\dots} \ident$_n$} - Is equivalent to {\tt subst \ident$_1$; \dots; subst \ident$_n$}. + This is equivalent to {\tt subst \ident$_1$; \dots; subst \ident$_n$}. \item {\tt subst} - Applies {\tt subst} repeatedly to all identifiers from the context - for which an equality exists. + This applies {\tt subst} repeatedly from top to bottom to all + identifiers of the context for which an equality of the form {\tt + \ident} = $t$ or $t$ {\tt = \ident} or {\tt \ident} := $t$ exists, with + {\ident} not occurring in $t$. -\noindent {\bf Remark: } The behavior of {\tt subst} can be controlled using option {\tt Set - Regular Subst Tactic}. When this option is activated, {\tt subst} - manages the following corner cases which otherwise it - does not: +\noindent {\bf Remark: } The behavior of {\tt subst} can be controlled +using option {\tt Set Regular Subst Tactic}. When this option is +activated, {\tt subst} also deals with the following corner cases: \begin{itemize} \item A context with ordered hypotheses {\tt \ident$_1$ = \ident$_2$} and {\tt \ident$_1$ = $t$}, or {$t'$ = \ident$_1$} with $t'$ not a variable, and no other hypotheses of the form {\tt \ident$_2$ = $u$} - or {\tt $u$ = \ident$_2$} + or {\tt $u$ = \ident$_2$}; without the option, a second call to {\tt + subst} would be necessary to replace {\ident$_2$} by $t$ or $t'$ + respectively. + \item A context with cyclic dependencies as with hypotheses {\tt - \ident$_1$ = f~\ident$_2$} and {\tt \ident$_2$ = g~\ident$_1$} + \ident$_1$ = f~\ident$_2$} and {\tt \ident$_2$ = g~\ident$_1$} which + without the option would be a cause of failure of {\tt subst}. \end{itemize} -Additionally, it prevents a local definition such as {\tt \ident := - $t$} to be unfolded which otherwise it would exceptionally unfold in +Additionally, it prevents a local definition such as {\tt \ident} := + $t$ to be unfolded which otherwise it would exceptionally unfold in configurations containing hypotheses of the form {\tt {\ident} = $u$}, or {\tt $u'$ = \ident} with $u'$ not a variable. -The option is off by default. +Finally, it preserves the initial order of hypotheses, which without +the option it may break. + +The option is on by default. \end{Variants} |