by_cases tags bug

Stream: std4

[Marcus Rossel]

When using Std's by_cases tactic, all goals' tags are overwritten to be called just pos or neg. E.g:

import Std

example : True := by
  by_cases 1 = 2 <;> by_cases 2 = 3

/-
case pos
h✝¹: 1 = 2
h✝: 2 = 3
⊢ True
case neg
h✝¹: 1 = 2
h✝: ¬2 = 3
⊢ True
case pos
h✝¹: ¬1 = 2
h✝: 2 = 3
⊢ True
case neg
h✝¹: ¬1 = 2
h✝: ¬2 = 3
⊢ True
-/

Is this a bug?

[Adrien Champion]

It doesn't look ideal :confused: It seems the problem has to do with refine which introduces sub-goals for the holes in the term it is given (see here)

macro_rules
  | `(tactic| by_cases $h : $e) =>
    `(tactic| open Classical in refine if $h:ident : $e then ?pos else ?neg)

[Adrien Champion]

As a test, changing the last line to `(tactic| open Classical in exact if $h:ident : $e then ?pos else ?neg) yields the sub-goal names expected

[Adrien Champion]

It seems like pushing refine down the if-then-else's branches helps, though someone actually qualified will have to weigh in, this "works" for sub-case names but might be nonsensical for what by_cases is going for:

macro_rules
  | `(tactic| by_cases $h : $e) =>
    `(tactic| open Classical in
      let cnd := refine $e
      let thn := refine ?pos
      let els := refine ?neg
      exact if $h:ident : cnd then thn else els
    )