## Stream: general

### Topic: naming issues

#### Kenny Lau (May 02 2018 at 07:41):

#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 (May 02 2018 at 07:41):

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

#### Mario Carneiro (May 02 2018 at 08:57):

what's the issue?

#### Kenny Lau (May 02 2018 at 09:40):

what's the issue?

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

#### Mario Carneiro (May 02 2018 at 09:43):

no? there is no usage of gt in those lemmas

#### Kenny Lau (May 02 2018 at 09:43):

I mean, how can both be lt

#### Kenny Lau (May 02 2018 at 09:43):

so does lt imply sub_pos or sub_neg?

both...

#### Mario Carneiro (May 02 2018 at 09:44):

it's just a matter of where the variables go

#### Mario Carneiro (May 02 2018 at 09:45):

in mathlib the analogous theorem is just called sub_pos

aha

#### Johan Commelin (May 02 2018 at 09:46):

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

#### Mario Carneiro (May 02 2018 at 09:46):

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

#### Simon Hudon (May 02 2018 at 12:43):

maybe -x should be called minus instead of neg?

#### Johan Commelin (Apr 07 2020 at 08:03):

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)


a pomonoid :-)

#### Alex J. Best (Apr 07 2020 at 08:11):

Cancellative partially ordered monoid?

#### Alex J. Best (Apr 07 2020 at 08:12):

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

#### Alex J. Best (Apr 07 2020 at 08:13):

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 (Apr 07 2020 at 08:20):

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 (Apr 07 2020 at 08:22):

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

#### Johan Commelin (Apr 07 2020 at 08:22):

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.

Last updated: May 09 2021 at 19:11 UTC