Completely confused by a trivial SSR proof with case

Using Coq
1

Given this:

Inductive color := Black | White.

  Inductive point_state :=
  | Occupied of color
  | Empty
  .

this works:


Fact ps_case (ps: point_state):
  ps = Occupied White ∨ ps = Occupied Black ∨ ps = Empty.
  Proof.
    case: ps => [c|].
    - by case: c; auto.
    - by auto.
  Qed.

but this doesn’t (it complains “no applicable tactic”):

Fact ps_case (ps: point_state):
  ps = Occupied White ∨ ps = Occupied Black ∨ ps = Empty.
  Proof.
    case: ps => [c|]; first [case: c; auto].

Why? By my (clearly flawed) reading of the manual, the two should be completely equivalent. In fact I didn’t expect to need the “auto” there either, but we can leave that for the next question.

Update: now also on Stack Exchange, as

2

case: ps => [c|]; first (case: c; auto). works as you seem to expect; case: ps => [c|]; first case: c; auto. applies case: c only to the first goal, and applies auto to both — solving everything.

We can also solve that goal via

case: ps => [c|]; first [by auto|case: c; by auto].

because first [ a | b | c ] is a different tactical — it basically applies the first of a, b and c that succeeds; and as usual for standard a; b, it applies to all goals.

3

How does Coq know which is which? I thought that by Requiring ssreflect I’d always get their versions of tactics when there was a conflict.

4

Yes and no. You will indeed get Ssreflect’s ones in case of conflict. But here there is no conflict. One of the tactic is first while the other is first []. The square bracket disambiguates them.

By the way, if first had overwritten first [], you would have gotten a completely different error message, e.g., Syntax error: [ssrfoo] expected after 'first', since Coq would have choked on the unexpected square bracket.