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

Lemma wandQ_frame_refine {A} {ND: NatDed A} {SL: SepLog A}: forall B C (P: B -> A) (f: C -> B),
  allp P |-- allp (fun c => P (f c)).
Proof.
(* Goal: forall (B : Type) (P : forall _ : B, A) (Q : A) (a : B), @eq A (@sepcon A ND SL (P a) (@allp A ND B (fun b : B => @wand A ND SL (P b) (@sepcon A ND SL (P b) Q)))) (@sepcon A ND SL (P a) Q) *)
  intros.
(* Goal: @derives A ND (@allp A ND B P) (@allp A ND C (fun c : C => P (f c))) *)
  apply allp_right; intros c.
(* Goal: @derives A ND (@allp A ND B P) (P (f c)) *)
  apply (allp_left _ (f c)).
(* Goal: @derives A ND (@wand A ND SL (P a) (@sepcon A ND SL (P a) Q)) (@wand A ND SL (P a) (@sepcon A ND SL (P a) Q)) *)
  auto.
Qed.

Lemma wandQ_frame_intro {A} {ND: NatDed A} {SL: SepLog A}: forall B (P: B -> A) (Q: A),
  Q |-- allp (P -* P * (fun _ => Q)).
Proof.
(* Goal: forall (B : Type) (P : forall _ : B, A) (Q : A) (a : B), @eq A (@sepcon A ND SL (P a) (@allp A ND B (fun b : B => @wand A ND SL (P b) (@sepcon A ND SL (P b) Q)))) (@sepcon A ND SL (P a) Q) *)
  intros. simpl.
(* Goal: @derives A ND (@allp A ND B (@wand (forall _ : B, A) (@LiftNatDed B A ND) (@LiftSepLog B A ND SL) P Q)) (@allp A ND B (@wand (forall _ : B, A) (@LiftNatDed B A ND) (@LiftSepLog B A ND SL) (@sepcon (forall _ : B, A) (@LiftNatDed B A ND) (@LiftSepLog B A ND SL) P F) (@sepcon (forall _ : B, A) (@LiftNatDed B A ND) (@LiftSepLog B A ND SL) Q F))) *)
  apply allp_right; intros a.
(* Goal: @derives A ND Q (@wand A ND SL (P a) (@sepcon A ND SL (P a) Q)) *)
  apply wand_frame_intro.
Qed.

Lemma wandQ_frame_intro' {A} {ND: NatDed A} {SL: SepLog A}: forall B (P: B -> A) (Q: A) (R: B -> A),
  (forall x: B, P x * Q |-- R x) ->
  Q |-- allp (P -* R).
Proof.
(* Goal: forall (B : Type) (P : forall _ : B, A) (Q : A) (a : B), @eq A (@sepcon A ND SL (P a) (@allp A ND B (fun b : B => @wand A ND SL (P b) (@sepcon A ND SL (P b) Q)))) (@sepcon A ND SL (P a) Q) *)
  intros. simpl.
(* Goal: @derives A ND (@allp A ND B (@wand (forall _ : B, A) (@LiftNatDed B A ND) (@LiftSepLog B A ND SL) P Q)) (@allp A ND B (@wand (forall _ : B, A) (@LiftNatDed B A ND) (@LiftSepLog B A ND SL) (@sepcon (forall _ : B, A) (@LiftNatDed B A ND) (@LiftSepLog B A ND SL) P F) (@sepcon (forall _ : B, A) (@LiftNatDed B A ND) (@LiftSepLog B A ND SL) Q F))) *)
  apply allp_right; intros a.
(* Goal: @derives A ND Q (@wand A ND SL (P a) (R a)) *)
  apply wand_frame_intro'.
(* Goal: @derives A ND (@sepcon A ND SL (P a) Q) (R a) *)
  apply H.
Qed.

Lemma wandQ_frame_elim {A} {ND: NatDed A} {SL: SepLog A}: forall B (P Q: B -> A) (a: B),
  P a * allp (P -* Q) |-- Q a.
Proof.
(* Goal: forall (B : Type) (P : forall _ : B, A) (Q : A) (a : B), @eq A (@sepcon A ND SL (P a) (@allp A ND B (fun b : B => @wand A ND SL (P b) (@sepcon A ND SL (P b) Q)))) (@sepcon A ND SL (P a) Q) *)
  intros.
(* Goal: @derives A ND (@sepcon A ND SL (P a) (@allp A ND B (fun b : B => @wand A ND SL (P b) (@sepcon A ND SL (P b) Q)))) (@sepcon A ND SL (P a) Q) *)
  rewrite sepcon_comm.
(* Goal: @derives A ND Q (@wand A ND SL (P v) (@sepcon A ND SL (P v) Q)) *)
  apply wand_sepcon_adjoint.
(* Goal: @derives A ND (@wand A ND SL (P a) (@sepcon A ND SL (P a) Q)) (@wand A ND SL (P a) (@sepcon A ND SL (P a) Q)) *)
  apply (allp_left _ a); simpl. auto.
Qed.

Lemma wandQ_frame_ver {A} {ND: NatDed A} {SL: SepLog A}: forall B (P Q R: B -> A),
  allp (P -* Q) * allp (Q -* R) |-- allp (P -* R).
Proof.
(* Goal: forall (B : Type) (P : forall _ : B, A) (Q : A) (a : B), @eq A (@sepcon A ND SL (P a) (@allp A ND B (fun b : B => @wand A ND SL (P b) (@sepcon A ND SL (P b) Q)))) (@sepcon A ND SL (P a) Q) *)
  intros.
(* Goal: @derives A ND (@allp A ND B (@wand (forall _ : B, A) (@LiftNatDed B A ND) (@LiftSepLog B A ND SL) P Q)) (@allp A ND B (@wand (forall _ : B, A) (@LiftNatDed B A ND) (@LiftSepLog B A ND SL) (@sepcon (forall _ : B, A) (@LiftNatDed B A ND) (@LiftSepLog B A ND SL) P F) (@sepcon (forall _ : B, A) (@LiftNatDed B A ND) (@LiftSepLog B A ND SL) Q F))) *)
  apply allp_right; intros a.
(* Goal: @derives A ND (@sepcon A ND SL (@allp A ND B (@wand (forall _ : B, A) (@LiftNatDed B A ND) (@LiftSepLog B A ND SL) P2 Q2)) (@wand (forall _ : B, A) (@LiftNatDed B A ND) (@LiftSepLog B A ND SL) P1 Q1 a)) (@wand (forall _ : B, A) (@LiftNatDed B A ND) (@LiftSepLog B A ND SL) (@sepcon (forall _ : B, A) (@LiftNatDed B A ND) (@LiftSepLog B A ND SL) P1 P2) (@sepcon (forall _ : B, A) (@LiftNatDed B A ND) (@LiftSepLog B A ND SL) Q1 Q2) a) *)
  apply <- wand_sepcon_adjoint.
(* Goal: @derives A ND (@allp A ND B (fun b : B => @wand A ND SL (P b) (@sepcon A ND SL (P b) Q))) (@wand A ND SL (P a) (@sepcon A ND SL (P a) Q)) *)
  apply (allp_left _ a).
(* Goal: @derives A ND (@wand (forall _ : B, A) (@LiftNatDed B A ND) (@LiftSepLog B A ND SL) P2 Q2 a) (@wand A ND SL (@wand (forall _ : B, A) (@LiftNatDed B A ND) (@LiftSepLog B A ND SL) P1 Q1 a) (@wand (forall _ : B, A) (@LiftNatDed B A ND) (@LiftSepLog B A ND SL) (@sepcon (forall _ : B, A) (@LiftNatDed B A ND) (@LiftSepLog B A ND SL) P1 P2) (@sepcon (forall _ : B, A) (@LiftNatDed B A ND) (@LiftSepLog B A ND SL) Q1 Q2) a)) *)
  apply -> wand_sepcon_adjoint.
(* Goal: @derives A ND (@sepcon A ND SL (P a) (@allp A ND B (fun b : B => @wand A ND SL (P b) (@sepcon A ND SL (P b) Q)))) (@sepcon A ND SL (P a) Q) *)
  rewrite sepcon_comm.
(* Goal: @derives A ND (@sepcon A ND SL (@allp A ND B (@wand (forall _ : B, A) (@LiftNatDed B A ND) (@LiftSepLog B A ND SL) P2 Q2)) (@wand (forall _ : B, A) (@LiftNatDed B A ND) (@LiftSepLog B A ND SL) P1 Q1 a)) (@wand (forall _ : B, A) (@LiftNatDed B A ND) (@LiftSepLog B A ND SL) (@sepcon (forall _ : B, A) (@LiftNatDed B A ND) (@LiftSepLog B A ND SL) P1 P2) (@sepcon (forall _ : B, A) (@LiftNatDed B A ND) (@LiftSepLog B A ND SL) Q1 Q2) a) *)
  apply <- wand_sepcon_adjoint.
(* Goal: @derives A ND (@allp A ND B (fun b : B => @wand A ND SL (P b) (@sepcon A ND SL (P b) Q))) (@wand A ND SL (P a) (@sepcon A ND SL (P a) Q)) *)
  apply (allp_left _ a).
(* Goal: @derives A ND (@wand (forall _ : B, A) (@LiftNatDed B A ND) (@LiftSepLog B A ND SL) P2 Q2 a) (@wand A ND SL (@wand (forall _ : B, A) (@LiftNatDed B A ND) (@LiftSepLog B A ND SL) P1 Q1 a) (@wand (forall _ : B, A) (@LiftNatDed B A ND) (@LiftSepLog B A ND SL) (@sepcon (forall _ : B, A) (@LiftNatDed B A ND) (@LiftSepLog B A ND SL) P1 P2) (@sepcon (forall _ : B, A) (@LiftNatDed B A ND) (@LiftSepLog B A ND SL) Q1 Q2) a)) *)
  apply -> wand_sepcon_adjoint.
(* Goal: @derives A ND (@sepcon A ND SL (P a) (@allp A ND B (fun b : B => @wand A ND SL (P b) (@sepcon A ND SL (P b) Q)))) (@sepcon A ND SL (P a) Q) *)
  rewrite sepcon_comm.
(* Goal: @derives A ND (@sepcon A ND SL (@wand (forall _ : B, A) (@LiftNatDed B A ND) (@LiftSepLog B A ND SL) P Q a) (@wand (forall _ : B, A) (@LiftNatDed B A ND) (@LiftSepLog B A ND SL) Q R a)) (@wand (forall _ : B, A) (@LiftNatDed B A ND) (@LiftSepLog B A ND SL) P R a) *)
  apply wand_frame_ver.
Qed.

Lemma wandQ_frame_hor {A} {ND: NatDed A} {SL: SepLog A}: forall B (P1 P2 Q1 Q2: B -> A),
  allp (P1 -* Q1) * allp (P2 -* Q2) |-- allp (P1 * P2 -* Q1 * Q2).
Proof.
(* Goal: forall (B : Type) (P : forall _ : B, A) (Q : A) (a : B), @eq A (@sepcon A ND SL (P a) (@allp A ND B (fun b : B => @wand A ND SL (P b) (@sepcon A ND SL (P b) Q)))) (@sepcon A ND SL (P a) Q) *)
  intros.
(* Goal: @derives A ND (@allp A ND B (@wand (forall _ : B, A) (@LiftNatDed B A ND) (@LiftSepLog B A ND SL) P Q)) (@allp A ND B (@wand (forall _ : B, A) (@LiftNatDed B A ND) (@LiftSepLog B A ND SL) (@sepcon (forall _ : B, A) (@LiftNatDed B A ND) (@LiftSepLog B A ND SL) P F) (@sepcon (forall _ : B, A) (@LiftNatDed B A ND) (@LiftSepLog B A ND SL) Q F))) *)
  apply allp_right; intros a.
(* Goal: @derives A ND (@sepcon A ND SL (@allp A ND B (@wand (forall _ : B, A) (@LiftNatDed B A ND) (@LiftSepLog B A ND SL) P2 Q2)) (@wand (forall _ : B, A) (@LiftNatDed B A ND) (@LiftSepLog B A ND SL) P1 Q1 a)) (@wand (forall _ : B, A) (@LiftNatDed B A ND) (@LiftSepLog B A ND SL) (@sepcon (forall _ : B, A) (@LiftNatDed B A ND) (@LiftSepLog B A ND SL) P1 P2) (@sepcon (forall _ : B, A) (@LiftNatDed B A ND) (@LiftSepLog B A ND SL) Q1 Q2) a) *)
  apply <- wand_sepcon_adjoint.
(* Goal: @derives A ND (@allp A ND B (fun b : B => @wand A ND SL (P b) (@sepcon A ND SL (P b) Q))) (@wand A ND SL (P a) (@sepcon A ND SL (P a) Q)) *)
  apply (allp_left _ a).
(* Goal: @derives A ND (@wand (forall _ : B, A) (@LiftNatDed B A ND) (@LiftSepLog B A ND SL) P2 Q2 a) (@wand A ND SL (@wand (forall _ : B, A) (@LiftNatDed B A ND) (@LiftSepLog B A ND SL) P1 Q1 a) (@wand (forall _ : B, A) (@LiftNatDed B A ND) (@LiftSepLog B A ND SL) (@sepcon (forall _ : B, A) (@LiftNatDed B A ND) (@LiftSepLog B A ND SL) P1 P2) (@sepcon (forall _ : B, A) (@LiftNatDed B A ND) (@LiftSepLog B A ND SL) Q1 Q2) a)) *)
  apply -> wand_sepcon_adjoint.
(* Goal: @derives A ND (@sepcon A ND SL (P a) (@allp A ND B (fun b : B => @wand A ND SL (P b) (@sepcon A ND SL (P b) Q)))) (@sepcon A ND SL (P a) Q) *)
  rewrite sepcon_comm.
(* Goal: @derives A ND (@sepcon A ND SL (@allp A ND B (@wand (forall _ : B, A) (@LiftNatDed B A ND) (@LiftSepLog B A ND SL) P2 Q2)) (@wand (forall _ : B, A) (@LiftNatDed B A ND) (@LiftSepLog B A ND SL) P1 Q1 a)) (@wand (forall _ : B, A) (@LiftNatDed B A ND) (@LiftSepLog B A ND SL) (@sepcon (forall _ : B, A) (@LiftNatDed B A ND) (@LiftSepLog B A ND SL) P1 P2) (@sepcon (forall _ : B, A) (@LiftNatDed B A ND) (@LiftSepLog B A ND SL) Q1 Q2) a) *)
  apply <- wand_sepcon_adjoint.
(* Goal: @derives A ND (@allp A ND B (fun b : B => @wand A ND SL (P b) (@sepcon A ND SL (P b) Q))) (@wand A ND SL (P a) (@sepcon A ND SL (P a) Q)) *)
  apply (allp_left _ a).
(* Goal: @derives A ND (@wand (forall _ : B, A) (@LiftNatDed B A ND) (@LiftSepLog B A ND SL) P2 Q2 a) (@wand A ND SL (@wand (forall _ : B, A) (@LiftNatDed B A ND) (@LiftSepLog B A ND SL) P1 Q1 a) (@wand (forall _ : B, A) (@LiftNatDed B A ND) (@LiftSepLog B A ND SL) (@sepcon (forall _ : B, A) (@LiftNatDed B A ND) (@LiftSepLog B A ND SL) P1 P2) (@sepcon (forall _ : B, A) (@LiftNatDed B A ND) (@LiftSepLog B A ND SL) Q1 Q2) a)) *)
  apply -> wand_sepcon_adjoint.
(* Goal: @derives A ND (@sepcon A ND SL (P a) (@allp A ND B (fun b : B => @wand A ND SL (P b) (@sepcon A ND SL (P b) Q)))) (@sepcon A ND SL (P a) Q) *)
  rewrite sepcon_comm.
(* Goal: @derives A ND (@sepcon A ND SL (@wand (forall _ : B, A) (@LiftNatDed B A ND) (@LiftSepLog B A ND SL) P1 Q1 a) (@wand (forall _ : B, A) (@LiftNatDed B A ND) (@LiftSepLog B A ND SL) P2 Q2 a)) (@wand (forall _ : B, A) (@LiftNatDed B A ND) (@LiftSepLog B A ND SL) (@sepcon (forall _ : B, A) (@LiftNatDed B A ND) (@LiftSepLog B A ND SL) P1 P2) (@sepcon (forall _ : B, A) (@LiftNatDed B A ND) (@LiftSepLog B A ND SL) Q1 Q2) a) *)
  apply wand_frame_hor.
Qed.

Lemma wandQ_frame_frame {A} {ND: NatDed A} {SL: SepLog A}: forall B (P Q F: B -> A),
  allp (P -* Q) |-- allp (P * F -* Q * F).
Proof.
(* Goal: forall (B : Type) (P : forall _ : B, A) (Q : A) (a : B), @eq A (@sepcon A ND SL (P a) (@allp A ND B (fun b : B => @wand A ND SL (P b) (@sepcon A ND SL (P b) Q)))) (@sepcon A ND SL (P a) Q) *)
  intros.
(* Goal: @derives A ND (@allp A ND B (@wand (forall _ : B, A) (@LiftNatDed B A ND) (@LiftSepLog B A ND SL) P Q)) (@allp A ND B (@wand (forall _ : B, A) (@LiftNatDed B A ND) (@LiftSepLog B A ND SL) (@sepcon (forall _ : B, A) (@LiftNatDed B A ND) (@LiftSepLog B A ND SL) P F) (@sepcon (forall _ : B, A) (@LiftNatDed B A ND) (@LiftSepLog B A ND SL) Q F))) *)
  apply allp_right; intros a.
(* Goal: @derives A ND (@allp A ND B (fun b : B => @wand A ND SL (P b) (@sepcon A ND SL (P b) Q))) (@wand A ND SL (P a) (@sepcon A ND SL (P a) Q)) *)
  apply (allp_left _ a).
(* Goal: @derives A ND (@wand (forall _ : B, A) (@LiftNatDed B A ND) (@LiftSepLog B A ND SL) P Q a) (@wand (forall _ : B, A) (@LiftNatDed B A ND) (@LiftSepLog B A ND SL) (@sepcon (forall _ : B, A) (@LiftNatDed B A ND) (@LiftSepLog B A ND SL) P F) (@sepcon (forall _ : B, A) (@LiftNatDed B A ND) (@LiftSepLog B A ND SL) Q F) a) *)
  apply wand_frame_frame.
Qed.

Lemma sepcon_wandQ_eq {A} {ND: NatDed A} {SL: SepLog A}: forall B (P: B -> A) (Q: A) (a: B),
  P a * (ALL b: B, P b -* P b * Q) = P a * Q.
Proof.
(* Goal: forall (B : Type) (P : forall _ : B, A) (Q : A) (a : B), @eq A (@sepcon A ND SL (P a) (@allp A ND B (fun b : B => @wand A ND SL (P b) (@sepcon A ND SL (P b) Q)))) (@sepcon A ND SL (P a) Q) *)
  intros.
(* Goal: @eq A (@sepcon A ND SL (P a) (@allp A ND B (fun b : B => @wand A ND SL (P b) (@sepcon A ND SL (P b) Q)))) (@sepcon A ND SL (P a) Q) *)
  apply pred_ext.
(* Goal: @derives A ND (@sepcon A ND SL (P a) (@allp A ND B (fun b : B => @wand A ND SL (P b) (@sepcon A ND SL (P b) Q)))) (@sepcon A ND SL (P a) Q) *)
  + rewrite sepcon_comm.
(* Goal: @derives A ND Q (@wand A ND SL (P v) (@sepcon A ND SL (P v) Q)) *)
    apply wand_sepcon_adjoint.
(* Goal: @derives A ND (@allp A ND B (fun b : B => @wand A ND SL (P b) (@sepcon A ND SL (P b) Q))) (@wand A ND SL (P a) (@sepcon A ND SL (P a) Q)) *)
    apply (allp_left _ a).
(* Goal: @derives A ND (@wand A ND SL (P a) (@sepcon A ND SL (P a) Q)) (@wand A ND SL (P a) (@sepcon A ND SL (P a) Q)) *)
    auto.
(* Goal: @derives A ND (@wand A ND SL (P a) (@sepcon A ND SL (P a) Q)) (@wand A ND SL (P a) (@sepcon A ND SL (P a) Q)) *)
  + apply sepcon_derives; auto.
(* Goal: forall (B : Type) (P : forall _ : B, A) (Q : A) (a : B), @eq A (@sepcon A ND SL (P a) (@allp A ND B (fun b : B => @wand A ND SL (P b) (@sepcon A ND SL (P b) Q)))) (@sepcon A ND SL (P a) Q) *)
    apply allp_right; intros.
(* Goal: @derives A ND Q (@wand A ND SL (P v) (@sepcon A ND SL (P v) Q)) *)
    apply wand_sepcon_adjoint.
(* Goal: @derives A ND (@wand A ND SL (P a) (@sepcon A ND SL (P a) Q)) (@wand A ND SL (P a) (@sepcon A ND SL (P a) Q)) *)
    rewrite sepcon_comm; auto.
Qed.
