# Zulip Chat Archive

## 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
```

instead of

```
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