Require Import Coq.Logic.Classical_Prop.
Require Import Logic.lib.Coqlib.
Require Import Logic.GeneralLogic.KripkeModel.
Require Import Logic.SeparationLogic.Model.SeparationAlgebra.
Require Import Logic.SeparationLogic.Model.OrderedSA.

Local Open Scope kripke_model.
Import KripkeModelNotation_Intuitionistic.

Section UpwardsClosure.

Context {worlds: Type}
        {R: Relation worlds}
        {po_R: PreOrder Krelation}
        {J: Join worlds}
        {SA: SeparationAlgebra worlds}
        {dSA: DownwardsClosedSeparationAlgebra worlds}.

(** *Upwards CLosure*)
Definition UpwardsClosure_J: Join worlds.
(* Goal: Join worlds *)
Proof. intros m1 m2 m; exact (exists n, n <= m /\ join m1 m2 n).
Defined.

Definition UpwardsClosure_SA:
  @SeparationAlgebra worlds (UpwardsClosure_J).
Proof.
(* Goal: @IncreasingSeparationAlgebra worlds R UpwardsClosure_J *)
  constructor.
  + intros.
(* Goal: @ex worlds (fun n : worlds => and (@join worlds UpwardsClosure_J n1 n2 n) (@Krelation worlds R n m)) *)
    destruct H as [n [? ?]].
(* Goal: @join worlds UpwardsClosure_J m2 m1 m *)
    exists n.
(* Goal: and (@Krelation worlds R n' n') (@join worlds J m n n') *)
    split; auto.
(* Goal: @join worlds J m2 m1 n *)
    apply join_comm; auto.
  + intros.
(* Goal: @ex worlds (fun myz : worlds => and (@join worlds UpwardsClosure_J my mz myz) (@join worlds UpwardsClosure_J mx myz mxyz)) *)
    rename mx into mx', my into my', mz into mz'.
(* Goal: @ex worlds (fun myz : worlds => and (@join worlds UpwardsClosure_J my' mz' myz) (@join worlds UpwardsClosure_J mx' myz mxyz)) *)
    destruct H as [mxy' [? ?]].
(* Goal: @ex worlds (fun myz : worlds => and (@join worlds UpwardsClosure_J my' mz' myz) (@join worlds UpwardsClosure_J mx' myz mxyz)) *)
    destruct H0 as [mxyz' [? ?]].
(* Goal: @ex worlds (fun myz : worlds => and (@join worlds UpwardsClosure_J my' mz' myz) (@join worlds UpwardsClosure_J mx' myz mxyz)) *)
    destruct (join_Korder_down _ _ _ _ mz' H2 H) as [mxyz'' [? ?]]; [reflexivity |].
(* Goal: @ex worlds (fun myz : worlds => and (@join worlds UpwardsClosure_J my' mz' myz) (@join worlds UpwardsClosure_J mx' myz mxyz)) *)
    destruct (join_assoc _ _ _ _ _ H1 H3) as [myz' [? ?]].
(* Goal: @ex worlds (fun myz : worlds => and (@join worlds UpwardsClosure_J my' mz' myz) (@join worlds UpwardsClosure_J mx' myz mxyz)) *)
    exists myz'.
(* Goal: and (@join worlds UpwardsClosure_J my' mz' myz') (@join worlds UpwardsClosure_J mx' myz' mxyz) *)
    split.
(* Goal: and (@Krelation worlds R n' n') (@join worlds J m n n') *)
    - exists myz'; split; auto.
(* Goal: @Krelation worlds R n' n' *)
      reflexivity.
(* Goal: and (@Krelation worlds R n' n') (@join worlds J m n n') *)
    - exists mxyz''; split; auto.
(* Goal: @Krelation worlds R n n' *)
      etransitivity; eauto.
Defined.

Lemma UpwardsClosure_increasing:
(* Goal: forall n : worlds, @ex worlds (fun m : worlds => and (@residue worlds R UpwardsClosure_J n m) (@increasing worlds R UpwardsClosure_J m)) *)
  forall m, @increasing _ _ J m <-> @increasing _ _ (UpwardsClosure_J) m.
Proof.
(* Goal: forall x : worlds, @increasing worlds R UpwardsClosure_J x *)
  intros.
(* Goal: forall x : worlds, @increasing worlds R UpwardsClosure_J x *)
  unfold increasing; split; intros.
  + destruct H0 as [n0 [? ?]].
(* Goal: @Krelation worlds R n n' *)
    etransitivity; eauto.
  + apply H.
(* Goal: @join worlds UpwardsClosure_J m1 m2 n *)
    exists n'.
(* Goal: and (@Krelation worlds R n' n') (@join worlds J m n n') *)
    split; auto.
(* Goal: @Krelation worlds R n' n' *)
    reflexivity.
Qed.

Definition UpwardsClosure_UpwardsClosed:
  @UpwardsClosedSeparationAlgebra worlds _ (UpwardsClosure_J).
Proof.
(* Goal: forall x : worlds, @increasing worlds R UpwardsClosure_J x *)
  intros until m2; intros.
(* Goal: @ex worlds (fun n1 : worlds => @ex worlds (fun n2 : worlds => and (@join worlds UpwardsClosure_J n1 n2 n) (and (@Krelation worlds R m1 n1) (@Krelation worlds R m2 n2)))) *)
  exists m1, m2.
(* Goal: and (@join worlds UpwardsClosure_J m1 m2 n) (and (@Krelation worlds R m1 m1) (@Krelation worlds R m2 m2)) *)
  split; [| split]; [| reflexivity | reflexivity].
(* Goal: @join worlds UpwardsClosure_J m1 m2 n *)
  destruct H as [n' [? ?]].
(* Goal: @join worlds UpwardsClosure_J m1 m2 n *)
  exists n'.
(* Goal: @Krelation worlds R n n' *)
  split; auto; etransitivity; eauto.
Defined.

Definition UpwardsClosure_DownwardsClosed:
  @DownwardsClosedSeparationAlgebra worlds _ (UpwardsClosure_J).
Proof.
(* Goal: forall x : worlds, @increasing worlds R UpwardsClosure_J x *)
  intros until n2; intros.
(* Goal: @ex worlds (fun n : worlds => and (@join worlds UpwardsClosure_J n1 n2 n) (@Krelation worlds R n m)) *)
  simpl in *.
(* Goal: @ex worlds (fun n : worlds => and (@join worlds UpwardsClosure_J n1 n2 n) (@Krelation worlds R n m)) *)
  destruct H as [n [? ?]].
(* Goal: @ex worlds (fun n : worlds => and (@join worlds UpwardsClosure_J n1 n2 n) (@Krelation worlds R n m)) *)
  destruct (join_Korder_down _ _ _ _ _ H2 H0 H1) as [n' [? ?]].
(* Goal: and (@Krelation worlds R n' n') (@join worlds J m n n') *)
  exists n; split; auto.
(* Goal: and (@Krelation worlds R n' n') (@join worlds J m n n') *)
  exists n'; split; auto.
Defined.

Definition UpwardsClosure_USA {USA: UnitalSeparationAlgebra worlds}:
  @UnitalSeparationAlgebra worlds _ (UpwardsClosure_J).
Proof.
(* Goal: @IncreasingSeparationAlgebra worlds R UpwardsClosure_J *)
  constructor.
(* Goal: forall x : worlds, @increasing worlds R UpwardsClosure_J x *)
  - intros.
(* Goal: forall x : worlds, @increasing worlds R UpwardsClosure_J x *)
    simpl.
(* Goal: @ex worlds (fun m : worlds => and (@residue worlds R UpwardsClosure_J n m) (@increasing worlds R UpwardsClosure_J m)) *)
    destruct (incr_exists n) as [u [? ?]].
(* Goal: @ex worlds (fun m : worlds => and (@residue worlds R UpwardsClosure_J n m) (@increasing worlds R UpwardsClosure_J m)) *)
    destruct H as [n' [H1 H2]].
(* Goal: and (@Krelation worlds R n' n') (@join worlds J m n n') *)
    exists u; split; auto.
    + exists n'; split; auto.
(* Goal: @Krelation worlds R n' n' *)
      exists n; split; auto; reflexivity.
    + rewrite <- UpwardsClosure_increasing; auto.
Defined.

Definition UpwardsClosure_incrSA {incrSA: IncreasingSeparationAlgebra worlds}:
  @IncreasingSeparationAlgebra worlds _ (UpwardsClosure_J).
Proof.
(* Goal: @IncreasingSeparationAlgebra worlds R UpwardsClosure_J *)
  constructor.
(* Goal: forall x : worlds, @increasing worlds R UpwardsClosure_J x *)
  simpl.
(* Goal: forall x : worlds, @increasing worlds R UpwardsClosure_J x *)
  intros.
(* Goal: forall x : worlds, @increasing worlds R UpwardsClosure_J x *)
  hnf; intros.
(* Goal: @Krelation worlds R n n' *)
  destruct H as [m [? ?]].
(* Goal: @Krelation worlds R n n' *)
  etransitivity; eauto.
(* Goal: @Krelation worlds R n m *)
  eapply all_increasing; eauto.
Qed.

End UpwardsClosure.
