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 meanZ->(Y->X)
andX_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 namedC_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