Difference between simp and unfold?

Stream: new members

[aron]

I'm not clear on the difference between simp and unfold. I only found out about the unfold tactic yesterday and now I'm confused because I thought simp would already unfold all definitions marked with the @[simp] attribute?

[aron]

Or is the difference that simp only unfolds a function definition when it knows the concrete values of all parameters, whereas unfold forces the specified definitions to be unfolded even when not all their params' definite values are known?

[Bjørn Kjos-Hanssen]

Generally, simp won't unfold unless you "ask it to".
(Intuitively, too much unfolding is almost the opposite of simplifying!)
Example:

import Mathlib
def a : ℕ := 0
example : a = 0 := by simp [a] -- works
example : a = 0 := by unfold a;  simp -- works
example : a = 0 := by  simp -- doesn't work

[Tanner Duve]

simp applies all relevant simp lemmas to the target. unfold just replaces a term with its definition. yes simp does indeed unfold all definitions that do have a @[simp] attribute, but not all definitions have a @[simp] attribute, and simp lemmas are not just definitions.

[Kyle Miller]

unfold a b c is similar to simp only [a]; simp only [b]; simp only [c].

aron said:

Or is the difference that simp only unfolds a function definition when it knows the concrete values of all parameters

simp uses the equation lemmas. This means it's not about concrete vs non-concrete, but whether the patterns in the arguments correspond to the patterns that appear in the definition. (E.g., Nat.add m (n + 1) can be unfolded with simp since there's a pattern in the definition of Nat.add this, namely | a, b + 1 => ...)

The unfold c tactic uses the c.eq_def lemma for definition c. This doesn't use equation lemmas, but instead unfolds the definition itself (it's not restricted to applications that correspond to the patterns). However, since it uses c.eq_def and not the c.eq_unfold lemma, it only unfolds if the function is given enough arguments.