diff options
| -rw-r--r-- | doc/changelog/04-tactics/10760-more-rapply.rst | 7 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 22 | ||||
| -rw-r--r-- | test-suite/success/rapply.v | 27 | ||||
| -rw-r--r-- | theories/Program/Tactics.v | 30 |
4 files changed, 65 insertions, 21 deletions
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..2815f8af8a --- /dev/null +++ b/doc/changelog/04-tactics/10760-more-rapply.rst @@ -0,0 +1,7 @@ +- 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. (`#10760 + <https://github.com/coq/coq/pull/10760>`_, by Jason Gross) diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 878118c48a..53cfb973d4 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -688,6 +688,28 @@ 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. 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`. + .. tacv:: simple apply @term. This behaves like :tacn:`apply` but it reasons modulo conversion only on subterms diff --git a/test-suite/success/rapply.v b/test-suite/success/rapply.v new file mode 100644 index 0000000000..13efd986f0 --- /dev/null +++ b/test-suite/success/rapply.v @@ -0,0 +1,27 @@ +Require Import Coq.Program.Tactics. + +(** We make a version of [rapply] that takes [uconstr]; we do not +currently test what scope [rapply] interprets terms in. *) + +Tactic Notation "urapply" uconstr(p) := rapply p. + +Ltac test n := + (*let __ := match goal with _ => idtac n end in*) + lazymatch n with + | O => let __ := match goal with _ => assert True by urapply I; clear end in + uconstr:(fun _ => I) + | S ?n' + => let lem := test n' in + let __ := match goal with _ => assert True by (unshelve urapply lem; try exact I); clear end in + uconstr:(fun _ : True => lem) + end. + +Goal True. + assert True by urapply I. + assert True by (unshelve urapply (fun _ => I); try exact I). + assert True by (unshelve urapply (fun _ _ => I); try exact I). + assert True by (unshelve urapply (fun _ _ _ => I); try exact I). + clear. + Time let __ := test 50 in idtac. + urapply I. +Qed. diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v index ba8e4dff6d..c8a100b0e7 100644 --- a/theories/Program/Tactics.v +++ b/theories/Program/Tactics.v @@ -61,12 +61,12 @@ Ltac destruct_pairs := repeat (destruct_one_pair). Ltac destruct_one_ex := let tac H := let ph := fresh "H" in (destruct H as [H ph]) in - let tac2 H := let ph := fresh "H" in let ph' := fresh "H" in - (destruct H as [H ph ph']) + let tac2 H := let ph := fresh "H" in let ph' := fresh "H" in + (destruct H as [H ph ph']) in let tacT H := let ph := fresh "X" in (destruct H as [H ph]) in - let tacT2 H := let ph := fresh "X" in let ph' := fresh "X" in - (destruct H as [H ph ph']) + let tacT2 H := let ph := fresh "X" in let ph' := fresh "X" in + (destruct H as [H ph ph']) in match goal with | [H : (ex _) |- _] => tac H @@ -140,7 +140,7 @@ Ltac clear_dups := repeat clear_dup. (** Try to clear everything except some hyp *) -Ltac clear_except hyp := +Ltac clear_except hyp := repeat match goal with [ H : _ |- _ ] => match H with | hyp => fail 1 @@ -173,22 +173,10 @@ Ltac on_application f tac T := (** A variant of [apply] using [refine], doing as much conversion as necessary. *) Ltac rapply p := - refine (p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) || - refine (p _ _ _ _ _ _ _ _ _ _ _ _ _ _) || - refine (p _ _ _ _ _ _ _ _ _ _ _ _ _) || - refine (p _ _ _ _ _ _ _ _ _ _ _ _) || - refine (p _ _ _ _ _ _ _ _ _ _ _) || - refine (p _ _ _ _ _ _ _ _ _ _) || - refine (p _ _ _ _ _ _ _ _ _) || - refine (p _ _ _ _ _ _ _ _) || - refine (p _ _ _ _ _ _ _) || - refine (p _ _ _ _ _ _) || - refine (p _ _ _ _ _) || - refine (p _ _ _ _) || - refine (p _ _ _) || - refine (p _ _) || - refine (p _) || - refine p. + (** before we try to add more underscores, first ensure that adding such underscores is valid *) + (assert_succeeds (idtac; let __ := open_constr:(p _) in idtac); + rapply uconstr:(p _)) + || refine p. (** Tactical [on_call f tac] applies [tac] on any application of [f] in the hypothesis or goal. *) |