naming issues

Stream: general

[Kenny Lau]

#check sub_pos_of_lt
-- sub_pos_of_lt : ?M_4 < ?M_3 → 0 < ?M_3 - ?M_4
#check sub_neg_of_lt
-- sub_neg_of_lt : ?M_3 < ?M_4 → ?M_3 - ?M_4 < 0
#check sub_nonpos_of_le
-- sub_nonpos_of_le : ?M_3 ≤ ?M_4 → ?M_3 - ?M_4 ≤ 0
#check sub_nonneg_of_le
-- sub_nonneg_of_le : ?M_4 ≤ ?M_3 → 0 ≤ ?M_3 - ?M_4

[Kenny Lau]

but I know the answer already: this is in core so we can't do nothing about it

[Mario Carneiro]

what's the issue?

[Kenny Lau]

what's the issue?

shouldn't one be lt and the other be gt?

[Mario Carneiro]

no? there is no usage of gt in those lemmas

[Kenny Lau]

I mean, how can both be lt

[Kenny Lau]

so does lt imply sub_pos or sub_neg?

[Mario Carneiro]

both...

[Mario Carneiro]

it's just a matter of where the variables go

[Mario Carneiro]

in mathlib the analogous theorem is just called sub_pos

[Kenny Lau]

aha

[Johan Commelin]

Lol, we need Lean to generate the names for us, given the type. Then we can have provably correct names

[Mario Carneiro]

although the usage of pos and neg as names for >0 and <0 is problematic since it overlaps neg meaning -x

[Simon Hudon]

maybe -x should be called minus instead of neg?

[Johan Commelin]

What is the correct name for the following class?

class give_me_a_name (α : 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)

[Kevin Buzzard]

a pomonoid :-)

[Alex J. Best]

Cancellative partially ordered monoid?

[Alex J. Best]

Is it equivalent to $a b \le a c \iff b \le c$ ?

[Alex J. Best]

Ahh I guess its not right, if I take $\ZZ_{\ge 0}$ then $0 * 3 \le 0 * 1$ but $3 \le 1$ is false.

[Kevin Buzzard]

Yes, this all comes up from the general "group with 0" thing meant to encapsulate targets of valuations/norms such as $\mathbb{R}_{\geq0}$

[Alex J. Best]

Yeah I found several references online to translation invariant monoids and pomonoids, but they all mean this stronger thing.

[Johan Commelin]

Alex J. Best said:

Cancellative partially ordered monoid?

You might want to call it an ordered_comm_monoid... but those already exist: just replace * with + in the definition.