Zulip Chat Archive

Stream: general

Topic: Simp normal form


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

view this post on Zulip Chris Hughes (Feb 22 2020 at 00:53):

I think maybe it should say right hand side.

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

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

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

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

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

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

view this post on Zulip Johan Commelin (Feb 22 2020 at 19:29):

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

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

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

view this post on Zulip Gabriel Ebner (Feb 22 2020 at 19:41):

Precisely.

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

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

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

view this post on Zulip Alex J. Best (Feb 22 2020 at 22:25):

Ah okay that makes sense, thanks!

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

view this post on Zulip Kevin Buzzard (Feb 22 2020 at 23:33):

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

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

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

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

view this post on Zulip Eric Wieser (Dec 11 2020 at 20:44):

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

view this post on Zulip Eric Wieser (Dec 11 2020 at 20:44):

And the former is a subexpression of the latter

view this post on Zulip Reid Barton (Dec 11 2020 at 20:45):

I guess the linter complains about symm_symm_apply?

view this post on Zulip Reid Barton (Dec 11 2020 at 20:46):

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

view this post on Zulip Eric Wieser (Dec 11 2020 at 20:47):

Should we have a dsimp attribute that aliases simp but is ignored by the linter?

view this post on Zulip Eric Wieser (Dec 11 2020 at 20:47):

I tried @[_refl_lemma] theorem symm_symm_apply but dsimp doesn't find it

view this post on Zulip Bryan Gin-ge Chen (Dec 11 2020 at 20:47):

So for now should we just nolint simp_nf?

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

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

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

view this post on Zulip Floris van Doorn (Dec 12 2020 at 00:31):

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

view this post on Zulip Reid Barton (Dec 12 2020 at 00:31):

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

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

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