From 0787886cea76f329b865645ac9aaaad4c3f9df91 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 13 Feb 2021 18:53:15 -0800
Subject: [PATCH] feat: improve `simp` local lemma elaboration

---
 src/Lean/Elab/Tactic/Simp.lean            | 14 ++++++++++++--
 src/Lean/Meta/Tactic/Simp/SimpLemmas.lean |  6 ++++++
 tests/lean/run/simp5.lean                 |  9 +++++++++
 3 files changed, 27 insertions(+), 2 deletions(-)
 create mode 100644 tests/lean/run/simp5.lean

diff --git a/src/Lean/Elab/Tactic/Simp.lean b/src/Lean/Elab/Tactic/Simp.lean
index fd94c18c60..94680f25d6 100644
--- a/src/Lean/Elab/Tactic/Simp.lean
+++ b/src/Lean/Elab/Tactic/Simp.lean
@@ -73,6 +73,14 @@ def elabSimpConfig (optConfig : Syntax) : TermElabM Meta.Simp.Config := do
       let c ← Term.elabTermEnsuringType optConfig[0] (Lean.mkConst ``Meta.Simp.Config)
       evalSimpConfig (← instantiateMVars c)
 
+/-- Return `some c`, if `e` is of the form `c.{?u_1, ..., ?u_n} ?m_1 ... ?m_k` -/
+private def isGlobalLemma? (e : Expr) : Option Name :=
+  e.withApp fun f args =>
+    if f.isConst && args.all (·.isMVar) && f.constLevels!.all (·.isMVar) then
+      some f.constName!
+    else
+      none
+
 /-- Elaborate extra simp lemmas provided to `simp`. `stx` is of the `simpLemma,*` -/
 private def elabSimpLemmas (stx : Syntax) (ctx : Simp.Context) : TacticM Simp.Context := do
   if stx.isNone then
@@ -92,8 +100,10 @@ private def elabSimpLemmas (stx : Syntax) (ctx : Simp.Context) : TacticM Simp.Co
             true
           else
             simpLemma[0][0].getKind == ``Parser.Tactic.simpPost
-        let term ← elabTerm simpLemma[1] none true
-        lemmas ← lemmas.add term post
+        let lemma ← elabTerm simpLemma[1] none (mayPostpone := false)
+        match isGlobalLemma? lemma with
+        | some declName => lemmas ← lemmas.addConst declName post
+        | none          => lemmas ← lemmas.add lemma post
       return { ctx with simpLemmas := lemmas }
 
 @[builtinTactic Lean.Parser.Tactic.simp] def evalSimp : Tactic := fun stx => do
diff --git a/src/Lean/Meta/Tactic/Simp/SimpLemmas.lean b/src/Lean/Meta/Tactic/Simp/SimpLemmas.lean
index 31e6ce2774..b61517bff9 100644
--- a/src/Lean/Meta/Tactic/Simp/SimpLemmas.lean
+++ b/src/Lean/Meta/Tactic/Simp/SimpLemmas.lean
@@ -120,6 +120,12 @@ def SimpLemmas.add (s : SimpLemmas) (e : Expr) (post : Bool := true) (prio : Nat
   let lemma ← mkSimpLemma e post prio name?
   return addSimpLemmaEntry s lemma
 
+/- Auxiliary method for adding a global declaration to a `SimpLemmas` datastructure. -/
+def SimpLemmas.addConst (s : SimpLemmas) (declName : Name) (post : Bool := true) (prio : Nat := evalPrio! default) : MetaM SimpLemmas := do
+  let cinfo ← getConstInfo declName
+  let lemma ← mkSimpLemmaCore (mkConst declName (cinfo.levelParams.map mkLevelParam)) (mkConst declName) post prio declName
+  return addSimpLemmaEntry s lemma
+
 def SimpLemma.getValue (lemma : SimpLemma) : MetaM Expr := do
   match lemma.val with
   | Expr.const declName [] _ =>
diff --git a/tests/lean/run/simp5.lean b/tests/lean/run/simp5.lean
new file mode 100644
index 0000000000..6f36b4be0c
--- /dev/null
+++ b/tests/lean/run/simp5.lean
@@ -0,0 +1,9 @@
+def f {α} (a b : α) := a
+
+theorem f_Eq {α} (a b : α) : f a b = a :=
+  rfl
+
+theorem ex (a b c : α) : f (f a b) c = a := by
+  simp [f_Eq]
+
+#print ex