是否可以切换当前目标或子目标来在 Coq 中进行证明?
例如,我有一个这样的目标(来自 eexists):
______________________________________(1/1)
?s > 0 /\ r1 * (r1 + s1) + ?s = r3 * (r3 + s2)
我想做的是split
并首先证明正确的连接。我认为这将给出存在变量的值?s
,并且左合取应该只是一个简化。
But 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)。
本文内容由网友自发贡献,版权归原作者所有,本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容,请联系:hwhale#tublm.com(使用前将#替换为@)