mathlib

mathlib copied to clipboard

• Add unique instances when the codomain types are subsingletons and rename the original unique instances (which apply when the domain is empty) to unique_of_is_empty. These are in analogy to pi.unique and pi.unique_of_is_empty.

• Golf the unique instances for (d)finsupp using fun_like.coe_injective.unique. The names unique_of_left and unique_of_right remain unchanged in the finsupp case, because finsupp is special in that it consists of non-dependent functions, unlike dfinsupp or direct_sum.

(There was a concern that adding unique instances would slow down simp (see #6025), but it has been fixed in lean#665.)

---

It was intentionally not an instance due to https://github.com/leanprover-community/mathlib/issues/6025 (potential performance issues), but now CI seems happy with this change.

I mentioned this on the other PR, but I think the real reason for making this into an instance is that the problem was specifically about subsingleton, and this is a unique instance.

I mentioned this on the other PR, but I think the real reason for making this into an instance is that the problem was specifically about subsingleton, and this is a unique instance.

I don't understand. If mv_polynomial.unique remains a def, then there is no subsingleton instance on mv_polynomial. If it's an instance, then there is one, via unique.subsingleton, and this subsingleton instance may cause performance issue according to #6025.

I don't know what the rule on what instances to avoid is, then. I've added a few unique and is_empty instances myself and I've never received feedback regarding #6025.

Maybe @eric-wieser can explain since he made the decision at #9124. I've personally been hit by this issue; if adding an instance causes a timeout then you'd definitely change it to a def and add a reference to #6025. But in this case it seems CI is happy from the beginning, so the decision seems strange to me.

The decision to avoid adding subsingleton or unique instances was made not to directly avoid a deterministic timeout, but rather to avoid making an already bad performance problem even worse.

I believe it was @sgouezel who advocated for it originally.

IIRC, one of the reason that we care so much about subsingleton instances is because simp used to eagerly look for ways to apply subsingleton.elim. I think @gebner might have more recently changed this behavior in core so that it doesn't do this; which might mean we can re-evaluate the decision.

What would it take to re-evaluate the decision? Any performance metric readily available? Build time depends a lot on which files are touched and resources on the machines. Randomly sample some files and build from scratch and count the heartbeat?

This PR is blocking #15889, so if it's gonna take a long time to re-evaluate, we may as well merge #15889 now.

I think re-evaluating #6025 is a discussion best had on Zulip; perhaps resuming the original thread.

Oh I see there are plenty of methods for performance testing in the original thread, which I haven't looked into before.

Thanks to @sgouezel who pointed out on Zulip that the subsingleton issue was fixed by lean#665.

So we can just make everything into an instance again, right?

So we can just make everything into an instance again, right?

I think so and you are welcome to submit a PR removing those gh-6025 references and hacks as I mentioned on Zulip. We can use set_option profiler true to measure any potential slowdown caused by the removal of the hacks on the subsequent proofs. I also plan to revive my old PR and see if I can now safely add the subsingleton instance ...

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests