coq - 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.

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