# Zulip Chat Archive

## Stream: general

### Topic: ordered_comm_monoid

#### Johan Commelin (Sep 29 2018 at 17:54):

Why is `ordered_comm_monoid`

additive? I thought `{x : real | x ≥ 1}`

is a really nice ordered commutative monoid...

#### Chris Hughes (Sep 29 2018 at 17:58):

Because most ordered comm monoids are additive, like reals, ints, nats, rats, with_bot nat

#### Johan Commelin (Sep 29 2018 at 18:00):

Sure, but we could still have the `add`

in the name right? And I think there are enough examples where they aren't additive, like positive reals, nats, positive rats...

#### Simon Hudon (Sep 29 2018 at 19:57):

That makes sense. Btw, isn't `{x : real | x ≥ 1}`

a commutative group?

#### Kenny Lau (Sep 29 2018 at 19:59):

inverse?

#### Sebastian Zimmer (Sep 29 2018 at 20:13):

Is your group operation (x, y) -> (x - 1)(y - 1) + 1 or something crazy like that?

#### Kenny Lau (Sep 29 2018 at 20:15):

that would make 1 have no inverse

#### Sebastian Zimmer (Sep 29 2018 at 20:15):

ah good point

#### Simon Hudon (Sep 29 2018 at 20:26):

Right, somehow, the fact that the inverse is less than one escaped me. You'd need { x : real | x > 0 } for a group.

#### Johan Commelin (May 27 2020 at 08:43):

@Mario Carneiro How should I interpret the last line of this docstring?

```
/-- An ordered commutative monoid is a commutative monoid
with a partial order such that multiplication is an order embedding, i.e.
`a * b ≤ a * c ↔ b ≤ c`. These monoids are automatically cancellative. -/
@[ancestor comm_monoid partial_order]
class ordered_comm_monoid (α : Type*) extends comm_monoid α, partial_order α :=
(mul_le_mul_left : ∀ a b : α, a ≤ b → ∀ c : α, c * a ≤ c * b)
(lt_of_mul_lt_mul_left : ∀ a b c : α, a * b < a * c → b < c)
```

Does this mean that this class is supposed to replace `ordered_cancel_add_comm_monoid`

which was recently liberated from core?

#### Mario Carneiro (May 27 2020 at 08:44):

I think this is a bad doc string

#### Mario Carneiro (May 27 2020 at 08:44):

it looks like it was copied from something else

#### Johan Commelin (May 27 2020 at 08:44):

Shall I just remove that sentence?

#### Mario Carneiro (May 27 2020 at 08:44):

The first sentence also looks fishy

#### Mario Carneiro (May 27 2020 at 08:45):

is the biconditional provable?

#### Kenny Lau (May 27 2020 at 08:46):

what is `ancestor`

?

#### Johan Commelin (May 27 2020 at 08:47):

Mario Carneiro said:

is the biconditional provable?

Je ne sais pas.

#### Johan Commelin (May 27 2020 at 08:47):

I haven't really thought about this.

#### Mario Carneiro (May 27 2020 at 08:47):

it's not listed in the immediate theorems so I would guess no

#### Johan Commelin (May 27 2020 at 08:47):

yup

#### Mario Carneiro (May 27 2020 at 08:48):

`ancestor`

is a workaround for the fact that an `old_structure_cmd`

doesn't track what structures it is extended from

#### Reid Barton (May 27 2020 at 08:48):

It's not provable, since the ordering could be `=`

.

#### Kevin Buzzard (May 27 2020 at 08:49):

I think it has been pointed out before that this docstring was wrong

#### Johan Commelin (May 27 2020 at 08:49):

I'm fixing it

#### Reid Barton (May 27 2020 at 08:49):

Are we sure it's not the definition that's wrong?

#### Mario Carneiro (May 27 2020 at 08:50):

well, the word `cancel`

is notably absent

#### Mario Carneiro (May 27 2020 at 08:50):

so I'm pretty sure this is deliberate

#### Mario Carneiro (May 27 2020 at 08:51):

I think it's supposed to be used as an additive-only version of ordered semirings that are not cancellative, like `with_top nat`

#### Mario Carneiro (May 27 2020 at 08:51):

or `fin 37`

with saturating addition

#### Johan Commelin (May 27 2020 at 08:52):

How is this:

```
/-- An ordered commutative monoid is a commutative monoid
with a partial order such that
* `a ≤ b → c * a ≤ c * b` (multiplication is monotone)
* `a * b < a * c → b < c`.
-/
@[ancestor comm_monoid partial_order]
class ordered_comm_monoid (α : Type*) extends comm_monoid α, partial_order α :=
(mul_le_mul_left : ∀ a b : α, a ≤ b → ∀ c : α, c * a ≤ c * b)
(lt_of_mul_lt_mul_left : ∀ a b c : α, a * b < a * c → b < c)
```

#### Mario Carneiro (May 27 2020 at 08:53):

You can read the second condition as saying that `not lt`

is also monotone

#### Johan Commelin (May 27 2020 at 08:53):

Would you like me to add that?

#### Mario Carneiro (May 27 2020 at 08:54):

it would make sense given the presentation

#### Kenny Lau (May 27 2020 at 08:54):

why can't I find `ordered_comm_monoid`

?

#### Mario Carneiro (May 27 2020 at 08:54):

look for `ordered_add_comm_monoid`

#### Mario Carneiro (May 27 2020 at 08:54):

I assume Johan is in the middle of a refactor to make a multiplicative version

#### Mario Carneiro (May 27 2020 at 08:55):

hence the questions about `one_le -> nonneg`

#### Reid Barton (May 27 2020 at 08:55):

What's an example of something with the first condition but not the second?

#### Mario Carneiro (May 27 2020 at 08:55):

that's why the second condition is there

#### Mario Carneiro (May 27 2020 at 08:55):

it's basically always true, but it's only redundant if the order is total

#### Mario Carneiro (May 27 2020 at 09:08):

I think an example is fin 2 x fin 2 with saturating pointwise addition and the product partial order. Let `a = (1,0)`

, `b = (1,0)`

and `c = (0,1)`

. Then `a + b = (1,0) < a + c = (1,1)`

, but `¬ (b < c)`

.

#### Mario Carneiro (May 27 2020 at 09:15):

That said, this property might be too strong, effectively saying that the order is total without saying it

#### Reid Barton (May 27 2020 at 09:16):

It seems to me that the second condition doesn't belong there but it happens to be true for the instances we have, mostly because they are totally ordered

#### Mario Carneiro (May 27 2020 at 09:16):

right, so it might be better to upgrade the class so that it assumes a total order

#### Reid Barton (May 27 2020 at 09:19):

I'd claim `ordered_comm_monoid`

is just `mul_le_mul_left`

and the other one is `totally_ordered_comm_monoid`

, but maybe that's too long

#### Mario Carneiro (May 27 2020 at 09:20):

`linear_comm_monoid`

?

#### Reid Barton (May 27 2020 at 09:21):

or we could also call this one `partially_ordered_comm_monoid`

if it's less used

#### Mario Carneiro (May 27 2020 at 09:21):

I think I recall some parent instance getting near the 100 character limit... you couldn't even type it with the usual indentation style

#### Reid Barton (May 27 2020 at 09:21):

these names don't seem to be very common anyways, so it's hard to say what's standard

#### Reid Barton (May 27 2020 at 09:21):

in Lean 4 we will have full Java style then

#### Mario Carneiro (May 27 2020 at 09:22):

I don't think you can put newlines in a namespaced name, can you?

#### Mario Carneiro (May 27 2020 at 09:25):

`comm_pomonoid`

#### Johan Commelin (May 27 2020 at 09:28):

What is that vowel `i`

doing there?

#### Mario Carneiro (May 27 2020 at 09:29):

pomonod?

#### Mario Carneiro (May 27 2020 at 09:30):

I would much rather make up quirky names for things we can't find in the literature than have overly descriptive 40+ character names

#### Reid Barton (May 27 2020 at 09:43):

Well, Wikipedia has https://en.wikipedia.org/wiki/Ordered_semigroup (which even contains the word "pomonoid")

Last updated: Aug 03 2023 at 10:10 UTC