rw? not closing goal

Stream: mathlib4

[Patrick Massot]

There is an inconsistency between apply? and rw? when the first suggestion closes the goal.

import Mathlib.Tactic
import Mathlib.Data.Real.Basic

example (x : ℝ) (h : 0 < x) : |x| = x := by -- no error
  apply?

example (x : ℝ) (h : 0 < x) : |x| = x := by -- unsolved goal
  rw?

I prefer the apply? behavior because i leave those tactics in my lecture notes when I want to point out there is no need to remember a lemma name.

[Patrick Massot]

@Scott Morrison

[Patrick Massot]

Wait, my example isn't good.

[Patrick Massot]

I meant to write an example where there is no remaining goal at all.

[Patrick Massot]

import Mathlib.Tactic
import Mathlib.Data.Real.Basic

example (x y : ℝ)  : x + y = y + x := by -- no error
  apply?

example (x y : ℝ) : x + y = y + x := by -- unsolved goal
  rw?

is what I meant

[Scott Morrison]

This is currently rw?!. I guess there is no harm in just making it the default.

[Scott Morrison]

@Patrick Massot, #7247

[Patrick Massot]

Thanks!

[Antoine Chambert-Loir]

There are also moments where I want to do some rewrite. My strategy then is to construct an example which asserts the equality and to search for a proof using apply?. But very often, its answer is rfl and I'm stuck in my ignorance.

[Scott Morrison]

@Antoine Chambert-Loir, doesn't rw? solve this problem for you? It won't ever say rfl. It's also often easy to use because you don't need to "isolate" the fact you know you need.

[Antoine Chambert-Loir]

I'm not sure I ever tried that… I'll try next time, thanks for the hint!

[Ruben Van de Velde]

Yeah, I also use it for this purpose. (Though it would be nice if apply? didn't insist on suggesting rfl so much)

[Scott Morrison]

The hooks are all there in solve_by_elim to reject that solution!

[Scott Morrison]

(Although I do plan to rewrite all those hooks in the new future, so maybe it is best not to learn/use them right now. :-)