## Stream: general

### Topic: Simp normal form

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

Does #2017 stop simpputting 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?

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 }


@[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 equivs 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