是否可以切换当前目标或子目标以在 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) 如果它在不同的上下文中，goal#2 可能是第三个或第 k_th 个目标。证明不会是便携式的。
这就是为什么我想将第二个目标设置为当前目标。
顺便说一句，我正在使用 CoqIDE (8.5)。