From 6d6729763f02feb9abaaedd1842885609c04790d Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 13 Dec 2024 20:58:54 +0100
Subject: [PATCH] add 'notypeclasses apply' tactic

---
 CHANGELOG.md                  |  2 ++
 stdpp/tactics.v               |  6 ++++++
 stdpp_bitvector/definitions.v |  2 +-
 tests/tactics.ref             | 22 ++++++++++++++++++++++
 tests/tactics.v               | 16 ++++++++++++++++
 5 files changed, 47 insertions(+), 1 deletion(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index ca42db36..8106f8d2 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -7,6 +7,8 @@ API-breaking change is listed.
 - Add lemma `lookup_total_fmap`.
 - Add lemmas about `last` and `head`: `last_app_Some`, `last_app_None`,
   `head_app_Some`, `head_app_None` and `head_app`. (by Marijn van Wezel)
+- Add tactic `notypeclasses apply` that works like `notypeclasses refine` but
+  automatically adds `_` until the given lemma takes no more arguments.
 
 ## std++ 1.11.0 (2024-10-30)
 
diff --git a/stdpp/tactics.v b/stdpp/tactics.v
index f838bf02..dd2c1598 100644
--- a/stdpp/tactics.v
+++ b/stdpp/tactics.v
@@ -736,6 +736,12 @@ Tactic Notation "ospecialize" "*" uconstr(p) :=
       pose proof p as H'; clear H; rename H' into H
   )).
 
+(** Tactic that works like [notypeclasses refine] but automatically determines
+the right number of [_]. This is *not* goal-directed, it will add [_] until the
+given term no longer has a function type (determined via syntactic matching). *)
+Tactic Notation "notypeclasses" "apply" uconstr(p) :=
+  opose_specialize_foralls_core p () ltac:(fun p => notypeclasses refine p).
+
 (** The block definitions are taken from [Coq.Program.Equality] and can be used
 by tactics to separate their goal from hypotheses they generalize over. *)
 Definition block {A : Type} (a : A) := a.
diff --git a/stdpp_bitvector/definitions.v b/stdpp_bitvector/definitions.v
index af709612..36a1b738 100644
--- a/stdpp_bitvector/definitions.v
+++ b/stdpp_bitvector/definitions.v
@@ -755,7 +755,7 @@ Global Hint Resolve bv_wrap_simplify_mul | 10 : bv_wrap_simplify_db.
  tries to simplify them by removing any [bv_wrap] inside z1. *)
 Ltac bv_wrap_simplify_left :=
   lazymatch goal with |- bv_wrap _ _ = _ => idtac end;
-  etrans; [ notypeclasses refine (bv_wrap_simplify_proof _ _ _);
+  etrans; [ notypeclasses apply bv_wrap_simplify_proof;
             typeclasses eauto with bv_wrap_simplify_db | ]
 .
 
diff --git a/tests/tactics.ref b/tests/tactics.ref
index 8004020e..439f7902 100644
--- a/tests/tactics.ref
+++ b/tests/tactics.ref
@@ -65,5 +65,27 @@ use opose proof instead.
   H' : even n
   ============================
   even n
+"notypeclasses_apply_test"
+     : string
+1 goal
+  
+  n : nat
+  ============================
+  Decision (n = 0)
+1 goal
+  
+  n : nat
+  ============================
+  Decision (n = 0)
+"notypeclasses_apply_error"
+     : string
+The command has indeed failed with message:
+In environment
+P, Q : Prop
+H : P → Q
+HQ : Q
+opose_internal : P
+The term "H opose_internal" has type "Q" while it is expected to have type
+ "P".
 The command has indeed failed with message:
 No such assumption.
diff --git a/tests/tactics.v b/tests/tactics.v
index 2e755290..990bccb0 100644
--- a/tests/tactics.v
+++ b/tests/tactics.v
@@ -234,6 +234,22 @@ Proof.
   done.
 Qed.
 
+Check "notypeclasses_apply_test".
+Lemma notypeclasses_apply_test n : {n = 0} + {¬ n = 0}.
+Proof.
+  (* Partially applied lemma with typeclass in one of the trailing [_]. *)
+  notypeclasses apply (@decide (n = 0)). Show.
+Restart. Proof.
+  (* Partially applied lemma with typeclass in one of the explicit [_]. *)
+  notypeclasses apply (@decide (n = 0) _). Show.
+Abort.
+
+Check "notypeclasses_apply_error".
+Lemma notypeclasses_apply_error (P Q : Prop) : (P → Q) → Q → P.
+Proof.
+  intros H HQ. Fail notypeclasses apply H.
+Abort.
+
 (** Some tests for f_equiv. *)
 (* Similar to [f_equal], it should solve goals by [reflexivity]. *)
 Lemma test_f_equiv_refl {A} (R : relation A) `{!Equivalence R} x :
-- 
GitLab