RFC: let `unfold` tactic zeta reduce local definitions

[kmill]

Proposal

Right now there's a feature mismatch between simp and unfold, where if f is a global definition and x is a local definition you can write simp only [f, x] to unfold f and zeta reduce x, but you cannot write unfold f x since the tactic expects that x be a global definition. Users frequently ask about this on Zulip, being familiar with unfold but confused why they can't unfold local definitions. Recently this was brought up explicitly by Jon Eugster on Zulip asking if there was any technical limitation to letting unfold unfold local definitions, hence this RFC.

One of the workarounds for this in mathlib, to have a direct analogue of unfold, is the unfold_let tactic. (Note: this tactic predates the feature allowing simp and dsimp to take local definitions.)

The proposal is to alter unfold to be able to handle unfolding local definitions. The implementation cost is low, and instead of resolving only global names, it would need to resolve a name in general and conditionally unfold a constant or zeta reduce a local definition depending on what kind of name it was. This would technically be a breaking change since if a local name shadowed a global one it would now be preferred.

The primary beneficiary for this change would be those learning Lean. Users tend to see local definitions and global definitions as being similar, and it's a common guess that if a tactic works with one it should work for the other. Making unfold work in this case will reduce frustration in the game of guess-the-tactic.

Side note: It's unclear whether users know that unfold f1 f2 f3 is the same as unfold f1; unfold f2; unfold f3, and they might expect it to interleave unfolding of the definitions. This RFC is not making a recommendation here beyond suggesting that when the tactic docstring this detail can be mentioned.

Community Feedback

Zulip discussion

Impact

Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.

[joneugster]

Here is a working example of how this could be done. Hopefully this could be used to facilitate a proper implementation.

The trys contain the content of mathlib's unfold_let while the catchs contain what core's unfold does currently.

Note that the try-catch block is subideal: Rather, one probably wants to figure out if the provided Syntax is either containing a Name or an FVarId (i.e. what's done with the variable x in the code), but I don't know how to do this.

Working example

import Lean
import Lean.Elab.Tactic

open Lean.Elab.Tactic Lean Elab Meta

namespace Test

/-- From Mathlib/Tactic/DefEqTransformations.lean
Not sure if there is something like it in Lean. -/
def unfoldFVar (fvarId : FVarId) (e : Expr) : MetaM Expr := do
  transform (usedLetOnly := true) e fun node => do
    match node with
    | .fvar otherFVarId =>
      if fvarId == otherFVarId then
        if let some val ← otherFVarId.getValue? then
          return .visit (← instantiateMVars val)
        else
          return .continue
      else
        return .continue
    | _ => return .continue

/-- From Mathlib/Tactic/DefEqTransformations.lean.
Not sure if we need it. -/
def _root_.Lean.MVarId.changeLocalDecl' (mvarId : MVarId) (fvarId : FVarId) (typeNew : Expr)
    (checkDefEq := true) : MetaM MVarId := do
  mvarId.checkNotAssigned `changeLocalDecl
  let lctx := (← mvarId.getDecl).lctx
  let some decl := lctx.find? fvarId | throwTacticEx `changeLocalDecl mvarId m!"\
    local variable {Expr.fvar fvarId} is not present in local context{mvarId}"
  let toRevert := lctx.foldl (init := #[]) fun arr decl' =>
    if decl.index ≤ decl'.index then arr.push decl'.fvarId else arr
  let (_, mvarId) ← mvarId.withReverted toRevert fun mvarId fvars => mvarId.withContext do
    let check (typeOld : Expr) : MetaM Unit := do
      if checkDefEq then
        unless ← isDefEq typeNew typeOld do
          throwTacticEx `changeLocalDecl mvarId
            m!"given type{indentExpr typeNew}\nis not definitionally equal to{indentExpr typeOld}"
    let finalize (targetNew : Expr) := do
      return ((), fvars.map .some, ← mvarId.replaceTargetDefEq targetNew)
    match ← mvarId.getType with
    | .forallE n d b bi => do check d; finalize (.forallE n typeNew b bi)
    | .letE n t v b ndep => do check t; finalize (.letE n typeNew v b ndep)
    | _ => throwTacticEx `changeLocalDecl mvarId "unexpected auxiliary target"
  return mvarId

/-- Modified `unfold` tactc, which first tries to unfold as a local definition
and if that fails, it tries to unfold the global definition.
-/
@[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
    withLocation loc
      (atLocal := fun fvar =>
        try
          let x ← getFVarId declNameId

          liftMetaTactic1 fun mvarId => do
            let ty ← fvar.getType
            let ty' ← (unfoldFVar x) (← instantiateMVars ty)
            if Expr.equal ty ty' then
              return mvarId
            else
              mvarId.changeLocalDecl' (checkDefEq := true) fvar ty'
        catch _ =>
          let x ← realizeGlobalConstNoOverloadWithInfo declNameId -- in `v4.7.0` this started with `resolve`

          unfoldLocalDecl x fvar )
      (atTarget :=
        try
          let x ← getFVarId declNameId

          liftMetaTactic1 fun mvarId => do
          let ty ← instantiateMVars (← mvarId.getType)
          mvarId.change (checkDefEq := true) (← (unfoldFVar x) ty)
        catch _ =>
          let x ← realizeGlobalConstNoOverloadWithInfo declNameId -- in `v4.7.0` this started with `resolve`

          unfoldTarget x)
      (failed := (throwTacticEx `unfold · m!"did not unfold '{declNameId}'"))


/-! Tests -/

example (A B : Type) (h : A = B) :
    let C := A
    C = B := by
  intro C
  unfold C
  rw [h]

def C := Nat

example (B : Type) (h : Nat = B) :
    C = B := by
  unfold C
  rw [h]