duplicate instances of `PosMulMono` and friends

Stream: mathlib4

[Jovan Gerbscheid]

I noticed that docs#PosMulMono.toCovariantClass and docs#PosMulMono.to_covariantClass_pos_mul_le are duplicates. One is declared with extends and the other with instance.

Should the extends be replaced with a def? (in #22090, it was changed from an abbrev to an extends by @Floris van Doorn)

[Eric Wieser]

Dropping the explicit instance one would be consistent with the goal of #22090

[Jovan Gerbscheid]

The goal of #22090 was to stop PosMulMono from unfolding into CovariantClass .. during type class search. This goal is also achieved if we use a def instead of an abbrev

[Eric Wieser]

I'm not sure there is any benefit to using a def though, usually we do that as a compromise when the class is too problematic

[Eric Wieser]

Here I think @Floris van Doorn forgot to clean up the duplicate when he introduces the extends instance

[Jovan Gerbscheid]

I think it's not his fault, because those duplicates were already unnecessary from the start.

[Jovan Gerbscheid]

Also I didn't realize it isn't possible to mark a def as a class, so keeping the extends instances is the way.

[Eric Wieser]

Jovan Gerbscheid said:

I think it's not his fault, because those duplicates were already unnecessary from the start.

I would guess then that actually that PR was unecessary (but perhaps a good idea anyway), and the performance issue is the instance you identified.

[Jovan Gerbscheid]

The performance issue was that CovariantClass α≥0 α (fun x y => y * x) (· ≤ ·) has bad discrimination tree keys, and this problem was definitely resolved by that PR.

Though there is a chance that removing these extra instances will also give a performace improvement.

[Jovan Gerbscheid]

(if I remember correctly)

[Jovan Gerbscheid]

Oh, one instance is talking about the type α≥0 and the other about α>0, my mistake.