fix: Fix/GuessLex: refine through more casesOnApp/matcherApp (#3176)

there was a check

if !Structural.recArgHasLooseBVarsAt recFnName fixedPrefixSize e then

that would avoid going through `.refineThrough`/`.addArg` for
matcher/casesOn applications. It seems it tries to detect when refining
the motive/param is pointless, but it was too eager, and cause confusion
with, for example, this reasonably reasonable function:

    def foo : (n : Nat) → (i : Fin n) → Bool
      | 0, _ => false
      | 1, _ => false
      | _+2, _ => foo 1 ⟨0, Nat.zero_lt_one⟩
    decreasing_by simp_wf; simp_arith

In particular, the `GuessLex` code later expects that the (implict)
`PProd.casesOn` in the implementation of `foo._unary` will refine the
paramter, because else the (rather picky) `unpackArg` fails. But it also
prevents this from being provable.

So let's try without this shortcut.

Fixing this also revealed that `withRecApps` wasn’t looking in all
corners
of a matcherApp/casesOnApp.

Fixes #3175

src/Lean/Elab/PreDefinition/WF/Fix.lean

@@ -79,9 +79,7 @@ where
     | Expr.app .. =>
       match (← matchMatcherApp? e) with
       | some matcherApp =>
-        if !Structural.recArgHasLooseBVarsAt recFnName fixedPrefixSize e then
-          processApp F e
-        else if let some matcherApp ← matcherApp.addArg? F then
+        if let some matcherApp ← matcherApp.addArg? F then
           if !(← Structural.refinedArgType matcherApp F) then
             processApp F e
           else
@@ -97,9 +95,7 @@ where
       | none =>
       match (← toCasesOnApp? e) with
       | some casesOnApp =>
-        if !Structural.recArgHasLooseBVarsAt recFnName fixedPrefixSize e then
-          processApp F e
-        else if let some casesOnApp ← casesOnApp.addArg? F (checkIfRefined := true) then
+        if let some casesOnApp ← casesOnApp.addArg? F (checkIfRefined := true) then
           let altsNew ← (Array.zip casesOnApp.alts casesOnApp.altNumParams).mapM fun (alt, numParams) =>
             lambdaTelescope alt fun xs altBody => do
               unless xs.size >= numParams do

src/Lean/Elab/PreDefinition/WF/GuessLex.lean

@@ -129,7 +129,7 @@ or `casesOn` application.
 -/
 partial def withRecApps {α} (recFnName : Name) (fixedPrefixSize : Nat) (param : Expr) (e : Expr)
     (k : Expr → Array Expr → MetaM α) : MetaM (Array α) := do
-  trace[Elab.definition.wf] "withRecApps: {indentExpr e}"
+  trace[Elab.definition.wf] "withRecApps (param {param}): {indentExpr e}"
   let (_, as) ← loop param e |>.run #[] |>.run' {}
   return as
 where
@@ -178,27 +178,24 @@ where
     | Expr.app .. =>
       match (← matchMatcherApp? e) with
       | some matcherApp =>
-        if !Structural.recArgHasLooseBVarsAt recFnName fixedPrefixSize e then
-          processApp param e
+        if let some altParams ← matcherApp.refineThrough? param then
+          matcherApp.discrs.forM (loop param)
+          (Array.zip matcherApp.alts (Array.zip matcherApp.altNumParams altParams)).forM
+            fun (alt, altNumParam, altParam) =>
+              lambdaTelescope altParam fun xs altParam => do
+                -- TODO: Use boundedLambdaTelescope
+                unless altNumParam = xs.size do
+                  throwError "unexpected `casesOn` application alternative{indentExpr alt}\nat application{indentExpr e}"
+                let altBody := alt.beta xs
+                loop altParam altBody
+          matcherApp.remaining.forM (loop param)
         else
-          if let some altParams ← matcherApp.refineThrough? param then
-            (Array.zip matcherApp.alts (Array.zip matcherApp.altNumParams altParams)).forM
-              fun (alt, altNumParam, altParam) =>
-                lambdaTelescope altParam fun xs altParam => do
-                  -- TODO: Use boundedLambdaTelescope
-                  unless altNumParam = xs.size do
-                    throwError "unexpected `casesOn` application alternative{indentExpr alt}\nat application{indentExpr e}"
-                  let altBody := alt.beta xs
-                  loop altParam altBody
-          else
-            processApp param e
+          processApp param e
       | none =>
       match (← toCasesOnApp? e) with
       | some casesOnApp =>
-        if !Structural.recArgHasLooseBVarsAt recFnName fixedPrefixSize e then
-          processApp param e
-        else
-          if let some altParams ← casesOnApp.refineThrough? param then
+        if let some altParams ← casesOnApp.refineThrough? param then
+          loop param casesOnApp.major
           (Array.zip casesOnApp.alts (Array.zip casesOnApp.altNumParams altParams)).forM
             fun (alt, altNumParam, altParam) =>
               lambdaTelescope altParam fun xs altParam => do
@@ -207,8 +204,10 @@ where
                   throwError "unexpected `casesOn` application alternative{indentExpr alt}\nat application{indentExpr e}"
                 let altBody := alt.beta xs
                 loop altParam altBody
-          else
-            processApp param e
+          casesOnApp.remaining.forM (loop param)
+        else
+          trace[Elab.definition.wf] "withRecApps: casesOnApp.refineThrough? failed"
+          processApp param e
       | none => processApp param e
     | e => do
       let _ ← ensureNoRecFn recFnName e
@@ -294,6 +293,7 @@ def collectRecCalls (unaryPreDef : PreDefinition) (fixedPrefixSize : Nat) (ariti
       unless args.size ≥ fixedPrefixSize + 1 do
         throwError "Insufficient arguments in recursive call"
       let arg := args[fixedPrefixSize]!
+      trace[Elab.definition.wf] "collectRecCalls: {unaryPreDef.declName} ({param}) → {unaryPreDef.declName} ({arg})"
       let (caller, params) ← unpackArg arities param
       let (callee, args) ← unpackArg arities arg
       RecCallWithContext.create (← getRef) caller params callee args

tests/lean/run/issue3175.lean

@@ -0,0 +1,12 @@
+def foo : (n : Nat) → (i : Fin n) → Bool
+  | 0, _ => false
+  | 1, _ => false
+  | _+2, _ => foo 1 ⟨0, Nat.zero_lt_one⟩
+decreasing_by simp_wf; simp_arith
+
+def bar : (n : Nat) → (i : Fin n) → Bool
+  | 0, _ => false
+  | 1, _ => false
+  | _+2, _ => bar 1 ⟨0, Nat.zero_lt_one⟩
+termination_by n i => n
+decreasing_by simp_wf; simp_arith

tests/lean/treeMap.lean.expected.out

@@ -2,5 +2,7 @@ treeMap.lean:8:59-8:69: 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
-t✝ t : TreeNode
-⊢ sizeOf t < sizeOf t✝
+name : String
+children : List TreeNode
+t : TreeNode
+⊢ sizeOf t < 1 + sizeOf name + sizeOf children