Require Import Coq.Logic.FunctionalExtensionality.
Require Import Coq.Logic.Classical_Prop.
Require Import Coq.Logic.Classical_Pred_Type.
Require Import Logic.lib.Ensembles_ext.
Require Import Logic.lib.Bijection.
Require Import Logic.lib.Countable.
Require Import Logic.GeneralLogic.Base.
Require Import Logic.GeneralLogic.KripkeModel.
Require Import Logic.GeneralLogic.ProofTheory.BasicSequentCalculus.
Require Import Logic.GeneralLogic.Semantics.Kripke.
Require Import Logic.GeneralLogic.Complete.ContextProperty.
Require Import Logic.GeneralLogic.Complete.ContextProperty_Kripke.
Require Import Logic.GeneralLogic.Complete.Lindenbaum.
Require Import Logic.MinimunLogic.Syntax.
Require Import Logic.MinimunLogic.ProofTheory.Minimun.
Require Import Logic.MinimunLogic.Semantics.Kripke.
Require Import Logic.MinimunLogic.Complete.ContextProperty_Kripke.
Require Import Logic.PropositionalLogic.Syntax.
Require Import Logic.PropositionalLogic.ProofTheory.Intuitionistic.
Require Import Logic.PropositionalLogic.ProofTheory.DeMorgan.
Require Import Logic.PropositionalLogic.ProofTheory.GodelDummett.
Require Import Logic.PropositionalLogic.ProofTheory.Classical.
Require Import Logic.PropositionalLogic.Semantics.Kripke.
Require Import Logic.PropositionalLogic.Complete.ContextProperty_Kripke.
Require Import Logic.PropositionalLogic.Complete.Canonical_Kripke.
Require Import Logic.SeparationLogic.Syntax.
Require Import Logic.SeparationLogic.ProofTheory.SeparationLogic.
Require Import Logic.SeparationLogic.ProofTheory.RewriteClass.
Require Import Logic.SeparationLogic.ProofTheory.DerivedRules.
Require Import Logic.SeparationLogic.Model.SeparationAlgebra.
Require Import Logic.SeparationLogic.Model.OrderedSA.
Require Import Logic.SeparationLogic.Semantics.FlatSemantics.
Require Import Logic.SeparationLogic.Complete.ContextProperty_Flat.

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

Section Canonical.

Context {L: Language}
        {minL: MinimunLanguage L}
        {pL: PropositionalLanguage L}
        {sL: SeparationLanguage L}
        {Gamma: ProofTheory L}
        {SC: NormalSequentCalculus L Gamma}
        {bSC: BasicSequentCalculus L Gamma}
        {minSC: MinimunSequentCalculus L Gamma}
        {ipSC: IntuitionisticPropositionalSequentCalculus L Gamma}
        {AX: NormalAxiomatization L Gamma}
        {minAX: MinimunAxiomatization L Gamma}
        {ipGamma: IntuitionisticPropositionalLogic L Gamma}
        {sGamma: SeparationLogic L Gamma}
        {MD: Model}
        {kMD: KripkeModel MD}
        {M: Kmodel}
        {R: Relation (Kworlds M)}
        {J: Join (Kworlds M)}
        {SM: Semantics L MD}
        {fsSM: SeparatingSemantics L MD M SM}.

Context (cP: context -> Prop)
        (rel: bijection (Kworlds M) (sig cP)).

Hypothesis H_R: forall m n Phi Psi, rel m Phi -> rel n Psi -> (m <= n <-> Included _ (proj1_sig Phi) (proj1_sig Psi)).

Hypothesis H_J: forall m1 m2 m Phi1 Phi2 Phi, rel m1 Phi1 -> rel m2 Phi2 -> rel m Phi -> (join m1 m2 m <-> Included _ (context_sepcon (proj1_sig Phi1) (proj1_sig Phi2)) (proj1_sig Phi)).

Instance SA
         (AL_DC: at_least derivable_closed cP)
         (LIN_SR: forall (Phi: context) (Psi: sig cP), Lindenbaum_constructable (context_sepcon_included_r Phi (proj1_sig Psi)) cP):
  SeparationAlgebra (Kworlds M).
Proof.
(* Goal: @UnitalSeparationAlgebra (@Kworlds MD kMD M) R J *)
  constructor.
  + intros.
(* Goal: @Krelation (@Kworlds MD kMD M) R m1 m *)
    destruct (im_bij _ _ rel m1) as [Phi1 ?].
(* Goal: @Krelation (@Kworlds MD kMD M) R m1 m *)
    destruct (im_bij _ _ rel m2) as [Phi2 ?].
(* Goal: @join (@Kworlds MD kMD M) J m m m *)
    destruct (im_bij _ _ rel m) as [Phi ?].
(* Goal: and (@join (@Kworlds MD kMD M) J n1 n2 m) (@Krelation (@Kworlds MD kMD M) R m m) *)
    erewrite H_J in H |- * by eauto.
(* Goal: forall n : @Kworlds MD kMD M, @ex (@Kworlds MD kMD M) (fun m : @Kworlds MD kMD M => and (@residue (@Kworlds MD kMD M) R J n m) (@increasing (@Kworlds MD kMD M) R J m)) *)
    hnf; intros.
(* Goal: Ensembles.In (@expr L) (@proj1_sig (@context L) cP Phi) x *)
    destruct H3 as [y [z [? [? ?]]]].
(* Goal: Ensembles.In (@expr L) (@proj1_sig (@context L) cP Phi) x *)
    subst.
(* Goal: @proj1_sig (@context L) cP Phi x *)
    rewrite derivable_closed_element_derivable by (apply AL_DC, (proj2_sig Phi)).
(* Goal: @derivable L Gamma (Ensembles.In (@expr L) (@proj1_sig (@context L) cP Phi)) (@sepcon L sL y z) *)
    rewrite sepcon_comm.
(* Goal: @derivable L Gamma (@proj1_sig (@context L) cP Phi) (@emp L sL s'L) *)
    rewrite <- derivable_closed_element_derivable by (apply AL_DC, (proj2_sig Phi)).
(* Goal: @proj1_sig (@context L) cP Phi_xy (@sepcon L sL x y) *)
    apply H.
(* Goal: Ensembles.In (@expr L) (@context_sepcon L sL Gamma (@proj1_sig (@context L) cP Phi1) (@proj1_sig (@context L) cP Phi2)) (@sepcon L sL z y) *)
    exists z, y; split; [| split]; auto.
  + intros.
(* Goal: @ex (@Kworlds MD kMD M) (fun myz : @Kworlds MD kMD M => and (@join (@Kworlds MD kMD M) J my mz myz) (@join (@Kworlds MD kMD M) J mx myz mxyz)) *)
    destruct (im_bij _ _ rel mx) as [Phi_x ?].
(* Goal: @ex (@Kworlds MD kMD M) (fun myz : @Kworlds MD kMD M => and (@join (@Kworlds MD kMD M) J my mz myz) (@join (@Kworlds MD kMD M) J mx myz mxyz)) *)
    destruct (im_bij _ _ rel my) as [Phi_y ?].
(* Goal: @ex (@Kworlds MD kMD M) (fun myz : @Kworlds MD kMD M => and (@join (@Kworlds MD kMD M) J my mz myz) (@join (@Kworlds MD kMD M) J mx myz mxyz)) *)
    destruct (im_bij _ _ rel mz) as [Phi_z ?].
(* Goal: @ex (@Kworlds MD kMD M) (fun myz : @Kworlds MD kMD M => and (@join (@Kworlds MD kMD M) J my mz myz) (@join (@Kworlds MD kMD M) J mx myz mxyz)) *)
    destruct (im_bij _ _ rel mxy) as [Phi_xy ?].
(* Goal: @ex (@Kworlds MD kMD M) (fun myz : @Kworlds MD kMD M => and (@join (@Kworlds MD kMD M) J my mz myz) (@join (@Kworlds MD kMD M) J mx myz mxyz)) *)
    destruct (im_bij _ _ rel mxyz) as [Phi_xyz ?].
(* Goal: @ex (@Kworlds MD kMD M) (fun myz : @Kworlds MD kMD M => and (@join (@Kworlds MD kMD M) J my mz myz) (@join (@Kworlds MD kMD M) J mx myz mxyz)) *)
    erewrite H_J in H, H0 by eauto.
    assert (Included _ (context_sepcon (proj1_sig Phi_x)
             (context_sepcon (proj1_sig Phi_y) (proj1_sig Phi_z))) (proj1_sig Phi_xyz)).
    - hnf; intros xyz ?.
(* Goal: Ensembles.In (@expr L) (@proj1_sig (@context L) cP Phi_xyz) xyz *)
      destruct H6 as [x [yz [? [? ?]]]]; subst xyz.
(* Goal: Ensembles.In (@expr L) (@proj1_sig (@context L) cP Phi_xyz) (@sepcon L sL x yz) *)
      apply context_sepcon_derivable in H8.
(* Goal: Ensembles.In (@expr L) (@proj1_sig (@context L) cP Phi_xyz) (@sepcon L sL x yz) *)
      destruct H8 as [y [z [? [? ?]]]].
(* Goal: Ensembles.In (@expr L) (@proj1_sig (@context L) cP Phi_xyz) (@sepcon L sL x yz) *)
      rewrite derivable_closed_element_derivable by (apply AL_DC, (proj2_sig Phi_xyz)).
      rewrite <- H6, sepcon_assoc.
      rewrite <- derivable_closed_element_derivable by (apply AL_DC, (proj2_sig Phi_xyz)).
(* Goal: Ensembles.In (@expr L) (@proj1_sig (@context L) cP Phi_xyz) (@sepcon L sL (@sepcon L sL x y) z) *)
      apply H0.
(* Goal: Ensembles.In (@expr L) (@context_sepcon L sL Gamma (@proj1_sig (@context L) cP Phi_xy) (@proj1_sig (@context L) cP Phi_z)) (@sepcon L sL (@sepcon L sL x y) z) *)
      exists (x * y), z; split; [| split]; auto.
      rewrite <- derivable_closed_element_derivable by (apply AL_DC, (proj2_sig Phi_xy)).
(* Goal: @proj1_sig (@context L) cP Phi_xy (@sepcon L sL x y) *)
      apply H.
(* Goal: Ensembles.In (@expr L) (@context_sepcon L sL Gamma (@proj1_sig (@context L) cP Phi_x) (@proj1_sig (@context L) cP Phi_y)) (@sepcon L sL x y) *)
      exists x, y; split; [| split]; auto.
    - apply LIN_SR in H6.
(* Goal: @ex (@Kworlds MD kMD M) (fun myz : @Kworlds MD kMD M => and (@join (@Kworlds MD kMD M) J my mz myz) (@join (@Kworlds MD kMD M) J mx myz mxyz)) *)
      destruct H6 as [Phi_yz [? ?]].
(* Goal: @ex (@Kworlds MD kMD M) (fun myz : @Kworlds MD kMD M => and (@join (@Kworlds MD kMD M) J my mz myz) (@join (@Kworlds MD kMD M) J mx myz mxyz)) *)
      unfold context_sepcon_included_r in H7.
(* Goal: @ex (@Kworlds MD kMD M) (fun myz : @Kworlds MD kMD M => and (@join (@Kworlds MD kMD M) J my mz myz) (@join (@Kworlds MD kMD M) J mx myz mxyz)) *)
      destruct (su_bij _ _ rel Phi_yz) as [myz ?].
(* Goal: @ex (@Kworlds MD kMD M) (fun myz : @Kworlds MD kMD M => and (@join (@Kworlds MD kMD M) J my mz myz) (@join (@Kworlds MD kMD M) J mx myz mxyz)) *)
      exists myz.
(* Goal: and (@join (@Kworlds MD kMD M) J my mz myz) (@join (@Kworlds MD kMD M) J mx myz mxyz) *)
      erewrite !H_J by eauto.
(* Goal: Included (@expr L) (@context_sepcon L sL Gamma (@proj1_sig (@context L) cP Phi) (@proj1_sig (@context L) cP Psi)) (@proj1_sig (@context L) cP Phi) *)
      auto.
Qed.

Instance uSA
         (AL_DC: at_least derivable_closed cP):
  UpwardsClosedSeparationAlgebra (Kworlds M).
Proof.
(* Goal: forall n : @Kworlds MD kMD M, @ex (@Kworlds MD kMD M) (fun m : @Kworlds MD kMD M => and (@residue (@Kworlds MD kMD M) R J n m) (@increasing (@Kworlds MD kMD M) R J m)) *)
  hnf; intros.
(* Goal: @ex (@Kworlds MD kMD M) (fun n1 : @Kworlds MD kMD M => @ex (@Kworlds MD kMD M) (fun n2 : @Kworlds MD kMD M => and (@join (@Kworlds MD kMD M) J n1 n2 n) (and (@Krelation (@Kworlds MD kMD M) R m1 n1) (@Krelation (@Kworlds MD kMD M) R m2 n2)))) *)
  exists m1, m2.
(* Goal: and (@join (@Kworlds MD kMD M) J m1 m2 n) (and (@Krelation (@Kworlds MD kMD M) R m1 m1) (@Krelation (@Kworlds MD kMD M) R m2 m2)) *)
  destruct (im_bij _ _ rel n) as [Psi ?].
(* Goal: @Krelation (@Kworlds MD kMD M) R m1 m *)
  destruct (im_bij _ _ rel m1) as [Phi1 ?].
(* Goal: @Krelation (@Kworlds MD kMD M) R m1 m *)
  destruct (im_bij _ _ rel m2) as [Phi2 ?].
(* Goal: @join (@Kworlds MD kMD M) J m m m *)
  destruct (im_bij _ _ rel m) as [Phi ?].
(* Goal: and (@join (@Kworlds MD kMD M) J n1 n2 m) (@Krelation (@Kworlds MD kMD M) R m m) *)
  erewrite H_J in H |- * by eauto.
(* Goal: Included (@expr L) (@context_sepcon L sL Gamma (@proj1_sig (@context L) cP Phi) (@proj1_sig (@context L) cP Psi)) (@proj1_sig (@context L) cP Phi) *)
  erewrite H_R in H0 by eauto.
(* Goal: Included (@expr L) (@context_sepcon L sL Gamma (@proj1_sig (@context L) cP Phi) (@proj1_sig (@context L) cP Psi)) (@proj1_sig (@context L) cP Phi) *)
  do 2 erewrite H_R by eauto.
(* Goal: and (Included (@expr L) (@context_sepcon L sL Gamma (@proj1_sig (@context L) cP Phi1) (@proj1_sig (@context L) cP Phi2)) (@proj1_sig (@context L) cP Psi)) (and (Included (@expr L) (@proj1_sig (@context L) cP Phi1) (@proj1_sig (@context L) cP Phi1)) (Included (@expr L) (@proj1_sig (@context L) cP Phi2) (@proj1_sig (@context L) cP Phi2))) *)
  split; [| split].
  + eapply Included_trans; eauto.
  + hnf; intros; auto.
  + hnf; intros; auto.
Qed.

Instance dSA
         (AL_DC: at_least derivable_closed cP):
  DownwardsClosedSeparationAlgebra (Kworlds M).
Proof.
(* Goal: forall n : @Kworlds MD kMD M, @ex (@Kworlds MD kMD M) (fun m : @Kworlds MD kMD M => and (@residue (@Kworlds MD kMD M) R J n m) (@increasing (@Kworlds MD kMD M) R J m)) *)
  hnf; intros.
(* Goal: @ex (@Kworlds MD kMD M) (fun m : @Kworlds MD kMD M => and (@residue (@Kworlds MD kMD M) R J n m) (@increasing (@Kworlds MD kMD M) R J m)) *)
  exists m.
(* Goal: @Krelation (@Kworlds MD kMD M) R n1 n2 *)
  destruct (im_bij _ _ rel n1) as [Psi1 ?].
(* Goal: @Krelation (@Kworlds MD kMD M) R n1 n2 *)
  destruct (im_bij _ _ rel n2) as [Psi2 ?].
(* Goal: @Krelation (@Kworlds MD kMD M) R m1 m *)
  destruct (im_bij _ _ rel m1) as [Phi1 ?].
(* Goal: @Krelation (@Kworlds MD kMD M) R m1 m *)
  destruct (im_bij _ _ rel m2) as [Phi2 ?].
(* Goal: @join (@Kworlds MD kMD M) J m m m *)
  destruct (im_bij _ _ rel m) as [Phi ?].
(* Goal: and (@join (@Kworlds MD kMD M) J n1 n2 m) (@Krelation (@Kworlds MD kMD M) R m m) *)
  erewrite H_J in H |- * by eauto.
  erewrite H_R in H0, H1 |- * by eauto.
(* Goal: and (Included (@expr L) (@context_sepcon L sL Gamma (@proj1_sig (@context L) cP Psi1) (@proj1_sig (@context L) cP Psi2)) (@proj1_sig (@context L) cP Phi)) (Included (@expr L) (@proj1_sig (@context L) cP Phi) (@proj1_sig (@context L) cP Phi)) *)
  split.
  + eapply Included_trans; eauto.
(* Goal: Ensembles.In (@expr L) (@proj1_sig (@context L) cP Phi) x *)
    hnf; intros z [x [y [? [? ?]]]]; subst.
(* Goal: Ensembles.In (@expr L) (@context_sepcon L sL Gamma (@proj1_sig (@context L) cP Phi1) (@proj1_sig (@context L) cP Phi2)) (@sepcon L sL x y) *)
    exists x, y.
(* Goal: Included (@expr L) (@context_sepcon L sL Gamma (@proj1_sig (@context L) cP Phi) (@proj1_sig (@context L) cP Psi)) (@proj1_sig (@context L) cP Phi) *)
    split; [| split]; auto.
    - eapply deduction_weaken; eauto.
    - eapply deduction_weaken; eauto.
  + hnf; intros; auto.
Qed.

Lemma garbage_collected_canonical_increaing
      {gcsGamma: GarbageCollectSeparationLogic L Gamma}
      (AL_DC: at_least derivable_closed cP):
  IncreasingSeparationAlgebra (Kworlds M).
Proof.
(* Goal: @UnitalSeparationAlgebra (@Kworlds MD kMD M) R J *)
  constructor.
(* Goal: forall x : @Kworlds MD kMD M, @increasing (@Kworlds MD kMD M) R J x *)
  intros m; hnf; intros n1 n2 ?.
(* Goal: @Krelation (@Kworlds MD kMD M) R n1 n2 *)
  destruct (im_bij _ _ rel n1) as [Psi1 ?].
(* Goal: @Krelation (@Kworlds MD kMD M) R n1 n2 *)
  destruct (im_bij _ _ rel n2) as [Psi2 ?].
(* Goal: @join (@Kworlds MD kMD M) J m m m *)
  destruct (im_bij _ _ rel m) as [Phi ?].
(* Goal: Included (@expr L) (@context_sepcon L sL Gamma (@proj1_sig (@context L) cP Phi) (@proj1_sig (@context L) cP Psi)) (@proj1_sig (@context L) cP Phi) *)
  erewrite H_R by eauto.
(* Goal: Included (@expr L) (@context_sepcon L sL Gamma (@proj1_sig (@context L) cP Phi) (@proj1_sig (@context L) cP Psi)) (@proj1_sig (@context L) cP Phi) *)
  erewrite H_J in H by eauto.
(* Goal: forall n : @Kworlds MD kMD M, @ex (@Kworlds MD kMD M) (fun m : @Kworlds MD kMD M => and (@residue (@Kworlds MD kMD M) R J n m) (@increasing (@Kworlds MD kMD M) R J m)) *)
  unfold Included, Ensembles.In; intros.
(* Goal: @proj1_sig (@context L) cP Psi2 x *)
  rewrite derivable_closed_element_derivable in H3 by (apply AL_DC, (proj2_sig Psi1)).
(* Goal: @proj1_sig (@context L) cP Psi2 x *)
  rewrite derivable_closed_element_derivable by (apply AL_DC, (proj2_sig Psi2)).
  rewrite <- (sepcon_elim2 TT).
  rewrite <- derivable_closed_element_derivable by (apply AL_DC, (proj2_sig Psi2)).
(* Goal: Included (@expr L) (@context_sepcon L sL Gamma (@proj1_sig (@context L) cP Phi) (@proj1_sig (@context L) cP Psi)) (@proj1_sig (@context L) cP Phi) *)
  apply H; auto.
(* Goal: Included (@expr L) (@context_sepcon L sL Gamma (@proj1_sig (@context L) cP Phi) (@proj1_sig (@context L) cP Psi)) (@proj1_sig (@context L) cP Phi) *)
  exists TT, x; split; [| split]; auto.
(* Goal: @derivable L Gamma (@proj1_sig (@context L) cP Phi2) (@truep L minL pL) *)
  apply derivable_impp_refl.
Qed.

Lemma ext_canonical_residual
      {ExtSGamma: ExtSeparationLogic L Gamma}
      (AL_DC: at_least derivable_closed cP)
      (LIN_SL: forall (Phi: context) (Psi: sig cP), Lindenbaum_constructable (context_sepcon_included_l Phi (proj1_sig Psi)) cP):
  ResidualSeparationAlgebra (Kworlds M).
Proof.
(* Goal: @UnitalSeparationAlgebra (@Kworlds MD kMD M) R J *)
  constructor.
(* Goal: forall n : @Kworlds MD kMD M, @ex (@Kworlds MD kMD M) (fun m : @Kworlds MD kMD M => and (@residue (@Kworlds MD kMD M) R J n m) (@increasing (@Kworlds MD kMD M) R J m)) *)
  intros.
(* Goal: @ex (@Kworlds MD kMD M) (fun m : @Kworlds MD kMD M => and (@residue (@Kworlds MD kMD M) R J n m) (@increasing (@Kworlds MD kMD M) R J m)) *)
  destruct (im_bij _ _ rel n) as [Phi ?].
(* Goal: @ex (@Kworlds MD kMD M) (fun m : @Kworlds MD kMD M => @residue (@Kworlds MD kMD M) R J n m) *)
  assert (Included _ (context_sepcon (Union _ empty_context (Singleton _ TT)) (proj1_sig Phi)) (proj1_sig Phi)).
  + hnf; intros.
(* Goal: Ensembles.In (@expr L) (@proj1_sig (@context L) cP Phi) x *)
    destruct H0 as [y [z [? [? ?]]]].
    rewrite deduction_theorem, <- provable_derivable in H1.
(* Goal: @proj1_sig (@context L) cP Phi x *)
    rewrite derivable_closed_element_derivable by (apply AL_DC, (proj2_sig Phi)).
    subst; rewrite <- H1.
    rewrite <- sepcon_comm, <- sepcon_ext; auto.
  + apply LIN_SL in H0.
(* Goal: @ex (@Kworlds MD kMD M) (fun m : @Kworlds MD kMD M => and (@residue (@Kworlds MD kMD M) R J n m) (@increasing (@Kworlds MD kMD M) R J m)) *)
    destruct H0 as [Psi [? ?]].
(* Goal: @ex (@Kworlds MD kMD M) (fun m : @Kworlds MD kMD M => and (@residue (@Kworlds MD kMD M) R J n m) (@increasing (@Kworlds MD kMD M) R J m)) *)
    destruct (su_bij _ _ rel Psi) as [m ?].
(* Goal: @ex (@Kworlds MD kMD M) (fun m : @Kworlds MD kMD M => and (@residue (@Kworlds MD kMD M) R J n m) (@increasing (@Kworlds MD kMD M) R J m)) *)
    exists m.
(* Goal: and (Included (@expr L) (@context_sepcon L sL Gamma (@proj1_sig (@context L) cP Psi1) (@proj1_sig (@context L) cP Psi2)) (@proj1_sig (@context L) cP Phi)) (Included (@expr L) (@proj1_sig (@context L) cP Phi) (@proj1_sig (@context L) cP Phi)) *)
    exists n; split.
    - erewrite H_J by eauto.
(* Goal: Included (@expr L) (@context_sepcon L sL Gamma (@proj1_sig (@context L) cP Phi) (@proj1_sig (@context L) cP Psi)) (@proj1_sig (@context L) cP Phi) *)
      auto.
    - erewrite H_R by eauto.
(* Goal: Included (@expr L) (@context_sepcon L sL Gamma (@proj1_sig (@context L) cP Phi) (@proj1_sig (@context L) cP Psi)) (@proj1_sig (@context L) cP Phi) *)
      hnf; intros; auto.
Qed.

Context {s'L: SeparationEmpLanguage L}
        {EmpsGamma: EmpSeparationLogic L Gamma}
        {feSM: EmpSemantics L MD M SM}.

Instance unitSA
         (AL_DC: at_least derivable_closed cP)
         (LIN_SR: forall (Phi: context) (Psi: sig cP), Lindenbaum_constructable (context_sepcon_included_r Phi (proj1_sig Psi)) cP)
         (TRUTH: forall x, forall m Phi, rel m Phi -> (KRIPKE: M, m |= x <-> proj1_sig Phi x)):
  UnitalSeparationAlgebra (Kworlds M).
Proof.
(* Goal: forall n : @Kworlds MD kMD M, @ex (@Kworlds MD kMD M) (fun m : @Kworlds MD kMD M => and (@residue (@Kworlds MD kMD M) R J n m) (@increasing (@Kworlds MD kMD M) R J m)) *)
  intros.
(* Goal: @UnitalSeparationAlgebra (@Kworlds MD kMD M) R J *)
  constructor.
(* Goal: forall n : @Kworlds MD kMD M, @ex (@Kworlds MD kMD M) (fun m : @Kworlds MD kMD M => and (@residue (@Kworlds MD kMD M) R J n m) (@increasing (@Kworlds MD kMD M) R J m)) *)
  intros.
(* Goal: @ex (@Kworlds MD kMD M) (fun m : @Kworlds MD kMD M => and (@residue (@Kworlds MD kMD M) R J n m) (@increasing (@Kworlds MD kMD M) R J m)) *)
  destruct (im_bij _ _ rel n) as [Phi ?].
(* Goal: @ex (@Kworlds MD kMD M) (fun m : @Kworlds MD kMD M => and (@residue (@Kworlds MD kMD M) R J n m) (@increasing (@Kworlds MD kMD M) R J m)) *)
  assert (Included _ (context_sepcon (proj1_sig Phi) (Union _ empty_context (Singleton _ emp))) (proj1_sig Phi)).
  + hnf; intros.
(* Goal: Ensembles.In (@expr L) (@proj1_sig (@context L) cP Phi) x *)
    destruct H0 as [y [z [? [? ?]]]].
    rewrite deduction_theorem, <- provable_derivable in H2.
(* Goal: @proj1_sig (@context L) cP Phi x *)
    rewrite derivable_closed_element_derivable by (apply AL_DC, (proj2_sig Phi)).
    subst; rewrite <- H2, sepcon_emp; auto.
  + apply LIN_SR in H0.
(* Goal: @ex (@Kworlds MD kMD M) (fun m : @Kworlds MD kMD M => and (@residue (@Kworlds MD kMD M) R J n m) (@increasing (@Kworlds MD kMD M) R J m)) *)
    destruct H0 as [Psi [? ?]].
(* Goal: @ex (@Kworlds MD kMD M) (fun m : @Kworlds MD kMD M => and (@residue (@Kworlds MD kMD M) R J n m) (@increasing (@Kworlds MD kMD M) R J m)) *)
    destruct (su_bij _ _ rel Psi) as [m ?].
(* Goal: @ex (@Kworlds MD kMD M) (fun m : @Kworlds MD kMD M => and (@residue (@Kworlds MD kMD M) R J n m) (@increasing (@Kworlds MD kMD M) R J m)) *)
    exists m.
(* Goal: and (@residue (@Kworlds MD kMD M) R J n m) (@increasing (@Kworlds MD kMD M) R J m) *)
    split; [exists n; split |].
    - apply (@join_comm _ _ (SA AL_DC LIN_SR)).
(* Goal: Included (@expr L) (@context_sepcon L sL Gamma (@proj1_sig (@context L) cP Phi) (@proj1_sig (@context L) cP Psi)) (@proj1_sig (@context L) cP Phi) *)
      erewrite H_J by eauto.
(* Goal: Included (@expr L) (@context_sepcon L sL Gamma (@proj1_sig (@context L) cP Phi) (@proj1_sig (@context L) cP Psi)) (@proj1_sig (@context L) cP Phi) *)
      auto.
    - erewrite H_R by eauto.
(* Goal: Included (@expr L) (@context_sepcon L sL Gamma (@proj1_sig (@context L) cP Phi) (@proj1_sig (@context L) cP Psi)) (@proj1_sig (@context L) cP Phi) *)
      hnf; intros; auto.
    - clear H1 n Phi H.
(* Goal: @increasing (@Kworlds MD kMD M) R J m *)
      specialize (H0 emp ltac:(right; constructor)).
(* Goal: @increasing (@Kworlds MD kMD M) R J m *)
      unfold Ensembles.In in H0.
      rewrite <- (TRUTH emp) in H0 by eauto.
(* Goal: Included (@expr L) (@context_sepcon L sL Gamma (@proj1_sig (@context L) cP Phi) (@proj1_sig (@context L) cP Psi)) (@proj1_sig (@context L) cP Phi) *)
      rewrite sat_emp in H0; auto.
Qed.

Lemma nonsplit_canonical_split_smaller
      {nssGamma: NonsplitEmpSeparationLogic L Gamma}
      (AL_DC: at_least derivable_closed cP)
      (TRUTH: forall x, forall m Phi, rel m Phi -> (KRIPKE: M, m |= x <-> proj1_sig Phi x)):
  IncreasingSplitSmallerSeparationAlgebra (Kworlds M).
Proof.
(* Goal: forall n : @Kworlds MD kMD M, @ex (@Kworlds MD kMD M) (fun m : @Kworlds MD kMD M => and (@residue (@Kworlds MD kMD M) R J n m) (@increasing (@Kworlds MD kMD M) R J m)) *)
  hnf; intros.
(* Goal: @Krelation (@Kworlds MD kMD M) R m1 m *)
  destruct (im_bij _ _ rel m1) as [Phi1 ?].
(* Goal: @Krelation (@Kworlds MD kMD M) R m1 m *)
  destruct (im_bij _ _ rel m2) as [Phi2 ?].
(* Goal: @join (@Kworlds MD kMD M) J m m m *)
  destruct (im_bij _ _ rel m) as [Phi ?].
(* Goal: Included (@expr L) (@context_sepcon L sL Gamma (@proj1_sig (@context L) cP Phi) (@proj1_sig (@context L) cP Psi)) (@proj1_sig (@context L) cP Phi) *)
  erewrite H_J in H0 by eauto.
(* Goal: Included (@expr L) (@context_sepcon L sL Gamma (@proj1_sig (@context L) cP Phi) (@proj1_sig (@context L) cP Psi)) (@proj1_sig (@context L) cP Phi) *)
  erewrite H_R by eauto.
(* Goal: Included (@expr L) (@proj1_sig (@context L) cP Phi1) (@proj1_sig (@context L) cP Phi) *)
  unfold Included, Ensembles.In; intros x ?.
(* Goal: @proj1_sig (@context L) cP Phi x *)
  rewrite derivable_closed_element_derivable by (apply AL_DC, (proj2_sig Phi)).
  rewrite <- (emp_sepcon_truep_elim x).
(* Goal: forall n : @Kworlds MD kMD M, @ex (@Kworlds MD kMD M) (fun m : @Kworlds MD kMD M => and (@residue (@Kworlds MD kMD M) R J n m) (@increasing (@Kworlds MD kMD M) R J m)) *)
  apply deduction_andp_intros.
  + apply derivable_assum; apply H0.
(* Goal: Included (@expr L) (@context_sepcon L sL Gamma (@proj1_sig (@context L) cP Phi) (@proj1_sig (@context L) cP Psi)) (@proj1_sig (@context L) cP Phi) *)
    exists x, TT; split; [| split]; auto.
    - apply derivable_assum; auto.
    - apply derivable_impp_refl.
  + rewrite <- derivable_closed_element_derivable by (apply AL_DC, (proj2_sig Phi)).
    rewrite <- (TRUTH emp) by eauto.
(* Goal: Included (@expr L) (@context_sepcon L sL Gamma (@proj1_sig (@context L) cP Phi) (@proj1_sig (@context L) cP Psi)) (@proj1_sig (@context L) cP Phi) *)
    rewrite sat_emp; auto.
Qed.

Lemma dup_canonical_incr_join
      {desGamma: DupEmpSeparationLogic L Gamma}
      (AL_DC: at_least derivable_closed cP)
      (TRUTH: forall x, forall m Phi, rel m Phi -> (KRIPKE: M, m |= x <-> proj1_sig Phi x)):
  IncreasingJoinSelfSeparationAlgebra (Kworlds M).
Proof.
(* Goal: forall n : @Kworlds MD kMD M, @ex (@Kworlds MD kMD M) (fun m : @Kworlds MD kMD M => and (@residue (@Kworlds MD kMD M) R J n m) (@increasing (@Kworlds MD kMD M) R J m)) *)
  hnf; intros.
(* Goal: @join (@Kworlds MD kMD M) J m m m *)
  destruct (im_bij _ _ rel m) as [Phi ?].
(* Goal: Included (@expr L) (@context_sepcon L sL Gamma (@proj1_sig (@context L) cP Phi) (@proj1_sig (@context L) cP Psi)) (@proj1_sig (@context L) cP Phi) *)
  erewrite H_J by eauto.
(* Goal: Ensembles.In (@expr L) (@proj1_sig (@context L) cP Phi) x *)
  intros z [x [y [? [? ?]]]]; subst.
(* Goal: Included (@expr L) (@context_sepcon L sL Gamma (@proj1_sig (@context L) cP Phi) (@proj1_sig (@context L) cP Psi)) (@proj1_sig (@context L) cP Phi) *)
  rewrite derivable_closed_element_derivable by (apply AL_DC, (proj2_sig Phi)); auto.
  rewrite <- (andp_elim1 x y).
  rewrite <- (andp_elim2 x y) at 2.
  rewrite <- emp_dup.
(* Goal: Included (@expr L) (@context_sepcon L sL Gamma (@proj1_sig (@context L) cP Phi) (@proj1_sig (@context L) cP Psi)) (@proj1_sig (@context L) cP Phi) *)
  apply deduction_andp_intros; [apply deduction_andp_intros |]; auto.
  rewrite <- derivable_closed_element_derivable by (apply AL_DC, (proj2_sig Phi)); auto.
  unfold Ensembles.In; rewrite <- (TRUTH emp) by eauto.
(* Goal: Included (@expr L) (@context_sepcon L sL Gamma (@proj1_sig (@context L) cP Phi) (@proj1_sig (@context L) cP Psi)) (@proj1_sig (@context L) cP Phi) *)
  rewrite sat_emp; auto.
Qed.

End Canonical.
