Ordered monoids

Stream: maths

[Antoine Chambert-Loir]

These two lemmas on nat are definitely useful.

lemma nat.add_lt_add_of_le_lt (a b c d : ℕ) (hac : a ≤ c) (hbd : b < d) : a + b < c + d :=
    lt_of_lt_of_le (add_lt_add_left hbd a) (add_le_add_right hac d)

lemma nat.add_lt_add_of_lt_le (a b c d : ℕ) (hab : a < c) (hbd : b ≤ d) : a + b < c + d :=
  lt_of_lt_of_le (add_lt_add_right hab b) (add_le_add_left hbd c)

Although they are easy to reprove each time, shouldn't they belong to mathlib ?
Probably in the framework of ordered monoids (if not magmas), rather than natural numbers,
but I don't have the impression that general ordered monoids exist in mathlib, only commutative ones…

[Eric Rodriguez]

docs#mul_lt_mul_of_le_of_lt, docs#add_lt_add_of_lt_of_le exist

[Notification Bot]

Antoine Chambert-Loir has marked this topic as resolved.

[Notification Bot]

Antoine Chambert-Loir has marked this topic as unresolved.

[Antoine Chambert-Loir]

(Not that I care too much about the answer , but the question about ordered monoids remains…)

[Eric Rodriguez]

Ordered monoids basically got "removed" in favour of co(ntra)variant_class, because this approach allows more flexibility. cc @Damiano Testa who started the refactor

[Damiano Testa]

Yes, I think that the consensus was that for a type with a single operation and a single relation, it was more flexible to have a single class that would be expressive enough to say which monotonicity was assumed on which side.

For types with two operations and one relation, there is some consensus that the current ordered_semiring is too strong and @Yaël Dillies is fixing this.

[Damiano Testa]

The general idea is that you should find the lemmas such as the one you mentioned by looking for a mixin of covariants and mul/add, but you may be able to unlock it from an ordered_semiring-like assumption as well, since these bigger typeclasses will have the relevant covariant instances on them.

[Antoine Chambert-Loir]

I see what you mean.
But wouldn't some shortcuts be useful ? Such as a ordered_magma (instance, or type ?),
which would automatically brings in *, <=, < and the correct covariant_class instance ?

[Damiano Testa]

There is a fine balance between number of typeclasses, instance between them and potential combinations. All choices lead to exponential blow ups. In your situation, you may want * to possibly be +, < is a stand-in for has_lt, preorder, partial_order, linear_order, plus, do you want to assume co(ntra)variant for strict inequality, weak inequality, both?

I think that it was decided that there weren't enough names to make everyone happy and separating

• what class of operation you want, from has_mul/add to group/add_group,
• what kind of order relation you want,
• which monotonicity and on which side of the operation you want,

was a solution that would provide the right assumptions to most people.

[Damiano Testa]

Right now, covariant_class has no typeclass assumptions: these are locked in once you start filling in the fields of the class and then the class converts into the appropriate covariance of the provided operation with respect to the provided relation.

It does not matter which typeclass assumptions are made on the operation/relation. In fact, the operation is usually + or *, but it does not have to be and the relation is usually </le, but again they do not need to be. Even more, the "operation" could be an action of one type on another, which is useful for when you want to have monotonicity only with respect to a subtype of the given type: you only want monotonicity of multiplication when the element is positive.