Announcement: New `grw` tactic

Stream: mathlib4

[Jovan Gerbscheid]

This is an announcement that the grw tactic is now available in mathlib. It allows rewriting with any relation, usually a transitive relation, if the relevant lemmas are tagged with @[gcongr]. Some examples are:

example (h₁ : a < b) (h₂ : b ≤ c) : a + d ≤ c + d := by
  grw [h₁, h₂]

example (h : a ≡ b [ZMOD n]) : a ^ 2 ≡ b ^ 2 [ZMOD n] := by
  grw [h]

example : (h₁ : a ∣ b) (h₂ : p ∣ a * d) : p ∣ b * d := by
  grw [← h₁]
  exact h₂

grw has been designed to have the same syntax and the same features as rw. This means that there is also an nth_grw tactic. And it means that grw cannot rewrite bound variables.

The original PR was opened 2 years ago. I took up this task one week ago, and thanks to the in-person review by @Floris van Doorn, it got merged this week.

I'm making this thread to list some more features that I'd like to have for gcongr and grw (and some of which I'll try to do soon). But I'd also appreciate feedback on the tactic. Although many lemmas have already been tagged with @[gcongr], I'm sure there will be new use cases for which the lemmas haven't been tagged.

[Floris van Doorn]

(I think there is a typo in your last example)

[Terence Tao]

I remember this tactic being proposed during the PFR project (where it would have come in handy). Great to see it finally over the finish line!

[Jovan Gerbscheid]

@Floris van Doorn, thanks for pointing that out. I'll have to fix the doc-string of grw. But now I'm actually not sure which relation should be used inside the RHS of a divisibility:

example (p a b : Int) : p ∣ a → p ∣ b := by
  gcongr
  -- ⊢ a ≡ b [ZMOD p]
  -- ⊢ a ∣ b

Which of the two possible goals do we expect?
A solution allowing both would be to get a ∣ b if the goal is p ∣ a → p ∣ b, and get a ≡ b [ZMOD p] if the goal is p ∣ a ↔ p ∣ b.
And grw could implement the heuristic that if the relation used for rewriting is symmetric, then it runs gcongr on an ↔ goal instead of an → goal.

[Andrew Yang]

Imagine how many more tactics we would have in mathlib if we just lock Jovan and Floris in a dungeon for a month.

[Filippo A. E. Nuccio]

Is there a way to obtain a list of all lemmas marked @[gcongr]?

[Aaron Liu]

import Mathlib

open Lean

run_meta do
  let env ← getEnv
  let map := Mathlib.Tactic.GCongr.gcongrExt.getState env
  logInfo (map.toList.flatMap fun k => k.snd.toList.map fun u => MessageData.ofConstName u.declName)

[Aaron Liu]

There's 610 of them right now and two duplicates for some reason so actually only 608 unique ones

[Aaron Liu]

The duplicates are docs#List.Sublist.drop and docs#Nat.succ_le_succ

[Filippo A. E. Nuccio]

Thanks!

[Filippo A. E. Nuccio]

Follow up question: how did you come up with the numbers & duplicates? Do they show up in your infoview (they don't in mine) or have you used some external tool?

[Aaron Liu]

For the number I did a List.length

[Aaron Liu]

For the duplicates I just filtered for duplicates

[Jovan Gerbscheid]

#25928 defines the gcongr 2 syntax for limiting the depth of gcongr. This is analogous to the congr tactic. It is in addition to the pattern syntax gcongr x + ?_ * _ which also allows you to limit the depth.

[Bhavik Mehta]

If you're playing with gcongr, I think it'd be nice to have gcongr? which gives you the pattern it used, analogous to simp?

[Jovan Gerbscheid]

Actually, gcongr? already exists. But it is an interactive widget tactic. And it is really poorly implemented. I agree with your suggestion (which means replacing the current one).

[Aaron Hill]

Is the inability to rewrite bound variables an intentional part of matching the rw behavior, or could grw eventually get support for it?

[Kevin Buzzard]

From the moment we had simp_rw which seemed to be "rw but works" I've always regarded "rw can't rewrite bound variables" as a bug rather than a feature. However rw has never been "fixed" in years. What is the logic here?

[Riccardo Brasca]

Wasn't the point that rewriting bound variables requires some sort of functional extensionality?

[Riccardo Brasca]

And maybe we don't want a very basic tactic to use additional axioms (this is less of a problem for a mathlib tactic).

[Joachim Breitner]

Kevin Buzzard schrieb:

From the moment we had simp_rw which seemed to be "rw but works" I've always regarded "rw can't rewrite bound variables" as a bug rather than a feature. However rw has never been "fixed" in years. What is the logic here?

I believe there is hope that it will be fixed this year :-)

[Yaël Dillies]

Riccardo Brasca said:

And maybe we don't want a very basic tactic to use additional axioms (this is less of a problem for a mathlib tactic).

Thought so too, but then split was using choice for the longest time :-)

[Ruben Van de Velde]

(Is it not anymore?)

[Yaël Dillies]

No! That was fixed alongside another bug

[Jovan Gerbscheid]

Aaron Hill said:

Is the inability to rewrite bound variables an intentional part of matching the rw behavior, or could grw eventually get support for it?

I agree it would be better if grw would rewrite bound variables. However, the current version is a lot simpler to implement, which is why I went with this implementation (for now).

[Jovan Gerbscheid]

#25942 fixes a bug in the grw tactic: grw currently doesn't work if the goal contains syntheticOpaque metavariables.

[Floris van Doorn]

Btw, for easy acccess, the grw PR is #8167.

[Etienne Marion]

I just used the tactic for the first time, it's amazing! Thanks a lot for this :tada:

[Rémy Degenne]

This looks great! Could it rewrite inside integrals with almost everywhere equalities? Or more generally rewrite with Filter.EventuallyEq

[Jovan Gerbscheid]

There are 2 limitations:

• we need to tag more lemmas with @[gcongr] (e.g. for Filter.EventuallyEq)
• grw currently cannot rewrite bound variables. If you do need to rewrite terms containing bound variables, you can use the gcongr tactic directly, which is a bit less convenient, because it requires you to write out the new expression (e.g. in a calc block).

So feel free to try some examples, and report which ones need tagging.

[Floris van Doorn]

Isn't a third limitation that if the relation is =, one or both of {gcongr, grw} currently have a special case to call {congr, rw}, which means that if you want these tactics to use docs#MeasureTheory.integral_congr_ae and then recursively call gcongr on the (now non-=) goal, you're out of luck?

[Michael Rothgang]

I was searching for grw in https://leanprover-community.github.io/mathlib-manual/html-multi/Tactics/All-tactics/#all_tactics and didn't find it. @Jon Eugster What's the procedure to make a new tactic appear there?

[Jon Eugster]

probably just need to bump the repo again, i.e. update it to the newest mathlib. I'll try to do that later today

[Jon Eugster]

Michael Rothgang said:

I was searching for grw in https://leanprover-community.github.io/mathlib-manual/html-multi/Tactics/All-tactics/#all_tactics and didn't find it. Jon Eugster What's the procedure to make a new tactic appear there?

I've bumped the manual to v4.21.0 over lunch, so the tactic is now here:
https://leanprover-community.github.io/mathlib-manual/html-multi//Tactics/All-tactics/#grw

I'll bump it again to v4.22 tonight

[Bryan Gin-ge Chen]

If bumping the repo is just a matter of running a script or something, I could try and throw together some automation for it.

[Jovan Gerbscheid]

An update on the progress for grw and gcongr:

• #26907 will hopefully be merged soon, and adds a few features to gcongr:

  1. Instead of having to tag all of add_le_add, add_le_add_left and add_le_add_right, it will suffice to just tag add_le_add; any extra reflexive subgoals will be closed using rfl. This will make future tagging of lemmas easier, (e.g. I'll do mul_dvd_mul, neg_dvd_neg, pow_dvd_powand Int.ModEq.of_dvd/Nat.ModEq.of_dvd)
  2. @[gcongr] lemmas can have a priority (just like with @[simp]). This will allow to fix #27058
  3. gcongr operates in the reducible transparency instead of reducible_and_instances. This helps to avoid applying the wrong lemma. This will help to revive #14739.

• lean#9304 extends the rfl tactic to close goals of the form p → p. This matches the fact that gcongr treats → as a binary relation. (unfortunately I can't anymore push directly to the mathlib adaptation branch, so I've made a PR to fix it https://github.com/leanprover-community/mathlib4-nightly-testing/pull/13)

• In #27135 I've started to write the gconvert tactic. This is the generalized version of the convert tactic, and this is similarly built upon gcongr. For example in

example (h : a * b < c + d) (ha : 0 ≤ a) : a * a < c + c

writing gconvert h will give you the new subgoals a ≤ b and d ≤ c.
Additionally, gconvert will be able to replace the peel tactic.

Future work may include:

• If a gcongr lemma applies successfully, but it has unsolved side goals, try to find another gcongr lemma that can satisfy all of its side goals. This would allow to rewrite under multiplication with a negative number (by tagging lemmas like mul_le_mul_of_nonpos_left)
• Let gcongr call the congruence prodedure of congr! on equality and iff goals if no gcongr lemmas apply.
• Let gcongr with x y z take rintro patterns instead of just variable names (just like congr!)
• Allow gcongr to go into a lambda e.g. using Pi.le_def.mpr. Maybe we need a @[gext] tag for this.
• Allow gcongrto go into function applications, e.g. using Pi.le_def.mp
• Make it easier to tag lemmas like ENat.coe_le_coe, or Filter.Eventually.mono that aren't quite in the right shape to be a gcongrlemma.

[Filippo A. E. Nuccio]

One question I've never understood about gcongr is why it fails on "basic" relations (and I suppose that the answer is that "it must", but I am not sure and at any rate I do not know why):

import Mathlib

example (a b c d : ℕ) : a ^ b + c = b ^ c + d := by
  congrm ?_ ^ ?_ + ?_ -- works

example (a b c d : ℕ) : a ^ b + c ≤ b ^ c + d := by
  gcongr ?_ ^ ?_ + ?_ --works

example (a b c d : ℕ) : a ^ b + c = b ^ c + d := by
  gcongr ?_ ^ ?_ + ?_ --fails

[Jovan Gerbscheid]

Yes, this is one of the "Future work" points: currently no = or ↔ lemmas have been tagged with gcongr. But instead of going around tagging equality lemmas with gcongr, it would be better to call the congr! tactic internally in the gcongr tactic on = and ↔ goals.

[Jovan Gerbscheid]

The motivation for supporting = and ↔ in gcongr (instead of simply calling the congr! tactic) is that there may be cases where we can move from an = or ↔ goal into a more general relation.

Some motivating example are

• ↔ and propositiona ≡ b [ZMOD n], which moves into the [ZMOD n] relation.
• = and the operation % n, which moves into the [ZMOD n] relation.
• ↔ and proposition∀ᶠ x in l, p x/∃ᶠ x in l, p x, which moves into the =ᶠ[l] relation. (Although the lemma f =ᶠ[l] g → (l.Eventually f ↔ l.Eventually g)seems to be missing in mathlib).
• = and the operation ∫ (a : α), f a ∂μ, which moves into the =ᶠ[ae μ] relation

[Jovan Gerbscheid]

Ping for #26907. Could someone review the @[gcongr] tag updates? The meta code has already been approved.

[Robert Maxton]

Jovan Gerbscheid said:

The motivation for supporting = and ↔ in gcongr (instead of simply calling the congr! tactic) is that there may be cases where we can move from an = or ↔ goal into a more general relation.

Another -- somewhat dangerous but occasionally useful -- transformation is going from a difficult = involing casts, to a HEq where the casts can be eliminated and the remaining expression solved using congr!. I am not at all sure how one would build heuristics for when this is a good idea (perhaps 'matches _ = _ ∘ _root_.cast _' or similar might be a good first step, though in e.g. category theory it's less clear how to handle expressions involving eqToHom), but it should probably be on the dock for consideration at least.

[Jovan Gerbscheid]

Going from = to HEq sounds like a job for the congr! tactic. I'm not sure to what extent it does this already.

(And when I add the congr! steps to gcongr, then it can also be a job for gcongr)

[Jovan Gerbscheid]

One obstacle to getting the congr! steps into gcongr is the fact that gcongr can work with a pattern and congr! doesn't. So the congr! steps first need to be made compatible with using a pattern.

[Yuyang Zhao]

Could grw support lemmas like docs#le_of_le_of_antisymmRel ? grw can be used in https://github.com/vihdzp/combinatorial-games/pull/194, but seems it can only be written as grw [(...).le]. In some worse cases, there are only lemmas about operations and AntisymmRel, but no lemmas about operations and \le.

[Jovan Gerbscheid]

gcongr usually tries to use the most general relation (so ≤ instead of </AntisymmRel (· ≤ ·)), and then tries to close the goal with possibly a stronger relation. For example we have special support for concluding ≤ from a < hypothesis using le_of_lt. In the same way AntisymmRel can be specially supported.

I've opened #28514 that implements this. In the meantime, you could copy this code into your project, to see if it works.

namespace Mathlib.Tactic.GCongr

variable {α : Type*} {a b : α} {r : α → α → Prop}

lemma AntisymmRel.left (h : AntisymmRel r a b) : r a b := h.1
lemma AntisymmRel.right (h : AntisymmRel r a b) : r b a := h.2

@[gcongr_forward] def exactAntisymmRelLeft : ForwardExt where
  eval h goal := do goal.assignIfDefEq (← Lean.Meta.mkAppM ``AntisymmRel.left #[h])

@[gcongr_forward] def exactAntisymmRelRight : ForwardExt where
  eval h goal := do goal.assignIfDefEq (← Lean.Meta.mkAppM ``AntisymmRel.right #[h])

end Mathlib.Tactic.GCongr

[Jovan Gerbscheid]

If there are lemmas about operations and AntisymmRel, but no lemmas about operations and ≤, then simply tagging the lemmas with @[gcongr] should be sufficient to allow rewriting with AntisymmRel. (Even without #28514)

[Yuyang Zhao]

This is very helpful, thank you! But it still doesn't make the last grw work.

section
variable {α} [Preorder α] {a b : α}

infix:50 " ≈ " => AntisymmRel (· ≤ ·)

def f : α → α := sorry

@[gcongr]
lemma f_congr : a ≈ b → f a ≈ f b := sorry

lemma foo (h : a ≈ b) : f a ≈ f b := by
  grw [h]

lemma bar (h : a ≈ b) : f a ≤ f b := by
  grw [h]

end

[Jovan Gerbscheid]

In this case, you can make it work by adding another @[gcongr] lemma:

@[gcongr]
lemma f_congr' : a ≈ b → f a ≤ f b := sorry

I've also been thinking about a heuristic to make this work out of the box, which is to have the grw check if the hypothesis relation is symmetric, and if so, call gcongr with the ↔ relation instead of →. But that might want to wait until ↔ is better supported in gcongr.

[Jovan Gerbscheid]

In order to work towards supporting =/↔ in gcongr/grw in the way I described above, we need to have a version of congr! which (in some combination with gcongr) applies congruences until it reaches a certain subexpression. It is already possible to limit the depth (with congr! 3), but that isn't specific enough. Recall that gcongr can also take a pattern (with gcongr 2 * ?_). From what I understand, the new rw tactic that is on the roadmap may come with such a congruence tactic.

Kyle Miller said:

The rough idea @Jovan Gerbscheid is that it will do the rewrite and then do a post-hoc congruence construction

@Kyle Miller, is this right? And do you know approximately when this development will happen?

[Heather Macbeth]

Jovan Gerbscheid said:

we need to have a version of congr! which (in some combination with gcongr) applies congruences until it reaches a certain subexpression. It is already possible to limit the depth (with congr! 3), but that isn't specific enough. Recall that gcongr can also take a pattern (with gcongr 2 * ?_).

This already exists right? The congrm tactic.

[Jovan Gerbscheid]

The congrm tactic is a thin wrapper around the congr(...) term elaborator (which is why I had originally discarded this option).

Looking more closely at congr(...), it elaborates the lhs and rhs into a form where the holes are annotated with some metadata, so that congr(...) knows up to where to do congruences. This seems like a reasonable approach to also take in gcongr. This would mean that in the implementation of gcongr, instead of keeping track of the pattern while doing the congruences, we would keep track of these metadata annotations.

[Jovan Gerbscheid]

And if want, we could also allow passing proofs directly in the pattern, in the same way that congrm allows:

example (a b : ℝ) (h : a ≤ b) : a + 1 ≤ b + 1 := by
  gcongr $h + 1

[Jovan Gerbscheid]

I have now reimplemented how patterns work in gcongr, so that they work with metadata, just like in congrm. This is a necessary step for supporting equality reasoning in gcongr, as I discussed above. (#30739)

There is also still the open PR #28339 which will allow tagging lemmas whose conclusion is Monotone _.

[Lara Toledano]

The grw tactic allows for

example [TopologicalSpace X] (s t: Set X) (hst : s ⊆ t) (ht : IsMeagre t) : IsMeagre s := by
  grw [hst]
  exact ht

It would be nice if it could also do the following

example [TopologicalSpace X] (s t: Set X) (hst : s ⊆ t) (hs : ¬IsMeagre s) : ¬IsMeagre t := by
  grw [hst]
  exact hs

I tried adding a new @[gcongr] lemma

@[gcongr] --error
lemma not_isMeagre_mono [TopologicalSpace X] (s t: Set X) (hst : s ⊆ t) (hs : ¬IsMeagre s) : ¬IsMeagre t := (IsMeagre.mono hst).mt hs

I also tried defining a new predicate.

def NonMeagre [TopologicalSpace X] (s : Set X) := ¬IsMeagre s

@[gcongr]
lemma NonMeagre.mono [TopologicalSpace X] {s t : Set X} (hst : s ⊆ t) (hs : NonMeagre s) :
    NonMeagre t := (IsMeagre.mono hst).mt hs

example [TopologicalSpace X] (s t: Set X) (hst : s ⊆ t) (hs : NonMeagre s) : NonMeagre t := by
  grw [hst] --error

In this last snippet, I do not understand why the gcongr attribute is added without error, but not used correctly in the example.

[Jovan Gerbscheid]

In your second example, you want to rewrite from right to left. So, just like in rw, you should use the left arrow: grw [← hst]

[Lara Toledano]

Thank you so much!

example [TopologicalSpace X] (s t: Set X) (hst : s ⊆ t) (hs : ¬IsMeagre s) : ¬IsMeagre t := by
  grw [← hst]
  exact hs