Require Import Coq.Logic.Classical_Prop.
Require Import Coq.Classes.RelationClasses.
Require Import Coq.Relations.Relation_Definitions.
Require Import Logic.lib.Coqlib.
Require Import Logic.GeneralLogic.Base.
Require Import Logic.SeparationLogic.Syntax.
Require Import Logic.GeneralLogic.KripkeModel.
Require Import Logic.SeparationLogic.Model.SeparationAlgebra.
Require Import Logic.SeparationLogic.Model.OrderedSA.
Require Import Logic.SeparationLogic.Semantics.WeakSemantics.
Require Import Logic.SeparationLogic.Semantics.StrongSemantics.

Local Open Scope logic_base.
Local Open Scope syntax.
Local Open Scope kripke_model.
Import SeparationLogicNotation.
Import KripkeModelFamilyNotation.
Import KripkeModelNotation_Intuitionistic.

Class SeparatingSemantics
      (L: Language)
      {SL: SeparationLanguage L}
      (MD: Model)
      {kMD: KripkeModel MD}
      (M: Kmodel)
      {R: Relation (Kworlds M)}
      {J: Join (Kworlds M)}
      (SM: Semantics L MD): Type :=
{
  denote_sepcon: forall x y, Same_set _ (Kdenotation M (x * y)) (StrongSemantics.sepcon (Kdenotation M x) (Kdenotation M y));
  denote_wand: forall x y, Same_set _ (Kdenotation M (x -* y)) (WeakSemantics.wand (Kdenotation M x) (Kdenotation M y))
}.

Class EmpSemantics
      (L: Language)
      {sL: SeparationLanguage L}
      {s'L: SeparationEmpLanguage L}
      (MD: Model)
      {kMD: KripkeModel MD}
      (M: Kmodel)
      {R: Relation (Kworlds M)}
      {J: Join (Kworlds M)}
      (SM: Semantics L MD): Type :=
  denote_emp: Same_set _ (Kdenotation M emp) WeakSemantics.emp.

Lemma sat_sepcon
      {L: Language}
      {sL: SeparationLanguage L}
      {MD: Model}
      {kMD: KripkeModel MD}
      {M: Kmodel}
      {R: Relation (Kworlds M)}
      {J: Join (Kworlds M)}
      {SM: Semantics L MD}
      {dsSM: SeparatingSemantics L MD M SM}:
  forall m x y,
    KRIPKE: M , m |= x * y <->
    exists m0 m1 m2, m0 <= m /\
                     join m1 m2 m0 /\
                     KRIPKE: M , m1 |= x /\
                     KRIPKE: M, m2 |= y.
Proof.
(* Goal: forall m : @Kworlds MD kMD M, iff (@satisfies L MD SM (@build_model MD kMD M m) (@emp L sL s'L)) (@increasing (@Kworlds MD kMD M) R J m) *)
  intros; simpl.
(* Goal: iff (@satisfies L MD SM (@build_model MD kMD M m) (@emp L sL s'L)) (@increasing (@Kworlds MD kMD M) R J m) *)
  unfold satisfies.
(* Goal: iff (@denotation L MD SM (@sepcon L sL x y) (@build_model MD kMD M m)) (@ex (@Kworlds MD kMD M) (fun m0 : @Kworlds MD kMD M => @ex (@Kworlds MD kMD M) (fun m1 : @Kworlds MD kMD M => @ex (@Kworlds MD kMD M) (fun m2 : @Kworlds MD kMD M => and (@Krelation (@Kworlds MD kMD M) R m0 m) (and (@join (@Kworlds MD kMD M) J m1 m2 m0) (and (@denotation L MD SM x (@build_model MD kMD M m1)) (@denotation L MD SM y (@build_model MD kMD M m2)))))))) *)
  destruct (denote_sepcon x y).
(* Goal: iff (@denotation L MD SM (@emp L sL s'L) (@build_model MD kMD M m)) (@increasing (@Kworlds MD kMD M) R J m) *)
  split; [apply H | apply H0].
Qed.

Lemma sat_wand
      {L: Language}
      {sL: SeparationLanguage L}
      {MD: Model}
      {kMD: KripkeModel MD}
      {M: Kmodel}
      {R: Relation (Kworlds M)}
      {J: Join (Kworlds M)}
      {SM: Semantics L MD}
      {dsSM: SeparatingSemantics L MD M SM}:
  forall m x y,
    KRIPKE: M , m |= x -* y <->
    forall m1 m2, join m m1 m2 ->
                  KRIPKE: M , m1 |= x ->
                  KRIPKE: M, m2 |= y.
Proof.
(* Goal: forall m : @Kworlds MD kMD M, iff (@satisfies L MD SM (@build_model MD kMD M m) (@emp L sL s'L)) (@increasing (@Kworlds MD kMD M) R J m) *)
  intros; simpl.
(* Goal: iff (@satisfies L MD SM (@build_model MD kMD M m) (@emp L sL s'L)) (@increasing (@Kworlds MD kMD M) R J m) *)
  unfold satisfies.
(* Goal: iff (@denotation L MD SM (@wand L sL x y) (@build_model MD kMD M m)) (forall (m1 m2 : @Kworlds MD kMD M) (_ : @join (@Kworlds MD kMD M) J m m1 m2) (_ : @denotation L MD SM x (@build_model MD kMD M m1)), @denotation L MD SM y (@build_model MD kMD M m2)) *)
  destruct (denote_wand x y).
(* Goal: iff (@denotation L MD SM (@emp L sL s'L) (@build_model MD kMD M m)) (@increasing (@Kworlds MD kMD M) R J m) *)
  split; [apply H | apply H0].
Qed.

Lemma sat_emp
      {L: Language}
      {sL: SeparationLanguage L}
      {s'L: SeparationEmpLanguage L}
      {MD: Model}
      {kMD: KripkeModel MD}
      {M: Kmodel}
      {R: Relation (Kworlds M)}
      {J: Join (Kworlds M)}
      {SM: Semantics L MD}
      {deSM: EmpSemantics L MD M SM}:
  forall (m: Kworlds M), KRIPKE: M, m |= emp <-> increasing m.
Proof.
(* Goal: forall m : @Kworlds MD kMD M, iff (@satisfies L MD SM (@build_model MD kMD M m) (@emp L sL s'L)) (@increasing (@Kworlds MD kMD M) R J m) *)
  intros; simpl.
(* Goal: iff (@satisfies L MD SM (@build_model MD kMD M m) (@emp L sL s'L)) (@increasing (@Kworlds MD kMD M) R J m) *)
  unfold satisfies.
(* Goal: iff (@denotation L MD SM (@emp L sL s'L) (@build_model MD kMD M m)) (@increasing (@Kworlds MD kMD M) R J m) *)
  destruct denote_emp.
(* Goal: iff (@denotation L MD SM (@emp L sL s'L) (@build_model MD kMD M m)) (@increasing (@Kworlds MD kMD M) R J m) *)
  split; [apply H | apply H0].
Qed.
