Require Import Coq.Sets.Ensembles.
Require Import Coq.Logic.Classical_Prop.
Require Import Coq.Classes.RelationClasses.
Require Import Coq.Classes.Equivalence.
Require Import Coq.Relations.Relation_Definitions.
Require Import Logic.lib.Ensembles_ext.
Require Import Logic.lib.Bisimulation.
Require Import Logic.GeneralLogic.Base.
Require Import Logic.GeneralLogic.KripkeModel.
Require Import Logic.ModalLogic.Model.KripkeModel.
Require Import Logic.SeparationLogic.Model.SeparationAlgebra.
Require Import Logic.MinimunLogic.Syntax.
Require Import Logic.PropositionalLogic.Syntax.
Require Import Logic.ModalLogic.Syntax.
Require Import Logic.SeparationLogic.Syntax.
Require Import Logic.Extensions.Semantics.SemanticStable.
Require Logic.PropositionalLogic.Semantics.Trivial.
Require Logic.ModalLogic.Semantics.Kripke.
Require Logic.GeneralLogic.Semantics.Kripke.
Require Logic.MinimunLogic.Semantics.Kripke.
Require Logic.PropositionalLogic.Semantics.Kripke.
Require Logic.ModalLogic.Semantics.Flat.
Require Import Logic.SeparationLogic.Semantics.WeakSemantics.
Require Logic.SeparationLogic.Semantics.FlatSemantics.

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

Module Sound_Trivial.

Import Logic.PropositionalLogic.Semantics.Trivial.
Import Logic.MinimunLogic.Semantics.Trivial.
Import Logic.ModalLogic.Semantics.Kripke.

Lemma sound_impp_stable {L: Language} {minL: MinimunLanguage L} {pL: PropositionalLanguage L} {MD: Model} {kMD: KripkeModel MD} {M: Kmodel} {R: SS.Relation (Kworlds M)} {SM: Semantics L MD} {tminSM: TrivialMinimunSemantics L MD SM} {tpSM: TrivialPropositionalSemantics L MD SM} {stableSM: SemanticStable L MD M SM}:
  forall x y: expr,
    semantic_stable x -> semantic_stable y -> semantic_stable (x --> y).
Proof.
(* Goal: forall (x y z : @expr L) (_ : @semantic_stable L MD kMD M R2 SM stableSM x) (m : @Kworlds MD kMD M), @satisfies L MD SM (@build_model MD kMD M m) (@iffp L minL pL (@sepcon L sL (@andp L pL x y) z) (@andp L pL x (@sepcon L sL y z))) *)
  intros.
(* Goal: @semantic_stable L MD kMD M R2 SM stableSM (@wand L sL x y) *)
  rewrite denote_stable in H, H0 |- *.
(* Goal: @Semantics.stable (@Kworlds MD kMD M) R2 (@Kdenotation L MD kMD M SM (@wand L sL x y)) *)
  unfold Semantics.stable in *.
(* Goal: forall (x y z : @expr L) (_ : @semantic_stable L MD kMD M R2 SM stableSM x) (m : @Kworlds MD kMD M), @satisfies L MD SM (@build_model MD kMD M m) (@iffp L minL pL (@sepcon L sL (@andp L pL x y) z) (@andp L pL x (@sepcon L sL y z))) *)
  intros.
(* Goal: iff (@Kdenotation L MD kMD M SM (@orp L pL x y) m) (@Kdenotation L MD kMD M SM (@orp L pL x y) n) *)
  unfold Kdenotation in *; simpl in *.
(* Goal: iff (@denotation L MD SM (@impp L minL x y) (@build_model MD kMD M m)) (@denotation L MD SM (@impp L minL x y) (@build_model MD kMD M n)) *)
  rewrite !(app_same_set (denote_impp _ _)).
(* Goal: iff (@Semantics.impp (@model MD) (@denotation L MD SM x) (@denotation L MD SM y) (@build_model MD kMD M m)) (@Semantics.impp (@model MD) (@denotation L MD SM x) (@denotation L MD SM y) (@build_model MD kMD M n)) *)
  unfold Semantics.impp; simpl.
(* Goal: @satisfies L MD SM (@build_model MD kMD M n) x *)
  specialize (H _ _ H1).
(* Goal: iff (or (@denotation L MD SM x (@build_model MD kMD M m)) (@denotation L MD SM y (@build_model MD kMD M m))) (or (@denotation L MD SM x (@build_model MD kMD M n)) (@denotation L MD SM y (@build_model MD kMD M n))) *)
  specialize (H0 _ _ H1).
(* Goal: @Kdenotation L MD kMD M SM y m2 *)
  tauto.
Qed.

Lemma sound_andp_stable {L: Language} {minL: MinimunLanguage L} {pL: PropositionalLanguage L} {MD: Model} {kMD: KripkeModel MD} {M: Kmodel} {R: SS.Relation (Kworlds M)} {SM: Semantics L MD} {tpSM: TrivialPropositionalSemantics L MD SM} {stableSM: SemanticStable L MD M SM}:
  forall x y: expr,
    semantic_stable x -> semantic_stable y -> semantic_stable (x && y).
Proof.
(* Goal: forall (x y z : @expr L) (_ : @semantic_stable L MD kMD M R2 SM stableSM x) (m : @Kworlds MD kMD M), @satisfies L MD SM (@build_model MD kMD M m) (@iffp L minL pL (@sepcon L sL (@andp L pL x y) z) (@andp L pL x (@sepcon L sL y z))) *)
  intros.
(* Goal: @semantic_stable L MD kMD M R2 SM stableSM (@wand L sL x y) *)
  rewrite denote_stable in H, H0 |- *.
(* Goal: @Semantics.stable (@Kworlds MD kMD M) R2 (@Kdenotation L MD kMD M SM (@wand L sL x y)) *)
  unfold Semantics.stable in *.
(* Goal: forall (x y z : @expr L) (_ : @semantic_stable L MD kMD M R2 SM stableSM x) (m : @Kworlds MD kMD M), @satisfies L MD SM (@build_model MD kMD M m) (@iffp L minL pL (@sepcon L sL (@andp L pL x y) z) (@andp L pL x (@sepcon L sL y z))) *)
  intros.
(* Goal: iff (@Kdenotation L MD kMD M SM (@orp L pL x y) m) (@Kdenotation L MD kMD M SM (@orp L pL x y) n) *)
  unfold Kdenotation in *; simpl in *.
(* Goal: iff (@denotation L MD SM (@andp L pL x y) (@build_model MD kMD M m)) (@denotation L MD SM (@andp L pL x y) (@build_model MD kMD M n)) *)
  rewrite !(app_same_set (denote_andp _ _)).
(* Goal: iff (@Semantics.andp (@model MD) (@denotation L MD SM x) (@denotation L MD SM y) (@build_model MD kMD M m)) (@Semantics.andp (@model MD) (@denotation L MD SM x) (@denotation L MD SM y) (@build_model MD kMD M n)) *)
  unfold Semantics.andp; simpl.
(* Goal: @satisfies L MD SM (@build_model MD kMD M n) x *)
  specialize (H _ _ H1).
(* Goal: iff (or (@denotation L MD SM x (@build_model MD kMD M m)) (@denotation L MD SM y (@build_model MD kMD M m))) (or (@denotation L MD SM x (@build_model MD kMD M n)) (@denotation L MD SM y (@build_model MD kMD M n))) *)
  specialize (H0 _ _ H1).
(* Goal: @Kdenotation L MD kMD M SM y m2 *)
  tauto.
Qed.

Lemma sound_orp_stable {L: Language} {minL: MinimunLanguage L} {pL: PropositionalLanguage L} {MD: Model} {kMD: KripkeModel MD} {M: Kmodel} {R: SS.Relation (Kworlds M)} {SM: Semantics L MD} {tpSM: TrivialPropositionalSemantics L MD SM} {stableSM: SemanticStable L MD M SM}:
  forall x y: expr,
    semantic_stable x -> semantic_stable y -> semantic_stable (x || y).
Proof.
(* Goal: forall (x y z : @expr L) (_ : @semantic_stable L MD kMD M R2 SM stableSM x) (m : @Kworlds MD kMD M), @satisfies L MD SM (@build_model MD kMD M m) (@iffp L minL pL (@sepcon L sL (@andp L pL x y) z) (@andp L pL x (@sepcon L sL y z))) *)
  intros.
(* Goal: @semantic_stable L MD kMD M R2 SM stableSM (@wand L sL x y) *)
  rewrite denote_stable in H, H0 |- *.
(* Goal: @Semantics.stable (@Kworlds MD kMD M) R2 (@Kdenotation L MD kMD M SM (@wand L sL x y)) *)
  unfold Semantics.stable in *.
(* Goal: forall (x y z : @expr L) (_ : @semantic_stable L MD kMD M R2 SM stableSM x) (m : @Kworlds MD kMD M), @satisfies L MD SM (@build_model MD kMD M m) (@iffp L minL pL (@sepcon L sL (@andp L pL x y) z) (@andp L pL x (@sepcon L sL y z))) *)
  intros.
(* Goal: iff (@Kdenotation L MD kMD M SM (@orp L pL x y) m) (@Kdenotation L MD kMD M SM (@orp L pL x y) n) *)
  unfold Kdenotation in *; simpl in *.
(* Goal: iff (@denotation L MD SM (@orp L pL x y) (@build_model MD kMD M m)) (@denotation L MD SM (@orp L pL x y) (@build_model MD kMD M n)) *)
  rewrite !(app_same_set (denote_orp _ _)).
(* Goal: iff (@Semantics.orp (@model MD) (@denotation L MD SM x) (@denotation L MD SM y) (@build_model MD kMD M m)) (@Semantics.orp (@model MD) (@denotation L MD SM x) (@denotation L MD SM y) (@build_model MD kMD M n)) *)
  unfold Semantics.orp; simpl.
(* Goal: @satisfies L MD SM (@build_model MD kMD M n) x *)
  specialize (H _ _ H1).
(* Goal: iff (or (@denotation L MD SM x (@build_model MD kMD M m)) (@denotation L MD SM y (@build_model MD kMD M m))) (or (@denotation L MD SM x (@build_model MD kMD M n)) (@denotation L MD SM y (@build_model MD kMD M n))) *)
  specialize (H0 _ _ H1).
(* Goal: @Kdenotation L MD kMD M SM y m2 *)
  tauto.
Qed.

Lemma sound_falsep_stable {L: Language} {minL: MinimunLanguage L} {pL: PropositionalLanguage L} {MD: Model} {kMD: KripkeModel MD} {M: Kmodel} {R: SS.Relation (Kworlds M)} {SM: Semantics L MD} {tpSM: TrivialPropositionalSemantics L MD SM} {stableSM: SemanticStable L MD M SM}:
  semantic_stable falsep.
Proof.
(* Goal: forall (x y z : @expr L) (_ : @semantic_stable L MD kMD M R2 SM stableSM x) (m : @Kworlds MD kMD M), @satisfies L MD SM (@build_model MD kMD M m) (@iffp L minL pL (@sepcon L sL (@andp L pL x y) z) (@andp L pL x (@sepcon L sL y z))) *)
  intros.
(* Goal: @semantic_stable L MD kMD M R SM stableSM (@falsep L pL) *)
  rewrite denote_stable.
(* Goal: iff (@Semantics.stable (@Kworlds MD kMD M) R (@Kdenotation L MD kMD M SM x)) (@Semantics.stable (@Kworlds MD kMD M) R (@Kdenotation L MD kMD M SM y)) *)
  unfold Semantics.stable.
(* Goal: forall (x y z : @expr L) (_ : @semantic_stable L MD kMD M R2 SM stableSM x) (m : @Kworlds MD kMD M), @satisfies L MD SM (@build_model MD kMD M m) (@iffp L minL pL (@sepcon L sL (@andp L pL x y) z) (@andp L pL x (@sepcon L sL y z))) *)
  intros.
(* Goal: iff (@Kdenotation L MD kMD M SM (@falsep L pL) m) (@Kdenotation L MD kMD M SM (@falsep L pL) n) *)
  unfold Kdenotation.
(* Goal: iff (@denotation L MD SM (@falsep L pL) (@build_model MD kMD M m)) (@denotation L MD SM (@falsep L pL) (@build_model MD kMD M n)) *)
  rewrite !(app_same_set denote_falsep).
(* Goal: iff (@Semantics.falsep (@model MD) (@build_model MD kMD M m)) (@Semantics.falsep (@model MD) (@build_model MD kMD M n)) *)
  reflexivity.
Qed.

Lemma sound_stable_proper_iffp {L: Language} {minL: MinimunLanguage L} {pL: PropositionalLanguage L} {MD: Model} {kMD: KripkeModel MD} {M: Kmodel} {R: SS.Relation (Kworlds M)} {SM: Semantics L MD} {tminSM: TrivialMinimunSemantics L MD SM} {tpSM: TrivialPropositionalSemantics L MD SM} {stableSM: SemanticStable L MD M SM}:
  forall x y,
    (forall m, KRIPKE: M, m |= x <--> y) ->
    (semantic_stable x <-> semantic_stable y).
Proof.
(* Goal: forall (x y z : @expr L) (_ : @semantic_stable L MD kMD M R2 SM stableSM x) (m : @Kworlds MD kMD M), @satisfies L MD SM (@build_model MD kMD M m) (@iffp L minL pL (@sepcon L sL (@andp L pL x y) z) (@andp L pL x (@sepcon L sL y z))) *)
  intros.
(* Goal: iff (@semantic_stable L MD kMD M R SM stableSM x) (@semantic_stable L MD kMD M R SM stableSM y) *)
  rewrite !denote_stable.
(* Goal: iff (@Semantics.stable (@Kworlds MD kMD M) R (@Kdenotation L MD kMD M SM x)) (@Semantics.stable (@Kworlds MD kMD M) R (@Kdenotation L MD kMD M SM y)) *)
  unfold Semantics.stable.
(* Goal: iff (forall (m n : @Kworlds MD kMD M) (_ : R m n), iff (@Kdenotation L MD kMD M SM x m) (@Kdenotation L MD kMD M SM x n)) (forall (m n : @Kworlds MD kMD M) (_ : R m n), iff (@Kdenotation L MD kMD M SM y m) (@Kdenotation L MD kMD M SM y n)) *)
  assert (forall m, Kdenotation M x m <-> Kdenotation M y m).
  + intros m.
(* Goal: iff (@Kdenotation L MD kMD M SM x m) (@Kdenotation L MD kMD M SM y m) *)
    specialize (H m).
(* Goal: iff (@Kdenotation L MD kMD M SM x m) (@Kdenotation L MD kMD M SM y m) *)
    unfold iffp in H; rewrite sat_andp, !sat_impp in H.
(* Goal: iff (@Kdenotation L MD kMD M SM x m) (@Kdenotation L MD kMD M SM y m) *)
    destruct H.
(* Goal: @Kdenotation L MD kMD M SM y m2 *)
    tauto.
  + split; intros HH ? ? H1;
    specialize (HH _ _ H1).
    - rewrite !H0 in HH.
(* Goal: and (@satisfies L MD SM (@build_model MD kMD M m1) x) (@satisfies L MD SM (@build_model MD kMD M m1) y) *)
      auto.
    - rewrite !H0.
(* Goal: and (@satisfies L MD SM (@build_model MD kMD M m1) x) (@satisfies L MD SM (@build_model MD kMD M m1) y) *)
      auto.
Qed.

Lemma sound_boxp_stable {L: Language} {minL: MinimunLanguage L} {mL: ModalLanguage L} {MD: Model} {kMD: KripkeModel MD} {M: Kmodel} {R1: KM.Relation (Kworlds M)} {R2: SS.Relation (Kworlds M)} {R1_bis: Bisimulation SS.Krelation KM.Krelation} {SM: Semantics L MD} {kmSM: KripkeModalSemantics L MD M SM} {stableSM: SemanticStable L MD M SM}:
  forall x: expr,
    semantic_stable x -> semantic_stable (boxp x).
Proof.
(* Goal: forall (x y z : @expr L) (_ : @semantic_stable L MD kMD M R2 SM stableSM x) (m : @Kworlds MD kMD M), @satisfies L MD SM (@build_model MD kMD M m) (@iffp L minL pL (@sepcon L sL (@andp L pL x y) z) (@andp L pL x (@sepcon L sL y z))) *)
  intros.
  rewrite denote_stable in H |- *.
(* Goal: @Semantics.stable (@Kworlds MD kMD M) R2 (@Kdenotation L MD kMD M SM (@wand L sL x y)) *)
  unfold Semantics.stable in *.
(* Goal: forall (x y z : @expr L) (_ : @semantic_stable L MD kMD M R2 SM stableSM x) (m : @Kworlds MD kMD M), @satisfies L MD SM (@build_model MD kMD M m) (@iffp L minL pL (@sepcon L sL (@andp L pL x y) z) (@andp L pL x (@sepcon L sL y z))) *)
  intros.
(* Goal: iff (@Kdenotation L MD kMD M SM (@boxp L mL x) m) (@Kdenotation L MD kMD M SM (@boxp L mL x) n) *)
  rewrite !(app_same_set (denote_boxp _)).
(* Goal: iff (@Semantics.boxp (@Kworlds MD kMD M) R1 (@Kdenotation L MD kMD M SM x) m) (@Semantics.boxp (@Kworlds MD kMD M) R1 (@Kdenotation L MD kMD M SM x) n) *)
  unfold Semantics.boxp; simpl.
(* Goal: iff (forall (m1 m2 : @Kworlds MD kMD M) (_ : @join (@Kworlds MD kMD M) J m m1 m2) (_ : @Kdenotation L MD kMD M SM x m1), @Kdenotation L MD kMD M SM y m2) (forall (m1 m2 : @Kworlds MD kMD M) (_ : @join (@Kworlds MD kMD M) J n m1 m2) (_ : @Kdenotation L MD kMD M SM x m1), @Kdenotation L MD kMD M SM y m2) *)
  split.
  + pose proof bis_r _ _ H0.
(* Goal: forall (x y z : @expr L) (_ : @semantic_stable L MD kMD M R2 SM stableSM x) (m : @Kworlds MD kMD M), @satisfies L MD SM (@build_model MD kMD M m) (@iffp L minL pL (@sepcon L sL (@andp L pL x y) z) (@andp L pL x (@sepcon L sL y z))) *)
    intros.
(* Goal: @Kdenotation L MD kMD M SM x m0 *)
    specialize (H1 _ H3).
(* Goal: @Kdenotation L MD kMD M SM x n0 *)
    destruct H1 as [m0 [? ?]].
(* Goal: @Kdenotation L MD kMD M SM x m0 *)
    specialize (H2 _ H1).
(* Goal: @Kdenotation L MD kMD M SM x m0 *)
    specialize (H _ _ H4).
(* Goal: @Kdenotation L MD kMD M SM y m2 *)
    tauto.
  + pose proof bis_l _ _ H0.
(* Goal: forall (_ : forall (n0 : @Kworlds MD kMD M) (_ : @KM.Krelation (@Kworlds MD kMD M) R1 n n0), @Kdenotation L MD kMD M SM x n0) (n : @Kworlds MD kMD M) (_ : @KM.Krelation (@Kworlds MD kMD M) R1 m n), @Kdenotation L MD kMD M SM x n *)
    intros; rename n0 into m0.
(* Goal: @Kdenotation L MD kMD M SM x m0 *)
    specialize (H1 _ H3).
(* Goal: @Kdenotation L MD kMD M SM x m0 *)
    destruct H1 as [n0 [? ?]].
(* Goal: @Kdenotation L MD kMD M SM x m0 *)
    specialize (H2 _ H1).
(* Goal: @Kdenotation L MD kMD M SM x m0 *)
    specialize (H _ _ H4).
(* Goal: @Kdenotation L MD kMD M SM y m2 *)
    tauto.
Qed.

Lemma sound_boxp_absorb_stable {L: Language} {minL: MinimunLanguage L} {pL: PropositionalLanguage L} {mL: ModalLanguage L} {MD: Model} {kMD: KripkeModel MD} {M: Kmodel} {R1: KM.Relation (Kworlds M)} {R2: SS.Relation (Kworlds M)} {R1_incl: Inclusion KM.Krelation SS.Krelation} {SM: Semantics L MD} {tminSM: TrivialMinimunSemantics L MD SM} {tpSM: TrivialPropositionalSemantics L MD SM} {kmSM: KripkeModalSemantics L MD M SM} {stableSM: SemanticStable L MD M SM}:
  forall x: expr,
    semantic_stable x ->
    (forall (m: Kworlds M), KRIPKE: M, m |= x --> boxp x).
Proof.
(* Goal: forall (x y z : @expr L) (_ : @semantic_stable L MD kMD M R2 SM stableSM x) (m : @Kworlds MD kMD M), @satisfies L MD SM (@build_model MD kMD M m) (@iffp L minL pL (@sepcon L sL (@andp L pL x y) z) (@andp L pL x (@sepcon L sL y z))) *)
  intros.
(* Goal: @satisfies L MD SM (@build_model MD kMD M m) (@impp L minL x (@boxp L mL x)) *)
  rewrite sat_impp, sat_boxp.
(* Goal: forall (x y z : @expr L) (_ : @semantic_stable L MD kMD M R2 SM stableSM x) (m : @Kworlds MD kMD M), @satisfies L MD SM (@build_model MD kMD M m) (@iffp L minL pL (@sepcon L sL (@andp L pL x y) z) (@andp L pL x (@sepcon L sL y z))) *)
  intros.
(* 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) J m1 m2 n) (and (@satisfies L MD SM (@build_model MD kMD M m1) (@andp L pL x y)) (@satisfies L MD SM (@build_model MD kMD M m2) z)))) *)
  rewrite denote_stable in H.
(* Goal: @satisfies L MD SM (@build_model MD kMD M n) x *)
  unfold Semantics.stable in H.
(* Goal: @satisfies L MD SM (@build_model MD kMD M n) x *)
  apply including in H1.
(* Goal: @satisfies L MD SM (@build_model MD kMD M n) x *)
  specialize (H _ _ H1).
(* Goal: @Kdenotation L MD kMD M SM y m2 *)
  tauto.
Qed.

End Sound_Trivial.

Module Sound_KripkeIntuitionistic.

Import Logic.GeneralLogic.Semantics.Kripke.
Import Logic.MinimunLogic.Semantics.Kripke.
Import Logic.PropositionalLogic.Semantics.Kripke.
Import Logic.ModalLogic.Semantics.Flat.
Import Logic.SeparationLogic.Semantics.FlatSemantics.

Lemma sound_impp_stable {L: Language} {minL: MinimunLanguage L} {pL: PropositionalLanguage L} {MD: Model} {kMD: KripkeModel MD} {M: Kmodel} {R1: KI.Relation (Kworlds M)} {R2: SS.Relation (Kworlds M)} {R1_bis: Bisimulation SS.Krelation KI.Krelation} {SM: Semantics L MD} {kiSM: KripkeIntuitionisticSemantics L MD M SM} {kminSM: KripkeMinimunSemantics L MD M SM} {kpSM: KripkePropositionalSemantics L MD M SM} {stableSM: SemanticStable L MD M SM}:
  forall x y: expr,
    semantic_stable x -> semantic_stable y -> semantic_stable (x --> y).
Proof.
(* Goal: forall (x y z : @expr L) (_ : @semantic_stable L MD kMD M R2 SM stableSM x) (m : @Kworlds MD kMD M), @satisfies L MD SM (@build_model MD kMD M m) (@iffp L minL pL (@sepcon L sL (@andp L pL x y) z) (@andp L pL x (@sepcon L sL y z))) *)
  intros.
(* Goal: @semantic_stable L MD kMD M R2 SM stableSM (@wand L sL x y) *)
  rewrite denote_stable in H, H0 |- *.
(* Goal: @Semantics.stable (@Kworlds MD kMD M) R2 (@Kdenotation L MD kMD M SM (@wand L sL x y)) *)
  unfold Semantics.stable in *.
(* Goal: forall (x y z : @expr L) (_ : @semantic_stable L MD kMD M R2 SM stableSM x) (m : @Kworlds MD kMD M), @satisfies L MD SM (@build_model MD kMD M m) (@iffp L minL pL (@sepcon L sL (@andp L pL x y) z) (@andp L pL x (@sepcon L sL y z))) *)
  intros.
(* Goal: iff (@denotation L MD SM (@impp L minL x y) (@build_model MD kMD M m)) (@denotation L MD SM (@impp L minL x y) (@build_model MD kMD M n)) *)
  rewrite !(app_same_set (denote_impp _ _)).
(* Goal: iff (@Semantics.impp (@model MD) (@denotation L MD SM x) (@denotation L MD SM y) (@build_model MD kMD M m)) (@Semantics.impp (@model MD) (@denotation L MD SM x) (@denotation L MD SM y) (@build_model MD kMD M n)) *)
  unfold Semantics.impp; simpl.
(* Goal: iff (forall (m1 m2 : @Kworlds MD kMD M) (_ : @join (@Kworlds MD kMD M) J m m1 m2) (_ : @Kdenotation L MD kMD M SM x m1), @Kdenotation L MD kMD M SM y m2) (forall (m1 m2 : @Kworlds MD kMD M) (_ : @join (@Kworlds MD kMD M) J n m1 m2) (_ : @Kdenotation L MD kMD M SM x m1), @Kdenotation L MD kMD M SM y m2) *)
  split.
  + pose proof bis_r _ _ H1.
(* Goal: forall (x y z : @expr L) (_ : @semantic_stable L MD kMD M R2 SM stableSM x) (m : @Kworlds MD kMD M), @satisfies L MD SM (@build_model MD kMD M m) (@iffp L minL pL (@sepcon L sL (@andp L pL x y) z) (@andp L pL x (@sepcon L sL y z))) *)
    intros.
    specialize (H2 _ H4).
    destruct H2 as [m0 [? ?]].
    specialize (H3 _ H2).
(* Goal: @Kdenotation L MD kMD M SM y m2 *)
    specialize (H _ _ H6).
    specialize (H0 _ _ H6).
(* Goal: @Kdenotation L MD kMD M SM y m2 *)
    tauto.
  + pose proof bis_l _ _ H1.
(* Goal: forall (x y z : @expr L) (_ : @semantic_stable L MD kMD M R2 SM stableSM x) (m : @Kworlds MD kMD M), @satisfies L MD SM (@build_model MD kMD M m) (@iffp L minL pL (@sepcon L sL (@andp L pL x y) z) (@andp L pL x (@sepcon L sL y z))) *)
    intros.
    rename n0 into m0.
    specialize (H2 _ H4).
    destruct H2 as [n0 [? ?]].
    specialize (H3 _ H2).
(* Goal: @Kdenotation L MD kMD M SM y m2 *)
    specialize (H _ _ H6).
    specialize (H0 _ _ H6).
(* Goal: @Kdenotation L MD kMD M SM y m2 *)
    tauto.
Qed.

Lemma sound_andp_stable {L: Language} {minL: MinimunLanguage L} {pL: PropositionalLanguage L} {MD: Model} {kMD: KripkeModel MD} {M: Kmodel} {R1: KI.Relation (Kworlds M)} {R2: SS.Relation (Kworlds M)} {SM: Semantics L MD} {kiSM: KripkeIntuitionisticSemantics L MD M SM} {kminSM: KripkeMinimunSemantics L MD M SM} {kpSM: KripkePropositionalSemantics L MD M SM} {stableSM: SemanticStable L MD M SM}:
  forall x y: expr,
    semantic_stable x -> semantic_stable y -> semantic_stable (x && y).
Proof.
(* Goal: forall (x y z : @expr L) (_ : @semantic_stable L MD kMD M R2 SM stableSM x) (m : @Kworlds MD kMD M), @satisfies L MD SM (@build_model MD kMD M m) (@iffp L minL pL (@sepcon L sL (@andp L pL x y) z) (@andp L pL x (@sepcon L sL y z))) *)
  intros.
(* Goal: @semantic_stable L MD kMD M R2 SM stableSM (@wand L sL x y) *)
  rewrite denote_stable in H, H0 |- *.
(* Goal: @Semantics.stable (@Kworlds MD kMD M) R2 (@Kdenotation L MD kMD M SM (@wand L sL x y)) *)
  unfold Semantics.stable in *.
(* Goal: forall (x y z : @expr L) (_ : @semantic_stable L MD kMD M R2 SM stableSM x) (m : @Kworlds MD kMD M), @satisfies L MD SM (@build_model MD kMD M m) (@iffp L minL pL (@sepcon L sL (@andp L pL x y) z) (@andp L pL x (@sepcon L sL y z))) *)
  intros.
(* Goal: iff (@denotation L MD SM (@andp L pL x y) (@build_model MD kMD M m)) (@denotation L MD SM (@andp L pL x y) (@build_model MD kMD M n)) *)
  rewrite !(app_same_set (denote_andp _ _)).
(* Goal: iff (@Semantics.andp (@model MD) (@denotation L MD SM x) (@denotation L MD SM y) (@build_model MD kMD M m)) (@Semantics.andp (@model MD) (@denotation L MD SM x) (@denotation L MD SM y) (@build_model MD kMD M n)) *)
  unfold Semantics.andp; simpl.
(* Goal: @satisfies L MD SM (@build_model MD kMD M n) x *)
  specialize (H _ _ H1).
(* Goal: iff (or (@denotation L MD SM x (@build_model MD kMD M m)) (@denotation L MD SM y (@build_model MD kMD M m))) (or (@denotation L MD SM x (@build_model MD kMD M n)) (@denotation L MD SM y (@build_model MD kMD M n))) *)
  specialize (H0 _ _ H1).
(* Goal: @Kdenotation L MD kMD M SM y m2 *)
  tauto.
Qed.

Lemma sound_orp_stable {L: Language} {minL: MinimunLanguage L} {pL: PropositionalLanguage L} {MD: Model} {kMD: KripkeModel MD} {M: Kmodel} {R1: KI.Relation (Kworlds M)} {R2: SS.Relation (Kworlds M)} {SM: Semantics L MD} {kiSM: KripkeIntuitionisticSemantics L MD M SM} {kminSM: KripkeMinimunSemantics L MD M SM} {kpSM: KripkePropositionalSemantics L MD M SM} {stableSM: SemanticStable L MD M SM}:
  forall x y: expr,
    semantic_stable x -> semantic_stable y -> semantic_stable (x || y).
Proof.
(* Goal: forall (x y z : @expr L) (_ : @semantic_stable L MD kMD M R2 SM stableSM x) (m : @Kworlds MD kMD M), @satisfies L MD SM (@build_model MD kMD M m) (@iffp L minL pL (@sepcon L sL (@andp L pL x y) z) (@andp L pL x (@sepcon L sL y z))) *)
  intros.
(* Goal: @semantic_stable L MD kMD M R2 SM stableSM (@wand L sL x y) *)
  rewrite denote_stable in H, H0 |- *.
(* Goal: @Semantics.stable (@Kworlds MD kMD M) R2 (@Kdenotation L MD kMD M SM (@wand L sL x y)) *)
  unfold Semantics.stable in *.
(* Goal: forall (x y z : @expr L) (_ : @semantic_stable L MD kMD M R2 SM stableSM x) (m : @Kworlds MD kMD M), @satisfies L MD SM (@build_model MD kMD M m) (@iffp L minL pL (@sepcon L sL (@andp L pL x y) z) (@andp L pL x (@sepcon L sL y z))) *)
  intros.
(* Goal: iff (@denotation L MD SM (@orp L pL x y) (@build_model MD kMD M m)) (@denotation L MD SM (@orp L pL x y) (@build_model MD kMD M n)) *)
  rewrite !(app_same_set (denote_orp _ _)).
(* Goal: iff (@Semantics.orp (@model MD) (@denotation L MD SM x) (@denotation L MD SM y) (@build_model MD kMD M m)) (@Semantics.orp (@model MD) (@denotation L MD SM x) (@denotation L MD SM y) (@build_model MD kMD M n)) *)
  unfold Semantics.orp; simpl.
(* Goal: @satisfies L MD SM (@build_model MD kMD M n) x *)
  specialize (H _ _ H1).
(* Goal: iff (or (@denotation L MD SM x (@build_model MD kMD M m)) (@denotation L MD SM y (@build_model MD kMD M m))) (or (@denotation L MD SM x (@build_model MD kMD M n)) (@denotation L MD SM y (@build_model MD kMD M n))) *)
  specialize (H0 _ _ H1).
(* Goal: @Kdenotation L MD kMD M SM y m2 *)
  tauto.
Qed.

Lemma sound_falsep_stable {L: Language} {minL: MinimunLanguage L} {pL: PropositionalLanguage L} {MD: Model} {kMD: KripkeModel MD} {M: Kmodel} {R1: KI.Relation (Kworlds M)} {R2: SS.Relation (Kworlds M)} {SM: Semantics L MD} {kiSM: KripkeIntuitionisticSemantics L MD M SM} {kminSM: KripkeMinimunSemantics L MD M SM} {kpSM: KripkePropositionalSemantics L MD M SM} {stableSM: SemanticStable L MD M SM}:
  semantic_stable falsep.
Proof.
(* Goal: forall (x y z : @expr L) (_ : @semantic_stable L MD kMD M R2 SM stableSM x) (m : @Kworlds MD kMD M), @satisfies L MD SM (@build_model MD kMD M m) (@iffp L minL pL (@sepcon L sL (@andp L pL x y) z) (@andp L pL x (@sepcon L sL y z))) *)
  intros.
(* Goal: @semantic_stable L MD kMD M R SM stableSM (@falsep L pL) *)
  rewrite denote_stable.
(* Goal: iff (@Semantics.stable (@Kworlds MD kMD M) R (@Kdenotation L MD kMD M SM x)) (@Semantics.stable (@Kworlds MD kMD M) R (@Kdenotation L MD kMD M SM y)) *)
  unfold Semantics.stable.
(* Goal: forall (x y z : @expr L) (_ : @semantic_stable L MD kMD M R2 SM stableSM x) (m : @Kworlds MD kMD M), @satisfies L MD SM (@build_model MD kMD M m) (@iffp L minL pL (@sepcon L sL (@andp L pL x y) z) (@andp L pL x (@sepcon L sL y z))) *)
  intros.
(* Goal: iff (@denotation L MD SM (@falsep L pL) (@build_model MD kMD M m)) (@denotation L MD SM (@falsep L pL) (@build_model MD kMD M n)) *)
  rewrite !(app_same_set denote_falsep).
(* Goal: iff (@Semantics.falsep (@model MD) (@build_model MD kMD M m)) (@Semantics.falsep (@model MD) (@build_model MD kMD M n)) *)
  reflexivity.
Qed.

Lemma sound_stable_proper_iffp {L: Language} {minL: MinimunLanguage L} {pL: PropositionalLanguage L} {MD: Model} {kMD: KripkeModel MD} {M: Kmodel} {R1: KI.Relation (Kworlds M)} {po_R: PreOrder KI.Krelation} {R2: SS.Relation (Kworlds M)} {SM: Semantics L MD} {kiSM: KripkeIntuitionisticSemantics L MD M SM} {kminSM: KripkeMinimunSemantics L MD M SM} {kpSM: KripkePropositionalSemantics L MD M SM} {stableSM: SemanticStable L MD M SM}:
  forall x y,
    (forall m, KRIPKE: M, m |= x <--> y) ->
    (semantic_stable x <-> semantic_stable y).
Proof.
(* Goal: forall (x y z : @expr L) (_ : @semantic_stable L MD kMD M R2 SM stableSM x) (m : @Kworlds MD kMD M), @satisfies L MD SM (@build_model MD kMD M m) (@iffp L minL pL (@sepcon L sL (@andp L pL x y) z) (@andp L pL x (@sepcon L sL y z))) *)
  intros.
(* Goal: iff (@semantic_stable L MD kMD M R SM stableSM x) (@semantic_stable L MD kMD M R SM stableSM y) *)
  rewrite !denote_stable.
(* Goal: iff (@Semantics.stable (@Kworlds MD kMD M) R (@Kdenotation L MD kMD M SM x)) (@Semantics.stable (@Kworlds MD kMD M) R (@Kdenotation L MD kMD M SM y)) *)
  unfold Semantics.stable.
(* Goal: iff (forall (m n : @Kworlds MD kMD M) (_ : R m n), iff (@Kdenotation L MD kMD M SM x m) (@Kdenotation L MD kMD M SM x n)) (forall (m n : @Kworlds MD kMD M) (_ : R m n), iff (@Kdenotation L MD kMD M SM y m) (@Kdenotation L MD kMD M SM y n)) *)
  assert (forall m, Kdenotation M x m <-> Kdenotation M y m).
  + intros m.
(* Goal: iff (@Kdenotation L MD kMD M SM x m) (@Kdenotation L MD kMD M SM y m) *)
    specialize (H m).
(* Goal: iff (@Kdenotation L MD kMD M SM x m) (@Kdenotation L MD kMD M SM y m) *)
    unfold iffp in H; rewrite sat_andp, !sat_impp in H.
(* Goal: iff (@Kdenotation L MD kMD M SM x m) (@Kdenotation L MD kMD M SM y m) *)
    destruct H.
(* Goal: forall (x y z : @expr L) (_ : @semantic_stable L MD kMD M R2 SM stableSM x) (m : @Kworlds MD kMD M), @satisfies L MD SM (@build_model MD kMD M m) (@iffp L minL pL (@sepcon L sL (@andp L pL x y) z) (@andp L pL x (@sepcon L sL y z))) *)
    split; intros.
    - apply (H m); auto.
(* Goal: iff (@Semantics.falsep (@model MD) (@build_model MD kMD M m)) (@Semantics.falsep (@model MD) (@build_model MD kMD M n)) *)
      reflexivity.
    - apply (H0 m); auto.
(* Goal: iff (@Semantics.falsep (@model MD) (@build_model MD kMD M m)) (@Semantics.falsep (@model MD) (@build_model MD kMD M n)) *)
      reflexivity.
  + split; intros HH ? ? H1;
    specialize (HH _ _ H1).
    - rewrite !H0 in HH.
(* Goal: and (@satisfies L MD SM (@build_model MD kMD M m1) x) (@satisfies L MD SM (@build_model MD kMD M m1) y) *)
      auto.
    - rewrite !H0.
(* Goal: and (@satisfies L MD SM (@build_model MD kMD M m1) x) (@satisfies L MD SM (@build_model MD kMD M m1) y) *)
      auto.
Qed.

Lemma sound_boxp_stable {L: Language} {minL: MinimunLanguage L} {pL: PropositionalLanguage L} {mL: ModalLanguage L} {MD: Model} {kMD: KripkeModel MD} {M: Kmodel} {R1: KI.Relation (Kworlds M)} {R2: KM.Relation (Kworlds M)} {R3: SS.Relation (Kworlds M)} {R2_bis: Bisimulation SS.Krelation KM.Krelation} {SM: Semantics L MD} {fmSM: FlatModalSemantics L MD M SM} {stableSM: SemanticStable L MD M SM}:
  forall x: expr,
    semantic_stable x -> semantic_stable (boxp x).
Proof.
(* Goal: forall (x y z : @expr L) (_ : @semantic_stable L MD kMD M R2 SM stableSM x) (m : @Kworlds MD kMD M), @satisfies L MD SM (@build_model MD kMD M m) (@iffp L minL pL (@sepcon L sL (@andp L pL x y) z) (@andp L pL x (@sepcon L sL y z))) *)
  intros.
  rewrite denote_stable in H |- *.
(* Goal: @Semantics.stable (@Kworlds MD kMD M) R2 (@Kdenotation L MD kMD M SM (@wand L sL x y)) *)
  unfold Semantics.stable in *.
(* Goal: forall (x y z : @expr L) (_ : @semantic_stable L MD kMD M R2 SM stableSM x) (m : @Kworlds MD kMD M), @satisfies L MD SM (@build_model MD kMD M m) (@iffp L minL pL (@sepcon L sL (@andp L pL x y) z) (@andp L pL x (@sepcon L sL y z))) *)
  intros.
(* Goal: iff (@Kdenotation L MD kMD M SM (@boxp L mL x) m) (@Kdenotation L MD kMD M SM (@boxp L mL x) n) *)
  rewrite !(app_same_set (denote_boxp _)).
(* Goal: iff (@Semantics.boxp (@Kworlds MD kMD M) R1 (@Kdenotation L MD kMD M SM x) m) (@Semantics.boxp (@Kworlds MD kMD M) R1 (@Kdenotation L MD kMD M SM x) n) *)
  unfold Semantics.boxp; simpl.
(* Goal: iff (forall (m1 m2 : @Kworlds MD kMD M) (_ : @join (@Kworlds MD kMD M) J m m1 m2) (_ : @Kdenotation L MD kMD M SM x m1), @Kdenotation L MD kMD M SM y m2) (forall (m1 m2 : @Kworlds MD kMD M) (_ : @join (@Kworlds MD kMD M) J n m1 m2) (_ : @Kdenotation L MD kMD M SM x m1), @Kdenotation L MD kMD M SM y m2) *)
  split.
  + pose proof bis_r _ _ H0.
(* Goal: forall (x y z : @expr L) (_ : @semantic_stable L MD kMD M R2 SM stableSM x) (m : @Kworlds MD kMD M), @satisfies L MD SM (@build_model MD kMD M m) (@iffp L minL pL (@sepcon L sL (@andp L pL x y) z) (@andp L pL x (@sepcon L sL y z))) *)
    intros.
(* Goal: @Kdenotation L MD kMD M SM x m0 *)
    specialize (H1 _ H3).
(* Goal: @Kdenotation L MD kMD M SM x n0 *)
    destruct H1 as [m0 [? ?]].
(* Goal: @Kdenotation L MD kMD M SM x m0 *)
    specialize (H2 _ H1).
(* Goal: @Kdenotation L MD kMD M SM x m0 *)
    specialize (H _ _ H4).
(* Goal: @Kdenotation L MD kMD M SM y m2 *)
    tauto.
  + pose proof bis_l _ _ H0.
(* Goal: forall (x y z : @expr L) (_ : @semantic_stable L MD kMD M R2 SM stableSM x) (m : @Kworlds MD kMD M), @satisfies L MD SM (@build_model MD kMD M m) (@iffp L minL pL (@sepcon L sL (@andp L pL x y) z) (@andp L pL x (@sepcon L sL y z))) *)
    intros.
    rename n0 into m0.
(* Goal: @Kdenotation L MD kMD M SM x m0 *)
    specialize (H1 _ H3).
(* Goal: @Kdenotation L MD kMD M SM x m0 *)
    destruct H1 as [n0 [? ?]].
(* Goal: @Kdenotation L MD kMD M SM x m0 *)
    specialize (H2 _ H1).
(* Goal: @Kdenotation L MD kMD M SM x m0 *)
    specialize (H _ _ H4).
(* Goal: @Kdenotation L MD kMD M SM y m2 *)
    tauto.
Qed.

Lemma sound_boxp_absorb_stable {L: Language} {minL: MinimunLanguage L} {pL: PropositionalLanguage L} {mL: ModalLanguage L} {MD: Model} {kMD: KripkeModel MD} {M: Kmodel} {R1: KI.Relation (Kworlds M)} {R2: KM.Relation (Kworlds M)} {R3: SS.Relation (Kworlds M)} {R2_incl: Inclusion KM.Krelation SS.Krelation} {SM: Semantics L MD} {kiSM: KripkeIntuitionisticSemantics L MD M SM} {kminSM: KripkeMinimunSemantics L MD M SM} {kpSM: KripkePropositionalSemantics L MD M SM} {fmSM: FlatModalSemantics L MD M SM} {stableSM: SemanticStable L MD M SM}:
  forall x: expr,
    semantic_stable x ->
    (forall (m: Kworlds M), KRIPKE: M, m |= x --> boxp x).
Proof.
(* Goal: forall (x y z : @expr L) (_ : @semantic_stable L MD kMD M R2 SM stableSM x) (m : @Kworlds MD kMD M), @satisfies L MD SM (@build_model MD kMD M m) (@iffp L minL pL (@sepcon L sL (@andp L pL x y) z) (@andp L pL x (@sepcon L sL y z))) *)
  intros.
  rewrite sat_impp.
(* Goal: forall (x y z : @expr L) (_ : @semantic_stable L MD kMD M R2 SM stableSM x) (m : @Kworlds MD kMD M), @satisfies L MD SM (@build_model MD kMD M m) (@iffp L minL pL (@sepcon L sL (@andp L pL x y) z) (@andp L pL x (@sepcon L sL y z))) *)
  intros.
  rewrite sat_boxp.
(* Goal: forall (x y z : @expr L) (_ : @semantic_stable L MD kMD M R2 SM stableSM x) (m : @Kworlds MD kMD M), @satisfies L MD SM (@build_model MD kMD M m) (@iffp L minL pL (@sepcon L sL (@andp L pL x y) z) (@andp L pL x (@sepcon L sL y z))) *)
  intros.
(* 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) J m1 m2 n) (and (@satisfies L MD SM (@build_model MD kMD M m1) (@andp L pL x y)) (@satisfies L MD SM (@build_model MD kMD M m2) z)))) *)
  rewrite denote_stable in H.
(* Goal: @satisfies L MD SM (@build_model MD kMD M n) x *)
  unfold Semantics.stable in H.
  apply including in H2.
  specialize (H _ _ H2).
(* Goal: @Kdenotation L MD kMD M SM y m2 *)
  tauto.
Qed.

Lemma sound_sepcon_stable {L: Language} {minL: MinimunLanguage L} {pL: PropositionalLanguage L} {sL: SeparationLanguage L} {MD: Model} {kMD: KripkeModel MD} {M: Kmodel} {R1: KI.Relation (Kworlds M)} {R2: SS.Relation (Kworlds M)} {J: Join (Kworlds M)} {SAbis: SeparationAlgebraBisStable (Kworlds M)} {SM: Semantics L MD} {fsSM: SeparatingSemantics L MD M SM} {stableSM: SemanticStable L MD M SM}:
  forall x y: expr,
    semantic_stable x -> semantic_stable y -> semantic_stable (x * y).
Proof.
(* Goal: forall (x y z : @expr L) (_ : @semantic_stable L MD kMD M R2 SM stableSM x) (m : @Kworlds MD kMD M), @satisfies L MD SM (@build_model MD kMD M m) (@iffp L minL pL (@sepcon L sL (@andp L pL x y) z) (@andp L pL x (@sepcon L sL y z))) *)
  intros.
(* Goal: @semantic_stable L MD kMD M R2 SM stableSM (@wand L sL x y) *)
  rewrite denote_stable in H, H0 |- *.
(* Goal: @Semantics.stable (@Kworlds MD kMD M) R2 (@Kdenotation L MD kMD M SM (@wand L sL x y)) *)
  unfold Semantics.stable in *.
(* Goal: forall (x y z : @expr L) (_ : @semantic_stable L MD kMD M R2 SM stableSM x) (m : @Kworlds MD kMD M), @satisfies L MD SM (@build_model MD kMD M m) (@iffp L minL pL (@sepcon L sL (@andp L pL x y) z) (@andp L pL x (@sepcon L sL y z))) *)
  intros.
(* Goal: iff (@Kdenotation L MD kMD M SM (@sepcon L sL x y) m) (@Kdenotation L MD kMD M SM (@sepcon L sL x y) n) *)
  rewrite !(app_same_set (denote_sepcon _ _)).
(* Goal: iff (@WeakSemantics.sepcon (@Kworlds MD kMD M) J (@Kdenotation L MD kMD M SM x) (@Kdenotation L MD kMD M SM y) m) (@WeakSemantics.sepcon (@Kworlds MD kMD M) J (@Kdenotation L MD kMD M SM x) (@Kdenotation L MD kMD M SM y) n) *)
  unfold WeakSemantics.sepcon; simpl.
(* Goal: iff (@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) J m1 m2 m) (and (@Kdenotation L MD kMD M SM x m1) (@Kdenotation L MD kMD M SM y m2))))) (@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) J m1 m2 n) (and (@Kdenotation L MD kMD M SM x m1) (@Kdenotation L MD kMD M SM y m2))))) *)
  pose proof split_bis_stable _ _ H1.
(* Goal: forall (x y z : @expr L) (_ : @semantic_stable L MD kMD M R2 SM stableSM x) (m : @Kworlds MD kMD M), @satisfies L MD SM (@build_model MD kMD M m) (@iffp L minL pL (@sepcon L sL (@andp L pL x y) z) (@andp L pL x (@sepcon L sL y z))) *)
  split; intros.
  + destruct H2 as [? _].
(* 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) J m1 m2 n) (and (@Kdenotation L MD kMD M SM x m1) (@Kdenotation L MD kMD M SM y m2)))) *)
    destruct H3 as [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) J m1 m2 m) (and (@Kdenotation L MD kMD M SM x m1) (@Kdenotation L MD kMD M SM y m2)))) *)
    specialize (H2 _ _ H3).
(* Goal: @Kdenotation L MD kMD M SM y m2 *)
    destruct H2 as [n1 [n2 [? [? ?]]]].
(* 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) J m1 m2 n) (and (@Kdenotation L MD kMD M SM x m1) (@Kdenotation L MD kMD M SM y m2)))) *)
    exists n1, n2.
(* Goal: @Kdenotation L MD kMD M SM y m2 *)
    specialize (H _ _ H6).
(* Goal: @Kdenotation L MD kMD M SM y m2 *)
    specialize (H0 _ _ H7).
(* Goal: @Kdenotation L MD kMD M SM y m2 *)
    tauto.
  + destruct H2 as [_ ?].
(* 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) J m1 m2 m) (and (@Kdenotation L MD kMD M SM x m1) (@Kdenotation L MD kMD M SM y m2)))) *)
    destruct H3 as [n1 [n2 [? [? ?]]]].
(* 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) J m1 m2 m) (and (@Kdenotation L MD kMD M SM x m1) (@Kdenotation L MD kMD M SM y m2)))) *)
    specialize (H2 _ _ H3).
(* Goal: @Kdenotation L MD kMD M SM y n2 *)
    destruct H2 as [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) J m1 m2 n) (and (@satisfies L MD SM (@build_model MD kMD M m1) (@andp L pL x y)) (@satisfies L MD SM (@build_model MD kMD M m2) z)))) *)
    exists m1, m2.
(* Goal: @Kdenotation L MD kMD M SM y m2 *)
    specialize (H _ _ H6).
(* Goal: @Kdenotation L MD kMD M SM y m2 *)
    specialize (H0 _ _ H7).
(* Goal: @Kdenotation L MD kMD M SM y m2 *)
    tauto.
Qed.

Lemma sound_wand_stable {L: Language} {minL: MinimunLanguage L} {pL: PropositionalLanguage L} {sL: SeparationLanguage L} {MD: Model} {kMD: KripkeModel MD} {M: Kmodel} {R1: KI.Relation (Kworlds M)} {R2: SS.Relation (Kworlds M)} {J: Join (Kworlds M)} {SAbis: SeparationAlgebraBisStable (Kworlds M)} {SM: Semantics L MD} {fsSM: SeparatingSemantics L MD M SM} {stableSM: SemanticStable L MD M SM}:
  forall x y: expr,
    semantic_stable x -> semantic_stable y -> semantic_stable (x -* y).
Proof.
(* Goal: forall (x y z : @expr L) (_ : @semantic_stable L MD kMD M R2 SM stableSM x) (m : @Kworlds MD kMD M), @satisfies L MD SM (@build_model MD kMD M m) (@iffp L minL pL (@sepcon L sL (@andp L pL x y) z) (@andp L pL x (@sepcon L sL y z))) *)
  intros.
(* Goal: @semantic_stable L MD kMD M R2 SM stableSM (@wand L sL x y) *)
  rewrite denote_stable in H, H0 |- *.
(* Goal: @Semantics.stable (@Kworlds MD kMD M) R2 (@Kdenotation L MD kMD M SM (@wand L sL x y)) *)
  unfold Semantics.stable in *.
(* Goal: forall (x y z : @expr L) (_ : @semantic_stable L MD kMD M R2 SM stableSM x) (m : @Kworlds MD kMD M), @satisfies L MD SM (@build_model MD kMD M m) (@iffp L minL pL (@sepcon L sL (@andp L pL x y) z) (@andp L pL x (@sepcon L sL y z))) *)
  intros.
(* Goal: iff (@Kdenotation L MD kMD M SM (@wand L sL x y) m) (@Kdenotation L MD kMD M SM (@wand L sL x y) n) *)
  rewrite !(app_same_set (denote_wand _ _)).
(* Goal: iff (@WeakSemantics.wand (@Kworlds MD kMD M) J (@Kdenotation L MD kMD M SM x) (@Kdenotation L MD kMD M SM y) m) (@WeakSemantics.wand (@Kworlds MD kMD M) J (@Kdenotation L MD kMD M SM x) (@Kdenotation L MD kMD M SM y) n) *)
  unfold WeakSemantics.wand; simpl.
(* Goal: iff (forall (m1 m2 : @Kworlds MD kMD M) (_ : @join (@Kworlds MD kMD M) J m m1 m2) (_ : @Kdenotation L MD kMD M SM x m1), @Kdenotation L MD kMD M SM y m2) (forall (m1 m2 : @Kworlds MD kMD M) (_ : @join (@Kworlds MD kMD M) J n m1 m2) (_ : @Kdenotation L MD kMD M SM x m1), @Kdenotation L MD kMD M SM y m2) *)
  pose proof extend_bis_stable _ _ H1.
(* Goal: iff (forall (m1 m2 : @Kworlds MD kMD M) (_ : @join (@Kworlds MD kMD M) J m m1 m2) (_ : @Kdenotation L MD kMD M SM x m1), @Kdenotation L MD kMD M SM y m2) (forall (m1 m2 : @Kworlds MD kMD M) (_ : @join (@Kworlds MD kMD M) J n m1 m2) (_ : @Kdenotation L MD kMD M SM x m1), @Kdenotation L MD kMD M SM y m2) *)
  split.
  + intros ? n1 n2 ? ?.
(* Goal: @Kdenotation L MD kMD M SM y n2 *)
    destruct H2 as [_ ?].
(* Goal: @Kdenotation L MD kMD M SM y m2 *)
    specialize (H2 _ _ H4).
(* Goal: @Kdenotation L MD kMD M SM y n2 *)
    destruct H2 as [m1 [m2 [? [? ?]]]].
(* Goal: @Kdenotation L MD kMD M SM y m2 *)
    specialize (H3 _ _ H2).
(* Goal: @Kdenotation L MD kMD M SM y m2 *)
    specialize (H0 _ _ H7).
(* Goal: @Kdenotation L MD kMD M SM y m2 *)
    specialize (H _ _ H6).
(* Goal: @Kdenotation L MD kMD M SM y m2 *)
    tauto.
  + intros ? m1 m2 ? ?.
(* Goal: @Kdenotation L MD kMD M SM y m2 *)
    destruct H2 as [? _].
(* Goal: @Kdenotation L MD kMD M SM y m2 *)
    specialize (H2 _ _ H4).
(* Goal: @Kdenotation L MD kMD M SM y m2 *)
    destruct H2 as [n1 [n2 [? [? ?]]]].
(* Goal: @Kdenotation L MD kMD M SM y m2 *)
    specialize (H3 _ _ H2).
(* Goal: @Kdenotation L MD kMD M SM y m2 *)
    specialize (H0 _ _ H7).
(* Goal: @Kdenotation L MD kMD M SM y m2 *)
    specialize (H _ _ H6).
(* Goal: @Kdenotation L MD kMD M SM y m2 *)
    tauto.
Qed.

Lemma sound_stable_andp_sepcon1 {L: Language} {minL: MinimunLanguage L} {pL: PropositionalLanguage L} {sL: SeparationLanguage L} {MD: Model} {kMD: KripkeModel MD} {M: Kmodel} {R1: KI.Relation (Kworlds M)} {R2: SS.Relation (Kworlds M)} {J: Join (Kworlds M)} {SAabs: SeparationAlgebraAbsorbStable (Kworlds M)} {SM: Semantics L MD} {kiSM: KripkeIntuitionisticSemantics L MD M SM} {kminSM: KripkeMinimunSemantics L MD M SM} {kpSM: KripkePropositionalSemantics L MD M SM} {fsSM: SeparatingSemantics L MD M SM} {stableSM: SemanticStable L MD M SM}:
  forall x y z, semantic_stable x ->
    forall m: Kworlds M, KRIPKE: M, m |= (x && y) * z <--> x && (y * z).
Proof.
(* Goal: forall (x y z : @expr L) (_ : @semantic_stable L MD kMD M R2 SM stableSM x) (m : @Kworlds MD kMD M), @satisfies L MD SM (@build_model MD kMD M m) (@iffp L minL pL (@sepcon L sL (@andp L pL x y) z) (@andp L pL x (@sepcon L sL y z))) *)
  intros.
(* Goal: @satisfies L MD SM (@build_model MD kMD M m) (@iffp L minL pL (@sepcon L sL (@andp L pL x y) z) (@andp L pL x (@sepcon L sL y z))) *)
  unfold iffp.
(* Goal: @satisfies L MD SM (@build_model MD kMD M m) (@andp L pL (@impp L minL (@sepcon L sL (@andp L pL x y) z) (@andp L pL x (@sepcon L sL y z))) (@impp L minL (@andp L pL x (@sepcon L sL y z)) (@sepcon L sL (@andp L pL x y) z))) *)
  rewrite sat_andp, !sat_impp.
(* Goal: forall (x y z : @expr L) (_ : @semantic_stable L MD kMD M R2 SM stableSM x) (m : @Kworlds MD kMD M), @satisfies L MD SM (@build_model MD kMD M m) (@iffp L minL pL (@sepcon L sL (@andp L pL x y) z) (@andp L pL x (@sepcon L sL y z))) *)
  split; intros.
  + clear m H0.
(* Goal: @satisfies L MD SM (@build_model MD kMD M n) (@andp L pL x (@sepcon L sL y z)) *)
    rewrite sat_andp, sat_sepcon.
(* Goal: and (@satisfies L MD SM (@build_model MD kMD M n) x) (@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) J m1 m2 n) (and (@satisfies L MD SM (@build_model MD kMD M m1) y) (@satisfies L MD SM (@build_model MD kMD M m2) z))))) *)
    rewrite sat_sepcon in H1.
(* Goal: and (@satisfies L MD SM (@build_model MD kMD M n) x) (@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) J m1 m2 n) (and (@satisfies L MD SM (@build_model MD kMD M m1) y) (@satisfies L MD SM (@build_model MD kMD M m2) z))))) *)
    destruct H1 as [n1 [n2 [? [? ?]]]].
(* Goal: and (@satisfies L MD SM (@build_model MD kMD M n) x) (@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) J m1 m2 n) (and (@satisfies L MD SM (@build_model MD kMD M m1) y) (@satisfies L MD SM (@build_model MD kMD M m2) z))))) *)
    rewrite sat_andp in H1.
(* Goal: and (@satisfies L MD SM (@build_model MD kMD M n) x) (@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) J m1 m2 n) (and (@satisfies L MD SM (@build_model MD kMD M m1) y) (@satisfies L MD SM (@build_model MD kMD M m2) z))))) *)
    destruct H1.
(* Goal: and (@satisfies L MD SM (@build_model MD kMD M n) x) (@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) J m1 m2 n) (and (@satisfies L MD SM (@build_model MD kMD M m1) y) (@satisfies L MD SM (@build_model MD kMD M m2) z))))) *)
    destruct (SA_absorb_stable _ _ _ H0) as [m1 [m2 [? [? [? [? ?]]]]]].
(* Goal: and (@satisfies L MD SM (@build_model MD kMD M n) x) (@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) J m1 m2 n) (and (@satisfies L MD SM (@build_model MD kMD M m1) y) (@satisfies L MD SM (@build_model MD kMD M m2) z))))) *)
    apply (sat_mono _ _ _ H7) in H1.
(* Goal: and (@satisfies L MD SM (@build_model MD kMD M n) x) (@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) J m1 m2 n) (and (@satisfies L MD SM (@build_model MD kMD M m1) y) (@satisfies L MD SM (@build_model MD kMD M m2) z))))) *)
    apply (sat_mono _ _ _ H7) in H3.
(* Goal: and (@satisfies L MD SM (@build_model MD kMD M n) x) (@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) J m1 m2 n) (and (@satisfies L MD SM (@build_model MD kMD M m1) y) (@satisfies L MD SM (@build_model MD kMD M m2) z))))) *)
    apply (sat_mono _ _ _ H8) in H2.
(* 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) J m1 m2 n) (and (@satisfies L MD SM (@build_model MD kMD M m1) (@andp L pL x y)) (@satisfies L MD SM (@build_model MD kMD M m2) z)))) *)
    rewrite denote_stable in H.
(* Goal: and (@satisfies L MD SM (@build_model MD kMD M n) x) (@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) J m1 m2 n) (and (@satisfies L MD SM (@build_model MD kMD M m1) y) (@satisfies L MD SM (@build_model MD kMD M m2) z))))) *)
    rewrite (H _ _ H5) in H1.
(* Goal: and (@satisfies L MD SM (@build_model MD kMD M m1) x) (@satisfies L MD SM (@build_model MD kMD M m1) y) *)
    split; auto.
(* Goal: and (@satisfies L MD SM (@build_model MD kMD M m1) x) (@satisfies L MD SM (@build_model MD kMD M m1) y) *)
    exists m1, m2; auto.
  + clear m H0.
(* Goal: @satisfies L MD SM (@build_model MD kMD M n) (@sepcon L sL (@andp L pL x y) z) *)
    rewrite sat_sepcon.
(* 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) J m1 m2 n) (and (@satisfies L MD SM (@build_model MD kMD M m1) (@andp L pL x y)) (@satisfies L MD SM (@build_model MD kMD M m2) z)))) *)
    rewrite sat_andp, sat_sepcon in H1.
(* 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) J m1 m2 n) (and (@satisfies L MD SM (@build_model MD kMD M m1) (@andp L pL x y)) (@satisfies L MD SM (@build_model MD kMD M m2) z)))) *)
    destruct H1 as [? [n1 [n2 [? [? ?]]]]].
(* 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) J m1 m2 n) (and (@satisfies L MD SM (@build_model MD kMD M m1) (@andp L pL x y)) (@satisfies L MD SM (@build_model MD kMD M m2) z)))) *)
    destruct (SA_absorb_stable _ _ _ H1) as [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) J m1 m2 n) (and (@satisfies L MD SM (@build_model MD kMD M m1) (@andp L pL x y)) (@satisfies L MD SM (@build_model MD kMD M m2) z)))) *)
    apply (sat_mono _ _ _ H7) in H2.
(* 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) J m1 m2 n) (and (@satisfies L MD SM (@build_model MD kMD M m1) (@andp L pL x y)) (@satisfies L MD SM (@build_model MD kMD M m2) z)))) *)
    apply (sat_mono _ _ _ H8) in H3.
(* 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) J m1 m2 n) (and (@satisfies L MD SM (@build_model MD kMD M m1) (@andp L pL x y)) (@satisfies L MD SM (@build_model MD kMD M m2) z)))) *)
    rewrite denote_stable in H.
    rewrite <- (H _ _ H5) in H0.
(* 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) J m1 m2 n) (and (@satisfies L MD SM (@build_model MD kMD M m1) (@andp L pL x y)) (@satisfies L MD SM (@build_model MD kMD M m2) z)))) *)
    exists m1, m2.
(* Goal: and (@satisfies L MD SM (@build_model MD kMD M m1) x) (@satisfies L MD SM (@build_model MD kMD M m1) y) *)
    split; [| split]; auto.
(* Goal: @satisfies L MD SM (@build_model MD kMD M m1) (@andp L pL x y) *)
    rewrite sat_andp.
(* Goal: and (@satisfies L MD SM (@build_model MD kMD M m1) x) (@satisfies L MD SM (@build_model MD kMD M m1) y) *)
    auto.
Qed.

End Sound_KripkeIntuitionistic.
