PosSMulMono and PosSMulStrictMono

Stream: maths

[Martin Dvořák]

Among implication here
https://github.com/leanprover-community/mathlib4/blob/12613ba84831f5fad339756384c2779b07a1dc8d/Mathlib/Algebra/Order/Module/Defs.lean#L53
I cannot find any path from PosSMulMono to PosSMulStrictMono.
If I assume NoZeroSMulDivisors shouldn't PosSMulMono and PosSMulStrictMono be equivalent?
I'm not sure whether my brain is buggy or the list is incomplete.

[Yaël Dillies]

You are right that this implication holds. I don't think it should be an instance though, as it would very clearly loop

[Martin Dvořák]

Thanks for confirming!

Should the section ## Implications contain only the implications for which Mathlib provides an instance? Or can I add info about PosSMulMono -> PosSMulStrictMono as well?

BTW cannot the typeclass-inference algorithm perform graph search instead of tree search? Is it because, for some non-Prop classes, we need to infer multiple instances of the same type?

[Yaël Dillies]

Martin Dvořák said:

Should the section ## Implications contain only the implications for which Mathlib provides an instance? Or can I add info about PosSMulMono -> PosSMulStrictMono as well?

You certainly should add information about non-instances

[Yaël Dillies]

Martin Dvořák said:

cannot the typeclass-inference algorithm perform graph search instead of tree search?

It can, but it seems the current loop detection algorithm is quite lenient (hence loops when it should not)

[Martin Dvořák]

Yaël Dillies said:

Martin Dvořák said:

Should the section ## Implications contain only the implications for which Mathlib provides an instance? Or can I add info about PosSMulMono -> PosSMulStrictMono as well?

You certainly should add information about non-instances

All right! I'm adding it to my TODO list with high priority.

[Martin Dvořák]

Yaël Dillies said:

Martin Dvořák said:

cannot the typeclass-inference algorithm perform graph search instead of tree search?

It can, but it seems the current loop detection algorithm is quite lenient (hence loops when it should not)

OK, I'll take it as a technical debt.

[Martin Dvořák]

Yaël Dillies said:

You certainly should add information about non-instances

#13931

[Yuyang Zhao]

Martin Dvořák said:

Yaël Dillies said:

Martin Dvořák said:

cannot the typeclass-inference algorithm perform graph search instead of tree search?

It can, but it seems the current loop detection algorithm is quite lenient (hence loops when it should not)

OK, I'll take it as a technical debt.

This is https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Ways.20to.20speed.20up.20Mathlib/near/440371144. It may also appear in any mixin even in the case of no loop.