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.UpwardsClosure.
Require Import Logic.SeparationLogic.Semantics.WeakSemantics.
Require Import Logic.SeparationLogic.Semantics.StrongSemantics.
Require Import Logic.SeparationLogic.Semantics.DownwardsSemantics.
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.
Import KripkeModelNotation_Intuitionistic.

Module Down2Flat.
Section Down2Flat.

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)}
        {dSA: DownwardsClosedSeparationAlgebra (Kworlds M)}
        {SM: Semantics L MD}
        {kiSM: KripkeIntuitionisticSemantics L MD M SM}
        {dsSM: DownwardsSemantics.SeparatingSemantics L MD M SM}.

Definition fsSM: @FlatSemantics.SeparatingSemantics L _ MD _ M _ UpwardsClosure_J SM.
Proof.
(* Goal: @SeparatingSemantics L sL MD kMD M R (@UpwardsClosure_J (@Kworlds MD kMD M) R J) SM *)
  constructor.
  + (* sat_sepcon *)
(* Goal: forall (m1 m2 : @Kworlds MD kMD M) (_ : @join (@Kworlds MD kMD M) (@UpwardsClosure_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) (@UpwardsClosure_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) (@UpwardsClosure_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 (DownwardsSemantics.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) (@UpwardsClosure_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 [m0 [m1 [m2 [? [? [? ?]]]]]].
(* 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) (@UpwardsClosure_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)))) *)
      exists m1, m2.
(* Goal: and (@join (@Kworlds MD kMD M) (@UpwardsClosure_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)) *)
      split; [| split]; auto.
(* Goal: @join (@Kworlds MD kMD M) (@UpwardsClosure_J (@Kworlds MD kMD M) R J) m1 m2 m *)
      exists m0; split; auto.
    - rewrite (app_same_set (DownwardsSemantics.denote_sepcon _ _) m).
(* Goal: @StrongSemantics.sepcon (@Kworlds MD kMD M) R J (@Kdenotation L MD kMD M SM x) (@Kdenotation L MD kMD M SM y) m *)
      destruct H as [m1 [m2 [[n [? ?]] [? ?]]]].
(* Goal: @StrongSemantics.sepcon (@Kworlds MD kMD M) R J (@Kdenotation L MD kMD M SM x) (@Kdenotation L MD kMD M SM y) m *)
      exists n, m1, m2.
(* Goal: and (@Krelation (@Kworlds MD kMD M) R n m) (and (@join (@Kworlds MD kMD M) J m1 m2 n) (and (@Kdenotation L MD kMD M SM x m1) (@Kdenotation L MD kMD M SM y m2))) *)
      split; [| split; [| split]]; auto.
  + (* sat_wand *)
(* Goal: forall (m1 m2 : @Kworlds MD kMD M) (_ : @join (@Kworlds MD kMD M) (@UpwardsClosure_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) (@UpwardsClosure_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) (@UpwardsClosure_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 (DownwardsSemantics.denote_wand _ _) m) in H.
(* Goal: forall (m1 m2 : @Kworlds MD kMD M) (_ : @join (@Kworlds MD kMD M) (@UpwardsClosure_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 [m2' [? ?]].
(* Goal: @Kdenotation L MD kMD M SM y m2 *)
      eapply sat_mono; eauto.
(* Goal: @satisfies L MD SM (@build_model MD kMD M m2') y *)
      eapply H; eauto.
    - rewrite (app_same_set (DownwardsSemantics.denote_wand _ _) m).
(* Goal: forall (m1 m2 : @Kworlds MD kMD M) (_ : @join (@Kworlds MD kMD M) (@UpwardsClosure_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) (@UpwardsClosure_J (@Kworlds MD kMD M) R J) m m1 m2 *)
      exists m2; split; auto.
(* Goal: @Krelation (@Kworlds MD kMD M) R m2 m2 *)
      reflexivity.
Qed.

Definition feSM {s'L: SeparationEmpLanguage L} {USA: UnitalSeparationAlgebra (Kworlds M)} {deSM: DownwardsSemantics.EmpSemantics L MD M SM}: @FlatSemantics.EmpSemantics L _ _ MD _ M _ UpwardsClosure_J SM.
Proof.
  split; intros m; unfold Ensembles.In; unfold WeakSemantics.emp;
  rewrite <- UpwardsClosure_increasing;
  apply DownwardsSemantics.denote_emp.
Qed.

End Down2Flat.
End Down2Flat.
