X_of_Y_of_Z naming

Stream: general

[Kevin Buzzard]

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]

Y -> Z -> X

[Chris Hughes]

as in lt_of_le_of_lt

[Kevin Buzzard]

Right, that's why I asked.

[Kevin Buzzard]

I just don't understand how the brackets work

[Kevin Buzzard]

If "of" means "follows from"

[Andrew Ashworth]

is of right associative

[Andrew Ashworth]

since it represents ->

[Kevin Buzzard]

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

[Kevin Buzzard]

which is (X_of_Z)_of_Y

[Andrew Ashworth]

it is also a mystery to me, hah

[Simon Hudon]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

Sorry

[Andrew Ashworth]

somewhere, a logician is crying

[Kevin Buzzard]

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

[Simon Hudon]

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]

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

[Simon Hudon]

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

[Andrew Ashworth]

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

[Andrew Ashworth]

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

[Andrew Ashworth]

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

[Andrew Ashworth]

oh

[Andrew Ashworth]

i have seen imp used in theorem names

[Simon Hudon]

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]

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

[Simon Hudon]

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]

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

[Andrew Ashworth]

otherwise my brain may explode

[Simon Hudon]

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]

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]

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

[Andrew Ashworth]

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

[Andrew Ashworth]

http://goshdarnfunctionpointers.com

[Simon Hudon]

Now I remember that fun :)

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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]

oh they are very anal about names here :-)

[Kevin Buzzard]

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

[Simon Hudon]

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]

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]

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]

right, as in lt_of_lt_and_le

[Simon Hudon]

Yeah, exactly

[Kevin Buzzard]

but not as in lt_is_implied_by_lt_which_is_implied_by_le

[Kevin Buzzard]

i.e. not as in lt_of_lt_of_le

[Kevin Buzzard]

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

[Kevin Buzzard]

and also not as in "(lt_is_implied_by_lt)_is_implied_by_le"

[Kevin Buzzard]

but actually exactly as in "(lt_is_implied_by_le)_is_implied_by_lt"

[Kevin Buzzard]

i.e. exactly "(lt_of_le)_of_lt"

[Simon Hudon]

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]

Aah

[Kevin Buzzard]

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

[Simon Hudon]

Yes. As you said

[Simon Hudon]

Because it's equivalent to lt_of_lt_and_le, the assumptions commute

[Simon Hudon]

They are logically equivalent

[Kevin Buzzard]

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

[Simon Hudon]

Nooooooo, no, no, no! :stuck_out_tongue_closed_eyes:

[Kevin Buzzard]

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

[Simon Hudon]

Because I'm a bad person

[Simon Hudon]

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]

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

[Mario Carneiro]

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]

Yes, I learnt that now, from example

[Kevin Buzzard]

I was just querying the logic

[Mario Carneiro]

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]

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]

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

[Moses Schönfinkel]

@Andrew Ashworth I 100% will.