Naming convention for binary theorems with left and right about mathlib HOT 13 CLOSED

I don't think that insert_subset and subset_insert are very good examples of positional naming. These names would not change regardless of the status of this PR. The examples I have in mind are typically binary operations applied to a special argument. The canonical examples are things like add_zero and zero_add, where the order of words indicates whether zero is to the left or right of the add.

This type of naming seems reasonable enough that I don't see a reason to change it, but in mathlib this type of naming is also used occasionally on binary operations that do not have a notation, meaning that the operator appears to the left of both arguments and the positionality is less obvious. For example:

theorem nil_product (l : list β) : product (@nil α) l = []
theorem product_nil (l : list α) : product l (@nil β) = []

The current convention is to order the words as if product was an infix operator. Here I can see a reason to change the convention so that these two become product_nil_left and product_nil_right, but a downside of this is that the name of the theorem becomes dependent on whether a notation is currently in use for the operator, while the "infix only" convention makes this choice irrelevant for naming.

I am okay with changing _left and _right suffixes to _l and _r or ₗ and ᵣ, since they are indeed very common, but I would run this by others first.

from mathlib.

@digama0 I'm not sure I understand how you are distinguishing finset.insert_subset and list.nil_product. To me, they are both examples of a positional naming scheme – since they both have binary name (subset, product) and a key argument (insert a s, nil) – which makes them both fall under the consideration of this issue.

Perhaps you're suggesting that, because subset does not take the same type of argument on each side, it does not suffer from the difficulty of determining the meaning of the name (or type of the theorem). But I don't see that.

I intentionally didn't make a point about notation because I don't think it should matter whether an infix operator is used or not. Conceptually, it seems to me that all that matters is whether the name being used is binary (i.e. has two explicit parameters and ignoring implicit parameters) or not.

from mathlib.

I am okay with changing _left and _right suffixes to _l and _r or ₗ and ᵣ, since they are indeed very common, but I would run this by others first.

Great!

Subscript would be fine with me, assuming there are non-ASCII subscript letters commonly supported in fonts. Unfortunately, it appears that ₗ (LATIN SUBSCRIPT SMALL LETTER L, U+2097) shows up for me as unsupported by every font in the macOS symbol viewer.

from mathlib.

I think that if you object to insert_subset on these grounds, though, you are calling into question the whole read-it-sequentially naming scheme that is used everywhere in lean. To take an obnoxiously long example:

lemma abs_sub_abs_le_abs_sub (a b : α) : abs a - abs b ≤ abs (a - b)

Here le is acting as a binary operator, and it is read between its arguments. This has things like subset_insert as special cases when there are only two operators (for insert_subset this is also combined with a rule for reading only the LHS of a biconditional or equality when the RHS is unambiguous).

from mathlib.

I'm not sure how my argument goes that far because insert_subset does not say anything about the other argument, unlike abs_sub_abs_le_abs_sub.

from mathlib.

Re: unicode, I think the usual response is "get a better font" if you can't see the characters. I certainly had to pick my lean font carefully to get good unicode coverage, but I don't know any previous example of a character being rejected for use because it wasn't well supported in most fonts.

from mathlib.

The lean naming convention does not read variables at all. Sometimes self is used to indicate that a variable is repeated, but it's generally ambiguous about variable placement.

from mathlib.

I think you can safely narrow the issue introduced here as pertaining to binary names referencing only one argument.

from mathlib.

I see. I think I would keep it as is for consistency, but I solicit other opinions on this issue.

from mathlib.

I think, at the very least, it should be documented (probably in docs/naming.md) what the current policy is, even if the resolution of this issue is to “keep it as is.” This documentation would provide a useful reference for PRs.

from mathlib.

I believe the relevant passage in naming.md is the following:

When an operation is written as infix, the theorem names follow suit. For example, we write neg_mul_neg rather than mul_neg_neg to describe the pattern -a * -b.

But feel free to PR a change to the wording if you think you can make it clearer.

from mathlib.

I see. Thanks, that was not obvious to me.

from mathlib.

I'm closing this issue now.

from mathlib.