删除 Coq 中的所有双重否定
Remove All Double Negations in Coq
我想系统地删除所有可能出现在我的假设和目标中的双重否定。我知道~~A -> A不是直觉主义逻辑的一部分，但我上的课程是经典的，所以我不介意。
我知道提到的公理可以通过 Coq.Logic.Classical_Prop.NNPP 访问，但是这个公理无助于从更复杂的句子中删除双重否定，例如 say
H : ~ ~ A \/ (B /\ ~ C)
我希望能够将 Ltac 策略应用于 H，这样它就会转变为
H1 : A \/ (B /\ ~C)。
非常感谢任何编写此类策略或任何其他建议的帮助。
你可以使用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.
! 表示 "rewrite zero or many times, until no rewrites are possible"，in * 表示 "apply the tactic in the context and to the goal"。
我想系统地删除所有可能出现在我的假设和目标中的双重否定。我知道~~A -> A不是直觉主义逻辑的一部分，但我上的课程是经典的，所以我不介意。
我知道提到的公理可以通过 Coq.Logic.Classical_Prop.NNPP 访问，但是这个公理无助于从更复杂的句子中删除双重否定，例如 say
H : ~ ~ A \/ (B /\ ~ C)
我希望能够将 Ltac 策略应用于 H，这样它就会转变为
H1 : A \/ (B /\ ~C)。
非常感谢任何编写此类策略或任何其他建议的帮助。
你可以使用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.
! 表示 "rewrite zero or many times, until no rewrites are possible"，in * 表示 "apply the tactic in the context and to the goal"。