From b09444fdaee1cf608dd40465d5e400fbd46ef6ad Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 16 Sep 2019 19:19:07 -0400 Subject: Make rapply handle all numbers of underscores Also add a tactic notation so that it takes in uconstrs by default. Also add some basic tests for `rapply`. Also document rapply in the manual --- doc/changelog/04-tactics/10760-more-rapply.rst | 19 +++++++++++++++++++ doc/sphinx/proof-engine/tactics.rst | 16 ++++++++++++++++ 2 files changed, 35 insertions(+) create mode 100644 doc/changelog/04-tactics/10760-more-rapply.rst (limited to 'doc') diff --git a/doc/changelog/04-tactics/10760-more-rapply.rst b/doc/changelog/04-tactics/10760-more-rapply.rst new file mode 100644 index 0000000000..e11a93d654 --- /dev/null +++ b/doc/changelog/04-tactics/10760-more-rapply.rst @@ -0,0 +1,19 @@ +- The tactic :tacn:`rapply` in :g:`Coq.Program.Tactics` now handles + arbitrary numbers of underscores and takes in a :g:`uconstr`. In + rare cases where users were relying on :tacn:`rapply` inserting + exactly 15 underscores and no more, due to the lemma having a + completely unspecified codomain (and thus allowing for any number of + underscores), the tactic will now instead loop. Additional + incompatibility may occur in cases where it was important to + interpret the lemma passed in to :tacn:`rapply` as a :g:`constr` + (thus failing on unresolved holes and resolving typeclasses before + adding arguments) before refining with it. Users may work around + this by replacing all invocations of :tacn:`rapply` with the + qualified :g:`Tactics.rapply` to get the underlying tactic rather + than the tactic notation. Finally, any users who defined their own + tactic :tacn:`rapply` and also imported :g:`Coq.Program.Tactics` may + see incompatibilities due to the fact that :g:`Coq.Program.Tactics` + now defines an :tacn:`rapply` as a :cmd:`Tactic Notation`. Users + can work around this by defining their :tacn:`rapply` as a + :cmd:`Tactic Notation` as well. (`#10760 + `_, by Jason Gross) diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 4f903d5776..843a8933be 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -685,6 +685,22 @@ Applying theorems instantiate (see :ref:`Existential-Variables`). The instantiation is intended to be found later in the proof. + .. tacv:: rapply @term + :name: rapply + + The tactic :tacn:`rapply` behaves like :tacn:`eapply` but it + uses the proof engine of :tacn:`refine` for dealing with + existential variables, holes, and conversion problems. This may + result in slightly different behavior regarding which conversion + problems are solvable. Note that :tacn:`rapply` prefers to + instantiate as many hypotheses of :n:`@term` as possible. As a + result, if it is possible to apply :n:`@term` to arbitrarily + many arguments without getting a type error, :tacn:`rapply` will + loop. + + Note that you need to :n:`Require Import Coq.Program.Tactics` to + make use of :tacn:`rapply`. + .. tacv:: simple apply @term. This behaves like :tacn:`apply` but it reasons modulo conversion only on subterms -- cgit v1.2.3 From 8d9afb9c459ed7affdf6c0752ff6397e0281e0c3 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 19 Sep 2019 16:31:33 -0400 Subject: Remove `rapply` tactic notation in favor of just the tactic This increases backwards compatibility. If desired, we can add a tactic notation to simplify the spec of `rapply` in the future if we want. --- doc/changelog/04-tactics/10760-more-rapply.rst | 14 +------------- doc/sphinx/proof-engine/tactics.rst | 16 +++++++++++----- 2 files changed, 12 insertions(+), 18 deletions(-) (limited to 'doc') diff --git a/doc/changelog/04-tactics/10760-more-rapply.rst b/doc/changelog/04-tactics/10760-more-rapply.rst index e11a93d654..2815f8af8a 100644 --- a/doc/changelog/04-tactics/10760-more-rapply.rst +++ b/doc/changelog/04-tactics/10760-more-rapply.rst @@ -3,17 +3,5 @@ rare cases where users were relying on :tacn:`rapply` inserting exactly 15 underscores and no more, due to the lemma having a completely unspecified codomain (and thus allowing for any number of - underscores), the tactic will now instead loop. Additional - incompatibility may occur in cases where it was important to - interpret the lemma passed in to :tacn:`rapply` as a :g:`constr` - (thus failing on unresolved holes and resolving typeclasses before - adding arguments) before refining with it. Users may work around - this by replacing all invocations of :tacn:`rapply` with the - qualified :g:`Tactics.rapply` to get the underlying tactic rather - than the tactic notation. Finally, any users who defined their own - tactic :tacn:`rapply` and also imported :g:`Coq.Program.Tactics` may - see incompatibilities due to the fact that :g:`Coq.Program.Tactics` - now defines an :tacn:`rapply` as a :cmd:`Tactic Notation`. Users - can work around this by defining their :tacn:`rapply` as a - :cmd:`Tactic Notation` as well. (`#10760 + underscores), the tactic will now instead loop. (`#10760 `_, by Jason Gross) diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 843a8933be..3994ff411c 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -692,11 +692,17 @@ Applying theorems uses the proof engine of :tacn:`refine` for dealing with existential variables, holes, and conversion problems. This may result in slightly different behavior regarding which conversion - problems are solvable. Note that :tacn:`rapply` prefers to - instantiate as many hypotheses of :n:`@term` as possible. As a - result, if it is possible to apply :n:`@term` to arbitrarily - many arguments without getting a type error, :tacn:`rapply` will - loop. + problems are solvable. However, like :tacn:`apply` but unlike + :tacn:`eapply`, :tacn:`rapply` will fail if there are any holes + which remain in :n:`@term` itself after typechecking and + typeclass resolution but before unification with the goal. More + technically, :n:`@term` is first parsed as a + :production:`constr` rather than as a :production:`uconstr` or + :production:`open_constr` before being applied to the goal. Note + that :tacn:`rapply` prefers to instantiate as many hypotheses of + :n:`@term` as possible. As a result, if it is possible to apply + :n:`@term` to arbitrarily many arguments without getting a type + error, :tacn:`rapply` will loop. Note that you need to :n:`Require Import Coq.Program.Tactics` to make use of :tacn:`rapply`. -- cgit v1.2.3