From 2edbbfee7fdcfb2a4804524091930c5dab7b9db4 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sun, 19 Apr 2020 17:37:27 -0400 Subject: Add a `with_strategy` tactic Useful for guarding calls to `unfold` or `cbv` to ensure that, e.g., `Opaque foo` doesn't break some automation which tries to unfold `foo`. We have some timeouts in the strategy success file. We should not run into issues, because we are not really testing how long these take. We could just as well use `Timeout 60` or longer, we just want to make sure the file dies more quickly rather than taking over 10^100 steps. Note that this tactic does not play well with `abstract`; I have a potentially controversial change that fixes this issue. One of the lines in the doc comes from https://github.com/coq/coq/pull/12129#issuecomment-619771556 Co-Authored-By: Pierre-Marie Pédrot Co-Authored-By: Théo Zimmermann Co-Authored-By: Michael Soegtrop <7895506+MSoegtropIMC@users.noreply.github.com> --- .../04-tactics/12129-add-with-strategy.rst | 4 +++ doc/sphinx/proof-engine/tactics.rst | 20 +++++++++++ doc/sphinx/proof-engine/vernacular-commands.rst | 4 ++- doc/sphinx/user-extensions/syntax-extensions.rst | 41 ++++++++++++++++------ doc/tools/docgram/common.edit_mlg | 4 +++ doc/tools/docgram/fullGrammar | 21 +++++++---- doc/tools/docgram/orderedGrammar | 6 ++++ 7 files changed, 82 insertions(+), 18 deletions(-) create mode 100644 doc/changelog/04-tactics/12129-add-with-strategy.rst (limited to 'doc') diff --git a/doc/changelog/04-tactics/12129-add-with-strategy.rst b/doc/changelog/04-tactics/12129-add-with-strategy.rst new file mode 100644 index 0000000000..68558c0cf4 --- /dev/null +++ b/doc/changelog/04-tactics/12129-add-with-strategy.rst @@ -0,0 +1,4 @@ +- **Added:** + New tactical :tacn:`with_strategy` added which behaves like the + command :cmd:`Strategy`, with effects local to the given tactic + (`#12129 `_, by Jason Gross). diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 8989dd29ab..fd6b2b3846 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -3355,6 +3355,26 @@ the conversion in hypotheses :n:`{+ @ident}`. This is the most general syntax that combines the different variants. +.. tacn:: with_strategy @strategy_level_or_var [ {+ @smart_qualid } ] @ltac_expr3 + :name: with_strategy + + Executes :token:`ltac_expr3`, applying the alternate unfolding + behavior that the :cmd:`Strategy` command controls, but only for + :token:`ltac_expr3`. This can be useful for guarding calls to + reduction in tactic automation to ensure that certain constants are + never unfolded by tactics like :tacn:`simpl` and :tacn:`cbn` or to + ensure that unfolding does not fail. + + .. note:: + + Use this tactic with care, as effects do not persist past the + end of the proof script. Notably, this fine-tuning of the + conversion strategy is not in effect during :cmd:`Qed` nor + :cmd:`Defined`, so this tactic is most useful to guard + calls to conversion in tactic automation to ensure that, e.g., + :tacn:`unfold` does not fail just because the user made a + constant :cmd:`Opaque`. + Conversion tactics applied to hypotheses ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index 1759264e87..7191444bac 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -817,13 +817,15 @@ described first. .. cmd:: Strategy {+ @strategy_level [ {+ @smart_qualid } ] } - .. insertprodn strategy_level strategy_level + .. insertprodn strategy_level strategy_level_or_var .. prodn:: strategy_level ::= opaque | @int | expand | transparent + strategy_level_or_var ::= @strategy_level + | @ident This command accepts the :attr:`local` attribute, which limits its effect to the current section or module, in which case the section and module diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index d72409e0d9..ea5ad79a80 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -1714,6 +1714,11 @@ Tactic notations allow customizing the syntax of tactics. - a global reference of term - :tacn:`unfold` + * - ``smart_global`` + - :token:`smart_qualid` + - a global reference of term + - :tacn:`with_strategy` + * - ``constr`` - :token:`term` - a term @@ -1734,6 +1739,16 @@ Tactic notations allow customizing the syntax of tactics. - an integer - :tacn:`do` + * - ``strategy_level`` + - :token:`strategy_level` + - a strategy level + - + + * - ``strategy_level_or_var`` + - :token:`strategy_level_or_var` + - a strategy level + - :tacn:`with_strategy` + * - ``tactic`` - :token:`ltac_expr` - a tactic @@ -1766,18 +1781,24 @@ Tactic notations allow customizing the syntax of tactics. .. todo: notation doesn't support italics - .. note:: In order to be bound in tactic definitions, each syntactic - entry for argument type must include the case of a simple |Ltac| - identifier as part of what it parses. This is naturally the case for - ``ident``, ``simple_intropattern``, ``reference``, ``constr``, ... but not for ``integer``. - This is the reason for introducing a special entry ``int_or_var`` which - evaluates to integers only but which syntactically includes + .. note:: In order to be bound in tactic definitions, each + syntactic entry for argument type must include the case + of a simple |Ltac| identifier as part of what it + parses. This is naturally the case for ``ident``, + ``simple_intropattern``, ``reference``, ``constr``, ... + but not for ``integer`` nor for ``strategy_level``. This + is the reason for introducing special entries + ``int_or_var`` and ``strategy_level_or_var`` which + evaluate to integers or strategy levels only, + respectively, but which syntactically includes identifiers in order to be usable in tactic definitions. - .. note:: The *entry*\ ``_list*`` and ``ne_``\ *entry*\ ``_list*`` entries can be used in - primitive tactics or in other notations at places where a list of the - underlying entry can be used: entry is either ``constr``, ``hyp``, ``integer`` - or ``int_or_var``. + .. note:: The *entry*\ ``_list*`` and ``ne_``\ *entry*\ ``_list*`` + entries can be used in primitive tactics or in other + notations at places where a list of the underlying entry + can be used: entry is either ``constr``, ``hyp``, + ``integer``, ``smart_qualid``, ``strategy_level``, + ``strategy_level_or_var``, or ``int_or_var``. .. rubric:: Footnotes diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg index c7e3ee18ad..62cc8ea86b 100644 --- a/doc/tools/docgram/common.edit_mlg +++ b/doc/tools/docgram/common.edit_mlg @@ -1839,3 +1839,7 @@ sentence: [ document: [ | LIST0 sentence ] + +strategy_level: [ +| DELETE strategy_level0 +] diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar index 4274dccb40..92e9df51d5 100644 --- a/doc/tools/docgram/fullGrammar +++ b/doc/tools/docgram/fullGrammar @@ -451,6 +451,14 @@ bar_cbrace: [ | test_pipe_closedcurly "|" "}" ] +strategy_level: [ +| "expand" +| "opaque" +| integer +| "transparent" +| strategy_level0 +] + vernac_toplevel: [ | "Drop" "." | "Quit" "." @@ -1213,13 +1221,6 @@ more_implicits_block: [ | "{" LIST1 name "}" ] -strategy_level: [ -| "expand" -| "opaque" -| integer -| "transparent" -] - instance_name: [ | ident_decl binders | @@ -1598,6 +1599,7 @@ simple_tactic: [ | "guard" test | "decompose" "[" LIST1 constr "]" constr | "optimize_heap" +| "with_strategy" strategy_level_or_var "[" LIST1 smart_global "]" tactic3 | "eassumption" | "eexact" constr | "trivial" auto_using hintbases @@ -1855,6 +1857,11 @@ test_lpar_id_colon: [ | local_test_lpar_id_colon ] +strategy_level_or_var: [ +| strategy_level +| identref +] + comparison: [ | "=" | "<" diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index df4e5a22e3..11f06b7b8a 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/doc/tools/docgram/orderedGrammar @@ -659,6 +659,11 @@ strategy_level: [ | "transparent" ] +strategy_level_or_var: [ +| strategy_level +| ident +] + reserv_list: [ | LIST1 ( "(" simple_reserv ")" ) | simple_reserv @@ -1234,6 +1239,7 @@ simple_tactic: [ | "guard" int_or_var comparison int_or_var | "decompose" "[" LIST1 one_term "]" one_term | "optimize_heap" +| "with_strategy" strategy_level_or_var "[" LIST1 smart_qualid "]" ltac_expr3 | "start" "ltac" "profiling" | "stop" "ltac" "profiling" | "reset" "ltac" "profile" -- cgit v1.2.3 From 33388d18f0165369a565cd5ca5b6eb153899271e Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sun, 19 Apr 2020 18:04:14 -0400 Subject: Fix the `with_strategy` tactic to work with `abstract` --- doc/sphinx/proof-engine/tactics.rst | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'doc') diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index fd6b2b3846..b376d9177f 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -3370,7 +3370,9 @@ the conversion in hypotheses :n:`{+ @ident}`. Use this tactic with care, as effects do not persist past the end of the proof script. Notably, this fine-tuning of the conversion strategy is not in effect during :cmd:`Qed` nor - :cmd:`Defined`, so this tactic is most useful to guard + :cmd:`Defined`, so this tactic is most useful either in + combination with :tacn:`abstract`, which will check the proof + early while the fine-tuning is still in effect, or to guard calls to conversion in tactic automation to ensure that, e.g., :tacn:`unfold` does not fail just because the user made a constant :cmd:`Opaque`. -- cgit v1.2.3 From ee3b91fe06c72a8ffe92d31a7e40fe54cd71f746 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sat, 25 Apr 2020 13:33:39 -0400 Subject: Elaborate with_strategy warning As per https://github.com/coq/coq/pull/12129#issuecomment-619389803 Note that we need to work around #12179 in doc of with_strategy --- doc/sphinx/proof-engine/tactics.rst | 90 +++++++++++++++++++++++++++++++++++++ 1 file changed, 90 insertions(+) (limited to 'doc') diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index b376d9177f..06954b1fb0 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -3367,6 +3367,27 @@ the conversion in hypotheses :n:`{+ @ident}`. .. note:: + This tactic unfortunately does not yet play well with tactic + internalization, resulting in interpretation-time errors when + you try to use it directly with opaque identifiers, as seen in + the following example. This can be worked around by binding the + identifier to an |Ltac| variable, and this issue should + disappear in a future version of |Coq|; see + `#12179 `_. + + .. example:: + + .. coqtop:: all reset abort + + Opaque id. + Goal id 10 = 10. + Fail unfold id. + (** This should work, but does not *) + Fail with_strategy transparent [id] unfold id. + let id' := id in with_strategy transparent [id] unfold id'. + + .. warning:: + Use this tactic with care, as effects do not persist past the end of the proof script. Notably, this fine-tuning of the conversion strategy is not in effect during :cmd:`Qed` nor @@ -3377,6 +3398,75 @@ the conversion in hypotheses :n:`{+ @ident}`. :tacn:`unfold` does not fail just because the user made a constant :cmd:`Opaque`. + This can be illustrated with the following example involving the + factorial function. + + .. coqtop:: in reset + + Fixpoint fact (n : nat) : nat := + match n with + | 0 => 1 + | S n' => n * fact n' + end. + + Suppose now that, for whatever reason, we want in general to + unfold the :g:`id` function very late during conversion: + + .. coqtop:: in + + Strategy 1000 [id]. + + If we try to prove :g:`id (fact n) = fact n` by + :tacn:`reflexivity`, it will now take time proportional to + :math:`n!`, because |Coq| will keep unfolding :g:`fact` and + :g:`*` and :g:`+` before it unfolds :g:`id`, resulting in a full + computation of :g:`fact n` (in unary, because we are using + :g:`nat`), which takes time :math:`n!`. We can see this cross + the relevant threshold at around :math:`n = 9`: + + .. coqtop:: all abort + + Goal True. + Time assert (id (fact 8) = fact 8) by reflexivity. + Time assert (id (fact 9) = fact 9) by reflexivity. + + Note that behavior will be the same if you mark :g:`id` as + :g:`Opaque` because while most reduction tactics refuse to + unfold :g:`Opaque` constants, conversion treats :g:`Opaque` as + merely a hint to unfold this constant last. + + We can get around this issue by using :tacn:`with_strategy`: + + .. coqtop:: all + + Goal True. + Fail Timeout 1 assert (id (fact 100) = fact 100) by reflexivity. + Time assert (id (fact 100) = fact 100) by with_strategy -1 [id] reflexivity. + + However, when we go to close the proof, we will run into + trouble, because the reduction strategy changes are local to the + tactic passed to :tacn:`with_strategy`. + + .. coqtop:: all abort + + exact I. + Fail Timeout 1 Defined. + + We can fix this issue by using :tacn:`abstract`: + + .. coqtop:: all + + Goal True. + Time assert (id (fact 100) = fact 100) by with_strategy -1 [id] abstract reflexivity. + exact I. + Time Defined. + + On small examples this sort of behavior doesn't matter, but + because |Coq| is a super-linear performance domain in so many + places, unless great care is taken, tactic automation using + :tacn:`with_strategy` may not be robustly performant when + scaling the size of the input. + Conversion tactics applied to hypotheses ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -- cgit v1.2.3 From 452f809a580a29626aa36f5f7061aca12f9f458e Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sun, 26 Apr 2020 15:44:55 -0400 Subject: Work around a bug in Coq in the doc This is the bug https://github.com/coq/coq/pull/12129#issuecomment-619613779 --- doc/sphinx/proof-engine/tactics.rst | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'doc') diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 06954b1fb0..fa45e10104 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -3447,10 +3447,10 @@ the conversion in hypotheses :n:`{+ @ident}`. trouble, because the reduction strategy changes are local to the tactic passed to :tacn:`with_strategy`. - .. coqtop:: all abort + .. coqtop:: all abort fail exact I. - Fail Timeout 1 Defined. + Timeout 1 Defined. We can fix this issue by using :tacn:`abstract`: -- cgit v1.2.3 From adff7277ef2ba08802d355304b5fa358a0152ab6 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 27 Apr 2020 18:37:00 -0400 Subject: [with_strategy] Work around #12191 --- doc/sphinx/proof-engine/tactics.rst | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'doc') diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index fa45e10104..7483ab3341 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -3370,10 +3370,11 @@ the conversion in hypotheses :n:`{+ @ident}`. This tactic unfortunately does not yet play well with tactic internalization, resulting in interpretation-time errors when you try to use it directly with opaque identifiers, as seen in - the following example. This can be worked around by binding the + the first (failing) use of :tacn:`with_strategy` in the + following example. This can be worked around by binding the identifier to an |Ltac| variable, and this issue should - disappear in a future version of |Coq|; see - `#12179 `_. + disappear in a future version of |Coq|; see `#12179 + `_. .. example:: @@ -3382,7 +3383,6 @@ the conversion in hypotheses :n:`{+ @ident}`. Opaque id. Goal id 10 = 10. Fail unfold id. - (** This should work, but does not *) Fail with_strategy transparent [id] unfold id. let id' := id in with_strategy transparent [id] unfold id'. -- cgit v1.2.3 From 6b223d1d668ecb76aa2609b7d6bb8a19e13136cd Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sat, 9 May 2020 13:39:34 -0400 Subject: Revert "[with_strategy] Fix for coqchk" This reverts commit 3c66c60e52b334482bcfe3d1d97bb77e4d011d18. We instead add a warning in the manual and a kludge in the test-suite. --- doc/sphinx/proof-engine/tactics.rst | 10 ++++++++++ 1 file changed, 10 insertions(+) (limited to 'doc') diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 7483ab3341..bc2168411b 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -3467,6 +3467,16 @@ the conversion in hypotheses :n:`{+ @ident}`. :tacn:`with_strategy` may not be robustly performant when scaling the size of the input. + .. warning:: + + In much the same way this tactic does not play well with + :cmd:`Qed` and :cmd:`Defined` without using :tacn:`abstract` as + an intermediary, this tactic does not play well with ``coqchk``, + even when used with :tacn:`abstract`, due to the inability of + tactics to persist information about conversion hints in the + proof term. See `#12200 + `_ for more details. + Conversion tactics applied to hypotheses ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -- cgit v1.2.3