"Expected a single focused goal but 2 goals are focused." error in coq regarding string equality(I think)

Question

I'm working through Software Foundations, I'm at "Maps" right now. There's an exercise:

Lemma t_update_eq : forall (A : Type) (m : total_map A) x v,
  (x !-> v ; m) x = v.
Proof.

I introduce the variables, unfold and destruct (x =? x)%string:

Proof.
   intros. unfold t_update. destruct ((x =? x)%string).

and after that point anything I do generates the error "Expected a single focused goal but 2 goals are focused."

I also tried working on (x =? x)%string by itself in a separate lemma, which again led to that error.

Lemma fuCK : forall x,
(x =? x)%string = true.
Proof.
intros. destruct ((x =? x)%string ) eqn:E. Abort.

What am I missing?

Tia!

Answer 1

Does Software Foundation use Set Default Goal Selector "!".? This commands means that any tactic will fail if there is not exactly one goal under focus. To avoid the error, you can either use goal selectors for a single tactic, or focus on a specific goal using either braces or bullets. Here is a complete proof of your lemma that demonstrates the usage of all of these features.

Lemma string_reflb : forall x,
(x =? x)%string = true.
Proof.
intros. destruct ((x =? x)%string ) eqn:E.
- reflexivity.
- exfalso.
  induction x as [|a ??] ; cbn in *.
  1: congruence.
  destruct (a =? a)%char eqn:Ea ; cbn in *.
  { eauto. }
  destruct a as [[] [] [] [] [] [] [] []] ; cbn in *.
  all: congruence.
Qed.

The idea behind the various goal selection tools is to make proof scripts more robust, by ensuring that a tactic does not wrongly get applied to an incorrect goal after a change in earlier code. The Default Goal Selector "!". lets one enforce that all proof scripts respect this discipline.