当在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/

    10-09 15:22
    查看更多