4
$\begingroup$

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.
$\endgroup$

1 Answer 1

7
$\begingroup$

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.

$\endgroup$
4
  • $\begingroup$ I am using ssreflect, in the sense that I Require Import ssreflect (and I use other features like => so I'm confident it has some effect). Maybe I should have made that more clear, sorry. I thought I would, as a consequence, always get the ssreflect versions of tactics whenever there was a conflict. Is that not so? And if not, how do I know which I'm in fact invoking? $\endgroup$
    – q.undertow
    Mar 28 at 1:18
  • 1
    $\begingroup$ The confusion arises from the fact that you get both the vanilla tactical written (first [ ... ]) and the ssreflect tactic (written ... ; first ...). That the parser is able to accommodate both surprises me too. $\endgroup$
    – Yves
    Mar 28 at 6:24
  • $\begingroup$ Thanks, Yves. I'm less confused now, but still surprised :-8 $\endgroup$
    – q.undertow
    Mar 28 at 6:29
  • 1
    $\begingroup$ Do you think I should update my answer to clarify this point? $\endgroup$ Mar 28 at 6:32

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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