Naming conventions for simprocs

Stream: mathlib4

[Eric Wieser]

How should simprocs be named? For a simproc which matches foo (bar _), should it be named:

1. reduceFooBar, to match builtin simprocs, and the fact that this generates a def?
2. foo_bar, so that the end use of simp can think of it as just another lemma, and so that we can use the more flexible lemma-naming rules?
3. Something else?

[Eric Wieser]

(cc @Vasilii Nesterov for https://github.com/leanprover-community/mathlib4/pull/22273#discussion_r1970074129)

[Yaël Dillies]

I am in favor of using lemma-naming rules, because simprocs are designed to be used like lemmas. This is what I do in #22039

[Eric Wieser]

Yes, this is my opinion too, but:

[Eric Wieser]

@loogle |- Lean.Meta.Simp.Simproc

[loogle]

:search: Lean.Meta.Simp.Methods.post, Lean.Meta.Simp.Methods.pre, and 83 more

[Eric Wieser]

suggests that it is not what has been done so far

[Yaël Dillies]

None of these are mathlib's, though.

[Ruben Van de Velde]

Well okay, but do we not want to align the naming convention as far as possible?

[Matthew Ballard]

I think divergence here is confusing though core has some internal divergence already in bv_decide land which may have some rules in place already?

[Henrik Böving]

The simprocs in bv_decide have names inspired by their respective friends in Bitwuzla so they shouldn't be taken as a naming convention.

[Eric Wieser]

So concretely, for simprocs that match

• Finset.Icc (ofNat _) (ofNat _)
• ∃ x, _ ∧ x = y ∧ _
• (of _ : Matrix (Fin _) (Fin _) _) * (of _ : Matrix (Fin _) (Fin _) _)

which of the following styles should we choose as names?

[Vasilii Nesterov]

My opinion is that it should be reduceFooBar following the conventions about simprocs from core and the general convention about naming defs. They are used like lemmas, but still different from them, and I think it's nice to be able to visually distinguish used lemmas and simprocs after simp?.

[Eric Wieser]

/poll For the above three examples, which style of name should we use?

• Finset.reduceIccOfNatOfNat, reduceExistsAndEq, Matrix.reduceOfMulOf
• Finset.icc_ofNat_ofNat, exists_and_eq, Matrix.of_mul_of

[Eric Wieser]

(edit: icc should obviously be Icc, please excuse the typo)

Vasilii Nesterov said:

and I think it's nice to be able to visually distinguish used lemmas from simprocs after simp?.

I agree, but I think it's also nice to have the extra naming expressivity that _ gives you; OfNatOfNat has fewer separators available than ofNat_ofNat.

[Eric Wieser]

Visual markers could still be achieved by prefixing with reduce_ or s!_ or some other unusual token

[Damiano Testa]

Eric Wieser said:

Visual markers could still be achieved by prefixing with reduce_ or s!_ or some other unusual token

I do like reduce_<def_convention>: could that be an option?

[Eric Wieser]

Unlike other recent polls, this one does let you add more options :)

[Eric Wieser]

reduce.<def_convention> and reduce!<def_convention> are similar options

[Damiano Testa]

I added an option, but would be happy with any of the remaining ones that you suggested that have reduce<something>def_convention.

[Vasilii Nesterov]

Eric Wieser said:

I agree, but I think it's also nice to have the extra naming expressivity that _ gives you; OfNatOfNat has fewer separators available than ofNat_ofNat.

My point here is that simprocs are actually defs, and naming them as theorems may be confusing.

[Eric Wieser]

But they are never actually used as defs by the end user, in the same way that the end user never cares what the name of the def is that implements the norm_num tactic or the + elaborator.

[Kim Morrison]

Could someone post an RFC proposing to rename the simprocs implemented in Lean? I think it would be plausible to just change these, and I agree it would be less confusing.

[Eric Wieser]

@Kim Morrison , are you suggesting renaming all the simprocs in response to how the poll concludes above, or just that the bv ones are misnamed and the reduceIte convention is already the FRO-approved naming?

[Eric Wieser]

Since this poll has few participants, should we say "authors choice" for now to get the simprocs merged, and clean up the naming later?

[Kim Morrison]

Sorry, I hadn't seen the poll, I had assumed that the snake case option would win: i.e. I was proposing an RFC to rename the Lean simprocs. But I'm also very happy to just punt on this one, it doesn't seem very high priority.

[Bhavik Mehta]

There was some previous discussion on this here: https://github.com/leanprover/lean4/pull/5167#issuecomment-2309512097