fix: Let MVarId.cleanup chase local declarations (#10712)

This PR lets `MVarId.cleanup` chase local declarations (a bit as if they
were equalities). Fixes #10710.

src/Lean/Data/Json/Printer.lean

@@ -59,6 +59,7 @@ private def escapeAux (acc : String) (c : Char) : String :=
     let d4 := Nat.digitChar (n % 16)
     acc ++ "\\u" |>.push d1 |>.push d2 |>.push d3 |>.push d4
 
+set_option maxRecDepth 10240 in
 private def needEscape (s : String) : Bool :=
   go s 0
 where

src/Lean/Meta/Tactic/Cleanup.lean

@@ -6,10 +6,9 @@ Authors: Leonardo de Moura
 module
 
 prelude
-public import Lean.Meta.CollectFVars
-public import Lean.Meta.Tactic.Clear
-
-public section
+public import Lean.Meta.Basic
+import Lean.Meta.CollectFVars
+import Lean.Meta.Tactic.Clear
 
 namespace Lean.Meta
 
@@ -44,11 +43,15 @@ where
 
   /-- We include `p` in the used-set, if `p` is a proposition that contains a `x` that is in the used-set. -/
   collectPropsStep : StateRefT (Bool × FVarIdSet) MetaM Unit := do
-    let usedSet := (← get).2
     for localDecl in (← getLCtx) do
-      if (← isProp localDecl.type) then
-        if (← dependsOnPred localDecl.type usedSet.contains) then
-          addUsedFVar localDecl.fvarId
+      let usedSet := (← get).2
+      unless usedSet.contains localDecl.fvarId do
+        if (← isProp localDecl.type) then
+          if (← dependsOnPred localDecl.type usedSet.contains) then
+            addUsedFVar localDecl.fvarId
+        if let some v := localDecl.value? then
+          if (← dependsOnPred v usedSet.contains) then
+            addUsedFVar localDecl.fvarId
 
   collectProps : StateRefT (Bool × FVarIdSet) MetaM Unit := do
     modify fun s => (false, s.2)
@@ -69,11 +72,12 @@ where
   - It occurs in the target type, or
   - There is a relevant variable `y` that depends on `x`, or
   - If `indirectProps` is true, the type of `x` is a proposition and it depends on a relevant variable `y`.
+  - If `indirectProps` is true, `x` is a local declartation and its value mentions a relevant variable `y`.
 
   By default, `toPreserve := #[]` and `indirectProps := true`. These settings are used in the mathlib tactic `extract_goal`
   to give the user more control over which variables to include.
 -/
-@[inline] def _root_.Lean.MVarId.cleanup (mvarId : MVarId) (toPreserve : Array FVarId := #[]) (indirectProps : Bool := true) : MetaM MVarId := do
+@[inline] public def _root_.Lean.MVarId.cleanup (mvarId : MVarId) (toPreserve : Array FVarId := #[]) (indirectProps : Bool := true) : MetaM MVarId := do
   cleanupCore mvarId toPreserve indirectProps
 
 end Lean.Meta

tests/lean/run/issue10710.lean

@@ -0,0 +1,20 @@
+-- works
+#guard_msgs in
+def go (numDigits : Nat) : Nat :=
+  if 4*numDigits < 64 then
+    go (numDigits+1)
+  else
+    numDigits
+termination_by 64 - 4*numDigits
+
+-- set_option trace.Elab.definition.wf true
+-- set_option debug.rawDecreasingByGoal true
+
+#guard_msgs(pass trace, all) in
+def foo (numDigits : Nat) : Nat :=
+  let sz := 4*numDigits
+  if sz < 64 then
+    foo (numDigits+1)
+  else
+    numDigits
+termination_by 64 - 4*numDigits

tests/lean/run/issue2102.lean

@@ -35,6 +35,10 @@ failed to prove termination, possible solutions:
 T✝ : Type
 head✝ : T✝
 tl : List T✝
+x✝ :
+  (y : (T : Type) ×' List T) →
+    (invImage (fun x => PSigma.casesOn x fun T ls => sizeOf ls) sizeOfWFRel).1 y ⟨T✝, head✝ :: tl⟩ → Option (List y.1)
+res : Option { x // x✝ ⟨T✝, tl⟩ ⋯ = some x } := (x✝ ⟨T✝, tl⟩ ⋯).attach
 T : Type
 ls : List T
 ⊢ sizeOf ls < 1 + sizeOf tl
@@ -55,6 +59,10 @@ error: failed to prove termination, possible solutions:
 T✝ : Type
 head✝ : T✝
 tl : List T✝
+x✝ :
+  (y : (T : Type) ×' List T) →
+    (invImage (fun x => PSigma.casesOn x fun T ls => sizeOf ls) sizeOfWFRel).1 y ⟨T✝, head✝ :: tl⟩ → Option (List y.1)
+res : Option { x // x✝ ⟨T✝, tl⟩ ⋯ = some x } := (x✝ ⟨T✝, tl⟩ ⋯).attach
 T : Type
 ls : List T
 ⊢ sizeOf ls < 1 + sizeOf tl

tests/lean/run/wf_preprocess.lean

@@ -25,6 +25,7 @@ Checking that the attaches make their way through `let`s.
 /--
 trace: α : Type u_1
 t : Tree α
+v : α := t.val
 cs : List (Tree α) := t.cs
 t' : Tree α
 h✝ : t' ∈ cs