Coq 分支和回溯的多次成功？

Question

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

Backtracking branching

We can branch with the following structure:

expr1 + expr2

Tactics can be seen as having several successes. When a tactic fails it asks for more successes of the prior tactics. expr1 + expr2 has all the successes of v1 followed by all the successes of v2.

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

另外从文档中可以看出，似乎有一些成本较低的分支规则 "biased"，包括

first [ expr1 | ::: | exprn ]

和

expr1 || expr2

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

Answer 1

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

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

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.

Coq 分支和回溯的多次成功？

multiple successes in Coq branching and backtracking?

coq

coq-tactic