Remove All Double Negations in Coq

Question

I would like to systematically remove all double negations which can appear in my hypotheses and goals. I know that ~~A -> Ais not a part of intuitionist logic, but the course I am taking is classical, so I don't mind.

I am aware that the mentioned axiom can be accessed by Coq.Logic.Classical_Prop.NNPPbut this axiom doesn't help removing double negation from more complex sentences such as say

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

Preferably I would like to be able to apply a Ltac tactic to Hso it would transform into

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

Any help writing such a tactic or any other suggestions are much appreciated.

Answer 1

You can use the rewrite tactic, because it can rewrite with logical equivalences in logical contexts, i.e. it can do setoid rewriting. First, you'd need the following simple lemma:

From Coq Require Import Classical_Prop.

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

Now, you can use NNP_iff_P to achieve what you want:

Section Example.

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

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

End Example.

! means "rewrite zero or many times, until no rewrites are possible" and in * means "apply the tactic in the context and to the goal".