About "apply in":

- Added "simple apply in" (cf wish 1917) + conversion and descent
  under conjunction + contraction of useless beta-redex in "apply in"
  + support for open terms.
- Did not solve the "problem" that "apply in" generates a let-in which
  is type-checked using a kernel conversion in the opposite side of what
  the proof indicated (hence leading to a potential unexpected penalty
  at Qed time).
- When applyng a sequence of lemmas, it would have been nice to allow
  temporary evars as intermediate steps but this was too long to implement.

Smoother API in tactics.mli for assert_by/assert_as/pose_proof.



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

1 files changed, 32 insertions, 5 deletions

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index ba106e240..07d9df9c5 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -376,7 +376,7 @@ well-formed in the local context.  The tactic {\tt apply} tries to
 match the current goal against the conclusion of the type of {\term}.
 If it succeeds, then the tactic returns as many subgoals as the number
 of non dependent premises of the type of {\term}. If the conclusion of
-the type of {\term} does not match the goal {\tt and} the conclusion
+the type of {\term} does not match the goal {\em and} the conclusion
 is an inductive type isomorphic to a tuple type, then each component
 of the tuple is recursively matched to the goal in the left-to-right
 order.
@@ -656,19 +656,27 @@ in the list of subgoals remaining to prove.
 \end{Variants}
 
 \subsection{{\tt apply {\term} in {\ident}}
-\tacindex{apply {\ldots} in}}
+\tacindex{apply \ldots\ in}}
 
 This tactic applies to any goal.  The argument {\term} is a term
 well-formed in the local context and the argument {\ident} is an
 hypothesis of the context.  The tactic {\tt apply {\term} in {\ident}}
 tries to match the conclusion of the type of {\ident} against a non
-dependent premises of the type of {\term}, trying them from right to
+dependent premise of the type of {\term}, trying them from right to
 left.  If it succeeds, the statement of hypothesis {\ident} is
 replaced by the conclusion of the type of {\term}. The tactic also
 returns as many subgoals as the number of other non dependent premises
 in the type of {\term} and of the non dependent premises of the type
-of {\ident}.  The tactic {\tt apply} relies on first-order
-pattern-matching with dependent types.
+of {\ident}.  If the conclusion of the type of {\term} does not match
+the goal {\em and} the conclusion is an inductive type isomorphic to a
+tuple type, then the tuple is (recursively) decomposed and the first
+component of the tuple of which a non dependent premise matches the
+conclusion of the type of {\ident}. Tuples are decomposed in a
+width-first left-to-right order (for instance if the type of {\tt H1}
+is a \verb=A <-> B= statement, and the type of {\tt H2} is \verb=B=
+then {\tt apply H1 in H2} transforms the type of {\tt H2} into {\tt
+  B}). The tactic {\tt apply} relies on first-order pattern-matching
+with dependent types.
 
 \begin{ErrMsgs}
 \item \errindex{Statement without assumptions}
@@ -693,6 +701,7 @@ instantiate the parameters of the corresponding type of {\term}
 (see syntax of bindings in Section~\ref{Binding-list}).
 
 \item {\tt eapply \nelist{{\term} {\bindinglist}}{,} in {\ident}}
+\tacindex{eapply {\ldots} in}
 
 This works as {\tt apply \nelist{{\term} {\bindinglist}}{,} in
 {\ident}} but turns unresolved bindings into existential variables, if
@@ -709,6 +718,24 @@ This works as {\tt apply \nelist{{\term}{,} {\bindinglist}}{,} in
 
 This works as {\tt apply \nelist{{\term}{,} {\bindinglist}}{,} in {\ident} as {\disjconjintropattern}} but using {\tt eapply}.
 
+\item {\tt simple apply {\term} in {\ident}}
+\tacindex{simple apply {\ldots} in} 
+\tacindex{simple eapply {\ldots} in} 
+
+This behaves like {\tt apply {\term} in {\ident}} but it reasons
+modulo conversion only on subterms that contain no variables to
+instantiate. For instance, if {\tt id := fun x:nat => x} and {\tt H :
+  forall y, id y = y -> True} and {\tt H0 : O = O} then {\tt simple
+  apply H in H0} does not succeed because it would require the
+conversion of {\tt f ?y} and {\tt O} where {\tt ?y} is a variable to
+instantiate.  Tactic {\tt simple apply {\term} in {\ident}} does not
+either traverse tuples as {\tt apply {\term} in {\ident}} does.
+
+\item {\tt simple apply \nelist{{\term}{,} {\bindinglist}}{,} in {\ident} as {\disjconjintropattern}}\\
+{\tt simple eapply \nelist{{\term}{,} {\bindinglist}}{,} in {\ident} as {\disjconjintropattern}}
+
+This are the general forms of {\tt simple apply {\term} in {\ident}} and 
+{\tt simple eapply {\term} in {\ident}}.
 \end{Variants}
 
 \subsection{\tt generalize \term