From d1174e10e694aa4f70b83b1a736bd106ee8d6987 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Thu, 15 Aug 2024 16:42:15 +0200
Subject: [PATCH] feat: always run clean_wf, even before decreasing_by (#5016)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Previously, the tactic state shown at `decreasing_by` would leak lots of
details about the translation, and mention `invImage`, `PSigma` etc.
This is not nice.

So this introduces `clean_wf`, which is like `simp_wf` but using
`simp`'s `only` mode, and runs this unconditionally. This should clean
up the goal to a reasonable extent.

Previously `simp_wf` was an unrestricted `simp […]` call, but we
probably don’t want arbitrary simplification to happen at this point, so
this now became `simp only` call. For backwards compatibility,
`decreasing_with` begins with `try simp`. The `simp_wf` tactic
is still available to not break too much existing code; it’s docstring
suggests to no longer use it.

With `set_option cleanDecreasingByGoal false` one can disable the use of
`clean_wf`. I hope this is only needed for debugging and understanding.

Migration advise: If your `decreasing_by` proof begins with `simp_wf`,
either remove that (if the proof still goes through), or replace with
`simp`.

I am a bit anxious about running even `simp only` unconditionally here,
as it may do more than some user might want, e.g. because of options
like `zetaDelta := true`. We'll see if we need to reign in this tactic
some more.

I wonder if in corner cases the `simp_wf` tactic might be able to close
the goal, and if that is a problem. If so, we may have to promote simp’s
internal `mayCloseGoal` parameter to a simp configuration option and use
that here.

fixes #4928
---
 src/Init/WFTactics.lean                      | 26 ++++++--
 src/Lean/Elab/PreDefinition/WF/Basic.lean    | 25 +++++++
 src/Lean/Elab/PreDefinition/WF/Fix.lean      |  3 +
 src/Lean/Elab/PreDefinition/WF/GuessLex.lean |  2 +
 tests/lean/decreasing_by.lean                | 25 +++----
 tests/lean/decreasing_by.lean.expected.out   | 42 ++++++------
 tests/lean/guessLex.lean                     |  8 +--
 tests/lean/guessLexDiff.lean                 | 10 +--
 tests/lean/guessLexTricky.lean               | 13 +---
 tests/lean/issue2981.lean.expected.out       |  7 +-
 tests/lean/mutwf1.lean                       |  2 -
 tests/lean/mutwf1.lean.expected.out          |  4 +-
 tests/lean/run/4928.lean                     | 69 ++++++++++++++++++++
 tests/lean/run/funind_tests.lean             |  4 +-
 tests/lean/run/issue3204.lean                |  4 +-
 tests/lean/run/mutwf3.lean                   |  3 -
 tests/lean/run/omega.lean                    |  2 +-
 tests/lean/run/splitList.lean                |  1 -
 tests/lean/run/wfEqns2.lean                  |  2 -
 tests/lean/run/wfEqns4.lean                  |  3 -
 tests/lean/run/wfEqnsIssue.lean              | 14 ----
 21 files changed, 170 insertions(+), 99 deletions(-)
 create mode 100644 src/Lean/Elab/PreDefinition/WF/Basic.lean
 create mode 100644 tests/lean/run/4928.lean

diff --git a/src/Init/WFTactics.lean b/src/Init/WFTactics.lean
index 3c970d083c..88f0dab18c 100644
--- a/src/Init/WFTactics.lean
+++ b/src/Init/WFTactics.lean
@@ -8,11 +8,26 @@ import Init.SizeOf
 import Init.MetaTypes
 import Init.WF
 
-/-- Unfold definitions commonly used in well founded relation definitions.
-This is primarily intended for internal use in `decreasing_tactic`. -/
+/--
+Unfold definitions commonly used in well founded relation definitions.
+
+Since Lean 4.12, Lean unfolds these definitions automatically before presenting the goal to the
+user, and this tactic should no longer be necessary. Calls to `simp_wf` can be removed or replaced
+by plain calls to `simp`.
+-/
 macro "simp_wf" : tactic =>
   `(tactic| try simp (config := { unfoldPartialApp := true, zetaDelta := true }) [invImage, InvImage, Prod.lex, sizeOfWFRel, measure, Nat.lt_wfRel, WellFoundedRelation.rel])
 
+/--
+This tactic is used internally by lean before presenting the proof obligations from a well-founded
+definition to the user via `decreasing_by`. It is not necessary to use this tactic manuall.
+-/
+macro "clean_wf" : tactic =>
+  `(tactic| simp
+     (config := { unfoldPartialApp := true, zetaDelta := true, failIfUnchanged := false })
+     only [invImage, InvImage, Prod.lex, sizeOfWFRel, measure, Nat.lt_wfRel,
+           WellFoundedRelation.rel, sizeOf_nat])
+
 /-- Extensible helper tactic for `decreasing_tactic`. This handles the "base case"
 reasoning after applying lexicographic order lemmas.
 It can be extended by adding more macro definitions, e.g.
@@ -36,12 +51,13 @@ macro_rules | `(tactic| decreasing_trivial_pre_omega) => `(tactic| apply Nat.pre
 macro_rules | `(tactic| decreasing_trivial_pre_omega) => `(tactic| apply Nat.pred_lt; assumption)  -- i-1 < i if i ≠ 0
 
 
-/-- Constructs a proof of decreasing along a well founded relation, by applying
-lexicographic order lemmas and using `ts` to solve the base case. If it fails,
+/-- Constructs a proof of decreasing along a well founded relation, by simplifying, then applying
+lexicographic order lemmas and finally using `ts` to solve the base case. If it fails,
 it prints a message to help the user diagnose an ill-founded recursive definition. -/
 macro "decreasing_with " ts:tacticSeq : tactic =>
  `(tactic|
-   (simp_wf
+   (clean_wf -- remove after next stage0 update
+    try simp
     repeat (first | apply Prod.Lex.right | apply Prod.Lex.left)
     repeat (first | apply PSigma.Lex.right | apply PSigma.Lex.left)
     first
diff --git a/src/Lean/Elab/PreDefinition/WF/Basic.lean b/src/Lean/Elab/PreDefinition/WF/Basic.lean
new file mode 100644
index 0000000000..3141da43d3
--- /dev/null
+++ b/src/Lean/Elab/PreDefinition/WF/Basic.lean
@@ -0,0 +1,25 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joachim Breitner
+-/
+
+prelude
+import Lean.Elab.Tactic.Basic
+
+namespace Lean.Elab.WF
+
+register_builtin_option cleanDecreasingByGoal : Bool := {
+  defValue := true
+  descr    := "Cleans up internal implementation details in the proof goals presented by \
+              `decreasing_by`, using the `clean_wf` tactic. Can be disabled for debugging \
+              purposes. Please report an issue if you have to disable this option."
+}
+
+open Lean Elab Tactic
+
+def applyCleanWfTactic : TacticM Unit := do
+  if cleanDecreasingByGoal.get (← getOptions) then
+    Tactic.evalTactic (← `(tactic| all_goals clean_wf))
+
+end Lean.Elab.WF
diff --git a/src/Lean/Elab/PreDefinition/WF/Fix.lean b/src/Lean/Elab/PreDefinition/WF/Fix.lean
index 50fb59c6d3..82a51e07ff 100644
--- a/src/Lean/Elab/PreDefinition/WF/Fix.lean
+++ b/src/Lean/Elab/PreDefinition/WF/Fix.lean
@@ -14,6 +14,7 @@ import Lean.Elab.RecAppSyntax
 import Lean.Elab.PreDefinition.Basic
 import Lean.Elab.PreDefinition.Structural.Basic
 import Lean.Elab.PreDefinition.Structural.BRecOn
+import Lean.Elab.PreDefinition.WF.Basic
 import Lean.Data.Array
 
 namespace Lean.Elab.WF
@@ -142,6 +143,7 @@ private partial def processPSigmaCasesOn (x F val : Expr) (k : (F : Expr) → (v
 
 private def applyDefaultDecrTactic (mvarId : MVarId) : TermElabM Unit := do
   let remainingGoals ← Tactic.run mvarId do
+    applyCleanWfTactic
     Tactic.evalTactic (← `(tactic| decreasing_tactic))
   unless remainingGoals.isEmpty do
     Term.reportUnsolvedGoals remainingGoals
@@ -202,6 +204,7 @@ def solveDecreasingGoals (argsPacker : ArgsPacker) (decrTactics : Array (Option
         goals.forM fun goal => pushInfoTree (.hole goal)
         let remainingGoals ← Tactic.run goals[0]! do
           Tactic.setGoals goals.toList
+          applyCleanWfTactic
           Tactic.withTacticInfoContext decrTactic.ref do
             Tactic.evalTactic decrTactic.tactic
         unless remainingGoals.isEmpty do
diff --git a/src/Lean/Elab/PreDefinition/WF/GuessLex.lean b/src/Lean/Elab/PreDefinition/WF/GuessLex.lean
index ad18706ae9..a0a23665bd 100644
--- a/src/Lean/Elab/PreDefinition/WF/GuessLex.lean
+++ b/src/Lean/Elab/PreDefinition/WF/GuessLex.lean
@@ -15,6 +15,7 @@ import Lean.Elab.RecAppSyntax
 import Lean.Elab.PreDefinition.Basic
 import Lean.Elab.PreDefinition.Structural.Basic
 import Lean.Elab.PreDefinition.TerminationArgument
+import Lean.Elab.PreDefinition.WF.Basic
 import Lean.Data.Array
 
 
@@ -445,6 +446,7 @@ def evalRecCall (decrTactic? : Option DecreasingBy) (callerMeasures calleeMeasur
         else do
           Lean.Elab.Term.TermElabM.run' do Term.withoutErrToSorry do
             let remainingGoals ← Tactic.run mvarId do Tactic.withoutRecover do
+              applyCleanWfTactic
               let tacticStx : Syntax ←
                 match decrTactic? with
                 | none => pure (← `(tactic| decreasing_tactic)).raw
diff --git a/tests/lean/decreasing_by.lean b/tests/lean/decreasing_by.lean
index 5adf883d9b..1a58fc6f17 100644
--- a/tests/lean/decreasing_by.lean
+++ b/tests/lean/decreasing_by.lean
@@ -19,11 +19,9 @@ namespace Ex1
 def foo (n m : Nat) : Nat := foo n (dec2 m) + foo (dec1 n) 100
 termination_by (n, m)
 decreasing_by
-  · simp_wf
-    apply Prod.Lex.right
+  · apply Prod.Lex.right
     apply dec2_lt
-  · simp_wf
-    apply Prod.Lex.left
+  · apply Prod.Lex.left
     apply dec1_lt
 
 end Ex1
@@ -35,11 +33,9 @@ namespace Ex2
 -- so this tactic script fails.
 def foo (n m : Nat) : Nat := foo n (dec2 m) + foo (dec1 n) 100 -- Error
 decreasing_by
-  · simp_wf
-    apply Prod.Lex.right
+  · apply Prod.Lex.right
     apply dec2_lt
-  · simp_wf
-    apply Prod.Lex.left
+  · apply Prod.Lex.left
     apply dec1_lt
 
 end Ex2
@@ -49,7 +45,6 @@ namespace Ex3
 def foo (n m : Nat) : Nat := foo n (dec2 m) + foo (dec1 n) 100
 termination_by (n, m)
 decreasing_by all_goals
-  simp_wf
   first
     | apply Prod.Lex.right
       apply dec2_lt
@@ -62,10 +57,9 @@ namespace Ex4
 
 -- Multiple goals, no termination_By
 -- This does work, because the tactic is flexible enough
--- (Not a recommended way; complex `decrasing_by` should go along with `termination_by`.)
+-- (Not a recommended way; complex `decreasing_by` should go along with `termination_by`.)
 def foo (n m : Nat) : Nat := foo n (dec2 m) + foo (dec1 n) 100 -- Error
 decreasing_by all_goals
-  simp_wf
   first
     | apply Prod.Lex.right
       apply dec2_lt
@@ -108,8 +102,7 @@ namespace Ex8
 def foo (n m : Nat) : Nat := foo n (dec2 m) + foo (dec1 n) 100
 termination_by (n, m)
 decreasing_by -- Error
-  · simp_wf
-    apply Prod.Lex.right
+  · apply Prod.Lex.right
     apply dec2_lt
 
 end Ex8
@@ -120,8 +113,7 @@ namespace Ex9
 -- Shows guess-lex matrix
 def foo (n m : Nat) : Nat := foo n (dec2 m) + foo (dec1 n) 100 -- Error
 decreasing_by
-  · simp_wf
-    apply Prod.Lex.right
+  · apply Prod.Lex.right
     apply dec2_lt
 
 end Ex9
@@ -132,7 +124,6 @@ namespace Ex10
 -- (If it would it would produce the wrong termination order and then we should see errors)
 def foo (n m : Nat) : Nat := foo (n - 1) (dec2 m)
 decreasing_by all_goals
-  · simp_wf
-    apply dec2_lt
+  · apply dec2_lt
 
 end Ex10
diff --git a/tests/lean/decreasing_by.lean.expected.out b/tests/lean/decreasing_by.lean.expected.out
index 9a05a03756..d1f488065d 100644
--- a/tests/lean/decreasing_by.lean.expected.out
+++ b/tests/lean/decreasing_by.lean.expected.out
@@ -1,45 +1,45 @@
-decreasing_by.lean:36:0-43:17: error: Could not find a decreasing measure.
+decreasing_by.lean:34:0-39:17: error: Could not find a decreasing measure.
 The arguments relate at each recursive call as follows:
 (<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
             n m
-1) 36:29-43 = ?
-2) 36:46-62 ? _
+1) 34:29-43 = ?
+2) 34:46-62 ? _
 Please use `termination_by` to specify a decreasing measure.
-decreasing_by.lean:66:0-73:19: error: Could not find a decreasing measure.
+decreasing_by.lean:61:0-67:19: error: Could not find a decreasing measure.
 The arguments relate at each recursive call as follows:
 (<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
             n m
-1) 66:29-43 = ?
-2) 66:46-62 ? _
+1) 61:29-43 = ?
+2) 61:46-62 ? _
 Please use `termination_by` to specify a decreasing measure.
-decreasing_by.lean:81:13-83:3: error: unexpected token 'end'; expected '{' or tactic
-decreasing_by.lean:81:0-81:13: error: unsolved goals
+decreasing_by.lean:75:13-77:3: error: unexpected token 'end'; expected '{' or tactic
+decreasing_by.lean:75:0-75:13: error: unsolved goals
 n m : Nat
-⊢ (invImage (fun x => PSigma.casesOn x fun n m => (n, m)) Prod.instWellFoundedRelation).1 ⟨n, dec2 m⟩ ⟨n, m⟩
+⊢ Prod.Lex (fun a₁ a₂ => a₁ < a₂) (fun a₁ a₂ => a₁ < a₂) (n, dec2 m) (n, m)
 
 n m : Nat
-⊢ (invImage (fun x => PSigma.casesOn x fun n m => (n, m)) Prod.instWellFoundedRelation).1 ⟨dec1 n, 100⟩ ⟨n, m⟩
-decreasing_by.lean:91:0-91:22: error: unsolved goals
+⊢ Prod.Lex (fun a₁ a₂ => a₁ < a₂) (fun a₁ a₂ => a₁ < a₂) (dec1 n, 100) (n, m)
+decreasing_by.lean:85:0-85:22: error: unsolved goals
 case a
 n m : Nat
-⊢ (invImage (fun x => PSigma.casesOn x fun n m => (n, m)) Prod.instWellFoundedRelation).1 ⟨n, dec2 m⟩ ⟨n, m⟩
+⊢ Prod.Lex (fun a₁ a₂ => a₁ < a₂) (fun a₁ a₂ => a₁ < a₂) (n, dec2 m) (n, m)
 
 n m : Nat
-⊢ (invImage (fun x => PSigma.casesOn x fun n m => (n, m)) Prod.instWellFoundedRelation).1 ⟨dec1 n, 100⟩ ⟨n, m⟩
-decreasing_by.lean:99:0-100:22: error: Could not find a decreasing measure.
+⊢ Prod.Lex (fun a₁ a₂ => a₁ < a₂) (fun a₁ a₂ => a₁ < a₂) (dec1 n, 100) (n, m)
+decreasing_by.lean:93:0-94:22: error: Could not find a decreasing measure.
 The arguments relate at each recursive call as follows:
 (<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
             n m
-1) 99:29-43 = ?
-2) 99:46-62 ? _
+1) 93:29-43 = ?
+2) 93:46-62 ? _
 Please use `termination_by` to specify a decreasing measure.
-decreasing_by.lean:110:0-113:17: error: unsolved goals
+decreasing_by.lean:104:0-106:17: error: unsolved goals
 n m : Nat
-⊢ (invImage (fun x => PSigma.casesOn x fun n m => (n, m)) Prod.instWellFoundedRelation).1 ⟨dec1 n, 100⟩ ⟨n, m⟩
-decreasing_by.lean:121:0-125:17: error: Could not find a decreasing measure.
+⊢ Prod.Lex (fun a₁ a₂ => a₁ < a₂) (fun a₁ a₂ => a₁ < a₂) (dec1 n, 100) (n, m)
+decreasing_by.lean:114:0-117:17: error: Could not find a decreasing measure.
 The arguments relate at each recursive call as follows:
 (<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
              n m
-1) 121:29-43 = ?
-2) 121:46-62 ? _
+1) 114:29-43 = ?
+2) 114:46-62 ? _
 Please use `termination_by` to specify a decreasing measure.
diff --git a/tests/lean/guessLex.lean b/tests/lean/guessLex.lean
index 0f92fe4246..ebb3c2cf40 100644
--- a/tests/lean/guessLex.lean
+++ b/tests/lean/guessLex.lean
@@ -207,10 +207,10 @@ def foo : Nat → Nat
   | n+1 =>
     if h : n < 42 then bar (42 - n) else 0
   -- termination_by x1 => x1
-  decreasing_by simp_wf; simp [OddNat3]; omega
+  decreasing_by simp; omega
 def bar (o : OddNat3) : Nat := if h : @id Nat o < 41 then foo (41 - @id Nat o) else 0
   -- termination_by sizeOf o
-  decreasing_by simp_wf; simp [id] at *; omega
+  decreasing_by simp [id] at *; omega
 end
 end MutualNotNat2
 
@@ -228,11 +228,11 @@ def foo : Nat → Nat
   | n+1 =>
     if h : n < 42 then bar (42 - n) else 0
   -- termination_by x1 => x1
-  decreasing_by simp_wf; simp [OddNat3]; omega
+  decreasing_by simp; omega
 def bar : OddNat3 → Nat
   | Nat.zero => 0
   | n+1 => if h : n < 41 then foo (40 - n) else 0
   -- termination_by x1 => sizeOf x1
-  decreasing_by simp_wf; omega
+  decreasing_by simp; omega
 end
 end MutualNotNat3
diff --git a/tests/lean/guessLexDiff.lean b/tests/lean/guessLexDiff.lean
index 9fc282521c..8351a2c0d2 100644
--- a/tests/lean/guessLexDiff.lean
+++ b/tests/lean/guessLexDiff.lean
@@ -56,11 +56,10 @@ def distinct (xs : Array Nat) : Bool :=
   loop 0 0
 
 -- This examples shows a limitation of our current `decreasing_tactic`.
--- Guesslex infers
--- termination_by (Array.size xs - i, i)
--- but because `decreasing_with` is using
+-- Guesslex infers `termination_by (Array.size xs - i, i)` but because `decreasing_with` is using
 --     repeat (first | apply Prod.Lex.right | apply Prod.Lex.left)
--- it cannot solve this goal. But if we leave the Prod.Lex-handling to omega, it works
+-- it cannot solve this goal. But if we leave the Prod.Lex-handling to omega, it works.
+-- See https://github.com/leanprover/lean4/issues/3906
 def weird (xs : Array Nat) (i : Nat) : Bool :=
   if _ : i < xs.size then
     if _ : 0 < i then
@@ -72,7 +71,8 @@ def weird (xs : Array Nat) (i : Nat) : Bool :=
       weird xs (i+1)
   else
     true
-decreasing_by all_goals simp_wf; omega
+decreasing_by all_goals (try simp only [Array.size_pop]); omega
+
 
 /--
 This checks
diff --git a/tests/lean/guessLexTricky.lean b/tests/lean/guessLexTricky.lean
index ac99981ead..556ef70d89 100644
--- a/tests/lean/guessLexTricky.lean
+++ b/tests/lean/guessLexTricky.lean
@@ -42,7 +42,6 @@ def prod (x y z : Nat) : Nat :=
 -- termination_by (y, 1, 0)
 decreasing_by
   all_goals
-    simp_wf
     search_lex solve
       | decreasing_trivial
       | apply Nat.bitwise_rec_lemma; assumption
@@ -50,19 +49,13 @@ decreasing_by
 def oprod (x y z : Nat) := eprod x (y - 1) (z + x)
 -- termination_by (y, 0, 1)
 decreasing_by
-  simp_wf
-  try -- the need for `try` here is fishy
-      -- the proof with explicit `termination_by` does not need it, so it should not throw
-      -- GuessLex off, but without `try` it does
-      -- This appeared after #4522, which made Nat.sub_le a simp lemma
-    search_lex solve
-      | decreasing_trivial
-      | apply Nat.bitwise_rec_lemma; assumption
+  search_lex solve
+    | decreasing_trivial
+    | apply Nat.bitwise_rec_lemma; assumption
 
 def eprod (x y z : Nat) := if y = 0 then z else prod (2 * x) (y / 2) z
 -- termination_by (y, 0, 0)
 decreasing_by
-  simp_wf
   search_lex solve
     | decreasing_trivial
     | apply Nat.bitwise_rec_lemma; assumption
diff --git a/tests/lean/issue2981.lean.expected.out b/tests/lean/issue2981.lean.expected.out
index 3ed6459f95..6551019d6c 100644
--- a/tests/lean/issue2981.lean.expected.out
+++ b/tests/lean/issue2981.lean.expected.out
@@ -3,10 +3,9 @@ Tactic is run (ideally only twice)
 Tactic is run (ideally only twice)
 Tactic is run (ideally only once, in most general context)
 n : Nat
-⊢ (invImage (fun x => x) instWellFoundedRelationOfSizeOf).1 n n.succ
+⊢ n < n.succ
 Tactic is run (ideally only twice, in most general context)
 Tactic is run (ideally only twice, in most general context)
 n : Nat
-⊢ sizeOf n < sizeOf n.succ
-n m : Nat
-⊢ (invImage (fun x => PSigma.casesOn x fun a a_1 => a) instWellFoundedRelationOfSizeOf).1 ⟨n, m + 1⟩ ⟨n.succ, m⟩
+⊢ n < n.succ
+n m : Nat ⊢ n < n.succ
diff --git a/tests/lean/mutwf1.lean b/tests/lean/mutwf1.lean
index a00c5f199f..7050a119e6 100644
--- a/tests/lean/mutwf1.lean
+++ b/tests/lean/mutwf1.lean
@@ -6,7 +6,6 @@ mutual
     | n, false => n + g n
   termination_by n b => (n, if b then 2 else 1)
   decreasing_by
-  all_goals simp_wf
   · apply Prod.Lex.right; decide
   · apply Prod.Lex.right; decide
 
@@ -17,7 +16,6 @@ mutual
       n
   termination_by (n, 0)
   decreasing_by
-  all_goals simp_wf
   apply Prod.Lex.left
   apply Nat.pred_lt
   done -- should fail
diff --git a/tests/lean/mutwf1.lean.expected.out b/tests/lean/mutwf1.lean.expected.out
index 7ac3508cd8..38e10798a9 100644
--- a/tests/lean/mutwf1.lean.expected.out
+++ b/tests/lean/mutwf1.lean.expected.out
@@ -1,9 +1,9 @@
-mutwf1.lean:23:2-23:6: error: unsolved goals
+mutwf1.lean:21:2-21:6: error: unsolved goals
 case h.a
 n : Nat
 h : n ≠ 0
 ⊢ n.sub 0 ≠ 0
-mutwf1.lean:33:22-33:29: error: failed to prove termination, possible solutions:
+mutwf1.lean:31:22-31:29: error: failed to prove termination, possible solutions:
   - Use `have`-expressions to prove the remaining goals
   - Use `termination_by` to specify a different well-founded relation
   - Use `decreasing_by` to specify your own tactic for discharging this kind of goal
diff --git a/tests/lean/run/4928.lean b/tests/lean/run/4928.lean
new file mode 100644
index 0000000000..67159a380d
--- /dev/null
+++ b/tests/lean/run/4928.lean
@@ -0,0 +1,69 @@
+/--
+error: tactic 'fail' failed
+x y : Nat
+⊢ x - 1 < x
+-/
+#guard_msgs in
+def g (x : Nat) (y : Nat) : Nat := g (x - 1) y
+termination_by x
+decreasing_by fail
+
+/--
+error: tactic 'fail' failed
+x : List Nat
+y : Nat
+⊢ sizeOf x.tail < sizeOf x
+-/
+#guard_msgs in
+def h (x : List Nat) (y : Nat) : Nat := h x.tail y
+termination_by x
+decreasing_by fail
+
+/--
+error: tactic 'fail' failed
+x : List Nat
+y : Nat
+⊢ x.tail.length < x.length
+-/
+#guard_msgs in
+def f (x : List Nat) (y : Nat) : Nat := f x.tail y
+termination_by x.length
+decreasing_by fail
+
+/--
+error: tactic 'fail' failed
+x : List Nat
+y : Nat
+⊢ x.tail.length < x.length
+-/
+#guard_msgs in
+mutual
+def f1 (x : List Nat) (y : Nat) : Nat := f2 x.tail y
+termination_by x.length
+decreasing_by fail
+def f2 (x : List Nat) (y : Nat) : Nat := f1 x.tail y
+termination_by x.length
+decreasing_by fail
+end
+
+/--
+error: tactic 'fail' failed
+x : List Nat
+y : Nat
+⊢ (invImage
+        (fun x =>
+          PSum.casesOn x (fun _x => PSigma.casesOn _x fun x y => x.length) fun _x =>
+            PSigma.casesOn _x fun x y => x.length)
+        instWellFoundedRelationOfSizeOf).1
+    (PSum.inr ⟨x.tail, y⟩) (PSum.inl ⟨x, y⟩)
+-/
+#guard_msgs in
+set_option cleanDecreasingByGoal false in
+mutual
+def g1 (x : List Nat) (y : Nat) : Nat := g2 x.tail y
+termination_by x.length
+decreasing_by fail
+def g2 (x : List Nat) (y : Nat) : Nat := g1 x.tail y
+termination_by x.length
+decreasing_by fail
+end
diff --git a/tests/lean/run/funind_tests.lean b/tests/lean/run/funind_tests.lean
index 98e4214486..4643df583c 100644
--- a/tests/lean/run/funind_tests.lean
+++ b/tests/lean/run/funind_tests.lean
@@ -495,9 +495,7 @@ def sum_below (n : Nat) (f : (i : Nat) → below n i → Nat) :=
 def foo (n : Nat) :=
   1 + sum_below n (fun i _ => foo i)
 termination_by n
-decreasing_by
-  simp_wf
-  simp [below_lt, *]
+decreasing_by simp [below_lt, *]
 
 /--
 info: GramSchmidt.foo.induct (motive : Nat → Prop) (case1 : ∀ (x : Nat), (∀ (i : Nat), below x i → motive i) → motive x)
diff --git a/tests/lean/run/issue3204.lean b/tests/lean/run/issue3204.lean
index 9a0309d801..e15c8c5033 100644
--- a/tests/lean/run/issue3204.lean
+++ b/tests/lean/run/issue3204.lean
@@ -4,7 +4,7 @@ def zero_out (arr : Array Nat) (i : Nat) : Array Nat :=
   else
     arr
 termination_by arr.size - i
-decreasing_by simp_wf; apply Nat.sub_succ_lt_self _ _ h
+decreasing_by simp; apply Nat.sub_succ_lt_self _ _ h
 
 -- set_option trace.Elab.definition true
 theorem size_zero_out (arr : Array Nat) (i : Nat) : (zero_out arr i).size = arr.size := by
@@ -14,4 +14,4 @@ theorem size_zero_out (arr : Array Nat) (i : Nat) : (zero_out arr i).size = arr.
     rw [Array.size_set]
   · rfl
 termination_by arr.size - i
-decreasing_by simp_wf; apply Nat.sub_succ_lt_self; assumption
+decreasing_by simp; apply Nat.sub_succ_lt_self; assumption
diff --git a/tests/lean/run/mutwf3.lean b/tests/lean/run/mutwf3.lean
index 91cd81b1fd..2480be7364 100644
--- a/tests/lean/run/mutwf3.lean
+++ b/tests/lean/run/mutwf3.lean
@@ -5,7 +5,6 @@ mutual
     | n, a, b => g a n b |>.1
   termination_by n _ _ => (n, 2)
   decreasing_by
-    simp_wf
     apply Prod.Lex.right
     decide
 
@@ -14,7 +13,6 @@ mutual
     | a, n, b => (h a b n, a)
   termination_by _ n _ => (n, 1)
   decreasing_by
-    simp_wf
     apply Prod.Lex.right
     decide
 
@@ -23,7 +21,6 @@ mutual
     | a, b, n+1 => f n a b
   termination_by _ _ n => (n, 0)
   decreasing_by
-    simp_wf
     apply Prod.Lex.left
     apply Nat.lt_succ_self
 end
diff --git a/tests/lean/run/omega.lean b/tests/lean/run/omega.lean
index c3c97f6990..56cbdf95a2 100644
--- a/tests/lean/run/omega.lean
+++ b/tests/lean/run/omega.lean
@@ -314,7 +314,7 @@ def List.permutationsAux.rec' {C : List α → List α → Sort v} (H0 : ∀ is,
   | t :: ts, is =>
       H1 t ts is (permutationsAux.rec' H0 H1 ts (t :: is)) (permutationsAux.rec' H0 H1 is [])
   termination_by ts is => (length ts + length is, length ts)
-  decreasing_by all_goals simp_wf; omega
+  decreasing_by all_goals simp; omega
 
 example {x y w z : Nat} (h : Prod.Lex (· < ·) (· < ·) (x + 1, y + 1) (w, z)) :
     Prod.Lex (· < ·) (· < ·) (x, y) (w, z) := by omega
diff --git a/tests/lean/run/splitList.lean b/tests/lean/run/splitList.lean
index 5d0229eb27..71b55047f2 100644
--- a/tests/lean/run/splitList.lean
+++ b/tests/lean/run/splitList.lean
@@ -78,7 +78,6 @@ def len : List α → Nat
 termination_by xs => xs.length
 decreasing_by
   all_goals
-    simp_wf
     have := splitList_length (fst ++ snd) (by simp_arith [h₁]) h₁
     subst h₂
     simp_arith [eq_of_heq h₃] at this |- ; simp [this]
diff --git a/tests/lean/run/wfEqns2.lean b/tests/lean/run/wfEqns2.lean
index 8909548bae..d820f16bee 100644
--- a/tests/lean/run/wfEqns2.lean
+++ b/tests/lean/run/wfEqns2.lean
@@ -6,7 +6,6 @@ def g (i j : Nat) : Nat :=
   | Nat.succ j => h i j
 termination_by (i + j, 0)
 decreasing_by
-  simp_wf
   · apply Prod.Lex.left
     apply Nat.lt_succ_self
 
@@ -16,7 +15,6 @@ def h (i j : Nat) : Nat :=
   | Nat.succ j => g i j
 termination_by (i + j, 1)
 decreasing_by
-  all_goals simp_wf
   · apply Prod.Lex.right
     decide
   · apply Prod.Lex.left
diff --git a/tests/lean/run/wfEqns4.lean b/tests/lean/run/wfEqns4.lean
index 9496a9ab40..3049aca83b 100644
--- a/tests/lean/run/wfEqns4.lean
+++ b/tests/lean/run/wfEqns4.lean
@@ -4,7 +4,6 @@ mutual
     | n, a, b => g a n b |>.1
   termination_by n _ _ => (n, 2)
   decreasing_by
-    simp_wf
     apply Prod.Lex.right
     decide
 
@@ -13,7 +12,6 @@ mutual
     | a, n, b => (h a b n, a)
   termination_by _ n _ => (n, 1)
   decreasing_by
-    simp_wf
     apply Prod.Lex.right
     decide
 
@@ -22,7 +20,6 @@ mutual
     | a, b, n+1 => f n a b
   termination_by _ _ n => (n, 0)
   decreasing_by
-    simp_wf
     apply Prod.Lex.left
     apply Nat.lt_succ_self
 end
diff --git a/tests/lean/run/wfEqnsIssue.lean b/tests/lean/run/wfEqnsIssue.lean
index 63b2429493..17c56e58d6 100644
--- a/tests/lean/run/wfEqnsIssue.lean
+++ b/tests/lean/run/wfEqnsIssue.lean
@@ -55,20 +55,6 @@ def Ctx.extend (x : α) : HList Γ → HList (α :: Γ) :=
 def Ctx.drop : HList (α :: Γ) → HList Γ
   | HList.cons a as => as
 
-macro_rules
-| `(tactic| decreasing_tactic) =>
- `(tactic|
-   (simp_wf
-    repeat (first | apply PSigma.Lex.right | apply PSigma.Lex.left)
-    simp [Nat.add_comm (n := 1), Nat.succ_add, Nat.mul_succ]
-    try apply Nat.lt_succ_of_le
-    repeat apply Nat.le_step
-    first
-    | repeat first | apply Nat.le_add_left | apply Nat.le_add_right_of_le
-    | assumption
-    all_goals apply Nat.le_refl
-))
-
 @[simp]
 def Stmt.mapCtx (f : HList Γ' → HList Γ) : Stmt m ω Γ Δ b c β → Stmt m ω Γ' Δ b c β
   | expr e => expr (e ∘ f)