simp [def]

Stream: general

[Kevin Buzzard]

I have really got into the habit recently, when making new definitions for teaching (e.g. foo), to instantly make lemma foo_def : foo = <definition> := rfl so that my students can rw foo_def instead of having to fire up simp [foo] or whatever. But occasionally I am lazy and don't do it. Earlier today I saw someone here encouraging someone else to use this simp [def] as the way to unfold a definition. But I've just found to my surprise that simp [def] might not be idempotent:

def foo : ℕ × ℕ → ℤ := λ ab, (ab.1 : ℤ) - ab.2

example (ab : ℕ × ℕ) : foo ab = 37 :=
begin
  cases ab with a b,
  -- ⊢ foo (a, b) = 37
  simp [foo],
  -- ⊢ ↑((a, b).fst) - ↑((a, b).snd) = 37
  simp [foo],
  -- ⊢ ↑a - ↑b = 37
end

I was surprised! If I make a simp lemma then the issue seems to go away.

[Mario Carneiro]

Actually a foo_def doesn't fix it:

def foo : ℕ × ℕ → ℤ := λ ab, (ab.1 : ℤ) - ab.2
theorem foo_def : foo = λ ab, (ab.1 : ℤ) - ab.2 := rfl

example (ab : ℕ × ℕ) : foo ab = 37 :=
begin
  cases ab with a b,
  -- ⊢ foo (a, b) = 37
  simp [foo_def],
  -- ⊢ ↑((a, b).fst) - ↑((a, b).snd) = 37
end

[Mario Carneiro]

The real issue is the fact that the definitional lemma is unapplied, like the replacement that I wrote manually, because you wrote

def foo : ℕ × ℕ → ℤ := λ ab, (ab.1 : ℤ) - ab.2

instead of

def foo (ab : ℕ × ℕ) : ℤ := (ab.1 : ℤ) - ab.2

[Kevin Buzzard]

Oh yeah! I have a non-idempotent simp example!

def foo : ℕ × ℕ → ℤ := λ ab, (ab.1 : ℤ) - ab.2
@[simp] theorem foo_def : foo = λ ab, (ab.1 : ℤ) - ab.2 := rfl

example (ab : ℕ × ℕ) : foo ab = 37 :=
begin
  cases ab with a b,
  -- ⊢ foo (a, b) = 37
  simp,
  -- ⊢ ↑((a, b).fst) - ↑((a, b).snd) = 37
  simp,
  -- ⊢ ↑a - ↑b = 37
  sorry
end

The reason I thought the simp lemma fixed it was that I instinctively moved stuff to the left of the colon when writing the lemma :-)

[Julian Berman]

instead of having to fire up simp [foo] or whatever

Can someone explain the rationale slightly more? I've also been told before to create foo_def lemmas, and then I also noticed that simp [def] worked and wondered why rw foo_def was any better than simp [def] -- is the point a performance optimization somehow? Or is it that rw is easier to apply selectively in a long expression? Or other?

[Mario Carneiro]

Generally, the definitional equations aren't stated exactly the way you want. If they are then rewriting with the definition is fine

[Mario Carneiro]

like in kevin's example, the definition might be stated as def foo : ℕ × ℕ → ℤ := λ ab, (ab.1 : ℤ) - ab.2 but the actual "definitional lemma" that should be used in simps is

@[simp] theorem foo_def (a b : ℕ) : foo (a, b) = (a : ℤ) - b

[Mario Carneiro]

In this case you can get an equivalent effect by using the equation compiler to write the definition, i.e.

@[simp] def foo : ℕ × ℕ → ℤ
| (a, b) := (a : ℤ) - b

but this definition is not defeq to the original one, and there are reasons to prefer the definition the way kevin wrote it