如何在coqide中通过分号分离的战术序列？

Question

在coqide中构造证明时，我没有找到一种方法

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

一个接一个的战术。因此，很难像上面的代码那样构造正确的证明。所以我的问题是

• 是否有一种方法可以通过上面的代码或
• ，如何像上面的代码那样构造证明呢？

转发一条命令或转到游标不起作用。

Answer 1

t1 ; t2不同于首先执行t1，然后执行t2。如果你想这样做，你可以做t1. t2.，这是通过它们的方式。

分号有三个用途，用于t1 ; t2

它在t1;

• and生成的所有子目标中应用t2，它允许回溯，如果t2失败，它将为t1尝试一个不同的成功，并再次在生成的subgoals;

• third，上应用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.

我个人不一定推荐它，因为它变得更难维护和其他用户更难阅读，因为问题是无法通过。我会将其限制在证明是有原则的情况下(比如应用构造函数并完成它)，并使用目标选择器进行分解。