Require Import VST.veric.base.
Require Import VST.msl.msl_standard.
Require Import VST.veric.shares.
Require Import VST.veric.compcert_rmaps.
Require Import VST.veric.res_predicates.

Local Open Scope pred.

Definition cleave (sh: share) :=
  (Share.lub (fst (Share.split (Share.glb Share.Lsh sh))) (fst (Share.split (Share.glb Share.Rsh sh))),
   Share.lub (snd (Share.split (Share.glb Share.Lsh sh))) (snd (Share.split (Share.glb Share.Rsh sh)))).

Lemma cleave_join:
 forall sh: share, sepalg.join (fst (cleave sh)) (snd (cleave sh)) sh.
Proof.
(* Goal: forall (l : AV.address) (_ : not (adr_range a (size_chunk ch) l)), @identity resource Join_resource (resource_at w l) *)
(* Goal: @app_pred rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun i : address => @andp rmap ag_rmap (shareat i sh1) (nonlockat i)) noat)) noghost) (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun loc : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) sh2 loc) noat)) noghost)) w *)
intros.
(* Goal: @identity share Share.Join_ba (Share.glb Share.Rsh (@snd Share.t Share.t (cleave sh))) *)
unfold cleave.
(* Goal: @join Share.t Share.Join_ba (@fst Share.t Share.t (@pair Share.t Share.t (Share.lub (@fst Share.t Share.t (Share.split (Share.glb Share.Lsh sh))) (@fst Share.t Share.t (Share.split (Share.glb Share.Rsh sh)))) (Share.lub (@snd Share.t Share.t (Share.split (Share.glb Share.Lsh sh))) (@snd Share.t Share.t (Share.split (Share.glb Share.Rsh sh)))))) (@snd Share.t Share.t (@pair Share.t Share.t (Share.lub (@fst Share.t Share.t (Share.split (Share.glb Share.Lsh sh))) (@fst Share.t Share.t (Share.split (Share.glb Share.Rsh sh)))) (Share.lub (@snd Share.t Share.t (Share.split (Share.glb Share.Lsh sh))) (@snd Share.t Share.t (Share.split (Share.glb Share.Rsh sh)))))) sh *)
destruct (Share.split (Share.glb Share.Lsh sh)) as [a b] eqn:?H.
(* Goal: @identity share Share.Join_ba (Share.glb Share.Rsh (@snd Share.t Share.t (@pair Share.t Share.t a b))) *)
apply split_join in H.
(* Goal: @join Share.t Share.Join_ba (@fst Share.t Share.t (@pair Share.t Share.t (Share.lub (@fst Share.t Share.t (@pair Share.t Share.t a b)) (@fst Share.t Share.t (Share.split (Share.glb Share.Rsh sh)))) (Share.lub (@snd Share.t Share.t (@pair Share.t Share.t a b)) (@snd Share.t Share.t (Share.split (Share.glb Share.Rsh sh)))))) (@snd Share.t Share.t (@pair Share.t Share.t (Share.lub (@fst Share.t Share.t (@pair Share.t Share.t a b)) (@fst Share.t Share.t (Share.split (Share.glb Share.Rsh sh)))) (Share.lub (@snd Share.t Share.t (@pair Share.t Share.t a b)) (@snd Share.t Share.t (Share.split (Share.glb Share.Rsh sh)))))) sh *)
destruct (Share.split (Share.glb Share.Rsh sh)) as [e f] eqn:?H.
(* Goal: @eq Share.t (Share.glb Share.Rsh (Share.lub (@snd Share.t Share.t (@pair Share.t Share.t a0 b0)) (@snd Share.t Share.t (Share.split (Share.glb Share.Rsh sh0))))) (Share.glb Share.Rsh (Share.lub (@snd Share.t Share.t (Share.split (Share.glb Share.Lsh sh))) (@snd Share.t Share.t (Share.split (Share.glb Share.Rsh sh))))) *)
apply split_join in H0.
(* Goal: @join Share.t Share.Join_ba (@fst Share.t Share.t (@pair Share.t Share.t (Share.lub (@fst Share.t Share.t (@pair Share.t Share.t a b)) (@fst Share.t Share.t (@pair Share.t Share.t e f))) (Share.lub (@snd Share.t Share.t (@pair Share.t Share.t a b)) (@snd Share.t Share.t (@pair Share.t Share.t e f))))) (@snd Share.t Share.t (@pair Share.t Share.t (Share.lub (@fst Share.t Share.t (@pair Share.t Share.t a b)) (@fst Share.t Share.t (@pair Share.t Share.t e f))) (Share.lub (@snd Share.t Share.t (@pair Share.t Share.t a b)) (@snd Share.t Share.t (@pair Share.t Share.t e f))))) sh *)
destruct (Share.split sh) as [c g] eqn:?H.
(* Goal: @eq Share.t (Share.glb Share.Rsh (Share.lub (@snd Share.t Share.t (@pair Share.t Share.t a0 b0)) (@snd Share.t Share.t (Share.split (Share.glb Share.Rsh sh0))))) (Share.glb Share.Rsh (Share.lub (@snd Share.t Share.t (@pair Share.t Share.t a b)) (@snd Share.t Share.t (Share.split (Share.glb Share.Rsh sh))))) *)
apply split_join in H1.
(* Goal: @eq resource (slice_resource sh2 (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt)))) (YES sh2 rsh2 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt))) *)
simpl.
(* Goal: @join Share.t Share.Join_ba (Share.lub a e) (Share.lub b f) sh *)
destruct H1.
(* Goal: @join Share.t Share.Join_ba (Share.lub a e) (Share.lub b f) sh *)
subst sh.
(* Goal: @eq Share.t (Share.glb Share.Rsh b) Share.bot *)
destruct H.
(* Goal: and (@eq (option share) (resource_share (slice_resource sh1 (resource_at w loc))) (@Some share sh1)) (nonlock (slice_resource sh1 (resource_at w loc))) *)
destruct H0.
(* Goal: @app_pred rmap ag_rmap (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun loc : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) sh2 loc) noat)) noghost) w2 *)
split.
*
(* Goal: @eq Share.t (Share.glb Share.Rsh (Share.lub b0 d0)) (Share.glb Share.Rsh (Share.lub b d0)) *)
rewrite !Share.distrib1.
(* Goal: @eq Share.t (Share.lub (Share.glb (Share.lub a e) b) (Share.glb (Share.lub a e) f)) Share.bot *)
rewrite !(Share.glb_commute (Share.lub _ _)).
(* Goal: @eq Share.t (Share.glb Share.Rsh (Share.lub b0 d0)) (Share.glb Share.Rsh (Share.lub b d0)) *)
rewrite !Share.distrib1.
(* Goal: @eq Share.t (Share.lub (Share.lub (Share.glb b a) (Share.glb b e)) (Share.lub (Share.glb f a) (Share.glb f e))) Share.bot *)
rewrite (Share.glb_commute b a), (Share.glb_commute f e).
(* Goal: @eq Share.t (Share.lub (Share.lub (Share.glb a b) (Share.glb b e)) (Share.lub (Share.glb f a) (Share.glb e f))) Share.bot *)
rewrite H,H0.
(* Goal: @eq Share.t (Share.lub (Share.lub Share.bot (Share.glb b e)) (Share.lub (Share.glb f a) Share.bot)) Share.bot *)
rewrite (Share.lub_commute Share.bot).
(* Goal: @eq Share.t (Share.lub (Share.lub (Share.glb b e) Share.bot) (Share.lub (Share.glb f a) Share.bot)) Share.bot *)
rewrite !Share.lub_bot.
(* Goal: @eq Share.t (Share.lub (Share.glb b e) (Share.glb f a)) Share.bot *)
rewrite Share.distrib2.
(* Goal: @eq Share.t (Share.glb (Share.lub (Share.glb b e) f) (Share.lub (Share.glb b e) a)) Share.bot *)
rewrite !(Share.lub_commute (Share.glb _ _)).
(* Goal: @eq Share.t (Share.glb (Share.lub f (Share.glb b e)) (Share.lub a (Share.glb b e))) Share.bot *)
rewrite !Share.distrib2.
(* Goal: @eq Share.t (Share.glb (Share.glb (Share.lub f b) (Share.lub f e)) (Share.glb (Share.lub a b) (Share.lub a e))) Share.bot *)
rewrite (Share.lub_commute f e), H3, H2.
(* Goal: @eq Share.t (Share.glb (Share.glb (Share.lub f b) (Share.glb Share.Rsh (Share.lub c g))) (Share.glb (Share.glb Share.Lsh (Share.lub c g)) (Share.lub a e))) Share.bot *)
rewrite (Share.glb_commute (Share.lub _ _)).
(* Goal: @eq Share.t (Share.glb Share.Rsh (Share.glb (Share.glb Share.Lsh (Share.glb (Share.lub c g) (Share.lub a e))) (Share.glb (Share.lub c g) (Share.lub f b)))) Share.bot *)
rewrite (Share.glb_assoc Share.Lsh).
(* Goal: @eq Share.t (Share.glb (Share.glb (Share.glb Share.Rsh (Share.lub c g)) (Share.lub f b)) (Share.glb Share.Lsh (Share.glb (Share.lub c g) (Share.lub a e)))) Share.bot *)
rewrite !(Share.glb_assoc Share.Rsh).
(* Goal: @eq Share.t (Share.glb Share.Rsh (Share.glb (Share.glb (Share.lub c g) (Share.lub f b)) (Share.glb Share.Lsh (Share.glb (Share.lub c g) (Share.lub a e))))) Share.bot *)
rewrite (Share.glb_commute _ (Share.glb Share.Lsh _)).
(* Goal: @eq Share.t (Share.glb Share.Rsh (Share.glb (Share.glb Share.Lsh (Share.glb (Share.lub c g) (Share.lub a e))) (Share.glb (Share.lub c g) (Share.lub f b)))) Share.bot *)
rewrite (Share.glb_assoc Share.Lsh).
(* Goal: @eq Share.t (Share.glb Share.Rsh (Share.glb Share.Lsh (Share.glb (Share.glb (Share.lub c g) (Share.lub a e)) (Share.glb (Share.lub c g) (Share.lub f b))))) Share.bot *)
rewrite <- (Share.glb_assoc Share.Rsh).
(* Goal: @eq Share.t (Share.glb (Share.glb Share.Rsh Share.Lsh) (Share.glb (Share.glb (Share.lub c g) (Share.lub a e)) (Share.glb (Share.lub c g) (Share.lub f b)))) Share.bot *)
rewrite (Share.glb_commute Share.Rsh).
(* Goal: @eq Share.t (Share.glb (Share.glb Share.Lsh Share.Rsh) (Share.glb (Share.glb (Share.lub c g) (Share.lub a e)) (Share.glb (Share.lub c g) (Share.lub f b)))) Share.bot *)
rewrite glb_Lsh_Rsh.
(* Goal: @eq Share.t (Share.glb Share.bot (Share.glb (Share.glb (Share.lub c g) (Share.lub a e)) (Share.glb (Share.lub c g) (Share.lub f b)))) Share.bot *)
rewrite Share.glb_commute. apply Share.glb_bot.
*
(* Goal: @eq Share.t (Share.lub (Share.lub a e) (Share.lub b f)) (Share.lub c g) *)
rewrite Share.lub_assoc.
(* Goal: @eq Share.t (Share.lub a (Share.lub e (Share.lub b f))) (Share.lub c g) *)
rewrite (Share.lub_commute e).
(* Goal: @eq Share.t (Share.lub a (Share.lub (Share.lub b f) e)) (Share.lub c g) *)
rewrite (Share.lub_assoc b).
(* Goal: @eq Share.t (Share.lub a (Share.lub b (Share.lub f e))) (Share.lub c g) *)
rewrite <- Share.lub_assoc.
(* Goal: if adr_range_dec a (size_chunk ch) loc then and (@eq (option share) (resource_share (resource_at w1 loc)) (@Some share sh1)) (nonlock (resource_at w1 loc)) else @identity resource Join_resource (resource_at w1 loc) *)
(* Goal: @app_pred rmap ag_rmap noghost w1 *)
rewrite H2.
(* Goal: @eq Share.t (Share.lub (Share.glb Share.Lsh (Share.lub c g)) (Share.lub f e)) (Share.lub c g) *)
rewrite (Share.lub_commute f e), H3.
(* Goal: @identity share Share.Join_ba (Share.glb Share.Rsh (@snd Share.t Share.t (Share.split (Share.glb Share.Lsh sh)))) *)
clear.
(* Goal: @eq Share.t (Share.lub (Share.glb Share.Lsh (Share.lub c g)) (Share.glb Share.Rsh (Share.lub c g))) (Share.lub c g) *)
do 2 rewrite (Share.glb_commute _ (Share.lub _ _)).
(* Goal: @eq Share.t (Share.lub (Share.glb (Share.lub c g) Share.Lsh) (Share.glb (Share.lub c g) Share.Rsh)) (Share.lub c g) *)
rewrite <- Share.distrib1.
(* Goal: @eq Share.t (Share.glb (Share.lub c g) (Share.lub Share.Lsh Share.Rsh)) (Share.lub c g) *)
rewrite lub_Lsh_Rsh.
(* Goal: @eq Share.t (Share.glb (Share.lub c g) Share.top) (Share.lub c g) *)
apply Share.glb_top.
Qed.

Lemma cleave_readable1:
 forall sh, readable_share sh -> readable_share (fst (cleave sh)).
Proof.
(* Goal: forall (l : AV.address) (_ : not (adr_range a (size_chunk ch) l)), @identity resource Join_resource (resource_at w l) *)
(* Goal: @app_pred rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun i : address => @andp rmap ag_rmap (shareat i sh1) (nonlockat i)) noat)) noghost) (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun loc : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) sh2 loc) noat)) noghost)) w *)
intros.
hnf in H|-*. contradict H.
(* Goal: @identity share Share.Join_ba (Share.glb Share.Rsh (Share.lub (@snd Share.t Share.t (Share.split (Share.glb Share.Lsh sh))) b)) *)
apply identity_share_bot in H.
(* Goal: @identity share Share.Join_ba (Share.glb Share.Rsh sh) *)
unfold cleave in H.
(* Goal: @identity share Share.Join_ba (Share.glb Share.Rsh sh) *)
simpl in H.
(* Goal: @identity share Share.Join_ba (Share.glb Share.Rsh sh) *)
rewrite Share.distrib1 in H.
(* Goal: @identity share Share.Join_ba (Share.glb Share.Rsh sh) *)
apply lub_bot_e in H. destruct H as [_ ?].
(* Goal: @identity share Share.Join_ba (Share.glb Share.Rsh sh) *)
destruct (Share.split (Share.glb Share.Rsh sh)) as [c d] eqn:H1.
(* Goal: @identity share Share.Join_ba (Share.glb Share.Rsh sh) *)
apply (split_nontrivial' _ _ _ H1).
(* Goal: or (@identity Share.t Share.Join_ba c) (@identity Share.t Share.Join_ba d) *)
left.
(* Goal: @eq Share.t (Share.glb Share.Rsh (Share.lub (@snd Share.t Share.t (@pair Share.t Share.t a0 b0)) (@snd Share.t Share.t (Share.split (Share.glb Share.Rsh sh0))))) (Share.glb Share.Rsh (Share.lub (@snd Share.t Share.t (@pair Share.t Share.t a b)) (@snd Share.t Share.t (Share.split (Share.glb Share.Rsh sh))))) *)
apply split_join in H1.
simpl in *.
(* Goal: @identity Share.t Share.Join_ba d *)
destruct (join_parts1 comp_Rsh_Lsh H1).
(* Goal: @identity Share.t Share.Join_ba d *)
rewrite <- H0, H.
(* Goal: @identity share Share.Join_ba Share.bot *)
(* Goal: @eq Share.t Share.bot (Share.glb Share.Rsh b) *)
apply bot_identity.
Qed.

Lemma cleave_readable2:
 forall sh, readable_share sh -> readable_share (snd (cleave sh)).
Proof.
(* Goal: forall (l : AV.address) (_ : not (adr_range a (size_chunk ch) l)), @identity resource Join_resource (resource_at w l) *)
(* Goal: @app_pred rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun i : address => @andp rmap ag_rmap (shareat i sh1) (nonlockat i)) noat)) noghost) (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun loc : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) sh2 loc) noat)) noghost)) w *)
intros.
hnf in H|-*. contradict H.
(* Goal: @identity share Share.Join_ba (Share.glb Share.Rsh (Share.lub (@snd Share.t Share.t (Share.split (Share.glb Share.Lsh sh))) b)) *)
apply identity_share_bot in H.
(* Goal: @identity share Share.Join_ba (Share.glb Share.Rsh sh) *)
unfold cleave in H.
(* Goal: @identity share Share.Join_ba (Share.glb Share.Rsh sh) *)
simpl in H.
(* Goal: @identity share Share.Join_ba (Share.glb Share.Rsh sh) *)
rewrite Share.distrib1 in H.
(* Goal: @identity share Share.Join_ba (Share.glb Share.Rsh sh) *)
apply lub_bot_e in H. destruct H as [_ ?].
(* Goal: @identity share Share.Join_ba (Share.glb Share.Rsh sh) *)
destruct (Share.split (Share.glb Share.Rsh sh)) as [c d] eqn:H1.
(* Goal: @identity share Share.Join_ba (Share.glb Share.Rsh sh) *)
apply (split_nontrivial' _ _ _ H1).
simpl in *.
(* Goal: or (@identity Share.t Share.Join_ba c) (@identity Share.t Share.Join_ba d) *)
right.
(* Goal: @eq Share.t (Share.glb Share.Rsh (Share.lub (@snd Share.t Share.t (@pair Share.t Share.t a0 b0)) (@snd Share.t Share.t (Share.split (Share.glb Share.Rsh sh0))))) (Share.glb Share.Rsh (Share.lub (@snd Share.t Share.t (@pair Share.t Share.t a b)) (@snd Share.t Share.t (Share.split (Share.glb Share.Rsh sh))))) *)
apply split_join in H1.
(* Goal: @eq Share.t (Share.glb Share.Rsh (Share.lub (@snd Share.t Share.t (@pair Share.t Share.t a0 b0)) (@snd Share.t Share.t (Share.split (Share.glb Share.Rsh sh0))))) (Share.glb Share.Rsh (Share.lub (@snd Share.t Share.t (@pair Share.t Share.t a b)) (@snd Share.t Share.t (Share.split (Share.glb Share.Rsh sh))))) *)
apply join_comm in H1.
simpl in *.
(* Goal: @identity Share.t Share.Join_ba d *)
destruct (join_parts1 comp_Rsh_Lsh H1).
(* Goal: @identity Share.t Share.Join_ba d *)
rewrite <- H0, H.
(* Goal: @identity share Share.Join_ba Share.bot *)
(* Goal: @eq Share.t Share.bot (Share.glb Share.Rsh b) *)
apply bot_identity.
Qed.

Lemma rshare_sh_readable:
 forall r, readable_share (rshare_sh r).
Proof.
(* Goal: @eq resource (slice_resource sh2 (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt)))) (YES sh2 rsh2 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt))) *)
destruct r; simpl.
destruct p;
(* Goal: @identity resource Join_resource (resource_at w l) *)
auto.
Qed.

Lemma cleave_nonreadable1:
  forall sh, ~readable_share sh -> ~ readable_share (fst (cleave sh)).
Proof.
(* Goal: forall (l : AV.address) (_ : not (adr_range a (size_chunk ch) l)), @identity resource Join_resource (resource_at w l) *)
(* Goal: @app_pred rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun i : address => @andp rmap ag_rmap (shareat i sh1) (nonlockat i)) noat)) noghost) (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun loc : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) sh2 loc) noat)) noghost)) w *)
intros.
(* Goal: not (@identity share Share.Join_ba (Share.glb Share.Rsh sh)) *)
contradict H.
do 3 red in H|-*.
(* Goal: not (@identity share Share.Join_ba (Share.glb Share.Rsh sh)) *)
contradict H.
(* Goal: @identity share Share.Join_ba (Share.glb Share.Rsh (@snd Share.t Share.t (cleave sh))) *)
unfold cleave. simpl.
(* Goal: @identity share Share.Join_ba (Share.glb Share.Rsh (Share.lub (@snd Share.t Share.t (Share.split (Share.glb Share.Lsh sh))) b)) *)
apply identity_share_bot in H.
(* Goal: @identity share Share.Join_ba (Share.glb Share.Rsh (Share.lub (@snd Share.t Share.t (Share.split (Share.glb Share.Lsh sh))) (@snd Share.t Share.t (Share.split (Share.glb Share.Rsh sh))))) *)
rewrite H. clear H.
(* Goal: @identity share Share.Join_ba (Share.glb Share.Rsh (Share.lub (@snd Share.t Share.t (Share.split (Share.glb Share.Lsh sh))) (@snd Share.t Share.t (Share.split Share.bot)))) *)
destruct (Share.split Share.bot) as [a b] eqn:?H.
(* Goal: @identity share Share.Join_ba (Share.glb Share.Rsh (@snd Share.t Share.t (@pair Share.t Share.t a b))) *)
apply split_join in H.
(* Goal: @eq resource (slice_resource sh2 (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt)))) (YES sh2 rsh2 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt))) *)
simpl.
(* Goal: @identity share Share.Join_ba (Share.glb Share.Rsh (Share.lub (@snd Share.t Share.t (Share.split (Share.glb Share.Lsh sh))) b)) *)
apply split_identity in H; [ | apply bot_identity].
(* Goal: @identity share Share.Join_ba (Share.glb Share.Rsh (Share.lub (@snd Share.t Share.t (Share.split (Share.glb Share.Lsh sh))) b)) *)
apply identity_share_bot in H. subst.
(* Goal: @eq Share.t (Share.glb Share.Lsh sh) (Share.lub (Share.glb Share.Lsh sh) Share.bot) *)
rewrite Share.lub_bot.
(* Goal: @identity share Share.Join_ba (Share.glb Share.Rsh (@snd Share.t Share.t (Share.split (Share.glb Share.Lsh sh)))) *)
clear.
(* Goal: @identity share Share.Join_ba (Share.glb Share.Rsh (@snd Share.t Share.t (Share.split (Share.glb Share.Lsh sh)))) *)
destruct (Share.split (Share.glb Share.Lsh sh)) as [a b] eqn:H.
(* Goal: @identity share Share.Join_ba (Share.glb Share.Rsh (@snd Share.t Share.t (@pair Share.t Share.t a b))) *)
apply split_join in H.
(* Goal: @eq resource (slice_resource sh2 (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt)))) (YES sh2 rsh2 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt))) *)
simpl.
(* Goal: @identity share Share.Join_ba (Share.glb Share.Rsh a) *)
replace (Share.glb Share.Rsh a) with Share.bot.
(* Goal: @identity share Share.Join_ba Share.bot *)
(* Goal: @eq Share.t Share.bot (Share.glb Share.Rsh b) *)
apply bot_identity.
(* Goal: @eq Share.t sh' (retainer_part sh') *)
symmetry.
(* Goal: @eq Share.t (Share.glb Share.Rsh b) Share.bot *)
destruct H.
(* Goal: @eq Share.t (Share.glb Share.Rsh b) Share.bot *)
apply (f_equal (Share.glb Share.Rsh)) in H0.
(* Goal: @eq Share.t (Share.glb Share.Rsh b) Share.bot *)
rewrite <- Share.glb_assoc in H0.
(* Goal: @eq Share.t (Share.glb Share.Rsh b) Share.bot *)
rewrite (Share.glb_commute _ Share.Lsh) in H0.
(* Goal: @eq Share.t (Share.glb Share.Rsh b) Share.bot *)
rewrite glb_Lsh_Rsh in H0.
(* Goal: @eq Share.t (Share.glb Share.Rsh b) Share.bot *)
rewrite (Share.glb_commute Share.bot) in H0.
(* Goal: @eq Share.t (Share.glb Share.Rsh b) Share.bot *)
rewrite Share.glb_bot in H0.
(* Goal: @eq Share.t (Share.glb Share.Rsh b) Share.bot *)
rewrite Share.distrib1 in H0.
(* Goal: @eq Share.t (Share.glb Share.Rsh b) Share.bot *)
apply lub_bot_e in H0. destruct H0 as [? _].
(* Goal: @identity resource Join_resource (resource_at w l) *)
auto.
Qed.

Lemma cleave_nonreadable2:
  forall sh, ~readable_share sh -> ~ readable_share (snd (cleave sh)).
Proof.
(* Goal: forall (l : AV.address) (_ : not (adr_range a (size_chunk ch) l)), @identity resource Join_resource (resource_at w l) *)
(* Goal: @app_pred rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun i : address => @andp rmap ag_rmap (shareat i sh1) (nonlockat i)) noat)) noghost) (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun loc : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) sh2 loc) noat)) noghost)) w *)
intros.
(* Goal: not (@identity share Share.Join_ba (Share.glb Share.Rsh sh)) *)
contradict H.
do 3 red in H|-*.
(* Goal: not (@identity share Share.Join_ba (Share.glb Share.Rsh sh)) *)
contradict H.
(* Goal: @identity share Share.Join_ba (Share.glb Share.Rsh (@snd Share.t Share.t (cleave sh))) *)
unfold cleave. simpl.
(* Goal: @identity share Share.Join_ba (Share.glb Share.Rsh (Share.lub (@snd Share.t Share.t (Share.split (Share.glb Share.Lsh sh))) b)) *)
apply identity_share_bot in H.
(* Goal: @identity share Share.Join_ba (Share.glb Share.Rsh (Share.lub (@snd Share.t Share.t (Share.split (Share.glb Share.Lsh sh))) (@snd Share.t Share.t (Share.split (Share.glb Share.Rsh sh))))) *)
rewrite H. clear H.
(* Goal: @identity share Share.Join_ba (Share.glb Share.Rsh (Share.lub (@snd Share.t Share.t (Share.split (Share.glb Share.Lsh sh))) (@snd Share.t Share.t (Share.split Share.bot)))) *)
destruct (Share.split Share.bot) as [a b] eqn:?H.
(* Goal: @identity share Share.Join_ba (Share.glb Share.Rsh (@snd Share.t Share.t (@pair Share.t Share.t a b))) *)
apply split_join in H.
(* Goal: @eq resource (slice_resource sh2 (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt)))) (YES sh2 rsh2 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt))) *)
simpl.
(* Goal: @identity share Share.Join_ba (Share.glb Share.Rsh (Share.lub (@snd Share.t Share.t (Share.split (Share.glb Share.Lsh sh))) b)) *)
apply join_comm in H.
(* Goal: @identity share Share.Join_ba (Share.glb Share.Rsh (Share.lub (@snd Share.t Share.t (Share.split (Share.glb Share.Lsh sh))) b)) *)
apply split_identity in H; [ | apply bot_identity].
(* Goal: @identity share Share.Join_ba (Share.glb Share.Rsh (Share.lub (@snd Share.t Share.t (Share.split (Share.glb Share.Lsh sh))) b)) *)
apply identity_share_bot in H. subst.
(* Goal: @eq Share.t (Share.glb Share.Lsh sh) (Share.lub (Share.glb Share.Lsh sh) Share.bot) *)
rewrite Share.lub_bot.
(* Goal: @identity share Share.Join_ba (Share.glb Share.Rsh (@snd Share.t Share.t (Share.split (Share.glb Share.Lsh sh)))) *)
clear.
(* Goal: @identity share Share.Join_ba (Share.glb Share.Rsh (@snd Share.t Share.t (Share.split (Share.glb Share.Lsh sh)))) *)
destruct (Share.split (Share.glb Share.Lsh sh)) as [a b] eqn:H.
(* Goal: @identity share Share.Join_ba (Share.glb Share.Rsh (@snd Share.t Share.t (@pair Share.t Share.t a b))) *)
apply split_join in H.
(* Goal: @eq resource (slice_resource sh2 (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt)))) (YES sh2 rsh2 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt))) *)
simpl.
(* Goal: @identity share Share.Join_ba (Share.glb Share.Rsh b) *)
replace (Share.glb Share.Rsh b) with Share.bot.
(* Goal: @identity share Share.Join_ba Share.bot *)
(* Goal: @eq Share.t Share.bot (Share.glb Share.Rsh b) *)
apply bot_identity.
(* Goal: @eq Share.t sh' (retainer_part sh') *)
symmetry.
(* Goal: @eq Share.t (Share.glb Share.Rsh b) Share.bot *)
destruct H.
(* Goal: @eq Share.t (Share.glb Share.Rsh b) Share.bot *)
apply (f_equal (Share.glb Share.Rsh)) in H0.
(* Goal: @eq Share.t (Share.glb Share.Rsh b) Share.bot *)
rewrite <- Share.glb_assoc in H0.
(* Goal: @eq Share.t (Share.glb Share.Rsh b) Share.bot *)
rewrite (Share.glb_commute _ Share.Lsh) in H0.
(* Goal: @eq Share.t (Share.glb Share.Rsh b) Share.bot *)
rewrite glb_Lsh_Rsh in H0.
(* Goal: @eq Share.t (Share.glb Share.Rsh b) Share.bot *)
rewrite (Share.glb_commute Share.bot) in H0.
(* Goal: @eq Share.t (Share.glb Share.Rsh b) Share.bot *)
rewrite Share.glb_bot in H0.
(* Goal: @eq Share.t (Share.glb Share.Rsh b) Share.bot *)
rewrite Share.lub_commute in H0.
(* Goal: @eq Share.t (Share.glb Share.Rsh b) Share.bot *)
rewrite Share.distrib1 in H0.
(* Goal: @eq Share.t (Share.glb Share.Rsh b) Share.bot *)
apply lub_bot_e in H0. destruct H0 as [? _].
(* Goal: @identity resource Join_resource (resource_at w l) *)
auto.
Qed.

Definition split_resource r :=
  match r with YES sh rsh k pp => 
               (YES (fst (cleave sh)) (cleave_readable1 _ rsh) k pp , 
                YES (snd (cleave sh)) (cleave_readable2 _ rsh) k pp)
             | PURE k pp => (PURE k pp, PURE k pp)
             | NO sh nsh => (NO (fst (cleave sh)) (cleave_nonreadable1 _ nsh),
                             NO (snd (cleave sh)) (cleave_nonreadable2 _ nsh))
  end.


Lemma glb_cleave_lemma1: forall sh0 sh,
  Share.glb Share.Rsh sh0 = Share.glb Share.Rsh sh ->
 Share.glb Share.Rsh (fst (cleave sh0)) =
 Share.glb Share.Rsh (fst (cleave sh)).
Proof.
(* Goal: forall (l : AV.address) (_ : not (adr_range a (size_chunk ch) l)), @identity resource Join_resource (resource_at w l) *)
(* Goal: @app_pred rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun i : address => @andp rmap ag_rmap (shareat i sh1) (nonlockat i)) noat)) noghost) (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun loc : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) sh2 loc) noat)) noghost)) w *)
intros.
(* Goal: @eq resource (slice_resource sh2 (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt)))) (YES sh2 rsh2 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt))) *)
unfold cleave; simpl.
destruct (Share.split (Share.glb Share.Lsh sh0)) as [a0 b0]  eqn:H0.
(* Goal: @eq Share.t (Share.glb Share.Rsh (Share.lub (@snd Share.t Share.t (@pair Share.t Share.t a0 b0)) (@snd Share.t Share.t (Share.split (Share.glb Share.Rsh sh0))))) (Share.glb Share.Rsh (Share.lub (@snd Share.t Share.t (Share.split (Share.glb Share.Lsh sh))) (@snd Share.t Share.t (Share.split (Share.glb Share.Rsh sh))))) *)
apply split_join in H0.
destruct (Share.split (Share.glb Share.Lsh sh)) as [a b]  eqn:H1.
(* Goal: @eq Share.t (Share.glb Share.Rsh (Share.lub (@snd Share.t Share.t (@pair Share.t Share.t a0 b0)) (@snd Share.t Share.t (Share.split (Share.glb Share.Rsh sh0))))) (Share.glb Share.Rsh (Share.lub (@snd Share.t Share.t (@pair Share.t Share.t a b)) (@snd Share.t Share.t (Share.split (Share.glb Share.Rsh sh))))) *)
apply split_join in H1.
destruct (Share.split (Share.glb Share.Rsh sh0)) as [c0 d0]  eqn:H2.
(* Goal: if adr_range_dec a (size_chunk ch) loc then and (@eq (option share) (resource_share (resource_at w1 loc)) (@Some share sh1)) (nonlock (resource_at w1 loc)) else @identity resource Join_resource (resource_at w1 loc) *)
(* Goal: @app_pred rmap ag_rmap noghost w1 *)
rewrite H in H2. rewrite H2.
(* Goal: @eq resource (slice_resource sh2 (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt)))) (YES sh2 rsh2 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt))) *)
simpl.
(* Goal: @eq Share.t (Share.glb Share.Rsh (Share.lub b0 d0)) (Share.glb Share.Rsh (Share.lub b d0)) *)
apply split_join in H2.
(* Goal: @eq Share.t (Share.glb Share.Rsh (Share.lub b0 d0)) (Share.glb Share.Rsh (Share.lub b d0)) *)
rewrite !Share.distrib1.
(* Goal: @eq Share.t (Share.lub (Share.glb Share.Rsh b0) (Share.glb Share.Rsh d0)) (Share.lub (Share.glb Share.Rsh b) (Share.glb Share.Rsh d0)) *)
apply (join_parts1 comp_Lsh_Rsh) in H1.
(* Goal: @eq Share.t (Share.lub (Share.glb Share.Rsh b0) (Share.glb Share.Rsh d0)) (Share.lub (Share.glb Share.Rsh b) (Share.glb Share.Rsh d0)) *)
destruct H1 as [_ ?]. rewrite H1.
(* Goal: @eq Share.t (Share.lub (Share.glb Share.Rsh b0) (Share.glb Share.Rsh d0)) (Share.lub Share.bot (Share.glb Share.Rsh d0)) *)
apply (join_parts1 comp_Lsh_Rsh) in H0.
(* Goal: @eq Share.t (Share.lub (Share.glb Share.Rsh b0) (Share.glb Share.Rsh d0)) (Share.lub Share.bot (Share.glb Share.Rsh d0)) *)
destruct H0 as [_ ?]. rewrite H0.
(* Goal: @identity resource Join_resource (resource_at w l) *)
auto.
Qed.

Lemma glb_cleave_lemma2: forall sh0 sh,
  Share.glb Share.Rsh sh0 = Share.glb Share.Rsh sh ->
 Share.glb Share.Rsh (snd (cleave sh0)) =
 Share.glb Share.Rsh (snd (cleave sh)).
Proof.
(* Goal: forall (l : AV.address) (_ : not (adr_range a (size_chunk ch) l)), @identity resource Join_resource (resource_at w l) *)
(* Goal: @app_pred rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun i : address => @andp rmap ag_rmap (shareat i sh1) (nonlockat i)) noat)) noghost) (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun loc : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) sh2 loc) noat)) noghost)) w *)
intros.
(* Goal: @eq resource (slice_resource sh2 (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt)))) (YES sh2 rsh2 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt))) *)
unfold cleave; simpl.
destruct (Share.split (Share.glb Share.Lsh sh0)) as [a0 b0]  eqn:H0.
(* Goal: @eq Share.t (Share.glb Share.Rsh (Share.lub (@snd Share.t Share.t (@pair Share.t Share.t a0 b0)) (@snd Share.t Share.t (Share.split (Share.glb Share.Rsh sh0))))) (Share.glb Share.Rsh (Share.lub (@snd Share.t Share.t (Share.split (Share.glb Share.Lsh sh))) (@snd Share.t Share.t (Share.split (Share.glb Share.Rsh sh))))) *)
apply split_join in H0.
destruct (Share.split (Share.glb Share.Lsh sh)) as [a b]  eqn:H1.
(* Goal: @eq Share.t (Share.glb Share.Rsh (Share.lub (@snd Share.t Share.t (@pair Share.t Share.t a0 b0)) (@snd Share.t Share.t (Share.split (Share.glb Share.Rsh sh0))))) (Share.glb Share.Rsh (Share.lub (@snd Share.t Share.t (@pair Share.t Share.t a b)) (@snd Share.t Share.t (Share.split (Share.glb Share.Rsh sh))))) *)
apply split_join in H1.
(* Goal: @eq Share.t (Share.glb Share.Rsh (Share.lub (@snd Share.t Share.t (@pair Share.t Share.t a0 b0)) (@snd Share.t Share.t (Share.split (Share.glb Share.Rsh sh0))))) (Share.glb Share.Rsh (Share.lub (@snd Share.t Share.t (@pair Share.t Share.t a b)) (@snd Share.t Share.t (Share.split (Share.glb Share.Rsh sh))))) *)
apply join_comm in H0.
(* Goal: @eq Share.t (Share.glb Share.Rsh (Share.lub (@snd Share.t Share.t (@pair Share.t Share.t a0 b0)) (@snd Share.t Share.t (Share.split (Share.glb Share.Rsh sh0))))) (Share.glb Share.Rsh (Share.lub (@snd Share.t Share.t (@pair Share.t Share.t a b)) (@snd Share.t Share.t (Share.split (Share.glb Share.Rsh sh))))) *)
apply join_comm in H1.
destruct (Share.split (Share.glb Share.Rsh sh0)) as [c0 d0]  eqn:H2.
(* Goal: if adr_range_dec a (size_chunk ch) loc then and (@eq (option share) (resource_share (resource_at w1 loc)) (@Some share sh1)) (nonlock (resource_at w1 loc)) else @identity resource Join_resource (resource_at w1 loc) *)
(* Goal: @app_pred rmap ag_rmap noghost w1 *)
rewrite H in H2. rewrite H2.
(* Goal: @eq resource (slice_resource sh2 (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt)))) (YES sh2 rsh2 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt))) *)
simpl.
(* Goal: @eq Share.t (Share.glb Share.Rsh (Share.lub b0 d0)) (Share.glb Share.Rsh (Share.lub b d0)) *)
apply split_join in H2.
(* Goal: @eq Share.t (Share.glb Share.Rsh (Share.lub b0 d0)) (Share.glb Share.Rsh (Share.lub b d0)) *)
rewrite !Share.distrib1.
(* Goal: @eq Share.t (Share.lub (Share.glb Share.Rsh b0) (Share.glb Share.Rsh d0)) (Share.lub (Share.glb Share.Rsh b) (Share.glb Share.Rsh d0)) *)
apply (join_parts1 comp_Lsh_Rsh) in H1.
(* Goal: @eq Share.t (Share.lub (Share.glb Share.Rsh b0) (Share.glb Share.Rsh d0)) (Share.lub (Share.glb Share.Rsh b) (Share.glb Share.Rsh d0)) *)
destruct H1 as [_ ?]. rewrite H1.
(* Goal: @eq Share.t (Share.lub (Share.glb Share.Rsh b0) (Share.glb Share.Rsh d0)) (Share.lub Share.bot (Share.glb Share.Rsh d0)) *)
apply (join_parts1 comp_Lsh_Rsh) in H0.
(* Goal: @eq Share.t (Share.lub (Share.glb Share.Rsh b0) (Share.glb Share.Rsh d0)) (Share.lub Share.bot (Share.glb Share.Rsh d0)) *)
destruct H0 as [_ ?]. rewrite H0.
(* Goal: @identity resource Join_resource (resource_at w l) *)
auto.
Qed.

Lemma split_rmap_ok1: forall m,
  resource_fmap (approx (level m)) (approx (level m)) oo (fun l => fst (split_resource (m @ l))) =
       (fun l => fst (split_resource (m @ l))).
Proof.
(* Goal: forall (l : AV.address) (_ : not (adr_range a (size_chunk ch) l)), @identity resource Join_resource (resource_at w l) *)
(* Goal: @app_pred rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun i : address => @andp rmap ag_rmap (shareat i sh1) (nonlockat i)) noat)) noghost) (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun loc : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) sh2 loc) noat)) noghost)) w *)
intros.
(* Goal: @eq resource (slice_resource sh2 (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt)))) (YES sh2 rsh2 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt))) *)
extensionality l; unfold compose; simpl.
(* Goal: @identity resource Join_resource (resource_at w l) *)
case_eq (m@l); simpl; intros; auto.
(* Goal: @eq resource (PURE k (preds_fmap (approx (@level rmap ag_rmap m)) (approx (@level rmap ag_rmap m)) p)) (PURE k p) *)
generalize (eq_sym (resource_at_approx m l)); intro.
(* Goal: @eq resource (PURE k (preds_fmap (approx (@level rmap ag_rmap m)) (approx (@level rmap ag_rmap m)) p)) (PURE k p) *)
pattern (m@l) at 2 in H0; rewrite H in H0.
(* Goal: @eq resource (slice_resource sh2 (resource_at w loc)) (YES sh2 rsh2 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt))) *)
simpl in H0.
(* Goal: @eq resource (PURE k (preds_fmap (approx (@level rmap ag_rmap m)) (approx (@level rmap ag_rmap m)) p)) (PURE k p) *)
rewrite H in H0.
(* Goal: @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (YES sh r0 k p0)) (YES sh r0 k p0) *)
inversion H0.
(* Goal: @eq resource (PURE k (preds_fmap (approx (@level rmap ag_rmap m)) (approx (@level rmap ag_rmap m)) p)) (PURE k p) *)
rewrite <- H2.
(* Goal: @eq resource (PURE k (preds_fmap (approx (@level rmap ag_rmap m)) (approx (@level rmap ag_rmap m)) p)) (PURE k p) *)
rewrite <- H2.
(* Goal: @identity resource Join_resource (resource_at w l) *)
auto.
(* Goal: @eq resource (PURE k (preds_fmap (approx (@level rmap ag_rmap m)) (approx (@level rmap ag_rmap m)) p)) (PURE k p) *)
generalize (eq_sym (resource_at_approx m l)); intro.
(* Goal: @eq resource (PURE k (preds_fmap (approx (@level rmap ag_rmap m)) (approx (@level rmap ag_rmap m)) p)) (PURE k p) *)
pattern (m@l) at 2 in H0; rewrite H in H0.
(* Goal: @eq resource (slice_resource sh2 (resource_at w loc)) (YES sh2 rsh2 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt))) *)
simpl in H0.
(* Goal: @eq resource (PURE k (preds_fmap (approx (@level rmap ag_rmap m)) (approx (@level rmap ag_rmap m)) p)) (PURE k p) *)
rewrite H in H0.
(* Goal: @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (YES sh r0 k p0)) (YES sh r0 k p0) *)
inversion H0.
(* Goal: @eq resource (PURE k (preds_fmap (approx (@level rmap ag_rmap m)) (approx (@level rmap ag_rmap m)) p)) (PURE k p) *)
rewrite <- H2.
(* Goal: @eq resource (PURE k (preds_fmap (approx (@level rmap ag_rmap m)) (approx (@level rmap ag_rmap m)) p)) (PURE k p) *)
rewrite <- H2.
(* Goal: @identity resource Join_resource (resource_at w l) *)
auto.
Qed.

Lemma split_rmap_ok2: forall m,
  resource_fmap (approx (level m)) (approx (level m)) oo (fun l => snd (split_resource (m @ l))) =
       (fun l => snd (split_resource (m @ l))).
Proof.
(* Goal: forall (l : AV.address) (_ : not (adr_range a (size_chunk ch) l)), @identity resource Join_resource (resource_at w l) *)
(* Goal: @app_pred rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun i : address => @andp rmap ag_rmap (shareat i sh1) (nonlockat i)) noat)) noghost) (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun loc : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) sh2 loc) noat)) noghost)) w *)
intros.
(* Goal: @eq resource (slice_resource sh2 (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt)))) (YES sh2 rsh2 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt))) *)
extensionality l; unfold compose; simpl.
(* Goal: @identity resource Join_resource (resource_at w l) *)
case_eq (m@l); simpl; intros; auto.
(* Goal: @eq resource (PURE k (preds_fmap (approx (@level rmap ag_rmap m)) (approx (@level rmap ag_rmap m)) p)) (PURE k p) *)
generalize (eq_sym (resource_at_approx m l)); intro.
(* Goal: @eq resource (PURE k (preds_fmap (approx (@level rmap ag_rmap m)) (approx (@level rmap ag_rmap m)) p)) (PURE k p) *)
pattern (m@l) at 2 in H0; rewrite H in H0.
(* Goal: @eq resource (slice_resource sh2 (resource_at w loc)) (YES sh2 rsh2 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt))) *)
simpl in H0.
(* Goal: @eq resource (PURE k (preds_fmap (approx (@level rmap ag_rmap m)) (approx (@level rmap ag_rmap m)) p)) (PURE k p) *)
rewrite H in H0.
(* Goal: @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (YES sh r0 k p0)) (YES sh r0 k p0) *)
inversion H0.
(* Goal: @eq resource (PURE k (preds_fmap (approx (@level rmap ag_rmap m)) (approx (@level rmap ag_rmap m)) p)) (PURE k p) *)
rewrite <- H2.
(* Goal: @eq resource (PURE k (preds_fmap (approx (@level rmap ag_rmap m)) (approx (@level rmap ag_rmap m)) p)) (PURE k p) *)
rewrite <- H2.
(* Goal: @identity resource Join_resource (resource_at w l) *)
auto.
(* Goal: @eq resource (PURE k (preds_fmap (approx (@level rmap ag_rmap m)) (approx (@level rmap ag_rmap m)) p)) (PURE k p) *)
generalize (eq_sym (resource_at_approx m l)); intro.
(* Goal: @eq resource (PURE k (preds_fmap (approx (@level rmap ag_rmap m)) (approx (@level rmap ag_rmap m)) p)) (PURE k p) *)
pattern (m@l) at 2 in H0; rewrite H in H0.
(* Goal: @eq resource (slice_resource sh2 (resource_at w loc)) (YES sh2 rsh2 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt))) *)
simpl in H0.
(* Goal: @eq resource (PURE k (preds_fmap (approx (@level rmap ag_rmap m)) (approx (@level rmap ag_rmap m)) p)) (PURE k p) *)
rewrite H in H0.
(* Goal: @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (YES sh r0 k p0)) (YES sh r0 k p0) *)
inversion H0.
(* Goal: @eq resource (PURE k (preds_fmap (approx (@level rmap ag_rmap m)) (approx (@level rmap ag_rmap m)) p)) (PURE k p) *)
rewrite <- H2.
(* Goal: @eq resource (PURE k (preds_fmap (approx (@level rmap ag_rmap m)) (approx (@level rmap ag_rmap m)) p)) (PURE k p) *)
rewrite <- H2.
(* Goal: @identity resource Join_resource (resource_at w l) *)
auto.
Qed.

(*
Definition split_rmap (m: rmap) : rmap * rmap :=
 (proj1_sig (make_rmap _ (split_rmap_valid1 m) (level m) (split_rmap_ok1 m)),
  proj1_sig (make_rmap _ (split_rmap_valid2 m) (level m) (split_rmap_ok2 m))).
*)

Lemma split_resource_join: 
  forall r, join (fst (split_resource r)) (snd (split_resource r)) r.
Proof.
(* Goal: forall loc : AV.address, @join resource Join_resource (resource_at w1 loc) (resource_at w2 loc) (resource_at w loc) *)
(* Goal: @join ghost ghost_join (ghost_of w1) (ghost_of w2) (ghost_of w) *)
intro.
(* Goal: @join resource Join_resource (@fst resource resource (split_resource r)) (@snd resource resource (split_resource r)) r *)
destruct r; simpl; constructor; auto; try (apply cleave_join; apply surjective_pairing).
Qed.

(*Lemma split_rmap_join:
  forall m, join (fst (split_rmap m)) (snd (split_rmap m)) m.
Proof.
(* Goal: forall (l : AV.address) (_ : not (adr_range a (size_chunk ch) l)), @identity resource Join_resource (resource_at w l) *)
(* Goal: @app_pred rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun i : address => @andp rmap ag_rmap (shareat i sh1) (nonlockat i)) noat)) noghost) (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun loc : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) sh2 loc) noat)) noghost)) w *)
intros.
(* Goal: @eq resource (slice_resource sh2 (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt)))) (YES sh2 rsh2 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt))) *)
unfold split_rmap; simpl.
(* Goal: forall (l : AV.address) (_ : not (adr_range a (size_chunk ch) l)), @identity resource Join_resource (resource_at w l) *)
(* Goal: @app_pred rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun i : address => @andp rmap ag_rmap (shareat i sh1) (nonlockat i)) noat)) noghost) (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun loc : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) sh2 loc) noat)) noghost)) w *)
case_eq (make_rmap _ (split_rmap_valid1 m) (level m) (split_rmap_ok1 m)); intros.
(* Goal: forall (l : AV.address) (_ : not (adr_range a (size_chunk ch) l)), @identity resource Join_resource (resource_at w l) *)
(* Goal: @app_pred rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun i : address => @andp rmap ag_rmap (shareat i sh1) (nonlockat i)) noat)) noghost) (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun loc : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) sh2 loc) noat)) noghost)) w *)
case_eq (make_rmap _ (split_rmap_valid2 m) (level m) (split_rmap_ok2 m)); intros.
simpl in *.
generalize a; intros  [? ?].
generalize a0; intros [? ?].
(* Goal: @eq resource (resource_at f l') (YES sh1 rsh1 k (preds_fmap (approx (@level rmap ag_rmap f)) (approx (@level rmap ag_rmap f)) pp)) *)
(* Goal: @identity resource Join_resource (resource_at f l') *)
apply resource_at_join2; simpl; try congruence.
(* Goal: @identity resource Join_resource (resource_at w l) *)
rewrite H2; rewrite H4; simpl; auto.
(* Goal: forall loc : AV.address, @join resource Join_resource (resource_at w1 loc) (resource_at w2 loc) (resource_at w loc) *)
(* Goal: @join ghost ghost_join (ghost_of w1) (ghost_of w2) (ghost_of w) *)
intro l.
(* Goal: @identity resource Join_resource (resource_at w l) *)
apply split_resource_join; auto.
Qed.

Lemma split_rmap_at1:
  forall m l , fst (split_rmap m) @ l = fst (split_resource (m @ l)).
Proof.
(* Goal: @eq resource (slice_resource sh2 (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt)))) (YES sh2 rsh2 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt))) *)
unfold split_rmap; intros; simpl.
(* Goal: forall (l : AV.address) (_ : not (adr_range a (size_chunk ch) l)), @identity resource Join_resource (resource_at w l) *)
(* Goal: @app_pred rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun i : address => @andp rmap ag_rmap (shareat i sh1) (nonlockat i)) noat)) noghost) (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun loc : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) sh2 loc) noat)) noghost)) w *)
case_eq (make_rmap _ (split_rmap_valid1 m) (level m) (split_rmap_ok1 m)); intros.
simpl in *.
(* Goal: @identity resource Join_resource (resource_at w l) *)
destruct a. rewrite e0; auto.
Qed.

Lemma split_rmap_at2:
  forall m l , snd (split_rmap m) @ l = snd (split_resource (m @ l)).
Proof.
(* Goal: @eq resource (slice_resource sh2 (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt)))) (YES sh2 rsh2 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt))) *)
unfold split_rmap; intros; simpl.
(* Goal: forall (l : AV.address) (_ : not (adr_range a (size_chunk ch) l)), @identity resource Join_resource (resource_at w l) *)
(* Goal: @app_pred rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun i : address => @andp rmap ag_rmap (shareat i sh1) (nonlockat i)) noat)) noghost) (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun loc : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) sh2 loc) noat)) noghost)) w *)
case_eq (make_rmap _ (split_rmap_valid2 m) (level m) (split_rmap_ok2 m)); intros.
(* Goal: @eq resource (slice_resource sh2 (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt)))) (YES sh2 rsh2 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt))) *)
simpl. clear H; destruct a. rewrite H0; auto.
Qed.*)

Definition split_shareval (shv: Share.t * val) : ((Share.t * val) * (Share.t * val)) :=
  ((fst (Share.split (fst shv)), snd shv), (snd (Share.split (fst shv)), snd shv)).

Definition slice_resource (sh: share) (r: resource) : resource :=
  match r with
   | NO _ _ => NO (retainer_part sh) (retainer_part_nonreadable sh)
   | YES _ _ k pp =>
    match readable_share_dec sh with
    | left r1 => YES sh r1 k pp
    | right n => NO sh n
    end
   | PURE k pp => PURE k pp
  end.


Lemma make_slice_rmap: forall w (P: address -> Prop) (P_DEC: forall l, {P l} + {~ P l}) sh,
  (forall l : AV.address, ~ P l -> identity (w @ l)) ->
(* Goal: forall (l : AV.address) (_ : not (P l)), @identity resource Join_resource (resource_at w l) *)
(* Goal: @ex rmap (fun y : rmap => @ex rmap (fun z : rmap => and (@join rmap Join_rmap y z w) (and (and (forall b : address, if P_DEC b then @app_pred rmap ag_rmap (q b) y else @identity resource Join_resource (resource_at y b)) (@identity ghost ghost_join (ghost_of y))) (and (forall b : address, if P_DEC b then @app_pred rmap ag_rmap (r b) z else @identity resource Join_resource (resource_at z b)) (@identity ghost ghost_join (ghost_of z)))))) *)
  {w' | level w' = level w /\ resource_at w' =
       (fun l => if P_DEC l then slice_resource sh (w @ l) else w @ l) /\
       ghost_of w' = ghost_of w}.
Proof.
(* Goal: forall (l : AV.address) (_ : not (adr_range a (size_chunk ch) l)), @identity resource Join_resource (resource_at w l) *)
(* Goal: @app_pred rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun i : address => @andp rmap ag_rmap (shareat i sh1) (nonlockat i)) noat)) noghost) (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun loc : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) sh2 loc) noat)) noghost)) w *)
  intros.
(* Goal: @sig rmap (fun w' : rmap => and (@eq nat (@level rmap ag_rmap w') (@level rmap ag_rmap w)) (and (@eq (forall _ : AV.address, resource) (resource_at w') (fun l : AV.address => if P_DEC l then slice_resource sh (resource_at w l) else resource_at w l)) (@eq ghost (ghost_of w') (ghost_of w)))) *)
  pose (f l := if P_DEC l then slice_resource sh (w @ l) else w @ l).
(* Goal: @sig rmap (fun w' : rmap => and (@eq nat (@level rmap ag_rmap w') (@level rmap ag_rmap w)) (and (@eq (forall _ : AV.address, resource) (resource_at w') (fun l : AV.address => if P_DEC l then slice_resource sh (resource_at w l) else resource_at w l)) (@eq ghost (ghost_of w') (ghost_of w)))) *)
  apply (make_rmap _ (ghost_of w) (level w)).
(* Goal: @eq (forall _ : AV.address, resource) (@compose AV.address resource resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w))) (fun l : AV.address => if P_DEC l then slice_resource sh (resource_at w l) else resource_at w l)) (fun l : AV.address => if P_DEC l then slice_resource sh (resource_at w l) else resource_at w l) *)
(* Goal: @eq ghost (ghost_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (ghost_of w)) (ghost_of w) *)
  extensionality loc; unfold compose, f.
(* Goal: @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (if P_DEC loc then slice_resource sh (resource_at w loc) else resource_at w loc)) (if P_DEC loc then slice_resource sh (resource_at w loc) else resource_at w loc) *)
(* Goal: @eq ghost (ghost_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (ghost_of w)) (ghost_of w) *)
  destruct (P_DEC loc).
  + pose proof resource_at_approx w loc.
(* Goal: @identity resource Join_resource (resource_at w l) *)
    destruct (w @ loc); auto.
(* Goal: @eq resource (slice_resource sh2 (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt)))) (YES sh2 rsh2 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt))) *)
    simpl.
(* Goal: @identity resource Join_resource (resource_at w l) *)
    destruct (readable_share_dec sh); auto.
(* Goal: @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (YES sh r0 k p0)) (YES sh r0 k p0) *)
    inversion H0.
(* Goal: @identity resource Join_resource (resource_at w l) *)
    simpl; f_equal; f_equal; auto.
  + apply resource_at_approx.
  + apply ghost_of_approx.
Qed.

Lemma jam_noat_splittable_aux:
  forall S' S Q (PARAMETRIC: spec_parametric Q)
           (sh1 sh2 sh3: share)
           (rsh1: readable_share sh1) (rsh2: readable_share sh2)
           l
           (H: join sh1 sh2 sh3)
           w (H0: allp (@jam _ _ _ _ _ _ (S' l) (S l) (Q l sh3) noat) w)
           f (Hf: resource_at f = fun loc => slice_resource (if S l loc then sh1 else Share.bot) (w @ loc))
           g (Hg: resource_at g = fun loc => slice_resource (if S l loc then sh2 else Share.bot) (w @ loc))
           (H1: join f g w),
           allp (jam (S l) (Q l sh1) noat) f.
Proof.
(* Goal: forall (l : AV.address) (_ : not (adr_range a (size_chunk ch) l)), @identity resource Join_resource (resource_at w l) *)
(* Goal: @app_pred rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun i : address => @andp rmap ag_rmap (shareat i sh1) (nonlockat i)) noat)) noghost) (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun loc : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) sh2 loc) noat)) noghost)) w *)
intros.
(*assert (rsh3: readable_share sh3) by (eapply readable_share_join ; eauto). *)
(* Goal: @app_pred rmap ag_rmap (@allp rmap ag_rmap AV.address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap AV.address (S' l) (S l) (Q l sh1) noat)) f *)
intro l'.
(* Goal: @app_pred rmap ag_rmap (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap AV.address (S' l) (S l) (Q l sh1) noat l') f *)
specialize ( H0 l').
unfold jam in H0 |- *.
simpl in H0|-*.
(* Goal: if adr_range_dec a (size_chunk ch) b then @app_pred rmap ag_rmap (yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z b) (@snd block Z a))) bl Undef)) sh b) z else @app_pred rmap ag_rmap (noat b) z *)
(* Goal: @app_pred rmap ag_rmap noghost z *)
if_tac.
(* Goal: @app_pred rmap ag_rmap (Q l sh1 l') f *)
(* Goal: @identity resource Join_resource (resource_at f l') *)
destruct (PARAMETRIC l l') as [pp [ok ?]]; clear PARAMETRIC.
rewrite H3 in H0 |- *; clear H3.
(* Goal: @ex (readable_share sh1) (fun p : readable_share sh1 => @ex AV.kind (fun k : AV.kind => and (ok k) (@eq resource (resource_at f l') (YES sh1 p k (preds_fmap (approx (@level rmap ag_rmap f)) (approx (@level rmap ag_rmap f)) pp))))) *)
(* Goal: @identity resource Join_resource (resource_at f l') *)
destruct H0 as [rsh3 [k [? ?]]].
(* Goal: @identity resource Join_resource (resource_at w l) *)
exists rsh1, k; split; auto.
(* Goal: @eq resource (slice_resource sh2 (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt)))) (YES sh2 rsh2 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt))) *)
clear H0.
(* Goal: forall (l : AV.address) (_ : not (adr_range a (size_chunk ch) l)), @identity resource Join_resource (resource_at w l) *)
(* Goal: @app_pred rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun i : address => @andp rmap ag_rmap (shareat i sh1) (nonlockat i)) noat)) noghost) (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun loc : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) sh2 loc) noat)) noghost)) w *)
case_eq (w @ l'); intros.
(* Goal: @eq resource (resource_at f l') (YES sh1 rsh1 k (preds_fmap (approx (@level rmap ag_rmap f)) (approx (@level rmap ag_rmap f)) pp)) *)
(* Goal: @eq resource (resource_at f l') (YES sh1 rsh1 k (preds_fmap (approx (@level rmap ag_rmap f)) (approx (@level rmap ag_rmap f)) pp)) *)
(* Goal: @identity resource Join_resource (resource_at f l') *)
inversion2 H0 H3. 
(* Goal: @eq resource (resource_at f l') (YES sh1 rsh1 k (preds_fmap (approx (@level rmap ag_rmap f)) (approx (@level rmap ag_rmap f)) pp)) *)
(* Goal: @eq resource (resource_at f l') (YES sh1 rsh1 k (preds_fmap (approx (@level rmap ag_rmap f)) (approx (@level rmap ag_rmap f)) pp)) *)
(* Goal: @identity resource Join_resource (resource_at f l') *)
destruct p.
(* Goal: @eq resource (resource_at f l') (YES sh1 rsh1 k (preds_fmap (approx (@level rmap ag_rmap f)) (approx (@level rmap ag_rmap f)) pp)) *)
(* Goal: @eq resource (resource_at f l') (YES sh1 rsh1 k (preds_fmap (approx (@level rmap ag_rmap f)) (approx (@level rmap ag_rmap f)) pp)) *)
(* Goal: @identity resource Join_resource (resource_at f l') *)
inversion2 H0 H3.
(* Goal: forall loc : AV.address, @join resource Join_resource (resource_at w1 loc) (resource_at w2 loc) (resource_at w loc) *)
(* Goal: @join ghost ghost_join (ghost_of w1) (ghost_of w2) (ghost_of w) *)
generalize (resource_at_join _ _ _ l' H1); intro.
(* Goal: forall loc : AV.address, @join resource Join_resource (resource_at w1 loc) (resource_at w2 loc) (resource_at w loc) *)
(* Goal: @join ghost ghost_join (ghost_of w1) (ghost_of w2) (ghost_of w) *)
generalize (f_equal (resource_at f) (refl_equal l')); intro.
(* Goal: @eq resource (resource_at f l') (YES sh1 rsh1 k0 (preds_fmap (approx (@level rmap ag_rmap f)) (approx (@level rmap ag_rmap f)) pp)) *)
(* Goal: @eq resource (resource_at f l') (YES sh1 rsh1 k (preds_fmap (approx (@level rmap ag_rmap f)) (approx (@level rmap ag_rmap f)) pp)) *)
(* Goal: @identity resource Join_resource (resource_at f l') *)
pattern f at 1 in H4; rewrite Hf in H4.
(* Goal: @eq resource (resource_at f l') (YES sh1 rsh1 k0 (preds_fmap (approx (@level rmap ag_rmap f)) (approx (@level rmap ag_rmap f)) pp)) *)
(* Goal: @eq resource (resource_at f l') (YES sh1 rsh1 k (preds_fmap (approx (@level rmap ag_rmap f)) (approx (@level rmap ag_rmap f)) pp)) *)
(* Goal: @identity resource Join_resource (resource_at f l') *)
rewrite H0 in H4.
(* Goal: if adr_range_dec a (size_chunk ch) loc then @ex (readable_share sh2) (fun rsh : readable_share sh2 => @eq resource (resource_at w2 loc) (YES sh2 rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt)))) else @identity resource Join_resource (resource_at w2 loc) *)
(* Goal: @app_pred rmap ag_rmap noghost w2 *)
rewrite H4.
rewrite if_true in H4|-* by auto.
(* Goal: @eq resource (slice_resource sh2 (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt)))) (YES sh2 rsh2 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt))) *)
simpl.
(* Goal: @eq resource match readable_share_dec sh1 with | left r1 => YES sh1 r1 k0 (SomeP A _f) | right n => NO sh1 n end (YES sh1 rsh1 k0 (preds_fmap (approx (@level rmap ag_rmap f)) (approx (@level rmap ag_rmap f)) pp)) *)
(* Goal: @eq resource (resource_at f l') (YES sh1 rsh1 k (preds_fmap (approx (@level rmap ag_rmap f)) (approx (@level rmap ag_rmap f)) pp)) *)
(* Goal: @identity resource Join_resource (resource_at f l') *)
destruct (readable_share_dec sh1); [ | contradiction].
(* Goal: @eq resource (YES sh1 r0 k0 (SomeP A _f)) (YES sh1 rsh1 k0 (preds_fmap (approx (@level rmap ag_rmap f)) (approx (@level rmap ag_rmap f)) pp)) *)
(* Goal: @eq resource (resource_at f l') (YES sh1 rsh1 k (preds_fmap (approx (@level rmap ag_rmap f)) (approx (@level rmap ag_rmap f)) pp)) *)
(* Goal: @identity resource Join_resource (resource_at f l') *)
replace (level f) with (level w). 
(* Goal: @eq resource (YES sh1 r0 k0 (SomeP A _f)) (YES sh1 rsh1 k0 (preds_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) pp)) *)
(* Goal: @eq nat (@level rmap ag_rmap w) (@level rmap ag_rmap f) *)
(* Goal: @eq resource (resource_at f l') (YES sh1 rsh1 k (preds_fmap (approx (@level rmap ag_rmap f)) (approx (@level rmap ag_rmap f)) pp)) *)
(* Goal: @identity resource Join_resource (resource_at f l') *)
rewrite H7.
(* Goal: @eq resource (YES sh rsh3 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z b) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt))) (YES sh p8 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z b) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt))) *)
f_equal. apply proof_irr.
(* Goal: @eq nat (@level rmap ag_rmap w) (@level rmap ag_rmap f) *)
(* Goal: @eq resource (resource_at f l') (YES sh1 rsh1 k (preds_fmap (approx (@level rmap ag_rmap f)) (approx (@level rmap ag_rmap f)) pp)) *)
(* Goal: @identity resource Join_resource (resource_at f l') *)
apply join_level in H1; intuition.
(* Goal: @eq resource (resource_at f l') (YES sh1 rsh1 k (preds_fmap (approx (@level rmap ag_rmap f)) (approx (@level rmap ag_rmap f)) pp)) *)
(* Goal: @identity resource Join_resource (resource_at f l') *)
congruence.
(* noat case *)
(* Goal: forall loc : AV.address, @join resource Join_resource (resource_at w1 loc) (resource_at w2 loc) (resource_at w loc) *)
(* Goal: @join ghost ghost_join (ghost_of w1) (ghost_of w2) (ghost_of w) *)
generalize (resource_at_join _ _ _ l' H1); intro.
(* Goal: @identity resource Join_resource (resource_at w l) *)
apply split_identity in H3; auto.
Qed.

Lemma slice_resource_identity:
  forall r, identity r -> slice_resource Share.bot r = r.
Proof.
(* Goal: forall (l : AV.address) (_ : not (adr_range a (size_chunk ch) l)), @identity resource Join_resource (resource_at w l) *)
(* Goal: @app_pred rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun i : address => @andp rmap ag_rmap (shareat i sh1) (nonlockat i)) noat)) noghost) (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun loc : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) sh2 loc) noat)) noghost)) w *)
 intros.
 destruct r; simpl in *; auto.
(* Goal: @eq resource (NO (retainer_part Share.bot) (retainer_part_nonreadable Share.bot)) (NO sh n) *)
(* Goal: @eq resource match readable_share_dec Share.bot with | left r1 => YES Share.bot r1 k p | right n => NO Share.bot n end (YES sh r k p) *)
 assert (sh = retainer_part Share.bot).
(* Goal: @eq Share.t (retainer_part sh) sh *)
   unfold retainer_part. rewrite Share.glb_bot.
(* Goal: @eq Share.t sh Share.bot *)
(* Goal: @eq resource (NO (retainer_part Share.bot) (retainer_part_nonreadable Share.bot)) (NO sh n) *)
(* Goal: @eq resource match readable_share_dec Share.bot with | left r1 => YES Share.bot r1 k p | right n => NO Share.bot n end (YES sh r k p) *)
   apply identity_NO in H.
(* Goal: @identity resource Join_resource (resource_at w l) *)
   destruct H as [|]. inv H. auto. destruct H as [? [? ?]]. inv H.
(* Goal: @eq resource (YES sh rsh3 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z b) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt))) (YES sh p8 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z b) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt))) *)
   subst; f_equal. apply proof_irr.
(* Goal: @eq resource match readable_share_dec Share.bot with | left r1 => YES Share.bot r1 k p | right n => NO Share.bot n end (YES sh r k p) *)
   apply YES_not_identity in H. contradiction.
Qed.

(* Goal: forall (l : AV.address) (_ : not (P l)), @identity resource Join_resource (resource_at w l) *)
(* Goal: @ex rmap (fun y : rmap => @ex rmap (fun z : rmap => and (@join rmap Join_rmap y z w) (and (and (forall b : address, if P_DEC b then @app_pred rmap ag_rmap (q b) y else @identity resource Join_resource (resource_at y b)) (@identity ghost ghost_join (ghost_of y))) (and (forall b : address, if P_DEC b then @app_pred rmap ag_rmap (r b) z else @identity resource Join_resource (resource_at z b)) (@identity ghost ghost_join (ghost_of z)))))) *)
Definition splittable {A} {JA: Join A}{PA: Perm_alg A}{agA: ageable A}{AgeA: Age_alg A} (Q: Share.t -> pred A) := 
  forall (sh1 sh2 sh3: Share.t) (rsh1: readable_share sh1) (rsh2: readable_share sh2),
    join sh1 sh2 sh3 ->
    Q sh1 * Q sh2 = Q sh3.

(*Lemma jam_noat_splittable:
  forall (S': address -> address -> Prop) S
           (Q: address -> spec)
     (PARAMETRIC: spec_parametric Q),
    forall l, splittable (fun sh => allp (@jam _ _ _ _ _ _ (S' l) (S l) (Q l sh) noat)).
Proof.
(* Goal: forall (l : AV.address) (_ : not (adr_range a (size_chunk ch) l)), @identity resource Join_resource (resource_at w l) *)
(* Goal: @app_pred rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun i : address => @andp rmap ag_rmap (shareat i sh1) (nonlockat i)) noat)) noghost) (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun loc : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) sh2 loc) noat)) noghost)) w *)
unfold splittable; intros.
(* Goal: @eq resource (slice_resource sh2 (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt)))) (YES sh2 rsh2 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt))) *)
apply pred_ext; intro w; simpl.
+  intros [w1 [w2 [? [? ?]]]].
(* Goal: @app_pred rmap ag_rmap (@allp rmap ag_rmap AV.address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap AV.address (S' l) (S l) (Q l sh1) noat)) f *)
  intro l'. specialize ( H1 l'); specialize ( H2 l').
  unfold jam in *.
  revert H1 H2.
(* Goal: if adr_range_dec a (size_chunk ch) b then @app_pred rmap ag_rmap (yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z b) (@snd block Z a))) bl Undef)) sh b) z else @app_pred rmap ag_rmap (noat b) z *)
(* Goal: @app_pred rmap ag_rmap noghost z *)
  if_tac.
(* Goal: forall (l : AV.address) (_ : not (adr_range a (size_chunk ch) l)), @identity resource Join_resource (resource_at w l) *)
(* Goal: @app_pred rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun i : address => @andp rmap ag_rmap (shareat i sh1) (nonlockat i)) noat)) noghost) (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun loc : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) sh2 loc) noat)) noghost)) w *)
  - intros.
    specialize (PARAMETRIC l l').
    destruct PARAMETRIC as [pp [ok ?]].
    rewrite H4 in H2. destruct H2 as [rsh1' [k1 [G1 H1']]]. 
    rewrite H4 in H3; destruct H3 as [rsh2' [k2 [G2 H2']]]. 
(* Goal: if adr_range_dec a (size_chunk ch) loc then @ex (readable_share sh2) (fun rsh : readable_share sh2 => @eq resource (resource_at w2 loc) (YES sh2 rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt)))) else @identity resource Join_resource (resource_at w2 loc) *)
(* Goal: @app_pred rmap ag_rmap noghost w2 *)
    rewrite H4.
    assert (rsh3 := join_readable1 H rsh1).
    exists rsh3.
    exists k2.
    generalize (resource_at_join _ _ _ l' H0); rewrite H1'; rewrite H2'; intro Hx.
(* Goal: @identity share Share.Join_ba (Share.glb Share.Rsh (Share.lub (@snd Share.t Share.t (Share.split (Share.glb Share.Lsh sh))) (@snd Share.t Share.t (Share.split Share.bot)))) *)
    generalize H; clear H.
    inv Hx. 
(* Goal: @identity resource Join_resource (resource_at w l) *)
    split; auto.
(* Goal: @eq resource (slice_resource sh2 (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt)))) (YES sh2 rsh2 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt))) *)
    simpl.
    replace (level w1) with (level w) by (apply join_level in H0; intuition).
    pose proof (join_eq H RJ). subst sh5.
    f_equal; auto with extensionality.
(* Goal: forall (l : AV.address) (_ : not (adr_range a (size_chunk ch) l)), @identity resource Join_resource (resource_at w l) *)
(* Goal: @app_pred rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun i : address => @andp rmap ag_rmap (shareat i sh1) (nonlockat i)) noat)) noghost) (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun loc : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) sh2 loc) noat)) noghost)) w *)
  - intros.
(* Goal: forall loc : AV.address, @join resource Join_resource (resource_at w1 loc) (resource_at w2 loc) (resource_at w loc) *)
(* Goal: @join ghost ghost_join (ghost_of w1) (ghost_of w2) (ghost_of w) *)
    generalize (resource_at_join _ _ _ l' H0); intro.
(* Goal: @identity resource Join_resource (resource_at w l) *)
    apply H2 in H4. rewrite H4 in H3; auto.
(* Goal: forall (l : AV.address) (_ : not (adr_range a (size_chunk ch) l)), @identity resource Join_resource (resource_at w l) *)
(* Goal: @app_pred rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun i : address => @andp rmap ag_rmap (shareat i sh1) (nonlockat i)) noat)) noghost) (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun loc : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) sh2 loc) noat)) noghost)) w *)
+ intros.
  pose (f loc := if S l loc then slice_resource sh1 (w @ loc) else w@loc).
(* Goal: forall (l : AV.address) (_ : not (P l)), @identity resource Join_resource (resource_at w l) *)
(* Goal: @ex rmap (fun y : rmap => @ex rmap (fun z : rmap => and (@join rmap Join_rmap y z w) (and (and (forall b : address, if P_DEC b then @app_pred rmap ag_rmap (q b) y else @identity resource Join_resource (resource_at y b)) (@identity ghost ghost_join (ghost_of y))) (and (forall b : address, if P_DEC b then @app_pred rmap ag_rmap (r b) z else @identity resource Join_resource (resource_at z b)) (@identity ghost ghost_join (ghost_of z)))))) *)
  assert (Vf: CompCert_AV.valid (res_option oo f)). {
     apply slice_resource_valid.
(* Goal: forall (l : AV.address) (_ : not (adr_range a (size_chunk ch) l)), @identity resource Join_resource (resource_at w l) *)
(* Goal: @app_pred rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun i : address => @andp rmap ag_rmap (shareat i sh1) (nonlockat i)) noat)) noghost) (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun loc : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) sh2 loc) noat)) noghost)) w *)
     intros. specialize (H0 l0). rewrite if_false in H0; auto.
  }
  destruct (make_rmap _ Vf (level w)) as [phi [Gf Hf]].
(* Goal: forall (l : AV.address) (_ : not (P l)), @identity resource Join_resource (resource_at w l) *)
(* Goal: @ex rmap (fun y : rmap => @ex rmap (fun z : rmap => and (@join rmap Join_rmap y z w) (and (and (forall b : address, if P_DEC b then @app_pred rmap ag_rmap (q b) y else @identity resource Join_resource (resource_at y b)) (@identity ghost ghost_join (ghost_of y))) (and (forall b : address, if P_DEC b then @app_pred rmap ag_rmap (r b) z else @identity resource Join_resource (resource_at z b)) (@identity ghost ghost_join (ghost_of z)))))) *)
  {
(* Goal: @eq (forall _ : AV.address, resource) (@compose AV.address resource resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w))) (fun l : AV.address => if P_DEC l then slice_resource sh (resource_at w l) else resource_at w l)) (fun l : AV.address => if P_DEC l then slice_resource sh (resource_at w l) else resource_at w l) *)
(* Goal: @eq ghost (ghost_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (ghost_of w)) (ghost_of w) *)
    extensionality loc; unfold compose, f.
    specialize (PARAMETRIC l loc).
    destruct PARAMETRIC as [pp [ok Jf]].
    specialize ( H0 loc).
    destruct (S l loc).
    rewrite Jf in H0.
    destruct H0 as [p3 [k3 [G0 H0]]].
(* Goal: forall loc : AV.address, @join resource Join_resource (resource_at w1 loc) (resource_at w2 loc) (resource_at w loc) *)
(* Goal: @join ghost ghost_join (ghost_of w1) (ghost_of w2) (ghost_of w) *)
    generalize (resource_at_approx w loc); intro.
    rewrite H0 in H1.
(* Goal: @identity resource Join_resource (resource_at w l) *)
    inversion H1; clear H1; auto.
(* Goal: @eq resource (slice_resource sh2 (resource_at w loc)) (YES sh2 rsh2 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt))) *)
    rewrite H0.
(* Goal: @eq resource (slice_resource sh2 (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt)))) (YES sh2 rsh2 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt))) *)
    simpl.
(* Goal: @identity resource Join_resource (resource_at w l) *)
    destruct (readable_share_dec sh1); auto.
(* Goal: @identity resource Join_resource (resource_at w l) *)
    revert H0; case_eq (w @ loc); intros; try contradiction; simpl; f_equal; auto.
(* Goal: @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (resource_at w loc)) (resource_at w loc) *)
    apply resource_at_approx.
  }
  pose (g loc := if S l loc then slice_resource sh2 (w @ loc) else w@loc).
(* Goal: forall (l : AV.address) (_ : not (P l)), @identity resource Join_resource (resource_at w l) *)
(* Goal: @ex rmap (fun y : rmap => @ex rmap (fun z : rmap => and (@join rmap Join_rmap y z w) (and (and (forall b : address, if P_DEC b then @app_pred rmap ag_rmap (q b) y else @identity resource Join_resource (resource_at y b)) (@identity ghost ghost_join (ghost_of y))) (and (forall b : address, if P_DEC b then @app_pred rmap ag_rmap (r b) z else @identity resource Join_resource (resource_at z b)) (@identity ghost ghost_join (ghost_of z)))))) *)
  assert (Vg: CompCert_AV.valid (res_option oo g)). {
     apply slice_resource_valid.
(* Goal: forall (l : AV.address) (_ : not (adr_range a (size_chunk ch) l)), @identity resource Join_resource (resource_at w l) *)
(* Goal: @app_pred rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun i : address => @andp rmap ag_rmap (shareat i sh1) (nonlockat i)) noat)) noghost) (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun loc : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) sh2 loc) noat)) noghost)) w *)
     intros. specialize (H0 l0). rewrite if_false in H0; auto.
  }
  destruct (make_rmap _ Vg (level w)) as [phi' [Gg Hg]].
(* Goal: forall (l : AV.address) (_ : not (P l)), @identity resource Join_resource (resource_at w l) *)
(* Goal: @ex rmap (fun y : rmap => @ex rmap (fun z : rmap => and (@join rmap Join_rmap y z w) (and (and (forall b : address, if P_DEC b then @app_pred rmap ag_rmap (q b) y else @identity resource Join_resource (resource_at y b)) (@identity ghost ghost_join (ghost_of y))) (and (forall b : address, if P_DEC b then @app_pred rmap ag_rmap (r b) z else @identity resource Join_resource (resource_at z b)) (@identity ghost ghost_join (ghost_of z)))))) *)
  {
    extensionality loc; unfold compose, g.
    specialize (PARAMETRIC l loc).
    destruct PARAMETRIC as [pp [ok Jg]].
    specialize ( H0 loc).
    destruct (S l loc).
    rewrite Jg in H0.
    destruct H0 as [p3 [k3 [G0 H0]]].
(* Goal: forall loc : AV.address, @join resource Join_resource (resource_at w1 loc) (resource_at w2 loc) (resource_at w loc) *)
(* Goal: @join ghost ghost_join (ghost_of w1) (ghost_of w2) (ghost_of w) *)
    generalize (resource_at_approx w loc); intro.
    rewrite H0 in H1.
(* Goal: @identity resource Join_resource (resource_at w l) *)
    inversion H1; clear H1; auto.
(* Goal: @eq resource (slice_resource sh2 (resource_at w loc)) (YES sh2 rsh2 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt))) *)
    rewrite H0.
(* Goal: @eq resource (slice_resource sh2 (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt)))) (YES sh2 rsh2 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt))) *)
    simpl.
(* Goal: @identity resource Join_resource (resource_at w l) *)
    destruct (readable_share_dec sh2); auto.
(* Goal: @identity resource Join_resource (resource_at w l) *)
    revert H0; case_eq (w @ loc); intros; try contradiction; simpl; f_equal; auto.
(* Goal: @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (resource_at w loc)) (resource_at w loc) *)
    apply resource_at_approx.
  }
  unfold f,g in *; clear f g.
  rename phi into f; rename phi' into g.
(* Goal: forall (l : AV.address) (_ : not (P l)), @identity resource Join_resource (resource_at w l) *)
(* Goal: @ex rmap (fun y : rmap => @ex rmap (fun z : rmap => and (@join rmap Join_rmap y z w) (and (and (forall b : address, if P_DEC b then @app_pred rmap ag_rmap (q b) y else @identity resource Join_resource (resource_at y b)) (@identity ghost ghost_join (ghost_of y))) (and (forall b : address, if P_DEC b then @app_pred rmap ag_rmap (r b) z else @identity resource Join_resource (resource_at z b)) (@identity ghost ghost_join (ghost_of z)))))) *)
  assert (join f g w). {
(* Goal: @identity resource Join_resource (resource_at w l) *)
   apply resource_at_join2; auto.
(* Goal: forall loc : AV.address, @join resource Join_resource (resource_at w1 loc) (resource_at w2 loc) (resource_at w loc) *)
(* Goal: @join ghost ghost_join (ghost_of w1) (ghost_of w2) (ghost_of w) *)
   intro.
   rewrite Hf; rewrite Hg.
   clear - PARAMETRIC H H0 rsh1 rsh2.
   specialize ( H0 loc).
(* Goal: if adr_range_dec a (size_chunk ch) loc then @ex (readable_share sh2) (fun rsh : readable_share sh2 => @eq resource (if adr_range_dec a (size_chunk ch) loc then slice_resource sh2 (resource_at w loc) else resource_at w loc) (YES sh2 rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt)))) else @identity resource Join_resource (if adr_range_dec a (size_chunk ch) loc then slice_resource sh2 (resource_at w loc) else resource_at w loc) *)
(* Goal: @app_pred rmap ag_rmap noghost w2 *)
   if_tac in H0.
   destruct (PARAMETRIC l loc) as [pp [ok ?]]; clear PARAMETRIC.
   rewrite H2 in H0.
   destruct H0 as [? [? [? ?]]].
   rewrite H3.
(* Goal: forall loc : AV.address, @join resource Join_resource (resource_at w1 loc) (resource_at w2 loc) (resource_at w loc) *)
(* Goal: @join ghost ghost_join (ghost_of w1) (ghost_of w2) (ghost_of w) *)
   generalize (preds_fmap (approx (level w)) (approx (level w)) pp); intro.
(* Goal: @eq resource (slice_resource sh2 (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt)))) (YES sh2 rsh2 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt))) *)
   simpl.
(* Goal: @eq resource match readable_share_dec sh1 with | left r1 => YES sh1 r1 k0 (SomeP A _f) | right n => NO sh1 n end (YES sh1 rsh1 k0 (preds_fmap (approx (@level rmap ag_rmap f)) (approx (@level rmap ag_rmap f)) pp)) *)
(* Goal: @eq resource (resource_at f l') (YES sh1 rsh1 k (preds_fmap (approx (@level rmap ag_rmap f)) (approx (@level rmap ag_rmap f)) pp)) *)
(* Goal: @identity resource Join_resource (resource_at f l') *)
   destruct (readable_share_dec sh1); [ | contradiction].
(* Goal: @eq resource match readable_share_dec sh2 with | left r1 => YES sh2 r1 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt)) | right n => NO sh2 n end (YES sh2 rsh2 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt))) *)
   destruct (readable_share_dec sh2); [ | contradiction].
(* Goal: @identity resource Join_resource (resource_at w l) *)
   constructor; auto.
(* Goal: @join resource Join_resource (resource_at w loc) (resource_at w loc) (resource_at w loc) *)
(* Goal: @join ghost ghost_join (ghost_of w1) (ghost_of w2) (ghost_of w) *)
   apply identity_unit' in H0. apply H0.
  }
  econstructor; econstructor; split; [apply H1|].
(* Goal: @app_pred rmap ag_rmap (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun loc : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) sh2 loc) noat)) noghost) w2 *)
  split.
(* Goal: @identity resource Join_resource (resource_at w l) *)
  eapply jam_noat_splittable_aux; eauto.
(* Goal: @identity resource Join_resource (resource_at w l) *)
  simpl; auto.
(* Goal: @identity resource Join_resource (resource_at w l) *)
  rewrite Hf. extensionality loc. if_tac. auto.
(* Goal: @identity resource Join_resource (resource_at w l) *)
  clear - H0 H2. specialize (H0 loc). rewrite if_false in H0 by auto.
(* Goal: @identity resource Join_resource (resource_at w l) *)
  symmetry; apply slice_resource_identity; auto.
(* Goal: @identity resource Join_resource (resource_at w l) *)
  rewrite Hg. extensionality loc. if_tac. auto.
(* Goal: @identity resource Join_resource (resource_at w l) *)
  clear - H0 H2. specialize (H0 loc). rewrite if_false in H0 by auto.
(* Goal: @identity resource Join_resource (resource_at w l) *)
  symmetry; apply slice_resource_identity; auto.
(* Goal: @identity share Share.Join_ba (Share.glb Share.Rsh (Share.lub (@snd Share.t Share.t (Share.split (Share.glb Share.Lsh sh))) b)) *)
  apply join_comm in H.
  eapply jam_noat_splittable_aux.
(* Goal: @identity resource Join_resource (resource_at w l) *)
  auto. auto. apply rsh1. eauto. 4: apply (join_comm H1).
(* Goal: @identity resource Join_resource (resource_at w l) *)
  simpl; auto.
(* Goal: @identity resource Join_resource (resource_at w l) *)
  rewrite Hg. extensionality loc. if_tac. auto.
(* Goal: @identity resource Join_resource (resource_at w l) *)
  clear - H0 H2. specialize (H0 loc). rewrite if_false in H0 by auto.
(* Goal: @identity resource Join_resource (resource_at w l) *)
  symmetry; apply slice_resource_identity; auto.
(* Goal: @identity resource Join_resource (resource_at w l) *)
  rewrite Hf. extensionality loc. if_tac. auto.
(* Goal: @identity resource Join_resource (resource_at w l) *)
  clear - H0 H2. specialize (H0 loc). rewrite if_false in H0 by auto.
(* Goal: @identity resource Join_resource (resource_at w l) *)
  symmetry; apply slice_resource_identity; auto.
Qed.*)

(*Lemma address_mapsto_splittable:
      forall ch v l, splittable (fun sh => address_mapsto ch v sh l).
Proof.
(* Goal: forall (l : AV.address) (_ : not (adr_range a (size_chunk ch) l)), @identity resource Join_resource (resource_at w l) *)
(* Goal: @app_pred rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun i : address => @andp rmap ag_rmap (shareat i sh1) (nonlockat i)) noat)) noghost) (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun loc : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) sh2 loc) noat)) noghost)) w *)
intros.
unfold splittable.
intros ? ? ? rsh1 rsh2 H.
apply pred_ext; intros ? ?.
*
destruct H0 as [m1 [m2 [? [? ?]]]].
unfold address_mapsto in *.
destruct H1 as [bl1 [[[LEN1 DECODE1] ?] Hg1]]; destruct H2 as [bl2 [[[LEN2 DECODE2] ?] Hg2]].
(* Goal: @identity resource Join_resource (resource_at w l) *)
exists bl1; split; [split|]; auto.
(* Goal: @identity resource Join_resource (resource_at w l) *)
simpl; auto.
intro loc; specialize ( H1 loc); specialize ( H2 loc).
unfold jam in *.
apply (resource_at_join _ _ _ loc) in H0.
hnf in H1, H2|-*.
(* Goal: if adr_range_dec a (size_chunk ch) b then @app_pred rmap ag_rmap (yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z b) (@snd block Z a))) bl Undef)) sh b) z else @app_pred rmap ag_rmap (noat b) z *)
(* Goal: @app_pred rmap ag_rmap noghost z *)
if_tac.
hnf in H1,H2.
destruct H1; destruct H2.
(* Goal: @app_pred rmap ag_rmap (yesat_raw NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z b) (@snd block Z a))) bl Undef)) sh p8 b) z *)
hnf.
exists (join_readable1 H rsh1).
unfold yesat_raw in *.
hnf in H1,H2|-*.
rewrite preds_fmap_NoneP in *.
repeat proof_irr.
rewrite H1 in H0; rewrite H2 in H0; clear H1 H2.
unfold yesat_raw.
(* Goal: @join resource Join_resource match readable_share_dec sh1 with | left r1 => YES sh1 r1 k p | right n => NO sh1 n end match readable_share_dec sh2 with | left r1 => YES sh2 r1 k p | right n => NO sh2 n end (YES sh0 r k p) *)
inv H0.
pose proof (join_eq H RJ); subst sh5; clear RJ rsh5 rsh6.
(* Goal: @eq resource (YES sh rsh3 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z b) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt))) (YES sh p8 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z b) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt))) *)
f_equal.
(* Goal: @eq (readable_share sh) rsh3 p8 *)
apply proof_irr.
apply H1 in H0. do 3 red in H2|-*. rewrite <- H0; auto.
(* Goal: @identity resource Join_resource (resource_at w l) *)
simpl; rewrite <- (Hg1 _ _ (ghost_of_join _ _ _ H0)); auto.
*
rename a into m.
hnf in H0|-*.
destruct H0 as [bl [[[? [? Halign]] ?] Hg]].
pose (rslice (rsh : Share.t) (loc: address) := if adr_range_dec l (size_chunk ch) loc then rsh else Share.bot).
assert (G1: forall l0 : AV.address,
(* Goal: forall (l : AV.address) (_ : not (P l)), @identity resource Join_resource (resource_at w l) *)
(* Goal: @ex rmap (fun y : rmap => @ex rmap (fun z : rmap => and (@join rmap Join_rmap y z w) (and (and (forall b : address, if P_DEC b then @app_pred rmap ag_rmap (q b) y else @identity resource Join_resource (resource_at y b)) (@identity ghost ghost_join (ghost_of y))) (and (forall b : address, if P_DEC b then @app_pred rmap ag_rmap (r b) z else @identity resource Join_resource (resource_at z b)) (@identity ghost ghost_join (ghost_of z)))))) *)
  ~ adr_range l (size_chunk ch) l0 -> identity (m @ l0)). {
(* Goal: forall (l : AV.address) (_ : not (adr_range a (size_chunk ch) l)), @identity resource Join_resource (resource_at w l) *)
(* Goal: @app_pred rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun i : address => @andp rmap ag_rmap (shareat i sh1) (nonlockat i)) noat)) noghost) (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun loc : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) sh2 loc) noat)) noghost)) w *)
   intros. specialize (H2 l0). rewrite  jam_false in H2 by auto.
   apply H2.
 }
destruct (make_slice_rmap m _ (adr_range_dec l (size_chunk ch)) sh1 G1)
  as [m1 [? ?]].
destruct (make_slice_rmap m _ (adr_range_dec l (size_chunk ch)) sh2 G1)
  as [m2 [? ?]].
exists m1, m2.
(* Goal: and (@join rmap Join_rmap w1 w2 w) (and (@app_pred rmap ag_rmap (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun i : address => @andp rmap ag_rmap (shareat i sh1) (nonlockat i)) noat)) noghost) w1) (@app_pred rmap ag_rmap (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun loc : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) sh2 loc) noat)) noghost) w2)) *)
split3.
+
(* Goal: @eq resource (resource_at f l') (YES sh1 rsh1 k (preds_fmap (approx (@level rmap ag_rmap f)) (approx (@level rmap ag_rmap f)) pp)) *)
(* Goal: @identity resource Join_resource (resource_at f l') *)
apply resource_at_join2; try congruence.
intro loc.
rewrite H4,H6. clear H4 H6. clear H3 H5. clear m1 m2.
specialize (G1 loc). clear rslice.
(* Goal: @app_pred rmap ag_rmap (yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z b) (@snd block Z a))) bl Undef)) sh b) z *)
specialize (H2 loc). hnf in H2.
(* Goal: if adr_range_dec a (size_chunk ch) b then @app_pred rmap ag_rmap (yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z b) (@snd block Z a))) bl Undef)) sh b) z else @app_pred rmap ag_rmap (noat b) z *)
(* Goal: @app_pred rmap ag_rmap noghost z *)
if_tac.
destruct H2 as [rsh ?].
(* Goal: if adr_range_dec a (size_chunk ch) loc then and (@eq (option share) (resource_share (resource_at w1 loc)) (@Some share sh1)) (nonlock (resource_at w1 loc)) else @identity resource Join_resource (resource_at w1 loc) *)
(* Goal: @app_pred rmap ag_rmap noghost w1 *)
hnf in H2. rewrite H2. clear H2.
(* Goal: and (@eq (option share) (resource_share (slice_resource sh1 (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (preds_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) NoneP)))) (@Some share sh1)) (nonlock (slice_resource sh1 (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (preds_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) NoneP)))) *)
unfold slice_resource.
(* Goal: @eq resource match readable_share_dec sh1 with | left r1 => YES sh1 r1 k0 (SomeP A _f) | right n => NO sh1 n end (YES sh1 rsh1 k0 (preds_fmap (approx (@level rmap ag_rmap f)) (approx (@level rmap ag_rmap f)) pp)) *)
(* Goal: @eq resource (resource_at f l') (YES sh1 rsh1 k (preds_fmap (approx (@level rmap ag_rmap f)) (approx (@level rmap ag_rmap f)) pp)) *)
(* Goal: @identity resource Join_resource (resource_at f l') *)
destruct (readable_share_dec sh1); [ | contradiction].
(* Goal: @eq resource match readable_share_dec sh2 with | left r1 => YES sh2 r1 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt)) | right n => NO sh2 n end (YES sh2 rsh2 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt))) *)
destruct (readable_share_dec sh2); [ | contradiction].
(* Goal: @identity resource Join_resource (resource_at w l) *)
constructor. auto.
(* Goal: @identity resource Join_resource (resource_at w l) *)
do 3 red in H2. apply identity_unit' in H2. apply H2; auto.
+
(* Goal: @identity resource Join_resource (resource_at w l) *)
exists bl; repeat split; auto.
intro loc; specialize ( H2 loc); unfold jam in *;  hnf in H2|-*; if_tac; auto.
exists rsh1.
(* Goal: @app_pred rmap ag_rmap (yesat_raw NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z b) (@snd block Z a))) bl Undef)) sh p8 b) z *)
hnf.
(* Goal: if adr_range_dec a (size_chunk ch) loc then @ex (readable_share sh2) (fun rsh : readable_share sh2 => @eq resource (resource_at w2 loc) (YES sh2 rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt)))) else @identity resource Join_resource (resource_at w2 loc) *)
(* Goal: @app_pred rmap ag_rmap noghost w2 *)
rewrite H4.
(* Goal: @identity resource Join_resource (resource_at w l) *)
rewrite if_true by auto.
(* Goal: and (@eq (option share) (resource_share (slice_resource sh1 (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (preds_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) NoneP)))) (@Some share sh1)) (nonlock (slice_resource sh1 (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (preds_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) NoneP)))) *)
unfold slice_resource.
(* Goal: @app_pred rmap ag_rmap (yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z b) (@snd block Z a))) bl Undef)) sh b) z *)
destruct H2. hnf in H2.
(* Goal: if adr_range_dec a (size_chunk ch) loc then and (@eq (option share) (resource_share (resource_at w1 loc)) (@Some share sh1)) (nonlock (resource_at w1 loc)) else @identity resource Join_resource (resource_at w1 loc) *)
(* Goal: @app_pred rmap ag_rmap noghost w1 *)
rewrite H2.
(* Goal: @eq resource match readable_share_dec sh1 with | left r1 => YES sh1 r1 k0 (SomeP A _f) | right n => NO sh1 n end (YES sh1 rsh1 k0 (preds_fmap (approx (@level rmap ag_rmap f)) (approx (@level rmap ag_rmap f)) pp)) *)
(* Goal: @eq resource (resource_at f l') (YES sh1 rsh1 k (preds_fmap (approx (@level rmap ag_rmap f)) (approx (@level rmap ag_rmap f)) pp)) *)
(* Goal: @identity resource Join_resource (resource_at f l') *)
destruct (readable_share_dec sh1); [ | contradiction].
(* Goal: @eq resource (YES sh rsh3 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z b) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt))) (YES sh p8 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z b) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt))) *)
f_equal. apply proof_irr.
do 3 red in H2|-*.
(* Goal: @identity resource Join_resource (resource_at w l) *)
rewrite H4. rewrite if_false by auto. auto.
+
(* Goal: @identity resource Join_resource (resource_at w l) *)
exists bl; repeat split; auto.
intro loc; specialize ( H2 loc); unfold jam in *;  hnf in H2|-*; if_tac; auto.
(* Goal: @ex (readable_share sh2) (fun rsh : readable_share sh2 => @eq resource (slice_resource sh2 (resource_at w loc)) (YES sh2 rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt)))) *)
exists rsh2.
(* Goal: @app_pred rmap ag_rmap (yesat_raw NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z b) (@snd block Z a))) bl Undef)) sh p8 b) z *)
hnf.
rewrite H6.
(* Goal: @identity resource Join_resource (resource_at w l) *)
rewrite if_true by auto.
(* Goal: and (@eq (option share) (resource_share (slice_resource sh1 (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (preds_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) NoneP)))) (@Some share sh1)) (nonlock (slice_resource sh1 (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (preds_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) NoneP)))) *)
unfold slice_resource.
(* Goal: @app_pred rmap ag_rmap (yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z b) (@snd block Z a))) bl Undef)) sh b) z *)
destruct H2. hnf in H2.
(* Goal: if adr_range_dec a (size_chunk ch) loc then and (@eq (option share) (resource_share (resource_at w1 loc)) (@Some share sh1)) (nonlock (resource_at w1 loc)) else @identity resource Join_resource (resource_at w1 loc) *)
(* Goal: @app_pred rmap ag_rmap noghost w1 *)
rewrite H2.
(* Goal: @eq resource match readable_share_dec sh2 with | left r1 => YES sh2 r1 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt)) | right n => NO sh2 n end (YES sh2 rsh2 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt))) *)
destruct (readable_share_dec sh2); [ | contradiction].
(* Goal: @eq resource (YES sh rsh3 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z b) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt))) (YES sh p8 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z b) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt))) *)
f_equal. apply proof_irr.
do 3 red in H2|-*.
(* Goal: @identity resource Join_resource (resource_at w l) *)
rewrite H6. rewrite if_false by auto. auto.
Qed.

Lemma VALspec_splittable: forall l, splittable (fun sh => VALspec sh l).
Proof.
apply jam_noat_splittable.
apply VALspec_parametric.
Qed.

Lemma LKspec_splittable size: forall R l, splittable (fun sh => LKspec size R sh l).
Proof.
(* Goal: forall loc : AV.address, @join resource Join_resource (resource_at w1 loc) (resource_at w2 loc) (resource_at w loc) *)
(* Goal: @join ghost ghost_join (ghost_of w1) (ghost_of w2) (ghost_of w) *)
intro.
apply jam_noat_splittable.
apply LKspec_parametric.
Qed.

Lemma VALspec_range_splittable: forall n l, splittable (fun sh => VALspec_range n sh l).
Proof.
(* Goal: forall loc : AV.address, @join resource Join_resource (resource_at w1 loc) (resource_at w2 loc) (resource_at w loc) *)
(* Goal: @join ghost ghost_join (ghost_of w1) (ghost_of w2) (ghost_of w) *)
intro.
apply jam_noat_splittable.
apply VALspec_parametric.
Qed. *)

Definition share_oblivious (P: pred rmap) :=
  forall w w',
   (forall l, match w' @ l , w @ l with
                 | NO _ _, NO _ _ => True
                 | YES _ sh1 k1 p1 , YES _ sh2 k2 p2 => k1=k2 /\ p1=p2
                 | PURE k1 p1, PURE k2 p2 => k1=k2 /\ p1=p2
                 | _ , _ => False
                 end) ->
     P w' -> P w.

(*Lemma intersection_splittable:
    forall (S': address -> address -> Prop) S P Q, 
         spec_parametric P -> 
         (forall l, share_oblivious (Q l)) ->
    forall l, splittable (fun sh => allp (@jam _ _ _ _ _ _ (S' l) (S l) (P l sh) noat) && Q l).
Proof.
(* Goal: forall (l : AV.address) (_ : not (adr_range a (size_chunk ch) l)), @identity resource Join_resource (resource_at w l) *)
(* Goal: @app_pred rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun i : address => @andp rmap ag_rmap (shareat i sh1) (nonlockat i)) noat)) noghost) (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun loc : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) sh2 loc) noat)) noghost)) w *)
intros.
(* Goal: forall (l : AV.address) (_ : not (adr_range a (size_chunk ch) l)), @identity resource Join_resource (resource_at w l) *)
(* Goal: @app_pred rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun i : address => @andp rmap ag_rmap (shareat i sh1) (nonlockat i)) noat)) noghost) (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun loc : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) sh2 loc) noat)) noghost)) w *)
intro; intros.
(* Goal: forall loc : AV.address, @join resource Join_resource (resource_at w1 loc) (resource_at w2 loc) (resource_at w loc) *)
(* Goal: @join ghost ghost_join (ghost_of w1) (ghost_of w2) (ghost_of w) *)
generalize (jam_noat_splittable S' S _ H); intro.
rewrite <- (H2  _ _ _  _ rsh1 rsh2 H1).
(* Goal: @derives rmap ag_rmap (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun loc : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) sh loc) noat)) noghost) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun i : address => @andp rmap ag_rmap (shareat i sh1) (nonlockat i)) noat)) noghost) (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun loc : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) sh2 loc) noat)) noghost)) *)
apply pred_ext; intros w ?.
destruct H3 as [w1 [w2 [? [[? ?] [? ?]]]]].
(* Goal: @app_pred rmap ag_rmap (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun loc : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) sh2 loc) noat)) noghost) w2 *)
split.
(* Goal: @identity resource Join_resource (resource_at w l) *)
exists w1; exists w2; auto.
(* Goal: @identity resource Join_resource (resource_at w l) *)
eapply H0; eauto.
(* Goal: forall loc : AV.address, @join resource Join_resource (resource_at w1 loc) (resource_at w2 loc) (resource_at w loc) *)
(* Goal: @join ghost ghost_join (ghost_of w1) (ghost_of w2) (ghost_of w) *)
intro.
generalize (resource_at_join _ _ _ l0 H3).
case_eq (w2 @ l0); case_eq (w @ l0); intros; auto; try solve [inv H10].
(* Goal: forall (l : AV.address) (_ : not (adr_range a (size_chunk ch) l)), @identity resource Join_resource (resource_at w l) *)
(* Goal: @app_pred rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun i : address => @andp rmap ag_rmap (shareat i sh1) (nonlockat i)) noat)) noghost) (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun loc : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) sh2 loc) noat)) noghost)) w *)
case_eq (w1 @ l0); intros.
rewrite H11 in H10; inv H10. 
rewrite H11 in H10; inv H10.
specialize (H4 l0).
specialize (H6 l0).
hnf in H4,H6.
(* Goal: @identity resource Join_resource (resource_at w l) *)
if_tac in H4; auto.
specialize (H l l0).
destruct H as [pp [ok ?]].
rewrite H in H4; rewrite H in H6.
destruct H4 as [? [? [? ?]]].
destruct H6 as [? [? [? ?]]].
inversion2 H11 H12.
inversion2 H9 H13.
do 3 red in H4. rewrite H11 in H4.
contradiction (YES_not_identity _ _ _ _ H4).
rewrite H11 in H10; inv H10.
(* Goal: @identity resource Join_resource (resource_at w l) *)
destruct (w1 @ l0); inv H10; auto.
(* Goal: @identity resource Join_resource (resource_at w l) *)
inv H10; auto.
destruct H3 as [[w1 [w2 [? [? ?]]]] ?].
exists w1; exists w2.
(* Goal: @identity resource Join_resource (resource_at w l) *)
split; auto.
(* Goal: @identity resource Join_resource (resource_at w l) *)
split; split; auto.
apply (H0 l w1 w).
intro l0; generalize (resource_at_join _ _ _ l0 H3).
case_eq (w @ l0); case_eq (w1 @ l0); intros; auto; try solve [inv H9].
(* Goal: forall (l : AV.address) (_ : not (adr_range a (size_chunk ch) l)), @identity resource Join_resource (resource_at w l) *)
(* Goal: @app_pred rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun i : address => @andp rmap ag_rmap (shareat i sh1) (nonlockat i)) noat)) noghost) (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun loc : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) sh2 loc) noat)) noghost)) w *)
case_eq (w2 @ l0); intros.
rewrite H10 in H9; inv H9. 
rewrite H10 in H9; inv H9.
specialize (H l l0).
destruct H as [pp [ok ?]].
specialize (H4 l0).
specialize (H5 l0).
hnf in H4,H5.
if_tac in H4.
rewrite H in H4,H5.
destruct H4 as [? [? [? ?]]].
destruct H5 as [? [? [? ?]]].
(* Goal: @eq resource (resource_at f l') (YES sh1 rsh1 k (preds_fmap (approx (@level rmap ag_rmap f)) (approx (@level rmap ag_rmap f)) pp)) *)
(* Goal: @identity resource Join_resource (resource_at f l') *)
congruence.
do 3 red in H5. rewrite H10 in H5. 
contradiction (YES_not_identity _ _ _ _ H5).
rewrite H10 in H9; inv H9.
(* Goal: @identity resource Join_resource (resource_at w l) *)
inv H9; auto.
(* Goal: @identity resource Join_resource (resource_at w l) *)
inv H9; auto.
(* Goal: @identity resource Join_resource (resource_at w l) *)
auto.
apply (H0 l w2 w ).
intro l0; generalize (resource_at_join _ _ _ l0 H3).
case_eq (w @ l0); case_eq (w2 @ l0); intros; auto; try solve [inv H9].
inv H9.
specialize (H l l0).
destruct H as [pp [ok ?]].
specialize (H4 l0).
specialize (H5 l0).
hnf in H4,H5.
if_tac in H4.
rewrite H in H4,H5.
destruct H4 as [? [? [? ?]]].
destruct H5 as [? [? [? ?]]].
(* Goal: @eq resource (resource_at f l') (YES sh1 rsh1 k (preds_fmap (approx (@level rmap ag_rmap f)) (approx (@level rmap ag_rmap f)) pp)) *)
(* Goal: @identity resource Join_resource (resource_at f l') *)
congruence.
do 3 red in H4. rewrite <- H11 in H4.
contradiction (YES_not_identity _ _ _ _ H4).
(* Goal: @identity resource Join_resource (resource_at w l) *)
inv H9; auto. inv H9; auto.
(* Goal: @identity resource Join_resource (resource_at w l) *)
auto.
Qed. *)

Lemma not_readable_share_retainer_part_eq:
  forall sh, ~ readable_share sh -> retainer_part sh = sh.
(* Goal: forall (l : AV.address) (_ : not (adr_range a (size_chunk ch) l)), @identity resource Join_resource (resource_at w l) *)
(* Goal: @app_pred rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun i : address => @andp rmap ag_rmap (shareat i sh1) (nonlockat i)) noat)) noghost) (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun loc : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) sh2 loc) noat)) noghost)) w *)
   intros.
(* Goal: @eq Share.t (retainer_part sh) sh *)
    apply not_not_share_identity in H.
(* Goal: @eq Share.t (retainer_part sh) sh *)
    unfold retainer_part.
(* Goal: @eq Share.t (Share.glb Share.Lsh sh) sh *)
    rewrite (comp_parts comp_Lsh_Rsh sh) at 2.
(* Goal: @identity share Share.Join_ba (Share.glb Share.Rsh (Share.lub (@snd Share.t Share.t (Share.split (Share.glb Share.Lsh sh))) (@snd Share.t Share.t (Share.split (Share.glb Share.Rsh sh))))) *)
    apply identity_share_bot in H; rewrite H.
(* Goal: @eq Share.t (Share.glb Share.Lsh sh) (Share.lub (Share.glb Share.Lsh sh) Share.bot) *)
    rewrite Share.lub_bot. auto.
Qed.

Lemma slice_resource_resource_share: forall r sh sh',
  resource_share r = Some sh ->
  join_sub sh' sh ->
  resource_share (slice_resource sh' r) = Some sh'.
Proof.
(* Goal: forall (l : AV.address) (_ : not (adr_range a (size_chunk ch) l)), @identity resource Join_resource (resource_at w l) *)
(* Goal: @app_pred rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun i : address => @andp rmap ag_rmap (shareat i sh1) (nonlockat i)) noat)) noghost) (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun loc : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) sh2 loc) noat)) noghost)) w *)
  intros.
(* Goal: @eq resource (slice_resource sh2 (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt)))) (YES sh2 rsh2 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt))) *)
  destruct r; inv H; unfold slice_resource; simpl.
  + f_equal.
(* Goal: and (@eq (option share) (resource_share (slice_resource sh1 (resource_at w loc))) (@Some share sh1)) (nonlock (slice_resource sh1 (resource_at w loc))) *)
    assert (~readable_share sh'). contradict n. destruct H0.
(* Goal: @identity resource Join_resource (resource_at w l) *)
    eapply join_readable1; eauto.
(* Goal: @identity resource Join_resource (resource_at w l) *)
    apply not_readable_share_retainer_part_eq; auto.
(* Goal: @identity resource Join_resource (resource_at w l) *)
  + destruct (readable_share_dec sh'); simpl; auto.
Qed.

Lemma slice_resource_nonlock: forall r sh sh',
  resource_share r = Some sh ->
  join_sub sh' sh ->
  nonlock r ->
  nonlock (slice_resource sh' r).
Proof.
(* Goal: forall (l : AV.address) (_ : not (adr_range a (size_chunk ch) l)), @identity resource Join_resource (resource_at w l) *)
(* Goal: @app_pred rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun i : address => @andp rmap ag_rmap (shareat i sh1) (nonlockat i)) noat)) noghost) (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun loc : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) sh2 loc) noat)) noghost)) w *)
  intros.
(* Goal: @identity resource Join_resource (resource_at w l) *)
  destruct r; inv H; unfold slice_resource; simpl; auto.
(* Goal: @identity resource Join_resource (resource_at w l) *)
  destruct (readable_share_dec sh'); simpl; auto.
Qed.

Lemma NO_ext: forall sh1 sh2 rsh1 rsh2, sh1=sh2 -> NO sh1 rsh1 = NO sh2 rsh2.
(* Goal: forall (l : AV.address) (_ : not (adr_range a (size_chunk ch) l)), @identity resource Join_resource (resource_at w l) *)
(* Goal: @app_pred rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun i : address => @andp rmap ag_rmap (shareat i sh1) (nonlockat i)) noat)) noghost) (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun loc : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) sh2 loc) noat)) noghost)) w *)
Proof. intros. subst sh1. f_equal. apply proof_irr. Qed.

Lemma join_sub_is_slice_resource: forall r r' sh',
  join_sub r' r ->
  resource_share r' = Some sh' ->
  r' = slice_resource sh' r.
Proof.
(* Goal: forall (l : AV.address) (_ : not (adr_range a (size_chunk ch) l)), @identity resource Join_resource (resource_at w l) *)
(* Goal: @app_pred rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun i : address => @andp rmap ag_rmap (shareat i sh1) (nonlockat i)) noat)) noghost) (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun loc : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) sh2 loc) noat)) noghost)) w *)
  intros.
(* Goal: @eq resource r' (slice_resource sh' r) *)
  destruct H as [r'' ?].
(* Goal: @eq resource (slice_resource sh2 (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt)))) (YES sh2 rsh2 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt))) *)
  destruct r, r'; inv H; inv H0; simpl.
  + f_equal.
(* Goal: @eq resource (NO sh' n0) (NO (retainer_part sh') (retainer_part_nonreadable sh')) *)
    clear - n0.
(* Goal: @eq Share.t sh' (retainer_part sh') *)
    apply NO_ext. symmetry.
(* Goal: @identity resource Join_resource (resource_at w l) *)
    rewrite not_readable_share_retainer_part_eq; auto.
  + destruct (readable_share_dec sh'); [ contradiction |].
(* Goal: @identity resource Join_resource (resource_at w l) *)
    apply NO_ext; auto.
  + destruct (readable_share_dec sh'); [| contradiction ].
(* Goal: @eq resource (YES sh rsh3 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z b) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt))) (YES sh p8 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z b) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt))) *)
    f_equal. apply proof_irr.
  + destruct (readable_share_dec sh'); [| contradiction ].
(* Goal: @eq resource (YES sh rsh3 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z b) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt))) (YES sh p8 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z b) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt))) *)
    f_equal. apply proof_irr.
Qed.

Lemma slice_resource_share_join: forall sh1 sh2 sh r,
  join sh1 sh2 sh ->
  resource_share r = Some sh ->
  join (slice_resource sh1 r) (slice_resource sh2 r) r.
Proof.
(* Goal: forall (l : AV.address) (_ : not (adr_range a (size_chunk ch) l)), @identity resource Join_resource (resource_at w l) *)
(* Goal: @app_pred rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun i : address => @andp rmap ag_rmap (shareat i sh1) (nonlockat i)) noat)) noghost) (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun loc : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) sh2 loc) noat)) noghost)) w *)
  intros.
  destruct r; simpl in *.
*
(* Goal: @join resource Join_resource (PURE k p) (PURE k p) (PURE k p) *)
  constructor. inv H0.
(* Goal: @join Share.t Share.Join_ba (retainer_part sh1) (retainer_part sh2) sh *)
  assert (~readable_share sh1) by (contradict n; eapply join_readable1; eauto).
(* Goal: @join Share.t Share.Join_ba (retainer_part sh1) (retainer_part sh2) sh *)
  assert (~readable_share sh2) by (contradict n; eapply join_readable2; eauto).
(* Goal: @identity resource Join_resource (resource_at w l) *)
  rewrite !(not_readable_share_retainer_part_eq); auto.
*
(* Goal: @join resource Join_resource match readable_share_dec sh1 with | left r1 => YES sh1 r1 k p | right n => NO sh1 n end match readable_share_dec sh2 with | left r1 => YES sh2 r1 k p | right n => NO sh2 n end (YES sh0 r k p) *)
  inv H0.
  destruct (readable_share_dec sh1), (readable_share_dec sh2);
  try (constructor; auto).
(* Goal: @join resource Join_resource (NO sh1 n) (NO sh2 n0) (YES sh r k p) *)
  contradiction (join_unreadable_shares H n n0).
*
(* Goal: @join resource Join_resource (PURE k p) (PURE k p) (PURE k p) *)
  constructor.
Qed.

Definition resource_share_split (p q r: address -> pred rmap): Prop :=
  exists p' q' r' p_sh q_sh r_sh,
    is_resource_pred p p' /\
    is_resource_pred q q' /\
    is_resource_pred r r' /\
    join q_sh r_sh p_sh /\
    (forall res l n, p' res l n ->
      resource_share res = Some p_sh /\
      q' (slice_resource q_sh res) l n /\
      r' (slice_resource r_sh res) l n) /\
    (forall p_res q_res r_res l n,
      join q_res r_res p_res ->
      q' q_res l n ->
      r' r_res l n ->
      p' p_res l n).

(* We should use this lemma to prove all share_join lemmas, also all splittable lemmas. *)
Lemma allp_jam_share_split: forall (P: address -> Prop) (p q r: address -> pred rmap)
  (P_DEC: forall l, {P l} + {~ P l}),
  resource_share_split p q r ->
  allp (jam P_DEC p noat) && noghost =
  (allp (jam P_DEC q noat) && noghost) * (allp (jam P_DEC r noat) && noghost).
Proof.
(* Goal: forall (l : AV.address) (_ : not (adr_range a (size_chunk ch) l)), @identity resource Join_resource (resource_at w l) *)
(* Goal: @app_pred rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun i : address => @andp rmap ag_rmap (shareat i sh1) (nonlockat i)) noat)) noghost) (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun loc : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) sh2 loc) noat)) noghost)) w *)
  intros.
(* Goal: @eq (@pred rmap ag_rmap) (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address P P_DEC p noat)) noghost) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address P P_DEC q noat)) noghost) (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address P P_DEC r noat)) noghost)) *)
  destruct H as [p' [q' [r' [p_sh [q_sh [r_sh [? [? [? [? [? ?]]]]]]]]]]].
(* Goal: forall (l : AV.address) (_ : not (adr_range a (size_chunk ch) l)), @identity resource Join_resource (resource_at w l) *)
(* Goal: @app_pred rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun i : address => @andp rmap ag_rmap (shareat i sh1) (nonlockat i)) noat)) noghost) (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun loc : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) sh2 loc) noat)) noghost)) w *)
  apply pred_ext; intros w; simpl; intros.
  + destruct H5 as [H5 Hg].
(* Goal: @ex rmap (fun y : rmap => @ex rmap (fun z : rmap => and (@join rmap Join_rmap y z w) (and (and (forall b : address, if P_DEC b then @app_pred rmap ag_rmap (q b) y else @identity resource Join_resource (resource_at y b)) (@identity ghost ghost_join (ghost_of y))) (and (forall b : address, if P_DEC b then @app_pred rmap ag_rmap (r b) z else @identity resource Join_resource (resource_at z b)) (@identity ghost ghost_join (ghost_of z)))))) *)
    destruct (make_slice_rmap w P P_DEC q_sh) as [w1 [? ?]].
(* Goal: forall (l : AV.address) (_ : not (P l)), @identity resource Join_resource (resource_at w l) *)
(* Goal: @ex rmap (fun y : rmap => @ex rmap (fun z : rmap => and (@join rmap Join_rmap y z w) (and (and (forall b : address, if P_DEC b then @app_pred rmap ag_rmap (q b) y else @identity resource Join_resource (resource_at y b)) (@identity ghost ghost_join (ghost_of y))) (and (forall b : address, if P_DEC b then @app_pred rmap ag_rmap (r b) z else @identity resource Join_resource (resource_at z b)) (@identity ghost ghost_join (ghost_of z)))))) *)
    {
(* Goal: forall (l : AV.address) (_ : not (P l)), @identity resource Join_resource (resource_at w l) *)
      intros; specialize (H5 l).
(* Goal: @identity resource Join_resource (resource_at w l) *)
      rewrite if_false in H5 by auto.
(* Goal: @identity resource Join_resource (resource_at w l) *)
      auto.
    }
(* Goal: @ex rmap (fun y : rmap => @ex rmap (fun z : rmap => and (@join rmap Join_rmap y z w) (and (and (forall b : address, if P_DEC b then @app_pred rmap ag_rmap (q b) y else @identity resource Join_resource (resource_at y b)) (@identity ghost ghost_join (ghost_of y))) (and (forall b : address, if P_DEC b then @app_pred rmap ag_rmap (r b) z else @identity resource Join_resource (resource_at z b)) (@identity ghost ghost_join (ghost_of z)))))) *)
    destruct (make_slice_rmap w P P_DEC r_sh) as [w2 [? ?]].
(* Goal: forall (l : AV.address) (_ : not (P l)), @identity resource Join_resource (resource_at w l) *)
(* Goal: @ex rmap (fun y : rmap => @ex rmap (fun z : rmap => and (@join rmap Join_rmap y z w) (and (and (forall b : address, if P_DEC b then @app_pred rmap ag_rmap (q b) y else @identity resource Join_resource (resource_at y b)) (@identity ghost ghost_join (ghost_of y))) (and (forall b : address, if P_DEC b then @app_pred rmap ag_rmap (r b) z else @identity resource Join_resource (resource_at z b)) (@identity ghost ghost_join (ghost_of z)))))) *)
    {
(* Goal: forall (l : AV.address) (_ : not (P l)), @identity resource Join_resource (resource_at w l) *)
      intros; specialize (H5 l).
(* Goal: @identity resource Join_resource (resource_at w l) *)
      rewrite if_false in H5 by auto.
(* Goal: @identity resource Join_resource (resource_at w l) *)
      auto.
    }
(* Goal: @app_pred rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun i : address => @andp rmap ag_rmap (shareat i sh1) (nonlockat i)) noat)) noghost) (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun loc : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) sh2 loc) noat)) noghost)) w *)
    exists w1, w2.
(* Goal: and (@join rmap Join_rmap w1 w2 w) (and (@app_pred rmap ag_rmap (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun i : address => @andp rmap ag_rmap (shareat i sh1) (nonlockat i)) noat)) noghost) w1) (@app_pred rmap ag_rmap (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun loc : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) sh2 loc) noat)) noghost) w2)) *)
    split3.
(* Goal: @eq resource (resource_at f l') (YES sh1 rsh1 k (preds_fmap (approx (@level rmap ag_rmap f)) (approx (@level rmap ag_rmap f)) pp)) *)
(* Goal: @identity resource Join_resource (resource_at f l') *)
    - apply resource_at_join2; try congruence.
(* Goal: forall loc : AV.address, @join resource Join_resource (resource_at w1 loc) (resource_at w2 loc) (resource_at w loc) *)
(* Goal: @join ghost ghost_join (ghost_of w1) (ghost_of w2) (ghost_of w) *)
      intro l.
(* Goal: @join resource Join_resource (resource_at w1 l) (resource_at w2 l) (resource_at w l) *)
(* Goal: @join ghost ghost_join (ghost_of w1) (ghost_of w2) (ghost_of w) *)
      destruct H7, H9; rewrite H7, H9; clear H7 H9.
(* Goal: @join resource Join_resource (if P_DEC l then slice_resource q_sh (resource_at w l) else resource_at w l) (if P_DEC l then slice_resource r_sh (resource_at w l) else resource_at w l) (resource_at w l) *)
(* Goal: @join ghost ghost_join (ghost_of w1) (ghost_of w2) (ghost_of w) *)
      specialize (H5 l); destruct (P_DEC l).
      * eapply slice_resource_share_join; eauto.
(* Goal: if P_DEC l then r' (if P_DEC l then slice_resource r_sh (resource_at w l) else resource_at w l) l (@level rmap ag_rmap w) else @identity resource Join_resource (if P_DEC l then slice_resource r_sh (resource_at w l) else resource_at w l) *)
        rewrite H in H5.
(* Goal: r' (slice_resource r_sh (resource_at w l)) l (@level rmap ag_rmap w) *)
        apply H3 in H5.
(* Goal: @identity resource Join_resource (resource_at w l) *)
        tauto.
      * apply identity_unit' in H5.
(* Goal: @join resource Join_resource (resource_at w l) (resource_at w l) (resource_at w l) *)
        exact H5.
      * destruct H7 as [? ->], H9 as [? ->].
(* Goal: @identity resource Join_resource (resource_at w l) *)
        apply identity_unit'; auto.
(* Goal: @identity resource Join_resource (resource_at w l) *)
    - destruct H7 as [H7 ->]; split; auto.
(* Goal: forall b : address, if P_DEC b then @app_pred rmap ag_rmap (r b) w2 else @identity resource Join_resource (resource_at w2 b) *)
      intros l.
(* Goal: if P_DEC l then @app_pred rmap ag_rmap (q l) w1 else @identity resource Join_resource (resource_at w1 l) *)
      rewrite H0, H7, H6.
(* Goal: if P_DEC l then r' (if P_DEC l then slice_resource r_sh (resource_at w l) else resource_at w l) l (@level rmap ag_rmap w) else @identity resource Join_resource (if P_DEC l then slice_resource r_sh (resource_at w l) else resource_at w l) *)
      specialize (H5 l).
(* Goal: if P_DEC l then r' (if P_DEC l then slice_resource r_sh (resource_at w l) else resource_at w l) l (@level rmap ag_rmap w) else @identity resource Join_resource (if P_DEC l then slice_resource r_sh (resource_at w l) else resource_at w l) *)
      rewrite H in H5.
(* Goal: if adr_range_dec a (size_chunk ch) b then @app_pred rmap ag_rmap (yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z b) (@snd block Z a))) bl Undef)) sh b) z else @app_pred rmap ag_rmap (noat b) z *)
(* Goal: @app_pred rmap ag_rmap noghost z *)
      if_tac.
      * apply H3 in H5.
(* Goal: @identity resource Join_resource (resource_at w l) *)
        tauto.
      * auto.
(* Goal: @identity resource Join_resource (resource_at w l) *)
    - destruct H9 as [H9 ->]; split; auto.
(* Goal: forall b : address, if P_DEC b then @app_pred rmap ag_rmap (r b) w2 else @identity resource Join_resource (resource_at w2 b) *)
      intros l.
(* Goal: if P_DEC l then @app_pred rmap ag_rmap (r l) w2 else @identity resource Join_resource (resource_at w2 l) *)
      rewrite H1, H9, H8.
(* Goal: if P_DEC l then r' (if P_DEC l then slice_resource r_sh (resource_at w l) else resource_at w l) l (@level rmap ag_rmap w) else @identity resource Join_resource (if P_DEC l then slice_resource r_sh (resource_at w l) else resource_at w l) *)
      specialize (H5 l).
(* Goal: if P_DEC l then r' (if P_DEC l then slice_resource r_sh (resource_at w l) else resource_at w l) l (@level rmap ag_rmap w) else @identity resource Join_resource (if P_DEC l then slice_resource r_sh (resource_at w l) else resource_at w l) *)
      rewrite H in H5.
(* Goal: if adr_range_dec a (size_chunk ch) b then @app_pred rmap ag_rmap (yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z b) (@snd block Z a))) bl Undef)) sh b) z else @app_pred rmap ag_rmap (noat b) z *)
(* Goal: @app_pred rmap ag_rmap noghost z *)
      if_tac.
      * apply H3 in H5.
(* Goal: @identity resource Join_resource (resource_at w l) *)
        tauto.
      * auto.
  + destruct H5 as [y [z [? [? ?]]]].
(* Goal: @app_pred rmap ag_rmap (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun loc : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) sh2 loc) noat)) noghost) w2 *)
    destruct H6 as [? Hg1], H7 as [? Hg2]; split.
(* Goal: forall b : address, if P_DEC b then @app_pred rmap ag_rmap (p b) w else @identity resource Join_resource (resource_at w b) *)
(* Goal: @identity ghost ghost_join (ghost_of w) *)
    intro b; specialize (H6 b); specialize (H7 b).
(* Goal: if adr_range_dec a (size_chunk ch) b then @app_pred rmap ag_rmap (yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z b) (@snd block Z a))) bl Undef)) sh b) z else @app_pred rmap ag_rmap (noat b) z *)
(* Goal: @app_pred rmap ag_rmap noghost z *)
    if_tac.
    - rewrite H; rewrite H0 in H6; rewrite H1 in H7.
(* Goal: p' (resource_at w b) b (@level rmap ag_rmap w) *)
      destruct (join_level _ _ _ H5).
(* Goal: p' (resource_at w b) b (@level rmap ag_rmap w) *)
      rewrite H9 in H6; rewrite H10 in H7.
(* Goal: @identity resource Join_resource (resource_at w l) *)
      eapply H4; eauto.
(* Goal: @identity resource Join_resource (resource_at w l) *)
      apply resource_at_join; auto.
    - apply resource_at_join with (loc := b) in H5.
(* Goal: @identity resource Join_resource (resource_at w l) *)
      apply H6 in H5; rewrite <- H5; auto.
(* Goal: @identity resource Join_resource (resource_at w l) *)
    - rewrite <- (Hg1 _ _ (ghost_of_join _ _ _ H5)); auto.
Qed.

Lemma address_mapsto_share_join:
 forall (sh1 sh2 sh : share) ch v a,
   join sh1 sh2 sh ->
   readable_share sh1 -> readable_share sh2 ->
   address_mapsto ch v sh1 a * address_mapsto ch v sh2 a 
    = address_mapsto ch v sh a.
Proof.
  intros ? ? ? ? ? ? H rsh1 rsh2.
(*  rename H1 into NON_UNIT1, H2 into NON_UNIT2.
  assert (NON_UNIT: nonunit sh) by (eapply nonunit_join; eauto; auto with typeclass_instances).
*)
(* Goal: @eq Share.t sh' (retainer_part sh') *)
  symmetry.
  unfold address_mapsto.
  transitivity
   (EX  bl : list memval,
    !!(length bl = size_chunk_nat ch /\
       decode_val ch bl = v /\ (align_chunk ch | snd a)) &&
   ((allp
      (jam (adr_range_dec a (size_chunk ch))
         (fun loc : address =>
          yesat NoneP (VAL (nth (nat_of_Z (snd loc - snd a)) bl Undef)) sh1
            loc) noat) && noghost) *
    (allp
      (jam (adr_range_dec a (size_chunk ch))
         (fun loc : address =>
          yesat NoneP (VAL (nth (nat_of_Z (snd loc - snd a)) bl Undef)) sh2
            loc) noat) && noghost))).
  + pose proof log_normalize.exp_congr (pred rmap) _ (list memval).
(* Goal: @eq resource (slice_resource sh2 (resource_at w loc)) (YES sh2 rsh2 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt))) *)
    simpl in H0.
(* Goal: @eq resource (slice_resource sh2 (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt)))) (YES sh2 rsh2 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt))) *)
    apply H0; clear H0.
    intros b.
(* Goal: @eq resource (YES sh rsh3 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z b) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt))) (YES sh p8 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z b) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt))) *)
    rewrite !andp_assoc; f_equal.
(* Goal: @app_pred rmap ag_rmap (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun loc : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) sh2 loc) noat)) noghost) w2 *)
    apply allp_jam_share_split.
    do 3 eexists.
    exists sh, sh1, sh2.
    split; [| split; [| split; [| split; [| split]]]].
    - apply is_resource_pred_YES_VAL'.
    - apply is_resource_pred_YES_VAL'.
    - apply is_resource_pred_YES_VAL'.
(* Goal: @identity resource Join_resource (resource_at w l) *)
    - auto.
(* Goal: forall (l : AV.address) (_ : not (adr_range a (size_chunk ch) l)), @identity resource Join_resource (resource_at w l) *)
(* Goal: @app_pred rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun i : address => @andp rmap ag_rmap (shareat i sh1) (nonlockat i)) noat)) noghost) (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun loc : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) sh2 loc) noat)) noghost)) w *)
    - simpl; intros.
(* Goal: and (@eq (option share) (resource_share (slice_resource sh1 (resource_at w loc))) (@Some share sh1)) (nonlock (slice_resource sh1 (resource_at w loc))) *)
      destruct H0.
      split; [subst; auto |].
(* Goal: @app_pred rmap ag_rmap (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun loc : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) sh2 loc) noat)) noghost) w2 *)
      split.
      * exists rsh1.
(* Goal: @eq resource (slice_resource sh2 (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt)))) (YES sh2 rsh2 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt))) *)
        subst; simpl.
(* Goal: @eq resource match readable_share_dec sh1 with | left r1 => YES sh1 r1 k0 (SomeP A _f) | right n => NO sh1 n end (YES sh1 rsh1 k0 (preds_fmap (approx (@level rmap ag_rmap f)) (approx (@level rmap ag_rmap f)) pp)) *)
(* Goal: @eq resource (resource_at f l') (YES sh1 rsh1 k (preds_fmap (approx (@level rmap ag_rmap f)) (approx (@level rmap ag_rmap f)) pp)) *)
(* Goal: @identity resource Join_resource (resource_at f l') *)
        destruct (readable_share_dec sh1); [| contradiction].
(* Goal: @eq resource (YES sh rsh3 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z b) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt))) (YES sh p8 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z b) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt))) *)
        f_equal.
        auto with extensionality.
      * exists rsh2.
(* Goal: @eq resource (slice_resource sh2 (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt)))) (YES sh2 rsh2 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt))) *)
        subst; simpl.
        destruct (readable_share_dec sh); [| contradiction].
(* Goal: @eq resource match readable_share_dec sh2 with | left r1 => YES sh2 r1 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt)) | right n => NO sh2 n end (YES sh2 rsh2 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt))) *)
        destruct (readable_share_dec sh2); [| contradiction].
(* Goal: @eq resource (YES sh rsh3 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z b) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt))) (YES sh p8 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z b) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt))) *)
        f_equal.
        auto with extensionality. 
(* Goal: forall (l : AV.address) (_ : not (adr_range a (size_chunk ch) l)), @identity resource Join_resource (resource_at w l) *)
(* Goal: @app_pred rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun i : address => @andp rmap ag_rmap (shareat i sh1) (nonlockat i)) noat)) noghost) (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun loc : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) sh2 loc) noat)) noghost)) w *)
    - simpl; intros.
      destruct H1,H2. repeat proof_irr.
      exists (join_readable1 H rsh1).
(* Goal: @identity share Share.Join_ba (Share.glb Share.Rsh (Share.lub (@snd Share.t Share.t (Share.split (Share.glb Share.Lsh sh))) b)) *)
      subst.
(* Goal: @join resource Join_resource match readable_share_dec sh1 with | left r1 => YES sh1 r1 k p | right n => NO sh1 n end match readable_share_dec sh2 with | left r1 => YES sh2 r1 k p | right n => NO sh2 n end (YES sh0 r k p) *)
      inv H0.
      apply YES_ext.
(* Goal: @identity resource Join_resource (resource_at w l) *)
      eapply join_eq; eauto.
  + apply pred_ext.
    - apply exp_left; intro bl.
(* Goal: forall loc : AV.address, @join resource Join_resource (resource_at w1 loc) (resource_at w2 loc) (resource_at w loc) *)
(* Goal: @join ghost ghost_join (ghost_of w1) (ghost_of w2) (ghost_of w) *)
      apply prop_andp_left; intro.
      rewrite exp_sepcon1.
      apply (exp_right bl).
(* Goal: @eq (@pred rmap ag_rmap) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun i : address => @andp rmap ag_rmap (shareat i sh1) (nonlockat i)) noat)) noghost) (@exp rmap ag_rmap (list memval) (fun bl : list memval => @andp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (and (@eq nat (@Datatypes.length memval bl) (size_chunk_nat ch)) (and (@eq val (decode_val ch bl) v) (Z.divide (align_chunk ch) (@snd block Z a))))) (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun loc : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) sh2 loc) noat))) noghost))) (@exp rmap ag_rmap (list memval) (fun bl : list memval => @andp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (and (@eq nat (@Datatypes.length memval bl) (size_chunk_nat ch)) (and (@eq val (decode_val ch bl) v) (Z.divide (align_chunk ch) (@snd block Z a))))) (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun loc : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) sh loc) noat))) noghost)) *)
      rewrite exp_sepcon2.
      apply (exp_right bl).
      rewrite andp_assoc, sepcon_andp_prop1.
      apply andp_right; [intros w _; simpl; auto |].
      rewrite andp_assoc, sepcon_andp_prop.
      apply andp_right; [intros w _; simpl; auto |].
(* Goal: @identity resource Join_resource (resource_at w l) *)
      auto.
    - rewrite exp_sepcon1.
      apply exp_left; intro bl1.
(* Goal: @eq (@pred rmap ag_rmap) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun i : address => @andp rmap ag_rmap (shareat i sh1) (nonlockat i)) noat)) noghost) (@exp rmap ag_rmap (list memval) (fun bl : list memval => @andp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (and (@eq nat (@Datatypes.length memval bl) (size_chunk_nat ch)) (and (@eq val (decode_val ch bl) v) (Z.divide (align_chunk ch) (@snd block Z a))))) (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun loc : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) sh2 loc) noat))) noghost))) (@exp rmap ag_rmap (list memval) (fun bl : list memval => @andp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (and (@eq nat (@Datatypes.length memval bl) (size_chunk_nat ch)) (and (@eq val (decode_val ch bl) v) (Z.divide (align_chunk ch) (@snd block Z a))))) (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun loc : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) sh loc) noat))) noghost)) *)
      rewrite exp_sepcon2.
      apply exp_left; intro bl2.
      rewrite andp_assoc, sepcon_andp_prop1.
(* Goal: forall loc : AV.address, @join resource Join_resource (resource_at w1 loc) (resource_at w2 loc) (resource_at w loc) *)
(* Goal: @join ghost ghost_join (ghost_of w1) (ghost_of w2) (ghost_of w) *)
      apply prop_andp_left; intro.
      rewrite andp_assoc, sepcon_andp_prop.
(* Goal: forall loc : AV.address, @join resource Join_resource (resource_at w1 loc) (resource_at w2 loc) (resource_at w loc) *)
(* Goal: @join ghost ghost_join (ghost_of w1) (ghost_of w2) (ghost_of w) *)
      apply prop_andp_left; intro.
      apply (exp_right bl1).
      apply andp_right; [intros w _; simpl; auto |].
(* Goal: @derives rmap ag_rmap (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun loc : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) sh loc) noat)) noghost) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun i : address => @andp rmap ag_rmap (shareat i sh1) (nonlockat i)) noat)) noghost) (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun loc : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) sh2 loc) noat)) noghost)) *)
      intros w ?.
      destruct H2 as [w1 [w2 [? [? ?]]]].
(* Goal: @app_pred rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun i : address => @andp rmap ag_rmap (shareat i sh1) (nonlockat i)) noat)) noghost) (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun loc : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) sh2 loc) noat)) noghost)) w *)
      exists w1, w2.
(* Goal: @identity resource Join_resource (resource_at w l) *)
      split; [| split]; auto.
(* Goal: @identity resource Join_resource (resource_at w l) *)
      destruct H4 as [H4 Hg]; split; auto.
      intro l; destruct H3; specialize (H3 l); specialize (H4 l).
      simpl in H3, H4 |- *.
(* Goal: @identity resource Join_resource (resource_at w l) *)
      if_tac; auto.
(* Goal: @ex (readable_share sh2) (fun rsh : readable_share sh2 => @eq resource (slice_resource sh2 (resource_at w loc)) (YES sh2 rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt)))) *)
      destruct H3, H4. exists rsh2.
      apply resource_at_join with (loc := l) in H2.
      rewrite H3, H4 in H2; inv H2.
(* Goal: @identity resource Join_resource (resource_at w l) *)
      rewrite H12. rewrite H4. apply YES_ext. auto.
Qed.

Lemma nonlock_permission_bytes_address_mapsto_join:
 forall (sh1 sh2 sh : share) ch v a,
   join sh1 sh2 sh ->
   readable_share sh2 ->
   nonlock_permission_bytes sh1 a (Memdata.size_chunk ch)
     * address_mapsto ch v sh2 a 
    = address_mapsto ch v sh a.
Proof.
(* Goal: forall (l : AV.address) (_ : not (adr_range a (size_chunk ch) l)), @identity resource Join_resource (resource_at w l) *)
(* Goal: @app_pred rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun i : address => @andp rmap ag_rmap (shareat i sh1) (nonlockat i)) noat)) noghost) (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun loc : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) sh2 loc) noat)) noghost)) w *)
intros. rename H0 into rsh2.
(* Goal: @eq (@pred rmap ag_rmap) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (nonlock_permission_bytes sh1 a (size_chunk ch)) (address_mapsto ch v sh2 a)) (address_mapsto ch v sh a) *)
unfold nonlock_permission_bytes, address_mapsto.
(* Goal: @eq (@pred rmap ag_rmap) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun i : address => @andp rmap ag_rmap (shareat i sh1) (nonlockat i)) noat)) noghost) (@exp rmap ag_rmap (list memval) (fun bl : list memval => @andp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (and (@eq nat (@Datatypes.length memval bl) (size_chunk_nat ch)) (and (@eq val (decode_val ch bl) v) (Z.divide (align_chunk ch) (@snd block Z a))))) (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun loc : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) sh2 loc) noat))) noghost))) (@exp rmap ag_rmap (list memval) (fun bl : list memval => @andp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (and (@eq nat (@Datatypes.length memval bl) (size_chunk_nat ch)) (and (@eq val (decode_val ch bl) v) (Z.divide (align_chunk ch) (@snd block Z a))))) (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun loc : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) sh loc) noat))) noghost)) *)
rewrite exp_sepcon2.
(* Goal: @eq resource (YES sh rsh3 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z b) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt))) (YES sh p8 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z b) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt))) *)
f_equal. extensionality bl.
(* Goal: @eq (@pred rmap ag_rmap) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun i : address => @andp rmap ag_rmap (shareat i sh1) (nonlockat i)) noat)) noghost) (@andp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (and (@eq nat (@Datatypes.length memval bl) (size_chunk_nat ch)) (and (@eq val (decode_val ch bl) v) (Z.divide (align_chunk ch) (@snd block Z a))))) (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun loc : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) sh2 loc) noat))) noghost)) (@andp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (and (@eq nat (@Datatypes.length memval bl) (size_chunk_nat ch)) (and (@eq val (decode_val ch bl) v) (Z.divide (align_chunk ch) (@snd block Z a))))) (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun loc : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) sh loc) noat))) noghost) *)
rewrite !andp_assoc, sepcon_andp_prop.
(* Goal: @eq resource (YES sh rsh3 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z b) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt))) (YES sh p8 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z b) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt))) *)
f_equal.
(* Goal: @eq (@pred rmap ag_rmap) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun i : address => @andp rmap ag_rmap (shareat i sh1) (nonlockat i)) noat)) noghost) (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun loc : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) sh2 loc) noat)) noghost)) (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun loc : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) sh loc) noat)) noghost) *)
apply pred_ext.
*
(* Goal: @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun i : address => @andp rmap ag_rmap (shareat i sh1) (nonlockat i)) noat)) noghost) (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun loc : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) sh2 loc) noat)) noghost)) (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun loc : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) sh loc) noat)) noghost) *)
 intros z [x [y [? [? ?]]]].
(* Goal: @app_pred rmap ag_rmap (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun loc : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) sh2 loc) noat)) noghost) w2 *)
 destruct H1 as [H1 Hg1], H2 as [H2 Hg2]; split.
(* Goal: @app_pred rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun loc : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) sh loc) noat)) z *)
(* Goal: @app_pred rmap ag_rmap noghost z *)
 intro b; specialize (H1 b); specialize (H2 b).
(* Goal: @app_pred rmap ag_rmap (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun loc : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) sh loc) noat b) z *)
(* Goal: @app_pred rmap ag_rmap noghost z *)
 pose proof (resource_at_join _ _ _ b H0).
 hnf in H1,H2|-*.
(* Goal: if adr_range_dec a (size_chunk ch) b then @app_pred rmap ag_rmap (yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z b) (@snd block Z a))) bl Undef)) sh b) z else @app_pred rmap ag_rmap (noat b) z *)
(* Goal: @app_pred rmap ag_rmap noghost z *)
 if_tac.
 +
(* Goal: @app_pred rmap ag_rmap (yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z b) (@snd block Z a))) bl Undef)) sh b) z *)
  destruct H2 as [p ?].
  hnf in H2. rewrite H2 in *. clear H2.
(* Goal: @app_pred rmap ag_rmap (yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z b) (@snd block Z a))) bl Undef)) sh b) z *)
  destruct H1 as [H1 H1'].
(* Goal: @app_pred rmap ag_rmap (yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z b) (@snd block Z a))) bl Undef)) sh b) z *)
  hnf in H1, H1'. unfold resource_share in H1.
(* Goal: @app_pred rmap ag_rmap (yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z b) (@snd block Z a))) bl Undef)) sh b) z *)
  assert (p8 := join_readable2 H p).
(* Goal: @app_pred rmap ag_rmap (yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z b) (@snd block Z a))) bl Undef)) sh b) z *)
  exists p8.
(* Goal: @app_pred rmap ag_rmap (yesat_raw NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z b) (@snd block Z a))) bl Undef)) sh p8 b) z *)
  destruct (x @ b); inv H1.
  -
(* Goal: @app_pred rmap ag_rmap (yesat_raw NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z b) (@snd block Z a))) bl Undef)) sh p8 b) z *)
    inv H3.
(* Goal: @eq resource (YES sh4 rsh3 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z b) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt))) (YES sh p8 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z b) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt))) *)
    pose proof (join_eq H RJ); subst sh4. clear RJ.
    hnf. rewrite <- H8; clear H8.
(* Goal: @eq resource (YES sh rsh3 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z b) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt))) (YES sh p8 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z b) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt))) *)
    f_equal. apply proof_irr.
  -
(* Goal: @app_pred rmap ag_rmap (yesat_raw NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z b) (@snd block Z a))) bl Undef)) sh p8 b) z *)
   clear H1'.  inv H3. 
(* Goal: @eq resource (slice_resource sh2 (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt)))) (YES sh2 rsh2 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt))) *)
   hnf. rewrite <- H10. clear H10. simpl.
(* Goal: @eq resource (YES sh4 rsh3 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z b) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt))) (YES sh p8 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z b) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt))) *)
    pose proof (join_eq H RJ); subst sh4. clear RJ.
(* Goal: @eq resource (YES sh rsh3 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z b) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt))) (YES sh p8 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z b) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt))) *)
   f_equal. apply proof_irr.
 +
   do 3 red in H1,H2|-*. 
(* Goal: @identity resource Join_resource (resource_at w l) *)
   apply join_unit1_e in H3; auto.
(* Goal: @identity resource Join_resource (resource_at w l) *)
   rewrite <- H3; auto.
(* Goal: @identity resource Join_resource (resource_at w l) *)
 + simpl; rewrite <- (Hg1 _ _ (ghost_of_join _ _ _ H0)); auto.
*
(* Goal: @derives rmap ag_rmap (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun loc : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) sh loc) noat)) noghost) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun i : address => @andp rmap ag_rmap (shareat i sh1) (nonlockat i)) noat)) noghost) (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun loc : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) sh2 loc) noat)) noghost)) *)
  assert (rsh := join_readable2 H rsh2).
(* Goal: @derives rmap ag_rmap (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun loc : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) sh loc) noat)) noghost) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun i : address => @andp rmap ag_rmap (shareat i sh1) (nonlockat i)) noat)) noghost) (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun loc : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) sh2 loc) noat)) noghost)) *)
  intros w ?.
(* Goal: @app_pred rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun i : address => @andp rmap ag_rmap (shareat i sh1) (nonlockat i)) noat)) noghost) (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun loc : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) sh2 loc) noat)) noghost)) w *)
  destruct H0 as [H0 Hg]; hnf in H0.
  destruct (make_slice_rmap w _ (adr_range_dec a (size_chunk ch)) sh1)
   as [w1 [? ?]].
(* Goal: forall (l : AV.address) (_ : not (adr_range a (size_chunk ch) l)), @identity resource Join_resource (resource_at w l) *)
(* Goal: @app_pred rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun i : address => @andp rmap ag_rmap (shareat i sh1) (nonlockat i)) noat)) noghost) (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun loc : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) sh2 loc) noat)) noghost)) w *)
  intros. specialize (H0 l). simpl in H0. rewrite if_false in H0; auto. 
  destruct (make_slice_rmap w _ (adr_range_dec a (size_chunk ch)) sh2)
   as [w2 [? ?]].
(* Goal: forall (l : AV.address) (_ : not (adr_range a (size_chunk ch) l)), @identity resource Join_resource (resource_at w l) *)
(* Goal: @app_pred rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun i : address => @andp rmap ag_rmap (shareat i sh1) (nonlockat i)) noat)) noghost) (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun loc : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) sh2 loc) noat)) noghost)) w *)
  intros. specialize (H0 l). simpl in H0. rewrite if_false in H0; auto. 
(* Goal: @app_pred rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun i : address => @andp rmap ag_rmap (shareat i sh1) (nonlockat i)) noat)) noghost) (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun loc : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) sh2 loc) noat)) noghost)) w *)
  exists w1, w2.
(* Goal: and (@join rmap Join_rmap w1 w2 w) (and (@app_pred rmap ag_rmap (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun i : address => @andp rmap ag_rmap (shareat i sh1) (nonlockat i)) noat)) noghost) w1) (@app_pred rmap ag_rmap (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun loc : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) sh2 loc) noat)) noghost) w2)) *)
  destruct H2 as [H2 Hg1], H4 as [H4 Hg2].
(* Goal: and (@join rmap Join_rmap w1 w2 w) (and (@app_pred rmap ag_rmap (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun i : address => @andp rmap ag_rmap (shareat i sh1) (nonlockat i)) noat)) noghost) w1) (@app_pred rmap ag_rmap (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun loc : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) sh2 loc) noat)) noghost) w2)) *)
  split3.
 +
(* Goal: @join rmap Join_rmap w1 w2 w *)
   eapply resource_at_join2; try omega.
(* Goal: forall loc : AV.address, @join resource Join_resource (resource_at w1 loc) (resource_at w2 loc) (resource_at w loc) *)
(* Goal: @join ghost ghost_join (ghost_of w1) (ghost_of w2) (ghost_of w) *)
  intro . rewrite H2,H4. clear dependent w1. clear dependent w2.
(* Goal: if adr_range_dec a (size_chunk ch) loc then @ex (readable_share sh2) (fun rsh : readable_share sh2 => @eq resource (if adr_range_dec a (size_chunk ch) loc then slice_resource sh2 (resource_at w loc) else resource_at w loc) (YES sh2 rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt)))) else @identity resource Join_resource (if adr_range_dec a (size_chunk ch) loc then slice_resource sh2 (resource_at w loc) else resource_at w loc) *)
(* Goal: @app_pred rmap ag_rmap noghost w2 *)
  specialize (H0 loc). hnf in H0.  
(* Goal: @eq resource (slice_resource sh2 (resource_at w loc)) (YES sh2 rsh2 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt))) *)
  if_tac in H0. destruct H0 as [rsh' H0]. proof_irr. rewrite H0.
(* Goal: and (@eq (option share) (resource_share (slice_resource sh1 (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (preds_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) NoneP)))) (@Some share sh1)) (nonlock (slice_resource sh1 (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (preds_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) NoneP)))) *)
  unfold slice_resource.
(* Goal: @eq resource (YES sh2 r (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt))) (YES sh2 rsh2 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt))) *)
  destruct (readable_share_dec sh2); [ | contradiction]. proof_irr.
(* Goal: and (@eq (option share) (resource_share match readable_share_dec sh1 with | left r1 => YES sh1 r1 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (preds_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) NoneP) | right n => NO sh1 n end) (@Some share sh1)) (nonlock match readable_share_dec sh1 with | left r1 => YES sh1 r1 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (preds_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) NoneP) | right n => NO sh1 n end) *)
  destruct (readable_share_dec sh1).
(* Goal: @identity resource Join_resource (resource_at w l) *)
  constructor; auto.
(* Goal: @identity resource Join_resource (resource_at w l) *)
  constructor; auto.
(* Goal: @join resource Join_resource (resource_at w loc) (resource_at w loc) (resource_at w loc) *)
(* Goal: @join ghost ghost_join (ghost_of w1) (ghost_of w2) (ghost_of w) *)
  do 3 red in H0.
(* Goal: @join resource Join_resource (resource_at w loc) (resource_at w loc) (resource_at w loc) *)
(* Goal: @join ghost ghost_join (ghost_of w1) (ghost_of w2) (ghost_of w) *)
  apply identity_unit' in H0. apply H0.
(* Goal: @identity resource Join_resource (resource_at w l) *)
  rewrite Hg1, Hg2; apply identity_unit'; auto.
 +
(* Goal: @app_pred rmap ag_rmap (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun loc : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) sh2 loc) noat)) noghost) w2 *)
   split.
(* Goal: @eq resource (slice_resource sh2 (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt)))) (YES sh2 rsh2 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt))) *)
   intro loc; hnf. simpl. rewrite H2.
(* Goal: if adr_range_dec a (size_chunk ch) loc then @ex (readable_share sh2) (fun rsh : readable_share sh2 => @eq resource (if adr_range_dec a (size_chunk ch) loc then slice_resource sh2 (resource_at w loc) else resource_at w loc) (YES sh2 rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt)))) else @identity resource Join_resource (if adr_range_dec a (size_chunk ch) loc then slice_resource sh2 (resource_at w loc) else resource_at w loc) *)
(* Goal: @app_pred rmap ag_rmap noghost w2 *)
  clear dependent w1. clear dependent w2.
(* Goal: if adr_range_dec a (size_chunk ch) loc then @ex (readable_share sh2) (fun rsh : readable_share sh2 => @eq resource (if adr_range_dec a (size_chunk ch) loc then slice_resource sh2 (resource_at w loc) else resource_at w loc) (YES sh2 rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt)))) else @identity resource Join_resource (if adr_range_dec a (size_chunk ch) loc then slice_resource sh2 (resource_at w loc) else resource_at w loc) *)
(* Goal: @app_pred rmap ag_rmap noghost w2 *)
  specialize (H0 loc). hnf in H0.  
(* Goal: if adr_range_dec a (size_chunk ch) loc then @ex (readable_share sh2) (fun rsh : readable_share sh2 => @eq resource (if adr_range_dec a (size_chunk ch) loc then slice_resource sh2 (resource_at w loc) else resource_at w loc) (YES sh2 rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt)))) else @identity resource Join_resource (if adr_range_dec a (size_chunk ch) loc then slice_resource sh2 (resource_at w loc) else resource_at w loc) *)
(* Goal: @app_pred rmap ag_rmap noghost w2 *)
  if_tac in H0.
  -
(* Goal: and (@eq (option share) (resource_share (slice_resource sh1 (resource_at w loc))) (@Some share sh1)) (nonlock (slice_resource sh1 (resource_at w loc))) *)
   destruct H0. proof_irr. rewrite H0.
(* Goal: and (@eq (option share) (resource_share (slice_resource sh1 (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (preds_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) NoneP)))) (@Some share sh1)) (nonlock (slice_resource sh1 (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (preds_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) NoneP)))) *)
   unfold slice_resource.
(* Goal: and (@eq (option share) (resource_share match readable_share_dec sh1 with | left r1 => YES sh1 r1 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (preds_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) NoneP) | right n => NO sh1 n end) (@Some share sh1)) (nonlock match readable_share_dec sh1 with | left r1 => YES sh1 r1 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (preds_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) NoneP) | right n => NO sh1 n end) *)
   destruct (readable_share_dec sh1).
(* Goal: @eq resource (slice_resource sh2 (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt)))) (YES sh2 rsh2 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt))) *)
   simpl. split; auto.
(* Goal: @identity resource Join_resource (resource_at w l) *)
   split; simpl; auto.
  -
(* Goal: @identity resource Join_resource (resource_at w loc) *)
   apply H0.
(* Goal: @identity resource Join_resource (resource_at w l) *)
  - simpl; rewrite Hg1; auto.
(* Goal: @app_pred rmap ag_rmap (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun loc : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) sh2 loc) noat)) noghost) w2 *)
 + split.
(* Goal: @eq resource (slice_resource sh2 (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt)))) (YES sh2 rsh2 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt))) *)
   intro loc; hnf. simpl. rewrite H4.  simpl.
(* Goal: if adr_range_dec a (size_chunk ch) loc then @ex (readable_share sh2) (fun rsh : readable_share sh2 => @eq resource (if adr_range_dec a (size_chunk ch) loc then slice_resource sh2 (resource_at w loc) else resource_at w loc) (YES sh2 rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt)))) else @identity resource Join_resource (if adr_range_dec a (size_chunk ch) loc then slice_resource sh2 (resource_at w loc) else resource_at w loc) *)
(* Goal: @app_pred rmap ag_rmap noghost w2 *)
  clear dependent w1. clear dependent w2.
(* Goal: if adr_range_dec a (size_chunk ch) loc then @ex (readable_share sh2) (fun rsh : readable_share sh2 => @eq resource (if adr_range_dec a (size_chunk ch) loc then slice_resource sh2 (resource_at w loc) else resource_at w loc) (YES sh2 rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt)))) else @identity resource Join_resource (if adr_range_dec a (size_chunk ch) loc then slice_resource sh2 (resource_at w loc) else resource_at w loc) *)
(* Goal: @app_pred rmap ag_rmap noghost w2 *)
  specialize (H0 loc). hnf in H0.  
(* Goal: if adr_range_dec a (size_chunk ch) loc then @ex (readable_share sh2) (fun rsh : readable_share sh2 => @eq resource (if adr_range_dec a (size_chunk ch) loc then slice_resource sh2 (resource_at w loc) else resource_at w loc) (YES sh2 rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt)))) else @identity resource Join_resource (if adr_range_dec a (size_chunk ch) loc then slice_resource sh2 (resource_at w loc) else resource_at w loc) *)
(* Goal: @app_pred rmap ag_rmap noghost w2 *)
  if_tac in H0.
  -
(* Goal: @ex (readable_share sh2) (fun rsh : readable_share sh2 => @eq resource (slice_resource sh2 (resource_at w loc)) (YES sh2 rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt)))) *)
   exists rsh2.
(* Goal: @eq resource (slice_resource sh2 (resource_at w loc)) (YES sh2 rsh2 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt))) *)
   destruct H0 as [p0 H0]. proof_irr. simpl in H0.
(* Goal: @eq resource (slice_resource sh2 (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt)))) (YES sh2 rsh2 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt))) *)
   rewrite H0. clear H0. simpl.
(* Goal: @eq resource (YES sh2 r (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt))) (YES sh2 rsh2 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt))) *)
   destruct (readable_share_dec sh2); [ | contradiction]. proof_irr.
(* Goal: @eq Prop (@app_pred rmap ag_rmap (yesat (SomeP rmaps.Mpred (fun _ : list Type => R)) (LK lock_size (Z.sub (@snd block Z l0) (@snd block Z l))) sh l0) w) (@ex (readable_share sh) (fun p : readable_share sh => @eq resource (resource_at w l0) (YES sh p (LK lock_size (Z.sub (@snd block Z l0) (@snd block Z l))) (SomeP rmaps.Mpred (fun _ : list Type => approx (@level rmap ag_rmap w) R))))) *)
   reflexivity.
 - apply H0.
(* Goal: @identity resource Join_resource (resource_at w l) *)
 - simpl; rewrite Hg2; auto.
Qed.

Lemma VALspec_range_share_join:
 forall sh1 sh2 sh n p,
  readable_share sh1 ->
  readable_share sh2 ->
  join sh1 sh2 sh ->
  VALspec_range n sh1 p *
  VALspec_range n sh2 p =
  VALspec_range n sh p.
Proof.
(* Goal: forall (l : AV.address) (_ : not (adr_range a (size_chunk ch) l)), @identity resource Join_resource (resource_at w l) *)
(* Goal: @app_pred rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun i : address => @andp rmap ag_rmap (shareat i sh1) (nonlockat i)) noat)) noghost) (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun loc : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) sh2 loc) noat)) noghost)) w *)
  intros.
(* Goal: @eq Share.t sh' (retainer_part sh') *)
  symmetry.
(* Goal: @app_pred rmap ag_rmap (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun loc : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) sh2 loc) noat)) noghost) w2 *)
  apply allp_jam_share_split.
  do 3 eexists.
  exists sh, sh1, sh2. 
  split; [| split; [| split; [| split; [| split]]]].
  + apply is_resource_pred_YES_VAL.
  + apply is_resource_pred_YES_VAL.
  + apply is_resource_pred_YES_VAL.
(* Goal: @identity resource Join_resource (resource_at w l) *)
  + auto.
(* Goal: forall (l : AV.address) (_ : not (adr_range a (size_chunk ch) l)), @identity resource Join_resource (resource_at w l) *)
(* Goal: @app_pred rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun i : address => @andp rmap ag_rmap (shareat i sh1) (nonlockat i)) noat)) noghost) (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun loc : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) sh2 loc) noat)) noghost)) w *)
  + simpl; intros.
    destruct H2 as [x [rsh ?]].
    split; [subst; simpl; auto |].
    split; [exists x, H | exists x, H0].
(* Goal: @eq resource (slice_resource sh2 (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt)))) (YES sh2 rsh2 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt))) *)
    - subst. simpl.
(* Goal: @eq resource match readable_share_dec sh1 with | left r1 => YES sh1 r1 k0 (SomeP A _f) | right n => NO sh1 n end (YES sh1 rsh1 k0 (preds_fmap (approx (@level rmap ag_rmap f)) (approx (@level rmap ag_rmap f)) pp)) *)
(* Goal: @eq resource (resource_at f l') (YES sh1 rsh1 k (preds_fmap (approx (@level rmap ag_rmap f)) (approx (@level rmap ag_rmap f)) pp)) *)
(* Goal: @identity resource Join_resource (resource_at f l') *)
      destruct (readable_share_dec sh1); [ | contradiction].
(* Goal: @eq resource (YES sh rsh3 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z b) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt))) (YES sh p8 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z b) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt))) *)
      f_equal. apply proof_irr.
(* Goal: @eq resource (slice_resource sh2 (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt)))) (YES sh2 rsh2 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt))) *)
    - subst. simpl.
(* Goal: @eq resource match readable_share_dec sh2 with | left r1 => YES sh2 r1 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt)) | right n => NO sh2 n end (YES sh2 rsh2 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt))) *)
      destruct (readable_share_dec sh2); [ | contradiction].
(* Goal: @eq resource (YES sh rsh3 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z b) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt))) (YES sh p8 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z b) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt))) *)
      f_equal. apply proof_irr.
(* Goal: forall (l : AV.address) (_ : not (adr_range a (size_chunk ch) l)), @identity resource Join_resource (resource_at w l) *)
(* Goal: @app_pred rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun i : address => @andp rmap ag_rmap (shareat i sh1) (nonlockat i)) noat)) noghost) (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun loc : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) sh2 loc) noat)) noghost)) w *)
  + simpl; intros.
    destruct H3 as [? [? ?]], H4 as [? [? ?]].
    exists x. exists (join_readable1 H1 H).
(* Goal: @identity share Share.Join_ba (Share.glb Share.Rsh (Share.lub (@snd Share.t Share.t (Share.split (Share.glb Share.Lsh sh))) b)) *)
    subst.
(* Goal: @identity resource Join_resource (resource_at w l) *)
    inv H2. apply YES_ext. eapply join_eq; eauto.
Qed.

Lemma nonlock_permission_bytes_share_join:
 forall sh1 sh2 sh a n,
  join sh1 sh2 sh ->
  nonlock_permission_bytes sh1 a n *
  nonlock_permission_bytes sh2 a n =
  nonlock_permission_bytes sh a n.
Proof.
(* Goal: forall (l : AV.address) (_ : not (adr_range a (size_chunk ch) l)), @identity resource Join_resource (resource_at w l) *)
(* Goal: @app_pred rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun i : address => @andp rmap ag_rmap (shareat i sh1) (nonlockat i)) noat)) noghost) (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun loc : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) sh2 loc) noat)) noghost)) w *)
  intros.
(* Goal: @eq Share.t sh' (retainer_part sh') *)
  symmetry.
(* Goal: @app_pred rmap ag_rmap (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun loc : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) sh2 loc) noat)) noghost) w2 *)
  apply allp_jam_share_split.
  do 3 eexists.
  exists sh, sh1, sh2.
  split; [| split; [| split; [| split; [| split]]]].
  + apply is_resource_pred_nonlock_shareat.
  + apply is_resource_pred_nonlock_shareat.
  + apply is_resource_pred_nonlock_shareat.
(* Goal: @identity resource Join_resource (resource_at w l) *)
  + auto.
(* Goal: forall (l : AV.address) (_ : not (adr_range a (size_chunk ch) l)), @identity resource Join_resource (resource_at w l) *)
(* Goal: @app_pred rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun i : address => @andp rmap ag_rmap (shareat i sh1) (nonlockat i)) noat)) noghost) (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun loc : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) sh2 loc) noat)) noghost)) w *)
  + simpl; intros.
(* Goal: and (@eq (option share) (resource_share (slice_resource sh1 (resource_at w loc))) (@Some share sh1)) (nonlock (slice_resource sh1 (resource_at w loc))) *)
    destruct H0.
    split; [auto |].
(* Goal: @app_pred rmap ag_rmap (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun loc : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) sh2 loc) noat)) noghost) w2 *)
    split; split.
    - eapply slice_resource_resource_share; [eauto | eexists; eauto ].
    - eapply slice_resource_nonlock; [eauto | eexists; eauto | auto].
    - eapply slice_resource_resource_share; [eauto | eexists; eapply join_comm; eauto].
    - eapply slice_resource_nonlock; [eauto | eexists; eapply join_comm; eauto | auto].
(* Goal: forall (l : AV.address) (_ : not (adr_range a (size_chunk ch) l)), @identity resource Join_resource (resource_at w l) *)
(* Goal: @app_pred rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun i : address => @andp rmap ag_rmap (shareat i sh1) (nonlockat i)) noat)) noghost) (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun loc : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) sh2 loc) noat)) noghost)) w *)
  + simpl; intros.
    destruct H1, H2.
(* Goal: @app_pred rmap ag_rmap (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun loc : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) sh2 loc) noat)) noghost) w2 *)
    split.
(* Goal: @identity resource Join_resource (resource_at w l) *)
    - eapply (resource_share_join q_res r_res); eauto.
(* Goal: @identity resource Join_resource (resource_at w l) *)
    - eapply (nonlock_join q_res r_res); eauto.
Qed.

Lemma nonlock_permission_bytes_VALspec_range_join:
 forall sh1 sh2 (rsh2: readable_share sh2) sh p n,
  join sh1 sh2 sh ->
  nonlock_permission_bytes sh1 p n *
  VALspec_range n sh2 p =
  VALspec_range n sh p.
Proof.
(* Goal: forall (l : AV.address) (_ : not (adr_range a (size_chunk ch) l)), @identity resource Join_resource (resource_at w l) *)
(* Goal: @app_pred rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun i : address => @andp rmap ag_rmap (shareat i sh1) (nonlockat i)) noat)) noghost) (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun loc : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) sh2 loc) noat)) noghost)) w *)
  intros.
(* Goal: @eq Share.t sh' (retainer_part sh') *)
  symmetry.
(* Goal: @app_pred rmap ag_rmap (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun loc : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) sh2 loc) noat)) noghost) w2 *)
  apply allp_jam_share_split.
  do 3 eexists.
  exists sh, sh1, sh2.
  split; [| split; [| split; [| split; [| split]]]].
  + apply is_resource_pred_YES_VAL.
  + apply is_resource_pred_nonlock_shareat.
  + apply is_resource_pred_YES_VAL.
(* Goal: @identity resource Join_resource (resource_at w l) *)
  + auto.
(* Goal: forall (l : AV.address) (_ : not (adr_range a (size_chunk ch) l)), @identity resource Join_resource (resource_at w l) *)
(* Goal: @app_pred rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun i : address => @andp rmap ag_rmap (shareat i sh1) (nonlockat i)) noat)) noghost) (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun loc : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) sh2 loc) noat)) noghost)) w *)
  + simpl; intros.
    destruct H0 as [? [? ?]]; subst; split; [| split; [split |]].
(* Goal: @identity resource Join_resource (resource_at w l) *)
    - simpl; auto.
(* Goal: @eq resource (slice_resource sh2 (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt)))) (YES sh2 rsh2 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt))) *)
    - simpl.
(* Goal: @eq Prop (@app_pred rmap ag_rmap (yesat (SomeP rmaps.Mpred (fun _ : list Type => R)) (LK lock_size (Z.sub (@snd block Z l0) (@snd block Z l))) sh l0) w) (@ex (readable_share sh) (fun p : readable_share sh => @eq resource (resource_at w l0) (YES sh p (LK lock_size (Z.sub (@snd block Z l0) (@snd block Z l))) (SomeP rmaps.Mpred (fun _ : list Type => approx (@level rmap ag_rmap w) R))))) *)
      destruct (readable_share_dec sh1); reflexivity.
(* Goal: @eq resource (slice_resource sh2 (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt)))) (YES sh2 rsh2 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt))) *)
    - simpl.
(* Goal: @identity resource Join_resource (resource_at w l) *)
      destruct (readable_share_dec sh1); simpl; auto.
(* Goal: @eq resource (slice_resource sh2 (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt)))) (YES sh2 rsh2 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt))) *)
    - simpl.
      exists x, rsh2.
(* Goal: @eq resource match readable_share_dec sh2 with | left r1 => YES sh2 r1 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt)) | right n => NO sh2 n end (YES sh2 rsh2 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt))) *)
      destruct (readable_share_dec sh2); [ | contradiction].
(* Goal: @identity resource Join_resource (resource_at w l) *)
      apply YES_ext. auto.
(* Goal: forall (l : AV.address) (_ : not (adr_range a (size_chunk ch) l)), @identity resource Join_resource (resource_at w l) *)
(* Goal: @app_pred rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun i : address => @andp rmap ag_rmap (shareat i sh1) (nonlockat i)) noat)) noghost) (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun loc : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) sh2 loc) noat)) noghost)) w *)
  + simpl; intros.
    destruct H2 as [? [? ?]].
(* Goal: @identity share Share.Join_ba (Share.glb Share.Rsh (Share.lub (@snd Share.t Share.t (Share.split (Share.glb Share.Lsh sh))) b)) *)
    subst. proof_irr.
    exists x, (join_readable2 H rsh2).
(* Goal: @join Share.t Share.Join_ba (Share.lub a e) (Share.lub b f) sh *)
    destruct H1.
    destruct q_res; simpl in H1.
(* Goal: @identity share Share.Join_ba (Share.glb Share.Rsh (Share.lub (@snd Share.t Share.t (Share.split (Share.glb Share.Lsh sh))) b)) *)
    - inversion H0; subst. inv H1.
      apply YES_ext.
(* Goal: @identity resource Join_resource (resource_at w l) *)
      eapply join_eq; eauto.
(* Goal: @identity resource Join_resource (resource_at w l) *)
    - inv H1. inv H0. apply YES_ext. eapply join_eq; eauto.
    - inv H1.
Qed.

Lemma is_resource_pred_YES_LK lock_size (l: address) (R: pred rmap) sh:
  is_resource_pred
    (fun l' => yesat (SomeP rmaps.Mpred (fun _ => R)) (LK lock_size (snd l' - snd l)) sh l')
    (fun r (l': address) n => exists p, r = YES sh p (LK lock_size (snd l' - snd l))
        (SomeP rmaps.Mpred (fun _ => approx n R))).
(* Goal: forall (l : AV.address) (_ : not (adr_range a (size_chunk ch) l)), @identity resource Join_resource (resource_at w l) *)
(* Goal: @app_pred rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun i : address => @andp rmap ag_rmap (shareat i sh1) (nonlockat i)) noat)) noghost) (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun loc : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) sh2 loc) noat)) noghost)) w *)
Proof. hnf; intros. reflexivity. Qed.

Lemma LKspec_share_join lock_size:
 forall sh1 sh2 (rsh1: readable_share sh1) (rsh2: readable_share sh2) sh R p,
  join sh1 sh2 sh ->
  LKspec lock_size R sh1 p *
  LKspec lock_size R sh2 p =
  LKspec lock_size R sh p.
Proof.
(* Goal: forall (l : AV.address) (_ : not (adr_range a (size_chunk ch) l)), @identity resource Join_resource (resource_at w l) *)
(* Goal: @app_pred rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun i : address => @andp rmap ag_rmap (shareat i sh1) (nonlockat i)) noat)) noghost) (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun loc : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) sh2 loc) noat)) noghost)) w *)
  intros.
(* Goal: @eq Share.t sh' (retainer_part sh') *)
  symmetry.
  unfold LKspec.
(* Goal: @app_pred rmap ag_rmap (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun loc : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) sh2 loc) noat)) noghost) w2 *)
  apply allp_jam_share_split.
  do 3 eexists.
  exists sh, sh1, sh2.
  split; [| split; [| split; [| split; [| split]]]].
  + apply is_resource_pred_YES_LK.
  + apply is_resource_pred_YES_LK.
  + apply is_resource_pred_YES_LK.
(* Goal: @identity resource Join_resource (resource_at w l) *)
  + auto.
(* Goal: forall (l : AV.address) (_ : not (adr_range a (size_chunk ch) l)), @identity resource Join_resource (resource_at w l) *)
(* Goal: @app_pred rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun i : address => @andp rmap ag_rmap (shareat i sh1) (nonlockat i)) noat)) noghost) (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun loc : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) sh2 loc) noat)) noghost)) w *)
  + simpl; intros.
    destruct (eq_dec p l); subst; destruct H0; split; try solve [subst; simpl; auto];
(* Goal: @app_pred rmap ag_rmap (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun loc : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) sh2 loc) noat)) noghost) w2 *)
    split.
(* Goal: @eq resource (slice_resource sh2 (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt)))) (YES sh2 rsh2 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt))) *)
    - exists rsh1. subst. simpl.
(* Goal: @eq resource match readable_share_dec sh1 with | left r1 => YES sh1 r1 k0 (SomeP A _f) | right n => NO sh1 n end (YES sh1 rsh1 k0 (preds_fmap (approx (@level rmap ag_rmap f)) (approx (@level rmap ag_rmap f)) pp)) *)
(* Goal: @eq resource (resource_at f l') (YES sh1 rsh1 k (preds_fmap (approx (@level rmap ag_rmap f)) (approx (@level rmap ag_rmap f)) pp)) *)
(* Goal: @identity resource Join_resource (resource_at f l') *)
      destruct (readable_share_dec sh1); [ | contradiction].
(* Goal: @identity resource Join_resource (resource_at w l) *)
      apply YES_ext; auto.
(* Goal: @eq resource (slice_resource sh2 (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt)))) (YES sh2 rsh2 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt))) *)
    - exists rsh2. subst. simpl.
(* Goal: @eq resource match readable_share_dec sh2 with | left r1 => YES sh2 r1 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt)) | right n => NO sh2 n end (YES sh2 rsh2 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt))) *)
      destruct (readable_share_dec sh2); [ | contradiction].
(* Goal: @identity resource Join_resource (resource_at w l) *)
      apply YES_ext; auto.
(* Goal: @eq resource (slice_resource sh2 (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt)))) (YES sh2 rsh2 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt))) *)
    - exists rsh1. subst. simpl.
(* Goal: @eq resource match readable_share_dec sh1 with | left r1 => YES sh1 r1 k0 (SomeP A _f) | right n => NO sh1 n end (YES sh1 rsh1 k0 (preds_fmap (approx (@level rmap ag_rmap f)) (approx (@level rmap ag_rmap f)) pp)) *)
(* Goal: @eq resource (resource_at f l') (YES sh1 rsh1 k (preds_fmap (approx (@level rmap ag_rmap f)) (approx (@level rmap ag_rmap f)) pp)) *)
(* Goal: @identity resource Join_resource (resource_at f l') *)
      destruct (readable_share_dec sh1); [ | contradiction].
(* Goal: @identity resource Join_resource (resource_at w l) *)
      apply YES_ext; auto.
(* Goal: @eq resource (slice_resource sh2 (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt)))) (YES sh2 rsh2 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt))) *)
    - exists rsh2. subst. simpl.
(* Goal: @eq resource match readable_share_dec sh2 with | left r1 => YES sh2 r1 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt)) | right n => NO sh2 n end (YES sh2 rsh2 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) (SomeP (rmaps.ConstType unit) (fun _ : list Type => tt))) *)
      destruct (readable_share_dec sh2); [ | contradiction].
(* Goal: @identity resource Join_resource (resource_at w l) *)
      apply YES_ext; auto.
(* Goal: forall (l : AV.address) (_ : not (adr_range a (size_chunk ch) l)), @identity resource Join_resource (resource_at w l) *)
(* Goal: @app_pred rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun i : address => @andp rmap ag_rmap (shareat i sh1) (nonlockat i)) noat)) noghost) (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk ch)) (adr_range_dec a (size_chunk ch)) (fun loc : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) sh2 loc) noat)) noghost)) w *)
  + simpl; intros.
    destruct (eq_dec p l); subst; destruct H1, H2. repeat proof_irr.
(* Goal: @identity share Share.Join_ba (Share.glb Share.Rsh (Share.lub (@snd Share.t Share.t (Share.split (Share.glb Share.Lsh sh))) b)) *)
    - exists (join_readable1 H rsh1). subst. inv H0. apply YES_ext.
(* Goal: @identity resource Join_resource (resource_at w l) *)
      eapply join_eq; eauto.
(* Goal: @identity share Share.Join_ba (Share.glb Share.Rsh (Share.lub (@snd Share.t Share.t (Share.split (Share.glb Share.Lsh sh))) b)) *)
    - exists (join_readable1 H rsh1). subst. inv H0. apply YES_ext.
(* Goal: @identity resource Join_resource (resource_at w l) *)
      eapply join_eq; eauto.
Qed.