How to switch the current goal in Coq?

Question

Is it possible to switch the current goal or subgoal to prove in Coq?

For example, I have a goal like this (from an eexists):

______________________________________(1/1)
?s > 0 /\ r1 * (r1 + s1) + ?s = r3 * (r3 + s2)

What I want to do is to split and prove the right conjunct first. This I think will give the value of the existential variable ?s, and the left conjunct should be just a simplification away.

But split by default set the left conjunct ?s > 0 as the current goal.

______________________________________(1/2)
?s > 0
______________________________________(2/2)
r1 * (r1 + s1) + ?s = r3 * (r3 + s2)

I know I can prefix tactics with 2: to operate on the second subgoal, but it's awkward because

1) I can't see the hypotheses for goal#2 and

2) if it's in a different context, goal#2 might be the third or the k_th goal. The proof won't be portable.

That's why I want to set the second goal as the current.

BTW, I am using CoqIDE (8.5).

Anosmia

fyi, The Focus command is deprecated; use '2: {' instead [deprecated-focus,deprecated] – Furnish

Answer 1

You can use Focus 2 to focus on the second goal.

Crowley

The Focus command is deprecated; use '2: {' instead [deprecated-focus,deprecated] – Furnish

Answer 2

Update from 2021: use 2:.

Focus 2 is deprecated at least since 8.13:

The Focus command is deprecated; use '2: {' instead [deprecated-focus,deprecated]

Sokol

sorry what is the command we need to use? – Furnish

@CharlieParker you actually write 2: { as a "tactic". – Foreshank