feat: let unfold do zeta-delta reduction of local definitions (#4834)

This is "upstreaming" mathlib's `unfold_let` tactic by incorporating its
functionality into `unfold`. Now `unfold` can, in addition to unfolding
global definitions, unfold local definitions. The PR also updates the
`conv` version of the tactic.

An improvement over `unfold_let` is that it beta reduces unfolded local
functions.

Two features not present in `unfold` are that (1) `unfold_let` with no
arguments does zeta delta reduction of *all* local definitions, and also
(2) `unfold_let` can interleave unfoldings (in contrast, `unfold a b c`
is exactly the same as `unfold a; unfold b; unfold c`).

Closes RFC #4090

src/Init/Conv.lean

@@ -97,11 +97,18 @@ Users should prefer `unfold` for unfolding definitions. -/
 syntax (name := delta) "delta" (ppSpace colGt ident)+ : conv
 
 /--
-* `unfold foo` unfolds all occurrences of `foo` in the target.
+* `unfold id` unfolds all occurrences of definition `id` in the target.
 * `unfold id1 id2 ...` is equivalent to `unfold id1; unfold id2; ...`.
-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. -/
+
+Definitions can be either global or local definitions.
+
+For non-recursive global definitions, this tactic is identical to `delta`.
+For recursive global definitions, it uses the "unfolding lemma" `id.eq_def`,
+which is generated for each recursive definition, to unfold according to the recursive definition given by the user.
+Only one level of unfolding is performed, in contrast to `simp only [id]`, which unfolds definition `id` recursively.
+
+This is the `conv` version of the `unfold` tactic.
+-/
 syntax (name := unfold) "unfold" (ppSpace colGt ident)+ : conv
 
 /--

src/Init/Tactics.lean

@@ -676,12 +676,16 @@ compiled by Lean.
 syntax (name := delta) "delta" (ppSpace colGt ident)+ (location)? : tactic
 
 /--
-* `unfold id` unfolds definition `id`.
+* `unfold id` unfolds all occurrences of definition `id` in the target.
 * `unfold id1 id2 ...` is equivalent to `unfold id1; unfold id2; ...`.
+* `unfold id at h` unfolds at the hypothesis `h`.
 
-For non-recursive definitions, this tactic is identical to `delta`. For recursive definitions,
-it uses the "unfolding lemma" `id.eq_def`, which is generated for each recursive definition,
-to unfold according to the recursive definition given by the user.
+Definitions can be either global or local definitions.
+
+For non-recursive global definitions, this tactic is identical to `delta`.
+For recursive global definitions, it uses the "unfolding lemma" `id.eq_def`,
+which is generated for each recursive definition, to unfold according to the recursive definition given by the user.
+Only one level of unfolding is performed, in contrast to `simp only [id]`, which unfolds definition `id` recursively.
 -/
 syntax (name := unfold) "unfold" (ppSpace colGt ident)+ (location)? : tactic
 

src/Lean/Elab/Tactic/Conv/Unfold.lean

@@ -12,7 +12,13 @@ open Meta
 
 @[builtin_tactic Lean.Parser.Tactic.Conv.unfold] def evalUnfold : Tactic := fun stx => withMainContext do
   for declNameId in stx[1].getArgs do
-    let declName ← realizeGlobalConstNoOverloadWithInfo declNameId
-    applySimpResult (← unfold (← getLhs) declName)
+    let e ← elabTermForApply declNameId (mayPostpone := false)
+    match e with
+    | .const declName _ =>
+      applySimpResult (← unfold (← getLhs) declName)
+    | .fvar declFVarId =>
+      let lhs ← instantiateMVars (← getLhs)
+      changeLhs (← Meta.zetaDeltaFVars lhs #[declFVarId])
+    | _ => throwErrorAt declNameId m!"'unfold' conv tactic failed, expression {e} is not a global or local constant"
 
 end Lean.Elab.Tactic.Conv

src/Lean/Elab/Tactic/Unfold.lean

@@ -17,14 +17,25 @@ def unfoldLocalDecl (declName : Name) (fvarId : FVarId) : TacticM Unit := do
 def unfoldTarget (declName : Name) : TacticM Unit := do
   replaceMainGoal [← Meta.unfoldTarget (← getMainGoal) declName]
 
+def zetaDeltaLocalDecl (declFVarId : FVarId) (fvarId : FVarId) : TacticM Unit := do
+  replaceMainGoal [← Meta.zetaDeltaLocalDecl (← getMainGoal) fvarId declFVarId]
+
+def zetaDeltaTarget (declFVarId : FVarId) : TacticM Unit := do
+  replaceMainGoal [← Meta.zetaDeltaTarget (← getMainGoal) declFVarId]
+
 /-- "unfold " ident+ (location)? -/
 @[builtin_tactic Lean.Parser.Tactic.unfold] def evalUnfold : Tactic := fun stx => do
   let loc := expandOptLocation stx[2]
   for declNameId in stx[1].getArgs do
     go declNameId loc
 where
-  go (declNameId : Syntax) (loc : Location) : TacticM Unit := do
-    let declName ← realizeGlobalConstNoOverloadWithInfo declNameId
-    withLocation loc (unfoldLocalDecl declName) (unfoldTarget declName) (throwTacticEx `unfold · m!"did not unfold '{declName}'")
+  go (declNameId : Syntax) (loc : Location) : TacticM Unit := withMainContext do
+    let e ← elabTermForApply declNameId (mayPostpone := false)
+    match e with
+    | .const declName _ =>
+      withLocation loc (unfoldLocalDecl declName) (unfoldTarget declName) (throwTacticEx `unfold · m!"did not unfold '{declName}'")
+    | .fvar declFVarId =>
+      withLocation loc (zetaDeltaLocalDecl declFVarId) (zetaDeltaTarget declFVarId) (throwTacticEx `unfold · m!"did not unfold '{e}'")
+    | _ => withRef declNameId <| throwTacticEx `unfold (← getMainGoal) m!"expression {e} is not a global or local constant"
 
 end Lean.Elab.Tactic

src/Lean/Meta/Tactic/Unfold.lean

@@ -43,4 +43,16 @@ def unfoldLocalDecl (mvarId : MVarId) (fvarId : FVarId) (declName : Name) : Meta
   let some (_, mvarId) ← applySimpResultToLocalDecl mvarId fvarId r (mayCloseGoal := false) | unreachable!
   return mvarId
 
+def zetaDeltaTarget (mvarId : MVarId) (declFVarId : FVarId) : MetaM MVarId := mvarId.withContext do
+  let target ← instantiateMVars (← mvarId.getType)
+  let target' ← Meta.zetaDeltaFVars target #[declFVarId]
+  if target' == target then throwError "tactic 'unfold' failed to unfold '{Expr.fvar declFVarId}' at{indentExpr target}"
+  mvarId.replaceTargetDefEq target'
+
+def zetaDeltaLocalDecl (mvarId : MVarId) (fvarId : FVarId) (declFVarId : FVarId) : MetaM MVarId := mvarId.withContext do
+  let type ← fvarId.getType
+  let type' ← Meta.zetaDeltaFVars (← instantiateMVars type) #[declFVarId]
+  if type' == type then throwError "tactic 'unfold' failed to unfold '{Expr.fvar fvarId}' at{indentExpr type}"
+  mvarId.replaceLocalDeclDefEq fvarId type'
+
 end Lean.Meta

src/Lean/Meta/Transform.lean

@@ -151,6 +151,22 @@ def zetaReduce (e : Expr) : MetaM Expr := do
     | _ => return .continue
   transform e (pre := pre) (usedLetOnly := true)
 
+/--
+Zeta reduces only the provided fvars, beta reducing the substitutions.
+-/
+def zetaDeltaFVars (e : Expr) (fvars : Array FVarId) : MetaM Expr :=
+  let unfold? (fvarId : FVarId) : MetaM (Option Expr) := do
+    if fvars.contains fvarId then
+      fvarId.getValue?
+    else
+      return none
+  let pre (e : Expr) : MetaM TransformStep := do
+    if let .fvar fvarId := e.getAppFn then
+      if let some val ← unfold? fvarId then
+        return .visit <| (← instantiateMVars val).beta e.getAppArgs
+    return .continue
+  transform e (pre := pre)
+
 /-- Unfold definitions and theorems in `e` that are not in the current environment, but are in `biggerEnv`. -/
 def unfoldDeclsFrom (biggerEnv : Environment) (e : Expr) : CoreM Expr := do
   withoutModifyingEnv do

tests/lean/run/unfoldTactic.lean

@@ -0,0 +1,95 @@
+/-!
+# Tests of the `unfold` tactic
+-/
+
+/-!
+Tests adapted from mathlib's `unfold_let` tactic
+-/
+
+example : let x := 1; let y := 2; x + y = y + x := by
+  intro x y
+  unfold x
+  guard_target =ₛ 1 + y = y + 1
+  let z := 3
+  have h : z - 3 = 0 := rfl
+  unfold z at h
+  guard_hyp h :ₛ 3 - 3 = 0
+  unfold y
+  guard_target =ₛ 1 + 2 = 2 + 1
+  rfl
+
+example : let x := 1; let y := 2; x + y = y + x := by
+  intro x y
+  unfold x y
+  guard_target =ₛ 1 + 2 = 2 + 1
+  rfl
+
+example : let x := 1; let y := 2 + x; y = 3 := by
+  intro x y
+  unfold y
+  guard_target =ₛ 2 + x = 3
+  unfold x
+  guard_target =ₛ 2 + 1 = 3
+  rfl
+
+example : let x := 1; let y := 2 + x; y = 3 := by
+  intro x y
+  fail_if_success unfold x y -- wrong order
+  unfold y x
+  guard_target =ₛ 2 + 1 = 3
+  rfl
+
+/-!
+Do not reorder hypotheses. (`unfold` makes a change)
+-/
+set_option linter.unusedVariables false in
+example : let ty := Int; ty → Nat → Nat := by
+  intro ty a a
+  unfold ty at *
+  exact a
+
+/-!
+Beta reduction of unfolded local functions
+-/
+example : True := by
+  let f (x y : Nat) := x + y
+  have : f 1 2 = 3 := by
+    unfold f
+    guard_target =ₛ 1 + 2 = 3
+    rfl
+  trivial
+
+/-!
+Nothing to unfold
+-/
+/--
+error: tactic 'unfold' failed to unfold 'id' at
+  True
+-/
+#guard_msgs in
+example : True := by
+  unfold id
+/--
+error: tactic 'unfold' failed to unfold 'x' at
+  True
+-/
+#guard_msgs in
+example : True := by
+  let x := 2
+  unfold x
+
+
+/-!
+Conv tactic
+-/
+
+example (h : False) : id true = false := by
+  conv => unfold id
+  guard_target =ₛ true = false
+  exact h.elim
+
+example : let x := 1; let y := 2; x + y = y + x := by
+  intro x y
+  conv => unfold x
+  guard_target =ₛ 1 + y = y + 1
+  rfl