Bug with tfae_have?

Stream: mathlib4

[Grant Barkley]

It looks like the tfae_have tactic doesn't work when variables appear in the TFAE list which were introduced into the context during tactic mode.

import Mathlib.Tactic.TFAE
example (n : ℕ) : List.TFAE [n = 1, n + 1 = 2] := by
  generalize n = m
  tfae_have 1 ↔ 2; simp
  -- error: [_uniq.5469 = 1, _uniq.5469 + 1 = 2] must be an explicit list of propositions
  tfae_finish

This is the sort of operation one wants to do when there's a rewrite that is helpful for multiple implications. Is this a bug? Is there a workaround?

Note that the following examples work fine.

import Mathlib.Tactic.TFAE
example (n : ℕ) : List.TFAE [n = 1, n + 1 = 2] := by
  generalize h : n = m
  rw [←h]
  tfae_have 1 ↔ 2; simp
  tfae_finish

example (n : ℕ) : List.TFAE [n = 1, n + 1 = 2] :=
fun (m : ℕ) (h : n = m) => by
  rw [h]
  tfae_have 1 ↔ 2; simp
  tfae_finish
    n rfl

[Thomas Murrills]

Definitely a bug; it seems to be a problem with the Qq match. If I replace ~q($a :: $l') => ... on line 94 with the manual version .app (.app (.app (.const ``List.cons _) _) a) l' => ..., there's no issue. I'm not quite sure why...

[Mario Carneiro]

the error looks like a missing withContext

[Patrick Massot]

Mario Carneiro said:

the error looks like a missing withContext

Do you have a Zulip hotkey pasting that sentence?

[Mario Carneiro]

note that Qq match uses isDefEq and hence needs a well formed local context appropriate for the thing being matched

[Thomas Murrills]

The withContexts were actually the second thing I looked at, but moving the goal.withContext line to the appropriate place in the tactic didn't help. Are there some cases where it can "fail to propagate inwards" somehow?

[Thomas Murrills]

Huh. Maybe the issue is that generalize n = m does not actually update the goal's context correctly? I'm not seeing any hypothesis of type n = m appear in the tactic state.

[Grant Barkley]

Same issue with generalize h : n = m

[Grant Barkley]

And with cases', which is how I originally noticed it

[Thomas Murrills]

Oh, I see, I misread the "works just fine" example. And there's no reason it should need the hypothesis in the context anyway. Hmmm.

[Thomas Murrills]

Actually, I was doing something silly which meant I was looking at the wrong output for ages, rip. Updating the context correctly works fine. PR to follow shortly

[Thomas Murrills]

!4#5358 ; I also added an instantiateMVars where it ought to be just to preempt problems from that, even though that's not related.