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.

[Bryan Gin-ge Chen]

To keep this moving forward, would someone like to volunteer to make a companion PR to the naming guide?

[Jovan Gerbscheid]

I realize now I should probably separate out the part of the PR that renames lemmas, so that that is easier to review. Then that could go together with a change to the naming guide. Should the PR also change all occurrences of the names? I'd rather temporarily keep the old names so that the PR is manageable, with a TODO to deprecate the old names.

There are also a few lemmas in core e.g. in the Nat and Int namespace that should be renamed for the new convention.

[Bryan Gin-ge Chen]

Yes, if it isn't too much trouble, splitting it up into more easily-reviewable chunks would be greatly appreciated.

[Jovan Gerbscheid]

Here are the changes I'm proposing for this PR

• adding ge/gt:

lt_or_le -> lt_or_ge
le_or_lt -> le_or_gt
not_lt_of_lt -> not_lt_of_gt
not_le_of_lt -> not_le_of_gt
not_lt_of_le -> not_lt_of_ge
le_of_not_le -> le_of_not_ge
le_of_not_lt -> le_of_not_gt
lt_of_not_le -> lt_of_not_ge
lt_iff_not_le -> lt_iff_not_ge
lt_of_le_not_le -> lt_of_le_not_ge
lt_iff_le_not_le -> lt_iff_le_not_ge
eq_or_lt_of_not_lt -> eq_or_lt_of_not_gt
not_lt_iff_le_imp_le -> not_lt_iff_le_imp_ge
ge_imp_eq_iff_le_imp_le -> le_imp_eq_iff_le_imp_ge : (a ≤ b → a = b) ↔ (a ≤ b → b ≤ a)

Ne.lt_or_lt -> Ne.lt_or_gt
Ne.not_le_or_not_le -> Ne.not_le_or_not_ge

LT.lt.not_lt -> LT.lt.not_gt
LT.lt.not_le -> LT.lt.not_ge
LE.le.not_lt -> LE.le.not_gt
LE.le.lt_of_not_le -> LE.le.lt_of_not_ge

• removing ge/gt:

gt_of_gt_of_ge -> lt_of_lt_of_le'
gt_of_ge_of_gt -> lt_of_le_of_lt'
ne_of_gt -> ne_of_lt'
ge_of_eq -> le_of_eq'
eq_or_gt_of_le -> eq_or_lt_of_le'
gt_or_eq_of_le -> lt_or_eq_of_le'

Eq.ge -> Eq.le'
Eq.not_gt -> Eq.not_lt'

LE.le.eq_or_gt -> LE.le.eq_or_lt'
LE.le.gt_or_eq -> LE.le.lt_or_eq'
LE.le.eq_or_gt -> LE.le.eq_or_lt'
LE.le.gt_or_eq -> LE.le.lt_or_eq'

• removing:

gt_irrefl (same as lt_irrefl)

• Bound variable plays the role of first argument:

LE.le.lt_or_le -> LE.le.(forall_)gt_or_le (h : a ≤ b) (c : α) : a < c ∨ c ≤ b
LE.le.le_or_lt -> LE.le.(forall_)ge_or_lt
LE.le.le_or_le -> LE.le.(forall_)ge_or_le

le_of_forall_lt' -> le_of_forall_gt (H : ∀ c, a < c → b < c) : b ≤ a
forall_lt_iff_le' -> forall_gt_iff_le

[Jovan Gerbscheid]

For some of the ones that remove ge/gt, I think it's not so clear that they are a good change, since they introduce primed names.

[Jovan Gerbscheid]

#24775 implements the first block of renames in my message above. It replaces all occurences and adds deprecations. The replacements were done automatically, in the first commit, so that the remaining commits are easier to review separately. It would be nice if this could be reviewed quickly, since it will probably quickly gather merge conflicts.

[Bryan Gin-ge Chen]

Do you mind also creating a PR to the naming guide (with examples, etc.) that we can reference / merge simultaneously?

[Jovan Gerbscheid]

https://github.com/leanprover-community/leanprover-community.github.io/pull/626

Here's the PR to the naming guide. The correctness of the included examples depends on more changes than just this mathilb PR.

[Jovan Gerbscheid]

In the update to the naming convention, I recommend ne_of_gt over ne_of_lt' (contrary to my message above). Feel free to make suggestions about the details of the new naming convention.

[Bryan Gin-ge Chen]

@Eric Wieser @Yaël Dillies When you have some time could you take a look at https://github.com/leanprover-community/leanprover-community.github.io/pull/626 and see if the rules are OK?

[Jovan Gerbscheid]

I've made a new PR to the naming guide clarifying how to determine which order is considered normal, and which is considered swapped. This uses the convention suggested by @Bryan Gin-ge Chen in a comment

https://github.com/leanprover-community/leanprover-community.github.io/pull/629

[Bryan Gin-ge Chen]

An example is:

theorem not_ge_of_lt [Preorder α] {a b : α} (h : a < b) : ¬b ≤ a := sorry

Jovan had named this not_le_of_gt in #24775, but using lt for h : a < b felt more natural to me since it shows up first in the theorem statement (as opposed to using le for b ≤ a which shows up first in the name).

Pinging @Bhavik Mehta @Yaël Dillies again for comments.

[Aaron Liu]

btw we also have docs#LT.lt.not_le

[Bryan Gin-ge Chen]

Thanks! I added a comment to #24775 pointing those out.

[Jovan Gerbscheid]

All right, I've ported #24775 to the updated naming convention, so it is ready for review again

[Jovan Gerbscheid]

Thanks for merging it. Part 2 is now at #25560

[Jovan Gerbscheid]

Here's part 3: #25566

[Jovan Gerbscheid]

I've also made #25567 to deprecate gt_irrefl.
And I've made #25568 to reorder some lemmas in Mathlib.Order.Basic, so that they are in the correct section.

[Jovan Gerbscheid]

LE.le.ge, GE.ge.le, LT.lt.gt and GT.gt.lt don't follow the new naming convention, and don't seem very useful. Should we deprecate them?

[Jovan Gerbscheid]

The same could be said about gt_iff_lt and ge_iff_le, but they are actually used sometimes. And those are defined in core.

[Ruben Van de Velde]

Keep them please

[Jovan Gerbscheid]

What do people think about adding the following line of code to Mathlib.Init:

/-- Declare `∃ x > y, ...` as syntax for `∃ x, y < x ∧ ...` -/
binder_predicate (priority := high) x " > " y:term => `($y < $x)

And modifying the pretty printer accordingly?

Then we can continue to use the nice ∃ x > y and ∀ x > y notation, without the headache of having to rewrite with gt_iff_lt every time.

[Yaël Dillies]

Yes, in fact I don't understand why Core doesn't do this already

[Edward van de Meent]

if core did this, i imagine it would rather turn it into `($x > $y)

[Edward van de Meent]

simply for the sake of consistency

[Jovan Gerbscheid]

That's what core is currently doing. Hence the need for (priority := high).

[Edward van de Meent]

ah, i misunderstood the issue

[Jovan Gerbscheid]

Here's part 4: #25572

This one fixes the transitivity lemmas. In particular, it deprecates gt_of_gt_of_ge and gt_of_ge_of_gt

[Ruben Van de Velde]

I tried to add that to core (or batteries?) but got refused

[Jovan Gerbscheid]

Yeah, I can imagine core wouldn't be too keen on this because it might be confusing. But it fits with the mathlib convention of mostly using ≤ and <. I'm making an attempt to do this in mathlib here #25573.

[Jovan Gerbscheid]

Do we agree with renames like these?

LE.le.le_iff_eq -> LE.le.ge_iff_eq' (h : a ≤ b) : b ≤ a ↔ b = a
LE.le.eq_of_not_gt -> LE.le.eq_of_not_lt' (hab : a ≤ b) (hba : ¬a < b) : b = a

Although this does follow the new naming rules, it means we end up with more primed names, which is not ideal.

[Jovan Gerbscheid]

All right, I haven't heard anyone complain, so here's part 5: #25586
Among other things, it does the above renames

[Jovan Gerbscheid]

I think this concludes all of the renaming of lemmas about ≤ and <. We haven't talked about EventuallyLE, but I presume we want it to follow the same naming, hence I've made #26969 which renames # EventuallyLE.le_iff_eq to EventuallyLE.ge_iff_eq'

[Jovan Gerbscheid]

I spotted one more wrongly named lemma: #27269

[Violeta Hernández]

Does docs#StrictAnti.lt_iff_lt count as badly named?

[Jovan Gerbscheid]

I made a PR for it #28314

[Violeta Hernández]

Oh, thanks! I got a bit distracted.

[Artie Khovanov]

(deleted)

[Artie Khovanov]

I've taken over the PR changing the bounded quantification delaborator at #32985 (edited)
I'd push for a consensus about whether to go ahead to prevent the PR rotting

[Violeta Hernández]

Thank you for this! I've seen this as a problem for the longest time.

[Artie Khovanov]

Looks like it's not happening :frowning:
From my understanding the maintainers want the change to be made in core by replacing GE with notation, if any change is made at all.

[Artie Khovanov]

If there is continued appetite for this change, please feel free to make an RFC to Lean (I don't have the capacity to and I don't care strongly enough).

[Violeta Hernández]

Getting rid of > altogether seems really drastic. But I support the iniciative.
Can't take it myself since the last times I've tried PRing to core it has not gone very well.

[Jovan Gerbscheid]

I don't think core lean should get rid of >, because it is a normal thing in real world mathematics. I also don't think that the change to the forall and exists binder predicates will be accepted in core, because it is confusing.

I can only imagine that core would improve the ability to use < and > interchangeably.

[Ruben Van de Velde]

We should have a > b, but I haven't seen the argument yet why it can't be notation for LT.lt b a

[Ruben Van de Velde]

Oh, maybe there's one that it messes with calc like \in does

[Artie Khovanov]

Violeta Hernández said:

Getting rid of > altogether seems really drastic. But I support the iniciative.
Can't take it myself since the last times I've tried PRing to core it has not gone very well.

It would be notation, not removed