Zulip Chat Archive

An issue came up in this file. One is that the simp attribute on unionᵢ_interᵢ_ge_nat_add triggered the linter Left-hand side does not simplify, when using the simp lemma on itself. This usually means that it will never apply. However, it does seem to apply when used on itself. Maybe a linter bug?

Patrick Massot (Dec 21 2022 at 10:24):

Kevin Buzzard (Dec 21 2022 at 11:39):

And as Eric points out, both this example and the other example have ge in.

Kevin Buzzard (Dec 21 2022 at 15:23):

@Chris Hughes your example is essentially the same lemma as Patrick's and in that thread Gabriel is suggesting that it's a bad simp lemma for other reasons; you'll understand them better than I do and if they also apply in your case then you can just remove the simp, add a porting note and at least you're unblocked, even though we don't actually understand what's going on.

Kevin Buzzard (Dec 21 2022 at 15:43):

I've recorded the issue here but clearly the short term solution is just to remove the simp and move on.

Eric Wieser (Dec 21 2022 at 16:49):

Note that the forward-port at mathlib4#1109 will conflict with the port of this file; which takes priority here? Do we make the forward-porter redo the forward-port, or make the porter redo the port?

Patrick Massot (Dec 21 2022 at 16:58):

This is really a mess. I think that each day brings us closer to the day where touching a mathlib3 file this already ported will simply be totally forbidden (maybe with some very rare exceptions discussed among maintainers).