[Merged by Bors] - chore(Tactic/GRewrite): rewrite `grw` family tactic docstrings by Vierkantor · Pull Request #36283 · leanprover-community/mathlib4

Vierkantor · 2026-03-06T17:11:54Z

This PR rewrites the docstrings for tactics in the grw family: grw, grewrite, apply_rw, apply_rewrite, nth_rw and nth_rewrite, to consistently match the official style guide, to make sure they are complete while not getting too long.

The grw tactic docstring was nice and complete, but the others were very brief and needed expansion (especially since it took me quite some time to understand the motivation behind apply_rw).

This PR rewrites the docstrings for tactics in the `grw` family: `grw`, `grewrite`, `apply_rw`, `apply_rewrite`, `nth_rw` and `nth_rewrite`, to consistently match the official style guide, to make sure they are complete while not getting too long. The `grw` tactic docstring was nice and complete, but the others were very brief and needed expansion (especially since it took me quite some time to understand the motivation behind `apply_rw`).

github-actions · 2026-03-06T17:16:01Z

PR summary 062adc5c07

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows

## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/reporting/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

JovanGerb

Thanks for uniformizing the doc-strings of these tactics! There are a few issues though.

Mathlib/Tactic/GRewrite/Elab.lean

JovanGerb · 2026-03-06T21:12:18Z

Mathlib/Tactic/GRewrite/Elab.lean

+If an expression `e` is a defined constant, then the equational theorems associated with `e` are
+used. This provides a convenient way to unfold `e`. If `e` has parameters, the tactic will try to
+fill these in by unification with the matching part of the target. Parameters are only filled in
+once per rule, restricting which later rewrites can be found. Parameters that are not filled in
+after unification will create side goals.


I don't think we should be explaining how rw works in the doc-string of grw. I'm not even sure myself if this paragraph is correct.

As far as I can tell they use the same rewrite rule elaborator. And I think it's better to be precise here, unless there's something explicit we can refer to (e.g. a section in the Lean reference manual).

I would rather not spend many words in the grw docstring talking about what rw does. I think this should be at most one sentence.

The reason is that generalized rewriting is quite a hard concept for many people to understand, and the main goal of the docstring of grw should be to help people understand it.

I agree that the point of a docstring is to help people understand what a tactic does. But more specifically, the reader should be able to parse and understand a tactic invocation by hovering and getting a docstring. So it is important to be complete and self-contained: we need to mention what happens if there are underscores or e isn't a lemma involving relations.

If this were documented well in the Lean reference manual then we could write something like:

Constants and holes in the expression `e` are treated like `rw [e]` would; see ... for details.

But currently this is not mentioned at all, not even in the rw docstring (I have a PR to core Lean that should fix this, but it hasn't been touched in a while).

Mathlib/Tactic/GRewrite/Elab.lean

JovanGerb · 2026-03-06T21:16:58Z

Mathlib/Tactic/GRewrite/Elab.lean

+If an expression `e` is a defined constant, then the equational theorems associated with `e` are
+used. This provides a convenient way to unfold `e`.


Again, this part should not be here.

I argue for keeping this for the same reason as we should keep it for grw.

JovanGerb · 2026-03-07T18:06:37Z

Many people find it unintuitive that they have to add the ← arrow when doing a generalized rewrite from right to left. In you current version, this is only mentioned briefly at the end. I think this should be one of the first things mentioned, and with some example or explanation.

The difference with rw is rewrite lemmas usually have a preferred rewrite direction, so most of the time you rewrite left to right, and you don't need to worry about the arrow. But in grw, when rewriting with inequalities, you need the left arrow about 50% of the time.

joneugster

Looks like the latest review comments haven't been adressed yet, so I'm marking this awaiting-author again

Mathlib/Tactic/GRewrite/Elab.lean

Vierkantor · 2026-03-30T13:48:18Z

Many people find it unintuitive that they have to add the ← arrow when doing a generalized rewrite from right to left. In you current version, this is only mentioned briefly at the end. I think this should be one of the first things mentioned, and with some example or explanation.

I have rewritten the first paragraphs of the docstrings, hopefully they are clearer now. (I would expect it's less expected that a symmetric relation like equality is assigned a direction. But I trust your experience!)

JovanGerb · 2026-03-30T17:51:57Z

Thanks, it looks good to me now.

At the end it's slightly awkward how apply_rw is mentioned twice. But I guess that is a consequence of the standard order you are using?

Mathlib/Tactic/GRewrite/Elab.lean

adamtopaz · 2026-04-08T16:13:07Z

Looks like just one more small comment, then it's good to go! Thanks!

bors d+

mathlib-bors · 2026-04-08T16:13:10Z

✌️ Vierkantor can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

Mathlib/Tactic/GRewrite/Elab.lean

Vierkantor · 2026-04-14T13:13:13Z

Oh right, the build succeeded so:

bors r+

This PR rewrites the docstrings for tactics in the `grw` family: `grw`, `grewrite`, `apply_rw`, `apply_rewrite`, `nth_rw` and `nth_rewrite`, to consistently match the official style guide, to make sure they are complete while not getting too long. The `grw` tactic docstring was nice and complete, but the others were very brief and needed expansion (especially since it took me quite some time to understand the motivation behind `apply_rw`). Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com>

mathlib-bors · 2026-04-14T13:50:54Z

Pull request successfully merged into master.

Build succeeded:

Vierkantor added documentation Improvements or additions to documentation t-meta Tactics, attributes or user commands labels Mar 6, 2026

JovanGerb reviewed Mar 6, 2026

View reviewed changes

Main goal doesn't need to be a relation.

d1b12e8

mathlib-triage bot assigned adamtopaz Mar 11, 2026

joneugster added the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 27, 2026

joneugster reviewed Mar 27, 2026

View reviewed changes

Mathlib/Tactic/GRewrite/Elab.lean Show resolved Hide resolved

Mathlib/Tactic/GRewrite/Elab.lean Outdated Show resolved Hide resolved

Vierkantor added 3 commits March 30, 2026 15:10

Rephrase apply_rw documentation focussing only on implication

e811c01

Add right-to-left variant too

72ab884

Rewrite first paragraph to indicate what exactly gets rewritten

6a04829

Vierkantor removed the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 30, 2026

JovanGerb reviewed Apr 8, 2026

View reviewed changes

Mathlib/Tactic/GRewrite/Elab.lean Outdated Show resolved Hide resolved

mathlib-triage bot added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Apr 8, 2026

Vierkantor commented Apr 13, 2026

View reviewed changes

Mathlib/Tactic/GRewrite/Elab.lean Outdated Show resolved Hide resolved

Vierkantor commented Apr 13, 2026

View reviewed changes

Mathlib/Tactic/GRewrite/Elab.lean Outdated Show resolved Hide resolved

Vierkantor and others added 2 commits April 13, 2026 16:20

Clarify apply_rw/apply_rewrite.

73ef1cb

Merge remote-tracking branch 'upstream/master' into document-grw-tactic

e1af8ae

mathlib-triage bot added the ready-to-merge This PR has been sent to bors. label Apr 14, 2026

mathlib-bors bot changed the title ~~chore(Tactic/GRewrite): rewrite grw family tactic docstrings~~ [Merged by Bors] - chore(Tactic/GRewrite): rewrite grw family tactic docstrings Apr 14, 2026

mathlib-bors bot closed this Apr 14, 2026

		If an expression `e` is a defined constant, then the equational theorems associated with `e` are
		used. This provides a convenient way to unfold `e`.

Conversation

Vierkantor commented Mar 6, 2026

Uh oh!

github-actions bot commented Mar 6, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 062adc5c07

Import changes for modified files

Declarations diff

Uh oh!

JovanGerb left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

JovanGerb Mar 6, 2026

Choose a reason for hiding this comment

Uh oh!

Vierkantor Mar 7, 2026

Choose a reason for hiding this comment

Uh oh!

JovanGerb Mar 7, 2026

Choose a reason for hiding this comment

Uh oh!

Vierkantor Mar 30, 2026

Choose a reason for hiding this comment

Uh oh!

Uh oh!

JovanGerb Mar 6, 2026

Choose a reason for hiding this comment

Uh oh!

Vierkantor Mar 30, 2026

Choose a reason for hiding this comment

Uh oh!

JovanGerb commented Mar 7, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

joneugster left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Vierkantor commented Mar 30, 2026

Uh oh!

JovanGerb commented Mar 30, 2026

Uh oh!

Uh oh!

adamtopaz commented Apr 8, 2026

Uh oh!

mathlib-bors bot commented Apr 8, 2026

Uh oh!

Uh oh!

Uh oh!

Vierkantor commented Apr 14, 2026

Uh oh!

mathlib-bors bot commented Apr 14, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

github-actions bot commented Mar 6, 2026 •

edited

Loading

JovanGerb commented Mar 7, 2026 •

edited

Loading