Naming convention: succ vs. add_one

Stream: mathlib4

[Michael Stoll]

Should it be

lemma Int.two_dvd_mul_add_one (k : ℤ) : 2 ∣ k * (k + 1) := ...

or

lemma Int.two_dvd_mul_succ_self (k : ℤ) : 2 ∣ k * (k + 1) := ...

? Compare the existing

lemma Int.even_mul_succ_self (n : ℤ) : Even (n * (n + 1)) := ...

If we prefer the add_one version, should all the declarations having succ in the name, but _ + 1 in the type be renamed? :innocent:

[Robin Arnez]

I think add_one is preferred unless you are talking about docs#Nat.succ but we aren't too strict on that

[Robin Arnez]

Compare
@loogle "succ", _ + 1

[loogle]

:search: Nat.succ_eq_add_one, Nat.instNeZeroSucc, and 1568 more

[Robin Arnez]

and
@loogle "add_one", _ + 1

[loogle]

:search: Nat.add_one_ne, Nat.add_one_ne_self, and 512 more

[Bhavik Mehta]

In my opinion, we shouldn't need to talk about docs#Nat.succ outside of the most basic theory of natural numbers (which is in core). And so, we should use add_one everywhere, since Nat.succ shouldn't be appearing at all

[Michael Stoll]

Should we add that to the technical debt counters? :slight_smile:

[Michael Stoll]

@loogle Nat.succ

[loogle]

:search: Nat.succ, Nat.le_succ, and 1514 more

[Robin Arnez]

Is there some way to loogle x and not b?

[Michael Stoll]

Is there some way to tell loogle to only look in Mathlib proper?

[Bhavik Mehta]

(cc @Joachim Breitner, since we brainstormed a few ways to do the above)

[Michael Rothgang]

Michael Stoll said:

Should we add that to the technical debt counters? :slight_smile:

If you find a programmatic way to count these (e.g. grep something something), that's easy to add!

[Damiano Testa]

We could probably write an easy regex that would catch most declaration names that contain succ.

[Joachim Breitner]

Robin Arnez schrieb:

Is there some way to loogle x and not b?

Not yet (https://github.com/nomeata/loogle/issues/6)

[Michael Stoll]

Michael Rothgang said:

If you find a programmatic way to count these (e.g. grep something something), that's easy to add!

This doesn't seem to be that easy -- the type of the declaration can extend over several lines, and we should check whether it contains succ.

[Damiano Testa]

Not the type signature, the declaration id.

[Damiano Testa]

If the id contains succ, it either means that the signature contains succ and should be changed, or the signature already does not contain succ and the name should still be changed! :slight_smile:

[Michael Stoll]

But you certainly want to avoid false positives? Like docs#Order.succ_mono etc.

[Damiano Testa]

Ah, sorry, I was confused by Michael quoting Michael... :man_facepalming:

[Damiano Testa]

Michael Stoll said:

But you certainly want to avoid false positives? Like docs#Order.succ_mono etc.

Well, what I am thinking is that there are probably not that many false positives...

[Michael Stoll]

@loogle Order.succ, "succ"

[loogle]

:search: Order.succ, Order.succ_mono, and 450 more

[Damiano Testa]

Otherwise, it would have to be a metaprogram: since this is meant to run on master, where the oleans are available, it is probably pretty quick to run.

[Damiano Testa]

Ok, so about 1/3 are from Order succ.

[Michael Stoll]

@loogle "succ"

[loogle]

:search: Nat.succ, Nat.le_succ, and 2976 more

[Michael Stoll]

No idea where they all come from...

[Damiano Testa]

In any case, I agree that doing it "correctly" is the way to go: as more get corrected, the proportion will get more and more skewed to being wrong.

[Jovan Gerbscheid]

The linter could flag all constants that have "succ" in the name, but don't have "succ" in any constant name in the type.

[Damiano Testa]

It does not even have to be a linter: a simple metaprogram would suffice.

[Robin Arnez]

Some of the results come from
@loogle Int.negSucc
but I'm not sure where all of them come from

[loogle]

:search: Int.negSucc, Int.negSucc.injEq, and 172 more

[Robin Arnez]

import Lean
import Mathlib

open Lean

run_meta
  let mut names := #[]
  for (n, i) in (← getEnv).constants.map₁ do
    let .thmInfo thm := i | continue
    let .str _ str := n | continue
    if str.containsSubstr "succ".toSubstring then
      let res := thm.type.find?
        (fun e => e.isConst && (e.constName!.toString.containsSubstr "succ" || e.constName!.toString.containsSubstr "Succ"))
      if res.isNone then
        let some modIdx := (← getEnv).getModuleIdxFor? n | throwError "internal error"
        if (`Mathlib).isPrefixOf (← getEnv).header.moduleNames[modIdx]! then
          names := names.push n
  names := names.qsort (fun a b => a.toString < b.toString)
  Lean.logInfo (String.intercalate "\n" (names.map (·.toString)).toList)
  Lean.logInfo m!"{names.size} total results"

Is probably more accurate (gives 617 results currently)

[Jovan Gerbscheid]

There are so many! Are we really sure we want to change so many theorem names?

[Jovan Gerbscheid]

Bhavik Mehta said:

In my opinion, we shouldn't need to talk about docs#Nat.succ outside of the most basic theory of natural numbers (which is in core). And so, we should use add_one everywhere, since Nat.succ shouldn't be appearing at all

I would like to turn that logic around: we shouldn't need to talk about docs#Nat.succ outside of the most basic theory of natural numbers (which is in core). And so, we are free to unambiguously use succ to mean add_one. This is the same logic that let us use ge and gt to talk about ≤ and <.

[Bhavik Mehta]

I disagree, since succ could (and in my view, exclusively should) refer to docs#Order.succ

[Jovan Gerbscheid]

That's fair, but in the majority of lemmas that currently use succ to refer to add_one, I don't think there is any ambiguity with Order.succ at all.

[Jovan Gerbscheid]

I adapted the script by @Robin Arnez to search for lemmas with an "add_one" that refers to a natural number "add_one" in the type.

import Lean
import Mathlib

open Lean

def isNatOne (e : Expr) : Bool := Id.run <| do
  let_expr HAdd.hAdd N _ _ _ _ one := e | false
  unless N matches .const ``Nat _ do return false
  let_expr OfNat.ofNat _ one _ := one | false
  one matches .lit (.natVal 1)

run_meta
  let mut names := #[]
  for (n, i) in (← getEnv).constants.map₁ do
    let .thmInfo thm := i | continue
    let .str _ str := n | continue
    if str.containsSubstr "add_one".toSubstring then
      let res := thm.type.find? isNatOne
      if res.isSome then
        let some modIdx := (← getEnv).getModuleIdxFor? n | throwError "internal error"
        if (`Mathlib).isPrefixOf (← getEnv).header.moduleNames[modIdx]! then
          names := names.push n
  names := names.qsort (fun a b => a.toString < b.toString)
  Lean.logInfo (String.intercalate "\n" (names.map (·.toString)).toList)
  Lean.logInfo m!"{names.size} total results"

It gives 120 with add_one, versus 704 results with succ in the name.

[Jovan Gerbscheid]

I do not propose that we change any of the add_one lemmas to use succ, but I think this is reasonable evidence that the succ naming convention is significantly more popular than add_one.

[Damiano Testa]

My impression is that succ is "more popular" for historical reasons. For instance, up until recently, induction n would show a goal involving Nat.succ. I was certainly happy to see this change.

[Damiano Testa]

Btw, replacing the two logInfos with

logInfo (.joinSep (m!"{names.size} total results"::""::(names.map .ofConstName).toList) m!"\n")

you get hover information on the outputs.

[Jovan Gerbscheid]

I even found a lemma which uses succ_succ to mean add_two, CategoryTheory.ComposableArrows.Precomp.map_zero_succ_succ. :mind:

lemma map_zero_succ_succ (j : ℕ) (hj : j + 2 < n + 1 + 1) :
    map F f 0 ⟨j + 2, hj⟩ (by simp) = f ≫ F.map' 0 (j+1) := rfl

[Damiano Testa]

This is so wrong: clearly is should have been add_zero_succ_succ.

[Jovan Gerbscheid]

Damiano Testa said:

My impression is that succ is "more popular" for historical reasons. For instance, up until recently, induction n would show a goal involving Nat.succ. I was certainly happy to see this change.

Do you mean that the lemmas used to talk about Nat.succ, and then the type was changed without changing the name?

[Damiano Testa]

No, this is what I meant:

example (n : Nat) : n = n := by
  induction n
  · sorry
  · -- goal used to be Nat.succ n = Nat.succ n
    sorry

[Damiano Testa]

So, people were used to have to battle with Nat.succ to convert it to _ + 1 and that trickled into having lemmas that involved Nat.succ.

[Damiano Testa]

I hope that the name was changed, but maybe this has not happened, I am not sure.

[Jovan Gerbscheid]

I am talking about lemmas that have succ in the name, which refers to a _ + 1 in the theorem statement. But you are talking about theorems that contain Nat.succ.

[Jovan Gerbscheid]

(That's why I asked if the types had changed without the names having been changed)

[Damiano Testa]

I think that there was a period where Nat.succ was so frequent, that Nat.succ and add_one weren't often distinguished very clearly. I hope that in the cases where the type changed to use _ + 1, the name was also changed to use add_one, but I am not sure if this actually happened consistently or not.

[Kyle Miller]

Yeah, my impression is the same as @Damiano Testa's. I did my fair share of naming Nat lemmas that referred to _ + 1 with "succ" because of this. I remember it feeling unclear on whether succ or add_one should be preferred.

[Damiano Testa]

In any case, historical reasons aside, even if the decision is not to systematically change all succs to add_one (names and types), I would still prefer if this was the drift.

[Damiano Testa]

So, reporting the number produced by the script above in the PR summarytech debt seems like a good idea: it is a small nudge in the right direction, without being an obligation.

[Damiano Testa]

(In terms of practical matters, this means that the tech debt script will require a Lean component and so the change to CI is not just the addition of a couple of lines.)

[Violeta Hernández]

Bhavik Mehta said:

I disagree, since succ could (and in my view, exclusively should) refer to docs#Order.succ

And really, in the case of a docs#SuccAddOrder, we should similarly be using x + 1 instead of succ x. That's a long-standing TODO blocked only by Ordinal which annoyingly chose the opposite convention.

[Kim Morrison]

I'm very much in favour of changing both names and statements to avoiding mentioning succ where possible.

[Kim Morrison]

:hot_pepper:: let's rename Nat.succ itself...?