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.
Require Import Logic.PropositionalLogic.ProofTheory.Classical.
Require Import Logic.PropositionalLogic.ProofTheory.RewriteClass.
Require Import Logic.ModalLogic.Syntax.
Require Import Logic.ModalLogic.ProofTheory.ModalLogic.
Require Import Logic.ModalLogic.ProofTheory.RewriteClass.
Require Import Logic.ModalLogic.ProofTheory.IntuitionisticDerivedRules.

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

Section ClassicalderivedRules.

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

Existing Instances Classical2GodelDummett GodelDummett2DeMorgan.

Lemma diamondp_orp: forall x y, |-- diamondp (x || y) <--> (diamondp x || diamondp y).
Proof.
(* Goal: forall x y : @expr L, @provable L Gamma (@iffp L minL pL (@boxp L mL (@impp L minL x y)) (@impp L minL (@boxp L mL x) (@boxp L mL y))) *)
  intros.
(* Goal: @provable L Gamma (@iffp L minL pL (@diamondp L minL pL mL (@orp L pL x y)) (@orp L pL (@diamondp L minL pL mL x) (@diamondp L minL pL mL y))) *)
  apply solve_andp_intros; [| apply orp_diamondp].
(* Goal: @provable L Gamma (@impp L minL (@diamondp L minL pL mL (@orp L pL x y)) (@orp L pL (@diamondp L minL pL mL x) (@diamondp L minL pL mL y))) *)
  unfold diamondp.
(* Goal: @provable L Gamma (@impp L minL (@negp L minL pL (@boxp L mL (@negp L minL pL (@orp L pL x y)))) (@orp L pL (@negp L minL pL (@boxp L mL (@negp L minL pL x))) (@negp L minL pL (@boxp L mL (@negp L minL pL y))))) *)
  rewrite <- demorgan_negp_andp.
(* Goal: @provable L Gamma (@impp L minL (@negp L minL pL (@boxp L mL (@negp L minL pL (@orp L pL x y)))) (@negp L minL pL (@andp L pL (@boxp L mL (@negp L minL pL x)) (@boxp L mL (@negp L minL pL y))))) *)
  rewrite <- contrapositivePP.
(* Goal: @provable L Gamma (@impp L minL (@andp L pL (@boxp L mL (@negp L minL pL x)) (@boxp L mL (@negp L minL pL y))) (@boxp L mL (@negp L minL pL (@orp L pL x y)))) *)
  rewrite <- boxp_andp.
(* Goal: @provable L Gamma (@impp L minL (@boxp L mL (@andp L pL (@negp L minL pL x) (@negp L minL pL y))) (@boxp L mL (@negp L minL pL (@orp L pL x y)))) *)
  rewrite demorgan_negp_orp.
(* Goal: @provable L Gamma (@impp L minL (@boxp L mL (@andp L pL (@negp L minL pL x) (@negp L minL pL y))) (@boxp L mL (@andp L pL (@negp L minL pL x) (@negp L minL pL y)))) *)
  apply provable_impp_refl.
Qed.

Instance PropositionalTransparentModality2StrongPropositionalTransparentModality {pmGamma: PropositionalTransparentModality L Gamma}: StrongPropositionalTransparentModality L Gamma.
Proof.
(* Goal: @StrongPropositionalTransparentModality L minL pL mL Gamma minAX ipGamma KmGamma pmGamma *)
  constructor.
(* Goal: forall x y : @expr L, @provable L Gamma (@iffp L minL pL (@boxp L mL (@impp L minL x y)) (@impp L minL (@boxp L mL x) (@boxp L mL y))) *)
  intros.
(* Goal: @provable L Gamma (@iffp L minL pL (@boxp L mL (@impp L minL x y)) (@impp L minL (@boxp L mL x) (@boxp L mL y))) *)
  apply solve_andp_intros; [apply axiom_K |].
(* Goal: @provable L Gamma (@impp L minL (@impp L minL (@boxp L mL x) (@boxp L mL y)) (@boxp L mL (@impp L minL x y))) *)
  rewrite (impp2orp x y), (impp2orp (boxp x) (boxp y)).
(* Goal: @provable L Gamma (@impp L minL (@boxp L mL (@orp L pL x (@negp L minL pL x))) (@impp L minL (@negp L minL pL (@boxp L mL x)) (@boxp L mL (@negp L minL pL x)))) *)
  rewrite boxp_orp.
(* Goal: @provable L Gamma (@impp L minL (@orp L pL (@negp L minL pL (@boxp L mL x)) (@boxp L mL y)) (@orp L pL (@boxp L mL (@negp L minL pL x)) (@boxp L mL y))) *)
  apply solve_orp_impp; [| apply orp_intros2].
(* Goal: @provable L Gamma (@impp L minL (@negp L minL pL (@boxp L mL x)) (@orp L pL (@boxp L mL (@negp L minL pL x)) (@boxp L mL y))) *)
  rewrite <- orp_intros1.
(* Goal: @provable L Gamma (@impp L minL (@negp L minL pL (@boxp L mL x)) (@boxp L mL (@negp L minL pL x))) *)
  apply (modus_ponens (boxp (x || ~~ x))).
(* Goal: @provable L Gamma (@impp L minL (@boxp L mL (@orp L pL x (@negp L minL pL x))) (@impp L minL (@negp L minL pL (@boxp L mL x)) (@boxp L mL (@negp L minL pL x)))) *)
  + rewrite boxp_orp.
(* Goal: @provable L Gamma (@impp L minL (@orp L pL (@boxp L mL x) (@boxp L mL (@negp L minL pL x))) (@impp L minL (@negp L minL pL (@boxp L mL x)) (@boxp L mL (@negp L minL pL x)))) *)
    apply solve_orp_impp; [| apply axiom1].
(* Goal: @provable L Gamma (@impp L minL (@boxp L mL x) (@impp L minL (@negp L minL pL (@boxp L mL x)) (@boxp L mL (@negp L minL pL x)))) *)
    clear KmGamma pmGamma; AddSequentCalculus Gamma.
(* Goal: @provable L Gamma (@impp L minL (@boxp L mL x) (@impp L minL (@negp L minL pL (@boxp L mL x)) (@boxp L mL (@negp L minL pL x)))) *)
    rewrite provable_derivable.
(* Goal: @derivable L Gamma (@empty_context L) (@impp L minL (@boxp L mL x) (@impp L minL (@negp L minL pL (@boxp L mL x)) (@boxp L mL (@negp L minL pL x)))) *)
    rewrite <- !deduction_theorem.
(* Goal: @derivable L Gamma (Union (@expr L) (Union (@expr L) (@empty_context L) (Singleton (@expr L) (@boxp L mL x))) (Singleton (@expr L) (@negp L minL pL (@boxp L mL x)))) (@boxp L mL (@negp L minL pL x)) *)
    apply deduction_falsep_elim.
(* Goal: @derivable L Gamma (Union (@expr L) (Union (@expr L) (@empty_context L) (Singleton (@expr L) (@boxp L mL x))) (Singleton (@expr L) (@negp L minL pL (@boxp L mL x)))) (@falsep L pL) *)
    apply deduction_modus_ponens with (boxp x); solve_assum.
  + apply rule_N.
(* Goal: @provable L Gamma (@orp L pL x (@negp L minL pL x)) *)
    apply excluded_middle.
Qed.

End ClassicalderivedRules.
