docstrings of `nth_rewrite` and `nth_rw`

Stream: mathlib4

[Shreyas Srinivas]

Currently the docstring of nth_rewrite gives no indicatinn of the syntax for specifying the occurrence number. I propose to add examples to it. nth_rw simply tells the user that nth_rw is the same as nth_rewrite with some rfl stuff. So a new user must first hunt around for nth_rewrite (or type it in to check the docstring). I suggest copying and adapting the docstring of nth_rewrite.

[Kim Morrison]

Please do!

[Shreyas Srinivas]

mathlib4#13877

[Shreyas Srinivas]

Found what might be a potential footgun for an unsuspecting user:

import Mathlib


-- footgun demo
example {a b : ℝ} (h : a = b + a) : a + a + a + a + a = b := by
  nth_rw 2 [h, h, h, h] -- footnote on infoview
  sorry

/-
footnote:
ab: ℝ
h: a = b + a
⊢ a + (b + (b + (b + (b + a)))) + a + a + a = b
-/

if the LHS of h is contained as a subterm in the RHS of h, then in successive nth_rws the new subterm will be rewritten over and over (or affect the occurrence count). I can document this too, but it sounds like a massive footgun either way.

[Richard Copley]

What is the desired behaviour? (I don't understand the problem. It seems to be doing exactly what it was asked to do.)

[Shreyas Srinivas]

It is tough to reason about the behaviour when you have complex equations and many of them instead of the four simple hs I have put in there. For example, if there's an unexpected occurrence of a in some long theorem statement it can heavily confuse users. Instead of eliminating the a's in the goal one by one you are simply substituting into the new a you have accidentally introduced. Basically binder substitution is hard.

[Shreyas Srinivas]

Anyway, I am just goiing to document this now and leave it at that. This might be worth a separate discussion.

[Kim Morrison]

Using nth_rw with multiple lemmas is kind of insane to begin with.

[Shreyas Srinivas]

I found at least one such occurrence of nth_rewrite in mathlib

[Shreyas Srinivas]

I added a brief one-liner to explain how this works. The PR is ready for review (It's building but I guess docstrings shouldn't affect the build).

[Shreyas Srinivas]

Some occurrences of nth_rewrite with multiples lemmas: here, here, here, and a large one here

[Shreyas Srinivas]

And one for nth_rw here

[Shreyas Srinivas]

I updated the docstrings of the PR (mathlib4#13877) this morning to add some examples.

[Shreyas Srinivas]

I request feedback on these. I just picked the simplest example that I think showed how it all works

[Jon Eugster]

I left you some comments :) not an official reviewer though, so take it with a grain of salt

[Shreyas Srinivas]

I liked the comments. I am responding to them right away.

[Shreyas Srinivas]

About that Nat.add_comm example: Is it correct to say nth_rw rewrites the nth occurrence of an expression in precedence order?

[Shreyas Srinivas]

I am trying to write things in a less computer sciencey way, so referring to things like expression trees is probably not a good way to go EDIT : made the necessary changes and used your example to explain why order of precedence can make thigns weird.

[Shreyas Srinivas]

About the extendDocs solution for the identical copies of docstrings for nth_rewrite and nth_rw, it would work better if one could hygienically substitute parameters representing the tactic name in this case into a docstring, like the s!"..{}" format strings. Is that possible in docstring comments?

[Shreyas Srinivas]

Also, @Kim Morrison : The note about the change of occurrence count from 0 to 1 between mathlib3 and mathlib4 appears redundant and pointless after the port. Shall I remove it?

[Jon Eugster]

Shreyas Srinivas said:

About the extendDocs solution for the identical copies of docstrings for nth_rewrite and nth_rw, it would work better if one could hygienically substitute parameters representing the tactic name in this case into a docstring, like the s!"..{}" format strings. Is that possible in docstring comments?

I don't think that's possible unfortunately, and that would need a feature request to core, I'm afraid. Would be a nice feature though.

[Shreyas Srinivas]

I think this PR is ready to merge. It has 3 approving reviews and passes all checks

[Ruben Van de Velde]

I assume you refer to #13877

[Shreyas Srinivas]

yes

[Shreyas Srinivas]

It was already labelled maintainer merge

[Ruben Van de Velde]

Yes, but the value of the comment is not in the label, but in the bot that posts to a private zulip stream