如何在 Coq 中切换当前目标？
How to switch the current goal in 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_th 目标。证明不可移植。
这就是为什么我想将第二个目标设置为当前目标。
顺便说一句，我正在使用 CoqIDE (8.5)。
您可以使用 Focus 2 专注于第二个目标。
2021 年更新：使用 2:。
Focus 2 至少自 8.13 起已弃用：
The Focus command is deprecated; use '2: {' instead [deprecated-focus,deprecated]
是否可以切换当前目标或子目标以在 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_th 目标。证明不可移植。
这就是为什么我想将第二个目标设置为当前目标。
顺便说一句，我正在使用 CoqIDE (8.5)。
您可以使用 Focus 2 专注于第二个目标。
2021 年更新：使用 2:。
Focus 2 至少自 8.13 起已弃用：
The Focus command is deprecated; use '2: {' instead [deprecated-focus,deprecated]