是否可以切换当前目标或子目标以在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).