Why does this trivial proof fail with structuring tacticals?

Question

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: the following works, and is definitely an improvement. But I still want to understand why the "first" way fails.

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

Answer 1

If you look at the documentation of first, first [ tac ] will apply tac to all subgoals. This means that in the second goal it also tries to apply case: c ; auto which it cannot because c is not bound in it.

Note that you can provide several options that coq will try one after another and write:

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

which succeeds as well.

You probably confused it with the first tactic from ssreflect which you would use by writing:

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

Notice how the two syntax are slightly different and can coexist at the same time.

This time it would only apply in the first goal, leaving you to prove the second goal.