Zulip Chat Archive

Stream: general

Topic: naming issues


view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (May 02 2018 at 08:57):

what's the issue?

view this post on Zulip Kenny Lau (May 02 2018 at 09:40):

what's the issue?

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

view this post on Zulip Mario Carneiro (May 02 2018 at 09:43):

no? there is no usage of gt in those lemmas

view this post on Zulip Kenny Lau (May 02 2018 at 09:43):

I mean, how can both be lt

view this post on Zulip Kenny Lau (May 02 2018 at 09:43):

so does lt imply sub_pos or sub_neg?

view this post on Zulip Mario Carneiro (May 02 2018 at 09:43):

both...

view this post on Zulip Mario Carneiro (May 02 2018 at 09:44):

it's just a matter of where the variables go

view this post on Zulip Mario Carneiro (May 02 2018 at 09:45):

in mathlib the analogous theorem is just called sub_pos

view this post on Zulip Kenny Lau (May 02 2018 at 09:45):

aha

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Simon Hudon (May 02 2018 at 12:43):

maybe -x should be called minus instead of neg?

view this post on Zulip 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)

view this post on Zulip Kevin Buzzard (Apr 07 2020 at 08:06):

a pomonoid :-)

view this post on Zulip Alex J. Best (Apr 07 2020 at 08:11):

Cancellative partially ordered monoid?

view this post on Zulip Alex J. Best (Apr 07 2020 at 08:12):

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

view this post on Zulip 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.

view this post on Zulip 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 R0\mathbb{R}_{\geq0}

view this post on Zulip 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.

view this post on Zulip 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