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> --- doc/sphinx/proof-engine/tactics.rst | 20 ++++++++++++++++++++ doc/sphinx/proof-engine/vernacular-commands.rst | 4 +++- 2 files changed, 23 insertions(+), 1 deletion(-) (limited to 'doc/sphinx/proof-engine') 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 -- 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/sphinx/proof-engine') 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/sphinx/proof-engine') 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/sphinx/proof-engine') 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/sphinx/proof-engine') 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/sphinx/proof-engine') 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