From 4848ad48696d60729dcdd67942f9987a8929de13 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 18 Apr 2022 16:43:16 -0700
Subject: [PATCH] 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                         | 23 ++++++++++++++++++
 src/Lean/Elab/Tactic/Simp.lean      |  5 +++-
 src/Lean/Meta/Tactic/Simp/Main.lean | 33 ++++++++++++++++++++++++-
 tests/lean/run/simpAutoUnfold.lean  | 37 +++++++++++++++++++++++++++++
 4 files changed, 96 insertions(+), 2 deletions(-)
 create mode 100644 tests/lean/run/simpAutoUnfold.lean

diff --git a/RELEASES.md b/RELEASES.md
index 0a45bdf63a..36a59ae5b0 100644
--- a/RELEASES.md
+++ b/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
diff --git a/src/Lean/Elab/Tactic/Simp.lean b/src/Lean/Elab/Tactic/Simp.lean
index 619ff02fb0..1de98f92b5 100644
--- a/src/Lean/Elab/Tactic/Simp.lean
+++ b/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
diff --git a/src/Lean/Meta/Tactic/Simp/Main.lean b/src/Lean/Meta/Tactic/Simp/Main.lean
index 5c739616bd..aa26563a84 100644
--- a/src/Lean/Meta/Tactic/Simp/Main.lean
+++ b/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
diff --git a/tests/lean/run/simpAutoUnfold.lean b/tests/lean/run/simpAutoUnfold.lean
new file mode 100644
index 0000000000..999a1fa8ba
--- /dev/null
+++ b/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!