0

深入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 应用到生成的子目标，依此类推。如果在 num 个应用程序完成之前 v 的应用程序失败，它就会失败。

所以我尝试了这个：

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

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

do 1 constructor 3.

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

4

1 回答 1

2

回答

线路有几个问题

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

首先，你不能在链运算符之后使用2:or 。您可以使用的最接近的东西是带有本地应用程序的序列。由于我们只想在第二个分支上做一些事情，我们可以在这里省略。{}; tac; [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).
  • 我们还可以使用命令使构造函数nostutter自动化。现在我们可以整件事了。（你可以在你的定义之后放置提示命令，然后你可以在任何地方使用它。）autoHint Constructorsautonostutterauto
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.
于 2019-06-27T23:59:10.893 回答