From 109e158a8c41b88d77bbda0ab62e8a1a7e38a7b5 Mon Sep 17 00:00:00 2001
From: "Anne C.A. Baanen" <vierkantor@vierkantor.com>
Date: Fri, 11 Oct 2024 10:34:11 +0200
Subject: [PATCH] feat(Tactic): `erw` tries `rw` first and warns if that
 succeeds

This PR adds a macro rule to the `erw` tactic that first tries `rw` at reducible transparency, and displays a "Try this:" if that succeeded. This should help us get rid of uselessly slow `erw`s.

This is a relatively simple implementation that does not verify if `erw` and `rw` would have resulted in the same exact rewrite. So it is possible that `erw` and `rw` both succeed but rewrite different occurrences, and there would be a suggestion to replace `erw` with `rw` in that case. I think the complication of running both at the same time and checking the goal state afterwards doesn't weigh up to accepting that this happens and adding an explanation to the warning generated by `erw`.

I import the `erw` extension in `Tactic.Common`: it might be nice to migrate this up even earlier in the import hierarchy but `Mathlib.Tactic.TryThis` is a somewhat heavy import to put in `Mathlib.Tactic.Core`.
---
 Mathlib.lean               |  1 +
 Mathlib/Tactic.lean        |  1 +
 Mathlib/Tactic/Common.lean |  1 +
 Mathlib/Tactic/Erw.lean    | 27 +++++++++++++++++++++++++++
 4 files changed, 30 insertions(+)
 create mode 100644 Mathlib/Tactic/Erw.lean

diff --git a/Mathlib.lean b/Mathlib.lean
index 3c455bcceb7e9..8ac1e19cbe1ce 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -4307,6 +4307,7 @@ import Mathlib.Tactic.DeriveFintype
 import Mathlib.Tactic.DeriveToExpr
 import Mathlib.Tactic.DeriveTraversable
 import Mathlib.Tactic.Eqns
+import Mathlib.Tactic.Erw
 import Mathlib.Tactic.Eval
 import Mathlib.Tactic.ExistsI
 import Mathlib.Tactic.Explode
diff --git a/Mathlib/Tactic.lean b/Mathlib/Tactic.lean
index cd494193a67b4..dfa931b9d17ed 100644
--- a/Mathlib/Tactic.lean
+++ b/Mathlib/Tactic.lean
@@ -69,6 +69,7 @@ import Mathlib.Tactic.DeriveFintype
 import Mathlib.Tactic.DeriveToExpr
 import Mathlib.Tactic.DeriveTraversable
 import Mathlib.Tactic.Eqns
+import Mathlib.Tactic.Erw
 import Mathlib.Tactic.Eval
 import Mathlib.Tactic.ExistsI
 import Mathlib.Tactic.Explode
diff --git a/Mathlib/Tactic/Common.lean b/Mathlib/Tactic/Common.lean
index f9c7a25eb782c..260891c52ef2a 100644
--- a/Mathlib/Tactic/Common.lean
+++ b/Mathlib/Tactic/Common.lean
@@ -47,6 +47,7 @@ import Mathlib.Tactic.DefEqTransformations
 import Mathlib.Tactic.DeprecateMe
 import Mathlib.Tactic.DeriveToExpr
 import Mathlib.Tactic.Eqns
+import Mathlib.Tactic.Erw
 import Mathlib.Tactic.ExistsI
 import Mathlib.Tactic.ExtractGoal
 import Mathlib.Tactic.ExtractLets
diff --git a/Mathlib/Tactic/Erw.lean b/Mathlib/Tactic/Erw.lean
new file mode 100644
index 0000000000000..b04db044c76e7
--- /dev/null
+++ b/Mathlib/Tactic/Erw.lean
@@ -0,0 +1,27 @@
+/-
+Copyright (c) 2024 Anne Baanen. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Anne Baanen
+-/
+
+import Mathlib.Tactic.TryThis
+
+/-!
+# Extension to the `erw` tactic
+
+This file adds a macro rule to the `erw` tactic that first tries to run the `rw` tactic at the
+faster `reducible` transparency, and adds a suggestion if that also succeeds.
+
+Note that `rw` succeeding is not the same as `rw` and `erw` doing exactly the same rewrite: they may
+have operated on different subterms. Since the suggested `rw` may not be an exact replacement, we
+display a hint explaining what to do if this happens.
+-/
+
+/-- If we call `erw`, first try running regular `rw` and warn if that succeds. -/
+macro_rules
+  | `(tactic| erw $s $(loc)?) =>
+    `(tactic|
+      try_this rw $(.none)? $s $(loc)?;
+      trace "Hint: `rw` succeeded here, but may have performed a different rewrite than `erw` would.
+If `erw` really is needed, try preceding this line with a `rw` to get rid of the other occurrences,
+or use `conv` to specify exactly which subterm to rewrite.")