Zulip Chat Archive

Stream: mathlib4

Topic: make `MulOpposite` a structure


Kevin Buzzard (Dec 15 2022 at 11:44):

I have started on this refactor at mathlib4#1036 . I'd claimed that I would have no time today but I'll push on a bit on the tube to work right now, so I'd like to "claim" this PR for the next hour; I will push some time before and then if anyone else wants a go then please feel free but perhaps also flag that you're working on it in this thread, as ideally we don't want people duplicating work.

Kevin Buzzard (Dec 15 2022 at 12:45):

Oh wow I've got all of mathlib4 building with the change. Very minimal changes were needed, which was surprising to me given that I changed the definition of a declaration which is used in a lot of places. This bodes very well for other changes of this nature, like order_dual.

A few rfls (which were working because of defeq abuse) needed to be changed into by exact rfl for some reason. Is this something I should think about?

The only other issue was that a linter I didn't know existed complained about the following two declarations:

@semiconj_by_unop :  {α : Type u} [inst : Mul α] {a x y : αᵐᵒᵖ}, SemiconjBy a.unop y.unop x.unop  SemiconjBy a x y

and

@commute_unop :  {α : Type u} [inst : Mul α] {x y : αᵐᵒᵖ}, Commute x.unop y.unop  Commute x y

are now (together with their additivised versions) victims of this:

/- The `simpComm` linter reports:
COMMUTATIVITY LEMMA IS SIMP.
Some commutativity lemmas are simp lemmas: -/

Should I really not mark them as simp?? These look fine to me.

Eric Wieser (Dec 15 2022 at 12:54):

That looks klike a bug in the linter to me

Eric Wieser (Dec 15 2022 at 12:54):

Unless lean knows how to match against a b: α commute a b by filling out the arguments withcommute (unop (op a)) (unop (op b)) in which case we're in trouble

Kevin Buzzard (Dec 15 2022 at 15:25):

I can report -- I don't have a clue about linters though. Is this in Std or core or mathlib?

Scott Morrison (Dec 16 2022 at 08:19):

@Kevin Buzzard, it's in Std.Tactic.Lint.Simp.

Gabriel Ebner (Dec 18 2022 at 02:39):

Eric Wieser said:

Unless lean knows how to match against a b: α commute a b by filling out the arguments withcommute (unop (op a)) (unop (op b)) in which case we're in trouble

The thing is, Lean knows to do that know. This is just an instance of structure eta.

Gabriel Ebner (Dec 18 2022 at 02:41):

The "good" news is that the discrimination trees don't know that, so simp will only apply the lemma if there's a literal unop in the term.

Kevin Buzzard (Dec 18 2022 at 08:45):

So what do I do?

Eric Wieser (Dec 18 2022 at 16:46):

This isn't even "structure eta" is it? This is proj (ctor x) = x not ctor (proj x) = x, which I think is iota reduction, and at any rate is true definitionally in Lean3.

Gabriel Ebner (Dec 18 2022 at 18:32):

Yes, you're right. But I don't think the unifier even tried to solve that one before. Now it can solve x =?= ?x.unop.

Kevin Buzzard (Dec 18 2022 at 19:08):

I don't understand this conversation really, but is the conclusion that the linter is buggy and I should mark this as "don't lint" and leave a porting note and open an issue, or is the conclusion that the linter is not buggy and I should not mark this with simp, or is the conclusion that the linter is not buggy and these lemmas should not even exist in mathlib4, or is the conclusion something else, or is there no conclusion as yet?

Gabriel Ebner (Dec 18 2022 at 19:08):

For now it's safe to mark as nolint.

Eric Wieser (Dec 18 2022 at 22:14):

It would be great if you could open an issue against the linter, and reference the issue number in a comment next to the nolint; that way, we can clean up all the nolints eventually

Gabriel Ebner (Dec 18 2022 at 22:47):

Mario has already fixed the linter.


Last updated: Dec 20 2023 at 11:08 UTC