Why does an `ordered_semiring` need to be add cancellative?

Stream: maths

[FR]

Why does an ordered_semiring need to be an add_cancel_comm_monoid?

[Damiano Testa]

This has been a subject of long discussions. A partial fix comes from using co(ntra)variant_classes, but the refactor is taking me a long time!

[FR]

In many cases, there is no add_left_cancel. Also, many lemmas do not need it. Would it become more appropriate if we rename the structure and def a new ordered_semiring?

[Damiano Testa]

My understanding is that norm_num, linarith and likely ring, abel, field_simp use ordered_semiring with its assumptions to work.

Changing the definition of ordered_semiring would break a lot of what is currently in mathlib. This is the ain reason for not having already done what you suggest.

At least, this is how I internalised the issue!

[FR]

I have written a version of algebra/order/ring.lean which ordered_semiring does not need to be an add_cancel_comm_monoid. The previous class is ordered_add_cancel_semiring now. But I'm still confused with canonically_ordered_comm_semiring. I even suspect it is a misspelling of conically_ordered.

[Yaël Dillies]

By canonically ordered we mean that a ≤ b ↔ ∃ c, a + c = b. Never heard of a conical order before.

[FR]

I've seen a similar expression (Conical) in the agda stdlib, although it doesn't refer to exactly the same thing. It doesn't matter. What confuses me is whether a canonically_ordered_comm_semiring is also an ordered_semiring.

[Yaël Dillies]

It currently is not, for the precise reason you started this thread.

[Trebor Huang]

I wonder if there's a counterexample...

[Trebor Huang]

Either I missed some assumptions, or $\{0, 1, \infty\}$ is ...?