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

5 files changed, 71 insertions, 16 deletions

diff --git a/dev/ci/user-overlays/10760-JasonGross-more-rapply.sh b/dev/ci/user-overlays/10760-JasonGross-more-rapply.sh
new file mode 100644
index 0000000000..c1cb1f15cd
--- /dev/null
+++ b/dev/ci/user-overlays/10760-JasonGross-more-rapply.sh
@@ -0,0 +1,7 @@
+if [ "$CI_PULL_REQUEST" = "10760" ] || [ "$CI_BRANCH" = "more-rapply" ]; then
+
+    math_classes_CI_BRANCH=fix-for-more-rapply-10760
+    math_classes_CI_REF=fix-for-more-rapply-10760
+    math_classes_CI_GITURL=https://github.com/JasonGross/math-classes
+
+fi
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
+  <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 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
diff --git a/test-suite/success/rapply.v b/test-suite/success/rapply.v
new file mode 100644
index 0000000000..5bc2322842
--- /dev/null
+++ b/test-suite/success/rapply.v
@@ -0,0 +1,22 @@
+Require Import Coq.Program.Tactics.
+
+Ltac test n :=
+  (*let __ := match goal with _ => idtac n end in*)
+  lazymatch n with
+  | O => let __ := match goal with _ => assert True by rapply I; clear end in
+         uconstr:(fun _ => I)
+  | S ?n'
+    => let lem := test n' in
+       let __ := match goal with _ => assert True by (unshelve rapply lem; try exact I); clear end in
+       uconstr:(fun _ : True => lem)
+  end.
+
+Goal True.
+  assert True by rapply I.
+  assert True by (unshelve rapply (fun _ => I); try exact I).
+  assert True by (unshelve rapply (fun _ _ => I); try exact I).
+  assert True by (unshelve rapply (fun _ _ _ => I); try exact I).
+  clear.
+  Time let __ := test 50 in idtac.
+  rapply I.
+Qed.
diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v
index 51c7fe81b9..06fc2f73b2 100644
--- a/theories/Program/Tactics.v
+++ b/theories/Program/Tactics.v
@@ -173,22 +173,13 @@ 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.
+
+(** The tactic [rapply] is a tactic notation so that it takes in uconstrs by default *)
+Tactic Notation "rapply" uconstr(p) := rapply p.
 
 (** Tactical [on_call f tac] applies [tac] on any application of [f] in the hypothesis or goal. *)