From 7f71f0161bda7a0ed44d5f324ddd3823569f6df8 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Mon, 3 Jun 2024 13:12:48 +0200
Subject: [PATCH] fix: GuessLex: delaborate unused parameters as _

fixes #4230
---
 .../PreDefinition/WF/TerminationArgument.lean | 20 +++++++++--------
 tests/lean/run/4230.lean                      | 22 +++++++++++++++++++
 2 files changed, 33 insertions(+), 9 deletions(-)
 create mode 100644 tests/lean/run/4230.lean

diff --git a/src/Lean/Elab/PreDefinition/WF/TerminationArgument.lean b/src/Lean/Elab/PreDefinition/WF/TerminationArgument.lean
index 2d4478772544..73508ef1fbaa 100644
--- a/src/Lean/Elab/PreDefinition/WF/TerminationArgument.lean
+++ b/src/Lean/Elab/PreDefinition/WF/TerminationArgument.lean
@@ -86,21 +86,23 @@ def TerminationArgument.delab (termArg : TerminationArgument) : MetaM (TSyntax `
     let e ← mkLambdaFVars ys[termArg.arity - termArg.extraParams:] e -- undo overshooting by lambdaTelescope
     pure (← delabCore e (delab := go termArg.extraParams #[])).1
   where
-    go : Nat → TSyntaxArray [`ident, `Lean.Parser.Term.hole] → DelabM (TSyntax ``terminationBy)
+    go : Nat → TSyntaxArray `ident → DelabM (TSyntax ``terminationBy)
     | 0, vars => do
+      let stxBody ← Delaborator.delab
+      let hole : TSyntax `Lean.Parser.Term.hole ← `(hole|_)
+
+      -- any variable not mentioned syntatically (it may appear in the `Expr`, so do not just use
+      -- `e.bindingBody!.hasLooseBVar`) should be delaborated as a hole.
+      let vars  : TSyntaxArray [`ident, `Lean.Parser.Term.hole] :=
+        Array.map (fun (i : Ident) => if hasIdent i.getId stxBody then i else hole) vars
       -- drop trailing underscores
       let mut vars := vars
       while ! vars.isEmpty && vars.back.raw.isOfKind ``hole do vars := vars.pop
       if vars.isEmpty then
-        `(terminationBy|termination_by $(← Delaborator.delab))
+        `(terminationBy|termination_by $stxBody)
       else
-        `(terminationBy|termination_by $vars* => $(← Delaborator.delab))
+        `(terminationBy|termination_by $vars* => $stxBody)
     | i+1, vars => do
       let e ← getExpr
       unless e.isLambda do return ← go 0 vars -- should not happen
-
-      -- Delaborate unused parameters with `_`
-      if e.bindingBody!.hasLooseBVar 0 then
-        withBindingBodyUnusedName fun n => go i (vars.push ⟨n⟩)
-      else
-        descend e.bindingBody! 1 (go i (vars.push (← `(hole|_))))
+      withBindingBodyUnusedName fun n => go i (vars.push ⟨n⟩)
diff --git a/tests/lean/run/4230.lean b/tests/lean/run/4230.lean
new file mode 100644
index 000000000000..a4c84df478c5
--- /dev/null
+++ b/tests/lean/run/4230.lean
@@ -0,0 +1,22 @@
+def copy (curr : Nat) (input : Array Nat) (output : Array Nat) : Array Nat :=
+  if hcurr:curr < input.size then
+    copy (curr + 1) input (output.push (input[curr]'hcurr))
+  else
+    output
+termination_by input.size - curr
+
+/-- info: Try this: termination_by input.size - curr -/
+#guard_msgs(drop warning, info) in
+theorem foo (curr : Nat) (input : Array Nat) (output : Array Nat)
+    : ∀ (idx : Nat) (hidx1 : idx < curr),
+        (copy curr input output)[idx]'sorry
+          =
+        output[idx]'sorry := by
+  intro idx hidx
+  unfold copy
+  split
+  . rw [foo]
+    . rw [Array.get_push_lt]
+    . omega
+  . rfl
+termination_by?