logic - 删除 Coq 中的所有双重否定

Question

我想系统地删除所有可能出现在我的假设和目标中的双重否定。我知道这~~A -> A不是直觉主义逻辑的一部分，但我所学的课程是经典的，所以我不介意。

我知道可以访问提到的公理，Coq.Logic.Classical_Prop.NNPP但是这个公理无助于从更复杂的句子中消除双重否定，例如说

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

最好我希望能够应用 Ltac 策略，H这样它就会变成

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

非常感谢编写此类策略的任何帮助或任何其他建议。

Answer 1

您可以使用该rewrite策略，因为它可以在逻辑上下文中使用逻辑等价进行重写，即它可以进行 setoid 重写。首先，您需要以下简单的引理：

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 *意思是“将策略应用于上下文和目标”。