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.
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".