feat: always run clean_wf, even before decreasing_by (#5016)

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

@@ -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

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

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

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

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

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.

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

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

tests/lean/guessLexTricky.lean

@@ -42,27 +42,20 @@ 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
 
 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

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

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

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