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.DownwardsSemantics.

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

Section Sound_Downwards.

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}
        {kminSM: KripkeMinimunSemantics L MD M SM}
        {kpSM: KripkePropositionalSemantics L MD M SM}
        {dsSM: DownwardsSemantics.SeparatingSemantics L MD M SM}.

Lemma sound_sepcon_comm:
  forall x y: expr,
    forall m,
      KRIPKE: M, m |= x * y --> y * x.
Proof.
(* Goal: forall (x : @expr L) (m : @Kworlds MD kMD M), @satisfies L MD SM (@build_model MD kMD M m) (@iffp L minL pL (@sepcon L sL x (@emp L sL s'L)) x) *)
  intros.
(* Goal: forall (x : @expr L) (m : @Kworlds MD kMD M), @satisfies L MD SM (@build_model MD kMD M m) (@iffp L minL pL (@sepcon L sL x (@emp L sL s'L)) x) *)
  rewrite sat_impp; intros.
(* Goal: forall (x : @expr L) (m : @Kworlds MD kMD M), @satisfies L MD SM (@build_model MD kMD M m) (@iffp L minL pL (@sepcon L sL x (@emp L sL s'L)) x) *)
  rewrite sat_sepcon in H0 |- *; intros.
(* Goal: @satisfies L MD SM (@build_model MD kMD M n) 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]; auto.
(* Goal: @join (@Kworlds MD kMD M) J n' u n *)
  apply join_comm; auto.
Qed.

Lemma sound_sepcon_assoc:
  forall x y z: expr,
    forall m,
      KRIPKE: M, m |= x * (y * z) <--> (x * y) * z.
Proof.
(* Goal: forall (x : @expr L) (m : @Kworlds MD kMD M), @satisfies L MD SM (@build_model MD kMD M m) (@iffp L minL pL (@sepcon L sL x (@emp L sL s'L)) x) *)
  intros.
(* Goal: @satisfies L MD SM (@build_model MD kMD M m) (@iffp L minL pL (@sepcon L sL x (@emp L sL s'L)) x) *)
  unfold iffp.
(* Goal: @satisfies L MD SM (@build_model MD kMD M m) (@andp L pL (@impp L minL (@sepcon L sL x (@emp L sL s'L)) x) (@impp L minL x (@sepcon L sL x (@emp L sL s'L)))) *)
  rewrite sat_andp.
(* Goal: forall (x : @expr L) (m : @Kworlds MD kMD M), @satisfies L MD SM (@build_model MD kMD M m) (@iffp L minL pL (@sepcon L sL x (@emp L sL s'L)) x) *)
  split; intros.
(* Goal: forall (x : @expr L) (m : @Kworlds MD kMD M), @satisfies L MD SM (@build_model MD kMD M m) (@iffp L minL pL (@sepcon L sL x (@emp L sL s'L)) x) *)
  + rewrite sat_impp; intros.
(* Goal: @satisfies L MD SM (@build_model MD kMD M n) x *)
    rewrite sat_sepcon in H0.
(* Goal: @satisfies L MD SM (@build_model MD kMD M n) (@sepcon L sL (@sepcon L sL x y) z) *)
    destruct H0 as [n' [mx' [myz' [? [? [? ?]]]]]].
(* Goal: @satisfies L MD SM (@build_model MD kMD M n) (@sepcon L sL (@sepcon L sL x y) z) *)
    rewrite sat_sepcon in H3.
(* Goal: @satisfies L MD SM (@build_model MD kMD M n) (@sepcon L sL (@sepcon L sL x y) z) *)
    destruct H3 as [myz'' [my'' [mz'' [? [? [? ?]]]]]].
(* Goal: @satisfies L MD SM (@build_model MD kMD M n) x *)
    apply join_comm in H1.
(* Goal: @satisfies L MD SM (@build_model MD kMD M n) (@sepcon L sL (@sepcon L sL x y) z) *)
    apply join_comm in H4.
(* Goal: @satisfies L MD SM (@build_model MD kMD M n) (@sepcon L sL (@sepcon L sL x y) z) *)
    assert (mx' <= mx') by reflexivity.
(* Goal: @satisfies L MD SM (@build_model MD kMD M n) (@sepcon L sL (@sepcon L sL x y) z) *)
    destruct (join_Korder_down _ _ _ _ _ H1 H3 H7) as [n'' [? ?]].
(* Goal: @satisfies L MD SM (@build_model MD kMD M n) (@sepcon L sL (@sepcon L sL x y) z) *)
    destruct (join_assoc mz'' my'' mx' myz'' n'' H4 H8) as [mxy'' [? ?]].
(* Goal: @satisfies L MD SM (@build_model MD kMD M n) (@sepcon L sL (@sepcon L sL x y) z) *)
    apply join_comm in H10.
(* Goal: @satisfies L MD SM (@build_model MD kMD M n) (@sepcon L sL (@sepcon L sL x y) z) *)
    apply join_comm in H11.
(* Goal: @satisfies L MD SM (@build_model MD kMD M n) (@sepcon L sL x (@emp L sL s'L)) *)
    rewrite sat_sepcon.
(* 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) (@sepcon L sL x y)) (@satisfies L MD SM (@build_model MD kMD M m2) z)))))) *)
    exists n'', mxy'', mz''.
(* Goal: and (@Krelation (@Kworlds MD kMD M) R n n) (and (@join (@Kworlds MD kMD M) J n' u n) (and (@satisfies L MD SM (@build_model MD kMD M n') x) (@satisfies L MD SM (@build_model MD kMD M u) (@emp L sL s'L)))) *)
    split; [| split; [| split]]; auto.
    - etransitivity; eauto.
(* Goal: @satisfies L MD SM (@build_model MD kMD M n) (@sepcon L sL x (@emp L sL s'L)) *)
    - rewrite sat_sepcon.
(* 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 mxy'') (and (@join (@Kworlds MD kMD M) J m1 m2 m0) (and (@satisfies L MD SM (@build_model MD kMD M m1) x) (@satisfies L MD SM (@build_model MD kMD M m2) y)))))) *)
      exists mxy'', mx', my''.
(* Goal: and (@Krelation (@Kworlds MD kMD M) R n n) (and (@join (@Kworlds MD kMD M) J n' u n) (and (@satisfies L MD SM (@build_model MD kMD M n') x) (@satisfies L MD SM (@build_model MD kMD M u) (@emp L sL s'L)))) *)
      split; [| split; [| split]]; auto.
(* Goal: @Krelation (@Kworlds MD kMD M) R n n *)
      reflexivity.
(* Goal: forall (x : @expr L) (m : @Kworlds MD kMD M), @satisfies L MD SM (@build_model MD kMD M m) (@iffp L minL pL (@sepcon L sL x (@emp L sL s'L)) x) *)
  + rewrite sat_impp; intros.
(* Goal: @satisfies L MD SM (@build_model MD kMD M n) x *)
    rewrite sat_sepcon in H0.
(* Goal: @satisfies L MD SM (@build_model MD kMD M n) (@sepcon L sL x (@sepcon L sL y z)) *)
    destruct H0 as [n' [mxy' [mz' [? [? [? ?]]]]]].
(* Goal: @satisfies L MD SM (@build_model MD kMD M n) (@sepcon L sL x (@sepcon L sL y z)) *)
    rewrite sat_sepcon in H2.
(* Goal: @satisfies L MD SM (@build_model MD kMD M n) (@sepcon L sL x (@sepcon L sL y z)) *)
    destruct H2 as [mxy'' [mx'' [my'' [? [? [? ?]]]]]].
(* Goal: @Krelation (@Kworlds MD kMD M) R n n *)
    assert (mz' <= mz') by reflexivity.
(* Goal: @satisfies L MD SM (@build_model MD kMD M n) (@sepcon L sL x (@sepcon L sL y z)) *)
    destruct (join_Korder_down _ _ _ _ _ H1 H2 H7) as [n'' [? ?]].
(* Goal: @satisfies L MD SM (@build_model MD kMD M n) (@sepcon L sL x (@sepcon L sL y z)) *)
    destruct (join_assoc mx'' my'' mz' mxy'' n'' H4 H8) as [myz'' [? ?]].
(* Goal: @satisfies L MD SM (@build_model MD kMD M n) (@sepcon L sL x (@emp L sL s'L)) *)
    rewrite sat_sepcon.
(* 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) x) (@satisfies L MD SM (@build_model MD kMD M m2) (@sepcon L sL y z))))))) *)
    exists n'', mx'', myz''.
(* Goal: and (@Krelation (@Kworlds MD kMD M) R n n) (and (@join (@Kworlds MD kMD M) J n' u n) (and (@satisfies L MD SM (@build_model MD kMD M n') x) (@satisfies L MD SM (@build_model MD kMD M u) (@emp L sL s'L)))) *)
    split; [| split; [| split]]; auto.
    - etransitivity; eauto.
(* Goal: @satisfies L MD SM (@build_model MD kMD M n) (@sepcon L sL x (@emp L sL s'L)) *)
    - rewrite sat_sepcon.
(* 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 myz'') (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) z)))))) *)
      exists myz'', my'', mz'.
(* Goal: and (@Krelation (@Kworlds MD kMD M) R n n) (and (@join (@Kworlds MD kMD M) J n' u n) (and (@satisfies L MD SM (@build_model MD kMD M n') x) (@satisfies L MD SM (@build_model MD kMD M u) (@emp L sL s'L)))) *)
      split; [| split; [| split]]; auto.
(* Goal: @Krelation (@Kworlds MD kMD M) R n n *)
      reflexivity.
Qed.

Lemma sound_wand_sepcon_adjoint:
  forall x y z: expr,
   (forall m, KRIPKE: M, m |= x * y --> z) <-> (forall m, KRIPKE: M, m |= x --> (y -* z)).
Proof.
(* Goal: forall (x : @expr L) (m : @Kworlds MD kMD M), @satisfies L MD SM (@build_model MD kMD M m) (@iffp L minL pL (@sepcon L sL x (@emp L sL s'L)) x) *)
  intros.
  split; intro.
  + assert (ASSU: forall m0 m1 m2 m, m0 <= m -> join m1 m2 m0 -> KRIPKE: M, m1 |= x -> KRIPKE: M, m2 |= y -> KRIPKE: M, m |= z).
    Focus 1. {
(* Goal: forall (x : @expr L) (m : @Kworlds MD kMD M), @satisfies L MD SM (@build_model MD kMD M m) (@iffp L minL pL (@sepcon L sL x (@emp L sL s'L)) x) *)
      intros.
      specialize (H m).
      rewrite sat_impp in H.
      apply (H m); [reflexivity |].
(* Goal: @satisfies L MD SM (@build_model MD kMD M n) (@sepcon L sL x (@emp L sL s'L)) *)
      rewrite sat_sepcon.
      exists m0, m1, m2; auto.
    } Unfocus.
    clear H.
(* Goal: forall (x : @expr L) (m : @Kworlds MD kMD M), @satisfies L MD SM (@build_model MD kMD M m) (@iffp L minL pL (@sepcon L sL x (@emp L sL s'L)) x) *)
    intros.
(* Goal: forall (x : @expr L) (m : @Kworlds MD kMD M), @satisfies L MD SM (@build_model MD kMD M m) (@iffp L minL pL (@sepcon L sL x (@emp L sL s'L)) x) *)
    rewrite sat_impp; intros.
(* Goal: forall (x : @expr L) (m : @Kworlds MD kMD M), @satisfies L MD SM (@build_model MD kMD M m) (@iffp L minL pL (@sepcon L sL x (@emp L sL s'L)) x) *)
    rewrite sat_wand; intros.
    apply (ASSU m2 n m1 m2); auto.
(* Goal: @Krelation (@Kworlds MD kMD M) R n n *)
    reflexivity.
  + assert (ASSU: forall m1 m2 m, join m m1 m2 -> KRIPKE: M, m |= x -> KRIPKE: M, m1 |= y -> KRIPKE: M, m2 |= z).
    Focus 1. {
(* Goal: forall (x : @expr L) (m : @Kworlds MD kMD M), @satisfies L MD SM (@build_model MD kMD M m) (@iffp L minL pL (@sepcon L sL x (@emp L sL s'L)) x) *)
      intros.
      specialize (H m).
      rewrite sat_impp in H.
      revert m1 m2 H0 H2.
      rewrite <- sat_wand.
      apply (H m); [reflexivity | auto].
    } Unfocus.
(* Goal: forall (x : @expr L) (m : @Kworlds MD kMD M), @satisfies L MD SM (@build_model MD kMD M m) (@iffp L minL pL (@sepcon L sL x (@emp L sL s'L)) x) *)
    intros.
(* Goal: forall (x : @expr L) (m : @Kworlds MD kMD M), @satisfies L MD SM (@build_model MD kMD M m) (@iffp L minL pL (@sepcon L sL x (@emp L sL s'L)) x) *)
    rewrite sat_impp; intros.
    rewrite sat_sepcon in H1.
    destruct H1 as [m0 [m1 [m2 [? [? [? ?]]]]]].
    pose proof (ASSU m2 m0 m1 H2 H3 H4).
(* Goal: @satisfies L MD SM (@build_model MD kMD M n') x *)
    eapply sat_mono; eauto.
Qed.

Lemma sound_sepcon_mono:
  forall x1 x2 y1 y2: expr,
   (forall m, KRIPKE: M, m |= x1 --> x2) ->
   (forall m, KRIPKE: M, m |= y1 --> y2) ->
   (forall m, KRIPKE: M, m |= x1 * y1 --> x2 * y2).
Proof.
(* Goal: forall (x : @expr L) (m : @Kworlds MD kMD M), @satisfies L MD SM (@build_model MD kMD M m) (@iffp L minL pL (@sepcon L sL x (@emp L sL s'L)) x) *)
  intros.
  assert (ASSUx: forall m, KRIPKE: M, m |= x1 -> KRIPKE: M, m |= x2).
  Focus 1. {
(* Goal: forall (x : @expr L) (m : @Kworlds MD kMD M), @satisfies L MD SM (@build_model MD kMD M m) (@iffp L minL pL (@sepcon L sL x (@emp L sL s'L)) x) *)
    intros.
    specialize (H m0).
    rewrite sat_impp in H.
    apply (H m0); [reflexivity | auto].
  } Unfocus.
  assert (ASSUy: forall m, KRIPKE: M, m |= y1 -> KRIPKE: M, m |= y2).
  Focus 1. {
(* Goal: forall (x : @expr L) (m : @Kworlds MD kMD M), @satisfies L MD SM (@build_model MD kMD M m) (@iffp L minL pL (@sepcon L sL x (@emp L sL s'L)) x) *)
    intros.
    specialize (H0 m0).
    rewrite sat_impp in H0.
    apply (H0 m0); [reflexivity | auto].
  } Unfocus.
(* Goal: forall (x : @expr L) (m : @Kworlds MD kMD M), @satisfies L MD SM (@build_model MD kMD M m) (@iffp L minL pL (@sepcon L sL x (@emp L sL s'L)) x) *)
  rewrite sat_impp; intros.
  rewrite sat_sepcon in H2 |- *.
  destruct H2 as [m0 [m1 [m2 [? [? [? ?]]]]]].
  exists m0, m1, m2; auto.
Qed.

Lemma sound_sepcon_elim1 {incrSA: IncreasingSeparationAlgebra (Kworlds M)}:
  forall x y: expr,
    forall m, KRIPKE: M, m |= x * y --> x.
Proof.
(* Goal: forall (x : @expr L) (m : @Kworlds MD kMD M), @satisfies L MD SM (@build_model MD kMD M m) (@iffp L minL pL (@sepcon L sL x (@emp L sL s'L)) x) *)
  intros.
(* Goal: forall (x : @expr L) (m : @Kworlds MD kMD M), @satisfies L MD SM (@build_model MD kMD M m) (@iffp L minL pL (@sepcon L sL x (@emp L sL s'L)) x) *)
  rewrite sat_impp; intros.
(* Goal: @satisfies L MD SM (@build_model MD kMD M n) x *)
  rewrite sat_sepcon in H0.
(* Goal: @satisfies L MD SM (@build_model MD kMD M n) x *)
  destruct H0 as [m0 [m1 [m2 [? [? [? ?]]]]]].
(* Goal: @satisfies L MD SM (@build_model MD kMD M n) x *)
  apply join_comm in H1.
(* Goal: @satisfies L MD SM (@build_model MD kMD M n) x *)
  apply all_increasing in H1.
(* Goal: @satisfies L MD SM (@build_model MD kMD M n') x *)
  eapply sat_mono; eauto.
(* Goal: @satisfies L MD SM (@build_model MD kMD M n') x *)
  eapply sat_mono; eauto.
Qed.

Context {s'L: SeparationEmpLanguage L}
        {deSM: DownwardsSemantics.EmpSemantics L MD M SM}.

Lemma sound_sepcon_emp {USA: UnitalSeparationAlgebra (Kworlds M)}:
  forall x: expr,
    forall m, KRIPKE: M, m |= x * emp <--> x.
Proof.
(* Goal: forall (x : @expr L) (m : @Kworlds MD kMD M), @satisfies L MD SM (@build_model MD kMD M m) (@iffp L minL pL (@sepcon L sL x (@emp L sL s'L)) x) *)
  intros.
(* Goal: @satisfies L MD SM (@build_model MD kMD M m) (@iffp L minL pL (@sepcon L sL x (@emp L sL s'L)) x) *)
  unfold iffp.
(* Goal: @satisfies L MD SM (@build_model MD kMD M m) (@andp L pL (@impp L minL (@sepcon L sL x (@emp L sL s'L)) x) (@impp L minL x (@sepcon L sL x (@emp L sL s'L)))) *)
  rewrite sat_andp.
(* Goal: and (@satisfies L MD SM (@build_model MD kMD M m) (@impp L minL (@sepcon L sL x (@emp L sL s'L)) x)) (@satisfies L MD SM (@build_model MD kMD M m) (@impp L minL x (@sepcon L sL x (@emp L sL s'L)))) *)
  split.
(* Goal: forall (x : @expr L) (m : @Kworlds MD kMD M), @satisfies L MD SM (@build_model MD kMD M m) (@iffp L minL pL (@sepcon L sL x (@emp L sL s'L)) x) *)
  + rewrite sat_impp; intros.
(* Goal: @satisfies L MD SM (@build_model MD kMD M n) x *)
    clear m H.
(* Goal: @satisfies L MD SM (@build_model MD kMD M n) x *)
    rewrite sat_sepcon in H0.
(* Goal: @satisfies L MD SM (@build_model MD kMD M n) x *)
    destruct H0 as [m'' [m' [u [? [? [? ?]]]]]].
(* Goal: @satisfies L MD SM (@build_model MD kMD M n) x *)
    rewrite sat_emp in H2.
(* Goal: @satisfies L MD SM (@build_model MD kMD M n) x *)
    apply join_comm in H0.
(* Goal: @satisfies L MD SM (@build_model MD kMD M n) x *)
    unfold increasing in H2.
(* Goal: @satisfies L MD SM (@build_model MD kMD M n) x *)
    apply H2 in H0.
(* Goal: @satisfies L MD SM (@build_model MD kMD M n') x *)
    eapply sat_mono; eauto.
(* Goal: @satisfies L MD SM (@build_model MD kMD M n') x *)
    eapply sat_mono; eauto.
(* Goal: forall (x : @expr L) (m : @Kworlds MD kMD M), @satisfies L MD SM (@build_model MD kMD M m) (@iffp L minL pL (@sepcon L sL x (@emp L sL s'L)) x) *)
  + rewrite sat_impp; intros.
(* Goal: @satisfies L MD SM (@build_model MD kMD M n) (@sepcon L sL x (@emp L sL s'L)) *)
    rewrite sat_sepcon.
(* 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) x) (@satisfies L MD SM (@build_model MD kMD M m2) (@emp L sL s'L))))))) *)
    destruct (incr_exists n) as [u [? ?]].
(* 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) x) (@satisfies L MD SM (@build_model MD kMD M m2) (@emp L sL s'L))))))) *)
    destruct H1 as [n' [H1 H1']].
(* 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) x) (@satisfies L MD SM (@build_model MD kMD M m2) (@emp L sL s'L))))))) *)
    exists n, n', u.
(* Goal: and (@Krelation (@Kworlds MD kMD M) R n n) (and (@join (@Kworlds MD kMD M) J n' u n) (and (@satisfies L MD SM (@build_model MD kMD M n') x) (@satisfies L MD SM (@build_model MD kMD M u) (@emp L sL s'L)))) *)
    split; [| split; [| split]]; auto.
    - reflexivity.
(* Goal: @join (@Kworlds MD kMD M) J n' u n *)
    - apply join_comm; auto.
    - eapply sat_mono; eauto.
    - rewrite sat_emp.
(* Goal: @increasing (@Kworlds MD kMD M) R J u *)
      auto.
Qed.

End Sound_Downwards.
