ordered_comm_monoid

Stream: maths

[Yury G. Kudryashov]

I want to add two typeclasses:

@[to_additive]
class weakly_ordered_comm_monoid (α : Type*) extends comm_monoid α, partial_order α :=
(mul_le_mul_left       : ∀ a b : α, a ≤ b → ∀ c : α, c * a ≤ c * b)

class canonically_weakly_ordered_add_monoid (α : Type*) extends weakly_ordered_add_comm_monoid α, order_bot α :=
(le_iff_exists_add : ∀a b:α, a ≤ b ↔ ∃c, b = a + c)

The main use cases for the second class are measure α and α → enreal. The axiom

(lt_of_add_lt_add_left : ∀ a b c : α, a + b < a + c → b < c)

doesn't work in these cases. E.g., for bool → ennreal the counterexample is given by a = λ x, cond x 0 ∞, b = λ x, cond x 0 1, c = λ x, cond x 1 0, a + b = λ x, cond x 0 ∞, a + c = λ x, cond x 1 ∞.

What do you think about this? Do you have better names for these classes?

[Johan Commelin]

I think those are useful. I'm just starting to wonder if we should transition to mixins in the order-meets-algebra part of the library...

[Scott Morrison]

Sorry to necro this thread, but

1. Where does our definition of ordered_comm_monoid with the additional axiom lt_of_add_lt_add_left : ∀ a b c : α, a + b < a + c → b < c come from (in the literature)? It is not the standard definition.
2. I'm sure we've discussed this before --- can anyone find an old thread?
3. Did @Yury G. Kudryashov find a different solution to his problem besides introducing weakly_ordered_comm_monoid?

[Kevin Buzzard]

@Damiano Testa ?

[Eric Wieser]

docs#has_le_iff_exist_add and the covariant stuff should cover the weaker axiomatization?

[Eric Wieser]

Hmm, I was sure we had that somewhere

[Alex J. Best]

There was the thread "canonically_ordered pathologies" is that relevant?

[Scott Morrison]

It seems (still :fencing:) that I may just be able to correct the definition to match the rest of the worlds, with minimal damage to mathlib...

[Scott Morrison]

#8877

[Eric Wieser]

I found the typeclass I was thinking of, edited above.

[Johan Commelin]

I'm happy with merging this. But since it drops 4 lemmas, maybe some other @maintainers want to have a look as well.

[Anne Baanen]

I think it's a good idea to remove the hypothesis from ordered_comm_monoid since we bring the library better in line with common usage, and if someone really needs the original version, there is a typeclass that provides it.

I'd rather not delete any lemmas if they can still be formulated in a useful way, but if the four deleted lemmas are never used, then I'm not so concerned.

[Sebastien Gouezel]

I had a look at the PR, and I'm fine with removing the lemmas.

[Floris van Doorn]

I'd be very happy to remove this field from ordered_comm_monoid. It would be very nice to make measure an ordered_add_comm_monoid.

Please don't remove the lemmas from ordered_sub though, but reformulate them for ordered_cancel_add_comm_monoid with an extra contravariant_class ... (<) axiom.
It is still a WIP to use the lemmas in ordered_sub throughout the library, so it's pretty likely that you're removing something that will be used in the library soon.

[Floris van Doorn]

I'm surprised so little breaks in the library by this change!

[Scott Morrison]

I was surprised too. I thought it was going to be a disaster, but mostly it is actually deleting unnecessary proofs!

[Scott Morrison]

I've restored these lemmas, adding a contravariant_class _ _ (+) (<) hypothesis. Hopefully this PR is good to go again.