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.GeneralLogic.KripkeModel.
Require Import Logic.ModalLogic.Model.KripkeModel.
Require Import Logic.SeparationLogic.Model.SeparationAlgebra.
Require Import Logic.SeparationLogic.Model.DownwardsClosure.
Require Import Logic.SeparationLogic.Model.OrderedSA.
Require Import Logic.SeparationLogic.Model.OSAGenerators.
Require Import Logic.SeparationLogic.Model.OSAExamples.

Local Open Scope kripke_model.
Import KripkeModelNotation_Intuitionistic.

Module SS.

Class Relation (worlds: Type): Type :=
  Krelation: worlds -> Ensemble worlds.

End SS.

Export SS.

Module Semantics.

Definition stable {worlds: Type} {R: Relation worlds} (X: Ensemble worlds): Prop := forall m n, R m n -> (X m <-> X n).

End Semantics.

Class SeparationAlgebraBisStable (worlds: Type) {J: Join worlds} {R: Relation worlds}: Type := {
  split_bis_stable:
    forall m n, R m n ->
      (forall m1 m2, join m1 m2 m -> exists n1 n2, join n1 n2 n /\ R m1 n1 /\ R m2 n2) /\
       (forall n1 n2, join n1 n2 n -> exists m1 m2, join m1 m2 m /\ R m1 n1 /\ R m2 n2);
  extend_bis_stable:
    forall m n, R m n ->
      (forall m1 m2, join m m1 m2 -> exists n1 n2, join n n1 n2 /\ R m1 n1 /\ R m2 n2) /\
       (forall n1 n2, join n n1 n2 -> exists m1 m2, join m m1 m2 /\ R m1 n1 /\ R m2 n2)
}.

Class SeparationAlgebraAbsorbStable (worlds: Type) {R1: KI.Relation worlds} {J: Join worlds} {R2: Relation worlds}: Type := {
  SA_absorb_stable:
    forall m m1 m2, join m1 m2 m ->
      exists n1 n2, join n1 n2 m /\ R2 n1 m /\ R2 n2 m /\ m1 <= n1 /\ m2 <= n2
}.

Class StrongSeparationAlgebraAbsorbStable (worlds: Type) {J: Join worlds} {R: Relation worlds}: Type := {
  strong_SA_absorb_stable:
    forall m m1 m2, join m1 m2 m -> R m1 m /\ R m2 m
}.

Lemma DownwardsClosure_SAAbsorbStable (worlds: Type) {R1: KI.Relation worlds} {po_R: PreOrder KI.Krelation} {J: Join worlds} {R2: Relation worlds} {SA_abs': StrongSeparationAlgebraAbsorbStable worlds}: @SeparationAlgebraAbsorbStable worlds R1 DownwardsClosure_J R2.
Proof.
(* Goal: @SeparationAlgebraAbsorbStable nat nat_geR min_Join (@eq nat) *)
  constructor.
(* Goal: forall (m m1 m2 : nat) (_ : @join nat min_Join m1 m2 m), @ex nat (fun n1 : nat => @ex nat (fun n2 : nat => and (@join nat min_Join n1 n2 m) (and (@eq nat n1 m) (and (@eq nat n2 m) (and (@KI.Krelation nat nat_geR m1 n1) (@KI.Krelation nat nat_geR m2 n2)))))) *)
  intros.
(* Goal: @ex worlds (fun n1 : worlds => @ex worlds (fun n2 : worlds => and (@join worlds (@DownwardsClosure_J worlds R1 J) n1 n2 m) (and (R2 n1 m) (and (R2 n2 m) (and (@KI.Krelation worlds R1 m1 n1) (@KI.Krelation worlds R1 m2 n2)))))) *)
  hnf in H.
(* Goal: @ex worlds (fun n1 : worlds => @ex worlds (fun n2 : worlds => and (@join worlds (@DownwardsClosure_J worlds R1 J) n1 n2 m) (and (R2 n1 m) (and (R2 n2 m) (and (@KI.Krelation worlds R1 m1 n1) (@KI.Krelation worlds R1 m2 n2)))))) *)
  destruct H as [n1 [n2 [? [? ?]]]].
(* Goal: @join worlds (@DownwardsClosure_J worlds R1 J) n1 n2 m *)
  exists n1, n2.
(* Goal: and (@join nat min_Join m m m) (and (@eq nat m m) (and (@eq nat m m) (and (@KI.Krelation nat nat_geR m1 m) (@KI.Krelation nat nat_geR m2 m)))) *)
  split; [| split; [| split; [| split ]]]; auto.
(* Goal: @join worlds (@DownwardsClosure_J worlds R1 J) n1 n2 m *)
  + exists n1, n2.
(* Goal: and (@KI.Krelation worlds R1 n1 n1) (and (@KI.Krelation worlds R1 n2 n2) (@join worlds J n1 n2 m)) *)
    split; [| split]; auto; reflexivity.
  + destruct (strong_SA_absorb_stable _ _ _ H1); auto.
  + destruct (strong_SA_absorb_stable _ _ _ H1); auto.
Qed.

Instance prod_SAbis (A B: Type) (JA: Join A) (JB: Join B) (RA: SS.Relation A) (RB: SS.Relation B) {SAbisA: SeparationAlgebraBisStable A} {SAbisB: SeparationAlgebraBisStable B}: @SeparationAlgebraBisStable (A * B) (@prod_Join _ _ JA JB) (RelProd RA RB).
Proof.
(* Goal: @SeparationAlgebraAbsorbStable nat nat_geR min_Join (@eq nat) *)
  constructor.
  + intros [m1 m2] [n1 n2] [? ?].
(* Goal: and (forall (m3 m4 : prod A B) (_ : @join (prod A B) (@prod_Join A B JA JB) m3 m4 (@pair A B m1 m2)), @ex (prod A B) (fun n3 : prod A B => @ex (prod A B) (fun n4 : prod A B => and (@join (prod A B) (@prod_Join A B JA JB) n3 n4 (@pair A B n1 n2)) (and (@RelProd A B RA RB m3 n3) (@RelProd A B RA RB m4 n4))))) (forall (n3 n4 : prod A B) (_ : @join (prod A B) (@prod_Join A B JA JB) n3 n4 (@pair A B n1 n2)), @ex (prod A B) (fun m3 : prod A B => @ex (prod A B) (fun m4 : prod A B => and (@join (prod A B) (@prod_Join A B JA JB) m3 m4 (@pair A B m1 m2)) (and (@RelProd A B RA RB m3 n3) (@RelProd A B RA RB m4 n4))))) *)
    pose proof (@split_bis_stable A _ _ SAbisA m1 n1 H).
(* Goal: and (forall (m3 m4 : prod A B) (_ : @join (prod A B) (@prod_Join A B JA JB) m3 m4 (@pair A B m1 m2)), @ex (prod A B) (fun n3 : prod A B => @ex (prod A B) (fun n4 : prod A B => and (@join (prod A B) (@prod_Join A B JA JB) n3 n4 (@pair A B n1 n2)) (and (@RelProd A B RA RB m3 n3) (@RelProd A B RA RB m4 n4))))) (forall (n3 n4 : prod A B) (_ : @join (prod A B) (@prod_Join A B JA JB) n3 n4 (@pair A B n1 n2)), @ex (prod A B) (fun m3 : prod A B => @ex (prod A B) (fun m4 : prod A B => and (@join (prod A B) (@prod_Join A B JA JB) m3 m4 (@pair A B m1 m2)) (and (@RelProd A B RA RB m3 n3) (@RelProd A B RA RB m4 n4))))) *)
    pose proof (@split_bis_stable B _ _ SAbisB m2 n2 H0).
(* Goal: and (forall (m3 m4 : prod A B) (_ : @join (prod A B) (@prod_Join A B JA JB) (@pair A B m1 m2) m3 m4), @ex (prod A B) (fun n3 : prod A B => @ex (prod A B) (fun n4 : prod A B => and (@join (prod A B) (@prod_Join A B JA JB) (@pair A B n1 n2) n3 n4) (and (@RelProd A B RA RB m3 n3) (@RelProd A B RA RB m4 n4))))) (forall (n3 n4 : prod A B) (_ : @join (prod A B) (@prod_Join A B JA JB) (@pair A B n1 n2) n3 n4), @ex (prod A B) (fun m3 : prod A B => @ex (prod A B) (fun m4 : prod A B => and (@join (prod A B) (@prod_Join A B JA JB) (@pair A B m1 m2) m3 m4) (and (@RelProd A B RA RB m3 n3) (@RelProd A B RA RB m4 n4))))) *)
    split.
    - intros [n11 n12] [n21 n22] [? ?].
(* Goal: @ex (prod A B) (fun n3 : prod A B => @ex (prod A B) (fun n4 : prod A B => and (@join (prod A B) (@prod_Join A B JA JB) (@pair A B n1 n2) n3 n4) (and (@RelProd A B RA RB (@pair A B n11 n12) n3) (@RelProd A B RA RB (@pair A B n21 n22) n4)))) *)
      destruct H1 as [? _].
(* Goal: @ex (prod A B) (fun n3 : prod A B => @ex (prod A B) (fun n4 : prod A B => and (@join (prod A B) (@prod_Join A B JA JB) (@pair A B n1 n2) n3 n4) (and (@RelProd A B RA RB (@pair A B n11 n12) n3) (@RelProd A B RA RB (@pair A B n21 n22) n4)))) *)
      destruct H2 as [? _].
(* Goal: @ex (prod A B) (fun m3 : prod A B => @ex (prod A B) (fun m4 : prod A B => and (@join (prod A B) (@prod_Join A B JA JB) (@pair A B m1 m2) m3 m4) (and (@RelProd A B RA RB m3 (@pair A B m11 m12)) (@RelProd A B RA RB m4 (@pair A B m21 m22))))) *)
      specialize (H1 _ _ H3).
(* Goal: @ex (prod A B) (fun n3 : prod A B => @ex (prod A B) (fun n4 : prod A B => and (@join (prod A B) (@prod_Join A B JA JB) (@pair A B n1 n2) n3 n4) (and (@RelProd A B RA RB (@pair A B n11 n12) n3) (@RelProd A B RA RB (@pair A B n21 n22) n4)))) *)
      destruct H1 as [m11 [m21 [? [? ?]]]].
(* Goal: @ex (prod A B) (fun m3 : prod A B => @ex (prod A B) (fun m4 : prod A B => and (@join (prod A B) (@prod_Join A B JA JB) (@pair A B m1 m2) m3 m4) (and (@RelProd A B RA RB m3 (@pair A B m11 m12)) (@RelProd A B RA RB m4 (@pair A B m21 m22))))) *)
      specialize (H2 _ _ H4).
(* Goal: @ex (prod A B) (fun n3 : prod A B => @ex (prod A B) (fun n4 : prod A B => and (@join (prod A B) (@prod_Join A B JA JB) (@pair A B n1 n2) n3 n4) (and (@RelProd A B RA RB (@pair A B n11 n12) n3) (@RelProd A B RA RB (@pair A B n21 n22) n4)))) *)
      destruct H2 as [m12 [m22 [? [? ?]]]].
(* Goal: @ex (prod A B) (fun n3 : prod A B => @ex (prod A B) (fun n4 : prod A B => and (@join (prod A B) (@prod_Join A B JA JB) (@pair A B n1 n2) n3 n4) (and (@RelProd A B RA RB (@pair A B n11 n12) n3) (@RelProd A B RA RB (@pair A B n21 n22) n4)))) *)
      exists (m11, m12), (m21, m22).
(* Goal: and (@join (prod A B) (@prod_Join A B JA JB) (@pair A B m1 m2) (@pair A B n11 n12) (@pair A B n21 n22)) (and (@RelProd A B RA RB (@pair A B n11 n12) (@pair A B m11 m12)) (@RelProd A B RA RB (@pair A B n21 n22) (@pair A B m21 m22))) *)
      split; [| split]; split; auto.
    - intros [m11 m12] [m21 m22] [? ?].
(* Goal: @ex (prod A B) (fun m3 : prod A B => @ex (prod A B) (fun m4 : prod A B => and (@join (prod A B) (@prod_Join A B JA JB) (@pair A B m1 m2) m3 m4) (and (@RelProd A B RA RB m3 (@pair A B m11 m12)) (@RelProd A B RA RB m4 (@pair A B m21 m22))))) *)
      destruct H1 as [_ ?].
(* Goal: @ex (prod A B) (fun m3 : prod A B => @ex (prod A B) (fun m4 : prod A B => and (@join (prod A B) (@prod_Join A B JA JB) (@pair A B m1 m2) m3 m4) (and (@RelProd A B RA RB m3 (@pair A B m11 m12)) (@RelProd A B RA RB m4 (@pair A B m21 m22))))) *)
      destruct H2 as [_ ?].
(* Goal: @ex (prod A B) (fun m3 : prod A B => @ex (prod A B) (fun m4 : prod A B => and (@join (prod A B) (@prod_Join A B JA JB) (@pair A B m1 m2) m3 m4) (and (@RelProd A B RA RB m3 (@pair A B m11 m12)) (@RelProd A B RA RB m4 (@pair A B m21 m22))))) *)
      specialize (H1 _ _ H3).
(* Goal: @ex (prod A B) (fun m3 : prod A B => @ex (prod A B) (fun m4 : prod A B => and (@join (prod A B) (@prod_Join A B JA JB) (@pair A B m1 m2) m3 m4) (and (@RelProd A B RA RB m3 (@pair A B m11 m12)) (@RelProd A B RA RB m4 (@pair A B m21 m22))))) *)
      destruct H1 as [n11 [n21 [? [? ?]]]].
(* Goal: @ex (prod A B) (fun m3 : prod A B => @ex (prod A B) (fun m4 : prod A B => and (@join (prod A B) (@prod_Join A B JA JB) (@pair A B m1 m2) m3 m4) (and (@RelProd A B RA RB m3 (@pair A B m11 m12)) (@RelProd A B RA RB m4 (@pair A B m21 m22))))) *)
      specialize (H2 _ _ H4).
(* Goal: @ex (prod A B) (fun m3 : prod A B => @ex (prod A B) (fun m4 : prod A B => and (@join (prod A B) (@prod_Join A B JA JB) (@pair A B m1 m2) m3 m4) (and (@RelProd A B RA RB m3 (@pair A B m11 m12)) (@RelProd A B RA RB m4 (@pair A B m21 m22))))) *)
      destruct H2 as [n12 [n22 [? [? ?]]]].
(* Goal: @ex (prod A B) (fun n1 : prod A B => @ex (prod A B) (fun n2 : prod A B => and (@join (prod A B) (@prod_Join A B JA JB) n1 n2 (@pair A B m1 m2)) (and (@RelProd A B R2A R2B n1 (@pair A B m1 m2)) (and (@RelProd A B R2A R2B n2 (@pair A B m1 m2)) (and (@KI.Krelation (prod A B) (@RelProd A B R1A R1B) (@pair A B m11 m12) n1) (@KI.Krelation (prod A B) (@RelProd A B R1A R1B) (@pair A B m21 m22) n2)))))) *)
      exists (n11, n12), (n21, n22).
(* Goal: and (@join (prod A B) (@prod_Join A B JA JB) (@pair A B m1 m2) (@pair A B n11 n12) (@pair A B n21 n22)) (and (@RelProd A B RA RB (@pair A B n11 n12) (@pair A B m11 m12)) (@RelProd A B RA RB (@pair A B n21 n22) (@pair A B m21 m22))) *)
      split; [| split]; split; auto.
  + intros [m1 m2] [n1 n2] [? ?].
(* Goal: and (forall (m3 m4 : prod A B) (_ : @join (prod A B) (@prod_Join A B JA JB) (@pair A B m1 m2) m3 m4), @ex (prod A B) (fun n3 : prod A B => @ex (prod A B) (fun n4 : prod A B => and (@join (prod A B) (@prod_Join A B JA JB) (@pair A B n1 n2) n3 n4) (and (@RelProd A B RA RB m3 n3) (@RelProd A B RA RB m4 n4))))) (forall (n3 n4 : prod A B) (_ : @join (prod A B) (@prod_Join A B JA JB) (@pair A B n1 n2) n3 n4), @ex (prod A B) (fun m3 : prod A B => @ex (prod A B) (fun m4 : prod A B => and (@join (prod A B) (@prod_Join A B JA JB) (@pair A B m1 m2) m3 m4) (and (@RelProd A B RA RB m3 n3) (@RelProd A B RA RB m4 n4))))) *)
    pose proof (@extend_bis_stable A _ _ SAbisA m1 n1 H).
(* Goal: and (forall (m3 m4 : prod A B) (_ : @join (prod A B) (@prod_Join A B JA JB) (@pair A B m1 m2) m3 m4), @ex (prod A B) (fun n3 : prod A B => @ex (prod A B) (fun n4 : prod A B => and (@join (prod A B) (@prod_Join A B JA JB) (@pair A B n1 n2) n3 n4) (and (@RelProd A B RA RB m3 n3) (@RelProd A B RA RB m4 n4))))) (forall (n3 n4 : prod A B) (_ : @join (prod A B) (@prod_Join A B JA JB) (@pair A B n1 n2) n3 n4), @ex (prod A B) (fun m3 : prod A B => @ex (prod A B) (fun m4 : prod A B => and (@join (prod A B) (@prod_Join A B JA JB) (@pair A B m1 m2) m3 m4) (and (@RelProd A B RA RB m3 n3) (@RelProd A B RA RB m4 n4))))) *)
    pose proof (@extend_bis_stable B _ _ SAbisB m2 n2 H0).
(* Goal: and (forall (m3 m4 : prod A B) (_ : @join (prod A B) (@prod_Join A B JA JB) (@pair A B m1 m2) m3 m4), @ex (prod A B) (fun n3 : prod A B => @ex (prod A B) (fun n4 : prod A B => and (@join (prod A B) (@prod_Join A B JA JB) (@pair A B n1 n2) n3 n4) (and (@RelProd A B RA RB m3 n3) (@RelProd A B RA RB m4 n4))))) (forall (n3 n4 : prod A B) (_ : @join (prod A B) (@prod_Join A B JA JB) (@pair A B n1 n2) n3 n4), @ex (prod A B) (fun m3 : prod A B => @ex (prod A B) (fun m4 : prod A B => and (@join (prod A B) (@prod_Join A B JA JB) (@pair A B m1 m2) m3 m4) (and (@RelProd A B RA RB m3 n3) (@RelProd A B RA RB m4 n4))))) *)
    split.
    - intros [n11 n12] [n21 n22] [? ?].
(* Goal: @ex (prod A B) (fun n3 : prod A B => @ex (prod A B) (fun n4 : prod A B => and (@join (prod A B) (@prod_Join A B JA JB) (@pair A B n1 n2) n3 n4) (and (@RelProd A B RA RB (@pair A B n11 n12) n3) (@RelProd A B RA RB (@pair A B n21 n22) n4)))) *)
      destruct H1 as [? _].
(* Goal: @ex (prod A B) (fun n3 : prod A B => @ex (prod A B) (fun n4 : prod A B => and (@join (prod A B) (@prod_Join A B JA JB) (@pair A B n1 n2) n3 n4) (and (@RelProd A B RA RB (@pair A B n11 n12) n3) (@RelProd A B RA RB (@pair A B n21 n22) n4)))) *)
      destruct H2 as [? _].
(* Goal: @ex (prod A B) (fun m3 : prod A B => @ex (prod A B) (fun m4 : prod A B => and (@join (prod A B) (@prod_Join A B JA JB) (@pair A B m1 m2) m3 m4) (and (@RelProd A B RA RB m3 (@pair A B m11 m12)) (@RelProd A B RA RB m4 (@pair A B m21 m22))))) *)
      specialize (H1 _ _ H3).
(* Goal: @ex (prod A B) (fun n3 : prod A B => @ex (prod A B) (fun n4 : prod A B => and (@join (prod A B) (@prod_Join A B JA JB) (@pair A B n1 n2) n3 n4) (and (@RelProd A B RA RB (@pair A B n11 n12) n3) (@RelProd A B RA RB (@pair A B n21 n22) n4)))) *)
      destruct H1 as [m11 [m21 [? [? ?]]]].
(* Goal: @ex (prod A B) (fun m3 : prod A B => @ex (prod A B) (fun m4 : prod A B => and (@join (prod A B) (@prod_Join A B JA JB) (@pair A B m1 m2) m3 m4) (and (@RelProd A B RA RB m3 (@pair A B m11 m12)) (@RelProd A B RA RB m4 (@pair A B m21 m22))))) *)
      specialize (H2 _ _ H4).
(* Goal: @ex (prod A B) (fun n3 : prod A B => @ex (prod A B) (fun n4 : prod A B => and (@join (prod A B) (@prod_Join A B JA JB) (@pair A B n1 n2) n3 n4) (and (@RelProd A B RA RB (@pair A B n11 n12) n3) (@RelProd A B RA RB (@pair A B n21 n22) n4)))) *)
      destruct H2 as [m12 [m22 [? [? ?]]]].
(* Goal: @ex (prod A B) (fun n3 : prod A B => @ex (prod A B) (fun n4 : prod A B => and (@join (prod A B) (@prod_Join A B JA JB) (@pair A B n1 n2) n3 n4) (and (@RelProd A B RA RB (@pair A B n11 n12) n3) (@RelProd A B RA RB (@pair A B n21 n22) n4)))) *)
      exists (m11, m12), (m21, m22).
(* Goal: and (@join (prod A B) (@prod_Join A B JA JB) (@pair A B m1 m2) (@pair A B n11 n12) (@pair A B n21 n22)) (and (@RelProd A B RA RB (@pair A B n11 n12) (@pair A B m11 m12)) (@RelProd A B RA RB (@pair A B n21 n22) (@pair A B m21 m22))) *)
      split; [| split]; split; auto.
    - intros [m11 m12] [m21 m22] [? ?].
(* Goal: @ex (prod A B) (fun m3 : prod A B => @ex (prod A B) (fun m4 : prod A B => and (@join (prod A B) (@prod_Join A B JA JB) (@pair A B m1 m2) m3 m4) (and (@RelProd A B RA RB m3 (@pair A B m11 m12)) (@RelProd A B RA RB m4 (@pair A B m21 m22))))) *)
      destruct H1 as [_ ?].
(* Goal: @ex (prod A B) (fun m3 : prod A B => @ex (prod A B) (fun m4 : prod A B => and (@join (prod A B) (@prod_Join A B JA JB) (@pair A B m1 m2) m3 m4) (and (@RelProd A B RA RB m3 (@pair A B m11 m12)) (@RelProd A B RA RB m4 (@pair A B m21 m22))))) *)
      destruct H2 as [_ ?].
(* Goal: @ex (prod A B) (fun m3 : prod A B => @ex (prod A B) (fun m4 : prod A B => and (@join (prod A B) (@prod_Join A B JA JB) (@pair A B m1 m2) m3 m4) (and (@RelProd A B RA RB m3 (@pair A B m11 m12)) (@RelProd A B RA RB m4 (@pair A B m21 m22))))) *)
      specialize (H1 _ _ H3).
(* Goal: @ex (prod A B) (fun m3 : prod A B => @ex (prod A B) (fun m4 : prod A B => and (@join (prod A B) (@prod_Join A B JA JB) (@pair A B m1 m2) m3 m4) (and (@RelProd A B RA RB m3 (@pair A B m11 m12)) (@RelProd A B RA RB m4 (@pair A B m21 m22))))) *)
      destruct H1 as [n11 [n21 [? [? ?]]]].
(* Goal: @ex (prod A B) (fun m3 : prod A B => @ex (prod A B) (fun m4 : prod A B => and (@join (prod A B) (@prod_Join A B JA JB) (@pair A B m1 m2) m3 m4) (and (@RelProd A B RA RB m3 (@pair A B m11 m12)) (@RelProd A B RA RB m4 (@pair A B m21 m22))))) *)
      specialize (H2 _ _ H4).
(* Goal: @ex (prod A B) (fun m3 : prod A B => @ex (prod A B) (fun m4 : prod A B => and (@join (prod A B) (@prod_Join A B JA JB) (@pair A B m1 m2) m3 m4) (and (@RelProd A B RA RB m3 (@pair A B m11 m12)) (@RelProd A B RA RB m4 (@pair A B m21 m22))))) *)
      destruct H2 as [n12 [n22 [? [? ?]]]].
(* Goal: @ex (prod A B) (fun n1 : prod A B => @ex (prod A B) (fun n2 : prod A B => and (@join (prod A B) (@prod_Join A B JA JB) n1 n2 (@pair A B m1 m2)) (and (@RelProd A B R2A R2B n1 (@pair A B m1 m2)) (and (@RelProd A B R2A R2B n2 (@pair A B m1 m2)) (and (@KI.Krelation (prod A B) (@RelProd A B R1A R1B) (@pair A B m11 m12) n1) (@KI.Krelation (prod A B) (@RelProd A B R1A R1B) (@pair A B m21 m22) n2)))))) *)
      exists (n11, n12), (n21, n22).
(* Goal: and (@join (prod A B) (@prod_Join A B JA JB) (@pair A B m1 m2) (@pair A B n11 n12) (@pair A B n21 n22)) (and (@RelProd A B RA RB (@pair A B n11 n12) (@pair A B m11 m12)) (@RelProd A B RA RB (@pair A B n21 n22) (@pair A B m21 m22))) *)
      split; [| split]; split; auto.
Qed.    

Instance prod_SAabs (A B: Type) (R1A: KI.Relation A) (R1B: KI.Relation B) (JA: Join A) (JB: Join B) (R2A: SS.Relation A) (R2B: SS.Relation B) {SAabsA: SeparationAlgebraAbsorbStable A} {SAabsB: SeparationAlgebraAbsorbStable B}: @SeparationAlgebraAbsorbStable (A * B) (RelProd R1A R1B) (@prod_Join _ _ JA JB) (RelProd R2A R2B).
Proof.
(* Goal: @SeparationAlgebraAbsorbStable nat nat_geR min_Join (@eq nat) *)
  constructor.
(* Goal: forall (m m1 m2 : prod A B) (_ : @join (prod A B) (@prod_Join A B JA JB) m1 m2 m), @ex (prod A B) (fun n1 : prod A B => @ex (prod A B) (fun n2 : prod A B => and (@join (prod A B) (@prod_Join A B JA JB) n1 n2 m) (and (@RelProd A B R2A R2B n1 m) (and (@RelProd A B R2A R2B n2 m) (and (@KI.Krelation (prod A B) (@RelProd A B R1A R1B) m1 n1) (@KI.Krelation (prod A B) (@RelProd A B R1A R1B) m2 n2)))))) *)
  intros [m1 m2] [m11 m12] [m21 m22] [? ?].
(* Goal: @ex (prod A B) (fun n1 : prod A B => @ex (prod A B) (fun n2 : prod A B => and (@join (prod A B) (@prod_Join A B JA JB) n1 n2 (@pair A B m1 m2)) (and (@RelProd A B R2A R2B n1 (@pair A B m1 m2)) (and (@RelProd A B R2A R2B n2 (@pair A B m1 m2)) (and (@KI.Krelation (prod A B) (@RelProd A B R1A R1B) (@pair A B m11 m12) n1) (@KI.Krelation (prod A B) (@RelProd A B R1A R1B) (@pair A B m21 m22) n2)))))) *)
  destruct (@SA_absorb_stable _ _ _ _ SAabsA _ _ _ H) as [n11 [n21 [? [? [? [? ?]]]]]].
(* Goal: @ex (prod A B) (fun n1 : prod A B => @ex (prod A B) (fun n2 : prod A B => and (@join (prod A B) (@prod_Join A B JA JB) n1 n2 (@pair A B m1 m2)) (and (@RelProd A B R2A R2B n1 (@pair A B m1 m2)) (and (@RelProd A B R2A R2B n2 (@pair A B m1 m2)) (and (@KI.Krelation (prod A B) (@RelProd A B R1A R1B) (@pair A B m11 m12) n1) (@KI.Krelation (prod A B) (@RelProd A B R1A R1B) (@pair A B m21 m22) n2)))))) *)
  destruct (@SA_absorb_stable _ _ _ _ SAabsB _ _ _ H0) as [n12 [n22 [? [? [? [? ?]]]]]].
(* Goal: @ex (prod A B) (fun n1 : prod A B => @ex (prod A B) (fun n2 : prod A B => and (@join (prod A B) (@prod_Join A B JA JB) n1 n2 (@pair A B m1 m2)) (and (@RelProd A B R2A R2B n1 (@pair A B m1 m2)) (and (@RelProd A B R2A R2B n2 (@pair A B m1 m2)) (and (@KI.Krelation (prod A B) (@RelProd A B R1A R1B) (@pair A B m11 m12) n1) (@KI.Krelation (prod A B) (@RelProd A B R1A R1B) (@pair A B m21 m22) n2)))))) *)
  exists (n11, n12), (n21, n22).
(* Goal: and (@join (prod A B) (@prod_Join A B JA JB) (@pair A B n11 n12) (@pair A B n21 n22) (@pair A B m1 m2)) (and (@RelProd A B R2A R2B (@pair A B n11 n12) (@pair A B m1 m2)) (and (@RelProd A B R2A R2B (@pair A B n21 n22) (@pair A B m1 m2)) (and (@KI.Krelation (prod A B) (@RelProd A B R1A R1B) (@pair A B m11 m12) (@pair A B n11 n12)) (@KI.Krelation (prod A B) (@RelProd A B R1A R1B) (@pair A B m21 m22) (@pair A B n21 n22))))) *)
  split; [| split; [| split; [| split]]]; split; auto.
Qed.

Instance full_SAbis (A: Type) {R: KI.Relation A} {po_R: PreOrder KI.Krelation} {J: Join A} {SA: SeparationAlgebra A} {dSA: DownwardsClosedSeparationAlgebra A} {resSA: ResidualSeparationAlgebra A} : @SeparationAlgebraBisStable A J full_relation.
Proof.
(* Goal: @SeparationAlgebraAbsorbStable nat nat_geR min_Join (@eq nat) *)
  constructor.
(* Goal: forall (m m1 m2 : nat) (_ : @join nat min_Join m1 m2 m), @ex nat (fun n1 : nat => @ex nat (fun n2 : nat => and (@join nat min_Join n1 n2 m) (and (@eq nat n1 m) (and (@eq nat n2 m) (and (@KI.Krelation nat nat_geR m1 n1) (@KI.Krelation nat nat_geR m2 n2)))))) *)
  + intros; split; intros.
    - destruct (residue_exists n) as [n1 [n2 [? ?]]].
(* Goal: @ex A (fun m1 : A => @ex A (fun m2 : A => and (@join A J n m1 m2) (and (@eq A m1 n1) (@eq A m2 n2)))) *)
      exists n1, n2; auto.
    - destruct (residue_exists m) as [m1 [m2 [? ?]]].
(* Goal: @ex A (fun n1 : A => @ex A (fun n2 : A => and (@join A J n n1 n2) (and (@eq A m1 n1) (@eq A m2 n2)))) *)
      exists m1, m2; auto.
(* Goal: forall (m m1 m2 : nat) (_ : @join nat min_Join m1 m2 m), @ex nat (fun n1 : nat => @ex nat (fun n2 : nat => and (@join nat min_Join n1 n2 m) (and (@eq nat n1 m) (and (@eq nat n2 m) (and (@KI.Krelation nat nat_geR m1 n1) (@KI.Krelation nat nat_geR m2 n2)))))) *)
  + intros; split; intros.
    - destruct (residual_extensible n) as [n1 [n2 ?]].
(* Goal: @ex A (fun m1 : A => @ex A (fun m2 : A => and (@join A J n m1 m2) (and (@eq A m1 n1) (@eq A m2 n2)))) *)
      exists n1, n2; auto.
    - destruct (residual_extensible m) as [m1 [m2 ?]].
(* Goal: @ex A (fun n1 : A => @ex A (fun n2 : A => and (@join A J n n1 n2) (and (@eq A m1 n1) (@eq A m2 n2)))) *)
      exists m1, m2; auto.
Qed.

Instance full_SAabs (A: Type) {R: KI.Relation A} {po_R: PreOrder KI.Krelation} {J: Join A} : @SeparationAlgebraAbsorbStable A R J full_relation.
Proof.
(* Goal: @SeparationAlgebraAbsorbStable nat nat_geR min_Join (@eq nat) *)
  constructor.
(* Goal: forall (m m1 m2 : nat) (_ : @join nat min_Join m1 m2 m), @ex nat (fun n1 : nat => @ex nat (fun n2 : nat => and (@join nat min_Join n1 n2 m) (and (@eq nat n1 m) (and (@eq nat n2 m) (and (@KI.Krelation nat nat_geR m1 n1) (@KI.Krelation nat nat_geR m2 n2)))))) *)
  intros.
(* Goal: @ex A (fun n1 : A => @ex A (fun n2 : A => and (@join A J n1 n2 m) (and (@full_relation A n1 m) (and (@full_relation A n2 m) (and (@KI.Krelation A R m1 n1) (@KI.Krelation A R m2 n2)))))) *)
  exists m1, m2.
(* Goal: and (@join A J m1 m2 m) (and (@full_relation A m1 m) (and (@full_relation A m2 m) (and (@KI.Krelation A R m1 m1) (@KI.Krelation A R m2 m2)))) *)
  split; [| split; [| split; [| split]]]; solve [hnf; auto | reflexivity].
Qed.

Instance eq_SAbis (A: Type) {J: Join A}: @SeparationAlgebraBisStable A J eq.
Proof.
(* Goal: @SeparationAlgebraAbsorbStable nat nat_geR min_Join (@eq nat) *)
  constructor.
(* Goal: forall (m m1 m2 : nat) (_ : @join nat min_Join m1 m2 m), @ex nat (fun n1 : nat => @ex nat (fun n2 : nat => and (@join nat min_Join n1 n2 m) (and (@eq nat n1 m) (and (@eq nat n2 m) (and (@KI.Krelation nat nat_geR m1 n1) (@KI.Krelation nat nat_geR m2 n2)))))) *)
  + intros; subst; split; intros.
    - exists m1, m2; auto.
    - exists n1, n2; auto.
(* Goal: forall (m m1 m2 : nat) (_ : @join nat min_Join m1 m2 m), @ex nat (fun n1 : nat => @ex nat (fun n2 : nat => and (@join nat min_Join n1 n2 m) (and (@eq nat n1 m) (and (@eq nat n2 m) (and (@KI.Krelation nat nat_geR m1 n1) (@KI.Krelation nat nat_geR m2 n2)))))) *)
  + intros; subst; split; intros.
    - exists m1, m2; auto.
    - exists n1, n2; auto.
Qed.

Instance geR_min_eq_SAabs: @SeparationAlgebraAbsorbStable nat nat_geR min_Join eq.
Proof.
(* Goal: @SeparationAlgebraAbsorbStable nat nat_geR min_Join (@eq nat) *)
  constructor.
(* Goal: forall (m m1 m2 : nat) (_ : @join nat min_Join m1 m2 m), @ex nat (fun n1 : nat => @ex nat (fun n2 : nat => and (@join nat min_Join n1 n2 m) (and (@eq nat n1 m) (and (@eq nat n2 m) (and (@KI.Krelation nat nat_geR m1 n1) (@KI.Krelation nat nat_geR m2 n2)))))) *)
  intros.
(* Goal: @ex nat (fun n1 : nat => @ex nat (fun n2 : nat => and (@join nat min_Join n1 n2 m) (and (@eq nat n1 m) (and (@eq nat n2 m) (and (@KI.Krelation nat nat_geR m1 n1) (@KI.Krelation nat nat_geR m2 n2)))))) *)
  exists m, m.
(* Goal: and (@join nat min_Join m m m) (and (@eq nat m m) (and (@eq nat m m) (and (@KI.Krelation nat nat_geR m1 m) (@KI.Krelation nat nat_geR m2 m)))) *)
  inversion H; subst.
(* Goal: and (@join nat min_Join m m m) (and (@eq nat m m) (and (@eq nat m m) (and (@KI.Krelation nat nat_geR m1 m) (@KI.Krelation nat nat_geR m2 m)))) *)
  split; [| split; [| split; [| split]]]; auto.
(* Goal: @join nat min_Join m m m *)
  constructor; auto.
Qed.

Require Import Logic.GeneralLogic.Base.

Class SemanticStable (L: Language) (MD: Model) {kMD: KripkeModel MD} (M: Kmodel) {R: Relation (Kworlds M)} (SM: Semantics L MD): Type := {
  semantic_stable: expr -> Prop;
  denote_stable: forall x, semantic_stable x <-> Semantics.stable (Kdenotation M x)
}.

