new elaborator: ofNat()

Stream: mathlib4

[Eric Wieser]

Just a heads up about:

rss-bot said:

refactor: add an ofNat() elaborator (mathlib4#20169)

ofNat(n) is a shorthand for no_index (OfNat.ofNat n).

(click through for the full commit message)

There are still stray OfNat.ofNats left in mathlib, but we should try to use ofNat() in any new work.

[Eric Wieser]

If anyone fancies writing a linter to detect these and including them in our tech debt stats, that would be great!

[Eric Wieser]

@Violeta Hernández, there are 27 matches for See note [no_index around OfNat.ofNat] in SetTheory; next time you put your tidying hat on, could you perhaps look at switching these to use ofNat() instead?

[Violeta Hernández]

Sure! I've been on somewhat of a vacation but I'll keep that in mind

[Johan Commelin]

@Eric Wieser Is this the counter you had in mind? Or something more subtle

$ rg "OfNat.ofNat" Mathlib | wc -l
403

Because this one would be trivial to add to the tech debt stats.

[Eric Wieser]

I think that might be too aggressive; as a conservative option we could start by counting the library note

[Johan Commelin]

So

$ rg "See note.*OfNat.ofNat" Mathlib | wc -l
97

[Eric Wieser]

Is that the same as the result for "See note \[no_index around OfNat.ofNat\]"? Would your regex match See note<100 lines follow>OfNat, or does rg operate on a per-line basis?

[Johan Commelin]

It is per line

[Johan Commelin]

The number is indeed the same if we match on the exact string.

[Edward van de Meent]

btw, does that mean we also have to update the library note itself? currently (i.e. on latest mathlib on the playground) the note reads as follows:

library_note "no_index around OfNat.ofNat"
* When writing lemmas about `OfNat.ofNat` that assume `Nat.AtLeastTwo`, the term needs to be wrapped
  in `no_index` so as not to confuse `simp`, as `no_index (OfNat.ofNat n)`.

  Rather than referencing this library note, use `ofNat(n)` as a shorthand for
  `no_index (OfNat.ofNat n)`.

  Some discussion is [on Zulip here](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/.E2.9C.94.20Polynomial.2Ecoeff.20example/near/395438147).

[Eric Wieser]

What are you proposing? The purpose of the library note is:

• To explain the existing uses of no_index (OfNat.ofNat in the library
• To tell you not to write more code in this way, and use ofNat( instead

[Edward van de Meent]

it seems i can't read :see_no_evil:

[Edward van de Meent]

indeed, the library note does explain that the shorthand should be used

[Eric Wieser]

Of course, really we want to delete the library note entirely, but we have to clear up the 52 (non-SetTheory in 19 files) + 27 (SetTheory in 7 files) references to it first

[Edward van de Meent]

still, a library note as to what the purpose of ofNat() is and what the distinction is between it and OfNat.ofNat might be useful?

[Eric Wieser]

Isn't that role served by the docstring of ofNat()?

[Edward van de Meent]

:thinking: i think you're right

[Eric Wieser]

Feel free to improve the wording there if it is unclear, but I'm pretty sure that's the right place for an explanation to be

[Michael Stoll]

The problem with having the info in the docstring of ofNat() is that one has to know aboutofNat() to find it. It would perhaps be good to have some info in the docstring of docs#OfNat.ofNat itself, but IIRC it is not (yet?) possible to extend docstrings in a later file. (OfNat.ofNat is in Init.Prelude...)

[Johan Commelin]

@Eric Wieser #20394 adds the tech debt metric

[Anne Baanen]

#20521 replaces all occurrences of no_index (ofNat _) that grep could find with the new ofNat() macro.

[Eric Wieser]

A spinoff from this discussion: #lean4 > Writing theorems about ofNat @ 💬

[Eric Wieser]

I remember saying in review at one point that I was uncomfortable with ofNat(n + 1), this provides some justification for that hunch.

[Johan Commelin]

Could that become a parse error? So that ofNat(x) only parses when x is a variable name?

[Eric Wieser]

Yes, certainly; but if we do that we should probably remove docs#Real.Gamma_ofNat_eq_factorial which breaks the rule

[Eric Wieser]

I think there are quite a few places where we want to apply a theorem with a literal like 37 on one side and get 36 on the other though, so it would be nice to have a mechanism to do this that doesn't require a simproc each time

[Oliver Nash]

Eric Wieser said:

Yes, certainly; but if we do that we should probably remove docs#Real.Gamma_ofNat_eq_factorial which breaks the rule

Glancing at this now is shouldn't we replace the horrid [(n + 1).AtLeastTwo] with [NeZero n]?

[Oliver Nash]

I guess we might need to add:

instance (n : ℕ) [NeZero n] : (n + 1).AtLeastTwo := ⟨have := NeZero.ne n; by omega⟩

[Eric Wieser]

I think the ofNat is the bigger concern in that lemma statement

[Oliver Nash]

Yes absolutely, I was just noting this in passing.

[Eric Wieser]

I would extend my claim to (almost) every occurence of (n + 1).AtLeastTwo being also guilty of this ofNat gray area!