Require Import VST.msl.msl_standard.
Require Import VST.msl.cjoins.
Require Import VST.msl.Coqlib2.
Require Import VST.msl.sepalg_list.
Require Import VST.veric.shares.
Require Import VST.veric.rmaps.

Module Rmaps_Lemmas (R0: RMAPS).
Module R := R0.
Import R.

Hint Resolve (@subp_sepcon _ Join_rmap Perm_rmap Sep_rmap): contractive.

 Lemma approx_p  : forall (p:pred rmap) n w, approx n p w -> p w.
(* Goal: forall (p : @pred rmap ag_rmap) (n : nat) (w : rmap) (_ : lt (@level rmap ag_rmap w) n) (_ : @app_pred rmap ag_rmap p w), @app_pred rmap ag_rmap (approx n p) w *)
 Proof. unfold approx; simpl; intuition. Qed.

 Lemma approx_lt : forall (p:pred rmap) n w, lt (level w) n -> p w -> approx n p w.
(* Goal: forall (p : @pred rmap ag_rmap) (n : nat) (w : rmap) (_ : lt (@level rmap ag_rmap w) n) (_ : @app_pred rmap ag_rmap p w), @app_pred rmap ag_rmap (approx n p) w *)
 Proof. unfold approx; simpl; intuition. Qed.

 Lemma approx_ge : forall p n w, ge (level w) n -> approx n p w -> False.
 Proof. unfold approx; intros. destruct H0; auto. omega. Qed.

  Lemma ageN_level : forall n (phi1 phi2 : rmap),
    ageN n phi1 = Some phi2 -> level phi1 = (n + (level phi2))%nat.
  Proof.
(* Goal: forall (n : nat) (phi1 phi2 : rmap) (_ : @eq (option rmap) (@ageN rmap ag_rmap n phi1) (@Some rmap phi2)), @eq nat (@level rmap ag_rmap phi1) (Init.Nat.add n (@level rmap ag_rmap phi2)) *)
    unfold ageN; induction n; simpl; intros.
(* Goal: @eq nat (@level rmap ag_rmap phi1) (@level rmap ag_rmap phi2) *)
(* Goal: @eq nat (@level rmap ag_rmap phi1) (S (Init.Nat.add n (@level rmap ag_rmap phi2))) *)
    injection H; intros; subst; auto.
(* Goal: @eq nat (@level rmap ag_rmap phi1) (S (Init.Nat.add n (@level rmap ag_rmap phi2))) *)
    revert H.
(* Goal: forall _ : @eq (option rmap) match @age1 rmap ag_rmap phi1 with | Some w' => @composeOptN rmap (@age1 rmap ag_rmap) n w' | None => @None rmap end (@Some rmap phi2), @eq nat (@level rmap ag_rmap phi1) (S (Init.Nat.add n (@level rmap ag_rmap phi2))) *)
    repeat rewrite rmap_level_eq in *.
(* Goal: forall (w : rmap) (loc : AV.address), @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (@core resource Join_resource Sep_resource (resource_at w loc))) (@core resource Join_resource Sep_resource (resource_at w loc)) *)
    intros. invSome.
(* Goal: @eq nat (@fst nat rmap' (unsquash phi1)) (S (Init.Nat.add n (@fst nat rmap' (unsquash phi2)))) *)
    specialize (IHn _ _ H2).
(* Goal: @eq nat (@level rmap ag_rmap m) (Init.Nat.add (S (Init.Nat.sub (@level rmap ag_rmap m) (S (@level rmap ag_rmap m')))) (@level rmap ag_rmap m')) *)
(* Goal: @ex rmap (fun m1 : rmap => and (@laterR rmap ag_rmap m m1) (@eq nat (@level rmap ag_rmap m1) (@level rmap ag_rmap m'))) *)
    apply  age_level in H.  rewrite rmap_level_eq in *. omega.
  Qed.

Lemma NO_identity: forall nsh, identity (NO Share.bot nsh).
Proof.
(* Goal: forall (w : rmap) (loc : AV.address), @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (@core resource Join_resource Sep_resource (resource_at w loc))) (@core resource Join_resource Sep_resource (resource_at w loc)) *)
  unfold identity; intros.
  inv H;
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
  apply join_unit1_e in RJ; auto;   subst sh3; repeat proof_irr; auto.
Qed.

Lemma PURE_identity: forall k pds, identity (PURE k pds).
Proof.
(* Goal: forall (w : rmap) (loc : AV.address), @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (@core resource Join_resource Sep_resource (resource_at w loc))) (@core resource Join_resource Sep_resource (resource_at w loc)) *)
  unfold identity; intros.
(* Goal: @eq resource (@core resource Join_resource Sep_resource (PURE k pp)) (PURE k pp) *)
  inv H; auto.
Qed.

Lemma identity_NO:
  forall r, identity  r -> r = NO Share.bot bot_unreadable \/ exists k, exists pds, r = PURE k pds.
Proof.
(* Goal: forall (w : rmap) (loc : AV.address), @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (@core resource Join_resource Sep_resource (resource_at w loc))) (@core resource Join_resource Sep_resource (resource_at w loc)) *)
  destruct r; auto; intros.
 * left.
(* Goal: @identity Share.t Share.Join_ba sh *)
   apply identity_unit' in H. inv H.
(* Goal: @eq resource (NO sh n) (NO Share.bot bot_unreadable) *)
(* Goal: or (@eq resource (YES sh r k p) (NO Share.bot bot_unreadable)) (@ex AV.kind (fun k0 : AV.kind => @ex preds (fun pds : preds => @eq resource (YES sh r k p) (PURE k0 pds)))) *)
(* Goal: or (@eq resource (PURE k p) (NO Share.bot bot_unreadable)) (@ex AV.kind (fun k0 : AV.kind => @ex preds (fun pds : preds => @eq resource (PURE k p) (PURE k0 pds)))) *)
   apply identity_unit_equiv in RJ. apply identity_share_bot in RJ. subst.
(* Goal: @eq resource (NO Share.bot nsh1) (NO Share.bot bot_unreadable) *)
   f_equal. apply proof_irr.
 * apply identity_unit' in H. inv H.
(* Goal: @eq resource (NO sh1 nsh1) (NO Share.bot bot_unreadable) *)
   apply unit_identity in RJ. apply identity_share_bot in RJ. subst.
(* Goal: or (@eq resource (YES Share.bot r k p) (NO Share.bot bot_unreadable)) (@ex AV.kind (fun k0 : AV.kind => @ex preds (fun pds : preds => @eq resource (YES Share.bot r k p) (PURE k0 pds)))) *)
   contradiction bot_unreadable.
 * right. exists k. exists p. trivial.
Qed.

Lemma age1_resource_at_identity:
  forall phi phi' loc, age1 phi = Some phi' ->
               (identity (phi@loc) <-> identity (phi'@loc)).
Proof.
(* Goal: iff (@identity resource Join_resource (NO sh n)) (@identity Share.t Share.Join_ba sh) *)
 split; intro.
 (* FORWARD DIRECTION *)
(* Goal: @identity resource Join_resource (resource_at phi loc) *)
  generalize (identity_NO _ H0); clear H0; intro.
  unfold resource_at in *.
  rewrite rmap_age1_eq in *.
(* Goal: forall (w : rmap) (loc : AV.address), @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (@core resource Join_resource Sep_resource (resource_at w loc))) (@core resource Join_resource Sep_resource (resource_at w loc)) *)
  revert H H0; case_eq (unsquash phi); simpl; intros.
(* Goal: @eq ghost (@snd (forall _ : AV.address, resource) ghost (@snd nat rmap' (unsquash phi'))) (ghost_fmap (approx (@fst nat rmap' (unsquash phi'))) (approx (@fst nat rmap' (unsquash phi'))) (@snd (forall _ : AV.address, resource) ghost r)) *)
  destruct n; inv H0.
(* Goal: @eq (prod nat rmap') (unsquash (squash (@pair nat rmap' n (rmap_fmap (approx (S n)) (approx (S n)) r0)))) (@pair nat rmap' n r0) *)
  rewrite unsquash_squash.
(* Goal: not (@identity share Share.Join_ba (Share.glb Share.Rsh (Share.lub a' (Share.glb Share.Rsh b)))) *)
  simpl.
  destruct r. simpl in *.
(* Goal: not (@identity share Share.Join_ba (Share.glb Share.Rsh (Share.lub a' (Share.glb Share.Rsh b)))) *)
  unfold compose; simpl. destruct H1 as [H1 | [k [pds H1]]]; rewrite H1; simpl; auto.
(* Goal: @identity resource Join_resource (NO Share.bot bot_unreadable) *)
(* Goal: @identity resource Join_resource (PURE k (preds_fmap (approx n) (approx n) pds)) *)
(* Goal: @identity resource Join_resource (resource_at phi loc) *)
  apply NO_identity.
(* Goal: @identity resource Join_resource (PURE k p) *)
  apply PURE_identity.
 (* BACKWARD DIRECTION *)
(* Goal: @identity resource Join_resource (resource_at phi loc) *)
  generalize (identity_NO _ H0); clear H0; intro.
  unfold resource_at in *. simpl in H.
(* Goal: @identity resource Join_resource (@fst (forall _ : AV.address, resource) ghost (@snd nat rmap' (unsquash phi)) loc) *)
  rewrite rmap_age1_eq in H.
(* Goal: forall (w : rmap) (loc : AV.address), @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (@core resource Join_resource Sep_resource (resource_at w loc))) (@core resource Join_resource Sep_resource (resource_at w loc)) *)
  revert H H0; case_eq (unsquash phi); simpl; intros.
(* Goal: @eq ghost (@snd (forall _ : AV.address, resource) ghost (@snd nat rmap' (unsquash phi'))) (ghost_fmap (approx (@fst nat rmap' (unsquash phi'))) (approx (@fst nat rmap' (unsquash phi'))) (@snd (forall _ : AV.address, resource) ghost r)) *)
  destruct n; inv H0.
  rewrite unsquash_squash in H1. simpl in *.
(* Goal: @identity resource Join_resource (@fst (forall _ : AV.address, resource) ghost r loc) *)
  unfold compose in H1; simpl in H1.
(* Goal: @identity resource Join_resource (@fst (forall _ : AV.address, resource) ghost r loc) *)
  unfold resource_fmap in H1.
(* Goal: @identity resource Join_resource (@fst (forall _ : AV.address, resource) ghost r loc) *)
  destruct (fst r loc).
(* Goal: @identity resource Join_resource (NO Share.bot bot_unreadable) *)
(* Goal: @identity resource Join_resource (PURE k (preds_fmap (approx n) (approx n) pds)) *)
(* Goal: @identity resource Join_resource (resource_at phi loc) *)
  destruct H1. inv H0;   apply NO_identity. destruct H0 as [? [? H0]]; inv H0.
(* Goal: @identity resource Join_resource (YES sh r0 k p) *)
(* Goal: @identity resource Join_resource (PURE k p) *)
  destruct H1 as [H1 | [k' [pds' H1]]]; inv H1.
(* Goal: @identity resource Join_resource (PURE k p) *)
  apply PURE_identity.
Qed.

Lemma necR_resource_at_identity:
  forall phi phi' loc, necR phi phi' ->
         identity (phi@loc) ->
         identity (phi'@loc).
Proof.
(* Goal: forall (phi phi' : rmap) (loc : AV.address) (_ : @necR rmap ag_rmap phi phi') (_ : @identity resource Join_resource (resource_at phi loc)), @identity resource Join_resource (resource_at phi' loc) *)
  induction 1; auto.
(* Goal: not (@identity resource Join_resource (YES sh rsh k Q)) *)
  intro.
(* Goal: @identity resource Join_resource (resource_at y loc) *)
 apply -> (age1_resource_at_identity _ _ loc H); auto.
Qed.

Lemma make_rmap': forall f g, 
          exists phi: rmap', phi = (f, g).
Proof.
(* Goal: forall (w : rmap) (loc : AV.address), @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (@core resource Join_resource Sep_resource (resource_at w loc))) (@core resource Join_resource Sep_resource (resource_at w loc)) *)
  intros.
(* Goal: @ex rmap' (fun phi : rmap' => @eq rmap' phi (@pair (forall _ : AV.address, resource) ghost f g)) *)
  unfold rmap'. exists (f,g).
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
  auto.
Qed.


Lemma make_rmap (f: AV.address -> resource) g
    (n: nat) (H: resource_fmap (approx n) (approx n) oo f = f)
    (HG: ghost_fmap (approx n) (approx n) g = g) :
  {phi: rmap | level phi = n /\ resource_at phi = f /\ ghost_of phi = g}.
Proof.
(* Goal: forall (w : rmap) (loc : AV.address), @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (@core resource Join_resource Sep_resource (resource_at w loc))) (@core resource Join_resource Sep_resource (resource_at w loc)) *)
intros.
(* Goal: @sig rmap (fun phi : rmap => and (@eq nat (@level rmap ag_rmap phi) n) (and (@eq (forall _ : AV.address, resource) (resource_at phi) f) (@eq ghost (ghost_of phi) g))) *)
apply (exist _ (squash (n, (f, g)))).
simpl level; rewrite rmap_level_eq in *; unfold resource_at, ghost_of. rewrite unsquash_squash.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
auto.
Qed.

Lemma make_rmap'':
    forall n (f: AV.address -> resource) g,
      exists phi:rmap, level phi = n /\ resource_at phi = resource_fmap (approx n) (approx n) oo f /\
      ghost_of phi = ghost_fmap (approx n) (approx n) g.
  Proof.
(* Goal: forall (w : rmap) (loc : AV.address), @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (@core resource Join_resource Sep_resource (resource_at w loc))) (@core resource Join_resource Sep_resource (resource_at w loc)) *)
    intros.
(* Goal: @ex rmap (fun phi : rmap => and (@eq nat (@level rmap ag_rmap phi) n) (and (@eq (forall _ : AV.address, resource) (resource_at phi) (@compose AV.address resource resource (resource_fmap (approx n) (approx n)) f)) (@eq ghost (ghost_of phi) (ghost_fmap (approx n) (approx n) g)))) *)
    exists (squash (n, (f, g))).
(* Goal: @eq nat (@level rmap ag_rmap (empty_rmap lev)) lev *)
    rewrite rmap_level_eq.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
      unfold resource_at, ghost_of; rewrite unsquash_squash; simpl; split; auto.
Qed.

Lemma approx_oo_approx':
  forall n n', (n' >= n)%nat -> approx n oo approx n' = approx n.
Proof.
(* Goal: forall (w : rmap) (loc : AV.address), @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (@core resource Join_resource Sep_resource (resource_at w loc))) (@core resource Join_resource Sep_resource (resource_at w loc)) *)
unfold compose; intros.
(* Goal: @eq (forall _ : @pred rmap ag_rmap, @pred rmap ag_rmap) (fun x : @pred rmap ag_rmap => approx n' (approx n x)) (approx n) *)
extensionality P.
 apply pred_ext; intros w ?; unfold approx; simpl in *; intuition.
Qed.

Lemma approx'_oo_approx:
  forall n n', (n' >= n)%nat -> approx n' oo approx n = approx n.
Proof.
(* Goal: forall (w : rmap) (loc : AV.address), @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (@core resource Join_resource Sep_resource (resource_at w loc))) (@core resource Join_resource Sep_resource (resource_at w loc)) *)
unfold compose; intros.
(* Goal: @eq (forall _ : @pred rmap ag_rmap, @pred rmap ag_rmap) (fun x : @pred rmap ag_rmap => approx n' (approx n x)) (approx n) *)
extensionality P.
 apply pred_ext; intros w ?; unfold approx; simpl in *; intuition.
Qed.

Lemma approx_oo_approx: forall n, approx n oo approx n = approx n.
Proof.
(* Goal: @eq nat (@level rmap ag_rmap m) (Init.Nat.add (S (Init.Nat.sub (@level rmap ag_rmap m) (S (@level rmap ag_rmap m')))) (@level rmap ag_rmap m')) *)
(* Goal: @ex rmap (fun m1 : rmap => and (@laterR rmap ag_rmap m m1) (@eq nat (@level rmap ag_rmap m1) (@level rmap ag_rmap m'))) *)
intros; apply approx_oo_approx'; omega.
Qed.

Lemma preds_fmap_fmap:
  forall f1 f2 g1 g2 pp, preds_fmap f1 f2 (preds_fmap g1 g2 pp) = preds_fmap (f1 oo g1) (g2 oo f2) pp.
Proof.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
destruct pp; simpl; auto.
(* Goal: @eq preds (SomeP A (fun i : list Type => @fmap (dependent_type_functor_rec i A) (@pred rmap ag_rmap) (@pred rmap ag_rmap) f1 f2 (@fmap (dependent_type_functor_rec i A) (@pred rmap ag_rmap) (@pred rmap ag_rmap) g1 g2 (_f i)))) (SomeP A (fun i : list Type => @fmap (dependent_type_functor_rec i A) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) f1 g1) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) g2 f2) (_f i))) *)
f_equal; extensionality i.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
rewrite <- fmap_comp; auto.
Qed.

Lemma resources_same_level:
   forall f phi,
     (forall l : AV.address, join_sub (f l) (phi @ l)) ->
        resource_fmap (approx (level phi)) (approx (level phi)) oo f = f.
Proof.
(* Goal: forall (w : rmap) (loc : AV.address), @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (@core resource Join_resource Sep_resource (resource_at w loc))) (@core resource Join_resource Sep_resource (resource_at w loc)) *)
  intros.
(* Goal: @eq nat (@level rmap ag_rmap (empty_rmap lev)) lev *)
  rewrite rmap_level_eq.
  unfold resource_fmap, resource_at in *.
(* Goal: @eq (forall _ : AV.address, resource) (@compose AV.address resource resource (fun x : resource => match x with | NO sh nsh => NO sh nsh | YES sh rsh k p => YES sh rsh k (preds_fmap (approx (@fst nat rmap' (unsquash phi))) (approx (@fst nat rmap' (unsquash phi))) p) | PURE k p => PURE k (preds_fmap (approx (@fst nat rmap' (unsquash phi))) (approx (@fst nat rmap' (unsquash phi))) p) end) f) f *)
  unfold compose; extensionality l. specialize ( H l).
(* Goal: @eq resource match f l with | NO sh nsh => NO sh nsh | YES sh rsh k p => YES sh rsh k (preds_fmap (approx (@fst nat rmap' (unsquash phi))) (approx (@fst nat rmap' (unsquash phi))) p) | PURE k p => PURE k (preds_fmap (approx (@fst nat rmap' (unsquash phi))) (approx (@fst nat rmap' (unsquash phi))) p) end (f l) *)
  destruct H as [g ?].
(* Goal: @eq ghost (ghost_fmap (approx (@fst nat rmap' (unsquash phi))) (approx (@fst nat rmap' (unsquash phi))) g) g *)
  revert H; case_eq (unsquash phi); intros n ? ?.
(* Goal: forall _ : @join_sub ghost ghost_join g (@snd (forall _ : AV.address, resource) ghost (@snd nat rmap' (@pair nat rmap' n r))), @eq ghost (ghost_fmap (approx (@fst nat rmap' (@pair nat rmap' n r))) (approx (@fst nat rmap' (@pair nat rmap' n r))) g) g *)
  generalize H; rewrite <- (squash_unsquash phi).
(* Goal: @eq (prod nat rmap') (unsquash (squash (@pair nat rmap' n (rmap_fmap (approx (S n)) (approx (S n)) r0)))) (@pair nat rmap' n r0) *)
  rewrite H. rewrite unsquash_squash.
(* Goal: forall (w : rmap) (loc : AV.address), @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (@core resource Join_resource Sep_resource (resource_at w loc))) (@core resource Join_resource Sep_resource (resource_at w loc)) *)
  simpl; intros.
(* Goal: not (@identity resource Join_resource (YES sh rsh k Q)) *)
  injection H0. clear H0. intro.
(* Goal: @eq ghost (ghost_fmap (approx n) (approx n) g) g *)
  clear phi H.
(* Goal: @eq ghost (ghost_fmap (approx n) (approx n) g) g *)
  rewrite <- H0 in H1.
(* Goal: @eq ghost (ghost_fmap (approx n) (approx n) g) g *)
  clear H0.
  unfold rmap_fmap in *.
  simpl in *.
(* Goal: @eq resource match f l with | NO sh nsh => NO sh nsh | YES sh rsh k p => YES sh rsh k (preds_fmap (approx n) (approx n) p) | PURE k p => PURE k (preds_fmap (approx n) (approx n) p) end (f l) *)
  revert H1.
(* Goal: forall _ : @join resource Join_resource (f l) g (@compose AV.address resource resource (resource_fmap (approx n) (approx n)) (@fst (forall _ : AV.address, resource) ghost r) l), @eq resource match f l with | NO sh nsh => NO sh nsh | YES sh rsh k p => YES sh rsh k (preds_fmap (approx n) (approx n) p) | PURE k p => PURE k (preds_fmap (approx n) (approx n) p) end (f l) *)
  unfold resource_fmap, compose.
  destruct (f l); destruct g; destruct (fst r l); simpl; intro; auto; inv H1;
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
    rewrite preds_fmap_fmap, approx_oo_approx; auto.
Qed.

Lemma ghost_fmap_fmap:  forall f1 f2 g1 g2 r,
  ghost_fmap f1 f2 (ghost_fmap g1 g2 r) = ghost_fmap (f1 oo g1) (g2 oo f2) r.
Proof.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
  intros; rewrite <- ghost_fmap_comp; auto.
Qed.

Lemma ghost_same_level:
   forall g phi, join_sub g (ghost_of phi) ->
   ghost_fmap (approx (level phi)) (approx (level phi)) g = g.
Proof.
(* Goal: forall (w : rmap) (loc : AV.address), @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (@core resource Join_resource Sep_resource (resource_at w loc))) (@core resource Join_resource Sep_resource (resource_at w loc)) *)
  intros.
(* Goal: @eq nat (@level rmap ag_rmap (empty_rmap lev)) lev *)
  rewrite rmap_level_eq.
  unfold ghost_of in *.
(* Goal: @eq ghost (ghost_fmap (approx (@fst nat rmap' (unsquash phi))) (approx (@fst nat rmap' (unsquash phi))) g) g *)
  revert H; case_eq (unsquash phi); intros n ? ?.
(* Goal: forall _ : @join_sub ghost ghost_join g (@snd (forall _ : AV.address, resource) ghost (@snd nat rmap' (@pair nat rmap' n r))), @eq ghost (ghost_fmap (approx (@fst nat rmap' (@pair nat rmap' n r))) (approx (@fst nat rmap' (@pair nat rmap' n r))) g) g *)
  generalize H; rewrite <- (squash_unsquash phi).
(* Goal: @eq (prod nat rmap') (unsquash (squash (@pair nat rmap' n (rmap_fmap (approx (S n)) (approx (S n)) r0)))) (@pair nat rmap' n r0) *)
  rewrite H. rewrite unsquash_squash.
(* Goal: forall (w : rmap) (loc : AV.address), @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (@core resource Join_resource Sep_resource (resource_at w loc))) (@core resource Join_resource Sep_resource (resource_at w loc)) *)
  simpl; intros.
(* Goal: not (@identity resource Join_resource (YES sh rsh k Q)) *)
  injection H0. clear H0. intro.
(* Goal: @eq ghost (ghost_fmap (approx n) (approx n) g) g *)
  clear phi H.
(* Goal: @eq ghost (ghost_fmap (approx n) (approx n) g) g *)
  rewrite <- H0 in H1.
(* Goal: @eq ghost (ghost_fmap (approx n) (approx n) g) g *)
  clear H0.
  unfold rmap_fmap in *.
(* Goal: iff (@identity resource Join_resource r) match r with | NO sh rsh => @identity Share.t Share.Join_ba sh | YES sh r k p => False | PURE k p => True end *)
  destruct r.
(* Goal: @identity resource Join_resource (NO sh n0) *)
(* Goal: @identity resource Join_resource (YES sh r0 k p) *)
(* Goal: @identity resource Join_resource (PURE k p) *)
  simpl in H1; destruct H1.
(* Goal: @eq ghost (ghost_fmap (approx n) (approx n) g) g *)
  remember (ghost_fmap (approx n) (approx n) g0) as g'.
(* Goal: False *)
  revert dependent g0; induction H; auto; intros; subst.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
  - rewrite ghost_fmap_fmap, approx_oo_approx; auto.
  - destruct g0; inv Heqg'.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
    simpl; f_equal; eauto.
(* Goal: not (@identity share Share.Join_ba (Share.glb Share.Rsh (Share.lub a' (Share.glb Share.Rsh b)))) *)
    inv H; auto; simpl.
(* Goal: not (@identity share Share.Join_ba (Share.glb Share.Rsh (Share.lub a' (Share.glb Share.Rsh b)))) *)
    + destruct o as [[]|]; auto; simpl.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
      rewrite preds_fmap_fmap, approx_oo_approx; auto.
    + destruct a0, a3, a4; inv H4; simpl in *.
(* Goal: None *)
      destruct o as [[]|]; inv H1.
(* Goal: None *)
      inv H2.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
      rewrite preds_fmap_fmap, approx_oo_approx; auto.
Qed.

Lemma deallocate:
  forall (phi: rmap) (f g : AV.address -> resource) a b,
  (forall l, join  (f l) (g l) (phi@l)) -> join a b (ghost_of phi) ->
   exists phi1, exists phi2,
     join phi1 phi2 phi /\ resource_at phi1 = f /\ ghost_of phi1 = a.
Proof.
(* Goal: forall (phi : rmap) (f g : forall _ : AV.address, resource) (a b : ghost) (_ : forall l : AV.address, @join resource Join_resource (f l) (g l) (resource_at phi l)) (_ : @join ghost ghost_join a b (ghost_of phi)), @ex rmap (fun phi1 : rmap => @ex rmap (fun phi2 : rmap => and (@join rmap Join_rmap phi1 phi2 phi) (and (@eq (forall _ : AV.address, resource) (resource_at phi1) f) (@eq ghost (ghost_of phi1) a)))) *)
  intros until b. intros H0 HG.
(* Goal: not (@identity resource Join_resource (YES sh rsh k Q)) *)
  generalize (resources_same_level f phi); intro.
(* Goal: False *)
  spec H. intro; econstructor; apply H0.
(* Goal: not (@identity resource Join_resource (YES sh rsh k Q)) *)
  generalize (resources_same_level g phi); intro.
(* Goal: @ex rmap (fun phi1 : rmap => @ex rmap (fun phi2 : rmap => and (@join rmap Join_rmap phi1 phi2 phi) (and (@eq (forall _ : AV.address, resource) (resource_at phi1) f) (@eq ghost (ghost_of phi1) a)))) *)
  spec H1.
(* Goal: not (@identity resource Join_resource (YES sh rsh k Q)) *)
  intro. econstructor; eapply join_comm; eauto.
(* Goal: @ex rmap (fun phi1 : rmap => @ex rmap (fun phi2 : rmap => and (@join rmap Join_rmap phi1 phi2 phi) (and (@eq (forall _ : AV.address, resource) (resource_at phi1) f) (@eq ghost (ghost_of phi1) a)))) *)
  generalize (ghost_same_level a phi); intro Ha.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
  spec Ha. eexists; eauto.
(* Goal: @ex rmap (fun phi1 : rmap => @ex rmap (fun phi2 : rmap => and (@join rmap Join_rmap phi1 phi2 phi) (and (@eq (forall _ : AV.address, resource) (resource_at phi1) f) (@eq ghost (ghost_of phi1) a)))) *)
  generalize (ghost_same_level b phi); intro Hb.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
  spec Hb. eexists; eauto.
(* Goal: @ex rmap (fun phi1 : rmap => @ex rmap (fun phi2 : rmap => and (@join rmap Join_rmap phi1 phi2 phi) (and (@eq (forall _ : AV.address, resource) (resource_at phi1) f) (@eq ghost (ghost_of phi1) a)))) *)
  generalize (make_rmap'' (level phi) f a); intros [phif [? [Gf Ga]]].
(* Goal: @ex rmap (fun phi1 : rmap => @ex rmap (fun phi2 : rmap => and (@join rmap Join_rmap phi1 phi2 phi) (and (@eq (forall _ : AV.address, resource) (resource_at phi1) f) (@eq ghost (ghost_of phi1) a)))) *)
  generalize (make_rmap'' (level phi) g b); intros [phig [? [Gg Gb]]].
(* Goal: @ex rmap (fun phi1 : rmap => @ex rmap (fun phi2 : rmap => and (@join rmap Join_rmap phi1 phi2 phi) (and (@eq (forall _ : AV.address, resource) (resource_at phi1) f) (@eq ghost (ghost_of phi1) a)))) *)
  exists phif; exists phig.
(* Goal: and (@join rmap Join_rmap phif phig phi) (and (@eq (forall _ : AV.address, resource) (resource_at phif) f) (@eq ghost (ghost_of phif) a)) *)
  split; [|rewrite Ga, Gf; auto].
(* Goal: forall (_ : @eq nat (@level rmap ag_rmap phi1) (@level rmap ag_rmap phi3)) (_ : @eq nat (@level rmap ag_rmap phi2) (@level rmap ag_rmap phi3)) (_ : forall loc : AV.address, @join resource Join_resource (resource_at phi1 loc) (resource_at phi2 loc) (resource_at phi3 loc)) (_ : @join ghost ghost_join (ghost_of phi1) (ghost_of phi2) (ghost_of phi3)), @join (prod nat rmap') Join_nat_rmap' (unsquash phi1) (unsquash phi2) (unsquash phi3) *)
  rewrite rmap_level_eq in *.
  unfold resource_at, ghost_of in *.
  revert H0 HG H Gf Ga H1 Gg Gb Ha Hb H2 H3;
  case_eq (unsquash phif); intros nf phif' ?.
(* Goal: forall (_ : forall l : AV.address, @join resource Join_resource (f l) (g l) (@fst (forall _ : AV.address, resource) ghost (@snd nat rmap' (unsquash phi)) l)) (_ : @join ghost ghost_join a b (@snd (forall _ : AV.address, resource) ghost (@snd nat rmap' (unsquash phi)))) (_ : @eq (forall _ : AV.address, resource) (@compose AV.address resource resource (resource_fmap (approx (@fst nat rmap' (unsquash phi))) (approx (@fst nat rmap' (unsquash phi)))) f) f) (_ : @eq (forall _ : AV.address, resource) (@fst (forall _ : AV.address, resource) ghost (@snd nat rmap' (@pair nat rmap' nf phif'))) (@compose AV.address resource resource (resource_fmap (approx (@fst nat rmap' (unsquash phi))) (approx (@fst nat rmap' (unsquash phi)))) f)) (_ : @eq ghost (@snd (forall _ : AV.address, resource) ghost (@snd nat rmap' (@pair nat rmap' nf phif'))) (ghost_fmap (approx (@fst nat rmap' (unsquash phi))) (approx (@fst nat rmap' (unsquash phi))) a)) (_ : @eq (forall _ : AV.address, resource) (@compose AV.address resource resource (resource_fmap (approx (@fst nat rmap' (unsquash phi))) (approx (@fst nat rmap' (unsquash phi)))) g) g) (_ : @eq (forall _ : AV.address, resource) (@fst (forall _ : AV.address, resource) ghost (@snd nat rmap' (unsquash phig))) (@compose AV.address resource resource (resource_fmap (approx (@fst nat rmap' (unsquash phi))) (approx (@fst nat rmap' (unsquash phi)))) g)) (_ : @eq ghost (@snd (forall _ : AV.address, resource) ghost (@snd nat rmap' (unsquash phig))) (ghost_fmap (approx (@fst nat rmap' (unsquash phi))) (approx (@fst nat rmap' (unsquash phi))) b)) (_ : @eq ghost (ghost_fmap (approx (@fst nat rmap' (unsquash phi))) (approx (@fst nat rmap' (unsquash phi))) a) a) (_ : @eq ghost (ghost_fmap (approx (@fst nat rmap' (unsquash phi))) (approx (@fst nat rmap' (unsquash phi))) b) b) (_ : @eq nat (@fst nat rmap' (@pair nat rmap' nf phif')) (@fst nat rmap' (unsquash phi))) (_ : @eq nat (@fst nat rmap' (unsquash phig)) (@fst nat rmap' (unsquash phi))), @join rmap Join_rmap phif phig phi *)
  case_eq (unsquash phig); intros ng phig' ?.
(* Goal: forall (_ : forall l : AV.address, @join resource Join_resource (f l) (g l) (@fst (forall _ : AV.address, resource) ghost (@snd nat rmap' (unsquash phi)) l)) (_ : @join ghost ghost_join a b (@snd (forall _ : AV.address, resource) ghost (@snd nat rmap' (unsquash phi)))) (_ : @eq (forall _ : AV.address, resource) (@compose AV.address resource resource (resource_fmap (approx (@fst nat rmap' (unsquash phi))) (approx (@fst nat rmap' (unsquash phi)))) f) f) (_ : @eq (forall _ : AV.address, resource) (@fst (forall _ : AV.address, resource) ghost (@snd nat rmap' (@pair nat rmap' nf phif'))) (@compose AV.address resource resource (resource_fmap (approx (@fst nat rmap' (unsquash phi))) (approx (@fst nat rmap' (unsquash phi)))) f)) (_ : @eq ghost (@snd (forall _ : AV.address, resource) ghost (@snd nat rmap' (@pair nat rmap' nf phif'))) (ghost_fmap (approx (@fst nat rmap' (unsquash phi))) (approx (@fst nat rmap' (unsquash phi))) a)) (_ : @eq (forall _ : AV.address, resource) (@compose AV.address resource resource (resource_fmap (approx (@fst nat rmap' (unsquash phi))) (approx (@fst nat rmap' (unsquash phi)))) g) g) (_ : @eq (forall _ : AV.address, resource) (@fst (forall _ : AV.address, resource) ghost (@snd nat rmap' (@pair nat rmap' ng phig'))) (@compose AV.address resource resource (resource_fmap (approx (@fst nat rmap' (unsquash phi))) (approx (@fst nat rmap' (unsquash phi)))) g)) (_ : @eq ghost (@snd (forall _ : AV.address, resource) ghost (@snd nat rmap' (@pair nat rmap' ng phig'))) (ghost_fmap (approx (@fst nat rmap' (unsquash phi))) (approx (@fst nat rmap' (unsquash phi))) b)) (_ : @eq ghost (ghost_fmap (approx (@fst nat rmap' (unsquash phi))) (approx (@fst nat rmap' (unsquash phi))) a) a) (_ : @eq ghost (ghost_fmap (approx (@fst nat rmap' (unsquash phi))) (approx (@fst nat rmap' (unsquash phi))) b) b) (_ : @eq nat (@fst nat rmap' (@pair nat rmap' nf phif')) (@fst nat rmap' (unsquash phi))) (_ : @eq nat (@fst nat rmap' (@pair nat rmap' ng phig')) (@fst nat rmap' (unsquash phi))), @join rmap Join_rmap phif phig phi *)
  case_eq (unsquash phi); intros n phi' ?.
(* Goal: not (@identity share Share.Join_ba (Share.glb Share.Rsh (Share.lub a' (Share.glb Share.Rsh b)))) *)
  simpl.
(* Goal: forall (_ : forall l : AV.address, @join resource Join_resource (f l) (g l) (@fst (forall _ : AV.address, resource) ghost phi' l)) (_ : @join ghost ghost_join a b (@snd (forall _ : AV.address, resource) ghost phi')) (_ : @eq (forall _ : AV.address, resource) (@compose AV.address resource resource (resource_fmap (approx n) (approx n)) f) f) (_ : @eq (forall _ : AV.address, resource) (@fst (forall _ : AV.address, resource) ghost phif') (@compose AV.address resource resource (resource_fmap (approx n) (approx n)) f)) (_ : @eq ghost (@snd (forall _ : AV.address, resource) ghost phif') (ghost_fmap (approx n) (approx n) a)) (_ : @eq (forall _ : AV.address, resource) (@compose AV.address resource resource (resource_fmap (approx n) (approx n)) g) g) (_ : @eq (forall _ : AV.address, resource) (@fst (forall _ : AV.address, resource) ghost phig') (@compose AV.address resource resource (resource_fmap (approx n) (approx n)) g)) (_ : @eq ghost (@snd (forall _ : AV.address, resource) ghost phig') (ghost_fmap (approx n) (approx n) b)) (_ : @eq ghost (ghost_fmap (approx n) (approx n) a) a) (_ : @eq ghost (ghost_fmap (approx n) (approx n) b) b) (_ : @eq nat nf n) (_ : @eq nat ng n), @join rmap Join_rmap phif phig phi *)
  intros; subst nf ng.
(* Goal: forall (_ : @eq nat (@level rmap ag_rmap phi1) (@level rmap ag_rmap phi3)) (_ : @eq nat (@level rmap ag_rmap phi2) (@level rmap ag_rmap phi3)) (_ : forall loc : AV.address, @join resource Join_resource (resource_at phi1 loc) (resource_at phi2 loc) (resource_at phi3 loc)) (_ : @join ghost ghost_join (ghost_of phi1) (ghost_of phi2) (ghost_of phi3)), @join rmap Join_rmap phi1 phi2 phi3 *)
  rewrite join_unsquash.
(* Goal: @join (prod nat rmap') Join_nat_rmap' (unsquash phif) (unsquash phig) (unsquash phi) *)
  rewrite H; rewrite H0.
(* Goal: @join (prod nat rmap') Join_nat_rmap' (@pair nat rmap' n phif') (@pair nat rmap' n phig') (unsquash phi) *)
  revert H1; case_eq (unsquash phi); intros n' phi'' ?.
(* Goal: forall (w : rmap) (loc : AV.address), @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (@core resource Join_resource Sep_resource (resource_at w loc))) (@core resource Join_resource Sep_resource (resource_at w loc)) *)
  intros.
(* Goal: @join (prod nat rmap') Join_nat_rmap' (@pair nat rmap' n phif') (@pair nat rmap' n phig') (@pair nat rmap' n' phi'') *)
  inversion H5.
(* Goal: not (@identity share Share.Join_ba (Share.glb Share.Rsh (Share.lub a' (Share.glb Share.Rsh b)))) *)
  simpl.
(* Goal: @join (prod nat rmap') Join_nat_rmap' (@pair nat rmap' n phif') (@pair nat rmap' n phig') (@pair nat rmap' n phi') *)
  split.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
  simpl; constructor; auto.
(* Goal: @join rmap' (Join_prod (forall _ : AV.address, resource) (Join_pi AV.address (fun _ : AV.address => resource) (fun _ : AV.address => Join_resource)) ghost ghost_join) (@snd nat rmap' (@pair nat rmap' n phif')) (@snd nat rmap' (@pair nat rmap' n phig')) (@snd nat rmap' (@pair nat rmap' n phi')) *)
  subst n' phi''.
(* Goal: @join resource Join_resource (YES sh r k p) (NO Share.bot bot_unreadable) (YES sh r k p) *)
(* Goal: False *)
  constructor.
(* Goal: @join (forall _ : AV.address, resource) (Join_pi AV.address (fun _ : AV.address => resource) (fun _ : AV.address => Join_resource)) (@fst (forall _ : AV.address, resource) ghost (@snd nat rmap' (@pair nat rmap' n phif'))) (@fst (forall _ : AV.address, resource) ghost (@snd nat rmap' (@pair nat rmap' n phig'))) (@fst (forall _ : AV.address, resource) ghost (@snd nat rmap' (@pair nat rmap' n phi'))) *)
(* Goal: @join ghost ghost_join (@snd (forall _ : AV.address, resource) ghost (@snd nat rmap' (@pair nat rmap' n phif'))) (@snd (forall _ : AV.address, resource) ghost (@snd nat rmap' (@pair nat rmap' n phig'))) (@snd (forall _ : AV.address, resource) ghost (@snd nat rmap' (@pair nat rmap' n phi'))) *)
  intro l; specialize ( H2 l).
(* Goal: not (@identity share Share.Join_ba (Share.glb Share.Rsh (Share.lub a' (Share.glb Share.Rsh b)))) *)
  simpl.
(* Goal: @join resource Join_resource (@fst (forall _ : AV.address, resource) ghost phif' l) (@fst (forall _ : AV.address, resource) ghost phig' l) (@fst (forall _ : AV.address, resource) ghost phi' l) *)
(* Goal: @join ghost ghost_join (@snd (forall _ : AV.address, resource) ghost (@snd nat rmap' (@pair nat rmap' n phif'))) (@snd (forall _ : AV.address, resource) ghost (@snd nat rmap' (@pair nat rmap' n phig'))) (@snd (forall _ : AV.address, resource) ghost (@snd nat rmap' (@pair nat rmap' n phi'))) *)
  rewrite Gf; rewrite Gg; clear Gf Gg.
(* Goal: @join resource Join_resource (@compose AV.address resource resource (resource_fmap (approx n) (approx n)) f l) (@compose AV.address resource resource (resource_fmap (approx n) (approx n)) g l) (@fst (forall _ : AV.address, resource) ghost phi' l) *)
(* Goal: @join ghost ghost_join (@snd (forall _ : AV.address, resource) ghost (@snd nat rmap' (@pair nat rmap' n phif'))) (@snd (forall _ : AV.address, resource) ghost (@snd nat rmap' (@pair nat rmap' n phig'))) (@snd (forall _ : AV.address, resource) ghost (@snd nat rmap' (@pair nat rmap' n phi'))) *)
  rewrite H3; rewrite H4.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
  auto.
(* Goal: not (@identity share Share.Join_ba (Share.glb Share.Rsh (Share.lub a' (Share.glb Share.Rsh b)))) *)
  simpl; rewrite Ga, Gb; simpl.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
  rewrite Ha, Hb; auto.
Qed.

  Lemma unsquash_inj : forall x y,
      unsquash x = unsquash y -> x = y.
  Proof.
(* Goal: forall (w : rmap) (loc : AV.address), @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (@core resource Join_resource Sep_resource (resource_at w loc))) (@core resource Join_resource Sep_resource (resource_at w loc)) *)
    intros.
    rewrite <- (squash_unsquash x).
    rewrite <- (squash_unsquash y).
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
    rewrite H; auto.
  Qed.

Lemma resource_fmap_fmap:  forall f1 f2 g1 g2 r, resource_fmap f1 f2 (resource_fmap g1 g2 r) =
                                                                      resource_fmap (f1 oo g1) (g2 oo f2) r.
Proof.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
destruct r; simpl; auto.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
rewrite preds_fmap_fmap; auto.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
rewrite preds_fmap_fmap; auto.
Qed.

Lemma ghost_of_approx:
  forall phi,
      ghost_fmap (approx (level phi)) (approx (level phi)) (ghost_of phi) = ghost_of phi.
Proof.
(* Goal: forall (w : rmap) (loc : AV.address), @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (@core resource Join_resource Sep_resource (resource_at w loc))) (@core resource Join_resource Sep_resource (resource_at w loc)) *)
intros. symmetry. rewrite rmap_level_eq. unfold ghost_of.
(* Goal: forall (w : rmap) (loc : AV.address), @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (@core resource Join_resource Sep_resource (resource_at w loc))) (@core resource Join_resource Sep_resource (resource_at w loc)) *)
case_eq (unsquash phi); intros.
(* Goal: not (@identity share Share.Join_ba (Share.glb Share.Rsh (Share.lub a' (Share.glb Share.Rsh b)))) *)
simpl.
set (phi' := (squash (n, (resource_fmap (approx n) (approx n) oo fst r, snd r)))).
(* Goal: not (@identity resource Join_resource (YES sh rsh k Q)) *)
generalize (unsquash_inj phi phi'); intro.
spec H0.
-
replace (unsquash phi) with (unsquash (squash (unsquash phi))).
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
2: rewrite squash_unsquash; auto.
(* Goal: @eq resource (resource_fmap (approx (@level rmap ag_rmap r0)) (approx (@level rmap ag_rmap r0)) (resource_at phi1 loc)) (resource_fmap (approx (@level rmap ag_rmap r)) (approx (@level rmap ag_rmap r)) (resource_at phi2 loc)) *)
rewrite H.
unfold phi'.
(* Goal: @eq (prod nat rmap') (unsquash (squash (@pair nat rmap' n (rmap_fmap (approx (S n)) (approx (S n)) r0)))) (@pair nat rmap' n r0) *)
repeat rewrite unsquash_squash.
(* Goal: @eq resource (NO Share.bot nsh1) (NO Share.bot bot_unreadable) *)
f_equal.
(* Goal: not (@identity share Share.Join_ba (Share.glb Share.Rsh (Share.lub a' (Share.glb Share.Rsh b)))) *)
unfold rmap_fmap. simpl.
(* Goal: @eq resource (@compose AV.address resource resource (resource_fmap (approx n) (approx n)) f l) (f l) *)
unfold compose.
(* Goal: @eq resource (NO Share.bot nsh1) (NO Share.bot bot_unreadable) *)
f_equal.
extensionality y.
(* Goal: @eq resource (resource_fmap (approx n) (approx n) (resource_fmap (approx (S n)) (approx (S n)) r0)) (resource_fmap (approx n) (approx n) r0) *)
rewrite resource_fmap_fmap.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
rewrite approx_oo_approx; auto.
-
unfold phi' in *; clear phi'.
(* Goal: False *)
subst.
(* Goal: @eq resource (r l) (r0 l) *)
(* Goal: @eq ghost (ghost_of a) (ghost_of b) *)
rewrite unsquash_squash in H.
(* Goal: not (@identity resource Join_resource (YES sh rsh k Q)) *)
injection H; clear H; intro.
pattern r at 1; rewrite <- H.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
auto.
Qed.

Lemma ghost_same_level_gen:
   forall n a b c, join (ghost_fmap (approx n) (approx n) a) (ghost_fmap (approx n) (approx n) b) c ->
   ghost_fmap (approx n) (approx n) c = c.
Proof.
(* Goal: forall (w : rmap) (loc : AV.address), @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (@core resource Join_resource Sep_resource (resource_at w loc))) (@core resource Join_resource Sep_resource (resource_at w loc)) *)
  intros.
(* Goal: @eq ghost (ghost_fmap (approx n) (approx n) c) c *)
  remember (ghost_fmap (approx n) (approx n) a) as a'; remember (ghost_fmap (approx n) (approx n) b) as b'.
(* Goal: False *)
  revert dependent b; revert dependent a; induction H; intros; subst.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
  - rewrite ghost_fmap_fmap, approx_oo_approx; auto.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
  - rewrite ghost_fmap_fmap, approx_oo_approx; auto.
  - destruct a, b; inv Heqa'; inv Heqb'.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
    simpl; f_equal; eauto.
(* Goal: not (@identity share Share.Join_ba (Share.glb Share.Rsh (Share.lub a' (Share.glb Share.Rsh b)))) *)
    inv H; simpl.
(* Goal: not (@identity share Share.Join_ba (Share.glb Share.Rsh (Share.lub a' (Share.glb Share.Rsh b)))) *)
    + destruct o0 as [[]|]; auto; simpl.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
      rewrite preds_fmap_fmap, approx_oo_approx; auto.
(* Goal: not (@identity share Share.Join_ba (Share.glb Share.Rsh (Share.lub a' (Share.glb Share.Rsh b)))) *)
    + destruct o as [[]|]; auto; simpl.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
      rewrite preds_fmap_fmap, approx_oo_approx; auto.
    + destruct a1, a2, a0; inv H3; simpl in *.
(* Goal: None *)
      destruct o as [[]|]; inv H1; inv H4.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
      rewrite preds_fmap_fmap, approx_oo_approx; auto.
Qed.

Lemma allocate:
     forall (phi : rmap) (f : AV.address -> resource) a,
        resource_fmap (approx (level phi)) (approx (level phi)) oo f = f ->
       (forall l, {r' | join (phi@l) (f l) r'}) ->
        ghost_fmap (approx (level phi)) (approx (level phi)) a = a ->
        {a' | join (ghost_of phi) a a'} ->
       exists phi1 : rmap,
         exists phi2 : rmap,
           join phi phi1 phi2 /\ resource_at phi1 = f /\ ghost_of phi1 = a.
Proof.
(* Goal: forall (w : rmap) (loc : AV.address), @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (@core resource Join_resource Sep_resource (resource_at w loc))) (@core resource Join_resource Sep_resource (resource_at w loc)) *)
 intros. rename H0 into Hg. rename X into H1.
(* Goal: @ex rmap (fun phi1 : rmap => @ex rmap (fun phi2 : rmap => and (@join rmap Join_rmap phi1 phi2 phi) (and (@eq (forall _ : AV.address, resource) (resource_at phi1) f) (@eq ghost (ghost_of phi1) a)))) *)
 generalize (make_rmap'' (level phi) f a); intros [phif [? [Gf Ga]]].
 pose (g loc := proj1_sig (H1 loc)).
 assert (H3: forall l, join (phi @ l) (f l) (g l))
   by (unfold g; intro; destruct (H1 l); simpl in *; auto).
 clearbody g.
 destruct X0 as [b X0].
(* Goal: not (@identity resource Join_resource (YES sh rsh k Q)) *)
 generalize (make_rmap'' (level phi) g b); intro.
 destruct H2 as [phig [H4 [H5 H6]]].
 rename H0 into H2.
(* Goal: @ex rmap (fun phi1 : rmap => @ex rmap (fun phi2 : rmap => and (@join rmap Join_rmap phi1 phi2 phi) (and (@eq (forall _ : AV.address, resource) (resource_at phi1) f) (@eq ghost (ghost_of phi1) a)))) *)
 exists phif; exists phig.
 split; [|split; congruence].
(* Goal: forall (_ : @eq nat (@level rmap ag_rmap phi1) (@level rmap ag_rmap phi3)) (_ : @eq nat (@level rmap ag_rmap phi2) (@level rmap ag_rmap phi3)) (_ : forall loc : AV.address, @join resource Join_resource (resource_at phi1 loc) (resource_at phi2 loc) (resource_at phi3 loc)) (_ : @join ghost ghost_join (ghost_of phi1) (ghost_of phi2) (ghost_of phi3)), @join rmap Join_rmap phi1 phi2 phi3 *)
 rewrite join_unsquash.
 unfold resource_at, ghost_of in *.
(* Goal: forall (_ : @eq nat (@level rmap ag_rmap phi1) (@level rmap ag_rmap phi3)) (_ : @eq nat (@level rmap ag_rmap phi2) (@level rmap ag_rmap phi3)) (_ : forall loc : AV.address, @join resource Join_resource (resource_at phi1 loc) (resource_at phi2 loc) (resource_at phi3 loc)) (_ : @join ghost ghost_join (ghost_of phi1) (ghost_of phi2) (ghost_of phi3)), @join (prod nat rmap') Join_nat_rmap' (unsquash phi1) (unsquash phi2) (unsquash phi3) *)
 rewrite rmap_level_eq in *.
 rename H into H0. pose proof I.
 revert H0 H1 Hg X0 H2 H3 H4 H5 H6 Gf Ga.
 case_eq (unsquash phif); intros nf phif' ?.
(* Goal: forall (_ : forall l : AV.address, @join resource Join_resource (f l) (g l) (@fst (forall _ : AV.address, resource) ghost (@snd nat rmap' (unsquash phi)) l)) (_ : @join ghost ghost_join a b (@snd (forall _ : AV.address, resource) ghost (@snd nat rmap' (unsquash phi)))) (_ : @eq (forall _ : AV.address, resource) (@compose AV.address resource resource (resource_fmap (approx (@fst nat rmap' (unsquash phi))) (approx (@fst nat rmap' (unsquash phi)))) f) f) (_ : @eq (forall _ : AV.address, resource) (@fst (forall _ : AV.address, resource) ghost (@snd nat rmap' (@pair nat rmap' nf phif'))) (@compose AV.address resource resource (resource_fmap (approx (@fst nat rmap' (unsquash phi))) (approx (@fst nat rmap' (unsquash phi)))) f)) (_ : @eq ghost (@snd (forall _ : AV.address, resource) ghost (@snd nat rmap' (@pair nat rmap' nf phif'))) (ghost_fmap (approx (@fst nat rmap' (unsquash phi))) (approx (@fst nat rmap' (unsquash phi))) a)) (_ : @eq (forall _ : AV.address, resource) (@compose AV.address resource resource (resource_fmap (approx (@fst nat rmap' (unsquash phi))) (approx (@fst nat rmap' (unsquash phi)))) g) g) (_ : @eq (forall _ : AV.address, resource) (@fst (forall _ : AV.address, resource) ghost (@snd nat rmap' (unsquash phig))) (@compose AV.address resource resource (resource_fmap (approx (@fst nat rmap' (unsquash phi))) (approx (@fst nat rmap' (unsquash phi)))) g)) (_ : @eq ghost (@snd (forall _ : AV.address, resource) ghost (@snd nat rmap' (unsquash phig))) (ghost_fmap (approx (@fst nat rmap' (unsquash phi))) (approx (@fst nat rmap' (unsquash phi))) b)) (_ : @eq ghost (ghost_fmap (approx (@fst nat rmap' (unsquash phi))) (approx (@fst nat rmap' (unsquash phi))) a) a) (_ : @eq ghost (ghost_fmap (approx (@fst nat rmap' (unsquash phi))) (approx (@fst nat rmap' (unsquash phi))) b) b) (_ : @eq nat (@fst nat rmap' (@pair nat rmap' nf phif')) (@fst nat rmap' (unsquash phi))) (_ : @eq nat (@fst nat rmap' (unsquash phig)) (@fst nat rmap' (unsquash phi))), @join rmap Join_rmap phif phig phi *)
 case_eq (unsquash phig); intros ng phig' ?.
(* Goal: forall (_ : forall l : AV.address, @join resource Join_resource (f l) (g l) (@fst (forall _ : AV.address, resource) ghost (@snd nat rmap' (unsquash phi)) l)) (_ : @join ghost ghost_join a b (@snd (forall _ : AV.address, resource) ghost (@snd nat rmap' (unsquash phi)))) (_ : @eq (forall _ : AV.address, resource) (@compose AV.address resource resource (resource_fmap (approx (@fst nat rmap' (unsquash phi))) (approx (@fst nat rmap' (unsquash phi)))) f) f) (_ : @eq (forall _ : AV.address, resource) (@fst (forall _ : AV.address, resource) ghost (@snd nat rmap' (@pair nat rmap' nf phif'))) (@compose AV.address resource resource (resource_fmap (approx (@fst nat rmap' (unsquash phi))) (approx (@fst nat rmap' (unsquash phi)))) f)) (_ : @eq ghost (@snd (forall _ : AV.address, resource) ghost (@snd nat rmap' (@pair nat rmap' nf phif'))) (ghost_fmap (approx (@fst nat rmap' (unsquash phi))) (approx (@fst nat rmap' (unsquash phi))) a)) (_ : @eq (forall _ : AV.address, resource) (@compose AV.address resource resource (resource_fmap (approx (@fst nat rmap' (unsquash phi))) (approx (@fst nat rmap' (unsquash phi)))) g) g) (_ : @eq (forall _ : AV.address, resource) (@fst (forall _ : AV.address, resource) ghost (@snd nat rmap' (@pair nat rmap' ng phig'))) (@compose AV.address resource resource (resource_fmap (approx (@fst nat rmap' (unsquash phi))) (approx (@fst nat rmap' (unsquash phi)))) g)) (_ : @eq ghost (@snd (forall _ : AV.address, resource) ghost (@snd nat rmap' (@pair nat rmap' ng phig'))) (ghost_fmap (approx (@fst nat rmap' (unsquash phi))) (approx (@fst nat rmap' (unsquash phi))) b)) (_ : @eq ghost (ghost_fmap (approx (@fst nat rmap' (unsquash phi))) (approx (@fst nat rmap' (unsquash phi))) a) a) (_ : @eq ghost (ghost_fmap (approx (@fst nat rmap' (unsquash phi))) (approx (@fst nat rmap' (unsquash phi))) b) b) (_ : @eq nat (@fst nat rmap' (@pair nat rmap' nf phif')) (@fst nat rmap' (unsquash phi))) (_ : @eq nat (@fst nat rmap' (@pair nat rmap' ng phig')) (@fst nat rmap' (unsquash phi))), @join rmap Join_rmap phif phig phi *)
 case_eq (unsquash phi); intros n phi' ?.
(* Goal: not (@identity share Share.Join_ba (Share.glb Share.Rsh (Share.lub a' (Share.glb Share.Rsh b)))) *)
 simpl.
(* Goal: forall (_ : forall l : AV.address, @join resource Join_resource (f l) (g l) (@fst (forall _ : AV.address, resource) ghost phi' l)) (_ : @join ghost ghost_join a b (@snd (forall _ : AV.address, resource) ghost phi')) (_ : @eq (forall _ : AV.address, resource) (@compose AV.address resource resource (resource_fmap (approx n) (approx n)) f) f) (_ : @eq (forall _ : AV.address, resource) (@fst (forall _ : AV.address, resource) ghost phif') (@compose AV.address resource resource (resource_fmap (approx n) (approx n)) f)) (_ : @eq ghost (@snd (forall _ : AV.address, resource) ghost phif') (ghost_fmap (approx n) (approx n) a)) (_ : @eq (forall _ : AV.address, resource) (@compose AV.address resource resource (resource_fmap (approx n) (approx n)) g) g) (_ : @eq (forall _ : AV.address, resource) (@fst (forall _ : AV.address, resource) ghost phig') (@compose AV.address resource resource (resource_fmap (approx n) (approx n)) g)) (_ : @eq ghost (@snd (forall _ : AV.address, resource) ghost phig') (ghost_fmap (approx n) (approx n) b)) (_ : @eq ghost (ghost_fmap (approx n) (approx n) a) a) (_ : @eq ghost (ghost_fmap (approx n) (approx n) b) b) (_ : @eq nat nf n) (_ : @eq nat ng n), @join rmap Join_rmap phif phig phi *)
 intros; subst nf ng.
(* Goal: @eq nat (@level rmap ag_rmap m') (@level rmap ag_rmap m') *)
(* Goal: @ex rmap (fun m1 : rmap => and (@laterR rmap ag_rmap m m1) (@eq nat (@level rmap ag_rmap m1) (@level rmap ag_rmap m'))) *)
 split. split; trivial.
(* Goal: not (@identity share Share.Join_ba (Share.glb Share.Rsh (Share.lub a' (Share.glb Share.Rsh b)))) *)
 simpl.
(* Goal: @join (prod nat rmap') Join_nat_rmap' (@pair nat rmap' n phif') (@pair nat rmap' n phig') (@pair nat rmap' n phi') *)
 split.
 intro l.
 specialize ( H6 l).
 assert (fst phig' l = g l).
(* Goal: not (@identity resource Join_resource (YES sh rsh k Q)) *)
   generalize (f_equal squash H2); intro.
   rewrite squash_unsquash in H5.
   subst phi.
   rewrite unsquash_squash in H2.
(* Goal: not (@identity resource Join_resource (YES sh rsh k Q)) *)
   injection H2; clear H2; intro.
   rewrite <- H2 in H6.
   rewrite <- H3 in H6.
   rewrite H8.
   clear - H6.
   revert H6.
(* Goal: not (@identity share Share.Join_ba (Share.glb Share.Rsh (Share.lub a' (Share.glb Share.Rsh b)))) *)
   unfold rmap_fmap, compose, resource_fmap. simpl.
   destruct (fst phi' l); destruct (f l); destruct (g l); simpl; intros; auto; try inv H6;
              try change (preds_fmap (approx n) (approx n) (preds_fmap (approx n) (approx n) p0)) with
                ((preds_fmap (approx n) (approx n) oo preds_fmap (approx n) (approx n)) p0);
              try change (preds_fmap (approx n) (approx n) (preds_fmap (approx n) (approx n) p)) with
                ((preds_fmap (approx n) (approx n) oo preds_fmap (approx n) (approx n)) p);
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
                rewrite preds_fmap_comp; rewrite approx_oo_approx; auto.
 rewrite H5.
 rewrite Gf.
 rewrite H3.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
 auto.

(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
  erewrite Ga, H9, Hg, ghost_same_level_gen; auto.
  rewrite <- Hg in X0.
  pose proof (ghost_of_approx phi) as X.
  unfold ghost_of in X.
  rewrite rmap_level_eq, H2 in X; simpl in X.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
  rewrite X; eauto.
Qed.

  Lemma rmap_ext: forall phi1 phi2,
    level phi1 = level phi2 ->
    (forall l, phi1@l = phi2@l) ->
    ghost_of phi1 = ghost_of phi2 ->
    phi1=phi2.
  Proof.
(* Goal: forall (w : rmap) (loc : AV.address), @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (@core resource Join_resource Sep_resource (resource_at w loc))) (@core resource Join_resource Sep_resource (resource_at w loc)) *)
    intros.
(* Goal: @eq rmap (squash (@pair nat rmap' n (rmap_fmap (approx (S n)) (approx (S n)) r0))) r *)
    apply unsquash_inj.
(* Goal: forall (_ : @eq nat (@level rmap ag_rmap phi1) (@level rmap ag_rmap phi3)) (_ : @eq nat (@level rmap ag_rmap phi2) (@level rmap ag_rmap phi3)) (_ : forall loc : AV.address, @join resource Join_resource (resource_at phi1 loc) (resource_at phi2 loc) (resource_at phi3 loc)) (_ : @join ghost ghost_join (ghost_of phi1) (ghost_of phi2) (ghost_of phi3)), @join (prod nat rmap') Join_nat_rmap' (unsquash phi1) (unsquash phi2) (unsquash phi3) *)
    rewrite rmap_level_eq in *.
    unfold resource_at, ghost_of in *.
    rewrite <- (squash_unsquash phi1).
    rewrite <- (squash_unsquash phi2).
(* Goal: @eq (prod nat rmap') (unsquash (squash (unsquash phi1))) (unsquash (squash (unsquash phi2))) *)
    destruct (unsquash phi1).
(* Goal: @eq (prod nat rmap') (unsquash (squash (@pair nat rmap' n r))) (unsquash (squash (unsquash phi2))) *)
    destruct (unsquash phi2).
(* Goal: @ex rmap (fun m1 : rmap => and (@laterR rmap ag_rmap m m1) (@eq nat (@level rmap ag_rmap m1) (@level rmap ag_rmap m'))) *)
(* Goal: @ex rmap (fun m1 : rmap => and (@laterR rmap ag_rmap m m1) (@eq nat (@level rmap ag_rmap m1) (@level rmap ag_rmap m'))) *)
    simpl in H.
(* Goal: @eq resource (resource_fmap (approx (@level rmap ag_rmap r0)) (approx (@level rmap ag_rmap r0)) (resource_at phi1 loc)) (resource_fmap (approx (@level rmap ag_rmap r)) (approx (@level rmap ag_rmap r)) (resource_at phi2 loc)) *)
    rewrite H.
(* Goal: @eq (prod nat rmap') (unsquash (squash (@pair nat rmap' n (rmap_fmap (approx (S n)) (approx (S n)) r0)))) (@pair nat rmap' n r0) *)
    rewrite unsquash_squash.
(* Goal: @eq (prod nat rmap') (unsquash (squash (@pair nat rmap' n (rmap_fmap (approx (S n)) (approx (S n)) r0)))) (@pair nat rmap' n r0) *)
    rewrite unsquash_squash.
(* Goal: @eq (prod nat rmap') (@pair nat rmap' n0 (rmap_fmap (approx n0) (approx n0) r)) (@pair nat rmap' n0 (rmap_fmap (approx n0) (approx n0) r0)) *)
    simpl in H0, H1.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
    replace (rmap_fmap (approx n0) (approx n0) r) with (rmap_fmap (approx n0) (approx n0) r0); auto.
    simpl in *. unfold rmap_fmap.
    replace (resource_fmap (approx n0) (approx n0) oo fst r0)
      with (resource_fmap (approx n0) (approx n0) oo fst r).
    destruct r,r0; simpl in *; subst; auto.
(* Goal: @eq (forall _ : AV.address, resource) (@compose AV.address resource resource (resource_fmap (approx n) (approx n)) f) f *)
    extensionality l.
(* Goal: @eq resource (@compose AV.address resource resource (resource_fmap (approx n) (approx n)) f l) (f l) *)
    unfold compose.
(* Goal: @eq resource (resource_fmap (approx n0) (approx n0) (@fst (forall _ : AV.address, resource) ghost r l)) (resource_fmap (approx n0) (approx n0) (@fst (forall _ : AV.address, resource) ghost r0 l)) *)
    specialize ( H0 l).
(* Goal: @eq resource (resource_fmap (approx n0) (approx n0) (@fst (forall _ : AV.address, resource) ghost r l)) (resource_fmap (approx n0) (approx n0) (@fst (forall _ : AV.address, resource) ghost r0 l)) *)
    subst n0.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
    rewrite H0; auto.
  Qed.

  Lemma resource_at_join:
    forall phi1 phi2 phi3 loc,
      join phi1 phi2 phi3 ->
      join (phi1@loc) (phi2@loc) (phi3@loc).
  Proof.
(* Goal: forall (w : rmap) (loc : AV.address), @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (@core resource Join_resource Sep_resource (resource_at w loc))) (@core resource Join_resource Sep_resource (resource_at w loc)) *)
    intros.
(* Goal: @join ghost ghost_join (ghost_of phi1) (ghost_of phi2) (ghost_of phi3) *)
    revert H; rewrite join_unsquash; unfold resource_at.
(* Goal: forall _ : @join (prod nat rmap') Join_nat_rmap' (unsquash phi1) (unsquash phi2) (unsquash phi3), @join ghost ghost_join (ghost_of phi1) (ghost_of phi2) (ghost_of phi3) *)
    intros [? ?].
(* Goal: @join ghost ghost_join (ghost_of phi1) (ghost_of phi2) (ghost_of phi3) *)
    apply H0.
  Qed.

  Lemma ghost_of_join:
    forall phi1 phi2 phi3,
      join phi1 phi2 phi3 ->
      join (ghost_of phi1) (ghost_of phi2) (ghost_of phi3).
  Proof.
(* Goal: forall (w : rmap) (loc : AV.address), @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (@core resource Join_resource Sep_resource (resource_at w loc))) (@core resource Join_resource Sep_resource (resource_at w loc)) *)
    intros.
(* Goal: @join ghost ghost_join (ghost_of phi1) (ghost_of phi2) (ghost_of phi3) *)
    revert H; rewrite join_unsquash; unfold resource_at.
(* Goal: forall _ : @join (prod nat rmap') Join_nat_rmap' (unsquash phi1) (unsquash phi2) (unsquash phi3), @join ghost ghost_join (ghost_of phi1) (ghost_of phi2) (ghost_of phi3) *)
    intros [? ?].
(* Goal: @join ghost ghost_join (ghost_of phi1) (ghost_of phi2) (ghost_of phi3) *)
    apply H0.
  Qed.

  Lemma resource_at_join2:
    forall phi1 phi2 phi3,
      level phi1 = level phi3 -> level phi2 = level phi3 ->
      (forall loc, join (phi1@loc) (phi2@loc) (phi3@loc)) ->
      join (ghost_of phi1) (ghost_of phi2) (ghost_of phi3) ->
      join phi1 phi2 phi3.
  Proof.
(* Goal: @identity resource Join_resource (PURE k p) *)
    intros ? ? ?.
(* Goal: forall (_ : @eq nat (@level rmap ag_rmap phi1) (@level rmap ag_rmap phi3)) (_ : @eq nat (@level rmap ag_rmap phi2) (@level rmap ag_rmap phi3)) (_ : forall loc : AV.address, @join resource Join_resource (resource_at phi1 loc) (resource_at phi2 loc) (resource_at phi3 loc)) (_ : @join ghost ghost_join (ghost_of phi1) (ghost_of phi2) (ghost_of phi3)), @join rmap Join_rmap phi1 phi2 phi3 *)
    rewrite join_unsquash.
(* Goal: forall (_ : @eq nat (@level rmap ag_rmap phi1) (@level rmap ag_rmap phi3)) (_ : @eq nat (@level rmap ag_rmap phi2) (@level rmap ag_rmap phi3)) (_ : forall loc : AV.address, @join resource Join_resource (resource_at phi1 loc) (resource_at phi2 loc) (resource_at phi3 loc)) (_ : @join ghost ghost_join (ghost_of phi1) (ghost_of phi2) (ghost_of phi3)), @join (prod nat rmap') Join_nat_rmap' (unsquash phi1) (unsquash phi2) (unsquash phi3) *)
    rewrite rmap_level_eq in *.
(* Goal: forall (_ : @eq nat (@fst nat rmap' (unsquash phi1)) (@fst nat rmap' (unsquash phi3))) (_ : @eq nat (@fst nat rmap' (unsquash phi2)) (@fst nat rmap' (unsquash phi3))) (_ : forall loc : AV.address, @join resource Join_resource (resource_at phi1 loc) (resource_at phi2 loc) (resource_at phi3 loc)) (_ : @join ghost ghost_join (ghost_of phi1) (ghost_of phi2) (ghost_of phi3)), @join (prod nat rmap') Join_nat_rmap' (unsquash phi1) (unsquash phi2) (unsquash phi3) *)
    unfold resource_at, ghost_of.
(* Goal: forall (w : rmap) (loc : AV.address), @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (@core resource Join_resource Sep_resource (resource_at w loc))) (@core resource Join_resource Sep_resource (resource_at w loc)) *)
    case_eq (unsquash phi1); case_eq (unsquash phi2); case_eq (unsquash phi3); simpl; intros.
(* Goal: False *)
    subst.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
    split; auto.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
    split; auto.
  Qed.

Lemma all_resource_at_identity:
  forall w, (forall l, identity (w@l)) -> identity (ghost_of w) ->
         identity w.
Proof.
(* Goal: not (@identity resource Join_resource (YES sh rsh k Q)) *)
  repeat intro.
(* Goal: @eq rmap a b *)
  apply rmap_ext.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
  { apply join_level in H1; tauto. }
  intro l; specialize (H l).
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
  apply (resource_at_join _ _ _ l), H in H1; auto.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
  apply H0, ghost_of_join; auto.
Qed.

  Lemma ageN_squash : forall d n rm, le d n ->
    ageN d (squash (n, rm)) = Some (squash ((n - d)%nat, rm)).
  Proof.
(* Goal: forall (w : rmap) (loc : AV.address), @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (@core resource Join_resource Sep_resource (resource_at w loc))) (@core resource Join_resource Sep_resource (resource_at w loc)) *)
    induction d; simpl; intros.
(* Goal: not (@identity share Share.Join_ba (Share.glb Share.Rsh (Share.lub a' (Share.glb Share.Rsh b)))) *)
    unfold ageN; simpl.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
    replace (n-0)%nat with n by omega; auto.
(* Goal: not (@identity share Share.Join_ba (Share.glb Share.Rsh (Share.lub a' (Share.glb Share.Rsh b)))) *)
    unfold ageN; simpl.
    rewrite rmap_age1_eq in *.
(* Goal: @eq (prod nat rmap') (unsquash (squash (@pair nat rmap' n (rmap_fmap (approx (S n)) (approx (S n)) r0)))) (@pair nat rmap' n r0) *)
    rewrite unsquash_squash.
    destruct n.
(* Goal: @eq resource (YES sh1 rsh1 k pp) (NO Share.bot bot_unreadable) *)
    inv H.
(* Goal: @eq nat (@level rmap ag_rmap m) (Init.Nat.add (S (Init.Nat.sub (@level rmap ag_rmap m) (S (@level rmap ag_rmap m')))) (@level rmap ag_rmap m')) *)
(* Goal: @ex rmap (fun m1 : rmap => and (@laterR rmap ag_rmap m m1) (@eq nat (@level rmap ag_rmap m1) (@level rmap ag_rmap m'))) *)
    replace (S n - S d)%nat with (n - d)%nat by omega.
    unfold ageN in IHd. rewrite rmap_age1_eq in IHd.
    rewrite IHd.
(* Goal: @eq nat (@level rmap ag_rmap m) (Init.Nat.add (S (Init.Nat.sub (@level rmap ag_rmap m) (S (@level rmap ag_rmap m')))) (@level rmap ag_rmap m')) *)
(* Goal: @ex rmap (fun m1 : rmap => and (@laterR rmap ag_rmap m m1) (@eq nat (@level rmap ag_rmap m1) (@level rmap ag_rmap m'))) *)
    2: omega.
(* Goal: @eq resource (NO Share.bot nsh1) (NO Share.bot bot_unreadable) *)
    f_equal.
(* Goal: @eq rmap (squash (@pair nat rmap' n (rmap_fmap (approx (S n)) (approx (S n)) r0))) r *)
    apply unsquash_inj.
    rewrite !unsquash_squash.
(* Goal: @eq resource (NO Share.bot nsh1) (NO Share.bot bot_unreadable) *)
    f_equal.
    change (rmap_fmap (approx (n - d)) (approx (n - d))
             (rmap_fmap (approx (S n)) (approx (S n)) rm)) with
           ((rmap_fmap (approx (n - d)) (approx (n - d)) oo
              rmap_fmap (approx (S n)) (approx (S n))) rm).
    rewrite rmap_fmap_comp.
(* Goal: @eq resource (NO Share.bot nsh1) (NO Share.bot bot_unreadable) *)
    f_equal.
    + clear.
(* Goal: @eq nat (@level rmap ag_rmap m) (Init.Nat.add (S (Init.Nat.sub (@level rmap ag_rmap m) (S (@level rmap ag_rmap m')))) (@level rmap ag_rmap m')) *)
(* Goal: @ex rmap (fun m1 : rmap => and (@laterR rmap ag_rmap m m1) (@eq nat (@level rmap ag_rmap m1) (@level rmap ag_rmap m'))) *)
      assert (n-d <= (S n))%nat by omega.
      revert H; generalize (n-d)%nat (S n).
      clear.
(* Goal: forall (w : rmap) (loc : AV.address), @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (@core resource Join_resource Sep_resource (resource_at w loc))) (@core resource Join_resource Sep_resource (resource_at w loc)) *)
      intros.
      extensionality p.
      apply pred_ext'.  extensionality w.
      unfold compose, approx.
      apply prop_ext; simpl; intuition.
    + clear.
(* Goal: @eq nat (@level rmap ag_rmap m) (Init.Nat.add (S (Init.Nat.sub (@level rmap ag_rmap m) (S (@level rmap ag_rmap m')))) (@level rmap ag_rmap m')) *)
(* Goal: @ex rmap (fun m1 : rmap => and (@laterR rmap ag_rmap m m1) (@eq nat (@level rmap ag_rmap m1) (@level rmap ag_rmap m'))) *)
      assert (n-d <= (S n))%nat by omega.
      revert H; generalize (n-d)%nat (S n).
      clear.
(* Goal: forall (w : rmap) (loc : AV.address), @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (@core resource Join_resource Sep_resource (resource_at w loc))) (@core resource Join_resource Sep_resource (resource_at w loc)) *)
      intros.
      extensionality p.
      apply pred_ext'.  extensionality w.
      unfold compose, approx.
      apply prop_ext; simpl; intuition.
  Qed.

  Lemma unageN: forall n (phi': rmap),   exists phi, ageN n phi = Some phi'.
  Proof.
(* Goal: forall (n : nat) (phi' : rmap), @ex rmap (fun phi : rmap => @eq (option rmap) (@ageN rmap ag_rmap n phi) (@Some rmap phi')) *)
    intros n phi'.
    rewrite <- (squash_unsquash phi').
(* Goal: @ex rmap (fun phi : rmap => @eq (option rmap) (@ageN rmap ag_rmap n phi) (@Some rmap (squash (unsquash phi')))) *)
    destruct (unsquash phi'); clear phi'.
    exists (squash ((n+n0)%nat,r)).
(* Goal: @eq (option rmap) (@ageN rmap ag_rmap n (squash (@pair nat rmap' (Init.Nat.add n n0) r))) (@Some rmap (squash (@pair nat rmap' n0 r))) *)
    rewrite ageN_squash.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
    replace (n + n0 - n)%nat with n0 by omega; auto.
(* Goal: @eq nat (@level rmap ag_rmap m) (Init.Nat.add (S (Init.Nat.sub (@level rmap ag_rmap m) (S (@level rmap ag_rmap m')))) (@level rmap ag_rmap m')) *)
(* Goal: @ex rmap (fun m1 : rmap => and (@laterR rmap ag_rmap m m1) (@eq nat (@level rmap ag_rmap m1) (@level rmap ag_rmap m'))) *)
    omega.
  Qed.

  Lemma ex_level0: exists phi, age1 phi = None.
  Proof.
    Print sig.
    set (g := nil: ghost).
    set (m := (fun _ : AV.address => NO emptyshare nonreadable_emptyshare): AV.address -> resource).
    set (r := (m, g): rmap').
    exists (squash (0%nat, r)).
(* Goal: @eq (option rmap) (@age1 rmap ag_rmap (squash (@pair nat rmap' (S n) r0))) (@Some rmap r) *)
    rewrite rmap_age1_eq.
(* Goal: @eq (prod nat rmap') (unsquash (squash (@pair nat rmap' n (rmap_fmap (approx (S n)) (approx (S n)) r0)))) (@pair nat rmap' n r0) *)
    rewrite unsquash_squash.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
    auto.
  Qed.

  Lemma ex_level: forall n, exists phi, level phi = n.
  Proof.
(* Goal: forall (w : rmap) (loc : AV.address), @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (@core resource Join_resource Sep_resource (resource_at w loc))) (@core resource Join_resource Sep_resource (resource_at w loc)) *)
    intros.
(* Goal: @ex rmap (fun phi : rmap => @eq nat (@level rmap ag_rmap phi) n) *)
    destruct ex_level0 as [phi ?].
(* Goal: @ex rmap (fun phi : rmap => @eq nat (@level rmap ag_rmap phi) n) *)
    rewrite age1_level0 in H.
(* Goal: @ex rmap (fun phi : rmap => @eq nat (@level rmap ag_rmap phi) n) *)
    destruct (unageN n phi) as [phi' ?].
(* Goal: @ex rmap (fun phi : rmap => @eq nat (@level rmap ag_rmap phi) n) *)
    exists phi'.
(* Goal: @eq nat (@level rmap ag_rmap phi') n *)
    apply ageN_level in H0.
(* Goal: @eq nat (@level rmap ag_rmap m) (Init.Nat.add (S (Init.Nat.sub (@level rmap ag_rmap m) (S (@level rmap ag_rmap m')))) (@level rmap ag_rmap m')) *)
(* Goal: @ex rmap (fun m1 : rmap => and (@laterR rmap ag_rmap m m1) (@eq nat (@level rmap ag_rmap m1) (@level rmap ag_rmap m'))) *)
    omega.
  Qed.

Lemma YES_join_full: 
   forall sh rsh n P r2 r3,
       join (R.YES sh rsh n P) r2 r3 ->
       writable0_share sh ->
       exists sh2 rsh2, r2 = NO sh2 rsh2.
Proof.
(* Goal: forall (w : rmap) (loc : AV.address), @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (@core resource Join_resource Sep_resource (resource_at w loc))) (@core resource Join_resource Sep_resource (resource_at w loc)) *)
  intros.
(* Goal: @eq resource (YES sh1 rsh1 k pp) (NO Share.bot bot_unreadable) *)
  inv H. eauto.
  elimtype False; clear - RJ H0 rsh2.
(* Goal: False *)
  destruct RJ.
(* Goal: False *)
  destruct H0. destruct H0. destruct rsh2. subst sh sh3.
(* Goal: @identity share Share.Join_ba (Share.glb Share.Rsh sh2) *)
  rewrite Share.glb_commute, Share.distrib1 in H.
(* Goal: @identity share Share.Join_ba (Share.glb Share.Rsh sh2) *)
  rewrite Share.glb_commute.
(* Goal: @eq resource (resource_fmap (approx (@level rmap ag_rmap r0)) (approx (@level rmap ag_rmap r0)) (resource_at phi1 loc)) (resource_fmap (approx (@level rmap ag_rmap r)) (approx (@level rmap ag_rmap r)) (resource_at phi2 loc)) *)
  apply lub_bot_e in H. destruct H. rewrite H. apply bot_identity.
Qed.


Lemma YES_not_identity:
  forall sh rsh k Q, ~ identity (YES sh rsh k Q).
Proof.
(* Goal: forall (w : rmap) (loc : AV.address), @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (@core resource Join_resource Sep_resource (resource_at w loc))) (@core resource Join_resource Sep_resource (resource_at w loc)) *)
intros. intro.
(* Goal: @identity Share.t Share.Join_ba sh *)
apply identity_unit' in H.
(* Goal: or (@eq resource (resource_at phi l) (NO Share.bot bot_unreadable)) (@ex AV.kind (fun k : AV.kind => @ex preds (fun pds : preds => @eq resource (resource_at phi l) (PURE k pds)))) *)
unfold unit_for in H.
(* Goal: @eq resource (YES sh1 rsh1 k pp) (NO Share.bot bot_unreadable) *)
inv H.
(* Goal: False *)
apply share_self_join_bot in RJ; subst.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
apply bot_unreadable in rsh. auto.
Qed.

Lemma YES_overlap:
forall sh0 rsh0 sh1 rsh1 (phi0 phi1: rmap) loc k k' p p',
  joins phi0 phi1 ->
  phi1@loc = R.YES sh1 rsh1 k p -> 
  writable0_share sh1 ->
  phi0@loc = R.YES sh0 rsh0 k' p' ->
  False.
Proof.
(* Goal: forall (w : rmap) (loc : AV.address), @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (@core resource Join_resource Sep_resource (resource_at w loc))) (@core resource Join_resource Sep_resource (resource_at w loc)) *)
  intros.
(* Goal: False *)
  destruct H as [phi3 ?].
(* Goal: not (@identity resource Join_resource (YES sh rsh k Q)) *)
  generalize (resource_at_join _ _ _ loc H); intro.
(* Goal: False *)
  rewrite H2 in H3.
(* Goal: False *)
  rewrite H0 in H3.
(* Goal: False *)
  apply join_comm in H3.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
  apply YES_join_full in H3; auto.
(* Goal: False *)
  destruct H3 as [? [? H3]]. inv H3.
Qed.

Lemma necR_NOx:
   forall phi phi' l sh nsh, 
      necR phi phi' -> 
      phi@l = NO sh nsh -> 
      phi'@l = NO sh nsh.
Proof.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
induction 1; eauto.
(* Goal: @ex rmap (fun m1 : rmap => and (@laterR rmap ag_rmap m m1) (@eq nat (@level rmap ag_rmap m1) (@level rmap ag_rmap m'))) *)
(* Goal: @ex rmap (fun m1 : rmap => and (@laterR rmap ag_rmap m m1) (@eq nat (@level rmap ag_rmap m1) (@level rmap ag_rmap m'))) *)
unfold age in H; simpl in H.
(* Goal: forall _ : @eq resource (resource_at x l) (NO sh nsh), @eq resource (resource_at y l) (NO sh nsh) *)
revert H; rewrite rmap_age1_eq; unfold resource_at.
(* Goal: forall (_ : @eq (option rmap) (let (n0, x) := unsquash x in match n0 with | O => @None rmap | S n => @Some rmap (squash (@pair nat rmap' n x)) end) (@Some rmap y)) (_ : @eq resource (@fst (forall _ : AV.address, resource) ghost (@snd nat rmap' (unsquash x)) l) (NO sh nsh)), @eq resource (@fst (forall _ : AV.address, resource) ghost (@snd nat rmap' (unsquash y)) l) (NO sh nsh) *)
destruct (unsquash x).
(* Goal: @eq resource (YES sh1 rsh1 k pp) (NO Share.bot bot_unreadable) *)
intros; destruct n; inv H.
rewrite unsquash_squash; simpl in *; auto.
destruct r; simpl in *.
(* Goal: @eq resource (@compose AV.address resource resource (resource_fmap (approx n) (approx n)) f l) (f l) *)
unfold compose.
(* Goal: @identity share Share.Join_ba (Share.glb Share.Rsh b) *)
rewrite H0.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
auto.
Qed.

Ltac do_map_arg :=
match goal with |- ?a = ?b =>
  match a with context [map ?x _] =>
    match b with context [map ?y _] => replace y with x; auto end end end.

Lemma resource_at_approx:
  forall phi l,
      resource_fmap (approx (level phi)) (approx (level phi)) (phi @ l) = phi @ l.
Proof.
(* Goal: forall (w : rmap) (loc : AV.address), @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (@core resource Join_resource Sep_resource (resource_at w loc))) (@core resource Join_resource Sep_resource (resource_at w loc)) *)
intros. symmetry. rewrite rmap_level_eq. unfold resource_at.
(* Goal: forall (w : rmap) (loc : AV.address), @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (@core resource Join_resource Sep_resource (resource_at w loc))) (@core resource Join_resource Sep_resource (resource_at w loc)) *)
case_eq (unsquash phi); intros.
(* Goal: not (@identity share Share.Join_ba (Share.glb Share.Rsh (Share.lub a' (Share.glb Share.Rsh b)))) *)
simpl.
set (phi' := (squash (n, (resource_fmap (approx n) (approx n) oo fst r, snd r)))).
pose proof I.
(* Goal: not (@identity resource Join_resource (YES sh rsh k Q)) *)
generalize (unsquash_inj phi phi'); intro.
(* Goal: @ex rmap (fun phi1 : rmap => @ex rmap (fun phi2 : rmap => and (@join rmap Join_rmap phi1 phi2 phi) (and (@eq (forall _ : AV.address, resource) (resource_at phi1) f) (@eq ghost (ghost_of phi1) a)))) *)
spec H1.
replace (unsquash phi) with (unsquash (squash (unsquash phi))).
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
2: rewrite squash_unsquash; auto.
(* Goal: @eq resource (resource_fmap (approx (@level rmap ag_rmap r0)) (approx (@level rmap ag_rmap r0)) (resource_at phi1 loc)) (resource_fmap (approx (@level rmap ag_rmap r)) (approx (@level rmap ag_rmap r)) (resource_at phi2 loc)) *)
rewrite H.
unfold phi'.
(* Goal: @eq (prod nat rmap') (unsquash (squash (@pair nat rmap' n (rmap_fmap (approx (S n)) (approx (S n)) r0)))) (@pair nat rmap' n r0) *)
repeat rewrite unsquash_squash.
(* Goal: not (@identity share Share.Join_ba (Share.glb Share.Rsh (Share.lub a' (Share.glb Share.Rsh b)))) *)
simpl.
(* Goal: @eq resource (NO Share.bot nsh1) (NO Share.bot bot_unreadable) *)
f_equal.
(* Goal: not (@identity share Share.Join_ba (Share.glb Share.Rsh (Share.lub a' (Share.glb Share.Rsh b)))) *)
unfold rmap_fmap, compose; simpl.
(* Goal: @eq resource (NO Share.bot nsh1) (NO Share.bot bot_unreadable) *)
f_equal.
extensionality y.
(* Goal: @eq resource (resource_fmap (approx n) (approx n) (resource_fmap (approx (S n)) (approx (S n)) r0)) (resource_fmap (approx n) (approx n) r0) *)
rewrite resource_fmap_fmap.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
rewrite approx_oo_approx; auto.
unfold phi' in *; clear phi'.
(* Goal: False *)
subst.
(* Goal: @eq resource (r l) (r0 l) *)
(* Goal: @eq ghost (ghost_of a) (ghost_of b) *)
rewrite unsquash_squash in H.
(* Goal: not (@identity resource Join_resource (YES sh rsh k Q)) *)
injection H; clear H; intro.
pattern r at 1; rewrite <- H.
unfold rmap_fmap, compose.
(* Goal: @eq resource (resource_fmap (approx n) (approx n) (resource_fmap (approx (S n)) (approx (S n)) r0)) (resource_fmap (approx n) (approx n) r0) *)
simpl; rewrite resource_fmap_fmap.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
rewrite approx_oo_approx; auto.
Qed.

Lemma necR_resource_at:
  forall phi phi' loc r,
        necR phi phi' ->
         phi @ loc = resource_fmap (approx (level phi)) (approx (level phi)) r ->
         phi' @ loc = resource_fmap (approx (level phi')) (approx (level phi')) r.
Proof.
(* Goal: forall (w : rmap) (loc : AV.address), @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (@core resource Join_resource Sep_resource (resource_at w loc))) (@core resource Join_resource Sep_resource (resource_at w loc)) *)
intros.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
revert r loc H0; induction H; intros; auto.
(* Goal: @eq resource (resource_at y loc) (resource_fmap (approx (@level rmap ag_rmap y)) (approx (@level rmap ag_rmap y)) r) *)
unfold age in H.
(* Goal: @ex rmap (fun m1 : rmap => and (@laterR rmap ag_rmap m m1) (@eq nat (@level rmap ag_rmap m1) (@level rmap ag_rmap m'))) *)
(* Goal: @ex rmap (fun m1 : rmap => and (@laterR rmap ag_rmap m m1) (@eq nat (@level rmap ag_rmap m1) (@level rmap ag_rmap m'))) *)
simpl in H.
revert H H0; rewrite rmap_level_eq, rmap_age1_eq; unfold resource_at.
(* Goal: forall (w : rmap) (loc : AV.address), @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (@core resource Join_resource Sep_resource (resource_at w loc))) (@core resource Join_resource Sep_resource (resource_at w loc)) *)
 case_eq (unsquash x); intros.
(* Goal: @eq ghost (@snd (forall _ : AV.address, resource) ghost (@snd nat rmap' (unsquash phi'))) (ghost_fmap (approx (@fst nat rmap' (unsquash phi'))) (approx (@fst nat rmap' (unsquash phi'))) (@snd (forall _ : AV.address, resource) ghost r)) *)
destruct n; inv H0.
simpl in *.
(* Goal: not (@identity share Share.Join_ba (Share.glb Share.Rsh (Share.lub a' (Share.glb Share.Rsh b)))) *)
rewrite unsquash_squash; simpl.
destruct r0; simpl in *.
unfold compose in *.
(* Goal: @eq resource (resource_fmap (approx n) (approx n) (r0 loc)) (resource_fmap (approx n) (approx n) r) *)
rewrite H1; clear H1.
(* Goal: @eq resource (resource_fmap (approx n) (approx n) (resource_fmap (approx (S n)) (approx (S n)) r0)) (resource_fmap (approx n) (approx n) r0) *)
rewrite resource_fmap_fmap.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
rewrite approx_oo_approx'; auto.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
rewrite approx'_oo_approx; auto.
Qed.

Lemma necR_YES:
  forall phi phi' loc rsh sh k pp,
        necR phi phi' ->
         phi @ loc = YES rsh sh k pp ->
         phi' @ loc = YES rsh sh k (preds_fmap (approx (level phi')) (approx (level phi')) pp).
Proof.
(* Goal: forall (w : rmap) (loc : AV.address), @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (@core resource Join_resource Sep_resource (resource_at w loc))) (@core resource Join_resource Sep_resource (resource_at w loc)) *)
intros.
generalize (eq_sym (resource_at_approx phi loc));
(* Goal: not (@identity resource Join_resource (YES sh rsh k Q)) *)
pattern (phi @ loc) at 2; rewrite H0; intro.
(* Goal: @eq resource (resource_at phi' loc) (PURE k (preds_fmap (approx (@level rmap ag_rmap phi')) (approx (@level rmap ag_rmap phi')) pp)) *)
apply (necR_resource_at _ _ _ _ H H1).
Qed.

Lemma necR_PURE:
  forall phi phi' loc k pp,
        necR phi phi' ->
         phi @ loc = PURE k pp ->
         phi' @ loc = PURE k (preds_fmap (approx (level phi')) (approx (level phi')) pp).
Proof.
(* Goal: forall (w : rmap) (loc : AV.address), @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (@core resource Join_resource Sep_resource (resource_at w loc))) (@core resource Join_resource Sep_resource (resource_at w loc)) *)
  intros.
  generalize (eq_sym (resource_at_approx phi loc));
(* Goal: not (@identity resource Join_resource (YES sh rsh k Q)) *)
  pattern (phi @ loc) at 2; rewrite H0; intro.
(* Goal: @eq resource (resource_at phi' loc) (PURE k (preds_fmap (approx (@level rmap ag_rmap phi')) (approx (@level rmap ag_rmap phi')) pp)) *)
  apply (necR_resource_at _ _ _ _ H H1).
Qed.

Lemma necR_NO:
   forall phi phi' l sh nsh, necR phi phi' -> 
   (phi@l = NO sh nsh <-> phi'@l = NO sh nsh).
Proof.
(* Goal: @join (prod nat rmap') Join_nat_rmap' (@pair nat rmap' n phif') (@pair nat rmap' n phig') (@pair nat rmap' n phi') *)
  intros; split.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
  apply necR_NOx; auto.
(* Goal: forall (w : rmap) (loc : AV.address), @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (@core resource Join_resource Sep_resource (resource_at w loc))) (@core resource Join_resource Sep_resource (resource_at w loc)) *)
  intros.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
  case_eq (phi @ l); intros; auto.
(* Goal: not (@identity resource Join_resource (YES sh rsh k Q)) *)
  generalize (necR_NOx _ _ l _ _ H H1); intro. congruence.
(* Goal: @eq rmap' (rmap_fmap (approx n) (approx n) r0) r0 *)
  generalize (necR_YES _ _ _ _ _ _ _ H H1); congruence.
(* Goal: @eq rmap' (rmap_fmap (approx n) (approx n) r0) r0 *)
  generalize (necR_PURE _ _ _ _ _ H H1); congruence.
Qed.

Lemma resource_at_empty: forall phi, 
     identity phi ->
     forall l, phi @ l = NO Share.bot bot_unreadable \/ exists k, exists pds, phi @ l = PURE k pds.
Proof.
(* Goal: forall (w : rmap) (loc : AV.address), @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (@core resource Join_resource Sep_resource (resource_at w loc))) (@core resource Join_resource Sep_resource (resource_at w loc)) *)
  intros.
(* Goal: @identity Share.t Share.Join_ba sh *)
  apply identity_unit' in H.
(* Goal: or (@eq resource (resource_at phi l) (NO Share.bot bot_unreadable)) (@ex AV.kind (fun k : AV.kind => @ex preds (fun pds : preds => @eq resource (resource_at phi l) (PURE k pds)))) *)
  unfold unit_for in H.
(* Goal: not (@identity resource Join_resource (YES sh rsh k Q)) *)
  generalize (resource_at_join _ _ _ l H); intro.
(* Goal: or (@eq resource (resource_at phi l) (NO Share.bot bot_unreadable)) (@ex AV.kind (fun k : AV.kind => @ex preds (fun pds : preds => @eq resource (resource_at phi l) (PURE k pds)))) *)
  remember (phi @ l) as r.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
  destruct r; inv H0; eauto.
(* Goal: or (@eq resource (NO sh n) (NO Share.bot bot_unreadable)) (@ex AV.kind (fun k : AV.kind => @ex preds (fun pds : preds => @eq resource (NO sh n) (PURE k pds)))) *)
(* Goal: or (@eq resource (YES sh r k p) (NO Share.bot bot_unreadable)) (@ex AV.kind (fun k0 : AV.kind => @ex preds (fun pds : preds => @eq resource (YES sh r k p) (PURE k0 pds)))) *)
(* Goal: or (@eq resource (PURE k p) (NO Share.bot bot_unreadable)) (@ex AV.kind (fun k0 : AV.kind => @ex preds (fun pds : preds => @eq resource (PURE k p) (PURE k0 pds)))) *)
  left. clear - RJ.
(* Goal: False *)
  apply identity_unit_equiv in RJ; apply identity_share_bot in RJ; subst.
(* Goal: @eq resource (NO Share.bot nsh1) (NO Share.bot bot_unreadable) *)
  f_equal. apply proof_irr.
  clear - r RJ.
(* Goal: False *)
  apply share_self_join_bot in RJ. subst.
(* Goal: or (@eq resource (YES Share.bot r k p) (NO Share.bot bot_unreadable)) (@ex AV.kind (fun k0 : AV.kind => @ex preds (fun pds : preds => @eq resource (YES Share.bot r k p) (PURE k0 pds)))) *)
  contradiction (bot_unreadable r).
Qed.
Arguments resource_at_empty [phi] _ _.

Ltac inj_pair_tac :=
 match goal with H: (@existT ?U ?P ?p ?x = @existT _ _ _ ?y) |- _ =>
   generalize (@inj_pair2 U P p x y H); clear H; intro; try (subst x || subst y)
 end.

Lemma preds_fmap_NoneP:
  forall f1 f2, preds_fmap f1 f2 NoneP = NoneP.
Proof.
(* Goal: forall (w : rmap) (loc : AV.address), @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (@core resource Join_resource Sep_resource (resource_at w loc))) (@core resource Join_resource Sep_resource (resource_at w loc)) *)
intros.
(* Goal: @eq preds (preds_fmap f1 f2 NoneP) NoneP *)
unfold NoneP.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
auto.
Qed.

Lemma necR_YES':
   forall phi phi' loc rsh sh k,
         necR phi phi' -> (phi@loc = YES rsh sh k NoneP <-> phi'@loc = YES rsh sh k NoneP).
Proof.
(* Goal: forall (w : rmap) (loc : AV.address), @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (@core resource Join_resource Sep_resource (resource_at w loc))) (@core resource Join_resource Sep_resource (resource_at w loc)) *)
intros.
(* Goal: iff (@eq resource (resource_at phi loc) (YES rsh sh k NoneP)) (@eq resource (resource_at phi' loc) (YES rsh sh k NoneP)) *)
induction H.
(* Goal: iff (@ex preds (fun pp : preds => @eq resource (resource_at x loc) (PURE k pp))) (@ex preds (fun pp : preds => @eq resource (resource_at y loc) (PURE k pp))) *)
rename x into phi; rename y into phi'.
(* Goal: @ex rmap (fun m1 : rmap => and (@laterR rmap ag_rmap m m1) (@eq nat (@level rmap ag_rmap m1) (@level rmap ag_rmap m'))) *)
(* Goal: @ex rmap (fun m1 : rmap => and (@laterR rmap ag_rmap m m1) (@eq nat (@level rmap ag_rmap m1) (@level rmap ag_rmap m'))) *)
unfold age in H; simpl in H.
(* revert H; case_eq (age1 phi); intros; try discriminate. *)
(* Goal: @eq resource (YES sh1 rsh1 k pp) (NO Share.bot bot_unreadable) *)
inv H.
(* Goal: forall (w : rmap) (loc : AV.address), @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (@core resource Join_resource Sep_resource (resource_at w loc))) (@core resource Join_resource Sep_resource (resource_at w loc)) *)
split; intros.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
rewrite (necR_YES phi phi' loc rsh sh k NoneP); auto. constructor 1; auto.
rewrite rmap_age1_eq in *.
unfold resource_at in *.
(* Goal: forall (w : rmap) (loc : AV.address), @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (@core resource Join_resource Sep_resource (resource_at w loc))) (@core resource Join_resource Sep_resource (resource_at w loc)) *)
revert H1; case_eq (unsquash phi); simpl; intros.
(* Goal: @ex preds (fun pp : preds => @eq resource (@fst (forall _ : AV.address, resource) ghost r0 loc) (PURE k pp)) *)
destruct n; inv H1.
(* Goal: @ex rmap (fun m1 : rmap => and (@laterR rmap ag_rmap m m1) (@eq nat (@level rmap ag_rmap m1) (@level rmap ag_rmap m'))) *)
(* Goal: @ex rmap (fun m1 : rmap => and (@laterR rmap ag_rmap m m1) (@eq nat (@level rmap ag_rmap m1) (@level rmap ag_rmap m'))) *)
rewrite unsquash_squash in H. simpl in H.
(* Goal: @eq resource (r l) (r0 l) *)
(* Goal: @eq ghost (ghost_of a) (ghost_of b) *)
unfold compose in H.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
revert H; destruct (fst r loc); simpl; intros; auto.
(* Goal: @eq resource (YES sh1 rsh1 k pp) (NO Share.bot bot_unreadable) *)
destruct p; inv H.
(* Goal: @eq resource (NO Share.bot nsh1) (NO Share.bot bot_unreadable) *)
inj_pair_tac. f_equal. apply proof_irr.
(* Goal: @eq resource (NO Share.bot nsh1) (NO Share.bot bot_unreadable) *)
unfold NoneP; f_equal.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
auto.
(* Goal: @eq resource (YES sh1 rsh1 k pp) (NO Share.bot bot_unreadable) *)
inv H.
(* Goal: iff (@identity resource Join_resource (PURE k p)) True *)
intuition.
(* Goal: iff (@identity resource Join_resource (PURE k p)) True *)
intuition.
Qed.

Lemma necR_YES'':
   forall phi phi' loc rsh sh k,
         necR phi phi' ->
    ((exists pp, phi@loc = YES rsh sh k pp) <->
    (exists pp, phi'@loc = YES rsh sh k pp)).
Proof.
(* Goal: forall (w : rmap) (loc : AV.address), @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (@core resource Join_resource Sep_resource (resource_at w loc))) (@core resource Join_resource Sep_resource (resource_at w loc)) *)
intros.
(* Goal: iff (@ex preds (fun pp : preds => @eq resource (resource_at phi loc) (PURE k pp))) (@ex preds (fun pp : preds => @eq resource (resource_at phi' loc) (PURE k pp))) *)
induction H; try solve [intuition].
(* Goal: iff (@ex preds (fun pp : preds => @eq resource (resource_at x loc) (PURE k pp))) (@ex preds (fun pp : preds => @eq resource (resource_at y loc) (PURE k pp))) *)
rename x into phi; rename y into phi'.
(* Goal: iff (@ex preds (fun pp : preds => @eq resource (resource_at phi loc) (PURE k pp))) (@ex preds (fun pp : preds => @eq resource (resource_at phi' loc) (PURE k pp))) *)
revert H; unfold age; case_eq (age1 phi); intros; try discriminate.
(* Goal: @eq resource a b *)
inv H0.
simpl in *.
(* Goal: iff (@ex preds (fun pp : preds => @eq resource (resource_at phi loc) (PURE k pp))) (@ex preds (fun pp : preds => @eq resource (resource_at phi' loc) (PURE k pp))) *)
split; intros [pp ?].
+ econstructor;
  apply (necR_YES phi phi' loc rsh sh k pp).
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
  constructor 1; auto. auto.
+ rename phi' into r.
  rewrite rmap_age1_eq in *.
  unfold resource_at in *.
(* Goal: forall (w : rmap) (loc : AV.address), @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (@core resource Join_resource Sep_resource (resource_at w loc))) (@core resource Join_resource Sep_resource (resource_at w loc)) *)
  revert H; case_eq (unsquash phi); simpl; intros.
(* Goal: @ex preds (fun pp : preds => @eq resource (@fst (forall _ : AV.address, resource) ghost r0 loc) (PURE k pp)) *)
  destruct n; inv H1.
(* Goal: @ex preds (fun pp : preds => @eq resource (@fst (forall _ : AV.address, resource) ghost r0 loc) (PURE k pp)) *)
  rewrite unsquash_squash in H0. simpl in H0.
(* Goal: @ex preds (fun pp : preds => @eq resource (@fst (forall _ : AV.address, resource) ghost r0 loc) (PURE k pp)) *)
  unfold compose in H0.
(* Goal: @eq resource a b *)
  revert H0; destruct (fst r0 loc); simpl; intros; inv H0.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
  econstructor; proof_irr; eauto.
Qed.

Lemma necR_PURE':
   forall phi phi' loc k,
         necR phi phi' ->
    ((exists pp, phi@loc = PURE k pp) <->
    (exists pp, phi'@loc = PURE k pp)).
Proof.
(* Goal: forall (w : rmap) (loc : AV.address), @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (@core resource Join_resource Sep_resource (resource_at w loc))) (@core resource Join_resource Sep_resource (resource_at w loc)) *)
intros.
(* Goal: iff (@ex preds (fun pp : preds => @eq resource (resource_at phi loc) (PURE k pp))) (@ex preds (fun pp : preds => @eq resource (resource_at phi' loc) (PURE k pp))) *)
induction H; try solve [intuition].
(* Goal: iff (@ex preds (fun pp : preds => @eq resource (resource_at x loc) (PURE k pp))) (@ex preds (fun pp : preds => @eq resource (resource_at y loc) (PURE k pp))) *)
rename x into phi; rename y into phi'.
(* Goal: iff (@ex preds (fun pp : preds => @eq resource (resource_at phi loc) (PURE k pp))) (@ex preds (fun pp : preds => @eq resource (resource_at phi' loc) (PURE k pp))) *)
revert H; unfold age; case_eq (age1 phi); intros; try discriminate.
(* Goal: @eq resource a b *)
inv H0.
simpl in *.
(* Goal: iff (@ex preds (fun pp : preds => @eq resource (resource_at phi loc) (PURE k pp))) (@ex preds (fun pp : preds => @eq resource (resource_at phi' loc) (PURE k pp))) *)
split; intros [pp ?].
+ econstructor;
  apply (necR_PURE phi phi' loc k pp).
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
  constructor 1; auto. auto.
+ rename phi' into r.
  rewrite rmap_age1_eq in *.
  unfold resource_at in *.
(* Goal: forall (w : rmap) (loc : AV.address), @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (@core resource Join_resource Sep_resource (resource_at w loc))) (@core resource Join_resource Sep_resource (resource_at w loc)) *)
  revert H; case_eq (unsquash phi); simpl; intros.
(* Goal: @ex preds (fun pp : preds => @eq resource (@fst (forall _ : AV.address, resource) ghost r0 loc) (PURE k pp)) *)
  destruct n; inv H1.
(* Goal: @ex preds (fun pp : preds => @eq resource (@fst (forall _ : AV.address, resource) ghost r0 loc) (PURE k pp)) *)
  rewrite unsquash_squash in H0. simpl in H0.
(* Goal: @ex preds (fun pp : preds => @eq resource (@fst (forall _ : AV.address, resource) ghost r0 loc) (PURE k pp)) *)
  unfold compose in H0.
(* Goal: @eq resource a b *)
  revert H0; destruct (fst r0 loc); simpl; intros; inv H0.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
  eauto.
Qed.


Lemma resource_at_join_sub:
  forall phi1 phi2 l,
       join_sub phi1 phi2 -> join_sub (phi1@l) (phi2@l).
Proof.
(* Goal: forall (w : rmap) (loc : AV.address), @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (@core resource Join_resource Sep_resource (resource_at w loc))) (@core resource Join_resource Sep_resource (resource_at w loc)) *)
intros.
(* Goal: @join_sub resource Join_resource (resource_at phi1 l) (resource_at phi2 l) *)
destruct H as [phi ?].
(* Goal: not (@identity resource Join_resource (YES sh rsh k Q)) *)
generalize (resource_at_join _ _ _ l H); intro.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
econstructor; eauto.
Qed.

Lemma age1_res_option: forall phi phi' loc,
     age1 phi = Some phi' -> res_option (phi @ loc) = res_option (phi' @ loc).
  Proof.
(* Goal: not (@identity share Share.Join_ba (Share.glb Share.Rsh (Share.lub a' (Share.glb Share.Rsh b)))) *)
    unfold res_option, resource_at; simpl.
(* Goal: forall (phi phi' : rmap) (loc : AV.address) (_ : @eq (option rmap) (@age1 rmap ag_rmap phi) (@Some rmap phi')), @eq (option (prod rshare AV.kind)) match @fst (forall _ : AV.address, resource) ghost (@snd nat rmap' (unsquash phi)) loc with | NO sh n => @None (prod rshare AV.kind) | YES sh rsh k p => @Some (prod rshare AV.kind) (@pair rshare AV.kind (@readable_part sh rsh) k) | PURE k p => @None (prod rshare AV.kind) end match @fst (forall _ : AV.address, resource) ghost (@snd nat rmap' (unsquash phi')) loc with | NO sh n => @None (prod rshare AV.kind) | YES sh rsh k p => @Some (prod rshare AV.kind) (@pair rshare AV.kind (@readable_part sh rsh) k) | PURE k p => @None (prod rshare AV.kind) end *)
   rewrite rmap_age1_eq; intros phi1 phi2 l.
(* Goal: forall (w : rmap) (loc : AV.address), @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (@core resource Join_resource Sep_resource (resource_at w loc))) (@core resource Join_resource Sep_resource (resource_at w loc)) *)
 case_eq (unsquash phi1); intros. destruct n; inv H0.
(* Goal: @eq (prod nat rmap') (unsquash (squash (@pair nat rmap' n (rmap_fmap (approx (S n)) (approx (S n)) r0)))) (@pair nat rmap' n r0) *)
 rewrite unsquash_squash.
   destruct r;
(* Goal: not (@identity share Share.Join_ba (Share.glb Share.Rsh (Share.lub a' (Share.glb Share.Rsh b)))) *)
    simpl.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
   unfold compose. destruct (r l); simpl; auto.
Qed.

Lemma necR_res_option:
  forall (phi phi' : rmap) (loc : AV.address),
  necR phi phi' -> res_option (phi @ loc) = res_option (phi' @ loc).
Proof.
(* Goal: forall (w : rmap) (loc : AV.address), @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (@core resource Join_resource Sep_resource (resource_at w loc))) (@core resource Join_resource Sep_resource (resource_at w loc)) *)
  intros.
(* Goal: forall (w : rmap) (loc : AV.address), @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (@core resource Join_resource Sep_resource (resource_at w loc))) (@core resource Join_resource Sep_resource (resource_at w loc)) *)
  case_eq (phi @ loc); intros.
(* Goal: @eq rmap' (rmap_fmap (approx n) (approx n) r0) r0 *)
  rewrite (necR_NO _ _ _ _ n H) in H0. congruence.
(* Goal: @eq (option (prod rshare AV.kind)) (res_option (YES sh r k p)) (res_option (resource_at phi' loc)) *)
(* Goal: @eq (option (prod rshare AV.kind)) (res_option (PURE k p)) (res_option (resource_at phi' loc)) *)
  destruct p.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
  rewrite (necR_YES phi phi' loc _ _ _ _ H H0); auto.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
  rewrite (necR_PURE phi phi' loc _ _ H H0); auto.
Qed.


Lemma age1_resource_at:
     forall phi phi',
          age1 phi = Some phi' ->
         forall loc r,
          phi @ loc = resource_fmap (approx (level phi)) (approx (level phi)) r ->
          phi' @ loc = resource_fmap (approx (level phi')) (approx (level phi')) r.
Proof.
(* Goal: forall (phi phi' : rmap) (_ : @eq (option rmap) (@age1 rmap ag_rmap phi) (@Some rmap phi')) (loc : AV.address) (r : resource) (_ : @eq resource (resource_at phi loc) (resource_fmap (approx (@level rmap ag_rmap phi)) (approx (@level rmap ag_rmap phi)) r)), @eq resource (resource_at phi' loc) (resource_fmap (approx (@level rmap ag_rmap phi')) (approx (@level rmap ag_rmap phi')) r) *)
   unfold resource_at; rewrite rmap_age1_eq, rmap_level_eq.
(* Goal: forall (w : rmap) (loc : AV.address), @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (@core resource Join_resource Sep_resource (resource_at w loc))) (@core resource Join_resource Sep_resource (resource_at w loc)) *)
intros until phi'; case_eq (unsquash phi); intros.
simpl in *.
(* Goal: @eq ghost (@snd (forall _ : AV.address, resource) ghost (@snd nat rmap' (unsquash phi'))) (ghost_fmap (approx (@fst nat rmap' (unsquash phi'))) (approx (@fst nat rmap' (unsquash phi'))) (@snd (forall _ : AV.address, resource) ghost r)) *)
destruct n; inv H0.
(* Goal: @eq (prod nat rmap') (unsquash (squash (@pair nat rmap' n (rmap_fmap (approx (S n)) (approx (S n)) r0)))) (@pair nat rmap' n r0) *)
rewrite unsquash_squash.
destruct r; simpl in *.
(* Goal: @eq resource (@compose AV.address resource resource (resource_fmap (approx n) (approx n)) r loc) (resource_fmap (approx n) (approx n) r0) *)
unfold compose; rewrite H1.
(* Goal: @eq resource (resource_fmap (approx n) (approx n) (resource_fmap (approx (S n)) (approx (S n)) r0)) (resource_fmap (approx n) (approx n) r0) *)
rewrite resource_fmap_fmap.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
rewrite approx_oo_approx'; auto.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
rewrite approx'_oo_approx; auto.
Qed.


Lemma age1_ghost_of:
     forall phi phi',
          age1 phi = Some phi' ->
          ghost_of phi' = ghost_fmap (approx (level phi')) (approx (level phi')) (ghost_of phi).
Proof.
(* Goal: forall (phi phi' : rmap) (_ : @eq (option rmap) (@age1 rmap ag_rmap phi) (@Some rmap phi')), @eq ghost (ghost_of phi') (ghost_fmap (approx (@level rmap ag_rmap phi')) (approx (@level rmap ag_rmap phi')) (ghost_of phi)) *)
unfold ghost_of; rewrite rmap_age1_eq, rmap_level_eq.
(* Goal: forall (w : rmap) (loc : AV.address), @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (@core resource Join_resource Sep_resource (resource_at w loc))) (@core resource Join_resource Sep_resource (resource_at w loc)) *)
intros until phi'; case_eq (unsquash phi); intros.
simpl in *.
(* Goal: @eq ghost (@snd (forall _ : AV.address, resource) ghost (@snd nat rmap' (unsquash phi'))) (ghost_fmap (approx (@fst nat rmap' (unsquash phi'))) (approx (@fst nat rmap' (unsquash phi'))) (@snd (forall _ : AV.address, resource) ghost r)) *)
destruct n; inv H0.
(* Goal: @eq (prod nat rmap') (unsquash (squash (@pair nat rmap' n (rmap_fmap (approx (S n)) (approx (S n)) r0)))) (@pair nat rmap' n r0) *)
rewrite unsquash_squash.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
destruct r; auto.
Qed.

Lemma ghost_fmap_join: forall a b c f g, join a b c ->
  join (ghost_fmap f g a) (ghost_fmap f g b) (ghost_fmap f g c).
Proof.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
  induction 1; constructor; auto.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
  inv H; constructor; auto.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
  destruct a0, a4, a5; inv H1; constructor; auto.
  simpl in *; inv H2; constructor; auto.
Qed.

Lemma age1_ghost_of_identity:
  forall phi phi', age1 phi = Some phi' ->
               (identity (ghost_of phi) <-> identity (ghost_of phi')).
Proof.
(* Goal: forall (w : rmap) (loc : AV.address), @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (@core resource Join_resource Sep_resource (resource_at w loc))) (@core resource Join_resource Sep_resource (resource_at w loc)) *)
 intros.
(* Goal: iff (@identity ghost ghost_join (ghost_of phi)) (@identity ghost ghost_join (ghost_of phi')) *)
 rewrite (age1_ghost_of _ _ H).
(* Goal: iff (@identity resource Join_resource (NO sh n)) (@identity Share.t Share.Join_ba sh) *)
 split; intro.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
 - replace (ghost_fmap _ _ _) with (ghost_of phi); auto.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
   rewrite (identity_core H0), ghost_core; auto.
 - replace (ghost_of phi) with (core (ghost_of phi)); [apply core_identity|].
(* Goal: @eq ghost (@core ghost ghost_join Sep_ghost (ghost_of phi)) (ghost_of phi) *)
   apply identity_core in H0.
   rewrite ghost_core in *; destruct (ghost_of phi); auto; discriminate.
Qed.

Lemma age1_YES: forall phi phi' l rsh sh k ,
  age1 phi = Some phi' -> (phi @ l = YES rsh sh k NoneP <-> phi' @ l = YES rsh sh k NoneP).
Proof.
(* Goal: forall (w : rmap) (loc : AV.address), @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (@core resource Join_resource Sep_resource (resource_at w loc))) (@core resource Join_resource Sep_resource (resource_at w loc)) *)
intros.
(* Goal: iff (@eq resource (resource_at phi l) (YES rsh sh k NoneP)) (@eq resource (resource_at phi' l) (YES rsh sh k NoneP)) *)
apply necR_YES'.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
constructor 1; auto.
Qed.

Lemma age1_YES': forall phi phi' l rsh sh k ,
  age1 phi = Some phi' -> ((exists P, phi @ l = YES rsh sh k P) <-> exists P, phi' @ l = YES rsh sh k P).
Proof.
(* Goal: forall (w : rmap) (loc : AV.address), @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (@core resource Join_resource Sep_resource (resource_at w loc))) (@core resource Join_resource Sep_resource (resource_at w loc)) *)
intros.
(* Goal: iff (@ex preds (fun P : preds => @eq resource (resource_at phi l) (YES rsh sh k P))) (@ex preds (fun P : preds => @eq resource (resource_at phi' l) (YES rsh sh k P))) *)
apply necR_YES''.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
constructor 1; auto.
Qed.

Lemma age1_NO: forall phi phi' l sh nsh,
  age1 phi = Some phi' -> (phi @ l = NO sh nsh <-> phi' @ l = NO sh nsh).
Proof.
(* Goal: forall (w : rmap) (loc : AV.address), @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (@core resource Join_resource Sep_resource (resource_at w loc))) (@core resource Join_resource Sep_resource (resource_at w loc)) *)
intros.
(* Goal: iff (@eq resource (resource_at phi l) (NO sh nsh)) (@eq resource (resource_at phi' l) (NO sh nsh)) *)
apply necR_NO.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
constructor 1; auto.
Qed.

Lemma age1_PURE: forall phi phi' l k ,
  age1 phi = Some phi' -> ((exists P, phi @ l = PURE k P) <-> exists P, phi' @ l = PURE k P).
Proof.
(* Goal: forall (w : rmap) (loc : AV.address), @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (@core resource Join_resource Sep_resource (resource_at w loc))) (@core resource Join_resource Sep_resource (resource_at w loc)) *)
  intros.
(* Goal: iff (@ex preds (fun P : preds => @eq resource (resource_at phi l) (PURE k P))) (@ex preds (fun P : preds => @eq resource (resource_at phi' l) (PURE k P))) *)
  apply necR_PURE'.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
  constructor 1; auto.
Qed.

Lemma necR_ghost_of:
  forall phi phi',
        necR phi phi' ->
         ghost_of phi' = ghost_fmap (approx (level phi')) (approx (level phi')) (ghost_of phi).
Proof.
(* Goal: forall (phi phi' : rmap) (_ : @necR rmap ag_rmap phi phi'), @eq ghost (ghost_of phi') (ghost_fmap (approx (@level rmap ag_rmap phi')) (approx (@level rmap ag_rmap phi')) (ghost_of phi)) *)
  induction 1.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
  - apply age1_ghost_of; auto.
  - symmetry; apply ghost_of_approx.
  - rewrite IHclos_refl_trans2, IHclos_refl_trans1, ghost_fmap_fmap.
(* Goal: @eq ghost (ghost_fmap (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx (@level rmap ag_rmap z)) (approx (@level rmap ag_rmap y))) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx (@level rmap ag_rmap y)) (approx (@level rmap ag_rmap z))) (ghost_of x)) (ghost_fmap (approx (@level rmap ag_rmap z)) (approx (@level rmap ag_rmap z)) (ghost_of x)) *)
    apply necR_level in H0.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
    rewrite approx_oo_approx', approx'_oo_approx; auto.
Qed.

Lemma empty_NO: forall r, identity r -> r = NO Share.bot bot_unreadable \/ exists k, exists pds, r = PURE k pds.
Proof.
(* Goal: forall (w : rmap) (loc : AV.address), @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (@core resource Join_resource Sep_resource (resource_at w loc))) (@core resource Join_resource Sep_resource (resource_at w loc)) *)
intros.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
destruct r; auto.
(* Goal: or (@eq resource (NO sh n) (NO Share.bot bot_unreadable)) (@ex AV.kind (fun k : AV.kind => @ex preds (fun pds : preds => @eq resource (NO sh n) (PURE k pds)))) *)
(* Goal: or (@eq resource (YES sh r k p) (NO Share.bot bot_unreadable)) (@ex AV.kind (fun k0 : AV.kind => @ex preds (fun pds : preds => @eq resource (YES sh r k p) (PURE k0 pds)))) *)
(* Goal: or (@eq resource (PURE k p) (NO Share.bot bot_unreadable)) (@ex AV.kind (fun k0 : AV.kind => @ex preds (fun pds : preds => @eq resource (PURE k p) (PURE k0 pds)))) *)
left. f_equal. apply identity_unit' in H. inv H.
(* Goal: @eq resource (NO sh n) (NO Share.bot bot_unreadable) *)
(* Goal: or (@eq resource (YES sh r k p) (NO Share.bot bot_unreadable)) (@ex AV.kind (fun k0 : AV.kind => @ex preds (fun pds : preds => @eq resource (YES sh r k p) (PURE k0 pds)))) *)
(* Goal: or (@eq resource (PURE k p) (NO Share.bot bot_unreadable)) (@ex AV.kind (fun k0 : AV.kind => @ex preds (fun pds : preds => @eq resource (PURE k p) (PURE k0 pds)))) *)
  apply identity_unit_equiv in RJ. apply identity_share_bot in RJ. subst.
(* Goal: @eq resource (NO Share.bot nsh1) (NO Share.bot bot_unreadable) *)
 f_equal. apply proof_irr.
(* Goal: or (@eq resource (YES sh r k p) (NO Share.bot bot_unreadable)) (@ex AV.kind (fun k0 : AV.kind => @ex preds (fun pds : preds => @eq resource (YES sh r k p) (PURE k0 pds)))) *)
(* Goal: or (@eq resource (PURE k p) (NO Share.bot bot_unreadable)) (@ex AV.kind (fun k0 : AV.kind => @ex preds (fun pds : preds => @eq resource (PURE k p) (PURE k0 pds)))) *)
unfold identity in H.
(* Goal: False *)
specialize ( H (NO Share.bot bot_unreadable) (YES sh r k p)).
(* Goal: False *)
spec H.
(* Goal: @join resource Join_resource (YES sh r k p) (NO Share.bot bot_unreadable) (YES sh r k p) *)
(* Goal: or (@eq resource (YES sh r k p) (NO Share.bot bot_unreadable)) (@ex AV.kind (fun k0 : AV.kind => @ex preds (fun pds : preds => @eq resource (YES sh r k p) (PURE k0 pds)))) *)
(* Goal: or (@eq resource (PURE k p) (NO Share.bot bot_unreadable)) (@ex AV.kind (fun k0 : AV.kind => @ex preds (fun pds : preds => @eq resource (PURE k p) (PURE k0 pds)))) *)
apply res_join_NO2.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
auto.
(* Goal: @eq resource (YES sh1 rsh1 k pp) (NO Share.bot bot_unreadable) *)
inv H.
(* Goal: or (@eq resource (PURE k p) (NO Share.bot bot_unreadable)) (@ex AV.kind (fun k0 : AV.kind => @ex preds (fun pds : preds => @eq resource (PURE k p) (PURE k0 pds)))) *)
right. exists k. exists p. trivial.
Qed.

Lemma level_age_fash:
  forall m m': rmap, level m = S (level m') -> exists m1, age m m1.
Proof.
(* Goal: forall (w : rmap) (loc : AV.address), @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (@core resource Join_resource Sep_resource (resource_at w loc))) (@core resource Join_resource Sep_resource (resource_at w loc)) *)
  intros.
(* Goal: forall (w : rmap) (loc : AV.address), @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (@core resource Join_resource Sep_resource (resource_at w loc))) (@core resource Join_resource Sep_resource (resource_at w loc)) *)
  case_eq (age1 m); intros.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
  exists r. auto.
(* Goal: @ex rmap (fun m1 : rmap => and (@laterR rmap ag_rmap m m1) (@eq nat (@level rmap ag_rmap m1) (@level rmap ag_rmap m'))) *)
  elimtype False.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
  eapply age1None_levelS_absurd in H0; eauto.
Qed.

Lemma level_later_fash:
 forall m m': rmap, (level m > level m')%nat  -> exists m1, laterR m m1 /\ level m1 = level m'.
Proof.
(* Goal: forall (w : rmap) (loc : AV.address), @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (@core resource Join_resource Sep_resource (resource_at w loc))) (@core resource Join_resource Sep_resource (resource_at w loc)) *)
  intros.
  assert (exists k, level m = S k + level m')%nat.
    exists (level m - S (level m'))%nat.
(* Goal: @eq nat (@level rmap ag_rmap m) (Init.Nat.add (S (Init.Nat.sub (@level rmap ag_rmap m) (S (@level rmap ag_rmap m')))) (@level rmap ag_rmap m')) *)
(* Goal: @ex rmap (fun m1 : rmap => and (@laterR rmap ag_rmap m m1) (@eq nat (@level rmap ag_rmap m1) (@level rmap ag_rmap m'))) *)
    omega.
(* Goal: @ex rmap (fun m1 : rmap => and (@laterR rmap ag_rmap m m1) (@eq nat (@level rmap ag_rmap m1) (@level rmap ag_rmap m'))) *)
  clear H; destruct H0 as [k ?].
(* Goal: forall (w : rmap) (loc : AV.address), @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (@core resource Join_resource Sep_resource (resource_at w loc))) (@core resource Join_resource Sep_resource (resource_at w loc)) *)
  revert m H; induction k; intros.
(* Goal: @ex rmap (fun m1 : rmap => and (@laterR rmap ag_rmap m m1) (@eq nat (@level rmap ag_rmap m1) (@level rmap ag_rmap m'))) *)
(* Goal: @ex rmap (fun m1 : rmap => and (@laterR rmap ag_rmap m m1) (@eq nat (@level rmap ag_rmap m1) (@level rmap ag_rmap m'))) *)
  simpl in H.
(* Goal: @ex rmap (fun m1 : rmap => and (@laterR rmap ag_rmap m m1) (@eq nat (@level rmap ag_rmap m1) (@level rmap ag_rmap m'))) *)
(* Goal: @ex rmap (fun m1 : rmap => and (@laterR rmap ag_rmap m m1) (@eq nat (@level rmap ag_rmap m1) (@level rmap ag_rmap m'))) *)
  destruct (level_age_fash _ _ H) as [m1 ?].
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
  exists m1; split; auto.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
  constructor 1; auto.
(* Goal: @eq nat (@level rmap ag_rmap m') (@level rmap ag_rmap m') *)
(* Goal: @ex rmap (fun m1 : rmap => and (@laterR rmap ag_rmap m m1) (@eq nat (@level rmap ag_rmap m1) (@level rmap ag_rmap m'))) *)
  apply age_level in H0. rewrite H in H0. inv H0. trivial.
(* Goal: forall (w : rmap) (loc : AV.address), @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (@core resource Join_resource Sep_resource (resource_at w loc))) (@core resource Join_resource Sep_resource (resource_at w loc)) *)
  case_eq (age1 m); intros.
(* Goal: @ex rmap (fun m1 : rmap => and (@laterR rmap ag_rmap m m1) (@eq nat (@level rmap ag_rmap m1) (@level rmap ag_rmap m'))) *)
(* Goal: @ex rmap (fun m1 : rmap => and (@laterR rmap ag_rmap m m1) (@eq nat (@level rmap ag_rmap m1) (@level rmap ag_rmap m'))) *)
  specialize ( IHk r).
  rewrite <- ageN1 in H0.
(* Goal: not (@identity resource Join_resource (YES sh rsh k Q)) *)
  generalize (ageN_level _ _ _ H0); intro.
(* Goal: @eq nat (@level rmap ag_rmap m) (Init.Nat.add (S (Init.Nat.sub (@level rmap ag_rmap m) (S (@level rmap ag_rmap m')))) (@level rmap ag_rmap m')) *)
(* Goal: @ex rmap (fun m1 : rmap => and (@laterR rmap ag_rmap m m1) (@eq nat (@level rmap ag_rmap m1) (@level rmap ag_rmap m'))) *)
  spec IHk; try omega.
(* Goal: @ex rmap (fun m1 : rmap => and (@laterR rmap ag_rmap m m1) (@eq nat (@level rmap ag_rmap m1) (@level rmap ag_rmap m'))) *)
(* Goal: @ex rmap (fun m1 : rmap => and (@laterR rmap ag_rmap m m1) (@eq nat (@level rmap ag_rmap m1) (@level rmap ag_rmap m'))) *)
  destruct IHk as [m1 [? ?]].
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
  exists m1; split; auto.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
  econstructor 2; eauto.
(* Goal: clos_trans rmap (@age rmap ag_rmap) m r *)
(* Goal: @ex rmap (fun m1 : rmap => and (@laterR rmap ag_rmap m m1) (@eq nat (@level rmap ag_rmap m1) (@level rmap ag_rmap m'))) *)
  rewrite ageN1 in H0.
(* Goal: clos_trans rmap (@age rmap ag_rmap) m r *)
(* Goal: @ex rmap (fun m1 : rmap => and (@laterR rmap ag_rmap m m1) (@eq nat (@level rmap ag_rmap m1) (@level rmap ag_rmap m'))) *)
  constructor 1.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
  auto.
(* Goal: @ex rmap (fun m1 : rmap => and (@laterR rmap ag_rmap m m1) (@eq nat (@level rmap ag_rmap m1) (@level rmap ag_rmap m'))) *)
  elimtype False.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
  eapply age1None_levelS_absurd in H0; eauto.
Qed.

Lemma resource_at_constructive_joins2:
  forall phi1 phi2,
       level phi1 = level phi2 ->
       (forall loc, constructive_joins (phi1 @ loc) (phi2 @ loc)) ->
       constructive_joins (ghost_of phi1) (ghost_of phi2) ->
         constructive_joins phi1 phi2.
Proof.
intros ? ? ? H0 Hg.
pose proof I.
destruct Hg.
destruct (make_rmap (fun loc => proj1_sig (H0 loc)) x (level phi1)) as [phi' [? [? ?]]].
clear H1.
unfold compose; extensionality loc.
(*specialize ( H0 loc). *)
(* Goal: @eq ghost (ghost_fmap (approx n) (approx n) g) g *)
destruct (H0 loc) as [? H1]. clear H0.
(* Goal: not (@identity share Share.Join_ba (Share.glb Share.Rsh (Share.lub a' (Share.glb Share.Rsh b)))) *)
simpl.
symmetry.
(* Goal: forall (w : rmap) (loc : AV.address), @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (@core resource Join_resource Sep_resource (resource_at w loc))) (@core resource Join_resource Sep_resource (resource_at w loc)) *)
revert H1; case_eq (phi1 @ loc); intros.
(* Goal: @eq resource (YES sh1 rsh1 k pp) (NO Share.bot bot_unreadable) *)
inv H1. reflexivity.
pose proof (resource_at_approx phi2 loc). rewrite <- H4 in H1. simpl in H1.
(* Goal: forall (w : rmap) (loc : AV.address), @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (@core resource Join_resource Sep_resource (resource_at w loc))) (@core resource Join_resource Sep_resource (resource_at w loc)) *)
injection H1; intros.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
simpl; f_equal; auto. rewrite H; auto.
(* Goal: @eq resource (YES sh1 rsh1 k pp) (NO Share.bot bot_unreadable) *)
inv H1.
pose proof (resource_at_approx phi1 loc). rewrite H0 in H1. simpl in H1.
(* Goal: forall (w : rmap) (loc : AV.address), @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (@core resource Join_resource Sep_resource (resource_at w loc))) (@core resource Join_resource Sep_resource (resource_at w loc)) *)
injection H1; intros.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
simpl; f_equal; auto.
(* Goal: @eq resource (NO Share.bot nsh1) (NO Share.bot bot_unreadable) *)
simpl; f_equal.
pose proof (resource_at_approx phi1 loc). rewrite H0 in H1. simpl in H1.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
injection H1; intros; auto.
(* Goal: @eq resource (YES sh1 rsh1 k pp) (NO Share.bot bot_unreadable) *)
inv H1.
(* Goal: @eq resource (NO Share.bot nsh1) (NO Share.bot bot_unreadable) *)
simpl; f_equal.
pose proof (resource_at_approx phi1 loc). rewrite H0 in H1. simpl in H1.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
injection H1; intros; auto.
eapply ghost_same_level_gen.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
rewrite ghost_of_approx, H, ghost_of_approx; auto.
(*  End of make_rmap proof *)
(* Goal: @ex rmap (fun phi : rmap => @eq nat (@level rmap ag_rmap phi) n) *)
exists phi'.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
apply resource_at_join2; auto.
(* Goal: @eq rmap' (rmap_fmap (approx n) (approx n) r0) r0 *)
congruence.
(* Goal: forall (w : rmap) (loc : AV.address), @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (@core resource Join_resource Sep_resource (resource_at w loc))) (@core resource Join_resource Sep_resource (resource_at w loc)) *)
intros.
rewrite H3.
destruct (H0 loc).
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
simpl; auto.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
rewrite H4; auto.
Qed.

Lemma resource_at_joins2:
  forall phi1 phi2,
       level phi1 = level phi2 ->
       (forall loc, constructive_joins (phi1 @ loc) (phi2 @ loc)) ->
       constructive_joins (ghost_of phi1) (ghost_of phi2) ->
         joins phi1 phi2.
Proof.
(* Goal: forall (w : rmap) (loc : AV.address), @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (@core resource Join_resource Sep_resource (resource_at w loc))) (@core resource Join_resource Sep_resource (resource_at w loc)) *)
  intros.
(* Goal: @joins rmap Join_rmap phi1 phi2 *)
  apply cjoins_joins.
(* Goal: @eq nat (@level rmap ag_rmap m') (@level rmap ag_rmap m') *)
(* Goal: @ex rmap (fun m1 : rmap => and (@laterR rmap ag_rmap m m1) (@eq nat (@level rmap ag_rmap m1) (@level rmap ag_rmap m'))) *)
  apply resource_at_constructive_joins2; trivial.
Qed.

Definition no_preds (r: resource) :=
   match r with NO _ _ => True | YES _ _ _ pp => pp=NoneP | PURE _ pp => pp=NoneP end.

Lemma remake_rmap:
  forall (f: AV.address -> resource) g,
       forall n,
       (forall l, (exists m, level m = n /\ f l = m @ l) \/ no_preds (f l)) ->
       ghost_fmap (approx n) (approx n) g = g ->
       {phi: rmap | level phi = n /\ resource_at phi = f /\ ghost_of phi = g}.
Proof.
(* Goal: forall (w : rmap) (loc : AV.address), @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (@core resource Join_resource Sep_resource (resource_at w loc))) (@core resource Join_resource Sep_resource (resource_at w loc)) *)
  intros.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
  apply make_rmap; auto.
(* Goal: @eq (forall _ : AV.address, resource) (@compose AV.address resource resource (resource_fmap (approx n) (approx n)) f) f *)
  extensionality l.
(* Goal: @eq resource (@compose AV.address resource resource (resource_fmap (approx n) (approx n)) f l) (f l) *)
  unfold compose.
(* Goal: @eq resource (resource_fmap (approx n) (approx n) (f l)) (f l) *)
  destruct (H l); clear H.
  destruct H1 as [m [?  ?]].
(* Goal: @eq resource (resource_fmap (approx n) (approx n) (f l)) (f l) *)
(* Goal: @eq resource (resource_fmap (approx n) (approx n) (f l)) (f l) *)
  rewrite H1.
(* Goal: False *)
  subst.
(* 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.
  destruct (f l); simpl in *; auto.
  subst p; reflexivity.
  subst p; reflexivity.
Qed.

Lemma rmap_unage_age:
  forall r, age (rmap_unage r) r.
Proof.
(* Goal: not (@identity share Share.Join_ba (Share.glb Share.Rsh (Share.lub a' (Share.glb Share.Rsh b)))) *)
intros; unfold age, rmap_unage; simpl.
(* Goal: forall (w : rmap) (loc : AV.address), @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (@core resource Join_resource Sep_resource (resource_at w loc))) (@core resource Join_resource Sep_resource (resource_at w loc)) *)
case_eq (unsquash r); intros.
(* Goal: @eq (option rmap) (@age1 rmap ag_rmap (squash (@pair nat rmap' (S n) r0))) (@Some rmap r) *)
rewrite rmap_age1_eq.
(* Goal: @eq (prod nat rmap') (unsquash (squash (@pair nat rmap' n (rmap_fmap (approx (S n)) (approx (S n)) r0)))) (@pair nat rmap' n r0) *)
rewrite unsquash_squash.
(* Goal: @eq resource (NO Share.bot nsh1) (NO Share.bot bot_unreadable) *)
f_equal.
(* Goal: @eq rmap (squash (@pair nat rmap' n (rmap_fmap (approx (S n)) (approx (S n)) r0))) r *)
apply unsquash_inj.
(* Goal: @eq resource (resource_fmap (approx (@level rmap ag_rmap r0)) (approx (@level rmap ag_rmap r0)) (resource_at phi1 loc)) (resource_fmap (approx (@level rmap ag_rmap r)) (approx (@level rmap ag_rmap r)) (resource_at phi2 loc)) *)
rewrite H.
(* Goal: @eq (prod nat rmap') (unsquash (squash (@pair nat rmap' n (rmap_fmap (approx (S n)) (approx (S n)) r0)))) (@pair nat rmap' n r0) *)
rewrite unsquash_squash.
(* Goal: @eq resource (NO Share.bot nsh1) (NO Share.bot bot_unreadable) *)
f_equal.
(* Goal: not (@identity resource Join_resource (YES sh rsh k Q)) *)
generalize (equal_f (rmap_fmap_comp (approx (S n)) (approx (S n)) (approx n) (approx n)) r0); intro.
(* Goal: @eq rmap' (rmap_fmap (approx n) (approx n) (rmap_fmap (approx (S n)) (approx (S n)) r0)) r0 *)
unfold compose at 1 in H0.
(* Goal: @identity share Share.Join_ba (Share.glb Share.Rsh b) *)
rewrite H0.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
rewrite approx_oo_approx'; auto.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
rewrite approx'_oo_approx; auto.
clear - H.
(* Goal: forall (w : rmap) (loc : AV.address), @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (@core resource Join_resource Sep_resource (resource_at w loc))) (@core resource Join_resource Sep_resource (resource_at w loc)) *)
generalize (unsquash_squash n r0); intros.
rewrite <- H in H0.
(* Goal: @eq rmap' (rmap_fmap (approx n) (approx n) r0) r0 *)
rewrite squash_unsquash in H0.
(* Goal: @eq rmap' (rmap_fmap (approx n) (approx n) r0) r0 *)
congruence.
Qed.

Lemma ageN_resource_at_eq:
  forall phi1 phi2 loc n phi1' phi2',
          level phi1 = level phi2 ->
          phi1 @ loc = phi2 @ loc ->
         ageN n phi1 = Some phi1' ->
         ageN n phi2 = Some phi2' ->
         phi1' @ loc = phi2' @ loc.
Proof.
(* Goal: forall (w : rmap) (loc : AV.address), @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (@core resource Join_resource Sep_resource (resource_at w loc))) (@core resource Join_resource Sep_resource (resource_at w loc)) *)
intros ? ? ? ? ? ? Hcomp ? ? ?; revert phi1 phi2 phi1' phi2' Hcomp H H0 H1; induction n; intros.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
inv H0; inv H1; auto.
(* Goal: @eq resource (resource_at phi1' loc) (resource_at phi2' loc) *)
unfold ageN in H0, H1.
simpl in *.
(* Goal: @eq resource (resource_at phi1' loc) (resource_at phi2' loc) *)
revert H0 H1; case_eq (age1 phi1); case_eq (age1 phi2); intros; try discriminate.
(* Goal: @eq resource (resource_at phi1' loc) (resource_at phi2' loc) *)
assert (level r = level r0) by (apply age_level in H0; apply age_level in H1; omega).
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
apply (IHn r0 r); auto.
(* Goal: @eq resource (resource_at r0 loc) (resource_at r loc) *)
rewrite (age1_resource_at _ _ H0 loc _ (eq_sym (resource_at_approx _ _))).
(* Goal: @eq resource (resource_at r0 loc) (resource_fmap (approx (@level rmap ag_rmap r)) (approx (@level rmap ag_rmap r)) (resource_at phi2 loc)) *)
rewrite (age1_resource_at _ _ H1 loc _ (eq_sym (resource_at_approx _ _))).
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
rewrite H. rewrite H4; auto.
Qed.

Definition empty_rmap' : rmap' :=
  ((fun _: AV.address => NO Share.bot bot_unreadable), nil).

Definition empty_rmap (n:nat) : rmap := R.squash (n, empty_rmap').

Lemma emp_empty_rmap: forall n, emp (empty_rmap n).
Proof.
(* Goal: forall (w : rmap) (loc : AV.address), @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (@core resource Join_resource Sep_resource (resource_at w loc))) (@core resource Join_resource Sep_resource (resource_at w loc)) *)
intros.
(* Goal: forall (w : rmap) (loc : AV.address), @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (@core resource Join_resource Sep_resource (resource_at w loc))) (@core resource Join_resource Sep_resource (resource_at w loc)) *)
intro; intros.
(* Goal: @eq rmap a b *)
apply rmap_ext.
(* Goal: @eq nat (@level rmap ag_rmap a) (@level rmap ag_rmap b) *)
(* Goal: forall l : AV.address, @eq resource (resource_at a l) (resource_at b l) *)
(* Goal: @eq ghost (ghost_of a) (ghost_of b) *)
Comp.
(* Goal: forall (w : rmap) (loc : AV.address), @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (@core resource Join_resource Sep_resource (resource_at w loc))) (@core resource Join_resource Sep_resource (resource_at w loc)) *)
intros.
(* Goal: @eq resource (resource_at a l) (resource_at b l) *)
(* Goal: @eq ghost (ghost_of a) (ghost_of b) *)
apply (resource_at_join _ _ _ l) in H.
unfold empty_rmap, empty_rmap', resource_at in *.
(* Goal: @eq resource (@fst (forall _ : AV.address, resource) ghost (@snd nat rmap' (unsquash a)) l) (@fst (forall _ : AV.address, resource) ghost (@snd nat rmap' (unsquash b)) l) *)
(* Goal: @eq ghost (ghost_of a) (ghost_of b) *)
destruct (unsquash a); destruct (unsquash b).
simpl in *.
destruct r; destruct r0; simpl in *.
(* Goal: @eq resource (r l) (r0 l) *)
(* Goal: @eq ghost (ghost_of a) (ghost_of b) *)
rewrite unsquash_squash in H.
simpl in *.
(* Goal: @eq resource (r l) (r0 l) *)
(* Goal: @eq ghost (ghost_of a) (ghost_of b) *)
unfold compose in H.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
inv H; auto; apply join_unit1_e in RJ; auto; subst; proof_irr; auto.
(* Goal: @eq ghost (ghost_of a) (ghost_of b) *)
eapply (core_identity nil).
(* Goal: @join (list (option (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds))) ghost_join (@core (list (option (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds))) ghost_join Sep_ghost (@nil (option (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds)))) (ghost_of a) (ghost_of b) *)
rewrite ghost_core.
(* Goal: @join (list (option (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds))) ghost_join (@nil (option (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds))) (ghost_of a) (ghost_of b) *)
replace nil with (ghost_of (empty_rmap n)); [apply ghost_of_join; auto|].
(* Goal: @eq ghost (ghost_of (empty_rmap n)) (@nil (option (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds))) *)
unfold ghost_of, empty_rmap, empty_rmap'.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
rewrite unsquash_squash; auto.
Qed.

Lemma empty_rmap_level:
  forall lev, level (empty_rmap lev) = lev.
Proof.
(* Goal: forall (w : rmap) (loc : AV.address), @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (@core resource Join_resource Sep_resource (resource_at w loc))) (@core resource Join_resource Sep_resource (resource_at w loc)) *)
intros.
(* Goal: not (@identity share Share.Join_ba (Share.glb Share.Rsh (Share.lub a' (Share.glb Share.Rsh b)))) *)
simpl.
(* Goal: @eq nat (@level rmap ag_rmap (empty_rmap lev)) lev *)
rewrite rmap_level_eq.
unfold  empty_rmap.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
rewrite unsquash_squash; auto.
Qed.

Lemma approx_FF: forall n, approx n FF = FF.
Proof.
(* Goal: forall (w : rmap) (loc : AV.address), @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (@core resource Join_resource Sep_resource (resource_at w loc))) (@core resource Join_resource Sep_resource (resource_at w loc)) *)
intros.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
apply pred_ext; auto.
(* Goal: @derives rmap ag_rmap (approx n (@FF rmap ag_rmap)) (@FF rmap ag_rmap) *)
unfold approx; intros ? ?.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
hnf in H. destruct H; auto.
Qed.

Lemma resource_at_make_rmap: forall f g lev H Hg, 
     resource_at (proj1_sig (make_rmap f g lev H Hg)) = f.
refine (fun f g lev H Hg => match proj2_sig (make_rmap f g lev H Hg) with
                           | conj _ (conj RESOURCE_AT _) => RESOURCE_AT
                         end).
Qed.

Lemma level_make_rmap: forall f g lev H Hg, @level rmap _ (proj1_sig (make_rmap f g lev H Hg)) = lev.
refine (fun f g lev H Hg => match proj2_sig (make_rmap f g lev H Hg) with
                           | conj LEVEL _ => LEVEL
                         end).
Qed.

Instance Join_trace : Join (AV.address -> option (rshare * AV.kind)) :=
     (Join_fun AV.address (option (rshare * AV.kind))
                   (Join_lower (Join_prod rshare Join_rshare AV.kind (Join_equiv AV.kind)))).


 Lemma res_option_join:
    forall x y z, 
     join x y z -> 
     @join _ (@Join_lower (rshare * AV.kind)
     (Join_prod rshare Join_rshare AV.kind (Join_equiv AV.kind))) (res_option x) (res_option y) (res_option  z).
 Proof.
(* Goal: forall (w : rmap) (loc : AV.address), @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (@core resource Join_resource Sep_resource (resource_at w loc))) (@core resource Join_resource Sep_resource (resource_at w loc)) *)
   intros.
(* Goal: @join resource Join_resource (YES sh r k p) (NO Share.bot bot_unreadable) (YES sh r k p) *)
(* Goal: False *)
   inv H; simpl; try constructor.
(* Goal: @join resource Join_resource (YES sh r k p) (NO Share.bot bot_unreadable) (YES sh r k p) *)
(* Goal: False *)
   erewrite join_readable_part_eq by eassumption. constructor.
   apply join_comm in  RJ.
(* Goal: @join resource Join_resource (YES sh r k p) (NO Share.bot bot_unreadable) (YES sh r k p) *)
(* Goal: False *)
   erewrite join_readable_part_eq by eassumption. constructor.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
   constructor. apply join_readable_part; auto.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
   split; auto. 
 Qed.

Ltac uniq_assert name P := 
 lazymatch goal with H: P |- _ => fail 
    | _ => let H1 := fresh "H" name in assert (H1:P) end.

Ltac readable_unreadable_join_prover := 
repeat match goal with
| H: join ?A ?B ?C, H1: ~readable_share ?C |- _ =>
   uniq_assert A (~readable_share A);
    [ clear - H H1; contradict H1; eapply join_readable1; eauto; fail | ]
| H: join ?A ?B ?C, H1: ~readable_share ?C |- _ =>
   uniq_assert B (~readable_share B);
    [ clear - H H1; contradict H1; eapply join_readable2; eauto; fail | ]
| H: join ?A ?B ?C, H0: ~readable_share ?B, H1: readable_share ?C |- _ =>
    (uniq_assert A (readable_share A);
    [ clear - H H0 H1; destruct (readable_share_dec A); 
      [solve [auto]
       |eapply join_unreadable_shares in H; eauto; solve [contradiction]] | ])
| H: join ?A ?B ?C, H0: ~readable_share ?A, H1: readable_share ?C |- _ =>
    (uniq_assert B (readable_share B);
    [ clear - H H0 H1; destruct (readable_share_dec B); 
      [solve [auto]
       | apply join_comm in H; 
         eapply join_unreadable_shares in H; eauto; solve [contradiction]] | ])
end.

(*Lemma Cross_resource: Cross_alg resource.
Proof.
(* Goal: forall (w : rmap) (loc : AV.address), @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (@core resource Join_resource Sep_resource (resource_at w loc))) (@core resource Join_resource Sep_resource (resource_at w loc)) *)
intro; intros.
destruct a as [ra | ra sa ka pa | ka pa | ma].
destruct b as [rb | rb sb kb pb | kb pb |]; try solve [elimtype False; inv H].
destruct z as [rz | rz sz kz pz | kz pz |]; try solve [elimtype False; inv H].
destruct c as [rc | rc sc kc pc | kc pc |]; try solve [elimtype False; inv H0].
destruct d as [rd | rd sd kd pd | kd pd |]; try solve [elimtype False; inv H0].
assert (J1: join ra rb rz) by (inv H; auto).
assert (J2: join rc rd rz) by (inv H0; auto).
destruct (share_cross_split _ _ _ _ _ J1 J2) as [[[[ac ad] bc] bd] [Ha [Hb [Hc Hd]]]].
readable_unreadable_join_prover.
exists (NO ac Hac,NO ad Had, NO bc Hbc, NO bd Hbd); 
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
  repeat split; simpl; auto; constructor; auto.
destruct z as [rz | rz sz kz pz | kz pz |]; try solve [elimtype False; inv H].
destruct c as [rc | rc sc kc pc | kc pc |]; try solve [elimtype False; inv H0].
destruct d as [rd | rd sd kd pd | kd pd |]; try solve [elimtype False; inv H0].
assert (J1: join ra rb rz) by (inv H; auto).
assert (J2: join rc rd rz) by (inv H0; auto).
destruct (share_cross_split _ _ _ _ _ J1 J2) as [[[[ac ad] bc] bd] [Ha [Hb [Hc Hd]]]].
readable_unreadable_join_prover.
exists (NO ac Hac, NO ad Had, NO bc Hbc, YES bd Hbd kb pb); inv H; inv H0;
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
  repeat split; simpl; auto; try constructor; auto.
assert (J1: join ra rb rz) by (inv H; auto).
destruct d as [rd | rd sd kd pd | kd pd |]; try solve [elimtype False; inv H0].
assert (J2: join rc rd rz) by (inv H0; auto).
destruct (share_cross_split _ _ _ _ _ J1 J2) as [[[[ac ad] bc] bd] [Ha [Hb [Hc Hd]]]].
readable_unreadable_join_prover.
exists (NO ac Hac, NO ad Had, YES bc Hbc kb pb, NO bd Hbd); inv H; inv H0;
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
  repeat split; simpl; auto; try constructor; auto.
assert (J2: join rc rd rz) by (inv H0; auto).
destruct (share_cross_split _ _ _ _ _ J1 J2) as [[[[ac ad] bc] bd] [Ha [Hb [Hc Hd]]]].
readable_unreadable_join_prover.
exists (NO ac Hac, NO ad Had, YES bc Hbc kb pb, YES bd Hbd kd pd); inv H; inv H0;
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
  repeat split; simpl; auto; try constructor; auto.
destruct b as [rb | rb sb kb pb | kb pb |]; try solve [elimtype False; inv H].
destruct z as [rz | rz sz kz pz | kz pz |]; try solve [elimtype False; inv H].
assert (J1: join ra rb rz) by (inv H; auto).
destruct c as [rc | rc sc kc pc | kc pc |]; try solve [elimtype False; inv H0].
destruct d as [rd | rd sd kd pd | kd pd |]; try solve [elimtype False; inv H0].
assert (J2: join rc rd rz) by (inv H0; auto).
destruct (share_cross_split _ _ _ _ _ J1 J2) as [[[[ac ad] bc] bd] [Ha [Hb [Hc Hd]]]].
readable_unreadable_join_prover.
exists (NO ac Hac, YES ad Had kd pd, NO bc Hbc, NO bd Hbd); inv H; inv H0;
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
  repeat split; simpl; auto; try constructor; auto.
destruct d as [rd | rd sd kd pd | kd pd |]; try solve [elimtype False; inv H0].
assert (J2: join rc rd rz) by (inv H0; auto).
destruct (share_cross_split _ _ _ _ _ J1 J2) as [[[[ac ad] bc] bd] [Ha [Hb [Hc Hd]]]].
readable_unreadable_join_prover.
exists (YES ac Hac kc pc, NO ad Had, NO bc Hbc, NO bd Hbd); inv H; inv H0;
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
  repeat split; simpl; auto; try constructor; auto.
assert (J2: join rc rd rz) by (inv H0; auto).
destruct (share_cross_split _ _ _ _ _ J1 J2) as [[[[ac ad] bc] bd] [Ha [Hb [Hc Hd]]]].
readable_unreadable_join_prover.
exists (YES ac Hac kc pc, YES ad Had kd pd, NO bc Hbc, NO bd Hbd); inv H; inv H0;
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
  repeat split; simpl; auto; try constructor; auto.
destruct z as [rz | rz sz kz pz | kz pz |]; try solve [elimtype False; inv H].
assert (J1: join ra rb rz) by (inv H; auto).
destruct c as [rc | rc sc kc pc | kc pc |]; try solve [elimtype False; inv H0].
destruct d as [rd | rd sd kd pd | kd pd |]; try solve [elimtype False; inv H0].
assert (J2: join rc rd rz) by (inv H0; auto).
destruct (share_cross_split _ _ _ _ _ J1 J2) as [[[[ac ad] bc] bd] [Ha [Hb [Hc Hd]]]].
readable_unreadable_join_prover.
exists (NO ac Hac, YES ad Had kd pd, NO bc Hbc, YES bd Hbd kd pd); inv H; inv H0;
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
  repeat split; simpl; auto; try constructor; auto.
destruct d as [rd | rd sd kd pd | kd pd |]; try solve [elimtype False; inv H0].
assert (J2: join rc rd rz) by (inv H0; auto).
destruct (share_cross_split _ _ _ _ _ J1 J2) as [[[[ac ad] bc] bd] [Ha [Hb [Hc Hd]]]].
readable_unreadable_join_prover.
exists (YES ac Hac kc pc, NO ad Had, YES bc Hbc kb pb, NO bd Hbd); inv H; inv H0;
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
  repeat split; simpl; auto; try constructor; auto.
assert (J2: join rc rd rz) by (inv H0; auto).
destruct (share_cross_split _ _ _ _ _ J1 J2) as [[[[ac ad] bc] bd] [Ha [Hb [Hc Hd]]]].
destruct (Sumbool.sumbool_not _ _ (readable_share_dec ac)) as [Hac|Hac].
readable_unreadable_join_prover.
destruct (Sumbool.sumbool_not _ _ (readable_share_dec bd)) as [Hbd|Hbd].
exists (NO ac Hac, YES ad Had ka pa, YES bc Hbc kc pc, NO bd Hbd); 
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
   inv H; inv H0; simpl; repeat split; auto;  constructor; auto.
exists (NO ac Hac, YES ad Had ka pa, YES bc Hbc kc pc, YES bd Hbd kd pd); 
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
   inv H; inv H0; simpl; repeat split; auto;  constructor; auto.
destruct (Sumbool.sumbool_not _ _ (readable_share_dec ad)) as [Had|Had];
readable_unreadable_join_prover;
destruct (Sumbool.sumbool_not _ _ (readable_share_dec bc)) as [Hbc|Hbc];
readable_unreadable_join_prover.
exists (YES ac Hac ka pa, NO ad Had, NO bc Hbc, YES bd Hbd kb pb); 
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
   inv H; inv H0; simpl; repeat split; auto;  constructor; auto.
exists (YES ac Hac ka pa, NO ad Had, YES bc Hbc kc pc, YES bd Hbd kd pd);
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
    inv H; inv H0; simpl; repeat split; auto;  constructor; auto.
exists (YES ac Hac kc pc, YES ad Had kc pc, NO bc Hbc, YES bd Hbd kb pb);
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
    inv H; inv H0; simpl; repeat split; auto;  constructor; auto.
destruct (Sumbool.sumbool_not _ _ (readable_share_dec bd)) as [Hbd|Hbd].
exists (YES ac Hac ka pa,  YES ad Had kd pd, YES bc Hbc kb pb, NO bd Hbd);
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
    inv H; inv H0; simpl; repeat split; auto;  constructor; auto.
exists (YES ac Hac ka pa, YES ad Had ka pa, 
       YES bc Hbc ka pa,  YES bd Hbd ka pa);
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
    inv H; inv H0; simpl; repeat split; auto;  constructor; auto.
exists (PURE ka pa, PURE ka pa, PURE ka pa, PURE ka pa).
(* Goal: @eq resource (YES sh1 rsh1 k pp) (NO Share.bot bot_unreadable) *)
inv H. inv H0.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
repeat split; constructor; auto.
destruct b as [| | | mb]; try solve [elimtype False; inv H].
destruct z as [| | | mz]; try solve [elimtype False; inv H].
destruct c as [| | | mc]; try solve [elimtype False; inv H0].
destruct d as [| | | md]; try solve [elimtype False; inv H0].
(* relies on cross-split for ghost state *)
Qed.*)

Definition res_retain (r: resource) : Share.t :=
 match r with
  | NO sh _ => retainer_part sh
  | YES sh _ _ _ => retainer_part sh
  | PURE _ _ => Share.bot
 end.

Lemma fixup_trace_readable:
  forall a (b: rshare), readable_share (Share.lub (Share.glb Share.Lsh a) (Share.glb Share.Rsh (proj1_sig b))).
Proof.
(* Goal: forall (w : rmap) (loc : AV.address), @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (@core resource Join_resource Sep_resource (resource_at w loc))) (@core resource Join_resource Sep_resource (resource_at w loc)) *)
intros.
(* Goal: readable_share (Share.lub (Share.glb Share.Lsh a) (Share.glb Share.Rsh (@proj1_sig Share.t pure_readable_share b))) *)
destruct b as [b H].
(* Goal: readable_share (Share.lub (Share.glb Share.Lsh a) (Share.glb Share.Rsh (@proj1_sig Share.t pure_readable_share (@exist Share.t pure_readable_share b H)))) *)
forget (Share.glb Share.Lsh a) as a'. clear a.
(* Goal: not (@identity share Share.Join_ba (Share.glb Share.Rsh (Share.lub a' (Share.glb Share.Rsh b)))) *)
simpl.
(* Goal: readable_share (Share.lub a' (Share.glb Share.Rsh b)) *)
destruct H as [H' H].
do 3 red in H|-*.
(* Goal: not (@identity share Share.Join_ba (Share.glb Share.Rsh (Share.lub a' (Share.glb Share.Rsh b)))) *)
simpl.
(* Goal: not (@identity share Share.Join_ba (Share.glb Share.Rsh (Share.lub a' (Share.glb Share.Rsh b)))) *)
contradict H.
(* Goal: @identity share Share.Join_ba (Share.glb Share.Rsh b) *)
rewrite Share.distrib1 in H.
rewrite <- Share.glb_assoc in H.
(* Goal: @identity share Share.Join_ba (Share.glb Share.Rsh b) *)
rewrite Share.glb_idem in H.
(* Goal: @identity share Share.Join_ba (Share.glb Share.Rsh b) *)
apply identity_share_bot in H.
(* Goal: @identity share Share.Join_ba (Share.glb Share.Rsh b) *)
apply lub_bot_e in H. destruct H.
(* Goal: @identity share Share.Join_ba Share.bot *)
rewrite H0. apply bot_identity.
Qed.

(*Definition fixup_trace (retain: AV.address -> Share.t)
                 (trace: AV.address -> option (rshare * AV.kind)) (gtrace: AV.address -> option M)
                 (f: AV.address -> resource) : AV.address -> resource :=
   fun x => match trace x, f x with
            | None, PURE k pp => PURE k pp
            | Some(sh,k), PURE _ pp =>
               YES _ (fixup_trace_readable (retain x) sh) k pp
            | Some (sh,k), YES _ _ _ pp => YES _ (fixup_trace_readable (retain x) sh) k pp
            | Some (sh, k), NO _ _ => YES _ (fixup_trace_readable (retain x) sh) k NoneP
            | None, _ => NO _ (@retainer_part_nonreadable (retain x))
            end.


Definition fixup_trace_ok (tr: AV.address -> option (rshare * AV.kind)) :=
 forall x, match tr x with None => True | Some(sh,_)=> Share.glb Share.Rsh (proj1_sig sh) = (proj1_sig sh) end.

Lemma fixup_trace_valid: forall retain
             tr 
             (trace_ok: fixup_trace_ok tr)
              f,
            AV.valid tr -> 
            AV.valid (res_option oo (fixup_trace retain tr f)).
(* Goal: forall (w : rmap) (loc : AV.address), @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (@core resource Join_resource Sep_resource (resource_at w loc))) (@core resource Join_resource Sep_resource (resource_at w loc)) *)
 Proof. intros.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
  replace (res_option oo fixup_trace retain tr f) with tr. auto.
(* Goal: @eq resource (@compose AV.address resource resource (resource_fmap (approx n) (approx n)) f l) (f l) *)
  extensionality l. unfold compose. unfold fixup_trace.
  specialize (trace_ok l).
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
  destruct (tr l); simpl; auto.
*
(* Goal: @eq (option (prod rshare AV.kind)) (res_option (YES sh r k p)) (res_option (resource_at phi' loc)) *)
(* Goal: @eq (option (prod rshare AV.kind)) (res_option (PURE k p)) (res_option (resource_at phi' loc)) *)
  destruct p. rename r into s.
  assert (s = readable_part (fixup_trace_readable (retain l) s)). {
    destruct s; apply exist_ext'; simpl in *.
    clear - trace_ok.
    rewrite Share.lub_commute.
    rewrite Share.distrib1.
    rewrite <- !Share.glb_assoc. rewrite Share.glb_idem.
    rewrite (Share.glb_commute _ Share.Lsh).
    rewrite glb_Lsh_Rsh. rewrite (Share.glb_commute Share.bot). rewrite Share.glb_bot.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
    rewrite Share.lub_bot. auto.
  }
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
  destruct (f l); simpl; f_equal; f_equal; auto.
*
  destruct (f l); reflexivity.
Qed.

Lemma fixup_trace_rmap:
    forall (retain: AV.address -> Share.t) 
             (tr: sig AV.valid) (trace_ok: fixup_trace_ok (proj1_sig tr)) (f: rmap),
        {phi: rmap | 
             level phi = level f 
            /\ resource_at phi = fixup_trace retain (proj1_sig tr) (resource_at f)}.
Proof.
(* Goal: forall (w : rmap) (loc : AV.address), @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (@core resource Join_resource Sep_resource (resource_at w loc))) (@core resource Join_resource Sep_resource (resource_at w loc)) *)
 intros.
 apply make_rmap.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
 apply fixup_trace_valid; auto. destruct tr; simpl; auto.
(* Goal: @eq (forall _ : AV.address, resource) (@compose AV.address resource resource (resource_fmap (approx n) (approx n)) f) f *)
 extensionality l.
 unfold compose, fixup_trace.
(* Goal: not (@identity share Share.Join_ba (Share.glb Share.Rsh (Share.lub a' (Share.glb Share.Rsh b)))) *)
 destruct tr. simpl.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
 destruct (x l); simpl; auto. destruct p.
(* Goal: forall (w : rmap) (loc : AV.address), @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (@core resource Join_resource Sep_resource (resource_at w loc))) (@core resource Join_resource Sep_resource (resource_at w loc)) *)
 case_eq (f @ l); intros.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
 unfold resource_fmap. rewrite preds_fmap_NoneP; auto.
(* Goal: not (@identity resource Join_resource (YES sh rsh k Q)) *)
 generalize (resource_at_approx f l); intro.
(* Goal: @eq nat (@level rmap ag_rmap m1) (@level rmap ag_rmap m') *)
(* Goal: @ex rmap (fun m1 : rmap => and (@laterR rmap ag_rmap m m1) (@eq nat (@level rmap ag_rmap m1) (@level rmap ag_rmap m'))) *)
 rewrite H in H0. symmetry in H0.
(* Goal: not (@identity share Share.Join_ba (Share.glb Share.Rsh (Share.lub a' (Share.glb Share.Rsh b)))) *)
  simpl in H0. simpl.
(* Goal: @eq resource (NO Share.bot nsh1) (NO Share.bot bot_unreadable) *)
   f_equal. injection H0; auto.
(* Goal: not (@identity resource Join_resource (YES sh rsh k Q)) *)
 generalize (resource_at_approx f l); intro.
(* Goal: @eq nat (@level rmap ag_rmap m1) (@level rmap ag_rmap m') *)
(* Goal: @ex rmap (fun m1 : rmap => and (@laterR rmap ag_rmap m m1) (@eq nat (@level rmap ag_rmap m1) (@level rmap ag_rmap m'))) *)
 rewrite H in H0. symmetry in H0.
(* Goal: not (@identity share Share.Join_ba (Share.glb Share.Rsh (Share.lub a' (Share.glb Share.Rsh b)))) *)
  simpl in H0. simpl.
(* Goal: @eq resource (NO Share.bot nsh1) (NO Share.bot bot_unreadable) *)
   f_equal. injection H0; auto.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
 auto.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
 case_eq (f @ l); intros; auto.
(* Goal: not (@identity resource Join_resource (YES sh rsh k Q)) *)
 generalize (resource_at_approx f l); intro.
(* Goal: @eq nat (@level rmap ag_rmap m1) (@level rmap ag_rmap m') *)
(* Goal: @ex rmap (fun m1 : rmap => and (@laterR rmap ag_rmap m m1) (@eq nat (@level rmap ag_rmap m1) (@level rmap ag_rmap m'))) *)
 rewrite H in H0. symmetry in H0.
(* Goal: not (@identity share Share.Join_ba (Share.glb Share.Rsh (Share.lub a' (Share.glb Share.Rsh b)))) *)
  simpl in H0. simpl.
(* Goal: @eq resource (NO Share.bot nsh1) (NO Share.bot bot_unreadable) *)
   f_equal. injection H0; auto.
Qed.

Lemma join_res_retain:
          forall a b c: rmap ,
              join a b c ->
              join (res_retain oo resource_at a) (res_retain oo resource_at b) (res_retain oo resource_at c).
Proof.
(* Goal: forall (w : rmap) (loc : AV.address), @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (@core resource Join_resource Sep_resource (resource_at w loc))) (@core resource Join_resource Sep_resource (resource_at w loc)) *)
 intros.
 intro loc; apply (resource_at_join _ _ _ loc) in H.
(* Goal: @eq resource (@compose AV.address resource resource (resource_fmap (approx n) (approx n)) f l) (f l) *)
  unfold compose.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
 inv H; simpl; auto; apply retainer_part_join; auto.
Qed.

Lemma join_fixup_trace_ok:
  forall (v w: sig AV.valid) a,
    join v w (exist AV.valid (res_option oo resource_at a) (rmap_valid a)) ->
    fixup_trace_ok (proj1_sig v).
Proof.
(* Goal: forall (w : rmap) (loc : AV.address), @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (@core resource Join_resource Sep_resource (resource_at w loc))) (@core resource Join_resource Sep_resource (resource_at w loc)) *)
  intros.
(* Goal: forall (w : rmap) (loc : AV.address), @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (@core resource Join_resource Sep_resource (resource_at w loc))) (@core resource Join_resource Sep_resource (resource_at w loc)) *)
   hnf; intros.
   destruct v, w. simpl in *.
(* Goal: @ex rmap (fun m1 : rmap => and (@laterR rmap ag_rmap m m1) (@eq nat (@level rmap ag_rmap m1) (@level rmap ag_rmap m'))) *)
(* Goal: @ex rmap (fun m1 : rmap => and (@laterR rmap ag_rmap m m1) (@eq nat (@level rmap ag_rmap m1) (@level rmap ag_rmap m'))) *)
   red in H. red in H. simpl in H.
   specialize (H x).
   clear - H.
   forget (x0 x) as u. forget (x1 x) as v.
   unfold res_option, compose in H.
(* Goal: @eq resource (@core resource Join_resource Sep_resource (PURE k pp)) (PURE k pp) *)
   destruct (a @ x); inv H; auto.
(* Goal: not (@identity share Share.Join_ba (Share.glb Share.Rsh (Share.lub a' (Share.glb Share.Rsh b)))) *)
   unfold readable_part. simpl.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
   rewrite <- Share.glb_assoc. rewrite Share.glb_idem; auto.
   destruct a1 as [[v ?] ?]. destruct a2 as [[w ?] ?].
   destruct H3 as [H3 _]. do 2 red in H3. simpl in H3.
(* Goal: not (@identity share Share.Join_ba (Share.glb Share.Rsh (Share.lub a' (Share.glb Share.Rsh b)))) *)
   simpl. clear - H3.
   assert (join_sub v (Share.glb Share.Rsh sh)) by (exists w; auto).
   clear H3.
   apply leq_join_sub in H.
   assert (Share.Ord (Share.glb Share.Rsh sh) Share.Rsh).
   apply Share.ord_spec1.
   symmetry. rewrite Share.glb_commute. rewrite <- Share.glb_assoc.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
   rewrite Share.glb_idem. auto.
   pose proof (Share.ord_trans _ _ _ H H0).
   clear - H1.
   apply Share.ord_spec1 in H1.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
   rewrite Share.glb_commute. auto.
Qed.

Instance Perm_foo: Perm_alg
               {x : AV.address -> option (rshare * AV.kind) |
               AV.valid x}.
Proof.
apply Perm_prop.
apply Perm_fun.
apply Perm_lower.
apply Perm_prod.
apply Perm_rshare.
apply Perm_equiv.
(* Goal: forall (w : rmap) (loc : AV.address), @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (@core resource Join_resource Sep_resource (resource_at w loc))) (@core resource Join_resource Sep_resource (resource_at w loc)) *)
intros.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
eapply AV.valid_join; eauto.
Qed.

Ltac crtac' :=
 repeat  (simpl in *; ((*solve [constructor; auto] ||*)
   match goal with
 | H: None = res_option ?A |- _ => destruct A; inv H
 | H: Some _ = res_option ?A |- _ => destruct A; inv H
 | H: join (NO _ _) _ _ |- _ => inv H
 | H: join _ (NO _ _) _ |- _ => inv H
 | H: join (YES _ _ _ _) _ _ |- _ => inv H
 | H: join _ (YES _ _ _ _) _ |- _ => inv H
 | H: join (PURE _ _) _ _ |- _ => inv H
 | H: join _ (PURE _ _) _ |- _ => inv H
 | H: @join _ _ (Some _) _ _ |- _ => inv H
 | H: @join _ _ _ (Some _) _ |- _ => inv H
 | H: join None _ _ |- _ =>  inv H
 | H: join _ None _ |- _ => inv H
 end; auto)).


Lemma join_fixup_trace:
 forall (Rc Rd: AV.address -> Share.t)
        (c d: AV.address -> option (rshare * AV.kind))
        (z a: rmap) (l: AV.address), 
   join_sub (a @ l) (z @ l) ->
   join (Rc l) (Rd l) (res_retain (a @ l)) ->
   @join (option (rshare * AV.kind))
       (@Join_lower (rshare * AV.kind)
          (Join_prod rshare Join_rshare AV.kind
             (Join_equiv AV.kind)))
         (c l) (d l) (res_option (a @ l)) ->
   join (fixup_trace Rc c (resource_at z) l) (fixup_trace Rd d (resource_at z) l) (a @ l).
Proof.
(* Goal: forall (w : rmap) (loc : AV.address), @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (@core resource Join_resource Sep_resource (resource_at w loc))) (@core resource Join_resource Sep_resource (resource_at w loc)) *)
intros.
unfold fixup_trace.
forget (a @ l) as al.
forget (z @ l) as zl.
forget (Rc l) as Rcl.
forget (c l) as cl.
forget (Rd l) as Rdl.
forget (d l) as dl.
destruct H as [bl H].
clear - H H0 H1.
(* Goal: @join resource Join_resource (YES sh r k p) (NO Share.bot bot_unreadable) (YES sh r k p) *)
(* Goal: False *)
destruct cl as [[? ?]|]; crtac'; try constructor.
*
destruct (join_parts comp_Lsh_Rsh H0) as [J1 [J2 [J3 J4]]].
unfold retainer_part.
rewrite ?J1,?J2,?J3,?J4, ?glb_twice, ?glb_Lsh_Rsh', ?Share.lub_bot, ?lub_bot'.
apply left_right_join.
rewrite Share.distrib1.
rewrite ?J1,?J2,?J3,?J4, ?glb_twice, ?glb_Lsh_Rsh', ?Share.lub_bot, ?lub_bot'.
assumption.
rewrite Share.distrib1.
rewrite ?J1,?J2,?J3,?J4, ?glb_twice, ?glb_Lsh_Rsh', ?Share.lub_bot, ?lub_bot'.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
apply join_unit2; auto.
*
destruct (join_parts comp_Lsh_Rsh H0) as [J1 [J2 [J3 J4]]].
unfold retainer_part.
rewrite ?J1,?J2,?J3,?J4, ?glb_twice, ?glb_Lsh_Rsh', ?Share.lub_bot, ?lub_bot'.
apply left_right_join.
rewrite Share.distrib1.
rewrite ?J1,?J2,?J3,?J4, ?glb_twice, ?glb_Lsh_Rsh', ?Share.lub_bot, ?lub_bot'.
assumption.
rewrite Share.distrib1.
rewrite ?J1,?J2,?J3,?J4, ?glb_twice, ?glb_Lsh_Rsh', ?Share.lub_bot, ?lub_bot'.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
apply join_unit2; auto.
*
destruct a2.
destruct H5; simpl in *. destruct H1; subst.
destruct r,r1; simpl in *.
do 2 red in H. simpl in *.
(* Goal: @join resource Join_resource (YES sh r k p) (NO Share.bot bot_unreadable) (YES sh r k p) *)
(* Goal: False *)
constructor.
destruct (join_parts comp_Lsh_Rsh H0) as [J1 [J2 [J3 J4]]].
apply left_right_join.
rewrite ?J1,?J2,?J3,?J4, ?glb_twice, ?glb_Lsh_Rsh', ?Share.lub_bot, ?lub_bot'.
rewrite Share.distrib1.
rewrite glb_Lsh_Rsh', Share.lub_bot.
rewrite Share.distrib1.
rewrite ?J1,?J2,?J3,?J4, ?glb_twice, ?glb_Lsh_Rsh', ?Share.lub_bot, ?lub_bot'.
assumption.
rewrite ?J1,?J2,?J3,?J4, ?glb_twice, ?glb_Lsh_Rsh', ?Share.lub_bot, ?lub_bot'.
rewrite Share.distrib1.
rewrite ?J1,?J2,?J3,?J4, ?glb_twice, ?glb_Lsh_Rsh', ?Share.lub_bot, ?lub_bot'.
rewrite Share.distrib1.
rewrite ?J1,?J2,?J3,?J4, ?glb_twice, ?glb_Lsh_Rsh', ?Share.lub_bot, ?lub_bot'.
destruct (join_parts comp_Rsh_Lsh H) as [K1 [K2 [K3 K4]]].
rewrite ?K1, ?K2,?K3,?K4.
assumption.
*
destruct a2.
destruct H5; simpl in *. destruct H1; subst.
destruct r,r1; simpl in *.
do 2 red in H. simpl in *.
(* Goal: @join resource Join_resource (YES sh r k p) (NO Share.bot bot_unreadable) (YES sh r k p) *)
(* Goal: False *)
constructor.
destruct (join_parts comp_Lsh_Rsh H0) as [J1 [J2 [J3 J4]]].
apply left_right_join.
rewrite ?J1,?J2,?J3,?J4, ?glb_twice, ?glb_Lsh_Rsh', ?Share.lub_bot, ?lub_bot'.
rewrite Share.distrib1.
rewrite glb_Lsh_Rsh', Share.lub_bot.
rewrite Share.distrib1.
rewrite ?J1,?J2,?J3,?J4, ?glb_twice, ?glb_Lsh_Rsh', ?Share.lub_bot, ?lub_bot'.
assumption.
rewrite ?J1,?J2,?J3,?J4, ?glb_twice, ?glb_Lsh_Rsh', ?Share.lub_bot, ?lub_bot'.
rewrite Share.distrib1.
rewrite ?J1,?J2,?J3,?J4, ?glb_twice, ?glb_Lsh_Rsh', ?Share.lub_bot, ?lub_bot'.
rewrite Share.distrib1.
rewrite ?J1,?J2,?J3,?J4, ?glb_twice, ?glb_Lsh_Rsh', ?Share.lub_bot, ?lub_bot'.
destruct (join_parts comp_Rsh_Lsh H) as [K1 [K2 [K3 K4]]].
rewrite ?K1, ?K2,?K3,?K4.
assumption.
*
unfold retainer_part in *.
destruct al; crtac'; try constructor;
unfold retainer_part in *.
 +
destruct (join_parts comp_Lsh_Rsh H0) as [J1 [J2 [J3 J4]]].
rewrite ?J1,?J2,?J3,?J4, ?glb_twice, ?glb_Lsh_Rsh', ?Share.lub_bot, ?lub_bot'.
rewrite <- (Share.glb_top sh). rewrite Share.glb_commute.
rewrite <- lub_Lsh_Rsh.
(* Goal: @identity share Share.Join_ba (Share.glb Share.Rsh sh2) *)
rewrite Share.glb_commute.
rewrite Share.distrib1.
apply not_readable_Rsh_part in nsh0.
rewrite (Share.glb_commute _ Share.Rsh), nsh0.
rewrite Share.lub_bot.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
rewrite Share.glb_commute; auto.
 +
rewrite <- (Share.glb_top sh). rewrite Share.glb_commute.
rewrite <- lub_Lsh_Rsh.
(* Goal: @identity share Share.Join_ba (Share.glb Share.Rsh sh2) *)
rewrite Share.glb_commute.
rewrite Share.distrib1.
apply not_readable_Rsh_part in nsh0.
rewrite (Share.glb_commute _ Share.Rsh), nsh0.
rewrite Share.lub_bot.
destruct (join_parts comp_Lsh_Rsh H0) as [J1 [J2 [J3 J4]]].
rewrite ?J1,?J2,?J3,?J4, ?glb_twice, ?glb_Lsh_Rsh', ?Share.lub_bot, ?lub_bot'.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
rewrite Share.glb_commute; auto.
 +
destruct (join_parts comp_Lsh_Rsh H0) as [J1 [J2 [J3 J4]]].
rewrite ?J1,?J2,?J3,?J4, ?glb_twice, ?glb_Lsh_Rsh', ?Share.lub_bot, ?lub_bot'.
apply left_right_join.
rewrite ?J1,?J2,?J3,?J4, ?glb_twice, ?glb_Lsh_Rsh', ?Share.lub_bot, ?lub_bot'.
rewrite Share.distrib1.
rewrite glb_Lsh_Rsh', Share.lub_bot.
rewrite ?J1,?J2,?J3,?J4, ?glb_twice, ?glb_Lsh_Rsh', ?Share.lub_bot, ?lub_bot'.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
auto.
rewrite Share.distrib1.
rewrite ?J1,?J2,?J3,?J4, ?glb_twice, ?glb_Lsh_Rsh', ?Share.lub_bot, ?lub_bot'.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
apply join_unit1; auto.
 +
rewrite ?J1,?J2,?J3,?J4, ?glb_twice, ?glb_Lsh_Rsh', ?Share.lub_bot, ?lub_bot'.
apply left_right_join.
rewrite ?J1,?J2,?J3,?J4, ?glb_twice, ?glb_Lsh_Rsh', ?Share.lub_bot, ?lub_bot'.
destruct (join_parts comp_Lsh_Rsh H0) as [J1 [J2 [J3 J4]]].
rewrite ?J1,?J2,?J3,?J4, ?glb_twice, ?glb_Lsh_Rsh', ?Share.lub_bot, ?lub_bot'.
rewrite Share.distrib1.
rewrite ?J1,?J2,?J3,?J4, ?glb_twice, ?glb_Lsh_Rsh', ?Share.lub_bot, ?lub_bot'.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
auto.
rewrite <- Share.glb_assoc. rewrite glb_Rsh_Lsh.
(* Goal: @identity share Share.Join_ba (Share.glb Share.Rsh sh2) *)
rewrite Share.glb_commute. rewrite Share.glb_bot. 
rewrite Share.distrib1.
rewrite <- Share.glb_assoc. rewrite glb_Rsh_Lsh.
(* Goal: @identity share Share.Join_ba (Share.glb Share.Rsh sh2) *)
rewrite Share.glb_commute. rewrite Share.glb_bot. 
rewrite Share.lub_commute, Share.lub_bot.
rewrite <- Share.glb_assoc. rewrite Share.glb_idem.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
apply join_unit1; auto.
 +
(* Goal: not (@identity share Share.Join_ba (Share.glb Share.Rsh (Share.lub a' (Share.glb Share.Rsh b)))) *)
inv H; simpl.
admit. (* What should fixup_trace do with a ghost? *)
*
destruct (join_parts comp_Lsh_Rsh H0) as [J1 [J2 [J3 J4]]].
unfold retainer_part in *.
rewrite ?J1,?J2,?J3,?J4, ?glb_twice, ?glb_Lsh_Rsh', ?Share.lub_bot, ?lub_bot'.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
auto.
rewrite <- (Share.glb_top sh). rewrite Share.glb_commute.
rewrite <- lub_Lsh_Rsh.
(* Goal: @identity share Share.Join_ba (Share.glb Share.Rsh sh2) *)
rewrite Share.glb_commute.
rewrite Share.distrib1.
apply not_readable_Rsh_part in nsh0.
rewrite (Share.glb_commute _ Share.Rsh), nsh0.
rewrite Share.lub_bot.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
rewrite Share.glb_commute; auto.
*
destruct (join_parts comp_Lsh_Rsh H0) as [J1 [J2 [J3 J4]]].
unfold retainer_part in *.
rewrite ?J1,?J2,?J3,?J4, ?glb_twice, ?glb_Lsh_Rsh', ?Share.lub_bot, ?lub_bot'.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
auto.
rewrite <- (Share.glb_top sh). rewrite Share.glb_commute.
rewrite <- lub_Lsh_Rsh.
(* Goal: @identity share Share.Join_ba (Share.glb Share.Rsh sh2) *)
rewrite Share.glb_commute.
rewrite Share.distrib1.
apply not_readable_Rsh_part in nsh0.
rewrite (Share.glb_commute _ Share.Rsh), nsh0.
rewrite Share.lub_bot.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
rewrite Share.glb_commute; auto.
*
(* Goal: @eq resource (YES sh1 rsh1 k pp) (NO Share.bot bot_unreadable) *)
inv H.
admit.
Abort.

Instance Cross_rmap:
      @Cross_alg _ (Join_prop _ Join_trace AV.valid) ->
      Cross_alg rmap.
Proof.
  intro CAV.
(* Goal: not (@identity resource Join_resource (YES sh rsh k Q)) *)
  repeat intro.
  assert (Hz : valid (resource_at z)).
  unfold resource_at.
(* Goal: forall (w : rmap) (loc : AV.address), @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (@core resource Join_resource Sep_resource (resource_at w loc))) (@core resource Join_resource Sep_resource (resource_at w loc)) *)
  case_eq (unsquash z); intros.
(* Goal: not (@identity share Share.Join_ba (Share.glb Share.Rsh (Share.lub a' (Share.glb Share.Rsh b)))) *)
  simpl.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
  destruct r; simpl; auto.
  specialize (CAV
          (exist AV.valid _ (rmap_valid a))
          (exist AV.valid _ (rmap_valid b))
          (exist AV.valid _ (rmap_valid c))
          (exist AV.valid _ (rmap_valid d))
          (exist AV.valid _ Hz)).
  destruct CAV as [[[[Vac Vad] Vbc] Vbd] [Va [Vb [Vc Vd]]]].
(* Goal: not (@identity share Share.Join_ba (Share.glb Share.Rsh (Share.lub a' (Share.glb Share.Rsh b)))) *)
  intro l.  unfold compose. simpl.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
  apply res_option_join. apply resource_at_join. auto.
(* Goal: not (@identity share Share.Join_ba (Share.glb Share.Rsh (Share.lub a' (Share.glb Share.Rsh b)))) *)
  intro l.  simpl. unfold compose.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
  apply res_option_join. apply resource_at_join. auto.
  assert (CAR: Cross_alg (AV.address -> Share.t)) by auto with typeclass_instances.
  specialize (CAR _ _ _ _ _ (join_res_retain _ _ _ H) (join_res_retain _ _ _ H0)).
  destruct CAR as [[[[Rac Rad] Rbc] Rbd] [Ra [Rb [Rc Rd]]]].
  destruct (fixup_trace_rmap  Rac Vac (join_fixup_trace_ok _ _ _ Va) z) as [Mac [? ?]].
  destruct (fixup_trace_rmap Rad Vad (join_fixup_trace_ok _ _ _ Vd) z) as [Mad [? ?]].
  destruct (fixup_trace_rmap Rbc Vbc (join_fixup_trace_ok _ _ _ Vb) z) as [Mbc [? ?]].
  destruct (fixup_trace_rmap Rbd Vbd (join_fixup_trace_ok _ _ _ (join_comm Vb)) z) as [Mbd [? ?]].
  exists (Mac,Mad,Mbc,Mbd).
  destruct Vac as [ac ?]; destruct Vad as [ad ?]; destruct Vbc as [bc ?];
  destruct Vbd as [bd ?]; simpl in *.
  assert (LEVa: level a = level z) by (apply join_level in H; destruct H; auto).
  assert (LEVb: level b = level z) by (apply join_level in H; destruct H; auto).
  assert (LEVc: level c = level z) by (apply join_level in H0; destruct H0; auto).
  assert (LEVd: level d = level z) by (apply join_level in H0; destruct H0; auto).
  do 2 red in Va,Vb,Vc,Vd; simpl in *.
  unfold compose in *. clear Hz.
  split; [|split3];   apply resource_at_join2; try congruence;
  repeat match goal with
  | H: AV.valid _ |- _ => clear H
  | H: level _ = level _ |- _ => clear H
  end;
  intro l;
  specialize ( Va l); specialize ( Vb l); specialize ( Vc l); specialize ( Vd l);
  specialize ( Ra l); specialize ( Rb l); specialize ( Rc l); specialize ( Rd l); 
  apply (resource_at_join _ _ _ l) in H;
  apply (resource_at_join _ _ _ l) in H0;
  try rewrite H2; try rewrite H4; try rewrite H6; try rewrite H8;
  simpl in *;
 eapply join_fixup_trace; eauto;
 (eapply join_join_sub; eassumption) || (eapply join_join_sub'; eassumption).
Qed.*)

Lemma identity_resource: forall r: resource, identity r <->
    match r with YES _ _ _ _ => False | NO sh rsh => identity sh | PURE _ _ => True end.
Proof.
(* Goal: forall (w : rmap) (loc : AV.address), @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (@core resource Join_resource Sep_resource (resource_at w loc))) (@core resource Join_resource Sep_resource (resource_at w loc)) *)
 intros. destruct r.
(* Goal: iff (@identity resource Join_resource (NO sh n)) (@identity Share.t Share.Join_ba sh) *)
 - split; intro.
(* Goal: @eq resource (@core resource Join_resource Sep_resource (PURE k pp)) (PURE k pp) *)
   + apply identity_unit' in H. inv H; auto. apply identity_unit_equiv; auto.
(* Goal: not (@identity resource Join_resource (YES sh rsh k Q)) *)
   + repeat intro.
(* Goal: @eq resource a b *)
     inv H0.
     * apply H in RJ; subst.
(* Goal: @eq (not (readable_share Share.bot)) nsh1 bot_unreadable *)
       f_equal; apply proof_irr.
     * apply H in RJ; subst.
(* Goal: @eq (not (readable_share Share.bot)) nsh1 bot_unreadable *)
       f_equal; apply proof_irr.
 - intuition.
(* Goal: False *)
   specialize (H (NO Share.bot bot_unreadable) (YES sh r k p)).
(* Goal: @eq resource (YES sh1 rsh1 k pp) (NO Share.bot bot_unreadable) *)
   spec H. constructor. apply join_unit2; auto. inv H.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
 - intuition. intros  ? ? ?. inv H0. auto.
Qed.

Lemma resource_at_core_identity:  forall m i, identity (core m @ i).
Proof.
(* Goal: forall (w : rmap) (loc : AV.address), @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (@core resource Join_resource Sep_resource (resource_at w loc))) (@core resource Join_resource Sep_resource (resource_at w loc)) *)
  intros.
(* Goal: @identity resource Join_resource (resource_at (@core rmap Join_rmap Sep_rmap m) i) *)
  generalize (core_duplicable m); intro Hdup. apply (resource_at_join _ _ _ i) in Hdup.
(* Goal: @identity resource Join_resource (resource_at (@core rmap Join_rmap Sep_rmap m) i) *)
  apply identity_resource.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
  case_eq (core m @ i); intros; auto.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
  rewrite H in Hdup. inv Hdup. apply identity_unit_equiv; auto.
(* Goal: False *)
  rewrite H in Hdup. inv Hdup.
  clear - r RJ.
(* Goal: @eq resource (NO sh1 nsh1) (NO Share.bot bot_unreadable) *)
  apply unit_identity in RJ. apply identity_share_bot in RJ.
(* Goal: False *)
  subst. apply bot_unreadable in r. auto.
Qed.

Lemma YES_inj: forall sh rsh k pp sh' rsh' k' pp',
           YES sh rsh k pp = YES sh' rsh' k' pp' ->
            (sh,k,pp) = (sh',k',pp').
Proof. intros. inv H. auto. Qed.

Lemma SomeP_inj1: forall t t' a a', SomeP t a = SomeP t' a' -> t=t'.
  Proof. intros. inv H; auto. Qed.
Lemma SomeP_inj2: forall t a a', SomeP t a = SomeP t a' -> a=a'.
  Proof. intros. inv H. apply inj_pair2 in H1. auto. Qed.
Lemma SomeP_inj:
   forall T a b, SomeP T a = SomeP T b -> a=b.
(* Goal: forall (w : rmap) (loc : AV.address), @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (@core resource Join_resource Sep_resource (resource_at w loc))) (@core resource Join_resource Sep_resource (resource_at w loc)) *)
Proof. intros. inv H. apply inj_pair2 in H1. auto.
Qed.

Lemma PURE_inj: forall T x x' y y', PURE x (SomeP T y) = PURE x' (SomeP T y') -> x=x' /\ y=y'.
(* Goal: forall (w : rmap) (loc : AV.address), @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (@core resource Join_resource Sep_resource (resource_at w loc))) (@core resource Join_resource Sep_resource (resource_at w loc)) *)
 Proof. intros. inv H. apply inj_pair2 in H2. subst; auto.
 Qed.

Lemma core_resource_at: forall w i, core (w @ i) = core w @ i.
Proof.
(* Goal: forall (w : rmap) (loc : AV.address), @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (@core resource Join_resource Sep_resource (resource_at w loc))) (@core resource Join_resource Sep_resource (resource_at w loc)) *)
 intros.
(* Goal: @eq resource (@core resource Join_resource Sep_resource (resource_at w i)) (resource_at (@core rmap Join_rmap Sep_rmap w) i) *)
 replace (core w @ i) with (core (core w @ i)).
(* Goal: @eq resource (@core resource Join_resource Sep_resource (resource_at w i)) (@core resource Join_resource Sep_resource (resource_at (@core rmap Join_rmap Sep_rmap w) i)) *)
(* Goal: @eq resource (@core resource Join_resource Sep_resource (resource_at (@core rmap Join_rmap Sep_rmap w) i)) (resource_at (@core rmap Join_rmap Sep_rmap w) i) *)
 pose proof (core_unit (w @ i)) as H1.
(* Goal: @eq resource (@core resource Join_resource Sep_resource (resource_at w i)) (@core resource Join_resource Sep_resource (resource_at (@core rmap Join_rmap Sep_rmap w) i)) *)
(* Goal: @eq resource (@core resource Join_resource Sep_resource (resource_at (@core rmap Join_rmap Sep_rmap w) i)) (resource_at (@core rmap Join_rmap Sep_rmap w) i) *)
 pose proof (core_unit w) as H2.
(* Goal: @eq resource (@core resource Join_resource Sep_resource (resource_at w i)) (@core resource Join_resource Sep_resource (resource_at (@core rmap Join_rmap Sep_rmap w) i)) *)
(* Goal: @eq resource (@core resource Join_resource Sep_resource (resource_at (@core rmap Join_rmap Sep_rmap w) i)) (resource_at (@core rmap Join_rmap Sep_rmap w) i) *)
 apply (resource_at_join _ _ _ i) in H2.
 unfold unit_for in *.
 rewrite <- core_idem.
(* Goal: @eq resource (@core resource Join_resource Sep_resource (@core resource Join_resource Sep_resource (resource_at w i))) (@core resource Join_resource Sep_resource (resource_at (@core rmap Join_rmap Sep_rmap w) i)) *)
(* Goal: @eq resource (@core resource Join_resource Sep_resource (resource_at (@core rmap Join_rmap Sep_rmap w) i)) (resource_at (@core rmap Join_rmap Sep_rmap w) i) *)
 destruct (join_assoc (join_comm H1) (join_comm H2)) as [? [? ?]].
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
 eapply join_core2; eauto.
(* Goal: @eq resource (@core resource Join_resource Sep_resource (resource_at (@core rmap Join_rmap Sep_rmap w) i)) (resource_at (@core rmap Join_rmap Sep_rmap w) i) *)
 symmetry; apply identity_core, resource_at_core_identity.
Qed.

Lemma core_ghost_of: forall w, core (ghost_of w) = ghost_of (core w).
Proof.
(* Goal: forall w : rmap, @eq ghost (@core ghost ghost_join Sep_ghost (ghost_of w)) (ghost_of (@core rmap Join_rmap Sep_rmap w)) *)
 symmetry; apply ghost_of_core.
Qed.

Lemma ghost_of_core_identity: forall m, identity (ghost_of (core m)).
Proof.
  intro; rewrite <- core_ghost_of; apply core_identity.
Qed.

Lemma resource_at_identity: forall (m: rmap) (loc: AV.address),
 identity m -> identity (m @ loc).
Proof.
(* Goal: forall (w : rmap) (loc : AV.address), @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (@core resource Join_resource Sep_resource (resource_at w loc))) (@core resource Join_resource Sep_resource (resource_at w loc)) *)
 intros.
 replace m with (core m) in * by (symmetry; apply identity_core; auto).
(* Goal: @identity resource Join_resource (resource_at (@core rmap Join_rmap Sep_rmap m) loc) *)
 apply resource_at_core_identity.
Qed.

Lemma ghost_of_identity: forall (m : rmap),
 identity m -> identity (ghost_of m).
Proof.
(* Goal: forall (w : rmap) (loc : AV.address), @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (@core resource Join_resource Sep_resource (resource_at w loc))) (@core resource Join_resource Sep_resource (resource_at w loc)) *)
 intros.
 replace m with (core m) in * by (symmetry; apply identity_core; auto).
(* Goal: @identity ghost ghost_join (ghost_of (@core rmap Join_rmap Sep_rmap m)) *)
 apply ghost_of_core_identity.
Qed.

Lemma core_YES: forall sh rsh k pp, core (YES sh rsh k pp) = NO Share.bot bot_unreadable.
Proof.
(* Goal: forall (w : rmap) (loc : AV.address), @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (@core resource Join_resource Sep_resource (resource_at w loc))) (@core resource Join_resource Sep_resource (resource_at w loc)) *)
 intros. generalize (core_unit (YES sh rsh k pp)); unfold unit_for; intros. 
(* Goal: @eq resource (@core resource Join_resource Sep_resource (PURE k pp)) (PURE k pp) *)
 inv H; auto.
(* Goal: @eq resource (NO sh1 nsh1) (NO Share.bot bot_unreadable) *)
 apply unit_identity in RJ. apply identity_share_bot in RJ. subst; auto.
(* Goal: @eq resource (NO Share.bot nsh1) (NO Share.bot bot_unreadable) *)
 f_equal. apply proof_irr.
 clear - H1.
(* Goal: @eq resource (YES sh1 rsh1 k pp) (NO Share.bot bot_unreadable) *)
 pose proof (core_unit (YES sh rsh k pp)).
(* Goal: @eq resource (YES sh1 rsh1 k pp) (NO Share.bot bot_unreadable) *)
 hnf in H. inv H.
 rewrite <- H2 in H1. inv H1.
 rewrite <- H2 in H1. inv H1.
(* Goal: @eq resource (NO sh1 nsh1) (NO Share.bot bot_unreadable) *)
 apply unit_identity in RJ. apply identity_share_bot in RJ. subst sh0.
(* Goal: @eq resource (YES Share.bot rsh1 k pp) (NO Share.bot bot_unreadable) *)
 contradiction (bot_unreadable rsh0).
Qed.

Lemma core_NO: forall sh nsh, core (NO sh nsh) = NO Share.bot bot_unreadable.
Proof.
(* Goal: forall (w : rmap) (loc : AV.address), @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (@core resource Join_resource Sep_resource (resource_at w loc))) (@core resource Join_resource Sep_resource (resource_at w loc)) *)
 intros.  generalize (core_unit (NO sh nsh)); unfold unit_for; intros.
(* Goal: @eq resource (@core resource Join_resource Sep_resource (PURE k pp)) (PURE k pp) *)
 inv H; auto.
(* Goal: @eq resource (NO sh1 nsh1) (NO Share.bot bot_unreadable) *)
 pose proof (core_unit (NO sh nsh)).
(* Goal: @eq resource (NO sh1 nsh1) (NO Share.bot bot_unreadable) *)
 apply unit_identity in RJ. apply identity_share_bot in RJ. subst sh1.
(* Goal: @eq resource (NO Share.bot nsh1) (NO Share.bot bot_unreadable) *)
 f_equal. apply proof_irr.
Qed.

Lemma core_PURE: forall k pp, core (PURE k pp) = PURE k pp.
Proof.
(* Goal: forall (w : rmap) (loc : AV.address), @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (@core resource Join_resource Sep_resource (resource_at w loc))) (@core resource Join_resource Sep_resource (resource_at w loc)) *)
 intros. generalize (core_unit (PURE k pp)); unfold unit_for; intros.
(* Goal: @eq resource (@core resource Join_resource Sep_resource (PURE k pp)) (PURE k pp) *)
 inv H; auto.
Qed.

Lemma core_not_YES: forall {w loc rsh sh k pp},
   core w @ loc = YES rsh sh k pp -> False.
Proof.
(* Goal: forall (w : rmap) (loc : AV.address), @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (@core resource Join_resource Sep_resource (resource_at w loc))) (@core resource Join_resource Sep_resource (resource_at w loc)) *)
intros.
(* Goal: False *)
pose proof (core_duplicable w) as Hj.
(* Goal: False *)
apply (resource_at_join _ _ _ loc) in Hj; rewrite H in Hj.
(* Goal: False *)
inv Hj.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
eapply readable_nonidentity; eauto.
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
eapply unit_identity; eauto.
Qed.

Lemma resource_at_empty2:
 forall phi: rmap, (forall l, identity (phi @ l)) -> identity (ghost_of phi) -> identity phi.
Proof.
  apply all_resource_at_identity. (* This was already proved. *)
Qed.

Lemma resource_fmap_core:
  forall w loc, resource_fmap (approx (level w)) (approx (level w)) (core (w @ loc)) = core (w @ loc).
Proof.
(* Goal: forall (w : rmap) (loc : AV.address), @eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (@core resource Join_resource Sep_resource (resource_at w loc))) (@core resource Join_resource Sep_resource (resource_at w loc)) *)
intros.
case_eq (w @ loc); intros;
(* Goal: @eq (forall ts : list Type, _functor (dependent_type_functor_rec ts T) (@pred rmap ag_rmap)) a b *)
 [rewrite core_NO | rewrite core_YES | rewrite core_PURE]; auto.
rewrite <- H. apply resource_at_approx.
Qed.

End Rmaps_Lemmas.
