Unfolding definitions: `dsimp`, `unfold`, `delta` or `simp`?

Stream: new members

[Louis Cabarion]

When unfolding a definition, what are some good rules of thumb for deciding between dsimp, unfold, delta, or simp?

For a simple definition, what is the idiomatic go-to choice, and which are better suited for special cases?

My guess would be that the "go-to choice" would be dsimp or unfold, but I'm not certain about when should one use dsimp instead of unfold, and vice versa.

[Ruben Van de Velde]

Maybe we should remove a few of those :)

[Alfredo Moreira-Rosa]

i use dsimp when i have annotated some definitions as simp, unfold when not, and when i want to mix unfolding with non annotated simplication rules (not just definitions), i use simp

[Violeta Hernández]

unfold foo is basically the same as dsimp only [foo], but I don't see the harm in having it. I've never used or even seen delta besides one or two times, isn't it one of those low-level tactics you're not supposed to use?

[Violeta Hernández]

dsimp and simp are very different. The former only accepts lemmas that are definitionally true, which makes it much more robust as a way to just unfold definitions. Meanwhile simp accepts any collection of equalities/equivalences, and will rewrite and rewrite in some potentially arbitrary order until it can't simplify anymore. Due to the decreased robustness (a proof might break if you add or remove a simp lemma somewhere) the advice is to use it only as a finishing tactic (the last tactic in a block), or to explicitly specify the simp set using simp only.

[Louis Cabarion]

For educational purposes, I’ve tried collecting the different methods one might use to transform the goal f = 3 ∧ True into 1 + 2 = 3 ∧ True (or further into 3 = 3 ∧ True) given the definition def f := 1 + 2.

The idea is to show tactics that you can reasonably expect to see "in the wild" in real Lean code.

1. Am I missing any obvious method here (see examples below)?
2. For this specific example, which approaches would be considered the most idiomatic, which are less idiomatic but still fine, and which would be regarded as unusual or "weird"?

[Louis Cabarion]

import Mathlib

def f := 1 + 2

example : f = 3 ∧ True := by
  unfold f
  -- ⊢ 1 + 2 = 3 ∧ True
  trivial

example : f = 3 ∧ True := by
  delta f
  -- ⊢ 1 + 2 = 3 ∧ True
  trivial

example : f = 3 ∧ True := by
  dsimp only [f]
  -- ⊢ 1 + 2 = 3 ∧ True
  trivial

example : f = 3 ∧ True := by
  rewrite [f]
  -- ⊢ 1 + 2 = 3 ∧ True
  trivial

example : f = 3 ∧ True := by
  rw [f]
  -- ⊢ 1 + 2 = 3 ∧ True
  trivial

example : f = 3 ∧ True := by
  change 1 + 2 = 3 ∧ True
  -- ⊢ 1 + 2 = 3 ∧ True
  trivial

example : f = 3 ∧ True := by
  show 1 + 2 = 3 ∧ True
  -- ⊢ 1 + 2 = 3 ∧ True
  trivial

example : f = 3 ∧ True := by
  dsimp [f]
  -- 3 = 3 ∧ True
  trivial

example : f = 3 ∧ True := by
  reduce
  -- ⊢ 3 = 3 ∧ True
  trivial

[Louis Cabarion]

Bump: Is unfold f the idiomatic "default choice" for simple cases like the one in the example? If so, what are some good examples of when it makes sense to use one of the other eight alternatives listed above instead?

[Kenny Lau]

the idiomatic default is to not rely on unfolding definitions

[Kenny Lau]

nobody needs to know that an ideal I being maximal is defined to be IsCoatom I

[Kenny Lau]

nobody ever unfolds the definition of Finset.image, you always use the lemma Finset.mem_image.

[Rado Kirov]

So ideomaric lean every def has a _mem or _def theorem even if it just repeats the def?

[Kenny Lau]

honestly that's what I would prefer but they don't do that every time

[Kenny Lau]

let's say every non-low level def should have a _def theorem

[Kenny Lau]

actually that's exactly the job of @[simps!] to generate those helper theorems

[Kenny Lau]

(we call those the "API")

[Louis Cabarion]

Kenny Lau said:

the idiomatic default is to not rely on unfolding definitions

I see your point.

I suppose we can distinguish two scenarios:

1. There is an existing API (or we’re in a position to add one). In that case, we should prefer using the API rather than unfolding definitions. To be concrete: for the toy example below, what would the idiomatic API look like?

2. There isn’t an API (and it’s not feasible for us to add one). In that situation, would unfold f generally be considered the idiomatic "default choice" for the toy example? What are some good examples of when it makes sense to use one of the other eight alternatives listed above instead?

Toy example:

import Mathlib

def f := 1 + 2

example : f = 3 ∧ True := by
  unfold f
  -- ⊢ 1 + 2 = 3 ∧ True
  trivial

[Damiano Testa]

I think that in the toy example there is no need for any of the titular tactics:

def f := 1 + 2

-- By hand, generally to be avoided
example : f = 3 ∧ True := by
  unfold f
  -- ⊢ 1 + 2 = 3 ∧ True
  trivial

-- This should be part of the API
theorem f_def : f = 1 + 2 := rfl

-- Now you can prove it as follows
example : f = 3 ∧ True := by
  rw [f_def]
  trivial

[Damiano Testa]

From a slightly further away perspective, whatever the current definition of f is, may change later on. However, most likely, the fact that the current definition is actually a valid definition for f would not change. So, the statement of the theorem f_def should still be true, just its proof may change.

E.g., at some later point, someone may realize that actually it would be easier to define f as 10^700 - 10^700 + 3, instead of 1 + 2. It is still true that f is equal to 1 + 2, although the proof may no longer be rfl (in this toy example, the proof is still actually rfl, but the literal code that proves it breaks).

[Alfredo Moreira-Rosa]

Unfolding has a lot of legitimate use cases:

• unfolding your own definitions when you build your API
• unfolding definitions for lack of API (so extending APIs)
• unfolding programs for program proofs (not everything is math oriented)
  I certainly miss a lot of use cases.

[Kenny Lau]

the first two points still imply that API is better than unfolding (i.e. unfold only when building API), and the third point is out of my area so i can't comment.