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

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

coq-tactic coq

1

Siddharth Bhat · 技术社区 · 8 年前

考虑证明代码:

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 回复 | 直到 8 年前

1

3

Siddharth Bhat 8 年前

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

用法: 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