# Completely confused by a trivial SSR proof with case

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

`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.

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.

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.