make `MulOpposite` a structure

Stream: mathlib4

[Kevin Buzzard]

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 2022-12-15T13:00:00Z 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]

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]

That looks klike a bug in the linter to me

[Eric Wieser]

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]

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

[Scott Morrison]

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

[Gabriel Ebner]

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]

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]

So what do I do?

[Eric Wieser]

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]

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]

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]

For now it's safe to mark as nolint.

[Eric Wieser]

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]

Mario has already fixed the linter.