Zulip Chat Archive

Stream: general

Topic: X_of_Y_of_Z naming


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?

Chris Hughes (Apr 11 2018 at 22:47):

Y -> Z -> X

Chris Hughes (Apr 11 2018 at 22:47):

as in lt_of_le_of_lt

Kevin Buzzard (Apr 11 2018 at 22:47):

Right, that's why I asked.

Kevin Buzzard (Apr 11 2018 at 22:47):

I just don't understand how the brackets work

Kevin Buzzard (Apr 11 2018 at 22:47):

If "of" means "follows from"

Andrew Ashworth (Apr 11 2018 at 22:47):

is of right associative

Andrew Ashworth (Apr 11 2018 at 22:48):

since it represents ->

Kevin Buzzard (Apr 11 2018 at 22:48):

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

Kevin Buzzard (Apr 11 2018 at 22:48):

which is (X_of_Z)_of_Y

Andrew Ashworth (Apr 11 2018 at 22:48):

it is also a mystery to me, hah

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

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

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?

Kevin Buzzard (Apr 11 2018 at 22:51):

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

Kevin Buzzard (Apr 11 2018 at 22:51):

Sorry

Andrew Ashworth (Apr 11 2018 at 22:51):

somewhere, a logician is crying

Kevin Buzzard (Apr 11 2018 at 22:51):

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

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

Chris Hughes (Apr 11 2018 at 22:52):

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

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.

Andrew Ashworth (Apr 11 2018 at 22:54):

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

Andrew Ashworth (Apr 11 2018 at 22:54):

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

Andrew Ashworth (Apr 11 2018 at 22:54):

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

Andrew Ashworth (Apr 11 2018 at 22:55):

oh

Andrew Ashworth (Apr 11 2018 at 22:55):

i have seen imp used in theorem names

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

Andrew Ashworth (Apr 11 2018 at 22:55):

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

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.

Andrew Ashworth (Apr 11 2018 at 22:56):

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

Andrew Ashworth (Apr 11 2018 at 22:56):

otherwise my brain may explode

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

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 :)

Andrew Ashworth (Apr 11 2018 at 23:00):

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

Andrew Ashworth (Apr 11 2018 at 23:01):

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

Andrew Ashworth (Apr 11 2018 at 23:01):

http://goshdarnfunctionpointers.com

Simon Hudon (Apr 11 2018 at 23:02):

Now I remember that fun :)

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

Kevin Buzzard (Apr 11 2018 at 23:11):

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

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

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.

Kevin Buzzard (Apr 11 2018 at 23:19):

oh they are very anal about names here :-)

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 ;-)

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.

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

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

Kevin Buzzard (Apr 11 2018 at 23:35):

right, as in lt_of_lt_and_le

Simon Hudon (Apr 11 2018 at 23:36):

Yeah, exactly

Kevin Buzzard (Apr 11 2018 at 23:36):

but not as in lt_is_implied_by_lt_which_is_implied_by_le

Kevin Buzzard (Apr 11 2018 at 23:36):

i.e. not as in lt_of_lt_of_le

Kevin Buzzard (Apr 11 2018 at 23:36):

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

Kevin Buzzard (Apr 11 2018 at 23:38):

and also not as in "(lt_is_implied_by_lt)_is_implied_by_le"

Kevin Buzzard (Apr 11 2018 at 23:38):

but actually exactly as in "(lt_is_implied_by_le)_is_implied_by_lt"

Kevin Buzzard (Apr 11 2018 at 23:38):

i.e. exactly "(lt_of_le)_of_lt"

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 ..

Kevin Buzzard (Apr 11 2018 at 23:38):

Aah

Kevin Buzzard (Apr 11 2018 at 23:39):

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

Simon Hudon (Apr 11 2018 at 23:39):

Yes. As you said

Simon Hudon (Apr 11 2018 at 23:39):

Because it's equivalent to lt_of_lt_and_le, the assumptions commute

Simon Hudon (Apr 11 2018 at 23:40):

They are logically equivalent

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? ;-)

Simon Hudon (Apr 11 2018 at 23:40):

Nooooooo, no, no, no! :stuck_out_tongue_closed_eyes:

Kevin Buzzard (Apr 11 2018 at 23:41):

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

Simon Hudon (Apr 11 2018 at 23:41):

Because I'm a bad person

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.

Simon Hudon (Apr 11 2018 at 23:43):

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

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

Kevin Buzzard (Apr 12 2018 at 00:32):

Yes, I learnt that now, from example

Kevin Buzzard (Apr 12 2018 at 00:32):

I was just querying the logic

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

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

Mario Carneiro (Apr 12 2018 at 00:36):

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

Moses Schönfinkel (Apr 12 2018 at 08:15):

@Andrew Ashworth I 100% will.


Last updated: Dec 20 2023 at 11:08 UTC