Require Import VST.msl.seplog.
Require Import VST.msl.log_normalize.
Local Open Scope logic.

Lemma wand_frame_intro {A} {ND: NatDed A} {SL: SepLog A}: forall (P Q: A),
  Q |-- P -* P * Q.
Proof.
(* Goal: forall P Q F : A, @derives A ND (@wand A ND SL P Q) (@wand A ND SL (@sepcon A ND SL P F) (@sepcon A ND SL Q F)) *)
  intros.
(* Goal: @derives A ND Q (@wand A ND SL P R) *)
  apply wand_sepcon_adjoint.
(* Goal: @derives A ND (@sepcon A ND SL Q P) R *)
  rewrite sepcon_comm; auto.
Qed.

Lemma wand_frame_intro' {A} {ND: NatDed A} {SL: SepLog A}: forall (P Q R: A),
  P * Q |-- R ->
  Q |-- P -* R.
Proof.
(* Goal: forall P Q F : A, @derives A ND (@wand A ND SL P Q) (@wand A ND SL (@sepcon A ND SL P F) (@sepcon A ND SL Q F)) *)
  intros.
(* Goal: @derives A ND Q (@wand A ND SL P R) *)
  apply wand_sepcon_adjoint.
(* Goal: @derives A ND (@sepcon A ND SL Q P) R *)
  rewrite sepcon_comm; auto.
Qed.

Lemma wand_frame_elim {A} {ND: NatDed A} {SL: SepLog A}: forall (P Q: A),
  P * (P -* Q) |-- Q.
Proof.
(* Goal: forall P Q F : A, @derives A ND (@wand A ND SL P Q) (@wand A ND SL (@sepcon A ND SL P F) (@sepcon A ND SL Q F)) *)
  intros.
(* Goal: @derives A ND (@sepcon A ND SL P (@wand A ND SL P' Q)) Q *)
  rewrite sepcon_comm.
(* Goal: @derives A ND (@sepcon A ND SL (@wand A ND SL P' Q) P) Q *)
  apply wand_sepcon_adjoint; auto.
Qed.

Lemma wand_frame_elim' {A} {ND: NatDed A} {SL: SepLog A}: forall (P P' Q: A),
  P |-- P' -> P * (P' -* Q) |-- Q.
Proof.
(* Goal: forall P Q F : A, @derives A ND (@wand A ND SL P Q) (@wand A ND SL (@sepcon A ND SL P F) (@sepcon A ND SL Q F)) *)
  intros.
(* Goal: @derives A ND (@sepcon A ND SL P (@wand A ND SL P' Q)) Q *)
  rewrite sepcon_comm.
(* Goal: @derives A ND (@sepcon A ND SL (@wand A ND SL P' Q) P) Q *)
  apply wand_sepcon_adjoint; auto.
(* Goal: @derives A ND (@wand A ND SL P' Q) (@wand A ND SL P Q) *)
  apply wand_derives; auto.
Qed.

Lemma wand_frame_ver {A} {ND: NatDed A} {SL: SepLog A}: forall (P Q R: A),
  (P -* Q) * (Q -* R) |-- P -* R.
Proof.
(* Goal: forall P Q F : A, @derives A ND (@wand A ND SL P Q) (@wand A ND SL (@sepcon A ND SL P F) (@sepcon A ND SL Q F)) *)
  intros.
(* Goal: @derives A ND (@wand A ND SL P Q) (@wand A ND SL (@sepcon A ND SL P F) (@sepcon A ND SL Q F)) *)
  apply -> wand_sepcon_adjoint.
  rewrite (sepcon_comm _ P), <- sepcon_assoc.
  eapply derives_trans.
  + eapply sepcon_derives; [apply wand_frame_elim | apply derives_refl].
  + apply wand_frame_elim.
Qed.

Lemma wand_frame_hor {A} {ND: NatDed A} {SL: SepLog A}: forall (P1 P2 Q1 Q2: A),
  (P1 -* Q1) * (P2 -* Q2) |-- P1 * P2 -* Q1 * Q2.
Proof.
(* Goal: forall P Q F : A, @derives A ND (@wand A ND SL P Q) (@wand A ND SL (@sepcon A ND SL P F) (@sepcon A ND SL Q F)) *)
  intros.
(* Goal: @derives A ND (@wand A ND SL P Q) (@wand A ND SL (@sepcon A ND SL P F) (@sepcon A ND SL Q F)) *)
  apply -> wand_sepcon_adjoint.
(* Goal: @derives A ND (@sepcon A ND SL (@sepcon A ND SL (@wand A ND SL P1 Q1) (@wand A ND SL P2 Q2)) (@sepcon A ND SL P1 P2)) (@sepcon A ND SL Q1 Q2) *)
  rewrite <- (sepcon_assoc _ P1), (sepcon_comm _ P1), <- (sepcon_assoc P1), (sepcon_assoc _ _ P2), (sepcon_comm _ P2).
  apply sepcon_derives; apply wand_frame_elim.
Qed.

Lemma wand_frame_frame {A} {ND: NatDed A} {SL: SepLog A}: forall (P Q F: A),
  P -* Q |-- P * F -* Q * F.
Proof.
(* Goal: forall P Q F : A, @derives A ND (@wand A ND SL P Q) (@wand A ND SL (@sepcon A ND SL P F) (@sepcon A ND SL Q F)) *)
  intros.
(* Goal: @derives A ND (@wand A ND SL P Q) (@wand A ND SL (@sepcon A ND SL P F) (@sepcon A ND SL Q F)) *)
  apply -> wand_sepcon_adjoint.
(* Goal: @derives A ND (@sepcon A ND SL (@wand A ND SL P Q) (@sepcon A ND SL P F)) (@sepcon A ND SL Q F) *)
  rewrite <- sepcon_assoc, (sepcon_comm _ P).
(* Goal: @derives A ND (@sepcon A ND SL (@sepcon A ND SL P (@wand A ND SL P Q)) F) (@sepcon A ND SL Q F) *)
  apply sepcon_derives; [apply wand_frame_elim | auto].
Qed.

