From 5e24da0c2e228a742dbf34f4fbd7ac62bf8437a2 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 16 Feb 2021 13:12:57 -0800
Subject: [PATCH] fix: `simp` argument issue

See new test.
---
 src/Lean/Elab/Tactic/Simp.lean | 29 ++++++++++++++++-------------
 tests/lean/run/simp7.lean      |  7 +++++++
 2 files changed, 23 insertions(+), 13 deletions(-)

diff --git a/src/Lean/Elab/Tactic/Simp.lean b/src/Lean/Elab/Tactic/Simp.lean
index d00f658b1e..66ed78dc85 100644
--- a/src/Lean/Elab/Tactic/Simp.lean
+++ b/src/Lean/Elab/Tactic/Simp.lean
@@ -73,14 +73,6 @@ 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 isGlobalDecl? (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
@@ -95,21 +87,32 @@ private def elabSimpLemmas (stx : Syntax) (ctx : Simp.Context) : TacticM Simp.Co
     withMVarContext g do
       let mut lemmas := ctx.simpLemmas
       let mut toUnfold : NameSet := {}
-      for arg in stx[1].getSepArgs do
+      for (arg : Syntax) in stx[1].getSepArgs do
         let post :=
           if arg[0].isNone then
             true
           else
             arg[0][0].getKind == ``Parser.Tactic.simpPost
-        let arg ← elabTerm arg[1] none (mayPostpone := false)
-        match isGlobalDecl? arg with
+        match (← resolveSimpIdLemma? arg[1]) with
         | some declName =>
-          if (← isProof arg) then
+          let info ← getConstInfo declName
+          if (← isProp info.type) then
             lemmas ← lemmas.addConst declName post
           else
             toUnfold := toUnfold.insert declName
-        | none          => lemmas ← lemmas.add arg post
+        | _ =>
+          let arg ← elabTerm arg[1] none (mayPostpone := false)
+          lemmas ← lemmas.add arg post
       return { ctx with simpLemmas := lemmas, toUnfold := toUnfold }
+where
+  resolveSimpIdLemma? (simpArgTerm : Syntax) : TacticM (Option Name) := do
+    if simpArgTerm.isIdent then
+      try
+        return some (← resolveGlobalConstNoOverload simpArgTerm.getId)
+      catch _ =>
+        return none
+    else
+      return none
 
 @[builtinTactic Lean.Parser.Tactic.simp] def evalSimp : Tactic := fun stx => do
   let ctx ← elabSimpLemmas stx[1] { config := (← elabSimpConfig stx[2]), simpLemmas := (← getSimpLemmas), congrLemmas := (← getCongrLemmas) }
diff --git a/tests/lean/run/simp7.lean b/tests/lean/run/simp7.lean
index 32ba8f86f3..2ce8cdb6a3 100644
--- a/tests/lean/run/simp7.lean
+++ b/tests/lean/run/simp7.lean
@@ -24,3 +24,10 @@ theorem ex3 : fact x > 0 := by
     apply Nat.mulPos
     apply Nat.zeroLtSucc
     apply ih
+
+def head [Inhabited α] : List α → α
+  | []   => arbitrary
+  | a::_ => a
+
+theorem ex [Inhabited α] (a : α) (as : List α) : head (a::as) = a :=
+  by simp [head]