# Zulip Chat Archive

## Stream: general

### Topic: Simp normal form

#### Kevin Buzzard (Feb 22 2020 at 00:52):

Does #2017 stop `simp`

putting things in simp normal form? Is that not what simp is supposed to do?

#### Chris Hughes (Feb 22 2020 at 00:53):

I think maybe it should say right hand side.

#### Kevin Buzzard (Feb 22 2020 at 00:57):

I've just read some of the discussion and it actually seems like quite a subtle issue

#### Yury G. Kudryashov (Feb 22 2020 at 17:39):

No, it stops users from creating unusable simp lemmas. If lhs of a lemma gets simplified to some other form before simp tries to apply this lemma, then simp will never rewrite on this lemma.

#### Kevin Buzzard (Feb 22 2020 at 18:54):

I would naively say that if a goal is not in simp normal form because something is expressed in a non canonical manner then the only simp lemma in the entire library which mentions that noncanonical form will be the one turning it into the canonical form

#### Kevin Buzzard (Feb 22 2020 at 18:55):

So no other simp lemma will change it. But this doesn't seem to be what people wiser than me are saying in the discussion

#### Gabriel Ebner (Feb 22 2020 at 19:27):

The question is not about the current goal. The simplifier simplifies terms inside-out, that is, it first simplifies the arguments of a function before simplifying the function. Hence a simp lemma is only ever used to rewrite terms where the arguments are already fully simplified (= in simp-normal form). Corollary: if the left-hand side of your simp lemma has an argument that is not fully simplified, then this simp lemma is never used to rewrite a term by the simplifier and is hence useless.

#### Johan Commelin (Feb 22 2020 at 19:27):

@Kevin Buzzard What's being discussed is maybe best illustrated with an example. Both you and me would think that for the prime spectrum of a ring

@[simp] lemma zero_locus_bot : zero_locus (\bot : ideal R) = univ := sorry

is a very good simp-lemma. But there is a catch:`zero_locus`

expects a subset, so the ideal is coerced to a set. So in fact, the lemma is saying: `zero_locus \u\bot = univ`

, with a little up-arrow.

Now suppose that `zero_locus \u\bot`

occurs in your goal, and you call `simp`

. Then the simplifier starts doing its little tricks, and one of the first things it realises is that

@[simp] lemma coe_bot : ((\bot : ideal R) : set R) = {0} := sorry

is a wonderful simp-lemma that applies to this goal. So it applies it.

The goal now contains `zero_locus {0}`

and hence the simp-lemma `zero_locus_bot`

will never trigger.

~~I guess that this could be fixed by carefully applying priorities.~~ But another way to fix it is to make sure that the LHS of a simp-lemma can't be further simplified, aka, is in simp normal form.

#### Johan Commelin (Feb 22 2020 at 19:29):

@Gabriel Ebner Please correct me if I just wrote a bunch of nonsense.

#### Gabriel Ebner (Feb 22 2020 at 19:31):

Everything you say is correct, except for:

I guess that this could be fixed by carefully applying priorities.

This cannot be fixed using priorities since the simplifier works inside-out (= innermost first = arguments first). It never tries to rewrite the term `zero_locus ↑⊥`

, the first time it comes to a term of the form `zero_locus _`

it is already rewritten to `zero_locus {0}`

.

#### Johan Commelin (Feb 22 2020 at 19:41):

@Gabriel Ebner But whether something is in simp-normal-form may depend on the imported files, right?

#### Gabriel Ebner (Feb 22 2020 at 19:41):

Precisely.

#### Johan Commelin (Feb 22 2020 at 19:43):

So I can maneuver myself into a situation where some simp-lemmas are still useless, even thought they look potentially useful.

#### Alex J. Best (Feb 22 2020 at 21:54):

I saw one example recently where a simp lemma I thought should fire didn't, it seems like the same problem but it looks like it wasn't changed in #2017, can anyone explain:

example (s : set ℕ) (h : s.nonempty) : s ≠ ∅ := begin simpa, end

should work as `set.ne_empty_iff_nonempty`

is a simp lemma, but we have to do

example (s : set ℕ) (h : s.nonempty) : s ≠ ∅ := begin simpa [-ne.def], end

instead as simp first changes `s ≠ ∅`

to `⊢ ¬s = ∅`

.

#### Gabriel Ebner (Feb 22 2020 at 22:24):

The current `simp_nf`

linter only checks that the *arguments* are in simp-normal form. I've had some performance troubles with checking that the whole lhs is in normal form (see recent PR about looping simp lemmas). (In your examples, the arguments are `s`

and `\emptyset`

and they are in nf.) This will soon come together with a linter that checks for redundant simp lemmas.

#### Alex J. Best (Feb 22 2020 at 22:25):

Ah okay that makes sense, thanks!

#### Mario Carneiro (Feb 22 2020 at 23:05):

One simplification you can do to the check is to first find all terms that are never part of simp normal form because there is a simp lemma that rewrites them away (for example, `sub`

and `ne`

) and then check that a simp lhs never contains these symbols

#### Kevin Buzzard (Feb 22 2020 at 23:33):

Either that or unsimp the lemma which rewrites them away...

#### Bryan Gin-ge Chen (Dec 11 2020 at 20:40):

There's a `simp_nf`

linter complaint in #5324 and I'm not sure how best to address it.

`data.equiv.basic`

currently has:

```
@[simp] theorem symm_symm (e : α ≃ β) : e.symm.symm = e := by { cases e, refl }
```

The PR adds:

```
@[simp] theorem symm_symm_apply (f : α ≃ β) (b : α) : f.symm.symm b = f b := rfl
```

and this is needed for `dsimp`

purposes.

Changing the priority / ordering of these two lemmas in the file doesn't seem to silence the linter, but removing `@[simp]`

from `symm_symm`

does. Is that an OK solution?

#### Eric Wieser (Dec 11 2020 at 20:41):

Removing `symm_symm`

might means terms like `equiv.arrow_congr e.symm.symm`

don't get simplified any more

#### Eric Wieser (Dec 11 2020 at 20:42):

I've seen a lot of places where `equiv`

s are unapplied, and it would be a shame for those not to be simplified.

#### Eric Wieser (Dec 11 2020 at 20:44):

The reason changing the priority has no effect is that simplification goes from the inside out

#### Eric Wieser (Dec 11 2020 at 20:44):

And the former is a subexpression of the latter

#### Reid Barton (Dec 11 2020 at 20:45):

I guess the linter complains about `symm_symm_apply`

?

#### Reid Barton (Dec 11 2020 at 20:46):

It sounds to me like the linter is wrong because of this simp vs. dsimp thing

#### Eric Wieser (Dec 11 2020 at 20:47):

Should we have a `dsimp`

attribute that aliases `simp`

but is ignored by the linter?

#### Eric Wieser (Dec 11 2020 at 20:47):

I tried `@[_refl_lemma] theorem symm_symm_apply`

but `dsimp`

doesn't find it

#### Bryan Gin-ge Chen (Dec 11 2020 at 20:47):

So for now should we just `nolint simp_nf`

?

#### Reid Barton (Dec 11 2020 at 20:48):

Actually the linter could see that `symm_symm_apply`

is a refl lemma... and maybe only consider other refl lemmas when checking it for simp normal form?

#### Eric Wieser (Dec 11 2020 at 22:17):

@Bhavik Mehta, what's the advantage of having this as a dsimp lemma; or in general, in using `dsimp`

over `simp`

? I don't really understand what dsimp is useful for yet.

#### Kevin Buzzard (Dec 11 2020 at 22:23):

I personally use `dsimp`

when I want to figure out what the heck the goal is so I can proceed, and then once I know which lemma to apply next I just delete the dsimp.

#### Floris van Doorn (Dec 12 2020 at 00:31):

@Reid Barton What is the "simp vs. dsimp thing"?

#### Reid Barton (Dec 12 2020 at 00:31):

`symm_symm_apply`

is not in simp normal form, but it is in "dsimp normal form"

#### Floris van Doorn (Dec 12 2020 at 00:33):

Oh, I see. `symm_symm`

cannot be proven by reflexivity.

I think adding a `nolint`

is a good solution for now. If it comes up frequently we can consider adding a new attribute.

#### Floris van Doorn (Dec 12 2020 at 00:47):

@Eric Wieser `dsimp`

can be useful if you don't want to change the goal too much: it guarantees that the resulting goal is definitionally equal to the original goal.

Sometimes the fact that `dsimp`

only uses definitional rewriting means that it can rewrite in a place that would lead to a type-incorrect goal otherwise.

For example, compare the resulting goal when using `simp`

versus `dsimp`

```
example (n : ℕ) (v w : vector bool (n + 0)) : v = w :=
by { simp [nat.add_zero] at v, }
```

Note that `simp`

creates a *new* local constant `v`

and the goal talks about the *old* constant `v`

(because if the type of the new `v`

was actually different than of the original `v`

, then the goal would be type incorrect). Here `dsimp`

does what you want, while `simp`

doesn't.

Last updated: May 08 2021 at 11:09 UTC