From 90353d7fd78309f9729218ee5f95d017758c5b93 Mon Sep 17 00:00:00 2001
From: Mario Carneiro <di.gama@gmail.com>
Date: Tue, 20 Sep 2022 20:41:38 -0400
Subject: [PATCH] feat: multiple `delta`, delta conv, `unfold`

---
 src/Init/Conv.lean                    |  4 ++--
 src/Lean/Elab/Tactic/Conv/Delta.lean  |  4 ++--
 src/Lean/Elab/Tactic/Conv/Unfold.lean |  5 +++--
 src/Lean/Elab/Tactic/Delta.lean       | 20 +++++++++++---------
 src/Lean/Elab/Tactic/Unfold.lean      |  3 ++-
 5 files changed, 20 insertions(+), 16 deletions(-)

diff --git a/src/Init/Conv.lean b/src/Init/Conv.lean
index 428225ba26..69c24999a0 100644
--- a/src/Init/Conv.lean
+++ b/src/Init/Conv.lean
@@ -82,13 +82,13 @@ syntax (name := change) "change " term : conv
 Like the `delta` tactic, this ignores any definitional equations and uses
 primitive delta-reduction instead, which may result in leaking implementation details.
 Users should prefer `unfold` for unfolding definitions. -/
-syntax (name := delta) "delta " ident : conv
+syntax (name := delta) "delta " ident,+ : conv
 
 /-- `unfold foo` unfolds all occurrences of `foo` in the target.
 Like the `unfold` tactic, this uses equational lemmas for the chosen definition
 to rewrite the target. For recursive definitions,
 only one layer of unfolding is performed. -/
-syntax (name := unfold) "unfold " ident : conv
+syntax (name := unfold) "unfold " ident,+ : conv
 
 /-- `pattern pat` traverses to the first subterm of the target that matches `pat`. -/
 syntax (name := pattern) "pattern " term : conv
diff --git a/src/Lean/Elab/Tactic/Conv/Delta.lean b/src/Lean/Elab/Tactic/Conv/Delta.lean
index 433ff2b40f..60202eb003 100644
--- a/src/Lean/Elab/Tactic/Conv/Delta.lean
+++ b/src/Lean/Elab/Tactic/Conv/Delta.lean
@@ -10,8 +10,8 @@ namespace Lean.Elab.Tactic.Conv
 open Meta
 
 @[builtinTactic Lean.Parser.Tactic.Conv.delta] def evalDelta : Tactic := fun stx => withMainContext do
-  let declName ← resolveGlobalConstNoOverloadWithInfo stx[1]
-  let lhsNew ← deltaExpand (← instantiateMVars (← getLhs)) (· == declName)
+  let declNames ← stx[1].getArgs.mapM resolveGlobalConstNoOverloadWithInfo
+  let lhsNew ← deltaExpand (← instantiateMVars (← getLhs)) declNames.contains
   changeLhs lhsNew
 
 end Lean.Elab.Tactic.Conv
diff --git a/src/Lean/Elab/Tactic/Conv/Unfold.lean b/src/Lean/Elab/Tactic/Conv/Unfold.lean
index c1c8b7d2cb..fd2c60c8e4 100644
--- a/src/Lean/Elab/Tactic/Conv/Unfold.lean
+++ b/src/Lean/Elab/Tactic/Conv/Unfold.lean
@@ -10,7 +10,8 @@ namespace Lean.Elab.Tactic.Conv
 open Meta
 
 @[builtinTactic Lean.Parser.Tactic.Conv.unfold] def evalUnfold : Tactic := fun stx => withMainContext do
-  let declName ← resolveGlobalConstNoOverloadWithInfo stx[1]
-  applySimpResult (← unfold (← getLhs) declName)
+  for declNameId in stx[1].getArgs do
+    let declName ← resolveGlobalConstNoOverloadWithInfo declNameId
+    applySimpResult (← unfold (← getLhs) declName)
 
 end Lean.Elab.Tactic.Conv
diff --git a/src/Lean/Elab/Tactic/Delta.lean b/src/Lean/Elab/Tactic/Delta.lean
index 5a7dcb6a05..bc130f8d19 100644
--- a/src/Lean/Elab/Tactic/Delta.lean
+++ b/src/Lean/Elab/Tactic/Delta.lean
@@ -10,28 +10,30 @@ import Lean.Elab.Tactic.Location
 namespace Lean.Elab.Tactic
 open Meta
 
-def deltaLocalDecl (declName : Name) (fvarId : FVarId) : TacticM Unit := do
+def deltaLocalDecl (declNames : Array Name) (fvarId : FVarId) : TacticM Unit := do
   let mvarId ← getMainGoal
   let localDecl ← fvarId.getDecl
-  let typeNew ← deltaExpand localDecl.type (· == declName)
+  let typeNew ← deltaExpand localDecl.type declNames.contains
   if typeNew == localDecl.type then
-    throwTacticEx `delta mvarId m!"did not delta reduce '{declName}' at '{localDecl.userName}'"
+    throwTacticEx `delta mvarId m!"did not delta reduce '{declNames}' at '{localDecl.userName}'"
   replaceMainGoal [← mvarId.replaceLocalDeclDefEq fvarId typeNew]
 
-def deltaTarget (declName : Name) : TacticM Unit := do
+def deltaTarget (declNames : Array Name) : TacticM Unit := do
   let mvarId ← getMainGoal
   let target ← getMainTarget
-  let targetNew ← deltaExpand target (· == declName)
+  let targetNew ← deltaExpand target declNames.contains
   if targetNew == target then
-    throwTacticEx `delta mvarId m!"did not delta reduce '{declName}'"
+    throwTacticEx `delta mvarId m!"did not delta reduce '{declNames}'"
   replaceMainGoal [← mvarId.replaceTargetDefEq targetNew]
 
 /--
-  "delta " ident (location)?
+  "delta " ident,+ (location)?
 -/
 @[builtinTactic Lean.Parser.Tactic.delta] def evalDelta : Tactic := fun stx => do
-  let declName ← resolveGlobalConstNoOverloadWithInfo stx[1]
+  let args := if stx[1].isIdent then #[stx[1]] else stx[1].getArgs
+  let declNames ← args.mapM resolveGlobalConstNoOverloadWithInfo
   let loc := expandOptLocation stx[2]
-  withLocation loc (deltaLocalDecl declName) (deltaTarget declName) (throwTacticEx `delta · m!"did not delta reduce '{declName}'")
+  withLocation loc (deltaLocalDecl declNames) (deltaTarget declNames)
+    (throwTacticEx `delta · m!"did not delta reduce '{declNames}'")
 
 end Lean.Elab.Tactic
diff --git a/src/Lean/Elab/Tactic/Unfold.lean b/src/Lean/Elab/Tactic/Unfold.lean
index 0b9ff9298d..a660080b1b 100644
--- a/src/Lean/Elab/Tactic/Unfold.lean
+++ b/src/Lean/Elab/Tactic/Unfold.lean
@@ -21,7 +21,8 @@ def unfoldTarget (declName : Name) : TacticM Unit := do
 -/
 @[builtinTactic Lean.Parser.Tactic.unfold] def evalUnfold : Tactic := fun stx => do
   let loc := expandOptLocation stx[2]
-  for declNameId in stx[1].getSepArgs do
+  let args := if stx[1][1].isAtom then stx[1].getSepArgs else stx[1].getArgs
+  for declNameId in args do
     go declNameId loc
 where
   go (declNameId : Syntax) (loc : Location) : TacticM Unit := do