Require Import Logic.lib.Coqlib.
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.Semantics.DownUpSemantics_Fail.

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

Lemma sound_sepcon_comm {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)} {SM: Semantics L MD} {kiSM: KripkeIntuitionisticSemantics L MD M SM} {kminSM: KripkeMinimunSemantics L MD M SM} {kpSM: KripkePropositionalSemantics L MD M SM} {dusSM: DownUpSemantics_Fail.SeparatingSemantics L MD M SM}:
  forall x y: expr,
    forall m,
      KRIPKE: M, m |= x * y --> y * x.
Proof.
(* Goal: forall (x y : @expr L) (m : @Kworlds MD kMD M), @satisfies L MD SM (@build_model MD kMD M m) (@impp L minL (@sepcon L sL x y) (@sepcon L sL y x)) *)
  intros.
(* Goal: forall (x y : @expr L) (m : @Kworlds MD kMD M), @satisfies L MD SM (@build_model MD kMD M m) (@impp L minL (@sepcon L sL x y) (@sepcon L sL y x)) *)
  rewrite sat_impp; intros.
(* Goal: forall (x y : @expr L) (m : @Kworlds MD kMD M), @satisfies L MD SM (@build_model MD kMD M m) (@impp L minL (@sepcon L sL x y) (@sepcon L sL y x)) *)
  rewrite sat_sepcon in H0 |- *; intros.
(* Goal: @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 n) (and (@join (@Kworlds MD kMD M) J m1 m2 m0) (and (@satisfies L MD SM (@build_model MD kMD M m1) y) (@satisfies L MD SM (@build_model MD kMD M m2) x)))))) *)
  destruct H0 as [m0 [m1 [m2 [? [? [? ?]]]]]].
(* Goal: @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 n) (and (@join (@Kworlds MD kMD M) J m1 m2 m0) (and (@satisfies L MD SM (@build_model MD kMD M m1) y) (@satisfies L MD SM (@build_model MD kMD M m2) x)))))) *)
  exists m0, m2, m1.
(* Goal: and (@Krelation (@Kworlds MD kMD M) R m0 n) (and (@join (@Kworlds MD kMD M) J m2 m1 m0) (and (@satisfies L MD SM (@build_model MD kMD M m2) y) (@satisfies L MD SM (@build_model MD kMD M m1) x))) *)
  split; [| split; [| split]]; auto.
(* Goal: @join (@Kworlds MD kMD M) J m2 m1 m0 *)
  apply join_comm; auto.
Qed.

Lemma sound_sepcon_assoc {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)} {SM: Semantics L MD} {kiSM: KripkeIntuitionisticSemantics L MD M SM} {kminSM: KripkeMinimunSemantics L MD M SM} {kpSM: KripkePropositionalSemantics L MD M SM} {dusSM: DownUpSemantics_Fail.SeparatingSemantics L MD M SM}:
  forall x y z: expr,
    forall m,
      KRIPKE: M, m |= x * (y * z) <--> (x * y) * z.
Proof.
(* Goal: forall (x y : @expr L) (m : @Kworlds MD kMD M), @satisfies L MD SM (@build_model MD kMD M m) (@impp L minL (@sepcon L sL x y) (@sepcon L sL y x)) *)
  intros.
  unfold iffp.
  rewrite sat_andp.
(* Goal: forall (x y : @expr L) (m : @Kworlds MD kMD M), @satisfies L MD SM (@build_model MD kMD M m) (@impp L minL (@sepcon L sL x y) (@sepcon L sL y x)) *)
  split; intros.
(* Goal: forall (x y : @expr L) (m : @Kworlds MD kMD M), @satisfies L MD SM (@build_model MD kMD M m) (@impp L minL (@sepcon L sL x y) (@sepcon L sL y x)) *)
  + rewrite sat_impp; intros.
    rewrite sat_sepcon in H0.
(* Goal: @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 n) (and (@join (@Kworlds MD kMD M) J m1 m2 m0) (and (@satisfies L MD SM (@build_model MD kMD M m1) y) (@satisfies L MD SM (@build_model MD kMD M m2) x)))))) *)
    destruct H0 as [m0 [m1 [m2 [? [? [? ?]]]]]].
    (* fail *)
Abort.
