grw loc

Stream: mathlib4

[Alex Meiburg]

I was giving a first demo about Lean to someone today, and ran into the following (embarrassing) issue:

import Mathlib

example (x : ℝ) (y : ℝ) (hx : 0 ≤ x) (h : x ≤ y) : 1 + 3 * x ≤ (1 + y)^3 := by
  have h_bernoulli := one_add_mul_le_pow (a := x) (by linarith) 3
  simp at h_bernoulli
  grw [h] at h_bernoulli
  sorry

This doesn't work, because grw only wants to rewrite the x to y on the LHS, not the RHS. And that's invalid. I couldn't find a way to do anything like nth_grewrite of course :slight_smile: Of course there were plenty of other ways I could handle this - I worked around it and showed the proof - but this would be a nice thing to do better.

[Aaron Liu]

so do you want it to rewrite on the lhs or the rhs or both?

[Aaron Liu]

If you want it to rewrite on just the rhs then you can do

  grw (occs := [2]) [h] at h_bernoulli

[Alex Meiburg]

Just the RHS, the LHS would be wrong mathematically. Okay, the syntax is good to know! I couldn't have guessed it, but I'm guessing that someone more familiar with the syntax for rw could have :)

[Aaron Liu]

yeah I knew that worked for rw so I guessed that it would work for grw too (:

[Alex Meiburg]

I think that my :star: perfect world :star: behavior of the tactic would be something like:

• it rewrites just where it can (so, in this case, just the RHS)
• if it didn't work at all, then it's an error
• if it only works in some locations and it had to try and fail some others (like the above), it works but gives a yellow-squiggly warning, with text something like:

grw couldn't rewrite first occurrence:
  Tactic `grewrite` failed: could not discharge y ≤ x using x ≤ y
grw did successful rewrite at occurrence 2. To make this behavior explicit,
Try this: grw (occs := [2]) [h] at h_bernoulli
or use grw! [h] at h_bernoulli to ignore this warning.

[Alex Meiburg]

but yeah in this case my fault has probably been that I never actually learned the right syntax for occs and just used other ways of specifying the rewrite I wanted lol.

[Jovan Gerbscheid]

There is also nth_grw, akin to nth_rw:

import Mathlib

example (x : ℝ) (y : ℝ) (hx : 0 ≤ x) (h : x ≤ y) : 1 + 3 * x ≤ (1 + y)^3 := by
  have h_bernoulli := one_add_mul_le_pow (a := x) (by linarith) 3
  simp at h_bernoulli
  nth_grw 2 [h] at h_bernoulli
  sorry

[Jovan Gerbscheid]

I agree that it would be nice for grw to figure out by itself which positions it can and cannot rewrite in. That would mean that in your example your original code would work. However, this is significantly harder to implement, so for the first version of the tactic I went with this more basic implementation.

[Alex Meiburg]

Ahh! I see nth_grw and nth_grewrite actually do exist. Shucks! :) Well then I really do have nothing to complain about. I think during the demo I might've typed gnth_rewrite, but that is clearly the "wrong" name for that tactic... awesome, thanks!