Shorten positivity

Stream: mathlib4

[Yaël Dillies]

The very long name of the positivity tactic is starting to grow old on me. It's many characters that I type very often, and it feels a lot like writing simplification instead of simp. Would it be possible to shorten it, maybe to pos? I realise this increases the likelihood of ambiguity, but in several years no tactic has tried to claim any other name starting with pos.

[Jireh Loreaux]

Personally, I would like this.

[Damiano Testa]

I am not sure exactly whether you are suggesting to replace positivity with pos, or adding a synonym. I would probably slightly prefer to have a synonym just for the tactic, but preserve the long name as well as the attribute.

[Yaël Dillies]

I am in principle not opposed to keeping both names around, but does another tactic enjoy such a "nickname"? I can't think of any

[Frédéric Dupuis]

rewrite actually exists :-)

[Yaël Dillies]

rw is not a nickname of rewrite (surprisingly!), instead it's rewrite + try rfl

[Damiano Testa]

I think that my inclination is that, as time passes, I am happier with using actual words, as opposed to abbreviations in code.

[Yaël Dillies]

positive is a word too :slight_smile:

[Damiano Testa]

True, I prefer positive over pos, but maybe it is not gaining much, given the intended goal?

[Damiano Testa]

I do find positive definitely easier to type than positivity, more so than just the gain in 2 letters.

[Damiano Testa]

So, would renaming positivity to positive feel like a good change?

[Damiano Testa]

And should then "all" of positivity be renamed, including the attribute?

[Damiano Testa]

I would be happy with this change, but if you think that this is still long, switching all the way to pos is still on the table!

[Damiano Testa]

(I don't use positivity much, so I am arguing mostly on personal grounds, rather than actual experience with the practical use.)

[Yaël Dillies]

Damiano Testa said:

So, would renaming positivity to positive feel like a good change?

It feels like a good change, but I would rather go all the way to pos unless someone comes up with a strong counter-point

[Ruben Van de Velde]

I think add the pos synonym first and then give it a while to see if we're happy with it

[Yaël Dillies]

Sounds like a plan :+1:

[Jireh Loreaux]

@Damiano Testa my reason for a short version is that it's ubiquitous (just like rw and simp). For example, writing rw [sq_le_sq₀ (by positivity) (by positivity)] (which I've done on a number of occasions) is painful, and it would be much more pleasant to write rw [sq_le_sq₀ (by pos) (by pos)].

[Damiano Testa]

Another argument in favour is that pos is also the naming convention for 0 < x.

[Yaël Dillies]

Jireh Loreaux said:

writing rw [sq_le_sq₀ (by positivity) (by positivity)] is painful

Arguably, we should be using auto-params here

[Jireh Loreaux]

There is a downside to auto-params. You then need to make the arguments (for the elements) to sq_le_sq₀ explicit, and you frequently have to type rw [sq_le_sq₀ ..] even once you do that. At least, this is what we have to do in auto-params for theorems about docs#cfc.

[Alex Meiburg]

I've often thought it would be nice to have a shorthand for by positivity, for the reason Jireh says, that I often want it as almost a "discharger" in some terms. As a tactic on its own in a larger block, I don't mind the name positivity at all; it's only when by positivity is the whole term that it feels long.

What if pos was a term that elaborated as by positivity, but positivity stayed the name for the tactic? Too crazy? :)

[Jovan Gerbscheid]

For some reason such fancy term elaborators always have a % sign. So should it be pos%?

[Aaron Liu]

Yes pos% sounds good

[Kim Morrison]

I'm opposed to shortening it to pos, that seems unnecessary burden on the reader. positive is an improvement over positivity, however.

[Eric Wieser]

Gramatically by positive is a bit weirder, but maybe by positivity was an outlier in not being weird originally

[Ben Eltschig]

by continuity was another example, but of course now that's replaced by fun_prop

[Edward van de Meent]

there's also by finiteness, by monicity, by measurability and a few tactics like by nontriviality which generate hypotheses instead of closing a goal

[Eric Wieser]

The pos% suggestion nicely solves the grammar issue by skipping by

[Eric Wieser]

But maybe having term shorthands for each by tac is bad for learning

[Jireh Loreaux]

Damiano Testa said:

I think that my inclination is that, as time passes, I am happier with using actual words, as opposed to abbreviations in code

In general, I agree with this, but for things which are ubiquitous (read: must be typed many times), I prefer much shorter spellings (pos is 70% shorter than positivity) if there is little to no loss in meaning.

[Jireh Loreaux]

This is also related to:
Kim Morrison said:

I'm opposed to shortening it to pos, that seems unnecessary burden on the reader. positive is an improvement over positivity, however.

I don't buy this argument at all. Anyone reading proofs without the benefit of an interactive environment is either an expert, or asking for pain anyway. And if you have an interactive environment, you can just hover to learn "the positivity tactic, pos, is used to close goals of the form 0 < _ which are structurally positive ..." (or whatever the docstring says / will say).

[Jireh Loreaux]

On the note of ubiquity compared to other noun-named tactics,rg --stats ⟨tactic⟩ Mathlib returns:

• positivity: 1569 (few false positives in docstrings because "positive" is more common, some related to meta code, but not that many)
• measurability: 622 (the vast majority, probably north of 80% although there are also many in documentaion, are things being tagged @[measurability])
• finiteness: 340 mostly true positives, although a decent number of docstring hits.
• monicity: 17
• nontriviality: 413

So, positivity makes up a good deal more than all the others of these combined.

[Kim Morrison]

Anyone reading proofs without the benefit of an interactive environment is either an expert, or asking for pain anyway.

But this argument makes no distinction about how much you have to rely on the hovers and infoview. Of course you will have to sometimes, but every time you do it increases the pain level.

[Kim Morrison]

I'm still hoping we will get grind to cover everything positivity does, and it is shorter. :-)

[Alex Meiburg]

Ah, with the 🦾% term for by grind... :)

[Kim Morrison]

∎

[Yaël Dillies]

Alex Meiburg said:

Ah, with the 🦾% term for by grind... :)

⚙️%

[Michael Rothgang]

With adding gears as alias for grind? Works for me :-)