Double-negation translation involves three logical systems. There's a classical logic and an intuitionistic logic, but the translation is not a part of either of these logics. After all, the translation is a relationship between two different universes of logic; how can it belong to one of them? Instead, these logics need to be constructed as objects inside some other logic (probably one you "believe" in, or is "real"), and then double-negation translation is a theorem of that ambient logic that describes the two inner logics. TL;DR: Double-negation translation is a process/theorem about logic, not within logic.
For this reason, you cannot write double-negation translation as such as a lemma within the logic of Coq. I mean, you could certainly define
Inductive sentence : Set := ... . (* E.g. syntax of FOL *)
Definition NN : sentence -> sentence.
Definition classically_provable : sentence -> Prop.
Definition intuitionistically_provable : sentence -> Prop.
Theorem double_negation_translation (p : sentence) :
classically_provable p <-> intuitionistically_provable (NN p).
but this does not prove anything about Coq. It only proves something about some other logics constructed inside Coq. If you wanted to prove this about Coq, you'd have to do that proof in some "higher" system of logic, which is usually either the informal, natural-language logic I'm using right now, or the language Ltac, the tactic language. Ltac programs are the programs that Coq runs to generate proofs. In particular, you could write two tactics. One, if you give it a term excluded_middle -> P (aka a classical proof of P), will essentially try to root out all the uses of that classicality to produce a new, intuitionistic proof of the double-negation translation of P. The other, given an (intuitionistic) proof of the double-negation translation P, turns it into a classical proof of P (aka it proves excluded_middle -> P). (Note my careful language: I say P but not NN P, only "the double-negation translation of P". That's because, outside of Coq, in natural language or Ltac, we can define what "the double-negation translation of P" is. Within Coq, there is no definable NN : Prop -> Prop for that.)
So, e.g., you can define the translation of propositions like this:
Ltac nn_transl P :=
lazymatch P with
| ?L /\ ?R =>
let L' := nn_transl L in
let R' := nn_transl R in
uconstr:(L' /\ R')
| ?L \/ ?R =>
let L' := nn_transl L in
let R' := nn_transl R in
uconstr:(~(~L' /\ ~R'))
| not ?Q =>
let Q' := nn_transl Q in
uconstr:(~Q')
| ?L -> ?R =>
let L' := nn_transl L in
let R' := nn_transl R in
uconstr:(L' -> R')
| forall t: ?T, @?Q t =>
constr:(
forall t: T,
ltac:(
let Qt := eval hnf in (Q t) in
let Qt' := nn_transl Qt in
exact Qt'))
| exists t: ?T, @?Q t =>
constr:(
~forall t: T,
~ltac:(
let Qt := eval hnf in (Q t) in
let Qt' := nn_transl Qt in
exact Qt'))
| _ => uconstr:(~~P)
end.
Implementing the actual translation of proofs does not seem as easy, but it should be doable. I've implemented the easier direction (double negation to classical):
Definition excluded_middle : Prop := forall x, x \/ ~x.
Tactic Notation "assert" "double" "negative" constr(P) "as" ident(H) :=
let P' := nn_transl P in
assert (H : P').
Ltac int_to_nn_class_gen' nn_int_to_class_gen P :=
let x := fresh "x" in
let excl := fresh "excl" in
lazymatch P with
| ?L /\ ?R =>
let xl := fresh x "_l" in
let xr := fresh x "_r" in
let rec_L := int_to_nn_class_gen' nn_int_to_class_gen L in
let rec_R := int_to_nn_class_gen' nn_int_to_class_gen R in
uconstr:(
fun (x : P) (excl : excluded_middle) =>
let (xl, xr) := x in
conj (rec_L xl excl) (rec_R xr excl))
| ?L \/ ?R =>
let L' := nn_transl L in
let R' := nn_transl R in
let arg := fresh x "_arg" in
let arg_l := fresh arg "_l" in
let arg_r := fresh arg "_r" in
let rec_L := int_to_nn_class_gen' nn_int_to_class_gen L in
let rec_R := int_to_nn_class_gen' nn_int_to_class_gen R in
uconstr:(
fun (x : P) (excl : excluded_middle) (arg : ~L' /\ ~R') =>
let (arg_l, arg_r) := arg in
match x with
| or_introl x => arg (rec_L x excl)
| or_intror x => arg (rec_R x excl)
end)
| not ?Q =>
let Q' := nn_transl Q in
let arg := fresh x "_arg" in
let rec_Q := nn_int_to_class_gen Q in
uconstr:(
fun (x : P) (excl : excluded_middle) (arg : Q') => x (rec_Q arg excl))
| ?L -> ?R =>
let L' := nn_transl L in
let arg := fresh x "_arg" in
let rec_L := nn_int_to_class_gen L in
let rec_R := int_to_nn_class_gen' nn_int_to_class_gen R in
uconstr:(
fun (x : P) (excl : excluded_middle) (arg : L') =>
rec_R (x (rec_L arg excl)) excl)
| forall t: ?T, @?Q t =>
constr:(
fun (x : P) (excl : excluded_middle) (t : T) =>
ltac:(
let Qt := eval hnf in (Q t) in
let rec_Qt := int_to_nn_class_gen' nn_int_to_class_gen Qt in
exact (rec_Qt (x t) excl)))
| exists t: ?T, @?Q t =>
let arg := fresh x "_arg" in
let wit := fresh x "_wit" in
constr:(
fun
(x : P) (excl : excluded_middle)
(arg :
forall t: T,
ltac:(
let Qt := eval hnf in (Q t) in
let Qt' := nn_transl Qt in
exact (~Qt'))) =>
match x with ex_intro _ t wit =>
ltac:(
let Qt := eval hnf in (Q t) in
let rec_Qt := int_to_nn_class_gen' nn_int_to_class_gen Qt in
exact (arg t (rec_Qt wit excl)))
end)
| _ =>
let arg := fresh x "_arg" in
uconstr:(fun (x : P) (excl : excluded_middle) (arg : ~P) => arg x)
end.
Ltac nn_int_to_class_gen' int_to_nn_class_gen P :=
let NNP := nn_transl P in
let nnx := fresh "nnx" in
let excl := fresh "excl" in
lazymatch P with
| ?L /\ ?R =>
let nnl := fresh nnx "_l" in
let nnr := fresh nnx "_r" in
let rec_L := nn_int_to_class_gen' int_to_nn_class_gen L in
let rec_R := nn_int_to_class_gen' int_to_nn_class_gen R in
uconstr:(
fun (nnx : NNP) (excl : excluded_middle) =>
let (nnl, nnr) := nnx in
conj (rec_L nnl excl) (rec_R nnr excl))
| ?L \/ ?R =>
let L' := nn_transl L in
let R' := nn_transl R in
let prf := fresh nnx "_prf" in
let arg := fresh nnx "_arg" in
let arg_l := fresh arg "_l" in
let arg_r := fresh arg "_r" in
let rec_L := nn_int_to_class_gen' int_to_nn_class_gen L in
let rec_R := nn_int_to_class_gen' int_to_nn_class_gen R in
uconstr:(
fun (nnx : NNP) (excl : excluded_middle) =>
match excl P with
| or_introl prf => prf
| or_intror prf =>
nnx (conj
(fun arg : L' => prf (or_introl (rec_L arg)))
(fun arg : R' => prf (or_intror (rec_R arg))))
end)
| not ?Q =>
let arg := fresh nnx "_arg" in
let rec_Q := int_to_nn_class_gen Q in
uconstr:(
fun (nnx : NNP) (excl : excluded_middle) (arg : Q) =>
nnx (rec_Q arg excl))
| ?L -> ?R =>
let arg := fresh nnx "_arg" in
let rec_L := int_to_nn_class_gen L in
let rec_R := nn_int_to_class_gen' int_to_nn_class_gen R in
uconstr:(
fun (nnx : NNP) (excl : excluded_middle) (arg : L) =>
rec_R (nnx (rec_L arg excl)) excl)
| forall t: ?T, @?Q t =>
constr:(
fun (nnx : NNP) (excl : excluded_middle) (t : T) =>
ltac:(
let Qt := eval hnf in (Q t) in
let rec_Qt := nn_int_to_class_gen' int_to_nn_class_gen Qt in
exact (rec_Qt (nnx t) excl)))
| exists t: ?T, @?Q t =>
let prf := fresh nnx "_prf" in
let wit := fresh nnx "_wit" in
constr:(
fun (nnx : NNP) (excl : excluded_middle) =>
match excl P with
| or_introl prf => prf
| or_intror prf =>
False_ind P
( nnx
( fun
(t : T)
(wit :
ltac:(
let Qt := eval hnf in (Q t) in
let Q' := nn_transl Qt in
exact Q')) =>
ltac:(
let Qt := eval hnf in (Q t) in
let rec_Qt := nn_int_to_class_gen' int_to_nn_class_gen Qt in
exact (prf (ex_intro _ t (rec_Qt wit excl))))))
end)
| _ =>
let prf := fresh nnx "_prf" in
uconstr:(
fun (nnx : NNP) (excl : excluded_middle) =>
match excl P with
| or_introl prf => prf
| or_intror prf => False_ind P (nnx prf)
end)
end.
Ltac int_to_nn_class_gen :=
let rec
int_to_nn_class_gen :=
fun P => int_to_nn_class_gen' nn_int_to_class_gen P
with
nn_int_to_class_gen :=
fun P => nn_int_to_class_gen' int_to_nn_class_gen P
in
int_to_nn_class_gen.
Ltac nn_int_to_class_gen :=
let rec
int_to_nn_class_gen :=
fun P => int_to_nn_class_gen' nn_int_to_class_gen P
with
nn_int_to_class_gen :=
fun P => nn_int_to_class_gen' int_to_nn_class_gen P
in
nn_int_to_class_gen.
Tactic Notation "nn_int_to_class" constr(P) hyp(H) :=
let new := fresh "class_" H in
let transl := nn_int_to_class_gen P in
refine (let new : excluded_middle -> P := transl H in _).
Looking back at this, I think you might be able to implement this direction with Classes and Instances (type-directed lookup of implicit values is another Coq process that is outside the logic of Coq), since the translation is done entirely by a self-contained term, but I'm not sure the other direction (which would be analyzing the actual proof term fun (excl : excluded_middle) => ... for uses of excl) can be done this way. Here's a proof of the Drinker's Paradox:
Theorem nn_excluded_middle X : ~~(X \/ ~X).
Proof. tauto. Defined.
Theorem drinker's (P : Set) (x : P) (D : P -> Prop)
: excluded_middle -> exists y, D y -> forall z, D z.
Proof.
assert double negative (exists y, D y -> forall z, D z) as prf.
{
intros no.
apply (nn_excluded_middle (forall y, D y)).
intros [everyone | someone].
- apply no with x.
intros prf_x y prf_y.
apply prf_y, everyone.
- apply (nn_excluded_middle (exists y, ~D y)).
intros [[y sober] | drunk].
+ apply no with y.
intros drunk.
contradiction (drunk sober).
+ contradict someone.
intros y.
specialize (no y).
contradict no.
intros drunk_y z sober_z.
apply drunk.
exists z.
exact sober_z.
}
nn_int_to_class (exists y, D y -> forall z, D z) prf.
exact class_prf.
Defined.
