3
$\begingroup$

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!

$\endgroup$
2
  • $\begingroup$ It’s best to give a minimal working example which produces this error, that someone can just plug into Coq. Or in your case you can point to the location in software foundations (and provide your partial proof). Also is this homework? $\endgroup$
    – Jason Rute
    Jul 31, 2023 at 16:35
  • $\begingroup$ It's not my homework, but I do believe the textbook is used in certain unis for class $\endgroup$
    – noCrayCray
    Jul 31, 2023 at 16:38

1 Answer 1

1
$\begingroup$

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.

$\endgroup$
1
  • 1
    $\begingroup$ Any chance we could rename the lemma? It's a bit French. $\endgroup$ Sep 1, 2023 at 6:15

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.