Zulip Chat Archive

Stream: general

Topic: simp [def]


view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

instead of

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

view this post on Zulip 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 :-)

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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