3

我无法理解multiple successesCoq (8.5p1, ch9.2) 中的分支和回溯行为的概念。例如，从文档中：

回溯分支

我们可以使用以下结构进行分支：

expr1 + expr2

战术可以被看作是有几个成功的。当一个策略失败时，它要求先前策略的更多成功。expr1 + expr2 具有 v1 的所有成功，然后是 v2 的所有成功。

我不明白的是，为什么我们首先需要多次成功？一次成功还不足以完成证明吗？

同样从文档中，似乎有一些成本较低的分支规则以某种方式“有偏见”，包括

first [ expr1 | ::: | exprn ]

和

expr1 || expr2

为什么我们需要更昂贵的选择+而不总是使用后者更有效的战术？

4

1 回答 1

4

问题是你有时试图实现一个目标，但进一步的子目标可能会导致你认为会被拒绝的解决方案。如果你积累了所有的成功，那么你可以回溯到你做出错误选择的地方，并探索搜索树的另一个分支。

这是一个愚蠢的例子。假设我想证明这个目标：

Goal exists m, m = 1.

现在，这是一个相当简单的目标，所以我可以手动完成，但我们不要这样做。让我们编写一个策略，当遇到 时exists，尝试所有可能的自然数。如果我写：

Ltac existNatFrom n :=
  exists n || existNatFrom (S n).

Ltac existNat := existNatFrom O.

然后，一旦我运行existNat，系统就会提交第一个成功的选择。特别是这意味着尽管 , 的递归定义existNatFrom，当调用时existNat我总是得到O并且只有O。

目标无法解决：

Goal exists m, m = 1.
  Fail (existNat; reflexivity).
Abort.

另一方面，如果我使用(+)而不是(||)，我将遍历所有可能的自然数（以一种懒惰的方式，通过使用回溯）。所以写：

Ltac existNatFrom' n :=
  exists n + existNatFrom' (S n).

Ltac existNat' := existNatFrom' O.

意味着我现在可以证明目标：

Goal exists m, m = 1.
  existNat'; reflexivity.
Qed.
于 2016-07-08T10:08:17.677 回答