From af70e2de832246a13fc2298a76e141a34d3d3cd4 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 24 Mar 2025 17:58:04 +0100
Subject: [PATCH] remove notypeclasses apply; it is somehow very slow
---
CHANGELOG.md | 2 --
stdpp/tactics.v | 13 -------------
stdpp_bitvector/definitions.v | 2 +-
tests/tactics.ref | 15 +--------------
tests/tactics.v | 10 ----------
5 files changed, 2 insertions(+), 40 deletions(-)
diff --git a/CHANGELOG.md b/CHANGELOG.md
index 1d6391d9..96e4c169 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -7,8 +7,6 @@ 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.
- Rename `map_filter_empty_iff` to `map_empty_filter` and add
`map_empty_filter_1` and `map_empty_filter_2`. (by Michael Sammler)
- Add lemma about `zip_with`: `lookup_zip_with_None` and add lemmas for `zip`:
diff --git a/stdpp/tactics.v b/stdpp/tactics.v
index a7e8552d..f3a30dc5 100644
--- a/stdpp/tactics.v
+++ b/stdpp/tactics.v
@@ -738,19 +738,6 @@ 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 without any unfolding). *)
-Tactic Notation "notypeclasses" "apply" uconstr(p) :=
- opose_core p ltac:(fun p => evar_foralls p () ltac:(fun t => t)
- ltac:(fun p => notypeclasses refine p ||
- let T := type of p in
- lazymatch goal with |- ?G =>
- fail "the given term has type" T "while it is expected to have type" G
- end
- )
- ).
-
(** 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 36a1b738..af709612 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 apply bv_wrap_simplify_proof;
+ etrans; [ notypeclasses refine (bv_wrap_simplify_proof _ _ _);
typeclasses eauto with bv_wrap_simplify_db | ]
.
diff --git a/tests/tactics.ref b/tests/tactics.ref
index 5bf23c45..ab5fadcf 100644
--- a/tests/tactics.ref
+++ b/tests/tactics.ref
@@ -65,22 +65,9 @@ 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:
-Tactic failure: the given term has type Q while it is expected to have type
-P.
+The reference notypeclasses was not found in the current environment.
The command has indeed failed with message:
No such assumption.
diff --git a/tests/tactics.v b/tests/tactics.v
index 990bccb0..7e7271b3 100644
--- a/tests/tactics.v
+++ b/tests/tactics.v
@@ -234,16 +234,6 @@ 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.
--
GitLab