naming convention for ≤ and <

Stream: mathlib4

[Jovan Gerbscheid]

We want use the to_dual attribute to generate dual statements for lemmas about order. Some of the dual lemmas are very similar to the original, so we need a naming convention that can distinguish them. For these simple lemas, to_dual just replaces any a ≤ b with b ≤ a and a < b with b < a. When there is ambiguity, we can either use ge/ gt for the reversed relations, or use a '. Here are some examples:

le_trans : a ≤ b → b ≤ c → a ≤ c
ge_trans/le_trans' : b ≤ a → c ≤ b → c ≤ a

le_of_eq : a = b → a ≤ b
ge_of_eq/le_of_eq' : a = b → b ≤ a

le_or_lt/le_or_gt : a ≤ b ∨ b < a

ne_iff_lt_or_lt/ne_iff_lt_or_gt : a ≠ b ↔ a < b ∨ b < a
ne_iff_lt_or_lt'/ne_iff_gt_or_lt : a ≠ b ↔ b < a ∨ a < b

Ne.lt_of_le : a ≠ b → a ≤ b → a < b
Ne.lt_of_le'/Ne.gt_of_ge : b ≠ a → a ≤ b → a < b

I made a PR for this at #24376, but I would like some feedback on what names people prefer.

[Eric Wieser]

From that PR, I found this name particularly confusing:

theorem gt_or_eq_of_ge : a ≤ b → a < b ∨ b = a

[Edward van de Meent]

i think this shows that for these lemmas, the current naming scheme is too ambiguous to be able to deduce the full statement, unless we reconsider when/how we choose between ge/le. In particular, it seems like swapping all occurrences gives names which are hard to interpret, while simply adding a prime still leaves the question of what the original statement is...
In order to try to shine some clarity on how these lemmas should be named, i'd like to put forward an observation:

• We don't actually use ≥ and > in theorems, which is what allows us to use ge and le instead for≤ and <.
• When lemmas have ge or gt instead of le or lt respectively, it tends to indicate a contravariantness compared to the order in which the arguments to the concerning operator usually occurs in. (i.e. if the first time the arguments occur in that order are a,b, the term a ≤ b is referred to with le, whereas b ≤ a is referred to as ge)

I don't know if this is a good way to give stronger meaning to a choice between ge and le, but i would like to know if people think this "co/contravariantness" is a relevant notion to think about for this problem

[Jovan Gerbscheid]

Yes, the way I was doing it in the case that there is also an a = b is to say that that is 'the' order. and then pick between le/ge based on that.

[Edward van de Meent]

the reason for that choice being, there is no "contravariant" for equality?

[Jovan Gerbscheid]

The idea was that normally, we always write a = b in the alphabetical order (assuming a and b are bound in the same place). So normally, this determines the alphabetical order.

[Edward van de Meent]

:thinking:

[Jovan Gerbscheid]

Alright, let's not involve the order of =, and use the contravariantness as you described. Then the lemmas become

le_trans : a ≤ b → b ≤ c → a ≤ c
ge_trans/le_trans' : b ≤ a → c ≤ b → c ≤ a

le_of_eq : a = b → a ≤ b
le_of_eq' : a = b → b ≤ a

le_or_gt : a ≤ b ∨ b < a

ne_iff_lt_or_gt : a ≠ b ↔ a < b ∨ b < a
ne_iff_lt_or_gt' : a ≠ b ↔ b < a ∨ a < b

Ne.lt_of_le : a ≠ b → a ≤ b → a < b
Ne.lt_of_le' : b ≠ a → a ≤ b → a < b

lt_or_eq_of_le' : a ≤ b → a < b ∨ b = a

And then I propose that these become aliases of le_trans', lt_trans', le_antisymm':

ge_trans : b ≤ a → c ≤ b → c ≤ a
gt_trans : b < a → c < b → c < a
ge_antisymm : b ≤ a → a ≤ b → a = b

[Jovan Gerbscheid]

What do you think about LT.lt.not_le : a < b → ¬b ≤ a? should it be renamed to LT.lt.not_ge?

[Edward van de Meent]

i think that makes sense, actually

[Jovan Gerbscheid]

For ne_of_lt' (h : b < a) : a ≠ b, mathlib uses ne_of_gt. I'll also replace that.