如何将 do 策略应用于序列

Question

深入了解test_nostutter_1 excersize 我找到了一种无需重复即可解决的方法：

Example test_nostutter_1: nostutter [3;1;4;1;5;6].
Proof.
  constructor 3.
  (* This will apply the tactics to the 2-nd subgoal *)
  2: {apply eqb_neq. auto. }
  constructor 3.
  2: {apply eqb_neq. auto. }
  constructor 3.
  2: {apply eqb_neq. auto. }
  constructor 3.
  2: {apply eqb_neq. auto. }
  constructor 2.
Qed.

我决定更多地使用它，在 coq 参考手册中我发现有 do tactical 可以多次循环一个策略。

do num expr

expr 被评估为 v ，它必须是一个策略值。这个策略值 v 被应用了 num 次。假设 num > 1，在第一个之后 v 的应用，v 至少应用一次，到生成的 子目标等等。如果 v 的应用在 已完成 num 个申请。

所以我尝试了这个：

do 4 constructor 3; 2: {apply eqb_neq. auto. }

但不幸的是它失败了。只有这样才有效：

do 1 constructor 3.

是否可以使用 do 使其工作？

Answer 1

回答

一行有几个问题

do 4 constructor 3; 2: {apply eqb_neq. auto. }

首先，不能在链运算符;之后使用2:或{}。你可以使用的最接近的东西是sequence with local applicationtac; [tac1 | tac2]。由于我们只想在第二个分支上做点什么，我们可以在这里省略tac1。

此外，您不能在战术中使用句点。句点标志着语句的结束，但整个do 表达式是一个语句。您应该始终使用序列运算符; 来链接多种策略。

最后，do n tac; tac 像 (do n tac); tac 一样工作。你可以用括号包裹一个策略表达式，例如do n (tac; tac) 改变行为。

所以这个应该可以工作：

do 4 (constructor 3; [ | apply eqb_neq; auto ]).

---

题外话

我们可以通过多种方式简化这条线。

• auto 可以被赋予额外的定理以实现自动化。任何可以用apply eqb_neq; auto 解决的目标也可以用auto using eqb_neq 解决。

do 4 (constructor 3; [ | auto using eqb_neq ]).

• auto 策略永远不会失败，因此它可以安全地用于两个分支。

do 4 (constructor 3; auto using eqb_neq).

• repeat 重复，直到某事失败或没有更多的子目标。以下将重复，直到第三个构造函数不再适用。

repeat (constructor 3; auto using eqb_neq).

• 我们可以让 Coq 选择应用哪个构造函数。这可以完成（或几乎完成）证明。

repeat (constructor; auto using eqb_neq).

• 我们还可以通过auto 使用Hint Constructors 命令使nostutter 的构造函数自动化。现在我们可以auto 整件事了。 （您可以在 nostutter 的定义之后放置提示命令，然后您可以在任何地方使用 auto。）

Hint Constructors nostutter.
auto using eqb_neq.
(* if the above fails, the following increases the search depth so it should succeed. *)
auto 6 using eqb_neq.

• 实际上，定理eqb_neq 已经注册为auto。所以我们可以：

auto 6.