From 70af80aad166bc54e4bbc80dfc9427cfee32aae6 Mon Sep 17 00:00:00 2001 From: herbelin Date: Tue, 9 Dec 2008 21:40:22 +0000 Subject: 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 --- doc/refman/RefMan-tac.tex | 37 ++++++++++++++++++++++++++++++++----- 1 file changed, 32 insertions(+), 5 deletions(-) (limited to 'doc') 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 -- cgit v1.2.3