add 'notypeclasses apply' tactic

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)
 

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.

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 | ]
 .
 

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.

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 :