Как правильно использовать локальную тактику Coq?

Я читаю справочное руководство Coq (8.5p1) о

Локальное применение тактики

Разные тактики можно применять к разным целям, используя следующую форму:

[> expr1 | ::: | exprn]

Выражения expri оцениваются как vi для i = 0; ...; п и все должно быть тактикой. Vi применяется к i-й цели для = 1; ...; п. Это не удается, если количество целевых целей не равно n.

Итак, я провел небольшой тест с двумя целями, пытаясь применить к каждой по две тривиальных idtac тактики, а именно:

Goal forall P Q: Prop, P \/ Q -> Q \/ P.
intros. destruct H. [ >  idtac | idtac  ].

Однако я получил сообщение об ошибке, в котором говорилось, что ожидается только одна тактика:

Ошибка: неправильное количество голов (ожидается 1 тактика).

Я смущен. Может кто-нибудь объяснить, что я сделал не так и как правильно использовать?


coq coq-tactic
person tinlyx    schedule 07.07.2016    source источник

Ответы (1)


arrow_upward
2
arrow_downward

Ключевой частью здесь является

Это не удается, если количество сфокусированных целей не равно n.

Вам нужны 2 целенаправленные цели. Количество целевых целей можно проверить так:

Ltac print_numgoals := let n := numgoals in idtac "# of goals:" n.

Goal forall P Q: Prop, P \/ Q -> Q \/ P.
  intros. destruct H.
  print_numgoals.  (* prints 1 *)

Есть несколько способов достичь нескольких конкретных целей:

(1) Использование последовательности: destruct H; [> idtac | idtac].

(2) Или немного короче: destruct H; [> idtac ..].

(3) С помощью селектора all (см. руководство, §8.1):

destruct H. all: [ > id_tac | id_tac ].

В последнем случае destruct H. all: print_numgoals. печатает 2.

В заключение следует упомянуть следующее - похоже, что локальное применение тактики в этой точной форме ([ > ...]) не очень полезно, потому что оно никогда не используется в стандартной библиотеке (и некоторых других библиотеках). ) и в инструкции об этом нет никаких упоминаний, кроме раздела, посвященного этой функции. Его вариант формы expr; [ expr_1 | ... | expr_n] кажется наиболее полезным.

person Anton Trunov    schedule 07.07.2016