1

我正在阅读 Coq 参考手册 (8.5p1) 关于

战术的局部应用

可以使用以下形式将不同的策略应用于不同的目标：

[ > expr1 | ::: | 解释]

表达式expri被计算为 vi，因为 i = 0；...; n 一切都必须是战术。vi 应用于第 i 个目标，对于 = 1；...; n. 如果重点目标的数量不完全是 n，它就会失败。

所以我做了一个小测试，有两个目标，试图对idtac每个目标应用两种微不足道的策略，如下所示：

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

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

错误：进球数不正确（预期为 1 个战术）。

我很困惑。有人可以解释我做错了什么，正确的用法是什么？

4

1 回答 1

2

这里的关键部分是

如果重点目标的数量不完全是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]似乎是最有用的。

于 2016-07-07T09:55:50.730 回答