如何在Coq中切换当前目标？

是否可以切换当前目标或子目标以在Coq中证明？

例如,我有一个这样的目标(来自eexists):

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

我想要做的是首先split证明合适的合并.我认为这将给出存在变量的值?s,而左合并应该只是一个简化.

但split默认情况下,将左合并设置?s > 0为当前目标.

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

我知道我可以在战术2:上加上第二个子目标的操作,但这很尴尬因为

1)我看不到目标#2和.的假设

2)如果它处于不同的上下文中,目标#2可能是第三个或第k个目标.证明不可移植.

这就是为什么我想把第二个目标设定为当前目标.

顺便说一下,我正在使用CoqIDE(8.5).

您可以Focus 2专注于第二个目标.