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

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

  (** *Downwards CLosure*)

Definition DownwardsClosure_J: Join worlds.
(* Goal: Join worlds *)
Proof. exact (fun m1 m2 m: worlds => exists n1 n2, m1 <= n1 /\ m2 <= n2 /\ join n1 n2 m).
Defined.

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

Lemma DownwardsClosure_increasing: forall m, @increasing' _ _ J m <-> @increasing _ _ (DownwardsClosure_J) m.
Proof.
(* Goal: forall x : worlds, @increasing worlds R DownwardsClosure_J x *)
  intros.
(* Goal: forall x : worlds, @increasing worlds R DownwardsClosure_J x *)
  unfold increasing', increasing; split; intros.
  + destruct H0 as [m0 [n0 [? [? ?]]]].
(* Goal: @Krelation worlds R n n' *)
    etransitivity; [eassumption |].
(* Goal: @Krelation worlds R n0 n' *)
    eapply H; [| eassumption].
(* Goal: @Krelation worlds R m m0 *)
    auto.
  + apply H.
(* Goal: @join worlds DownwardsClosure_J m n0 n' *)
    exists n, n0.
(* Goal: @Krelation worlds R myz' myz' *)
    split; [| split]; auto; reflexivity.
Qed.

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

Definition DownwardsClosure_UpwardsClosed : @UpwardsClosedSeparationAlgebra worlds _ (DownwardsClosure_J).
Proof.
(* Goal: forall x : worlds, @increasing worlds R DownwardsClosure_J x *)
  intros until m2; intros.
  simpl in *.
(* Goal: @Krelation worlds R n n' *)
  destruct H as [n1 [n2 [? [? ?]]]].
(* Goal: @ex worlds (fun n1 : worlds => @ex worlds (fun n2 : worlds => and (@join worlds DownwardsClosure_J n1 n2 n) (and (@Krelation worlds R m1 n1) (@Krelation worlds R m2 n2)))) *)
  destruct (join_Korder_up _ _ _ _ H2 H0) as [n1' [n2' [? [? ?]]]].
(* Goal: and (@Krelation worlds R m2 n2) (and (@Krelation worlds R m1 n1) (@join worlds J n2 n1 m)) *)
  exists n1, n2; split; [| split]; auto.
(* Goal: and (@Krelation worlds R m2 n2) (and (@Krelation worlds R m1 n1) (@join worlds J n2 n1 m)) *)
  exists n1', n2'; split; [| split]; auto.
Qed.

Definition DownwardsClosure_USA {USA': UnitalSeparationAlgebra' worlds}: @UnitalSeparationAlgebra worlds _ (DownwardsClosure_J).
Proof.
(* Goal: @IncreasingSeparationAlgebra worlds R DownwardsClosure_J *)
  constructor.
(* Goal: forall x : worlds, @increasing worlds R DownwardsClosure_J x *)
  intros.
(* Goal: @ex worlds (fun m : worlds => and (@residue worlds R DownwardsClosure_J n m) (@increasing worlds R DownwardsClosure_J m)) *)
  destruct (incr'_exists n) as [u [? ?]].
(* Goal: @ex worlds (fun m : worlds => and (@residue worlds R DownwardsClosure_J n m) (@increasing worlds R DownwardsClosure_J m)) *)
  destruct H as [n' [H1 H2]].
(* Goal: @Krelation worlds R m m0 *)
  exists u; split; auto.
  + exists n'; split; auto.
(* Goal: @Krelation worlds R myz' myz' *)
    exists u, n'; split; [| split]; auto; reflexivity.
  + rewrite <- DownwardsClosure_increasing; auto.
Defined.

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

End DownwardsClosure.
