difference between dsimp and unfold

Stream: new members

[Rado Kirov]

Working on a problem from Tao's Analysis 3.5, but the question is pretty general.

We have two definitions (side q: why are they abbrev? and not def)

abbrev SetTheory.Set.curry {X Y Z:Set} (f: X ×ˢ Y → Z) : X → Y → Z :=
  fun x y ↦ f ⟨ (⟨ x, y ⟩:OrderedPair), by rw [mem_cartesian]; use x, y ⟩

noncomputable abbrev SetTheory.Set.uncurry {X Y Z:Set} (f: X → Y → Z) : X ×ˢ Y → Z :=
  fun z ↦ f (fst z) (snd z)

and want to prove

theorem SetTheory.Set.curry_uncurry {X Y Z:Set} (f: X → Y → Z) : curry (uncurry f) = f := ...

by trial and answer I found out that unfold will expand the definitions but dsimp, simp and rw wont. How should I think about this properly.

[Rado Kirov]

Also, for the next step to go from

(fun x y ↦ (fun z ↦ f (fst z) (snd z)) ⟨OrderedPair.toObject { fst := ↑x, snd := ↑y }, ⋯⟩) = f

to

(fun x y ↦
    f (fst ⟨OrderedPair.toObject { fst := ↑x, snd := ↑y }, ⋯⟩)
      (snd ⟨OrderedPair.toObject { fst := ↑x, snd := ↑y }, ⋯⟩)) =
  f

I found I can do it by doing simp_only with no theorems. Why does plain simp run one step of the evaluation?

[Ruben Van de Velde]

That's one of the Greek letter reductions that simp does by default. Beta? Try simp -beta only if that leaves it alone

[Rado Kirov]

Makes sense. Is ‘simp’ the preferred way to run beta reduction? I think the reduced form is defeq so I have also seen using ‘change’ but then one has to spell out the outcome which is cumbersome

[Aaron Liu]

I prefer dsimp but there's also beta_reduce from mathlib