Coq "local application of tactics" 的正确用法是什么？

Question

我正在阅读关于

的 Coq 参考手册 (8.5p1)

Local application of tactics

Different tactics can be applied to the different goals using the following form:

[ > expr1 | ::: | exprn ]

The expressions expri are evaluated to vi, for i = 0; ...; n and all have to be tactics. The vi is applied to the i-th goal, for = 1; ...; n. It fails if the number of focused goals is not exactly n.

所以我做了一个带有两个目标的小测试，试图对每个目标应用两个琐碎的 idtac 策略，如下所示：

Goal forall P Q: Prop, P \/ Q -> Q \/ P.
intros. destruct H. [ >  idtac | idtac  ].

但是，我收到一条错误消息，告诉我只需要一种策略：

Error: Incorrect number of goals (expected 1 tactic).

我很困惑。谁能解释一下我做错了什么，正确的用法是什么？

Answer 1

这里的关键部分是

It fails if the number of focused goals is not exactly n.

您需要 2 个重点目标。关注目标的数量可以这样查看：

Ltac print_numgoals := let n := numgoals in idtac "# of goals:" n.

Goal forall P Q: Prop, P \/ Q -> Q \/ P.
  intros. destruct H.
  print_numgoals.  (* prints 1 *)

有多种方法可以实现多个集中目标：

(1) 使用排序：destruct H; [> idtac | idtac].

(2) 或者稍微短一些：destruct H; [> idtac ..].

(3) 使用 all 选择器（参见手册，§8.1）：

destruct H. all: [ > id_tac | id_tac ].

在最后一种情况下，destruct H. all: print_numgoals. 打印 2。

总而言之，应该提到以下内容——似乎 精确形式 ([ > ...]) 中的策略的局部应用不是很有用，因为它从未在标准库（和其他几个库）中使用过，手册中也没有提及它，除了专门介绍此功能的部分。它的 expr; [ expr_1 | ... | expr_n] 形式的版本似乎是最有用的。

Coq "local application of tactics" 的正确用法是什么？

what's the correct usage for Coq "local application of tactics"?

coq

coq-tactic