Require Import Logic.GeneralLogic.Base.
Require Import Logic.GeneralLogic.ProofTheory.BasicSequentCalculus.
Require Import Logic.MinimunLogic.Syntax.
Require Import Logic.MinimunLogic.ProofTheory.Minimun.
Require Import Logic.MinimunLogic.ProofTheory.RewriteClass.
Require Import Logic.PropositionalLogic.Syntax.
Require Import Logic.PropositionalLogic.ProofTheory.Intuitionistic.
Require Import Logic.PropositionalLogic.ProofTheory.DeMorgan.
Require Import Logic.PropositionalLogic.ProofTheory.GodelDummett.

Local Open Scope logic_base.
Local Open Scope syntax.
Import PropositionalLanguageNotation.

Class ClassicalPropositionalLogic (L: Language) {minL: MinimunLanguage L} {pL: PropositionalLanguage L} (Gamma: ProofTheory L) {minAX: MinimunAxiomatization L Gamma} {ipGamma: IntuitionisticPropositionalLogic L Gamma} := {
  excluded_middle: forall x, |-- x || ~~ x
}.

Class ClassicalPropositionalSequentCalculus (L: Language) {minL: MinimunLanguage L} {pL: PropositionalLanguage L} (Gamma: ProofTheory L) {bSC: BasicSequentCalculus L Gamma} {minSC: MinimunSequentCalculus L Gamma} {ipSC: IntuitionisticPropositionalSequentCalculus L Gamma} := {
  derivable_excluded_middle: forall Phi x, Phi |-- x || ~~ x
}.

Section Axiomatization2SequentCalculus.

Context {L: Language}
        {minL: MinimunLanguage L}
        {pL: PropositionalLanguage L}
        {Gamma: ProofTheory L}
        {minAX: MinimunAxiomatization L Gamma}
        {ipGamma: IntuitionisticPropositionalLogic L Gamma}
        {cpGamma: ClassicalPropositionalLogic L Gamma}
        {SC: NormalSequentCalculus L Gamma}
        {bSC: BasicSequentCalculus L Gamma}
        {minSC: MinimunSequentCalculus L Gamma}
        {ipSC: IntuitionisticPropositionalSequentCalculus L Gamma}.

Lemma Axiomatization2SequentCalculus_cpSC: ClassicalPropositionalSequentCalculus L Gamma.
Proof.
(* Goal: forall x y : @expr L, @provable L Gamma (@iffp L minL pL (@impp L minL x y) (@orp L pL (@negp L minL pL x) y)) *)
  intros.
(* Goal: @GodelDummettPropositionalLogic L minL pL Gamma minAX ipGamma *)
  constructor.
(* Goal: forall x y : @expr L, @provable L Gamma (@iffp L minL pL (@impp L minL x y) (@orp L pL (@negp L minL pL x) y)) *)
  intros.
(* Goal: @derivable L Gamma Phi (@orp L pL x (@negp L minL pL x)) *)
  apply deduction_weaken0.
(* Goal: @provable L Gamma (@orp L pL x (@negp L minL pL x)) *)
  apply excluded_middle.
Qed.

End Axiomatization2SequentCalculus.

Section AddSequentCalculus.

Context {L: Language}
        {minL: MinimunLanguage L}
        {pL: PropositionalLanguage L}
        {Gamma: ProofTheory L}
        {minAX: MinimunAxiomatization L Gamma}
        {ipGamma: IntuitionisticPropositionalLogic L Gamma}
        {cpGamma: ClassicalPropositionalLogic L Gamma}
        {minAX': MinimunAxiomatization L (Build_AxiomaticProofTheory (@provable L Gamma))}
        {ipGamma': IntuitionisticPropositionalLogic L (Build_AxiomaticProofTheory (@provable L Gamma))}
        {SC: NormalSequentCalculus L (Build_AxiomaticProofTheory (@provable L Gamma))}
        {bSC: BasicSequentCalculus L (Build_AxiomaticProofTheory (@provable L Gamma))}
        {minSC: MinimunSequentCalculus L (Build_AxiomaticProofTheory (@provable L Gamma))}
        {ipSC: IntuitionisticPropositionalSequentCalculus L (Build_AxiomaticProofTheory (@provable L Gamma))}.

Lemma MakeSequentCalculus_ClassicalPropositionalLogic:
  Typeclass_Rewrite (exist (fun X: Prop => X) (IntuitionisticPropositionalLogic L (Build_AxiomaticProofTheory (@provable L Gamma))) ipGamma' :: exist (fun X: Prop => X) (IntuitionisticPropositionalSequentCalculus L (Build_AxiomaticProofTheory (@provable L Gamma))) ipSC :: exist (fun X: Prop => X) (BasicSequentCalculus L (Build_AxiomaticProofTheory (@provable L Gamma))) bSC :: exist (fun X: Prop => X) (MinimunSequentCalculus L (Build_AxiomaticProofTheory (@provable L Gamma))) minSC :: nil) ->
  forall (G: Prop) (l: list (sig (fun X: Prop => X))),
  (forall
     (cpSC: ClassicalPropositionalSequentCalculus L (Build_AxiomaticProofTheory (@provable L Gamma)))
     (cpGamma: ClassicalPropositionalLogic L (Build_AxiomaticProofTheory (@provable L Gamma))),
     OpaqueProp (Typeclass_Rewrite l -> G)) <->
  OpaqueProp (Typeclass_Rewrite ((exist (fun X: Prop => X) (ClassicalPropositionalLogic L Gamma) cpGamma) :: l) -> G).
Proof.
(* Goal: forall (_ : Typeclass_Rewrite (@cons (@sig Prop (fun X : Prop => X)) (@exist Prop (fun X : Prop => X) (@IntuitionisticPropositionalLogic L minL pL (@Build_SequentCalculus L (@derivable L Gamma)) minAX) ipGamma) (@cons (@sig Prop (fun X : Prop => X)) (@exist Prop (fun X : Prop => X) (@IntuitionisticPropositionalSequentCalculus L pL (@Build_SequentCalculus L (@derivable L Gamma))) ipSC') (@cons (@sig Prop (fun X : Prop => X)) (@exist Prop (fun X : Prop => X) (BasicSequentCalculus L (@Build_SequentCalculus L (@derivable L Gamma))) bSC') (@cons (@sig Prop (fun X : Prop => X)) (@exist Prop (fun X : Prop => X) (@MinimunSequentCalculus L minL (@Build_SequentCalculus L (@derivable L Gamma))) minSC') (@nil (@sig Prop (fun X : Prop => X)))))))) (G : Prop) (l : list (@sig Prop (fun X : Prop => X))), iff (forall (_ : @ClassicalPropositionalSequentCalculus L minL pL (@Build_SequentCalculus L (@derivable L Gamma)) bSC' minSC' ipSC') (_ : @ClassicalPropositionalLogic L minL pL (@Build_SequentCalculus L (@derivable L Gamma)) minAX ipGamma), OpaqueProp (forall _ : Typeclass_Rewrite l, G)) (OpaqueProp (forall _ : Typeclass_Rewrite (@cons (@sig Prop (fun X : Prop => X)) (@exist Prop (fun X : Prop => X) (@ClassicalPropositionalSequentCalculus L minL pL Gamma bSC minSC ipSC) cpSC) l), G)) *)
  unfold OpaqueProp.
(* Goal: forall (_ : Typeclass_Rewrite (@cons (@sig Prop (fun X : Prop => X)) (@exist Prop (fun X : Prop => X) (@IntuitionisticPropositionalLogic L minL pL (@Build_SequentCalculus L (@derivable L Gamma)) minAX) ipGamma) (@cons (@sig Prop (fun X : Prop => X)) (@exist Prop (fun X : Prop => X) (@IntuitionisticPropositionalSequentCalculus L pL (@Build_SequentCalculus L (@derivable L Gamma))) ipSC') (@cons (@sig Prop (fun X : Prop => X)) (@exist Prop (fun X : Prop => X) (BasicSequentCalculus L (@Build_SequentCalculus L (@derivable L Gamma))) bSC') (@cons (@sig Prop (fun X : Prop => X)) (@exist Prop (fun X : Prop => X) (@MinimunSequentCalculus L minL (@Build_SequentCalculus L (@derivable L Gamma))) minSC') (@nil (@sig Prop (fun X : Prop => X)))))))) (G : Prop) (l : list (@sig Prop (fun X : Prop => X))), iff (forall (_ : @ClassicalPropositionalSequentCalculus L minL pL (@Build_SequentCalculus L (@derivable L Gamma)) bSC' minSC' ipSC') (_ : @ClassicalPropositionalLogic L minL pL (@Build_SequentCalculus L (@derivable L Gamma)) minAX ipGamma) (_ : Typeclass_Rewrite l), G) (forall _ : Typeclass_Rewrite (@cons (@sig Prop (fun X : Prop => X)) (@exist Prop (fun X : Prop => X) (@ClassicalPropositionalSequentCalculus L minL pL Gamma bSC minSC ipSC) cpSC) l), G) *)
  intros _.
(* Goal: forall x y : @expr L, @provable L Gamma (@iffp L minL pL (@impp L minL x y) (@orp L pL (@negp L minL pL x) y)) *)
  intros.
(* Goal: forall x y : @expr L, @provable L Gamma (@iffp L minL pL (@impp L minL x y) (@orp L pL (@negp L minL pL x) y)) *)
  split; intros.
  + clear H0.
    assert (ClassicalPropositionalLogic L (Build_AxiomaticProofTheory provable))
      by (destruct cpGamma; constructor; auto).
(* Goal: G *)
    apply H; auto.
    - apply Axiomatization2SequentCalculus_cpSC.
    - apply Typeclass_Rewrite_I.
  + apply H; auto.
(* Goal: Typeclass_Rewrite (@cons (@sig Prop (fun X : Prop => X)) (@exist Prop (fun X : Prop => X) (@ClassicalPropositionalSequentCalculus L minL pL Gamma bSC minSC ipSC) cpSC) l) *)
    apply Typeclass_Rewrite_I.
Qed.

End AddSequentCalculus.

Hint Rewrite <- @MakeSequentCalculus_ClassicalPropositionalLogic using first [typeclasses eauto | instantiate (1 := _); instantiate (1 := _); instantiate (1 := _); instantiate_must_succeed; apply Typeclass_Rewrite_I]: AddSC.

Section SequentCalculus2Axiomatization.

Context {L: Language}
        {minL: MinimunLanguage L}
        {pL: PropositionalLanguage L}
        {Gamma: ProofTheory L}
        {SC: NormalSequentCalculus L Gamma}
        {bSC: BasicSequentCalculus L Gamma}
        {minSC: MinimunSequentCalculus L Gamma}
        {ipSC: IntuitionisticPropositionalSequentCalculus L Gamma}
        {cpSC: ClassicalPropositionalSequentCalculus L Gamma}
        {minAX: MinimunAxiomatization L Gamma}
        {ipGamma: IntuitionisticPropositionalLogic L Gamma}.

Lemma SequentCalculus2Axiomatization_cpGamma: ClassicalPropositionalLogic L Gamma.
Proof.
(* Goal: forall x y : @expr L, @provable L Gamma (@iffp L minL pL (@impp L minL x y) (@orp L pL (@negp L minL pL x) y)) *)
  intros.
(* Goal: @GodelDummettPropositionalLogic L minL pL Gamma minAX ipGamma *)
  constructor.
(* Goal: forall x y : @expr L, @provable L Gamma (@iffp L minL pL (@impp L minL x y) (@orp L pL (@negp L minL pL x) y)) *)
  intros.
(* Goal: @provable L Gamma (@iffp L minL pL (@impp L minL x y) (@orp L pL (@negp L minL pL x) y)) *)
  rewrite provable_derivable.
(* Goal: @derivable L Gamma (@empty_context L) (@orp L pL x (@negp L minL pL x)) *)
  apply derivable_excluded_middle.
Qed.

End SequentCalculus2Axiomatization.

Section AddAxiomatization.

Context {L: Language}
        {minL: MinimunLanguage L}
        {pL: PropositionalLanguage L}
        {Gamma: ProofTheory L}
        {bSC: BasicSequentCalculus L Gamma}
        {minSC: MinimunSequentCalculus L Gamma}
        {ipSC: IntuitionisticPropositionalSequentCalculus L Gamma}
        {cpSC: ClassicalPropositionalSequentCalculus L Gamma}
        {minAX: MinimunAxiomatization L (Build_SequentCalculus (@derivable L Gamma))}
        {ipGamma: IntuitionisticPropositionalLogic L (Build_SequentCalculus (@derivable L Gamma))}
        {SC': NormalSequentCalculus L (Build_SequentCalculus (@derivable L Gamma))}
        {bSC': BasicSequentCalculus L (Build_SequentCalculus (@derivable L Gamma))}
        {minSC': MinimunSequentCalculus L (Build_SequentCalculus (@derivable L Gamma))}
        {ipSC': IntuitionisticPropositionalSequentCalculus L (Build_SequentCalculus (@derivable L Gamma))}.

Lemma MakeAxiomatization_ClassicalPropositionalSequentCalculus:
  Typeclass_Rewrite (exist (fun X: Prop => X) (IntuitionisticPropositionalLogic L (Build_SequentCalculus (@derivable L Gamma))) ipGamma :: exist (fun X: Prop => X) (IntuitionisticPropositionalSequentCalculus L (Build_SequentCalculus (@derivable L Gamma))) ipSC' :: exist (fun X: Prop => X) (BasicSequentCalculus L (Build_SequentCalculus (@derivable L Gamma))) bSC' :: exist (fun X: Prop => X) (MinimunSequentCalculus L (Build_SequentCalculus (@derivable L Gamma))) minSC' :: nil) ->
  forall (G: Prop) (l: list (sig (fun X: Prop => X))),
  (forall
     (cpSC: ClassicalPropositionalSequentCalculus L (Build_SequentCalculus (@derivable L Gamma)))
     (cpGamma: ClassicalPropositionalLogic L (Build_SequentCalculus (@derivable L Gamma))),
     OpaqueProp (Typeclass_Rewrite l -> G)) <->
  OpaqueProp (Typeclass_Rewrite ((exist (fun X: Prop => X) (ClassicalPropositionalSequentCalculus L Gamma) cpSC) :: l) -> G).
Proof.
(* Goal: forall (_ : Typeclass_Rewrite (@cons (@sig Prop (fun X : Prop => X)) (@exist Prop (fun X : Prop => X) (@IntuitionisticPropositionalLogic L minL pL (@Build_SequentCalculus L (@derivable L Gamma)) minAX) ipGamma) (@cons (@sig Prop (fun X : Prop => X)) (@exist Prop (fun X : Prop => X) (@IntuitionisticPropositionalSequentCalculus L pL (@Build_SequentCalculus L (@derivable L Gamma))) ipSC') (@cons (@sig Prop (fun X : Prop => X)) (@exist Prop (fun X : Prop => X) (BasicSequentCalculus L (@Build_SequentCalculus L (@derivable L Gamma))) bSC') (@cons (@sig Prop (fun X : Prop => X)) (@exist Prop (fun X : Prop => X) (@MinimunSequentCalculus L minL (@Build_SequentCalculus L (@derivable L Gamma))) minSC') (@nil (@sig Prop (fun X : Prop => X)))))))) (G : Prop) (l : list (@sig Prop (fun X : Prop => X))), iff (forall (_ : @ClassicalPropositionalSequentCalculus L minL pL (@Build_SequentCalculus L (@derivable L Gamma)) bSC' minSC' ipSC') (_ : @ClassicalPropositionalLogic L minL pL (@Build_SequentCalculus L (@derivable L Gamma)) minAX ipGamma), OpaqueProp (forall _ : Typeclass_Rewrite l, G)) (OpaqueProp (forall _ : Typeclass_Rewrite (@cons (@sig Prop (fun X : Prop => X)) (@exist Prop (fun X : Prop => X) (@ClassicalPropositionalSequentCalculus L minL pL Gamma bSC minSC ipSC) cpSC) l), G)) *)
  unfold OpaqueProp.
(* Goal: forall (_ : Typeclass_Rewrite (@cons (@sig Prop (fun X : Prop => X)) (@exist Prop (fun X : Prop => X) (@IntuitionisticPropositionalLogic L minL pL (@Build_SequentCalculus L (@derivable L Gamma)) minAX) ipGamma) (@cons (@sig Prop (fun X : Prop => X)) (@exist Prop (fun X : Prop => X) (@IntuitionisticPropositionalSequentCalculus L pL (@Build_SequentCalculus L (@derivable L Gamma))) ipSC') (@cons (@sig Prop (fun X : Prop => X)) (@exist Prop (fun X : Prop => X) (BasicSequentCalculus L (@Build_SequentCalculus L (@derivable L Gamma))) bSC') (@cons (@sig Prop (fun X : Prop => X)) (@exist Prop (fun X : Prop => X) (@MinimunSequentCalculus L minL (@Build_SequentCalculus L (@derivable L Gamma))) minSC') (@nil (@sig Prop (fun X : Prop => X)))))))) (G : Prop) (l : list (@sig Prop (fun X : Prop => X))), iff (forall (_ : @ClassicalPropositionalSequentCalculus L minL pL (@Build_SequentCalculus L (@derivable L Gamma)) bSC' minSC' ipSC') (_ : @ClassicalPropositionalLogic L minL pL (@Build_SequentCalculus L (@derivable L Gamma)) minAX ipGamma) (_ : Typeclass_Rewrite l), G) (forall _ : Typeclass_Rewrite (@cons (@sig Prop (fun X : Prop => X)) (@exist Prop (fun X : Prop => X) (@ClassicalPropositionalSequentCalculus L minL pL Gamma bSC minSC ipSC) cpSC) l), G) *)
  intros _.
(* Goal: forall x y : @expr L, @provable L Gamma (@iffp L minL pL (@impp L minL x y) (@orp L pL (@negp L minL pL x) y)) *)
  intros.
(* Goal: forall x y : @expr L, @provable L Gamma (@iffp L minL pL (@impp L minL x y) (@orp L pL (@negp L minL pL x) y)) *)
  split; intros.
  + clear H0.
    assert (ClassicalPropositionalSequentCalculus L (Build_SequentCalculus (@derivable L Gamma)))
      by (destruct cpSC; constructor; auto).
(* Goal: G *)
    apply H; auto.
    - apply SequentCalculus2Axiomatization_cpGamma.
    - apply Typeclass_Rewrite_I.
  + apply H; auto.
(* Goal: Typeclass_Rewrite (@cons (@sig Prop (fun X : Prop => X)) (@exist Prop (fun X : Prop => X) (@ClassicalPropositionalSequentCalculus L minL pL Gamma bSC minSC ipSC) cpSC) l) *)
    apply Typeclass_Rewrite_I.
Qed.

End AddAxiomatization.

Hint Rewrite <- @MakeAxiomatization_ClassicalPropositionalSequentCalculus using first [typeclasses eauto | instantiate (1 := _); instantiate (1 := _); instantiate (1 := _); instantiate_must_succeed; apply Typeclass_Rewrite_I]: AddAX.

Section DerivableRulesFromAxiomatization1.

Context {L: Language}
        {minL: MinimunLanguage L}
        {pL: PropositionalLanguage L}
        {Gamma: ProofTheory L}
        {minAX: MinimunAxiomatization L Gamma}
        {ipGamma: IntuitionisticPropositionalLogic L Gamma}
        {cpGamma: ClassicalPropositionalLogic L Gamma}.

Lemma double_negp_elim: forall (x: expr),
  |-- ~~ (~~ x) --> x.
Proof.
(* Goal: forall x y : @expr L, @provable L Gamma (@iffp L minL pL (@impp L minL x y) (@orp L pL (@negp L minL pL x) y)) *)
  AddSequentCalculus Gamma.
(* Goal: forall x y : @expr L, @provable L Gamma (@iffp L minL pL (@impp L minL x y) (@orp L pL (@negp L minL pL x) y)) *)
  intros.
(* Goal: @provable L Gamma (@impp L minL (@negp L minL pL (@negp L minL pL x)) x) *)
  unfold negp.
  pose proof orp_elim x (x --> FF) (((x --> FF) --> FF) --> x).
  pose proof axiom1 x ((x --> FF) --> FF).
(* Goal: @provable L Gamma (@impp L minL (@impp L minL (@impp L minL x (@falsep L pL)) (@falsep L pL)) x) *)
  pose proof modus_ponens _ _ H H0.
(* Goal: @provable L Gamma (@impp L minL (@impp L minL (@impp L minL x (@falsep L pL)) (@falsep L pL)) x) *)
  clear H H0.

  pose proof derivable_contradiction_elim empty_context (x --> FF) x.
  rewrite <- provable_derivable in H.
(* Goal: @provable L Gamma (@impp L minL (@impp L minL (@impp L minL x (@falsep L pL)) (@falsep L pL)) x) *)
  pose proof modus_ponens _ _ H1 H.
(* Goal: @provable L Gamma (@impp L minL (@impp L minL (@impp L minL x (@falsep L pL)) (@falsep L pL)) x) *)
  clear H H1.

(* Goal: @derivable L Gamma Phi (@orp L pL (@impp L minL x y) (@impp L minL y x)) *)
  pose proof excluded_middle x.
(* Goal: @provable L Gamma (@impp L minL (@impp L minL (@impp L minL x (@falsep L pL)) (@falsep L pL)) x) *)
  pose proof modus_ponens _ _ H0 H.
(* Goal: @derivable L Gamma Phi (@impp L minL (@negp L minL pL y) x) *)
  auto.
Qed.

Lemma double_negp: forall (x: expr),
  |-- ~~ (~~ x) <--> x.
Proof.
(* Goal: forall x y : @expr L, @provable L Gamma (@iffp L minL pL (@impp L minL x y) (@orp L pL (@negp L minL pL x) y)) *)
  AddSequentCalculus Gamma.
(* Goal: forall x y : @expr L, @provable L Gamma (@iffp L minL pL (@impp L minL x y) (@orp L pL (@negp L minL pL x) y)) *)
  intros.
(* Goal: @provable L Gamma (@iffp L minL pL (@impp L minL x y) (@orp L pL (@negp L minL pL x) y)) *)
  rewrite provable_derivable.
  apply deduction_andp_intros;
  rewrite <- provable_derivable.
  + apply double_negp_elim.
(* Goal: forall x y : @expr L, @provable L Gamma (@iffp L minL pL (@impp L minL x y) (@orp L pL (@negp L minL pL x) y)) *)
  + apply double_negp_intros.
Qed.

Instance Classical2GodelDummett: GodelDummettPropositionalLogic L Gamma.
Proof.
(* Goal: @GodelDummettPropositionalLogic L minL pL Gamma minAX ipGamma *)
  constructor.
(* Goal: forall x y : @expr L, @provable L Gamma (@iffp L minL pL (@impp L minL x y) (@orp L pL (@negp L minL pL x) y)) *)
  AddSequentCalculus Gamma.
(* Goal: forall x y : @expr L, @provable L Gamma (@iffp L minL pL (@impp L minL x y) (@orp L pL (@negp L minL pL x) y)) *)
  intros.
(* Goal: @provable L Gamma (@iffp L minL pL (@impp L minL x y) (@orp L pL (@negp L minL pL x) y)) *)
  rewrite provable_derivable.
(* Goal: @derivable L Gamma (@empty_context L) (@orp L pL (@impp L minL x y) (@impp L minL y x)) *)
  set (Phi := empty_context).
(* Goal: @derivable L Gamma Phi (@orp L pL (@impp L minL x y) (@impp L minL y x)) *)
  clearbody Phi.
(* Goal: @derivable L Gamma Phi (@orp L pL (@impp L minL x y) (@impp L minL y x)) *)
  pose proof excluded_middle x.
(* Goal: @derivable L Gamma Phi (@orp L pL (@impp L minL x y) (@impp L minL y x)) *)
  apply deduction_weaken0 with (Phi0 := Phi) in H.
(* Goal: @derivable L Gamma Phi (@orp L pL (@impp L minL x y) (@impp L minL y x)) *)
  eapply deduction_modus_ponens; [exact H |].
(* Goal: @derivable L Gamma (@empty_context L) (@impp L minL (@orp L pL (@negp L minL pL x) y) (@impp L minL x y)) *)
  apply deduction_orp_elim'.
  + rewrite <- deduction_theorem.
(* Goal: @derivable L Gamma (Union (@expr L) (Union (@expr L) (@empty_context L) (Singleton (@expr L) (@impp L minL x y))) (Singleton (@expr L) x)) (@orp L pL (@negp L minL pL x) y) *)
    apply deduction_orp_intros2.
(* Goal: @derivable L Gamma (Union (@expr L) (Union (@expr L) (@empty_context L) (Singleton (@expr L) (@negp L minL pL x))) (Singleton (@expr L) x)) (@falsep L pL) *)
    rewrite deduction_theorem.
(* Goal: @derivable L Gamma (@empty_context L) (@impp L minL y (@impp L minL x y)) *)
    apply derivable_axiom1.
  + rewrite <- deduction_theorem.
(* Goal: @derivable L Gamma (Union (@expr L) (Union (@expr L) (@empty_context L) (Singleton (@expr L) (@impp L minL x y))) (Singleton (@expr L) (@negp L minL pL x))) (@orp L pL (@negp L minL pL x) y) *)
    apply deduction_orp_intros1.
(* Goal: @derivable L Gamma (Union (@expr L) (Union (@expr L) (@empty_context L) (Singleton (@expr L) (@negp L minL pL x))) (Singleton (@expr L) x)) (@falsep L pL) *)
    rewrite deduction_theorem.
(* Goal: @derivable L Gamma Phi (@impp L minL (@negp L minL pL x) (@impp L minL x y)) *)
    apply deduction_impp_arg_switch.
(* Goal: @derivable L Gamma Phi (@impp L minL x (@impp L minL (@negp L minL pL x) y)) *)
    apply derivable_contradiction_elim.
Qed.

Lemma contrapositiveNN: forall (x y: expr),
  |-- (~~ y --> ~~ x) --> (x --> y).
Proof.
(* Goal: forall x y : @expr L, @provable L Gamma (@iffp L minL pL (@impp L minL x y) (@orp L pL (@negp L minL pL x) y)) *)
  AddSequentCalculus Gamma.
(* Goal: forall x y : @expr L, @provable L Gamma (@iffp L minL pL (@impp L minL x y) (@orp L pL (@negp L minL pL x) y)) *)
  intros.
  rewrite <- (double_negp_elim y) at 2.
(* Goal: @provable L Gamma (@iffp L minL pL (@impp L minL x y) (@orp L pL (@negp L minL pL x) y)) *)
  rewrite provable_derivable.
  rewrite <- deduction_theorem.
(* Goal: @derivable L Gamma (Union (@expr L) (@empty_context L) (Singleton (@expr L) (@impp L minL (@negp L minL pL y) (@negp L minL pL x)))) (@impp L minL x (@negp L minL pL (@negp L minL pL y))) *)
  apply deduction_contrapositivePN.
(* Goal: @derivable L Gamma (Union (@expr L) (@empty_context L) (Singleton (@expr L) (@impp L minL (@negp L minL pL y) (@negp L minL pL x)))) (@impp L minL (@negp L minL pL y) (@negp L minL pL x)) *)
  solve_assum.
Qed.

Lemma contrapositiveNP: forall (x y: expr),
  |-- (~~ y --> x) --> (~~ x --> y).
Proof.
(* Goal: forall x y : @expr L, @provable L Gamma (@iffp L minL pL (@impp L minL x y) (@orp L pL (@negp L minL pL x) y)) *)
  AddSequentCalculus Gamma.
(* Goal: forall x y : @expr L, @provable L Gamma (@iffp L minL pL (@impp L minL x y) (@orp L pL (@negp L minL pL x) y)) *)
  intros.
  rewrite <- (contrapositiveNN (~~ x) y).
  rewrite <- (double_negp_intros x).
(* Goal: @provable L Gamma (@impp L minL (@impp L minL (@negp L minL pL y) x) (@impp L minL (@negp L minL pL y) x)) *)
  apply provable_impp_refl.
Qed.

End DerivableRulesFromAxiomatization1.

Section DerivableRulesFromSequentCalculus.

Context {L: Language}
        {minL: MinimunLanguage L}
        {pL: PropositionalLanguage L}
        {Gamma: ProofTheory L}
        {bSC: BasicSequentCalculus L Gamma}
        {minSC: MinimunSequentCalculus L Gamma}
        {ipSC: IntuitionisticPropositionalSequentCalculus L Gamma}
        {cpSC: ClassicalPropositionalSequentCalculus L Gamma}.

Lemma deduction_contrapositiveNN: forall Phi (x y: expr),
  Phi |-- ~~ y --> ~~ x ->
  Phi |-- x --> y.
Proof.
(* Goal: forall (Phi : @context L) (x y : @expr L) (_ : @derivable L Gamma Phi (@impp L minL (@negp L minL pL y) x)), @derivable L Gamma Phi (@impp L minL (@negp L minL pL x) y) *)
  AddAxiomatization Gamma.
(* Goal: forall x y : @expr L, @provable L Gamma (@iffp L minL pL (@impp L minL x y) (@orp L pL (@negp L minL pL x) y)) *)
  intros.
  rewrite <- contrapositiveNN.
(* Goal: @derivable L Gamma Phi (@impp L minL (@negp L minL pL y) x) *)
  auto.
Qed.

Lemma deduction_contrapositiveNP: forall Phi (x y: expr),
  Phi |-- ~~ y --> x ->
  Phi |-- ~~ x --> y.
Proof.
(* Goal: forall (Phi : @context L) (x y : @expr L) (_ : @derivable L Gamma Phi (@impp L minL (@negp L minL pL y) x)), @derivable L Gamma Phi (@impp L minL (@negp L minL pL x) y) *)
  AddAxiomatization Gamma.
(* Goal: forall x y : @expr L, @provable L Gamma (@iffp L minL pL (@impp L minL x y) (@orp L pL (@negp L minL pL x) y)) *)
  intros.
  rewrite <- contrapositiveNP.
(* Goal: @derivable L Gamma Phi (@impp L minL (@negp L minL pL y) x) *)
  auto.
Qed.

End DerivableRulesFromSequentCalculus.

Section DerivableRulesFromAxiomatization2.

Context {L: Language}
        {minL: MinimunLanguage L}
        {pL: PropositionalLanguage L}
        {Gamma: ProofTheory L}
        {minAX: MinimunAxiomatization L Gamma}
        {ipGamma: IntuitionisticPropositionalLogic L Gamma}
        {cpGamma: ClassicalPropositionalLogic L Gamma}.

Lemma impp2orp: forall (x y: expr),
  |-- (x --> y) <--> (~~ x || y).
Proof.
(* Goal: forall x y : @expr L, @provable L Gamma (@iffp L minL pL (@impp L minL x y) (@orp L pL (@negp L minL pL x) y)) *)
  AddSequentCalculus Gamma.
(* Goal: forall x y : @expr L, @provable L Gamma (@iffp L minL pL (@impp L minL x y) (@orp L pL (@negp L minL pL x) y)) *)
  intros.
(* Goal: @provable L Gamma (@iffp L minL pL (@impp L minL x y) (@orp L pL (@negp L minL pL x) y)) *)
  rewrite provable_derivable.
(* Goal: forall x y : @expr L, @provable L Gamma (@iffp L minL pL (@impp L minL x y) (@orp L pL (@negp L minL pL x) y)) *)
  apply deduction_andp_intros.
  + rewrite <- deduction_theorem.
(* Goal: @derivable L Gamma (Union (@expr L) (@empty_context L) (Singleton (@expr L) (@impp L minL x y))) (@orp L pL (@negp L minL pL x) y) *)
    apply (deduction_modus_ponens _ (x || ~~ x)); [apply derivable_excluded_middle |].
(* Goal: @derivable L Gamma (@empty_context L) (@impp L minL (@orp L pL (@negp L minL pL x) y) (@impp L minL x y)) *)
    apply deduction_orp_elim'.
    - rewrite <- deduction_theorem.
(* Goal: @derivable L Gamma (Union (@expr L) (Union (@expr L) (@empty_context L) (Singleton (@expr L) (@impp L minL x y))) (Singleton (@expr L) x)) (@orp L pL (@negp L minL pL x) y) *)
      apply deduction_orp_intros2.
      rewrite -> deduction_theorem.
(* Goal: @derivable L Gamma (Union (@expr L) (@empty_context L) (Singleton (@expr L) (@negp L minL pL x))) (@impp L minL x (@falsep L pL)) *)
      apply derivable_assum1.
    - rewrite <- deduction_theorem.
(* Goal: @derivable L Gamma (Union (@expr L) (Union (@expr L) (@empty_context L) (Singleton (@expr L) (@impp L minL x y))) (Singleton (@expr L) (@negp L minL pL x))) (@orp L pL (@negp L minL pL x) y) *)
      apply deduction_orp_intros1.
(* Goal: @derivable L Gamma (Union (@expr L) (@empty_context L) (Singleton (@expr L) (@negp L minL pL x))) (@impp L minL x (@falsep L pL)) *)
      apply derivable_assum1.
  + apply deduction_orp_elim'.
    - rewrite <- deduction_theorem.
      rewrite <- deduction_theorem.
(* Goal: @derivable L Gamma (Union (@expr L) (Union (@expr L) (@empty_context L) (Singleton (@expr L) (@negp L minL pL x))) (Singleton (@expr L) x)) y *)
      apply deduction_falsep_elim.
      rewrite -> deduction_theorem.
(* Goal: @derivable L Gamma (Union (@expr L) (@empty_context L) (Singleton (@expr L) (@negp L minL pL x))) (@impp L minL x (@falsep L pL)) *)
      apply derivable_assum1.
    - apply derivable_axiom1.
Qed.

End DerivableRulesFromAxiomatization2.

