Spelling `congrArg` or `congr_arg`

Stream: mathlib4

[Martin Dvořák]

Which spelling is preferred in Mathlib?
I find congr_arg more often, but congrArg is what exact? gives me.

[Eric Rodriguez]

:shrug: I think the new preferred style is Kyle's congr(...)

[Martin Dvořák]

Can I see an example?

[Mario Carneiro]

it's a theorem, so congr_arg

[Kyle Miller]

@Martin Dvořák If h : x = y you can write congr(f $h) to get f x = f y

[Eric Wieser]

Mario Carneiro said:

it's a theorem, so congr_arg

Can we just remove the other spelling?

[Martin Dvořák]

Do we have power to rename the declaration in Init.Prelude please?

[Mario Carneiro]

it's in core

[Martin Dvořák]

Kyle Miller said:

Martin Dvořák If h : x = y you can write congr(f $h) to get f x = f y

Is there a motivation for this particular syntax?

[Mario Carneiro]

there is a PR which does this which has been sitting for 6+ months

[Martin Dvořák]

In the meanwhile, can I PR a replacement of all congrArg in Mathlib?

[Mario Carneiro]

actually almost a year lean4#1897

[Mario Carneiro]

can you mark a theorem in another file as deprecated?

[Mario Carneiro]

invalid attribute 'deprecated', declaration is in an imported module :sad:

[Martin Dvořák]

I don't know what you mean.
I would just replace all these
https://github.com/search?q=repo%3Aleanprover-community%2Fmathlib4+congrArg&type=code
by congr_arg as we prefer.

[Mario Carneiro]

there is a really nifty mechanism I added to core std to make it easy to find and replace deprecated things

[Mario Carneiro]

import Std

def foo := 1
@[deprecated] alias bar := foo

example : bar = 1 := rfl
       -- ^^ code action here

[Mario Carneiro]

unfortunately it only works when the alias is the one being deprecated, not the target

[Eric Wieser]

Mario Carneiro said:

there is a PR which does this which has been sitting for 6+ months

I think this PR suffers from making too many renames at once

[Mario Carneiro]

you're not wrong, it was discussed in the dev meeting and all but one or two categories was accepted

[Mario Carneiro]

unfortunately I forget most of the results of the meeting. I think Membership.Mem was rejected and either IsLawfulFunctor or OptParam was contentious

[Eric Wieser]

Presumably a Pr to rename just congrArg would be fine?

[Martin Dvořák]

And congrFun at the same time.

[Eric Wieser]

It seems the highest-value renames are the ones where mathlib has decided it has to make an alias because of a "bad" name in core

[Martin Dvořák]

FYI, there are quite a few aliases in Mathlib.Init.Logic including these:

alias proofIrrel ← proof_irrel
alias congrFun ← congr_fun
alias congrArg ← congr_arg

[Mario Carneiro]

do we have aliases for T.constr.inj_eq?

[Eric Wieser]

Ok, so maybe the low hanging fruit is:

• A PR that makes all 14 replacements in Mathlib.Init.Logic
• Another PR that changes all the generated names

[Mario Carneiro]

I think that's the only generated name in my list

[Eric Wieser]

On the first point; why is docs#eq_rec_heq preferred to docs#eqRec_heq ?

[Mario Carneiro]

is that an alias?

[Eric Wieser]

Yes

[Mario Carneiro]

it was written very early on in mathlib4 history, before we had decided what to do about namespaced names and mostly only had the guidance "theorems are snake cased"

[Eric Wieser]

I think this is a gap in #naming where we don't say whether to tokenize Foo.barBaz as foo_barBaz_eq or fooBarBaz_eq

[Mario Carneiro]

I think we now have a decent amount of precedent in the form of natCast_add et al that they should be treated as one name including namespaces (when needed for disambiguation)

[Eric Wieser]

I don't think this thread ever reached a consensus

[Martin Dvořák]

Kyle Miller said:

Martin Dvořák If h : x = y you can write congr(f $h) to get f x = f y

Is this syntax useful for Mathlib?

[Mario Carneiro]

I guess we proceeded in spite of a poll that is mildly negative to this conclusion

[Eric Wieser]

Mario Carneiro said:

I think we now have a decent amount of precedent in the form of natCast_add et al that they should be treated as one name including namespaces (when needed for disambiguation)

We also have quite a lot of things of the form docs#map_multiset_sum, so I'd argue there's no established convention

[Mario Carneiro]

in that case it seems fine to just have the alias

[Eric Wieser]

(besides establishing a lack of convention)

[Eric Wieser]

I've revived the old thread to discuss this further. I suggest we don't rename eqRec_heq in core for now, and only make the other 13 renames.

[Mario Carneiro]

what are the 13?

[Kyle Miller]

@Martin Dvořák Have you read the documentation for the syntax? You can take a look at docs#Mathlib.Tactic.TermCongr.termCongr and see more examples all in one place in the test/TermCongr.lean file.

[Eric Wieser]

Mario Carneiro said:

what are the 13?

Sorry, 12:

alias proof_irrel := proofIrrel
alias congr_fun := congrFun
alias congr_arg := congrArg

alias Or.decidable := instDecidableOr
alias And.decidable := instDecidableAnd
alias Not.decidable := instDecidableNot
alias Iff.decidable := instDecidableIff
alias decidableTrue := instDecidableTrue
alias decidableFalse := instDecidableFalse

alias by_cases := byCases
alias by_contradiction := byContradiction
alias not_not_iff := not_not

[Eric Wieser]

I guess the decidable aliases are bad too, so really only 4 should be moved to core:

alias proof_irrel := proofIrrel
alias congr_fun := congrFun
alias congr_arg := congrArg

alias Decidable.by_contradiction := Decidable.byContradiction

[Mario Carneiro]

yeah they don't look very important, although I don't think you will get much pushback

[Mario Carneiro]

in fact they look like what you will get if you just delete the name

[Mario Carneiro]

oh wait I'm reading them backward

[Yaël Dillies]

I would have expected something like

alias Or.instDecidable := instDecidableOr
alias And.instDecidable := instDecidableAnd
alias Not.instDecidable  := instDecidableNot
alias Iff.instDecidable  := instDecidableIff
alias decidableTrue := instDecidableTrue
alias decidableFalse := instDecidableFalse

[Mario Carneiro]

those decidable aliases look like a good opportunity to test out @[deprecated] alias :smiley:

[Eric Wieser]

I think it's probably best not to make any PRs renaming instances in core; that's best left to the proposal to change the naming heuristics

[Mario Carneiro]

(the point of my comment was to replace uses of the alias in mathlib)

[Mario Carneiro]

I think we should always try to keep the naming convention for instances close to the autogenerated name because people will have to deal with both anyway

[Kevin Buzzard]

Don't we also have infer_instance and inferInstance?

[Scott Morrison]

That one is tactic vs term.

[Mario Carneiro]

unfortunately that's per the naming convention

[Mario Carneiro]

although actually both are bad

[Mario Carneiro]

the lean 3 apply_instance would call typeclass inference to fill your term, the lean 4 infer_instance is just exact inferInstance which infers the goal as an argument of the inferInstance no-op function

[Mario Carneiro]

which means the term ends up with some extra garbage

[Mario Carneiro]

by the way my list had byCases in the same category as byContradiction

[Eric Wieser]

docs#Decidable.byCases is special because it's sort-valued

[Eric Wieser]

So having both versions of the name seems to fit the naming conventions

[Yuyang Zhao]

Do we need to rename docs#Quotient.inductionOn (and ₂ ₃ ' versions)?

[Eric Wieser]

Yes, I think so; though I think if we want any hope of these being merged they should be separate PRs