diff options
| author | Hugo Herbelin | 2015-12-05 00:14:37 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2015-12-05 00:58:19 +0100 |
| commit | 387351b4c0ffeff65d8a7192f5073cfd4bd20f53 (patch) | |
| tree | d4a40c40d0f5c4db29be160f3ede1baeb3649e2b /doc | |
| parent | cbceffe424a6b4477eb822f3887776b587503cbd (diff) | |
Changing "destruct !hyp" into "destruct (hyp)" (and similarly for induction)
based on a suggestion of Guillaume M. (done like this in ssreflect).
This is actually consistent with the hack of using "destruct (1)" to
mean the term 1 by opposition to the use of "destruct 1" to mean the
first non-dependent hypothesis of the goal.
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 47 |
1 files changed, 20 insertions, 27 deletions
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 03c4f6a365..55b5f622ff 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -1531,25 +1531,27 @@ for each possible form of {\term}, i.e. one for each constructor of the inductive or co-inductive type. Unlike {\tt induction}, no induction hypothesis is generated by {\tt destruct}. -If the argument is dependent in either the conclusion or some -hypotheses of the goal, the argument is replaced by the appropriate -constructor form in each of the resulting subgoals, thus performing -case analysis. If non-dependent, the tactic simply exposes the -inductive or co-inductive structure of the argument. - There are special cases: \begin{itemize} \item If {\term} is an identifier {\ident} denoting a quantified -variable of the conclusion of the goal, then {\tt destruct {\ident}} -behaves as {\tt intros until {\ident}; destruct {\ident}}. + variable of the conclusion of the goal, then {\tt destruct {\ident}} + behaves as {\tt intros until {\ident}; destruct {\ident}}. If + {\ident} is not anymore dependent in the goal after application of + {\tt destruct}, it is erased (to avoid erasure, use + parentheses, as in {\tt destruct ({\ident})}). \item If {\term} is a {\num}, then {\tt destruct {\num}} behaves as {\tt intros until {\num}} followed by {\tt destruct} applied to the last introduced hypothesis. Remark: For destruction of a numeral, use syntax {\tt destruct ({\num})} (not very interesting anyway). +\item In case {\term} is an hypothesis {\ident} of the context, + and {\ident} is not anymore dependent in the goal after + application of {\tt destruct}, it is erased (to avoid erasure, use + parentheses, as in {\tt destruct ({\ident})}). + \item The argument {\term} can also be a pattern of which holes are denoted by ``\_''. In this case, the tactic checks that all subterms matching the pattern in the conclusion and the hypotheses are @@ -1626,14 +1628,6 @@ syntax {\tt destruct ({\num})} (not very interesting anyway). They combine the effects of the {\tt with}, {\tt as}, {\tt eqn:}, {\tt using}, and {\tt in} clauses. -\item{\tt destruct !{\ident}} - - This is a case when the destructed term is an hypothesis of the - context. The ``!'' modifier tells to keep the hypothesis in the - context after destruction. - - This applies also to the other form of {\tt destruct} and {\tt edestruct}. - \item{\tt case \term}\label{case}\tacindex{case} The tactic {\tt case} is a more basic tactic to perform case @@ -1699,14 +1693,22 @@ There are particular cases: \begin{itemize} \item If {\term} is an identifier {\ident} denoting a quantified -variable of the conclusion of the goal, then {\tt induction {\ident}} -behaves as {\tt intros until {\ident}; induction {\ident}}. + variable of the conclusion of the goal, then {\tt induction + {\ident}} behaves as {\tt intros until {\ident}; induction + {\ident}}. If {\ident} is not anymore dependent in the goal + after application of {\tt induction}, it is erased (to avoid + erasure, use parentheses, as in {\tt induction ({\ident})}). \item If {\term} is a {\num}, then {\tt induction {\num}} behaves as {\tt intros until {\num}} followed by {\tt induction} applied to the last introduced hypothesis. Remark: For simple induction on a numeral, use syntax {\tt induction ({\num})} (not very interesting anyway). +\item In case {\term} is an hypothesis {\ident} of the context, + and {\ident} is not anymore dependent in the goal after + application of {\tt induction}, it is erased (to avoid erasure, use + parentheses, as in {\tt induction ({\ident})}). + \item The argument {\term} can also be a pattern of which holes are denoted by ``\_''. In this case, the tactic checks that all subterms matching the pattern in the conclusion and the hypotheses are @@ -1821,15 +1823,6 @@ Show 2. einduction}. It combines the effects of the {\tt with}, {\tt as}, %%{\tt eqn:}, {\tt using}, and {\tt in} clauses. -\item{\tt induction !{\ident}} - - This is a case when the term on which to apply induction is an - hypothesis of the context. The ``!'' modifier tells to keep the - hypothesis in the context after induction. - - This applies also to the other form of {\tt induction} and {\tt - einduction}. - \item {\tt elim \term}\label{elim} This is a more basic induction tactic. Again, the type of the |
