Require Import VST.msl.base.
Require Import VST.msl.sepalg.

Require Import Coq.funind.Recdef.
Require Coq.Wellfounded.Wellfounded. (* Can't Import this, because that brings the identifier B into
           scope, which breaks things like `{ageable B}  in this file.
          Stupid feature of Coq, that the B in `{ageable B} is not unambiguously a
        binding occurrence of B.  *)
Delimit Scope pred with pred.
Local Open Scope pred.

Definition pred (A:Type) := A -> Prop.
Bind Scope pred with pred.

Definition derives (A:Type) (P Q:pred A) := forall a:A, P a -> Q a.
Arguments derives [A] _ _.

Lemma pred_ext : forall A (P Q:pred A),
  derives P Q -> derives Q P -> P = Q.
Proof.
(* Goal: forall P Q R : pred T, @derives T (@andp T (@sepcon T JT P Q) (@ewand T JT R (@prop T True))) (@sepcon T JT (@andp T P (@ewand T JT R (@prop T True))) (@andp T Q (@ewand T JT R (@prop T True)))) *)
  intros.
(* Goal: @eq (pred A) P Q *)
  extensionality a.
(* Goal: @eq Prop (and True (Q w)) (Q w) *)
  apply prop_ext; intuition.
Qed.


Lemma derives_cut {A}  : forall Q P R : pred A,
  derives P Q ->
  derives Q R ->
  derives P R.
Proof.
(* Goal: forall (Q P R : pred A) (_ : @derives A P Q) (_ : @derives A Q R), @derives A P R *)
  repeat intro; intuition.
Qed.

Definition prop {A: Type}  (P: Prop) : pred A := (fun _  => P).
Hint Unfold prop.

Definition TT {A}: pred A := prop True.
Definition FF  {A}: pred A := prop False.

Set Implicit Arguments.

Definition imp {A}  (P Q:pred A) :=
   fun a:A => P a -> Q a.
Definition orp {A} (P Q:pred A) :=
   fun a:A => P a \/ Q a.
Definition andp {A} (P Q:pred A) :=
   fun a:A => P a /\ Q a.

Definition allp {A B: Type} (f: B -> pred A) : pred A
  := fun a => forall b, f b a.
Definition exp {A B: Type} (f: B -> pred A) : pred A
  := fun a => exists b, f b a.

Notation "'emp'" := identity.

Definition sepcon {A} {JA: Join A}(p q:pred A) := fun z:A =>
  exists x:A, exists y:A, join x y z /\ p x /\ q y.
Definition wand {A}  {JA: Join A}  (p q:pred A) := fun y =>
  forall x z, join x y z -> p x -> q z.

Notation "P '|--' Q" := (derives P Q) (at level 80, no associativity).
Notation "'EX'  x ':' T ',' P " := (exp (fun x:T => P%pred)) (at level 65, x at level 99) : pred.
Notation "'ALL'  x ':' T  ',' P " := (allp (fun x:T => P%pred)) (at level 65, x at level 99) : pred.
Infix "||" := orp (at level 50, left associativity) : pred.
Infix "&&" := andp (at level 40, left associativity) : pred.
Notation "P '-->' Q" := (imp P Q) (at level 55, right associativity) : pred.
Notation "P '<-->' Q" := (andp (imp P Q) (imp Q P)) (at level 57, no associativity) : pred.
Notation "P '*' Q" := (sepcon P Q) : pred.
Notation "P '-*' Q" := (wand P Q) (at level 60, right associativity) : pred.
Notation "'!!' e" := (prop e) (at level 25) : pred.

Definition precise {A}  {JA: Join A}{PA: Perm_alg A}  (P: pred A) : Prop :=
     forall w w1 w2, P w1 -> P w2 -> join_sub w1 w -> join_sub w2 w -> w1=w2.

Definition precise2  {A} {JA: Join A}{PA: Perm_alg A}  (P: pred A) : Prop :=
     forall Q R, P * (Q && R) = (P * Q) && (P * R).

Lemma precise_eq {A}  {JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A}{CA: Canc_alg A}:
     precise =
                 fun P : pred A => forall Q R, P * (Q && R) = (P * Q) && (P * R).
Proof.
(* Goal: @eq (forall _ : pred A, Prop) (@precise A JA PA) (fun P : pred A => forall Q R : pred A, @eq (forall _ : A, Prop) (@sepcon A JA P (@andp A Q R)) (@andp A (@sepcon A JA P Q) (@sepcon A JA P R))) *)
extensionality P.
(* Goal: @eq Prop (@precise A JA PA P) (forall Q R : pred A, @eq (forall _ : A, Prop) (@sepcon A JA P (@andp A Q R)) (@andp A (@sepcon A JA P Q) (@sepcon A JA P R))) *)
unfold precise.
(* Goal: forall P Q R : pred T, @derives T (@andp T (@sepcon T JT P Q) (@ewand T JT R (@prop T True))) (@sepcon T JT (@andp T P (@ewand T JT R (@prop T True))) (@andp T Q (@ewand T JT R (@prop T True)))) *)
apply prop_ext; split; intros.
(* Goal: @eq (forall _ : A, Prop) (@sepcon A JA (@exp A T P) Q) (@exp A T (fun x : T => @sepcon A JA (P x) Q)) *)
extensionality w.
(* Goal: forall P Q R : pred T, @derives T (@andp T (@sepcon T JT P Q) (@ewand T JT R (@prop T True))) (@sepcon T JT (@andp T P (@ewand T JT R (@prop T True))) (@andp T Q (@ewand T JT R (@prop T True)))) *)
apply prop_ext; split; intros.
(* Goal: @andp A (@sepcon A JA P Q) (@sepcon A JA P R) w *)
(* Goal: @sepcon A JA P (@andp A Q R) w *)
(* Goal: @eq A w1 w2 *)
destruct H0 as [phi1 [phi2 [? [? [? ?]]]]].
(* Goal: @andp A (@sepcon A JA P Q) (@sepcon A JA P R) w *)
(* Goal: @sepcon A JA P (@andp A Q R) w *)
(* Goal: @eq A w1 w2 *)
split; exists phi1; exists phi2; auto.
(* Goal: @sepcon A JA P (@andp A Q R) w *)
(* Goal: @eq A w1 w2 *)
destruct H0 as [[phi1a [phi2a [? [? ?]]]] [phi1b [phi2b [? [? ?]]]]].
(* Goal: @sepcon A JA P (@andp A Q R) w *)
(* Goal: @eq A w1 w2 *)
specialize (H w _ _ H1 H4).
(* Goal: @sepcon A JA P (@andp A Q R) w *)
(* Goal: @eq A w1 w2 *)
spec H.
(* Goal: @joins A JA w2 w1 *)
(* Goal: P w *)
(* Goal: @sepcon A JA P (@identity A JA) w *)
econstructor; eauto.
(* Goal: @sepcon A JA P (@andp A Q R) w *)
(* Goal: @eq A w1 w2 *)
spec H.
(* Goal: @joins A JA w2 w1 *)
(* Goal: P w *)
(* Goal: @sepcon A JA P (@identity A JA) w *)
econstructor; eauto.
(* Goal: @sepcon A JA P (@andp A Q R) w *)
(* Goal: @eq A w1 w2 *)
subst phi1b.
(* Goal: @sepcon A JA P (@andp A Q R) w *)
(* Goal: @eq A w1 w2 *)
generalize (join_canc (join_comm H0) (join_comm H3)).
(* Goal: forall _ : @eq A phi2a phi2b, @sepcon A JA P (@andp A Q R) w *)
(* Goal: @eq A w1 w2 *)
intro; subst phi2b.
(* Goal: @sepcon A JA P (@andp A Q R) w *)
(* Goal: @eq A w1 w2 *)
exists phi1a; exists phi2a; split; auto.
(* Goal: @andp A P Q w *)
(* Goal: @sepcon A JA P Q w *)
split; auto.
(* Goal: @andp A P Q w *)
(* Goal: @sepcon A JA P Q w *)
split; auto.
(* Goal: @eq A w1 w2 *)
rename w1 into w1a.
(* Goal: @eq A w1a w2 *)
rename w2 into w1b.
(* Goal: @eq A w1a w1b *)
destruct H2 as [w2a ?].
(* Goal: @eq A w1a w1b *)
destruct H3 as [w2b ?].
(* Goal: @eq A w1a w1b *)
pose (fa x := x=w2a).
(* Goal: @eq A w1a w1b *)
pose (fb x := x=w2b).
(* Goal: @eq A w1a w1b *)
assert (((P * fa) && (P * fb)) w).
(* Goal: @andp A (@sepcon A JA P fa) (@sepcon A JA P fb) w *)
(* Goal: @eq A w1a w1b *)
split; do 2 econstructor; repeat split; eauto.
(* Goal: @eq A w1a w1b *)
rewrite <- H in H4.
(* Goal: @eq A w1a w1b *)
destruct H4 as [w1 [w2 [? [? [? ?]]]]].
(* Goal: @eq A w1a w1b *)
unfold fa,fb in *.
(* Goal: Q w *)
subst.
(* Goal: @eq A w1a w1b *)
generalize (join_canc H2 H4); intro.
(* Goal: Q w *)
subst.
(* Goal: @eq A w1 w1b *)
eapply join_canc; eauto.
Qed.

Lemma derives_precise {A} {JA: Join A}{PA: Perm_alg A}:
  forall P Q, (P |-- Q) -> precise Q -> precise P.
Proof.
(* Goal: forall (P Q : pred A) (_ : @derives A P Q) (_ : @precise A JA PA Q), @precise A JA PA P *)
intros; intro; intros; eauto.
Qed.

Lemma prop_true_and:
  forall (P: Prop) A (Q: pred A), P -> (!! P && Q = Q).
Proof.
(* Goal: forall P Q R : pred T, @derives T (@andp T (@sepcon T JT P Q) (@ewand T JT R (@prop T True))) (@sepcon T JT (@andp T P (@ewand T JT R (@prop T True))) (@andp T Q (@ewand T JT R (@prop T True)))) *)
intros. unfold prop, andp;
(* Goal: forall (P Q R : pred A) (_ : @derives A P Q) (_ : @derives A P R), @derives A P (@andp A Q R) *)
extensionality w; apply prop_ext; split; intuition.
Qed.

Lemma prop_andp_e {A}:  forall P Q (w:A), (!! P && Q) w -> P /\ Q w.
Proof.
(* Goal: forall (P : Prop) (Q : pred A) (w : A) (_ : @andp A (@prop A P) Q w), and P (Q w) *)
intuition; destruct H; auto.
Qed.

Lemma prop_andp_i {A}:  forall P Q (w:A), P /\ Q w -> (!! P && Q) w.
Proof.
(* Goal: forall (P Q R : pred A) (_ : @derives A P Q) (_ : @derives A P R), @derives A P (@andp A Q R) *)
intuition.
(* Goal: @andp A P Q w *)
(* Goal: @sepcon A JA P Q w *)
split; auto.
Qed.

Lemma derives_trans {A}:  forall (P Q R: pred A), P |-- Q -> Q |-- R -> P |-- R.
Proof.
(* Goal: forall P : pred A, @derives A P P *)
firstorder.
Qed.

Lemma and_i {A}: forall (P Q R: pred A),
    P |-- Q -> P |-- R -> P |-- Q && R.
(* Goal: forall (P Q R : pred A) (_ : @derives A P Q) (_ : @derives A P R), @derives A P (@andp A Q R) *)
Proof. intuition.
(* Goal: @derives A (@exp A B (fun x : B => @wand A JA P (Q x))) (@wand A JA P (@exp A B (fun x : B => Q x))) *)
intros w ?.
(* Goal: @andp A Q R w *)
split; eauto.
Qed.

Lemma andp_derives {A}  :
  forall P Q P' Q': pred A, P |-- P' -> Q |-- Q' -> P && Q |-- P' && Q'.
Proof.
(* Goal: forall P Q R : pred T, @derives T (@andp T (@sepcon T JT P Q) (@ewand T JT R (@prop T True))) (@sepcon T JT (@andp T P (@ewand T JT R (@prop T True))) (@andp T Q (@ewand T JT R (@prop T True)))) *)
intros.
(* Goal: @andp A P Q w *)
(* Goal: @sepcon A JA P Q w *)
intros w [? ?]; split; auto.
Qed.

Lemma sepcon_assoc {A} {JA: Join A}{PA: Perm_alg A}:
  forall p q r, (((p * q) * r) = (p * (q * r))).
Proof.
(* Goal: forall (P Q : pred A) (_ : @pure A JA PA SA P), @eq (forall _ : A, Prop) (@andp A (@sepcon A JA P (@TT A)) Q) (@sepcon A JA P Q) *)
pose proof I.
(* Goal: forall P Q R : pred T, @derives T (@andp T (@sepcon T JT P Q) (@ewand T JT R (@prop T True))) (@sepcon T JT (@andp T P (@ewand T JT R (@prop T True))) (@andp T Q (@ewand T JT R (@prop T True)))) *)
intros.
(* Goal: forall P Q R : pred T, @derives T (@andp T (@sepcon T JT P Q) (@ewand T JT R (@prop T True))) (@sepcon T JT (@andp T P (@ewand T JT R (@prop T True))) (@andp T Q (@ewand T JT R (@prop T True)))) *)
extensionality w; apply prop_ext; split; intros.
(* Goal: @sepcon A JA p (@sepcon A JA q r) w *)
(* Goal: @sepcon A JA (@sepcon A JA p q) r w *)
destruct H0 as [w12 [w3 [? [[w1 [w2 [? [? ?]]]] ?]]]].
(* Goal: @sepcon A JA p (@sepcon A JA q r) w *)
(* Goal: @sepcon A JA (@sepcon A JA p q) r w *)
destruct (join_assoc H1 H0) as [w23 [? ?]].
(* Goal: @andp A P Q w *)
(* Goal: @sepcon A JA P Q w *)
exists w1; exists w23; repeat split; auto.
(* Goal: @andp A P Q w *)
(* Goal: @sepcon A JA P Q w *)
exists w2; exists w3; split; auto.
(* Goal: @sepcon A JA (@sepcon A JA p q) r w *)
destruct H0 as [w1 [w23 [? [? [w2 [w3 [? [? ?]]]]]]]].
(* Goal: @sepcon A JA (@sepcon A JA p q) r w *)
 destruct (join_assoc (join_comm H2) (join_comm H0)) as [w12 [? ?]].
(* Goal: @andp A P Q w *)
(* Goal: @sepcon A JA P Q w *)
exists w12; exists w3; repeat split; auto.
(* Goal: @andp A P Q w *)
(* Goal: @sepcon A JA P Q w *)
exists w1; exists w2; repeat split; auto.
Qed.

Lemma sepcon_comm {A} {JA: Join A}{PA: Perm_alg A}:  forall (P Q: pred A) , P * Q = Q * P.
Proof.
(* Goal: forall P Q R : pred T, @derives T (@andp T (@sepcon T JT P Q) (@ewand T JT R (@prop T True))) (@sepcon T JT (@andp T P (@ewand T JT R (@prop T True))) (@andp T Q (@ewand T JT R (@prop T True)))) *)
intros.
extensionality w; apply prop_ext; split; intros;
(destruct H as [w1 [w2 [? [? ?]]]]; exists w2; exists w1; split ; [apply join_comm; auto | split; auto]).
Qed.

Lemma sepcon_emp {A} {JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A}: forall P, (P * emp) = P.
Proof.
(* Goal: forall P Q R : pred T, @derives T (@andp T (@sepcon T JT P Q) (@ewand T JT R (@prop T True))) (@sepcon T JT (@andp T P (@ewand T JT R (@prop T True))) (@andp T Q (@ewand T JT R (@prop T True)))) *)
intros.
(* Goal: forall P Q R : pred T, @derives T (@andp T (@sepcon T JT P Q) (@ewand T JT R (@prop T True))) (@sepcon T JT (@andp T P (@ewand T JT R (@prop T True))) (@andp T Q (@ewand T JT R (@prop T True)))) *)
extensionality w; apply prop_ext; split; intros.
(* Goal: @ewand A JA (@sepcon A JA P Q) R w *)
destruct H as [w1 [w2 [? [? ?]]]].
(* Goal: P w *)
(* Goal: @sepcon A JA P (@identity A JA) w *)
generalize (identity_unit (a:=w1) H1); intro.
(* Goal: P w *)
(* Goal: @sepcon A JA P (@identity A JA) w *)
spec H2.
(* Goal: @joins A JA w2 w1 *)
(* Goal: P w *)
(* Goal: @sepcon A JA P (@identity A JA) w *)
econstructor; eauto.
(* Goal: P w *)
(* Goal: @sepcon A JA P (@identity A JA) w *)
unfold unit_for in H2.
(* Goal: P w *)
(* Goal: @sepcon A JA P (@identity A JA) w *)
generalize (join_eq H (join_comm H2)).
(* Goal: forall _ : @eq A w w1, P w *)
(* Goal: @sepcon A JA P (@identity A JA) w *)
intros; subst; auto.
(* Goal: @sepcon A JA P (@identity A JA) w *)
destruct (join_ex_identities w) as [e [? ?]].
(* Goal: @andp A P Q w *)
(* Goal: @sepcon A JA P Q w *)
exists w; exists e; repeat split; auto.
(* Goal: @join A JA w e w *)
apply join_comm.
(* Goal: @join A JA e w w *)
apply identity_unit; auto.
Qed.

Lemma emp_sepcon {A} {JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A}:
    forall P, (emp*P) = P.
(* Goal: forall P Q R : pred T, @derives T (@andp T (@sepcon T JT P Q) (@ewand T JT R (@prop T True))) (@sepcon T JT (@andp T P (@ewand T JT R (@prop T True))) (@andp T Q (@ewand T JT R (@prop T True)))) *)
Proof. intros. rewrite sepcon_comm; rewrite sepcon_emp; auto. Qed.

Lemma precise_emp {A} {JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A}:
     precise emp.
Proof.
(* Goal: forall (P Q R : pred A) (_ : @derives A P R), @derives A P (@orp A Q R) *)
repeat intro.
(* Goal: @eq A w1 w2 *)
eapply join_sub_same_identity with (a := w1); eauto.
(* Goal: @unit_for A JA w2 w2 *)
apply identity_unit'; auto.
(* Goal: @unit_for A JA w2 w *)
eapply join_sub_unit_for; eauto.
(* Goal: @unit_for A JA w2 w2 *)
apply identity_unit'; auto.
Qed.

Definition exactly {A} (x: A) : pred A := fun w => w=x.

Lemma join_exactly {A} {JA: Join A}{PA: Perm_alg A}:
  forall w1 w2 w3, join w1 w2 w3 -> exactly w1 * exactly w2 = exactly w3.
Proof.
(* Goal: forall P Q R : pred T, @derives T (@andp T (@sepcon T JT P Q) (@ewand T JT R (@prop T True))) (@sepcon T JT (@andp T P (@ewand T JT R (@prop T True))) (@andp T Q (@ewand T JT R (@prop T True)))) *)
intros.
(* Goal: @eq (forall _ : A, Prop) (@sepcon A JA (@exactly A w1) (@exactly A w2)) (@exactly A w3) *)
unfold exactly.
(* Goal: @eq (forall _ : A, Prop) (@sepcon A JA (@exp A T P) Q) (@exp A T (fun x : T => @sepcon A JA (P x) Q)) *)
extensionality w.
(* Goal: forall P Q R : pred T, @derives T (@andp T (@sepcon T JT P Q) (@ewand T JT R (@prop T True))) (@sepcon T JT (@andp T P (@ewand T JT R (@prop T True))) (@andp T Q (@ewand T JT R (@prop T True)))) *)
apply prop_ext; split; intros.
(* Goal: @eq A w w3 *)
(* Goal: @sepcon A JA (fun w : A => @eq A w w1) (fun w : A => @eq A w w2) w *)
destruct H0 as [? [? [? [? ?]]]].
(* Goal: Q w *)
subst. eapply join_eq; eauto.
(* Goal: @sepcon A JA (fun w : A => @eq A w w1) (fun w : A => @eq A w w2) w *)
subst w3.
(* Goal: @andp A P Q w *)
(* Goal: @sepcon A JA P Q w *)
exists w1; exists w2; split; auto.
Qed.


Lemma exists_and1 {A: Type} : forall {T: Type} (P: T -> pred A) (Q: pred A),
                   exp P && Q = EX x:T, P x && Q.
Proof.
(* Goal: forall P Q R : pred T, @derives T (@andp T (@sepcon T JT P Q) (@ewand T JT R (@prop T True))) (@sepcon T JT (@andp T P (@ewand T JT R (@prop T True))) (@andp T Q (@ewand T JT R (@prop T True)))) *)
intros.
(* Goal: @eq (forall _ : A, Prop) (@sepcon A JA (@exp A T P) Q) (@exp A T (fun x : T => @sepcon A JA (P x) Q)) *)
extensionality w.
(* Goal: forall P Q R : pred T, @derives T (@andp T (@sepcon T JT P Q) (@ewand T JT R (@prop T True))) (@sepcon T JT (@andp T P (@ewand T JT R (@prop T True))) (@andp T Q (@ewand T JT R (@prop T True)))) *)
apply prop_ext; split; intros.
(* Goal: @exp A B (fun x : B => @andp A (p x) q) w *)
(* Goal: @andp A (@exp A B p) q w *)
destruct H as [[x ?] ?].
(* Goal: @andp A P Q w *)
(* Goal: @sepcon A JA P Q w *)
exists x; split; auto.
(* Goal: @andp A (@exp A T P) Q w *)
destruct H as [x [? ?]].
(* Goal: @andp A P Q w *)
(* Goal: @sepcon A JA P Q w *)
split; auto.
(* Goal: @exp A T P w1 *)
exists x; auto.
Qed.

Lemma andp_comm {A: Type}: forall (P Q: pred A), P && Q = Q && P.
Proof.
(* Goal: forall P Q R : pred T, @derives T (@andp T (@sepcon T JT P Q) (@ewand T JT R (@prop T True))) (@sepcon T JT (@andp T P (@ewand T JT R (@prop T True))) (@andp T Q (@ewand T JT R (@prop T True)))) *)
intros.
(* Goal: @eq (forall _ : A, Prop) (@sepcon A JA (@exp A T P) Q) (@exp A T (fun x : T => @sepcon A JA (P x) Q)) *)
extensionality w.
unfold andp;
(* Goal: forall (P Q R : pred A) (_ : @derives A P Q) (_ : @derives A P R), @derives A P (@andp A Q R) *)
apply prop_ext; split; intuition.
Qed.

Lemma andp_assoc {A}: forall (P Q R: pred A),
                 ((P && Q) && R = P && (Q && R)).
Proof.
(* Goal: forall P Q R : pred T, @derives T (@andp T (@sepcon T JT P Q) (@ewand T JT R (@prop T True))) (@sepcon T JT (@andp T P (@ewand T JT R (@prop T True))) (@andp T Q (@ewand T JT R (@prop T True)))) *)
intros.
(* Goal: @eq (forall _ : A, Prop) (@sepcon A JA (@exp A T P) Q) (@exp A T (fun x : T => @sepcon A JA (P x) Q)) *)
extensionality w.
(* Goal: @eq Prop (@andp A (@andp A P Q) R w) (@andp A P (@andp A Q R) w) *)
unfold andp.
(* Goal: @eq Prop (and True (Q w)) (Q w) *)
apply prop_ext; intuition.
Qed.

Lemma True_andp_eq {A}:
  forall (P: Prop) (Q: pred A), P -> (!!P && Q)%pred = Q.
(* Goal: forall P Q R : pred T, @derives T (@andp T (@sepcon T JT P Q) (@ewand T JT R (@prop T True))) (@sepcon T JT (@andp T P (@ewand T JT R (@prop T True))) (@andp T Q (@ewand T JT R (@prop T True)))) *)
intros.
(* Goal: forall (P Q R : pred A) (_ : @derives A P Q) (_ : @derives A P R), @derives A P (@andp A Q R) *)
extensionality w; apply prop_ext; split; unfold prop, andp; simpl; intros; intuition.
Qed.

Lemma TT_i  {A} : forall w: A,  TT w.
Proof.
(* Goal: forall w : A, @TT A w *)
unfold TT, prop; simpl; auto.
Qed.

Hint Resolve @TT_i.

Lemma TT_and {A}: forall (Q: pred A), TT && Q = Q.
(* Goal: @eq (forall _ : A, Prop) (@sepcon A JA (@exp A T P) Q) (@exp A T (fun x : T => @sepcon A JA (P x) Q)) *)
intros; unfold andp,  TT, prop; extensionality w.
(* Goal: @eq Prop (and True (Q w)) (Q w) *)
apply prop_ext; intuition.
Qed.


Lemma andp_TT {A}: forall (P: pred A), P && TT = P.
Proof.
(* Goal: forall P Q R : pred T, @derives T (@andp T (@sepcon T JT P Q) (@ewand T JT R (@prop T True))) (@sepcon T JT (@andp T P (@ewand T JT R (@prop T True))) (@andp T Q (@ewand T JT R (@prop T True)))) *)
intros.
(* Goal: forall P Q R : pred T, @derives T (@andp T (@sepcon T JT P Q) (@ewand T JT R (@prop T True))) (@sepcon T JT (@andp T P (@ewand T JT R (@prop T True))) (@andp T Q (@ewand T JT R (@prop T True)))) *)
extensionality w; apply prop_ext; split; intros.
(* Goal: P w *)
(* Goal: @andp A P (@TT A) w *)
destruct H; auto.
(* Goal: @andp A P Q w *)
(* Goal: @sepcon A JA P Q w *)
split; auto.
Qed.

Lemma emp_wand {A} {JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A}:
    forall P, emp -* P = P.
Proof.
(* Goal: forall P Q R : pred T, @derives T (@andp T (@sepcon T JT P Q) (@ewand T JT R (@prop T True))) (@sepcon T JT (@andp T P (@ewand T JT R (@prop T True))) (@andp T Q (@ewand T JT R (@prop T True)))) *)
intros.
(* Goal: forall P Q R : pred T, @derives T (@andp T (@sepcon T JT P Q) (@ewand T JT R (@prop T True))) (@sepcon T JT (@andp T P (@ewand T JT R (@prop T True))) (@andp T Q (@ewand T JT R (@prop T True)))) *)
extensionality w; apply prop_ext; split; intros.
(* Goal: @ewand A JA (@identity A JA) P w *)
destruct (join_ex_identities w) as [e [He [? Hj]]].
(* Goal: q w *)
eapply H; eauto.
(* Goal: @join A JA e w w *)
specialize (He _ _ Hj); subst; auto.
(* Goal: forall P Q R : pred T, @derives T (@andp T (@sepcon T JT P Q) (@ewand T JT R (@prop T True))) (@sepcon T JT (@andp T P (@ewand T JT R (@prop T True))) (@andp T Q (@ewand T JT R (@prop T True)))) *)
intro; intros.
(* Goal: P z *)
replace z with w; auto.
Qed.

Lemma wand_derives {A} {JA: Join A}{PA: Perm_alg A}:
  forall P P' Q Q',  P' |-- P -> Q |-- Q' -> P -* Q |-- P' -* Q'.
Proof.
(* Goal: forall P Q R : pred T, @derives T (@andp T (@sepcon T JT P Q) (@ewand T JT R (@prop T True))) (@sepcon T JT (@andp T P (@ewand T JT R (@prop T True))) (@andp T Q (@ewand T JT R (@prop T True)))) *)
intros.
(* Goal: @derives A (@exp A B (fun x : B => @wand A JA P (Q x))) (@wand A JA P (@exp A B (fun x : B => Q x))) *)
intros w ?.
(* Goal: forall P Q R : pred T, @derives T (@andp T (@sepcon T JT P Q) (@ewand T JT R (@prop T True))) (@sepcon T JT (@andp T P (@ewand T JT R (@prop T True))) (@andp T Q (@ewand T JT R (@prop T True)))) *)
intro; intros.
(* Goal: Q' z *)
eauto.
Qed.

Lemma TT_sepcon_TT {A} {JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A}: TT * TT = TT.
Proof.
(* Goal: forall P Q R : pred T, @derives T (@andp T (@sepcon T JT P Q) (@ewand T JT R (@prop T True))) (@sepcon T JT (@andp T P (@ewand T JT R (@prop T True))) (@andp T Q (@ewand T JT R (@prop T True)))) *)
intros.
(* Goal: @eq (forall _ : A, Prop) (@sepcon A JA (@TT A) (@TT A)) (@TT A) *)
extensionality w; apply prop_ext; split; intros; auto.
(* Goal: @sepcon A JA (@TT A) (@TT A) w *)
destruct (join_ex_units w).
(* Goal: @andp A P Q w *)
(* Goal: @sepcon A JA P Q w *)
exists x; exists w; split; auto.
Qed.

Definition ewand {A} {JA: Join A} (P Q: pred A) : pred A :=
  fun w => exists w1, exists w2, join w1 w w2 /\ P w1 /\ Q w2.

(* Notation "P '-o' Q" := (ewand P Q) (at level 60, right associativity). *)

Lemma emp_ewand {A} {JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A}:  forall P, ewand emp P = P.
Proof.
(* Goal: forall P Q R : pred T, @derives T (@andp T (@sepcon T JT P Q) (@ewand T JT R (@prop T True))) (@sepcon T JT (@andp T P (@ewand T JT R (@prop T True))) (@andp T Q (@ewand T JT R (@prop T True)))) *)
intros.
(* Goal: forall P Q R : pred T, @derives T (@andp T (@sepcon T JT P Q) (@ewand T JT R (@prop T True))) (@sepcon T JT (@andp T P (@ewand T JT R (@prop T True))) (@andp T Q (@ewand T JT R (@prop T True)))) *)
extensionality w; apply prop_ext; split; intros.
(* Goal: @ewand A JA (@sepcon A JA P Q) R w *)
destruct H as [w1 [w2 [? [? ?]]]].
(* Goal: P w *)
(* Goal: @ewand A JA (@identity A JA) P w *)
replace w with w2; auto.
(* Goal: @eq A w3 w *)
eapply join_eq; eauto.
(* Goal: Q' z *)
eapply identity_unit; eauto.
(* Goal: @ewand A JA (@identity A JA) P w *)
destruct (join_ex_identities w) as [e [He [? Hj]]].
(* Goal: @ewand A JA (@identity A JA) P w *)
exists e; exists w.
(* Goal: @andp A P Q w *)
(* Goal: @sepcon A JA P Q w *)
split; auto.
(* Goal: @join A JA e w w *)
specialize (He _ _ Hj); subst; auto.
Qed.


Lemma exists_sepcon1 {A} {JA: Join A}{PA: Perm_alg A}:
  forall T (P: T ->  pred A) Q,  exp P * Q = exp (fun x => P x * Q).
Proof.
(* Goal: forall P Q R : pred T, @derives T (@andp T (@sepcon T JT P Q) (@ewand T JT R (@prop T True))) (@sepcon T JT (@andp T P (@ewand T JT R (@prop T True))) (@andp T Q (@ewand T JT R (@prop T True)))) *)
intros.
(* Goal: @eq (forall _ : A, Prop) (@sepcon A JA (@exp A T P) Q) (@exp A T (fun x : T => @sepcon A JA (P x) Q)) *)
extensionality w.
(* Goal: forall P Q R : pred T, @derives T (@andp T (@sepcon T JT P Q) (@ewand T JT R (@prop T True))) (@sepcon T JT (@andp T P (@ewand T JT R (@prop T True))) (@andp T Q (@ewand T JT R (@prop T True)))) *)
apply prop_ext; split; intros.
(* Goal: @exp A T (fun x : T => @sepcon A JA (P x) Q) a *)
(* Goal: @sepcon A JA (@exp A T P) Q a *)
destruct H as [w1 [w2 [? [[x ?] ?]]]].
(* Goal: @andp A P Q w *)
(* Goal: @sepcon A JA P Q w *)
exists x; exists w1; exists w2; split; auto.
(* Goal: @sepcon A JA (@exp A T P) Q a *)
destruct H as [x [w1 [w2 [? [? ?]]]]].
(* Goal: @andp A P Q w *)
(* Goal: @sepcon A JA P Q w *)
exists w1; exists w2; split; auto.
(* Goal: @andp A P Q w *)
(* Goal: @sepcon A JA P Q w *)
split; auto.
(* Goal: @exp A T P w1 *)
exists x; auto.
Qed.

Lemma derives_refl {A: Type}:
  forall (P: pred A), (P |-- P).
(* Goal: forall P : pred A, @derives A P P *)
Proof. firstorder.
Qed.

Hint Resolve @derives_refl.

Lemma derives_TT {A}: forall (P: pred A), P |-- TT.
Proof.
(* Goal: forall P Q R : pred T, @derives T (@andp T (@sepcon T JT P Q) (@ewand T JT R (@prop T True))) (@sepcon T JT (@andp T P (@ewand T JT R (@prop T True))) (@andp T Q (@ewand T JT R (@prop T True)))) *)
intros.
(* Goal: @derives A P (@TT A) *)
intros ? ?; auto.
Qed.
Hint Resolve @derives_TT.

Lemma sepcon_derives {A} {JA: Join A}{PA: Perm_alg A}:
  forall p q p' q', (p |-- p') -> (q |-- q') -> (p * q |-- p' * q').
Proof.
(* Goal: forall P Q R : pred T, @derives T (@andp T (@sepcon T JT P Q) (@ewand T JT R (@prop T True))) (@sepcon T JT (@andp T P (@ewand T JT R (@prop T True))) (@andp T Q (@ewand T JT R (@prop T True)))) *)
intros.
(* Goal: @derives A (@sepcon A JA p q) (@sepcon A JA p' q') *)
do 2 intro.
(* Goal: @sepcon A JA P Q w *)
(* Goal: @derives A (@sepcon A JA P Q) (@andp A (@sepcon A JA P (@TT A)) Q) *)
destruct H1 as [w1 [w2 [? [? ?]]]].
(* Goal: @sepcon T JT (@andp T P (@ewand T JT R (@prop T True))) (@andp T Q (@ewand T JT R (@prop T True))) w *)
exists w1; exists w2; repeat split ;auto.
Qed.

Lemma derives_e {A: Type}: forall p q (st: A),
      (p |-- q) -> p st -> q st.
Proof.
(* Goal: p a *)
auto.
Qed.

Lemma exp_derives {A} :
       forall B (P: B -> pred A) Q , (forall x:B, P x |-- Q x) -> (exp P |-- exp Q).
Proof.
(* Goal: forall P Q R : pred T, @derives T (@andp T (@sepcon T JT P Q) (@ewand T JT R (@prop T True))) (@sepcon T JT (@andp T P (@ewand T JT R (@prop T True))) (@andp T Q (@ewand T JT R (@prop T True)))) *)
intros.
(* Goal: @derives A (@exp A B P) (@exp A B Q) *)
intros w [b ?].
(* Goal: q w *)
exists b; eapply H; eauto.
Qed.


Lemma unmodus_wand {A}  {JA: Join A}{PA: Perm_alg A}:
 forall P Q R, Q = P * R ->  Q |-- P * (P -* Q).
Proof.
(* Goal: forall P Q R : pred T, @derives T (@andp T (@sepcon T JT P Q) (@ewand T JT R (@prop T True))) (@sepcon T JT (@andp T P (@ewand T JT R (@prop T True))) (@andp T Q (@ewand T JT R (@prop T True)))) *)
intros.
(* Goal: Q w *)
subst.
(* Goal: p a *)
apply sepcon_derives; auto.
(* Goal: forall P Q R : pred T, @derives T (@andp T (@sepcon T JT P Q) (@ewand T JT R (@prop T True))) (@sepcon T JT (@andp T P (@ewand T JT R (@prop T True))) (@andp T Q (@ewand T JT R (@prop T True)))) *)
intros ?w ?; intro; intros.
(* Goal: @andp A P Q w *)
(* Goal: @sepcon A JA P Q w *)
exists x; exists w; split; auto.
Qed.

Definition superprecise {A}  {JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A} (P: pred A) :=
   forall w1 w2, P w1 -> P w2 -> comparable w1 w2 -> w1=w2.

Lemma modus_ewand {A}  {JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A} :  forall P Q, superprecise P -> P * (ewand P Q) |-- Q.
Proof.
(* Goal: forall (P Q : pred A) (_ : @pure A JA PA SA P), @eq (forall _ : A, Prop) (@andp A (@sepcon A JA P (@TT A)) Q) (@sepcon A JA P Q) *)
pose proof I.
(* Goal: forall P Q R : pred T, @derives T (@andp T (@sepcon T JT P Q) (@ewand T JT R (@prop T True))) (@sepcon T JT (@andp T P (@ewand T JT R (@prop T True))) (@andp T Q (@ewand T JT R (@prop T True)))) *)
intros.
(* Goal: @derives A (@exp A B (fun x : B => @wand A JA P (Q x))) (@wand A JA P (@exp A B (fun x : B => Q x))) *)
intros w ?.
(* Goal: @sepcon A JA P Q w *)
(* Goal: @derives A (@sepcon A JA P Q) (@andp A (@sepcon A JA P (@TT A)) Q) *)
destruct H1 as [w1 [w2 [? [? ?]]]].
(* Goal: Q w *)
unfold ewand in H3.
(* Goal: Q w *)
destruct H3 as [w1' [w3 [? [? ?]]]].
(* Goal: Q w *)
assert (w1'=w1).
(* Goal: p a *)
  apply H0; auto.
(* Goal: Q' z *)
  apply comparable_trans with w2. eapply join_comparable2; eauto.
(* Goal: Q' z *)
  apply comparable_sym.  eapply join_comparable2; eauto.
(* Goal: Q w *)
  subst.
(* Goal: p a *)
replace w with w3; auto.
(* Goal: @eq A w3 w *)
eapply join_eq; eauto.
Qed.

Lemma exists_expand_sepcon {A}  {JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A}:
 forall B (p: B -> pred A) q, (exp p * q)%pred = (exp (fun x => p x * q))%pred.
Proof.
(* Goal: forall P Q R : pred T, @derives T (@andp T (@sepcon T JT P Q) (@ewand T JT R (@prop T True))) (@sepcon T JT (@andp T P (@ewand T JT R (@prop T True))) (@andp T Q (@ewand T JT R (@prop T True)))) *)
intros; extensionality w; apply prop_ext; split; intros.
(* Goal: @exp A B (fun x : B => @sepcon A JA p (q x)) w *)
(* Goal: @sepcon A JA p (@exp A B q) w *)
destruct H as [? [? [? [? ?]]]].
(* Goal: R a *)
destruct H0.
(* Goal: @andp A P Q w *)
(* Goal: @sepcon A JA P Q w *)
exists x1; exists x; exists x0; split; auto.
(* Goal: @sepcon A JA p (@exp A B q) w *)
destruct H as [? [? [? [? [? ?]]]]].
(* Goal: @andp A P Q w *)
(* Goal: @sepcon A JA P Q w *)
exists x0; exists x1; split; auto.
(* Goal: @andp A P Q w *)
(* Goal: @sepcon A JA P Q w *)
split; auto.
(* Goal: @exp A T P w1 *)
exists x; auto.
Qed.

Lemma exists_expand_sepcon' {A}  {JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A}:
 forall B p (q: B -> pred A), (p * exp q)%pred = (exp (fun x => p * q x))%pred.
Proof.
(* Goal: forall P Q R : pred T, @derives T (@andp T (@sepcon T JT P Q) (@ewand T JT R (@prop T True))) (@sepcon T JT (@andp T P (@ewand T JT R (@prop T True))) (@andp T Q (@ewand T JT R (@prop T True)))) *)
intros; extensionality w; apply prop_ext; split; intros.
(* Goal: @exp A B (fun x : B => @sepcon A JA p (q x)) w *)
(* Goal: @sepcon A JA p (@exp A B q) w *)
destruct H as [? [? [? [? ?]]]].
(* Goal: @sepcon A JA P Q w *)
destruct H1.
(* Goal: @andp A P Q w *)
(* Goal: @sepcon A JA P Q w *)
exists x1; exists x; exists x0; split; auto.
(* Goal: @sepcon A JA p (@exp A B q) w *)
destruct H as [? [? [? [? [? ?]]]]].
(* Goal: @andp A P Q w *)
(* Goal: @sepcon A JA P Q w *)
exists x0; exists x1; split; auto.
(* Goal: @andp A P Q w *)
(* Goal: @sepcon A JA P Q w *)
split; auto.
(* Goal: @exp A T P w1 *)
exists x; auto.
Qed.

Lemma exists_expand_and {A}  {JA: Join A}:
 forall B (p: B -> pred A) q, (exp p && q)%pred = (exp (fun x => p x && q))%pred.
Proof.
(* Goal: forall P Q R : pred T, @derives T (@andp T (@sepcon T JT P Q) (@ewand T JT R (@prop T True))) (@sepcon T JT (@andp T P (@ewand T JT R (@prop T True))) (@andp T Q (@ewand T JT R (@prop T True)))) *)
intros; extensionality w; apply prop_ext; split; intros.
(* Goal: @sepcon A JA P (@andp A (@prop A Q) R) w *)
destruct H.
(* Goal: @sepcon A JA P (@andp A (@prop A Q) R) w *)
destruct H.
(* Goal: @andp A P Q w *)
(* Goal: @sepcon A JA P Q w *)
exists x; split; auto.
(* Goal: @sepcon A JA P (@andp A (@prop A Q) R) w *)
destruct H. destruct H.
(* Goal: @andp A P Q w *)
(* Goal: @sepcon A JA P Q w *)
split; auto.
(* Goal: @exp A T P w1 *)
exists x; auto.
Qed.

Lemma exists_expand_and' {A} {JA: Join A}:
 forall B p (q: B -> pred A), (p && exp q)%pred = (exp (fun x => p && q x))%pred.
Proof.
(* Goal: forall P Q R : pred T, @derives T (@andp T (@sepcon T JT P Q) (@ewand T JT R (@prop T True))) (@sepcon T JT (@andp T P (@ewand T JT R (@prop T True))) (@andp T Q (@ewand T JT R (@prop T True)))) *)
intros; extensionality w; apply prop_ext; split; intros.
(* Goal: @sepcon A JA P (@andp A (@prop A Q) R) w *)
destruct H.
(* Goal: R a *)
destruct H0.
(* Goal: @andp A P Q w *)
(* Goal: @sepcon A JA P Q w *)
exists x; split; auto.
(* Goal: @sepcon A JA P (@andp A (@prop A Q) R) w *)
destruct H. destruct H.
(* Goal: @andp A P Q w *)
(* Goal: @sepcon A JA P Q w *)
split; auto.
(* Goal: @exp A T P w1 *)
exists x; auto.
Qed.

Lemma allp_derives_right {A} : forall B p (q: B -> pred A),
  ((p |-- allp q) <-> (forall x, p |-- q x)).
Proof.
(* Goal: forall P Q R : pred T, @derives T (@andp T (@sepcon T JT P Q) (@ewand T JT R (@prop T True))) (@sepcon T JT (@andp T P (@ewand T JT R (@prop T True))) (@andp T Q (@ewand T JT R (@prop T True)))) *)
intros.
(* Goal: forall P Q R : pred T, @derives T (@andp T (@sepcon T JT P Q) (@ewand T JT R (@prop T True))) (@sepcon T JT (@andp T P (@ewand T JT R (@prop T True))) (@andp T Q (@ewand T JT R (@prop T True)))) *)
split; intros.
(* Goal: Q' z *)
eapply derives_trans; eauto.
(* Goal: @derives A (@allp A B P) Q *)
intros ? ?. apply H0.
(* Goal: @derives A p (@allp A B q) *)
intros ? ? ?.
(* Goal: q b a *)
eapply (H b).
(* Goal: p a *)
auto.
Qed.

Lemma wand_exists {A} {JA: Join A}{PA: Perm_alg A}:
   forall B P Q,  (EX x: B, P -* Q x) |-- (P -* EX x : B, Q x).
Proof.
(* Goal: forall (P Q : pred A) (_ : @pure A JA PA SA P), @eq (forall _ : A, Prop) (@andp A (@sepcon A JA P (@TT A)) Q) (@sepcon A JA P Q) *)
pose proof I.
(* Goal: forall P Q R : pred T, @derives T (@andp T (@sepcon T JT P Q) (@ewand T JT R (@prop T True))) (@sepcon T JT (@andp T P (@ewand T JT R (@prop T True))) (@andp T Q (@ewand T JT R (@prop T True)))) *)
intros.
(* Goal: @derives A (@exp A B (fun x : B => @wand A JA P (Q x))) (@wand A JA P (@exp A B (fun x : B => Q x))) *)
intros w ?.
(* Goal: @wand A JA P (@exp A B (fun x : B => Q x)) w *)
destruct H0 as [x ?].
(* Goal: @wand A JA P (@exp A B (fun x : B => Q x)) w *)
intros ?w ?w ? ?.
(* Goal: @exp A B (fun x : B => Q x) w1 *)
specialize ( H0 w0 w1 H1 H2).
(* Goal: @exp A T P w1 *)
exists x; auto.
Qed.

Lemma modus_wand {A} {JA: Join A}{PA: Perm_alg A}:
  forall P Q,  P * (P -* Q) |-- Q.
Proof.
(* Goal: forall P Q R : pred T, @derives T (@andp T (@sepcon T JT P Q) (@ewand T JT R (@prop T True))) (@sepcon T JT (@andp T P (@ewand T JT R (@prop T True))) (@andp T Q (@ewand T JT R (@prop T True)))) *)
intros.
intros w  [?w [?w [? [? ?]]]].
(* Goal: Q' z *)
eapply H1; eauto.
Qed.

Lemma distrib_sepcon_andp {A} {JA: Join A}{PA: Perm_alg A}:
  forall P Q R, P * (Q && R) |-- (P * Q) && (P * R).
Proof.
(* Goal: forall P Q R : pred T, @derives T (@andp T (@sepcon T JT P Q) (@ewand T JT R (@prop T True))) (@sepcon T JT (@andp T P (@ewand T JT R (@prop T True))) (@andp T Q (@ewand T JT R (@prop T True)))) *)
intros. intros w [w1 [w2 [? [? ?]]]].
(* Goal: @sepcon A JA P Q w *)
destruct H1.
(* Goal: @andp A P Q w *)
(* Goal: @sepcon A JA P Q w *)
split; exists w1; exists w2; split; auto.
Qed.

Lemma andp_r {A: Type} : forall (P Q R: pred A), P |-- Q -> P |-- R -> P |-- Q && R.
Proof.
(* Goal: forall P Q R : pred T, @derives T (@andp T (@sepcon T JT P Q) (@ewand T JT R (@prop T True))) (@sepcon T JT (@andp T P (@ewand T JT R (@prop T True))) (@andp T Q (@ewand T JT R (@prop T True)))) *)
intros.
(* Goal: @andp A P Q w *)
(* Goal: @sepcon A JA P Q w *)
intros w ?; split; auto.
Qed.

Definition list_sepcon {A} {JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A} : list (pred A) -> pred A := fold_right sepcon emp.

Lemma sepcon_andp_prop {A} {JA: Join A}{PA: Perm_alg A}: forall P Q R, P * (!!Q && R) = !!Q && (P * R).
Proof.
(* Goal: forall P Q R : pred T, @derives T (@andp T (@sepcon T JT P Q) (@ewand T JT R (@prop T True))) (@sepcon T JT (@andp T P (@ewand T JT R (@prop T True))) (@andp T Q (@ewand T JT R (@prop T True)))) *)
intros.
(* Goal: forall P Q R : pred T, @derives T (@andp T (@sepcon T JT P Q) (@ewand T JT R (@prop T True))) (@sepcon T JT (@andp T P (@ewand T JT R (@prop T True))) (@andp T Q (@ewand T JT R (@prop T True)))) *)
extensionality w; apply prop_ext; split; intros.
(* Goal: @andp A (@prop A Q) (@sepcon A JA P R) w *)
(* Goal: @sepcon A JA P (@andp A (@prop A Q) R) w *)
destruct H as [w1 [w2 [? [? [? ?]]]]].
(* Goal: @andp A (@prop A Q) (@sepcon A JA P R) w *)
(* Goal: @sepcon A JA P (@andp A (@prop A Q) R) w *)
split. apply H1.
(* Goal: p a *)
exists w1; exists w2; split; [|split]; auto.
(* Goal: @sepcon A JA P (@andp A (@prop A Q) R) w *)
destruct H.
(* Goal: @sepcon A JA P (@andp A (@prop A Q) R) w *)
destruct H0 as [w1 [w2 [? [? ?]]]].
(* Goal: @andp A P Q w *)
(* Goal: @sepcon A JA P Q w *)
exists w1; exists w2; repeat split; auto.
Qed.

(* Goal: @andp A (@prop A Q) (@sepcon A JA P R) w *)
(* Goal: @sepcon A JA P (@andp A (@prop A Q) R) w *)
Require Import VST.msl.cross_split.

Lemma exactly_i {A} : forall x: A, exactly x x.
(* Goal: forall P Q R : pred T, @derives T (@andp T (@sepcon T JT P Q) (@ewand T JT R (@prop T True))) (@sepcon T JT (@andp T P (@ewand T JT R (@prop T True))) (@andp T Q (@ewand T JT R (@prop T True)))) *)
Proof. intros. reflexivity.
Qed.
Hint Resolve @exactly_i.

Lemma superprecise_exactly {A} {JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A}: forall x, superprecise (exactly x).
Proof.
(* Goal: forall P Q R : pred T, @derives T (@andp T (@sepcon T JT P Q) (@ewand T JT R (@prop T True))) (@sepcon T JT (@andp T P (@ewand T JT R (@prop T True))) (@andp T Q (@ewand T JT R (@prop T True)))) *)
unfold exactly, superprecise; intros.
(* Goal: p a *)
subst; auto.
Qed.
Hint Resolve @superprecise_exactly.

Lemma find_overlap {A} {JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A}:
     Cross_alg A ->
     forall S P Q R, (S * P) && (Q * R) |--
                          EX SQ:_, EX SR:_, EX PQ:_, EX PR:_,
                            (((SQ* SR) && S)*((PQ* PR) && P)) &&
                            (((SQ* PQ) && Q)*((SR* PR) && R)) &&
                            !! (superprecise SQ /\ superprecise SR /\ superprecise PQ /\ superprecise PR).
Proof.
(* Goal: forall (P Q : pred A) (_ : @pure A JA PA SA P), @eq (forall _ : A, Prop) (@andp A (@sepcon A JA P (@TT A)) Q) (@sepcon A JA P Q) *)
pose proof I.
(* Goal: forall P Q R : pred T, @derives T (@andp T (@sepcon T JT P Q) (@ewand T JT R (@prop T True))) (@sepcon T JT (@andp T P (@ewand T JT R (@prop T True))) (@andp T Q (@ewand T JT R (@prop T True)))) *)
intros.
(* Goal: @derives T (@andp T (@sepcon T JT P Q) (@ewand T JT R (@prop T True))) (@sepcon T JT (@andp T P (@ewand T JT R (@prop T True))) (@andp T Q (@ewand T JT R (@prop T True)))) *)
intros w [[w1 [w2 [? [? ?]]]] [w3 [w4 [? [? ?]]]]].
(* Goal: @exp A (pred A) (fun SQ : pred A => @exp A (pred A) (fun SR : pred A => @exp A (pred A) (fun PQ : pred A => @exp A (pred A) (fun PR : pred A => @andp A (@andp A (@sepcon A JA (@andp A (@sepcon A JA SQ SR) S) (@andp A (@sepcon A JA PQ PR) P)) (@sepcon A JA (@andp A (@sepcon A JA SQ PQ) Q) (@andp A (@sepcon A JA SR PR) R))) (@prop A (and (@superprecise A JA PA SA SQ) (and (@superprecise A JA PA SA SR) (and (@superprecise A JA PA SA PQ) (@superprecise A JA PA SA PR))))))))) w *)
destruct (X _ _ _ _ _ H0 H3) as [[[[wa wb] wc] wd] [? [? [? ?]]]].
(* Goal: @exp A (pred A) (fun SQ : pred A => @exp A (pred A) (fun SR : pred A => @exp A (pred A) (fun PQ : pred A => @exp A (pred A) (fun PR : pred A => @andp A (@andp A (@sepcon A JA (@andp A (@sepcon A JA SQ SR) S) (@andp A (@sepcon A JA PQ PR) P)) (@sepcon A JA (@andp A (@sepcon A JA SQ PQ) Q) (@andp A (@sepcon A JA SR PR) R))) (@prop A (and (@superprecise A JA PA SA SQ) (and (@superprecise A JA PA SA SR) (and (@superprecise A JA PA SA PQ) (@superprecise A JA PA SA PR))))))))) w *)
exists (exactly wa); exists (exactly wb); exists (exactly wc); exists (exactly wd).
(* Goal: @andp A P Q w *)
(* Goal: @sepcon A JA P Q w *)
repeat split; auto.
(* Goal: @andp A P Q w *)
(* Goal: @sepcon A JA P Q w *)
exists w1; exists w2; split; [|split]; auto; split; auto.
(* Goal: p a *)
exists wa; exists wb; split; [|split]; auto.
(* Goal: p a *)
exists wc; exists wd; split; [|split]; auto.
(* Goal: @andp A P Q w *)
(* Goal: @sepcon A JA P Q w *)
exists w3; exists w4; split; [|split]; auto; split; auto.
(* Goal: p a *)
exists wa; exists wc; split; [|split]; auto.
(* Goal: p a *)
exists wb; exists wd; split; [|split]; auto.
Qed.

Lemma modus_ponens {A} : forall (X P Q:pred A),
  X |-- P ->
  X |-- (P --> Q) ->
  X |-- Q.
Proof.
(* Goal: Q' z *)
  unfold derives, imp; simpl; intuition eauto.
Qed.

Lemma and_intro {A}  : forall (X P Q:pred A),
  X |-- P ->
  X |-- Q ->
  X |-- P && Q.
Proof.
(* Goal: forall (P Q R : pred A) (_ : @derives A P Q) (_ : @derives A P R), @derives A P (@andp A Q R) *)
  unfold derives, imp, andp; simpl; intuition.
Qed.

Lemma and1 {A}  : forall (X P Q:pred A),
  X |-- P && Q --> P.
Proof.
(* Goal: Q' z *)
  unfold derives, imp, andp; simpl; intuition eauto.
Qed.

Lemma and2 {A}  : forall (X P Q:pred A),
  X |-- P && Q --> Q.
Proof.
(* Goal: Q' z *)
  unfold derives, imp, andp; simpl; intuition eauto.
Qed.

Lemma and3 {A}  : forall (X P Q R:pred A),
  X |-- (P --> Q) --> (P --> R) --> (P --> Q && R).
Proof.
(* Goal: Q' z *)
  unfold derives, imp, andp; simpl; intuition eauto.
Qed.

Lemma or1 {A}  : forall (X P Q:pred A),
  X |-- P --> P || Q.
Proof.
(* Goal: forall (P Q R : pred A) (_ : @derives A P Q) (_ : @derives A P R), @derives A P (@andp A Q R) *)
  unfold derives, imp, orp; simpl; intuition.
Qed.

Lemma or2 {A}  : forall (X P Q:pred A),
  X |-- Q --> P || Q.
Proof.
(* Goal: forall (P Q R : pred A) (_ : @derives A P Q) (_ : @derives A P R), @derives A P (@andp A Q R) *)
  unfold derives, imp, orp; simpl; intuition.
Qed.

Lemma or3 {A}  : forall (X P Q R:pred A),
  X |-- (P --> R) --> (Q --> R) --> (P || Q --> R).
Proof.
(* Goal: Q' z *)
  unfold derives, imp, orp; simpl; intuition eauto.
Qed.

Lemma TTrule {A}  : forall X (P: pred A),
  X |-- P --> TT.
Proof.
(* Goal: forall (P Q R : pred A) (_ : @derives A P Q) (_ : @derives A P R), @derives A P (@andp A Q R) *)
  unfold derives, imp, TT; simpl; intuition.
Qed.

Lemma FFrule {A}  : forall X (P: pred A),
  X |-- FF --> P.
Proof.
(* Goal: forall (P Q R : pred A) (_ : @derives A P Q) (_ : @derives A P R), @derives A P (@andp A Q R) *)
  unfold derives, imp, FF; simpl; intuition.
(* Goal: P a *)
hnf in H0; contradiction.
Qed.

Lemma distribution {A}  : forall (X P Q R:pred A),
  X |-- P && (Q || R) --> (P && Q) || (P && R).
Proof.
(* Goal: forall (P Q R : pred A) (_ : @derives A P Q) (_ : @derives A P R), @derives A P (@andp A Q R) *)
  unfold derives, imp, orp, andp; simpl; intuition.
Qed.

Lemma wand_sepcon_adjoint {A} {JA: Join A}{PA: Perm_alg A} : forall (P Q R:pred A),
  ((P * Q) |-- R) = (P |-- (Q -* R)).
Proof.
(* Goal: forall P Q R : pred T, @derives T (@andp T (@sepcon T JT P Q) (@ewand T JT R (@prop T True))) (@sepcon T JT (@andp T P (@ewand T JT R (@prop T True))) (@andp T Q (@ewand T JT R (@prop T True)))) *)
  intros. apply prop_ext.
(* Goal: forall P Q R : pred T, @derives T (@andp T (@sepcon T JT P Q) (@ewand T JT R (@prop T True))) (@sepcon T JT (@andp T P (@ewand T JT R (@prop T True))) (@andp T Q (@ewand T JT R (@prop T True)))) *)
  split; intros.
(* Goal: forall P Q R : pred T, @derives T (@andp T (@sepcon T JT P Q) (@ewand T JT R (@prop T True))) (@sepcon T JT (@andp T P (@ewand T JT R (@prop T True))) (@andp T Q (@ewand T JT R (@prop T True)))) *)
  hnf; intros; simpl; intros.
(* Goal: forall P Q R : pred T, @derives T (@andp T (@sepcon T JT P Q) (@ewand T JT R (@prop T True))) (@sepcon T JT (@andp T P (@ewand T JT R (@prop T True))) (@andp T Q (@ewand T JT R (@prop T True)))) *)
  hnf; intros.
(* Goal: @FF T w *)
  apply H.
(* Goal: @andp A P Q w *)
(* Goal: @sepcon A JA P Q w *)
  exists a; exists x; split; auto.
(* Goal: forall P Q R : pred T, @derives T (@andp T (@sepcon T JT P Q) (@ewand T JT R (@prop T True))) (@sepcon T JT (@andp T P (@ewand T JT R (@prop T True))) (@andp T Q (@ewand T JT R (@prop T True)))) *)
  hnf; intros.
(* Goal: R a *)
  destruct H0 as [w [v [? [? ?]]]].
(* Goal: q w *)
  eapply H; eauto.
Qed.

Lemma ewand_sepcon {A} {JA: Join A}{PA: Perm_alg A}: forall P Q R,
      (ewand (P * Q) R = ewand P (ewand Q R))%pred.
Proof.
(* Goal: @derives A (@exp A B (fun x : B => @wand A JA P (Q x))) (@wand A JA P (@exp A B (fun x : B => Q x))) *)
intros; apply pred_ext; intros w ?.
(* Goal: @ewand A JA (@sepcon A JA P Q) R w *)
destruct H as [w1 [w2 [? [? ?]]]].
(* Goal: @ewand A JA P (@ewand A JA Q R) w *)
(* Goal: @ewand A JA (@sepcon A JA P Q) R w *)
destruct H0 as [w3 [w4 [? [? ?]]]].
(* Goal: @ewand A JA P (@ewand A JA Q R) w *)
(* Goal: @ewand A JA (@sepcon A JA P Q) R w *)
exists w3.
(* Goal: @ex A (fun w2 : A => and (@join A JA w3 w w2) (and (P w3) (@ewand A JA Q R w2))) *)
(* Goal: @ewand A JA (@sepcon A JA P Q) R w *)
destruct (join_assoc (join_comm H0) H) as [wf [? ?]].
(* Goal: @ewand A JA (@sepcon A JA P Q) R w *)
exists wf.
(* Goal: p a *)
split; [|split]; auto.
(* Goal: @andp A P Q w *)
(* Goal: @sepcon A JA P Q w *)
exists w4. exists w2. split; auto.
(* Goal: @ewand A JA (@sepcon A JA P Q) R w *)
destruct H as [w1 [w2 [? [? ?]]]].
(* Goal: @ewand A JA (@sepcon A JA P Q) R w *)
destruct H1 as [w3 [w4 [? [? ?]]]].
(* Goal: @ewand A JA (@sepcon A JA P Q) R w *)
destruct (join_assoc (join_comm H) (join_comm H1)) as [wf [? ?]].
(* Goal: p a *)
exists wf. exists w4. split; [|split]; auto.
(* Goal: @andp A P Q w *)
(* Goal: @sepcon A JA P Q w *)
exists w1; exists w3; split; auto.
Qed.


Lemma andp_right {A}  : forall (X P Q:pred A),
  X |-- P ->
  X |-- Q ->
  X |-- P && Q.
Proof.
(* Goal: forall (P Q R : pred A) (_ : @derives A P Q) (_ : @derives A P R), @derives A P (@andp A Q R) *)
  unfold derives, imp, andp; simpl; intuition.
Qed.


Lemma andp_left1{A}: forall P Q R: pred A,  P |-- R -> P && Q |-- R.
(* Goal: forall (P Q R : pred A) (_ : @derives A P R), @derives A P (@orp A Q R) *)
Proof. repeat intro. destruct H0; auto.
Qed.

Lemma andp_left2{A}: forall P Q R: pred A,  Q |-- R -> P && Q |-- R.
(* Goal: forall (P Q R : pred A) (_ : @derives A P R), @derives A P (@orp A Q R) *)
Proof. repeat intro. destruct H0; auto.
Qed.


Lemma orp_left{A}: forall P Q R: pred A,  P |-- R -> Q |-- R -> P || Q |-- R.
(* Goal: forall (P Q R : pred A) (_ : @derives A P R), @derives A P (@orp A Q R) *)
Proof. repeat intro. destruct H1; auto.
Qed.

Lemma orp_right1{A}: forall P Q R: pred A,  P |-- Q -> P |-- Q || R.
(* Goal: forall (P Q R : pred A) (_ : @derives A P R), @derives A P (@orp A Q R) *)
Proof. repeat intro. left; auto.
Qed.

Lemma orp_right2{A}: forall P Q R: pred A,  P |-- R -> P |-- Q || R.
(* Goal: forall (P Q R : pred A) (_ : @derives A P R), @derives A P (@orp A Q R) *)
Proof. repeat intro. right; auto.
Qed.

Lemma exp_right:
  forall {B A: Type}(x:B) p (q: B -> pred A),
    p |-- q x ->
    p |-- exp q.
Proof.
(* Goal: forall P Q R : pred T, @derives T (@andp T (@sepcon T JT P Q) (@ewand T JT R (@prop T True))) (@sepcon T JT (@andp T P (@ewand T JT R (@prop T True))) (@andp T Q (@ewand T JT R (@prop T True)))) *)
intros.
(* Goal: @FF T w *)
eapply derives_trans; try apply H.
(* Goal: @exp A T P w1 *)
intros w ?; exists x; auto.
Qed.

Lemma exp_left:
  forall {B A: Type}(p: B -> pred A) q,
  (forall x, p x |-- q) ->
   exp p |-- q.
Proof.
(* Goal: forall P Q R : pred T, @derives T (@andp T (@sepcon T JT P Q) (@ewand T JT R (@prop T True))) (@sepcon T JT (@andp T P (@ewand T JT R (@prop T True))) (@andp T Q (@ewand T JT R (@prop T True)))) *)
intros.
(* Goal: @derives A (@exp A B p) q *)
intros w [x' ?].
(* Goal: q w *)
eapply H; eauto.
Qed.


Lemma allp_right {B A: Type}:
  forall (P: pred A) (Q: B -> pred A),
  (forall v, P |-- Q v) ->
   P |-- allp Q.
Proof.
(* Goal: forall P Q R : pred T, @derives T (@andp T (@sepcon T JT P Q) (@ewand T JT R (@prop T True))) (@sepcon T JT (@andp T P (@ewand T JT R (@prop T True))) (@andp T Q (@ewand T JT R (@prop T True)))) *)
 intros. intros w ? v; apply (H v); auto.
Qed.

Lemma allp_left {B}{A}:
   forall (P: B -> pred A) x Q, P x |-- Q -> allp P |-- Q.
 Proof.
(* Goal: forall P Q R : pred T, @derives T (@andp T (@sepcon T JT P Q) (@ewand T JT R (@prop T True))) (@sepcon T JT (@andp T P (@ewand T JT R (@prop T True))) (@andp T Q (@ewand T JT R (@prop T True)))) *)
   intros. intros ? ?. apply H. apply H0.
Qed.

Lemma imp_andp_adjoint {A}  : forall (P Q R:pred A),
  (P && Q) |-- R <-> P |-- (Q --> R).
Proof.
(* Goal: forall P Q R : pred T, @derives T (@andp T (@sepcon T JT P Q) (@ewand T JT R (@prop T True))) (@sepcon T JT (@andp T P (@ewand T JT R (@prop T True))) (@andp T Q (@ewand T JT R (@prop T True)))) *)
  split; intros.
(* Goal: forall P Q R : pred T, @derives T (@andp T (@sepcon T JT P Q) (@ewand T JT R (@prop T True))) (@sepcon T JT (@andp T P (@ewand T JT R (@prop T True))) (@andp T Q (@ewand T JT R (@prop T True)))) *)
  hnf; intros; simpl; intros.
(* Goal: forall P Q R : pred T, @derives T (@andp T (@sepcon T JT P Q) (@ewand T JT R (@prop T True))) (@sepcon T JT (@andp T P (@ewand T JT R (@prop T True))) (@andp T Q (@ewand T JT R (@prop T True)))) *)
  intro; intros. apply H. split; auto.
(* Goal: forall P Q R : pred T, @derives T (@andp T (@sepcon T JT P Q) (@ewand T JT R (@prop T True))) (@sepcon T JT (@andp T P (@ewand T JT R (@prop T True))) (@andp T Q (@ewand T JT R (@prop T True)))) *)
  intro; intros. destruct H0. apply H; auto.
Qed.


Lemma exp_andp1 {A} :
 forall B (p: B -> pred A) q, (exp p && q)%pred = (exp (fun x => p x && q))%pred.
Proof.
(* Goal: @derives A (@exp A B (fun x : B => @wand A JA P (Q x))) (@wand A JA P (@exp A B (fun x : B => Q x))) *)
intros; apply pred_ext; intros w ?.
(* Goal: @exp A B (fun x : B => @andp A (p x) q) w *)
(* Goal: @andp A (@exp A B p) q w *)
destruct H as [[x ?] ?].
(* Goal: @andp A P Q w *)
(* Goal: @sepcon A JA P Q w *)
exists x; split; auto.
(* Goal: @andp A P Q w *)
(* Goal: @sepcon A JA P Q w *)
destruct H as [x [? ?]]; split; auto. exists x; auto.
Qed.


Lemma exp_sepcon1 {A}  {JA: Join A}{PA: Perm_alg A}:
  forall T (P: T ->  pred A) Q,  (exp P * Q = exp (fun x => P x * Q))%pred.
Proof.
(* Goal: forall P Q R : pred T, @derives T (@andp T (@sepcon T JT P Q) (@ewand T JT R (@prop T True))) (@sepcon T JT (@andp T P (@ewand T JT R (@prop T True))) (@andp T Q (@ewand T JT R (@prop T True)))) *)
intros.
(* Goal: @derives A (@allp A B P) Q *)
apply pred_ext; intros ? ?.
(* Goal: @exp A T (fun x : T => @sepcon A JA (P x) Q) a *)
(* Goal: @sepcon A JA (@exp A T P) Q a *)
destruct H as [w1 [w2 [? [[x ?] ?]]]].
(* Goal: @andp A P Q w *)
(* Goal: @sepcon A JA P Q w *)
exists x; exists w1; exists w2; split; auto.
(* Goal: @sepcon A JA (@exp A T P) Q a *)
destruct H as [x [w1 [w2 [? [? ?]]]]].
(* Goal: @andp A P Q w *)
(* Goal: @sepcon A JA P Q w *)
exists w1; exists w2; split; auto.
(* Goal: @andp A P Q w *)
(* Goal: @sepcon A JA P Q w *)
split; auto.
(* Goal: @exp A T P w1 *)
exists x; auto.
Qed.


Definition pure {A}{JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A}
     (P: pred A) : Prop :=
   P |-- emp.

Lemma sepcon_pure_andp {A} {JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A}:
 forall P Q, pure P -> pure Q -> ((P * Q) = (P && Q)).
Proof.
(* Goal: forall P Q R : pred T, @derives T (@andp T (@sepcon T JT P Q) (@ewand T JT R (@prop T True))) (@sepcon T JT (@andp T P (@ewand T JT R (@prop T True))) (@andp T Q (@ewand T JT R (@prop T True)))) *)
intros.
(* Goal: @derives A (@exp A B (fun x : B => @wand A JA P (Q x))) (@wand A JA P (@exp A B (fun x : B => Q x))) *)
apply pred_ext; intros w ?.
(* Goal: @sepcon A JA P Q w *)
(* Goal: @derives A (@sepcon A JA P Q) (@andp A (@sepcon A JA P (@TT A)) Q) *)
destruct H1 as [w1 [w2 [? [? ?]]]].
(* Goal: @andp A P Q w *)
(* Goal: @sepcon A JA P Q w *)
unfold pure in *.
(* Goal: @andp A P Q w *)
(* Goal: @sepcon A JA P Q w *)
assert (unit_for w1 w2). apply H in H2; simpl in H2;
(* Goal: @join A JA e w w *)
apply identity_unit; auto. exists w; auto.
(* Goal: @andp A P Q w *)
(* Goal: @sepcon A JA P Q w *)
unfold unit_for in H4.
(* Goal: @andp A P Q w *)
(* Goal: @sepcon A JA P Q w *)
assert (w2=w) by (apply (join_eq H4 H1)).
(* Goal: @andp A P Q w *)
(* Goal: @sepcon A JA P Q w *)
subst w2.
(* Goal: @andp A P Q w *)
(* Goal: @sepcon A JA P Q w *)
assert (join w w1 w1).
(* Goal: p a *)
apply identity_unit; apply H0 in H3; simpl in H3; auto. exists w; auto.
(* Goal: @andp A P Q w *)
(* Goal: @sepcon A JA P Q w *)
assert (w1=w) by (apply (join_eq H5 (join_comm H1))).
(* Goal: @andp A P Q w *)
(* Goal: @sepcon A JA P Q w *)
subst w1.
(* Goal: @andp A P Q w *)
(* Goal: @sepcon A JA P Q w *)
split; auto.
(* Goal: @sepcon A JA P Q w *)
destruct H1.
(* Goal: p a *)
exists w; exists w; split; [|split]; auto.
(* Goal: @join A JA w w w *)
apply H in H1.
(* Goal: @join A JA w w w *)
clear dependent P. clear dependent Q.
(* Goal: @join A JA w w w *)
pose proof (core_unit w); unfold unit_for in *.
(* Goal: @join A JA w w w *)
pose proof (H1 _ _ (join_comm H)).
(* Goal: p a *)
rewrite H0 in H; auto.
Qed.

Lemma pure_sepcon_TT_andp {A} {JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A}:
  forall P Q, pure P -> (P * TT) && Q = (P*Q).
Proof.
(* Goal: forall (P Q : pred A) (_ : @pure A JA PA SA P), @eq (forall _ : A, Prop) (@andp A (@sepcon A JA P (@TT A)) Q) (@sepcon A JA P Q) *)
 pose proof I.
(* Goal: forall P Q R : pred T, @derives T (@andp T (@sepcon T JT P Q) (@ewand T JT R (@prop T True))) (@sepcon T JT (@andp T P (@ewand T JT R (@prop T True))) (@andp T Q (@ewand T JT R (@prop T True)))) *)
intros.
(* Goal: @eq (forall _ : A, Prop) (@andp A (@sepcon A JA P (@TT A)) Q) (@sepcon A JA P Q) *)
apply pred_ext.
(* Goal: @derives A (@andp A (@sepcon A JA P (@TT A)) Q) (@sepcon A JA P Q) *)
(* Goal: @derives A (@sepcon A JA P Q) (@andp A (@sepcon A JA P (@TT A)) Q) *)
intros w [? ?].
(* Goal: @sepcon A JA P Q w *)
(* Goal: @derives A (@sepcon A JA P Q) (@andp A (@sepcon A JA P (@TT A)) Q) *)
destruct H1 as [w1 [w2 [? [? ?]]]].
(* Goal: p a *)
exists w1; exists w2; split; [|split]; auto.
(* Goal: p a *)
apply join_unit1_e in H1; auto.
(* Goal: p a *)
subst; auto.
(* Goal: @derives A (@sepcon A JA P Q) (@andp A (@sepcon A JA P (@TT A)) Q) *)
apply andp_right.
(* Goal: p a *)
apply sepcon_derives; auto.
(* Goal: @derives A (@sepcon A JA P Q) Q *)
intros w [w1 [w2 [? [? ?]]]].
(* Goal: p a *)
apply join_unit1_e in H1; auto.
(* Goal: p a *)
subst; auto.
Qed.

Lemma ewand_conflict {T}{JT: Join T}{PT: Perm_alg T}{ST: Sep_alg T}:
       forall P Q R, sepcon P Q |-- FF -> andp P (ewand Q R) |-- FF.
Proof.
(* Goal: forall P Q R : pred T, @derives T (@andp T (@sepcon T JT P Q) (@ewand T JT R (@prop T True))) (@sepcon T JT (@andp T P (@ewand T JT R (@prop T True))) (@andp T Q (@ewand T JT R (@prop T True)))) *)
 intros. intros w [? [w1 [w2 [? [? ?]]]]].
(* Goal: @andp A P Q w *)
(* Goal: @sepcon A JA P Q w *)
 specialize (H w2). apply H. exists w; exists w1; repeat split; auto.
Qed.

Lemma ewand_TT_sepcon {T}{JT: Join T}{PT: Perm_alg T}{ST: Sep_alg T}:
      forall P Q R,
(P * Q && ewand R (!!True))%pred |-- (P && ewand R (!!True) * (Q && ewand R (!!True)))%pred.
Proof.
(* Goal: forall P Q R : pred T, @derives T (@andp T (@sepcon T JT P Q) (@ewand T JT R (@prop T True))) (@sepcon T JT (@andp T P (@ewand T JT R (@prop T True))) (@andp T Q (@ewand T JT R (@prop T True)))) *)
intros.
(* Goal: @derives T (@andp T (@sepcon T JT P Q) (@ewand T JT R (@prop T True))) (@sepcon T JT (@andp T P (@ewand T JT R (@prop T True))) (@andp T Q (@ewand T JT R (@prop T True)))) *)
intros w [[w1 [w2 [? [? ?]]]] [w3 [w4 [? [? ?]]]]].
(* Goal: @andp A P Q w *)
(* Goal: @sepcon A JA P Q w *)
exists w1; exists w2; repeat split; auto.
(* Goal: @ewand T JT R (@prop T True) w1 *)
(* Goal: @ewand T JT R (@prop T True) w2 *)
destruct (join_assoc (join_comm H) (join_comm H2)) as [f [? ?]].
(* Goal: @andp A P Q w *)
(* Goal: @sepcon A JA P Q w *)
exists w3; exists f; repeat split; auto.
(* Goal: @ewand T JT R (@prop T True) w2 *)
destruct (join_assoc H (join_comm H2)) as [g [? ?]].
(* Goal: @andp A P Q w *)
(* Goal: @sepcon A JA P Q w *)
exists w3; exists g; repeat split; auto.
Qed.
