如何使用循环/掉期策略？

Question

考虑证明代码：

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 似乎不起作用。为什么以及如何正确使用它们？

Answer 1

所以，这个故事很有趣但不直观。

tac; cycle 的用法，因为 ; cycle 在 all 上运行 cycle ] 目标，正确循环。

然而，tac. cycle 没有。为什么？

原因是 tac. 对于 "call the current goal selector, and then run tac" 实际上是 shorthand。默认目标选择器是 Focus 1.

这会导致 cycle 尝试循环包含 1 个目标（重点目标）的列表，这什么都不做。

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

解决方案是使用all: swap或all:cycle。这首先关注所有目标，这允许 swap 和 cycle 按预期工作。

完整代码清单：

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;DR 使用 tactic; swap 或 all:swap

如何使用循环/掉期策略？

How to use Cycle / Swap tactics?

coq

coq-tactic