How to use nth_rewrite in NNG4?

Stream: general

[Alex Sweeney]

I'm on Power World 7/10 (https://adam.math.hhu.de/#/g/hhu-adam/NNG4/world/Power/level/7)
and I would like to use nth_rewrite with mul_comm to help move the terms around easier.

I'm here:

Current Goal
Objects:
abn_1: ℕ
Assumptions:
n_ih: (a * b) ^ n_1 = a ^ n_1 * b ^ n_1
Goal:
a ^ n_1 * b ^ n_1 * (a * b) = a ^ n_1 * a * (b ^ n_1 * b)

But nth_rewrite X [mul_comm] only does something when X=1. The error under mul_comm for X>1 is

tactic 'rewrite' failed, did not find instance of the pattern in the target expression

Even though there are plenty of multiplications to commute on the lhs. Am I using it wrong?

[Scott Morrison]

No, this is a known problem: lean4#2538, with a fix at lean#2539 that is stalled in review.

For now most people provide extra arguments, e.g. rw [mul_comm x].

[Kevin Buzzard]

Can we have Natural number game high prio tag on the issue? ;-)

@Alex Sweeney sorry about this :-)

[Kevin Buzzard]

(lean4#2539 I guess)

[Scott Morrison]

Part of making things high priority is to +1 the issue/PR, and even leave a comment explaining why you want it.

So far I have only wanted this for internal use in rw? and rw_search.

[Michael Stoll]

I'm putting together some "tips & tricks" for the students in my formalization "seminar". I was thinking of mentioning nth_rw as an alternative to rw when there are several places matching the lhs and more selective rewriting is desired. But in the current state, I feel that I can't do this, as explaining how it works precisely would be rather confusing. :frown:

[Mario Carneiro]

BTW there is also rw (occs := n) for doing nth rewrite, I'm not sure if it still has the same issues that motivated nth_rw in lean 3

[Patrick Massot]

Michael you can use conv to do that. This is now easier using the conv? widget.

[Michael Stoll]

I can certainly find some work-around. I'm complaining on behalf of my students :smile: .

[Patrick Massot]

I understand, but I'm pointing out that conv is now a lot easier to use.

[Michael Stoll]

rw (occs := 2) [pow_two] gives me an "unexpected token '('" error. What would be correct syntax?

[Michael Stoll]

Doing conv? in the example above and then shift-clicking the lhs of the equality and then clicking on "Generate conv" results in

example (x y z : ℤ) : x^2 + y^2 = x^2 + y*y := by
  conv =>
   enter [1]

but then the widget is gone and I cannot zoom in further.

[Patrick Massot]

This works as intended, you can now operate on what you clicked on.

[Patrick Massot]

But indeed we could add a conv version of conv? to repeatedly zoom. However the current tool should be enough for most situations for your students.

[Michael Stoll]

But how can I use the widget now to get from x^2 + y^2 to y^2?

[Michael Stoll]

Ah, OK; I have to do it in one step.

[Patrick Massot]

You can't without have a conv version of the conv? tactic. I don't know how to write conv-mode tactics, but this shouldn't be hard.

[Yaël Dillies]

Michael Stoll said:

rw (occs := 2) [pow_two] gives me an "unexpected token '('" error. What would be correct syntax?

rw [pow_two] (occs := 2) I believe?

[Michael Stoll]

Nope, same error.

[Scott Morrison]

rw [pos_two] (config := {occs := .pos [2]}), sadly

[Scott Morrison]

It still suffers from the same problem that necessitated nth_rewrite in Lean 3, please see lean4#2539.

Note that the nth_rewrite implemented in Mathlib is just a wrapper around occs, and in particular is not at all a re-implementation of my nth_rewrite from Lean 3.

We'll get this functionality back when lean4#2539 is merged.