Require Import VST.msl.Extensionality.
Require Import VST.msl.seplog.
Require Import VST.msl.sepalg.
Require Import VST.msl.ghost.

Local Open Scope logic.

Class BupdSepLog (A N D: Type) {ND: NatDed A}{SL: SepLog A} := mkBSL {
  bupd: A -> A;
  own: forall {RA: Ghost}, N -> G -> D -> A;
  bupd_intro: forall P, P |-- bupd P;
  bupd_mono: forall P Q, P |-- Q -> bupd P |-- bupd Q;
  bupd_trans: forall P, bupd (bupd P) |-- bupd P;
  bupd_frame_r: forall P Q, bupd P * Q |-- bupd (P * Q);
  own_alloc: forall {RA: Ghost} a pp, valid a ->
    emp |-- bupd (EX g: N, own g a pp);
  own_op: forall {RA: Ghost} g (a1 a2 a3: G) pp, join a1 a2 a3 ->
    own g a3 pp = own g a1 pp * own g a2 pp;
  own_valid_2: forall {RA: Ghost} g (a1 a2: G) pp,
    own g a1 pp * own g a2 pp |-- !!valid_2 a1 a2;
  own_update_ND: forall {RA: Ghost} g (a: G) B pp, fp_update_ND a B ->
    own g a pp |-- bupd (EX b : _, !!(B b) && own g b pp);
  own_dealloc: forall {RA: Ghost} g (a: G) pp,
    own g a pp |-- bupd emp
  }.

Notation "|==> P" := (bupd P) (at level 62): logic.

Lemma bupd_orp_r: forall `{BupdSepLog} (P Q: A), ((|==> P) || Q) |-- |==> P || Q.
Proof.
(* Goal: forall (A N D : Type) (ND : NatDed A) (SL : @SepLog A ND) (H : @BupdSepLog A N D ND SL) (RA : Ghost) (g : N) (a : @G RA) (pp : D), @derives A ND (@own A N D ND SL H RA g a pp) (@prop A ND (@valid RA a)) *)
  intros.
(* Goal: @derives A ND (@orp A ND (@bupd A N D ND SL H P) Q) (@bupd A N D ND SL H (@orp A ND P Q)) *)
  apply orp_left.
  + apply bupd_mono.
(* Goal: @derives A ND P (@orp A ND P Q) *)
    apply orp_right1, derives_refl.
  + eapply derives_trans; [| apply bupd_intro].
(* Goal: @derives A ND Q (@orp A ND P Q) *)
    apply orp_right2, derives_refl.
Qed.

Lemma bupd_orp_l: forall `{BupdSepLog} (P Q: A), (P || |==> Q) |-- |==> P || Q.
Proof.
(* Goal: forall (A N D : Type) (ND : NatDed A) (SL : @SepLog A ND) (H : @BupdSepLog A N D ND SL) (P Q : A), @derives A ND (@orp A ND P (@bupd A N D ND SL H Q)) (@bupd A N D ND SL H (@orp A ND P Q)) *)
  intros; rewrite orp_comm, (orp_comm P Q); apply bupd_orp_r.
Qed.

Lemma bupd_orp: forall `{BupdSepLog} (P Q: A), ((|==> P) || |==> Q) |-- |==> P || Q.
Proof.
(* Goal: forall (A N D : Type) (ND : NatDed A) (SL : @SepLog A ND) (H : @BupdSepLog A N D ND SL) (RA : Ghost) (g : N) (a : @G RA) (pp : D), @derives A ND (@own A N D ND SL H RA g a pp) (@prop A ND (@valid RA a)) *)
  intros.
(* Goal: @derives A ND (@sepcon A ND SL (@bupd A N D ND SL H P) (@bupd A N D ND SL H Q)) (@bupd A N D ND SL H (@sepcon A ND SL P Q)) *)
  eapply derives_trans, bupd_trans.
(* Goal: @derives A ND (@orp A ND (@bupd A N D ND SL H P) (@bupd A N D ND SL H Q)) (@bupd A N D ND SL H (@bupd A N D ND SL H (@orp A ND P Q))) *)
  eapply derives_trans; [apply bupd_orp_l|].
(* Goal: @derives A ND (@bupd A N D ND SL H (@orp A ND (@bupd A N D ND SL H P) Q)) (@bupd A N D ND SL H (@bupd A N D ND SL H (@orp A ND P Q))) *)
  apply bupd_mono, bupd_orp_r.
Qed.

Lemma bupd_frame_l: forall `{BupdSepLog} (P Q: A), (P * |==> Q) |-- |==> P * Q.
Proof.
(* Goal: forall (A N D : Type) (ND : NatDed A) (SL : @SepLog A ND) (H : @BupdSepLog A N D ND SL) (P Q : A), @derives A ND (@sepcon A ND SL P (@bupd A N D ND SL H Q)) (@bupd A N D ND SL H (@sepcon A ND SL P Q)) *)
  intros; rewrite sepcon_comm, (sepcon_comm P Q); apply bupd_frame_r.
Qed.

Lemma bupd_sepcon: forall `{BupdSepLog} (P Q: A), ((|==> P) * |==> Q) |-- |==> P * Q.
Proof.
(* Goal: forall (A N D : Type) (ND : NatDed A) (SL : @SepLog A ND) (H : @BupdSepLog A N D ND SL) (RA : Ghost) (g : N) (a : @G RA) (pp : D), @derives A ND (@own A N D ND SL H RA g a pp) (@prop A ND (@valid RA a)) *)
  intros.
(* Goal: @derives A ND (@sepcon A ND SL (@bupd A N D ND SL H P) (@bupd A N D ND SL H Q)) (@bupd A N D ND SL H (@sepcon A ND SL P Q)) *)
  eapply derives_trans, bupd_trans.
(* Goal: @derives A ND (@sepcon A ND SL (@bupd A N D ND SL H P) (@bupd A N D ND SL H Q)) (@bupd A N D ND SL H (@bupd A N D ND SL H (@sepcon A ND SL P Q))) *)
  eapply derives_trans; [apply bupd_frame_l|].
(* Goal: @derives A ND (@bupd A N D ND SL H (@sepcon A ND SL (@bupd A N D ND SL H P) Q)) (@bupd A N D ND SL H (@bupd A N D ND SL H (@sepcon A ND SL P Q))) *)
  apply bupd_mono, bupd_frame_r.
Qed.

Inductive Singleton {A} (x : A) : A -> Prop :=
| Singleton_I : Singleton x x.

Lemma own_update: forall `{BUPD: BupdSepLog} {RA: Ghost} g (a: G) b pp, fp_update a b ->
    own g a pp |-- |==> (own g b pp).
Proof.
(* Goal: forall (A N D : Type) (ND : NatDed A) (SL : @SepLog A ND) (H : @BupdSepLog A N D ND SL) (RA : Ghost) (g : N) (a : @G RA) (pp : D), @derives A ND (@own A N D ND SL H RA g a pp) (@prop A ND (@valid RA a)) *)
  intros.
(* Goal: @derives A ND (@own A N D ND SL BUPD RA g a pp) (@bupd A N D ND SL BUPD (@own A N D ND SL BUPD RA g b pp)) *)
  eapply derives_trans; [apply own_update_ND with (B := Singleton b)|].
  - intros ? J; destruct (H _ J).
(* Goal: @ex (@G RA) (fun b0 : @G RA => and (@Singleton (@G RA) b b0) (@valid_2 RA b0 c)) *)
    do 2 eexists; [constructor | eauto].
(* Goal: @derives A ND (@bupd A N D ND SL BUPD (@exp A ND (@G RA) (fun b0 : @G RA => @andp A ND (@prop A ND (@Singleton (@G RA) b b0)) (@own A N D ND SL BUPD RA g b0 pp)))) (@bupd A N D ND SL BUPD (@own A N D ND SL BUPD RA g b pp)) *)
  - apply bupd_mono.
(* Goal: @derives A ND (@exp A ND (@G RA) (fun b0 : @G RA => @andp A ND (@prop A ND (@Singleton (@G RA) b b0)) (@own A N D ND SL BUPD RA g b0 pp))) (@own A N D ND SL BUPD RA g b pp) *)
    apply exp_left; intro.
(* Goal: @derives A ND (@andp A ND (@prop A ND (@Singleton (@G RA) b x)) (@own A N D ND SL BUPD RA g x pp)) (@own A N D ND SL BUPD RA g b pp) *)
    rewrite imp_andp_adjoint; apply prop_left; intro X.
(* Goal: @derives A ND (@TT A ND) (@imp A ND (@own A N D ND SL BUPD RA g x pp) (@own A N D ND SL BUPD RA g b pp)) *)
    inversion X; auto.
    rewrite <- imp_andp_adjoint; apply andp_left2, derives_refl.
Qed.

Lemma own_valid: forall `{BupdSepLog} {RA: Ghost} g (a: G) pp,
  own g a pp |-- !!valid a.
Proof.
(* Goal: forall (A N D : Type) (ND : NatDed A) (SL : @SepLog A ND) (H : @BupdSepLog A N D ND SL) (RA : Ghost) (g : N) (a : @G RA) (pp : D), @derives A ND (@own A N D ND SL H RA g a pp) (@prop A ND (@valid RA a)) *)
  intros.
(* Goal: @derives A ND (@own A N D ND SL H RA g a pp) (@prop A ND (@valid RA a)) *)
  erewrite own_op by apply core_unit.
(* Goal: @derives A ND (@sepcon A ND SL (@own A N D ND SL H RA g (@core (@G RA) (let (G, valid, Join_G, _, _, _) as Ghost return (Join (@G Ghost)) := RA in Join_G) (@Sep_G RA) a) pp) (@own A N D ND SL H RA g a pp)) (@prop A ND (@valid RA a)) *)
  eapply derives_trans; [apply own_valid_2|].
(* Goal: @derives A ND (@prop A ND (@valid_2 RA (@core (@G RA) (let (G, valid, Join_G, _, _, _) as Ghost return (Join (@G Ghost)) := RA in Join_G) (@Sep_G RA) a) a)) (@prop A ND (@valid RA a)) *)
  apply prop_left; intros (a' & J & ?); apply prop_right.
(* Goal: @valid RA a *)
  apply core_identity in J; subst; auto.
Qed.

Lemma own_core: forall `{BupdSepLog} {RA: Ghost} g (a: G) pp,
  own g a pp |-- |==> own g (core a) pp.
Proof.
(* Goal: forall (A N D : Type) (ND : NatDed A) (SL : @SepLog A ND) (H : @BupdSepLog A N D ND SL) (RA : Ghost) (g : N) (a : @G RA) (pp : D), @derives A ND (@own A N D ND SL H RA g a pp) (@bupd A N D ND SL H (@own A N D ND SL H RA g (@core (@G RA) (@Join_G RA) (@Sep_G RA) a) pp)) *)
  intros; apply own_update.
(* Goal: @fp_update RA a (@core (@G RA) (@Join_G RA) (@Sep_G RA) a) *)
  intros ? (? & J & ?).
(* Goal: @valid_2 RA (@core (@G RA) (@Join_G RA) (@Sep_G RA) a) c *)
  exists c; split.
  - rewrite (join_core J), <- (join_core (join_comm J)); apply core_unit.
  - eapply join_valid; eauto.
Qed.

Instance LiftBupdSepLog (A B N D: Type) {NB: NatDed B}{SB: SepLog B}{BSLB: BupdSepLog B N D} :
  BupdSepLog (A -> B) N D.
 apply (mkBSL _ _ _ _ _ (fun P rho => |==> P rho) (fun RA g a pp rho => own g a pp));
   repeat intro; simpl.
(* Goal: @derives B NB (P x) (@bupd B N D NB SB BSLB (P x)) *)
(* Goal: @derives B NB (@bupd B N D NB SB BSLB (P x)) (@bupd B N D NB SB BSLB (Q x)) *)
(* Goal: @derives B NB (@bupd B N D NB SB BSLB (@bupd B N D NB SB BSLB (P x))) (@bupd B N D NB SB BSLB (P x)) *)
(* Goal: @derives B NB (@sepcon B NB SB (@bupd B N D NB SB BSLB (P x)) (Q x)) (@bupd B N D NB SB BSLB (@sepcon B NB SB (P x) (Q x))) *)
(* Goal: @derives B NB (@emp B NB SB) (@bupd B N D NB SB BSLB (@exp B NB N (fun x : N => @own B N D NB SB BSLB RA x a pp))) *)
(* Goal: @eq (forall _ : A, B) (fun _ : A => @own B N D NB SB BSLB RA g a3 pp) (fun _ : A => @sepcon B NB SB (@own B N D NB SB BSLB RA g a1 pp) (@own B N D NB SB BSLB RA g a2 pp)) *)
(* Goal: @derives B NB (@sepcon B NB SB (@own B N D NB SB BSLB RA g a1 pp) (@own B N D NB SB BSLB RA g a2 pp)) (@prop B NB (@valid_2 RA a1 a2)) *)
(* Goal: @derives B NB (@own B N D NB SB BSLB RA g a pp) (@bupd B N D NB SB BSLB (@exp B NB (@G RA) (fun x : @G RA => @andp B NB (@prop B NB (B0 x)) (@own B N D NB SB BSLB RA g x pp)))) *)
(* Goal: @derives B NB (@own B N D NB SB BSLB RA g a pp) (@bupd B N D NB SB BSLB (@emp B NB SB)) *)
 apply bupd_intro.
(* Goal: @derives B NB (@bupd B N D NB SB BSLB (P x)) (@bupd B N D NB SB BSLB (Q x)) *)
(* Goal: @derives B NB (@bupd B N D NB SB BSLB (@bupd B N D NB SB BSLB (P x))) (@bupd B N D NB SB BSLB (P x)) *)
(* Goal: @derives B NB (@sepcon B NB SB (@bupd B N D NB SB BSLB (P x)) (Q x)) (@bupd B N D NB SB BSLB (@sepcon B NB SB (P x) (Q x))) *)
(* Goal: @derives B NB (@emp B NB SB) (@bupd B N D NB SB BSLB (@exp B NB N (fun x : N => @own B N D NB SB BSLB RA x a pp))) *)
(* Goal: @eq (forall _ : A, B) (fun _ : A => @own B N D NB SB BSLB RA g a3 pp) (fun _ : A => @sepcon B NB SB (@own B N D NB SB BSLB RA g a1 pp) (@own B N D NB SB BSLB RA g a2 pp)) *)
(* Goal: @derives B NB (@sepcon B NB SB (@own B N D NB SB BSLB RA g a1 pp) (@own B N D NB SB BSLB RA g a2 pp)) (@prop B NB (@valid_2 RA a1 a2)) *)
(* Goal: @derives B NB (@own B N D NB SB BSLB RA g a pp) (@bupd B N D NB SB BSLB (@exp B NB (@G RA) (fun x : @G RA => @andp B NB (@prop B NB (B0 x)) (@own B N D NB SB BSLB RA g x pp)))) *)
(* Goal: @derives B NB (@own B N D NB SB BSLB RA g a pp) (@bupd B N D NB SB BSLB (@emp B NB SB)) *)
 apply bupd_mono; auto.
(* Goal: @derives B NB (@bupd B N D NB SB BSLB (@bupd B N D NB SB BSLB (P x))) (@bupd B N D NB SB BSLB (P x)) *)
(* Goal: @derives B NB (@sepcon B NB SB (@bupd B N D NB SB BSLB (P x)) (Q x)) (@bupd B N D NB SB BSLB (@sepcon B NB SB (P x) (Q x))) *)
(* Goal: @derives B NB (@emp B NB SB) (@bupd B N D NB SB BSLB (@exp B NB N (fun x : N => @own B N D NB SB BSLB RA x a pp))) *)
(* Goal: @eq (forall _ : A, B) (fun _ : A => @own B N D NB SB BSLB RA g a3 pp) (fun _ : A => @sepcon B NB SB (@own B N D NB SB BSLB RA g a1 pp) (@own B N D NB SB BSLB RA g a2 pp)) *)
(* Goal: @derives B NB (@sepcon B NB SB (@own B N D NB SB BSLB RA g a1 pp) (@own B N D NB SB BSLB RA g a2 pp)) (@prop B NB (@valid_2 RA a1 a2)) *)
(* Goal: @derives B NB (@own B N D NB SB BSLB RA g a pp) (@bupd B N D NB SB BSLB (@exp B NB (@G RA) (fun x : @G RA => @andp B NB (@prop B NB (B0 x)) (@own B N D NB SB BSLB RA g x pp)))) *)
(* Goal: @derives B NB (@own B N D NB SB BSLB RA g a pp) (@bupd B N D NB SB BSLB (@emp B NB SB)) *)
 apply bupd_trans.
(* Goal: @derives B NB (@sepcon B NB SB (@bupd B N D NB SB BSLB (P x)) (Q x)) (@bupd B N D NB SB BSLB (@sepcon B NB SB (P x) (Q x))) *)
(* Goal: @derives B NB (@emp B NB SB) (@bupd B N D NB SB BSLB (@exp B NB N (fun x : N => @own B N D NB SB BSLB RA x a pp))) *)
(* Goal: @eq (forall _ : A, B) (fun _ : A => @own B N D NB SB BSLB RA g a3 pp) (fun _ : A => @sepcon B NB SB (@own B N D NB SB BSLB RA g a1 pp) (@own B N D NB SB BSLB RA g a2 pp)) *)
(* Goal: @derives B NB (@sepcon B NB SB (@own B N D NB SB BSLB RA g a1 pp) (@own B N D NB SB BSLB RA g a2 pp)) (@prop B NB (@valid_2 RA a1 a2)) *)
(* Goal: @derives B NB (@own B N D NB SB BSLB RA g a pp) (@bupd B N D NB SB BSLB (@exp B NB (@G RA) (fun x : @G RA => @andp B NB (@prop B NB (B0 x)) (@own B N D NB SB BSLB RA g x pp)))) *)
(* Goal: @derives B NB (@own B N D NB SB BSLB RA g a pp) (@bupd B N D NB SB BSLB (@emp B NB SB)) *)
 apply bupd_frame_r.
(* Goal: @derives B NB (@emp B NB SB) (@bupd B N D NB SB BSLB (@exp B NB N (fun x : N => @own B N D NB SB BSLB RA x a pp))) *)
(* Goal: @eq (forall _ : A, B) (fun _ : A => @own B N D NB SB BSLB RA g a3 pp) (fun _ : A => @sepcon B NB SB (@own B N D NB SB BSLB RA g a1 pp) (@own B N D NB SB BSLB RA g a2 pp)) *)
(* Goal: @derives B NB (@sepcon B NB SB (@own B N D NB SB BSLB RA g a1 pp) (@own B N D NB SB BSLB RA g a2 pp)) (@prop B NB (@valid_2 RA a1 a2)) *)
(* Goal: @derives B NB (@own B N D NB SB BSLB RA g a pp) (@bupd B N D NB SB BSLB (@exp B NB (@G RA) (fun x : @G RA => @andp B NB (@prop B NB (B0 x)) (@own B N D NB SB BSLB RA g x pp)))) *)
(* Goal: @derives B NB (@own B N D NB SB BSLB RA g a pp) (@bupd B N D NB SB BSLB (@emp B NB SB)) *)
 apply own_alloc; auto.
(* Goal: @eq (forall _ : A, B) (fun _ : A => @own B N D NB SB BSLB RA g a3 pp) (fun _ : A => @sepcon B NB SB (@own B N D NB SB BSLB RA g a1 pp) (@own B N D NB SB BSLB RA g a2 pp)) *)
(* Goal: @derives B NB (@sepcon B NB SB (@own B N D NB SB BSLB RA g a1 pp) (@own B N D NB SB BSLB RA g a2 pp)) (@prop B NB (@valid_2 RA a1 a2)) *)
(* Goal: @derives B NB (@own B N D NB SB BSLB RA g a pp) (@bupd B N D NB SB BSLB (@exp B NB (@G RA) (fun x : @G RA => @andp B NB (@prop B NB (B0 x)) (@own B N D NB SB BSLB RA g x pp)))) *)
(* Goal: @derives B NB (@own B N D NB SB BSLB RA g a pp) (@bupd B N D NB SB BSLB (@emp B NB SB)) *)
 extensionality rho; apply own_op; auto.
(* Goal: @derives B NB (@sepcon B NB SB (@own B N D NB SB BSLB RA g a1 pp) (@own B N D NB SB BSLB RA g a2 pp)) (@prop B NB (@valid_2 RA a1 a2)) *)
(* Goal: @derives B NB (@own B N D NB SB BSLB RA g a pp) (@bupd B N D NB SB BSLB (@exp B NB (@G RA) (fun x : @G RA => @andp B NB (@prop B NB (B0 x)) (@own B N D NB SB BSLB RA g x pp)))) *)
(* Goal: @derives B NB (@own B N D NB SB BSLB RA g a pp) (@bupd B N D NB SB BSLB (@emp B NB SB)) *)
 apply own_valid_2.
(* Goal: @derives B NB (@own B N D NB SB BSLB RA g a pp) (@bupd B N D NB SB BSLB (@exp B NB (@G RA) (fun x : @G RA => @andp B NB (@prop B NB (B0 x)) (@own B N D NB SB BSLB RA g x pp)))) *)
(* Goal: @derives B NB (@own B N D NB SB BSLB RA g a pp) (@bupd B N D NB SB BSLB (@emp B NB SB)) *)
 apply own_update_ND; auto.
(* Goal: @derives B NB (@own B N D NB SB BSLB RA g a pp) (@bupd B N D NB SB BSLB (@emp B NB SB)) *)
 apply own_dealloc; auto.
Defined.
