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.ProofTheoryPatterns.
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.PropositionalLogic.ProofTheory.ProofTheoryPatterns.
Require Import Logic.SeparationLogic.Syntax.

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

Class SeparationLogic
        (L: Language)
        {minL: MinimunLanguage L}
        {pL: PropositionalLanguage L}
        {sL: SeparationLanguage L}
        (Gamma: ProofTheory L)
        {minAX: MinimunAxiomatization L Gamma}
        {ipGamma: IntuitionisticPropositionalLogic L Gamma} := {
  sepcon_comm_impp: forall x y, |-- x * y --> y * x;
  sepcon_assoc: forall x y z, |-- x * (y * z) <--> (x * y) * z;
  wand_sepcon_adjoint: forall x y z, |-- x * y --> z <-> |-- x --> (y -* z)
}.

Class EmpSeparationLogic
        (L: Language)
        {minL: MinimunLanguage L}
        {pL: PropositionalLanguage L}
        {sL: SeparationLanguage L}
        {s'L: SeparationEmpLanguage L}
        (Gamma: ProofTheory L)
        {minAX: MinimunAxiomatization L Gamma}
        {ipGamma: IntuitionisticPropositionalLogic L Gamma}
        {sGamma: SeparationLogic L Gamma} := {
  sepcon_emp: forall x, |-- x * emp <--> x
}.

Class ExtSeparationLogic
        (L: Language)
        {minL: MinimunLanguage L}
        {pL: PropositionalLanguage L}
        {sL: SeparationLanguage L}
        (Gamma: ProofTheory L)
        {minAX: MinimunAxiomatization L Gamma}
        {ipGamma: IntuitionisticPropositionalLogic L Gamma}
        {sGamma: SeparationLogic L Gamma} := {
  sepcon_ext: forall x, |-- x --> x * TT
}.

Class NonsplitEmpSeparationLogic
        (L: Language)
        {minL: MinimunLanguage L}
        {pL: PropositionalLanguage L}
        {sL: SeparationLanguage L}
        {s'L: SeparationEmpLanguage L}
        (Gamma: ProofTheory L)
        {minAX: MinimunAxiomatization L Gamma}
        {ipGamma: IntuitionisticPropositionalLogic L Gamma}
        {sGamma: SeparationLogic L Gamma}
        {eGamma: EmpSeparationLogic L Gamma} := {
  emp_sepcon_truep_elim: forall x, |-- x * TT && emp --> x
}.

Class DupEmpSeparationLogic
        (L: Language)
        {minL: MinimunLanguage L}
        {pL: PropositionalLanguage L}
        {sL: SeparationLanguage L}
        {s'L: SeparationEmpLanguage L}
        (Gamma: ProofTheory L)
        {minAX: MinimunAxiomatization L Gamma}
        {ipGamma: IntuitionisticPropositionalLogic L Gamma}
        {sGamma: SeparationLogic L Gamma}
        {eGamma: EmpSeparationLogic L Gamma} := {
  emp_dup: forall x, |-- x && emp --> x * x
}.

Class MallocFreeSeparationLogic
        (L: Language)
        {minL: MinimunLanguage L}
        {pL: PropositionalLanguage L}
        {sL: SeparationLanguage L}
        {s'L: SeparationEmpLanguage L}
        (Gamma: ProofTheory L)
        {minAX: MinimunAxiomatization L Gamma}
        {ipGamma: IntuitionisticPropositionalLogic L Gamma}
        {sGamma: SeparationLogic L Gamma}
        {eGamma: EmpSeparationLogic L Gamma} := {
  MallocFreeSeparationLogic_NonsplitEmpSeparationLogic :>
    NonsplitEmpSeparationLogic L Gamma;
  MallocFreeSeparationLogic_DupEmpSeparationLogic :>
    DupEmpSeparationLogic L Gamma
}.

Class GarbageCollectSeparationLogic
        (L: Language)
        {minL: MinimunLanguage L}
        {pL: PropositionalLanguage L}
        {sL: SeparationLanguage L}
        (Gamma: ProofTheory L)
        {minAX: MinimunAxiomatization L Gamma}
        {ipGamma: IntuitionisticPropositionalLogic L Gamma}
        {sGamma: SeparationLogic L Gamma} := {
  sepcon_elim1: forall x y, |-- x * y --> x
}.

Section DerivableRules.

Context {L: Language}
        {minL: MinimunLanguage L}
        {pL: PropositionalLanguage L}
        {sL: SeparationLanguage L}
        {Gamma: ProofTheory L}
        {minAX: MinimunAxiomatization L Gamma}
        {ipGamma: IntuitionisticPropositionalLogic L Gamma}
        {sGamma: SeparationLogic L Gamma}.

Lemma wand_sepcon_Adj: Adjointness L Gamma sepcon wand.
Proof.
(* Goal: @Commutativity L minL Gamma (@sepcon L sL) *)
  constructor.
(* Goal: forall (s'L : @SeparationEmpLanguage L sL) (eGamma : @EmpSeparationLogic L minL pL sL s'L Gamma minAX ipGamma sGamma) (_ : @NonsplitEmpSeparationLogic L minL pL sL s'L Gamma minAX ipGamma sGamma eGamma) (x y : @expr L), @provable L Gamma (@impp L minL (@andp L pL (@sepcon L sL x y) (@emp L sL s'L)) y) *)
  intros.
(* Goal: iff (@provable L Gamma (@impp L minL (@sepcon L sL x y) z)) (@provable L Gamma (@impp L minL x (@wand L sL y z))) *)
  apply wand_sepcon_adjoint.
Qed.

Lemma sepcon_orp_distr_l: forall (x y z: expr),
  |-- (x || y) * z <--> x * z || y * z.
Proof.
(* Goal: forall (s'L : @SeparationEmpLanguage L sL) (eGamma : @EmpSeparationLogic L minL pL sL s'L Gamma minAX ipGamma sGamma) (_ : @NonsplitEmpSeparationLogic L minL pL sL s'L Gamma minAX ipGamma sGamma eGamma) (x y : @expr L), @provable L Gamma (@impp L minL (@andp L pL (@sepcon L sL x y) (@emp L sL s'L)) y) *)
  intros.
(* Goal: @provable L Gamma (@iffp L minL pL (@sepcon L sL (@orp L pL x y) z) (@orp L pL (@sepcon L sL x z) (@sepcon L sL y z))) *)
  apply (@prodp_orp_distr_l _ _ _ _ _ _ _ _ wand_sepcon_Adj).
Qed.

Lemma falsep_sepcon: forall (x: expr),
  |-- FF * x <--> FF.
Proof.
(* Goal: forall (s'L : @SeparationEmpLanguage L sL) (eGamma : @EmpSeparationLogic L minL pL sL s'L Gamma minAX ipGamma sGamma) (_ : @NonsplitEmpSeparationLogic L minL pL sL s'L Gamma minAX ipGamma sGamma eGamma) (x y : @expr L), @provable L Gamma (@impp L minL (@andp L pL (@sepcon L sL x y) (@emp L sL s'L)) y) *)
  intros.
(* Goal: @provable L Gamma (@iffp L minL pL (@sepcon L sL (@falsep L pL) x) (@falsep L pL)) *)
  apply (@falsep_prodp _ _ _ _ _ _ _ _ wand_sepcon_Adj).
Qed.

Lemma provable_wand_sepcon_modus_ponens1: forall (x y: expr),
  |-- (x -* y) * x --> y.
Proof.
(* Goal: forall (s'L : @SeparationEmpLanguage L sL) (eGamma : @EmpSeparationLogic L minL pL sL s'L Gamma minAX ipGamma sGamma) (_ : @NonsplitEmpSeparationLogic L minL pL sL s'L Gamma minAX ipGamma sGamma eGamma) (x y : @expr L), @provable L Gamma (@impp L minL (@andp L pL (@sepcon L sL x y) (@emp L sL s'L)) y) *)
  intros.
(* Goal: @provable L Gamma (@impp L minL (@sepcon L sL (@wand L sL x y) x) y) *)
  apply (@adjoint_modus_ponens _ _ _ _ _ _ wand_sepcon_Adj).
Qed.

Lemma wand_andp: forall x y z: expr,
  |-- x -* y && z <--> (x -* y) && (x -* z).
Proof.
(* Goal: forall (s'L : @SeparationEmpLanguage L sL) (eGamma : @EmpSeparationLogic L minL pL sL s'L Gamma minAX ipGamma sGamma) (_ : @NonsplitEmpSeparationLogic L minL pL sL s'L Gamma minAX ipGamma sGamma eGamma) (x y : @expr L), @provable L Gamma (@impp L minL (@andp L pL (@sepcon L sL x y) (@emp L sL s'L)) y) *)
  intros.
(* Goal: @provable L Gamma (@iffp L minL pL (@wand L sL x (@andp L pL y z)) (@andp L pL (@wand L sL x y) (@wand L sL x z))) *)
  apply (@funcp_andp_distr_r _ _ _ _ _ _ _ _ wand_sepcon_Adj); auto.
Qed.

Lemma sepcon_Comm: Commutativity L Gamma sepcon.
Proof.
(* Goal: @Commutativity L minL Gamma (@sepcon L sL) *)
  constructor.
(* Goal: forall (s'L : @SeparationEmpLanguage L sL) (eGamma : @EmpSeparationLogic L minL pL sL s'L Gamma minAX ipGamma sGamma) (_ : @NonsplitEmpSeparationLogic L minL pL sL s'L Gamma minAX ipGamma sGamma eGamma) (x y : @expr L), @provable L Gamma (@impp L minL (@andp L pL (@sepcon L sL x y) (@emp L sL s'L)) y) *)
  intros.
(* Goal: @provable L Gamma (@impp L minL (@sepcon L sL x y) (@sepcon L sL y x)) *)
  apply sepcon_comm_impp.
Qed.

Lemma sepcon_comm: forall (x y: expr),
  |-- x * y <--> y * x.
Proof.
(* Goal: forall (s'L : @SeparationEmpLanguage L sL) (eGamma : @EmpSeparationLogic L minL pL sL s'L Gamma minAX ipGamma sGamma) (_ : @NonsplitEmpSeparationLogic L minL pL sL s'L Gamma minAX ipGamma sGamma eGamma) (x y : @expr L), @provable L Gamma (@impp L minL (@andp L pL (@sepcon L sL x y) (@emp L sL s'L)) y) *)
  intros.
(* Goal: @provable L Gamma (@iffp L minL pL (@sepcon L sL x y) (@sepcon L sL y x)) *)
  apply (@prodp_comm _ _ _ _ _ _ _ sepcon_Comm).
Qed.

Lemma sepcon_orp_distr_r: forall (x y z: expr),
  |-- x * (y || z) <--> x * y || x * z.
Proof.
(* Goal: forall (s'L : @SeparationEmpLanguage L sL) (eGamma : @EmpSeparationLogic L minL pL sL s'L Gamma minAX ipGamma sGamma) (_ : @NonsplitEmpSeparationLogic L minL pL sL s'L Gamma minAX ipGamma sGamma eGamma) (x y : @expr L), @provable L Gamma (@impp L minL (@andp L pL (@sepcon L sL x y) (@emp L sL s'L)) y) *)
  intros.
(* Goal: @provable L Gamma (@iffp L minL pL (@sepcon L sL x (@orp L pL y z)) (@orp L pL (@sepcon L sL x y) (@sepcon L sL x z))) *)
  apply (@prodp_orp_distr_r _ _ _ _ _ _ _ _ wand_sepcon_Adj sepcon_Comm).
Qed.

Lemma sepcon_falsep: forall (x: expr),
  |-- x * FF <--> FF.
Proof.
(* Goal: forall (s'L : @SeparationEmpLanguage L sL) (eGamma : @EmpSeparationLogic L minL pL sL s'L Gamma minAX ipGamma sGamma) (_ : @NonsplitEmpSeparationLogic L minL pL sL s'L Gamma minAX ipGamma sGamma eGamma) (x y : @expr L), @provable L Gamma (@impp L minL (@andp L pL (@sepcon L sL x y) (@emp L sL s'L)) y) *)
  intros.
(* Goal: @provable L Gamma (@iffp L minL pL (@sepcon L sL x (@falsep L pL)) (@falsep L pL)) *)
  apply (@prodp_falsep _ _ _ _ _ _ _ _ wand_sepcon_Adj sepcon_Comm).
Qed.

Lemma provable_wand_sepcon_modus_ponens2: forall (x y: expr),
  |-- x * (x -* y) --> y.
Proof.
(* Goal: forall (s'L : @SeparationEmpLanguage L sL) (eGamma : @EmpSeparationLogic L minL pL sL s'L Gamma minAX ipGamma sGamma) (_ : @NonsplitEmpSeparationLogic L minL pL sL s'L Gamma minAX ipGamma sGamma eGamma) (x y : @expr L), @provable L Gamma (@impp L minL (@andp L pL (@sepcon L sL x y) (@emp L sL s'L)) y) *)
  intros.
(* Goal: @provable L Gamma (@impp L minL (@sepcon L sL x (@wand L sL x y)) y) *)
  rewrite (sepcon_comm x (x -* y)).
(* Goal: @provable L Gamma (@impp L minL (@sepcon L sL (@wand L sL x y) x) y) *)
  apply provable_wand_sepcon_modus_ponens1.
Qed.

Lemma wand_mono: forall x1 x2 y1 y2, |-- x2 --> x1 -> |-- y1 --> y2 -> |-- (x1 -* y1) --> (x2 -* y2).
Proof.
(* Goal: forall (s'L : @SeparationEmpLanguage L sL) (eGamma : @EmpSeparationLogic L minL pL sL s'L Gamma minAX ipGamma sGamma) (_ : @NonsplitEmpSeparationLogic L minL pL sL s'L Gamma minAX ipGamma sGamma eGamma) (x y : @expr L), @provable L Gamma (@impp L minL (@andp L pL (@sepcon L sL x y) (@emp L sL s'L)) y) *)
  intros.
(* Goal: @provable L Gamma (@impp L minL (@wand L sL x1 y1) (@wand L sL x2 y2)) *)
  apply (@funcp_mono _ _ _ _ _ _ wand_sepcon_Adj sepcon_Comm); auto.
Qed.

Lemma orp_wand: forall x y z: expr,
  |-- (x || y) -* z <--> (x -* z) && (y -* z).
Proof.
(* Goal: forall (s'L : @SeparationEmpLanguage L sL) (eGamma : @EmpSeparationLogic L minL pL sL s'L Gamma minAX ipGamma sGamma) (_ : @NonsplitEmpSeparationLogic L minL pL sL s'L Gamma minAX ipGamma sGamma eGamma) (x y : @expr L), @provable L Gamma (@impp L minL (@andp L pL (@sepcon L sL x y) (@emp L sL s'L)) y) *)
  intros.
(* Goal: @provable L Gamma (@iffp L minL pL (@wand L sL (@orp L pL x y) z) (@andp L pL (@wand L sL x z) (@wand L sL y z))) *)
  apply (@orp_funcp _ _ _ _ _ _ _ _ wand_sepcon_Adj sepcon_Comm); auto.
Qed.

Lemma sepcon_Mono: Monotonicity L Gamma sepcon.
Proof.
(* Goal: @Monotonicity L minL Gamma (@sepcon L sL) *)
  apply @Adjoint2Mono with (funcp := wand).
  + auto.
  + apply wand_sepcon_Adj.
  + apply sepcon_Comm.
Qed.

Lemma sepcon_mono: forall x1 x2 y1 y2, |-- x1 --> x2 -> |-- y1 --> y2 -> |-- (x1 * y1) --> (x2 * y2).
Proof.
(* Goal: forall (s'L : @SeparationEmpLanguage L sL) (eGamma : @EmpSeparationLogic L minL pL sL s'L Gamma minAX ipGamma sGamma) (_ : @NonsplitEmpSeparationLogic L minL pL sL s'L Gamma minAX ipGamma sGamma eGamma) (x y : @expr L), @provable L Gamma (@impp L minL (@andp L pL (@sepcon L sL x y) (@emp L sL s'L)) y) *)
  intros.
(* Goal: @MinimunAxiomatization L minL Gamma *)
  apply (@prodp_mono _ _ _ _ sepcon_Mono); auto.
Qed.

Lemma sepcon_Assoc: Associativity L Gamma sepcon.
Proof.
(* Goal: @Associativity L minL Gamma (@sepcon L sL) *)
  apply Build_Associativity'.
(* Goal: forall (s'L : @SeparationEmpLanguage L sL) (eGamma : @EmpSeparationLogic L minL pL sL s'L Gamma minAX ipGamma sGamma) (_ : @NonsplitEmpSeparationLogic L minL pL sL s'L Gamma minAX ipGamma sGamma eGamma) (x y : @expr L), @provable L Gamma (@impp L minL (@andp L pL (@sepcon L sL x y) (@emp L sL s'L)) y) *)
  intros.
(* Goal: @provable L Gamma (@iffp L minL pL (@sepcon L sL (@sepcon L sL x y) z) (@sepcon L sL x (@sepcon L sL y z))) *)
  rewrite sepcon_assoc.
(* Goal: @provable L Gamma (@iffp L minL pL (@sepcon L sL (@sepcon L sL x y) z) (@sepcon L sL (@sepcon L sL x y) z)) *)
  apply provable_iffp_refl.
Qed.

Lemma sepcon_LU {s'L: SeparationEmpLanguage L} {eGamma: EmpSeparationLogic L Gamma}: LeftUnit L Gamma emp sepcon.
Proof.
(* Goal: @LeftUnit L minL Gamma (@emp L sL s'L) (@sepcon L sL) *)
  apply Build_LeftUnit'.
(* Goal: forall (s'L : @SeparationEmpLanguage L sL) (eGamma : @EmpSeparationLogic L minL pL sL s'L Gamma minAX ipGamma sGamma) (_ : @NonsplitEmpSeparationLogic L minL pL sL s'L Gamma minAX ipGamma sGamma eGamma) (x y : @expr L), @provable L Gamma (@impp L minL (@andp L pL (@sepcon L sL x y) (@emp L sL s'L)) y) *)
  intros.
(* Goal: @provable L Gamma (@impp L minL (@andp L pL (@sepcon L sL x y) (@emp L sL s'L)) y) *)
  rewrite sepcon_comm.
(* Goal: @provable L Gamma (@iffp L minL pL (@sepcon L sL x (@emp L sL s'L)) x) *)
  apply sepcon_emp.
Qed.

Lemma sepcon_RU {s'L: SeparationEmpLanguage L} {eGamma: EmpSeparationLogic L Gamma}: RightUnit L Gamma emp sepcon.
Proof.
(* Goal: @RightUnit L minL Gamma (@emp L sL s'L) (@sepcon L sL) *)
  apply Build_RightUnit'.
(* Goal: forall (s'L : @SeparationEmpLanguage L sL) (eGamma : @EmpSeparationLogic L minL pL sL s'L Gamma minAX ipGamma sGamma) (_ : @NonsplitEmpSeparationLogic L minL pL sL s'L Gamma minAX ipGamma sGamma eGamma) (x y : @expr L), @provable L Gamma (@impp L minL (@andp L pL (@sepcon L sL x y) (@emp L sL s'L)) y) *)
  intros.
(* Goal: @provable L Gamma (@iffp L minL pL (@sepcon L sL x (@emp L sL s'L)) x) *)
  apply sepcon_emp.
Qed.

Lemma sepcon_elim2: forall {gcsGamma: GarbageCollectSeparationLogic L Gamma} (x y: expr),
  |-- x * y --> y.
Proof.
(* Goal: forall (s'L : @SeparationEmpLanguage L sL) (eGamma : @EmpSeparationLogic L minL pL sL s'L Gamma minAX ipGamma sGamma) (_ : @NonsplitEmpSeparationLogic L minL pL sL s'L Gamma minAX ipGamma sGamma eGamma) (x y : @expr L), @provable L Gamma (@impp L minL (@andp L pL (@sepcon L sL x y) (@emp L sL s'L)) y) *)
  intros.
(* Goal: @provable L Gamma (@impp L minL (@sepcon L sL x y) y) *)
  rewrite (sepcon_comm x y).
(* Goal: @provable L Gamma (@impp L minL (@sepcon L sL y x) y) *)
  apply sepcon_elim1.
Qed.

Lemma emp_sepcon_elim1: forall {s'L: SeparationEmpLanguage L} {eGamma: EmpSeparationLogic L Gamma} {nssGamma: NonsplitEmpSeparationLogic L Gamma} x y,
  |-- x * y && emp --> x.
Proof.
(* Goal: forall (s'L : @SeparationEmpLanguage L sL) (eGamma : @EmpSeparationLogic L minL pL sL s'L Gamma minAX ipGamma sGamma) (_ : @NonsplitEmpSeparationLogic L minL pL sL s'L Gamma minAX ipGamma sGamma eGamma) (x y : @expr L), @provable L Gamma (@impp L minL (@andp L pL (@sepcon L sL x y) (@emp L sL s'L)) y) *)
  intros.
(* Goal: @provable L Gamma (@impp L minL (@andp L pL (@sepcon L sL x y) (@emp L sL s'L)) x) *)
  rewrite <- (emp_sepcon_truep_elim x) at 2.
(* Goal: @provable L Gamma (@impp L minL (@andp L pL (@sepcon L sL x y) (@emp L sL s'L)) (@andp L pL (@sepcon L sL x (@truep L minL pL)) (@emp L sL s'L))) *)
  apply andp_proper_impp; [| apply provable_impp_refl].
(* Goal: @provable L Gamma (@impp L minL (@sepcon L sL x y) (@sepcon L sL x (@truep L minL pL))) *)
  apply sepcon_mono; [apply provable_impp_refl |].
(* Goal: @provable L Gamma (@impp L minL y (@truep L minL pL)) *)
  apply solve_impp_elim_left, provable_truep.
Qed.

Lemma emp_sepcon_elim2: forall {s'L: SeparationEmpLanguage L} {eGamma: EmpSeparationLogic L Gamma} {nssGamma: NonsplitEmpSeparationLogic L Gamma} x y,
  |-- x * y && emp --> y.
Proof.
(* Goal: forall (s'L : @SeparationEmpLanguage L sL) (eGamma : @EmpSeparationLogic L minL pL sL s'L Gamma minAX ipGamma sGamma) (_ : @NonsplitEmpSeparationLogic L minL pL sL s'L Gamma minAX ipGamma sGamma eGamma) (x y : @expr L), @provable L Gamma (@impp L minL (@andp L pL (@sepcon L sL x y) (@emp L sL s'L)) y) *)
  intros.
(* Goal: @provable L Gamma (@impp L minL (@andp L pL (@sepcon L sL x y) (@emp L sL s'L)) y) *)
  rewrite sepcon_comm.
(* Goal: @provable L Gamma (@impp L minL (@andp L pL (@sepcon L sL y x) (@emp L sL s'L)) y) *)
  apply emp_sepcon_elim1.
Qed.

End DerivableRules.
