Require Import Coq.Classes.RelationClasses.
Require Import Coq.Relations.Relation_Definitions.
Require Import Logic.lib.Coqlib.
Require Import Logic.lib.Ensembles_ext.
Require Import Logic.GeneralLogic.Base.
Require Import Logic.GeneralLogic.KripkeModel.
Require Import Logic.GeneralLogic.Semantics.Kripke.
Require Import Logic.MinimunLogic.Syntax.
Require Import Logic.MinimunLogic.Semantics.Kripke.
Require Import Logic.PropositionalLogic.Syntax.
Require Import Logic.PropositionalLogic.Semantics.Kripke.
Require Import Logic.SeparationLogic.Syntax.
Require Import Logic.SeparationLogic.Model.SeparationAlgebra.
Require Import Logic.SeparationLogic.Model.OrderedSA.
Require Import Logic.SeparationLogic.Model.DownwardsClosure.
Require Import Logic.SeparationLogic.Semantics.WeakSemantics.
Require Import Logic.SeparationLogic.Semantics.StrongSemantics.
Require Import Logic.SeparationLogic.Semantics.UpwardsSemantics.
Require Import Logic.SeparationLogic.Semantics.FlatSemantics.

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

Module Up2Flat.
Section Up2Flat.

Context {L: Language}
        {minL: MinimunLanguage L}
        {pL: PropositionalLanguage L}
        {sL: SeparationLanguage L}
        {MD: Model}
        {kMD: KripkeModel MD}
        {M: Kmodel}
        {R: Relation (Kworlds M)}
        {po_R: PreOrder Krelation}
        {J: Join (Kworlds M)}
        {SA: SeparationAlgebra (Kworlds M)}
        {uSA: UpwardsClosedSeparationAlgebra (Kworlds M)}
        {SM: Semantics L MD}
        {kiSM: KripkeIntuitionisticSemantics L MD M SM}
        {usSM: UpwardsSemantics.SeparatingSemantics L MD M SM}.

Definition fsSM: @FlatSemantics.SeparatingSemantics L sL MD kMD M _ (DownwardsClosure_J) SM.
Proof.
(* Goal: @SeparatingSemantics L sL MD kMD M R (@DownwardsClosure_J (@Kworlds MD kMD M) R J) SM *)
  constructor.
  + (* sat_sepcon *)
(* Goal: forall (m1 m2 : @Kworlds MD kMD M) (_ : @join (@Kworlds MD kMD M) (@DownwardsClosure_J (@Kworlds MD kMD M) R J) m m1 m2) (_ : @Kdenotation L MD kMD M SM x m1), @Kdenotation L MD kMD M SM y m2 *)
    intros.
(* Goal: Same_set (@Kworlds MD kMD M) (@Kdenotation L MD kMD M SM (@sepcon L sL x y)) (@WeakSemantics.sepcon (@Kworlds MD kMD M) (@DownwardsClosure_J (@Kworlds MD kMD M) R J) (@Kdenotation L MD kMD M SM x) (@Kdenotation L MD kMD M SM y)) *)
    unfold WeakSemantics.sepcon.
(* Goal: Same_set (@Kworlds MD kMD M) (@Kdenotation L MD kMD M SM (@wand L sL x y)) (fun m : @Kworlds MD kMD M => forall (m1 m2 : @Kworlds MD kMD M) (_ : @join (@Kworlds MD kMD M) (@DownwardsClosure_J (@Kworlds MD kMD M) R J) m m1 m2) (_ : @Kdenotation L MD kMD M SM x m1), @Kdenotation L MD kMD M SM y m2) *)
    split; unfold Included, Ensembles.In; intros m ?.
    - rewrite (app_same_set (UpwardsSemantics.denote_sepcon _ _) m) in H.
(* Goal: @ex (@Kworlds MD kMD M) (fun m1 : @Kworlds MD kMD M => @ex (@Kworlds MD kMD M) (fun m2 : @Kworlds MD kMD M => and (@join (@Kworlds MD kMD M) (@DownwardsClosure_J (@Kworlds MD kMD M) R J) m1 m2 m) (and (@Kdenotation L MD kMD M SM x m1) (@Kdenotation L MD kMD M SM y m2)))) *)
      destruct H as [m1 [m2 [? [? ?]]]].
(* Goal: @join (@Kworlds MD kMD M) (@DownwardsClosure_J (@Kworlds MD kMD M) R J) m1 m2 m *)
      exists m1, m2.
(* Goal: and (@Krelation (@Kworlds MD kMD M) R m m0) (and (@Krelation (@Kworlds MD kMD M) R m1 m1) (@join (@Kworlds MD kMD M) J m0 m1 m2)) *)
      split; [| split]; auto.
(* Goal: @join (@Kworlds MD kMD M) (@DownwardsClosure_J (@Kworlds MD kMD M) R J) m1 m2 m *)
      exists m1, m2.
(* Goal: and (@Krelation (@Kworlds MD kMD M) R m1 m1) (and (@Krelation (@Kworlds MD kMD M) R m2 m2) (@join (@Kworlds MD kMD M) J m1 m2 m)) *)
      split; [| split]; auto; reflexivity.
    - rewrite (app_same_set (UpwardsSemantics.denote_sepcon _ _) m).
(* Goal: @WeakSemantics.sepcon (@Kworlds MD kMD M) J (@Kdenotation L MD kMD M SM x) (@Kdenotation L MD kMD M SM y) m *)
      destruct H as [m1 [m2 [[n1 [n2 [? [? ?]]]] [? ?]]]].
(* Goal: @WeakSemantics.sepcon (@Kworlds MD kMD M) J (@Kdenotation L MD kMD M SM x) (@Kdenotation L MD kMD M SM y) m *)
      exists n1, n2.
(* Goal: and (@join (@Kworlds MD kMD M) J n1 n2 m) (and (@Kdenotation L MD kMD M SM x n1) (@Kdenotation L MD kMD M SM y n2)) *)
      split; [| split]; auto; eapply sat_mono; eauto.
  + (* sat_wand *)
(* Goal: forall (m1 m2 : @Kworlds MD kMD M) (_ : @join (@Kworlds MD kMD M) (@DownwardsClosure_J (@Kworlds MD kMD M) R J) m m1 m2) (_ : @Kdenotation L MD kMD M SM x m1), @Kdenotation L MD kMD M SM y m2 *)
    intros.
(* Goal: Same_set (@Kworlds MD kMD M) (@Kdenotation L MD kMD M SM (@wand L sL x y)) (@WeakSemantics.wand (@Kworlds MD kMD M) (@DownwardsClosure_J (@Kworlds MD kMD M) R J) (@Kdenotation L MD kMD M SM x) (@Kdenotation L MD kMD M SM y)) *)
    unfold WeakSemantics.wand.
(* Goal: Same_set (@Kworlds MD kMD M) (@Kdenotation L MD kMD M SM (@wand L sL x y)) (fun m : @Kworlds MD kMD M => forall (m1 m2 : @Kworlds MD kMD M) (_ : @join (@Kworlds MD kMD M) (@DownwardsClosure_J (@Kworlds MD kMD M) R J) m m1 m2) (_ : @Kdenotation L MD kMD M SM x m1), @Kdenotation L MD kMD M SM y m2) *)
    split; unfold Included, Ensembles.In; intros m ?.
    - rewrite (app_same_set (UpwardsSemantics.denote_wand _ _) m) in H.
(* Goal: forall (m1 m2 : @Kworlds MD kMD M) (_ : @join (@Kworlds MD kMD M) (@DownwardsClosure_J (@Kworlds MD kMD M) R J) m m1 m2) (_ : @Kdenotation L MD kMD M SM x m1), @Kdenotation L MD kMD M SM y m2 *)
      intros.
(* Goal: @Kdenotation L MD kMD M SM y m2 *)
      destruct H0 as [m' [m1' [? [? ?]]]].
      apply (H  _ _ _ H0 H3).
(* Goal: @Kdenotation L MD kMD M SM x m1' *)
      eapply sat_mono; eauto.
    - rewrite (app_same_set (UpwardsSemantics.denote_wand _ _) m).
(* Goal: forall (m1 m2 : @Kworlds MD kMD M) (_ : @join (@Kworlds MD kMD M) (@DownwardsClosure_J (@Kworlds MD kMD M) R J) m m1 m2) (_ : @Kdenotation L MD kMD M SM x m1), @Kdenotation L MD kMD M SM y m2 *)
      hnf; intros.
(* Goal: @Kdenotation L MD kMD M SM y m2 *)
      apply (H m1 m2); auto.
(* Goal: @join (@Kworlds MD kMD M) (@DownwardsClosure_J (@Kworlds MD kMD M) R J) m m1 m2 *)
      exists m0, m1.
(* Goal: and (@Krelation (@Kworlds MD kMD M) R m m0) (and (@Krelation (@Kworlds MD kMD M) R m1 m1) (@join (@Kworlds MD kMD M) J m0 m1 m2)) *)
      split; [| split]; auto.
(* Goal: @Krelation (@Kworlds MD kMD M) R m1 m1 *)
      reflexivity.
Qed.

Definition feSM {s'L: SeparationEmpLanguage L} {USA': UnitalSeparationAlgebra' (Kworlds M)} {ueSM: UpwardsSemantics.EmpSemantics L MD M SM}: @FlatSemantics.EmpSemantics L _ _ MD _ M _ (DownwardsClosure_J) SM.
Proof.
  constructor;
  intros m; simpl; unfold Ensembles.In; unfold WeakSemantics.emp;
  rewrite <- DownwardsClosure_increasing;
  apply UpwardsSemantics.denote_emp.
Qed.

End Up2Flat.
End Up2Flat.
