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: Dec 20 2023 at 11:08 UTC