Using (le/lt/ge/gt)_zero instead of (non)pos/neg

Stream: mathlib4

[David Ang]

Is it possible to enforce the naming convention of le_zero/lt_zero/ge_zero/gt_zero instead of pos/neg/nonpos/nonneg? The latter does not save much character space, but the former has the important advantage of not clashing with neg being negation (e.g. what should add_neg be?). I'm sure this has been discussed countless times, but I couldn't find a topic precisely about this.

[Edward van de Meent]

(possibly unpopular opinion: it should be add_neg_eq if it refers to x + -y = ..., which would disambiguate these uses)

[David Ang]

I think that's precisely my point - there is no need to have _eq if we don't allow ... -> x + y < 0 to be called add_neg in the first place.

[Edward van de Meent]

sure, but i think _eq does a good enough job that we don't need to change this.

[David Ang]

The other issue with x < 0 being neg is that there are two identical things being given different names, which I'd imagine is annoying in general.

[David Ang]

This is similar to x + 1 being add_one and succ amongst other things, but we do have Nat.succ x so that's understandable.

[Yury G. Kudryashov]

There were some discussions about that. AFAIR, they came to nothing.

[Yury G. Kudryashov]

(note: it should be zero_le_*, not *_ge_zero)

[Alex Meiburg]

Side note: docs#if_pos and docs#if_neg have always been a confusing name choice to me, in particular how they almost-clash with docs#ite_pos and docs#ite_neg. (Similar dif/dite versions.)

[David Ang]

I’d argue these should be if_true and if_false and zero_lt_ite and ite_lt_zero

[Kevin Buzzard]

The problem is that true means something else :-/ But I agree that the names feel more descriptive!

[Ruben Van de Velde]

if_of_true could work, if_true is currently correct

[Alex Meiburg]

I guess I would suggest if_cond and if_not_cond. There are docs#ite_cond_eq_false and docs#ite_cond_eq_true which kind of follow the pattern

[Aaron Liu]

I feel like this might clash with docs#cond

[Ruben Van de Velde]

OTOH, if_pos is short :)

[Kevin Buzzard]

And it's been there since at least 2017

[Alex Meiburg]

Was just reminded of this: spent some ten minutes trying to find a lemma only to find it was called docs#iSup_pos. The name is probably based on if_pos but I wouldn't have guessed it. :(
(I only found it by doing simp? [<the proof of h>] at the relevant goal)