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.predicates_sl.
Require Import VST.msl.subtypes.

Local Open Scope pred.


Lemma unfash_derives {A} `{agA : ageable A}:
  forall {P Q}, (P |-- Q) -> @derives A _ (! P) (! Q).
Proof.
(* Goal: forall (T : Type) (agT : ageable T) (JoinT : Join T) (PermT : @Perm_alg T JoinT) (_ : @Sep_alg T JoinT) (AgeT : @Age_alg T JoinT agT) (P : @pred nat ag_nat) (Q R : @pred T agT), @eq (@pred T agT) (@andp T agT (@unfash T agT P) (@sepcon T JoinT PermT agT AgeT Q R)) (@sepcon T JoinT PermT agT AgeT (@andp T agT (@unfash T agT P) Q) (@andp T agT (@unfash T agT P) R)) *)
intros. intros w ?. simpl in *. apply H. auto.
Qed.

Lemma subp_sepcon {A} {JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A}{AG: ageable A}{XA: Age_alg A} : forall G P P' Q Q',
  G |-- P >=> P' ->
  G |-- Q >=> Q' ->
  G |-- P * Q >=> P' * Q'.
Proof.
(* Goal: forall (P P' Q Q' : @pred A AG) (st : nat) (_ : @app_pred nat ag_nat (@fash A AG (@imp A AG P P')) st) (_ : @app_pred nat ag_nat (@fash A AG (@imp A AG Q Q')) st), @app_pred nat ag_nat (@fash A AG (@imp A AG (@sepcon A JA PA AG XA P Q) (@sepcon A JA PA AG XA P' Q'))) st *)
  pose proof I.
(* Goal: forall (G : @pred nat ag_nat) (P P' Q Q' : @pred A AG) (_ : @derives nat ag_nat G (@fash A AG (@imp A AG P' P))) (_ : @derives nat ag_nat G (@fash A AG (@imp A AG Q Q'))), @derives nat ag_nat G (@fash A AG (@imp A AG (@wand A JA PA AG XA P Q) (@wand A JA PA AG XA P' Q'))) *)
  repeat intro.
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA P' Q') a' *)
  specialize (H0 _ H2).
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA P' Q') a' *)
  specialize (H1 _ H2).
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA P' Q') a' *)
  clear G H2.
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA P' Q') a' *)
  destruct H5 as [w1 [w2 [? [? ?]]]].
(* Goal: @app_pred nat ag_nat P (@level A as_age w') *)
  exists w1; exists w2; split; auto.
(* Goal: @app_pred T agT (@andp T agT (@unfash T agT P) (@sepcon T JoinT PermT agT AgeT Q R)) w *)
  split.
(* Goal: @app_pred nat ag_nat P (@level A as_age w') *)
  eapply H0; auto.
(* Goal: ge a (@level A AG w1) *)
(* Goal: @app_pred A AG Q' w2 *)
  assert (level w1 = level a').
(* Goal: @app_pred nat ag_nat P (@level A as_age w') *)
  apply comparable_fashionR.  eapply join_sub_comparable; eauto.
(* Goal: ge a (@level A AG y0) *)
 apply necR_level in H4. omega.
(* Goal: @app_pred nat ag_nat P (@level A as_age w') *)
  eapply H1; auto.
(* Goal: ge a (@level A AG w2) *)
  assert (level w2 = level a').
(* Goal: @app_pred nat ag_nat P (@level A as_age w') *)
  apply comparable_fashionR. eapply join_sub_comparable; eauto.
(* Goal: ge a (@level A AG y0) *)
 apply necR_level in H4. omega.
Qed.

Lemma sub_wand {A} {JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A}{AG: ageable A}{XA: Age_alg A} : forall G P P' Q Q',
  G |-- P' >=> P ->
  G |-- Q >=> Q' ->
  G |-- (P -* Q) >=> (P' -* Q').
Proof.
(* Goal: forall (P P' Q Q' : @pred A AG) (st : nat) (_ : @app_pred nat ag_nat (@fash A AG (@imp A AG P P')) st) (_ : @app_pred nat ag_nat (@fash A AG (@imp A AG Q Q')) st), @app_pred nat ag_nat (@fash A AG (@imp A AG (@sepcon A JA PA AG XA P Q) (@sepcon A JA PA AG XA P' Q'))) st *)
  pose proof I.
(* Goal: forall (G : @pred nat ag_nat) (P P' Q Q' : @pred A AG) (_ : @derives nat ag_nat G (@fash A AG (@imp A AG P' P))) (_ : @derives nat ag_nat G (@fash A AG (@imp A AG Q Q'))), @derives nat ag_nat G (@fash A AG (@imp A AG (@wand A JA PA AG XA P Q) (@wand A JA PA AG XA P' Q'))) *)
  repeat intro.
(* Goal: @app_pred A AG Q' z *)
  specialize (H0 _ H2); specialize (H1 _ H2); clear G H2; pose (H2:=True).
(* Goal: @app_pred A AG Q' z *)
  eapply H0 in H8; try apply necR_refl.
(* Goal: @app_pred A AG Q' z *)
(* Goal: ge a (@level A AG y0) *)
  eapply H1; try apply necR_refl.
(* Goal: ge a (@level A AG y0) *)
  apply necR_level in H4. apply necR_level in H6. apply join_comparable in H7.
(* Goal: ge a (@level A AG y0) *)
  apply comparable_fashionR in H7. unfold fashionR in H7. omega.
(* Goal: @app_pred nat ag_nat P (@level A as_age w') *)
  eapply H5; eauto.
(* Goal: ge a (@level A AG y0) *)
  apply necR_level in H4. apply necR_level in H6.
(* Goal: ge a (@level A AG y0) *)
   apply join_comparable2 in H7.
(* Goal: ge a (@level A AG y0) *)
  apply comparable_fashionR in H7. unfold fashionR in H7. omega.
Qed.

Lemma find_superprecise {A} {JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A}{AG: ageable A}{XA: Age_alg A}:
   forall Q, Q |-- EX P:_, P && !(P >=> Q) && !!superprecise (P).
Proof.
(* Goal: forall (T : Type) (agT : ageable T) (JoinT : Join T) (PermT : @Perm_alg T JoinT) (_ : @Sep_alg T JoinT) (AgeT : @Age_alg T JoinT agT) (P : @pred nat ag_nat) (Q R : @pred T agT), @eq (@pred T agT) (@andp T agT (@unfash T agT P) (@sepcon T JoinT PermT agT AgeT Q R)) (@sepcon T JoinT PermT agT AgeT (@andp T agT (@unfash T agT P) Q) (@andp T agT (@unfash T agT P) R)) *)
intros.
(* Goal: @app_pred nat ag_nat (@fash A as_age (@imp A as_age (@unfash A as_age P) (@unfash A as_age Q))) n *)
intros w ?.
(* Goal: @app_pred A AG (@exp A AG (@pred A AG) (fun P : @pred A AG => @andp A AG (@andp A AG P (@unfash A AG (@fash A AG (@imp A AG P Q)))) (@prop A AG (@superprecise A JA PA SA AG XA P)))) w *)
exists (exactly w).
(* Goal: @app_pred nat ag_nat P (@level A as_age w') *)
split; auto.
(* Goal: @app_pred nat ag_nat P (@level A as_age w') *)
split; auto.
(* Goal: @app_pred A AG (@exactly A AG w) w *)
(* Goal: @app_pred A AG (@unfash A AG (@fash A AG (@imp A AG (@exactly A AG w) Q))) w *)
(* Goal: @app_pred A AG (@prop A AG (@superprecise A JA PA SA AG XA (@exactly A AG w))) w *)
hnf; apply necR_refl.
(* Goal: @app_pred nat ag_nat (@fash A agA (@imp A agA Q P)) w *)
intros w' ? w'' ? ?.
(* Goal: @app_pred A AG Q w'' *)
(* Goal: @app_pred A AG (@prop A AG (@superprecise A JA PA SA AG XA (@exactly A AG w))) w *)
hnf in H2.
(* Goal: @app_pred nat ag_nat P (@level A as_age w') *)
apply pred_nec_hereditary with w; auto.
(* Goal: @app_pred A AG (@prop A AG (@superprecise A JA PA SA AG XA (@exactly A AG w))) w *)
do 3 red.
(* Goal: @superprecise A JA PA SA AG XA (@exactly A AG w) *)
apply superprecise_exactly.
Qed.

Lemma sepcon_subp' {A} {JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A}{AG: ageable A}{XA: Age_alg A}:
  forall (P P' Q Q' : pred A) (st: nat),
    (P >=> P') st ->
    (Q >=> Q') st ->
    (P * Q >=> P' * Q') st.
Proof.
(* Goal: forall (P P' Q Q' : @pred A AG) (st : nat) (_ : @app_pred nat ag_nat (@fash A AG (@imp A AG P P')) st) (_ : @app_pred nat ag_nat (@fash A AG (@imp A AG Q Q')) st), @app_pred nat ag_nat (@fash A AG (@imp A AG (@sepcon A JA PA AG XA P Q) (@sepcon A JA PA AG XA P' Q'))) st *)
 pose proof I.
(* Goal: forall (T : Type) (agT : ageable T) (JoinT : Join T) (PermT : @Perm_alg T JoinT) (_ : @Sep_alg T JoinT) (AgeT : @Age_alg T JoinT agT) (P : @pred nat ag_nat) (Q R : @pred T agT), @eq (@pred T agT) (@andp T agT (@unfash T agT P) (@sepcon T JoinT PermT agT AgeT Q R)) (@sepcon T JoinT PermT agT AgeT (@andp T agT (@unfash T agT P) Q) (@andp T agT (@unfash T agT P) R)) *)
intros.
(* Goal: @app_pred nat ag_nat (@fash A AG (@imp A AG (@sepcon A JA PA AG XA P Q) (@sepcon A JA PA AG XA P' Q'))) st *)
intros w' ? w'' ? [w1 [w2 [? [? ?]]]].
(* Goal: @app_pred A AG (@sepcon A JA PA AG XA P' Q') w'' *)
destruct (nec_join4 _ _ _ _ H4 H3) as [w1' [w2' [? [? ?]]]].
(* Goal: @app_pred nat ag_nat P (@level A as_age w') *)
exists w1; exists w2; repeat split; auto.
(* Goal: @app_pred nat ag_nat P (@level A as_age w') *)
eapply (H0 w1'); eauto.
(* Goal: ge st (@level A AG w1') *)
(* Goal: @app_pred A AG Q' w2 *)
simpl in *.
(* Goal: ge st (@level A AG w1') *)
(* Goal: @app_pred A AG Q' w2 *)
subst.
(* Goal: @app_pred nat ag_nat P (@level A as_age w') *)
replace (level w1') with (level w'); auto.
(* Goal: @app_pred nat ag_nat P (@level A as_age w') *)
symmetry; apply comparable_fashionR; eapply join_comparable; eauto.
(* Goal: @app_pred nat ag_nat P (@level A as_age w') *)
eapply (H1 w2'); eauto.
(* Goal: @app_pred nat ag_nat P (@level A as_age w') *)
replace (level w2') with (level w'); auto.
(* Goal: @eq nat (@level A AG w) (@level A AG w') *)
symmetry. apply comparable_fashionR.
(* Goal: @app_pred nat ag_nat P (@level A as_age w') *)
eapply join_comparable; eauto.
Qed.

Lemma subp_refl'  {A} `{agA : ageable A} :  forall (Q: pred A) (st: nat), (Q >=> Q) st.
Proof.
(* Goal: forall (T : Type) (agT : ageable T) (JoinT : Join T) (PermT : @Perm_alg T JoinT) (_ : @Sep_alg T JoinT) (AgeT : @Age_alg T JoinT agT) (P : @pred nat ag_nat) (Q R : @pred T agT), @eq (@pred T agT) (@andp T agT (@unfash T agT P) (@sepcon T JoinT PermT agT AgeT Q R)) (@sepcon T JoinT PermT agT AgeT (@andp T agT (@unfash T agT P) Q) (@andp T agT (@unfash T agT P) R)) *)
intros.
(* Goal: @app_pred nat ag_nat P (@level A as_age w') *)
intros ? ? ? ?; auto.
Qed.

Lemma subp_trans' {A} `{agA : ageable A}:
  forall (B C D: pred A) (w: nat), (B >=> C)%pred w -> (C >=> D)% pred w -> (B >=> D)%pred w.
Proof.
(* Goal: forall (T : Type) (agT : ageable T) (JoinT : Join T) (PermT : @Perm_alg T JoinT) (_ : @Sep_alg T JoinT) (AgeT : @Age_alg T JoinT agT) (P : @pred nat ag_nat) (Q R : @pred T agT), @eq (@pred T agT) (@andp T agT (@unfash T agT P) (@sepcon T JoinT PermT agT AgeT Q R)) (@sepcon T JoinT PermT agT AgeT (@andp T agT (@unfash T agT P) Q) (@andp T agT (@unfash T agT P) R)) *)
intros.
(* Goal: @app_pred nat ag_nat (@fash A agA (@imp A agA Q P)) w *)
intros w' ? w'' ? ?.
(* Goal: @app_pred nat ag_nat P (@level A as_age w') *)
eapply H0; eauto.
(* Goal: @app_pred nat ag_nat P (@level A as_age w') *)
eapply H; eauto.
Qed.

Lemma andp_subp'  {A} `{agA : ageable A} :
 forall (P P' Q Q': pred A) (w: nat), (P >=> P') w -> (Q >=> Q') w -> (P && Q >=> P' && Q') w.
Proof.
(* Goal: forall (T : Type) (agT : ageable T) (JoinT : Join T) (PermT : @Perm_alg T JoinT) (_ : @Sep_alg T JoinT) (AgeT : @Age_alg T JoinT agT) (P : @pred nat ag_nat) (Q R : @pred T agT), @eq (@pred T agT) (@andp T agT (@unfash T agT P) (@sepcon T JoinT PermT agT AgeT Q R)) (@sepcon T JoinT PermT agT AgeT (@andp T agT (@unfash T agT P) Q) (@andp T agT (@unfash T agT P) R)) *)
intros.
(* Goal: @app_pred T agT (@andp T agT (@unfash T agT P) (@sepcon T JoinT PermT agT AgeT Q R)) w *)
intros w' ? w'' ? [? ?]; split.
(* Goal: @app_pred nat ag_nat P (@level A as_age w') *)
eapply H; eauto.
(* Goal: @app_pred nat ag_nat P (@level A as_age w') *)
eapply H0; eauto.
Qed.

Lemma allp_subp' {A} `{agA : ageable A}: forall T (F G: T -> pred A) (w: nat),
   (forall x,  (F x >=> G x) w) -> (allp (fun x:T => (F x >=> G x)) w).
Proof.
(* Goal: forall (T : Type) (agT : ageable T) (JoinT : Join T) (PermT : @Perm_alg T JoinT) (_ : @Sep_alg T JoinT) (AgeT : @Age_alg T JoinT agT) (P : @pred nat ag_nat) (Q R : @pred T agT), @eq (@pred T agT) (@andp T agT (@unfash T agT P) (@sepcon T JoinT PermT agT AgeT Q R)) (@sepcon T JoinT PermT agT AgeT (@andp T agT (@unfash T agT P) Q) (@andp T agT (@unfash T agT P) R)) *)
intros.
(* Goal: @app_pred nat ag_nat P (@level A as_age w') *)
intro x; apply H; auto.
Qed.


Lemma pred_eq_e1 {A} `{agA : ageable A}: forall (P Q: pred A) w,
       ((P <=> Q) w -> (P >=> Q) w).
Proof.
(* Goal: forall (T : Type) (agT : ageable T) (JoinT : Join T) (PermT : @Perm_alg T JoinT) (_ : @Sep_alg T JoinT) (AgeT : @Age_alg T JoinT agT) (P : @pred nat ag_nat) (Q R : @pred T agT), @eq (@pred T agT) (@andp T agT (@unfash T agT P) (@sepcon T JoinT PermT agT AgeT Q R)) (@sepcon T JoinT PermT agT AgeT (@andp T agT (@unfash T agT P) Q) (@andp T agT (@unfash T agT P) R)) *)
intros.
(* Goal: @app_pred nat ag_nat (@fash A agA (@imp A agA Q P)) w *)
intros w' ? w'' ? ?.
(* Goal: @app_pred nat ag_nat P (@level A as_age w') *)
eapply H; eauto.
Qed.

Lemma pred_eq_e2 {A} `{agA : ageable A}: forall (P Q: pred A)  w,
     ((P <=> Q) w -> (Q >=> P) w).
Proof.
Proof.
(* Goal: forall (T : Type) (agT : ageable T) (JoinT : Join T) (PermT : @Perm_alg T JoinT) (_ : @Sep_alg T JoinT) (AgeT : @Age_alg T JoinT agT) (P : @pred nat ag_nat) (Q R : @pred T agT), @eq (@pred T agT) (@andp T agT (@unfash T agT P) (@sepcon T JoinT PermT agT AgeT Q R)) (@sepcon T JoinT PermT agT AgeT (@andp T agT (@unfash T agT P) Q) (@andp T agT (@unfash T agT P) R)) *)
intros.
(* Goal: @app_pred nat ag_nat (@fash A agA (@imp A agA Q P)) w *)
intros w' ? w'' ? ?.
(* Goal: @app_pred nat ag_nat P (@level A as_age w') *)
eapply H; eauto.
Qed.

Hint Resolve @sepcon_subp'.
Hint Resolve @subp_refl'.
Hint Resolve @andp_subp'.
Hint Resolve @allp_subp'.
Hint Resolve @derives_subp.
Hint Resolve @pred_eq_e1.
Hint Resolve @pred_eq_e2.


Lemma allp_imp2_later_e2 {B}{A}{agA: ageable A}:
   forall (P Q: B -> pred A) (y: B) ,
      (ALL x:B, |> P x <=> |> Q x) |-- |> Q y >=> |> P y.
Proof.
(* Goal: forall (T : Type) (agT : ageable T) (JoinT : Join T) (PermT : @Perm_alg T JoinT) (_ : @Sep_alg T JoinT) (AgeT : @Age_alg T JoinT agT) (P : @pred nat ag_nat) (Q R : @pred T agT), @eq (@pred T agT) (@andp T agT (@unfash T agT P) (@sepcon T JoinT PermT agT AgeT Q R)) (@sepcon T JoinT PermT agT AgeT (@andp T agT (@unfash T agT P) Q) (@andp T agT (@unfash T agT P) R)) *)
  intros.  intros w ?. specialize (H y). apply pred_eq_e2. auto.
Qed.
Lemma allp_imp2_later_e1 {B}{A}{agA: ageable A}:
   forall (P Q: B -> pred A) (y: B) ,
      (ALL x:B, |> P x <=> |> Q x) |-- |> P y >=> |> Q y.
Proof.
(* Goal: forall (T : Type) (agT : ageable T) (JoinT : Join T) (PermT : @Perm_alg T JoinT) (_ : @Sep_alg T JoinT) (AgeT : @Age_alg T JoinT agT) (P : @pred nat ag_nat) (Q R : @pred T agT), @eq (@pred T agT) (@andp T agT (@unfash T agT P) (@sepcon T JoinT PermT agT AgeT Q R)) (@sepcon T JoinT PermT agT AgeT (@andp T agT (@unfash T agT P) Q) (@andp T agT (@unfash T agT P) R)) *)
  intros.  intros w ?. specialize (H y). apply pred_eq_e1. auto.
Qed.

(*
Lemma subp_later {A} `{agA:  ageable A} (SS: natty A):
 forall (P Q: pred A), |> (P >=> Q) |-- |> P >=> |> Q.
Proof.
(* Goal: forall (T : Type) (agT : ageable T) (JoinT : Join T) (PermT : @Perm_alg T JoinT) (_ : @Sep_alg T JoinT) (AgeT : @Age_alg T JoinT agT) (P : @pred nat ag_nat) (Q R : @pred T agT), @eq (@pred T agT) (@andp T agT (@unfash T agT P) (@sepcon T JoinT PermT agT AgeT Q R)) (@sepcon T JoinT PermT agT AgeT (@andp T agT (@unfash T agT P) Q) (@andp T agT (@unfash T agT P) R)) *)
intros.
(* Goal: @app_pred nat ag_nat P (@level A as_age w') *)
rewrite later_fash; auto.
apply fash_derives.
apply axiomK.
Qed.
*)

Lemma extend_unfash {A} {JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A}{AG: ageable A}{XA: Age_alg A} : forall (P: pred nat), boxy extendM (! P).
Proof.
(* Goal: forall (T : Type) (agT : ageable T) (JoinT : Join T) (PermT : @Perm_alg T JoinT) (_ : @Sep_alg T JoinT) (AgeT : @Age_alg T JoinT agT) (P : @pred nat ag_nat) (Q R : @pred T agT), @eq (@pred T agT) (@andp T agT (@unfash T agT P) (@sepcon T JoinT PermT agT AgeT Q R)) (@sepcon T JoinT PermT agT AgeT (@andp T agT (@unfash T agT P) Q) (@andp T agT (@unfash T agT P) R)) *)
intros.
(* Goal: forall (T : Type) (agT : ageable T) (JoinT : Join T) (PermT : @Perm_alg T JoinT) (_ : @Sep_alg T JoinT) (AgeT : @Age_alg T JoinT agT) (P : @pred nat ag_nat) (Q R : @pred T agT), @eq (@pred T agT) (@andp T agT (@unfash T agT P) (@sepcon T JoinT PermT agT AgeT Q R)) (@sepcon T JoinT PermT agT AgeT (@andp T agT (@unfash T agT P) Q) (@andp T agT (@unfash T agT P) R)) *)
apply boxy_i; auto; intros.
(* Goal: @app_pred A AG (@unfash A AG P) w' *)
unfold unfash in *.
(* Goal: @app_pred A AG (@exist (forall _ : A, Prop) (fun p : forall _ : A, Prop => @hereditary A (@age A AG) p) (fun x : A => @app_pred nat ag_nat P (@level A AG x)) (subtypes.unfash_obligation_1 A AG P)) w' *)
simpl in H. destruct H.
(* Goal: @app_pred T agT (@unfash T agT P) w *)
(* Goal: @app_pred T agT (@sepcon T JoinT PermT agT AgeT Q R) w *)
hnf in H0|-*.
(* Goal: @app_pred nat ag_nat P (@level A as_age w') *)
replace (level w') with (level w); auto.
(* Goal: @eq nat (@level A AG w) (@level A AG w') *)
apply comparable_fashionR.
(* Goal: @app_pred nat ag_nat P (@level A as_age w') *)
eapply join_comparable; eauto.
Qed.

Hint Resolve @extend_unfash.

Lemma subp_unfash {A} `{Age_alg A}:
  forall (P Q : pred nat) (n: nat), (P >=> Q) n -> ( ! P >=> ! Q) n.
Proof.
(* Goal: forall (T : Type) (agT : ageable T) (JoinT : Join T) (PermT : @Perm_alg T JoinT) (_ : @Sep_alg T JoinT) (AgeT : @Age_alg T JoinT agT) (P : @pred nat ag_nat) (Q R : @pred T agT), @eq (@pred T agT) (@andp T agT (@unfash T agT P) (@sepcon T JoinT PermT agT AgeT Q R)) (@sepcon T JoinT PermT agT AgeT (@andp T agT (@unfash T agT P) Q) (@andp T agT (@unfash T agT P) R)) *)
intros.
(* Goal: @app_pred nat ag_nat (@fash A as_age (@imp A as_age (@unfash A as_age P) (@unfash A as_age Q))) n *)
intros w ?. specialize (H0 _ H1).
(* Goal: @app_pred A as_age (@imp A as_age (@unfash A as_age P) (@unfash A as_age Q)) w *)
intros w' ? ?. apply (H0 _ (necR_level' H2)).
(* Goal: @app_pred nat ag_nat P (@level A as_age w') *)
auto.
Qed.
Hint Resolve @subp_unfash.


Lemma unfash_sepcon_distrib:
        forall {T}{agT: ageable T}{JoinT: Join T}{PermT: Perm_alg T}{SepT: Sep_alg T}{AgeT: Age_alg T}
           (P: pred nat) (Q R: pred T),
               unfash P && (Q*R) = (unfash P && Q) * (unfash P && R).
Proof.
(* Goal: forall (T : Type) (agT : ageable T) (JoinT : Join T) (PermT : @Perm_alg T JoinT) (_ : @Sep_alg T JoinT) (AgeT : @Age_alg T JoinT agT) (P : @pred nat ag_nat) (Q R : @pred T agT), @eq (@pred T agT) (@andp T agT (@unfash T agT P) (@sepcon T JoinT PermT agT AgeT Q R)) (@sepcon T JoinT PermT agT AgeT (@andp T agT (@unfash T agT P) Q) (@andp T agT (@unfash T agT P) R)) *)
intros.
(* Goal: @eq (@pred T agT) (@andp T agT (@unfash T agT P) (@sepcon T JoinT PermT agT AgeT Q R)) (@sepcon T JoinT PermT agT AgeT (@andp T agT (@unfash T agT P) Q) (@andp T agT (@unfash T agT P) R)) *)
apply pred_ext.
(* Goal: @derives T agT (@andp T agT (@unfash T agT P) (@sepcon T JoinT PermT agT AgeT Q R)) (@sepcon T JoinT PermT agT AgeT (@andp T agT (@unfash T agT P) Q) (@andp T agT (@unfash T agT P) R)) *)
(* Goal: @derives T agT (@sepcon T JoinT PermT agT AgeT (@andp T agT (@unfash T agT P) Q) (@andp T agT (@unfash T agT P) R)) (@andp T agT (@unfash T agT P) (@sepcon T JoinT PermT agT AgeT Q R)) *)
intros w [? [w1 [w2 [? [? ?]]]]].
(* Goal: @app_pred nat ag_nat P (@level A as_age w') *)
exists w1; exists w2; repeat split; auto.
(* Goal: @app_pred T agT (@unfash T agT P) w2 *)
(* Goal: @derives T agT (@sepcon T JoinT PermT agT AgeT (@andp T agT (@unfash T agT P) Q) (@andp T agT (@unfash T agT P) R)) (@andp T agT (@unfash T agT P) (@sepcon T JoinT PermT agT AgeT Q R)) *)
apply join_level in H0. destruct H0.
(* Goal: @app_pred T agT (@unfash T agT P) w2 *)
(* Goal: @derives T agT (@sepcon T JoinT PermT agT AgeT (@andp T agT (@unfash T agT P) Q) (@andp T agT (@unfash T agT P) R)) (@andp T agT (@unfash T agT P) (@sepcon T JoinT PermT agT AgeT Q R)) *)
hnf in H|-*. congruence.
(* Goal: @app_pred T agT (@unfash T agT P) w2 *)
(* Goal: @derives T agT (@sepcon T JoinT PermT agT AgeT (@andp T agT (@unfash T agT P) Q) (@andp T agT (@unfash T agT P) R)) (@andp T agT (@unfash T agT P) (@sepcon T JoinT PermT agT AgeT Q R)) *)
apply join_level in H0. destruct H0.
(* Goal: @app_pred T agT (@unfash T agT P) w2 *)
(* Goal: @derives T agT (@sepcon T JoinT PermT agT AgeT (@andp T agT (@unfash T agT P) Q) (@andp T agT (@unfash T agT P) R)) (@andp T agT (@unfash T agT P) (@sepcon T JoinT PermT agT AgeT Q R)) *)
hnf in H|-*. congruence.
(* Goal: @derives T agT (@sepcon T JoinT PermT agT AgeT (@andp T agT (@unfash T agT P) Q) (@andp T agT (@unfash T agT P) R)) (@andp T agT (@unfash T agT P) (@sepcon T JoinT PermT agT AgeT Q R)) *)
intros w [w1 [w2 [? [[? ?] [? ?]]]]].
(* Goal: @app_pred T agT (@andp T agT (@unfash T agT P) (@sepcon T JoinT PermT agT AgeT Q R)) w *)
split.
(* Goal: @app_pred T agT (@unfash T agT P) w *)
(* Goal: @app_pred T agT (@sepcon T JoinT PermT agT AgeT Q R) w *)
apply join_level in H. destruct H.
(* Goal: @app_pred T agT (@unfash T agT P) w *)
(* Goal: @app_pred T agT (@sepcon T JoinT PermT agT AgeT Q R) w *)
hnf in H0|-*. congruence.
(* Goal: @app_pred nat ag_nat P (@level A as_age w') *)
exists w1; exists w2; repeat split; auto.
Qed.


