Stream: general

Topic: simp [def]

Kevin Buzzard (Mar 04 2021 at 10:56):

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 (Mar 04 2021 at 10:59):

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 (Mar 04 2021 at 11:00):

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


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


Kevin Buzzard (Mar 04 2021 at 11:00):

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 (Mar 04 2021 at 13:45):

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 (Mar 04 2021 at 13:58):

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

Mario Carneiro (Mar 04 2021 at 14:00):

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 (Mar 04 2021 at 14:01):

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

Last updated: May 14 2021 at 07:19 UTC