feat: implement autoUnfold at simp

Right now, it only supports the following kind of definitions
- Recursive definitions that support smart unfolding.
- Non-recursive definitions where the body is a match-expression. This
kind of definition is only unfolded if the match can be reduced.

RELEASES.md

@@ -1,6 +1,29 @@
 Unreleased
 ---------
 
+* Add `autoUnfold` option to `Lean.Meta.Simp.Config`, and the following macros
+  - `simp!` for `simp (config := { autoUnfold := true })`
+  - `simp_arith!` for `simp (config := { autoUnfold := true, arith := true })`
+  - `simp_all!` for `simp_all (config := { autoUnfold := true })`
+  - `simp_all_arith!` for `simp_all (config := { autoUnfold := true, arith := true })`
+  When the `autoUnfold` is set to true, `simp` tries to unfold the following kinds of definition
+  - Recursive definitions defined by structural recursion.
+  - Non-recursive definitions where the body is a `match`-expression. This
+    kind of definition is only unfolded if the `match` can be reduced.
+  Example:
+  ```lean
+  def append (as bs : List α) : List α :=
+    match as with
+    | [] => bs
+    | a :: as => a :: append as bs
+
+  theorem append_nil (as : List α) : append as [] = as := by
+    induction as <;> simp_all!
+
+  theorem append_assoc (as bs cs : List α) : append (append as bs) cs = append as (append bs cs) := by
+    induction as <;> simp_all!
+  ```
+
 * Add `save` tactic for creating checkpoints more conveniently. Example:
 ```lean
 example : <some-proposition> := by

src/Lean/Elab/Tactic/Simp.lean

@@ -141,7 +141,10 @@ private def elabSimpArgs (stx : Syntax) (ctx : Simp.Context) (eraseLocal : Bool)
             thms := thms.eraseCore arg[1].getId
           else
             let declName ← resolveGlobalConstNoOverloadWithInfo arg[1]
-            thms ← thms.erase declName
+            if ctx.config.autoUnfold then
+              thms := thms.eraseCore declName
+            else
+              thms ← thms.erase declName
         else if arg.getKind == ``Lean.Parser.Tactic.simpLemma then
           let post :=
             if arg[0].isNone then

src/Lean/Meta/Tactic/Simp/Main.lean

@@ -94,6 +94,25 @@ private def reduceFVar (cfg : Config) (e : Expr) : MetaM Expr := do
   else
     return e
 
+/--
+  Return true if `declName` is the name of a definition of the form
+  ```
+  def declName ... :=
+    match ... with
+    | ...
+  ```
+-/
+private partial def isMatchDef (declName : Name) : CoreM Bool := do
+  let .defnInfo info ← getConstInfo declName | return false
+  return go (← getEnv) info.value
+where
+  go (env : Environment) (e : Expr) : Bool :=
+    if e.isLambda then
+      go env e.bindingBody!
+    else
+      let f := e.getAppFn
+      f.isConst && isMatcherCore env f.constName!
+
 private def unfold? (e : Expr) : SimpM (Option Expr) := do
   let f := e.getAppFn
   if !f.isConst then
@@ -101,7 +120,19 @@ private def unfold? (e : Expr) : SimpM (Option Expr) := do
   let fName := f.constName!
   if (← isProjectionFn fName) then
     return none -- should be reduced by `reduceProjFn?`
-  if (← read).isDeclToUnfold e.getAppFn.constName! then
+  let ctx ← read
+  if ctx.config.autoUnfold then
+    if ctx.simpTheorems.isErased fName then
+      return none
+    else if hasSmartUnfoldingDecl (← getEnv) fName then
+      withDefault <| unfoldDefinition? e
+    else if (← isMatchDef fName) then
+      let some value ← withDefault <| unfoldDefinition? e | return none
+      let .reduced value ← reduceMatcher? value | return none
+      return some value
+    else
+      return none
+  else if ctx.isDeclToUnfold fName then
     withDefault <| unfoldDefinition? e
   else
     return none

tests/lean/run/simpAutoUnfold.lean

@@ -0,0 +1,37 @@
+def append (as bs : List α) : List α :=
+  match as with
+  | [] => bs
+  | a :: as => a :: append as bs
+
+theorem append_nil (as : List α) : append as [] = as := by
+  induction as <;> simp_all!
+
+theorem append_nil' (as : List α) : append as [] = as := by
+  induction as <;> simp! [*]
+
+theorem append_assoc (as bs cs : List α) : append (append as bs) cs = append as (append bs cs) := by
+  induction as <;> simp_all!
+
+theorem append_assoc' (as bs cs : List α) : append (append as bs) cs = append as (append bs cs) := by
+  induction as <;> simp! [*]
+
+def g : Nat → Nat
+  | 0   => 1
+  | n+1 => n + 2
+
+example (a : Nat) : g a > 0 := by
+  cases a <;> simp_arith!
+
+example (a : Nat) : g a > 0 := by
+  cases a <;> simp_arith!
+
+example (a : Nat) : g a > 0 := by
+  cases a <;> simp_arith! [-g]
+  simp_arith!
+
+example (a : Nat) (h : b + 2 = 2) : g a > b := by
+  cases a <;> simp_all_arith!
+
+example (a : Nat) (h : b + 2 = 2) : g a > b := by
+  cases a <;> simp_all_arith! [-g]
+  simp_arith!