Require Import Logic.GeneralLogic.Base.
Require Import Logic.MinimunLogic.Syntax.
Require Import Logic.PropositionalLogic.Syntax.
Require Import Logic.ModalLogic.Syntax.
Require Import Logic.SeparationLogic.Syntax.
Require Import Logic.MinimunLogic.ProofTheory.Minimun.
Require Import Logic.MinimunLogic.ProofTheory.RewriteClass.
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.ProofTheory.ModalLogic.
Require Import Logic.ModalLogic.ProofTheory.RewriteClass.
Require Import Logic.SeparationLogic.ProofTheory.SeparationLogic.
Require Import Logic.SeparationLogic.ProofTheory.DerivedRules.

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

Class SeparationTransparentModality1 (L: Language) {minL: MinimunLanguage L} {pL: PropositionalLanguage L} {mL: ModalLanguage L} {sL: SeparationLanguage L} (Gamma: ProofTheory L) {minAX: MinimunAxiomatization L Gamma} {ipGamma: IntuitionisticPropositionalLogic L Gamma} {KmGamma: SystemK L Gamma} {sGamma: SeparationLogic L Gamma} := {
  sepcon_boxp: forall x y, |-- boxp x * boxp y --> boxp (x * y)
}.

Class SeparationTransparentModality2 (L: Language) {minL: MinimunLanguage L} {pL: PropositionalLanguage L} {mL: ModalLanguage L} {sL: SeparationLanguage L} (Gamma: ProofTheory L) {minAX: MinimunAxiomatization L Gamma} {ipGamma: IntuitionisticPropositionalLogic L Gamma} {KmGamma: SystemK L Gamma} {sGamma: SeparationLogic L Gamma} := {
  boxp_sepcon: forall x y, |-- boxp (x * y) --> boxp x * boxp y
}.

Class SeparationTransparentModality3 (L: Language) {minL: MinimunLanguage L} {pL: PropositionalLanguage L} {mL: ModalLanguage L} {sL: SeparationLanguage L} (Gamma: ProofTheory L) {minAX: MinimunAxiomatization L Gamma} {ipGamma: IntuitionisticPropositionalLogic L Gamma} {KmGamma: SystemK L Gamma} {sGamma: SeparationLogic L Gamma} := {
  wand_boxp: forall x y, |-- (boxp x -* boxp y) --> boxp (x -* y)
}.

Class SeparationTransparentModality4 (L: Language) {minL: MinimunLanguage L} {pL: PropositionalLanguage L} {mL: ModalLanguage L} {sL: SeparationLanguage L} (Gamma: ProofTheory L) {minAX: MinimunAxiomatization L Gamma} {ipGamma: IntuitionisticPropositionalLogic L Gamma} {KmGamma: SystemK L Gamma} {sGamma: SeparationLogic L Gamma} := {
  boxp_wand: forall x y, |-- boxp (x -* y) --> (boxp x -* boxp y)
}.

Instance SeparationTransparentModality14 (L: Language) {minL: MinimunLanguage L} {pL: PropositionalLanguage L} {mL: ModalLanguage L} {sL: SeparationLanguage L} (Gamma: ProofTheory L) {minAX: MinimunAxiomatization L Gamma} {ipGamma: IntuitionisticPropositionalLogic L Gamma} {KmGamma: SystemK L Gamma} {sGamma: SeparationLogic L Gamma} {sm1Gamma: SeparationTransparentModality1 L Gamma}:
  SeparationTransparentModality4 L Gamma.
Proof.
(* Goal: @SeparationTransparentModality1 L minL pL mL sL Gamma minAX ipGamma KmGamma sGamma *)
  constructor.
(* Goal: forall x y : @expr L, @provable L Gamma (@impp L minL (@sepcon L sL (@boxp L mL x) (@boxp L mL y)) (@boxp L mL (@sepcon L sL x y))) *)
  intros.
(* Goal: @provable L Gamma (@impp L minL x (@wand L sL y (@sepcon L sL x y))) *)
  apply wand_sepcon_adjoint.
(* Goal: @provable L Gamma (@impp L minL (@sepcon L sL (@boxp L mL (@wand L sL x y)) (@boxp L mL x)) (@boxp L mL y)) *)
  rewrite sepcon_boxp.
(* Goal: @provable L Gamma (@impp L minL (@boxp L mL (@sepcon L sL (@wand L sL x y) x)) (@boxp L mL y)) *)
  rewrite provable_wand_sepcon_modus_ponens1.
(* Goal: @provable L Gamma (@impp L minL (@sepcon L sL x y) (@sepcon L sL x y)) *)
  apply provable_impp_refl.
Qed.

Instance SeparationTransparentModality41 (L: Language) {minL: MinimunLanguage L} {pL: PropositionalLanguage L} {mL: ModalLanguage L} {sL: SeparationLanguage L} (Gamma: ProofTheory L) {minAX: MinimunAxiomatization L Gamma} {ipGamma: IntuitionisticPropositionalLogic L Gamma} {KmGamma: SystemK L Gamma} {sGamma: SeparationLogic L Gamma} {sm3Gamma: SeparationTransparentModality4 L Gamma}:
  SeparationTransparentModality1 L Gamma.
Proof.
(* Goal: @SeparationTransparentModality1 L minL pL mL sL Gamma minAX ipGamma KmGamma sGamma *)
  constructor.
(* Goal: forall x y : @expr L, @provable L Gamma (@impp L minL (@sepcon L sL (@boxp L mL x) (@boxp L mL y)) (@boxp L mL (@sepcon L sL x y))) *)
  intros.
(* Goal: @provable L Gamma (@impp L minL x (@wand L sL y (@sepcon L sL x y))) *)
  apply wand_sepcon_adjoint.
(* Goal: @provable L Gamma (@impp L minL (@boxp L mL x) (@wand L sL (@boxp L mL y) (@boxp L mL (@sepcon L sL x y)))) *)
  rewrite <- boxp_wand.
(* Goal: @provable L Gamma (@impp L minL (@boxp L mL x) (@boxp L mL (@wand L sL y (@sepcon L sL x y)))) *)
  eapply modus_ponens; [apply axiom_K |].
(* Goal: @provable L Gamma (@boxp L mL (@impp L minL x (@wand L sL y (@sepcon L sL x y)))) *)
  apply rule_N.
(* Goal: @provable L Gamma (@impp L minL x (@wand L sL y (@sepcon L sL x y))) *)
  apply wand_sepcon_adjoint.
(* Goal: @provable L Gamma (@impp L minL (@sepcon L sL x y) (@sepcon L sL x y)) *)
  apply provable_impp_refl.
Qed.
