Require Import Logic.GeneralLogic.Base.
Require Import Logic.MinimunLogic.Syntax.
Require Import Logic.MinimunLogic.ProofTheory.Minimun.
Require Import Logic.MinimunLogic.ProofTheory.RewriteClass.
Require Import Logic.MinimunLogic.Syntax.
Require Import Logic.MinimunLogic.ProofTheory.Minimun.
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.SeparationLogic.Syntax.
Require Import Logic.SeparationLogic.ProofTheory.SeparationLogic.
Require Import Logic.SeparationLogic.DeepEmbedded.Parameter.
Require Logic.SeparationLogic.DeepEmbedded.SeparationLanguage.
Require Logic.SeparationLogic.DeepEmbedded.SeparationEmpLanguage.

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

Module ReynoldsLogic.
Section ReynoldsLogic.

Context {Sigma: SeparationLanguage.PropositionalVariables}.

Existing Instances SeparationLanguage.L SeparationLanguage.minL SeparationLanguage.pL SeparationLanguage.sL.

Inductive provable: SeparationLanguage.expr Sigma -> Prop :=
| modus_ponens: forall x y, provable (x --> y) -> provable x -> provable y
| axiom1: forall x y, provable (x --> (y --> x))
| axiom2: forall x y z, provable ((x --> y --> z) --> (x --> y) --> (x --> z))
| andp_intros: forall x y, provable (x --> y --> x && y)
| andp_elim1: forall x y, provable (x && y --> x)
| andp_elim2: forall x y, provable (x && y --> y)
| orp_intros1: forall x y, provable (x --> x || y)
| orp_intros2: forall x y, provable (y --> x || y)
| orp_elim: forall x y z, provable ((x --> z) --> (y --> z) --> (x || y --> z))
| falsep_elim: forall x, provable (FF --> x)
| sepcon_comm: forall x y, provable (x * y --> y * x)
| sepcon_assoc: forall x y z, provable (x * (y * z) <--> (x * y) * z)
| wand_sepcon_adjoint1: forall x y z, provable (x * y --> z) -> provable (x --> (y -* z))
| wand_sepcon_adjoint2: forall x y z, provable (x --> (y -* z)) -> provable (x * y --> z)
| sepcon_elim1: forall x y, provable (x * y --> x).

Instance G: ProofTheory SeparationLanguage.L := Build_AxiomaticProofTheory provable.

Instance AX: NormalAxiomatization SeparationLanguage.L G := Build_AxiomaticProofTheory_AX provable.

Instance minAX: MinimunAxiomatization SeparationLanguage.L G.
Proof.
(* Goal: @EmpSeparationLogic (@SeparationEmpLanguage.L Sigma) (@SeparationEmpLanguage.minL Sigma) (@SeparationEmpLanguage.pL Sigma) (@SeparationEmpLanguage.sL Sigma) (@SeparationEmpLanguage.s'L Sigma) G minAX ipG sG *)
  constructor.
  + apply modus_ponens.
  + apply axiom1.
  + apply axiom2.
Qed.

Instance ipG: IntuitionisticPropositionalLogic SeparationLanguage.L G.
Proof.
(* Goal: @EmpSeparationLogic (@SeparationEmpLanguage.L Sigma) (@SeparationEmpLanguage.minL Sigma) (@SeparationEmpLanguage.pL Sigma) (@SeparationEmpLanguage.sL Sigma) (@SeparationEmpLanguage.s'L Sigma) G minAX ipG sG *)
  constructor.
  + apply andp_intros.
  + apply andp_elim1.
  + apply andp_elim2.
  + apply orp_intros1.
  + apply orp_intros2.
  + apply orp_elim.
  + apply falsep_elim.
Qed.

Instance sG: SeparationLogic SeparationLanguage.L G.
Proof.
(* Goal: @EmpSeparationLogic (@SeparationEmpLanguage.L Sigma) (@SeparationEmpLanguage.minL Sigma) (@SeparationEmpLanguage.pL Sigma) (@SeparationEmpLanguage.sL Sigma) (@SeparationEmpLanguage.s'L Sigma) G minAX ipG sG *)
  constructor.
  + apply sepcon_comm.
  + apply sepcon_assoc.
  + intros; split.
    - apply wand_sepcon_adjoint1.
    - apply wand_sepcon_adjoint2.
Qed.

Instance gcsG: GarbageCollectSeparationLogic SeparationLanguage.L G.
Proof.
(* Goal: @EmpSeparationLogic (@SeparationEmpLanguage.L Sigma) (@SeparationEmpLanguage.minL Sigma) (@SeparationEmpLanguage.pL Sigma) (@SeparationEmpLanguage.sL Sigma) (@SeparationEmpLanguage.s'L Sigma) G minAX ipG sG *)
  constructor.
(* Goal: forall x y : @expr (@SeparationLanguage.L Sigma), @Base.provable (@SeparationLanguage.L Sigma) G (@impp (@SeparationLanguage.L Sigma) (@SeparationLanguage.minL Sigma) (@sepcon (@SeparationLanguage.L Sigma) (@SeparationLanguage.sL Sigma) x y) x) *)
  apply sepcon_elim1.
Qed.

End ReynoldsLogic.
End ReynoldsLogic.

Module OHearnLogic.
Section OHearnLogic.

Context {Sigma: SeparationEmpLanguage.PropositionalVariables}.

Existing Instances SeparationEmpLanguage.L SeparationEmpLanguage.minL SeparationEmpLanguage.pL SeparationEmpLanguage.sL SeparationEmpLanguage.s'L.

Inductive provable: SeparationEmpLanguage.expr Sigma -> Prop :=
| modus_ponens: forall x y, provable (x --> y) -> provable x -> provable y
| axiom1: forall x y, provable (x --> (y --> x))
| axiom2: forall x y z, provable ((x --> y --> z) --> (x --> y) --> (x --> z))
| andp_intros: forall x y, provable (x --> y --> x && y)
| andp_elim1: forall x y, provable (x && y --> x)
| andp_elim2: forall x y, provable (x && y --> y)
| orp_intros1: forall x y, provable (x --> x || y)
| orp_intros2: forall x y, provable (y --> x || y)
| orp_elim: forall x y z, provable ((x --> z) --> (y --> z) --> (x || y --> z))
| falsep_elim: forall x, provable (FF --> x)
| excluded_middle: forall x, provable (x || ~~ x)
| sepcon_comm: forall x y, provable (x * y --> y * x)
| sepcon_assoc: forall x y z, provable (x * (y * z) <--> (x * y) * z)
| wand_sepcon_adjoint1: forall x y z, provable (x * y --> z) -> provable (x --> (y -* z))
| wand_sepcon_adjoint2: forall x y z, provable (x --> (y -* z)) -> provable (x * y --> z)
| sepcon_emp: forall x, provable (x * emp <--> x).

Instance G: ProofTheory SeparationEmpLanguage.L := Build_AxiomaticProofTheory provable.

Instance AX: NormalAxiomatization SeparationEmpLanguage.L G := Build_AxiomaticProofTheory_AX provable.

Instance minAX: MinimunAxiomatization SeparationEmpLanguage.L G.
Proof.
(* Goal: @EmpSeparationLogic (@SeparationEmpLanguage.L Sigma) (@SeparationEmpLanguage.minL Sigma) (@SeparationEmpLanguage.pL Sigma) (@SeparationEmpLanguage.sL Sigma) (@SeparationEmpLanguage.s'L Sigma) G minAX ipG sG *)
  constructor.
  + apply modus_ponens.
  + apply axiom1.
  + apply axiom2.
Qed.

Instance ipG: IntuitionisticPropositionalLogic SeparationEmpLanguage.L G.
Proof.
(* Goal: @EmpSeparationLogic (@SeparationEmpLanguage.L Sigma) (@SeparationEmpLanguage.minL Sigma) (@SeparationEmpLanguage.pL Sigma) (@SeparationEmpLanguage.sL Sigma) (@SeparationEmpLanguage.s'L Sigma) G minAX ipG sG *)
  constructor.
  + apply andp_intros.
  + apply andp_elim1.
  + apply andp_elim2.
  + apply orp_intros1.
  + apply orp_intros2.
  + apply orp_elim.
  + apply falsep_elim.
Qed.

Instance cpG: ClassicalPropositionalLogic SeparationEmpLanguage.L G.
Proof.
(* Goal: @EmpSeparationLogic (@SeparationEmpLanguage.L Sigma) (@SeparationEmpLanguage.minL Sigma) (@SeparationEmpLanguage.pL Sigma) (@SeparationEmpLanguage.sL Sigma) (@SeparationEmpLanguage.s'L Sigma) G minAX ipG sG *)
  constructor.
(* Goal: forall x : @expr (@SeparationEmpLanguage.L Sigma), @Base.provable (@SeparationEmpLanguage.L Sigma) G (@orp (@SeparationEmpLanguage.L Sigma) (@SeparationEmpLanguage.pL Sigma) x (@negp (@SeparationEmpLanguage.L Sigma) (@SeparationEmpLanguage.minL Sigma) (@SeparationEmpLanguage.pL Sigma) x)) *)
  apply excluded_middle.
Qed.

Instance sG: SeparationLogic SeparationEmpLanguage.L G.
Proof.
(* Goal: @EmpSeparationLogic (@SeparationEmpLanguage.L Sigma) (@SeparationEmpLanguage.minL Sigma) (@SeparationEmpLanguage.pL Sigma) (@SeparationEmpLanguage.sL Sigma) (@SeparationEmpLanguage.s'L Sigma) G minAX ipG sG *)
  constructor.
  + apply sepcon_comm.
  + apply sepcon_assoc.
  + intros; split.
    - apply wand_sepcon_adjoint1.
    - apply wand_sepcon_adjoint2.
Qed.

Instance EmpsG: EmpSeparationLogic SeparationEmpLanguage.L G.
Proof.
(* Goal: @EmpSeparationLogic (@SeparationEmpLanguage.L Sigma) (@SeparationEmpLanguage.minL Sigma) (@SeparationEmpLanguage.pL Sigma) (@SeparationEmpLanguage.sL Sigma) (@SeparationEmpLanguage.s'L Sigma) G minAX ipG sG *)
  constructor.
(* Goal: forall x : @expr (@SeparationEmpLanguage.L Sigma), @Base.provable (@SeparationEmpLanguage.L Sigma) G (@iffp (@SeparationEmpLanguage.L Sigma) (@SeparationEmpLanguage.minL Sigma) (@SeparationEmpLanguage.pL Sigma) (@sepcon (@SeparationEmpLanguage.L Sigma) (@SeparationEmpLanguage.sL Sigma) x (@emp (@SeparationEmpLanguage.L Sigma) (@SeparationEmpLanguage.sL Sigma) (@SeparationEmpLanguage.s'L Sigma))) x) *)
  apply sepcon_emp.
Qed.

End OHearnLogic.
End OHearnLogic.

Module LogicOnModuResModel.
Section LogicOnModuResModel.

Context {Sigma: SeparationEmpLanguage.PropositionalVariables}.

Existing Instances SeparationEmpLanguage.L SeparationEmpLanguage.minL SeparationEmpLanguage.pL SeparationEmpLanguage.sL SeparationEmpLanguage.s'L.

Inductive provable: SeparationEmpLanguage.expr Sigma -> Prop :=
| modus_ponens: forall x y, provable (x --> y) -> provable x -> provable y
| axiom1: forall x y, provable (x --> (y --> x))
| axiom2: forall x y z, provable ((x --> y --> z) --> (x --> y) --> (x --> z))
| andp_intros: forall x y, provable (x --> y --> x && y)
| andp_elim1: forall x y, provable (x && y --> x)
| andp_elim2: forall x y, provable (x && y --> y)
| orp_intros1: forall x y, provable (x --> x || y)
| orp_intros2: forall x y, provable (y --> x || y)
| orp_elim: forall x y z, provable ((x --> z) --> (y --> z) --> (x || y --> z))
| falsep_elim: forall x, provable (FF --> x)
| sepcon_comm: forall x y, provable (x * y --> y * x)
| sepcon_assoc: forall x y z, provable (x * (y * z) <--> (x * y) * z)
| wand_sepcon_adjoint1: forall x y z, provable (x * y --> z) -> provable (x --> (y -* z))
| wand_sepcon_adjoint2: forall x y z, provable (x --> (y -* z)) -> provable (x * y --> z)
| sepcon_emp: forall x, provable (x * emp <--> x)
| sepcon_elim1: forall x y, provable (x * y --> x).

Instance G: ProofTheory SeparationEmpLanguage.L := Build_AxiomaticProofTheory provable.

Instance AX: NormalAxiomatization SeparationEmpLanguage.L G := Build_AxiomaticProofTheory_AX provable.

Instance minAX: MinimunAxiomatization SeparationEmpLanguage.L G.
Proof.
(* Goal: @EmpSeparationLogic (@SeparationEmpLanguage.L Sigma) (@SeparationEmpLanguage.minL Sigma) (@SeparationEmpLanguage.pL Sigma) (@SeparationEmpLanguage.sL Sigma) (@SeparationEmpLanguage.s'L Sigma) G minAX ipG sG *)
  constructor.
  + apply modus_ponens.
  + apply axiom1.
  + apply axiom2.
Qed.

Instance ipG: IntuitionisticPropositionalLogic SeparationEmpLanguage.L G.
Proof.
(* Goal: @EmpSeparationLogic (@SeparationEmpLanguage.L Sigma) (@SeparationEmpLanguage.minL Sigma) (@SeparationEmpLanguage.pL Sigma) (@SeparationEmpLanguage.sL Sigma) (@SeparationEmpLanguage.s'L Sigma) G minAX ipG sG *)
  constructor.
  + apply andp_intros.
  + apply andp_elim1.
  + apply andp_elim2.
  + apply orp_intros1.
  + apply orp_intros2.
  + apply orp_elim.
  + apply falsep_elim.
Qed.

Instance sG: SeparationLogic SeparationEmpLanguage.L G.
Proof.
(* Goal: @EmpSeparationLogic (@SeparationEmpLanguage.L Sigma) (@SeparationEmpLanguage.minL Sigma) (@SeparationEmpLanguage.pL Sigma) (@SeparationEmpLanguage.sL Sigma) (@SeparationEmpLanguage.s'L Sigma) G minAX ipG sG *)
  constructor.
  + apply sepcon_comm.
  + apply sepcon_assoc.
  + intros; split.
    - apply wand_sepcon_adjoint1.
    - apply wand_sepcon_adjoint2.
Qed.

Instance EmpsG: EmpSeparationLogic SeparationEmpLanguage.L G.
Proof.
(* Goal: @EmpSeparationLogic (@SeparationEmpLanguage.L Sigma) (@SeparationEmpLanguage.minL Sigma) (@SeparationEmpLanguage.pL Sigma) (@SeparationEmpLanguage.sL Sigma) (@SeparationEmpLanguage.s'L Sigma) G minAX ipG sG *)
  constructor.
(* Goal: forall x : @expr (@SeparationEmpLanguage.L Sigma), @Base.provable (@SeparationEmpLanguage.L Sigma) G (@iffp (@SeparationEmpLanguage.L Sigma) (@SeparationEmpLanguage.minL Sigma) (@SeparationEmpLanguage.pL Sigma) (@sepcon (@SeparationEmpLanguage.L Sigma) (@SeparationEmpLanguage.sL Sigma) x (@emp (@SeparationEmpLanguage.L Sigma) (@SeparationEmpLanguage.sL Sigma) (@SeparationEmpLanguage.s'L Sigma))) x) *)
  apply sepcon_emp.
Qed.

Instance gcsG: GarbageCollectSeparationLogic SeparationEmpLanguage.L G.
Proof.
(* Goal: @EmpSeparationLogic (@SeparationEmpLanguage.L Sigma) (@SeparationEmpLanguage.minL Sigma) (@SeparationEmpLanguage.pL Sigma) (@SeparationEmpLanguage.sL Sigma) (@SeparationEmpLanguage.s'L Sigma) G minAX ipG sG *)
  constructor.
(* Goal: forall x y : @expr (@SeparationLanguage.L Sigma), @Base.provable (@SeparationLanguage.L Sigma) G (@impp (@SeparationLanguage.L Sigma) (@SeparationLanguage.minL Sigma) (@sepcon (@SeparationLanguage.L Sigma) (@SeparationLanguage.sL Sigma) x y) x) *)
  apply sepcon_elim1.
Qed.

End LogicOnModuResModel. 
End LogicOnModuResModel.

Module LogicOnMSL.
Section LogicOnMSL.

Context {Sigma: SeparationEmpLanguage.PropositionalVariables}.

Existing Instances SeparationEmpLanguage.L SeparationEmpLanguage.minL SeparationEmpLanguage.pL SeparationEmpLanguage.sL SeparationEmpLanguage.s'L.

Inductive provable: SeparationEmpLanguage.expr Sigma -> Prop :=
| modus_ponens: forall x y, provable (x --> y) -> provable x -> provable y
| axiom1: forall x y, provable (x --> (y --> x))
| axiom2: forall x y z, provable ((x --> y --> z) --> (x --> y) --> (x --> z))
| andp_intros: forall x y, provable (x --> y --> x && y)
| andp_elim1: forall x y, provable (x && y --> x)
| andp_elim2: forall x y, provable (x && y --> y)
| orp_intros1: forall x y, provable (x --> x || y)
| orp_intros2: forall x y, provable (y --> x || y)
| orp_elim: forall x y z, provable ((x --> z) --> (y --> z) --> (x || y --> z))
| falsep_elim: forall x, provable (FF --> x)
| impp_choice: forall x y, provable ((x --> y) || (y --> x))
| sepcon_comm: forall x y, provable (x * y --> y * x)
| sepcon_assoc: forall x y z, provable (x * (y * z) <--> (x * y) * z)
| wand_sepcon_adjoint1: forall x y z, provable (x * y --> z) -> provable (x --> (y -* z))
| wand_sepcon_adjoint2: forall x y z, provable (x --> (y -* z)) -> provable (x * y --> z)
| sepcon_emp: forall x, provable (x * emp <--> x).

Instance G: ProofTheory SeparationEmpLanguage.L := Build_AxiomaticProofTheory provable.

Instance AX: NormalAxiomatization SeparationEmpLanguage.L G := Build_AxiomaticProofTheory_AX provable.

Instance minAX: MinimunAxiomatization SeparationEmpLanguage.L G.
Proof.
(* Goal: @EmpSeparationLogic (@SeparationEmpLanguage.L Sigma) (@SeparationEmpLanguage.minL Sigma) (@SeparationEmpLanguage.pL Sigma) (@SeparationEmpLanguage.sL Sigma) (@SeparationEmpLanguage.s'L Sigma) G minAX ipG sG *)
  constructor.
  + apply modus_ponens.
  + apply axiom1.
  + apply axiom2.
Qed.

Instance ipG: IntuitionisticPropositionalLogic SeparationEmpLanguage.L G.
Proof.
(* Goal: @EmpSeparationLogic (@SeparationEmpLanguage.L Sigma) (@SeparationEmpLanguage.minL Sigma) (@SeparationEmpLanguage.pL Sigma) (@SeparationEmpLanguage.sL Sigma) (@SeparationEmpLanguage.s'L Sigma) G minAX ipG sG *)
  constructor.
  + apply andp_intros.
  + apply andp_elim1.
  + apply andp_elim2.
  + apply orp_intros1.
  + apply orp_intros2.
  + apply orp_elim.
  + apply falsep_elim.
Qed.

Instance sG: SeparationLogic SeparationEmpLanguage.L G.
Proof.
(* Goal: @EmpSeparationLogic (@SeparationEmpLanguage.L Sigma) (@SeparationEmpLanguage.minL Sigma) (@SeparationEmpLanguage.pL Sigma) (@SeparationEmpLanguage.sL Sigma) (@SeparationEmpLanguage.s'L Sigma) G minAX ipG sG *)
  constructor.
  + apply sepcon_comm.
  + apply sepcon_assoc.
  + intros; split.
    - apply wand_sepcon_adjoint1.
    - apply wand_sepcon_adjoint2.
Qed.

Instance EmpsG: EmpSeparationLogic SeparationEmpLanguage.L G.
Proof.
(* Goal: @EmpSeparationLogic (@SeparationEmpLanguage.L Sigma) (@SeparationEmpLanguage.minL Sigma) (@SeparationEmpLanguage.pL Sigma) (@SeparationEmpLanguage.sL Sigma) (@SeparationEmpLanguage.s'L Sigma) G minAX ipG sG *)
  constructor.
(* Goal: forall x : @expr (@SeparationEmpLanguage.L Sigma), @Base.provable (@SeparationEmpLanguage.L Sigma) G (@iffp (@SeparationEmpLanguage.L Sigma) (@SeparationEmpLanguage.minL Sigma) (@SeparationEmpLanguage.pL Sigma) (@sepcon (@SeparationEmpLanguage.L Sigma) (@SeparationEmpLanguage.sL Sigma) x (@emp (@SeparationEmpLanguage.L Sigma) (@SeparationEmpLanguage.sL Sigma) (@SeparationEmpLanguage.s'L Sigma))) x) *)
  apply sepcon_emp.
Qed.


End LogicOnMSL.
End LogicOnMSL.
