Bug(?) in `congrm` and `refine`

Stream: mathlib4

[Yury G. Kudryashov]

Here is a #mwe:

import Mathlib.Tactic.CongrM

-- works
example (a b : ℤ) : (a - b + b) + a + b = a + (a - b + b) + (b - a + a) := by
  congrm ?h1 + ?h2
  · congrm ?h3 + ?h4 <;> rw [Int.sub_add_cancel]
  · rw [Int.sub_add_cancel]

-- fails
example (a b : ℤ) : (a - b + b) + a + b = a + (a - b + b) + (b - a + a) := by
  congrm ?h1 + ?h2
  · congrm ?h1 + ?h2 <;> rw [Int.sub_add_cancel]
  · rw [Int.sub_add_cancel]

[Yury G. Kudryashov]

In the second example, the second call to congrm tries to reuse ?h1 and ?h2 from the first call to congrm.

[Yury G. Kudryashov]

CC: @Moritz Doll , @Damiano Testa

[Damiano Testa]

That's interesting: thanks for the report!

[Damiano Testa]

This could be fixed by replacing the given metavar names with "fresh" ones, although I am not completely sure that the current behaviour is undesirable.

[Yury G. Kudryashov]

refine does the same:

import Mathlib.Tactic.CongrM

example (a b : ℤ) : (a - b + b) + a + b = a + (a - b + b) + (b - a + a) := by
  refine congrArg₂ (· + ·) ?h1 ?h2
  · refine congrArg₂ (· + ·) ?h1 ?h2 -- fail

[Yury G. Kudryashov]

I think that it should be either documented or changed.

[Yury G. Kudryashov]

Generally, I wouldn't expect tactic calls in different branches of the proof interact in any way.

[Damiano Testa]

The congrm tactic is implemented via refine (congr(pattern)), so the two are correlated. :smile:

[Damiano Testa]

Let me try to see if my proposed "fix" builds mathlib.

[Yury G. Kudryashov]

Here is a Mathlib-free example:

theorem congrArg₂ (f : α → β → γ) {x x' : α} {y y' : β}
    (hx : x = x') (hy : y = y') : f x y = f x' y' := by subst hx hy; rfl

example (a b : Int) : (a + b) + (b + a) = (a + b) + (b + a) := by
  refine congrArg₂ (· + ·) ?_ ?_
  · have : ∀ a b : Int, a + b = a + b := by
      refine fun a b => congrArg₂ (· + ·) ?h1 ?_
      rfl
    rfl
  · refine congrArg₂ (· + ·) ?h1 ?_ <;> rfl

[Damiano Testa]

#22422 has the "downstream" fix, but, if this is something that should be fixed, it should be in refine or further upstream.

[Yury G. Kudryashov]

@Kim Morrison Is it a bug or an underdocumented feature?

[Kyle Miller]

This is a problem with how metavariable names work. There's a single namespace for metavariables, and when they're re-used, they refer to the same metavariable. This is used by some people, for better or for worse, to be able to use values across multiple tactic branches.

It's not a bug with refine itself, but with how ?m syntax is elaborated.

The thing is, congrm really is wanting metavariables here, since they stand for the equality proof.

It makes sense that refine and congrm might want to elaborate ?m as a guaranteed new metavariable. I think we should think about how to get that done in a consistent way, rather than add a workaround in congrm itself.

Right now, the safest thing to do is use ?_ instead, like congrm ?_ + ?_.

[Damiano Testa]

I will close the PR: it was fun to work out what the issue was, but I agree that this feature/bug is upstream! :smile:

[Kyle Miller]

With your solution @Damiano Testa, did using case work , like case h1 =>, to select one of the goals after congrm?

[Damiano Testa]

Yes, I had tried that.

[Damiano Testa]

I was worried that the hygienic names would get in the way, but they didn't.

[Damiano Testa]

I suspect that the matching in case is by "username", rather than by actual name.

[Kyle Miller]

I think the only two names a metavariable has are its mvarid and its username

[Damiano Testa]

Ok, I updated the test to use case h1 and it seems to have passed (I'm no longer at a computer, though).

[Damiano Testa]

In a previous iteration, my phone's autocorrection had case H1 => and the error message seemed to talk about the hygienic names.