simp and subsingleton instances

Stream: general

[Rob Lewis]

I was debugging some strange behavior #11315 with @Heather Macbeth and noticed (once again) things were pretty slow. It reminded me of type class issues we had a while back, so I looked at the instance search trace, and the trace for a tiny simp onlythat took 300ms was > 15k lines long. It's entirely failing searches for subsingleton instances.

[Rob Lewis]

With local attribute [-instance] char_p.subsingleton unique.subsingleton is_empty.subsingleton the time for that simp only goes down to 40ms.

[Rob Lewis]

The failures seem to be cached properly -- this is a goal with a lot of different types in it, although it's probably no bigger than most at the leafier corners of the library.

[Rob Lewis]

Which means that these subsingleton instances are costing a lot of compile time. char_p.subsingleton seems especially rare to fire, but at least it doesn't lead to another open search like the others, it fails a bit quicker.

[Rob Lewis]

I feel like this discussion has happened before, but I can't find where or remember the conclusion. On a scale of 1-10, how painful would it be to remove these instance, making them defs or localized?

[Eric Rodriguez]

#6025 for reference

[Reid Barton]

I would assume removing char_p.subsingleton as an instance would be somewhere around a 1.

[Reid Barton]

I'm sort of surprised unique isn't just defined as subsingleton + inhabited.

[Reid Barton]

Not that it would necessarily help.

[Eric Rodriguez]

Char_p does need rewriting with out_param, imo

[Eric Rodriguez]

So I wonder if that will help to remove that instance too

[Rob Lewis]

Eric Rodriguez said:

#6025 for reference

Thanks! Glad I wasn't making up those memories

[Rob Lewis]

Reid Barton said:

I would assume removing char_p.subsingleton as an instance would be somewhere around a 1.

Also the least effective, since it leads to fewer branches in the type class search

[Rob Lewis]

But probably good to do anyway

[Gabriel Ebner]

Do you have a mathlib-free mwe for the subsingleton simp issue? It might be easier to reduce the subsingleton queries in simp.

[Sebastien Gouezel]

https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.235672.20breaks.20timeout/near/223034983

[Jeremy Avigad]

I also struggled with the problem a while ago (and asked about it here on Zulip). At the time, this magical incantation solved all my problems:
https://github.com/starkware-libs/formal-proofs/blob/master/src/util.lean#L494-L504
It requires putting open_locale disable_subsingleton_simps at the top of subsequent files.

[Eric Rodriguez]

Maybe we should make a simp-set for subsingleton-related simp lemmas, and that will fix the issue indirectly

[Gabriel Ebner]

lean#665 For testing it would be great if somebody could port mathlib to 3.37 (otherwise I'll have to rebase the change to 3.36).

[Rob Lewis]

Thanks Gabriel!!

[Rob Lewis]

I see you just clicked merge on the 3.37 update :smile:

[Alex J. Best]

Does this close lean#521 then?

[Gabriel Ebner]

It fixes the problems that bug causes, not the bug itself.

[Gabriel Ebner]

The biggest problem with this refactoring so far is the following: simp [if_congr] doesn't work, it doesn't pick up if_congr as a congruence lemma.
Similarly, attribute [my_simp_set] if_congr also (silently) fails.

[Gabriel Ebner]

Automatically detecting whether something is a congr lemma or a simp lemma is also hard.

For example: eq_comm : a = b ↔ b = a can be both a congr lemma (for the = function, without hypotheses), or a simp lemma.

[Rob Lewis]

How common is it/will it be to need to give custom congr lemmas to simp?

[Gabriel Ebner]

Right now, very. Because simp only doesn't include any congr lemmas.

[Gabriel Ebner]

simp only should probably use the global congr lemmas.

[Gabriel Ebner]

This is a much more useful change than I'd expected. The automatically generated congr lemmas were simply broken because they generated decidable instance diamonds. While porting mathlib, I need to add a lot of *_congr lemmas but in exchange simp becomes more powerful.

[Rob Lewis]

Amazing, any sense if simp has gotten faster too?

[Gabriel Ebner]

I'm currently in data.multiset.basic.

[Gabriel Ebner]

Benchmarks will need to wait a little.

[Gabriel Ebner]

Hmm, this now runs into limitations with congr lemmas. :sad:

Simply put, we cannot declare a manual congr lemma for ite p a b x. I'll try to generate the lemmas automatically.

[Gabriel Ebner]

Okay, mathlib builds now, so there shouldn't be any major issues left. :-P https://github.com/leanprover-community/mathlib/compare/sscongr?expand=1

lean#665 now automatically creates the congr lemmas that we expect for decidability arguments, that is,
∀ ... [i : decidable p] [j : decidable q], @f p i = @f q j.

If there is a rough consensus that we want this, then I'd like to merge the Lean PR and get a new release out soon. (So that the mathlib branch doesn't rot too much.)

[Rob Lewis]

Cool!

[Rob Lewis]

Are there reasons we wouldn't want this? The diff generally looks like an improvement to me

[Gabriel Ebner]

It's a somewhat hacky approach, since it only supports decidable arguments. We want the same treatment for e.g. fintype as well, but there custom congr lemmas are still required (for example fintype.card_congr).

There's also the question about how this will work in Lean 4. But if it is a welcome change for mathlib, then that makes it easier to push for the same behavior in Lean 4.

[Gabriel Ebner]

I've also changed simp only to apply @[congr] lemmas (with no way to opt out), this could be controversial as well.

[Sebastien Gouezel]

Just to check that I understand what you are doing here. You made a change in core after which simp does not try to infer subsingleton instances on everything, right (which should be a nice performance improvement)? But to make sure simp still remains powerful enough, you have added a bunch of congr lemmas (either created by hand, or autogenerated) to imitate the old behavior. Right?

[Gabriel Ebner]

Yes, simp no longer infers subsingleton instances everywhere (although the simp lemma eq_iff_true_of_subsingleton will of course infer subsingleton instances for every equality).

The subsingleton instances were used by simp to create better congruence lemmas, simp could rewrite list.filter xs p to list.filter xs p' because the [decidable_pred p] argument was a subsingleton. The downside of this feature was that the new decidable_pred instance was eq.rec ... _inst_1 (i.e., a beautiful diamond). The subsingleton change made simp significantly less powerful, by no longer being able to rewrite the predicate in list.filter (and lots of other other functions).

Writing all these congruence lemmas (such as for list.filter) is cumbersome and didn't work in all cases (such as for ite p f g x). Therefore the PR includes a second (more significant) change, which adds special support for decidable instance arguments in the congruence lemma generator. As a bonus, it now generates congruence lemmas that avoid diamonds.

[Rob Lewis]

Personally I think it's a net improvement even with the hackiness! The fact that adding innocent looking subsingleton instances can have such a huge effect on the most important tactic feels like a pretty bad thing. If the fix improves instance diamonds, even better.

[Anne Baanen]

Gabriel Ebner said:

If there is a rough consensus that we want this, then I'd like to merge the Lean PR and get a new release out soon.

I'm in favour of the concept, especially since there are not too many changes to mathlib and quite a few are strictly better. Let me do a quick code review.

[Anne Baanen]

Gabriel Ebner said:

I've also changed simp only to apply @[congr] lemmas (with no way to opt out), this could be controversial as well.

Would it be a lot of work to implement opting out of specific congr lemma by re-using the simp only [simp_lemma, -congr_lemma] symtax?

[Eric Wieser]

count_congr seems to be missing @[congr] in the mathlib branch above?

[Gabriel Ebner]

Would it be a lot of work to implement opting out of specific congr lemma by re-using the simp only [simp_lemma, -congr_lemma] symtax?

Not a lot of work (but it might require a new simp_lemmas.erase_congr function). I don't think we require this anywhere though. PRs are of course welcome.

[Gabriel Ebner]

count_congr seems to be missing @[congr] in the mathlib branch above?

Thanks, I deleted them.

[Johan Commelin]

@Gabriel Ebner I managed to bump LTE to this newest version of mathlib. It went quite smoothly, and I was happy to see a bunch of congr's gone, because simp became more powerful.

Is there some commit message that explains exactly what changed, and how users should update their mental model of simp? Does this warrant a short blogpost? It seems to me one of the biggest changes to Lean in several months.
(Aside: do you think the changes impacted the performance of simp -- up or down?)

[Riccardo Brasca]

Ah, that's why today's bump of the flt-regular was more complicated than usual (nothing special, but usually it's just that some lemmas landed in mathlib and are duplicated)

[Gabriel Ebner]

@Johan Commelin You shouldn't need to update your mental model of simp. The only thing that changed is that simp now magically does the expected thing more often. The closest thing to an explanation is my response to Sébastien above: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/simp.20and.20subsingleton.20instances/near/267492975 I can also write a longer explanation for the blog if you think that's interesting.

Re: performance improvement. I think mathlib's gotten a little faster, but nothing spectacular. Hopefully Jannis' bot will give more substantial data to evaluate the change. I also tried removing the local attribute [-instance] commands in mathlib, but there's still two of those analysis lemmas timing out (to be fair, they're already at the edge of timing out right now).

[Johan Commelin]

Ok, thanks for confirming that I can kepp using simp as I'm used to. I could imagine a blogpost about the congr-lemma change. But you are in a better position to judge whether there's enough material for a story. I just got the impression that this was one of the more substantial changes to Lean in quite a while, so it might be worth it.