(*
 * Copyright (c) 2009-2010, Andrew Appel, Robert Dockins and Aquinas Hobor.
 *
 *)

Require Import VST.msl.base.
Require Import VST.msl.ageable.
Require Import VST.msl.sepalg.
Require Import VST.msl.sepalg_generators.
Require Import VST.msl.age_sepalg.
Require Import VST.msl.predicates_hered.
Require Import VST.msl.cross_split.

Definition compareR {A} {JA: Join A}{SA: Sep_alg A}{AG: ageable A} : relation A
   := comparable.
Definition extendR  {A} {JA: Join A}{PA: Perm_alg A}{AG: ageable A} : relation A := join_sub.

Lemma valid_rel_compare {A} {JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A}{AG: ageable A}{XA: Age_alg A} : valid_rel compareR.
Proof.
(* Goal: @valid_rel A AG (@compareR A JA SA AG) *)
  split; hnf; intros.

(* Goal: @ex2 A (fun y' : A => @compareR A JA SA AG y' x) (fun y' : A => @age A AG z y') *)
(* Goal: @ex2 A (fun y' : A => @age A AG y' x) (fun y' : A => @compareR A JA SA AG z y') *)
  apply comparable_common_unit in H0.
(* Goal: @ex2 A (fun y' : A => @compareR A JA SA AG y' x) (fun y' : A => @age A AG z y') *)
(* Goal: @ex2 A (fun y' : A => @age A AG y' x) (fun y' : A => @compareR A JA SA AG z y') *)
  destruct H0 as [w [? ?]].
  destruct (age1_join2  _ H1 H)
    as [u [v [? [? ?]]]].
  destruct (age1_join _ H0 H3)
    as [u' [v' [? [? ?]]]].
(* Goal: @ex2 A (fun y' : A => @compareR A JA SA AG y' x) (fun y' : A => @age A AG z y') *)
(* Goal: @ex2 A (fun y' : A => @age A AG y' x) (fun y' : A => @compareR A JA SA AG z y') *)
  assert (u' = v').
(* Goal: @eq A v a' *)
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@box A AG (@ageM A AG) P) (@box A AG (@ageM A AG) Q)) a *)
(* Goal: @app_pred A AG (@box A AG (@ageM A AG) (@sepcon A JA PA AG XA P Q)) a *)
  unfold age in *; congruence.
(* Goal: @ex2 A (fun y' : A => @compareR A JA SA AG y' x) (fun y' : A => @age A AG z y') *)
(* Goal: @ex2 A (fun y' : A => @age A AG y' x) (fun y' : A => @compareR A JA SA AG z y') *)
  subst v'.
(* Goal: @ex2 A (fun y' : A => @compareR A JA SA AG y' x) (fun y' : A => @age A AG z y') *)
(* Goal: @ex2 A (fun y' : A => @age A AG y' x) (fun y' : A => @compareR A JA SA AG z y') *)
  exists u'; auto.
(* Goal: @compareR A JA SA AG u' x *)
(* Goal: @ex2 A (fun y' : A => @age A AG y' x) (fun y' : A => @compareR A JA SA AG z y') *)
  assert (x = v).
(* Goal: @eq A v a' *)
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@box A AG (@ageM A AG) P) (@box A AG (@ageM A AG) Q)) a *)
(* Goal: @app_pred A AG (@box A AG (@ageM A AG) (@sepcon A JA PA AG XA P Q)) a *)
  unfold age in *; congruence.
(* Goal: @compareR A JA SA AG u' x *)
(* Goal: @ex2 A (fun y' : A => @age A AG y' x) (fun y' : A => @compareR A JA SA AG z y') *)
  subst v.
(* Goal: @compareR A JA SA AG z v' *)
  apply common_unit_comparable.
(* Goal: @extendR A JA PA AG z v *)
  exists u; auto.

(* Goal: @ex2 A (fun y' : A => @age A AG y' x) (fun y' : A => @compareR A JA SA AG z y') *)
  apply comparable_common_unit in H.
(* Goal: @ex2 A (fun y' : A => @age A AG y' x) (fun y' : A => @compareR A JA SA AG z y') *)
  destruct H as [w [? ?]].
  destruct (unage_join2 _ H H0)
    as [u [v [? [? ?]]]].
  destruct (unage_join _ H1 H3)
    as [u' [v' [? [? ?]]]].
(* Goal: @ex2 A (fun y' : A => @age A AG y' x) (fun y' : A => @compareR A JA SA AG z y') *)
  exists v'; auto.
(* Goal: @compareR A JA SA AG z v' *)
  apply common_unit_comparable.
(* Goal: @ex A (fun e : A => and (@join A JA e z z) (@join A JA e v' v')) *)
  destruct (join_ex_units u) as [uu Huu].
(* Goal: @ex A (fun e : A => and (@join A JA e z z) (@join A JA e v' v')) *)
  red in Huu.
(* Goal: @ex A (fun e : A => and (@join A JA e z z) (@join A JA e v' v')) *)
  exists uu; split.
(* Goal: @join A JA uu z z *)
(* Goal: @join A JA uu v' v' *)
  destruct (join_assoc Huu H2) as [q [? ?]].
(* Goal: @join A JA uu z z *)
(* Goal: @join A JA uu v' v' *)
  assert (q = z).
(* Goal: @eq A f w2 *)
(* Goal: @app_pred A AG (@ewand A JA PA AG XA (@TT A AG) (@sepcon A JA PA AG XA P Q)) w *)
  eapply join_eq; eauto.
(* Goal: @join A JA uu z z *)
(* Goal: @join A JA uu v' v' *)
  subst q; auto.
(* Goal: @join A JA uu v' v' *)
  destruct (join_assoc Huu H5) as [q [? ?]].
(* Goal: @join A JA uu v' v' *)
  assert (q = v').
(* Goal: @eq A f w2 *)
(* Goal: @app_pred A AG (@ewand A JA PA AG XA (@TT A AG) (@sepcon A JA PA AG XA P Q)) w *)
  eapply join_eq; eauto.
(* Goal: @join A JA uu v' v' *)
  subst q.
(* Goal: @join A JA w1 w5 w3 *)
  auto.
Qed.

Lemma valid_rel_extend {A}  {JA: Join A}{PA: Perm_alg A}{AG: ageable A}{XA: Age_alg A} : valid_rel extendR.
Proof.
(* Goal: @valid_rel A AG (@compareR A JA SA AG) *)
  intros; split; hnf; intros.
(* Goal: @ex2 A (fun y' : A => @extendR A JA PA AG y' x) (fun y' : A => @age A AG z y') *)
(* Goal: @ex2 A (fun y' : A => @age A AG y' x) (fun y' : A => @extendR A JA PA AG z y') *)
  destruct H0 as [w ?].
  destruct (age1_join2 _ H0 H)
    as [u [v [? [? ?]]]].
(* Goal: @extendR A JA PA AG z v *)
  exists u; auto.
(* Goal: @join A JA w1 w5 w3 *)
  exists v; auto.

(* Goal: @app_pred A AG (@sepcon A JA PA AG XA P (@andp A AG (@prop A AG Q) R)) w *)
  destruct H.
  destruct (unage_join _ H H0)
    as [u [v [? [? ?]]]].
(* Goal: @join A JA w1 w5 w3 *)
  exists v; auto.
(* Goal: @extendR A JA PA AG z v *)
  exists u; auto.
Qed.

Definition compareM {A} {JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A}{AG: ageable A}{XA: Age_alg A} : modality
  := exist _ compareR valid_rel_compare.
Definition extendM {A}{JA: Join A}{PA: Perm_alg A}{AG: ageable A}{XA: Age_alg A} : modality
  := exist _ extendR valid_rel_extend.

(* Definitions of the BI connectives. *)
Obligation Tactic := unfold hereditary; intros; try solve [intuition].

Program Definition emp {A}  {JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A}{AG: ageable A}{XA: Age_alg A} : pred A := identity.
Next Obligation.
(* Goal: @precise A JA PA SA AG XA (@emp A JA PA SA AG XA) *)
  repeat intro.
(* Goal: @eq A a0 b *)
  destruct (unage_join _ H1 H) as [a0' [b' [? [? ?]]]].
(* Goal: @eq A a0 b *)
  apply H0 in H2. subst b'. unfold age in H3, H4. congruence.
Qed.

Program Definition sepcon {A}  {JA: Join A}{PA: Perm_alg A}{AG: ageable A}{XA: Age_alg A} (p q:pred A) : pred A := fun x:A =>
  exists y:A, exists z:A, join y z x /\ p y /\ q z.
Next Obligation.
(* Goal: @ex A (fun y : A => @ex A (fun z : A => and (@join A JA y z a') (and (@app_pred A AG p y) (@app_pred A AG q z)))) *)
  destruct H0 as [y [z [? [? ?]]]].
(* Goal: @ex A (fun y : A => @ex A (fun z : A => and (@join A JA y z a') (and (@app_pred A AG p y) (@app_pred A AG q z)))) *)
  destruct (age1_join2 _ H0 H) as [w [v [? [? ?]]]].
(* Goal: @join A JA w1 w5 w3 *)
  exists w; exists v; split; auto.
(* Goal: @app_pred A AG (@andp A AG (@prop A AG Q) (@sepcon A JA PA AG XA P R)) w *)
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA P (@andp A AG (@prop A AG Q) R)) w *)
  split.
(* Goal: @join A JA w1 w5 w3 *)
  apply pred_hereditary with y; auto.
(* Goal: @join A JA w1 w5 w3 *)
  apply pred_hereditary with z; auto.
Qed.

Program Definition wand {A}  {JA: Join A}{PA: Perm_alg A}{AG: ageable A}{XA: Age_alg A} (p q:pred A) : pred A := fun x =>
  forall x' y z, necR x x' -> join x' y z -> p y -> q z.
Next Obligation.
(* Goal: @join A JA w1 w5 w3 *)
  apply H0 with x' y; auto.
(* Goal: @join A JA w1 w5 w3 *)
  apply rt_trans with a'; auto.
(* Goal: @join A JA w1 w5 w3 *)
  apply rt_step; auto.
Qed.

Notation "P '*' Q" := (sepcon P Q) : pred.
Notation "P '-*' Q" := (wand P Q) (at level 60, right associativity) : pred.
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@box A AG (@ageM A AG) P) (@box A AG (@ageM A AG) Q)) a *)
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@box A AG (@ageM A AG) P) (@box A AG (@ageM A AG) Q)) a *)
(* Goal: @app_pred A AG (@box A AG (@ageM A AG) (@sepcon A JA PA AG XA P Q)) a *)
Notation "'%' e"  := (box extendM e)(at level 30, right associativity): pred.

Lemma extendM_refl {A} {JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A}{AG: ageable A}{XA: Age_alg A}: reflexive _ extendM.
Proof.
(* Goal: reflexive A (@app_mode A AG (@extendM A JA PA AG XA)) *)
intros; intro; simpl; apply join_sub_refl.
Qed.

Lemma compareM_refl {A}{JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A}{AG: ageable A}{XA: Age_alg A} : reflexive _ compareM.
Proof.
(* Goal: reflexive A (@app_mode A AG (@compareM A JA PA SA AG XA)) *)
intros; intro; simpl.
(* Goal: @compareR A JA SA AG x x *)
apply comparable_refl.
Qed.

Hint Resolve @extendM_refl.
Hint Resolve @compareM_refl.


(* Rules for the BI connectives *)

Lemma wand_sepcon_adjoint {A} {JA: Join A}{PA: Perm_alg A}{AG: ageable A}{XA: Age_alg A} : forall (P Q R:pred A),
  ((P * Q) |-- R) = (P |-- (Q -* R)).
Proof.
(* Goal: forall P Q R : @pred T agT, @derives T agT (@andp T agT (@sepcon T JT PT agT AT P Q) (@ewand T JT PT agT AT R (@prop T agT True))) (@sepcon T JT PT agT AT (@andp T agT P (@ewand T JT PT agT AT R (@prop T agT True))) (@andp T agT Q (@ewand T JT PT agT AT R (@prop T agT True)))) *)
  intros. apply prop_ext.
(* Goal: forall P Q R : @pred T agT, @derives T agT (@andp T agT (@sepcon T JT PT agT AT P Q) (@ewand T JT PT agT AT R (@prop T agT True))) (@sepcon T JT PT agT AT (@andp T agT P (@ewand T JT PT agT AT R (@prop T agT True))) (@andp T agT Q (@ewand T JT PT agT AT R (@prop T agT True)))) *)
  split; intros.
(* Goal: forall P Q R : @pred T agT, @derives T agT (@andp T agT (@sepcon T JT PT agT AT P Q) (@ewand T JT PT agT AT R (@prop T agT True))) (@sepcon T JT PT agT AT (@andp T agT P (@ewand T JT PT agT AT R (@prop T agT True))) (@andp T agT Q (@ewand T JT PT agT AT R (@prop T agT True)))) *)
  hnf; intros; simpl; intros.
(* Goal: @app_pred T agT (@FF T agT) w *)
  apply H.
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA P Q) z *)
(* Goal: @derives A AG (@sepcon A JA PA AG XA P Q) R *)
  exists x'; exists y.
(* Goal: and (@join A JA x a a) (and (@app_pred A AG (@box A AG (@ageM A AG) P) x) (@app_pred A AG (@box A AG (@ageM A AG) Q) a)) *)
(* Goal: @app_pred A AG (@box A AG (@ageM A AG) (@sepcon A JA PA AG XA P Q)) a *)
  intuition.
(* Goal: @join A JA w1 w5 w3 *)
  apply pred_nec_hereditary with a; auto.
(* Goal: forall P Q R : @pred T agT, @derives T agT (@andp T agT (@sepcon T JT PT agT AT P Q) (@ewand T JT PT agT AT R (@prop T agT True))) (@sepcon T JT PT agT AT (@andp T agT P (@ewand T JT PT agT AT R (@prop T agT True))) (@andp T agT Q (@ewand T JT PT agT AT R (@prop T agT True)))) *)
  hnf; intros.
(* Goal: @app_pred A AG R a *)
  hnf in H.
(* Goal: @app_pred A AG R a *)
  unfold wand in H; simpl in H.
(* Goal: @app_pred A AG (@box A AG (@ageM A AG) (@sepcon A JA PA AG XA P Q)) a *)
  destruct H0 as [w [v [? [? ?]]]].
(* Goal: @join A JA w1 w5 w3 *)
  eapply H; eauto.
Qed.

Lemma sepcon_assoc {A} {JA: Join A}{PA: Perm_alg A}{AG: ageable A}{XA: Age_alg A} : forall (P Q R:pred A),
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@box A AG (@ageM A AG) P) (@box A AG (@ageM A AG) Q)) a *)
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@box A AG (@ageM A AG) P) (@box A AG (@ageM A AG) Q)) a *)
(* Goal: @app_pred A AG (@box A AG (@ageM A AG) (@sepcon A JA PA AG XA P Q)) a *)
  ((P * Q) * R = P * (Q * R))%pred.
Proof.
(* Goal: forall (G P Q : @pred A AG) (_ : @superprecise A JA PA SA AG XA G) (_ : @eq (@pred A AG) P (@ewand A JA PA AG XA G (@sepcon A JA PA AG XA G P))), @derives A AG (@andp A AG (@sepcon A JA PA AG XA P Q) (@sepcon A JA PA AG XA G (@TT A AG))) (@sepcon A JA PA AG XA (@sepcon A JA PA AG XA P G) (@ewand A JA PA AG XA G Q)) *)
  pose proof I.
(* Goal: forall P Q R : @pred T agT, @derives T agT (@andp T agT (@sepcon T JT PT agT AT P Q) (@ewand T JT PT agT AT R (@prop T agT True))) (@sepcon T JT PT agT AT (@andp T agT P (@ewand T JT PT agT AT R (@prop T agT True))) (@andp T agT Q (@ewand T JT PT agT AT R (@prop T agT True)))) *)
  intros; apply pred_ext; hnf; intros.
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA P Q) a *)
  destruct H0 as [x [y [? [? ?]]]].
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA P (@sepcon A JA PA AG XA Q R)) a *)
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@sepcon A JA PA AG XA P Q) R) a *)
  destruct H1 as [z [w [? [? ?]]]].
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA P (@sepcon A JA PA AG XA Q R)) a *)
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@sepcon A JA PA AG XA P Q) R) a *)
  destruct (join_assoc H1 H0) as [q [? ?]].
(* Goal: and (@join A JA x a a) (and (@app_pred A AG (@box A AG (@ageM A AG) P) x) (@app_pred A AG (@box A AG (@ageM A AG) Q) a)) *)
(* Goal: @app_pred A AG (@box A AG (@ageM A AG) (@sepcon A JA PA AG XA P Q)) a *)
  exists z; exists q; intuition.
(* Goal: and (@join A JA x a a) (and (@app_pred A AG (@box A AG (@ageM A AG) P) x) (@app_pred A AG (@box A AG (@ageM A AG) Q) a)) *)
(* Goal: @app_pred A AG (@box A AG (@ageM A AG) (@sepcon A JA PA AG XA P Q)) a *)
  exists w; exists y; intuition.
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA P Q) a *)
  destruct H0 as [x [y [? [? ?]]]].
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@sepcon A JA PA AG XA P Q) R) a *)
  destruct H2 as [z [w [? [? ?]]]].
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@sepcon A JA PA AG XA P Q) R) a *)
  apply join_comm in H0.
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@sepcon A JA PA AG XA P Q) R) a *)
  apply join_comm in H2.
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@sepcon A JA PA AG XA P Q) R) a *)
  destruct (join_assoc H2 H0) as [q [? ?]].
(* Goal: and (@join A JA x a a) (and (@app_pred A AG (@box A AG (@ageM A AG) P) x) (@app_pred A AG (@box A AG (@ageM A AG) Q) a)) *)
(* Goal: @app_pred A AG (@box A AG (@ageM A AG) (@sepcon A JA PA AG XA P Q)) a *)
  exists q; exists w; intuition.
(* Goal: and (@join A JA x a a) (and (@app_pred A AG (@box A AG (@ageM A AG) P) x) (@app_pred A AG (@box A AG (@ageM A AG) Q) a)) *)
(* Goal: @app_pred A AG (@box A AG (@ageM A AG) (@sepcon A JA PA AG XA P Q)) a *)
  exists x; exists z; intuition.
Qed.

Lemma sepcon_comm {A} {JA: Join A}{PA: Perm_alg A}{AG: ageable A}{XA: Age_alg A} : forall (P Q:pred A),
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@box A AG (@ageM A AG) P) (@box A AG (@ageM A AG) Q)) a *)
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@box A AG (@ageM A AG) P) (@box A AG (@ageM A AG) Q)) a *)
(* Goal: @app_pred A AG (@box A AG (@ageM A AG) (@sepcon A JA PA AG XA P Q)) a *)
  (P * Q = Q * P)%pred.
Proof.
(* Goal: forall (G P Q : @pred A AG) (_ : @superprecise A JA PA SA AG XA G) (_ : @eq (@pred A AG) P (@ewand A JA PA AG XA G (@sepcon A JA PA AG XA G P))), @derives A AG (@andp A AG (@sepcon A JA PA AG XA P Q) (@sepcon A JA PA AG XA G (@TT A AG))) (@sepcon A JA PA AG XA (@sepcon A JA PA AG XA P G) (@ewand A JA PA AG XA G Q)) *)
  pose proof I.
(* Goal: forall P Q R : @pred T agT, @derives T agT (@andp T agT (@sepcon T JT PT agT AT P Q) (@ewand T JT PT agT AT R (@prop T agT True))) (@sepcon T JT PT agT AT (@andp T agT P (@ewand T JT PT agT AT R (@prop T agT True))) (@andp T agT Q (@ewand T JT PT agT AT R (@prop T agT True)))) *)
  intros; apply pred_ext; hnf; intros.
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA P Q) a *)
  destruct H0 as [x [y [? [? ?]]]].
(* Goal: @join A JA w1 w5 w3 *)
  exists y; exists x; intuition; apply join_comm; auto.
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA P Q) a *)
  destruct H0 as [x [y [? [? ?]]]].
(* Goal: @join A JA w1 w5 w3 *)
  exists y; exists x; intuition; apply join_comm; auto.
Qed.

Lemma split_sepcon {A} {JA: Join A}{PA: Perm_alg A}{AG: ageable A}{XA: Age_alg A} : forall (P Q R S:pred A),
  P |-- Q ->
  R |-- S ->
  (P * R) |-- (Q * S).
Proof.
(* Goal: forall P Q R : @pred T agT, @derives T agT (@andp T agT (@sepcon T JT PT agT AT P Q) (@ewand T JT PT agT AT R (@prop T agT True))) (@sepcon T JT PT agT AT (@andp T agT P (@ewand T JT PT agT AT R (@prop T agT True))) (@andp T agT Q (@ewand T JT PT agT AT R (@prop T agT True)))) *)
  intros; hnf; intros.
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA Q S) a *)
  destruct H1 as [x [y [? [? ?]]]].
(* Goal: and (@join A JA x a a) (and (@app_pred A AG (@box A AG (@ageM A AG) P) x) (@app_pred A AG (@box A AG (@ageM A AG) Q) a)) *)
(* Goal: @app_pred A AG (@box A AG (@ageM A AG) (@sepcon A JA PA AG XA P Q)) a *)
  exists x; exists y; intuition.
Qed.

Lemma sepcon_cut {A} {JA: Join A}{PA: Perm_alg A}{AG: ageable A}{XA: Age_alg A} : forall (P Q R S:pred A),
  P |-- (Q -* R) ->
  S |-- Q ->
  (P * S) |-- R.
Proof.
(* Goal: forall P Q R : @pred T agT, @derives T agT (@andp T agT (@sepcon T JT PT agT AT P Q) (@ewand T JT PT agT AT R (@prop T agT True))) (@sepcon T JT PT agT AT (@andp T agT P (@ewand T JT PT agT AT R (@prop T agT True))) (@andp T agT Q (@ewand T JT PT agT AT R (@prop T agT True)))) *)
  intros.
(* Goal: @derives A AG (@sepcon A JA PA AG XA P S) R *)
  rewrite wand_sepcon_adjoint.
(* Goal: forall P Q R : @pred T agT, @derives T agT (@andp T agT (@sepcon T JT PT agT AT P Q) (@ewand T JT PT agT AT R (@prop T agT True))) (@sepcon T JT PT agT AT (@andp T agT P (@ewand T JT PT agT AT R (@prop T agT True))) (@andp T agT Q (@ewand T JT PT agT AT R (@prop T agT True)))) *)
  hnf; intros.
(* Goal: forall P Q R : @pred T agT, @derives T agT (@andp T agT (@sepcon T JT PT agT AT P Q) (@ewand T JT PT agT AT R (@prop T agT True))) (@sepcon T JT PT agT AT (@andp T agT P (@ewand T JT PT agT AT R (@prop T agT True))) (@andp T agT Q (@ewand T JT PT agT AT R (@prop T agT True)))) *)
  simpl; intros.
(* Goal: @join A JA w1 w5 w3 *)
  eapply H; eauto.
Qed.

Lemma emp_sepcon {A} {JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A}{AG: ageable A}{XA: Age_alg A} : forall (P:pred A),
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@box A AG (@ageM A AG) P) (@box A AG (@ageM A AG) Q)) a *)
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@box A AG (@ageM A AG) P) (@box A AG (@ageM A AG) Q)) a *)
(* Goal: @app_pred A AG (@box A AG (@ageM A AG) (@sepcon A JA PA AG XA P Q)) a *)
  (emp * P = P)%pred.
Proof.
(* Goal: forall P Q R : @pred T agT, @derives T agT (@andp T agT (@sepcon T JT PT agT AT P Q) (@ewand T JT PT agT AT R (@prop T agT True))) (@sepcon T JT PT agT AT (@andp T agT P (@ewand T JT PT agT AT R (@prop T agT True))) (@andp T agT Q (@ewand T JT PT agT AT R (@prop T agT True)))) *)
  intros; apply pred_ext; hnf; intros.
(* Goal: @app_pred A AG P a *)
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@emp A JA PA SA AG XA) P) a *)
  destruct H as [x [y [? [? ?]]]].
(* Goal: @ex A (fun phi2' : A => and (@eq (option A) (@ageN A AG (S n) phi2) (@Some A phi2')) (@comparable A JA SA phi1' phi2')) *)
  simpl in H0.
(* Goal: @join A JA w1 w5 w3 *)
  replace a with y; auto.
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@emp A JA PA SA AG XA) P) a *)
  destruct (join_ex_identities a) as [u [Hu [? Hj]]].
(* Goal: @join A JA w1 w5 w3 *)
  exists u; exists a. split; auto.
(* Goal: @join A JA w1 w5 w3 *)
  specialize (Hu _ _ Hj); subst; auto.
Qed.

Lemma sepcon_emp {A} {JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A}{AG: ageable A}{XA: Age_alg A}  : forall (P:pred A),
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@box A AG (@ageM A AG) P) (@box A AG (@ageM A AG) Q)) a *)
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@box A AG (@ageM A AG) P) (@box A AG (@ageM A AG) Q)) a *)
(* Goal: @app_pred A AG (@box A AG (@ageM A AG) (@sepcon A JA PA AG XA P Q)) a *)
  (P * emp = P)%pred.
Proof.
(* Goal: forall P Q R : @pred T agT, @derives T agT (@andp T agT (@sepcon T JT PT agT AT P Q) (@ewand T JT PT agT AT R (@prop T agT True))) (@sepcon T JT PT agT AT (@andp T agT P (@ewand T JT PT agT AT R (@prop T agT True))) (@andp T agT Q (@ewand T JT PT agT AT R (@prop T agT True)))) *)
  intros.
(* Goal: @eq (@pred A agA) (@sepcon A JA PA agA AgeA (@andp A agA (@prop A agA P) Q) R) (@andp A agA (@prop A agA P) (@sepcon A JA PA agA AgeA Q R)) *)
  rewrite sepcon_comm.
(* Goal: @eq (@pred A AG) (@sepcon A JA PA AG XA (@emp A JA PA SA AG XA) P) P *)
  apply emp_sepcon.
Qed.

(*Lemma emp_sepcon : forall {A} `{Age_alg A} (P:pred A), emp * P = P.
Proof. exact @emp_sepcon. Qed.
Lemma sepcon_emp : forall {A} `{Age_alg A} (P:pred A), P * emp = P.
Proof. exact @sepcon_emp. Qed.
*)
	
Lemma later_wand {A} {JA: Join A}{PA: Perm_alg A}{AG: ageable A}{XA: Age_alg A} : forall P Q,
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@box A AG (@ageM A AG) P) (@box A AG (@ageM A AG) Q)) a *)
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@box A AG (@ageM A AG) P) (@box A AG (@ageM A AG) Q)) a *)
(* Goal: @app_pred A AG (@box A AG (@ageM A AG) (@sepcon A JA PA AG XA P Q)) a *)
  (|>(P -* Q) = |>P -* |>Q)%pred.
Proof.
(* Goal: forall (G P Q : @pred A AG) (_ : @superprecise A JA PA SA AG XA G) (_ : @eq (@pred A AG) P (@ewand A JA PA AG XA G (@sepcon A JA PA AG XA G P))), @derives A AG (@andp A AG (@sepcon A JA PA AG XA P Q) (@sepcon A JA PA AG XA G (@TT A AG))) (@sepcon A JA PA AG XA (@sepcon A JA PA AG XA P G) (@ewand A JA PA AG XA G Q)) *)
  pose proof I.
(* Goal: forall P Q R : @pred T agT, @derives T agT (@andp T agT (@sepcon T JT PT agT AT P Q) (@ewand T JT PT agT AT R (@prop T agT True))) (@sepcon T JT PT agT AT (@andp T agT P (@ewand T JT PT agT AT R (@prop T agT True))) (@andp T agT Q (@ewand T JT PT agT AT R (@prop T agT True)))) *)
  intros.
(* Goal: @eq (@pred A AG) (@box A AG (@laterM A AG) (@sepcon A JA PA AG XA P Q)) (@sepcon A JA PA AG XA (@box A AG (@laterM A AG) P) (@box A AG (@laterM A AG) Q)) *)
  repeat rewrite later_age.
(* Goal: forall P Q R : @pred T agT, @derives T agT (@andp T agT (@sepcon T JT PT agT AT P Q) (@ewand T JT PT agT AT R (@prop T agT True))) (@sepcon T JT PT agT AT (@andp T agT P (@ewand T JT PT agT AT R (@prop T agT True))) (@andp T agT Q (@ewand T JT PT agT AT R (@prop T agT True)))) *)
  apply pred_ext; hnf; intros.
(* Goal: forall P Q R : @pred T agT, @derives T agT (@andp T agT (@sepcon T JT PT agT AT P Q) (@ewand T JT PT agT AT R (@prop T agT True))) (@sepcon T JT PT agT AT (@andp T agT P (@ewand T JT PT agT AT R (@prop T agT True))) (@andp T agT Q (@ewand T JT PT agT AT R (@prop T agT True)))) *)
  simpl; intros.
(* Goal: @ex A (fun phi2' : A => and (@eq (option A) (@ageN A AG (S n) phi2) (@Some A phi2')) (@comparable A JA SA phi1' phi2')) *)
  simpl in H0.
(* Goal: forall P Q R : @pred T agT, @derives T agT (@andp T agT (@sepcon T JT PT agT AT P Q) (@ewand T JT PT agT AT R (@prop T agT True))) (@sepcon T JT PT agT AT (@andp T agT P (@ewand T JT PT agT AT R (@prop T agT True))) (@andp T agT Q (@ewand T JT PT agT AT R (@prop T agT True)))) *)
  case_eq (age1 a); intros.
(* Goal: @app_pred A AG Q a' *)
(* Goal: @app_pred A AG Q a' *)
(* Goal: @app_pred A AG (@box A AG (@ageM A AG) (@wand A JA PA AG XA P Q)) a *)
  specialize ( H0 a0 H5).
(* Goal: @app_pred A AG Q a' *)
(* Goal: @app_pred A AG Q a' *)
(* Goal: @app_pred A AG (@box A AG (@ageM A AG) (@wand A JA PA AG XA P Q)) a *)
  apply nec_refl_or_later in H1.
(* Goal: @app_pred A AG Q a' *)
(* Goal: @app_pred A AG Q a' *)
(* Goal: @app_pred A AG (@box A AG (@ageM A AG) (@wand A JA PA AG XA P Q)) a *)
  destruct H1; subst.
(* Goal: @app_pred A AG Q a' *)
(* Goal: @app_pred A AG Q a' *)
(* Goal: @app_pred A AG (@box A AG (@ageM A AG) (@wand A JA PA AG XA P Q)) a *)
  destruct (age1_join2 _ H2 H4) as [w [v [? [? ?]]]].
(* Goal: @join A JA w1 w5 w3 *)
  eapply H0; eauto.
(* Goal: @join A JA w1 w5 w3 *)
  replace a0 with w; auto.
(* Goal: @eq A y a'0 *)
  congruence.
(* Goal: @app_pred A AG Q a' *)
(* Goal: @app_pred A AG Q a' *)
(* Goal: @app_pred A AG (@box A AG (@ageM A AG) (@wand A JA PA AG XA P Q)) a *)
  assert (necR a0 x').
(* Goal: @join A JA w1 w5 w3 *)
  eapply age_later_nec; eauto.
(* Goal: @app_pred A AG Q a' *)
(* Goal: @app_pred A AG Q a' *)
(* Goal: @app_pred A AG (@box A AG (@ageM A AG) (@wand A JA PA AG XA P Q)) a *)
  destruct (age1_join2 _ H2 H4) as [w [v [? [? ?]]]].
(* Goal: @join A JA w1 w5 w3 *)
  apply H0 with w v; auto.
(* Goal: @join A JA w1 w5 w3 *)
  apply rt_trans with x'; auto.
(* Goal: @join A JA w1 w5 w3 *)
  apply rt_step; auto.
(* Goal: @app_pred A AG Q a' *)
(* Goal: @app_pred A AG Q a' *)
(* Goal: @app_pred A AG (@box A AG (@ageM A AG) (@wand A JA PA AG XA P Q)) a *)
  apply nec_refl_or_later in H1; destruct H1; subst.
  destruct (age1_join2 _  H2 H4) as [w [v [? [? ?]]]].
(* Goal: @app_pred A AG Q a' *)
(* Goal: @app_pred A AG Q a' *)
(* Goal: @app_pred A AG (@box A AG (@ageM A AG) (@wand A JA PA AG XA P Q)) a *)
  hnf in H6.
(* Goal: @app_pred A AG Q a' *)
(* Goal: @app_pred A AG Q a' *)
(* Goal: @app_pred A AG (@box A AG (@ageM A AG) (@wand A JA PA AG XA P Q)) a *)
  rewrite H5 in H6; discriminate.
(* Goal: @app_pred A AG Q a' *)
(* Goal: @app_pred A AG (@box A AG (@ageM A AG) (@wand A JA PA AG XA P Q)) a *)
  clear -H1 H5.
(* Goal: @app_pred A AG Q a' *)
(* Goal: @app_pred A AG (@box A AG (@ageM A AG) (@wand A JA PA AG XA P Q)) a *)
  elimtype False.
(* Goal: @join A JA w1 w5 w3 *)
  revert H5; induction H1; auto.
(* Goal: forall P Q R : @pred T agT, @derives T agT (@andp T agT (@sepcon T JT PT agT AT P Q) (@ewand T JT PT agT AT R (@prop T agT True))) (@sepcon T JT PT agT AT (@andp T agT P (@ewand T JT PT agT AT R (@prop T agT True))) (@andp T agT Q (@ewand T JT PT agT AT R (@prop T agT True)))) *)
  intros.
(* Goal: False *)
(* Goal: @app_pred A AG (@box A AG (@ageM A AG) (@wand A JA PA AG XA P Q)) a *)
  unfold age in H.
(* Goal: False *)
(* Goal: @app_pred A AG (@box A AG (@ageM A AG) (@wand A JA PA AG XA P Q)) a *)
  rewrite H in H5; discriminate.

(* Goal: forall P Q R : @pred T agT, @derives T agT (@andp T agT (@sepcon T JT PT agT AT P Q) (@ewand T JT PT agT AT R (@prop T agT True))) (@sepcon T JT PT agT AT (@andp T agT P (@ewand T JT PT agT AT R (@prop T agT True))) (@andp T agT Q (@ewand T JT PT agT AT R (@prop T agT True)))) *)
  simpl; intros.
(* Goal: @ex A (fun phi2' : A => and (@eq (option A) (@ageN A AG (S n) phi2) (@Some A phi2')) (@comparable A JA SA phi1' phi2')) *)
  simpl in H0.
(* Goal: @app_pred A AG Q z *)
  destruct (valid_rel_nec).
(* Goal: @app_pred A AG Q z *)
  destruct (H6 _ _ H2 _ H1).
(* Goal: @app_pred A AG Q z *)
  destruct (unage_join _ H3 H7) as [w [v [? [? ?]]]].
(* Goal: @join A JA w1 w5 w3 *)
  apply H0 with x w v; auto.
(* Goal: forall P Q R : @pred T agT, @derives T agT (@andp T agT (@sepcon T JT PT agT AT P Q) (@ewand T JT PT agT AT R (@prop T agT True))) (@sepcon T JT PT agT AT (@andp T agT P (@ewand T JT PT agT AT R (@prop T agT True))) (@andp T agT Q (@ewand T JT PT agT AT R (@prop T agT True)))) *)
  intros.
(* Goal: @join A JA w1 w5 w3 *)
  replace a'0 with y; auto.
(* Goal: @eq A y a'0 *)
  congruence.
Qed.

Lemma later_sepcon {A} {JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A}{AG: ageable A}{XA: Age_alg A} : forall P Q,
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@box A AG (@ageM A AG) P) (@box A AG (@ageM A AG) Q)) a *)
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@box A AG (@ageM A AG) P) (@box A AG (@ageM A AG) Q)) a *)
(* Goal: @app_pred A AG (@box A AG (@ageM A AG) (@sepcon A JA PA AG XA P Q)) a *)
  (|>(P * Q) = |>P * |>Q)%pred.
Proof.
(* Goal: forall P Q : @pred A AG, @eq (@pred A AG) (@box A AG (@laterM A AG) (@sepcon A JA PA AG XA P Q)) (@sepcon A JA PA AG XA (@box A AG (@laterM A AG) P) (@box A AG (@laterM A AG) Q)) *)
  pose (H:=True).
(* Goal: forall P Q R : @pred T agT, @derives T agT (@andp T agT (@sepcon T JT PT agT AT P Q) (@ewand T JT PT agT AT R (@prop T agT True))) (@sepcon T JT PT agT AT (@andp T agT P (@ewand T JT PT agT AT R (@prop T agT True))) (@andp T agT Q (@ewand T JT PT agT AT R (@prop T agT True)))) *)
  intros.
(* Goal: @eq (@pred A AG) (@box A AG (@laterM A AG) (@sepcon A JA PA AG XA P Q)) (@sepcon A JA PA AG XA (@box A AG (@laterM A AG) P) (@box A AG (@laterM A AG) Q)) *)
  repeat rewrite later_age.
(* Goal: forall P Q R : @pred T agT, @derives T agT (@andp T agT (@sepcon T JT PT agT AT P Q) (@ewand T JT PT agT AT R (@prop T agT True))) (@sepcon T JT PT agT AT (@andp T agT P (@ewand T JT PT agT AT R (@prop T agT True))) (@andp T agT Q (@ewand T JT PT agT AT R (@prop T agT True)))) *)
  apply pred_ext; hnf; intros.
(* Goal: @ex A (fun phi2' : A => and (@eq (option A) (@ageN A AG (S n) phi2) (@Some A phi2')) (@comparable A JA SA phi1' phi2')) *)
  simpl in H0.
(* Goal: forall P Q R : @pred T agT, @derives T agT (@andp T agT (@sepcon T JT PT agT AT P Q) (@ewand T JT PT agT AT R (@prop T agT True))) (@sepcon T JT PT agT AT (@andp T agT P (@ewand T JT PT agT AT R (@prop T agT True))) (@andp T agT Q (@ewand T JT PT agT AT R (@prop T agT True)))) *)
  case_eq (age1 a); intros.
(* Goal: @join A JA w1 w5 w3 *)
  destruct (H0 a0) as [w [v [? [? ?]]]]; auto.
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@box A AG (@ageM A AG) P) (@box A AG (@ageM A AG) Q)) a *)
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@box A AG (@ageM A AG) P) (@box A AG (@ageM A AG) Q)) a *)
(* Goal: @app_pred A AG (@box A AG (@ageM A AG) (@sepcon A JA PA AG XA P Q)) a *)
  destruct (unage_join2 _ H2 H1) as [w' [v' [? [? ?]]]].
(* Goal: and (@join A JA x a a) (and (@app_pred A AG (@box A AG (@ageM A AG) P) x) (@app_pred A AG (@box A AG (@ageM A AG) Q) a)) *)
(* Goal: @app_pred A AG (@box A AG (@ageM A AG) (@sepcon A JA PA AG XA P Q)) a *)
  exists w'; exists v'; intuition.
(* Goal: forall P Q R : @pred T agT, @derives T agT (@andp T agT (@sepcon T JT PT agT AT P Q) (@ewand T JT PT agT AT R (@prop T agT True))) (@sepcon T JT PT agT AT (@andp T agT P (@ewand T JT PT agT AT R (@prop T agT True))) (@andp T agT Q (@ewand T JT PT agT AT R (@prop T agT True)))) *)
  simpl; intros.
(* Goal: @join A JA w1 w5 w3 *)
  replace a' with w; auto.
(* Goal: @eq A v a' *)
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@box A AG (@ageM A AG) P) (@box A AG (@ageM A AG) Q)) a *)
(* Goal: @app_pred A AG (@box A AG (@ageM A AG) (@sepcon A JA PA AG XA P Q)) a *)
  unfold age in *; congruence.
(* Goal: forall P Q R : @pred T agT, @derives T agT (@andp T agT (@sepcon T JT PT agT AT P Q) (@ewand T JT PT agT AT R (@prop T agT True))) (@sepcon T JT PT agT AT (@andp T agT P (@ewand T JT PT agT AT R (@prop T agT True))) (@andp T agT Q (@ewand T JT PT agT AT R (@prop T agT True)))) *)
  simpl; intros.
(* Goal: @join A JA w1 w5 w3 *)
  replace a' with v; auto.
(* Goal: @eq A v a' *)
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@box A AG (@ageM A AG) P) (@box A AG (@ageM A AG) Q)) a *)
(* Goal: @app_pred A AG (@box A AG (@ageM A AG) (@sepcon A JA PA AG XA P Q)) a *)
  unfold age in *; congruence.
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@box A AG (@ageM A AG) P) (@box A AG (@ageM A AG) Q)) a *)
(* Goal: @app_pred A AG (@box A AG (@ageM A AG) (@sepcon A JA PA AG XA P Q)) a *)
  destruct (join_ex_units a).
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@box A AG (@ageM A AG) P) (@box A AG (@ageM A AG) Q)) a *)
(* Goal: @app_pred A AG (@box A AG (@ageM A AG) (@sepcon A JA PA AG XA P Q)) a *)
  exists x; exists a.
(* Goal: and (@join A JA x a a) (and (@app_pred A AG (@box A AG (@ageM A AG) P) x) (@app_pred A AG (@box A AG (@ageM A AG) Q) a)) *)
(* Goal: @app_pred A AG (@box A AG (@ageM A AG) (@sepcon A JA PA AG XA P Q)) a *)
  intuition.
(* Goal: forall P Q R : @pred T agT, @derives T agT (@andp T agT (@sepcon T JT PT agT AT P Q) (@ewand T JT PT agT AT R (@prop T agT True))) (@sepcon T JT PT agT AT (@andp T agT P (@ewand T JT PT agT AT R (@prop T agT True))) (@andp T agT Q (@ewand T JT PT agT AT R (@prop T agT True)))) *)
  hnf; intros.
(* Goal: @app_pred A AG P a' *)
(* Goal: @app_pred A AG (@box A AG (@ageM A AG) Q) a *)
(* Goal: @app_pred A AG (@box A AG (@ageM A AG) (@sepcon A JA PA AG XA P Q)) a *)
  red in u.
(* Goal: @app_pred A AG Q a' *)
(* Goal: @app_pred A AG (@box A AG (@ageM A AG) (@sepcon A JA PA AG XA P Q)) a *)
  simpl in H2.
(* Goal: @app_pred A AG P a' *)
(* Goal: @app_pred A AG (@box A AG (@ageM A AG) Q) a *)
(* Goal: @app_pred A AG (@box A AG (@ageM A AG) (@sepcon A JA PA AG XA P Q)) a *)
  destruct (age1_join _ u H2) as [s [t [? [? ?]]]].
(* Goal: @app_pred A AG P a' *)
(* Goal: @app_pred A AG (@box A AG (@ageM A AG) Q) a *)
(* Goal: @app_pred A AG (@box A AG (@ageM A AG) (@sepcon A JA PA AG XA P Q)) a *)
  unfold age in H5.
(* Goal: @app_pred A AG P a' *)
(* Goal: @app_pred A AG (@box A AG (@ageM A AG) Q) a *)
(* Goal: @app_pred A AG (@box A AG (@ageM A AG) (@sepcon A JA PA AG XA P Q)) a *)
  rewrite H1 in H5; discriminate.
(* Goal: forall P Q R : @pred T agT, @derives T agT (@andp T agT (@sepcon T JT PT agT AT P Q) (@ewand T JT PT agT AT R (@prop T agT True))) (@sepcon T JT PT agT AT (@andp T agT P (@ewand T JT PT agT AT R (@prop T agT True))) (@andp T agT Q (@ewand T JT PT agT AT R (@prop T agT True)))) *)
  hnf; intros.
(* Goal: @app_pred A AG Q a' *)
(* Goal: @app_pred A AG (@box A AG (@ageM A AG) (@sepcon A JA PA AG XA P Q)) a *)
  simpl in H2.
(* Goal: @app_pred A AG Q a' *)
(* Goal: @app_pred A AG (@box A AG (@ageM A AG) (@sepcon A JA PA AG XA P Q)) a *)
  unfold age in H2.
(* Goal: @app_pred A AG Q a' *)
(* Goal: @app_pred A AG (@box A AG (@ageM A AG) (@sepcon A JA PA AG XA P Q)) a *)
  rewrite H1 in H2; discriminate.

(* Goal: @app_pred A AG (@box A AG (@ageM A AG) (@sepcon A JA PA AG XA P Q)) a *)
  destruct H0 as [w [v [? [? ?]]]].
(* Goal: forall P Q R : @pred T agT, @derives T agT (@andp T agT (@sepcon T JT PT agT AT P Q) (@ewand T JT PT agT AT R (@prop T agT True))) (@sepcon T JT PT agT AT (@andp T agT P (@ewand T JT PT agT AT R (@prop T agT True))) (@andp T agT Q (@ewand T JT PT agT AT R (@prop T agT True)))) *)
  hnf; intros.
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA P Q) a' *)
  simpl in H3.
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA P Q) a' *)
  destruct (age1_join2 _ H0 H3) as [w' [v' [? [? ?]]]].
(* Goal: and (@join A JA x a a) (and (@app_pred A AG (@box A AG (@ageM A AG) P) x) (@app_pred A AG (@box A AG (@ageM A AG) Q) a)) *)
(* Goal: @app_pred A AG (@box A AG (@ageM A AG) (@sepcon A JA PA AG XA P Q)) a *)
  exists w'; exists v'; intuition.
Qed.

Lemma FF_sepcon : forall {A}{JA: Join A}{PA: Perm_alg A}{AG: ageable A}{XA: Age_alg A} (P:pred A),
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@box A AG (@ageM A AG) P) (@box A AG (@ageM A AG) Q)) a *)
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@box A AG (@ageM A AG) P) (@box A AG (@ageM A AG) Q)) a *)
(* Goal: @app_pred A AG (@box A AG (@ageM A AG) (@sepcon A JA PA AG XA P Q)) a *)
  (FF * P = FF)%pred.
Proof.
(* Goal: @precise A JA PA SA AG XA (@emp A JA PA SA AG XA) *)
  intros. apply pred_ext; repeat intro.
(* Goal: @app_pred A AG (@FF A AG) a *)
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@FF A AG) P) a *)
  destruct H as [? [? [? [? ?]]]].  elim H0.
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@FF A AG) P) a *)
  elim H.
Qed.

Lemma sepcon_derives {A} {JA: Join A}{PA: Perm_alg A}{AG: ageable A}{XA: Age_alg A}:
  forall p q p' q', (p |-- p') -> (q |-- q') -> (p * q |-- p' * q').
Proof.
(* Goal: forall P Q R : @pred T agT, @derives T agT (@andp T agT (@sepcon T JT PT agT AT P Q) (@ewand T JT PT agT AT R (@prop T agT True))) (@sepcon T JT PT agT AT (@andp T agT P (@ewand T JT PT agT AT R (@prop T agT True))) (@andp T agT Q (@ewand T JT PT agT AT R (@prop T agT True)))) *)
intros.
(* Goal: @derives A AG (@sepcon A JA PA AG XA p q) (@sepcon A JA PA AG XA p' q') *)
do 2 intro.
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA p' q') a *)
destruct H1 as [w1 [w2 [? [? ?]]]].
(* Goal: @join A JA w1 w5 w3 *)
exists w1; exists w2; repeat split ;auto.
Qed.

Lemma exp_sepcon1 {A}  {JA: Join A}{PA: Perm_alg A}{AG: ageable A}{XA: Age_alg A}:
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@box A AG (@ageM A AG) P) (@box A AG (@ageM A AG) Q)) a *)
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@box A AG (@ageM A AG) P) (@box A AG (@ageM A AG) Q)) a *)
(* Goal: @app_pred A AG (@box A AG (@ageM A AG) (@sepcon A JA PA AG XA P Q)) 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 agT, @derives T agT (@andp T agT (@sepcon T JT PT agT AT P Q) (@ewand T JT PT agT AT R (@prop T agT True))) (@sepcon T JT PT agT AT (@andp T agT P (@ewand T JT PT agT AT R (@prop T agT True))) (@andp T agT Q (@ewand T JT PT agT AT R (@prop T agT True)))) *)
intros.
(* Goal: @eq (@pred A AG) (@sepcon A JA PA AG XA P (@exp A AG T Q)) (@exp A AG T (fun x : T => @sepcon A JA PA AG XA P (Q x))) *)
apply pred_ext; intros ? ?.
(* Goal: @app_pred A AG (@exp A AG T (fun x : T => @sepcon A JA PA AG XA (P x) Q)) a *)
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@exp A AG T P) Q) a *)
destruct H as [w1 [w2 [? [[x ?] ?]]]].
(* Goal: @join A JA w1 w5 w3 *)
exists x; exists w1; exists w2; split; auto.
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA P (@exp A AG T Q)) a *)
destruct H as [x [w1 [w2 [? [? ?]]]]].
(* Goal: @join A JA w1 w5 w3 *)
exists w1; exists w2; split; auto.
(* Goal: @join A JA w1 w5 w3 *)
split; auto.
(* Goal: @join A JA w1 w5 w3 *)
exists x; auto.
Qed.

Lemma exp_sepcon2 {A}  {JA: Join A}{PA: Perm_alg A}{AG: ageable A}{XA: Age_alg A}:
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@box A AG (@ageM A AG) P) (@box A AG (@ageM A AG) Q)) a *)
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@box A AG (@ageM A AG) P) (@box A AG (@ageM A AG) Q)) a *)
(* Goal: @app_pred A AG (@box A AG (@ageM A AG) (@sepcon A JA PA AG XA P Q)) a *)
  forall T (P: pred A) (Q: T -> pred A),  (P * exp Q = exp (fun x => P * Q x))%pred.
Proof.
(* Goal: forall P Q R : @pred T agT, @derives T agT (@andp T agT (@sepcon T JT PT agT AT P Q) (@ewand T JT PT agT AT R (@prop T agT True))) (@sepcon T JT PT agT AT (@andp T agT P (@ewand T JT PT agT AT R (@prop T agT True))) (@andp T agT Q (@ewand T JT PT agT AT R (@prop T agT True)))) *)
intros.
(* Goal: @eq (@pred A AG) (@sepcon A JA PA AG XA P (@exp A AG T Q)) (@exp A AG T (fun x : T => @sepcon A JA PA AG XA P (Q x))) *)
apply pred_ext; intros ? ?.
(* Goal: @app_pred A AG (@exp A AG T (fun x : T => @sepcon A JA PA AG XA P (Q x))) a *)
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA P (@exp A AG T Q)) a *)
destruct H as [w1 [w2 [? [? [x ?]]]]].
(* Goal: @join A JA w1 w5 w3 *)
exists x; exists w1; exists w2; split; auto.
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA P (@exp A AG T Q)) a *)
destruct H as [x [w1 [w2 [? [? ?]]]]].
(* Goal: @join A JA w1 w5 w3 *)
exists w1; exists w2; split; auto.
(* Goal: @join A JA w1 w5 w3 *)
split; auto.
(* Goal: @join A JA w1 w5 w3 *)
exists x; auto.
Qed.

(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@box A AG (@ageM A AG) P) (@box A AG (@ageM A AG) Q)) a *)
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@box A AG (@ageM A AG) P) (@box A AG (@ageM A AG) Q)) a *)
(* Goal: @app_pred A AG (@box A AG (@ageM A AG) (@sepcon A JA PA AG XA P Q)) a *)
Lemma extend_later {A}  {JA: Join A}{PA: Perm_alg A}{AG: ageable A}{XA: Age_alg A}: forall P, (%|>P = |>%P)%pred.
Proof.
(* Goal: @join A JA w1 w5 w3 *)
  intros; rewrite later_commute; auto.
Qed.

Lemma extend_later' {A}{JA: Join A}{PA: Perm_alg A}{agA: ageable A}{AgeA: Age_alg A}: forall P, boxy extendM P -> boxy extendM (|> P).
Proof.
(* Goal: @join A JA w1 w5 w3 *)
intros. unfold boxy in *. rewrite later_commute. rewrite H. auto.
Qed.
Hint Resolve @extend_later'.

Lemma age_sepcon {A}  {JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A}{AG: ageable A}{XA: Age_alg A} :
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@box A AG (@ageM A AG) P) (@box A AG (@ageM A AG) Q)) a *)
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@box A AG (@ageM A AG) P) (@box A AG (@ageM A AG) Q)) a *)
(* Goal: @app_pred A AG (@box A AG (@ageM A AG) (@sepcon A JA PA AG XA P Q)) a *)
      forall P Q, (box ageM (P * Q) = box ageM P * box ageM Q)%pred.
Proof.
(* Goal: forall (G P Q : @pred A AG) (_ : @superprecise A JA PA SA AG XA G) (_ : @eq (@pred A AG) P (@ewand A JA PA AG XA G (@sepcon A JA PA AG XA G P))), @derives A AG (@andp A AG (@sepcon A JA PA AG XA P Q) (@sepcon A JA PA AG XA G (@TT A AG))) (@sepcon A JA PA AG XA (@sepcon A JA PA AG XA P G) (@ewand A JA PA AG XA G Q)) *)
  pose proof I.
(* Goal: forall P Q R : @pred T agT, @derives T agT (@andp T agT (@sepcon T JT PT agT AT P Q) (@ewand T JT PT agT AT R (@prop T agT True))) (@sepcon T JT PT agT AT (@andp T agT P (@ewand T JT PT agT AT R (@prop T agT True))) (@andp T agT Q (@ewand T JT PT agT AT R (@prop T agT True)))) *)
  intros.
(* Goal: forall P Q R : @pred T agT, @derives T agT (@andp T agT (@sepcon T JT PT agT AT P Q) (@ewand T JT PT agT AT R (@prop T agT True))) (@sepcon T JT PT agT AT (@andp T agT P (@ewand T JT PT agT AT R (@prop T agT True))) (@andp T agT Q (@ewand T JT PT agT AT R (@prop T agT True)))) *)
  apply pred_ext; hnf; intros.
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@box A AG (@ageM A AG) P) (@box A AG (@ageM A AG) Q)) a *)
(* Goal: @app_pred A AG (@box A AG (@ageM A AG) (@sepcon A JA PA AG XA P Q)) a *)
  hnf in H0.
(* Goal: forall P Q R : @pred T agT, @derives T agT (@andp T agT (@sepcon T JT PT agT AT P Q) (@ewand T JT PT agT AT R (@prop T agT True))) (@sepcon T JT PT agT AT (@andp T agT P (@ewand T JT PT agT AT R (@prop T agT True))) (@andp T agT Q (@ewand T JT PT agT AT R (@prop T agT True)))) *)
  case_eq (age1 a); intros.
(* Goal: @join A JA w1 w5 w3 *)
  destruct (H0 a0) as [u [v [? [? ?]]]]; auto.
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@box A AG (@ageM A AG) P) (@box A AG (@ageM A AG) Q)) a *)
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@box A AG (@ageM A AG) P) (@box A AG (@ageM A AG) Q)) a *)
(* Goal: @app_pred A AG (@box A AG (@ageM A AG) (@sepcon A JA PA AG XA P Q)) a *)
  red.
(* Goal: @proj1_sig (forall _ : A, Prop) (fun p : forall _ : A, Prop => @hereditary A (@age A AG) p) (@sepcon A JA PA AG XA (@box A AG (@ageM A AG) P) (@box A AG (@ageM A AG) Q)) a *)
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@box A AG (@ageM A AG) P) (@box A AG (@ageM A AG) Q)) a *)
(* Goal: @app_pred A AG (@box A AG (@ageM A AG) (@sepcon A JA PA AG XA P Q)) a *)
  destruct (unage_join2 _ H2 H1) as [x [y [? [? ?]]]].
(* Goal: @proj1_sig (forall _ : A, Prop) (fun p : forall _ : A, Prop => @hereditary A (@age A AG) p) (@sepcon A JA PA AG XA (@box A AG (@ageM A AG) P) (@box A AG (@ageM A AG) Q)) a *)
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@box A AG (@ageM A AG) P) (@box A AG (@ageM A AG) Q)) a *)
(* Goal: @app_pred A AG (@box A AG (@ageM A AG) (@sepcon A JA PA AG XA P Q)) a *)
  exists x; exists y.
(* Goal: and (@join A JA x a a) (and (@app_pred A AG (@box A AG (@ageM A AG) P) x) (@app_pred A AG (@box A AG (@ageM A AG) Q) a)) *)
(* Goal: @app_pred A AG (@box A AG (@ageM A AG) (@sepcon A JA PA AG XA P Q)) a *)
  intuition.
(* Goal: forall P Q R : @pred T agT, @derives T agT (@andp T agT (@sepcon T JT PT agT AT P Q) (@ewand T JT PT agT AT R (@prop T agT True))) (@sepcon T JT PT agT AT (@andp T agT P (@ewand T JT PT agT AT R (@prop T agT True))) (@andp T agT Q (@ewand T JT PT agT AT R (@prop T agT True)))) *)
  hnf; intros.
(* Goal: @join A JA w1 w5 w3 *)
  replace a' with u; auto.
(* Goal: @eq A v a' *)
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@box A AG (@ageM A AG) P) (@box A AG (@ageM A AG) Q)) a *)
(* Goal: @app_pred A AG (@box A AG (@ageM A AG) (@sepcon A JA PA AG XA P Q)) a *)
  unfold age in *; congruence.
(* Goal: forall P Q R : @pred T agT, @derives T agT (@andp T agT (@sepcon T JT PT agT AT P Q) (@ewand T JT PT agT AT R (@prop T agT True))) (@sepcon T JT PT agT AT (@andp T agT P (@ewand T JT PT agT AT R (@prop T agT True))) (@andp T agT Q (@ewand T JT PT agT AT R (@prop T agT True)))) *)
  hnf; intros.
(* Goal: @join A JA w1 w5 w3 *)
  replace a' with v; auto.
(* Goal: @eq A v a' *)
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@box A AG (@ageM A AG) P) (@box A AG (@ageM A AG) Q)) a *)
(* Goal: @app_pred A AG (@box A AG (@ageM A AG) (@sepcon A JA PA AG XA P Q)) a *)
  unfold age in *; congruence.
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@box A AG (@ageM A AG) P) (@box A AG (@ageM A AG) Q)) a *)
(* Goal: @app_pred A AG (@box A AG (@ageM A AG) (@sepcon A JA PA AG XA P Q)) a *)
  destruct (join_ex_units a).
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@box A AG (@ageM A AG) P) (@box A AG (@ageM A AG) Q)) a *)
(* Goal: @app_pred A AG (@box A AG (@ageM A AG) (@sepcon A JA PA AG XA P Q)) a *)
  exists x; exists a.
(* Goal: and (@join A JA x a a) (and (@app_pred A AG (@box A AG (@ageM A AG) P) x) (@app_pred A AG (@box A AG (@ageM A AG) Q) a)) *)
(* Goal: @app_pred A AG (@box A AG (@ageM A AG) (@sepcon A JA PA AG XA P Q)) a *)
  intuition.
(* Goal: forall P Q R : @pred T agT, @derives T agT (@andp T agT (@sepcon T JT PT agT AT P Q) (@ewand T JT PT agT AT R (@prop T agT True))) (@sepcon T JT PT agT AT (@andp T agT P (@ewand T JT PT agT AT R (@prop T agT True))) (@andp T agT Q (@ewand T JT PT agT AT R (@prop T agT True)))) *)
  hnf; intros.
(* Goal: @app_pred A AG P a' *)
(* Goal: @app_pred A AG (@box A AG (@ageM A AG) Q) a *)
(* Goal: @app_pred A AG (@box A AG (@ageM A AG) (@sepcon A JA PA AG XA P Q)) a *)
  red in u.
  destruct (age1_join _ u H2)
(* Goal: @join A JA w1 w5 w3 *)
    as [p [q [? [? ?]]]]; auto.
(* Goal: @app_pred A AG Q a' *)
(* Goal: @app_pred A AG (@box A AG (@ageM A AG) (@sepcon A JA PA AG XA P Q)) a *)
  unfold age in *.
(* Goal: @app_pred A AG P a' *)
(* Goal: @app_pred A AG (@box A AG (@ageM A AG) Q) a *)
(* Goal: @app_pred A AG (@box A AG (@ageM A AG) (@sepcon A JA PA AG XA P Q)) a *)
  rewrite H1 in H4; discriminate.
(* Goal: forall P Q R : @pred T agT, @derives T agT (@andp T agT (@sepcon T JT PT agT AT P Q) (@ewand T JT PT agT AT R (@prop T agT True))) (@sepcon T JT PT agT AT (@andp T agT P (@ewand T JT PT agT AT R (@prop T agT True))) (@andp T agT Q (@ewand T JT PT agT AT R (@prop T agT True)))) *)
  hnf; intros.
(* Goal: @app_pred A AG Q a' *)
(* Goal: @app_pred A AG (@box A AG (@ageM A AG) (@sepcon A JA PA AG XA P Q)) a *)
  simpl in *.
(* Goal: @app_pred A AG Q a' *)
(* Goal: @app_pred A AG (@box A AG (@ageM A AG) (@sepcon A JA PA AG XA P Q)) a *)
  unfold age in *.
(* Goal: @app_pred A AG Q a' *)
(* Goal: @app_pred A AG (@box A AG (@ageM A AG) (@sepcon A JA PA AG XA P Q)) a *)
  rewrite H1 in H2; discriminate.

(* Goal: @app_pred A AG (@box A AG (@ageM A AG) (@sepcon A JA PA AG XA P Q)) a *)
  destruct H0 as [u [v [? [? ?]]]].
(* Goal: forall P Q R : @pred T agT, @derives T agT (@andp T agT (@sepcon T JT PT agT AT P Q) (@ewand T JT PT agT AT R (@prop T agT True))) (@sepcon T JT PT agT AT (@andp T agT P (@ewand T JT PT agT AT R (@prop T agT True))) (@andp T agT Q (@ewand T JT PT agT AT R (@prop T agT True)))) *)
  hnf; intros.
  destruct (age1_join2 _ H0 H3)
(* Goal: @join A JA w1 w5 w3 *)
    as [p [q [? [? ?]]]]; auto.
(* Goal: and (@join A JA x a a) (and (@app_pred A AG (@box A AG (@ageM A AG) P) x) (@app_pred A AG (@box A AG (@ageM A AG) Q) a)) *)
(* Goal: @app_pred A AG (@box A AG (@ageM A AG) (@sepcon A JA PA AG XA P Q)) a *)
  exists p; exists q; intuition.
Qed.


Lemma age_twin {A}  {JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A}{AG: ageable A}{XA: Age_alg A}:
  forall phi1 phi2 n phi1',
  comparable phi1 phi2 ->
  ageN n phi1 = Some phi1' ->
  exists phi2', ageN n phi2 = Some phi2' /\ comparable phi1' phi2'.
Proof.
(* Goal: forall (phi1 phi2 : A) (n : nat) (phi1' : A) (_ : @comparable A JA SA phi1 phi2) (_ : @eq (option A) (@ageN A AG n phi1) (@Some A phi1')), @ex A (fun phi2' : A => and (@eq (option A) (@ageN A AG n phi2) (@Some A phi2')) (@comparable A JA SA phi1' phi2')) *)
intros until n; revert n phi1 phi2.
(* Goal: forall P Q R : @pred T agT, @derives T agT (@andp T agT (@sepcon T JT PT agT AT P Q) (@ewand T JT PT agT AT R (@prop T agT True))) (@sepcon T JT PT agT AT (@andp T agT P (@ewand T JT PT agT AT R (@prop T agT True))) (@andp T agT Q (@ewand T JT PT agT AT R (@prop T agT True)))) *)
induction n; intros.
(* Goal: @ex A (fun phi2' : A => and (@eq (option A) (@ageN A AG O phi2) (@Some A phi2')) (@comparable A JA SA phi1' phi2')) *)
(* Goal: @ex A (fun phi2' : A => and (@eq (option A) (@ageN A AG (S n) phi2) (@Some A phi2')) (@comparable A JA SA phi1' phi2')) *)
exists phi2.
(* Goal: and (@eq (option A) (@ageN A AG (S n) phi2) (@Some A phi2')) (@comparable A JA SA phi1' phi2') *)
split; trivial.
(* Goal: @comparable A JA SA phi1' phi2 *)
(* Goal: @ex A (fun phi2' : A => and (@eq (option A) (@ageN A AG (S n) phi2) (@Some A phi2')) (@comparable A JA SA phi1' phi2')) *)
inversion H0.
(* Goal: @comparable A JA SA phi1' phi2 *)
(* Goal: @ex A (fun phi2' : A => and (@eq (option A) (@ageN A AG (S n) phi2) (@Some A phi2')) (@comparable A JA SA phi1' phi2')) *)
subst phi1'.
(* Goal: @eq (option A) (@composeOptN A (@age1 A AG) n ophi2) (@Some A phi2') *)
trivial.
(* Goal: @ex A (fun phi2' : A => and (@eq (option A) (@ageN A AG (S n) phi2) (@Some A phi2')) (@comparable A JA SA phi1' phi2')) *)
unfold ageN in H0.
(* Goal: @ex A (fun phi2' : A => and (@eq (option A) (@ageN A AG (S n) phi2) (@Some A phi2')) (@comparable A JA SA phi1' phi2')) *)
simpl in H0.
(* Goal: @ex A (fun phi2' : A => and (@eq (option A) (@ageN A AG (S n) phi2) (@Some A phi2')) (@comparable A JA SA phi1' phi2')) *)
revert H0; case_eq (age1 phi1); intros; try discriminate.
(* Goal: @ex A (fun phi2' : A => and (@eq (option A) (@ageN A AG (S n) phi2) (@Some A phi2')) (@comparable A JA SA phi1' phi2')) *)
rename a into phi.
(* Goal: @ex A (fun phi2' : A => and (@eq (option A) (@ageN A AG (S n) phi2) (@Some A phi2')) (@comparable A JA SA phi1' phi2')) *)
assert (exists ophi2, age phi2 ophi2 /\ comparable phi ophi2).
(* Goal: @ex A (fun ophi2 : A => and (@age A AG phi2 ophi2) (@comparable A JA SA phi ophi2)) *)
(* Goal: @ex A (fun phi2' : A => and (@eq (option A) (@ageN A AG (S n) phi2) (@Some A phi2')) (@comparable A JA SA phi1' phi2')) *)
destruct (comparable_common_unit H) as [e [? ?]].
(* Goal: @ex A (fun ophi2 : A => and (@age A AG phi2 ophi2) (@comparable A JA SA phi ophi2)) *)
(* Goal: @ex A (fun phi2' : A => and (@eq (option A) (@ageN A AG (S n) phi2) (@Some A phi2')) (@comparable A JA SA phi1' phi2')) *)
destruct (age1_join _ (join_comm H2) H0) as [eo [phi1'a [eof [? ?]]]].
(* Goal: @ex A (fun ophi2 : A => and (@age A AG phi2 ophi2) (@comparable A JA SA phi ophi2)) *)
(* Goal: @ex A (fun phi2' : A => and (@eq (option A) (@ageN A AG (S n) phi2) (@Some A phi2')) (@comparable A JA SA phi1' phi2')) *)
destruct (age1_join _ H3 H4) as [phi2' [phi2'a [eof' [? ?]]]].
(* Goal: @ex A (fun ophi2 : A => and (@age A AG phi2 ophi2) (@comparable A JA SA phi ophi2)) *)
(* Goal: @ex A (fun phi2' : A => and (@eq (option A) (@ageN A AG (S n) phi2) (@Some A phi2')) (@comparable A JA SA phi1' phi2')) *)
unfold age in H7. rewrite H6 in H7. symmetry in H7; inv H7.
(* Goal: @ex A (fun ophi2 : A => and (@age A AG phi2 ophi2) (@comparable A JA SA phi ophi2)) *)
(* Goal: @ex A (fun phi2' : A => and (@eq (option A) (@ageN A AG (S n) phi2) (@Some A phi2')) (@comparable A JA SA phi1' phi2')) *)
rewrite H5 in H0. inv H0.
(* Goal: @join A JA w1 w5 w3 *)
exists phi2'. split; auto.
(* Goal: @join A JA w1 w5 w3 *)
apply common_unit_comparable; exists eo; split; auto.
(* Goal: @ex A (fun phi2' : A => and (@eq (option A) (@ageN A AG (S n) phi2) (@Some A phi2')) (@comparable A JA SA phi1' phi2')) *)
destruct H2 as [ophi2 [? ?]].
(* Goal: @ex A (fun phi2' : A => and (@eq (option A) (@ageN A AG (S n) phi2) (@Some A phi2')) (@comparable A JA SA phi1' phi2')) *)
specialize (IHn _ _ _ H3 H1).
(* Goal: @ex A (fun phi2' : A => and (@eq (option A) (@ageN A AG (S n) phi2) (@Some A phi2')) (@comparable A JA SA phi1' phi2')) *)
destruct IHn as [phi2' [? ?]].
(* Goal: @ex A (fun phi2' : A => and (@eq (option A) (@ageN A AG (S n) phi2) (@Some A phi2')) (@comparable A JA SA phi1' phi2')) *)
exists phi2'.
(* Goal: and (@eq (option A) (@ageN A AG (S n) phi2) (@Some A phi2')) (@comparable A JA SA phi1' phi2') *)
split; trivial.
(* Goal: @eq (option A) (@ageN A AG (S n) phi2) (@Some A phi2') *)
unfold ageN.
(* Goal: @eq (option A) (@composeOptN A (@age1 A AG) (S n) phi2) (@Some A phi2') *)
simpl.
(* Goal: @eq (option A) match @age1 A AG phi2 with | Some w' => @composeOptN A (@age1 A AG) n w' | None => @None A end (@Some A phi2') *)
rewrite H2.
(* Goal: @eq (option A) (@composeOptN A (@age1 A AG) n ophi2) (@Some A phi2') *)
trivial.
Qed.

Lemma ageN_different {A} {JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A}{AG: ageable A}{XA: Age_alg A}: forall n phi phi', ageN (S n) phi = Some phi' ->
    ~ comparable phi phi'.
Proof.
(* Goal: forall P Q R : @pred T agT, @derives T agT (@andp T agT (@sepcon T JT PT agT AT P Q) (@ewand T JT PT agT AT R (@prop T agT True))) (@sepcon T JT PT agT AT (@andp T agT P (@ewand T JT PT agT AT R (@prop T agT True))) (@andp T agT Q (@ewand T JT PT agT AT R (@prop T agT True)))) *)
   intros.
(* Goal: not (@comparable A JA SA phi phi') *)
   intro.
(* Goal: False *)
   generalize (age_noetherian' phi); intros [k [[? [? ?]] H4]].
(* Goal: False *)
   assert (k <= n \/ k > n)%nat by omega.
(* Goal: False *)
   destruct H3.
(* Goal: False *)
(* Goal: False *)
   replace (S n) with (k + (S n - k))%nat in H by omega.
(* Goal: False *)
(* Goal: False *)
   destruct (ageN_compose' _ _ _ _ H) as [b [? ?]].
(* Goal: False *)
(* Goal: False *)
   rewrite H1 in H5; inv H5.
(* Goal: False *)
(* Goal: False *)
   replace (S n - k)%nat with (S (n-k))%nat in H6 by omega.
(* Goal: False *)
(* Goal: False *)
   unfold ageN in H6; simpl in H6. rewrite H2 in H6; inv H6.
(* Goal: False *)
   replace k with (S n + (k - S n))%nat in H1 by omega.
(* Goal: False *)
   destruct (ageN_compose' _ _ _ _ H1) as [c [? ?]].
(* Goal: False *)
   rewrite H in H5; inv H5.
(* Goal: False *)
   destruct (age_twin phi c _ _ H0 H1) as [b [? ?]].
(* Goal: False *)
   replace (S n + (k - S n))%nat with ((k - S n) + S n)%nat in H5 by omega.
(* Goal: False *)
   destruct (ageN_compose' _ _ _ _ H5) as [d [? ?]].
(* Goal: False *)
   rewrite H6 in H8; inv H8.
(* Goal: False *)
   clear - H9 H2.
   unfold ageN in H9; simpl  in H9; rewrite H2 in H9; inv H9.
Qed.

Lemma necR_comparable{A} {JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A}{AG: ageable A}{XA: Age_alg A}:
  forall w w', necR w w' -> comparable w w' -> w=w'.
Proof.
(* Goal: forall P Q R : @pred T agT, @derives T agT (@andp T agT (@sepcon T JT PT agT AT P Q) (@ewand T JT PT agT AT R (@prop T agT True))) (@sepcon T JT PT agT AT (@andp T agT P (@ewand T JT PT agT AT R (@prop T agT True))) (@andp T agT Q (@ewand T JT PT agT AT R (@prop T agT True)))) *)
intros.
(* Goal: @eq A w w' *)
rewrite necR_evolve in H.
(* Goal: @eq A w w' *)
destruct H as [n H].
(* Goal: @eq A w w' *)
destruct n.
(* Goal: @join A JA w1 w5 w3 *)
inv H; auto.
(* Goal: @join A JA w1 w5 w3 *)
contradiction (ageN_different _ _ _ H); auto.
Qed.


Lemma sepcon_andp_prop {A} {JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A}{AG: ageable A}{XA: Age_alg A}:
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@box A AG (@ageM A AG) P) (@box A AG (@ageM A AG) Q)) a *)
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@box A AG (@ageM A AG) P) (@box A AG (@ageM A AG) Q)) a *)
(* Goal: @app_pred A AG (@box A AG (@ageM A AG) (@sepcon A JA PA AG XA P Q)) a *)
  forall P Q R, (P * (!!Q && R) = !!Q && (P * R))%pred.
Proof.
(* Goal: forall P Q R : @pred T agT, @derives T agT (@andp T agT (@sepcon T JT PT agT AT P Q) (@ewand T JT PT agT AT R (@prop T agT True))) (@sepcon T JT PT agT AT (@andp T agT P (@ewand T JT PT agT AT R (@prop T agT True))) (@andp T agT Q (@ewand T JT PT agT AT R (@prop T agT True)))) *)
intros.
(* Goal: @eq (@pred A AG) (@sepcon A JA PA AG XA P (@andp A AG (@prop A AG Q) R)) (@andp A AG (@prop A AG Q) (@sepcon A JA PA AG XA P R)) *)
apply pred_ext; intros w ?.
(* Goal: @app_pred A AG (@andp A AG (@prop A AG Q) (@sepcon A JA PA AG XA P R)) w *)
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA P (@andp A AG (@prop A AG Q) R)) w *)
destruct H as [w1 [w2 [? [? [? ?]]]]].
(* Goal: @app_pred A AG (@andp A AG (@prop A AG Q) (@sepcon A JA PA AG XA P R)) w *)
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA P (@andp A AG (@prop A AG Q) R)) w *)
split. apply H1.
(* Goal: @join A JA w1 w5 w3 *)
exists w1; exists w2; split; [|split]; auto.
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA P (@andp A AG (@prop A AG Q) R)) w *)
destruct H.
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA P (@andp A AG (@prop A AG Q) R)) w *)
destruct H0 as [w1 [w2 [? [? ?]]]].
(* Goal: @join A JA w1 w5 w3 *)
exists w1; exists w2; repeat split; auto.
Qed.

(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@box A AG (@ageM A AG) P) (@box A AG (@ageM A AG) Q)) a *)
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@box A AG (@ageM A AG) P) (@box A AG (@ageM A AG) Q)) a *)
(* Goal: @app_pred A AG (@box A AG (@ageM A AG) (@sepcon A JA PA AG XA P Q)) a *)
Lemma TT_sepcon_TT {A} {JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A}{AG: ageable A}{XA: Age_alg A}: (TT * TT = TT)%pred.
Proof.
(* Goal: forall P Q R : @pred T agT, @derives T agT (@andp T agT (@sepcon T JT PT agT AT P Q) (@ewand T JT PT agT AT R (@prop T agT True))) (@sepcon T JT PT agT AT (@andp T agT P (@ewand T JT PT agT AT R (@prop T agT True))) (@andp T agT Q (@ewand T JT PT agT AT R (@prop T agT True)))) *)
intros.
(* Goal: @join A JA w1 w5 w3 *)
apply pred_ext; intros w ?; auto.
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@TT A AG) (@TT A AG)) w *)
destruct (join_ex_units w).
(* Goal: @join A JA w1 w5 w3 *)
exists x; exists w; split; auto.
Qed.


Lemma join_exactly {A}  {JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A}{AG: ageable A}{XA: Age_alg A}:
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@box A AG (@ageM A AG) P) (@box A AG (@ageM A AG) Q)) a *)
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@box A AG (@ageM A AG) P) (@box A AG (@ageM A AG) Q)) a *)
(* Goal: @app_pred A AG (@box A AG (@ageM A AG) (@sepcon A JA PA AG XA P Q)) a *)
  forall w1 w2 w3, join w1 w2 w3 ->  (exactly w1 * exactly w2 = exactly w3)%pred.
Proof.
(* Goal: forall (G P Q : @pred A AG) (_ : @superprecise A JA PA SA AG XA G) (_ : @eq (@pred A AG) P (@ewand A JA PA AG XA G (@sepcon A JA PA AG XA G P))), @derives A AG (@andp A AG (@sepcon A JA PA AG XA P Q) (@sepcon A JA PA AG XA G (@TT A AG))) (@sepcon A JA PA AG XA (@sepcon A JA PA AG XA P G) (@ewand A JA PA AG XA G Q)) *)
pose proof I.
(* Goal: forall P Q R : @pred T agT, @derives T agT (@andp T agT (@sepcon T JT PT agT AT P Q) (@ewand T JT PT agT AT R (@prop T agT True))) (@sepcon T JT PT agT AT (@andp T agT P (@ewand T JT PT agT AT R (@prop T agT True))) (@andp T agT Q (@ewand T JT PT agT AT R (@prop T agT True)))) *)
intros.
(* Goal: @eq (@pred A AG) (@sepcon A JA PA AG XA (@exactly A AG w1) (@exactly A AG w2)) (@exactly A AG w3) *)
unfold exactly.
(* Goal: @app_pred A AG Q a' *)
(* Goal: @app_pred A AG (@box A AG (@ageM A AG) (@sepcon A JA PA AG XA P Q)) a *)
apply pred_ext; intros w ?; simpl in *.
(* Goal: @necR A AG w3 w *)
(* Goal: @ex A (fun y : A => @ex A (fun z : A => and (@join A JA y z w) (and (@necR A AG w1 y) (@necR A AG w2 z)))) *)
destruct H1 as [? [? [? [? ?]]]].
(* Goal: @necR A AG w3 w *)
(* Goal: @ex A (fun y : A => @ex A (fun z : A => and (@join A JA y z w) (and (@necR A AG w1 y) (@necR A AG w2 z)))) *)
destruct (nec_join H0 H2) as [a [b [? [? ?]]]].
(* Goal: @necR A AG w3 w *)
(* Goal: @ex A (fun y : A => @ex A (fun z : A => and (@join A JA y z w) (and (@necR A AG w1 y) (@necR A AG w2 z)))) *)
assert (x0=a).
(* Goal: @join A JA w1 w5 w3 *)
 eapply necR_linear'; eauto.
(* Goal: @eq nat (@level A AG x0) (@level A AG a) *)
(* Goal: @necR A AG w3 w *)
(* Goal: @ex A (fun y : A => @ex A (fun z : A => and (@join A JA y z w) (and (@necR A AG w1 y) (@necR A AG w2 z)))) *)
  transitivity (level x).
(* Goal: @join A JA w1 w5 w3 *)
  symmetry; apply comparable_fashionR. eapply join_comparable2; eauto.
(* Goal: @join A JA w1 w5 w3 *)
  apply comparable_fashionR. eapply join_comparable2; eauto.
(* Goal: @necR A AG w3 w *)
(* Goal: @ex A (fun y : A => @ex A (fun z : A => and (@join A JA y z w) (and (@necR A AG w1 y) (@necR A AG w2 z)))) *)
subst x0.
(* Goal: @necR A AG w3 w *)
(* Goal: @ex A (fun y : A => @ex A (fun z : A => and (@join A JA y z w) (and (@necR A AG w1 y) (@necR A AG w2 z)))) *)
generalize (join_eq H4 H1); clear H4; intro; subst.
(* Goal: @join A JA w1 w5 w3 *)
auto.
(* Goal: @join A JA w1 w5 w3 *)
eapply nec_join2; eauto.
Qed.

Lemma extend_sepcon_andp {A} {JA: Join A}{PA: Perm_alg A}{AG: ageable A}{XA: Age_alg A}:
  forall P Q R, boxy extendM Q -> P * (Q && R) |-- Q && (P * R).
Proof.
(* Goal: forall P Q R : @pred T agT, @derives T agT (@andp T agT (@sepcon T JT PT agT AT P Q) (@ewand T JT PT agT AT R (@prop T agT True))) (@sepcon T JT PT agT AT (@andp T agT P (@ewand T JT PT agT AT R (@prop T agT True))) (@andp T agT Q (@ewand T JT PT agT AT R (@prop T agT True)))) *)
intros.
(* Goal: @derives A AG (@sepcon A JA PA AG XA P (@andp A AG Q R)) (@andp A AG Q (@sepcon A JA PA AG XA P R)) *)
intros ?w [?w [?w [? [? [? ?]]]]].
(* Goal: @app_pred A AG (@andp A AG (@prop A AG Q) (@sepcon A JA PA AG XA P R)) w *)
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA P (@andp A AG (@prop A AG Q) R)) w *)
split.
(* Goal: @app_pred A AG Q w *)
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA P R) w *)
rewrite <- H in H2.
(* Goal: @app_pred A AG Q w2' *)
(* Goal: @app_pred A AG (@ewand A JA PA AG XA P Q) z *)
eapply H2.
(* Goal: @app_mode A AG (@extendM A JA PA AG XA) w1 w *)
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA P R) w *)
exists w0.
(* Goal: @join A JA w1 w5 w3 *)
apply join_comm; auto.
(* Goal: @join A JA w1 w5 w3 *)
exists w0; exists w1; auto.
Qed.
Arguments extend_sepcon_andp : clear implicits.

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

Lemma modus_wand {A} {JA: Join A}{PA: Perm_alg A}{AG: ageable A}{XA: Age_alg A}:
  forall P Q,  P * (P -* Q) |-- Q.
Proof.
(* Goal: forall P Q R : @pred T agT, @derives T agT (@andp T agT (@sepcon T JT PT agT AT P Q) (@ewand T JT PT agT AT R (@prop T agT True))) (@sepcon T JT PT agT AT (@andp T agT P (@ewand T JT PT agT AT R (@prop T agT True))) (@andp T agT Q (@ewand T JT PT agT AT R (@prop T agT True)))) *)
intros.
intros w  [?w [?w [? [? ?]]]].
(* Goal: @join A JA w1 w5 w3 *)
eapply H1; eauto.
Qed.

Lemma extend_sepcon {A} {JA: Join A}{PA: Perm_alg A}{AG: ageable A}{XA: Age_alg A}:
  forall {Q R: pred A}, boxy extendM Q ->  Q * R |-- Q.
Proof.
(* Goal: forall P Q R : @pred T agT, @derives T agT (@andp T agT (@sepcon T JT PT agT AT P Q) (@ewand T JT PT agT AT R (@prop T agT True))) (@sepcon T JT PT agT AT (@andp T agT P (@ewand T JT PT agT AT R (@prop T agT True))) (@andp T agT Q (@ewand T JT PT agT AT R (@prop T agT True)))) *)
intros.
(* Goal: @derives A AG (@sepcon A JA PA AG XA Q R) Q *)
intros w [w1 [w2 [? [? _]]]].
(* Goal: @join A JA w1 w5 w3 *)
rewrite <- H in H1. eapply H1; eauto.
(* Goal: @join A JA w1 w5 w3 *)
simpl; eauto.
(* Goal: @join A JA w1 w5 w3 *)
exists w2; auto.
Qed.

Definition precise {A} {JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A}{AG: ageable A}{XA: Age_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}{SA: Sep_alg A}{AG: ageable A}{XA: Age_alg A} (P: pred A) : Prop :=
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@box A AG (@ageM A AG) P) (@box A AG (@ageM A AG) Q)) a *)
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@box A AG (@ageM A AG) P) (@box A AG (@ageM A AG) Q)) a *)
(* Goal: @app_pred A AG (@box A AG (@ageM A AG) (@sepcon A JA PA AG XA P Q)) a *)
     forall Q R, (P * (Q && R) = (P * Q) && (P * R))%pred.

Lemma precise_eq {A} {JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A}{CA: Canc_alg A}{AG: ageable A}{XA: Age_alg A}: precise =
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@box A AG (@ageM A AG) P) (@box A AG (@ageM A AG) Q)) a *)
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@box A AG (@ageM A AG) P) (@box A AG (@ageM A AG) Q)) a *)
(* Goal: @app_pred A AG (@box A AG (@ageM A AG) (@sepcon A JA PA AG XA P Q)) a *)
                 fun P : pred A => forall Q R, (P * (Q && R) = (P * Q) && (P * R))%pred.
Proof.
extensionality P.
(* Goal: forall (P : @pred A AG) (_ : @superprecise A JA PA SA AG XA P), @precise A JA PA SA AG XA P *)
unfold precise.
(* Goal: forall P Q R : @pred T agT, @derives T agT (@andp T agT (@sepcon T JT PT agT AT P Q) (@ewand T JT PT agT AT R (@prop T agT True))) (@sepcon T JT PT agT AT (@andp T agT P (@ewand T JT PT agT AT R (@prop T agT True))) (@andp T agT Q (@ewand T JT PT agT AT R (@prop T agT True)))) *)
apply prop_ext; split; intros.
apply pred_ext; unfold derives; intros; rename a into w.
destruct H0 as [phi1 [phi2 [? [? [? ?]]]]].
(* Goal: @join A JA w1 w5 w3 *)
split; exists phi1; exists phi2; auto.
destruct H0 as [[phi1a [phi2a [? [? ?]]]] [phi1b [phi2b [? [? ?]]]]].
specialize (H w _ _ H1 H4).
spec H.
(* Goal: @join A JA w1 w5 w3 *)
econstructor; eauto.
spec H.
(* Goal: @join A JA w1 w5 w3 *)
econstructor; eauto.
subst phi1b.
generalize (join_canc (join_comm H0) (join_comm H3)).
intro; subst phi2b.
(* Goal: @join A JA w1 w5 w3 *)
exists phi1a; exists phi2a; split; auto.
(* Goal: @join A JA w1 w5 w3 *)
split; auto.
(* Goal: @join A JA w1 w5 w3 *)
split; auto.
rename w1 into w1a.
rename w2 into w1b.
destruct H2 as [w2a ?].
destruct H3 as [w2b ?].
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@box A AG (@ageM A AG) P) (@box A AG (@ageM A AG) Q)) a *)
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@box A AG (@ageM A AG) P) (@box A AG (@ageM A AG) Q)) a *)
(* Goal: @app_pred A AG (@box A AG (@ageM A AG) (@sepcon A JA PA AG XA P Q)) a *)
assert (((P * exactly w2a) && (P * exactly w2b)) w)%pred.
split; do 2 econstructor; repeat split;
try solve [simpl; apply necR_refl].
(* Goal: @join A JA w1 w5 w3 *)
eassumption. auto. eassumption. auto.
rewrite <- H in H4.
destruct H4 as [w1 [w2 [? [? [? ?]]]]].
simpl in H6,H7.
rewrite (necR_comparable _ _ H6) in H2.
rewrite (necR_comparable _ _ H7) in H3.
(* Goal: @join A JA w1 w5 w3 *)
eapply join_canc; eauto.
(* Goal: @comparable A JA SA w2 w4 *)
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@sepcon A JA PA AG XA P G) (@exist (forall _ : A, Prop) (fun p : forall _ : A, Prop => @hereditary A (@age A AG) p) (fun w : A => @ex A (fun w1 : A => @ex A (fun w2 : A => and (@join A JA w1 w w2) (and (@app_pred A AG G w1) (@app_pred A AG Q w2))))) (ewand_obligation_1 A JA PA AG XA G Q))) w *)
apply comparable_trans with w.
(* Goal: @join A JA w1 w5 w3 *)
apply join_comparable with w1b; auto.
(* Goal: @join A JA w1 w5 w3 *)
apply comparable_sym; apply join_comparable with w1; auto.
(* Goal: @comparable A JA SA w2 w4 *)
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@sepcon A JA PA AG XA P G) (@exist (forall _ : A, Prop) (fun p : forall _ : A, Prop => @hereditary A (@age A AG) p) (fun w : A => @ex A (fun w1 : A => @ex A (fun w2 : A => and (@join A JA w1 w w2) (and (@app_pred A AG G w1) (@app_pred A AG Q w2))))) (ewand_obligation_1 A JA PA AG XA G Q))) w *)
apply comparable_trans with w.
(* Goal: @join A JA w1 w5 w3 *)
apply join_comparable with w1a; auto.
(* Goal: @join A JA w1 w5 w3 *)
apply comparable_sym; apply join_comparable with w1; auto.
Qed.

Lemma derives_precise {A} {JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A}{AG: ageable A}{XA: Age_alg A}:
  forall P Q, (P |-- Q) -> precise Q -> precise P.
Proof.
(* Goal: @join A JA w1 w5 w3 *)
intros; intro; intros; eauto.
Qed.

Lemma precise_emp {A} {JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A}{AG: ageable A}{XA: Age_alg A}: precise emp.
Proof.
(* Goal: @precise A JA PA SA AG XA (@emp A JA PA SA AG XA) *)
repeat intro.
(* Goal: @join A JA w1 w5 w3 *)
eapply join_sub_same_identity with (a := w1)(c := w); auto.
(* Goal: @join A JA w1 w5 w3 *)
apply identity_unit'; auto.
(* Goal: @join A JA w1 w5 w3 *)
eapply join_sub_unit_for; eauto.
(* Goal: @join A JA w1 w5 w3 *)
apply identity_unit'; auto.
Qed.

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

Lemma superprecise_exactly {A} {JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A}{AG: ageable A}{XA: Age_alg A}: forall w, superprecise (exactly w).
Proof.
(* Goal: forall P Q R : @pred T agT, @derives T agT (@andp T agT (@sepcon T JT PT agT AT P Q) (@ewand T JT PT agT AT R (@prop T agT True))) (@sepcon T JT PT agT AT (@andp T agT P (@ewand T JT PT agT AT R (@prop T agT True))) (@andp T agT Q (@ewand T JT PT agT AT R (@prop T agT True)))) *)
unfold superprecise; intros.
(* Goal: @eq A w1 w2 *)
hnf in H,H0.
(* Goal: @join A JA w1 w5 w3 *)
eapply necR_linear'; eauto.
(* Goal: @join A JA w1 w5 w3 *)
apply comparable_fashionR; auto.
Qed.
Hint Resolve @superprecise_exactly.

Lemma superprecise_precise {A} {JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A}{AG: ageable A}{XA: Age_alg A}: forall (P: pred A) , superprecise P -> precise P.
Proof.
(* Goal: forall (G P Q : @pred A AG) (_ : @superprecise A JA PA SA AG XA G) (_ : @eq (@pred A AG) P (@ewand A JA PA AG XA G (@sepcon A JA PA AG XA G P))), @derives A AG (@andp A AG (@sepcon A JA PA AG XA P Q) (@sepcon A JA PA AG XA G (@TT A AG))) (@sepcon A JA PA AG XA (@sepcon A JA PA AG XA P G) (@ewand A JA PA AG XA G Q)) *)
  pose proof I.
(* Goal: forall (P : @pred A AG) (_ : @superprecise A JA PA SA AG XA P), @precise A JA PA SA AG XA P *)
  unfold precise. unfold superprecise.
(* Goal: forall P Q R : @pred T agT, @derives T agT (@andp T agT (@sepcon T JT PT agT AT P Q) (@ewand T JT PT agT AT R (@prop T agT True))) (@sepcon T JT PT agT AT (@andp T agT P (@ewand T JT PT agT AT R (@prop T agT True))) (@andp T agT Q (@ewand T JT PT agT AT R (@prop T agT True)))) *)
  intros.
(* Goal: @eq A w1 w2 *)
  assert (comparable w1 w2). assert (comparable w1 w) by apply (join_sub_comparable H3).
(* Goal: @comparable A JA SA w1 w2 *)
(* Goal: @eq A w1 w2 *)
  assert (comparable w w2).
(* Goal: @join A JA w1 w5 w3 *)
    apply comparable_sym; destruct H4; eapply join_comparable; eauto.
(* Goal: @comparable A JA SA w1 w2 *)
(* Goal: @eq A w1 w2 *)
    apply (comparable_trans H5 H6).
(* Goal: @eq A w1 w2 *)
  apply (H0 _ _ H1 H2 H5).
Qed.

(* EXistential Magic Wand *)

Program Definition ewand {A} {JA: Join A}{PA: Perm_alg A}{AG: ageable A}{XA: Age_alg A} (P Q: pred A) : pred A :=
  fun w => exists w1, exists w2, join w1 w w2 /\ P w1 /\ Q w2.
Next Obligation.
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA P (@andp A AG (@prop A AG Q) R)) w *)
destruct H0 as [w1 [w2 [? [? ?]]]].
(* Goal: @join A JA w1 w5 w3 *)
apply join_comm in H0; eapply age1_join in H0; eauto.
(* Goal: @ex A (fun w1 : A => @ex A (fun w2 : A => and (@join A JA w1 a' w2) (and (@app_pred A AG P w1) (@app_pred A AG Q w2)))) *)
destruct H0 as [w1' [w3' [? [? ?]]]].
(* Goal: @join A JA w1 w5 w3 *)
exists w1'; exists w3'; split; auto.
split;   eapply pred_nec_hereditary; try eassumption.
(* Goal: @join A JA w1 w5 w3 *)
constructor 1; auto.
(* Goal: @join A JA w1 w5 w3 *)
constructor 1; auto.
Qed.

Lemma later_ewand {A} {JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A}{AG: ageable A}{XA: Age_alg A} : forall P Q,
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@box A AG (@ageM A AG) P) (@box A AG (@ageM A AG) Q)) a *)
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@box A AG (@ageM A AG) P) (@box A AG (@ageM A AG) Q)) a *)
(* Goal: @app_pred A AG (@box A AG (@ageM A AG) (@sepcon A JA PA AG XA P Q)) a *)
  (|>(ewand P Q) = ewand (|>P) (|>Q))%pred.
Proof.
(* Goal: forall P Q R : @pred T agT, @derives T agT (@andp T agT (@sepcon T JT PT agT AT P Q) (@ewand T JT PT agT AT R (@prop T agT True))) (@sepcon T JT PT agT AT (@andp T agT P (@ewand T JT PT agT AT R (@prop T agT True))) (@andp T agT Q (@ewand T JT PT agT AT R (@prop T agT True)))) *)
intros.
(* Goal: @eq (@pred A agA) (@sepcon A JA PA agA AgeA (@orp A agA P Q) R) (@orp A agA (@sepcon A JA PA agA AgeA P R) (@sepcon A JA PA agA AgeA Q R)) *)
apply pred_ext.
(* Goal: @derives A AG (@ewand A JA PA AG XA P (@sepcon A JA PA AG XA Q R)) (@sepcon A JA PA AG XA (@ewand A JA PA AG XA P Q) R) *)
intros w ?.
(* Goal: forall P Q R : @pred T agT, @derives T agT (@andp T agT (@sepcon T JT PT agT AT P Q) (@ewand T JT PT agT AT R (@prop T agT True))) (@sepcon T JT PT agT AT (@andp T agT P (@ewand T JT PT agT AT R (@prop T agT True))) (@andp T agT Q (@ewand T JT PT agT AT R (@prop T agT True)))) *)
case_eq (age1 w); intros.
(* Goal: @app_pred A AG (@ewand A JA PA AG XA (@box A AG (@laterM A AG) P) (@box A AG (@laterM A AG) Q)) w *)
(* Goal: @app_pred A AG (@ewand A JA PA AG XA (@box A AG (@laterM A AG) P) (@box A AG (@laterM A AG) Q)) w *)
(* Goal: @derives A AG (@ewand A JA PA AG XA (@box A AG (@laterM A AG) P) (@box A AG (@laterM A AG) Q)) (@box A AG (@laterM A AG) (@ewand A JA PA AG XA P Q)) *)
destruct (H a (t_step _ _ _ _ H0)) as [a1 [a2 [? [? ?]]]].
(* Goal: @app_pred A AG (@ewand A JA PA AG XA (@box A AG (@laterM A AG) P) (@box A AG (@laterM A AG) Q)) w *)
(* Goal: @app_pred A AG (@ewand A JA PA AG XA (@box A AG (@laterM A AG) P) (@box A AG (@laterM A AG) Q)) w *)
(* Goal: @derives A AG (@ewand A JA PA AG XA (@box A AG (@laterM A AG) P) (@box A AG (@laterM A AG) Q)) (@box A AG (@laterM A AG) (@ewand A JA PA AG XA P Q)) *)
destruct (unage_join _ (join_comm H1) H0) as [w1 [w2 [? [? ?]]]].
(* Goal: @join A JA w1 w5 w3 *)
exists w1; exists w2; split; [|split]; auto.
(* Goal: forall P Q R : @pred T agT, @derives T agT (@andp T agT (@sepcon T JT PT agT AT P Q) (@ewand T JT PT agT AT R (@prop T agT True))) (@sepcon T JT PT agT AT (@andp T agT P (@ewand T JT PT agT AT R (@prop T agT True))) (@andp T agT Q (@ewand T JT PT agT AT R (@prop T agT True)))) *)
hnf; intros.
(* Goal: @join A JA w1 w5 w3 *)
apply pred_nec_hereditary with a1; auto.
(* Goal: @join A JA w1 w5 w3 *)
eapply age_later_nec; eauto.
(* Goal: forall P Q R : @pred T agT, @derives T agT (@andp T agT (@sepcon T JT PT agT AT P Q) (@ewand T JT PT agT AT R (@prop T agT True))) (@sepcon T JT PT agT AT (@andp T agT P (@ewand T JT PT agT AT R (@prop T agT True))) (@andp T agT Q (@ewand T JT PT agT AT R (@prop T agT True)))) *)
hnf; intros.
(* Goal: @join A JA w1 w5 w3 *)
apply pred_nec_hereditary with a2; auto.
(* Goal: @join A JA w1 w5 w3 *)
eapply age_later_nec; eauto.
(* Goal: @app_pred A AG (@ewand A JA PA AG XA (@box A AG (@laterM A AG) P) (@box A AG (@laterM A AG) Q)) w *)
(* Goal: @derives A AG (@ewand A JA PA AG XA (@box A AG (@laterM A AG) P) (@box A AG (@laterM A AG) Q)) (@box A AG (@laterM A AG) (@ewand A JA PA AG XA P Q)) *)
exists (core w), w.
(* Goal: and (@join A JA (@core A JA SA w) w w) (and (@app_pred A AG (@box A AG (@laterM A AG) P) (@core A JA SA w)) (@app_pred A AG (@box A AG (@laterM A AG) Q) w)) *)
(* Goal: @derives A AG (@ewand A JA PA AG XA (@box A AG (@laterM A AG) P) (@box A AG (@laterM A AG) Q)) (@box A AG (@laterM A AG) (@ewand A JA PA AG XA P Q)) *)
split; [|split].
(* Goal: @join A JA (@core A JA SA w) w w *)
(* Goal: @app_pred A AG (@box A AG (@laterM A AG) P) (@core A JA SA w) *)
(* Goal: @app_pred A AG (@box A AG (@laterM A AG) Q) w *)
(* Goal: @derives A AG (@ewand A JA PA AG XA (@box A AG (@laterM A AG) P) (@box A AG (@laterM A AG) Q)) (@box A AG (@laterM A AG) (@ewand A JA PA AG XA P Q)) *)
apply core_unit.
(* Goal: forall P Q R : @pred T agT, @derives T agT (@andp T agT (@sepcon T JT PT agT AT P Q) (@ewand T JT PT agT AT R (@prop T agT True))) (@sepcon T JT PT agT AT (@andp T agT P (@ewand T JT PT agT AT R (@prop T agT True))) (@andp T agT Q (@ewand T JT PT agT AT R (@prop T agT True)))) *)
hnf; intros.
(* Goal: @app_pred A AG P a' *)
(* Goal: @app_pred A AG (@box A AG (@laterM A AG) Q) w *)
(* Goal: @derives A AG (@ewand A JA PA AG XA (@box A AG (@laterM A AG) P) (@box A AG (@laterM A AG) Q)) (@box A AG (@laterM A AG) (@ewand A JA PA AG XA P Q)) *)
assert (age1 (core w) = None).
(* Goal: @join A JA w1 w5 w3 *)
apply age1_None_joins with w; auto.
(* Goal: @join A JA (@core A JA SA w) w w *)
(* Goal: @app_pred A AG (@box A AG (@laterM A AG) P) (@core A JA SA w) *)
(* Goal: @app_pred A AG (@box A AG (@laterM A AG) Q) w *)
(* Goal: @derives A AG (@ewand A JA PA AG XA (@box A AG (@laterM A AG) P) (@box A AG (@laterM A AG) Q)) (@box A AG (@laterM A AG) (@ewand A JA PA AG XA P Q)) *)
exists w; apply join_comm; apply core_unit.
(* Goal: @app_pred A AG P a' *)
(* Goal: @app_pred A AG (@box A AG (@laterM A AG) Q) w *)
(* Goal: @derives A AG (@ewand A JA PA AG XA (@box A AG (@laterM A AG) P) (@box A AG (@laterM A AG) Q)) (@box A AG (@laterM A AG) (@ewand A JA PA AG XA P Q)) *)
unfold laterM in H1. simpl in H1.
(* Goal: @app_pred A AG P a' *)
(* Goal: @app_pred A AG (@box A AG (@laterM A AG) Q) w *)
(* Goal: @derives A AG (@ewand A JA PA AG XA (@box A AG (@laterM A AG) P) (@box A AG (@laterM A AG) Q)) (@box A AG (@laterM A AG) (@ewand A JA PA AG XA P Q)) *)
unfold laterR in H1.
(* Goal: @app_pred A AG Q w' *)
(* Goal: @derives A AG (@ewand A JA PA AG XA (@box A AG (@laterM A AG) P) (@box A AG (@laterM A AG) Q)) (@box A AG (@laterM A AG) (@ewand A JA PA AG XA P Q)) *)
apply clos_trans_t1n in H1. inv H1; rewrite H3 in H2; inv H2.
(* Goal: @app_pred A AG (@box A AG (@laterM A AG) (@ewand A JA PA AG XA P Q)) w *)
intros w' ?.
(* Goal: @app_pred A AG Q w' *)
(* Goal: @derives A AG (@ewand A JA PA AG XA (@box A AG (@laterM A AG) P) (@box A AG (@laterM A AG) Q)) (@box A AG (@laterM A AG) (@ewand A JA PA AG XA P Q)) *)
hnf in H1. apply clos_trans_t1n in H1.
(* Goal: @ex A (fun ophi2 : A => and (@age A AG phi2 ophi2) (@comparable A JA SA phi ophi2)) *)
(* Goal: @ex A (fun phi2' : A => and (@eq (option A) (@ageN A AG (S n) phi2) (@Some A phi2')) (@comparable A JA SA phi1' phi2')) *)
inv H1; rewrite H2 in H0; inv H0.

(* Goal: @derives A AG (@sepcon A JA PA AG XA (@ewand A JA PA AG XA (@TT A AG) (@sepcon A JA PA AG XA P Q)) Q) (@ewand A JA PA AG XA (@TT A AG) (@sepcon A JA PA AG XA P Q)) *)
intros w [w1 [w2 [? [? ?]]]].
(* Goal: @app_pred A AG (@box A AG (@laterM A AG) (@ewand A JA PA AG XA P Q)) w *)
intros w' ?.
(* Goal: @app_pred A AG (@ewand A JA PA AG XA P Q) w' *)
hnf in H2. apply clos_trans_t1n in H2.
(* Goal: forall P Q R : @pred T agT, @derives T agT (@andp T agT (@sepcon T JT PT agT AT P Q) (@ewand T JT PT agT AT R (@prop T agT True))) (@sepcon T JT PT agT AT (@andp T agT P (@ewand T JT PT agT AT R (@prop T agT True))) (@andp T agT Q (@ewand T JT PT agT AT R (@prop T agT True)))) *)
revert w1 w2 H H0 H1; induction H2; intros.
(* Goal: @app_pred A AG (@ewand A JA PA AG XA P Q) z *)
destruct (age1_join _ (join_comm H0) H) as [w1' [w2' [? [? ?]]]].
(* Goal: @join A JA w1 w5 w3 *)
exists w1'; exists w2'; split; auto.
(* Goal: @app_pred A AG (@andp A AG (@prop A AG Q) (@sepcon A JA PA AG XA P R)) w *)
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA P (@andp A AG (@prop A AG Q) R)) w *)
split.
(* Goal: @join A JA w1 w5 w3 *)
eapply H1. hnf; apply clos_t1n_trans. constructor 1; auto.
(* Goal: @join A JA w1 w5 w3 *)
eapply H2. hnf; apply clos_t1n_trans. constructor 1; auto.
(* Goal: @app_pred A AG (@ewand A JA PA AG XA P Q) z *)
destruct (age1_join _ (join_comm H0) H) as [w1' [w2' [? [? ?]]]].
(* Goal: @join A JA w1 w5 w3 *)
apply (IHclos_trans_1n _ _ (join_comm H4)); auto; eapply pred_hereditary; eauto.
Qed.

(* 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}{AG: ageable A}{XA: Age_alg A}:
      forall P, ewand emp P = P.
Proof.
(* Goal: forall P Q R : @pred T agT, @derives T agT (@andp T agT (@sepcon T JT PT agT AT P Q) (@ewand T JT PT agT AT R (@prop T agT True))) (@sepcon T JT PT agT AT (@andp T agT P (@ewand T JT PT agT AT R (@prop T agT True))) (@andp T agT Q (@ewand T JT PT agT AT R (@prop T agT True)))) *)
intros.
(* Goal: @eq (@pred A AG) (@sepcon A JA PA AG XA P (@andp A AG (@prop A AG Q) R)) (@andp A AG (@prop A AG Q) (@sepcon A JA PA AG XA P R)) *)
apply pred_ext; intros w ?.
(* Goal: @app_pred A AG (@ewand A JA PA AG XA (@sepcon A JA PA AG XA P Q) R) w *)
destruct H as [w1 [w2 [? [? ?]]]].
(* Goal: @join A JA w1 w5 w3 *)
replace w with w2; auto.
(* Goal: @eq A f w2 *)
(* Goal: @app_pred A AG (@ewand A JA PA AG XA (@TT A AG) (@sepcon A JA PA AG XA P Q)) w *)
eapply join_eq; eauto.
(* Goal: @join A JA w1 w5 w3 *)
eapply identity_unit; eauto.
(* Goal: @app_pred A AG (@ewand A JA PA AG XA (@emp A JA PA SA AG XA) P) w *)
destruct (join_ex_identities w) as [e [He [? Hj]]].
(* Goal: @app_pred A AG (@ewand A JA PA AG XA (@emp A JA PA SA AG XA) P) w *)
exists e; exists w.
(* Goal: @join A JA w1 w5 w3 *)
split; auto.
(* Goal: @join A JA w1 w5 w3 *)
specialize (He _ _ Hj); subst; auto.
Qed.


Lemma pry_apart {A}  {JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A}{CA: Canc_alg A}{DA: Disj_alg A}{CrA: Cross_alg A}{AG: ageable A}{XA: Age_alg A}:
  forall G P Q, superprecise G -> P = ewand G (G * P) ->
                       (P * Q) && (G * TT) |-- (P * G * (ewand G Q)).
Proof.
(* Goal: forall P Q R : @pred T agT, @derives T agT (@andp T agT (@sepcon T JT PT agT AT P Q) (@ewand T JT PT agT AT R (@prop T agT True))) (@sepcon T JT PT agT AT (@andp T agT P (@ewand T JT PT agT AT R (@prop T agT True))) (@andp T agT Q (@ewand T JT PT agT AT R (@prop T agT True)))) *)
 pose proof I. intros.
(* Goal: @derives A AG (@andp A AG (@sepcon A JA PA AG XA P Q) (@sepcon A JA PA AG XA G (@TT A AG))) (@sepcon A JA PA AG XA (@sepcon A JA PA AG XA P G) (@ewand A JA PA AG XA G Q)) *)
intros w [? ?].
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@sepcon A JA PA AG XA P G) (@exist (forall _ : A, Prop) (fun p : forall _ : A, Prop => @hereditary A (@age A AG) p) (fun w : A => @ex A (fun w1 : A => @ex A (fun w2 : A => and (@join A JA w1 w w2) (and (@app_pred A AG G w1) (@app_pred A AG Q w2))))) (ewand_obligation_1 A JA PA AG XA G Q))) w *)
destruct H2 as [w2 [w3 [? [? Hq]]]].
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@sepcon A JA PA AG XA P G) (@exist (forall _ : A, Prop) (fun p : forall _ : A, Prop => @hereditary A (@age A AG) p) (fun w : A => @ex A (fun w1 : A => @ex A (fun w2 : A => and (@join A JA w1 w w2) (and (@app_pred A AG G w1) (@app_pred A AG Q w2))))) (ewand_obligation_1 A JA PA AG XA G Q))) w *)
destruct H3 as [w4 [w5 [? [? _]]]].
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@sepcon A JA PA AG XA P G) (@exist (forall _ : A, Prop) (fun p : forall _ : A, Prop => @hereditary A (@age A AG) p) (fun w : A => @ex A (fun w1 : A => @ex A (fun w2 : A => and (@join A JA w1 w w2) (and (@app_pred A AG G w1) (@app_pred A AG Q w2))))) (ewand_obligation_1 A JA PA AG XA G Q))) w *)
rewrite H1 in H4.
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@sepcon A JA PA AG XA P G) (@exist (forall _ : A, Prop) (fun p : forall _ : A, Prop => @hereditary A (@age A AG) p) (fun w : A => @ex A (fun w1 : A => @ex A (fun w2 : A => and (@join A JA w1 w w2) (and (@app_pred A AG G w1) (@app_pred A AG Q w2))))) (ewand_obligation_1 A JA PA AG XA G Q))) w *)
destruct H4 as [wa [wb [? [? ?]]]].
(* Goal: @join A JA w1 w5 w3 *)
assert (wa = w4). apply H0; auto.
(* Goal: @join A JA w1 w5 w3 *)
apply comparable_trans with w2. apply join_comparable2 with wb; auto.
(* Goal: @join A JA w1 w5 w3 *)
apply comparable_trans with w. apply join_comparable with w3; auto.
(* Goal: @join A JA w1 w5 w3 *)
apply comparable_sym. apply join_comparable with w5; auto.
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@sepcon A JA PA AG XA P G) (@exist (forall _ : A, Prop) (fun p : forall _ : A, Prop => @hereditary A (@age A AG) p) (fun w : A => @ex A (fun w1 : A => @ex A (fun w2 : A => and (@join A JA w1 w w2) (and (@app_pred A AG G w1) (@app_pred A AG Q w2))))) (ewand_obligation_1 A JA PA AG XA G Q))) w *)
subst wa; clear H6.
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@sepcon A JA PA AG XA P G) (@exist (forall _ : A, Prop) (fun p : forall _ : A, Prop => @hereditary A (@age A AG) p) (fun w : A => @ex A (fun w1 : A => @ex A (fun w2 : A => and (@join A JA w1 w w2) (and (@app_pred A AG G w1) (@app_pred A AG Q w2))))) (ewand_obligation_1 A JA PA AG XA G Q))) w *)
destruct H7 as [w4' [w2' [? [? ?]]]].
(* Goal: @join A JA w1 w5 w3 *)
assert (w4' = w4). apply H0; auto.
(* Goal: @join A JA w1 w5 w3 *)
apply comparable_trans with wb. eapply join_comparable; eauto.
(* Goal: @join A JA w1 w5 w3 *)
apply comparable_sym.  eapply join_comparable; eauto.
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@sepcon A JA PA AG XA P G) (@exist (forall _ : A, Prop) (fun p : forall _ : A, Prop => @hereditary A (@age A AG) p) (fun w : A => @ex A (fun w1 : A => @ex A (fun w2 : A => and (@join A JA w1 w w2) (and (@app_pred A AG G w1) (@app_pred A AG Q w2))))) (ewand_obligation_1 A JA PA AG XA G Q))) w *)
subst w4'; clear H7.
(* Goal: @join A JA w1 w5 w3 *)
assert (w2' = w2). eapply join_canc; try apply join_comm; eauto.
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@sepcon A JA PA AG XA P G) (@exist (forall _ : A, Prop) (fun p : forall _ : A, Prop => @hereditary A (@age A AG) p) (fun w : A => @ex A (fun w1 : A => @ex A (fun w2 : A => and (@join A JA w1 w w2) (and (@app_pred A AG G w1) (@app_pred A AG Q w2))))) (ewand_obligation_1 A JA PA AG XA G Q))) w *)
subst w2'; clear H6.
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@sepcon A JA PA AG XA P G) (@ewand A JA PA AG XA G Q)) w *)
destruct (CrA _ _ _ _ _ H2 H3) as [[[[w24 w25] w34] w35] [? [? [? ?]]]].
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@sepcon A JA PA AG XA P G) (@ewand A JA PA AG XA G Q)) w *)
assert (identity w24).
(* Goal: @identity A JA w24 *)
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@sepcon A JA PA AG XA P G) (@ewand A JA PA AG XA G Q)) w *)
  destruct (join_assoc (join_comm H9) H4) as [f [? ?]].
(* Goal: @identity A JA w24 *)
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@sepcon A JA PA AG XA P G) (@ewand A JA PA AG XA G Q)) w *)
  destruct (join_assoc (join_comm H6) (join_comm H11)) as [g [? ?]].
(* Goal: @join A JA w1 w5 w3 *)
  eapply join_self; eauto.
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@sepcon A JA PA AG XA P G) (@ewand A JA PA AG XA G Q)) w *)
assert (w34=w4). eapply join_eq; [eapply identity_unit; eauto | auto ].
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@sepcon A JA PA AG XA P G) (@ewand A JA PA AG XA G Q)) w *)
subst w34.
(* Goal: @eq A w25 w2 *)
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@sepcon A JA PA AG XA P G) (@ewand A JA PA AG XA G Q)) w *)
assert (w25 = w2). eapply join_eq; [eapply identity_unit; eauto | auto ].
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@sepcon A JA PA AG XA P G) (@ewand A JA PA AG XA G Q)) w *)
subst w25.
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@sepcon A JA PA AG XA P G) (@ewand A JA PA AG XA G Q)) w *)
clear H11 H9 H6 w24.
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@sepcon A JA PA AG XA P G) (@ewand A JA PA AG XA G Q)) w *)
destruct (join_assoc (join_comm H10) (join_comm H3)) as [h [? ?]].
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@sepcon A JA PA AG XA P G) (@ewand A JA PA AG XA G Q)) w *)
generalize (join_eq H6 (join_comm H4)); clear H6; intro; subst h.
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@sepcon A JA PA AG XA P G) (@ewand A JA PA AG XA G Q)) w *)
destruct (join_assoc (join_comm H4) (join_comm H9)) as [h [? ?]].
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@sepcon A JA PA AG XA P G) (@ewand A JA PA AG XA G Q)) w *)
generalize (join_eq H6 H7); clear H6; intro; subst h.
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@sepcon A JA PA AG XA P G) (@ewand A JA PA AG XA G Q)) w *)
clear H11.
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@sepcon A JA PA AG XA P G) (@ewand A JA PA AG XA G Q)) w *)
exists wb; exists w35.
(* Goal: @join A JA w1 w5 w3 *)
split. apply join_comm; auto.
(* Goal: @join A JA w1 w5 w3 *)
split; auto.
(* Goal: @join A JA w1 w5 w3 *)
exists w2; exists w4; split; auto.
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@sepcon A JA PA AG XA P G) (@ewand A JA PA AG XA G Q)) w *)
unfold ewand.
(* Goal: @join A JA w1 w5 w3 *)
exists w4; exists w3; split; auto.
Qed.

Definition wk_split {A} {JA: Join A} :=
      forall a b c d e : A, join a b c -> join d e c -> joins a d -> join_sub d b.

Lemma crosssplit_wkSplit {A}  {JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A}{DA: Disj_alg A}{CrA: Cross_alg A}{AG: ageable A}{XA: Age_alg A}:
(* Goal: @app_pred A AG (@andp A AG (@prop A AG Q) (@sepcon A JA PA AG XA P R)) w *)
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA P (@andp A AG (@prop A AG Q) R)) w *)
    wk_split.
Proof.
(* Goal: forall P Q R : @pred T agT, @derives T agT (@andp T agT (@sepcon T JT PT agT AT P Q) (@ewand T JT PT agT AT R (@prop T agT True))) (@sepcon T JT PT agT AT (@andp T agT P (@ewand T JT PT agT AT R (@prop T agT True))) (@andp T agT Q (@ewand T JT PT agT AT R (@prop T agT True)))) *)
unfold wk_split; intros.
destruct (CrA _ _ _ _ _ H H0) as [[[[ad ae] bd] be] [myH1 [myH2 [myH3 myH4]]]].
destruct H1 as [x H_x].
assert (exists X, join ad X be) as [X HX].
2:{   exists X.
               destruct (join_assoc (join_comm HX) (join_comm myH2)) as [y [myH5 myH6]].
               assert (y=d) by apply (join_eq myH5 myH3).  subst y.
(* Goal: @join A JA u y w *)
(* Goal: and (@app_pred A AG (@sepcon A JA PA AG XA P G) u) (@app_pred A AG (@exist (forall _ : A, Prop) (fun p : forall _ : A, Prop => @hereditary A (@age A AG) p) (fun w : A => @ex A (fun w1 : A => @ex A (fun w2 : A => and (@join A JA w1 w w2) (and (@app_pred A AG G w1) (@app_pred A AG Q w2))))) (ewand_obligation_1 A JA PA AG XA G Q)) y) *)
               apply (join_comm myH6).
}
destruct (join_assoc (join_comm myH1) H_x) as [y [myH5 myH6]].
destruct (join_assoc (join_comm myH3) (join_comm myH5)) as [? [Had ?]].
apply join_self in Had.
pose proof (Had _ _ myH1); subst.
destruct (join_assoc (join_comm myH1) myH4) as [? [Hbe ?]].
(* Goal: @join A JA w1 w5 w3 *)
specialize (Had _ _ Hbe); subst; eauto.
Qed.

Lemma wk_pry_apart {A}  {JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A}{CA: Canc_alg A}{DA: Disj_alg A}{CrA: Cross_alg A}{AG: ageable A}{XA: Age_alg A}:
  forall G P Q, wk_split -> superprecise G -> P = ewand G (G * P) ->
                       (P * Q) && (G * TT) |-- (P * G * (ewand G Q)).
Proof.
(* Goal: forall P Q R : @pred T agT, @derives T agT (@andp T agT (@sepcon T JT PT agT AT P Q) (@ewand T JT PT agT AT R (@prop T agT True))) (@sepcon T JT PT agT AT (@andp T agT P (@ewand T JT PT agT AT R (@prop T agT True))) (@andp T agT Q (@ewand T JT PT agT AT R (@prop T agT True)))) *)
intros.
(* Goal: @derives A AG (@andp A AG (@sepcon A JA PA AG XA P Q) (@sepcon A JA PA AG XA G (@TT A AG))) (@sepcon A JA PA AG XA (@sepcon A JA PA AG XA P G) (@ewand A JA PA AG XA G Q)) *)
intros w [? ?]. unfold ewand.
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@sepcon A JA PA AG XA P G) (@exist (forall _ : A, Prop) (fun p : forall _ : A, Prop => @hereditary A (@age A AG) p) (fun w : A => @ex A (fun w1 : A => @ex A (fun w2 : A => and (@join A JA w1 w w2) (and (@app_pred A AG G w1) (@app_pred A AG Q w2))))) (ewand_obligation_1 A JA PA AG XA G Q))) w *)
destruct H2 as [w2 [w3 [? [? Hq]]]].
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@sepcon A JA PA AG XA P G) (@exist (forall _ : A, Prop) (fun p : forall _ : A, Prop => @hereditary A (@age A AG) p) (fun w : A => @ex A (fun w1 : A => @ex A (fun w2 : A => and (@join A JA w1 w w2) (and (@app_pred A AG G w1) (@app_pred A AG Q w2))))) (ewand_obligation_1 A JA PA AG XA G Q))) w *)
destruct H3 as [w4 [w5 [? [? _]]]].
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@sepcon A JA PA AG XA P G) (@exist (forall _ : A, Prop) (fun p : forall _ : A, Prop => @hereditary A (@age A AG) p) (fun w : A => @ex A (fun w1 : A => @ex A (fun w2 : A => and (@join A JA w1 w w2) (and (@app_pred A AG G w1) (@app_pred A AG Q w2))))) (ewand_obligation_1 A JA PA AG XA G Q))) w *)
rewrite H1 in H4.
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@sepcon A JA PA AG XA P G) (@exist (forall _ : A, Prop) (fun p : forall _ : A, Prop => @hereditary A (@age A AG) p) (fun w : A => @ex A (fun w1 : A => @ex A (fun w2 : A => and (@join A JA w1 w w2) (and (@app_pred A AG G w1) (@app_pred A AG Q w2))))) (ewand_obligation_1 A JA PA AG XA G Q))) w *)
destruct H4 as [wa [wb [? [? ?]]]].
(* Goal: @join A JA w1 w5 w3 *)
assert (wa = w4). apply H0; auto.
(* Goal: @join A JA w1 w5 w3 *)
apply comparable_trans with w2. eapply join_comparable2; eauto.
(* Goal: @join A JA w1 w5 w3 *)
apply comparable_trans with w. eapply join_comparable; eauto.
(* Goal: @join A JA w1 w5 w3 *)
apply comparable_sym.  eapply join_comparable; eauto.
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@sepcon A JA PA AG XA P G) (@exist (forall _ : A, Prop) (fun p : forall _ : A, Prop => @hereditary A (@age A AG) p) (fun w : A => @ex A (fun w1 : A => @ex A (fun w2 : A => and (@join A JA w1 w w2) (and (@app_pred A AG G w1) (@app_pred A AG Q w2))))) (ewand_obligation_1 A JA PA AG XA G Q))) w *)
subst wa; clear H6.
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@sepcon A JA PA AG XA P G) (@exist (forall _ : A, Prop) (fun p : forall _ : A, Prop => @hereditary A (@age A AG) p) (fun w : A => @ex A (fun w1 : A => @ex A (fun w2 : A => and (@join A JA w1 w w2) (and (@app_pred A AG G w1) (@app_pred A AG Q w2))))) (ewand_obligation_1 A JA PA AG XA G Q))) w *)
destruct H7 as [w4' [w2' [? [? ?]]]].
(* Goal: @join A JA w1 w5 w3 *)
assert (w4' = w4). apply H0; auto.
(* Goal: @join A JA w1 w5 w3 *)
apply comparable_trans with wb. eapply join_comparable; eauto.
(* Goal: @join A JA w1 w5 w3 *)
apply comparable_sym.  eapply join_comparable; eauto.
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@sepcon A JA PA AG XA P G) (@exist (forall _ : A, Prop) (fun p : forall _ : A, Prop => @hereditary A (@age A AG) p) (fun w : A => @ex A (fun w1 : A => @ex A (fun w2 : A => and (@join A JA w1 w w2) (and (@app_pred A AG G w1) (@app_pred A AG Q w2))))) (ewand_obligation_1 A JA PA AG XA G Q))) w *)
subst w4'; clear H7.
(* Goal: @join A JA w1 w5 w3 *)
assert (w2' = w2). eapply join_canc; try apply join_comm; eauto.
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@sepcon A JA PA AG XA P G) (@exist (forall _ : A, Prop) (fun p : forall _ : A, Prop => @hereditary A (@age A AG) p) (fun w : A => @ex A (fun w1 : A => @ex A (fun w2 : A => and (@join A JA w1 w w2) (and (@app_pred A AG G w1) (@app_pred A AG Q w2))))) (ewand_obligation_1 A JA PA AG XA G Q))) w *)
subst w2'; clear H6.
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@sepcon A JA PA AG XA P G) (@exist (forall _ : A, Prop) (fun p : forall _ : A, Prop => @hereditary A (@age A AG) p) (fun w : A => @ex A (fun w1 : A => @ex A (fun w2 : A => and (@join A JA w1 w w2) (and (@app_pred A AG G w1) (@app_pred A AG Q w2))))) (ewand_obligation_1 A JA PA AG XA G Q))) w *)
assert (exists y, join w2 y w5).
(* Goal: @ex A (fun y : A => @join A JA w2 y w5) *)
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@sepcon A JA PA AG XA P G) (@exist (forall _ : A, Prop) (fun p : forall _ : A, Prop => @hereditary A (@age A AG) p) (fun w : A => @ex A (fun w1 : A => @ex A (fun w2 : A => and (@join A JA w1 w w2) (and (@app_pred A AG G w1) (@app_pred A AG Q w2))))) (ewand_obligation_1 A JA PA AG XA G Q))) w *)
    destruct (H _ _ _ _ _ H2 H3 (join_joins (join_comm H4))).
(* Goal: @ex A (fun y : A => @join A JA w2 y w5) *)
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@sepcon A JA PA AG XA P G) (@exist (forall _ : A, Prop) (fun p : forall _ : A, Prop => @hereditary A (@age A AG) p) (fun w : A => @ex A (fun w1 : A => @ex A (fun w2 : A => and (@join A JA w1 w w2) (and (@app_pred A AG G w1) (@app_pred A AG Q w2))))) (ewand_obligation_1 A JA PA AG XA G Q))) w *)
    destruct (join_assoc H6 (join_comm H2)) as [y [myH1 myH2]].
(* Goal: @ex A (fun y : A => @join A JA w2 y w5) *)
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@sepcon A JA PA AG XA P G) (@exist (forall _ : A, Prop) (fun p : forall _ : A, Prop => @hereditary A (@age A AG) p) (fun w : A => @ex A (fun w1 : A => @ex A (fun w2 : A => and (@join A JA w1 w w2) (and (@app_pred A AG G w1) (@app_pred A AG Q w2))))) (ewand_obligation_1 A JA PA AG XA G Q))) w *)
    assert (y=w5) by apply (join_canc  (join_comm myH2) (join_comm H3)). subst y.
(* Goal: @ex A (fun y : A => @join A JA w2 y w5) *)
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@sepcon A JA PA AG XA P G) (@exist (forall _ : A, Prop) (fun p : forall _ : A, Prop => @hereditary A (@age A AG) p) (fun w : A => @ex A (fun w1 : A => @ex A (fun w2 : A => and (@join A JA w1 w w2) (and (@app_pred A AG G w1) (@app_pred A AG Q w2))))) (ewand_obligation_1 A JA PA AG XA G Q))) w *)
    exists x. apply (join_comm myH1).
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@sepcon A JA PA AG XA P G) (@exist (forall _ : A, Prop) (fun p : forall _ : A, Prop => @hereditary A (@age A AG) p) (fun w : A => @ex A (fun w1 : A => @ex A (fun w2 : A => and (@join A JA w1 w w2) (and (@app_pred A AG G w1) (@app_pred A AG Q w2))))) (ewand_obligation_1 A JA PA AG XA G Q))) w *)
exists wb.
(* Goal: @ex A (fun z : A => and (@join A JA wb z w) (and (@app_pred A AG (@sepcon A JA PA AG XA P G) wb) (@app_pred A AG (@exist (forall _ : A, Prop) (fun p : forall _ : A, Prop => @hereditary A (@age A AG) p) (fun w : A => @ex A (fun w1 : A => @ex A (fun w2 : A => and (@join A JA w1 w w2) (and (@app_pred A AG G w1) (@app_pred A AG Q w2))))) (ewand_obligation_1 A JA PA AG XA G Q)) z))) *)
destruct H6 as [y w2_y_w5].
(* Goal: @ex A (fun z : A => and (@join A JA wb z w) (and (@app_pred A AG (@sepcon A JA PA AG XA P G) wb) (@app_pred A AG (@exist (forall _ : A, Prop) (fun p : forall _ : A, Prop => @hereditary A (@age A AG) p) (fun w : A => @ex A (fun w1 : A => @ex A (fun w2 : A => and (@join A JA w1 w w2) (and (@app_pred A AG G w1) (@app_pred A AG Q w2))))) (ewand_obligation_1 A JA PA AG XA G Q)) z))) *)
               destruct (join_assoc w2_y_w5 (join_comm H3)) as [x [myH1 myH2]].
               destruct (join_assoc  (join_comm myH1) (join_comm myH2)) as [z [myH3 myH4]].
(* Goal: @ex A (fun z : A => and (@join A JA wb z w) (and (@app_pred A AG (@sepcon A JA PA AG XA P G) wb) (@app_pred A AG (@exist (forall _ : A, Prop) (fun p : forall _ : A, Prop => @hereditary A (@age A AG) p) (fun w : A => @ex A (fun w1 : A => @ex A (fun w2 : A => and (@join A JA w1 w w2) (and (@app_pred A AG G w1) (@app_pred A AG Q w2))))) (ewand_obligation_1 A JA PA AG XA G Q)) z))) *)
                                        assert (w5=z) by apply  (join_canc (join_comm H3) (join_comm myH4)). subst w5.
(* Goal: @ex A (fun z : A => and (@join A JA wb z w) (and (@app_pred A AG (@sepcon A JA PA AG XA P G) wb) (@app_pred A AG (@exist (forall _ : A, Prop) (fun p : forall _ : A, Prop => @hereditary A (@age A AG) p) (fun w : A => @ex A (fun w1 : A => @ex A (fun w2 : A => and (@join A JA w1 w w2) (and (@app_pred A AG G w1) (@app_pred A AG Q w2))))) (ewand_obligation_1 A JA PA AG XA G Q)) z))) *)
                                        assert (w3=x) by apply (join_canc (join_comm H2) (join_comm myH2)).  subst w3.
(* Goal: @ex A (fun z : A => and (@join A JA wb z w) (and (@app_pred A AG (@sepcon A JA PA AG XA P G) wb) (@app_pred A AG (@exist (forall _ : A, Prop) (fun p : forall _ : A, Prop => @hereditary A (@age A AG) p) (fun w : A => @ex A (fun w1 : A => @ex A (fun w2 : A => and (@join A JA w1 w w2) (and (@app_pred A AG G w1) (@app_pred A AG Q w2))))) (ewand_obligation_1 A JA PA AG XA G Q)) z))) *)
                                        destruct (join_assoc myH3 (join_comm myH4)) as [u [myH5 myH6]].
(* Goal: @ex A (fun z : A => and (@join A JA wb z w) (and (@app_pred A AG (@sepcon A JA PA AG XA P G) wb) (@app_pred A AG (@exist (forall _ : A, Prop) (fun p : forall _ : A, Prop => @hereditary A (@age A AG) p) (fun w : A => @ex A (fun w1 : A => @ex A (fun w2 : A => and (@join A JA w1 w w2) (and (@app_pred A AG G w1) (@app_pred A AG Q w2))))) (ewand_obligation_1 A JA PA AG XA G Q)) z))) *)
                                        assert (wb=u) by apply (join_eq H4 (join_comm myH5)). subst wb.
(* Goal: @app_pred A AG (@andp A AG (@prop A AG Q) (@sepcon A JA PA AG XA P R)) w *)
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA P (@andp A AG (@prop A AG Q) R)) w *)
               exists y. split. apply (join_comm myH6).
(* Goal: @app_pred A AG (@andp A AG (@prop A AG Q) (@sepcon A JA PA AG XA P R)) w *)
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA P (@andp A AG (@prop A AG Q) R)) w *)
               split. exists w2. exists w4. split. apply (join_comm H4). split; assumption.
(* Goal: @app_pred A AG (@andp A AG (@prop A AG Q) (@sepcon A JA PA AG XA P R)) w *)
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA P (@andp A AG (@prop A AG Q) R)) w *)
               exists w4. exists x; split. apply (join_comm myH1). split; assumption.
Qed.

Lemma ewand_overlap {A} {JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A}{CA: Canc_alg A}{DA: Disj_alg A}{CrA: Cross_alg A}{AG: ageable A}{XA: Age_alg A}:
    forall (P Q: pred A),
       superprecise Q ->
       ewand TT (P * Q) * Q |-- ewand TT (P * Q).
Proof.
(* Goal: forall (P Q : @pred A AG) (_ : @superprecise A JA PA SA AG XA Q), @derives A AG (@sepcon A JA PA AG XA (@ewand A JA PA AG XA (@TT A AG) (@sepcon A JA PA AG XA P Q)) Q) (@ewand A JA PA AG XA (@TT A AG) (@sepcon A JA PA AG XA P Q)) *)
intros P Q PrecQ.
(* Goal: @derives A AG (@sepcon A JA PA AG XA (@ewand A JA PA AG XA (@TT A AG) (@sepcon A JA PA AG XA P Q)) Q) (@ewand A JA PA AG XA (@TT A AG) (@sepcon A JA PA AG XA P Q)) *)
intros w [w1 [w2 [? [? ?]]]].
(* Goal: @app_pred A AG (@ewand A JA PA AG XA (@TT A AG) (@sepcon A JA PA AG XA P Q)) w *)
destruct H0 as [w5 [w6 [? [_ ?]]]].
(* Goal: @app_pred A AG (@ewand A JA PA AG XA (@TT A AG) (@sepcon A JA PA AG XA P Q)) w *)
destruct H2 as [w3 [w4 [? [? ?]]]].
(* Goal: not (@comparable A JA SA phi phi') *)
generalize (PrecQ  _ _ H4 H1); clear H4; intro.
(* Goal: @joins A JA w1 w4 *)
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@ewand A JA PA AG XA P Q) R) w *)
spec H4.
(* Goal: @comparable A JA SA w4 w2 *)
(* Goal: @app_pred A AG (@ewand A JA PA AG XA (@TT A AG) (@sepcon A JA PA AG XA P Q)) w *)
apply comparable_trans with w6.
(* Goal: @join A JA w1 w5 w3 *)
apply join_comparable with w3; apply join_comm; auto.
(* Goal: @comparable A JA SA wa w34 *)
(* Goal: @comparable A JA SA w34 w4 *)
(* Goal: @joins A JA w1 w4 *)
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@ewand A JA PA AG XA P Q) R) w *)
apply comparable_trans with w1.
(* Goal: @join A JA w1 w5 w3 *)
apply comparable_sym; apply join_comparable with w5; apply join_comm; auto.
(* Goal: @join A JA w1 w5 w3 *)
eapply join_comparable2; eauto.
(* Goal: @app_pred A AG (@ewand A JA PA AG XA (@TT A AG) (@sepcon A JA PA AG XA P Q)) w *)
subst w4.
(* Goal: @app_pred A AG (@ewand A JA PA AG XA (@TT A AG) (@sepcon A JA PA AG XA P Q)) w *)
destruct (CrA _ _ _ _ _ H0 H2) as [[[[a b] c] d] [? [? [? ?]]]].
(* Goal: @app_pred A AG (@ewand A JA PA AG XA (@TT A AG) (@sepcon A JA PA AG XA P Q)) w *)
destruct (join_assoc H5 H) as [f [? ?]].
(* Goal: @app_pred A AG (@ewand A JA PA AG XA (@TT A AG) (@sepcon A JA PA AG XA P Q)) w *)
destruct (join_assoc H7 (join_comm H8)) as [g [? ?]].
(* Goal: not (@comparable A JA SA phi phi') *)
generalize (join_self' H10); intro.
(* Goal: @app_pred A AG (@ewand A JA PA AG XA (@TT A AG) (@sepcon A JA PA AG XA P Q)) w *)
subst g.
(* Goal: @app_pred A AG (@ewand A JA PA AG XA (@TT A AG) (@sepcon A JA PA AG XA P Q)) w *)
assert (identity d).
(* Goal: @join A JA w1 w5 w3 *)
eapply unit_identity; eauto.
(* Goal: @app_pred A AG (@ewand A JA PA AG XA (@TT A AG) (@sepcon A JA PA AG XA P Q)) w *)
assert (b=w2).
(* Goal: @join A JA w1 w5 w3 *)
eapply join_canc; eauto.
(* Goal: @app_pred A AG (@ewand A JA PA AG XA (@TT A AG) (@sepcon A JA PA AG XA P Q)) w *)
subst b.
(* Goal: @app_pred A AG (@ewand A JA PA AG XA (@TT A AG) (@sepcon A JA PA AG XA P Q)) w *)
assert (f=w2).
(* Goal: @eq A f w2 *)
(* Goal: @app_pred A AG (@ewand A JA PA AG XA (@TT A AG) (@sepcon A JA PA AG XA P Q)) w *)
eapply join_eq; eauto.
(* Goal: @app_pred A AG (@ewand A JA PA AG XA (@TT A AG) (@sepcon A JA PA AG XA P Q)) w *)
subst f.
(* Goal: @app_pred A AG (@ewand A JA PA AG XA (@TT A AG) (@sepcon A JA PA AG XA P Q)) w *)
clear H11 H10 H7.
(* Goal: @app_pred A AG (@ewand A JA PA AG XA (@TT A AG) (@sepcon A JA PA AG XA P Q)) w *)
assert (c=w1).
(* Goal: @join A JA w1 w5 w3 *)
 specialize ( H12 c w1). apply H12. auto.
(* Goal: @app_pred A AG (@ewand A JA PA AG XA (@TT A AG) (@sepcon A JA PA AG XA P Q)) w *)
subst c.
(* Goal: @app_pred A AG (@ewand A JA PA AG XA (@TT A AG) (@sepcon A JA PA AG XA P Q)) w *)
clear H9 H5.
(* Goal: @app_pred A AG (@ewand A JA PA AG XA (@TT A AG) (@sepcon A JA PA AG XA P Q)) w *)
destruct (join_assoc H6 H2) as [h [? ?]].
(* Goal: @app_pred A AG (@ewand A JA PA AG XA (@TT A AG) (@sepcon A JA PA AG XA P Q)) w *)
generalize (join_eq H5 H); clear H5; intro; subst h.
(* Goal: @join A JA w1 w5 w3 *)
exists a; exists w6; split; auto.
(* Goal: @join A JA w1 w5 w3 *)
split; auto.
(* Goal: @join A JA w1 w5 w3 *)
exists w3; exists w2; split; auto.
Qed.

Lemma ewand_derives {A} {JA: Join A}{PA: Perm_alg A}{AG: ageable A}{XA: Age_alg A}:
  forall P P' Q Q',  P |-- P' -> Q |-- Q' -> ewand P Q |-- ewand P' Q'.
Proof.
(* Goal: forall P Q R : @pred T agT, @derives T agT (@andp T agT (@sepcon T JT PT agT AT P Q) (@ewand T JT PT agT AT R (@prop T agT True))) (@sepcon T JT PT agT AT (@andp T agT P (@ewand T JT PT agT AT R (@prop T agT True))) (@andp T agT Q (@ewand T JT PT agT AT R (@prop T agT True)))) *)
intros.
(* Goal: @derives A AG (@ewand A JA PA AG XA P (@sepcon A JA PA AG XA Q R)) (@sepcon A JA PA AG XA (@ewand A JA PA AG XA P Q) R) *)
intros w ?.
(* Goal: @app_pred A AG (@ewand A JA PA AG XA P' Q') w *)
destruct H1 as [?w [?w [? [? ?]]]].
(* Goal: @join A JA w1 w5 w3 *)
exists w0; exists w1; split; auto.
Qed.

Lemma ewand_sepcon {A} {JA: Join A}{PA: Perm_alg A}{AG: ageable A}{XA: Age_alg A}: forall P Q R,
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@box A AG (@ageM A AG) P) (@box A AG (@ageM A AG) Q)) a *)
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@box A AG (@ageM A AG) P) (@box A AG (@ageM A AG) Q)) a *)
(* Goal: @app_pred A AG (@box A AG (@ageM A AG) (@sepcon A JA PA AG XA P Q)) a *)
      (ewand (P * Q) R = ewand P (ewand Q R))%pred.
Proof.
(* Goal: @eq (@pred A AG) (@sepcon A JA PA AG XA P (@andp A AG (@prop A AG Q) R)) (@andp A AG (@prop A AG Q) (@sepcon A JA PA AG XA P R)) *)
intros; apply pred_ext; intros w ?.
(* Goal: @app_pred A AG (@ewand A JA PA AG XA (@sepcon A JA PA AG XA P Q) R) w *)
destruct H as [w1 [w2 [? [? ?]]]].
(* Goal: @app_pred A AG (@ewand A JA PA AG XA P (@ewand A JA PA AG XA Q R)) w *)
(* Goal: @app_pred A AG (@ewand A JA PA AG XA (@sepcon A JA PA AG XA P Q) R) w *)
destruct H0 as [w3 [w4 [? [? ?]]]].
(* Goal: @app_pred A AG (@ewand A JA PA AG XA P (@ewand A JA PA AG XA Q R)) w *)
(* Goal: @app_pred A AG (@ewand A JA PA AG XA (@sepcon A JA PA AG XA P Q) R) w *)
exists w3.
(* Goal: @ex A (fun w2 : A => and (@join A JA w3 w w2) (and (@app_pred A AG P w3) (@app_pred A AG (@ewand A JA PA AG XA Q R) w2))) *)
(* Goal: @app_pred A AG (@ewand A JA PA AG XA (@sepcon A JA PA AG XA P Q) R) w *)
destruct (join_assoc (join_comm H0) H) as [wf [? ?]].
(* Goal: @app_pred A AG (@ewand A JA PA AG XA (@sepcon A JA PA AG XA P Q) R) w *)
exists wf.
(* Goal: @join A JA w1 w5 w3 *)
split; [|split]; auto.
(* Goal: @join A JA w1 w5 w3 *)
exists w4. exists w2. split; auto.
(* Goal: @app_pred A AG (@ewand A JA PA AG XA (@sepcon A JA PA AG XA P Q) R) w *)
destruct H as [w1 [w2 [? [? ?]]]].
(* Goal: @app_pred A AG (@ewand A JA PA AG XA (@sepcon A JA PA AG XA P Q) R) w *)
destruct H1 as [w3 [w4 [? [? ?]]]].
(* Goal: @app_pred A AG (@ewand A JA PA AG XA (@sepcon A JA PA AG XA P Q) R) w *)
destruct (join_assoc (join_comm H) (join_comm H1)) as [wf [? ?]].
(* Goal: @join A JA w1 w5 w3 *)
exists wf. exists w4. split; [|split]; auto.
(* Goal: @join A JA w1 w5 w3 *)
exists w1; exists w3; split; auto.
Qed.

Lemma ewand_sepcon_assoc {A} {JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A}{CrA: Cross_alg A}{AG: ageable A}{XA: Age_alg A}:
  Trip_alg A ->
  forall P Q R: pred A,
      (forall w1 w2 w3, join w1 w2 w3 -> P w3 -> P w1) ->
      (forall w w', comparable w w' -> P w -> R w' -> joins w w') ->
      (ewand TT P) && (ewand TT R) |-- emp ->
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@box A AG (@ageM A AG) P) (@box A AG (@ageM A AG) Q)) a *)
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@box A AG (@ageM A AG) P) (@box A AG (@ageM A AG) Q)) a *)
(* Goal: @app_pred A AG (@box A AG (@ageM A AG) (@sepcon A JA PA AG XA P Q)) a *)
     (ewand P (Q * R) = (ewand P Q * R))%pred.
Proof.
intros TRIPLE P Q R ?H Hjoins ?H.
(* Goal: @eq (@pred A AG) (@sepcon A JA PA AG XA P (@andp A AG (@prop A AG Q) R)) (@andp A AG (@prop A AG Q) (@sepcon A JA PA AG XA P R)) *)
apply pred_ext; intros w ?.
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA p' q') a *)
destruct H1 as [w1 [w2 [? [? ?]]]].
destruct H3 as [w3 [w4 [? [? ?]]]].
destruct (CrA _ _ _ _ _ H1 H3) as [[[[? ?] ?] ?] [? [? [? ?]]]].
(* Goal: not (@comparable A JA SA phi phi') *)
generalize (H _ _ _ (join_comm H6) H2); intro.
assert (emp a0).
apply H0.
(* Goal: @app_pred A AG (@andp A AG (@prop A AG Q) (@sepcon A JA PA AG XA P R)) w *)
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA P (@andp A AG (@prop A AG Q) R)) w *)
split.
(* Goal: @join A JA w1 w5 w3 *)
2:{ do 2 econstructor; (split; [|split]). 3: eauto. eauto. auto. }
(* Goal: @join A JA w1 w5 w3 *)
exists a; exists w1; split; [|split]; eauto.
(* Goal: @join A JA w1 w5 w3 *)
apply join_unit2_e in H6; auto.
subst a.
(* Goal: @join A JA w1 w5 w3 *)
apply join_unit1_e in H9; auto.
subst a2.
(* Goal: @join A JA w1 w5 w3 *)
exists a1; exists w4; split; [|split]; auto.
(* Goal: @join A JA w1 w5 w3 *)
do 2 econstructor; eauto.
(*****)
destruct H1 as [w1 [wR [? [? ?]]]].
destruct H2 as [wP [wQ [? [? ?]]]].
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@sepcon A JA PA AG XA P Q) R) a *)
apply join_comm in H2.
specialize (Hjoins wP wR).
spec Hjoins.
(* Goal: @join A JA w1 w5 w3 *)
apply comparable_trans with w1; eapply join_comparable2; eauto.
(* Goal: @join A JA w1 w5 w3 *)
destruct Hjoins as [w6 ?]; auto.
destruct (TRIPLE _ _ _ _ _ _ H1 (join_comm H6) H2) as [wQR ?].
exists wP. exists wQR.
(* Goal: @join A JA w1 w5 w3 *)
split; [|split]; auto.
destruct (join_assoc H1 j) as [wf [? ?]].
generalize (join_eq H6 (join_comm H7)); clear H6; intros; subst w6.
destruct (join_assoc H7 (join_comm H8)) as [wg [? ?]].
generalize (join_eq H2 (join_comm H6)); clear H6; intros; subst wg.
(* Goal: @join A JA w1 w5 w3 *)
do 2 econstructor; eauto.
Qed.


Lemma ewand_sepcon2 {A} {JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A}{CA: Canc_alg A}{DA: Disj_alg A}{CrA: Cross_alg A}{AG: ageable A}{XA: Age_alg A}:
      forall
          R (SP: superprecise R)
          P (H: P = ewand R (R * P))
          Q,
          ewand P (Q * R) |-- ewand P Q * R.
Proof.
(* Goal: forall P Q R : @pred T agT, @derives T agT (@andp T agT (@sepcon T JT PT agT AT P Q) (@ewand T JT PT agT AT R (@prop T agT True))) (@sepcon T JT PT agT AT (@andp T agT P (@ewand T JT PT agT AT R (@prop T agT True))) (@andp T agT Q (@ewand T JT PT agT AT R (@prop T agT True)))) *)
intros.
(* Goal: @derives A AG (@ewand A JA PA AG XA P (@sepcon A JA PA AG XA Q R)) (@sepcon A JA PA AG XA (@ewand A JA PA AG XA P Q) R) *)
intros w ?.
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@ewand A JA PA AG XA P Q) R) w *)
destruct H0 as [w1 [w34 [? [? [w3 [w4 [? [? ?]]]]]]]].
(* Goal: not (@comparable A JA SA phi phi') *)
generalize (crosssplit_wkSplit  _ _ _ _ _ H0 (join_comm H2)); unfold wk_split; intro.
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@ewand A JA PA AG XA P Q) R) w *)
spec H5.
(* Goal: @joins A JA w1 w4 *)
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@ewand A JA PA AG XA P Q) R) w *)
rewrite H in H1.
(* Goal: @joins A JA w1 w4 *)
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@ewand A JA PA AG XA P Q) R) w *)
destruct H1 as [wa [wb [? [? ?]]]].
(* Goal: not (@comparable A JA SA phi phi') *)
generalize (SP _ _ H6 H4); clear H4; intro.
(* Goal: @joins A JA w1 w4 *)
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@ewand A JA PA AG XA P Q) R) w *)
spec H4.
(* Goal: @comparable A JA SA wa w34 *)
(* Goal: @comparable A JA SA w34 w4 *)
(* Goal: @joins A JA w1 w4 *)
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@ewand A JA PA AG XA P Q) R) w *)
apply comparable_trans with w34. apply comparable_trans with w1.
(* Goal: @join A JA w1 w5 w3 *)
eapply join_comparable2; eauto. eapply join_comparable; eauto.
(* Goal: @join A JA w1 w5 w3 *)
apply comparable_sym; eapply join_comparable; eauto.
(* Goal: @joins A JA w1 w4 *)
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@ewand A JA PA AG XA P Q) R) w *)
subst wa.
(* Goal: @joins A JA w1 w4 *)
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@ewand A JA PA AG XA P Q) R) w *)
destruct H7 as [wx [wy [? [? ?]]]].
(* Goal: not (@comparable A JA SA phi phi') *)
generalize (SP _ _ H7 H6); clear H7; intro.
(* Goal: @joins A JA w1 w4 *)
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@ewand A JA PA AG XA P Q) R) w *)
spec H7.
(* Goal: @join A JA w1 w5 w3 *)
apply comparable_trans with wb.  eapply join_comparable; eauto.
(* Goal: @join A JA w1 w5 w3 *)
apply comparable_sym; eapply join_comparable; eauto.
(* Goal: @joins A JA w1 w4 *)
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@ewand A JA PA AG XA P Q) R) w *)
subst wx.
(* Goal: not (@comparable A JA SA phi phi') *)
generalize (join_canc (join_comm H1) (join_comm H4)); clear H4; intro.
(* Goal: @joins A JA w1 w4 *)
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@ewand A JA PA AG XA P Q) R) w *)
subst wy.
(* Goal: @join A JA w1 w5 w3 *)
econstructor; eauto.
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@ewand A JA PA AG XA P Q) R) w *)
destruct H5 as [w5 ?].
(* Goal: @join A JA w1 w5 w3 *)
exists w5; exists w4; split; [|split]; auto.
(* Goal: @join A JA w1 w5 w3 *)
exists w1; exists w3; split; [|split]; auto.
(* Goal: @join A JA w1 w5 w3 *)
destruct (join_assoc H5 (join_comm H0)) as [wf [? ?]].
(* Goal: not (@comparable A JA SA phi phi') *)
generalize (join_canc (join_comm H7) H2); clear H7; intro.
(* Goal: @join A JA w1 w5 w3 *)
subst wf.
(* Goal: @join A JA w1 w5 w3 *)
auto.
Qed.

Lemma sepcon_andp_prop2 {A} {JA: Join A}{PA: Perm_alg A}{AG: ageable A}{XA: Age_alg A}:
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@box A AG (@ageM A AG) P) (@box A AG (@ageM A AG) Q)) a *)
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@box A AG (@ageM A AG) P) (@box A AG (@ageM A AG) Q)) a *)
(* Goal: @app_pred A AG (@box A AG (@ageM A AG) (@sepcon A JA PA AG XA P Q)) a *)
  forall P Q R,  (P * (!!Q && R) = !!Q && (P * R))%pred.
Proof.
(* Goal: forall P Q R : @pred T agT, @derives T agT (@andp T agT (@sepcon T JT PT agT AT P Q) (@ewand T JT PT agT AT R (@prop T agT True))) (@sepcon T JT PT agT AT (@andp T agT P (@ewand T JT PT agT AT R (@prop T agT True))) (@andp T agT Q (@ewand T JT PT agT AT R (@prop T agT True)))) *)
intros.
(* Goal: @eq (@pred A AG) (@sepcon A JA PA AG XA P (@andp A AG (@prop A AG Q) R)) (@andp A AG (@prop A AG Q) (@sepcon A JA PA AG XA P R)) *)
apply pred_ext; intros w ?.
(* Goal: @app_pred A AG (@andp A AG (@prop A AG Q) (@sepcon A JA PA AG XA P R)) w *)
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA P (@andp A AG (@prop A AG Q) R)) w *)
destruct H as [w1 [w2 [? [? [? ?]]]]].
(* Goal: @app_pred A AG (@andp A AG (@prop A AG Q) (@sepcon A JA PA AG XA P R)) w *)
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA P (@andp A AG (@prop A AG Q) R)) w *)
split. apply H1.
(* Goal: @join A JA w1 w5 w3 *)
exists w1; exists w2; split; [|split]; auto.
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA P (@andp A AG (@prop A AG Q) R)) w *)
destruct H.
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA P (@andp A AG (@prop A AG Q) R)) w *)
destruct H0 as [w1 [w2 [? [? ?]]]].
(* Goal: @join A JA w1 w5 w3 *)
exists w1; exists w2; repeat split; auto.
Qed.

Lemma sepcon_andp_prop1 {A}{JA: Join A}{PA: Perm_alg A}{agA: ageable A}{AgeA: Age_alg A}:
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@box A AG (@ageM A AG) P) (@box A AG (@ageM A AG) Q)) a *)
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@box A AG (@ageM A AG) P) (@box A AG (@ageM A AG) Q)) a *)
(* Goal: @app_pred A AG (@box A AG (@ageM A AG) (@sepcon A JA PA AG XA P Q)) a *)
   forall (P: Prop) (Q R: pred A) , ((!! P && Q) * R = !! P && (Q * R))%pred.
Proof.
(* Goal: @join A JA w1 w5 w3 *)
 intros. rewrite (sepcon_comm). rewrite sepcon_andp_prop2. rewrite sepcon_comm; auto.
Qed.

Lemma distrib_orp_sepcon {A : Type}{JA : Join A}{PA : Perm_alg A}{agA : ageable A}
    {AgeA : Age_alg A}:
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@box A AG (@ageM A AG) P) (@box A AG (@ageM A AG) Q)) a *)
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@box A AG (@ageM A AG) P) (@box A AG (@ageM A AG) Q)) a *)
(* Goal: @app_pred A AG (@box A AG (@ageM A AG) (@sepcon A JA PA AG XA P Q)) a *)
  forall (P Q R : pred A), ((P || Q) * R = P * R || Q * R)%pred.
Proof.
(* Goal: forall P Q R : @pred T agT, @derives T agT (@andp T agT (@sepcon T JT PT agT AT P Q) (@ewand T JT PT agT AT R (@prop T agT True))) (@sepcon T JT PT agT AT (@andp T agT P (@ewand T JT PT agT AT R (@prop T agT True))) (@andp T agT Q (@ewand T JT PT agT AT R (@prop T agT True)))) *)
 intros. apply pred_ext.
(* Goal: @join A JA w1 w5 w3 *)
  intros w [w1 [w2 [? [[?|?] ?]]]]; [left|right]; exists w1; exists w2; repeat split; auto.
(* Goal: @join A JA w1 w5 w3 *)
 intros ? [?|?];  destruct H as [w1 [w2 [? [? ?]]]]; exists w1; exists w2; repeat split; auto.
(* Goal: @join A JA w1 w5 w3 *)
  left; auto. right; auto.
Qed.

Lemma distrib_orp_sepcon2{A : Type}{JA : Join A}{PA : Perm_alg A}{agA : ageable A}
    {AgeA : Age_alg A}:
  forall (P Q R : pred A),
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@box A AG (@ageM A AG) P) (@box A AG (@ageM A AG) Q)) a *)
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA (@box A AG (@ageM A AG) P) (@box A AG (@ageM A AG) Q)) a *)
(* Goal: @app_pred A AG (@box A AG (@ageM A AG) (@sepcon A JA PA AG XA P Q)) a *)
     (R * (P || Q) = R * P || R * Q)%pred.
Proof.
(* Goal: forall P Q R : @pred T agT, @derives T agT (@andp T agT (@sepcon T JT PT agT AT P Q) (@ewand T JT PT agT AT R (@prop T agT True))) (@sepcon T JT PT agT AT (@andp T agT P (@ewand T JT PT agT AT R (@prop T agT True))) (@andp T agT Q (@ewand T JT PT agT AT R (@prop T agT True)))) *)
intros. rewrite !(sepcon_comm R). apply distrib_orp_sepcon.
Qed.

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

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