CanonicallyOrderedMul.toOrderBot

Stream: mathlib4

[Violeta Hernández]

Currently, any type with a canonically ordered multiplication/addition will automatically get an OrderBot instance, with bottom 1/0 respectively. Is this desirable?

[Violeta Hernández]

On the one hand, a type whose bottom element is either 1 or 0 will almost surely have an OrderBot instance which sets ⊥ = 1 or ⊥ = 0 as a def-eq. But also, it seems like somewhat of an antipattern to have a more complicated instance setting a def-eq on a simpler instance.

[Violeta Hernández]

I imagine this must've been discussed during @Yuyang Zhao's refactor. Is this behavior intentional?

[Ruben Van de Velde]

Sounds odd to me as well

[Violeta Hernández]

I mostly want to know if this is an intentional decision. If it is, there's a few proofs in the Algebra.Order.Canonical.Monoid.Defs file that can be golfed by def-eqs to theorems on bot.

[Violeta Hernández]

If it's not, then maybe it should be addressed?

[Eric Wieser]

This sounds safe enough as is to me

[Eric Wieser]

I don't think the "deriving data from data" concern applies when the process is the identity function.

[Violeta Hernández]

If this def-eq is intentional, I've made a PR golfing some proofs by using it: #21203

[Yaël Dillies]

Possibly relevant: In #19193, I made docs#CanonicallyOrderedCommMonoidWithZero extend docs#OrderBot

[Yaël Dillies]

Oh wait, did my refactor get undone immediately?

[Violeta Hernández]

Seems intact: docs#LinearOrderedCommMonoidWithZero

[Yaël Dillies]

Ah sorry, brain was clearly off