代码之家 › 专栏 › 技术社区 › thor BabarQB

Coq“局部战术应用”的正确用法是什么?

coq-tactic coq

thor BabarQB · 技术社区 · 8 年前

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

战术的局部应用

使用以下表格:

表达式 expri i=0时计算为vi。。。;n和所有必须是战术。vi适用于第i个目标,=1。。。; n、如果集中目标的数量不完全是n,那么它就失败了。

因此,我做了一个小测试,有两个目标,试图应用两个微不足道的 idtac 策略,如下所示:

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

然而,我错误地告诉我,只需要一种策略:

错误:目标数不正确(应为1个战术)。

我很困惑。有人能解释我做错了什么吗?正确的用法是什么?

1 回复 | 直到 8 年前

Anton Trunov 8 年前

这里的关键部分是

聚焦目标并不确切 n .

你需要两个目标。可以这样检查重点目标的数量:

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]

推荐文章

Jian Wang · elim在Coq中是如何工作的?

7 年前

Lorenz · Coq强制和目标匹配

7 年前

Carl Patenaude Poulin · 证明共自然数的共归纳原理

7 年前

user285827 · 如何利用Coq中包含forall的假设?

7 年前

Carl Patenaude Poulin · 问:为什么我需要手动展开一个值,即使它上面有一个“提示展开”?

7 年前

scubed · 如何在每次调用函数时选择性地简化参数,而不计算函数本身?

8 年前

thor BabarQB · Coq“局部战术应用”的正确用法是什么?

8 年前

Sara · 如何在Coq中使用带有假设的策略?

8 年前