Require Import VST.msl.log_normalize.
Require Import VST.msl.ghost.
Require Import VST.msl.ghost_seplog.
Require Export VST.veric.base.
Require Import VST.veric.rmaps.
Require Import VST.veric.compcert_rmaps.
Require Import VST.veric.res_predicates.

Import RML. Import R.
Local Open Scope pred.

Notation ghost_approx m := (ghost_fmap (approx (level m)) (approx (level m))).

(* Ownership construction based on "Iris from the ground up", Jung et al. *)
Program Definition ghost_is g: pred rmap :=
  fun m => ghost_of m = ghost_approx m g.
Next Obligation.
(* Goal: forall g : ghost, (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun m : rmap => @eq ghost (ghost_of m) (ghost_fmap (approx (@level rmap ag_rmap m)) (approx (@level rmap ag_rmap m)) g)) *)
  intros ???? Hg.
(* Goal: @eq ghost (ghost_of a') (ghost_fmap (approx (@level rmap ag_rmap a')) (approx (@level rmap ag_rmap a')) g) *)
  rewrite (age1_ghost_of _ _ H), Hg.
(* Goal: @ex ghost (fun b : ghost => and (@joins ghost ghost_join b (ghost_fmap (approx (@level rmap ag_rmap a')) (approx (@level rmap ag_rmap a')) c)) (@ex rmap (fun m' : rmap => and (@eq nat (@level rmap ag_rmap m') (@level rmap ag_rmap a')) (and (@eq (forall _ : AV.address, resource) (resource_at m') (resource_at a')) (and (@eq ghost (ghost_of m') b) (@app_pred rmap ag_rmap P m')))))) *)
  pose proof (age_level _ _ H).
(* Goal: @eq ghost (ghost_fmap (approx (@level rmap ag_rmap a')) (approx (@level rmap ag_rmap a')) (ghost_fmap (approx (@level rmap ag_rmap a)) (approx (@level rmap ag_rmap a)) g)) (ghost_fmap (approx (@level rmap ag_rmap a')) (approx (@level rmap ag_rmap a')) g) *)
  rewrite ghost_fmap_fmap, approx_oo_approx', approx'_oo_approx by omega; eauto.
Qed.

Definition Own g: pred rmap := allp noat && ghost_is g.

Lemma Own_op: forall a b c, join a b c -> Own c = Own a * Own b.
Proof.
  intros; apply pred_ext.
  - intros w (Hno & Hg).
    destruct (make_rmap (resource_at w) (ghost_approx w a) (level w))
      as (wa & Hla & Hra & Hga).
(* Goal: @eq (forall _ : AV.address, resource) (@compose AV.address resource resource (resource_fmap (approx (@level rmap ag_rmap a)) (approx (@level rmap ag_rmap a))) (resource_at a)) (resource_at a) *)
(* Goal: @ex rmap (fun m' : rmap => and (@eq nat (@level rmap ag_rmap m') (@level rmap ag_rmap a)) (and (@eq (forall _ : AV.address, resource) (resource_at m') (resource_at a)) (and (@eq ghost (ghost_of m') (@nil (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)))) (@app_pred rmap ag_rmap (@emp rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap) m')))) *)
    { extensionality; apply resource_at_approx. }
(* Goal: @eq (forall _ : AV.address, resource) (@compose AV.address resource resource (resource_fmap (approx (@level rmap ag_rmap a)) (approx (@level rmap ag_rmap a))) (resource_at a)) (resource_at a) *)
(* Goal: @ex rmap (fun m' : rmap => and (@eq nat (@level rmap ag_rmap m') (@level rmap ag_rmap a)) (and (@eq (forall _ : AV.address, resource) (resource_at m') (resource_at a)) (and (@eq ghost (ghost_of m') (@nil (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)))) (@app_pred rmap ag_rmap (@emp rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap) m')))) *)
    { rewrite ghost_fmap_fmap, approx_oo_approx; auto. }
    destruct (make_rmap (resource_at w) (ghost_approx w b) (level w))
      as (wb & Hlb & Hrb & Hgb).
(* Goal: @eq (forall _ : AV.address, resource) (@compose AV.address resource resource (resource_fmap (approx (@level rmap ag_rmap a)) (approx (@level rmap ag_rmap a))) (resource_at a)) (resource_at a) *)
(* Goal: @ex rmap (fun m' : rmap => and (@eq nat (@level rmap ag_rmap m') (@level rmap ag_rmap a)) (and (@eq (forall _ : AV.address, resource) (resource_at m') (resource_at a)) (and (@eq ghost (ghost_of m') (@nil (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)))) (@app_pred rmap ag_rmap (@emp rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap) m')))) *)
    { extensionality; apply resource_at_approx. }
(* Goal: @eq (forall _ : AV.address, resource) (@compose AV.address resource resource (resource_fmap (approx (@level rmap ag_rmap a)) (approx (@level rmap ag_rmap a))) (resource_at a)) (resource_at a) *)
(* Goal: @ex rmap (fun m' : rmap => and (@eq nat (@level rmap ag_rmap m') (@level rmap ag_rmap a)) (and (@eq (forall _ : AV.address, resource) (resource_at m') (resource_at a)) (and (@eq ghost (ghost_of m') (@nil (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)))) (@app_pred rmap ag_rmap (@emp rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap) m')))) *)
    { rewrite ghost_fmap_fmap, approx_oo_approx; auto. }
    exists wa, wb; split.
    + apply resource_at_join2; auto.
      * intro; rewrite Hra, Hrb.
        apply identity_unit', Hno.
      * rewrite Hg, Hga, Hgb.
        apply ghost_fmap_join; auto.
    + simpl; rewrite Hla, Hlb, Hra, Hrb, Hga, Hgb; simpl; eauto 6.
  - intros w (w1 & w2 & J & (Hnoa & Hga) & (Hnob & Hgb)).
(* Goal: iff (@join (list (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds))) ghost_join (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) (@Some (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds) a) (@nil (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)))) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) (@Some (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds) b) (@nil (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)))) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) (@Some (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds) c) (@nil (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds))))) (@join (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds) (Join_prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) ghost_elem_join preds preds_join) a b c) *)
    split.
    + intro l; apply (resource_at_join _ _ _ l) in J.
      simpl in *; rewrite <- (Hnoa _ _ _ J); auto.
    + destruct (join_level _ _ _ J) as [Hl1 Hl2].
      apply ghost_of_join in J.
      rewrite Hga, Hgb in J.
      eapply join_eq; eauto.
      rewrite Hl1, Hl2; apply ghost_fmap_join; auto.
Qed.

Fixpoint make_join (a c : ghost) : ghost :=
  match a, c with
  | nil, _ => c
  | _, nil => nil
  | None :: a', x :: c' => x :: make_join a' c'
  | _ :: a', None :: c' => None :: make_join a' c'
  | Some (ga, pa) :: a', Some (gc, _) :: c' => Some (gc, pa) :: make_join a' c'
  end.

Lemma make_join_nil : forall a, make_join a nil = nil.
Proof.
(* Goal: forall a : ghost, @eq ghost (make_join a (@nil (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a0 : @G g => @valid g a0))) preds)))) (@nil (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a0 : @G g => @valid g a0))) preds))) *)
  destruct a; auto.
(* Goal: forall (o : option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) (a : list (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds))) (c : list (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a0 : @G g => @valid g a0))) preds))), @eq ghost (make_join (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a0 : @G g => @valid g a0))) preds)) o a) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a0 : @G g => @valid g a0))) preds)) (@None (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a0 : @G g => @valid g a0))) preds)) c)) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a0 : @G g => @valid g a0))) preds)) (@None (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a0 : @G g => @valid g a0))) preds)) (make_join a c)) *)
  destruct o as [[]|]; auto.
Qed.

Lemma make_join_nil_cons : forall o a c, make_join (o :: a) (None :: c) = None :: make_join a c.
Proof.
(* Goal: forall (o : option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) (a : list (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds))) (c : list (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a0 : @G g => @valid g a0))) preds))), @eq ghost (make_join (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a0 : @G g => @valid g a0))) preds)) o a) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a0 : @G g => @valid g a0))) preds)) (@None (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a0 : @G g => @valid g a0))) preds)) c)) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a0 : @G g => @valid g a0))) preds)) (@None (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a0 : @G g => @valid g a0))) preds)) (make_join a c)) *)
  destruct o as [[]|]; auto.
Qed.

Lemma ghost_joins_approx: forall n a c,
  joins (ghost_fmap (approx n) (approx n) a) (ghost_fmap (approx n) (approx n) c) ->
  let c' := make_join a c in
  joins (ghost_fmap (approx (S n)) (approx (S n)) a) (ghost_fmap (approx (S n)) (approx (S n)) c') /\
    forall b, joins b (ghost_fmap (approx (S n)) (approx (S n)) c') ->
      joins (ghost_fmap (approx n) (approx n) b) (ghost_fmap (approx n) (approx n) c).
Proof.
  intros ???; revert a; induction c; intros; subst c'; simpl.
  - rewrite make_join_nil; split.
    + eexists; constructor.
    + eexists; constructor.
  - destruct H; inv H.
    + destruct a0; inv H1.
(* Goal: iff (@join (list (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds))) ghost_join (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) (@Some (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds) a) (@nil (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)))) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) (@Some (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds) b) (@nil (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)))) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) (@Some (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds) c) (@nil (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds))))) (@join (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds) (Join_prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) ghost_elem_join preds preds_join) a b c) *)
      split.
(* Goal: @eq (forall _ : AV.address, resource) (@compose AV.address resource resource (resource_fmap (approx (@level rmap ag_rmap a)) (approx (@level rmap ag_rmap a))) (resource_at a)) (resource_at a) *)
(* Goal: @ex rmap (fun m' : rmap => and (@eq nat (@level rmap ag_rmap m') (@level rmap ag_rmap a)) (and (@eq (forall _ : AV.address, resource) (resource_at m') (resource_at a)) (and (@eq ghost (ghost_of m') (@nil (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)))) (@app_pred rmap ag_rmap (@emp rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap) m')))) *)
      { eexists; constructor. }
      intros ? []; eexists.
      apply ghost_fmap_join with (f := approx n)(g := approx n) in H.
      rewrite ghost_fmap_fmap, approx_oo_approx', approx'_oo_approx in H by auto; eauto.
    + destruct a0; inv H0.
      destruct (IHc a0) as (H & Hc'); eauto.
      inv H3.
      * destruct o; inv H1.
(* Goal: iff (@join (list (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds))) ghost_join (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) (@Some (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds) a) (@nil (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)))) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) (@Some (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds) b) (@nil (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)))) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) (@Some (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds) c) (@nil (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds))))) (@join (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds) (Join_prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) ghost_elem_join preds preds_join) a b c) *)
        split.
(* Goal: @eq (forall _ : AV.address, resource) (@compose AV.address resource resource (resource_fmap (approx (@level rmap ag_rmap a)) (approx (@level rmap ag_rmap a))) (resource_at a)) (resource_at a) *)
(* Goal: @ex rmap (fun m' : rmap => and (@eq nat (@level rmap ag_rmap m') (@level rmap ag_rmap a)) (and (@eq (forall _ : AV.address, resource) (resource_at m') (resource_at a)) (and (@eq ghost (ghost_of m') (@nil (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)))) (@app_pred rmap ag_rmap (@emp rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap) m')))) *)
        { destruct H; eexists; constructor; eauto; constructor. }
        intros ? [? J]; inv J; [eexists; constructor|].
        destruct (Hc' m1); eauto.
        eexists; constructor; eauto.
        instantiate (1 := option_map (fun '(a, b) => (a, preds_fmap (approx n) (approx n) b)) a3).
        inv H3.
        -- destruct a as [[]|]; [simpl | constructor].
           rewrite preds_fmap_fmap, approx_oo_approx', approx'_oo_approx by auto; constructor; auto.
        -- destruct a; inv H4; constructor.
        -- destruct a as [[]|]; inv H1; constructor.
           destruct a2, a5; inv H4; constructor; auto; simpl in *.
           inv H2.
           rewrite preds_fmap_fmap, approx_oo_approx', approx'_oo_approx by auto; constructor; auto.
      * destruct a; inv H2.
        rewrite make_join_nil_cons.
(* Goal: iff (@join (list (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds))) ghost_join (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) (@Some (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds) a) (@nil (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)))) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) (@Some (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds) b) (@nil (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)))) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) (@Some (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds) c) (@nil (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds))))) (@join (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds) (Join_prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) ghost_elem_join preds preds_join) a b c) *)
        split.
(* Goal: @eq (forall _ : AV.address, resource) (@compose AV.address resource resource (resource_fmap (approx (@level rmap ag_rmap a)) (approx (@level rmap ag_rmap a))) (resource_at a)) (resource_at a) *)
(* Goal: @ex rmap (fun m' : rmap => and (@eq nat (@level rmap ag_rmap m') (@level rmap ag_rmap a)) (and (@eq (forall _ : AV.address, resource) (resource_at m') (resource_at a)) (and (@eq ghost (ghost_of m') (@nil (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)))) (@app_pred rmap ag_rmap (@emp rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap) m')))) *)
        { destruct H; eexists; constructor; eauto; constructor. }
        intros ? [? J]; inv J; [eexists; constructor|].
        destruct (Hc' m1); eauto.
        eexists; constructor; eauto; constructor.
      * destruct o as [[]|], a as [[]|]; inv H0; inv H1.
(* Goal: iff (@join (list (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds))) ghost_join (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) (@Some (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds) a) (@nil (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)))) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) (@Some (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds) b) (@nil (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)))) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) (@Some (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds) c) (@nil (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds))))) (@join (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds) (Join_prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) ghost_elem_join preds preds_join) a b c) *)
        split.
(* Goal: @eq (forall _ : AV.address, resource) (@compose AV.address resource resource (resource_fmap (approx (@level rmap ag_rmap a)) (approx (@level rmap ag_rmap a))) (resource_at a)) (resource_at a) *)
(* Goal: @ex rmap (fun m' : rmap => and (@eq nat (@level rmap ag_rmap m') (@level rmap ag_rmap a)) (and (@eq (forall _ : AV.address, resource) (resource_at m') (resource_at a)) (and (@eq ghost (ghost_of m') (@nil (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)))) (@app_pred rmap ag_rmap (@emp rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap) m')))) *)
        { destruct H.
          destruct a4; inv H2; simpl in *.
          inv H1.
          eexists (Some (_, _) :: _); constructor; eauto; constructor.
          constructor; simpl; eauto; constructor; eauto. }
        intros ? [? J]; inv J; [eexists; constructor|].
        destruct (Hc' m1); eauto.
        eexists; constructor; eauto.
        instantiate (1 := option_map (fun '(a, b) => (a, preds_fmap (approx n) (approx n) b)) a3).
        inv H4.
        -- destruct a4; inv H2; simpl in *.
           inv H3.
           rewrite <- H2, preds_fmap_fmap, approx_oo_approx', approx'_oo_approx by auto; constructor.
        -- constructor.
           destruct a2, a4, a6; inv H2; inv H6; constructor; auto; simpl in *.
           inv H3; inv H4.
           rewrite <- H6, preds_fmap_fmap, approx_oo_approx', approx'_oo_approx by auto; constructor; auto.
Qed.

Program Definition bupd (P: pred rmap): pred rmap :=
  fun m => forall c, joins (ghost_of m) (ghost_approx m c) ->
    exists b, joins b (ghost_approx m c) /\
    exists m', level m' = level m /\ resource_at m' = resource_at m /\ ghost_of m' = b /\ P m'.
Next Obligation.
Proof.
(* Goal: forall w : rmap, (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun w' : rmap => @necR rmap ag_rmap w w') *)
  repeat intro.
(* Goal: @ex ghost (fun b : ghost => and (@joins ghost ghost_join b (ghost_fmap (approx (@level rmap ag_rmap a')) (approx (@level rmap ag_rmap a')) c)) (@ex rmap (fun m' : rmap => and (@eq nat (@level rmap ag_rmap m') (@level rmap ag_rmap a')) (and (@eq (forall _ : AV.address, resource) (resource_at m') (resource_at a')) (and (@eq ghost (ghost_of m') b) (@app_pred rmap ag_rmap P m')))))) *)
  rewrite (age1_ghost_of _ _ H) in H1.
  rewrite <- ghost_of_approx in H0.
(* Goal: @ex ghost (fun b : ghost => and (@joins ghost ghost_join b (ghost_fmap (approx (@level rmap ag_rmap a')) (approx (@level rmap ag_rmap a')) c)) (@ex rmap (fun m' : rmap => and (@eq nat (@level rmap ag_rmap m') (@level rmap ag_rmap a')) (and (@eq (forall _ : AV.address, resource) (resource_at m') (resource_at a')) (and (@eq ghost (ghost_of m') b) (@app_pred rmap ag_rmap P m')))))) *)
  destruct (ghost_joins_approx _ _ _ H1) as (J0 & Hc0).
  rewrite <- (age_level _ _ H) in *.
(* Goal: @ex ghost (fun b : ghost => and (@joins ghost ghost_join b (ghost_fmap (approx (@level rmap ag_rmap a')) (approx (@level rmap ag_rmap a')) c)) (@ex rmap (fun m' : rmap => and (@eq nat (@level rmap ag_rmap m') (@level rmap ag_rmap a')) (and (@eq (forall _ : AV.address, resource) (resource_at m') (resource_at a')) (and (@eq ghost (ghost_of m') b) (@app_pred rmap ag_rmap P m')))))) *)
  specialize (H0 _ J0); destruct H0 as (b & J & Hrb).
(* Goal: @ex ghost (fun b : ghost => and (@joins ghost ghost_join b (ghost_fmap (approx (@level rmap ag_rmap a')) (approx (@level rmap ag_rmap a')) c)) (@ex rmap (fun m' : rmap => and (@eq nat (@level rmap ag_rmap m') (@level rmap ag_rmap a')) (and (@eq (forall _ : AV.address, resource) (resource_at m') (resource_at a')) (and (@eq ghost (ghost_of m') b) (@app_pred rmap ag_rmap P m')))))) *)
  pose proof (age_level _ _ H).
(* Goal: @ex ghost (fun b : ghost => and (@joins ghost ghost_join b (ghost_fmap (approx (@level rmap ag_rmap a')) (approx (@level rmap ag_rmap a')) c)) (@ex rmap (fun m' : rmap => and (@eq nat (@level rmap ag_rmap m') (@level rmap ag_rmap a')) (and (@eq (forall _ : AV.address, resource) (resource_at m') (resource_at a')) (and (@eq ghost (ghost_of m') b) (@app_pred rmap ag_rmap P m')))))) *)
  exists (ghost_approx a' b); split; auto.
(* Goal: @ex rmap (fun m' : rmap => and (@eq nat (@level rmap ag_rmap m') (@level rmap ag_rmap a')) (and (@eq (forall _ : AV.address, resource) (resource_at m') (resource_at a')) (and (@eq ghost (ghost_of m') (ghost_fmap (approx (@level rmap ag_rmap a')) (approx (@level rmap ag_rmap a')) b)) (@app_pred rmap ag_rmap P m')))) *)
  destruct Hrb as (m' & Hl' & Hr' & Hg' & HP).
(* Goal: @ex rmap (fun m' : rmap => and (@eq nat (@level rmap ag_rmap m') (@level rmap ag_rmap a')) (and (@eq (forall _ : AV.address, resource) (resource_at m') (resource_at a')) (and (@eq ghost (ghost_of m') (ghost_fmap (approx (@level rmap ag_rmap a')) (approx (@level rmap ag_rmap a')) b)) (@app_pred rmap ag_rmap P m')))) *)
  destruct (levelS_age m' (level a')) as (m'' & Hage' & Hl'').
(* Goal: @eq (forall _ : AV.address, resource) (@compose AV.address resource resource (resource_fmap (approx (@level rmap ag_rmap a)) (approx (@level rmap ag_rmap a))) (resource_at a)) (resource_at a) *)
(* Goal: @ex rmap (fun m' : rmap => and (@eq nat (@level rmap ag_rmap m') (@level rmap ag_rmap a)) (and (@eq (forall _ : AV.address, resource) (resource_at m') (resource_at a)) (and (@eq ghost (ghost_of m') (@nil (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)))) (@app_pred rmap ag_rmap (@emp rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap) m')))) *)
  { congruence. }
(* Goal: @ex rmap (fun m' : rmap => and (@eq nat (@level rmap ag_rmap m') (@level rmap ag_rmap a')) (and (@eq (forall _ : AV.address, resource) (resource_at m') (resource_at a')) (and (@eq ghost (ghost_of m') (ghost_fmap (approx (@level rmap ag_rmap a')) (approx (@level rmap ag_rmap a')) b)) (@app_pred rmap ag_rmap P m')))) *)
  exists m''; repeat split; auto.
  + extensionality l.
(* Goal: @eq resource (resource_at m'' l) (resource_at a' l) *)
    erewrite (age1_resource_at _ _ H l) by (symmetry; apply resource_at_approx).
(* Goal: @eq resource (resource_at m'' l) (resource_fmap (approx (@level rmap ag_rmap a')) (approx (@level rmap ag_rmap a')) (resource_at a l)) *)
    erewrite (age1_resource_at _ _ Hage' l) by (symmetry; apply resource_at_approx).
(* Goal: @eq resource (resource_fmap (approx (@level rmap ag_rmap m'')) (approx (@level rmap ag_rmap m'')) (resource_at m' l)) (resource_fmap (approx (@level rmap ag_rmap a')) (approx (@level rmap ag_rmap a')) (resource_at a l)) *)
    congruence.
  + rewrite (age1_ghost_of _ _ Hage').
    rewrite Hg', <- Hl''; auto.
  + eapply (proj2_sig P); eauto.
Qed.

Lemma bupd_intro: forall P, P |-- bupd P.
Proof.
(* Goal: forall P : @pred rmap ag_rmap, @derives rmap ag_rmap P (bupd P) *)
  repeat intro; eauto 7.
Qed.

Lemma bupd_mono: forall P Q, P |-- Q -> bupd P |-- bupd Q.
Proof.
(* Goal: forall w : rmap, (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun w' : rmap => @necR rmap ag_rmap w w') *)
  repeat intro.
  simpl in *.
(* Goal: @ex ghost (fun b : ghost => and (@joins ghost ghost_join b (ghost_fmap (approx (@level rmap ag_rmap a)) (approx (@level rmap ag_rmap a)) c)) (@ex rmap (fun m' : rmap => and (@eq nat (@level rmap ag_rmap m') (@level rmap ag_rmap a)) (and (@eq (forall _ : AV.address, resource) (resource_at m') (resource_at a)) (and (@eq ghost (ghost_of m') b) (@app_pred rmap ag_rmap Q m')))))) *)
  destruct (H0 _ H1) as (b & ? & m' & ? & ? & ? & ?).
(* Goal: @ex ghost (fun b : ghost => and (@joins ghost ghost_join b (ghost_fmap (approx (@level rmap ag_rmap a)) (approx (@level rmap ag_rmap a)) c)) (@ex rmap (fun m' : rmap => and (@eq nat (@level rmap ag_rmap m') (@level rmap ag_rmap a)) (and (@eq (forall _ : AV.address, resource) (resource_at m') (resource_at a)) (and (@eq ghost (ghost_of m') b) (@app_pred rmap ag_rmap Q m')))))) *)
  exists b; split; auto.
(* Goal: @ex rmap (fun m' : rmap => and (@eq nat (@level rmap ag_rmap m') (@level rmap ag_rmap a)) (and (@eq (forall _ : AV.address, resource) (resource_at m') (resource_at a)) (and (@eq ghost (ghost_of m') (@nil (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)))) (@app_pred rmap ag_rmap (@emp rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap) m')))) *)
  exists m'; repeat split; auto.
Qed.

Lemma bupd_frame_r: forall P Q, bupd P * Q |-- bupd (P * Q).
Proof.
(* Goal: forall w : rmap, (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun w' : rmap => @necR rmap ag_rmap w w') *)
  repeat intro.
  destruct H as (w1 & w2 & J & HP & HQ).
  destruct (join_level _ _ _ J) as [Hl1 Hl2].
  pose proof (ghost_of_join _ _ _ J) as Jg.
  destruct H0 as [? J'].
  destruct (join_assoc Jg J') as (c' & J1 & J2).
  erewrite <- (ghost_same_level_gen (level a) (ghost_of w2) c c') in J2, J1
    by (rewrite <- Hl2 at 1 2; rewrite ghost_of_approx; auto).
  destruct (HP c') as (? & [? J1'] & w1' & ? & Hr' & ? & HP'); subst.
(* Goal: @eq (forall _ : AV.address, resource) (@compose AV.address resource resource (resource_fmap (approx (@level rmap ag_rmap a)) (approx (@level rmap ag_rmap a))) (resource_at a)) (resource_at a) *)
(* Goal: @ex rmap (fun m' : rmap => and (@eq nat (@level rmap ag_rmap m') (@level rmap ag_rmap a)) (and (@eq (forall _ : AV.address, resource) (resource_at m') (resource_at a)) (and (@eq ghost (ghost_of m') (@nil (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)))) (@app_pred rmap ag_rmap (@emp rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap) m')))) *)
  { rewrite Hl1; eauto. }
  rewrite Hl1 in J1'; destruct (join_assoc (join_comm J1) (join_comm J1')) as (w' & ? & ?).
  exists w'; split; [eexists; apply join_comm; eauto|].
  destruct (make_rmap (resource_at a) w' (level a)) as (m' & ? & Hr'' & ?); subst.
(* Goal: @eq (forall _ : AV.address, resource) (@compose AV.address resource resource (resource_fmap (approx (@level rmap ag_rmap a)) (approx (@level rmap ag_rmap a))) (resource_at a)) (resource_at a) *)
(* Goal: @ex rmap (fun m' : rmap => and (@eq nat (@level rmap ag_rmap m') (@level rmap ag_rmap a)) (and (@eq (forall _ : AV.address, resource) (resource_at m') (resource_at a)) (and (@eq ghost (ghost_of m') (@nil (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)))) (@app_pred rmap ag_rmap (@emp rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap) m')))) *)
  { extensionality l; apply resource_at_approx. }
(* Goal: @eq (forall _ : AV.address, resource) (@compose AV.address resource resource (resource_fmap (approx (@level rmap ag_rmap a)) (approx (@level rmap ag_rmap a))) (resource_at a)) (resource_at a) *)
(* Goal: @ex rmap (fun m' : rmap => and (@eq nat (@level rmap ag_rmap m') (@level rmap ag_rmap a)) (and (@eq (forall _ : AV.address, resource) (resource_at m') (resource_at a)) (and (@eq ghost (ghost_of m') (@nil (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)))) (@app_pred rmap ag_rmap (@emp rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap) m')))) *)
  { eapply ghost_same_level_gen.
    rewrite <- (ghost_of_approx w2), <- (ghost_of_approx w1'), H, Hl1, Hl2 in H0.
    apply join_comm; eauto. }
(* Goal: @ex rmap (fun m' : rmap => and (@eq nat (@level rmap ag_rmap m') (@level rmap ag_rmap a)) (and (@eq (forall _ : AV.address, resource) (resource_at m') (resource_at a)) (and (@eq ghost (ghost_of m') (@nil (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)))) (@app_pred rmap ag_rmap (@emp rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap) m')))) *)
  exists m'; repeat split; auto.
  exists w1', w2; repeat split; auto.
  apply resource_at_join2; auto; try omega.
  intro; rewrite Hr', Hr''.
  apply resource_at_join; auto.
Qed.

Lemma bupd_frame_l: forall P Q, P * bupd Q |-- bupd (P * Q).
Proof.
(* Goal: forall P Q : @pred rmap ag_rmap, @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P (bupd Q)) (bupd (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P Q)) *)
  intros; rewrite sepcon_comm, (sepcon_comm P Q); apply bupd_frame_r.
Qed.

Lemma bupd_trans: forall P, bupd (bupd P) |-- bupd P.
Proof.
(* Goal: forall w : rmap, (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun w' : rmap => @necR rmap ag_rmap w w') *)
  repeat intro.
(* Goal: @ex ghost (fun b : ghost => and (@joins ghost ghost_join b (ghost_fmap (approx (@level rmap ag_rmap a)) (approx (@level rmap ag_rmap a)) c)) (@ex rmap (fun m' : rmap => and (@eq nat (@level rmap ag_rmap m') (@level rmap ag_rmap a)) (and (@eq (forall _ : AV.address, resource) (resource_at m') (resource_at a)) (and (@eq ghost (ghost_of m') b) (@app_pred rmap ag_rmap P m')))))) *)
  destruct (H _ H0) as (b & J & a' & Hl & Hr & ? & Ha'); subst.
  rewrite <- Hl in J; destruct (Ha' _ J) as (b' & ? & Hm').
  rewrite <- Hl, <- Hr; eauto.
Qed.

Lemma bupd_prop : forall P, bupd (!! P) = !! P.
Proof.
  intros ?; apply pred_ext.
  - intros ??; simpl in *.
    destruct (H (core (ghost_of a))) as (? & ? & ? & ? & ? & ? & ?); auto.
    eexists.
    rewrite ghost_core; simpl; erewrite <- ghost_core.
    apply join_comm, core_unit.
  - intros ??.
    do 2 eexists; eauto.
Qed.

Lemma subp_bupd: forall (G : pred nat) (P P' : pred rmap), G |-- P >=> P' ->
    G |-- (bupd P >=> bupd P')%pred.
Proof.
(* Goal: forall w : rmap, (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun w' : rmap => @necR rmap ag_rmap w w') *)
  repeat intro.
(* Goal: @ex ghost (fun b : ghost => and (@joins ghost ghost_join b (ghost_fmap (approx (@level rmap ag_rmap a')) (approx (@level rmap ag_rmap a')) c)) (@ex rmap (fun m' : rmap => and (@eq nat (@level rmap ag_rmap m') (@level rmap ag_rmap a')) (and (@eq (forall _ : AV.address, resource) (resource_at m') (resource_at a')) (and (@eq ghost (ghost_of m') b) (@app_pred rmap ag_rmap P' m')))))) *)
  specialize (H3 _ H4) as (? & ? & ? & ? & ? & ? & HP).
(* Goal: @ex ghost (fun b : ghost => and (@joins ghost ghost_join b (ghost_fmap (approx (@level rmap ag_rmap a')) (approx (@level rmap ag_rmap a')) c)) (@ex rmap (fun m' : rmap => and (@eq nat (@level rmap ag_rmap m') (@level rmap ag_rmap a')) (and (@eq (forall _ : AV.address, resource) (resource_at m') (resource_at a')) (and (@eq ghost (ghost_of m') b) (@app_pred rmap ag_rmap P' m')))))) *)
  do 2 eexists; eauto; do 2 eexists; eauto; repeat (split; auto).
(* Goal: @app_pred rmap ag_rmap P' x0 *)
  pose proof (necR_level _ _ H2).
(* Goal: @app_pred rmap ag_rmap P' x0 *)
  apply (H _ H0 x0 ltac:(omega) _ (necR_refl _)); auto.
Qed.

Lemma eqp_bupd: forall (G : pred nat) (P P' : pred rmap), G |-- P <=> P' ->
    G |-- (bupd P <=> bupd P').
Proof.
(* Goal: forall (RA : Ghost) (g : gname) (a : @G RA) (pp : preds), @derives rmap ag_rmap (@own RA g a pp) (@prop rmap ag_rmap (@valid RA a)) *)
  intros.
  rewrite fash_and in *.
  apply andp_right; apply subp_bupd; eapply derives_trans; try apply H;
    [apply andp_left1 | apply andp_left2]; apply derives_refl.
Qed.

Definition ghost_fp_update_ND a B :=
  forall n c, joins (ghost_fmap (approx n) (approx n) a) c ->
    exists b, B b /\ joins (ghost_fmap (approx n) (approx n) b) c.

Lemma Own_update_ND: forall a B, ghost_fp_update_ND a B ->
  Own a |-- bupd (EX b : _, !!(B b) && Own b).
Proof.
(* Goal: forall w : rmap, (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun w' : rmap => @necR rmap ag_rmap w w') *)
  repeat intro.
  destruct H0 as (Hno & Hg).
  rewrite Hg in H1.
  destruct H1 as [? J].
  destruct (H (level a0) (ghost_approx a0 c)) as (g' & ? & J').
(* Goal: @eq (forall _ : AV.address, resource) (@compose AV.address resource resource (resource_fmap (approx (@level rmap ag_rmap a)) (approx (@level rmap ag_rmap a))) (resource_at a)) (resource_at a) *)
(* Goal: @ex rmap (fun m' : rmap => and (@eq nat (@level rmap ag_rmap m') (@level rmap ag_rmap a)) (and (@eq (forall _ : AV.address, resource) (resource_at m') (resource_at a)) (and (@eq ghost (ghost_of m') (@nil (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)))) (@app_pred rmap ag_rmap (@emp rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap) m')))) *)
  { eexists; eauto. }
  exists (ghost_fmap (approx (level a0)) (approx (level a0)) g'); split; auto.
  destruct (make_rmap (resource_at a0)
    (ghost_fmap (approx (level a0)) (approx (level a0)) g') (level a0))
    as (m' & Hl & Hr & Hg').
(* Goal: @eq (forall _ : AV.address, resource) (@compose AV.address resource resource (resource_fmap (approx (@level rmap ag_rmap a)) (approx (@level rmap ag_rmap a))) (resource_at a)) (resource_at a) *)
(* Goal: @ex rmap (fun m' : rmap => and (@eq nat (@level rmap ag_rmap m') (@level rmap ag_rmap a)) (and (@eq (forall _ : AV.address, resource) (resource_at m') (resource_at a)) (and (@eq ghost (ghost_of m') (@nil (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)))) (@app_pred rmap ag_rmap (@emp rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap) m')))) *)
  { extensionality; apply resource_at_approx. }
(* Goal: @eq (forall _ : AV.address, resource) (@compose AV.address resource resource (resource_fmap (approx (@level rmap ag_rmap a)) (approx (@level rmap ag_rmap a))) (resource_at a)) (resource_at a) *)
(* Goal: @ex rmap (fun m' : rmap => and (@eq nat (@level rmap ag_rmap m') (@level rmap ag_rmap a)) (and (@eq (forall _ : AV.address, resource) (resource_at m') (resource_at a)) (and (@eq ghost (ghost_of m') (@nil (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)))) (@app_pred rmap ag_rmap (@emp rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap) m')))) *)
  { rewrite ghost_fmap_fmap, approx_oo_approx; auto. }
(* Goal: @ex rmap (fun m' : rmap => and (@eq nat (@level rmap ag_rmap m') (@level rmap ag_rmap a)) (and (@eq (forall _ : AV.address, resource) (resource_at m') (resource_at a)) (and (@eq ghost (ghost_of m') (@nil (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)))) (@app_pred rmap ag_rmap (@emp rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap) m')))) *)
  exists m'; repeat split; auto.
  exists g'; repeat split; auto.
  - simpl in *; intro; rewrite Hr; auto.
  - simpl; rewrite Hg', Hl; simpl; eauto.
Qed.

Definition ghost_fp_update (a b : ghost) :=
  forall n c, joins (ghost_fmap (approx n) (approx n) a) c ->
               joins (ghost_fmap (approx n) (approx n) b) c.

Instance ghost_fp_update_preorder: RelationClasses.PreOrder ghost_fp_update.
Proof.
(* Goal: @RelationClasses.PreOrder ghost ghost_fp_update *)
  split; repeat intro; auto.
Qed.

Lemma ghost_fp_update_approx: forall a b n, ghost_fp_update a b ->
  ghost_fp_update (ghost_fmap (approx n) (approx n) a) (ghost_fmap (approx n) (approx n) b).
Proof.
(* Goal: forall (a b : ghost) (n : nat) (_ : ghost_fp_update a b), ghost_fp_update (ghost_fmap (approx n) (approx n) a) (ghost_fmap (approx n) (approx n) b) *)
  intros; intros m c J.
  rewrite ghost_fmap_fmap in *.
  replace (approx m oo approx n) with (approx (min m n)) in *.
  replace (approx n oo approx m) with (approx (min m n)) in *.
(* Goal: @joins ghost ghost_join (ghost_fmap (approx (Init.Nat.min m n)) (approx (Init.Nat.min m n)) b) c *)
(* Goal: @eq (forall _ : @pred rmap ag_rmap, @pred rmap ag_rmap) (approx (Init.Nat.min m n)) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx m)) *)
(* Goal: @eq (forall _ : @pred rmap ag_rmap, @pred rmap ag_rmap) (approx (Init.Nat.min m n)) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx m) (approx n)) *)
  auto.
  { destruct (Min.min_spec m n) as [[? ->] | [? ->]];
      [rewrite approx'_oo_approx | rewrite approx_oo_approx']; auto; omega. }
  { destruct (Min.min_spec m n) as [[? ->] | [? ->]];
      [rewrite approx_oo_approx' | rewrite approx'_oo_approx]; auto; omega. }
Qed.

Lemma Own_update: forall a b, ghost_fp_update a b ->
  Own a |-- bupd (Own b).
Proof.
  intros; eapply derives_trans.
  - eapply (Own_update_ND _ (eq _)).
(* Goal: forall w : rmap, (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun w' : rmap => @necR rmap ag_rmap w w') *)
    repeat intro.
    eexists; split; [constructor|].
(* Goal: @joins ghost ghost_join (ghost_fmap (approx (Init.Nat.min m n)) (approx (Init.Nat.min m n)) b) c *)
(* Goal: @eq (forall _ : @pred rmap ag_rmap, @pred rmap ag_rmap) (approx (Init.Nat.min m n)) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx m)) *)
(* Goal: @eq (forall _ : @pred rmap ag_rmap, @pred rmap ag_rmap) (approx (Init.Nat.min m n)) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx m) (approx n)) *)
    apply H; eauto.
  - apply bupd_mono.
    repeat (apply exp_left; intro).
(* Goal: @joins ghost ghost_join (ghost_fmap (approx (Init.Nat.min m n)) (approx (Init.Nat.min m n)) b) c *)
(* Goal: @eq (forall _ : @pred rmap ag_rmap, @pred rmap ag_rmap) (approx (Init.Nat.min m n)) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx m)) *)
(* Goal: @eq (forall _ : @pred rmap ag_rmap, @pred rmap ag_rmap) (approx (Init.Nat.min m n)) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx m) (approx n)) *)
    apply prop_andp_left; intro X; inv X; auto.
Qed.

Lemma Own_unit: emp |-- EX a : _, !!(identity a) && Own a.
Proof.
  intros w ?; simpl in *.
(* Goal: @ex ghost (fun b : ghost => and (@identity ghost ghost_join b) (and (forall b0 : AV.address, @identity resource Join_resource (resource_at w b0)) (@eq ghost (ghost_of w) (ghost_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) b)))) *)
  exists (ghost_of w); split; [|split].
  - apply ghost_of_identity; auto.
  - intro; apply resource_at_identity; auto.
  - rewrite ghost_of_approx; auto.
Qed.

Lemma Own_dealloc: forall a, Own a |-- bupd emp.
Proof.
  intros ? w [] ??.
  exists (core ((ghost_approx w) c)); split; [eexists; apply core_unit|].
  destruct (make_rmap (resource_at w) (core (ghost_approx w c)) (level w)) as (w' & ? & Hr & Hg).
(* Goal: @eq (forall _ : AV.address, resource) (@compose AV.address resource resource (resource_fmap (approx (@level rmap ag_rmap a)) (approx (@level rmap ag_rmap a))) (resource_at a)) (resource_at a) *)
(* Goal: @ex rmap (fun m' : rmap => and (@eq nat (@level rmap ag_rmap m') (@level rmap ag_rmap a)) (and (@eq (forall _ : AV.address, resource) (resource_at m') (resource_at a)) (and (@eq ghost (ghost_of m') (@nil (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)))) (@app_pred rmap ag_rmap (@emp rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap) m')))) *)
  { extensionality; apply resource_at_approx. }
(* Goal: @eq (forall _ : AV.address, resource) (@compose AV.address resource resource (resource_fmap (approx (@level rmap ag_rmap a)) (approx (@level rmap ag_rmap a))) (resource_at a)) (resource_at a) *)
(* Goal: @ex rmap (fun m' : rmap => and (@eq nat (@level rmap ag_rmap m') (@level rmap ag_rmap a)) (and (@eq (forall _ : AV.address, resource) (resource_at m') (resource_at a)) (and (@eq ghost (ghost_of m') (@nil (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)))) (@app_pred rmap ag_rmap (@emp rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap) m')))) *)
  { rewrite ghost_core; auto. }
(* Goal: @joins ghost ghost_join (ghost_fmap (approx (Init.Nat.min m n)) (approx (Init.Nat.min m n)) b) c *)
(* Goal: @eq (forall _ : @pred rmap ag_rmap, @pred rmap ag_rmap) (approx (Init.Nat.min m n)) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx m)) *)
(* Goal: @eq (forall _ : @pred rmap ag_rmap, @pred rmap ag_rmap) (approx (Init.Nat.min m n)) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx m) (approx n)) *)
  exists w'; repeat split; auto.
(* Goal: @app_pred rmap ag_rmap (@emp rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap) m' *)
  apply all_resource_at_identity.
  - rewrite Hr; auto.
  - rewrite Hg; apply core_identity.
Qed.

(* Goal: @eq (forall _ : AV.address, resource) (@compose AV.address resource resource (resource_fmap (approx (@level rmap ag_rmap a)) (approx (@level rmap ag_rmap a))) (resource_at a)) (resource_at a) *)
(* Goal: @ex rmap (fun m' : rmap => and (@eq nat (@level rmap ag_rmap m') (@level rmap ag_rmap a)) (and (@eq (forall _ : AV.address, resource) (resource_at m') (resource_at a)) (and (@eq ghost (ghost_of m') (@nil (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)))) (@app_pred rmap ag_rmap (@emp rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap) m')))) *)
Definition singleton {A} k (x : A) : list (option A) := repeat None k ++ Some x :: nil.

Definition gname := nat.

(* Goal: @eq (forall _ : AV.address, resource) (@compose AV.address resource resource (resource_fmap (approx (@level rmap ag_rmap a)) (approx (@level rmap ag_rmap a))) (resource_at a)) (resource_at a) *)
(* Goal: @ex rmap (fun m' : rmap => and (@eq nat (@level rmap ag_rmap m') (@level rmap ag_rmap a)) (and (@eq (forall _ : AV.address, resource) (resource_at m') (resource_at a)) (and (@eq ghost (ghost_of m') (@nil (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)))) (@app_pred rmap ag_rmap (@emp rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap) m')))) *)
Definition own {RA: Ghost} (n: gname) (a: G) (pp: preds) :=
  EX v : _, Own (singleton n (existT _ RA (exist _ a v), pp)).

(* Goal: @eq (forall _ : AV.address, resource) (@compose AV.address resource resource (resource_fmap (approx (@level rmap ag_rmap a)) (approx (@level rmap ag_rmap a))) (resource_at a)) (resource_at a) *)
(* Goal: @ex rmap (fun m' : rmap => and (@eq nat (@level rmap ag_rmap m') (@level rmap ag_rmap a)) (and (@eq (forall _ : AV.address, resource) (resource_at m') (resource_at a)) (and (@eq ghost (ghost_of m') (@nil (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)))) (@app_pred rmap ag_rmap (@emp rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap) m')))) *)
Definition list_set {A} (m : list (option A)) k v : list (option A) :=
  firstn k m ++ repeat None (k - length m) ++ Some v :: skipn (S k) m.

Lemma singleton_join_gen: forall k a c (m: ghost)
  (Hjoin: join (Some a) (nth k m None) (Some c)),
  join (singleton k a) m (list_set m k c).
Proof.
(* Goal: forall (RA : Ghost) (g : gname) (a : @G RA) (pp : preds), @derives rmap ag_rmap (@own RA g a pp) (@prop rmap ag_rmap (@valid RA a)) *)
  induction k; intros.
  - destruct m; simpl in *; subst; inv Hjoin; constructor; constructor; auto.
  - destruct m; simpl in *.
    + inv Hjoin; constructor.
    + constructor; [constructor | apply IHk; auto].
Qed.

Lemma map_repeat : forall {A B} (f : A -> B) x n, map f (repeat x n) = repeat (f x) n.
Proof.
(* Goal: forall (A B : Type) (f : forall _ : A, B) (x : A) (n : nat), @eq (list B) (@map A B f (@repeat A x n)) (@repeat B (f x) n) *)
  induction n; auto; simpl.
(* Goal: @joins ghost ghost_join (ghost_fmap (approx (Init.Nat.min m n)) (approx (Init.Nat.min m n)) b) c *)
(* Goal: @eq (forall _ : @pred rmap ag_rmap, @pred rmap ag_rmap) (approx (Init.Nat.min m n)) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx m)) *)
(* Goal: @eq (forall _ : @pred rmap ag_rmap, @pred rmap ag_rmap) (approx (Init.Nat.min m n)) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx m) (approx n)) *)
  rewrite IHn; auto.
Qed.

Lemma ghost_fmap_singleton: forall f g k v, ghost_fmap f g (singleton k v) =
  singleton k (match v with (a, b) => (a, preds_fmap f g b) end).
Proof.
(* Goal: forall (f g : forall _ : @pred rmap ag_rmap, @pred rmap ag_rmap) (k : nat) (v : prod (@sigT Ghost (fun g0 : Ghost => @sig (@G g0) (fun a : @G g0 => @valid g0 a))) preds), @eq ghost (ghost_fmap f g (@singleton (prod (@sigT Ghost (fun g0 : Ghost => @sig (@G g0) (fun a : @G g0 => @valid g0 a))) preds) k v)) (@singleton (prod (@sigT Ghost (fun g0 : Ghost => @sig (@G g0) (fun a : @G g0 => @valid g0 a))) preds) k (let (a, b) := v in @pair (@sigT Ghost (fun g0 : Ghost => @sig (@G g0) (fun a0 : @G g0 => @valid g0 a0))) preds a (preds_fmap f g b))) *)
  intros; unfold ghost_fmap, singleton.
(* Goal: @joins ghost ghost_join (ghost_fmap (approx (Init.Nat.min m n)) (approx (Init.Nat.min m n)) b) c *)
(* Goal: @eq (forall _ : @pred rmap ag_rmap, @pred rmap ag_rmap) (approx (Init.Nat.min m n)) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx m)) *)
(* Goal: @eq (forall _ : @pred rmap ag_rmap, @pred rmap ag_rmap) (approx (Init.Nat.min m n)) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx m) (approx n)) *)
  rewrite map_app, map_repeat; auto.
Qed.

Lemma ghost_fmap_singleton_inv : forall f g a k v,
  ghost_fmap f g a = singleton k v ->
  exists v', a = singleton k v' /\ v = let (a, b) := v' in (a, preds_fmap f g b).
Proof.
(* Goal: forall (RA : Ghost) (g : gname) (a : @G RA) (pp : preds), @derives rmap ag_rmap (@own RA g a pp) (@prop rmap ag_rmap (@valid RA a)) *)
  unfold singleton; induction a; simpl; intros.
  - destruct k; discriminate.
  - destruct a as [[]|]; simpl in *.
    + destruct k; inv H.
      destruct a0; inv H2.
(* Goal: @joins ghost ghost_join (ghost_fmap (approx (Init.Nat.min m n)) (approx (Init.Nat.min m n)) b) c *)
(* Goal: @eq (forall _ : @pred rmap ag_rmap, @pred rmap ag_rmap) (approx (Init.Nat.min m n)) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx m)) *)
(* Goal: @eq (forall _ : @pred rmap ag_rmap, @pred rmap ag_rmap) (approx (Init.Nat.min m n)) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx m) (approx n)) *)
      simpl; eauto.
    + destruct k; inv H.
(* Goal: @ex (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds) (fun v' : prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds => and (@eq ghost (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) (@None (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) a0) (@app (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) (@repeat (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) (@None (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) (S k)) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) (@Some (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds) v') (@nil (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)))))) (@eq (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds) v (let (a, b) := v' in @pair (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a0 : @G g => @valid g a0))) preds a (preds_fmap f g b)))) *)
      edestruct IHa as (? & ? & ?); eauto; subst.
(* Goal: @joins ghost ghost_join (ghost_fmap (approx (Init.Nat.min m n)) (approx (Init.Nat.min m n)) b) c *)
(* Goal: @eq (forall _ : @pred rmap ag_rmap, @pred rmap ag_rmap) (approx (Init.Nat.min m n)) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx m)) *)
(* Goal: @eq (forall _ : @pred rmap ag_rmap, @pred rmap ag_rmap) (approx (Init.Nat.min m n)) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx m) (approx n)) *)
      simpl; eauto.
Qed.

Lemma ghost_alloc: forall {RA: Ghost} a pp, ghost.valid a ->
  emp |-- bupd (EX g: gname, own g a pp).
Proof.
(* Goal: forall (RA : Ghost) (g : gname) (a : @G RA) (pp : preds), @derives rmap ag_rmap (@own RA g a pp) (@prop rmap ag_rmap (@valid RA a)) *)
  intros.
  eapply derives_trans; [apply Own_unit|].
  apply exp_left; intro g0.
  apply prop_andp_left; intro Hg0.
  eapply derives_trans.
  - apply Own_update_ND with (B := fun b => exists g, b = singleton g (existT _ RA (exist _ _ H), pp)).
    intros ? c [? J]; exists (singleton (length c) (existT _ RA (exist _ _ H), pp)).
(* Goal: @joins ghost ghost_join (ghost_fmap (approx (Init.Nat.min m n)) (approx (Init.Nat.min m n)) b) c *)
(* Goal: @eq (forall _ : @pred rmap ag_rmap, @pred rmap ag_rmap) (approx (Init.Nat.min m n)) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx m)) *)
(* Goal: @eq (forall _ : @pred rmap ag_rmap, @pred rmap ag_rmap) (approx (Init.Nat.min m n)) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx m) (approx n)) *)
    split; eauto.
    rewrite (identity_core Hg0), ghost_core in J; inv J; [|eexists; constructor].
    rewrite ghost_fmap_singleton; eexists; apply singleton_join_gen.
    rewrite nth_overflow by auto; constructor.
  - apply bupd_mono, exp_left; intro g'.
    apply prop_andp_left; intros [g]; subst.
    apply exp_right with g.
(* Goal: @joins ghost ghost_join (ghost_fmap (approx (Init.Nat.min m n)) (approx (Init.Nat.min m n)) b) c *)
(* Goal: @eq (forall _ : @pred rmap ag_rmap, @pred rmap ag_rmap) (approx (Init.Nat.min m n)) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx m)) *)
(* Goal: @eq (forall _ : @pred rmap ag_rmap, @pred rmap ag_rmap) (approx (Init.Nat.min m n)) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx m) (approx n)) *)
    eapply exp_right; eauto.
Qed.

Lemma singleton_join: forall a b c k,
  join (singleton k a) (singleton k b) (singleton k c) <-> join a b c.
Proof.
(* Goal: forall (a : prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds) (b c : prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a0 : @G g => @valid g a0))) preds) (k : nat), iff (@join (list (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a0 : @G g => @valid g a0))) preds))) ghost_join (@singleton (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a0 : @G g => @valid g a0))) preds) k a) (@singleton (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a0 : @G g => @valid g a0))) preds) k b) (@singleton (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a0 : @G g => @valid g a0))) preds) k c)) (@join (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a0 : @G g => @valid g a0))) preds) (Join_prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a0 : @G g => @valid g a0))) ghost_elem_join preds preds_join) a b c) *)
  unfold singleton; induction k; simpl.
  - split.
    + inversion 1; subst.
(* Goal: @joins ghost ghost_join (ghost_fmap (approx (Init.Nat.min m n)) (approx (Init.Nat.min m n)) b) c *)
(* Goal: @eq (forall _ : @pred rmap ag_rmap, @pred rmap ag_rmap) (approx (Init.Nat.min m n)) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx m)) *)
(* Goal: @eq (forall _ : @pred rmap ag_rmap, @pred rmap ag_rmap) (approx (Init.Nat.min m n)) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx m) (approx n)) *)
      inv H3; auto.
    + intro; do 2 constructor; auto.
  - rewrite <- IHk.
(* Goal: @joins ghost ghost_join (ghost_fmap (approx (Init.Nat.min m n)) (approx (Init.Nat.min m n)) b) c *)
(* Goal: @eq (forall _ : @pred rmap ag_rmap, @pred rmap ag_rmap) (approx (Init.Nat.min m n)) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx m)) *)
(* Goal: @eq (forall _ : @pred rmap ag_rmap, @pred rmap ag_rmap) (approx (Init.Nat.min m n)) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx m) (approx n)) *)
    split; [inversion 1 | repeat constructor]; auto.
Qed.

Lemma singleton_join_inv: forall k a b c,
  join (singleton k a) (singleton k b) c -> exists c', join a b c' /\ c = singleton k c'.
Proof.
(* Goal: forall _ : @join (list (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds))) ghost_join (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) (@Some (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds) a) (@nil (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)))) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) (@Some (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds) b) (@nil (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)))) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) (@Some (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds) c) (@nil (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)))), @join (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds) (Join_prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) ghost_elem_join preds preds_join) a b c *)
  unfold singleton; induction k; inversion 1; subst.
  - assert (m3 = nil) by (inv H6; auto).
(* Goal: @joins ghost ghost_join (ghost_fmap (approx (Init.Nat.min m n)) (approx (Init.Nat.min m n)) b) c *)
(* Goal: @eq (forall _ : @pred rmap ag_rmap, @pred rmap ag_rmap) (approx (Init.Nat.min m n)) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx m)) *)
(* Goal: @eq (forall _ : @pred rmap ag_rmap, @pred rmap ag_rmap) (approx (Init.Nat.min m n)) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx m) (approx n)) *)
    inv H5; eauto.
  - assert (a3 = None) by (inv H5; auto); subst.
(* Goal: @joins ghost ghost_join (ghost_fmap (approx (Init.Nat.min m n)) (approx (Init.Nat.min m n)) b) c *)
(* Goal: @eq (forall _ : @pred rmap ag_rmap, @pred rmap ag_rmap) (approx (Init.Nat.min m n)) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx m)) *)
(* Goal: @eq (forall _ : @pred rmap ag_rmap, @pred rmap ag_rmap) (approx (Init.Nat.min m n)) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx m) (approx n)) *)
    edestruct IHk as (? & ? & ?); eauto; subst; eauto.
Qed.

(* Goal: @eq (forall _ : AV.address, resource) (@compose AV.address resource resource (resource_fmap (approx (@level rmap ag_rmap a)) (approx (@level rmap ag_rmap a))) (resource_at a)) (resource_at a) *)
(* Goal: @ex rmap (fun m' : rmap => and (@eq nat (@level rmap ag_rmap m') (@level rmap ag_rmap a)) (and (@eq (forall _ : AV.address, resource) (resource_at m') (resource_at a)) (and (@eq ghost (ghost_of m') (@nil (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)))) (@app_pred rmap ag_rmap (@emp rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap) m')))) *)
Lemma ghost_valid_2: forall {RA: Ghost} g a1 a2 pp,
  own g a1 pp * own g a2 pp |-- !!ghost.valid_2 a1 a2.
Proof.
(* Goal: forall (RA : Ghost) (g : gname) (a : @G RA) (pp : preds), @derives rmap ag_rmap (@own RA g a pp) (@prop rmap ag_rmap (@valid RA a)) *)
  intros.
(* Goal: @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (@own RA g a1 pp) (@own RA g a2 pp)) (@prop rmap ag_rmap (@valid_2 RA a1 a2)) *)
  intros w (? & ? & J%ghost_of_join & (? & ? & Hg1) & (? & ? & Hg2)).
(* Goal: @app_pred rmap ag_rmap (@prop rmap ag_rmap (@valid_2 RA a1 a2)) w *)
  rewrite Hg1, Hg2, !ghost_fmap_singleton in J.
(* Goal: @app_pred rmap ag_rmap (@prop rmap ag_rmap (@valid_2 RA a1 a2)) w *)
  apply singleton_join_inv in J as ([] & J & ?).
  inv J; simpl in *.
(* Goal: @valid_2 RA a1 a2 *)
  inv H2; repeat inj_pair_tac.
(* Goal: @valid_2 RA a1 a2 *)
  eexists; eauto.
Qed.

Lemma ghost_op: forall {RA: Ghost} g (a1 a2 a3: G) pp, join a1 a2 a3 ->
  own g a3 pp = own g a1 pp * own g a2 pp.
Proof.
  intros; apply pred_ext.
  - apply exp_left; intro.
    erewrite Own_op; [apply sepcon_derives; eapply exp_right; eauto|].
(* Goal: @joins ghost ghost_join (ghost_fmap (approx (Init.Nat.min m n)) (approx (Init.Nat.min m n)) b) c *)
(* Goal: @eq (forall _ : @pred rmap ag_rmap, @pred rmap ag_rmap) (approx (Init.Nat.min m n)) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx m)) *)
(* Goal: @eq (forall _ : @pred rmap ag_rmap, @pred rmap ag_rmap) (approx (Init.Nat.min m n)) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx m) (approx n)) *)
    apply singleton_join; constructor; constructor; auto.
  - eapply derives_trans; [apply andp_right, derives_refl; apply ghost_valid_2|].
    apply prop_andp_left; intros (? & J & ?).
    eapply join_eq in H; eauto; subst.
    unfold own; rewrite exp_sepcon1; apply exp_left; intro.
    rewrite exp_sepcon2; apply exp_left; intro.
    erewrite <- Own_op; [eapply exp_right; eauto|].
(* Goal: @joins ghost ghost_join (ghost_fmap (approx (Init.Nat.min m n)) (approx (Init.Nat.min m n)) b) c *)
(* Goal: @eq (forall _ : @pred rmap ag_rmap, @pred rmap ag_rmap) (approx (Init.Nat.min m n)) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx m)) *)
(* Goal: @eq (forall _ : @pred rmap ag_rmap, @pred rmap ag_rmap) (approx (Init.Nat.min m n)) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx m) (approx n)) *)
    apply singleton_join; constructor; constructor; auto.
  Unshelve.
(* Goal: @joins ghost ghost_join (ghost_fmap (approx (Init.Nat.min m n)) (approx (Init.Nat.min m n)) b) c *)
(* Goal: @eq (forall _ : @pred rmap ag_rmap, @pred rmap ag_rmap) (approx (Init.Nat.min m n)) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx m)) *)
(* Goal: @eq (forall _ : @pred rmap ag_rmap, @pred rmap ag_rmap) (approx (Init.Nat.min m n)) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx m) (approx n)) *)
  eapply join_valid; eauto.
(* Goal: @joins ghost ghost_join (ghost_fmap (approx (Init.Nat.min m n)) (approx (Init.Nat.min m n)) b) c *)
(* Goal: @eq (forall _ : @pred rmap ag_rmap, @pred rmap ag_rmap) (approx (Init.Nat.min m n)) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx m)) *)
(* Goal: @eq (forall _ : @pred rmap ag_rmap, @pred rmap ag_rmap) (approx (Init.Nat.min m n)) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx m) (approx n)) *)
  eapply join_valid; eauto.
(* Goal: @joins ghost ghost_join (ghost_fmap (approx (Init.Nat.min m n)) (approx (Init.Nat.min m n)) b) c *)
(* Goal: @eq (forall _ : @pred rmap ag_rmap, @pred rmap ag_rmap) (approx (Init.Nat.min m n)) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx m)) *)
(* Goal: @eq (forall _ : @pred rmap ag_rmap, @pred rmap ag_rmap) (approx (Init.Nat.min m n)) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx m) (approx n)) *)
  auto.
Qed.

(* Goal: @eq (forall _ : AV.address, resource) (@compose AV.address resource resource (resource_fmap (approx (@level rmap ag_rmap a)) (approx (@level rmap ag_rmap a))) (resource_at a)) (resource_at a) *)
(* Goal: @ex rmap (fun m' : rmap => and (@eq nat (@level rmap ag_rmap m') (@level rmap ag_rmap a)) (and (@eq (forall _ : AV.address, resource) (resource_at m') (resource_at a)) (and (@eq ghost (ghost_of m') (@nil (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)))) (@app_pred rmap ag_rmap (@emp rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap) m')))) *)
Lemma ghost_valid: forall {RA: Ghost} g a pp,
  own g a pp |-- !!ghost.valid a.
Proof.
(* Goal: forall (RA : Ghost) (g : gname) (a : @G RA) (pp : preds), @derives rmap ag_rmap (@own RA g a pp) (@prop rmap ag_rmap (@valid RA a)) *)
  intros.
  rewrite <- (normalize.andp_TT (!!_)).
(* Goal: @derives rmap ag_rmap (@own RA g a pp) (@andp rmap ag_rmap (@prop rmap ag_rmap (@valid RA a)) (@TT rmap ag_rmap)) *)
  erewrite ghost_op by apply core_unit.
(* Goal: @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (@own RA g (@core (@G RA) (let (G, valid, Join_G, _, _, _) as Ghost return (Join (@G Ghost)) := RA in Join_G) (@Sep_G RA) a) pp) (@own RA g a pp)) (@andp rmap ag_rmap (@prop rmap ag_rmap (@valid RA a)) (@TT rmap ag_rmap)) *)
  eapply derives_trans; [apply andp_right, derives_refl; apply ghost_valid_2|].
(* Goal: @joins ghost ghost_join (ghost_fmap (approx (Init.Nat.min m n)) (approx (Init.Nat.min m n)) b) c *)
(* Goal: @eq (forall _ : @pred rmap ag_rmap, @pred rmap ag_rmap) (approx (Init.Nat.min m n)) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx m)) *)
(* Goal: @eq (forall _ : @pred rmap ag_rmap, @pred rmap ag_rmap) (approx (Init.Nat.min m n)) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx m) (approx n)) *)
  apply prop_andp_left; intros (? & J & ?); apply prop_andp_right; auto.
(* Goal: @joins ghost ghost_join (ghost_fmap (approx (Init.Nat.min m n)) (approx (Init.Nat.min m n)) b) c *)
(* Goal: @eq (forall _ : @pred rmap ag_rmap, @pred rmap ag_rmap) (approx (Init.Nat.min m n)) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx m)) *)
(* Goal: @eq (forall _ : @pred rmap ag_rmap, @pred rmap ag_rmap) (approx (Init.Nat.min m n)) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx m) (approx n)) *)
  apply core_identity in J; subst; auto.
Qed.

Lemma singleton_join_inv_gen: forall k a (b c: ghost),
  join (singleton k a) b c ->
  join (Some a) (nth k b None) (nth k c None) /\
    exists c', nth k c None = Some c' /\ c = list_set b k c'.
Proof.
(* Goal: @joins ghost ghost_join (ghost_fmap (approx (Init.Nat.min m n)) (approx (Init.Nat.min m n)) b) c *)
(* Goal: @eq (forall _ : @pred rmap ag_rmap, @pred rmap ag_rmap) (approx (Init.Nat.min m n)) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx m)) *)
(* Goal: @eq (forall _ : @pred rmap ag_rmap, @pred rmap ag_rmap) (approx (Init.Nat.min m n)) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx m) (approx n)) *)
  unfold singleton; induction k; inversion 1; subst; auto.
  - split; simpl; eauto; constructor.
  - split; auto.
(* Goal: @ex (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds) (fun c' : prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds => and (@eq (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) (@nth (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) O (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) a3 m3) (@None (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds))) (@Some (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds) c')) (@eq ghost (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) a3 m3) (@list_set (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) a2 m2) O c'))) *)
    unfold list_set; simpl.
    rewrite <- (ghost_core m2) in H5.
(* Goal: @ex (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds) (fun c' : prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds => and (@eq (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) a3 (@Some (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds) c')) (@eq ghost (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) a3 m3) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) (@Some (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds) c') m2))) *)
    apply (core_identity m2) in H5; subst.
(* Goal: @joins ghost ghost_join (ghost_fmap (approx (Init.Nat.min m n)) (approx (Init.Nat.min m n)) b) c *)
(* Goal: @eq (forall _ : @pred rmap ag_rmap, @pred rmap ag_rmap) (approx (Init.Nat.min m n)) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx m)) *)
(* Goal: @eq (forall _ : @pred rmap ag_rmap, @pred rmap ag_rmap) (approx (Init.Nat.min m n)) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx m) (approx n)) *)
    inv H2; eauto.
  - rewrite app_nth2; rewrite repeat_length; auto.
(* Goal: and (@join (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) (@Join_lower (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds) (Join_prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) ghost_elem_join preds preds_join)) (@Some (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds) a) (@nth (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) (S k) (@nil (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds))) (@None (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds))) (@nth (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) (Init.Nat.sub (S k) (S k)) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) (@Some (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds) a) (@nil (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)))) (@None (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)))) (@ex (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds) (fun c' : prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds => and (@eq (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) (@nth (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) (Init.Nat.sub (S k) (S k)) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) (@Some (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds) a) (@nil (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)))) (@None (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds))) (@Some (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds) c')) (@eq ghost (@app (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) (@repeat (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) (@None (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) (S k)) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) (@Some (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds) a) (@nil (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds))))) (@list_set (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds) (@nil (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds))) (S k) c')))) *)
    rewrite minus_diag; split; [constructor | simpl; eauto].
  - assert (a2 = a3) by (inv H2; auto).
(* Goal: @joins ghost ghost_join (ghost_fmap (approx (Init.Nat.min m n)) (approx (Init.Nat.min m n)) b) c *)
(* Goal: @eq (forall _ : @pred rmap ag_rmap, @pred rmap ag_rmap) (approx (Init.Nat.min m n)) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx m)) *)
(* Goal: @eq (forall _ : @pred rmap ag_rmap, @pred rmap ag_rmap) (approx (Init.Nat.min m n)) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx m) (approx n)) *)
    destruct (IHk _ _ _ H5) as (? & ? & ? & ?); subst; eauto.
Qed.

(* Goal: @eq (forall _ : AV.address, resource) (@compose AV.address resource resource (resource_fmap (approx (@level rmap ag_rmap a)) (approx (@level rmap ag_rmap a))) (resource_at a)) (resource_at a) *)
(* Goal: @ex rmap (fun m' : rmap => and (@eq nat (@level rmap ag_rmap m') (@level rmap ag_rmap a)) (and (@eq (forall _ : AV.address, resource) (resource_at m') (resource_at a)) (and (@eq ghost (ghost_of m') (@nil (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)))) (@app_pred rmap ag_rmap (@emp rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap) m')))) *)
Lemma ghost_update_ND: forall {RA: Ghost} g (a: G) B pp,
  fp_update_ND a B -> own g a pp |-- bupd (EX b : _, !!(B b) && own g b pp).
Proof.
(* Goal: forall (RA : Ghost) (g : gname) (a : @G RA) (pp : preds), @derives rmap ag_rmap (@own RA g a pp) (@prop rmap ag_rmap (@valid RA a)) *)
  intros.
  apply exp_left; intro Hva.
  eapply derives_trans.
  - apply Own_update_ND with
      (B := fun b => exists b' Hvb, B b' /\ b = singleton g (existT _ RA (exist _ b' Hvb), pp)).
    intros ?? [? J].
    rewrite ghost_fmap_singleton in J.
    destruct (singleton_join_inv_gen _ _ _ _ J) as [Jg _].
    inv Jg.
    + destruct (H (core a)) as (b & ? & Hv).
(* Goal: @eq (forall _ : AV.address, resource) (@compose AV.address resource resource (resource_fmap (approx (@level rmap ag_rmap a)) (approx (@level rmap ag_rmap a))) (resource_at a)) (resource_at a) *)
(* Goal: @ex rmap (fun m' : rmap => and (@eq nat (@level rmap ag_rmap m') (@level rmap ag_rmap a)) (and (@eq (forall _ : AV.address, resource) (resource_at m') (resource_at a)) (and (@eq ghost (ghost_of m') (@nil (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)))) (@app_pred rmap ag_rmap (@emp rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap) m')))) *)
      { eexists; split; [apply join_comm, core_unit | auto]. }
      assert (ghost.valid b) as Hvb.
(* Goal: @eq (forall _ : AV.address, resource) (@compose AV.address resource resource (resource_fmap (approx (@level rmap ag_rmap a)) (approx (@level rmap ag_rmap a))) (resource_at a)) (resource_at a) *)
(* Goal: @ex rmap (fun m' : rmap => and (@eq nat (@level rmap ag_rmap m') (@level rmap ag_rmap a)) (and (@eq (forall _ : AV.address, resource) (resource_at m') (resource_at a)) (and (@eq ghost (ghost_of m') (@nil (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)))) (@app_pred rmap ag_rmap (@emp rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap) m')))) *)
      { destruct Hv as (? & ? & ?); eapply join_valid; eauto. }
(* Goal: @joins ghost ghost_join (ghost_fmap (approx (Init.Nat.min m n)) (approx (Init.Nat.min m n)) b) c *)
(* Goal: @eq (forall _ : @pred rmap ag_rmap, @pred rmap ag_rmap) (approx (Init.Nat.min m n)) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx m)) *)
(* Goal: @eq (forall _ : @pred rmap ag_rmap, @pred rmap ag_rmap) (approx (Init.Nat.min m n)) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx m) (approx n)) *)
      exists (singleton g (existT _ RA (exist _ _ Hvb), pp)); split; eauto.
      rewrite ghost_fmap_singleton.
      eexists; apply singleton_join_gen.
      rewrite <- H2; constructor.
    + destruct a2, a3; inv H3; simpl in *.
      inv H0; inj_pair_tac.
      destruct (H b0) as (b & ? & Hv).
(* Goal: @eq (forall _ : AV.address, resource) (@compose AV.address resource resource (resource_fmap (approx (@level rmap ag_rmap a)) (approx (@level rmap ag_rmap a))) (resource_at a)) (resource_at a) *)
(* Goal: @ex rmap (fun m' : rmap => and (@eq nat (@level rmap ag_rmap m') (@level rmap ag_rmap a)) (and (@eq (forall _ : AV.address, resource) (resource_at m') (resource_at a)) (and (@eq ghost (ghost_of m') (@nil (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)))) (@app_pred rmap ag_rmap (@emp rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap) m')))) *)
      { eexists; eauto. }
      destruct Hv as (? & ? & ?).
      assert (ghost.valid b) as Hvb by (eapply join_valid; eauto).
(* Goal: @joins ghost ghost_join (ghost_fmap (approx (Init.Nat.min m n)) (approx (Init.Nat.min m n)) b) c *)
(* Goal: @eq (forall _ : @pred rmap ag_rmap, @pred rmap ag_rmap) (approx (Init.Nat.min m n)) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx m)) *)
(* Goal: @eq (forall _ : @pred rmap ag_rmap, @pred rmap ag_rmap) (approx (Init.Nat.min m n)) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx m) (approx n)) *)
      exists (singleton g (existT _ RA (exist _ _ Hvb), pp)); split; eauto.
      rewrite ghost_fmap_singleton.
      eexists; apply singleton_join_gen.
      instantiate (1 := (_, _)).
      rewrite <- H1; constructor; constructor; [constructor|]; eauto.
  - apply bupd_mono, exp_left; intro.
    apply prop_andp_left; intros (b & ? & ? & ?); subst.
(* Goal: @joins ghost ghost_join (ghost_fmap (approx (Init.Nat.min m n)) (approx (Init.Nat.min m n)) b) c *)
(* Goal: @eq (forall _ : @pred rmap ag_rmap, @pred rmap ag_rmap) (approx (Init.Nat.min m n)) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx m)) *)
(* Goal: @eq (forall _ : @pred rmap ag_rmap, @pred rmap ag_rmap) (approx (Init.Nat.min m n)) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx m) (approx n)) *)
    apply exp_right with b, prop_andp_right; auto.
(* Goal: @joins ghost ghost_join (ghost_fmap (approx (Init.Nat.min m n)) (approx (Init.Nat.min m n)) b) c *)
(* Goal: @eq (forall _ : @pred rmap ag_rmap, @pred rmap ag_rmap) (approx (Init.Nat.min m n)) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx m)) *)
(* Goal: @eq (forall _ : @pred rmap ag_rmap, @pred rmap ag_rmap) (approx (Init.Nat.min m n)) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx m) (approx n)) *)
    eapply exp_right; auto.
  Unshelve.
(* Goal: @joins ghost ghost_join (ghost_fmap (approx (Init.Nat.min m n)) (approx (Init.Nat.min m n)) b) c *)
(* Goal: @eq (forall _ : @pred rmap ag_rmap, @pred rmap ag_rmap) (approx (Init.Nat.min m n)) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx m)) *)
(* Goal: @eq (forall _ : @pred rmap ag_rmap, @pred rmap ag_rmap) (approx (Init.Nat.min m n)) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx m) (approx n)) *)
  auto.
Qed.

(* Goal: @eq (forall _ : AV.address, resource) (@compose AV.address resource resource (resource_fmap (approx (@level rmap ag_rmap a)) (approx (@level rmap ag_rmap a))) (resource_at a)) (resource_at a) *)
(* Goal: @ex rmap (fun m' : rmap => and (@eq nat (@level rmap ag_rmap m') (@level rmap ag_rmap a)) (and (@eq (forall _ : AV.address, resource) (resource_at m') (resource_at a)) (and (@eq ghost (ghost_of m') (@nil (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)))) (@app_pred rmap ag_rmap (@emp rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap) m')))) *)
Lemma ghost_update: forall {RA: Ghost} g (a b: G) pp,
  fp_update a b -> own g a pp |-- bupd (own g b pp).
Proof.
  intros; eapply derives_trans.
  - apply (ghost_update_ND g a (eq b)).
    intros ? J; destruct (H _ J).
    do 2 eexists; [constructor | eauto].
  - apply bupd_mono.
(* Goal: @joins ghost ghost_join (ghost_fmap (approx (Init.Nat.min m n)) (approx (Init.Nat.min m n)) b) c *)
(* Goal: @eq (forall _ : @pred rmap ag_rmap, @pred rmap ag_rmap) (approx (Init.Nat.min m n)) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx m)) *)
(* Goal: @eq (forall _ : @pred rmap ag_rmap, @pred rmap ag_rmap) (approx (Init.Nat.min m n)) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx m) (approx n)) *)
    apply exp_left; intro; apply prop_andp_left; intro X; inv X; auto.
Qed.

(* Goal: @eq (forall _ : AV.address, resource) (@compose AV.address resource resource (resource_fmap (approx (@level rmap ag_rmap a)) (approx (@level rmap ag_rmap a))) (resource_at a)) (resource_at a) *)
(* Goal: @ex rmap (fun m' : rmap => and (@eq nat (@level rmap ag_rmap m') (@level rmap ag_rmap a)) (and (@eq (forall _ : AV.address, resource) (resource_at m') (resource_at a)) (and (@eq ghost (ghost_of m') (@nil (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)))) (@app_pred rmap ag_rmap (@emp rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap) m')))) *)
Lemma ghost_dealloc: forall {RA: Ghost} g a pp,
  own g a pp |-- bupd emp.
Proof.
(* Goal: forall (RA : Ghost) (n : nat) (g : gname) (a : @G RA) (pp : preds), @eq (@pred rmap ag_rmap) (approx n (@own RA g a pp)) (approx n (@own RA g a (preds_fmap (approx n) (approx n) pp))) *)
  intros; unfold own.
(* Goal: @derives rmap ag_rmap (@exp rmap ag_rmap (@valid RA a) (fun v : @valid RA a => Own (@singleton (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds) g (@pair (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds (@existT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a)) RA (@exist (@G RA) (fun a : @G RA => @valid RA a) a v)) pp)))) (bupd (@emp rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap)) *)
  apply exp_left; intro; apply Own_dealloc.
Qed.

Lemma list_set_same : forall {A} n l (a : A), nth n l None = Some a ->
  list_set l n a = l.
Proof.
(* Goal: @joins ghost ghost_join (ghost_fmap (approx (Init.Nat.min m n)) (approx (Init.Nat.min m n)) b) c *)
(* Goal: @eq (forall _ : @pred rmap ag_rmap, @pred rmap ag_rmap) (approx (Init.Nat.min m n)) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx m)) *)
(* Goal: @eq (forall _ : @pred rmap ag_rmap, @pred rmap ag_rmap) (approx (Init.Nat.min m n)) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx m) (approx n)) *)
  unfold list_set; induction n; destruct l; simpl; try discriminate; intros; subst; auto.
(* Goal: @joins ghost ghost_join (ghost_fmap (approx (Init.Nat.min m n)) (approx (Init.Nat.min m n)) b) c *)
(* Goal: @eq (forall _ : @pred rmap ag_rmap, @pred rmap ag_rmap) (approx (Init.Nat.min m n)) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx m)) *)
(* Goal: @eq (forall _ : @pred rmap ag_rmap, @pred rmap ag_rmap) (approx (Init.Nat.min m n)) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx m) (approx n)) *)
  f_equal; eauto.
Qed.

(* The addition of ghost state means that there are rmaps that have only
   cores for ghost state, but are not cores themselves (since they have ghost
   state at all). An rmap of this sort is not emp, but is its own unit. *)

Definition cored: pred rmap := ALL P : pred rmap, ALL Q : pred rmap,
  P && Q --> P * Q.

Program Definition is_w w: pred rmap := fun w' => necR w w'.
Next Obligation.
Proof.
(* Goal: forall w : rmap, (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun w' : rmap => @necR rmap ag_rmap w w') *)
  repeat intro.
(* Goal: @joins ghost ghost_join (ghost_fmap (approx (Init.Nat.min m n)) (approx (Init.Nat.min m n)) b) c *)
(* Goal: @eq (forall _ : @pred rmap ag_rmap, @pred rmap ag_rmap) (approx (Init.Nat.min m n)) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx m)) *)
(* Goal: @eq (forall _ : @pred rmap ag_rmap, @pred rmap ag_rmap) (approx (Init.Nat.min m n)) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx m) (approx n)) *)
  eapply necR_trans; eauto.
(* Goal: @joins ghost ghost_join (ghost_fmap (approx (Init.Nat.min m n)) (approx (Init.Nat.min m n)) b) c *)
(* Goal: @eq (forall _ : @pred rmap ag_rmap, @pred rmap ag_rmap) (approx (Init.Nat.min m n)) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx m)) *)
(* Goal: @eq (forall _ : @pred rmap ag_rmap, @pred rmap ag_rmap) (approx (Init.Nat.min m n)) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx m) (approx n)) *)
  constructor; auto.
Qed.

Lemma cored_unit: forall w, cored w = join w w w.
Proof.
  intro; apply prop_ext; split; unfold cored; intro.
  - edestruct (H (is_w w) (is_w w)) as (? & ? & J & Hw1 & Hw2).
(* Goal: @eq (forall _ : AV.address, resource) (@compose AV.address resource resource (resource_fmap (approx (@level rmap ag_rmap a)) (approx (@level rmap ag_rmap a))) (resource_at a)) (resource_at a) *)
(* Goal: @ex rmap (fun m' : rmap => and (@eq nat (@level rmap ag_rmap m') (@level rmap ag_rmap a)) (and (@eq (forall _ : AV.address, resource) (resource_at m') (resource_at a)) (and (@eq ghost (ghost_of m') (@nil (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)))) (@app_pred rmap ag_rmap (@emp rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap) m')))) *)
    { apply necR_refl. }
(* Goal: @eq (forall _ : AV.address, resource) (@compose AV.address resource resource (resource_fmap (approx (@level rmap ag_rmap a)) (approx (@level rmap ag_rmap a))) (resource_at a)) (resource_at a) *)
(* Goal: @ex rmap (fun m' : rmap => and (@eq nat (@level rmap ag_rmap m') (@level rmap ag_rmap a)) (and (@eq (forall _ : AV.address, resource) (resource_at m') (resource_at a)) (and (@eq ghost (ghost_of m') (@nil (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)))) (@app_pred rmap ag_rmap (@emp rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap) m')))) *)
    { split; apply necR_refl. }
    simpl in *.
    destruct (join_level _ _ _ J).
(* Goal: @joins ghost ghost_join (ghost_fmap (approx (Init.Nat.min m n)) (approx (Init.Nat.min m n)) b) c *)
(* Goal: @eq (forall _ : @pred rmap ag_rmap, @pred rmap ag_rmap) (approx (Init.Nat.min m n)) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx m)) *)
(* Goal: @eq (forall _ : @pred rmap ag_rmap, @pred rmap ag_rmap) (approx (Init.Nat.min m n)) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx m) (approx n)) *)
    eapply necR_linear' in Hw1; try apply necR_refl; auto.
(* Goal: @joins ghost ghost_join (ghost_fmap (approx (Init.Nat.min m n)) (approx (Init.Nat.min m n)) b) c *)
(* Goal: @eq (forall _ : @pred rmap ag_rmap, @pred rmap ag_rmap) (approx (Init.Nat.min m n)) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx m)) *)
(* Goal: @eq (forall _ : @pred rmap ag_rmap, @pred rmap ag_rmap) (approx (Init.Nat.min m n)) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx m) (approx n)) *)
    eapply necR_linear' in Hw2; try apply necR_refl; auto.
(* Goal: @joins ghost ghost_join (ghost_fmap (approx (Init.Nat.min m n)) (approx (Init.Nat.min m n)) b) c *)
(* Goal: @eq (forall _ : @pred rmap ag_rmap, @pred rmap ag_rmap) (approx (Init.Nat.min m n)) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx m)) *)
(* Goal: @eq (forall _ : @pred rmap ag_rmap, @pred rmap ag_rmap) (approx (Init.Nat.min m n)) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx m) (approx n)) *)
    subst; auto.
  - intros P Q ?? [HP HQ].
(* Goal: @joins ghost ghost_join (ghost_fmap (approx (Init.Nat.min m n)) (approx (Init.Nat.min m n)) b) c *)
(* Goal: @eq (forall _ : @pred rmap ag_rmap, @pred rmap ag_rmap) (approx (Init.Nat.min m n)) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx m)) *)
(* Goal: @eq (forall _ : @pred rmap ag_rmap, @pred rmap ag_rmap) (approx (Init.Nat.min m n)) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx m) (approx n)) *)
    exists a', a'; repeat split; auto.
(* Goal: @joins ghost ghost_join (ghost_fmap (approx (Init.Nat.min m n)) (approx (Init.Nat.min m n)) b) c *)
(* Goal: @eq (forall _ : @pred rmap ag_rmap, @pred rmap ag_rmap) (approx (Init.Nat.min m n)) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx m)) *)
(* Goal: @eq (forall _ : @pred rmap ag_rmap, @pred rmap ag_rmap) (approx (Init.Nat.min m n)) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx m) (approx n)) *)
    eapply nec_join in H as (? & ? & ? & Hw1 & Hw2); eauto.
    destruct (join_level _ _ _ H).
    eapply necR_linear' in Hw1; try apply H0; [|omega].
    eapply necR_linear' in Hw2; try apply H0; [|omega].
(* Goal: @joins ghost ghost_join (ghost_fmap (approx (Init.Nat.min m n)) (approx (Init.Nat.min m n)) b) c *)
(* Goal: @eq (forall _ : @pred rmap ag_rmap, @pred rmap ag_rmap) (approx (Init.Nat.min m n)) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx m)) *)
(* Goal: @eq (forall _ : @pred rmap ag_rmap, @pred rmap ag_rmap) (approx (Init.Nat.min m n)) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx m) (approx n)) *)
    subst; auto.
Qed.

Lemma cored_dup: forall P, P && cored |-- (P && cored) * (P && cored).
Proof.
(* Goal: forall (RA : Ghost) (g : gname) (a : @G RA) (pp : preds), @derives rmap ag_rmap (@own RA g a pp) (@prop rmap ag_rmap (@valid RA a)) *)
  intros.
  rewrite <- (andp_dup cored) at 1.
  rewrite <- andp_assoc.
  intros; unfold cored at 2.
  eapply modus_ponens.
  + apply andp_left1, derives_refl.
  + eapply andp_left2, allp_left, allp_left.
    rewrite andp_dup; apply derives_refl.
Qed.

Lemma cored_core: forall w, cored (core w).
Proof.
(* Goal: forall w : rmap, @app_pred rmap ag_rmap cored (@core rmap Join_rmap Sep_rmap w) *)
  intro; rewrite cored_unit.
(* Goal: @join rmap Join_rmap (@core rmap Join_rmap Sep_rmap w) (@core rmap Join_rmap Sep_rmap w) (@core rmap Join_rmap Sep_rmap w) *)
  apply identity_unit', core_identity.
Qed.

Lemma cored_duplicable: cored = cored * cored.
Proof.
(* Goal: @eq (@pred rmap ag_rmap) cored (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap cored cored) *)
  apply pred_ext.
  - rewrite <- andp_dup at 1.
(* Goal: @derives rmap ag_rmap (@andp rmap ag_rmap cored cored) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap cored cored) *)
    eapply derives_trans; [apply cored_dup|].
(* Goal: @joins ghost ghost_join (ghost_fmap (approx (Init.Nat.min m n)) (approx (Init.Nat.min m n)) b) c *)
(* Goal: @eq (forall _ : @pred rmap ag_rmap, @pred rmap ag_rmap) (approx (Init.Nat.min m n)) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx m)) *)
(* Goal: @eq (forall _ : @pred rmap ag_rmap, @pred rmap ag_rmap) (approx (Init.Nat.min m n)) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx m) (approx n)) *)
    apply sepcon_derives; apply andp_left1; auto.
  - intros ? (? & ? & J & J1 & J2).
    rewrite cored_unit in *.
(* Goal: @join rmap Join_rmap a a a *)
    destruct (join_assoc J1 J) as (? & J' & J1').
(* Goal: @join rmap Join_rmap a a a *)
    eapply join_eq in J'; [|apply J]; subst.
(* Goal: @join rmap Join_rmap x1 x1 x1 *)
    destruct (join_assoc J2 (join_comm J)) as (? & J' & J2').
(* Goal: @join rmap Join_rmap x1 x1 x1 *)
    eapply join_eq in J'; [|apply join_comm, J]; subst.
(* Goal: @join rmap Join_rmap x2 x2 x2 *)
    destruct (join_assoc (join_comm J1') (join_comm J2')) as (? & J' & ?).
(* Goal: @joins ghost ghost_join (ghost_fmap (approx (Init.Nat.min m n)) (approx (Init.Nat.min m n)) b) c *)
(* Goal: @eq (forall _ : @pred rmap ag_rmap, @pred rmap ag_rmap) (approx (Init.Nat.min m n)) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx m)) *)
(* Goal: @eq (forall _ : @pred rmap ag_rmap, @pred rmap ag_rmap) (approx (Init.Nat.min m n)) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx m) (approx n)) *)
    eapply join_eq in J'; [|apply J]; subst; auto.
Qed.

Lemma cored_emp: cored |-- bupd emp.
Proof.
(* Goal: @derives rmap ag_rmap cored (bupd (@emp rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap)) *)
  intro; rewrite cored_unit; intros J ??.
(* Goal: @ex ghost (fun b : ghost => and (@joins ghost ghost_join b (ghost_fmap (approx (@level rmap ag_rmap a)) (approx (@level rmap ag_rmap a)) c)) (@ex rmap (fun m' : rmap => and (@eq nat (@level rmap ag_rmap m') (@level rmap ag_rmap a)) (and (@eq (forall _ : AV.address, resource) (resource_at m') (resource_at a)) (and (@eq ghost (ghost_of m') b) (@app_pred rmap ag_rmap (@emp rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap) m')))))) *)
  exists nil; split; [eexists; constructor|].
(* Goal: @joins ghost ghost_join (ghost_fmap (approx (Init.Nat.min m n)) (approx (Init.Nat.min m n)) b) c *)
(* Goal: @eq (forall _ : @pred rmap ag_rmap, @pred rmap ag_rmap) (approx (Init.Nat.min m n)) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx m)) *)
(* Goal: @eq (forall _ : @pred rmap ag_rmap, @pred rmap ag_rmap) (approx (Init.Nat.min m n)) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx m) (approx n)) *)
  destruct (make_rmap (resource_at a) nil (level a)) as (m' & ? & Hr & Hg); auto.
(* Goal: @eq (forall _ : AV.address, resource) (@compose AV.address resource resource (resource_fmap (approx (@level rmap ag_rmap a)) (approx (@level rmap ag_rmap a))) (resource_at a)) (resource_at a) *)
(* Goal: @ex rmap (fun m' : rmap => and (@eq nat (@level rmap ag_rmap m') (@level rmap ag_rmap a)) (and (@eq (forall _ : AV.address, resource) (resource_at m') (resource_at a)) (and (@eq ghost (ghost_of m') (@nil (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)))) (@app_pred rmap ag_rmap (@emp rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap) m')))) *)
  { intros; extensionality; apply resource_at_approx. }
(* Goal: @ex rmap (fun m' : rmap => and (@eq nat (@level rmap ag_rmap m') (@level rmap ag_rmap a)) (and (@eq (forall _ : AV.address, resource) (resource_at m') (resource_at a)) (and (@eq ghost (ghost_of m') (@nil (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)))) (@app_pred rmap ag_rmap (@emp rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap) m')))) *)
  exists m'; repeat split; auto.
(* Goal: @app_pred rmap ag_rmap (@emp rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap) m' *)
  apply all_resource_at_identity.
  - intro; rewrite Hr.
(* Goal: @identity resource Join_resource (resource_at a l) *)
    apply (resource_at_join _ _ _ l) in J.
(* Goal: @identity resource Join_resource (resource_at a l) *)
    inv J.
    + apply join_self, identity_share_bot in RJ; subst.
(* Goal: @identity resource Join_resource (NO Share.bot nsh1) *)
      apply NO_identity.
    + apply join_self, identity_share_bot in RJ; subst.
(* Goal: @identity resource Join_resource (YES Share.bot rsh1 k p) *)
      contradiction shares.bot_unreadable.
    + apply PURE_identity.
  - rewrite Hg, <- (ghost_core nil); apply core_identity.
Qed.

Lemma join_singleton_inv: forall k a b RA c v pp,
  join a b (singleton k (existT _ RA (exist _ (core c) v), pp)) ->
  a = singleton k (existT _ RA (exist _ (core c) v), pp) \/ b = singleton k (existT _ RA (exist _ (core c) v), pp).
Proof.
  induction k; unfold singleton; intros; simpl in *.
  - inv H; auto.
(* Goal: or (@eq (list (option (prod (@sigT Ghost (fun RA : Ghost => @sig (@G RA) (fun a : @G RA => @valid RA a))) preds))) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) a1 m1) (@cons (option (prod (@sigT Ghost (fun RA : Ghost => @sig (@G RA) (fun a : @G RA => @valid RA a))) preds)) (@Some (prod (@sigT Ghost (fun RA : Ghost => @sig (@G RA) (fun a : @G RA => @valid RA a))) preds) (@pair (@sigT Ghost (fun RA : Ghost => @sig (@G RA) (fun a : @G RA => @valid RA a))) preds (@existT Ghost (fun RA : Ghost => @sig (@G RA) (fun a : @G RA => @valid RA a)) RA (@exist (@G RA) (fun a : @G RA => @valid RA a) (@core (@G RA) (@Join_G RA) (@Sep_G RA) c) v)) pp)) (@nil (option (prod (@sigT Ghost (fun RA : Ghost => @sig (@G RA) (fun a : @G RA => @valid RA a))) preds))))) (@eq (list (option (prod (@sigT Ghost (fun RA : Ghost => @sig (@G RA) (fun a : @G RA => @valid RA a))) preds))) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) a2 m2) (@cons (option (prod (@sigT Ghost (fun RA : Ghost => @sig (@G RA) (fun a : @G RA => @valid RA a))) preds)) (@Some (prod (@sigT Ghost (fun RA : Ghost => @sig (@G RA) (fun a : @G RA => @valid RA a))) preds) (@pair (@sigT Ghost (fun RA : Ghost => @sig (@G RA) (fun a : @G RA => @valid RA a))) preds (@existT Ghost (fun RA : Ghost => @sig (@G RA) (fun a : @G RA => @valid RA a)) RA (@exist (@G RA) (fun a : @G RA => @valid RA a) (@core (@G RA) (@Join_G RA) (@Sep_G RA) c) v)) pp)) (@nil (option (prod (@sigT Ghost (fun RA : Ghost => @sig (@G RA) (fun a : @G RA => @valid RA a))) preds))))) *)
    assert (m1 = nil /\ m2 = nil) as [] by (inv H5; auto); subst.
(* Goal: @joins ghost ghost_join (ghost_fmap (approx (Init.Nat.min m n)) (approx (Init.Nat.min m n)) b) c *)
(* Goal: @eq (forall _ : @pred rmap ag_rmap, @pred rmap ag_rmap) (approx (Init.Nat.min m n)) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx m)) *)
(* Goal: @eq (forall _ : @pred rmap ag_rmap, @pred rmap ag_rmap) (approx (Init.Nat.min m n)) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx m) (approx n)) *)
    inv H4; auto.
    destruct a0, a3; inv H2; simpl in *.
(* Goal: or (@eq (list (option (prod (@sigT Ghost (fun RA : Ghost => @sig (@G RA) (fun a : @G RA => @valid RA a))) preds))) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) (@Some (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds) (@pair (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds s p)) (@nil (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)))) (@cons (option (prod (@sigT Ghost (fun RA : Ghost => @sig (@G RA) (fun a : @G RA => @valid RA a))) preds)) (@Some (prod (@sigT Ghost (fun RA : Ghost => @sig (@G RA) (fun a : @G RA => @valid RA a))) preds) (@pair (@sigT Ghost (fun RA : Ghost => @sig (@G RA) (fun a : @G RA => @valid RA a))) preds (@existT Ghost (fun RA : Ghost => @sig (@G RA) (fun a : @G RA => @valid RA a)) RA (@exist (@G RA) (fun a : @G RA => @valid RA a) (@core (@G RA) (@Join_G RA) (@Sep_G RA) c) v)) pp)) (@nil (option (prod (@sigT Ghost (fun RA : Ghost => @sig (@G RA) (fun a : @G RA => @valid RA a))) preds))))) (@eq (list (option (prod (@sigT Ghost (fun RA : Ghost => @sig (@G RA) (fun a : @G RA => @valid RA a))) preds))) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) (@Some (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds) (@pair (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds s0 p0)) (@nil (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)))) (@cons (option (prod (@sigT Ghost (fun RA : Ghost => @sig (@G RA) (fun a : @G RA => @valid RA a))) preds)) (@Some (prod (@sigT Ghost (fun RA : Ghost => @sig (@G RA) (fun a : @G RA => @valid RA a))) preds) (@pair (@sigT Ghost (fun RA : Ghost => @sig (@G RA) (fun a : @G RA => @valid RA a))) preds (@existT Ghost (fun RA : Ghost => @sig (@G RA) (fun a : @G RA => @valid RA a)) RA (@exist (@G RA) (fun a : @G RA => @valid RA a) (@core (@G RA) (@Join_G RA) (@Sep_G RA) c) v)) pp)) (@nil (option (prod (@sigT Ghost (fun RA : Ghost => @sig (@G RA) (fun a : @G RA => @valid RA a))) preds))))) *)
    inv H0; inv H.
(* Goal: or (@eq (list (option (prod (@sigT Ghost (fun RA : Ghost => @sig (@G RA) (fun a : @G RA => @valid RA a))) preds))) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) (@Some (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds) (@pair (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds (@existT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a)) RA (@exist (@G RA) (fun a : @G RA => @valid RA a) a0 va0)) pp)) (@nil (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)))) (@cons (option (prod (@sigT Ghost (fun RA : Ghost => @sig (@G RA) (fun a : @G RA => @valid RA a))) preds)) (@Some (prod (@sigT Ghost (fun RA : Ghost => @sig (@G RA) (fun a : @G RA => @valid RA a))) preds) (@pair (@sigT Ghost (fun RA : Ghost => @sig (@G RA) (fun a : @G RA => @valid RA a))) preds (@existT Ghost (fun RA : Ghost => @sig (@G RA) (fun a : @G RA => @valid RA a)) RA (@exist (@G RA) (fun a : @G RA => @valid RA a) (@core (@G RA) (@Join_G RA) (@Sep_G RA) c) v)) pp)) (@nil (option (prod (@sigT Ghost (fun RA : Ghost => @sig (@G RA) (fun a : @G RA => @valid RA a))) preds))))) (@eq (list (option (prod (@sigT Ghost (fun RA : Ghost => @sig (@G RA) (fun a : @G RA => @valid RA a))) preds))) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) (@Some (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds) (@pair (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds (@existT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a)) RA (@exist (@G RA) (fun a : @G RA => @valid RA a) b0 vb0)) pp)) (@nil (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)))) (@cons (option (prod (@sigT Ghost (fun RA : Ghost => @sig (@G RA) (fun a : @G RA => @valid RA a))) preds)) (@Some (prod (@sigT Ghost (fun RA : Ghost => @sig (@G RA) (fun a : @G RA => @valid RA a))) preds) (@pair (@sigT Ghost (fun RA : Ghost => @sig (@G RA) (fun a : @G RA => @valid RA a))) preds (@existT Ghost (fun RA : Ghost => @sig (@G RA) (fun a : @G RA => @valid RA a)) RA (@exist (@G RA) (fun a : @G RA => @valid RA a) (@core (@G RA) (@Join_G RA) (@Sep_G RA) c) v)) pp)) (@nil (option (prod (@sigT Ghost (fun RA : Ghost => @sig (@G RA) (fun a : @G RA => @valid RA a))) preds))))) *)
    inj_pair_tac.
(* Goal: or (@eq (list (option (prod (@sigT Ghost (fun RA : Ghost => @sig (@G RA) (fun a : @G RA => @valid RA a))) preds))) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) (@Some (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds) (@pair (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds (@existT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a)) RA (@exist (@G RA) (fun a : @G RA => @valid RA a) a0 va0)) pp)) (@nil (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)))) (@cons (option (prod (@sigT Ghost (fun RA : Ghost => @sig (@G RA) (fun a : @G RA => @valid RA a))) preds)) (@Some (prod (@sigT Ghost (fun RA : Ghost => @sig (@G RA) (fun a : @G RA => @valid RA a))) preds) (@pair (@sigT Ghost (fun RA : Ghost => @sig (@G RA) (fun a : @G RA => @valid RA a))) preds (@existT Ghost (fun RA : Ghost => @sig (@G RA) (fun a : @G RA => @valid RA a)) RA (@exist (@G RA) (fun a : @G RA => @valid RA a) (@core (@G RA) (@Join_G RA) (@Sep_G RA) c) v)) pp)) (@nil (option (prod (@sigT Ghost (fun RA : Ghost => @sig (@G RA) (fun a : @G RA => @valid RA a))) preds))))) (@eq (list (option (prod (@sigT Ghost (fun RA : Ghost => @sig (@G RA) (fun a : @G RA => @valid RA a))) preds))) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) (@Some (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds) (@pair (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds (@existT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a)) RA (@exist (@G RA) (fun a : @G RA => @valid RA a) b0 vb0)) pp)) (@nil (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)))) (@cons (option (prod (@sigT Ghost (fun RA : Ghost => @sig (@G RA) (fun a : @G RA => @valid RA a))) preds)) (@Some (prod (@sigT Ghost (fun RA : Ghost => @sig (@G RA) (fun a : @G RA => @valid RA a))) preds) (@pair (@sigT Ghost (fun RA : Ghost => @sig (@G RA) (fun a : @G RA => @valid RA a))) preds (@existT Ghost (fun RA : Ghost => @sig (@G RA) (fun a : @G RA => @valid RA a)) RA (@exist (@G RA) (fun a : @G RA => @valid RA a) (@core (@G RA) (@Join_G RA) (@Sep_G RA) c) v)) pp)) (@nil (option (prod (@sigT Ghost (fun RA : Ghost => @sig (@G RA) (fun a : @G RA => @valid RA a))) preds))))) *)
    pose proof (core_unit a0) as J.
(* Goal: @joins ghost ghost_join (ghost_fmap (approx (Init.Nat.min m n)) (approx (Init.Nat.min m n)) b) c *)
(* Goal: @eq (forall _ : @pred rmap ag_rmap, @pred rmap ag_rmap) (approx (Init.Nat.min m n)) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx m)) *)
(* Goal: @eq (forall _ : @pred rmap ag_rmap, @pred rmap ag_rmap) (approx (Init.Nat.min m n)) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx m) (approx n)) *)
    erewrite join_core, core_idem in J by eauto.
(* Goal: or (@eq (list (option (prod (@sigT Ghost (fun RA : Ghost => @sig (@G RA) (fun a : @G RA => @valid RA a))) preds))) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) (@Some (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds) (@pair (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds (@existT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a)) RA (@exist (@G RA) (fun a : @G RA => @valid RA a) a0 va0)) pp)) (@nil (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)))) (@cons (option (prod (@sigT Ghost (fun RA : Ghost => @sig (@G RA) (fun a : @G RA => @valid RA a))) preds)) (@Some (prod (@sigT Ghost (fun RA : Ghost => @sig (@G RA) (fun a : @G RA => @valid RA a))) preds) (@pair (@sigT Ghost (fun RA : Ghost => @sig (@G RA) (fun a : @G RA => @valid RA a))) preds (@existT Ghost (fun RA : Ghost => @sig (@G RA) (fun a : @G RA => @valid RA a)) RA (@exist (@G RA) (fun a : @G RA => @valid RA a) (@core (@G RA) (@Join_G RA) (@Sep_G RA) c) v)) pp)) (@nil (option (prod (@sigT Ghost (fun RA : Ghost => @sig (@G RA) (fun a : @G RA => @valid RA a))) preds))))) (@eq (list (option (prod (@sigT Ghost (fun RA : Ghost => @sig (@G RA) (fun a : @G RA => @valid RA a))) preds))) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) (@Some (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds) (@pair (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds (@existT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a)) RA (@exist (@G RA) (fun a : @G RA => @valid RA a) b0 vb0)) pp)) (@nil (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)))) (@cons (option (prod (@sigT Ghost (fun RA : Ghost => @sig (@G RA) (fun a : @G RA => @valid RA a))) preds)) (@Some (prod (@sigT Ghost (fun RA : Ghost => @sig (@G RA) (fun a : @G RA => @valid RA a))) preds) (@pair (@sigT Ghost (fun RA : Ghost => @sig (@G RA) (fun a : @G RA => @valid RA a))) preds (@existT Ghost (fun RA : Ghost => @sig (@G RA) (fun a : @G RA => @valid RA a)) RA (@exist (@G RA) (fun a : @G RA => @valid RA a) (@core (@G RA) (@Join_G RA) (@Sep_G RA) c) v)) pp)) (@nil (option (prod (@sigT Ghost (fun RA : Ghost => @sig (@G RA) (fun a : @G RA => @valid RA a))) preds))))) *)
    unfold unit_for in J.
(* Goal: or (@eq (list (option (prod (@sigT Ghost (fun RA : Ghost => @sig (@G RA) (fun a : @G RA => @valid RA a))) preds))) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) (@Some (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds) (@pair (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds (@existT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a)) RA (@exist (@G RA) (fun a : @G RA => @valid RA a) a0 va0)) pp)) (@nil (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)))) (@cons (option (prod (@sigT Ghost (fun RA : Ghost => @sig (@G RA) (fun a : @G RA => @valid RA a))) preds)) (@Some (prod (@sigT Ghost (fun RA : Ghost => @sig (@G RA) (fun a : @G RA => @valid RA a))) preds) (@pair (@sigT Ghost (fun RA : Ghost => @sig (@G RA) (fun a : @G RA => @valid RA a))) preds (@existT Ghost (fun RA : Ghost => @sig (@G RA) (fun a : @G RA => @valid RA a)) RA (@exist (@G RA) (fun a : @G RA => @valid RA a) (@core (@G RA) (@Join_G RA) (@Sep_G RA) c) v)) pp)) (@nil (option (prod (@sigT Ghost (fun RA : Ghost => @sig (@G RA) (fun a : @G RA => @valid RA a))) preds))))) (@eq (list (option (prod (@sigT Ghost (fun RA : Ghost => @sig (@G RA) (fun a : @G RA => @valid RA a))) preds))) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) (@Some (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds) (@pair (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds (@existT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a)) RA (@exist (@G RA) (fun a : @G RA => @valid RA a) b0 vb0)) pp)) (@nil (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)))) (@cons (option (prod (@sigT Ghost (fun RA : Ghost => @sig (@G RA) (fun a : @G RA => @valid RA a))) preds)) (@Some (prod (@sigT Ghost (fun RA : Ghost => @sig (@G RA) (fun a : @G RA => @valid RA a))) preds) (@pair (@sigT Ghost (fun RA : Ghost => @sig (@G RA) (fun a : @G RA => @valid RA a))) preds (@existT Ghost (fun RA : Ghost => @sig (@G RA) (fun a : @G RA => @valid RA a)) RA (@exist (@G RA) (fun a : @G RA => @valid RA a) (@core (@G RA) (@Join_G RA) (@Sep_G RA) c) v)) pp)) (@nil (option (prod (@sigT Ghost (fun RA : Ghost => @sig (@G RA) (fun a : @G RA => @valid RA a))) preds))))) *)
    eapply join_positivity in J; eauto; subst.
(* Goal: or (@eq (list (option (prod (@sigT Ghost (fun RA : Ghost => @sig (@G RA) (fun a : @G RA => @valid RA a))) preds))) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) (@Some (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds) (@pair (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds (@existT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a)) RA (@exist (@G RA) (fun a : @G RA => @valid RA a) (@core (@G RA) (@Join_G RA) (@Sep_G RA) c) va0)) pp)) (@nil (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)))) (@cons (option (prod (@sigT Ghost (fun RA : Ghost => @sig (@G RA) (fun a : @G RA => @valid RA a))) preds)) (@Some (prod (@sigT Ghost (fun RA : Ghost => @sig (@G RA) (fun a : @G RA => @valid RA a))) preds) (@pair (@sigT Ghost (fun RA : Ghost => @sig (@G RA) (fun a : @G RA => @valid RA a))) preds (@existT Ghost (fun RA : Ghost => @sig (@G RA) (fun a : @G RA => @valid RA a)) RA (@exist (@G RA) (fun a : @G RA => @valid RA a) (@core (@G RA) (@Join_G RA) (@Sep_G RA) c) v)) pp)) (@nil (option (prod (@sigT Ghost (fun RA : Ghost => @sig (@G RA) (fun a : @G RA => @valid RA a))) preds))))) (@eq (list (option (prod (@sigT Ghost (fun RA : Ghost => @sig (@G RA) (fun a : @G RA => @valid RA a))) preds))) (@cons (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)) (@Some (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds) (@pair (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds (@existT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a)) RA (@exist (@G RA) (fun a : @G RA => @valid RA a) b0 vb0)) pp)) (@nil (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)))) (@cons (option (prod (@sigT Ghost (fun RA : Ghost => @sig (@G RA) (fun a : @G RA => @valid RA a))) preds)) (@Some (prod (@sigT Ghost (fun RA : Ghost => @sig (@G RA) (fun a : @G RA => @valid RA a))) preds) (@pair (@sigT Ghost (fun RA : Ghost => @sig (@G RA) (fun a : @G RA => @valid RA a))) preds (@existT Ghost (fun RA : Ghost => @sig (@G RA) (fun a : @G RA => @valid RA a)) RA (@exist (@G RA) (fun a : @G RA => @valid RA a) (@core (@G RA) (@Join_G RA) (@Sep_G RA) c) v)) pp)) (@nil (option (prod (@sigT Ghost (fun RA : Ghost => @sig (@G RA) (fun a : @G RA => @valid RA a))) preds))))) *)
    left; repeat f_equal; apply proof_irr.
  - inv H; auto.
(* Goal: @joins ghost ghost_join (ghost_fmap (approx (Init.Nat.min m n)) (approx (Init.Nat.min m n)) b) c *)
(* Goal: @eq (forall _ : @pred rmap ag_rmap, @pred rmap ag_rmap) (approx (Init.Nat.min m n)) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx m)) *)
(* Goal: @eq (forall _ : @pred rmap ag_rmap, @pred rmap ag_rmap) (approx (Init.Nat.min m n)) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx m) (approx n)) *)
    edestruct IHk as [|]; eauto; [left | right]; f_equal; auto; inv H4; auto.
Qed.

Lemma own_cored: forall {RA: Ghost} g a pp, join a a a -> own g a pp |-- cored.
Proof.
(* Goal: forall (RA : Ghost) (g : gname) (a : @G RA) (pp : preds) (_ : @join (@G RA) (@Join_G RA) a a a), @derives rmap ag_rmap (@own RA g a pp) cored *)
  intros; intros ? (? & ? & Hg).
  rewrite cored_unit; simpl in *.
(* Goal: @join rmap Join_rmap a0 a0 a0 *)
  apply resource_at_join2; auto.
  - intro; apply identity_unit'.
(* Goal: @joins ghost ghost_join (ghost_fmap (approx (Init.Nat.min m n)) (approx (Init.Nat.min m n)) b) c *)
(* Goal: @eq (forall _ : @pred rmap ag_rmap, @pred rmap ag_rmap) (approx (Init.Nat.min m n)) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx m)) *)
(* Goal: @eq (forall _ : @pred rmap ag_rmap, @pred rmap ag_rmap) (approx (Init.Nat.min m n)) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx m) (approx n)) *)
    eapply necR_resource_at_identity; eauto.
  - rewrite Hg, ghost_fmap_singleton.
(* Goal: @joins ghost ghost_join (ghost_fmap (approx (Init.Nat.min m n)) (approx (Init.Nat.min m n)) b) c *)
(* Goal: @eq (forall _ : @pred rmap ag_rmap, @pred rmap ag_rmap) (approx (Init.Nat.min m n)) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx m)) *)
(* Goal: @eq (forall _ : @pred rmap ag_rmap, @pred rmap ag_rmap) (approx (Init.Nat.min m n)) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx m) (approx n)) *)
    apply singleton_join; repeat constructor; auto.
Qed.

Require Import VST.veric.tycontext.
Require Import VST.veric.Clight_seplog.
 
(* Goal: @eq (forall _ : AV.address, resource) (@compose AV.address resource resource (resource_fmap (approx (@level rmap ag_rmap a)) (approx (@level rmap ag_rmap a))) (resource_at a)) (resource_at a) *)
(* Goal: @ex rmap (fun m' : rmap => and (@eq nat (@level rmap ag_rmap m') (@level rmap ag_rmap a)) (and (@eq (forall _ : AV.address, resource) (resource_at m') (resource_at a)) (and (@eq ghost (ghost_of m') (@nil (option (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds)))) (@app_pred rmap ag_rmap (@emp rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap) m')))) *)
Lemma own_super_non_expansive: forall {RA: Ghost} n g a pp,
  approx n (own g a pp) = approx n (own g a (preds_fmap (approx n) (approx n) pp)).
Proof.
(* Goal: forall (RA : Ghost) (n : nat) (g : gname) (a : @G RA) (pp : preds), @eq (@pred rmap ag_rmap) (approx n (@own RA g a pp)) (approx n (@own RA g a (preds_fmap (approx n) (approx n) pp))) *)
  intros; unfold own.
(* Goal: @eq (@pred rmap ag_rmap) (approx n (@exp rmap ag_rmap (@valid RA a) (fun v : @valid RA a => Own (@singleton (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds) g (@pair (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds (@existT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a)) RA (@exist (@G RA) (fun a : @G RA => @valid RA a) a v)) pp))))) (approx n (@exp rmap ag_rmap (@valid RA a) (fun v : @valid RA a => Own (@singleton (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds) g (@pair (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds (@existT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a)) RA (@exist (@G RA) (fun a : @G RA => @valid RA a) a v)) (preds_fmap (approx n) (approx n) pp)))))) *)
  rewrite !approx_exp; f_equal; extensionality v.
(* Goal: @eq (@pred rmap ag_rmap) (approx n (Own (@singleton (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds) g (@pair (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds (@existT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a)) RA (@exist (@G RA) (fun a : @G RA => @valid RA a) a v)) pp)))) (approx n (Own (@singleton (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds) g (@pair (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds (@existT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a)) RA (@exist (@G RA) (fun a : @G RA => @valid RA a) a v)) (preds_fmap (approx n) (approx n) pp))))) *)
  unfold Own.
(* Goal: @eq (@pred rmap ag_rmap) (approx n (@andp rmap ag_rmap (@allp rmap ag_rmap AV.address noat) (ghost_is (@singleton (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds) g (@pair (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds (@existT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a)) RA (@exist (@G RA) (fun a : @G RA => @valid RA a) a v)) pp))))) (approx n (@andp rmap ag_rmap (@allp rmap ag_rmap AV.address noat) (ghost_is (@singleton (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds) g (@pair (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds (@existT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a)) RA (@exist (@G RA) (fun a : @G RA => @valid RA a) a v)) (preds_fmap (approx n) (approx n) pp)))))) *)
  rewrite !approx_andp; f_equal.
  apply pred_ext; intros ? [? Hg]; split; auto; simpl in *.
  - rewrite <- ghost_of_approx, Hg.
(* Goal: @eq ghost (ghost_fmap (approx (@level rmap ag_rmap a0)) (approx (@level rmap ag_rmap a0)) (ghost_fmap (approx (@level rmap ag_rmap a0)) (approx (@level rmap ag_rmap a0)) (@singleton (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds) g (@pair (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds (@existT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a)) RA (@exist (@G RA) (fun a : @G RA => @valid RA a) a v)) pp)))) (ghost_fmap (approx (@level rmap ag_rmap a0)) (approx (@level rmap ag_rmap a0)) (@singleton (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds) g (@pair (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds (@existT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a)) RA (@exist (@G RA) (fun a : @G RA => @valid RA a) a v)) (preds_fmap (approx n) (approx n) pp)))) *)
    rewrite !ghost_fmap_singleton, !preds_fmap_fmap.
(* Goal: @joins ghost ghost_join (ghost_fmap (approx (Init.Nat.min m n)) (approx (Init.Nat.min m n)) b) c *)
(* Goal: @eq (forall _ : @pred rmap ag_rmap, @pred rmap ag_rmap) (approx (Init.Nat.min m n)) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx m)) *)
(* Goal: @eq (forall _ : @pred rmap ag_rmap, @pred rmap ag_rmap) (approx (Init.Nat.min m n)) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx m) (approx n)) *)
    rewrite approx_oo_approx, approx_oo_approx', approx'_oo_approx by omega; auto.
  - rewrite ghost_fmap_singleton in *.
(* Goal: @eq ghost (ghost_of a0) (@singleton (prod (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds) g (@pair (@sigT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a))) preds (@existT Ghost (fun g : Ghost => @sig (@G g) (fun a : @G g => @valid g a)) RA (@exist (@G RA) (fun a : @G RA => @valid RA a) a v)) (preds_fmap (approx (@level rmap ag_rmap a0)) (approx (@level rmap ag_rmap a0)) pp))) *)
    rewrite preds_fmap_fmap in Hg.
(* Goal: @joins ghost ghost_join (ghost_fmap (approx (Init.Nat.min m n)) (approx (Init.Nat.min m n)) b) c *)
(* Goal: @eq (forall _ : @pred rmap ag_rmap, @pred rmap ag_rmap) (approx (Init.Nat.min m n)) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) (approx m)) *)
(* Goal: @eq (forall _ : @pred rmap ag_rmap, @pred rmap ag_rmap) (approx (Init.Nat.min m n)) (@compose (@pred rmap ag_rmap) (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx m) (approx n)) *)
    rewrite approx_oo_approx', approx'_oo_approx in Hg by omega; auto.
Qed.
