How to use Cycle / Swap tactics?

Question

Consider the proof code:

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.

Unfortunately, it seems that cycle and swap do not work. Why, and how do I use them correctly?

Answer 1

So, the story is interesting and unintuitive.

A usage of : tac; cycle does work, because ; cycle runs cycle on all goals, which cycles properly.

However, tac. cycle does not. Why?

The reason is that tac. is actually shorthand for "call the current goal selector, and then run tac". The default goal selector is Focus 1.

This causes cycle to try to cycle a list of 1 goal, (the focued goal), which does nothing.

However, in this model, swap 1 2 should produce an error, because we try to swap 1 and 2 from a list of one goal. I raised an issue about this on the coq bug tracker

The solution is to use all: swap or all:cycle. This focuses on all the goals first, which allows swap and cycle to work as expected.

Full code listing:

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 use tactic; swap or all:swap