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.

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

Section IntuitionisticDerivedRules.

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

Lemma boxp_andp: forall x y, |-- boxp (x && y) <--> (boxp x && boxp y).
Proof.
(* Goal: forall x : @expr L, @provable L Gamma (@impp L minL x (@diamondp L minL pL mL x)) *)
  intros.
(* Goal: forall x : @expr L, @provable L Gamma (@impp L minL x (@diamondp L minL pL mL x)) *)
  apply solve_andp_intros.
  + rewrite <- (andp_elim1 x y) at 2.
(* Goal: @provable L Gamma (@impp L minL (@boxp L mL (@andp L pL x y)) (@andp L pL (@boxp L mL (@andp L pL x y)) (@boxp L mL y))) *)
    rewrite <- (andp_elim2 x y) at 3.
(* Goal: @provable L Gamma (@impp L minL (@boxp L mL (@andp L pL x y)) (@andp L pL (@boxp L mL (@andp L pL x y)) (@boxp L mL (@andp L pL x y)))) *)
    rewrite andp_dup.
(* Goal: @provable L Gamma (@negp L minL pL (@falsep L pL)) *)
    apply provable_impp_refl.
  + rewrite <- impp_curry_uncurry.
(* Goal: @provable L Gamma (@impp L minL (@boxp L mL (@impp L minL x y)) (@boxp L mL (@impp L minL (@negp L minL pL y) (@negp L minL pL x)))) *)
    rewrite <- axiom_K.
(* Goal: @provable L Gamma (@impp L minL (@boxp L mL (@impp L minL x y)) (@boxp L mL (@impp L minL (@negp L minL pL y) (@negp L minL pL x)))) *)
    rewrite <- axiom_K.
(* Goal: @provable L Gamma (@boxp L mL (@impp L minL y (@orp L pL x y))) *)
    apply rule_N.
(* Goal: forall x : @expr L, @provable L Gamma (@impp L minL x (@diamondp L minL pL mL x)) *)
    apply andp_intros.
Qed.

Lemma orp_boxp: forall x y, |-- boxp x || boxp y --> boxp (x || y).
Proof.
(* Goal: forall x : @expr L, @provable L Gamma (@impp L minL x (@diamondp L minL pL mL x)) *)
  intros.
(* Goal: @provable L Gamma (@impp L minL (@orp L pL (@diamondp L minL pL mL x) (@diamondp L minL pL mL y)) (@diamondp L minL pL mL (@orp L pL x y))) *)
  apply solve_orp_impp.
  + rewrite <- axiom_K.
(* Goal: @provable L Gamma (@boxp L mL (@impp L minL y (@orp L pL x y))) *)
    apply rule_N.
(* Goal: @provable L Gamma (@impp L minL x (@orp L pL x y)) *)
    apply orp_intros1.
  + rewrite <- axiom_K.
(* Goal: @provable L Gamma (@boxp L mL (@impp L minL y (@orp L pL x y))) *)
    apply rule_N.
(* Goal: @provable L Gamma (@impp L minL y (@orp L pL x y)) *)
    apply orp_intros2.
Qed.

Lemma boxp_TT: |-- boxp TT.
Proof.
(* Goal: @provable L Gamma (@boxp L mL (@impp L minL y (@orp L pL x y))) *)
  apply rule_N.
(* Goal: @provable L Gamma (@negp L minL pL (@falsep L pL)) *)
  apply provable_impp_refl.
Qed.

Lemma not_diamondp_FF: |-- ~~ diamondp FF.
Proof.
(* Goal: forall x : @expr L, @provable L Gamma (@impp L minL x (@diamondp L minL pL mL x)) *)
  intros.
(* Goal: @provable L Gamma (@impp L minL x (@diamondp L minL pL mL x)) *)
  unfold diamondp.
(* Goal: forall x : @expr L, @provable L Gamma (@impp L minL x (@diamondp L minL pL mL x)) *)
  rewrite <- double_negp_intros.
(* Goal: @provable L Gamma (@boxp L mL (@impp L minL y (@orp L pL x y))) *)
  apply rule_N.
(* Goal: @provable L Gamma (@negp L minL pL (@falsep L pL)) *)
  apply provable_impp_refl.
Qed.

Lemma impp_diamondp: forall x y, |-- boxp (x --> y) --> (diamondp x --> diamondp y).
Proof.
(* Goal: forall x : @expr L, @provable L Gamma (@impp L minL x (@diamondp L minL pL mL x)) *)
  intros.
(* Goal: @provable L Gamma (@impp L minL x (@diamondp L minL pL mL x)) *)
  unfold diamondp.
(* Goal: @provable L Gamma (@impp L minL (@boxp L mL (@impp L minL x y)) (@impp L minL (@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 <- contrapositivePP.
(* Goal: @provable L Gamma (@impp L minL (@boxp L mL (@impp L minL x y)) (@boxp L mL (@impp L minL (@negp L minL pL y) (@negp L minL pL x)))) *)
  rewrite <- axiom_K.
(* Goal: @provable L Gamma (@impp L minL (@boxp L mL (@impp L minL x y)) (@boxp L mL (@impp L minL (@negp L minL pL y) (@negp L minL pL x)))) *)
  rewrite <- axiom_K.
(* Goal: @provable L Gamma (@boxp L mL (@impp L minL y (@orp L pL x y))) *)
  apply rule_N.
(* Goal: @provable L Gamma (@impp L minL (@impp L minL x y) (@impp L minL (@negp L minL pL y) (@negp L minL pL x))) *)
  apply contrapositivePP.
Qed.
(*
Lemma derivable_impp_diamondp: forall Phi x y, Phi |-- boxp (x --> y) --> (diamondp x --> diamondp y).
Proof.
(* Goal: forall x : @expr L, @provable L Gamma (@impp L minL x (@diamondp L minL pL mL x)) *)
  intros.
  apply deduction_weaken0.
  apply impp_diamondp.
Qed.

Lemma deduction_impp_diamondp: forall Phi x y,
  Phi |-- boxp (x --> y) ->
  Phi |-- (diamondp x --> diamondp y).
Proof.
(* Goal: forall x : @expr L, @provable L Gamma (@impp L minL x (@diamondp L minL pL mL x)) *)
  intros.
  eapply deduction_modus_ponens; eauto.
  apply derivable_impp_diamondp.
Qed.
*)
Lemma diamondp_andp: forall x y, |-- diamondp (x && y) --> (diamondp x && diamondp y).
Proof.
(* Goal: forall x : @expr L, @provable L Gamma (@impp L minL x (@diamondp L minL pL mL x)) *)
  intros.
(* Goal: @provable L Gamma (@impp L minL (@diamondp L minL pL mL (@andp L pL x y)) (@andp L pL (@diamondp L minL pL mL x) (@diamondp L minL pL mL y))) *)
  apply solve_impp_andp.
  + rewrite <- impp_diamondp.
(* Goal: @provable L Gamma (@boxp L mL (@impp L minL y (@orp L pL x y))) *)
    apply rule_N.
(* Goal: @provable L Gamma (@impp L minL (@andp L pL x y) x) *)
    apply andp_elim1.
  + rewrite <- impp_diamondp.
(* Goal: @provable L Gamma (@boxp L mL (@impp L minL y (@orp L pL x y))) *)
    apply rule_N.
(* Goal: @provable L Gamma (@impp L minL (@andp L pL x y) y) *)
    apply andp_elim2.
Qed.

Lemma orp_diamondp: forall x y, |-- diamondp x || diamondp y --> diamondp (x || y).
Proof.
(* Goal: forall x : @expr L, @provable L Gamma (@impp L minL x (@diamondp L minL pL mL x)) *)
  intros.
(* Goal: @provable L Gamma (@impp L minL (@orp L pL (@diamondp L minL pL mL x) (@diamondp L minL pL mL y)) (@diamondp L minL pL mL (@orp L pL x y))) *)
  apply solve_orp_impp.
  + rewrite <- impp_diamondp.
(* Goal: @provable L Gamma (@boxp L mL (@impp L minL y (@orp L pL x y))) *)
    apply rule_N.
(* Goal: @provable L Gamma (@impp L minL x (@orp L pL x y)) *)
    apply orp_intros1.
  + rewrite <- impp_diamondp.
(* Goal: @provable L Gamma (@boxp L mL (@impp L minL y (@orp L pL x y))) *)
    apply rule_N.
(* Goal: @provable L Gamma (@impp L minL y (@orp L pL x y)) *)
    apply orp_intros2.
Qed.

Lemma P_diamondp_P {TmGamma: SystemT L Gamma}: forall x, |-- x --> diamondp x.
Proof.
(* Goal: forall x : @expr L, @provable L Gamma (@impp L minL x (@diamondp L minL pL mL x)) *)
  intros.
(* Goal: @provable L Gamma (@impp L minL x (@diamondp L minL pL mL x)) *)
  unfold diamondp.
(* Goal: @provable L Gamma (@impp L minL x (@negp L minL pL (@boxp L mL (@negp L minL pL x)))) *)
  rewrite <- contrapositivePN.
(* Goal: @provable L Gamma (@impp L minL (@boxp L mL (@negp L minL pL x)) (@negp L minL pL x)) *)
  apply axiom_T.
Qed.

End IntuitionisticDerivedRules.
