当在coqide中构建证明时,我没有找到方法
T1; T2; T3; ...; Tn.
一种策略一种策略。因此,像上面的代码一样,构造正确证明变得非常困难。所以我的问题是
转发一个命令或转到光标均无效。
最佳答案
t1 ; t2
与首先执行t1
然后执行t2
不同。
如果要执行此操作,可以执行t1. t2.
,这是逐步解决它们的方法。
分号有3个用途,针对t1 ; t2
进行了说明:
t2
生成的所有子目标中应用t1
; t2
失败,它将为t1
尝试不同的成功,然后在生成的子目标上再次应用t2
; 如果您很幸运,这是第一种或第三种情况,那么您可以通过替换以下内容来修改脚本
t1 ; t2
经过
t1. all: t2.
使用目标选择器。
这样,第一步将允许您查看
t1
生成的目标,第二步将显示t2
如何影响目标。如果需要更高的精度,还可以集中关注其中一个子目标,以查看t2
的实际使用情况。当涉及回溯时,要了解正在发生的事情变得更加困难,但是我相信可以一开始就避免它,或者将其限制在简单的情况下。
例如,您可以说可以通过应用引入规则(
constructor
)来实现目标,然后这应该很容易。如果有多个入门规则/构造方法适用
constructor. easy.
可能会导致失败,而
constructor ; easy.
可能会成功。实际上,如果
easy
在第一个构造函数上失败,则coq将尝试第二个构造函数,依此类推。为了回答您有关如何编写它们的问题,我想这可能是反复试验的结果,并且大部分可能来自证明脚本的分解或自动化。
假设您具有以下证明脚本:
split.
- constructor.
+ assumption.
+ eassumption.
- constructor. eassumption.
您可能要总结如下:
split ; constructor ; eassumption.
我个人并不一定推荐它,因为由于无法逐步解决问题,它变得难以维护,也难以为其他用户阅读。
我将限制证明是原则性的这两种情况(例如应用构造函数并由其完成),并诉诸于目标选择器进行因式分解。
关于coq - 如何在coqide中逐步进行分号分隔的策略序列?,我们在Stack Overflow上找到一个类似的问题:https://stackoverflow.com/questions/58021053/