Added support for referring to subterms of the goal by pattern.

Tactics set/remember and destruct/induction take benefit of it.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14499 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 40 insertions, 22 deletions

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 200919b8c..e027794f8 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -591,6 +591,11 @@ hypotheses of the current goal and adds the new definition {\ident
 {\tt :=} \term} to the local context. The default is to make this
 replacement only in the conclusion.
 
+If {\term} has holes (i.e. subexpressions of the form ``\_''), the
+tactic first checks that all subterms matching the pattern are
+compatible before doing the replacement using the leftmost subterm
+matching the pattern.
+
 \begin{Variants}
 
 \item {\tt set (} {\ident} {\tt :=} {\term} {\tt ) in {\occgoalset}}
@@ -626,7 +631,7 @@ Section~\ref{Occurrences clauses}.
   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 )}}
+\item {\tt pose ( {\ident} := {\term} )}
   
   This adds the local definition {\ident} := {\term} to the current
   context without performing any replacement in the goal or in the
@@ -1619,18 +1624,16 @@ Section~\ref{Cic-inductive-definitions}).
 \subsection{\tt induction \term
 \tacindex{induction}}
 
-This tactic applies to any goal. The type of the argument {\term} must
-be an inductive constant. Then, the tactic {\tt induction}
-generates subgoals, one for each possible form of {\term}, i.e. one
-for each constructor of the inductive type.
+This tactic applies to any goal. The argument {\term} must be of
+inductive type and the tactic {\tt induction} generates subgoals,
+one for each possible form of {\term}, i.e. one for each constructor
+of the inductive type.
 
-The tactic {\tt induction} automatically replaces every occurrences
-of {\term} in the conclusion and the hypotheses of the goal.  It
-automatically adds induction hypotheses (using names of the form {\tt
-  IHn1}) to the local context. If some hypothesis must not be taken
-into account in the induction hypothesis, then it needs to be removed
-first (you can also use the tactics {\tt elim} or {\tt simple induction},
-see below).
+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 and induction
+hypotheses are added to the local context using names whose prefix is
+{\tt IH}.
 
 There are particular cases:
 
@@ -1642,10 +1645,13 @@ behaves as {\tt intros until {\ident}; 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.
+last introduced hypothesis. Remark: For simple induction on a numeral,
+use syntax {\tt induction ({\num})} (not very interesting anyway).
 
-\Rem For simple induction on a numeral, use syntax {\tt induction
-({\num})} (not very interesting anyway).
+\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
+  compatible and performs induction using this subterm.
 
 \end{itemize}
 
@@ -1833,10 +1839,19 @@ instantiate premises of the type of {\term$_2$}.
 \tacindex{destruct}}
 \label{destruct}
 
-The tactic {\tt destruct} is used to perform case analysis without
-recursion. Its behavior is similar to {\tt induction} except
-that no induction hypothesis is generated.  It applies to any goal and
-the type of {\term} must be inductively defined. There are particular cases:
+This tactic applies to any goal. The argument {\term} must be of
+inductive or coinductive type and the tactic generates subgoals, one
+for each possible form of {\term}, i.e. one for each constructor of
+the inductive or coinductive 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 coinductive structure of the argument.
+
+There are special cases:
 
 \begin{itemize}
 
@@ -1846,10 +1861,13 @@ behaves as {\tt intros until {\ident}; 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.
+last introduced hypothesis. Remark: For destruction of a numeral, use
+syntax {\tt destruct ({\num})} (not very interesting anyway).
 
-\Rem For destruction of a numeral, use syntax {\tt destruct
-({\num})} (not very interesting anyway).
+\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
+  compatible and performs case analysis using this subterm.
 
 \end{itemize}