Разъединение Commutavity в Coq - PullRequest
Новая
       88

Разъединение Commutavity в Coq

0 голосов
/ 24 октября 2018

Я хотел бы иметь тактику Ltac, которая выполняет работу Disjunction Commutavity.Главным образом, если у меня есть гипотеза P \/ Q где-то в гипотезе H, Ltac Com H добавит Q \/ P в качестве другой гипотезы к контексту.

Я попытался поставить правило коммуникативности через аксиому и apply it;но это работает только для простых гипотез, например, терпит неудачу в R -> (P \/ Q);где следует добавить в контекст R -> (Q \/ P).

1 Ответ

0 голосов
/ 24 октября 2018

Вы можете использовать библиотеку переписывания setoid, которая позволяет переписывать с отношениями, отличными от равенства.Следующий фрагмент показывает, как заменить A \/ B на B \/ A в гипотезе: 

Require Import Setoid.

Variables A B C : Prop.

Goal ~ (A \/ B -> C).
intros H.
rewrite or_comm in H.
Abort.

Чтобы реализовать желаемую тактику, нам просто нужно продублировать гипотезу и переписать ее.Обратите внимание на использование тактики fresh, которая генерирует новое имя гипотезы. 

Ltac Comm H :=
  let H' := fresh "H" in
  pose proof H as H';
  rewrite or_comm in H'.

Вот демонстрация Comm в действии. 

Goal ~ (A \/ B -> C).
intros H.
Comm H.
Abort.

Редактировать В руководстве Coq есть раздел о переписывании сетоидов.Грубо говоря, вы можете переписать с помощью любое отношение R в гипотезе, при условии, что вы докажете, что операции, которые появляются в этой гипотезе, совместимы с отношением.Например, если мы примем R за <->, вышеуказанное переписывание работает, потому что в стандартной библиотеке есть леммы, показывающие, что логическая эквивалентность соблюдается косвенно.

Примечание Я бы вообще рекомендовал не допускать, чтобы Coq называл гипотезы сами по себе: эти имена, как правило, довольно нестабильны, что часто приводит к поломке сценариев проверки.Как правило, вы должны позволить Coq выбирать имена самостоятельно, если вы пишете полностью автоматизированные сценарии проверки, которые никогда не ссылаются на автоматически выбранные имена.Вот еще одна версия Comm, которая позволяет избежать этой проблемы. 

Ltac Comm' H H' :=
  pose proof H as H';
  rewrite or_comm in H'.

Goal ~ (A \/ B -> C).
intros H.
Comm H H'.
Abort.
...