From adda3a9e0239cff80d7d0cd7f5acdaae7fe8d5da Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 13 Apr 2021 10:29:56 -0700
Subject: [PATCH] fix: improve structural recursion

---
 src/Lean/Elab/PreDefinition/Structural.lean | 24 ++++++++++++++++++++
 tests/lean/run/structuralIssue2.lean        | 25 +++++++++++++++++++++
 2 files changed, 49 insertions(+)
 create mode 100644 tests/lean/run/structuralIssue2.lean

diff --git a/src/Lean/Elab/PreDefinition/Structural.lean b/src/Lean/Elab/PreDefinition/Structural.lean
index 9b34e81550..b6d8f15a44 100644
--- a/src/Lean/Elab/PreDefinition/Structural.lean
+++ b/src/Lean/Elab/PreDefinition/Structural.lean
@@ -7,6 +7,7 @@ import Lean.Util.ForEachExpr
 import Lean.Meta.ForEachExpr
 import Lean.Meta.RecursorInfo
 import Lean.Meta.Match.Match
+import Lean.Meta.Transform
 import Lean.Elab.PreDefinition.Basic
 namespace Lean.Elab
 namespace Structural
@@ -376,9 +377,32 @@ private def mkBRecOn (recFnName : Name) (recArgInfo : RecArgInfo) (value : Expr)
       let brecOn       := mkApp brecOn Farg
       pure $ mkAppN brecOn otherArgs
 
+private def shouldBetaReduce (e : Expr) (recFnName : Name) : Bool :=
+  if e.isHeadBetaTarget then
+    e.getAppFn.find? (·.isConstOf recFnName) |>.isSome
+  else
+    false
+
+/--
+  Beta reduce terms where the recursive function occurs in the lambda term.
+  This is useful to improve the effectiveness of `elimRecursion`.
+  Example:
+  ```
+
+  ```
+-/
+private def preprocess (e : Expr) (recFnName : Name) : CoreM Expr :=
+  Core.transform e
+   fun e => return TransformStep.visit <|
+     if shouldBetaReduce e recFnName then
+       e.headBeta
+     else
+       e
+
 private def elimRecursion (preDef : PreDefinition) : M PreDefinition :=
   withoutModifyingEnv do lambdaTelescope preDef.value fun xs value => do
     addAsAxiom preDef
+    let value ← preprocess value preDef.declName
     trace[Elab.definition.structural] "{preDef.declName} {xs} :=\n{value}"
     let numFixed ← getFixedPrefix preDef.declName xs value
     trace[Elab.definition.structural] "numFixed: {numFixed}"
diff --git a/tests/lean/run/structuralIssue2.lean b/tests/lean/run/structuralIssue2.lean
new file mode 100644
index 0000000000..797da1daa2
--- /dev/null
+++ b/tests/lean/run/structuralIssue2.lean
@@ -0,0 +1,25 @@
+namespace List
+
+@[simp] theorem filter_nil {p : α → Bool} : filter p [] = [] := by
+  simp [filter, filterAux, reverse, reverseAux]
+
+theorem cons_eq_append (a : α) (as : List α) : a :: as = [a] ++ as := rfl
+
+theorem filter_cons (a : α) (as : List α) :
+  filter p (a :: as) = if p a then a :: filter p as else filter p as :=
+  sorry
+
+@[simp] theorem filter_append {as bs : List α} {p : α → Bool} :
+  filter p (as ++ bs) = filter p as ++ filter p bs :=
+  match as with
+  | []      => by simp
+  | a :: as => by
+    rw [filter_cons, cons_append, filter_cons]
+    cases p a
+    simp [filter_append]
+    simp [filter_append]
+
+-- the previous contains a more complicated version of
+def f : Nat → Nat
+  | 0 => 1
+  | i+1 => (fun x => f x) i