coq - Coq Qed 战术被挂了

Question

我证明了一个引理（证明完成），但是当我使用 Qed 保存它时，系统变得很忙。在同一个文件中，还有其他类似的引理，其中 Qed 执行正常，除了这个。任何机构都可以教我它的解决方案吗？

谢谢，

维拉亚特

Answer 1

如果不知道您正在处理哪个特定示例，就很难说。每当您输入QedCoq 时，内核都会分析您的策略产生的证明，并确保它确实有效；战术引擎本身实际上并没有执行很多检查。因此，即使您的有问题的证明与其他证明略有不同，也可能导致它产生了一个非常大的证明项，这使得内核需要很长时间。