Удалить все двойные отрицания в 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 * означает "применять тактику в контексте и к цели".