如何在coqide中逐步进行分号分隔的策略序列？

Question

当在coqide中构建证明时，我没有找到方法

T1; T2; T3; ...; Tn.

一种策略一种策略。因此，像上面的代码那样构造正确的证明变得非常困难。所以我的问题是

• 有没有办法逐步浏览上面的代码，或者
• 您如何像上面的代码那样构造证明？

转发一个命令或转到光标均无效。

Answer 1

t1 ; t2是不一样的做第一个t1，然后t2。如果您想这样做，那么可以这样做t1. t2.，这是逐步解决它们的方法。

分号用于三个目的，用于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.

我个人并不一定推荐它，因为由于无法逐步解决问题，它变得更难维护且难以为其他用户阅读。我将限制证明是原则性的两种情况（例如应用构造函数并使用它完成），并诉诸于目标选择器进行因式分解。