ordered_comm_monoid

Stream: general

[Johan Commelin]

Why is ordered_comm_monoid additive? I thought {x : real | x ≥ 1} is a really nice ordered commutative monoid...

[Chris Hughes]

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

[Johan Commelin]

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]

That makes sense. Btw, isn't {x : real | x ≥ 1} a commutative group?

[Kenny Lau]

inverse?

[Sebastian Zimmer]

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

[Kenny Lau]

that would make 1 have no inverse

[Sebastian Zimmer]

ah good point

[Simon Hudon]

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]

@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]

I think this is a bad doc string

[Mario Carneiro]

it looks like it was copied from something else

[Johan Commelin]

Shall I just remove that sentence?

[Mario Carneiro]

The first sentence also looks fishy

[Mario Carneiro]

is the biconditional provable?

[Kenny Lau]

what is ancestor?

[Johan Commelin]

Mario Carneiro said:

is the biconditional provable?

Je ne sais pas.

[Johan Commelin]

I haven't really thought about this.

[Mario Carneiro]

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

[Johan Commelin]

yup

[Mario Carneiro]

ancestor is a workaround for the fact that an old_structure_cmd doesn't track what structures it is extended from

[Reid Barton]

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

[Kevin Buzzard]

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

[Johan Commelin]

I'm fixing it

[Reid Barton]

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

[Mario Carneiro]

well, the word cancel is notably absent

[Mario Carneiro]

so I'm pretty sure this is deliberate

[Mario Carneiro]

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]

or fin 37 with saturating addition

[Johan Commelin]

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]

You can read the second condition as saying that not lt is also monotone

[Johan Commelin]

Would you like me to add that?

[Mario Carneiro]

it would make sense given the presentation

[Kenny Lau]

why can't I find ordered_comm_monoid?

[Mario Carneiro]

look for ordered_add_comm_monoid

[Mario Carneiro]

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

[Mario Carneiro]

hence the questions about one_le -> nonneg

[Reid Barton]

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

[Mario Carneiro]

that's why the second condition is there

[Mario Carneiro]

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

[Mario Carneiro]

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]

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

[Reid Barton]

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]

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

[Reid Barton]

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]

linear_comm_monoid?

[Reid Barton]

or we could also call this one partially_ordered_comm_monoid if it's less used

[Mario Carneiro]

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]

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

[Reid Barton]

in Lean 4 we will have full Java style then

[Mario Carneiro]

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

[Mario Carneiro]

comm_pomonoid

[Johan Commelin]

What is that vowel i doing there?

[Mario Carneiro]

pomonod?

[Mario Carneiro]

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]

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