Как использовать тактику Cycle / Swap? - PullRequest
Новая
       8

Как использовать тактику Cycle / Swap?

0 голосов
/ 27 июня 2018

Рассмотрим код подтверждения: 

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 Ответ

0 голосов
/ 27 июня 2018

Итак, история интересная и не интуитивная.

Использование: tac; cycle действительно работает, потому что ; cycle выполняет cycle на всех целях, которые циклически корректны.

Однако tac. cycle нет. Почему?

Причина в том, что tac. на самом деле является сокращением для "вызова текущего селектора целей , а затем запуска tac". Селектор целей по умолчанию - Focus 1.

Это приводит к тому, что cycle пытается циклично перебрать список из 1 цели (целевой цели), которая ничего не делает.

Однако в этой модели swap 1 2 должен выдавать ошибку, потому что мы пытаемся поменять 1 и 2 из списка одной цели. Я поднял вопрос об этом на coq баг-трекере

Решение заключается в использовании 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

...