unfold and unfold_let

Stream: lean4

[Jon Eugster]

unfold_let and unfold seem to serve a very similar purpose, one for "local definitions" and the other one for "global" definitions.

Would it make sense to merge the two tactics to a single unfold that can handle both or are there good reasons why they should stay distinct? Is it a problem if Lean first has to figure out what the arguments provided are, fvars or global constants?

import Mathlib

example (A B : Type) (h : A = B) :
    let C := A
    C = B := by
  intro C
  /-
  AB: Type
  h: A = B
  C: Type := A
  ⊢ C = B
  -/
  unfold_let C
  rw [h]


def C := Nat

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

[Patrick Massot]

I agree that this distinction looks like a historical accident that could be fixed now that everything is in core (I guess everything is core?).

[Kyle Miller]

unfold_let is a mathlib tactic, and it pre-dated being able to write dsimp only [C]

[Patrick Massot]

Can’t you simply merge it with unfold now? This is a really natural expectation for new users.

[Ruben Van de Velde]

I wonder if there's a clear explanation somewhere when you need unfold rather than dsimp or the other way around

[Jon Eugster]

ok, in that case I might give it a shot to merge the two at some point :+1:

[Kyle Miller]

@Patrick Massot It's on my list of things to look into

[Jon Eugster]

I'm not exactly sure, but I think dsimp [C] does just a little bit more than unfold . So far I've been using unfold as "plug in the definition but don't do anything else". Not aware of anything that unfold could do which dsimp does not

[Kyle Miller]

dsimp only [C] makes sure to not use dsimp lemmas (simp lemmas that are proved by rfl), but it also does some reductions, like beta reduction, etc.

[Kyle Miller]

RFC: lean4#4090