From 6518578ec19e32e68ea061a804edf10f17f6b232 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

---
 stdpp/tactics.v               | 6 ++++++
 stdpp_bitvector/definitions.v | 2 +-
 tests/tactics.ref             | 7 +++++++
 tests/tactics.v               | 6 ++++++
 4 files changed, 20 insertions(+), 1 deletion(-)

diff --git a/stdpp/tactics.v b/stdpp/tactics.v
index f838bf02..038d0c74 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 is no longer a function type. *)
+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..02a77924 100644
--- a/tests/tactics.ref
+++ b/tests/tactics.ref
@@ -65,5 +65,12 @@ use opose proof instead.
   H' : even n
   ============================
   even n
+"notypeclasses_apply_test"
+     : string
+1 goal
+  
+  n : nat
+  ============================
+  Decision (n = 0)
 The command has indeed failed with message:
 No such assumption.
diff --git a/tests/tactics.v b/tests/tactics.v
index 2e755290..0df8646f 100644
--- a/tests/tactics.v
+++ b/tests/tactics.v
@@ -234,6 +234,12 @@ Proof.
   done.
 Qed.
 
+Check "notypeclasses_apply_test".
+Lemma notypeclasses_apply_test n : {n = 0} + {¬ n = 0}.
+Proof.
+  notypeclasses apply (@decide _). Show.
+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