Commit 2026-06-07 02:12 ab5497e4

feat(GRewrite): new grw implementation (#38318) This PR adds a new implementation of the grewrite tactic. It replaces grw with the new implementation. The old implementation can be used with grw +useKAbstract. New features:

• The new grw can rewrite terms with bound variables.
• The new grw will only rewrite in places where this is valid. Previously, if there were both valid and non-valid positions, it would try rewriting everywhere and then complain. Future features that will build on the new implementation:
• I'd like to add support for strict rewrites that can change the strictness of parts of the goal. This would require the concept of asymmetric gcongr lemmas, something like le_imp_lt_of_lt_left and le_imp_lt_of_lt_right. An example of such a lemma that already exists in mathlib is Ico_subset_Ioo_left.
• I'd like to improve the support for rewriting with symmetric relations such as =ᵥ. The following doesn't work very well yet:

variable {R : Type*} [CommRing R] [ValuativeRel R] {x y z : R}
example (h : x =ᵥ y) : x <ᵥ z ↔ y <ᵥ z := by
  grw [h]

Limitations:

• The new implementation does not support occurrences. So, nth_grw still uses the old kabstract-based implementation. The reason is that there are often multiple gcongr lemmas for rewriting in the same place (e.g. add_le_add and add_le_add_left), and it's tricky to keep track of exactly what is "the same" subexpression.
• The new implementation tries gcongr lemmas one by one, and commits to the first gcongr lemma that lets us do a rewrite. This means that we need to lower the priority of add_le_add_left, so that add_le_add is preferred, so that we can rewrite on both sides of + at the same time. However, mul_le_mul_of_nonneg_left and mul_le_mul_of_nonneg_right are still tried before mul_le_mul, to avoid getting unnecessary side goals.
• Because the new term is constructed from gcongr lemmas, rather than by instantiating the result of kabstract, it may be that metadata gets lost, or that some implicit arguments change. For example, rewriting inside a ≤ b for a b : Nat will change the instance argument from Nat.instLE to Nat.instPreorder.toLE. This is not really a problem.
• Some problems arise when implementing a rewriting tactic that can rewrite under binders, because metavariables have a fixed local context of free variables that they are allowed to depend on. This issue also affects the new rw tactic that the FRO is currenlty working on. This PR works around this by "illegally" changing the local context of metavariabes, so as to allow them to depend on bound variables. This has the unfortunate side effect that the "Expected Type" view can get messed up when rewriting bound variables, because the expression is being delaborated with the wrong local context. But I think this is only a minor problem. We coould reconsider this design when the new rw tactic is done. Changes to gcongr:
• The @[goncgr] attribute now checks more thoroughly whether the given lemma is of the right form. Some lemmas are not suitable for use in grw, but they still "feel" like a gcongr lemma, so we still allow them to be used in gcongr. For such cases I've added a linter warning that can be turned off.
• I've refactored how gcongr lemmas are applied, in order to share this code between gcongr and grw. Now, binder names are taken from the goal when possible, rather than not giving any name to new free variables. This improves gcongr (as it means you don't anymore need to write gcongr with ... to give the variable a name), and allows grw to preserve binder names in the goal. The grewrite test file now tests the new grw implementation. Should I make a copy of the test file to also test the old implementation? I have put myself as the copyright holder, instead of Sebastian Zimmer, as I think this more accurately reflect code ownership. The original grw PR was by Sebastian in 2023, but it was majorly rewritten by me in 2025. Sebastian is still in the list of authors.