Удалить все двойные отрицания в Coq

Question

Я хотел бы систематически убрать все двойные отрицания, которые могут появиться в моих гипотезах и целях. Я знаю, что ~~A -> A не является частью интуиционистской логики, но курс, который я выбираю, является классическим, поэтому я не против.

Мне известно, что к упомянутой аксиоме может обратиться Coq.Logic.Classical_Prop.NNPP, но эта аксиома не помогает убрать двойное отрицание из более сложных предложений, таких как, скажем,

H : ~ ~ A \/ (B /\ ~ C)

Предпочтительно я хотел бы иметь возможность применить тактику Ltac к H, чтобы она трансформировалась в

H1 : A \/ (B /\ ~C).

Любая помощь в написании такой тактики или любые другие предложения приветствуются.

Answer 1

Вы можете использовать тактику rewrite, потому что она может перезаписывать с логическими эквивалентами в логических контекстах, то есть она может выполнять переписывание сетоидов. Во-первых, вам понадобится следующая простая лемма:

From Coq Require Import Classical_Prop.

Lemma NNP_iff_P (P : Prop) : ~~ P <-> P.
Proof. split; [apply NNPP | intuition]. Qed.

Теперь вы можете использовать NNP_iff_P для достижения того, что вы хотите:

Section Example.

Context (A B C D : Prop).
Context (H : ~ ~ A \/ (B /\ ~ C)).

Goal ~~ A.
rewrite !NNP_iff_P in *.
Abort.

End Example.

! означает «переписать ноль или много раз, пока перезапись невозможна», а in * означает «применить тактику в контексте и к цели».