grw: more useful handling of

Stream: mathlib4

---

[Albert Smith]

I've been playing around with the (excellent) grw tactic and had the following situation:

import Mathlib

example {α} [Preorder α] (a b c : α) (h : a < b) : a < c := by
  grw [h] -- ⊢ b < c

It would be ideal if grw made the goal b ≤ c instead. Is this doable? Simply marking lt_of_le_of_lt' as @[gcongr] doesn't work.

[Jovan Gerbscheid]

Since grw is a rewriting tactic, it just rewrites the left hand side into the right hand side, without modifying anything else in the expression. So unfortunately it doesn't modify the strictness of the inequality. (I agree it would be nice if it did this, but I don't have a clear idea of how to implement this)

There will also be the gconvert tactic in the future which will work as follows:

import Mathlib

example {α} [Preorder α] (a b c : α) (h : a < b) : a < c := by
  gconvert h -- ⊢ b ≤ c

To get the behaviour of gconvert h, you can currently use revert h; gcongr:

example {α} [Preorder α] (a b c : α) (h : a < b) : a < c := by
  revert h -- ⊢ a < b → a < c
  gcongr -- ⊢ b ≤ c

This approach however only works when the shape of the hypothesis and the goal are the same. If the goal is something like 2 * a < c, then this doesn't work. In that case I would suggest using the gcongr tactic in combination with a have statement or a calc block:

example (a b c : ℝ) (h : a < b) : 2 * a < c := by
  calc 2 * a < 2 * b := by gcongr
  _ ≤ c := by sorry

[Albert Smith]

Ah, I see. I guess the most natural edit to grw would be to try relaxing the expected new goal's relation to ≤ whenever it's <. But that could be 2x slower, and also doesn't work because it involves calling gcongr on a goal like b ≤ c → a < c, which is not of the required form f ⋯ ~ f ⋯. A possible solution is to extend gcongr to support goals f ⋯ ~ g ⋯ as long as f, g have the same signature (maybe this is only useful for this specific scenario)

[Albert Smith]

anyway, seems like it's not trivial; thanks for the alternatives