From 17ec7a0c875014e5322f6098dcd2014072cde9d8 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Tue, 18 Oct 2016 14:23:23 +0200 Subject: Improve the documentation of eauto. Improve the description of what auto/eauto do. These two tactics rely on the simple version of apply/eapply. Since this simple version is available to the end user, it is better to mention it. See also the confusion that such description can create in the thread "Understanding auto" on Coq-Club. --- doc/refman/RefMan-tac.tex | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 5eb8cedd95..fc6d9c143c 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -3513,8 +3513,8 @@ intact. \texttt{auto} and \texttt{trivial} never fail. This tactic generalizes {\tt auto}. While {\tt auto} does not try resolution hints which would leave existential variables in the goal, -{\tt eauto} does try them (informally speaking, it uses {\tt eapply} -where {\tt auto} uses {\tt apply}). +{\tt eauto} does try them (informally speaking, it uses +{\tt simple eapply} where {\tt auto} uses {\tt simple apply}). As a consequence, {\tt eauto} can solve such a goal: \begin{coq_eval} @@ -3529,8 +3529,7 @@ eauto. Abort. \end{coq_eval} -Note that {\tt ex\_intro} should be declared as an -hint. +Note that {\tt ex\_intro} should be declared as a hint. \SeeAlso Section~\ref{Hints-databases} -- cgit v1.2.3 From 6791a37b4e4ba9be829959b419e37a96e2eb5b84 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Tue, 18 Oct 2016 16:51:21 +0200 Subject: Document info_auto. Now that this tactic has been fixed (commit 58d1381), it needed to get documented. --- doc/refman/RefMan-tac.tex | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index fc6d9c143c..dccd6f5907 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -3490,6 +3490,12 @@ hints of the database named {\tt core}. This combines the effects of the {\tt using} and {\tt with} options. +\item {\tt info\_auto} + + Behaves like {\tt auto} but shows the tactics it uses to solve the goal. + This variant is very useful for getting a better understanding of automation, + or to know what lemmas/assumptions were used. + \item {\tt trivial}\tacindex{trivial} This tactic is a restriction of {\tt auto} that is not recursive and -- cgit v1.2.3 From 8d77523f8883fae56a8a338060bb2a52b0fd566c Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Tue, 18 Oct 2016 16:56:58 +0200 Subject: Extending the doc with a general summary of auto variants. This way of giving the summary avoids redundancy as much as possible. It is helpful for the auto-completion of Company-Coq of @cpitclaudel. --- doc/refman/RefMan-tac.tex | 30 +++++++++++++++++++++++++----- 1 file changed, 25 insertions(+), 5 deletions(-) diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index dccd6f5907..49a5b7983a 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -3472,7 +3472,7 @@ hints of the database named {\tt core}. Uses the hint databases $\ident_1$ \dots\ $\ident_n$ in addition to the database {\tt core}. See Section~\ref{Hints-databases} for the list of pre-defined databases and the way to create or extend a - database. This option can be combined with the previous one. + database. \item {\tt auto with *} @@ -3486,16 +3486,18 @@ hints of the database named {\tt core}. $lemma_i$ is an inductive type, it is the collection of its constructors which is added as hints. -\item \texttt{auto using} \nterm{lemma}$_1$ {\tt ,} {\ldots} {\tt ,} \nterm{lemma}$_n$ with \ident$_1$ {\ldots} \ident$_n$ - - This combines the effects of the {\tt using} and {\tt with} options. - \item {\tt info\_auto} Behaves like {\tt auto} but shows the tactics it uses to solve the goal. This variant is very useful for getting a better understanding of automation, or to know what lemmas/assumptions were used. +\item {\tt \zeroone{info\_}auto \zeroone{\num}} \zeroone{{\tt using} \nterm{lemma}$_1$ + {\tt ,} {\ldots} {\tt ,} \nterm{lemma}$_n$} \zeroone{{\tt with} + \ident$_1$ {\ldots} \ident$_n$} + + This is the most general form, combining the various options. + \item {\tt trivial}\tacindex{trivial} This tactic is a restriction of {\tt auto} that is not recursive and @@ -3506,6 +3508,14 @@ hints of the database named {\tt core}. \item \texttt{trivial with *} +\item \texttt{trivial using} \nterm{lemma}$_1$ {\tt ,} {\ldots} {\tt ,} \nterm{lemma}$_n$ + +\item {\tt info\_trivial} + +\item {\tt \zeroone{info\_}trivial} \zeroone{{\tt using} \nterm{lemma}$_1$ + {\tt ,} {\ldots} {\tt ,} \nterm{lemma}$_n$} \zeroone{{\tt with} + \ident$_1$ {\ldots} \ident$_n$} + \end{Variants} \Rem {\tt auto} either solves completely the goal or else leaves it @@ -3537,6 +3547,16 @@ Abort. Note that {\tt ex\_intro} should be declared as a hint. +\begin{Variants} + +\item {\tt \zeroone{info\_}eauto \zeroone{\num}} \zeroone{{\tt using} \nterm{lemma}$_1$ + {\tt ,} {\ldots} {\tt ,} \nterm{lemma}$_n$} \zeroone{{\tt with} + \ident$_1$ {\ldots} \ident$_n$} + + The various options for eauto are the same as for auto. + +\end{Variants} + \SeeAlso Section~\ref{Hints-databases} \subsection{\tt autounfold with \ident$_1$ \mbox{\dots} \ident$_n$} -- cgit v1.2.3 From 5be957316c23db6366aefc246d1d24480aa2f1ea Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Wed, 19 Oct 2016 14:18:52 +0200 Subject: Making the doc of auto hints more precise. The doc of auto hints now mention again that sometimes a hint will be used with simple apply and sometimes it will be used with exact. It does not try to be fully precise in that we don't necessarily want to document the behaviors of auto that we might like to change. See also the discussion on commit 9227d6e. --- doc/refman/RefMan-tac.tex | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 49a5b7983a..263766b272 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -3709,11 +3709,12 @@ The {\hintdef} is one of the following expressions: the number of subgoals generated by {\tt simple apply {\term}}. %{\tt auto} actually uses a slightly modified variant of {\tt simple apply} with use_metas_eagerly_in_conv_on_closed_terms set to false - % Is it really needed? - %% In case the inferred type of \term\ does not start with a product - %% the tactic added in the hint list is {\tt exact {\term}}. In case - %% this type can however be reduced to a type starting with a product, - %% the tactic {\tt apply {\term}} is also stored in the hints list. + In case the inferred type of \term\ does not start with a product + the tactic added in the hint list is {\tt exact {\term}}. +% Actually, a slightly restricted version is used (no conversion on the head symbol) + In case + this type can however be reduced to a type starting with a product, + the tactic {\tt simple apply {\term}} is also stored in the hints list. If the inferred type of \term\ contains a dependent quantification on a variable which occurs only in the premisses of the type and not -- cgit v1.2.3 From 3a507c03c91efe67afa9f2dd51bf77c7af6df0f5 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Wed, 19 Oct 2016 18:09:36 +0200 Subject: Documenting Hint Resolve -> and <- variants. These variants are from 8.3 but were never documented except in CHANGES. --- doc/refman/RefMan-tac.tex | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 263766b272..11de4f35e0 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -3744,6 +3744,17 @@ The {\hintdef} is one of the following expressions: Adds each \texttt{Resolve} {\term$_i$}. + \item {\tt Resolve -> \term} + + Adds the left-to-right implication of an equivalence as a hint + (informally the hint will be used as {\tt apply <- \term}, + although as mentionned before, the tactic actually used is + a restricted version of apply). + + \item {\tt Resolve <- \term} + + Adds the right-to-left implication of an equivalence as a hint. + \end{Variants} \item \texttt{Immediate {\term}} -- cgit v1.2.3