bug in cases' goal management

Stream: mathlib4

[Rob Lewis]

There seems to be a bug in cases' related to goal management:

import Mathlib.Tactic.Cases

example (p q : Prop) : (p → ¬ q) → ¬ (p ∧ q) := by
  intro hpnq hpq
  apply hpnq
  cases' hpq with hp hq
  assumption
  -- (kernel) declaration has metavariables '_example'


example (p q : Prop) : (p → ¬ q) → ¬ (p ∧ q) := by
  intro hpnq hpq
  apply hpnq
  cases hpq
  assumption
  cases hpq
  assumption -- succeeds

Focusing on the first subgoals produced by apply makes the error go away, as does using cases instead of cases'. Any ideas what's up here? Unfortunately a student already ran into this about 30 minutes after my first Lean homework dropped :sad:

[Rob Lewis]

I can fix this with a focus at the beginning of the implementation of cases', which seems like it wouldn't hurt, but I'm not sure that's the root cause?

[Heather Macbeth]

(never mind my proposed other example, this seems to just be slow updating in my infoview)

[Rob Lewis]

Reported as mathlib4#2016 so it doesn't get lost

[Mario Carneiro]

Rob Lewis said:

I can fix this with a focus at the beginning of the implementation of cases', which seems like it wouldn't hurt, but I'm not sure that's the root cause?

Yes, that's the root cause. It's a copy/alteration of Lean.Elab.Tactic.evalCases, which uses focus at the start and this was not replicated in the rewrite. A fix is up at !4#2021

[Rob Lewis]

Amazing, thanks! I'm still wrapping my head around Lean 4 goal management. Is there a short explanation for why the focus is needed here, and why withMainContext doesn't have the same effect?

[Mario Carneiro]

withMainContext doesn't do anything with the goal list. It only sets the local context to match the local context of the main goal, so that elabTerm will work correctly. What the focus combinator does is to stash all the goals in the list except for the first and then append them once the inner tactic is done making its modifications. Without that, cases calls getMainGoal at the start (which pulls only the first goal) and setGoals at the end (which drops any trailing goals). An alternative would be to use replaceMainGoal instead of setGoals at the end, which removes the head of the goal list and prepends the provided list of subgoals.

[Mario Carneiro]

Notably, focus is also not a replacement for withMainContext - it does not set the local context so you would need to use both if you need both the goal management behavior and setting the local context.

[Rob Lewis]

Got it. That makes sense, and I see now where this behavior is coming from!