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

Question

是否可以在 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)。

Answer 1

您可以使用 Focus 2专注于第二个目标。