Zulip Chat Archive

Stream: general

Topic: X_of_Y_of_Z naming


view this post on Zulip Kevin Buzzard (Apr 11 2018 at 22:45):

What theorem is called X_of_Y_of_Z? Is it Y -> Z -> X or Z -> Y -> X or even something else? Or are things more fluid than this?

view this post on Zulip Chris Hughes (Apr 11 2018 at 22:47):

Y -> Z -> X

view this post on Zulip Chris Hughes (Apr 11 2018 at 22:47):

as in lt_of_le_of_lt

view this post on Zulip Kevin Buzzard (Apr 11 2018 at 22:47):

Right, that's why I asked.

view this post on Zulip Kevin Buzzard (Apr 11 2018 at 22:47):

I just don't understand how the brackets work

view this post on Zulip Kevin Buzzard (Apr 11 2018 at 22:47):

If "of" means "follows from"

view this post on Zulip Andrew Ashworth (Apr 11 2018 at 22:47):

is of right associative

view this post on Zulip Andrew Ashworth (Apr 11 2018 at 22:48):

since it represents ->

view this post on Zulip Kevin Buzzard (Apr 11 2018 at 22:48):

then Y->Z->X is Y->(Z->X)

view this post on Zulip Kevin Buzzard (Apr 11 2018 at 22:48):

which is (X_of_Z)_of_Y

view this post on Zulip Andrew Ashworth (Apr 11 2018 at 22:48):

it is also a mystery to me, hah

view this post on Zulip Simon Hudon (Apr 11 2018 at 22:49):

I think X_of_Y_of_Z is Y -> Z -> X: only the consequent is out of order in the name

view this post on Zulip Kevin Buzzard (Apr 11 2018 at 22:49):

well (X_of_Y)_of_Z seems to mean Z->(Y->X) and X_of_(Y_of_Z) seems to mean (Z->Y)->X

view this post on Zulip Kevin Buzzard (Apr 11 2018 at 22:50):

So are you clear on the logic? What does A_of_B_of_C_of_D say?

view this post on Zulip Kevin Buzzard (Apr 11 2018 at 22:51):

I don't know these fancy CS terms like consequent by the way

view this post on Zulip Kevin Buzzard (Apr 11 2018 at 22:51):

Sorry

view this post on Zulip Andrew Ashworth (Apr 11 2018 at 22:51):

somewhere, a logician is crying

view this post on Zulip Kevin Buzzard (Apr 11 2018 at 22:51):

next you'll be telling me that something is a minor premise

view this post on Zulip Simon Hudon (Apr 11 2018 at 22:52):

well (X_of_Y)_of_Z seems to mean Z->(Y->X) and X_of_(Y_of_Z) seems to mean (Z->Y)->X

I disagree with that assessment. I would say that A_of_B_of_C_of_D is B -> C -> D -> A

view this post on Zulip Chris Hughes (Apr 11 2018 at 22:52):

I think of doesn't follow right or left associativity rules

view this post on Zulip Simon Hudon (Apr 11 2018 at 22:52):

Consequent is the only positive term in a chain of implications, i.e. the right-most term.

view this post on Zulip Andrew Ashworth (Apr 11 2018 at 22:54):

if i had to guess i would think like simon it's right assoc

view this post on Zulip Andrew Ashworth (Apr 11 2018 at 22:54):

so a_of_b... is B -> C -> D -> A

view this post on Zulip Andrew Ashworth (Apr 11 2018 at 22:54):

so how do we put parentheses in our theorem names? who knows

view this post on Zulip Andrew Ashworth (Apr 11 2018 at 22:55):

oh

view this post on Zulip Andrew Ashworth (Apr 11 2018 at 22:55):

i have seen imp used in theorem names

view this post on Zulip Simon Hudon (Apr 11 2018 at 22:55):

I don't know these fancy CS terms like consequent by the way

I wonder if we could create a sitcom where a mathematician and a computer scientist share a flat. I'm sure they'd get into lots of crazy (conceptual) hijinks

view this post on Zulip Andrew Ashworth (Apr 11 2018 at 22:55):

so (a->b)->c is c_of_a_imp_b

view this post on Zulip Simon Hudon (Apr 11 2018 at 22:56):

if i had to guess i would think like simon it's right assoc

I don't think that's an associativity rule actually.

view this post on Zulip Andrew Ashworth (Apr 11 2018 at 22:56):

if it isn't that way, it should be, it should follow the same rules as ->

view this post on Zulip Andrew Ashworth (Apr 11 2018 at 22:56):

otherwise my brain may explode

view this post on Zulip Simon Hudon (Apr 11 2018 at 22:57):

As for imp, the difference is that you use imp where you would normally use le or lt: and_imp_and_of_imp_of_imp for example to state that conjunction is monotonic in both arguments

view this post on Zulip Andrew Ashworth (Apr 11 2018 at 22:58):

frankly speaking, trying to remember how a theorem should be named is kinda of ridiculous. when lean 4 comes out i'm sure @Moses Schönfinkel will write the Lean SearchAbout we've been waiting for :)

view this post on Zulip Andrew Ashworth (Apr 11 2018 at 23:00):

i have the same general hatred when it comes to reading C++ qualifiers

view this post on Zulip Andrew Ashworth (Apr 11 2018 at 23:01):

the rule is, read it from the right and wrap around, which is terrible

view this post on Zulip Andrew Ashworth (Apr 11 2018 at 23:01):

http://goshdarnfunctionpointers.com

view this post on Zulip Simon Hudon (Apr 11 2018 at 23:02):

Now I remember that fun :)

view this post on Zulip Kevin Buzzard (Apr 11 2018 at 23:10):

Looking through mathlib it does seem to be consistently using X_of_Y_of_Z : Y -> Z -> X

view this post on Zulip Kevin Buzzard (Apr 11 2018 at 23:11):

and there was me thinking there would be some sort of logic ;-)

view this post on Zulip Kevin Buzzard (Apr 11 2018 at 23:12):

lt_of_lt_of_le
lt_of_le_of_lt
pos_of_dvd_of_pos
decidable_of_decidable_of_iff
neg_of_nat_of_succ
lt_add_of_le_of_pos
mem_of_eq_of_mem
mem_of_subset_of_mem
eq_of_subset_of_subset
nat.not_coprime_of_dvd_of_dvd
eq_of_le_of_forall_le_of_dense
mul_nonpos_of_nonpos_of_nonneg
lt_add_of_lt_of_nonneg
eq_of_sublist_of_length_le
not_mem_cons_of_ne_of_not_mem
eq_of_sorted_of_perm
heq_of_heq_of_eq
decidable_of_decidable_of_iff
div_of_neg_of_pos

view this post on Zulip Chris Hughes (Apr 11 2018 at 23:18):

Does it really matter? If I want pos_of_dvd_of_pos and I get pos_of_pos_of_dvd they're both the same thing.

view this post on Zulip Kevin Buzzard (Apr 11 2018 at 23:19):

oh they are very anal about names here :-)

view this post on Zulip Kevin Buzzard (Apr 11 2018 at 23:20):

looking through that stacks file you wrote I see lemma thingy ... so perhaps you are less fussy than them ;-)

view this post on Zulip Simon Hudon (Apr 11 2018 at 23:25):

The logic I see is: <something>_of_<list_of_assumptions_separated_by_of> and that list of assumptions is in the order that you should feed them to a function application if you build the proof term by hand. You could advocate for <list_of_assumptions_separated_by_of>_of_<something> so that the name mentions assumptions in the same order as the type but I think it's very useful that the first thing you see in the name is what you can achieve with it.

view this post on Zulip Kevin Buzzard (Apr 11 2018 at 23:33):

Yes that's why they went for of rather than imp, right? I like that, I just can't make any sense of the logic for the rest of it when there are two ofs

view this post on Zulip Simon Hudon (Apr 11 2018 at 23:35):

You mean like lt_of_lt_of_le? It proves lt from two assumptions: 1. lt; 2. le. The order of those assumptions is the same as in the name

view this post on Zulip Kevin Buzzard (Apr 11 2018 at 23:35):

right, as in lt_of_lt_and_le

view this post on Zulip Simon Hudon (Apr 11 2018 at 23:36):

Yeah, exactly

view this post on Zulip Kevin Buzzard (Apr 11 2018 at 23:36):

but not as in lt_is_implied_by_lt_which_is_implied_by_le

view this post on Zulip Kevin Buzzard (Apr 11 2018 at 23:36):

i.e. not as in lt_of_lt_of_le

view this post on Zulip Kevin Buzzard (Apr 11 2018 at 23:36):

if "of" is supposed to mean "is implied by"

view this post on Zulip Kevin Buzzard (Apr 11 2018 at 23:38):

and also not as in "(lt_is_implied_by_lt)_is_implied_by_le"

view this post on Zulip Kevin Buzzard (Apr 11 2018 at 23:38):

but actually exactly as in "(lt_is_implied_by_le)_is_implied_by_lt"

view this post on Zulip Kevin Buzzard (Apr 11 2018 at 23:38):

i.e. exactly "(lt_of_le)_of_lt"

view this post on Zulip Simon Hudon (Apr 11 2018 at 23:38):

Right. I guess that's where the associativity talk is relevant. It's (lt of lt) of le with the little twist that the assumptions are shuffled ..

view this post on Zulip Kevin Buzzard (Apr 11 2018 at 23:38):

Aah

view this post on Zulip Kevin Buzzard (Apr 11 2018 at 23:39):

for you X -> Y ->Z and Y -> X -> Z are exactly the same

view this post on Zulip Simon Hudon (Apr 11 2018 at 23:39):

Yes. As you said

view this post on Zulip Simon Hudon (Apr 11 2018 at 23:39):

Because it's equivalent to lt_of_lt_and_le, the assumptions commute

view this post on Zulip Simon Hudon (Apr 11 2018 at 23:40):

They are logically equivalent

view this post on Zulip Kevin Buzzard (Apr 11 2018 at 23:40):

so you're saying lt_of_lt_of_le and lt_of_le_of_lt should be defeq? ;-)

view this post on Zulip Simon Hudon (Apr 11 2018 at 23:40):

Nooooooo, no, no, no! :stuck_out_tongue_closed_eyes:

view this post on Zulip Kevin Buzzard (Apr 11 2018 at 23:41):

then why did you name one after what the other one does? ;-)

view this post on Zulip Simon Hudon (Apr 11 2018 at 23:41):

Because I'm a bad person

view this post on Zulip Simon Hudon (Apr 11 2018 at 23:43):

Of course the names leave out important information that we have to rely on your imagination to fill in. The full name should be x_lt_z_of_x_lt_y_of_y_le_z. Then swapping the assumptions is not semantically meaningful, it's just confusing.

view this post on Zulip Simon Hudon (Apr 11 2018 at 23:43):

Note: defeq and logically equivalent, are not the same by the way ;-)

view this post on Zulip Mario Carneiro (Apr 12 2018 at 00:32):

The X_of_Y_of_Z means Y -> Z -> X convention is used throughout mathlib, and it was documented a long time ago in Jeremy's style notes

view this post on Zulip Kevin Buzzard (Apr 12 2018 at 00:32):

Yes, I learnt that now, from example

view this post on Zulip Kevin Buzzard (Apr 12 2018 at 00:32):

I was just querying the logic

view this post on Zulip Mario Carneiro (Apr 12 2018 at 00:33):

The hypotheses are listed in the order they appear, not reverse order. For example, the theorem A → B → C would be named C_of_A_of_B.

https://github.com/leanprover/mathlib/blob/master/docs/naming.md

view this post on Zulip Mario Carneiro (Apr 12 2018 at 00:34):

The logic is, the consequent is the most important part, so it comes first (this is important for autocomplete), but otherwise there is no reshuffling of names from the order they appear in the statement or the order you use them

view this post on Zulip Mario Carneiro (Apr 12 2018 at 00:36):

Don't think too hard about currying these things, theorems are generally fully applied anyway

view this post on Zulip Moses Schönfinkel (Apr 12 2018 at 08:15):

@Andrew Ashworth I 100% will.


Last updated: May 10 2021 at 00:31 UTC