(** Proof of Glivenko's theorem **)
(* please ignore the technicalities below, these are just to
make your life easy *)
Require Import List.
Definition ctxt := list Prop.
Implicit Type Γ Δ : ctxt.
Implicit Type A B C : Prop.
Reserved Notation " Γ ⊢ A" (at level 70, no associativity).
Reserved Notation " Γ ⊩ A" (at level 70, no associativity).
Notation "l ',' a" := (cons a l) (at level 69, left associativity).
Notation "A → B" := (A -> B) (at level 68, right associativity).
Notation "A ∧ B" := (A /\ B) (at level 67).
Notation "A ∨ B" := (A \/ B) (at level 66).
Notation "¬ A" := (~A) (at level 65, right associativity).
Notation "'⊥'" := False.
(* Question 1: define NJ *)
(* NJ : intuitionistic natural deduction *)
Inductive NJ : ctxt -> Prop -> Prop :=
| NJ_axiom : forall Γ A, In A Γ -> Γ ⊢ A
| NJ_impl_intro : forall Γ A B, Γ, A ⊢ B -> Γ ⊢ A → B
(* COMPLETE HERE *)
where "G ⊢ A" := (NJ G A).
(* Question 2: define NK *)
(* NK : classical natural deduction *)
Inductive NK : ctxt -> Prop -> Prop :=
| NK_axiom : forall Γ A, In A Γ -> Γ ⊩ A
(* COMPLETE HERE *)
where "G ⊩ A" := (NK G A).
(* Question 3: prove the lemma remove_double_negation *)
(* In NJ if you want to prove Γ, ¬¬A ⊢ ⊥
it is enough to prove Γ, ¬¬A, A ⊢ ⊥ *)
Lemma remove_double_negation : forall Γ A, In (¬¬A) Γ -> (Γ, A ⊢ ⊥) -> (Γ ⊢ ⊥).
Proof.
(* COMPLETE HERE *)
Admitted.
(* Question 4: for each of those tactics, explains what they
are supposed to do, i.e. when to use them? *)
Ltac AXIOM := apply NJ_axiom; unfold In; eauto 30.
Ltac INTRO := apply NJ_impl_intro.
Ltac ELIM t := apply NJ_impl_elim with t.
Ltac EXFALSO := apply NJ_False_elim.
Ltac NOTNOTNOT A := apply remove_double_negation with A ; [ unfold In; eauto 30 | ].
(* WRITE THE ANSWER HERE *)
(* Question 5: prove Glivenko's theorem.
- indent correctly to see the shape of the derivation trees
- keep them short (use the tactics above)
*)
Theorem Glivenko : forall Γ A, Γ ⊩ A -> Γ ⊢ ¬¬A.
Proof.
(* COMPLETE HERE *)
Admitted.