Изменение порядка целей (Изабель)

Question

Я хотел бы знать, как изменить порядок целей в следующей ситуации:

lemma "P=Q"
  proof (rule iffI, (*here I would like to swap goal order*), rule ccontr)
oops

Я хотел бы решение, которое не включает в себя изменение утверждения леммы. Я понимаю что prefer а также defer может быть использован в доказательствах в стиле применения, но я хотел бы иметь метод, который может быть использован в proof (...) часть.

Редактировать:

Как говорит Андреас Лохбихлер, пишущий rule iffI[rotated] работает в приведенном выше примере. Однако возможно ли поменять порядок ворот в следующей ситуации, не меняя формулировку леммы?

lemma "P==>Q" "Q==>P"
  proof ((*here I would like to swap goal order*), rule ccontr)
oops

Этот пример может показаться надуманным, но я чувствую, что могут возникнуть ситуации, когда неудобно менять формулировку леммы или необходимо поменять порядок целей, если ранее не применялось правило, такое как iffI,

Answer 1

Порядок подцелей определяется порядком допущений правила, которое вы применяете. Так что достаточно поменять предположения iffI правило, например, используя атрибут [rotated] как в

proof(rule iffI[rotated], rule ccontr)

В общем, нет способа доказательства, чтобы изменить порядок целей. И если вы думаете об использовании этого с более сложной автоматизацией доказательства как autoЯ бы настоятельно советовал вам не делать подобные вещи. Скрипты проверки с большой автоматизацией должны работать независимо от порядка целей. В противном случае ваши доказательства легко сломаются, если что-то из настроек автоматизации проверки изменится.

Тем не менее, несколько низкоуровневых доказательств позволяют использовать явную адресацию цели (в основном те, которые заканчиваются _tac). Например,

proof(rule iffI, rule_tac [2] ccontr)

применяет ccontr Правило второй подцели вместо первого.