fix: Float RecApp out of applications (#2818)

This didn't work before
```
def f (n : Nat) : Nat :=
  match n with
  | 0 => 0
  | n + 1 => (f) n
```
because the `RecApp` metadata marker gets in the way. More practically
relevant, such code is to be produced when using `rw` or `simp` in
recursive theorems (see included test case).

We can fix this by preprocessing the definitions and floating the
`.mdata` marker out of applications.

For structural recursion, there already exists a `preprocess` function;
this now also floats out `.mdata` markers.

For well-founded recursion, this introduces an analogous `preprocess`
function.

Fixes #2810.

One test case output changes: With the `.mdata` out of the way, we get a
different error message. Seems fine.

Alternative approaches are:

* Leaving the `.mdata` marker where it is, and looking around it.
  Tried in #2813, but not nice (many many places where `withApp` etc.
  need to be adjusted).
* Moving the `.mdata` _inside_ the application, so that `withApp` still
  works. Tried in #2814. Also not nice, the invariant that the `.mdata`
  is around the `.const` is tedious to maintain.

src/Lean/Elab/PreDefinition/Structural/Preprocess.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 import Lean.Meta.Transform
+import Lean.Elab.RecAppSyntax
 
 namespace Lean.Elab.Structural
 open Meta
@@ -15,21 +16,39 @@ private def shouldBetaReduce (e : Expr) (recFnName : Name) : Bool :=
     false
 
 /--
-  Beta reduce terms where the recursive function occurs in the lambda term.
-  This is useful to improve the effectiveness of `elimRecursion`.
+Preprocesses the expessions to improve the effectiveness of `elimRecursion`.
+
+* Beta reduce terms where the recursive function occurs in the lambda term.
   Example:
   ```
   def f : Nat → Nat
     | 0 => 1
     | i+1 => (fun x => f x) i
   ```
+
+* Floats out the RecApp markers.
+  Example:
+  ```
+  def f : Nat → Nat
+    | 0 => 1
+    | i+1 => (f x) i
+  ```
 -/
 def preprocess (e : Expr) (recFnName : Name) : CoreM Expr :=
   Core.transform e
-   fun e =>
-     if shouldBetaReduce e recFnName then
-       return .visit e.headBeta
-     else
-       return .continue
+    (pre := fun e =>
+      if shouldBetaReduce e recFnName then
+        return .visit e.headBeta
+      else
+        return .continue)
+    (post := fun e =>
+      match e with
+      | .app (.mdata m f) a =>
+        if m.isRecApp then
+          return .done (.mdata m (.app f a))
+        else
+          return .done e
+      | _ => return .done e)
+
 
 end Lean.Elab.Structural

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

@@ -7,6 +7,7 @@ import Lean.Elab.PreDefinition.Basic
 import Lean.Elab.PreDefinition.WF.TerminationHint
 import Lean.Elab.PreDefinition.WF.PackDomain
 import Lean.Elab.PreDefinition.WF.PackMutual
+import Lean.Elab.PreDefinition.WF.Preprocess
 import Lean.Elab.PreDefinition.WF.Rel
 import Lean.Elab.PreDefinition.WF.Fix
 import Lean.Elab.PreDefinition.WF.Eqns
@@ -79,6 +80,7 @@ private def isOnlyOneUnaryDef (preDefs : Array PreDefinition) (fixedPrefixSize :
     return false
 
 def wfRecursion (preDefs : Array PreDefinition) (wf? : Option TerminationWF) (decrTactic? : Option Syntax) : TermElabM Unit := do
+  let preDefs ← preDefs.mapM fun preDef => return { preDef with value := (← preprocess preDef.value) }
   let (unaryPreDef, fixedPrefixSize) ← withoutModifyingEnv do
     for preDef in preDefs do
       addAsAxiom preDef

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

@@ -0,0 +1,37 @@
+/-
+Copyright (c) 2021 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+import Lean.Meta.Transform
+import Lean.Elab.RecAppSyntax
+
+namespace Lean.Elab.WF
+open Meta
+
+/--
+Preprocesses the expessions to improve the effectiveness of `wfRecursion`.
+
+* Floats out the RecApp markers.
+  Example:
+  ```
+  def f : Nat → Nat
+    | 0 => 1
+    | i+1 => (f x) i
+  ```
+
+Unlike `Lean.Elab.Structural.preprocess`, do _not_ beta-reduce, as it could
+remove `let_fun`-lambdas that contain explicit termination proofs.
+-/
+def preprocess (e : Expr) : CoreM Expr :=
+  Core.transform e
+    (post := fun e =>
+      match e with
+      | .app (.mdata m f) a =>
+        if m.isRecApp then
+          return .done (.mdata m (.app f a))
+        else
+          return .done e
+      | _ => return .done e)
+
+end Lean.Elab.WF

src/Lean/Elab/RecAppSyntax.lean

@@ -27,4 +27,10 @@ def getRecAppSyntax? (e : Expr) : Option Syntax :=
     | _ => none
   | _                => none
 
+/--
+  Checks if the `MData` is for a recursive applciation.
+-/
+def MData.isRecApp (d : MData) : Bool :=
+  d.contains recAppKey
+
 end Lean

tests/lean/1673.lean.expected.out

@@ -3,4 +3,4 @@
 with errors
 structural recursion cannot be used
 
-failed to prove termination, use `termination_by` to specify a well-founded relation
+well-founded recursion cannot be used, 'foo.a' does not take any (non-fixed) arguments

tests/lean/run/2810.lean

@@ -0,0 +1,41 @@
+/-!
+Test that parentheses don't get in the way of structural recursion.
+https://github.com/leanprover/lean4/issues/2810
+-/
+
+def f (n : Nat) : Nat :=
+  match n with
+  | 0 => 0
+  | n + 1 => (f) n
+
+-- with beta-reduction
+def f2 (n : Nat) : Nat :=
+  match n with
+  | 0 => 0
+  | n + 1 => (fun n' => (f2) n') n
+
+-- structural recursion
+def f3 (n : Nat) : Nat :=
+  match n with
+  | 0 => 0
+  | n + 1 => (f3) n
+termination_by f3 n => n
+
+-- Same with rewrite
+
+theorem f_zero (n : Nat) : f n = 0 := by
+  match n with
+  | .zero => rfl
+  | .succ n  =>
+    unfold f
+    rewrite [f_zero]
+    rfl
+
+-- Same with simp
+
+theorem f_zero' (n : Nat) : f n = 0 := by
+  match n with
+  | .zero => rfl
+  | .succ n  =>
+    unfold f
+    simp only [f_zero']