代码之家 › 专栏 › 技术社区 › Siddharth Bhat

如何使用循环/交换策略?

coq-tactic coq

Siddharth Bhat · 技术社区 · 7 年前

考虑证明代码:

Definition f (a: nat): nat.
Proof.
Admitted.



Lemma rew: forall (a p : nat) (A: a + 1 = p),
    f a = f p.
Proof.
Admitted.

Lemma userew: forall (a b: nat), f a = f b.
Proof.
  intros.
  erewrite rew.
  cycle 1.
  (* Goal does not cycle *)
  swap 1 2.
  (* Goal does not swap *)
Abort.

不幸的是,看起来 cycle 和 swap 不要工作。为什么,如何正确使用它们?

1 回复 | 直到 7 年前

Siddharth Bhat 7 年前

所以,这个故事很有趣,也不具有说服力。

用法: tac; cycle 做工作,因为 ; cycle 跑 cycle 在 全部的 正确循环的目标。

然而, tac. cycle 没有。为什么?

原因是 tac. 实际上是“呼叫当前 goal selector ,然后运行 tac “。默认目标选择器为 Focus 1 .

这导致了 周期 试着循环一个目标列表,(聚焦目标),它什么都不做。

然而,在这个模型中, swap 1 2 应该会产生一个错误,因为我们试图交换 1 和 2 从一个目标的列表中。 I raised an issue about this on the coq bug tracker

解决方案是使用 all: swap 或 all:cycle .这首先关注所有的目标,这使得 swap 和 周期 按预期工作。

完整代码列表:

Definition f (a: nat): nat.
Proof.
Admitted.

Lemma rew: forall (a p : nat) (A: a + 1 = p),
    f a = f p.
Proof.
Admitted.

Lemma userew: forall (a b: nat), f a = f b.
Proof.
  intros.
  erewrite rew.
  (* NOTICE all: *)
  all: cycle 1.
  (* NOTICE all: *)
  all: swap 1 2.
Abort.

TL;医生 使用 tactic; swap 或 all:swap

推荐文章

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

7 年前

Lorenz · Coq强制和目标匹配

8 年前

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

8 年前

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

8 年前

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

8 年前

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

8 年前

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

9 年前

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

9 年前