Simp normal form

Stream: general

[Kevin Buzzard]

Does #2017 stop simpputting things in simp normal form? Is that not what simp is supposed to do?

[Chris Hughes]

I think maybe it should say right hand side.

[Kevin Buzzard]

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

[Yury G. Kudryashov]

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]

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]

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]

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]

@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]

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

[Gabriel Ebner]

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]

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

[Gabriel Ebner]

Precisely.

[Johan Commelin]

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

[Alex J. Best]

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]

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]

Ah okay that makes sense, thanks!

[Mario Carneiro]

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]

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

[Bryan Gin-ge Chen]

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]

Removing symm_symm might means terms like equiv.arrow_congr e.symm.symm don't get simplified any more

[Eric Wieser]

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]

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

[Eric Wieser]

And the former is a subexpression of the latter

[Reid Barton]

I guess the linter complains about symm_symm_apply?

[Reid Barton]

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

[Eric Wieser]

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

[Eric Wieser]

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

[Bryan Gin-ge Chen]

So for now should we just nolint simp_nf?

[Reid Barton]

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]

@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]

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]

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

[Reid Barton]

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

[Floris van Doorn]

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]

@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.