Require Import VST.veric.compcert_rmaps.
Require Export VST.msl.ghost.
Require Import VST.msl.sepalg.
Require Import VST.msl.sepalg_generators.
Require Import VST.veric.SeparationLogic.
Require Import VST.progs.conclib.
Import List.

(* Lemmas about ghost state and common instances *)
(* Where should this sit? *)

Hint Resolve Share.nontrivial.

Definition gname := own.gname.

Instance Inhabitant_preds : Inhabitant preds := NoneP.

Section ghost.

Context {RA: Ghost}.

Lemma own_op' : forall g a1 a2 pp,
  own g a1 pp * own g a2 pp = EX a3 : _, !!(join a1 a2 a3 /\ valid a3) && own g a3 pp.
Proof.
(* Goal: forall P Q : mpred, @derives mpred Nveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (weak_view_shift P Q) (@emp mpred Nveric Sveric)) P) (@bupd mpred own.gname preds Nveric Sveric Bveric Q) *)
  intros.
(* Goal: @eq mpred (@exp mpred Nveric (@G map_PCM) (fun v : @G map_PCM => @andp mpred Nveric (@prop mpred Nveric (@join (@G map_PCM) (@Join_G map_PCM) m1 m2 v)) (@ghost_snap map_PCM map_incl fmap_order v p))) (@andp mpred Nveric (@prop mpred Nveric (compatible m1 m2)) (@ghost_snap map_PCM map_incl fmap_order (map_add m1 m2) p)) *)
  apply pred_ext.
  - assert_PROP (valid_2 a1 a2) as Hjoin by (apply own_valid_2).
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@own mpred own.gname preds Nveric Sveric Bveric RA g a1 pp) (@own mpred own.gname preds Nveric Sveric Bveric RA g a2 pp)) (@exp mpred Nveric (@G RA) (fun a3 : @G RA => @andp mpred Nveric (@prop mpred Nveric (and (@join (@G RA) (@Join_G RA) a1 a2 a3) (@valid RA a3))) (@own mpred own.gname preds Nveric Sveric Bveric RA g a3 pp))) *)
    destruct Hjoin as (a3 & ? & ?); Exists a3; entailer!.
    erewrite <- own_op by eauto.  apply derives_refl.
  - Intros a3.
(* Goal: @derives mpred Nveric (ghost_master Tsh v' p) (ghost_master1 v' p) *)
    erewrite own_op by eauto.  apply derives_refl.
Qed.

Lemma own_op_gen : forall g a1 a2 a3 pp, (valid_2 a1 a2 -> join a1 a2 a3) ->
  own g a1 pp * own g a2 pp = !!(valid_2 a1 a2) && own g a3 pp.
Proof.
(* Goal: @eq mpred (@exp mpred Nveric (@G map_PCM) (fun v : @G map_PCM => @andp mpred Nveric (@prop mpred Nveric (@join (@G map_PCM) (@Join_G map_PCM) m1 m2 v)) (@ghost_snap map_PCM map_incl fmap_order v p))) (@andp mpred Nveric (@prop mpred Nveric (compatible m1 m2)) (@ghost_snap map_PCM map_incl fmap_order (map_add m1 m2) p)) *)
  intros; apply pred_ext.
  - assert_PROP (valid_2 a1 a2) as Hv by apply own_valid_2.
    erewrite <- own_op by eauto; entailer!.
  - Intros.
(* Goal: @derives mpred Nveric (@own mpred own.gname preds Nveric Sveric Bveric RA g a3 pp) (@sepcon mpred Nveric Sveric (@own mpred own.gname preds Nveric Sveric Bveric RA g a1 pp) (@own mpred own.gname preds Nveric Sveric Bveric RA g a2 pp)) *)
    erewrite own_op by eauto; entailer!.
Qed.

(* own isn't precise unless the ghost is a Disj_alg. Is this a problem? *)

Lemma own_list_alloc : forall la lp, Forall valid la -> length lp = length la ->
  emp |-- |==> (EX lg : _, !!(Zlength lg = Zlength la) &&
    iter_sepcon (fun '(g, a, p) => own g a p) (combine (combine lg la) lp)).
Proof.
(* Goal: forall P Q : mpred, @derives mpred Nveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (weak_view_shift P Q) (@emp mpred Nveric Sveric)) P) (@bupd mpred own.gname preds Nveric Sveric Bveric Q) *)
  intros until 1; revert lp; induction H; intros.
  - eapply derives_trans, bupd_intro.
    Exists (@nil own.gname). simpl. entailer!.
  - destruct lp; inv H1.
    rewrite <- emp_sepcon at 1.
    eapply derives_trans; [apply sepcon_derives; [apply IHForall; eauto | apply own_alloc; eauto]|].
    eapply derives_trans; [apply bupd_sepcon|].
    apply bupd_mono.
    Intros lg g.
(* Goal: match empty_map k with | Some v => match t k with | Some b => False | None => @eq (option B) (t k) (@Some B v) end | None => match t k with | Some v => @eq (option B) (t k) (@Some B v) | None => @eq (option B) (t k) (@None B) end end *)
    Exists (g :: lg); rewrite !Zlength_cons; simpl.
    rewrite sepcon_comm; entailer!.
(* Goal: @derives mpred Nveric (ghost_master Tsh v' p) (ghost_master1 v' p) *)
    apply derives_refl.
Qed.

Corollary own_list_alloc' : forall a pp i, 0 <= i -> valid a ->
  emp |-- |==> (EX lg : _, !!(Zlength lg = i) && iter_sepcon (fun g => own g a pp) lg).
Proof.
(* Goal: forall P Q : mpred, @derives mpred Nveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (weak_view_shift P Q) (@emp mpred Nveric Sveric)) P) (@bupd mpred own.gname preds Nveric Sveric Bveric Q) *)
  intros.
  eapply derives_trans;
    [apply own_list_alloc with (la := repeat a (Z.to_nat i))(lp := repeat pp (Z.to_nat i))|].
(* Goal: @compatible nat hist_el (@map_upd nat hist_el nat_eq_dec h2 t e) h *)
  { apply Forall_repeat; auto. }
(* Goal: @compatible nat hist_el (@map_upd nat hist_el nat_eq_dec h2 t e) h *)
  { rewrite !repeat_length; auto. }
  apply bupd_mono; Intros lg; Exists lg.
  rewrite Zlength_repeat, Z2Nat.id in H1 by omega.
  rewrite !combine_const1 by (rewrite ?Zlength_combine, ?Zlength_repeat, ?Z2Nat.id, ?Z.min_r; omega).
  entailer!.
  clear H; induction lg; simpl; entailer!.
Qed.

(* Goal: @compatible nat hist_el (@map_upd nat hist_el nat_eq_dec h2 t e) h *)
Lemma own_list_dealloc : forall {A} f (l : list A),
  (forall b, exists g a pp, f b |-- own g a pp) ->
  iter_sepcon f l |-- |==> emp.
Proof.
(* Goal: match empty_map k with | Some v => match t k with | Some b => False | None => @eq (option B) (t k) (@Some B v) end | None => match t k with | Some v => @eq (option B) (t k) (@Some B v) | None => @eq (option B) (t k) (@None B) end end *)
  intros; induction l; simpl.
  - apply bupd_intro.
  - eapply derives_trans; [apply sepcon_derives, IHl|].
    + destruct (H a) as (? & ? & ? & Hf).
      eapply derives_trans; [apply Hf | apply own_dealloc].
    + eapply derives_trans, bupd_mono; [apply bupd_sepcon | cancel].
Qed.

(* Goal: @compatible nat hist_el (@map_upd nat hist_el nat_eq_dec h2 t e) h *)
Lemma own_list_dealloc' : forall {A} g a p (l : list A),
  iter_sepcon (fun x => own (g x) (a x) (p x)) l |-- |==> emp.
Proof.
(* Goal: forall (A : Type) (g : forall _ : A, own.gname) (a : forall _ : A, @G RA) (p : forall _ : A, preds) (l : list A), @derives mpred Nveric (@iter_sepcon mpred A Nveric Sveric (fun x : A => @own mpred own.gname preds Nveric Sveric Bveric RA (g x) (a x) (p x)) l) (@bupd mpred own.gname preds Nveric Sveric Bveric (@emp mpred Nveric Sveric)) *)
  intros; apply own_list_dealloc.
(* Goal: @derives mpred Nveric (ghost_master Tsh v' p) (ghost_master1 v' p) *)
  repeat eexists; apply derives_refl.
Qed.

End ghost.

(* Goal: @compatible nat hist_el (@map_upd nat hist_el nat_eq_dec h2 t e) h *)
Program Instance exclusive_PCM A : Ghost := { valid a := True;
  Join_G := Join_lower (Join_discrete A) }.

(* Goal: @compatible nat hist_el (@map_upd nat hist_el nat_eq_dec h2 t e) h *)
Definition excl {A} g a := own(RA := exclusive_PCM A) g (Some a) NoneP.

Lemma exclusive_update : forall {A} (v v' : A) p, excl p v |-- |==> excl p v'.
Proof.
(* Goal: forall (v : A) (p : own.gname) (v' : A), @derives mpred Nveric (ghost_var Tsh v p) (@bupd mpred own.gname preds Nveric Sveric Bveric (ghost_var Tsh v' p)) *)
  intros; apply own_update.
(* Goal: @fp_update (exclusive_PCM A) (@Some A v) (@Some A v') *)
  intros ? (? & ? & _).
(* Goal: @valid_2 (exclusive_PCM A) (@Some A v') c *)
  exists (Some v'); split; simpl; auto; inv H; constructor.
(* Goal: @join A (Join_discrete A) v' a2 v' *)
  inv H1.
Qed.

Local Obligation Tactic := idtac.

(* Goal: @compatible nat hist_el (@map_upd nat hist_el nat_eq_dec h2 t e) h *)
Program Instance prod_PCM (GA GB: Ghost): Ghost := { G := @G GA * @G GB;
  valid a := valid (fst a) /\ valid (snd a); Join_G := Join_prod _ _ _ _ }.
Next Obligation.
(* Goal: forall (GA GB : Ghost) (a b c : prod (@G GA) (@G GB)) (_ : @join (prod (@G GA) (@G GB)) (Join_prod (@G GA) (@Join_G GA) (@G GB) (@Join_G GB)) a b c) (_ : (fun a0 : prod (@G GA) (@G GB) => and (@valid GA (@fst (@G GA) (@G GB) a0)) (@valid GB (@snd (@G GA) (@G GB) a0))) c), (fun a0 : prod (@G GA) (@G GB) => and (@valid GA (@fst (@G GA) (@G GB) a0)) (@valid GB (@snd (@G GA) (@G GB) a0))) a *)
  intros GA GB ??? [] []; split; eapply join_valid; eauto.
Defined.

(* Can we use Santiago and Qinxiang's paper to simplify this? *)
Class PCM_order `{P : Ghost} (ord : G -> G -> Prop) := { ord_refl :> RelationClasses.Reflexive ord;
  ord_trans :> RelationClasses.Transitive ord;
  ord_lub : forall a b c, ord a c -> ord b c -> {c' | join a b c' /\ ord c' c};
  join_ord : forall a b c, join a b c -> ord a c /\ ord b c; ord_join : forall a b, ord b a -> join a b a }.

(*Class lub_ord {A} (ord : A -> A -> Prop) := { lub_ord_refl :> RelationClasses.Reflexive ord;
  lub_ord_trans :> RelationClasses.Transitive ord;
  has_lub : forall a b c, ord a c -> ord b c -> exists c', ord a c' /\ ord b c' /\
    forall d, ord a d -> ord b d -> ord c' d }.

(* Goal: @compatible nat hist_el (@map_upd nat hist_el nat_eq_dec h2 t e) h *)
Global Instance ord_PCM `{lub_ord} : Ghost := { Join_G a b c := ord a c /\ ord b c /\
  forall c', ord a c' -> ord b c' -> ord c c' }.
Proof.
  - 
  - intros ??? (? & ? & ?); eauto.
  - intros ????? (? & ? & Hc) (? & ? & He).
    destruct (has_lub b d e) as (c' & ? & ? & Hlub); try solve [etransitivity; eauto].
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
    exists c'; repeat split; auto.
    + etransitivity; eauto.
    + apply Hlub; auto; transitivity c; auto.
(* Goal: forall P Q : mpred, @derives mpred Nveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (weak_view_shift P Q) (@emp mpred Nveric Sveric)) P) (@bupd mpred own.gname preds Nveric Sveric Bveric Q) *)
    + intros.
      apply He.
(* Goal: ord v1 c *)
      * apply Hc; auto; etransitivity; eauto.
(* Goal: ord v1 c *)
      * etransitivity; eauto.
Defined.

(* Goal: @compatible nat hist_el (@map_upd nat hist_el nat_eq_dec h2 t e) h *)
Global Instance ord_PCM_ord `{lub_ord} : PCM_order ord.
Proof.
(* Goal: hist_list' (@map_upd nat hist_el nat_eq_dec h0 (@Datatypes.length hist_el l) x) (@app hist_el l (@cons hist_el x (@nil hist_el))) *)
(* Goal: @eq (forall _ : nat, option hist_el) (@map_upd nat hist_el nat_eq_dec h0 (@Datatypes.length hist_el l) x) h *)
  constructor.
  - apply lub_ord_refl.
  - apply lub_ord_trans.
  - intros ??? Ha Hb.
    destruct (has_lub _ _ _ Ha Hb) as (c' & ? & ? & ?).
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
    exists c'; simpl; eauto.
  - simpl; intros; tauto.
  - intros; simpl.
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
    repeat split; auto.
    reflexivity.
Defined.*)

(* Instances of ghost state *)
Section Snapshot.
(* One common kind of PCM is one in which a central authority has a reference copy, and clients pass around
   partial knowledge. *)

(* Goal: @compatible nat hist_el (@map_upd nat hist_el nat_eq_dec h2 t e) h *)
Context `{ORD : PCM_order}.

Lemma join_refl : forall (v : G), join v v v.
Proof.
(* Goal: forall P Q : mpred, @derives mpred Nveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (weak_view_shift P Q) (@emp mpred Nveric Sveric)) P) (@bupd mpred own.gname preds Nveric Sveric Bveric Q) *)
  intros. apply ord_join; reflexivity.
Qed.

Lemma join_compat : forall v1 v2 v' v'', join v2 v' v'' -> ord v1 v2 -> exists v0, join v1 v' v0 /\ ord v0 v''.
Proof.
(* Goal: forall P Q : mpred, @derives mpred Nveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (weak_view_shift P Q) (@emp mpred Nveric Sveric)) P) (@bupd mpred own.gname preds Nveric Sveric Bveric Q) *)
  intros.
(* Goal: @ex (@G P) (fun v0 : @G P => and (@join (@G P) (@Join_G P) v1 v' v0) (ord v0 v'')) *)
  destruct (join_ord _ _ _ H).
(* Goal: @ex (@G P) (fun v0 : @G P => and (@join (@G P) (@Join_G P) v1 v' v0) (ord v0 v'')) *)
  destruct (ord_lub v1 v' v'') as (? & ? & ?); eauto.
(* Goal: ord v1 c *)
  etransitivity; eauto.
Qed.

Lemma join_ord_eq : forall a b, ord a b <-> exists c, join a c b.
Proof.
(* Goal: and (not (@eq share (Share.comp sh) Share.bot)) (and (@join share Share.Join_ba sh (Share.comp sh) Tsh) (@join (forall _ : nat, option hist_el) (@map_disj_join nat hist_el) h h' hr)) *)
  split.
  - intros; exists b.
(* Goal: @join (@G P) (@Join_G P) a b b *)
    apply ord_join in H.
(* Goal: @join (@G P) (@Join_G P) a b b *)
    apply join_comm; auto.
  - intros (? & H); apply join_ord in H; tauto.
Qed.

(* The master-snapshot PCM in the RCU paper divides the master into shares, which is useful for having both
   an authoritative writer and an up-to-date invariant. *)

Global Program Instance snap_PCM : Ghost :=
(* Goal: @compatible nat hist_el (@map_upd nat hist_el nat_eq_dec h2 t e) h *)
  { valid _ := True; Join_G a b c := sepalg.join (fst a) (fst b) (fst c) /\
      if eq_dec (fst a) Share.bot then if eq_dec (fst b) Share.bot then join (snd a) (snd b) (snd c)
        else ord (snd a) (snd b) /\ snd c = snd b else snd c = snd a /\
          if eq_dec (fst b) Share.bot then ord (snd b) (snd a) else snd c = snd b }.
Next Obligation.
(* Goal: @Sep_alg (prod Share.t (@G P)) (fun a b c : prod Share.t (@G P) => and (@join Share.t Share.Join_ba (@fst Share.t (@G P) a) (@fst Share.t (@G P) b) (@fst Share.t (@G P) c)) (if @eq_dec Share.t Share.EqDec_share (@fst Share.t (@G P) a) Share.bot then if @eq_dec Share.t Share.EqDec_share (@fst Share.t (@G P) b) Share.bot then @join (@G P) (@Join_G P) (@snd Share.t (@G P) a) (@snd Share.t (@G P) b) (@snd Share.t (@G P) c) else and (ord (@snd Share.t (@G P) a) (@snd Share.t (@G P) b)) (@eq (@G P) (@snd Share.t (@G P) c) (@snd Share.t (@G P) b)) else and (@eq (@G P) (@snd Share.t (@G P) c) (@snd Share.t (@G P) a)) (if @eq_dec Share.t Share.EqDec_share (@fst Share.t (@G P) b) Share.bot then ord (@snd Share.t (@G P) b) (@snd Share.t (@G P) a) else @eq (@G P) (@snd Share.t (@G P) c) (@snd Share.t (@G P) b)))) *)
  exists (fun '(sh, a) => (Share.bot, core a)); repeat intro.
(* Goal: match empty_map k with | Some v => match t k with | Some b => False | None => @eq (option B) (t k) (@Some B v) end | None => match t k with | Some v => @eq (option B) (t k) (@Some B v) | None => @eq (option B) (t k) (@None B) end end *)
  + destruct t; constructor; auto; simpl.
(* Goal: if @eq_dec Share.t Share.EqDec_share Share.bot Share.bot then if @eq_dec Share.t Share.EqDec_share t Share.bot then @join (@G P) (@Join_G P) (@core (@G P) (@Join_G P) (@Sep_G P) g) g g else and (ord (@core (@G P) (@Join_G P) (@Sep_G P) g) g) (@eq (@G P) g g) else and (@eq (@G P) g (@core (@G P) (@Join_G P) (@Sep_G P) g)) (if @eq_dec Share.t Share.EqDec_share t Share.bot then ord g (@core (@G P) (@Join_G P) (@Sep_G P) g) else @eq (@G P) g g) *)
    rewrite eq_dec_refl.
(* Goal: if @eq_dec Share.t Share.EqDec_share t Share.bot then @join (@G P) (@Join_G P) (@core (@G P) (@Join_G P) (@Sep_G P) g) g g else and (ord (@core (@G P) (@Join_G P) (@Sep_G P) g) g) (@eq (@G P) g g) *)
    if_tac; [apply core_unit | split; auto].
(* Goal: ord (@core (@G P) (@Join_G P) (@Sep_G P) g) g *)
    rewrite join_ord_eq; eexists; apply core_unit.
  + destruct a, b, c; f_equal.
(* Goal: @eq (@G P) (@core (@G P) (@Join_G P) (@Sep_G P) g) (@core (@G P) (@Join_G P) (@Sep_G P) g1) *)
    inv H; simpl in *.
(* Goal: @eq (@G P) (@core (@G P) (@Join_G P) (@Sep_G P) g) (@core (@G P) (@Join_G P) (@Sep_G P) g1) *)
    destruct (eq_dec t Share.bot); [|destruct H1; subst; auto].
(* Goal: @eq (@G P) (@core (@G P) (@Join_G P) (@Sep_G P) g) (@core (@G P) (@Join_G P) (@Sep_G P) g1) *)
    subst; apply bot_identity in H0; subst.
(* Goal: @eq (@G P) (@core (@G P) (@Join_G P) (@Sep_G P) g) (@core (@G P) (@Join_G P) (@Sep_G P) g1) *)
    destruct (eq_dec t1 Share.bot); [|destruct H1; subst; auto].
    * eapply join_core; eauto.
    * rewrite join_ord_eq in H; destruct H.
(* Goal: @eq (@G P) (@core (@G P) (@Join_G P) (@Sep_G P) g) (@core (@G P) (@Join_G P) (@Sep_G P) g0) *)
      eapply join_core; eauto.
Defined.
Next Obligation.
(* Goal: hist_list' (@map_upd nat hist_el nat_eq_dec h0 (@Datatypes.length hist_el l) x) (@app hist_el l (@cons hist_el x (@nil hist_el))) *)
(* Goal: @eq (forall _ : nat, option hist_el) (@map_upd nat hist_el nat_eq_dec h0 (@Datatypes.length hist_el l) x) h *)
  constructor.
  - intros ???? [? Hjoin1] [? Hjoin2].
(* Goal: @eq (prod Share.t (@G P)) z z' *)
    assert (fst z = fst z') by (eapply join_eq; eauto).
    destruct z, z'; simpl in *; subst; f_equal.
(* Goal: @eq (@G P) g g0 *)
    destruct (eq_dec (fst x) Share.bot); [|destruct Hjoin1, Hjoin2; subst; auto].
(* Goal: @eq (@G P) g g0 *)
    destruct (eq_dec (fst y) Share.bot); [|destruct Hjoin1, Hjoin2; subst; auto].
(* Goal: @eq (@G P) g g0 *)
    eapply join_eq; eauto.
  - intros ????? [Hsh1 Hjoin1] [Hsh2 Hjoin2].
(* Goal: @sigT (prod Share.t (@G P)) (fun f : prod Share.t (@G P) => and (@join (prod Share.t (@G P)) (fun a b c : prod Share.t (@G P) => and (@join Share.t Share.Join_ba (@fst Share.t (@G P) a) (@fst Share.t (@G P) b) (@fst Share.t (@G P) c)) (if @eq_dec Share.t Share.EqDec_share (@fst Share.t (@G P) a) Share.bot then if @eq_dec Share.t Share.EqDec_share (@fst Share.t (@G P) b) Share.bot then @join (@G P) (@Join_G P) (@snd Share.t (@G P) a) (@snd Share.t (@G P) b) (@snd Share.t (@G P) c) else and (ord (@snd Share.t (@G P) a) (@snd Share.t (@G P) b)) (@eq (@G P) (@snd Share.t (@G P) c) (@snd Share.t (@G P) b)) else and (@eq (@G P) (@snd Share.t (@G P) c) (@snd Share.t (@G P) a)) (if @eq_dec Share.t Share.EqDec_share (@fst Share.t (@G P) b) Share.bot then ord (@snd Share.t (@G P) b) (@snd Share.t (@G P) a) else @eq (@G P) (@snd Share.t (@G P) c) (@snd Share.t (@G P) b)))) b c f) (@join (prod Share.t (@G P)) (fun a b c : prod Share.t (@G P) => and (@join Share.t Share.Join_ba (@fst Share.t (@G P) a) (@fst Share.t (@G P) b) (@fst Share.t (@G P) c)) (if @eq_dec Share.t Share.EqDec_share (@fst Share.t (@G P) a) Share.bot then if @eq_dec Share.t Share.EqDec_share (@fst Share.t (@G P) b) Share.bot then @join (@G P) (@Join_G P) (@snd Share.t (@G P) a) (@snd Share.t (@G P) b) (@snd Share.t (@G P) c) else and (ord (@snd Share.t (@G P) a) (@snd Share.t (@G P) b)) (@eq (@G P) (@snd Share.t (@G P) c) (@snd Share.t (@G P) b)) else and (@eq (@G P) (@snd Share.t (@G P) c) (@snd Share.t (@G P) a)) (if @eq_dec Share.t Share.EqDec_share (@fst Share.t (@G P) b) Share.bot then ord (@snd Share.t (@G P) b) (@snd Share.t (@G P) a) else @eq (@G P) (@snd Share.t (@G P) c) (@snd Share.t (@G P) b)))) a f e)) *)
    destruct (sepalg.join_assoc Hsh1 Hsh2) as [sh' []].
(* Goal: @sigT (prod Share.t (@G P)) (fun f : prod Share.t (@G P) => and (@join (prod Share.t (@G P)) (fun a b c : prod Share.t (@G P) => and (@join Share.t Share.Join_ba (@fst Share.t (@G P) a) (@fst Share.t (@G P) b) (@fst Share.t (@G P) c)) (if @eq_dec Share.t Share.EqDec_share (@fst Share.t (@G P) a) Share.bot then if @eq_dec Share.t Share.EqDec_share (@fst Share.t (@G P) b) Share.bot then @join (@G P) (@Join_G P) (@snd Share.t (@G P) a) (@snd Share.t (@G P) b) (@snd Share.t (@G P) c) else and (ord (@snd Share.t (@G P) a) (@snd Share.t (@G P) b)) (@eq (@G P) (@snd Share.t (@G P) c) (@snd Share.t (@G P) b)) else and (@eq (@G P) (@snd Share.t (@G P) c) (@snd Share.t (@G P) a)) (if @eq_dec Share.t Share.EqDec_share (@fst Share.t (@G P) b) Share.bot then ord (@snd Share.t (@G P) b) (@snd Share.t (@G P) a) else @eq (@G P) (@snd Share.t (@G P) c) (@snd Share.t (@G P) b)))) b c f) (@join (prod Share.t (@G P)) (fun a b c : prod Share.t (@G P) => and (@join Share.t Share.Join_ba (@fst Share.t (@G P) a) (@fst Share.t (@G P) b) (@fst Share.t (@G P) c)) (if @eq_dec Share.t Share.EqDec_share (@fst Share.t (@G P) a) Share.bot then if @eq_dec Share.t Share.EqDec_share (@fst Share.t (@G P) b) Share.bot then @join (@G P) (@Join_G P) (@snd Share.t (@G P) a) (@snd Share.t (@G P) b) (@snd Share.t (@G P) c) else and (ord (@snd Share.t (@G P) a) (@snd Share.t (@G P) b)) (@eq (@G P) (@snd Share.t (@G P) c) (@snd Share.t (@G P) b)) else and (@eq (@G P) (@snd Share.t (@G P) c) (@snd Share.t (@G P) a)) (if @eq_dec Share.t Share.EqDec_share (@fst Share.t (@G P) b) Share.bot then ord (@snd Share.t (@G P) b) (@snd Share.t (@G P) a) else @eq (@G P) (@snd Share.t (@G P) c) (@snd Share.t (@G P) b)))) a f e)) *)
    destruct (eq_dec (fst b) Share.bot) eqn: Hb.
    + assert (fst d = fst a) as Hd.
(* Goal: @compatible nat hist_el (@map_upd nat hist_el nat_eq_dec h2 t e) h *)
      { eapply sepalg.join_eq; eauto.
        rewrite e0; apply join_bot_eq. }
      rewrite Hd in *.
(* Goal: @sigT (prod Share.t (@G P)) (fun f : prod Share.t (@G P) => and (@join (prod Share.t (@G P)) (fun a b c : prod Share.t (@G P) => and (@join Share.t Share.Join_ba (@fst Share.t (@G P) a) (@fst Share.t (@G P) b) (@fst Share.t (@G P) c)) (if @eq_dec Share.t Share.EqDec_share (@fst Share.t (@G P) a) Share.bot then if @eq_dec Share.t Share.EqDec_share (@fst Share.t (@G P) b) Share.bot then @join (@G P) (@Join_G P) (@snd Share.t (@G P) a) (@snd Share.t (@G P) b) (@snd Share.t (@G P) c) else and (ord (@snd Share.t (@G P) a) (@snd Share.t (@G P) b)) (@eq (@G P) (@snd Share.t (@G P) c) (@snd Share.t (@G P) b)) else and (@eq (@G P) (@snd Share.t (@G P) c) (@snd Share.t (@G P) a)) (if @eq_dec Share.t Share.EqDec_share (@fst Share.t (@G P) b) Share.bot then ord (@snd Share.t (@G P) b) (@snd Share.t (@G P) a) else @eq (@G P) (@snd Share.t (@G P) c) (@snd Share.t (@G P) b)))) b c f) (@join (prod Share.t (@G P)) (fun a b c : prod Share.t (@G P) => and (@join Share.t Share.Join_ba (@fst Share.t (@G P) a) (@fst Share.t (@G P) b) (@fst Share.t (@G P) c)) (if @eq_dec Share.t Share.EqDec_share (@fst Share.t (@G P) a) Share.bot then if @eq_dec Share.t Share.EqDec_share (@fst Share.t (@G P) b) Share.bot then @join (@G P) (@Join_G P) (@snd Share.t (@G P) a) (@snd Share.t (@G P) b) (@snd Share.t (@G P) c) else and (ord (@snd Share.t (@G P) a) (@snd Share.t (@G P) b)) (@eq (@G P) (@snd Share.t (@G P) c) (@snd Share.t (@G P) b)) else and (@eq (@G P) (@snd Share.t (@G P) c) (@snd Share.t (@G P) a)) (if @eq_dec Share.t Share.EqDec_share (@fst Share.t (@G P) b) Share.bot then ord (@snd Share.t (@G P) b) (@snd Share.t (@G P) a) else @eq (@G P) (@snd Share.t (@G P) c) (@snd Share.t (@G P) b)))) a f e)) *)
      assert (sh' = fst c) as Hc.
(* Goal: @compatible nat hist_el (@map_upd nat hist_el nat_eq_dec h2 t e) h *)
      { eapply sepalg.join_eq; eauto.
        rewrite e0; apply bot_join_eq. }
      rewrite Hc in *.
(* Goal: @sigT (prod Share.t (@G P)) (fun f : prod Share.t (@G P) => and (@join (prod Share.t (@G P)) (fun a b c : prod Share.t (@G P) => and (@join Share.t Share.Join_ba (@fst Share.t (@G P) a) (@fst Share.t (@G P) b) (@fst Share.t (@G P) c)) (if @eq_dec Share.t Share.EqDec_share (@fst Share.t (@G P) a) Share.bot then if @eq_dec Share.t Share.EqDec_share (@fst Share.t (@G P) b) Share.bot then @join (@G P) (@Join_G P) (@snd Share.t (@G P) a) (@snd Share.t (@G P) b) (@snd Share.t (@G P) c) else and (ord (@snd Share.t (@G P) a) (@snd Share.t (@G P) b)) (@eq (@G P) (@snd Share.t (@G P) c) (@snd Share.t (@G P) b)) else and (@eq (@G P) (@snd Share.t (@G P) c) (@snd Share.t (@G P) a)) (if @eq_dec Share.t Share.EqDec_share (@fst Share.t (@G P) b) Share.bot then ord (@snd Share.t (@G P) b) (@snd Share.t (@G P) a) else @eq (@G P) (@snd Share.t (@G P) c) (@snd Share.t (@G P) b)))) b c f) (@join (prod Share.t (@G P)) (fun a b c : prod Share.t (@G P) => and (@join Share.t Share.Join_ba (@fst Share.t (@G P) a) (@fst Share.t (@G P) b) (@fst Share.t (@G P) c)) (if @eq_dec Share.t Share.EqDec_share (@fst Share.t (@G P) a) Share.bot then if @eq_dec Share.t Share.EqDec_share (@fst Share.t (@G P) b) Share.bot then @join (@G P) (@Join_G P) (@snd Share.t (@G P) a) (@snd Share.t (@G P) b) (@snd Share.t (@G P) c) else and (ord (@snd Share.t (@G P) a) (@snd Share.t (@G P) b)) (@eq (@G P) (@snd Share.t (@G P) c) (@snd Share.t (@G P) b)) else and (@eq (@G P) (@snd Share.t (@G P) c) (@snd Share.t (@G P) a)) (if @eq_dec Share.t Share.EqDec_share (@fst Share.t (@G P) b) Share.bot then ord (@snd Share.t (@G P) b) (@snd Share.t (@G P) a) else @eq (@G P) (@snd Share.t (@G P) c) (@snd Share.t (@G P) b)))) a f e)) *)
      destruct (eq_dec (fst c) Share.bot) eqn: Hc1.
      * destruct (eq_dec (fst a) Share.bot) eqn: Ha.
        -- destruct (join_assoc Hjoin1 Hjoin2) as [c' []].
           exists (Share.bot, c'); split; split; rewrite ?e2, ?e0, ?e1, ?eq_dec_refl in *; auto.
        -- destruct Hjoin1 as [Hc' ?]; rewrite Hc' in *.
(* Goal: @sigT (prod Share.t (@G P)) (fun f : prod Share.t (@G P) => and (@join (prod Share.t (@G P)) (fun a b c : prod Share.t (@G P) => and (@join Share.t Share.Join_ba (@fst Share.t (@G P) a) (@fst Share.t (@G P) b) (@fst Share.t (@G P) c)) (if @eq_dec Share.t Share.EqDec_share (@fst Share.t (@G P) a) Share.bot then if @eq_dec Share.t Share.EqDec_share (@fst Share.t (@G P) b) Share.bot then @join (@G P) (@Join_G P) (@snd Share.t (@G P) a) (@snd Share.t (@G P) b) (@snd Share.t (@G P) c) else and (ord (@snd Share.t (@G P) a) (@snd Share.t (@G P) b)) (@eq (@G P) (@snd Share.t (@G P) c) (@snd Share.t (@G P) b)) else and (@eq (@G P) (@snd Share.t (@G P) c) (@snd Share.t (@G P) a)) (if @eq_dec Share.t Share.EqDec_share (@fst Share.t (@G P) b) Share.bot then ord (@snd Share.t (@G P) b) (@snd Share.t (@G P) a) else @eq (@G P) (@snd Share.t (@G P) c) (@snd Share.t (@G P) b)))) b c f) (@join (prod Share.t (@G P)) (fun a b c : prod Share.t (@G P) => and (@join Share.t Share.Join_ba (@fst Share.t (@G P) a) (@fst Share.t (@G P) b) (@fst Share.t (@G P) c)) (if @eq_dec Share.t Share.EqDec_share (@fst Share.t (@G P) a) Share.bot then if @eq_dec Share.t Share.EqDec_share (@fst Share.t (@G P) b) Share.bot then @join (@G P) (@Join_G P) (@snd Share.t (@G P) a) (@snd Share.t (@G P) b) (@snd Share.t (@G P) c) else and (ord (@snd Share.t (@G P) a) (@snd Share.t (@G P) b)) (@eq (@G P) (@snd Share.t (@G P) c) (@snd Share.t (@G P) b)) else and (@eq (@G P) (@snd Share.t (@G P) c) (@snd Share.t (@G P) a)) (if @eq_dec Share.t Share.EqDec_share (@fst Share.t (@G P) b) Share.bot then ord (@snd Share.t (@G P) b) (@snd Share.t (@G P) a) else @eq (@G P) (@snd Share.t (@G P) c) (@snd Share.t (@G P) b)))) a f e)) *)
           destruct Hjoin2, (ord_lub (snd b) (snd c) (snd a)) as [c' []]; eauto.
           exists (Share.bot, c'); split; split; rewrite ?e0, ?e1, ?eq_dec_refl, ?Ha in *; auto.
      * exists c.
(* Goal: and (@join (prod Share.t (@G P)) (fun a b c : prod Share.t (@G P) => and (@join Share.t Share.Join_ba (@fst Share.t (@G P) a) (@fst Share.t (@G P) b) (@fst Share.t (@G P) c)) (if @eq_dec Share.t Share.EqDec_share (@fst Share.t (@G P) a) Share.bot then if @eq_dec Share.t Share.EqDec_share (@fst Share.t (@G P) b) Share.bot then @join (@G P) (@Join_G P) (@snd Share.t (@G P) a) (@snd Share.t (@G P) b) (@snd Share.t (@G P) c) else and (ord (@snd Share.t (@G P) a) (@snd Share.t (@G P) b)) (@eq (@G P) (@snd Share.t (@G P) c) (@snd Share.t (@G P) b)) else and (@eq (@G P) (@snd Share.t (@G P) c) (@snd Share.t (@G P) a)) (if @eq_dec Share.t Share.EqDec_share (@fst Share.t (@G P) b) Share.bot then ord (@snd Share.t (@G P) b) (@snd Share.t (@G P) a) else @eq (@G P) (@snd Share.t (@G P) c) (@snd Share.t (@G P) b)))) b c c) (@join (prod Share.t (@G P)) (fun a b c : prod Share.t (@G P) => and (@join Share.t Share.Join_ba (@fst Share.t (@G P) a) (@fst Share.t (@G P) b) (@fst Share.t (@G P) c)) (if @eq_dec Share.t Share.EqDec_share (@fst Share.t (@G P) a) Share.bot then if @eq_dec Share.t Share.EqDec_share (@fst Share.t (@G P) b) Share.bot then @join (@G P) (@Join_G P) (@snd Share.t (@G P) a) (@snd Share.t (@G P) b) (@snd Share.t (@G P) c) else and (ord (@snd Share.t (@G P) a) (@snd Share.t (@G P) b)) (@eq (@G P) (@snd Share.t (@G P) c) (@snd Share.t (@G P) b)) else and (@eq (@G P) (@snd Share.t (@G P) c) (@snd Share.t (@G P) a)) (if @eq_dec Share.t Share.EqDec_share (@fst Share.t (@G P) b) Share.bot then ord (@snd Share.t (@G P) b) (@snd Share.t (@G P) a) else @eq (@G P) (@snd Share.t (@G P) c) (@snd Share.t (@G P) b)))) a c e) *)
        destruct (eq_dec (fst a) Share.bot) eqn: Ha; try solve [split; split; auto].
        -- destruct Hjoin2.
(* Goal: and (@join (prod Share.t (@G P)) (fun a b c : prod Share.t (@G P) => and (@join Share.t Share.Join_ba (@fst Share.t (@G P) a) (@fst Share.t (@G P) b) (@fst Share.t (@G P) c)) (if @eq_dec Share.t Share.EqDec_share (@fst Share.t (@G P) a) Share.bot then if @eq_dec Share.t Share.EqDec_share (@fst Share.t (@G P) b) Share.bot then @join (@G P) (@Join_G P) (@snd Share.t (@G P) a) (@snd Share.t (@G P) b) (@snd Share.t (@G P) c) else and (ord (@snd Share.t (@G P) a) (@snd Share.t (@G P) b)) (@eq (@G P) (@snd Share.t (@G P) c) (@snd Share.t (@G P) b)) else and (@eq (@G P) (@snd Share.t (@G P) c) (@snd Share.t (@G P) a)) (if @eq_dec Share.t Share.EqDec_share (@fst Share.t (@G P) b) Share.bot then ord (@snd Share.t (@G P) b) (@snd Share.t (@G P) a) else @eq (@G P) (@snd Share.t (@G P) c) (@snd Share.t (@G P) b)))) b c c) (@join (prod Share.t (@G P)) (fun a b c : prod Share.t (@G P) => and (@join Share.t Share.Join_ba (@fst Share.t (@G P) a) (@fst Share.t (@G P) b) (@fst Share.t (@G P) c)) (if @eq_dec Share.t Share.EqDec_share (@fst Share.t (@G P) a) Share.bot then if @eq_dec Share.t Share.EqDec_share (@fst Share.t (@G P) b) Share.bot then @join (@G P) (@Join_G P) (@snd Share.t (@G P) a) (@snd Share.t (@G P) b) (@snd Share.t (@G P) c) else and (ord (@snd Share.t (@G P) a) (@snd Share.t (@G P) b)) (@eq (@G P) (@snd Share.t (@G P) c) (@snd Share.t (@G P) b)) else and (@eq (@G P) (@snd Share.t (@G P) c) (@snd Share.t (@G P) a)) (if @eq_dec Share.t Share.EqDec_share (@fst Share.t (@G P) b) Share.bot then ord (@snd Share.t (@G P) b) (@snd Share.t (@G P) a) else @eq (@G P) (@snd Share.t (@G P) c) (@snd Share.t (@G P) b)))) a c e) *)
           apply join_ord in Hjoin1; destruct Hjoin1.
(* Goal: ord v1 c *)
           split; split; rewrite ?e0, ?Ha, ?Hc1, ?eq_dec_refl; auto; split; auto; etransitivity; eauto.
        -- destruct Hjoin2 as [He1 He2]; rewrite He1, He2 in *.
           destruct Hjoin1 as [Hd' ?]; rewrite Hd' in *; split; split; rewrite ?e0, ?Ha, ?Hc1, ?eq_dec_refl, ?Hd'; auto.
(* Goal: match empty_map k with | Some v => match t k with | Some b => False | None => @eq (option B) (t k) (@Some B v) end | None => match t k with | Some v => @eq (option B) (t k) (@Some B v) | None => @eq (option B) (t k) (@None B) end end *)
    + exists (sh', snd b); simpl.
(* Goal: and (@join (prod Share.t (@G P)) (fun a b c : prod Share.t (@G P) => and (@join Share.t Share.Join_ba (@fst Share.t (@G P) a) (@fst Share.t (@G P) b) (@fst Share.t (@G P) c)) (if @eq_dec Share.t Share.EqDec_share (@fst Share.t (@G P) a) Share.bot then if @eq_dec Share.t Share.EqDec_share (@fst Share.t (@G P) b) Share.bot then @join (@G P) (@Join_G P) (@snd Share.t (@G P) a) (@snd Share.t (@G P) b) (@snd Share.t (@G P) c) else and (ord (@snd Share.t (@G P) a) (@snd Share.t (@G P) b)) (@eq (@G P) (@snd Share.t (@G P) c) (@snd Share.t (@G P) b)) else and (@eq (@G P) (@snd Share.t (@G P) c) (@snd Share.t (@G P) a)) (if @eq_dec Share.t Share.EqDec_share (@fst Share.t (@G P) b) Share.bot then ord (@snd Share.t (@G P) b) (@snd Share.t (@G P) a) else @eq (@G P) (@snd Share.t (@G P) c) (@snd Share.t (@G P) b)))) b c (@pair Share.t (@G P) sh' (@snd Share.t (@G P) b))) (@join (prod Share.t (@G P)) (fun a b c : prod Share.t (@G P) => and (@join Share.t Share.Join_ba (@fst Share.t (@G P) a) (@fst Share.t (@G P) b) (@fst Share.t (@G P) c)) (if @eq_dec Share.t Share.EqDec_share (@fst Share.t (@G P) a) Share.bot then if @eq_dec Share.t Share.EqDec_share (@fst Share.t (@G P) b) Share.bot then @join (@G P) (@Join_G P) (@snd Share.t (@G P) a) (@snd Share.t (@G P) b) (@snd Share.t (@G P) c) else and (ord (@snd Share.t (@G P) a) (@snd Share.t (@G P) b)) (@eq (@G P) (@snd Share.t (@G P) c) (@snd Share.t (@G P) b)) else and (@eq (@G P) (@snd Share.t (@G P) c) (@snd Share.t (@G P) a)) (if @eq_dec Share.t Share.EqDec_share (@fst Share.t (@G P) b) Share.bot then ord (@snd Share.t (@G P) b) (@snd Share.t (@G P) a) else @eq (@G P) (@snd Share.t (@G P) c) (@snd Share.t (@G P) b)))) a (@pair Share.t (@G P) sh' (@snd Share.t (@G P) b)) e) *)
      destruct (eq_dec (fst d) Share.bot).
(* Goal: @compatible nat hist_el (@map_upd nat hist_el nat_eq_dec h2 t e) h *)
      { rewrite e0 in Hsh1; apply join_Bot in Hsh1; destruct Hsh1; contradiction. }
(* Goal: and (@join (prod Share.t (@G P)) (fun a b c : prod Share.t (@G P) => and (@join Share.t Share.Join_ba (@fst Share.t (@G P) a) (@fst Share.t (@G P) b) (@fst Share.t (@G P) c)) (if @eq_dec Share.t Share.EqDec_share (@fst Share.t (@G P) a) Share.bot then if @eq_dec Share.t Share.EqDec_share (@fst Share.t (@G P) b) Share.bot then @join (@G P) (@Join_G P) (@snd Share.t (@G P) a) (@snd Share.t (@G P) b) (@snd Share.t (@G P) c) else and (ord (@snd Share.t (@G P) a) (@snd Share.t (@G P) b)) (@eq (@G P) (@snd Share.t (@G P) c) (@snd Share.t (@G P) b)) else and (@eq (@G P) (@snd Share.t (@G P) c) (@snd Share.t (@G P) a)) (if @eq_dec Share.t Share.EqDec_share (@fst Share.t (@G P) b) Share.bot then ord (@snd Share.t (@G P) b) (@snd Share.t (@G P) a) else @eq (@G P) (@snd Share.t (@G P) c) (@snd Share.t (@G P) b)))) b c (@pair Share.t (@G P) sh' (@snd Share.t (@G P) b))) (@join (prod Share.t (@G P)) (fun a b c : prod Share.t (@G P) => and (@join Share.t Share.Join_ba (@fst Share.t (@G P) a) (@fst Share.t (@G P) b) (@fst Share.t (@G P) c)) (if @eq_dec Share.t Share.EqDec_share (@fst Share.t (@G P) a) Share.bot then if @eq_dec Share.t Share.EqDec_share (@fst Share.t (@G P) b) Share.bot then @join (@G P) (@Join_G P) (@snd Share.t (@G P) a) (@snd Share.t (@G P) b) (@snd Share.t (@G P) c) else and (ord (@snd Share.t (@G P) a) (@snd Share.t (@G P) b)) (@eq (@G P) (@snd Share.t (@G P) c) (@snd Share.t (@G P) b)) else and (@eq (@G P) (@snd Share.t (@G P) c) (@snd Share.t (@G P) a)) (if @eq_dec Share.t Share.EqDec_share (@fst Share.t (@G P) b) Share.bot then ord (@snd Share.t (@G P) b) (@snd Share.t (@G P) a) else @eq (@G P) (@snd Share.t (@G P) c) (@snd Share.t (@G P) b)))) a (@pair Share.t (@G P) sh' (@snd Share.t (@G P) b)) e) *)
      destruct (eq_dec sh' Share.bot) eqn: Hn'.
(* Goal: @compatible nat hist_el (@map_upd nat hist_el nat_eq_dec h2 t e) h *)
      { subst; apply join_Bot in H; destruct H; contradiction. }
(* Goal: and (@join (prod Share.t (@G P)) (fun a b c : prod Share.t (@G P) => and (@join Share.t Share.Join_ba (@fst Share.t (@G P) a) (@fst Share.t (@G P) b) (@fst Share.t (@G P) c)) (if @eq_dec Share.t Share.EqDec_share (@fst Share.t (@G P) a) Share.bot then if @eq_dec Share.t Share.EqDec_share (@fst Share.t (@G P) b) Share.bot then @join (@G P) (@Join_G P) (@snd Share.t (@G P) a) (@snd Share.t (@G P) b) (@snd Share.t (@G P) c) else and (ord (@snd Share.t (@G P) a) (@snd Share.t (@G P) b)) (@eq (@G P) (@snd Share.t (@G P) c) (@snd Share.t (@G P) b)) else and (@eq (@G P) (@snd Share.t (@G P) c) (@snd Share.t (@G P) a)) (if @eq_dec Share.t Share.EqDec_share (@fst Share.t (@G P) b) Share.bot then ord (@snd Share.t (@G P) b) (@snd Share.t (@G P) a) else @eq (@G P) (@snd Share.t (@G P) c) (@snd Share.t (@G P) b)))) b c (@pair Share.t (@G P) sh' (@snd Share.t (@G P) b))) (@join (prod Share.t (@G P)) (fun a b c : prod Share.t (@G P) => and (@join Share.t Share.Join_ba (@fst Share.t (@G P) a) (@fst Share.t (@G P) b) (@fst Share.t (@G P) c)) (if @eq_dec Share.t Share.EqDec_share (@fst Share.t (@G P) a) Share.bot then if @eq_dec Share.t Share.EqDec_share (@fst Share.t (@G P) b) Share.bot then @join (@G P) (@Join_G P) (@snd Share.t (@G P) a) (@snd Share.t (@G P) b) (@snd Share.t (@G P) c) else and (ord (@snd Share.t (@G P) a) (@snd Share.t (@G P) b)) (@eq (@G P) (@snd Share.t (@G P) c) (@snd Share.t (@G P) b)) else and (@eq (@G P) (@snd Share.t (@G P) c) (@snd Share.t (@G P) a)) (if @eq_dec Share.t Share.EqDec_share (@fst Share.t (@G P) b) Share.bot then ord (@snd Share.t (@G P) b) (@snd Share.t (@G P) a) else @eq (@G P) (@snd Share.t (@G P) c) (@snd Share.t (@G P) b)))) a (@pair Share.t (@G P) sh' (@snd Share.t (@G P) b)) e) *)
      assert (snd d = snd b) as Hd by (destruct (eq_dec (fst a) Share.bot); tauto).
      destruct Hjoin2 as [He ?]; rewrite He in *; split; split; simpl; rewrite ?Hb, ?Hn', ?Hd, ?He in *; auto.
  - intros ??? []; split; [apply join_comm; auto|].
(* Goal: if @eq_dec Share.t Share.EqDec_share (@fst Share.t (@G P) b) Share.bot then if @eq_dec Share.t Share.EqDec_share (@fst Share.t (@G P) a) Share.bot then @join (@G P) (@Join_G P) (@snd Share.t (@G P) b) (@snd Share.t (@G P) a) (@snd Share.t (@G P) c) else and (ord (@snd Share.t (@G P) b) (@snd Share.t (@G P) a)) (@eq (@G P) (@snd Share.t (@G P) c) (@snd Share.t (@G P) a)) else and (@eq (@G P) (@snd Share.t (@G P) c) (@snd Share.t (@G P) b)) (if @eq_dec Share.t Share.EqDec_share (@fst Share.t (@G P) a) Share.bot then ord (@snd Share.t (@G P) a) (@snd Share.t (@G P) b) else @eq (@G P) (@snd Share.t (@G P) c) (@snd Share.t (@G P) a)) *)
    if_tac; if_tac; auto; tauto.
  - intros ???? [? Hjoin1] [? Hjoin2].
(* Goal: @eq (prod Share.t (@G P)) a b *)
    assert (fst a = fst b) by (eapply join_positivity; eauto).
    destruct (eq_dec (fst a) Share.bot), a, a', b, b'; simpl in *; subst; f_equal.
    + apply join_Bot in H0 as []; subst.
(* Goal: @eq (@G P) g g1 *)
      apply join_Bot in H as []; subst.
(* Goal: @eq (@G P) g g1 *)
      rewrite eq_dec_refl in Hjoin1, Hjoin2, Hjoin2.
(* Goal: @eq (@G P) g g1 *)
      eapply join_positivity; eauto.
    + destruct Hjoin1; auto.
Defined.
Next Obligation.
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
  auto.
Defined.

Definition ghost_snap (a : @G P) p := own p (Share.bot, a) NoneP.

Lemma ghost_snap_join : forall v1 v2 p v, join v1 v2 v ->
  ghost_snap v1 p * ghost_snap v2 p = ghost_snap v p.
Proof.
(* Goal: forall (sh1 sh2 sh : Share.t) (v : A) (p : own.gname) (_ : @join Share.t Share.Join_ba sh1 sh2 sh) (_ : not (@eq Share.t sh1 Share.bot)) (_ : not (@eq Share.t sh2 Share.bot)), @eq mpred (@sepcon mpred Nveric Sveric (ghost_var sh1 v p) (ghost_var sh2 v p)) (ghost_var sh v p) *)
  intros; symmetry; apply own_op.
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
  split; simpl; rewrite ?eq_dec_refl; auto.
Qed.

Lemma ghost_snap_conflict : forall v1 v2 p, ghost_snap v1 p * ghost_snap v2 p |-- !!(joins v1 v2).
Proof.
(* Goal: forall (v1 v2 : @G P) (p : own.gname), @derives mpred Nveric (@sepcon mpred Nveric Sveric (ghost_snap v1 p) (ghost_snap v2 p)) (@prop mpred Nveric (@joins (@G P) (@Join_G P) v1 v2)) *)
  intros; eapply derives_trans; [apply own_valid_2|].
(* Goal: @derives mpred Nveric (@prop mpred Nveric (@valid_2 snap_PCM (@pair Share.t (@G P) Share.bot v1) (@pair Share.t (@G P) Share.bot v2))) (@prop mpred Nveric (@joins (@G P) (@Join_G P) v1 v2)) *)
  apply prop_left; intros ((?, a) & (? & Hj) & _); simpl in Hj.
(* Goal: @derives mpred Nveric (@own mpred own.gname preds Nveric Sveric Bveric snap_PCM p (@pair Share.t (@G P) Share.bot g) NoneP) (@bupd mpred own.gname preds Nveric Sveric Bveric (ghost_snap v1 p)) *)
  rewrite !eq_dec_refl in Hj.
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
  apply prop_right; exists a; auto.
Qed.

Lemma ghost_snap_join' : forall v1 v2 p,
  ghost_snap v1 p * ghost_snap v2 p = EX v : _, !!(join v1 v2 v) && ghost_snap v p.
Proof.
(* Goal: @eq mpred (@exp mpred Nveric (@G map_PCM) (fun v : @G map_PCM => @andp mpred Nveric (@prop mpred Nveric (@join (@G map_PCM) (@Join_G map_PCM) m1 m2 v)) (@ghost_snap map_PCM map_incl fmap_order v p))) (@andp mpred Nveric (@prop mpred Nveric (compatible m1 m2)) (@ghost_snap map_PCM map_incl fmap_order (map_add m1 m2) p)) *)
  intros; apply pred_ext.
  - assert_PROP (joins v1 v2) as H by apply ghost_snap_conflict.
    destruct H as [v]; Exists v; entailer!.
(* Goal: @derives mpred Nveric (ghost_master Tsh v' p) (ghost_master1 v' p) *)
    erewrite ghost_snap_join; eauto.  apply derives_refl.
  - Intros v; erewrite ghost_snap_join; eauto.  apply derives_refl.
Qed.

Definition ghost_master sh (a : @G P) p := own p (sh, a) NoneP.

Lemma snap_master_join : forall v1 sh v2 p, sh <> Share.bot ->
  ghost_snap v1 p * ghost_master sh v2 p = !!(ord v1 v2) && ghost_master sh v2 p.
Proof.
(* Goal: forall (sh1 sh2 : share) (v1 v2 : A) (p : own.gname), @eq mpred (@sepcon mpred Nveric Sveric (ghost_var sh1 v1 p) (ghost_var sh2 v2 p)) (@exp mpred Nveric share (fun sh : share => @andp mpred Nveric (@prop mpred Nveric (and (@eq A v1 v2) (and (not (@eq share sh1 Share.bot)) (and (not (@eq share sh2 Share.bot)) (@join share Share.Join_ba sh1 sh2 sh))))) (ghost_var sh v1 p))) *)
  intros; setoid_rewrite own_op'.
(* Goal: @eq mpred (@exp mpred Nveric (@G map_PCM) (fun v : @G map_PCM => @andp mpred Nveric (@prop mpred Nveric (@join (@G map_PCM) (@Join_G map_PCM) m1 m2 v)) (@ghost_snap map_PCM map_incl fmap_order v p))) (@andp mpred Nveric (@prop mpred Nveric (compatible m1 m2)) (@ghost_snap map_PCM map_incl fmap_order (map_add m1 m2) p)) *)
  apply pred_ext.
  - Intros a3.
    destruct a3 as (sh', ?), H0 as [Hsh Hj]; simpl in *.
(* Goal: @derives mpred Nveric (@own mpred own.gname preds Nveric Sveric Bveric snap_PCM p (@pair Share.t (@G P) sh' g) NoneP) (@andp mpred Nveric (@prop mpred Nveric (ord v1 v2)) (ghost_master sh v2 p)) *)
    apply bot_identity in Hsh; subst sh'.
(* Goal: @valid_2 snap_PCM (@pair Share.t (@G P) Share.bot v1) (@pair Share.t (@G P) shc c) *)
    rewrite eq_dec_refl in Hj.
(* Goal: @derives mpred Nveric (@own mpred own.gname preds Nveric Sveric Bveric snap_PCM p (@pair Share.t (@G P) sh g) NoneP) (@andp mpred Nveric (@prop mpred Nveric (ord v1 v2)) (ghost_master sh v2 p)) *)
    destruct (eq_dec sh Share.bot); [contradiction|].
    destruct Hj; subst; entailer!.
  - Intros; Exists (sh, v2); entailer!.
(* Goal: @join (@G snap_PCM) (@Join_G snap_PCM) (@pair Share.t (@G P) Share.bot v1) (@pair Share.t (@G P) sh v2) (@pair Share.t (@G P) sh v2) *)
(* Goal: @derives mpred Nveric (ghost_master sh v2 p) (@own mpred own.gname preds Nveric Sveric Bveric snap_PCM p (@pair Share.t (@G P) sh v2) NoneP) *)
    split; simpl; rewrite ?eq_dec_refl.
    + apply bot_join_eq.
    + if_tac; auto; contradiction.
(* Goal: @derives mpred Nveric (ghost_master Tsh v' p) (ghost_master1 v' p) *)
    + apply derives_refl.
Qed.

Corollary snaps_master_join : forall lv sh v2 p, sh <> Share.bot ->
  fold_right sepcon emp (map (fun v => ghost_snap v p) lv) * ghost_master sh v2 p =
  !!(Forall (fun v1 => ord v1 v2) lv) && ghost_master sh v2 p.
Proof.
(* Goal: forall P Q : mpred, @derives mpred Nveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (weak_view_shift P Q) (@emp mpred Nveric Sveric)) P) (@bupd mpred own.gname preds Nveric Sveric Bveric Q) *)
  induction lv; simpl; intros.
  - rewrite emp_sepcon, prop_true_andp; auto.
  - rewrite sepcon_comm, <- sepcon_assoc, (sepcon_comm (ghost_master _ _ _)), snap_master_join by auto.
(* Goal: @eq mpred (@exp mpred Nveric (@G map_PCM) (fun v : @G map_PCM => @andp mpred Nveric (@prop mpred Nveric (@join (@G map_PCM) (@Join_G map_PCM) m1 m2 v)) (@ghost_snap map_PCM map_incl fmap_order v p))) (@andp mpred Nveric (@prop mpred Nveric (compatible m1 m2)) (@ghost_snap map_PCM map_incl fmap_order (map_add m1 m2) p)) *)
    apply pred_ext.
    + Intros; rewrite sepcon_comm, IHlv by auto; entailer!.
(* Goal: @derives mpred Nveric (@andp mpred Nveric (ghost_hist_ref sh h h' p) (@prop mpred Nveric (@valid (ref_PCM (@map_disj_PCM nat hist_el)) (@pair (option (prod share (forall _ : nat, option hist_el))) (option (forall _ : nat, option hist_el)) (@Some (prod share (forall _ : nat, option hist_el)) (@pair share (forall _ : nat, option hist_el) sh h)) (@Some (forall _ : nat, option hist_el) h'))))) (@bupd mpred own.gname preds Nveric Sveric Bveric (ghost_hist_ref sh (@map_upd nat hist_el nat_eq_dec h t' e) (@map_upd nat hist_el nat_eq_dec h' t' e) p)) *)
    + Intros.
      match goal with H : Forall _ _ |- _ => inv H end.
      rewrite prop_true_andp, sepcon_comm, IHlv by auto; entailer!.
Qed.

Lemma master_update : forall v v' p, ord v v' -> ghost_master Tsh v p |-- |==> ghost_master Tsh v' p.
Proof.
(* Goal: forall (v : A) (p : own.gname) (v' : A), @derives mpred Nveric (ghost_var Tsh v p) (@bupd mpred own.gname preds Nveric Sveric Bveric (ghost_var Tsh v' p)) *)
  intros; apply own_update.
(* Goal: @fp_update snap_PCM (@pair Share.t (@G P) Tsh v) (@pair Share.t (@G P) Tsh v') *)
  intros ? (x & Hj & _); simpl in Hj.
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
  exists (Tsh, v'); simpl; split; auto.
  destruct Hj as [Hsh Hj]; simpl in *.
  apply join_Tsh in Hsh as []; destruct c, x; simpl in *; subst.
(* Goal: match empty_map k with | Some v => match t k with | Some b => False | None => @eq (option B) (t k) (@Some B v) end | None => match t k with | Some v => @eq (option B) (t k) (@Some B v) | None => @eq (option B) (t k) (@None B) end end *)
  split; auto; simpl.
  fold share in *; destruct (eq_dec Tsh Share.bot); [contradiction Share.nontrivial|].
(* Goal: and (@eq (@G P) v' v') (if @eq_dec share Share.EqDec_share Share.bot Share.bot then ord g v' else @eq (@G P) v' g) *)
  destruct Hj as [? Hc']; subst.
  rewrite eq_dec_refl in Hc' |- *; split; auto.
(* Goal: ord v1 c *)
  etransitivity; eauto.
Qed.

Lemma master_init : forall (a : @G P), exists g', joins (Tsh, a) g'.
Proof.
(* Goal: match empty_map k with | Some v => match t k with | Some b => False | None => @eq (option B) (t k) (@Some B v) end | None => match t k with | Some v => @eq (option B) (t k) (@Some B v) | None => @eq (option B) (t k) (@None B) end end *)
  intros; exists (Share.bot, a), (Tsh, a); simpl.
(* Goal: match empty_map k with | Some v => match t k with | Some b => False | None => @eq (option B) (t k) (@Some B v) end | None => match t k with | Some v => @eq (option B) (t k) (@Some B v) | None => @eq (option B) (t k) (@None B) end end *)
  split; auto; simpl.
(* Goal: @join (@G P) (@Join_G P) a a a *)
  apply join_refl.
Qed.

Lemma make_snap : forall (sh : share) v p, ghost_master sh v p |-- |==> ghost_snap v p * ghost_master sh v p.
Proof.
(* Goal: forall (sh : share) (v : @G P) (p : own.gname), @derives mpred Nveric (ghost_master sh v p) (@bupd mpred own.gname preds Nveric Sveric Bveric (@sepcon mpred Nveric Sveric (ghost_snap v p) (ghost_master sh v p))) *)
  intros; destruct (eq_dec sh Share.bot).
  - subst; setoid_rewrite ghost_snap_join; [apply bupd_intro | apply join_refl].
  - rewrite snap_master_join by auto.
    eapply derives_trans, bupd_intro; entailer!.
Qed.

Lemma ghost_snap_forget : forall v1 v2 p, ord v1 v2 -> ghost_snap v2 p |-- |==> ghost_snap v1 p.
Proof.
(* Goal: forall (v : A) (p : own.gname) (v' : A), @derives mpred Nveric (ghost_var Tsh v p) (@bupd mpred own.gname preds Nveric Sveric Bveric (ghost_var Tsh v' p)) *)
  intros; apply own_update.
  intros (shc, c) [(shx, x) [[? Hj] _]]; simpl in *.
(* Goal: @valid_2 snap_PCM (@pair Share.t (@G P) Share.bot v1) (@pair Share.t (@G P) shc c) *)
  rewrite eq_dec_refl in Hj.
(* Goal: @valid_2 snap_PCM (@pair Share.t (@G P) Share.bot v1) (@pair Share.t (@G P) shc c) *)
  assert (shx = shc) by (eapply sepalg.join_eq; eauto); subst.
(* Goal: @valid_2 snap_PCM (@pair Share.t (@G P) Share.bot v1) (@pair Share.t (@G P) shc c) *)
  unfold share in Hj; destruct (eq_dec shc Share.bot); subst.
  - destruct (join_compat _ _ _ _ Hj H) as [x' []].
(* Goal: match empty_map k with | Some v => match t k with | Some b => False | None => @eq (option B) (t k) (@Some B v) end | None => match t k with | Some v => @eq (option B) (t k) (@Some B v) | None => @eq (option B) (t k) (@None B) end end *)
    exists (Share.bot, x'); simpl; split; auto; split; auto; simpl.
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
    rewrite !eq_dec_refl; auto.
  - destruct Hj; subst.
(* Goal: match empty_map k with | Some v => match t k with | Some b => False | None => @eq (option B) (t k) (@Some B v) end | None => match t k with | Some v => @eq (option B) (t k) (@Some B v) | None => @eq (option B) (t k) (@None B) end end *)
    exists (shc, c); simpl; split; auto; split; auto; simpl.
(* Goal: if @eq_dec Share.t Share.EqDec_share Share.bot Share.bot then if @eq_dec Share.t Share.EqDec_share shc Share.bot then @join (@G P) (@Join_G P) v1 c c else and (ord v1 c) (@eq (@G P) c c) else and (@eq (@G P) c v1) (if @eq_dec Share.t Share.EqDec_share shc Share.bot then ord c v1 else @eq (@G P) c c) *)
    rewrite eq_dec_refl; if_tac; [contradiction|].
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
    split; auto.
(* Goal: ord v1 c *)
    etransitivity; eauto.
Qed.

Lemma ghost_snap_choose : forall v1 v2 p, ghost_snap v1 p * ghost_snap v2 p |-- |==> ghost_snap v1 p.
Proof.
(* Goal: forall P Q : mpred, @derives mpred Nveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (weak_view_shift P Q) (@emp mpred Nveric Sveric)) P) (@bupd mpred own.gname preds Nveric Sveric Bveric Q) *)
  intros.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (ghost_snap v1 p) (ghost_snap v2 p)) (@bupd mpred own.gname preds Nveric Sveric Bveric (ghost_snap v1 p)) *)
  setoid_rewrite own_op'.
(* Goal: @derives mpred Nveric (@exp mpred Nveric (@G snap_PCM) (fun a3 : @G snap_PCM => @andp mpred Nveric (@prop mpred Nveric (and (@join (@G snap_PCM) (@Join_G snap_PCM) (@pair Share.t (@G P) Share.bot v1) (@pair Share.t (@G P) Share.bot v2) a3) (@valid snap_PCM a3))) (@own mpred own.gname preds Nveric Sveric Bveric snap_PCM p a3 NoneP))) (@bupd mpred own.gname preds Nveric Sveric Bveric (ghost_snap v1 p)) *)
  Intros v'.
  destruct v', H as [Hsh Hj]; apply bot_identity in Hsh; simpl in *; subst.
(* Goal: @derives mpred Nveric (@own mpred own.gname preds Nveric Sveric Bveric snap_PCM p (@pair Share.t (@G P) Share.bot g) NoneP) (@bupd mpred own.gname preds Nveric Sveric Bveric (ghost_snap v1 p)) *)
  rewrite !eq_dec_refl in Hj.
(* Goal: @derives mpred Nveric (@own mpred own.gname preds Nveric Sveric Bveric snap_PCM p (@pair Share.t (@G P) Share.bot g) NoneP) (@bupd mpred own.gname preds Nveric Sveric Bveric (ghost_snap v1 p)) *)
  apply ghost_snap_forget.
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
  rewrite join_ord_eq; eauto.
Qed.

Lemma master_share_join : forall sh1 sh2 sh v p, sepalg.join sh1 sh2 sh ->
  ghost_master sh1 v p * ghost_master sh2 v p = ghost_master sh v p.
Proof.
(* Goal: match empty_map k with | Some v => match t k with | Some b => False | None => @eq (option B) (t k) (@Some B v) end | None => match t k with | Some v => @eq (option B) (t k) (@Some B v) | None => @eq (option B) (t k) (@None B) end end *)
  intros; symmetry; apply own_op; split; auto; simpl.
(* Goal: @join (@G P) (@Join_G P) a a a *)
  if_tac; if_tac; try split; auto; try apply ord_refl; apply join_refl.
Qed.

Lemma master_inj : forall sh1 sh2 v1 v2 p, readable_share sh1 -> readable_share sh2 ->
  ghost_master sh1 v1 p * ghost_master sh2 v2 p |-- !!(v1 = v2).
Proof.
(* Goal: forall P Q : mpred, @derives mpred Nveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (weak_view_shift P Q) (@emp mpred Nveric Sveric)) P) (@bupd mpred own.gname preds Nveric Sveric Bveric Q) *)
  intros.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@own mpred own.gname preds Nveric Sveric Bveric (ref_PCM P) g (@pair (option (prod share (@G P))) (option (@G P)) (@Some (prod share (@G P)) (@pair share (@G P) sh a)) (@None (@G P))) pp) (@own mpred own.gname preds Nveric Sveric Bveric (ref_PCM P) g (@pair (option (prod share (@G P))) (option (@G P)) (@None (prod share (@G P))) (@Some (@G P) b)) pp)) (@prop mpred Nveric (if @eq_dec share Share.EqDec_share sh Tsh then @eq (@G P) a b else @ex (@G P) (fun x : @G P => @join (@G P) (@Join_G P) a x b))) *)
  eapply derives_trans; [apply own_valid_2|].
(* Goal: @derives mpred Nveric (@prop mpred Nveric (@valid_2 snap_PCM (@pair Share.t (@G P) sh1 v1) (@pair Share.t (@G P) sh2 v2))) (@prop mpred Nveric (@eq (@G P) v1 v2)) *)
  apply prop_left; intros ((?, ?) & [[? Hj] _]); simpl in Hj.
  fold share in *.
(* Goal: @derives mpred Nveric (@TT mpred Nveric) (@prop mpred Nveric (@eq (@G P) v1 v2)) *)
  destruct (eq_dec sh1 Share.bot); [subst; contradiction unreadable_bot|].
(* Goal: @derives mpred Nveric (@TT mpred Nveric) (@prop mpred Nveric (@eq (@G P) v1 v2)) *)
  destruct (eq_dec sh2 Share.bot); [subst; contradiction unreadable_bot|].
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
  destruct Hj; subst; apply prop_right; auto.
Qed.

Lemma master_share_join' : forall sh1 sh2 sh v1 v2 p, readable_share sh1 -> readable_share sh2 ->
  sepalg.join sh1 sh2 sh ->
  ghost_master sh1 v1 p * ghost_master sh2 v2 p = !!(v1 = v2) && ghost_master sh v2 p.
Proof.
(* Goal: @eq mpred (@exp mpred Nveric (@G map_PCM) (fun v : @G map_PCM => @andp mpred Nveric (@prop mpred Nveric (@join (@G map_PCM) (@Join_G map_PCM) m1 m2 v)) (@ghost_snap map_PCM map_incl fmap_order v p))) (@andp mpred Nveric (@prop mpred Nveric (compatible m1 m2)) (@ghost_snap map_PCM map_incl fmap_order (map_add m1 m2) p)) *)
  intros; apply pred_ext.
  - assert_PROP (v1 = v2) by (apply master_inj; auto).
    subst; erewrite master_share_join; eauto; entailer!.
  - Intros; subst.
(* Goal: @derives mpred Nveric (ghost_master Tsh v' p) (ghost_master1 v' p) *)
    erewrite master_share_join; eauto.  apply derives_refl.
Qed.

(* useful when we only want to deal with full masters *)
Definition ghost_master1 a p := ghost_master Tsh a p.

Lemma snap_master_join1 : forall v1 v2 p,
  ghost_snap v1 p * ghost_master1 v2 p = !!(ord v1 v2) && ghost_master1 v2 p.
Proof.
(* Goal: forall (v1 v2 : @G P) (p : own.gname), @eq mpred (@sepcon mpred Nveric Sveric (ghost_snap v1 p) (ghost_master1 v2 p)) (@andp mpred Nveric (@prop mpred Nveric (ord v1 v2)) (ghost_master1 v2 p)) *)
  intros; apply snap_master_join, Share.nontrivial.
Qed.

Lemma snap_master_update1 : forall v1 v2 p v', ord v2 v' ->
  ghost_snap v1 p * ghost_master1 v2 p |-- |==> ghost_snap v' p * ghost_master1 v' p.
Proof.
(* Goal: forall (v1 v2 : @G P) (p : own.gname) (v' : @G P) (_ : ord v2 v'), @derives mpred Nveric (@sepcon mpred Nveric Sveric (ghost_snap v1 p) (ghost_master1 v2 p)) (@bupd mpred own.gname preds Nveric Sveric Bveric (@sepcon mpred Nveric Sveric (ghost_snap v' p) (ghost_master1 v' p))) *)
  intros; rewrite !snap_master_join1.
(* Goal: @derives mpred Nveric (@andp mpred Nveric (ghost_hist_ref sh h h' p) (@prop mpred Nveric (@valid (ref_PCM (@map_disj_PCM nat hist_el)) (@pair (option (prod share (forall _ : nat, option hist_el))) (option (forall _ : nat, option hist_el)) (@Some (prod share (forall _ : nat, option hist_el)) (@pair share (forall _ : nat, option hist_el) sh h)) (@Some (forall _ : nat, option hist_el) h'))))) (@bupd mpred own.gname preds Nveric Sveric Bveric (ghost_hist_ref sh (@map_upd nat hist_el nat_eq_dec h t' e) (@map_upd nat hist_el nat_eq_dec h' t' e) p)) *)
  Intros.
(* Goal: @derives mpred Nveric (ghost_master1 v2 p) (@bupd mpred own.gname preds Nveric Sveric Bveric (@andp mpred Nveric (@prop mpred Nveric (ord v' v')) (ghost_master1 v' p))) *)
  eapply derives_trans; [apply master_update; eauto|].
  apply bupd_mono; entailer!.
(* Goal: @derives mpred Nveric (ghost_master Tsh v' p) (ghost_master1 v' p) *)
  apply derives_refl.
Qed.

End Snapshot.

Definition pos_PCM := ghost_PCM.pos_PCM.
Definition ref_PCM := ghost_PCM.ref_PCM.
Notation completable := ghost_PCM.completable.

Section Reference.

(* Goal: @compatible nat hist_el (@map_upd nat hist_el nat_eq_dec h2 t e) h *)
Context {P : Ghost}.

Definition ghost_reference g a := own(RA := ref_PCM P) g (None, Some a) NoneP.
Definition ghost_part g sh a := own(RA := ref_PCM P) g (Some (sh, a), None) NoneP.
Definition ghost_part_ref g sh a r :=
  own(RA := ref_PCM P) g (Some (sh, a), Some r) NoneP.

Lemma ghost_part_ref_join : forall g (sh : share) a b,
  ghost_part g sh a * ghost_reference g b = ghost_part_ref g sh a b.
Proof.
(* Goal: forall P Q : mpred, @derives mpred Nveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (weak_view_shift P Q) (@emp mpred Nveric Sveric)) P) (@bupd mpred own.gname preds Nveric Sveric Bveric Q) *)
  intros.
(* Goal: @eq mpred (@sepcon mpred Nveric Sveric (ghost_part g sh a) (ghost_reference g b)) (ghost_part_ref g sh a b) *)
  symmetry; apply own_op.
(* Goal: match empty_map k with | Some v => match t k with | Some b => False | None => @eq (option B) (t k) (@Some B v) end | None => match t k with | Some v => @eq (option B) (t k) (@Some B v) | None => @eq (option B) (t k) (@None B) end end *)
  hnf; simpl.
(* Goal: hist_list' (@map_upd nat hist_el nat_eq_dec h0 (@Datatypes.length hist_el l) x) (@app hist_el l (@cons hist_el x (@nil hist_el))) *)
(* Goal: @eq (forall _ : nat, option hist_el) (@map_upd nat hist_el nat_eq_dec h0 (@Datatypes.length hist_el l) x) h *)
  split; auto; constructor.
Qed.

Lemma ref_sub : forall g sh a b pp,
  own(RA := ref_PCM P) g (Some (sh, a), None) pp * own(RA := ref_PCM P) g (None, Some b) pp |--
    !!(if eq_dec sh Tsh then a = b else exists x, join a x b).
Proof.
(* Goal: forall P Q : mpred, @derives mpred Nveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (weak_view_shift P Q) (@emp mpred Nveric Sveric)) P) (@bupd mpred own.gname preds Nveric Sveric Bveric Q) *)
  intros.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@own mpred own.gname preds Nveric Sveric Bveric (ref_PCM P) g (@pair (option (prod share (@G P))) (option (@G P)) (@Some (prod share (@G P)) (@pair share (@G P) sh a)) (@None (@G P))) pp) (@own mpred own.gname preds Nveric Sveric Bveric (ref_PCM P) g (@pair (option (prod share (@G P))) (option (@G P)) (@None (prod share (@G P))) (@Some (@G P) b)) pp)) (@prop mpred Nveric (if @eq_dec share Share.EqDec_share sh Tsh then @eq (@G P) a b else @ex (@G P) (fun x : @G P => @join (@G P) (@Join_G P) a x b))) *)
  eapply derives_trans; [apply own_valid_2|].
  apply prop_left; intros (c & [Hsh Hj] & ?); simpl in *.
(* Goal: @derives mpred Nveric (@TT mpred Nveric) (@prop mpred Nveric (if @eq_dec share Share.EqDec_share sh Tsh then @eq (@G P) a b else @ex (@G P) (fun x : @G P => @join (@G P) (@Join_G P) a x b))) *)
  apply prop_right.
(* Goal: if @eq_dec share Share.EqDec_share sh Tsh then @eq (@G P) a b else @ex (@G P) (fun x : @G P => @join (@G P) (@Join_G P) a x b) *)
  destruct (fst c); [subst | contradiction].
(* Goal: if @eq_dec share Share.EqDec_share sh Tsh then @eq (@G P) a b else @ex (@G P) (fun x : @G P => @join (@G P) (@Join_G P) a x b) *)
  inv Hj.
  rewrite <- H0 in H.
(* Goal: if @eq_dec share Share.EqDec_share sh Tsh then @eq (@G P) a b else @ex (@G P) (fun x : @G P => @join (@G P) (@Join_G P) a x b) *)
  destruct H as (? & c' & Hsub).
(* Goal: if @eq_dec share Share.EqDec_share sh Tsh then @eq (@G P) a b else @ex (@G P) (fun x : @G P => @join (@G P) (@Join_G P) a x b) *)
  destruct c' as [(?, ?)|].
  - destruct Hsub as (? & ? & Hsh & ?).
(* Goal: if @eq_dec share Share.EqDec_share sh Tsh then @eq (@G P) a b else @ex (@G P) (fun x : @G P => @join (@G P) (@Join_G P) a x b) *)
    if_tac; eauto; subst.
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
    apply join_Tsh in Hsh; tauto.
  - inv Hsub.
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
    rewrite eq_dec_refl; auto.
Qed.

Lemma ref_add : forall g sh a r b a' r' pp
  (Ha : join a b a') (Hr : join r b r') (Hb : forall c, join_sub a c -> join_sub c r -> joins c b),
  own(RA := ref_PCM P) g (Some (sh, a), Some r) pp |-- |==>
  own(RA := ref_PCM P) g (Some (sh, a'), Some r') pp.
Proof.
(* Goal: forall (v : A) (p : own.gname) (v' : A), @derives mpred Nveric (ghost_var Tsh v p) (@bupd mpred own.gname preds Nveric Sveric Bveric (ghost_var Tsh v' p)) *)
  intros; apply own_update.
  intros (c, ?) ((x, ?) & [J1 J2] & [? Hvalid]); simpl in *.
  inv J2; [|contradiction].
  destruct c as [(?, c)|], x as [(shx, x)|]; try contradiction.
  - destruct J1 as (? & ? & ? & Hx).
    destruct (Hb x) as [x' Hx'].
(* Goal: @compatible nat hist_el (@map_upd nat hist_el nat_eq_dec h2 t e) h *)
    { eexists; eauto. }
(* Goal: @compatible nat hist_el (@map_upd nat hist_el nat_eq_dec h2 t e) h *)
    { destruct Hvalid as [[(?, ?)|] Hvalid]; hnf in Hvalid.
      + destruct Hvalid as (? & ? & ? & ?); eexists; eauto.
      + inv Hvalid; apply join_sub_refl. }
(* Goal: match empty_map k with | Some v => match t k with | Some b => False | None => @eq (option B) (t k) (@Some B v) end | None => match t k with | Some v => @eq (option B) (t k) (@Some B v) | None => @eq (option B) (t k) (@None B) end end *)
    exists (Some (shx, x'), Some r'); repeat (split; auto); try constructor; simpl.
    + destruct (join_assoc (join_comm Hx) Hx') as (? & ? & ?).
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
      eapply join_eq in Ha; eauto; subst; auto.
    + destruct Hvalid as (d & Hvalid); hnf in Hvalid.
      exists d; destruct d as [(shd, d)|]; hnf.
      * destruct Hvalid as (? & ? & ? & Hd); repeat (split; auto).
        destruct (join_assoc (join_comm Hd) Hr) as (? & ? & ?).
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
        eapply join_eq in Hx'; eauto; subst; auto.
      * inv Hvalid; f_equal.
(* Goal: @eq (@G P) g g0 *)
        eapply join_eq; eauto.
  - inv J1.
(* Goal: hist_list' (@map_upd nat hist_el nat_eq_dec h0 (@Datatypes.length hist_el l) x) (@app hist_el l (@cons hist_el x (@nil hist_el))) *)
(* Goal: @eq (forall _ : nat, option hist_el) (@map_upd nat hist_el nat_eq_dec h0 (@Datatypes.length hist_el l) x) h *)
    exists (Some (sh, a'), Some r'); repeat split; simpl; auto; try constructor.
    destruct Hvalid as (d & Hvalid); hnf in Hvalid.
    exists d; destruct d as [(shd, d)|]; hnf.
    + destruct Hvalid as (? & ? & ? & Hd); repeat (split; auto).
      destruct (join_assoc (join_comm Hd) Hr) as (? & ? & ?).
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
      eapply join_eq in Ha; eauto; subst; auto.
    + inv Hvalid; f_equal.
(* Goal: @eq (@G P) g g0 *)
      eapply join_eq; eauto.
Qed.

Lemma self_completable : forall a, completable (Some (Tsh, a)) a.
Proof.
(* Goal: forall a : @G P, @ghost_PCM.completable P (@Some (prod share (@G P)) (@pair share (@G P) Tsh a)) a *)
  intros; unfold completable.
(* Goal: hist_list' (@map_upd nat hist_el nat_eq_dec h0 (@Datatypes.length hist_el l) x) (@app hist_el l (@cons hist_el x (@nil hist_el))) *)
(* Goal: @eq (forall _ : nat, option hist_el) (@map_upd nat hist_el nat_eq_dec h0 (@Datatypes.length hist_el l) x) h *)
  exists None; constructor.
Qed.

End Reference.

Hint Resolve self_completable : init.

Section Discrete.

(* Goal: @compatible nat hist_el (@map_upd nat hist_el nat_eq_dec h2 t e) h *)
Program Instance discrete_PCM (A : Type) : Ghost := { valid a := True;
  Join_G := Join_equiv A }.
Next Obligation.
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
  auto.
Defined.

End Discrete.

Section GVar.

(* Goal: @compatible nat hist_el (@map_upd nat hist_el nat_eq_dec h2 t e) h *)
Context {A : Type}.

Definition ghost_var (sh : share) (v : A) g :=
  own(RA := @pos_PCM (discrete_PCM A)) g (Some (sh, v)) NoneP.

Lemma ghost_var_share_join : forall sh1 sh2 sh v p, sepalg.join sh1 sh2 sh ->
  sh1 <> Share.bot -> sh2 <> Share.bot ->
  ghost_var sh1 v p * ghost_var sh2 v p = ghost_var sh v p.
Proof.
(* Goal: forall (sh1 sh2 sh : Share.t) (v : A) (p : own.gname) (_ : @join Share.t Share.Join_ba sh1 sh2 sh) (_ : not (@eq Share.t sh1 Share.bot)) (_ : not (@eq Share.t sh2 Share.bot)), @eq mpred (@sepcon mpred Nveric Sveric (ghost_var sh1 v p) (ghost_var sh2 v p)) (ghost_var sh v p) *)
  intros; symmetry; apply own_op.
(* Goal: @join (@G (pos_PCM (discrete_PCM A))) (@Join_G (pos_PCM (discrete_PCM A))) (@Some (prod share A) (@pair share A sh1 v)) (@Some (prod share A) (@pair share A sh2 v)) (@Some (prod share A) (@pair share A sh v)) *)
  repeat (split; auto).
Qed.

Lemma ghost_var_share_join_gen : forall sh1 sh2 v1 v2 p,
  ghost_var sh1 v1 p * ghost_var sh2 v2 p = EX sh : _,
  !!(v1 = v2 /\ sh1 <> Share.bot /\ sh2 <> Share.bot /\ sepalg.join sh1 sh2 sh) && ghost_var sh v1 p.
Proof.
(* Goal: forall (sh1 sh2 : share) (v1 v2 : A) (p : own.gname), @eq mpred (@sepcon mpred Nveric Sveric (ghost_var sh1 v1 p) (ghost_var sh2 v2 p)) (@exp mpred Nveric share (fun sh : share => @andp mpred Nveric (@prop mpred Nveric (and (@eq A v1 v2) (and (not (@eq share sh1 Share.bot)) (and (not (@eq share sh2 Share.bot)) (@join share Share.Join_ba sh1 sh2 sh))))) (ghost_var sh v1 p))) *)
  intros; setoid_rewrite own_op'.
(* Goal: @eq mpred (@exp mpred Nveric (@G map_PCM) (fun v : @G map_PCM => @andp mpred Nveric (@prop mpred Nveric (@join (@G map_PCM) (@Join_G map_PCM) m1 m2 v)) (@ghost_snap map_PCM map_incl fmap_order v p))) (@andp mpred Nveric (@prop mpred Nveric (compatible m1 m2)) (@ghost_snap map_PCM map_incl fmap_order (map_add m1 m2) p)) *)
  apply pred_ext.
  - Intros a.
(* Goal: @derives mpred Nveric (@own mpred own.gname preds Nveric Sveric Bveric (pos_PCM (discrete_PCM A)) p a NoneP) (@exp mpred Nveric share (fun sh : share => @andp mpred Nveric (@prop mpred Nveric (and (@eq A v1 v2) (and (not (@eq share sh1 Share.bot)) (and (not (@eq share sh2 Share.bot)) (@join share Share.Join_ba sh1 sh2 sh))))) (ghost_var sh v1 p))) *)
    destruct a as [(sh, v')|]; inv H.
(* Goal: @derives mpred Nveric (@own mpred own.gname preds Nveric Sveric Bveric (pos_PCM (discrete_PCM A)) p (@Some (prod share (@G (discrete_PCM A))) (@pair share (@G (discrete_PCM A)) sh v')) NoneP) (@exp mpred Nveric share (fun sh : share => @andp mpred Nveric (@prop mpred Nveric (and (@eq A v1 v2) (and (not (@eq share sh1 Share.bot)) (and (not (@eq share sh2 Share.bot)) (@join share Share.Join_ba sh1 sh2 sh))))) (ghost_var sh v1 p))) *)
    destruct H2 as (? & ? & Hv); inv Hv.
    Exists sh; entailer!.
  - Intros sh; subst.
(* Goal: @derives mpred Nveric (ghost_var sh v2 p) (@exp mpred Nveric (@G (pos_PCM (discrete_PCM A))) (fun a3 : @G (pos_PCM (discrete_PCM A)) => @andp mpred Nveric (@prop mpred Nveric (and (@join (@G (pos_PCM (discrete_PCM A))) (@Join_G (pos_PCM (discrete_PCM A))) (@Some (prod share A) (@pair share A sh1 v2)) (@Some (prod share A) (@pair share A sh2 v2)) a3) (@valid (pos_PCM (discrete_PCM A)) a3))) (@own mpred own.gname preds Nveric Sveric Bveric (pos_PCM (discrete_PCM A)) p a3 NoneP))) *)
    Exists (Some (sh, v2)); apply andp_right, derives_refl.
(* Goal: match empty_map k with | Some v => match t k with | Some b => False | None => @eq (option B) (t k) (@Some B v) end | None => match t k with | Some v => @eq (option B) (t k) (@Some B v) | None => @eq (option B) (t k) (@None B) end end *)
    apply prop_right; repeat (split; auto); simpl.
(* Goal: not (@eq share sh Share.bot) *)
    intro; subst; apply join_Bot in H2 as []; contradiction.
Qed.

Lemma ghost_var_inj : forall sh1 sh2 v1 v2 p, sh1 <> Share.bot -> sh2 <> Share.bot ->
  ghost_var sh1 v1 p * ghost_var sh2 v2 p |-- !!(v1 = v2).
Proof.
  intros; rewrite ghost_var_share_join_gen; Intros sh; entailer!.
Qed.

Lemma ghost_var_share_join' : forall sh1 sh2 sh v1 v2 p, sh1 <> Share.bot -> sh2 <> Share.bot ->
  sepalg.join sh1 sh2 sh ->
  ghost_var sh1 v1 p * ghost_var sh2 v2 p = !!(v1 = v2) && ghost_var sh v2 p.
Proof.
(* Goal: forall (sh1 sh2 sh : Share.t) (v1 v2 : A) (p : own.gname) (_ : not (@eq Share.t sh1 Share.bot)) (_ : not (@eq Share.t sh2 Share.bot)) (_ : @join Share.t Share.Join_ba sh1 sh2 sh), @eq mpred (@sepcon mpred Nveric Sveric (ghost_var sh1 v1 p) (ghost_var sh2 v2 p)) (@andp mpred Nveric (@prop mpred Nveric (@eq A v1 v2)) (ghost_var sh v2 p)) *)
  intros; rewrite ghost_var_share_join_gen.
(* Goal: @eq mpred (@exp mpred Nveric (@G map_PCM) (fun v : @G map_PCM => @andp mpred Nveric (@prop mpred Nveric (@join (@G map_PCM) (@Join_G map_PCM) m1 m2 v)) (@ghost_snap map_PCM map_incl fmap_order v p))) (@andp mpred Nveric (@prop mpred Nveric (compatible m1 m2)) (@ghost_snap map_PCM map_incl fmap_order (map_add m1 m2) p)) *)
  apply pred_ext.
  - Intros sh'; entailer!.
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
    eapply join_eq in H1; eauto; subst; auto.
  - Intros; Exists sh; entailer!.
Qed.

Lemma ghost_var_update : forall v p v', ghost_var Tsh v p |-- |==> ghost_var Tsh v' p.
Proof.
(* Goal: forall (v : A) (p : own.gname) (v' : A), @derives mpred Nveric (ghost_var Tsh v p) (@bupd mpred own.gname preds Nveric Sveric Bveric (ghost_var Tsh v' p)) *)
  intros; apply own_update.
(* Goal: @fp_update (pos_PCM (discrete_PCM A)) (@Some (prod share A) (@pair share A Tsh v)) (@Some (prod share A) (@pair share A Tsh v')) *)
  intros [[]|] ([[]|] & J & ?); inv J.
  - destruct H1 as (? & ?%join_Tsh & ?); tauto.
  - exists (Some (Tsh, v')); split; [constructor | auto].
Qed.

(*Lemma ghost_var_precise : forall sh p, precise (EX v : A, ghost_var sh v p).
Proof.
  intros; apply derives_precise' with (EX g : share * A, ghost g p), ex_ghost_precise.
(* Goal: @derives mpred Nveric (ghost_master Tsh v' p) (ghost_master1 v' p) *)
  Intro v; Exists (sh, v); auto.  apply derives_refl.
Qed.

Lemma ghost_var_precise' : forall sh v p, precise (ghost_var sh v p).
Proof.
  intros; apply derives_precise with (Q := EX v : A, ghost_var sh v p);
    [exists v; auto | apply ghost_var_precise].
Qed.*)

End GVar.

Section PVar.
(* Like ghost variables, but the partial values may be out of date. *)

(* Goal: @compatible nat hist_el (@map_upd nat hist_el nat_eq_dec h2 t e) h *)
Global Program Instance nat_PCM: Ghost := { valid a := True; Join_G a b c := c = Nat.max a b }.
Next Obligation.
(* Goal: forall P Q : mpred, @derives mpred Nveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (weak_view_shift P Q) (@emp mpred Nveric Sveric)) P) (@bupd mpred own.gname preds Nveric Sveric Bveric Q) *)
  exists (fun _ => O); auto; intros.
(* Goal: @unit_for nat (fun a b c : nat => @eq nat c (Nat.max a b)) O t *)
  apply Nat.max_0_l.
Defined.
Next Obligation.
(* Goal: hist_list' (@map_upd nat hist_el nat_eq_dec h0 (@Datatypes.length hist_el l) x) (@app hist_el l (@cons hist_el x (@nil hist_el))) *)
(* Goal: @eq (forall _ : nat, option hist_el) (@map_upd nat hist_el nat_eq_dec h0 (@Datatypes.length hist_el l) x) h *)
  constructor.
  - unfold join; congruence.
  - unfold join; eexists; split; eauto.
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
    rewrite Nat.max_assoc; subst; auto.
(* Goal: forall P Q : mpred, @derives mpred Nveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (weak_view_shift P Q) (@emp mpred Nveric Sveric)) P) (@bupd mpred own.gname preds Nveric Sveric Bveric Q) *)
  - unfold join; intros.
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
    rewrite Nat.max_comm; auto.
(* Goal: forall P Q : mpred, @derives mpred Nveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (weak_view_shift P Q) (@emp mpred Nveric Sveric)) P) (@bupd mpred own.gname preds Nveric Sveric Bveric Q) *)
  - unfold join; intros.
(* Goal: @eq nat a b *)
    apply Nat.le_antisymm; [subst b | subst a]; apply Nat.le_max_l.
Defined.
Next Obligation.
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
  auto.
Defined.

Global Instance max_order : PCM_order le.
Proof.
(* Goal: forall P Q : mpred, @derives mpred Nveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (weak_view_shift P Q) (@emp mpred Nveric Sveric)) P) (@bupd mpred own.gname preds Nveric Sveric Bveric Q) *)
  constructor; auto; intros.
  - intros ???; omega.
  - eexists; unfold join; simpl; split; eauto.
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
    apply Nat.max_lub; auto.
  - hnf in H; subst.
(* Goal: and (le a (Nat.max a b)) (le b (Nat.max a b)) *)
    split; [apply Nat.le_max_l | apply Nat.le_max_r].
  - hnf.
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
    rewrite Nat.max_l; auto.
Defined.

Lemma ghost_snap_join_N : forall v1 v2 p, ghost_snap v1 p * ghost_snap v2 p = ghost_snap (Nat.max v1 v2) p.
Proof.
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
  intros; apply ghost_snap_join; hnf; auto.
Qed.

Lemma snap_master_join' : forall v1 v2 p,
  ghost_snap v1 p * ghost_master1 v2 p = !!(v1 <= v2)%nat && ghost_master1 v2 p.
Proof.
(* Goal: forall (v1 v2 : @G nat_PCM) (p : own.gname), @eq mpred (@sepcon mpred Nveric Sveric (@ghost_snap nat_PCM le max_order v1 p) (@ghost_master1 nat_PCM le max_order v2 p)) (@andp mpred Nveric (@prop mpred Nveric (le v1 v2)) (@ghost_master1 nat_PCM le max_order v2 p)) *)
  intros; apply snap_master_join1.
Qed.

Lemma snap_master_update' : forall (v1 v2 : nat) p v', (v2 <= v')%nat ->
  ghost_snap v1 p * ghost_master1 v2 p |-- |==> ghost_snap v' p * ghost_master1 v' p.
Proof.
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
  intros; apply snap_master_update1; auto.
Qed.

End PVar.

Section Maps.

(* Goal: @compatible nat hist_el (@map_upd nat hist_el nat_eq_dec h2 t e) h *)
Context {A B : Type} {A_eq : EqDec A}.

Implicit Types (k : A) (v : B) (m : A -> option B).

Definition map_upd m k v k' := if eq_dec k' k then Some v else m k'.

Lemma map_upd_triv : forall m k v, m k = Some v -> map_upd m k v = m.
Proof.
(* Goal: forall (m : forall _ : A, option B) (k : A) (v : B) (_ : @eq (option B) (m k) (@Some B v)), @eq (forall _ : A, option B) (map_upd m k v) m *)
  intros; extensionality; unfold map_upd.
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
  if_tac; subst; auto.
Qed.

Fixpoint map_upd_list m l :=
  match l with
  | [] => m
  | (k, v) :: rest => map_upd_list (map_upd m k v) rest
  end.

Definition map_add m1 m2 k := match m1 k with Some v' => Some v' | None => m2 k end.

Definition empty_map k : option B := None.

Global Instance Inhabitant_map : Inhabitant (A -> option B) := empty_map.

Definition singleton k v k1 := if eq_dec k1 k then Some v else None.

Definition map_incl m1 m2 := forall k v, m1 k = Some v -> m2 k = Some v.

Global Instance map_incl_refl : Reflexive map_incl.
Proof.
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
  repeat intro; auto.
Qed.

Global Instance map_incl_antisym : Antisymmetric _ _ map_incl.
Proof.
(* Goal: @Antisymmetric (forall _ : A, option B) (@pointwise_relation A (option B) (@eq (option B))) (@Equivalence.pointwise_equivalence A (option B) (@eq (option B)) (@eq_equivalence (option B))) map_incl *)
  intros x y Hx Hy a.
(* Goal: @eq (option B) (x a) (y a) *)
  specialize (Hx a); specialize (Hy a).
(* Goal: @eq (option B) (x a) (y a) *)
  destruct (x a); [erewrite Hx; eauto|].
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
  destruct (y a); auto.
Qed.

Global Instance map_incl_trans : Transitive map_incl.
Proof.
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
  repeat intro; auto.
Qed.

Lemma map_add_incl_compat : forall m1 m2 m3, map_incl m1 m2 -> map_incl (map_add m3 m1) (map_add m3 m2).
Proof.
(* Goal: forall (m1 m2 m3 : forall _ : A, option B) (_ : map_incl m1 m2), map_incl (map_add m3 m1) (map_add m3 m2) *)
  unfold map_add; repeat intro.
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
  destruct (m3 k); auto.
Qed.

Definition compatible m1 m2 := forall k v1 v2, m1 k = Some v1 -> m2 k = Some v2 -> v1 = v2.

Global Instance compatible_refl : Reflexive compatible.
Proof.
(* Goal: forall (P Q : mpred) (n : nat), @eq (@pred rmap ag_rmap) (approx n (weak_view_shift P Q)) (approx n (weak_view_shift P (approx n Q))) *)
  repeat intro.
(* Goal: @eq B v1 v2 *)
  congruence.
Qed.

Global Instance compatible_comm : Symmetric compatible.
Proof.
(* Goal: forall (P Q : mpred) (n : nat), @eq (@pred rmap ag_rmap) (approx n (weak_view_shift P Q)) (approx n (weak_view_shift P (approx n Q))) *)
  repeat intro.
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
  symmetry; eauto.
Qed.

Lemma map_add_comm : forall m1 m2, compatible m1 m2 -> map_add m1 m2 = map_add m2 m1.
Proof.
(* Goal: forall (m1 m2 : forall _ : A, option B) (_ : compatible m1 m2), @eq (forall _ : A, option B) (map_add m1 m2) (map_add m2 m1) *)
  intros; extensionality x; unfold map_add.
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
  destruct (m1 x) eqn: Hm1, (m2 x) eqn: Hm2; eauto.
Qed.

Lemma map_add_assoc : forall m1 m2 m3, map_add (map_add m1 m2) m3 = map_add m1 (map_add m2 m3).
Proof.
(* Goal: forall m1 m2 m3 : forall _ : A, option B, @eq (forall _ : A, option B) (map_add (map_add m1 m2) m3) (map_add m1 (map_add m2 m3)) *)
  intros; extensionality; unfold map_add.
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
  destruct (m1 x); auto.
Qed.

Lemma compatible_add_assoc : forall m1 m2 m3, compatible m1 m2 ->
  compatible (map_add m1 m2) m3 -> compatible m1 (map_add m2 m3).
Proof.
(* Goal: forall P Q : mpred, @derives mpred Nveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (weak_view_shift P Q) (@emp mpred Nveric Sveric)) P) (@bupd mpred own.gname preds Nveric Sveric Bveric Q) *)
  unfold compatible, map_add; intros.
  repeat match goal with H : forall _, _ |- _ => specialize (H k) end.
  replace (m1 k) with (Some v1) in *.
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
  destruct (m2 k); auto.
Qed.

Lemma compatible_incl : forall m1 m2 m (Hcompat : compatible m2 m) (Hincl : map_incl m1 m2), compatible m1 m.
Proof.
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
  repeat intro; eauto.
Qed.

Lemma map_incl_add : forall m1 m2, map_incl m1 (map_add m1 m2).
Proof.
(* Goal: forall m1 m2 : forall _ : A, option B, map_incl m1 (map_add m1 m2) *)
  repeat intro; unfold map_add.
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
  rewrite H; auto.
Qed.

Lemma map_incl_compatible : forall m1 m2 m3 (Hincl1 : map_incl m1 m3) (Hincl2 : map_incl m2 m3),
  compatible m1 m2.
Proof.
(* Goal: forall (m1 m2 : forall _ : A, option B) (_ : map_incl m1 m2), compatible m1 m2 *)
  intros; intros ??? Hk1 Hk2.
(* Goal: @eq B v1 v2 *)
  apply Hincl1 in Hk1; apply Hincl2 in Hk2.
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
  rewrite Hk1 in Hk2; inv Hk2; auto.
Qed.

Lemma map_add_incl : forall m1 m2 m3, map_incl m1 m3 -> map_incl m2 m3 -> map_incl (map_add m1 m2) m3.
Proof.
(* Goal: forall P Q : mpred, @derives mpred Nveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (weak_view_shift P Q) (@emp mpred Nveric Sveric)) P) (@bupd mpred own.gname preds Nveric Sveric Bveric Q) *)
  unfold map_add; intros.
(* Goal: map_incl (fun k : A => match m1 k with | Some v' => @Some B v' | None => m2 k end) m3 *)
  intros ?? Hk.
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
  destruct (m1 k) eqn: Hk1; auto.
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
  inv Hk; auto.
Qed.

Global Instance map_join : Join (A -> option B) :=
  fun a b c => forall k v, c k = Some v <-> a k = Some v \/ b k = Some v.

Lemma map_join_spec : forall m1 m2 m3, join m1 m2 m3 <-> compatible m1 m2 /\ m3 = map_add m1 m2.
Proof.
(* Goal: forall P Q : mpred, @derives mpred Nveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (weak_view_shift P Q) (@emp mpred Nveric Sveric)) P) (@bupd mpred own.gname preds Nveric Sveric Bveric Q) *)
  unfold join, map_join; simpl; split; intros.
  - split.
    + repeat intro.
(* Goal: @eq B v1 v2 *)
      assert (m3 k = Some v1) as Hk by (rewrite H; auto).
(* Goal: @eq B v1 v2 *)
      replace (m3 k) with (Some v2) in Hk by (symmetry; rewrite H; auto).
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
      inv Hk; auto.
    + extensionality x; unfold map_add.
(* Goal: @eq (option B) (m3 x) match m1 x with | Some v' => @Some B v' | None => m2 x end *)
      destruct (m1 x) eqn: Hm1; [rewrite H; auto|].
(* Goal: @eq (option B) (m3 x) (m2 x) *)
      destruct (m2 x) eqn: Hm2; [rewrite H; auto|].
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
      destruct (m3 x) eqn: Hm3; auto.
      rewrite H in Hm3; destruct Hm3 as [Hm3 | Hm3]; rewrite Hm3 in *; discriminate.
  - destruct H as [Hcompat]; subst; unfold map_add.
(* Goal: iff (@eq (option B) match m1 k with | Some v' => @Some B v' | None => m2 k end (@Some B v)) (or (@eq (option B) (m1 k) (@Some B v)) (@eq (option B) (m2 k) (@Some B v))) *)
    destruct (m1 k) eqn: Hm1; split; auto; intros [?|?]; eauto; discriminate.
Qed.

(* Goal: @compatible nat hist_el (@map_upd nat hist_el nat_eq_dec h2 t e) h *)
Global Program Instance map_PCM : Ghost := { valid a := True; Join_G := map_join }.
Next Obligation.
(* Goal: forall (P Q : mpred) (n : nat), @eq (@pred rmap ag_rmap) (approx n (weak_view_shift P Q)) (approx n (weak_view_shift P (approx n Q))) *)
  exists (fun _ => empty_map); auto; repeat intro.
(* Goal: iff (@eq (option B) (t k) (@Some B v)) (or (@eq (option B) (empty_map k) (@Some B v)) (@eq (option B) (t k) (@Some B v))) *)
  split; auto; intros [|]; auto; discriminate.
Defined.
Next Obligation.
(* Goal: hist_list' (@map_upd nat hist_el nat_eq_dec h0 (@Datatypes.length hist_el l) x) (@app hist_el l (@cons hist_el x (@nil hist_el))) *)
(* Goal: @eq (forall _ : nat, option hist_el) (@map_upd nat hist_el nat_eq_dec h0 (@Datatypes.length hist_el l) x) h *)
  constructor.
(* Goal: forall P Q : mpred, @derives mpred Nveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (weak_view_shift P Q) (@emp mpred Nveric Sveric)) P) (@bupd mpred own.gname preds Nveric Sveric Bveric Q) *)
  - intros.
(* Goal: @eq (forall _ : A, option B) z z' *)
    extensionality k.
(* Goal: @eq (option B) (z k) (z' k) *)
    specialize (H k); specialize (H0 k).
(* Goal: @eq (option B) (z k) (z' k) *)
    destruct (z k).
    + destruct (H b) as [X _]; specialize (X eq_refl).
      rewrite <- H0 in X; auto.
    + destruct (z' k); auto.
(* Goal: @eq (option B) (@None B) (@Some B b) *)
      destruct (H0 b) as [X _]; specialize (X eq_refl).
      rewrite <- H in X; auto.
(* Goal: forall P Q : mpred, @derives mpred Nveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (weak_view_shift P Q) (@emp mpred Nveric Sveric)) P) (@bupd mpred own.gname preds Nveric Sveric Bveric Q) *)
  - intros.
    rewrite map_join_spec in *.
(* Goal: @sigT (forall _ : A, option B) (fun f : forall _ : A, option B => and (@join (forall _ : A, option B) map_disj_join b c f) (@join (forall _ : A, option B) map_disj_join a f e)) *)
    destruct H, H0; subst.
(* Goal: @sigT (forall _ : A, option B) (fun f : forall _ : A, option B => and (@join (forall _ : A, option B) map_disj_join b c f) (@join (forall _ : A, option B) map_disj_join a f (map_add (map_add a b) c))) *)
    rewrite map_add_assoc.
(* Goal: and (not (@eq share (Share.comp sh) Share.bot)) (and (@join share Share.Join_ba sh (Share.comp sh) Tsh) (@join (forall _ : nat, option hist_el) (@map_disj_join nat hist_el) h h' hr)) *)
    eexists; rewrite !map_join_spec; repeat split.
    + eapply compatible_incl; eauto.
(* Goal: map_incl b (map_add a b) *)
      rewrite map_add_comm by auto; apply map_incl_add.
    + apply compatible_add_assoc; auto.
  - intros ???; rewrite !map_join_spec; intros []; subst.
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
    split; [symmetry | apply map_add_comm]; auto.
(* Goal: forall P Q : mpred, @derives mpred Nveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (weak_view_shift P Q) (@emp mpred Nveric Sveric)) P) (@bupd mpred own.gname preds Nveric Sveric Bveric Q) *)
  - intros.
(* Goal: @eq (option B) (z k) (z' k) *)
    extensionality k; specialize (H k); specialize (H0 k).
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
    destruct (a k), (b k); auto.
    + apply H0; auto.
    + destruct (H b0) as [_ H']; lapply H'; auto.
    + destruct (H0 b0) as [_ H']; lapply H'; auto.
Defined.
Next Obligation.
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
  auto.
Defined.

Instance fmap_order : PCM_order map_incl.
Proof.
(* Goal: hist_list' (@map_upd nat hist_el nat_eq_dec h0 (@Datatypes.length hist_el l) x) (@app hist_el l (@cons hist_el x (@nil hist_el))) *)
(* Goal: @eq (forall _ : nat, option hist_el) (@map_upd nat hist_el nat_eq_dec h0 (@Datatypes.length hist_el l) x) h *)
  constructor.
  - apply map_incl_refl.
  - apply map_incl_trans.
  - intros ??? Ha Hb; exists (map_add a b); split; simpl.
    + rewrite map_join_spec; split; auto.
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
      eapply map_incl_compatible; eauto.
    + apply map_add_incl; auto.
  - split; repeat intro; specialize (H k v); rewrite H; auto.
  - split; auto; intros [|]; auto.
Defined.

Lemma map_snap_join : forall m1 m2 p,
  ghost_snap m1 p * ghost_snap m2 p = !!(compatible m1 m2) && ghost_snap (map_add m1 m2) p.
Proof.
(* Goal: forall (m1 m2 : forall _ : A, option B) (p : own.gname), @eq mpred (@sepcon mpred Nveric Sveric (@ghost_snap map_PCM map_incl fmap_order m1 p) (@ghost_snap map_PCM map_incl fmap_order m2 p)) (@andp mpred Nveric (@prop mpred Nveric (compatible m1 m2)) (@ghost_snap map_PCM map_incl fmap_order (map_add m1 m2) p)) *)
  intros; rewrite ghost_snap_join'.
(* Goal: @eq mpred (@exp mpred Nveric (@G map_PCM) (fun v : @G map_PCM => @andp mpred Nveric (@prop mpred Nveric (@join (@G map_PCM) (@Join_G map_PCM) m1 m2 v)) (@ghost_snap map_PCM map_incl fmap_order v p))) (@andp mpred Nveric (@prop mpred Nveric (compatible m1 m2)) (@ghost_snap map_PCM map_incl fmap_order (map_add m1 m2) p)) *)
  apply pred_ext.
  - Intros m.
    rewrite map_join_spec in H; destruct H; subst; entailer!.
  - Intros; Exists (map_add m1 m2).
    rewrite map_join_spec; entailer!.
Qed.

Lemma map_upd_list_app : forall l1 l2 m, map_upd_list m (l1 ++ l2) = map_upd_list (map_upd_list m l1) l2.
Proof.
(* Goal: forall P Q : mpred, @derives mpred Nveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (weak_view_shift P Q) (@emp mpred Nveric Sveric)) P) (@bupd mpred own.gname preds Nveric Sveric Bveric Q) *)
  induction l1; auto; simpl; intros.
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
  destruct a; auto.
Qed.

Lemma map_upd_list_out : forall l m k, m k = None -> ~In k (map fst l) -> map_upd_list m l k = None.
Proof.
(* Goal: forall P Q : mpred, @derives mpred Nveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (weak_view_shift P Q) (@emp mpred Nveric Sveric)) P) (@bupd mpred own.gname preds Nveric Sveric Bveric Q) *)
  induction l; auto; simpl; intros.
(* Goal: @eq (option B) ((let (k, v) := a in map_upd_list (map_upd m k v) l) k) (@None B) *)
  destruct a; apply IHl.
  - unfold map_upd; if_tac; auto.
    subst; simpl in *; tauto.
  - tauto.
Qed.

Lemma compatible_k : forall m1 m2 (Hcompat : compatible m1 m2) k v, m2 k = Some v -> map_add m1 m2 k = Some v.
Proof.
(* Goal: forall P Q : mpred, @derives mpred Nveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (weak_view_shift P Q) (@emp mpred Nveric Sveric)) P) (@bupd mpred own.gname preds Nveric Sveric Bveric Q) *)
  unfold compatible; intros.
(* Goal: not (@eq (option hist_el) (@map_add nat hist_el h h2 t') (@None hist_el)) *)
  unfold map_add.
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
  destruct (m1 k) eqn: Hk; eauto.
Qed.

Lemma map_join_incl_compat : forall m1 m2 m' m'' (Hincl : map_incl m1 m2) (Hjoin : join m2 m' m''),
  exists m, join m1 m' m /\ map_incl m m''.
Proof.
(* Goal: forall (m1 m2 m' m'' : forall _ : A, option B) (_ : map_incl m1 m2) (_ : @join (forall _ : A, option B) map_join m2 m' m''), @ex (forall _ : A, option B) (fun m : forall _ : A, option B => and (@join (forall _ : A, option B) map_join m1 m' m) (map_incl m m'')) *)
  intros; apply (@join_comm _ _ (@Perm_G map_PCM)) in Hjoin.
(* Goal: @ex (forall _ : A, option B) (fun m : forall _ : A, option B => and (@join (forall _ : A, option B) map_join m1 m' m) (map_incl m m'')) *)
  rewrite map_join_spec in Hjoin; destruct Hjoin as [Hjoin]; subst.
(* Goal: @ex (forall _ : A, option B) (fun m : forall _ : A, option B => and (@join (forall _ : A, option B) map_join m1 m' m) (map_incl m (map_add m' m2))) *)
  do 2 eexists; [|apply map_add_incl_compat; eauto].
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
  symmetry in Hjoin; eapply compatible_incl in Hjoin; eauto.
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
  rewrite map_join_spec; split; auto.
  rewrite <- map_add_comm; auto.
Qed.

Lemma map_add_empty : forall m, map_add m empty_map = m.
Proof.
(* Goal: forall m : forall _ : A, option B, @eq (forall _ : A, option B) (map_add m empty_map) m *)
  intros; extensionality; unfold map_add, empty_map.
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
  destruct (m x); auto.
Qed.

Lemma map_upd_incl : forall m1 m2 k v, map_incl m1 m2 ->
  m2 k = Some v -> map_incl (map_upd m1 k v) m2.
Proof.
(* Goal: forall (P Q : mpred) (n : nat), @eq (@pred rmap ag_rmap) (approx n (weak_view_shift P Q)) (approx n (weak_view_shift P (approx n Q))) *)
  unfold map_upd; repeat intro.
(* Goal: @eq (option B) (m2 k0) (@Some B v0) *)
  destruct (eq_dec k0 k); [congruence | auto].
Qed.

Lemma map_add_single : forall m k v, map_add (singleton k v) m = map_upd m k v.
Proof.
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
  intros; extensionality; unfold map_add, singleton, map_upd; if_tac; auto.
Qed.

Lemma incl_compatible : forall m1 m2, map_incl m1 m2 -> compatible m1 m2.
Proof.
(* Goal: forall (m1 m2 : forall _ : A, option B) (_ : map_incl m1 m2), compatible m1 m2 *)
  intros; intros ??? Hk1 Hk2.
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
  specialize (H _ _ Hk1); rewrite H in Hk2; inv Hk2; auto.
Qed.

Lemma map_add_redundant : forall m1 m2, map_incl m1 m2 -> map_add m1 m2 = m2.
Proof.
(* Goal: @eq (forall _ : A, option B) z z' *)
  intros; unfold map_add; extensionality k.
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
  destruct (m1 k) eqn: Hk; auto; symmetry; auto.
Qed.

Lemma empty_map_incl : forall m, map_incl empty_map m.
Proof.
(* Goal: forall h : list hist_el, hist_incl (@empty_map nat hist_el) h *)
  repeat intro; discriminate.
Qed.

Lemma map_upd2_incl : forall m1 m2 k v, map_incl m1 m2 -> map_incl (map_upd m1 k v) (map_upd m2 k v).
Proof.
(* Goal: forall (P Q : mpred) (n : nat), @eq (@pred rmap ag_rmap) (approx n (weak_view_shift P Q)) (approx n (weak_view_shift P (approx n Q))) *)
  unfold map_upd; repeat intro.
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
  if_tac; auto.
Qed.

Lemma compatible_upd : forall m1 m2 k v, compatible m1 m2 -> m2 k = None ->
  compatible (map_upd m1 k v) m2.
Proof.
(* Goal: forall (P Q : mpred) (n : nat), @eq (@pred rmap ag_rmap) (approx n (weak_view_shift P Q)) (approx n (weak_view_shift P (approx n Q))) *)
  unfold map_upd; repeat intro.
(* Goal: @eq B v1 v2 *)
  destruct (eq_dec k0 k); eauto; congruence.
Qed.

Lemma map_add_upd : forall m1 m2 k v, map_upd (map_add m1 m2) k v = map_add (map_upd m1 k v) m2.
Proof.
(* Goal: forall P Q : mpred, @derives mpred Nveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (weak_view_shift P Q) (@emp mpred Nveric Sveric)) P) (@bupd mpred own.gname preds Nveric Sveric Bveric Q) *)
  intros.
  rewrite <- !map_add_single.
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
  rewrite map_add_assoc; auto.
Qed.

Notation maps_add l := (fold_right map_add empty_map l).

Lemma in_maps_add : forall l (k : A) (v : B), maps_add l k = Some v -> exists m, In m l /\ m k = Some v.
Proof.
(* Goal: forall (l : list (forall _ : A, option B)) (k : A) (v : B) (_ : @eq (option B) (@fold_right (forall _ : A, option B) (forall _ : A, option B) map_add empty_map l k) (@Some B v)), @ex (forall _ : A, option B) (fun m : forall _ : A, option B => and (@In (forall _ : A, option B) m l) (@eq (option B) (m k) (@Some B v))) *)
  induction l; [discriminate | simpl; intros].
(* Goal: @ex (forall _ : A, option B) (fun m : forall _ : A, option B => and (or (@eq (forall _ : A, option B) a m) (@In (forall _ : A, option B) m l)) (@eq (option B) (m k) (@Some B v))) *)
  unfold map_add at 1 in H.
(* Goal: @ex (forall _ : A, option B) (fun m : forall _ : A, option B => and (or (@eq (forall _ : A, option B) a m) (@In (forall _ : A, option B) m l)) (@eq (option B) (m k) (@Some B v))) *)
  destruct (a k) eqn: Ha.
  - inv H; eauto.
  - destruct (IHl _ _ H) as (? & ? & ?); eauto.
Qed.

Definition all_compatible (l : list (A -> option B)) := forall m1 m2, In m1 l -> In m2 l -> compatible m1 m2.

Lemma all_compatible_cons : forall (m : A -> option B) l, all_compatible (m :: l) -> compatible m (maps_add l) /\ all_compatible l.
Proof.
(* Goal: forall (P Q : mpred) (n : nat), @eq (@pred rmap ag_rmap) (approx n (weak_view_shift P Q)) (approx n (weak_view_shift P (approx n Q))) *)
  split; repeat intro.
  - eapply in_maps_add in H1 as (m2 & ? & ?).
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
    eapply (H m m2); simpl; eauto.
  - eapply (H m1 m2); simpl; eauto.
Qed.

Lemma maps_add_in : forall l m (k : A) (v : B) (Hcompat : all_compatible l),
  In m l -> m k = Some v -> maps_add l k = Some v.
Proof.
(* Goal: forall (l : list (forall _ : A, option B)) (m : forall _ : A, option B) (k : A) (v : B) (_ : all_compatible l) (_ : @In (forall _ : A, option B) m l) (_ : @eq (option B) (m k) (@Some B v)), @eq (option B) (@fold_right (forall _ : A, option B) (forall _ : A, option B) map_add empty_map l k) (@Some B v) *)
  induction l; [contradiction | simpl; intros].
(* Goal: @eq (option B) (map_add a (@fold_right (forall _ : A, option B) (forall _ : A, option B) map_add empty_map l) k) (@Some B v) *)
  destruct H.
  - subst.
(* Goal: not (@eq (option hist_el) (@map_add nat hist_el h h2 t') (@None hist_el)) *)
    unfold map_add.
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
    replace (m k) with (Some v); auto.
  - apply all_compatible_cons in Hcompat as [].
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
    rewrite map_add_comm by auto.
(* Goal: not (@eq (option hist_el) (@map_add nat hist_el h h2 t') (@None hist_el)) *)
    unfold map_add.
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
    erewrite IHl; eauto.
Qed.

Lemma fold_right_maps_add : forall l (e : A -> option B), fold_right map_add e l = map_add (maps_add l) e.
Proof.
(* Goal: forall P Q : mpred, @derives mpred Nveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (weak_view_shift P Q) (@emp mpred Nveric Sveric)) P) (@bupd mpred own.gname preds Nveric Sveric Bveric Q) *)
  induction l; auto; simpl; intros.
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
  rewrite map_add_assoc, IHl; auto.
Qed.

Section Maps_Disjoint.
(* This map instance requires that maps be disjoint, providing e.g. uniqueness of
   timestamps for histories. *)

Definition disjoint m1 m2 := forall k v1, m1 k = Some v1 -> m2 k = None.

Global Instance disjoint_comm : Symmetric disjoint.
Proof.
(* Goal: forall (P Q : mpred) (n : nat), @eq (@pred rmap ag_rmap) (approx n (weak_view_shift P Q)) (approx n (weak_view_shift P (approx n Q))) *)
  repeat intro.
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
  destruct (x k) eqn: Hx; auto.
(* Goal: @eq B v1 v2 *)
  specialize (H _ _ Hx); congruence.
Qed.

Lemma disjoint_compatible : forall m1 m2, disjoint m1 m2 -> compatible m1 m2.
Proof.
(* Goal: forall (P Q : mpred) (n : nat), @eq (@pred rmap ag_rmap) (approx n (weak_view_shift P Q)) (approx n (weak_view_shift P (approx n Q))) *)
  repeat intro.
(* Goal: @eq B v1 v2 *)
  specialize (H _ _ H0); congruence.
Qed.

Instance map_disj_join : Join (A -> option B) :=
  fun a b c => forall k, match a k, b k with Some v, None | None, Some v => c k = Some v | None, None => c k = None | _, _ => False end.

Lemma map_disj_join_spec : forall m1 m2 m3, join m1 m2 m3 <-> disjoint m1 m2 /\ m3 = map_add m1 m2.
Proof.
(* Goal: forall P Q : mpred, @derives mpred Nveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (weak_view_shift P Q) (@emp mpred Nveric Sveric)) P) (@bupd mpred own.gname preds Nveric Sveric Bveric Q) *)
  unfold join, map_disj_join; simpl; split; intros.
  - split.
    + repeat intro.
(* Goal: @eq (option B) (m2 k) (@None B) *)
      specialize (H k); rewrite H0 in H.
(* Goal: @eq (option B) (m2 k) (@None B) *)
      destruct (m2 k); auto; contradiction.
    + extensionality k; unfold map_add.
(* Goal: @eq (option B) (m3 k) match m1 k with | Some v' => @Some B v' | None => m2 k end *)
      specialize (H k).
(* Goal: @eq (option B) (m3 k) match m1 k with | Some v' => @Some B v' | None => m2 k end *)
      destruct (m1 k), (m2 k); auto; contradiction.
  - destruct H as [Hdisj]; subst; unfold map_add.
(* Goal: match m1 k with | Some v => match m2 k with | Some b => False | None => @eq (option B) match m1 k with | Some v' => @Some B v' | None => m2 k end (@Some B v) end | None => match m2 k with | Some v => @eq (option B) match m1 k with | Some v' => @Some B v' | None => m2 k end (@Some B v) | None => @eq (option B) match m1 k with | Some v' => @Some B v' | None => m2 k end (@None B) end end *)
    specialize (Hdisj k).
    destruct (m1 k); [specialize (Hdisj _ eq_refl) as ->; auto|].
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
    destruct (m2 k); auto.
Qed.

Lemma disjoint_incl : forall m1 m2 m (Hcompat : disjoint m2 m) (Hincl : map_incl m1 m2), disjoint m1 m.
Proof.
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
  repeat intro; eauto.
Qed.

Lemma disjoint_add : forall m1 m2 m3, disjoint m1 m2 -> disjoint m1 m3 -> disjoint m1 (map_add m2 m3).
Proof.
(* Goal: forall P Q : mpred, @derives mpred Nveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (weak_view_shift P Q) (@emp mpred Nveric Sveric)) P) (@bupd mpred own.gname preds Nveric Sveric Bveric Q) *)
  unfold disjoint; intros.
(* Goal: not (@eq (option hist_el) (@map_add nat hist_el h h2 t') (@None hist_el)) *)
  unfold map_add.
(* Goal: @eq (option B) match m2 k with | Some v' => @Some B v' | None => m3 k end (@None B) *)
  specialize (H _ _ H1); specialize (H0 _ _ H1).
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
  rewrite H, H0; auto.
Qed.

(* Goal: @compatible nat hist_el (@map_upd nat hist_el nat_eq_dec h2 t e) h *)
Global Program Instance map_disj_PCM : Ghost := { valid a := True; Join_G := map_disj_join }.
Next Obligation.
(* Goal: forall (P Q : mpred) (n : nat), @eq (@pred rmap ag_rmap) (approx n (weak_view_shift P Q)) (approx n (weak_view_shift P (approx n Q))) *)
  exists (fun _ => empty_map); auto; repeat intro.
(* Goal: match empty_map k with | Some v => match t k with | Some b => False | None => @eq (option B) (t k) (@Some B v) end | None => match t k with | Some v => @eq (option B) (t k) (@Some B v) | None => @eq (option B) (t k) (@None B) end end *)
  simpl.
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
  destruct (t k); auto.
Defined.
Next Obligation.
(* Goal: hist_list' (@map_upd nat hist_el nat_eq_dec h0 (@Datatypes.length hist_el l) x) (@app hist_el l (@cons hist_el x (@nil hist_el))) *)
(* Goal: @eq (forall _ : nat, option hist_el) (@map_upd nat hist_el nat_eq_dec h0 (@Datatypes.length hist_el l) x) h *)
  constructor.
(* Goal: forall P Q : mpred, @derives mpred Nveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (weak_view_shift P Q) (@emp mpred Nveric Sveric)) P) (@bupd mpred own.gname preds Nveric Sveric Bveric Q) *)
  - intros.
(* Goal: @eq (forall _ : A, option B) z z' *)
    extensionality k.
(* Goal: @eq (option B) (z k) (z' k) *)
    specialize (H k); specialize (H0 k).
(* Goal: @eq (option B) (z k) (z' k) *)
    destruct (x k), (y k); try congruence; contradiction.
(* Goal: forall P Q : mpred, @derives mpred Nveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (weak_view_shift P Q) (@emp mpred Nveric Sveric)) P) (@bupd mpred own.gname preds Nveric Sveric Bveric Q) *)
  - intros.
    rewrite map_disj_join_spec in *.
(* Goal: @sigT (forall _ : A, option B) (fun f : forall _ : A, option B => and (@join (forall _ : A, option B) map_disj_join b c f) (@join (forall _ : A, option B) map_disj_join a f e)) *)
    destruct H, H0; subst.
(* Goal: @sigT (forall _ : A, option B) (fun f : forall _ : A, option B => and (@join (forall _ : A, option B) map_disj_join b c f) (@join (forall _ : A, option B) map_disj_join a f (map_add (map_add a b) c))) *)
    rewrite map_add_assoc.
(* Goal: and (not (@eq share (Share.comp sh) Share.bot)) (and (@join share Share.Join_ba sh (Share.comp sh) Tsh) (@join (forall _ : nat, option hist_el) (@map_disj_join nat hist_el) h h' hr)) *)
    eexists; rewrite !map_disj_join_spec; repeat split.
    + eapply disjoint_incl; eauto.
(* Goal: map_incl b (map_add a b) *)
      rewrite map_add_comm by (apply disjoint_compatible; auto); apply map_incl_add.
    + apply disjoint_add; auto.
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
      eapply disjoint_incl; eauto.
(* Goal: @map_incl nat hist_el h (@map_add nat hist_el h x) *)
      apply map_incl_add.
  - intros ???; rewrite !map_disj_join_spec; intros []; subst.
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
    split; [symmetry | apply map_add_comm, disjoint_compatible]; auto.
(* Goal: forall P Q : mpred, @derives mpred Nveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (weak_view_shift P Q) (@emp mpred Nveric Sveric)) P) (@bupd mpred own.gname preds Nveric Sveric Bveric Q) *)
  - intros.
(* Goal: @eq (option B) (z k) (z' k) *)
    extensionality k; specialize (H k); specialize (H0 k).
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
    destruct (a k), (b k); auto.
    + destruct (a' k); [contradiction | auto].
    + destruct (a' k); [contradiction | auto].
    + destruct (b' k); [contradiction | auto].
Defined.
Next Obligation.
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
  auto.
Defined.

Lemma disj_join_sub : forall m1 m2, map_incl m1 m2 -> exists m3, join m1 m3 m2.
Proof.
(* Goal: forall (m1 m2 : forall _ : A, option B) (_ : map_incl m1 m2), @ex (forall _ : A, option B) (fun m3 : forall _ : A, option B => @join (forall _ : A, option B) map_disj_join m1 m3 m2) *)
  intros; exists (fun x => match m2 x, m1 x with Some v, None => Some v | _, _ => None end).
(* Goal: @eq (option B) (m3 k) match m1 k with | Some v' => @Some B v' | None => m2 k end *)
  intro k; specialize (H k).
(* Goal: match m1 k with | Some v => match match m2 k with | Some v0 => match m1 k with | Some b => @None B | None => @Some B v0 end | None => @None B end with | Some b => False | None => @eq (option B) (m2 k) (@Some B v) end | None => match match m2 k with | Some v => match m1 k with | Some b => @None B | None => @Some B v end | None => @None B end with | Some v => @eq (option B) (m2 k) (@Some B v) | None => @eq (option B) (m2 k) (@None B) end end *)
  destruct (m1 k).
  - erewrite H; eauto.
  - destruct (m2 k); auto.
Qed.

Definition all_disjoint (l : list (A -> option B)) := forall i j, 0 <= i < Zlength l -> 0 <= j < Zlength l ->
  i <> j -> disjoint (Znth i l) (Znth j l).

Lemma all_disjoint_compatible : forall l, all_disjoint l -> all_compatible l.
Proof.
(* Goal: forall P Q : mpred, @derives mpred Nveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (weak_view_shift P Q) (@emp mpred Nveric Sveric)) P) (@bupd mpred own.gname preds Nveric Sveric Bveric Q) *)
  unfold all_disjoint, all_compatible; intros.
(* Goal: @eq (option B) (map_add a (@fold_right (forall _ : A, option B) (forall _ : A, option B) map_add empty_map l) k) (@Some B v) *)
  apply In_Znth in H0 as (i & ? & ?); apply In_Znth in H1 as (j & ? & ?); subst.
(* Goal: compatible (@Znth (forall _ : A, option B) Inhabitant_map i l) (@Znth (forall _ : A, option B) Inhabitant_map j l) *)
  destruct (eq_dec i j); [subst; reflexivity|].
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
  apply disjoint_compatible; auto.
Qed.

Lemma all_disjoint_nil : all_disjoint [].
Proof.
(* Goal: forall (P Q : mpred) (n : nat), @eq (@pred rmap ag_rmap) (approx n (weak_view_shift P Q)) (approx n (weak_view_shift P (approx n Q))) *)
  repeat intro.
  rewrite Zlength_nil in *; omega.
Qed.

Lemma all_disjoint_cons : forall (m : A -> option B) l, all_disjoint (m :: l) <-> disjoint m (maps_add l) /\ all_disjoint l.
Proof.
(* Goal: and (not (@eq share (Share.comp sh) Share.bot)) (and (@join share Share.Join_ba sh (Share.comp sh) Tsh) (@join (forall _ : nat, option hist_el) (@map_disj_join nat hist_el) h h' hr)) *)
  split.
  - split; repeat intro.
    + destruct (maps_add l k) eqn: Hl; auto.
(* Goal: @eq (option B) (@Some B b) (@None B) *)
      eapply in_maps_add in Hl as (m2 & ? & ?).
(* Goal: @eq (option B) (map_add a (@fold_right (forall _ : A, option B) (forall _ : A, option B) map_add empty_map l) k) (@Some B v) *)
      apply In_Znth in H1 as (j & ? & ?); subst.
      specialize (H 0 (j + 1)).
(* Goal: @eq (option B) (@Some B b) (@None B) *)
      rewrite Znth_0_cons, Znth_pos_cons, Z.add_simpl_r, Zlength_cons in H by omega.
(* Goal: @eq (option B) (@Some B b) (@None B) *)
      erewrite H in H2; eauto; omega.
    + specialize (H (i + 1) (j + 1)).
(* Goal: @eq (option B) (@Znth (forall _ : A, option B) Inhabitant_map j l k) (@None B) *)
      rewrite !Znth_pos_cons, !Z.add_simpl_r, Zlength_cons in H by omega.
(* Goal: @eq (option B) (@Znth (forall _ : A, option B) Inhabitant_map j l k) (@None B) *)
      eapply H; eauto; omega.
  - intros []; repeat intro.
    rewrite Zlength_cons in *.
(* Goal: @eq (option B) (@Znth (forall _ : A, option B) Inhabitant_map j (@cons (forall _ : A, option B) m l) k) (@None B) *)
    destruct (eq_dec i 0), (eq_dec j 0); subst; try contradiction.
    + rewrite Znth_0_cons in H4; rewrite Znth_pos_cons by omega.
(* Goal: @eq (option B) (@Znth (forall _ : A, option B) Inhabitant_map (Z.sub j (Zpos xH)) l k) (@None B) *)
      specialize (H _ _ H4).
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
      destruct (Znth _ _ _) eqn: Hj; auto.
(* Goal: @eq B v1 v2 *)
      apply maps_add_in with (l := l) in Hj; try congruence.
      * apply all_disjoint_compatible; auto.
      * apply Znth_In; omega.
    + rewrite Znth_0_cons; rewrite Znth_pos_cons in H4 by omega.
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
      destruct (m k) eqn: Hm; auto.
(* Goal: @eq (option B) (@Some B b) (@None B) *)
      specialize (H _ _ Hm).
(* Goal: @eq B v1 v2 *)
      apply maps_add_in with (l := l) in H4; try congruence.
      * apply all_disjoint_compatible; auto.
      * apply Znth_In; omega.
    + rewrite Znth_pos_cons in * by omega.
      eapply (H0 (i - 1) (j - 1)); eauto; omega.
Qed.

Lemma all_disjoint_rev1 : forall l, all_disjoint l -> all_disjoint (rev l).
Proof.
(* Goal: forall P Q : mpred, @derives mpred Nveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (weak_view_shift P Q) (@emp mpred Nveric Sveric)) P) (@bupd mpred own.gname preds Nveric Sveric Bveric Q) *)
  unfold all_disjoint; intros.
  rewrite Zlength_rev in *.
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
  rewrite !Znth_rev by auto.
(* Goal: disjoint (@Znth (forall _ : A, option B) Inhabitant_map (Z.sub (Z.sub (@Zlength (forall _ : A, option B) l) i) (Zpos xH)) l) (@Znth (forall _ : A, option B) Inhabitant_map (Z.sub (Z.sub (@Zlength (forall _ : A, option B) l) j) (Zpos xH)) l) *)
  apply H; omega.
Qed.

Lemma all_disjoint_rev : forall l, all_disjoint l <-> all_disjoint (rev l).
Proof.
(* Goal: forall l : list (forall _ : A, option B), iff (all_disjoint l) (all_disjoint (@rev (forall _ : A, option B) l)) *)
  split; [apply all_disjoint_rev1|].
(* Goal: forall _ : all_disjoint (@rev (forall _ : A, option B) l), all_disjoint l *)
  intros ?%all_disjoint_rev1.
  rewrite rev_involutive in *; auto.
Qed.

Lemma maps_add_rev : forall l, all_compatible l -> maps_add (rev l) = maps_add l.
Proof.
(* Goal: forall P Q : mpred, @derives mpred Nveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (weak_view_shift P Q) (@emp mpred Nveric Sveric)) P) (@bupd mpred own.gname preds Nveric Sveric Bveric Q) *)
  induction l; auto; simpl; intros.
(* Goal: @eq (forall _ : A, option B) (@fold_right (forall _ : A, option B) (forall _ : A, option B) map_add empty_map (@app (forall _ : A, option B) (@rev (forall _ : A, option B) l) (@cons (forall _ : A, option B) a (@nil (forall _ : A, option B))))) (map_add a (@fold_right (forall _ : A, option B) (forall _ : A, option B) map_add empty_map l)) *)
  apply all_compatible_cons in H as [].
(* Goal: match empty_map k with | Some v => match t k with | Some b => False | None => @eq (option B) (t k) (@Some B v) end | None => match t k with | Some v => @eq (option B) (t k) (@Some B v) | None => @eq (option B) (t k) (@None B) end end *)
  rewrite map_add_comm, fold_right_app by auto; simpl.
(* Goal: @eq (forall _ : A, option B) (@fold_right (forall _ : A, option B) (forall _ : A, option B) map_add (map_add a empty_map) (@rev (forall _ : A, option B) l)) (map_add (@fold_right (forall _ : A, option B) (forall _ : A, option B) map_add empty_map l) a) *)
  rewrite map_add_empty.
(* Goal: @eq (forall _ : A, option B) (@fold_right (forall _ : A, option B) (forall _ : A, option B) map_add a (@rev (forall _ : A, option B) l)) (map_add (@fold_right (forall _ : A, option B) (forall _ : A, option B) map_add empty_map l) a) *)
  rewrite (fold_right_maps_add _ a).
  rewrite <- IHl; auto.
Qed.

Lemma all_disjoint_snoc : forall m l, all_disjoint (l ++ [m]) <-> disjoint m (maps_add l) /\ all_disjoint l.
Proof.
(* Goal: forall P Q : mpred, @derives mpred Nveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (weak_view_shift P Q) (@emp mpred Nveric Sveric)) P) (@bupd mpred own.gname preds Nveric Sveric Bveric Q) *)
  intros.
  replace (l ++ [m]) with (rev (m :: rev l)) by (simpl; rewrite rev_involutive; auto).
  rewrite all_disjoint_rev, rev_involutive, all_disjoint_cons, <- all_disjoint_rev.
  split; intros []; rewrite maps_add_rev in *; auto; apply all_disjoint_compatible; auto.
Qed.

Lemma empty_map_disjoint : forall m, disjoint empty_map m.
Proof.
(* Goal: forall h : list hist_el, hist_incl (@empty_map nat hist_el) h *)
  repeat intro; discriminate.
Qed.

Definition map_sub (m : A -> option B) k := fun x => if eq_dec x k then None else m x.

Lemma map_upd_sub : forall m (k : A) (v : B), m k = Some v -> map_upd (map_sub m k) k v = m.
Proof.
(* Goal: forall (m : forall _ : A, option B) (k : A) (v : B) (_ : @eq (option B) (m k) (@None B)), @eq (forall _ : A, option B) (map_sub (map_upd m k v) k) m *)
  intros; unfold map_upd, map_sub.
(* Goal: @eq (forall _ : A, option B) (fun x : A => if @eq_dec A A_eq x k then @None B else if @eq_dec A A_eq x k then @Some B v else m x) m *)
  extensionality x.
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
  if_tac; subst; auto.
Qed.

Lemma map_sub_upd : forall m (k : A) (v : B), m k = None -> map_sub (map_upd m k v) k = m.
Proof.
(* Goal: forall (m : forall _ : A, option B) (k : A) (v : B) (_ : @eq (option B) (m k) (@None B)), @eq (forall _ : A, option B) (map_sub (map_upd m k v) k) m *)
  intros; unfold map_upd, map_sub.
(* Goal: @eq (forall _ : A, option B) (fun x : A => if @eq_dec A A_eq x k then @None B else if @eq_dec A A_eq x k then @Some B v else m x) m *)
  extensionality x.
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
  if_tac; subst; auto.
Qed.

Lemma disjoint_sub : forall (m1 m2 : A -> option B) k, disjoint m1 m2 ->
  disjoint (map_sub m1 k) m2.
Proof.
(* Goal: forall P Q : mpred, @derives mpred Nveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (weak_view_shift P Q) (@emp mpred Nveric Sveric)) P) (@bupd mpred own.gname preds Nveric Sveric Bveric Q) *)
  unfold map_sub, disjoint; intros.
(* Goal: @eq (option B) (m2 k0) (@None B) *)
  destruct (eq_dec _ _); [discriminate | eauto].
Qed.

End Maps_Disjoint.

End Maps.

Notation maps_add l := (fold_right map_add empty_map l).

Hint Resolve empty_map_incl empty_map_disjoint all_disjoint_nil.

Section GHist.

(* Ghost histories in the style of Nanevsky *)
(* Goal: @compatible nat hist_el (@map_upd nat hist_el nat_eq_dec h2 t e) h *)
Context {hist_el : Type}.

Notation hist_part := (nat -> option hist_el).

Definition hist_sub sh (h : hist_part) hr := sh <> Share.bot /\ if eq_dec sh Tsh then h = hr
  else map_incl h hr.

Lemma completable_alt : forall sh h hr, @completable map_disj_PCM (Some (sh, h)) hr <-> hist_sub sh h hr.
Proof.
(* Goal: and (not (@eq share (Share.comp sh) Share.bot)) (and (@join share Share.Join_ba sh (Share.comp sh) Tsh) (@join (forall _ : nat, option hist_el) (@map_disj_join nat hist_el) h h' hr)) *)
  unfold completable, hist_sub; intros; simpl; split.
  - intros ([(?, ?)|] & Hcase).
    + destruct Hcase as (? & ? & Hsh & Hj); split; auto.
(* Goal: forall _ : @eq (option hist_el) (@nth_error hist_el (@app hist_el l (@cons hist_el e (@nil hist_el))) t) (@Some hist_el e0), @eq (option hist_el) (if @eq_dec nat nat_eq_dec t (@Datatypes.length hist_el l) then @Some hist_el e else h t) (@Some hist_el e0) *)
      if_tac.
      * subst; apply join_Tsh in Hsh; tauto.
      * rewrite map_disj_join_spec in Hj; destruct Hj; subst.
(* Goal: @map_incl nat hist_el h (@map_add nat hist_el h x) *)
        apply map_incl_add.
    + hnf in Hcase.
(* Goal: and (not (@eq Share.t sh Share.bot)) (if @eq_dec Share.t Share.EqDec_share sh Tsh then @eq (forall _ : nat, option hist_el) h hr else @map_incl nat hist_el h hr) *)
      inv Hcase.
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
      rewrite eq_dec_refl; auto.
  - if_tac.
    + intros []; subst; exists None; split; auto.
    + intros [? Hincl].
(* Goal: @ex (option (prod share (forall _ : nat, option hist_el))) (fun x : option (prod share (forall _ : nat, option hist_el)) => @join (option (prod share (forall _ : nat, option hist_el))) (fun a b c : option (prod share (forall _ : nat, option hist_el)) => match a as c' return (forall (_ : @eq (option (prod share (forall _ : nat, option hist_el))) c' a) (_ : @eq (option (prod share (forall _ : nat, option hist_el))) b b) (_ : @eq (option (prod share (forall _ : nat, option hist_el))) c c), Prop) with | Some p => let (sh, a0) as p0 return (forall (_ : @eq (option (prod share (forall _ : nat, option hist_el))) (@Some (prod share (forall _ : nat, option hist_el)) p0) a) (_ : @eq (option (prod share (forall _ : nat, option hist_el))) b b) (_ : @eq (option (prod share (forall _ : nat, option hist_el))) c c), Prop) := p in match b as b' return (forall (_ : @eq (option (prod share (forall _ : nat, option hist_el))) (@Some (prod share (forall _ : nat, option hist_el)) (@pair share (forall _ : nat, option hist_el) sh a0)) a) (_ : @eq (option (prod share (forall _ : nat, option hist_el))) b' b) (_ : @eq (option (prod share (forall _ : nat, option hist_el))) c c), Prop) with | Some p0 => let (shb, b') as p1 return (forall (_ : @eq (option (prod share (forall _ : nat, option hist_el))) (@Some (prod share (forall _ : nat, option hist_el)) (@pair share (forall _ : nat, option hist_el) sh a0)) a) (_ : @eq (option (prod share (forall _ : nat, option hist_el))) (@Some (prod share (forall _ : nat, option hist_el)) p1) b) (_ : @eq (option (prod share (forall _ : nat, option hist_el))) c c), Prop) := p0 in match c as a' return (forall (_ : @eq (option (prod share (forall _ : nat, option hist_el))) (@Some (prod share (forall _ : nat, option hist_el)) (@pair share (forall _ : nat, option hist_el) sh a0)) a) (_ : @eq (option (prod share (forall _ : nat, option hist_el))) (@Some (prod share (forall _ : nat, option hist_el)) (@pair share (forall _ : nat, option hist_el) shb b')) b) (_ : @eq (option (prod share (forall _ : nat, option hist_el))) a' c), Prop) with | Some p1 => let (shc, c') as p2 return (forall (_ : @eq (option (prod share (forall _ : nat, option hist_el))) (@Some (prod share (forall _ : nat, option hist_el)) (@pair share (forall _ : nat, option hist_el) sh a0)) a) (_ : @eq (option (prod share (forall _ : nat, option hist_el))) (@Some (prod share (forall _ : nat, option hist_el)) (@pair share (forall _ : nat, option hist_el) shb b')) b) (_ : @eq (option (prod share (forall _ : nat, option hist_el))) (@Some (prod share (forall _ : nat, option hist_el)) p2) c), Prop) := p1 in fun (_ : @eq (option (prod share (forall _ : nat, option hist_el))) (@Some (prod share (forall _ : nat, option hist_el)) (@pair share (forall _ : nat, option hist_el) sh a0)) a) (_ : @eq (option (prod share (forall _ : nat, option hist_el))) (@Some (prod share (forall _ : nat, option hist_el)) (@pair share (forall _ : nat, option hist_el) shb b')) b) (_ : @eq (option (prod share (forall _ : nat, option hist_el))) (@Some (prod share (forall _ : nat, option hist_el)) (@pair share (forall _ : nat, option hist_el) shc c')) c) => and (not (@eq share sh Share.bot)) (and (not (@eq share shb Share.bot)) (and (@join share Share.Join_ba sh shb shc) (@join (forall _ : nat, option hist_el) (@map_disj_join nat hist_el) a0 b' c'))) | None => fun (_ : @eq (option (prod share (forall _ : nat, option hist_el))) (@Some (prod share (forall _ : nat, option hist_el)) (@pair share (forall _ : nat, option hist_el) sh a0)) a) (_ : @eq (option (prod share (forall _ : nat, option hist_el))) (@Some (prod share (forall _ : nat, option hist_el)) (@pair share (forall _ : nat, option hist_el) shb b')) b) (_ : @eq (option (prod share (forall _ : nat, option hist_el))) (@None (prod share (forall _ : nat, option hist_el))) c) => False end | None => match c as a' return (forall (_ : @eq (option (prod share (forall _ : nat, option hist_el))) (@Some (prod share (forall _ : nat, option hist_el)) (@pair share (forall _ : nat, option hist_el) sh a0)) a) (_ : @eq (option (prod share (forall _ : nat, option hist_el))) (@None (prod share (forall _ : nat, option hist_el))) b) (_ : @eq (option (prod share (forall _ : nat, option hist_el))) a' c), Prop) with | Some c' => fun (_ : @eq (option (prod share (forall _ : nat, option hist_el))) (@Some (prod share (forall _ : nat, option hist_el)) (@pair share (forall _ : nat, option hist_el) sh a0)) a) (_ : @eq (option (prod share (forall _ : nat, option hist_el))) (@None (prod share (forall _ : nat, option hist_el))) b) (_ : @eq (option (prod share (forall _ : nat, option hist_el))) (@Some (prod share (forall _ : nat, option hist_el)) c') c) => @eq (prod share (forall _ : nat, option hist_el)) c' (@pair share (forall _ : nat, option hist_el) sh a0) | None => fun (_ : @eq (option (prod share (forall _ : nat, option hist_el))) (@Some (prod share (forall _ : nat, option hist_el)) (@pair share (forall _ : nat, option hist_el) sh a0)) a) (_ : @eq (option (prod share (forall _ : nat, option hist_el))) (@None (prod share (forall _ : nat, option hist_el))) b) (_ : @eq (option (prod share (forall _ : nat, option hist_el))) (@None (prod share (forall _ : nat, option hist_el))) c) => False end end | None => match b as b' return (forall (_ : @eq (option (prod share (forall _ : nat, option hist_el))) (@None (prod share (forall _ : nat, option hist_el))) a) (_ : @eq (option (prod share (forall _ : nat, option hist_el))) b' b) (_ : @eq (option (prod share (forall _ : nat, option hist_el))) c c), Prop) with | Some p => let (sh, a0) as p0 return (forall (_ : @eq (option (prod share (forall _ : nat, option hist_el))) (@None (prod share (forall _ : nat, option hist_el))) a) (_ : @eq (option (prod share (forall _ : nat, option hist_el))) (@Some (prod share (forall _ : nat, option hist_el)) p0) b) (_ : @eq (option (prod share (forall _ : nat, option hist_el))) c c), Prop) := p in match c as a' return (forall (_ : @eq (option (prod share (forall _ : nat, option hist_el))) (@None (prod share (forall _ : nat, option hist_el))) a) (_ : @eq (option (prod share (forall _ : nat, option hist_el))) (@Some (prod share (forall _ : nat, option hist_el)) (@pair share (forall _ : nat, option hist_el) sh a0)) b) (_ : @eq (option (prod share (forall _ : nat, option hist_el))) a' c), Prop) with | Some c' => fun (_ : @eq (option (prod share (forall _ : nat, option hist_el))) (@None (prod share (forall _ : nat, option hist_el))) a) (_ : @eq (option (prod share (forall _ : nat, option hist_el))) (@Some (prod share (forall _ : nat, option hist_el)) (@pair share (forall _ : nat, option hist_el) sh a0)) b) (_ : @eq (option (prod share (forall _ : nat, option hist_el))) (@Some (prod share (forall _ : nat, option hist_el)) c') c) => @eq (prod share (forall _ : nat, option hist_el)) c' (@pair share (forall _ : nat, option hist_el) sh a0) | None => fun (_ : @eq (option (prod share (forall _ : nat, option hist_el))) (@None (prod share (forall _ : nat, option hist_el))) a) (_ : @eq (option (prod share (forall _ : nat, option hist_el))) (@Some (prod share (forall _ : nat, option hist_el)) (@pair share (forall _ : nat, option hist_el) sh a0)) b) (_ : @eq (option (prod share (forall _ : nat, option hist_el))) (@None (prod share (forall _ : nat, option hist_el))) c) => False end | None => match c as a' return (forall (_ : @eq (option (prod share (forall _ : nat, option hist_el))) (@None (prod share (forall _ : nat, option hist_el))) a) (_ : @eq (option (prod share (forall _ : nat, option hist_el))) (@None (prod share (forall _ : nat, option hist_el))) b) (_ : @eq (option (prod share (forall _ : nat, option hist_el))) a' c), Prop) with | Some p => fun (_ : @eq (option (prod share (forall _ : nat, option hist_el))) (@None (prod share (forall _ : nat, option hist_el))) a) (_ : @eq (option (prod share (forall _ : nat, option hist_el))) (@None (prod share (forall _ : nat, option hist_el))) b) (_ : @eq (option (prod share (forall _ : nat, option hist_el))) (@Some (prod share (forall _ : nat, option hist_el)) p) c) => False | None => fun (_ : @eq (option (prod share (forall _ : nat, option hist_el))) (@None (prod share (forall _ : nat, option hist_el))) a) (_ : @eq (option (prod share (forall _ : nat, option hist_el))) (@None (prod share (forall _ : nat, option hist_el))) b) (_ : @eq (option (prod share (forall _ : nat, option hist_el))) (@None (prod share (forall _ : nat, option hist_el))) c) => True end end end (@eq_refl (option (prod share (forall _ : nat, option hist_el))) a) (@eq_refl (option (prod share (forall _ : nat, option hist_el))) b) (@eq_refl (option (prod share (forall _ : nat, option hist_el))) c)) (@Some (prod share (forall _ : nat, option hist_el)) (@pair share (forall _ : nat, option hist_el) sh h)) x (@Some (prod share (forall _ : nat, option hist_el)) (@pair share (forall _ : nat, option hist_el) Tsh hr))) *)
      apply disj_join_sub in Hincl as (h' & ?).
(* Goal: @ex (option (prod share (forall _ : nat, option hist_el))) (fun x : option (prod share (forall _ : nat, option hist_el)) => @join (option (prod share (forall _ : nat, option hist_el))) (fun a b c : option (prod share (forall _ : nat, option hist_el)) => match a as c' return (forall (_ : @eq (option (prod share (forall _ : nat, option hist_el))) c' a) (_ : @eq (option (prod share (forall _ : nat, option hist_el))) b b) (_ : @eq (option (prod share (forall _ : nat, option hist_el))) c c), Prop) with | Some p => let (sh, a0) as p0 return (forall (_ : @eq (option (prod share (forall _ : nat, option hist_el))) (@Some (prod share (forall _ : nat, option hist_el)) p0) a) (_ : @eq (option (prod share (forall _ : nat, option hist_el))) b b) (_ : @eq (option (prod share (forall _ : nat, option hist_el))) c c), Prop) := p in match b as b' return (forall (_ : @eq (option (prod share (forall _ : nat, option hist_el))) (@Some (prod share (forall _ : nat, option hist_el)) (@pair share (forall _ : nat, option hist_el) sh a0)) a) (_ : @eq (option (prod share (forall _ : nat, option hist_el))) b' b) (_ : @eq (option (prod share (forall _ : nat, option hist_el))) c c), Prop) with | Some p0 => let (shb, b') as p1 return (forall (_ : @eq (option (prod share (forall _ : nat, option hist_el))) (@Some (prod share (forall _ : nat, option hist_el)) (@pair share (forall _ : nat, option hist_el) sh a0)) a) (_ : @eq (option (prod share (forall _ : nat, option hist_el))) (@Some (prod share (forall _ : nat, option hist_el)) p1) b) (_ : @eq (option (prod share (forall _ : nat, option hist_el))) c c), Prop) := p0 in match c as a' return (forall (_ : @eq (option (prod share (forall _ : nat, option hist_el))) (@Some (prod share (forall _ : nat, option hist_el)) (@pair share (forall _ : nat, option hist_el) sh a0)) a) (_ : @eq (option (prod share (forall _ : nat, option hist_el))) (@Some (prod share (forall _ : nat, option hist_el)) (@pair share (forall _ : nat, option hist_el) shb b')) b) (_ : @eq (option (prod share (forall _ : nat, option hist_el))) a' c), Prop) with | Some p1 => let (shc, c') as p2 return (forall (_ : @eq (option (prod share (forall _ : nat, option hist_el))) (@Some (prod share (forall _ : nat, option hist_el)) (@pair share (forall _ : nat, option hist_el) sh a0)) a) (_ : @eq (option (prod share (forall _ : nat, option hist_el))) (@Some (prod share (forall _ : nat, option hist_el)) (@pair share (forall _ : nat, option hist_el) shb b')) b) (_ : @eq (option (prod share (forall _ : nat, option hist_el))) (@Some (prod share (forall _ : nat, option hist_el)) p2) c), Prop) := p1 in fun (_ : @eq (option (prod share (forall _ : nat, option hist_el))) (@Some (prod share (forall _ : nat, option hist_el)) (@pair share (forall _ : nat, option hist_el) sh a0)) a) (_ : @eq (option (prod share (forall _ : nat, option hist_el))) (@Some (prod share (forall _ : nat, option hist_el)) (@pair share (forall _ : nat, option hist_el) shb b')) b) (_ : @eq (option (prod share (forall _ : nat, option hist_el))) (@Some (prod share (forall _ : nat, option hist_el)) (@pair share (forall _ : nat, option hist_el) shc c')) c) => and (not (@eq share sh Share.bot)) (and (not (@eq share shb Share.bot)) (and (@join share Share.Join_ba sh shb shc) (@join (forall _ : nat, option hist_el) (@map_disj_join nat hist_el) a0 b' c'))) | None => fun (_ : @eq (option (prod share (forall _ : nat, option hist_el))) (@Some (prod share (forall _ : nat, option hist_el)) (@pair share (forall _ : nat, option hist_el) sh a0)) a) (_ : @eq (option (prod share (forall _ : nat, option hist_el))) (@Some (prod share (forall _ : nat, option hist_el)) (@pair share (forall _ : nat, option hist_el) shb b')) b) (_ : @eq (option (prod share (forall _ : nat, option hist_el))) (@None (prod share (forall _ : nat, option hist_el))) c) => False end | None => match c as a' return (forall (_ : @eq (option (prod share (forall _ : nat, option hist_el))) (@Some (prod share (forall _ : nat, option hist_el)) (@pair share (forall _ : nat, option hist_el) sh a0)) a) (_ : @eq (option (prod share (forall _ : nat, option hist_el))) (@None (prod share (forall _ : nat, option hist_el))) b) (_ : @eq (option (prod share (forall _ : nat, option hist_el))) a' c), Prop) with | Some c' => fun (_ : @eq (option (prod share (forall _ : nat, option hist_el))) (@Some (prod share (forall _ : nat, option hist_el)) (@pair share (forall _ : nat, option hist_el) sh a0)) a) (_ : @eq (option (prod share (forall _ : nat, option hist_el))) (@None (prod share (forall _ : nat, option hist_el))) b) (_ : @eq (option (prod share (forall _ : nat, option hist_el))) (@Some (prod share (forall _ : nat, option hist_el)) c') c) => @eq (prod share (forall _ : nat, option hist_el)) c' (@pair share (forall _ : nat, option hist_el) sh a0) | None => fun (_ : @eq (option (prod share (forall _ : nat, option hist_el))) (@Some (prod share (forall _ : nat, option hist_el)) (@pair share (forall _ : nat, option hist_el) sh a0)) a) (_ : @eq (option (prod share (forall _ : nat, option hist_el))) (@None (prod share (forall _ : nat, option hist_el))) b) (_ : @eq (option (prod share (forall _ : nat, option hist_el))) (@None (prod share (forall _ : nat, option hist_el))) c) => False end end | None => match b as b' return (forall (_ : @eq (option (prod share (forall _ : nat, option hist_el))) (@None (prod share (forall _ : nat, option hist_el))) a) (_ : @eq (option (prod share (forall _ : nat, option hist_el))) b' b) (_ : @eq (option (prod share (forall _ : nat, option hist_el))) c c), Prop) with | Some p => let (sh, a0) as p0 return (forall (_ : @eq (option (prod share (forall _ : nat, option hist_el))) (@None (prod share (forall _ : nat, option hist_el))) a) (_ : @eq (option (prod share (forall _ : nat, option hist_el))) (@Some (prod share (forall _ : nat, option hist_el)) p0) b) (_ : @eq (option (prod share (forall _ : nat, option hist_el))) c c), Prop) := p in match c as a' return (forall (_ : @eq (option (prod share (forall _ : nat, option hist_el))) (@None (prod share (forall _ : nat, option hist_el))) a) (_ : @eq (option (prod share (forall _ : nat, option hist_el))) (@Some (prod share (forall _ : nat, option hist_el)) (@pair share (forall _ : nat, option hist_el) sh a0)) b) (_ : @eq (option (prod share (forall _ : nat, option hist_el))) a' c), Prop) with | Some c' => fun (_ : @eq (option (prod share (forall _ : nat, option hist_el))) (@None (prod share (forall _ : nat, option hist_el))) a) (_ : @eq (option (prod share (forall _ : nat, option hist_el))) (@Some (prod share (forall _ : nat, option hist_el)) (@pair share (forall _ : nat, option hist_el) sh a0)) b) (_ : @eq (option (prod share (forall _ : nat, option hist_el))) (@Some (prod share (forall _ : nat, option hist_el)) c') c) => @eq (prod share (forall _ : nat, option hist_el)) c' (@pair share (forall _ : nat, option hist_el) sh a0) | None => fun (_ : @eq (option (prod share (forall _ : nat, option hist_el))) (@None (prod share (forall _ : nat, option hist_el))) a) (_ : @eq (option (prod share (forall _ : nat, option hist_el))) (@Some (prod share (forall _ : nat, option hist_el)) (@pair share (forall _ : nat, option hist_el) sh a0)) b) (_ : @eq (option (prod share (forall _ : nat, option hist_el))) (@None (prod share (forall _ : nat, option hist_el))) c) => False end | None => match c as a' return (forall (_ : @eq (option (prod share (forall _ : nat, option hist_el))) (@None (prod share (forall _ : nat, option hist_el))) a) (_ : @eq (option (prod share (forall _ : nat, option hist_el))) (@None (prod share (forall _ : nat, option hist_el))) b) (_ : @eq (option (prod share (forall _ : nat, option hist_el))) a' c), Prop) with | Some p => fun (_ : @eq (option (prod share (forall _ : nat, option hist_el))) (@None (prod share (forall _ : nat, option hist_el))) a) (_ : @eq (option (prod share (forall _ : nat, option hist_el))) (@None (prod share (forall _ : nat, option hist_el))) b) (_ : @eq (option (prod share (forall _ : nat, option hist_el))) (@Some (prod share (forall _ : nat, option hist_el)) p) c) => False | None => fun (_ : @eq (option (prod share (forall _ : nat, option hist_el))) (@None (prod share (forall _ : nat, option hist_el))) a) (_ : @eq (option (prod share (forall _ : nat, option hist_el))) (@None (prod share (forall _ : nat, option hist_el))) b) (_ : @eq (option (prod share (forall _ : nat, option hist_el))) (@None (prod share (forall _ : nat, option hist_el))) c) => True end end end (@eq_refl (option (prod share (forall _ : nat, option hist_el))) a) (@eq_refl (option (prod share (forall _ : nat, option hist_el))) b) (@eq_refl (option (prod share (forall _ : nat, option hist_el))) c)) (@Some (prod share (forall _ : nat, option hist_el)) (@pair share (forall _ : nat, option hist_el) sh h)) x (@Some (prod share (forall _ : nat, option hist_el)) (@pair share (forall _ : nat, option hist_el) Tsh hr))) *)
      exists (Some (Share.comp sh, h')).
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
      split; auto.
(* Goal: and (not (@eq share (Share.comp sh) Share.bot)) (and (@join share Share.Join_ba sh (Share.comp sh) Tsh) (@join (forall _ : nat, option hist_el) (@map_disj_join nat hist_el) h h' hr)) *)
      split.
(* Goal: @compatible nat hist_el (@map_upd nat hist_el nat_eq_dec h2 t e) h *)
      { intro Hbot; contradiction H.
        rewrite <- Share.comp_inv at 1.
        rewrite Hbot; apply comp_bot. }
(* Goal: and (@join share Share.Join_ba sh (Share.comp sh) Tsh) (@join (forall _ : nat, option hist_el) (@map_disj_join nat hist_el) h h' hr) *)
      split; [apply comp_join_top | auto].
Qed.

Lemma hist_sub_upd : forall sh h hr t' e (Hsub : hist_sub sh h hr),
  hist_sub sh (map_upd h t' e) (map_upd hr t' e).
Proof.
(* Goal: forall P Q : mpred, @derives mpred Nveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (weak_view_shift P Q) (@emp mpred Nveric Sveric)) P) (@bupd mpred own.gname preds Nveric Sveric Bveric Q) *)
  unfold hist_sub; intros.
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
  destruct Hsub; split; auto.
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
  if_tac; subst; auto.
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
  apply map_upd2_incl; auto.
Qed.

Definition ghost_hist (sh : share) (h : hist_part) g :=
  own(RA := ref_PCM map_disj_PCM) g (Some (sh, h), None) NoneP.

Lemma ghost_hist_join : forall sh1 sh2 sh h1 h2 p (Hsh : sepalg.join sh1 sh2 sh)
  (Hsh1 : sh1 <> Share.bot) (Hsh2 : sh2 <> Share.bot),
  ghost_hist sh1 h1 p * ghost_hist sh2 h2 p = !!(disjoint h1 h2) && ghost_hist sh (map_add h1 h2) p.
Proof.
  intros; unfold ghost_hist.
  erewrite own_op_gen.
(* Goal: @derives mpred Nveric (@TT mpred Nveric) (@prop mpred Nveric (if @eq_dec share Share.EqDec_share sh Tsh then @eq (@G P) a b else @ex (@G P) (fun x : @G P => @join (@G P) (@Join_G P) a x b))) *)
  apply pred_ext; Intros; apply andp_right, derives_refl; apply prop_right.
  - destruct H as (? & [] & ?); simpl in *.
    destruct (fst x) as [[]|]; [|contradiction].
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
    rewrite map_disj_join_spec in H; tauto.
  - eexists (Some (sh, map_add h1 h2), None); split; [split|]; simpl.
    + rewrite map_disj_join_spec; auto.
    + constructor.
    + split; auto.
(* Goal: @eq (option B) (map_add a (@fold_right (forall _ : A, option B) (forall _ : A, option B) map_add empty_map l) k) (@Some B v) *)
      intro; subst.
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
      apply join_Bot in Hsh as []; auto.
  - intros (? & [] & ?); simpl in *.
    destruct (fst x) as [[]|]; [|contradiction].
    split; [simpl | constructor].
    rewrite map_disj_join_spec in *; tauto.
Qed.

Definition hist_incl (h : hist_part) l := forall t e, h t = Some e -> nth_error l t = Some e.

Definition hist_list (h : hist_part) l := forall t e, h t = Some e <-> nth_error l t = Some e.

Lemma hist_list_inj : forall h l1 l2 (Hl1 : hist_list h l1) (Hl2 : hist_list h l2), l1 = l2.
Proof.
(* Goal: forall (h : forall _ : nat, option hist_el) (l1 l2 : list hist_el) (_ : hist_list h l1) (_ : hist_list h l2), @eq (list hist_el) l1 l2 *)
  unfold hist_list; intros; apply list_nth_error_eq.
(* Goal: forall j : nat, @eq (option hist_el) (@nth_error hist_el l1 j) (@nth_error hist_el l2 j) *)
  intro j; specialize (Hl1 j); specialize (Hl2 j).
(* Goal: @eq (option hist_el) (@nth_error hist_el l1 j) (@nth_error hist_el l2 j) *)
  destruct (nth_error l1 j).
  - symmetry; rewrite <- Hl2, Hl1; auto.
  - destruct (nth_error l2 j); auto.
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
    specialize (Hl2 h0); rewrite Hl1 in Hl2; tauto.
Qed.

Lemma hist_list_nil_inv1 : forall l, hist_list empty_map l -> l = [].
Proof.
(* Goal: forall P Q : mpred, @derives mpred Nveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (weak_view_shift P Q) (@emp mpred Nveric Sveric)) P) (@bupd mpred own.gname preds Nveric Sveric Bveric Q) *)
  unfold hist_list; intros.
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
  destruct l; auto.
(* Goal: @eq (list hist_el) (@cons hist_el h l) (@nil hist_el) *)
  specialize (H O h); destruct H as [_ H]; specialize (H eq_refl); discriminate.
Qed.

Lemma hist_list_nil_inv2 : forall h, hist_list h [] -> h = empty_map.
Proof.
(* Goal: forall P Q : mpred, @derives mpred Nveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (weak_view_shift P Q) (@emp mpred Nveric Sveric)) P) (@bupd mpred own.gname preds Nveric Sveric Bveric Q) *)
  unfold hist_list; intros.
(* Goal: @eq (forall _ : nat, option hist_el) h (@empty_map nat hist_el) *)
  extensionality t.
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
  specialize (H t); destruct (h t); auto.
(* Goal: @eq (option hist_el) (@Some hist_el h0) (@empty_map nat hist_el t) *)
  destruct (H h0) as [H' _].
(* Goal: @eq (option hist_el) (@Some hist_el h0) (@empty_map nat hist_el t) *)
  specialize (H' eq_refl); rewrite nth_error_nil in H'; discriminate.
Qed.

Definition ghost_ref l g := EX hr : hist_part, !!(hist_list hr l) &&
  own(RA := ref_PCM map_disj_PCM) g (None, Some hr) NoneP.

Lemma hist_next : forall h l (Hlist : hist_list h l), h (length l) = None.
Proof.
(* Goal: forall P Q : mpred, @derives mpred Nveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (weak_view_shift P Q) (@emp mpred Nveric Sveric)) P) (@bupd mpred own.gname preds Nveric Sveric Bveric Q) *)
  intros.
(* Goal: @eq (option hist_el) (h (@Datatypes.length hist_el l)) (@None hist_el) *)
  specialize (Hlist (length l)).
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
  destruct (h (length l)); auto.
(* Goal: @eq (option hist_el) (@Some hist_el h0) (@None hist_el) *)
  destruct (Hlist h0) as [H' _].
(* Goal: @eq (option hist_el) (@Some hist_el h0) (@None hist_el) *)
  pose proof (nth_error_Some l (length l)) as (Hlt & _).
(* Goal: @eq (option hist_el) (@Some hist_el h0) (@None hist_el) *)
  lapply Hlt; [omega|].
(* Goal: not (@eq (option hist_el) (@nth_error hist_el l (@Datatypes.length hist_el l)) (@None hist_el)) *)
  rewrite H' by auto; discriminate.
Qed.

Definition ghost_hist_ref sh (h r : hist_part) g :=
  own(RA := ref_PCM map_disj_PCM) g (Some (sh, h), Some r) NoneP.

Lemma hist_add : forall (sh : share) (h h' : hist_part) e p t' (Hfresh : h' t' = None),
  ghost_hist_ref sh h h' p |-- |==> ghost_hist_ref sh (map_upd h t' e) (map_upd h' t' e) p.
Proof.
(* Goal: forall P Q : mpred, @derives mpred Nveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (weak_view_shift P Q) (@emp mpred Nveric Sveric)) P) (@bupd mpred own.gname preds Nveric Sveric Bveric Q) *)
  intros.
(* Goal: @derives mpred Nveric (ghost_hist_ref sh h h' p) (@bupd mpred own.gname preds Nveric Sveric Bveric (ghost_hist_ref sh (@map_upd nat hist_el nat_eq_dec h t' e) (@map_upd nat hist_el nat_eq_dec h' t' e) p)) *)
  erewrite (add_andp (ghost_hist_ref _ _ _ _)) by apply own_valid.
(* Goal: @derives mpred Nveric (@andp mpred Nveric (ghost_hist_ref sh h h' p) (@prop mpred Nveric (@valid (ref_PCM (@map_disj_PCM nat hist_el)) (@pair (option (prod share (forall _ : nat, option hist_el))) (option (forall _ : nat, option hist_el)) (@Some (prod share (forall _ : nat, option hist_el)) (@pair share (forall _ : nat, option hist_el) sh h)) (@Some (forall _ : nat, option hist_el) h'))))) (@bupd mpred own.gname preds Nveric Sveric Bveric (ghost_hist_ref sh (@map_upd nat hist_el nat_eq_dec h t' e) (@map_upd nat hist_el nat_eq_dec h' t' e) p)) *)
  Intros.
  destruct H as [? Hcomp]; simpl in *.
(* Goal: @derives mpred Nveric (ghost_hist_ref sh h h' p) (@bupd mpred own.gname preds Nveric Sveric Bveric (ghost_hist_ref sh (@map_upd nat hist_el nat_eq_dec h t' e) (@map_upd nat hist_el nat_eq_dec h' t' e) p)) *)
  rewrite completable_alt in Hcomp; destruct Hcomp as [_ Hcomp].
(* Goal: @derives mpred Nveric (ghost_hist_ref sh h h' p) (@bupd mpred own.gname preds Nveric Sveric Bveric (ghost_hist_ref sh (@map_upd nat hist_el nat_eq_dec h t' e) (@map_upd nat hist_el nat_eq_dec h' t' e) p)) *)
  apply (ref_add(P := map_disj_PCM)) with (b := fun k => if eq_dec k t' then Some e else None).
  - repeat intro.
(* Goal: match c k with | Some v => match (if @eq_dec nat nat_eq_dec k t' then @Some hist_el e else @None hist_el) with | Some b => False | None => @eq (option hist_el) (@map_upd nat hist_el nat_eq_dec c t' e k) (@Some hist_el v) end | None => match (if @eq_dec nat nat_eq_dec k t' then @Some hist_el e else @None hist_el) with | Some v => @eq (option hist_el) (@map_upd nat hist_el nat_eq_dec c t' e k) (@Some hist_el v) | None => @eq (option hist_el) (@map_upd nat hist_el nat_eq_dec c t' e k) (@None hist_el) end end *)
    unfold map_upd.
(* Goal: match h k with | Some v => match (if @eq_dec nat nat_eq_dec k t' then @Some hist_el e else @None hist_el) with | Some b => False | None => @eq (option hist_el) (if @eq_dec nat nat_eq_dec k t' then @Some hist_el e else h k) (@Some hist_el v) end | None => match (if @eq_dec nat nat_eq_dec k t' then @Some hist_el e else @None hist_el) with | Some v => @eq (option hist_el) (if @eq_dec nat nat_eq_dec k t' then @Some hist_el e else h k) (@Some hist_el v) | None => @eq (option hist_el) (if @eq_dec nat nat_eq_dec k t' then @Some hist_el e else h k) (@None hist_el) end end *)
    if_tac; [|destruct (h k); auto].
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
    subst; destruct (h t') eqn: Hh; auto.
(* Goal: False *)
    if_tac in Hcomp; [congruence|].
(* Goal: @eq B v1 v2 *)
    apply Hcomp in Hh; congruence.
  - repeat intro.
(* Goal: match c k with | Some v => match (if @eq_dec nat nat_eq_dec k t' then @Some hist_el e else @None hist_el) with | Some b => False | None => @eq (option hist_el) (@map_upd nat hist_el nat_eq_dec c t' e k) (@Some hist_el v) end | None => match (if @eq_dec nat nat_eq_dec k t' then @Some hist_el e else @None hist_el) with | Some v => @eq (option hist_el) (@map_upd nat hist_el nat_eq_dec c t' e k) (@Some hist_el v) | None => @eq (option hist_el) (@map_upd nat hist_el nat_eq_dec c t' e k) (@None hist_el) end end *)
    unfold map_upd.
(* Goal: match h' k with | Some v => match (if @eq_dec nat nat_eq_dec k t' then @Some hist_el e else @None hist_el) with | Some b => False | None => @eq (option hist_el) (if @eq_dec nat nat_eq_dec k t' then @Some hist_el e else h' k) (@Some hist_el v) end | None => match (if @eq_dec nat nat_eq_dec k t' then @Some hist_el e else @None hist_el) with | Some v => @eq (option hist_el) (if @eq_dec nat nat_eq_dec k t' then @Some hist_el e else h' k) (@Some hist_el v) | None => @eq (option hist_el) (if @eq_dec nat nat_eq_dec k t' then @Some hist_el e else h' k) (@None hist_el) end end *)
    if_tac; [|destruct (h' k); auto].
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
    subst; rewrite Hfresh; auto.
  - intros ?? Hsub.
(* Goal: forall (P Q : mpred) (n : nat), @eq (@pred rmap ag_rmap) (approx n (weak_view_shift P Q)) (approx n (weak_view_shift P (approx n Q))) *)
    exists (map_upd c t' e); repeat intro.
(* Goal: match c k with | Some v => match (if @eq_dec nat nat_eq_dec k t' then @Some hist_el e else @None hist_el) with | Some b => False | None => @eq (option hist_el) (@map_upd nat hist_el nat_eq_dec c t' e k) (@Some hist_el v) end | None => match (if @eq_dec nat nat_eq_dec k t' then @Some hist_el e else @None hist_el) with | Some v => @eq (option hist_el) (@map_upd nat hist_el nat_eq_dec c t' e k) (@Some hist_el v) | None => @eq (option hist_el) (@map_upd nat hist_el nat_eq_dec c t' e k) (@None hist_el) end end *)
    unfold map_upd.
(* Goal: match c k with | Some v => match (if @eq_dec nat nat_eq_dec k t' then @Some hist_el e else @None hist_el) with | Some b => False | None => @eq (option hist_el) (if @eq_dec nat nat_eq_dec k t' then @Some hist_el e else c k) (@Some hist_el v) end | None => match (if @eq_dec nat nat_eq_dec k t' then @Some hist_el e else @None hist_el) with | Some v => @eq (option hist_el) (if @eq_dec nat nat_eq_dec k t' then @Some hist_el e else c k) (@Some hist_el v) | None => @eq (option hist_el) (if @eq_dec nat nat_eq_dec k t' then @Some hist_el e else c k) (@None hist_el) end end *)
    if_tac; [|destruct (c k); auto].
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
    subst; destruct (c t') eqn: Hc; auto.
(* Goal: False *)
    destruct Hsub as [x Hsub]; hnf in Hsub.
(* Goal: False *)
    specialize (Hsub t'); rewrite Hc in Hsub.
(* Goal: @eq B v1 v2 *)
    destruct (x t'); congruence.
Qed.

Lemma hist_incl_nil : forall h, hist_incl empty_map h.
Proof.
(* Goal: forall h : list hist_el, hist_incl (@empty_map nat hist_el) h *)
  repeat intro; discriminate.
Qed.

Lemma hist_list_nil : hist_list empty_map [].
Proof.
(* Goal: iff (@eq (option hist_el) (@None hist_el) (@Some hist_el e)) (@eq (option hist_el) (@nth_error hist_el l t) (@Some hist_el e)) *)
  split; [discriminate|].
(* Goal: forall _ : @eq (option hist_el) (@nth_error hist_el (@nil hist_el) t) (@Some hist_el e), @eq (option hist_el) (@empty_map nat hist_el t) (@Some hist_el e) *)
  rewrite nth_error_nil; discriminate.
Qed.

Lemma hist_list_snoc : forall h l e, hist_list h l ->
  hist_list (map_upd h (length l) e) (l ++ [e]).
Proof.
(* Goal: and (not (@eq share (Share.comp sh) Share.bot)) (and (@join share Share.Join_ba sh (Share.comp sh) Tsh) (@join (forall _ : nat, option hist_el) (@map_disj_join nat hist_el) h h' hr)) *)
  unfold hist_list, map_upd; split.
  - if_tac.
    + intro X; inv X.
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
      rewrite nth_error_app2, minus_diag; auto.
    + rewrite H.
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
      intro X; rewrite nth_error_app1; auto.
      rewrite <- nth_error_Some, X; discriminate.
  - if_tac.
    + subst; rewrite nth_error_app2, minus_diag; auto.
    + intro X; apply H; rewrite nth_error_app1 in X; auto.
      assert (t < length (l ++ [e]))%nat; [|rewrite app_length in *; simpl in *; omega].
      rewrite <- nth_error_Some, X; discriminate.
Qed.

Lemma hist_sub_list_incl : forall sh h h' l (Hsub : hist_sub sh h h') (Hlist : hist_list h' l),
  hist_incl h l.
Proof.
(* Goal: forall P Q : mpred, @derives mpred Nveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (weak_view_shift P Q) (@emp mpred Nveric Sveric)) P) (@bupd mpred own.gname preds Nveric Sveric Bveric Q) *)
  unfold hist_list, hist_incl; intros.
(* Goal: @eq (option hist_el) (@nth_error hist_el l t) (@Some hist_el e) *)
  apply Hlist.
(* Goal: @eq (option hist_el) (h' t) (@Some hist_el e) *)
  destruct Hsub.
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
  destruct (eq_dec sh Tsh); subst; auto.
Qed.

Lemma hist_sub_Tsh : forall h h', hist_sub Tsh h h' <-> (h = h').
Proof.
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
  intros; unfold hist_sub; rewrite eq_dec_refl; repeat split; auto; tauto.
Qed.

Lemma hist_ref_join : forall sh h l p, sh <> Share.bot ->
  ghost_hist sh h p * ghost_ref l p =
  EX h' : hist_part, !!(hist_list h' l /\ hist_sub sh h h') && ghost_hist_ref sh h h' p.
Proof.
(* Goal: @eq mpred (@exp mpred Nveric (@G map_PCM) (fun v : @G map_PCM => @andp mpred Nveric (@prop mpred Nveric (@join (@G map_PCM) (@Join_G map_PCM) m1 m2 v)) (@ghost_snap map_PCM map_incl fmap_order v p))) (@andp mpred Nveric (@prop mpred Nveric (compatible m1 m2)) (@ghost_snap map_PCM map_incl fmap_order (map_add m1 m2) p)) *)
  unfold ghost_hist, ghost_ref; intros; apply pred_ext.
  - Intros hr; Exists hr.
    erewrite own_op_gen.
    + Intros; apply andp_right, derives_refl; apply prop_right.
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
      split; auto.
      destruct H1 as ([g] & [H1 H2] & [? Hcompat]); simpl in *.
      destruct g as [[]|]; [|contradiction].
      inv H1; inv H2.
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
      apply completable_alt; auto.
    + split; simpl; auto; constructor.
  - Intros h'; Exists h'; entailer!.
    erewrite <- own_op; [apply derives_refl|].
(* Goal: hist_list' (@map_upd nat hist_el nat_eq_dec h0 (@Datatypes.length hist_el l) x) (@app hist_el l (@cons hist_el x (@nil hist_el))) *)
(* Goal: @eq (forall _ : nat, option hist_el) (@map_upd nat hist_el nat_eq_dec h0 (@Datatypes.length hist_el l) x) h *)
    split; simpl; auto; constructor.
Qed.

Corollary hist_ref_join_nil : forall sh p, sh <> Share.bot ->
  ghost_hist sh empty_map p * ghost_ref [] p = ghost_hist_ref sh empty_map empty_map p.
Proof.
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
  intros; rewrite hist_ref_join by auto.
  apply pred_ext; entailer!.
  - apply hist_list_nil_inv2 in H0; subst; auto.
  - Exists (fun _ : nat => @None hist_el); apply andp_right, derives_refl.
(* Goal: @derives mpred Nveric (ghost_hist_ref sh (@empty_map nat hist_el) (@empty_map nat hist_el) p) (@prop mpred Nveric (and (hist_list (fun _ : nat => @None hist_el) (@nil hist_el)) (hist_sub sh (@empty_map nat hist_el) (fun _ : nat => @None hist_el)))) *)
    apply prop_right; split; [apply hist_list_nil|].
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
    split; auto.
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
    if_tac; auto.
Qed.

Lemma hist_ref_incl : forall sh h h' p, sh <> Share.bot ->
  ghost_hist sh h p * ghost_ref h' p |-- !!hist_incl h h'.
Proof.
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
  intros; rewrite hist_ref_join by auto.
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
  Intros l; eapply prop_right, hist_sub_list_incl; eauto.
Qed.

Lemma hist_add' : forall sh h h' e p, sh <> Share.bot ->
  ghost_hist sh h p * ghost_ref h' p |-- |==>
  ghost_hist sh (map_upd h (length h') e) p * ghost_ref (h' ++ [e]) p.
Proof.
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
  intros; rewrite !hist_ref_join by auto.
  Intros hr.
  eapply derives_trans; [apply hist_add|].
(* Goal: @compatible nat hist_el (@map_upd nat hist_el nat_eq_dec h2 t e) h *)
  { apply hist_next; eauto. }
  apply bupd_mono.
  Exists (map_upd hr (length h') e); apply andp_right, derives_refl.
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
  apply prop_right; split; [apply hist_list_snoc | apply hist_sub_upd]; auto.
Qed.

Definition newer (l : hist_part) t := forall t', l t' <> None -> (t' < t)%nat.

Lemma newer_trans : forall l t1 t2, newer l t1 -> (t1 <= t2)%nat -> newer l t2.
Proof.
(* Goal: forall (P Q : mpred) (n : nat), @eq (@pred rmap ag_rmap) (approx n (weak_view_shift P Q)) (approx n (weak_view_shift P (approx n Q))) *)
  repeat intro.
(* Goal: lt t' t2 *)
  specialize (H _ H1); omega.
Qed.

Corollary newer_upd : forall l t1 e t2, newer l t1 -> (t1 < t2)%nat ->
  newer (map_upd l t1 e) t2.
Proof.
(* Goal: forall P Q : mpred, @derives mpred Nveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (weak_view_shift P Q) (@emp mpred Nveric Sveric)) P) (@bupd mpred own.gname preds Nveric Sveric Bveric Q) *)
  unfold newer, map_upd; intros.
(* Goal: lt t' t2 *)
  destruct (eq_dec t' t1); [omega|].
(* Goal: lt t' t2 *)
  eapply newer_trans; eauto; omega.
Qed.

Lemma newer_over : forall h t t', newer h t -> (t <= t')%nat -> h t' = None.
Proof.
(* Goal: forall P Q : mpred, @derives mpred Nveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (weak_view_shift P Q) (@emp mpred Nveric Sveric)) P) (@bupd mpred own.gname preds Nveric Sveric Bveric Q) *)
  intros.
(* Goal: lt t' (@Datatypes.length hist_el l) *)
  specialize (H t').
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
  destruct (h t'); auto.
(* Goal: @eq (option hist_el) (@Some hist_el h0) (@None hist_el) *)
  lapply H; [omega | discriminate].
Qed.

Corollary newer_out : forall h t, newer h t -> h t = None.
Proof.
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
  intros; eapply newer_over; eauto.
Qed.

Lemma add_new_inj : forall h h' t t' v v' (Ht : newer h t) (Ht' : newer h' t'),
  map_upd h t v = map_upd h' t' v' -> h = h' /\ t = t' /\ v = v'.
Proof.
(* Goal: forall P Q : mpred, @derives mpred Nveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (weak_view_shift P Q) (@emp mpred Nveric Sveric)) P) (@bupd mpred own.gname preds Nveric Sveric Bveric Q) *)
  intros.
  pose proof (equal_f H t) as Hh.
  pose proof (equal_f H t') as Hh'.
  pose proof (newer_out _ _ Ht) as Hout.
  pose proof (newer_out _ _ Ht') as Hout'.
  unfold map_upd in Hh, Hh'.
  rewrite eq_dec_refl in Hh, Hh'.
  if_tac in Hh.
  - inv Hh; clear Hh'.
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
    repeat split; auto.
    erewrite <- (map_sub_upd h) by (eapply newer_out; eauto).
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
    rewrite H, map_sub_upd; auto.
  - rewrite if_false in Hh' by auto.
    lapply (Ht t'); [|rewrite Hh'; discriminate].
    lapply (Ht' t); [|rewrite <- Hh; discriminate].
    omega.
Qed.

Lemma hist_incl_lt : forall h l, hist_incl h l -> newer h (length l).
Proof.
(* Goal: forall (P Q : mpred) (n : nat), @eq (@pred rmap ag_rmap) (approx n (weak_view_shift P Q)) (approx n (weak_view_shift P (approx n Q))) *)
  unfold hist_incl; repeat intro.
(* Goal: lt t' (@Datatypes.length hist_el l) *)
  specialize (H t').
(* Goal: lt t' (@Datatypes.length hist_el l) *)
  destruct (h t'); [|contradiction].
(* Goal: lt t' (@Datatypes.length hist_el l) *)
  specialize (H _ eq_refl).
  rewrite <- nth_error_Some, H; discriminate.
Qed.

Corollary hist_list_lt : forall h l, hist_list h l -> newer h (length l).
Proof.
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
  intros; apply hist_incl_lt; repeat intro; apply H; auto.
Qed.

(* We want to be able to remove irrelevant operations from a history, leading to a slightly weaker
   correspondence between history and list of operations. *)
Inductive hist_list' : hist_part -> list hist_el -> Prop :=
| hist_list'_nil : hist_list' empty_map []
| hist_list'_snoc : forall h l t e (Hlast : newer h t) (Hrest : hist_list' h l),
    hist_list' (map_upd h t e) (l ++ [e]).
Hint Resolve hist_list'_nil.

Lemma hist_list'_in : forall h l (Hl : hist_list' h l) e, (exists t, h t = Some e) <-> In e l.
Proof.
(* Goal: forall (h : forall _ : nat, option hist_el) (le : list hist_el) (h' : forall _ : nat, option hist_el) (_ : add_events h le h'), @ex (forall _ : nat, option hist_el) (fun h2 : forall _ : nat, option hist_el => and (@eq (forall _ : nat, option hist_el) h' (@map_add nat hist_el h h2)) (forall (t : nat) (e : hist_el) (_ : @eq (option hist_el) (h2 t) (@Some hist_el e)), and (newer h t) (@In hist_el e le))) *)
  induction 1.
  - split; [intros (? & ?); discriminate | contradiction].
  - intro; subst; split.
    + unfold map_upd; intros (? & Hin); rewrite in_app in *.
(* Goal: or (@In hist_el e0 l) (@In hist_el e0 (@cons hist_el e (@nil hist_el))) *)
      destruct (eq_dec x t); [inv Hin; simpl; auto|].
      rewrite <- IHHl; eauto.
    + rewrite in_app; intros [Hin | [Heq | ?]]; [| inv Heq | contradiction].
      * rewrite <- IHHl in Hin; destruct Hin as (? & ?).
(* Goal: @ex nat (fun t0 : nat => @eq (option hist_el) (@map_upd nat hist_el nat_eq_dec h t e t0) (@Some hist_el e0)) *)
        apply newer_out in Hlast.
(* Goal: @eq B v1 v2 *)
        unfold map_upd; exists x; if_tac; auto; congruence.
      * unfold map_upd; eexists; apply eq_dec_refl.
Qed.

Lemma hist_list_weak : forall l h (Hl : hist_list h l), hist_list' h l.
Proof.
(* Goal: forall P Q : mpred, @derives mpred Nveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (weak_view_shift P Q) (@emp mpred Nveric Sveric)) P) (@bupd mpred own.gname preds Nveric Sveric Bveric Q) *)
  induction l using rev_ind; intros.
  - apply hist_list_nil_inv2 in Hl; subst; auto.
  - destruct (Hl (length l) x) as (_ & H); exploit H.
(* Goal: @compatible nat hist_el (@map_upd nat hist_el nat_eq_dec h2 t e) h *)
    { rewrite nth_error_app2, minus_diag by omega; auto. }
(* Goal: forall _ : @eq (option hist_el) (h (@Datatypes.length hist_el l)) (@Some hist_el x), hist_list' h (@app hist_el l (@cons hist_el x (@nil hist_el))) *)
    intro Hx.
(* Goal: hist_list' h (@app hist_el l (@cons hist_el x (@nil hist_el))) *)
    set (h0 := fun k => if eq_dec k (length l) then None else h k).
(* Goal: hist_list' h (@app hist_el l (@cons hist_el x (@nil hist_el))) *)
    replace h with (map_upd h0 (length l) x).
(* Goal: hist_list' (@map_upd nat hist_el nat_eq_dec h0 (@Datatypes.length hist_el l) x) (@app hist_el l (@cons hist_el x (@nil hist_el))) *)
(* Goal: @eq (forall _ : nat, option hist_el) (@map_upd nat hist_el nat_eq_dec h0 (@Datatypes.length hist_el l) x) h *)
    constructor.
    + pose proof (hist_list_lt _ _ Hl) as Hn.
(* Goal: newer h0 (@Datatypes.length hist_el l) *)
      intro t; specialize (Hn t).
(* Goal: forall _ : not (@eq (option hist_el) (h0 t) (@None hist_el)), lt t (@Datatypes.length hist_el l) *)
      subst h0; simpl; if_tac; [contradiction|].
      intro X; specialize (Hn X); rewrite app_length in Hn; simpl in Hn; omega.
    + apply IHl.
(* Goal: hist_list h0 l *)
      intros t e; specialize (Hl t e).
(* Goal: forall _ : @eq (option hist_el) (@nth_error hist_el (@app hist_el l (@cons hist_el e (@nil hist_el))) t) (@Some hist_el e0), @eq (option hist_el) (if @eq_dec nat nat_eq_dec t (@Datatypes.length hist_el l) then @Some hist_el e else h t) (@Some hist_el e0) *)
      subst h0; simpl; if_tac.
      * split; [discriminate|].
        intro X; assert (t < length l)%nat by (rewrite <- nth_error_Some, X; discriminate); omega.
      * rewrite Hl; destruct (lt_dec t (length l)).
(* Goal: @compatible nat hist_el (@map_upd nat hist_el nat_eq_dec h2 t e) h *)
        { rewrite nth_error_app1 by auto; reflexivity. }
(* Goal: iff (@eq (option hist_el) (@nth_error hist_el (@app hist_el l (@cons hist_el x (@nil hist_el))) t) (@Some hist_el e)) (@eq (option hist_el) (@nth_error hist_el l t) (@Some hist_el e)) *)
        split; intro X.
        -- assert (t < length (l ++ [x]))%nat by (rewrite <- nth_error_Some, X; discriminate);
             rewrite app_length in *; simpl in *; omega.
        -- assert (t < length l)%nat by (rewrite <- nth_error_Some, X; discriminate); contradiction.
(* Goal: match empty_map k with | Some v => match t k with | Some b => False | None => @eq (option B) (t k) (@Some B v) end | None => match t k with | Some v => @eq (option B) (t k) (@Some B v) | None => @eq (option B) (t k) (@None B) end end *)
    + unfold map_upd; subst h0; simpl.
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
      extensionality k'; if_tac; subst; auto.
Qed.

Lemma hist_list'_add : forall h1 h2 (l : list hist_el) (Hdisj : disjoint h1 h2), hist_list' (map_add h1 h2) l ->
  exists l1 l2, Permutation l (l1 ++ l2) /\ hist_list' h1 l1 /\ hist_list' h2 l2.
Proof.
(* Goal: forall P Q : mpred, @derives mpred Nveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (weak_view_shift P Q) (@emp mpred Nveric Sveric)) P) (@bupd mpred own.gname preds Nveric Sveric Bveric Q) *)
  intros.
  remember (map_add h1 h2) as h.
(* Goal: forall P Q : mpred, @derives mpred Nveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (weak_view_shift P Q) (@emp mpred Nveric Sveric)) P) (@bupd mpred own.gname preds Nveric Sveric Bveric Q) *)
  revert dependent h2; revert h1; induction H; intros.
  - exists [], []; split; [reflexivity|].
    assert (h1 = empty_map /\ h2 = empty_map) as [].
(* Goal: @compatible nat hist_el (@map_upd nat hist_el nat_eq_dec h2 t e) h *)
    { split; extensionality k; apply equal_f with (x := k) in Heqh; unfold map_add in Heqh;
        destruct (h1 k); auto; discriminate. }
(* Goal: hist_list' (@map_upd nat hist_el nat_eq_dec h0 (@Datatypes.length hist_el l) x) (@app hist_el l (@cons hist_el x (@nil hist_el))) *)
(* Goal: @eq (forall _ : nat, option hist_el) (@map_upd nat hist_el nat_eq_dec h0 (@Datatypes.length hist_el l) x) h *)
    subst; split; constructor.
  - pose proof (equal_f Heqh t) as Ht.
    unfold map_upd, map_add in Ht.
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
    rewrite eq_dec_refl in Ht by auto.
    destruct (h1 t) eqn: Hh1.
    + inv Ht.
      destruct (IHhist_list' (map_sub h1 t) h2) as (l1 & l2 & ? & ? & ?).
(* Goal: @compatible nat hist_el (@map_upd nat hist_el nat_eq_dec h2 t e) h *)
      { apply disjoint_sub; auto. }
(* Goal: @compatible nat hist_el (@map_upd nat hist_el nat_eq_dec h2 t e) h *)
      { extensionality k.
        apply equal_f with (x := k) in Heqh.
        unfold map_upd, map_sub, map_add in *.
(* Goal: @eq (option B) (map_add a (@fold_right (forall _ : A, option B) (forall _ : A, option B) map_add empty_map l) k) (@Some B v) *)
        if_tac; auto; subst.
(* Goal: @ex nat (fun t0 : nat => @eq (option hist_el) (@map_upd nat hist_el nat_eq_dec h t e t0) (@Some hist_el e0)) *)
        apply newer_out in Hlast.
        apply Hdisj in Hh1; congruence. }
      exists (l1 ++ [h0]), l2; repeat split; auto.
      * etransitivity; [|apply Permutation_app_comm].
        rewrite app_assoc; apply Permutation_app_tail.
(* Goal: ord v1 c *)
        etransitivity; eauto.
        apply Permutation_app_comm.
      * erewrite <- (map_upd_sub h1 t) by eauto.
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
        constructor; auto.
(* Goal: forall (P Q : mpred) (n : nat), @eq (@pred rmap ag_rmap) (approx n (weak_view_shift P Q)) (approx n (weak_view_shift P (approx n Q))) *)
        repeat intro.
        unfold map_sub in *.
        apply equal_f with (x := t') in Heqh.
        unfold map_upd, map_add in Heqh.
        apply Hlast.
        destruct (eq_dec _ _); [contradiction|].
        destruct (h1 t'); [congruence | contradiction].
    + destruct (IHhist_list' h1 (map_sub h2 t)) as (l1 & l2 & ? & ? & ?).
(* Goal: @compatible nat hist_el (@map_upd nat hist_el nat_eq_dec h2 t e) h *)
      { symmetry; apply disjoint_sub; symmetry; auto. }
(* Goal: @compatible nat hist_el (@map_upd nat hist_el nat_eq_dec h2 t e) h *)
      { extensionality k.
        apply equal_f with (x := k) in Heqh.
        unfold map_upd, map_sub, map_add in *.
(* Goal: @eq (option B) (map_add a (@fold_right (forall _ : A, option B) (forall _ : A, option B) map_add empty_map l) k) (@Some B v) *)
        if_tac; auto; subst.
(* Goal: @ex nat (fun t0 : nat => @eq (option hist_el) (@map_upd nat hist_el nat_eq_dec h t e t0) (@Some hist_el e0)) *)
        apply newer_out in Hlast.
        rewrite Hh1; auto. }
      exists l1, (l2 ++ [e]); repeat split; auto.
      * rewrite app_assoc; apply Permutation_app_tail; auto.
      * erewrite <- (map_upd_sub h2 t) by eauto.
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
        constructor; auto.
(* Goal: forall (P Q : mpred) (n : nat), @eq (@pred rmap ag_rmap) (approx n (weak_view_shift P Q)) (approx n (weak_view_shift P (approx n Q))) *)
        repeat intro.
        unfold map_sub in *.
        apply equal_f with (x := t') in Heqh.
        unfold map_upd, map_add in Heqh.
        apply Hlast.
        destruct (eq_dec _ _); [contradiction|].
(* Goal: @eq B v1 v2 *)
        destruct (h1 t'); congruence.
Qed.

Lemma ghost_hist_init : @valid (ref_PCM (@map_disj_PCM nat hist_el)) (Some (Tsh, empty_map), Some empty_map).
Proof.
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
  split; simpl; auto.
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
  rewrite completable_alt; split; auto.
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
  rewrite eq_dec_refl; auto.
Qed.

Inductive add_events h : list hist_el -> hist_part -> Prop :=
| add_events_nil : add_events h [] h
| add_events_snoc : forall le h' t e (Hh' : add_events h le h') (Ht : newer h' t),
    add_events h (le ++ [e]) (map_upd h' t e).
Hint Resolve add_events_nil.

Lemma add_events_1 : forall h t e (Ht : newer h t), add_events h [e] (map_upd h t e).
Proof.
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
  intros; apply (add_events_snoc _ []); auto.
Qed.

Lemma add_events_trans : forall h le h' le' h'' (H1 : add_events h le h') (H2 : add_events h' le' h''),
  add_events h (le ++ le') h''.
Proof.
(* Goal: forall (h : forall _ : nat, option hist_el) (le : list hist_el) (h' : forall _ : nat, option hist_el) (le' : list hist_el) (h'' : forall _ : nat, option hist_el) (_ : add_events h le h') (_ : add_events h' le' h''), add_events h (@app hist_el le le') h'' *)
  induction 2.
  - rewrite app_nil_r; auto.
  - rewrite app_assoc; constructor; auto.
Qed.

Lemma add_events_add : forall h le h', add_events h le h' ->
  exists h2, h' = map_add h h2 /\ forall t e, h2 t = Some e -> newer h t /\ In e le.
Proof.
(* Goal: forall (h : forall _ : nat, option hist_el) (le : list hist_el) (h' : forall _ : nat, option hist_el) (_ : add_events h le h'), @ex (forall _ : nat, option hist_el) (fun h2 : forall _ : nat, option hist_el => and (@eq (forall _ : nat, option hist_el) h' (@map_add nat hist_el h h2)) (forall (t : nat) (e : hist_el) (_ : @eq (option hist_el) (h2 t) (@Some hist_el e)), and (newer h t) (@In hist_el e le))) *)
  induction 1.
  - eexists; rewrite map_add_empty; split; auto; discriminate.
  - destruct IHadd_events as (h2 & ? & Hh2); subst.
(* Goal: @ex (forall _ : nat, option hist_el) (fun h3 : forall _ : nat, option hist_el => and (@eq (forall _ : nat, option hist_el) (@map_upd nat hist_el nat_eq_dec (@map_add nat hist_el h h2) t e) (@map_add nat hist_el h h3)) (forall (t : nat) (e0 : hist_el) (_ : @eq (option hist_el) (h3 t) (@Some hist_el e0)), and (newer h t) (@In hist_el e0 (@app hist_el le (@cons hist_el e (@nil hist_el)))))) *)
    assert (compatible h h2).
(* Goal: @compatible nat hist_el (@map_upd nat hist_el nat_eq_dec h2 t e) h *)
    { repeat intro.
(* Goal: @eq hist_el v1 v2 *)
      destruct (Hh2 _ _ H1) as [Hk _].
      specialize (Hk k); lapply Hk; [omega | congruence]. }
(* Goal: @ex (forall _ : nat, option hist_el) (fun h3 : forall _ : nat, option hist_el => and (@eq (forall _ : nat, option hist_el) (@map_upd nat hist_el nat_eq_dec (@map_add nat hist_el h h2) t e) (@map_add nat hist_el h h3)) (forall (t : nat) (e0 : hist_el) (_ : @eq (option hist_el) (h3 t) (@Some hist_el e0)), and (newer h t) (@In hist_el e0 (@app hist_el le (@cons hist_el e (@nil hist_el)))))) *)
    assert (newer h t).
(* Goal: @compatible nat hist_el (@map_upd nat hist_el nat_eq_dec h2 t e) h *)
    { repeat intro; apply Ht.
(* Goal: not (@eq (option hist_el) (@map_add nat hist_el h h2 t') (@None hist_el)) *)
      unfold map_add.
      destruct (h t'); auto. }
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
    rewrite map_add_comm, map_add_upd, map_add_comm; auto.
(* Goal: forall P Q : mpred, @derives mpred Nveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (weak_view_shift P Q) (@emp mpred Nveric Sveric)) P) (@bupd mpred own.gname preds Nveric Sveric Bveric Q) *)
    eexists; split; eauto; intros.
    unfold map_upd in *.
(* Goal: match empty_map k with | Some v => match t k with | Some b => False | None => @eq (option B) (t k) (@Some B v) end | None => match t k with | Some v => @eq (option B) (t k) (@Some B v) | None => @eq (option B) (t k) (@None B) end end *)
    rewrite in_app; simpl.
(* Goal: and (newer h t0) (or (@In hist_el e0 le) (or (@eq hist_el e e0) False)) *)
(* Goal: @compatible nat hist_el (@map_upd nat hist_el nat_eq_dec h2 t e) h *)
    destruct (eq_dec t0 t); [inv H2; auto|].
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
    destruct (Hh2 _ _ H2); auto.
(* Goal: @compatible nat hist_el (@map_upd nat hist_el nat_eq_dec h2 t e) h *)
    { apply compatible_upd; [symmetry; auto|].
(* Goal: @eq (option hist_el) (h t) (@None hist_el) *)
      specialize (H1 t).
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
      destruct (h t); auto.
      lapply H1; [omega | discriminate]. }
Qed.

Corollary add_events_dom : forall h le h' t e, add_events h le h' -> h' t = Some e ->
  h t = Some e \/ In e le.
Proof.
(* Goal: @eq (option B) (map_add a (@fold_right (forall _ : A, option B) (forall _ : A, option B) map_add empty_map l) k) (@Some B v) *)
  intros; apply add_events_add in H as (? & ? & Hh2); subst.
(* Goal: or (@eq (option hist_el) (h t) (@Some hist_el e)) (@In hist_el e le) *)
  unfold map_add in H0.
(* Goal: or (@eq (option hist_el) (h t) (@Some hist_el e)) (@In hist_el e le) *)
  destruct (h t); [inv H0; auto|].
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
  destruct (Hh2 _ _ H0); auto.
Qed.

Corollary add_events_incl : forall h le h', add_events h le h' -> map_incl h h'.
Proof.
(* Goal: @eq (option B) (map_add a (@fold_right (forall _ : A, option B) (forall _ : A, option B) map_add empty_map l) k) (@Some B v) *)
  intros; apply add_events_add in H as (? & ? & ?); subst.
(* Goal: @map_incl nat hist_el h (@map_add nat hist_el h x) *)
  apply map_incl_add.
Qed.

Corollary add_events_newer : forall h le h' t, add_events h le h' -> newer h' t -> newer h t.
Proof.
(* Goal: forall (P Q : mpred) (n : nat), @eq (@pred rmap ag_rmap) (approx n (weak_view_shift P Q)) (approx n (weak_view_shift P (approx n Q))) *)
  repeat intro.
(* Goal: lt t' t *)
  apply H0.
(* Goal: not (@eq (option hist_el) (h' t') (@None hist_el)) *)
  destruct (h t') eqn: Ht'; [|contradiction].
  eapply add_events_incl in Ht' as ->; eauto.
Qed.

Lemma add_events_in : forall h le h' e, add_events h le h' -> In e le ->
  exists t, newer h t /\ h' t = Some e.
Proof.
(* Goal: forall (h : forall _ : nat, option hist_el) (le : list hist_el) (h' : forall _ : nat, option hist_el) (e : hist_el) (_ : add_events h le h') (_ : @In hist_el e le), @ex nat (fun t : nat => and (newer h t) (@eq (option hist_el) (h' t) (@Some hist_el e))) *)
  induction 1; [contradiction|].
(* Goal: forall _ : @In hist_el e (@app hist_el le (@cons hist_el e0 (@nil hist_el))), @ex nat (fun t0 : nat => and (newer h t0) (@eq (option hist_el) (@map_upd nat hist_el nat_eq_dec h' t e0 t0) (@Some hist_el e))) *)
  rewrite in_app; intros [? | [? | ?]]; try contradiction.
  - destruct IHadd_events as (? & ? & ?); auto.
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
    do 2 eexists; eauto.
(* Goal: @eq (option B) (map_add a (@fold_right (forall _ : A, option B) (forall _ : A, option B) map_add empty_map l) k) (@Some B v) *)
    unfold map_upd; if_tac; auto; subst.
(* Goal: @eq (option hist_el) (@Some hist_el e0) (@Some hist_el e) *)
    specialize (Ht t); rewrite H2 in Ht; lapply Ht; [omega | discriminate].
  - subst; unfold map_upd; do 2 eexists; [|apply eq_dec_refl].
(* Goal: forall (a b c : forall _ : A, option B) (_ : @join (forall _ : A, option B) map_disj_join a b c) (_ : (fun _ : forall _ : A, option B => True) c), (fun _ : forall _ : A, option B => True) a *)
    eapply add_events_newer; eauto.
Qed.

End GHist.

Hint Resolve hist_incl_nil hist_list_nil hist_list'_nil add_events_nil.
(*Hint Resolve ghost_var_precise ghost_var_precise'.*)
Hint Resolve (*ghost_var_init*) master_init (*ghost_map_init*) ghost_hist_init : init.

Ltac ghost_alloc G :=
  match goal with |-semax _ (PROPx ?P (LOCALx ?Q (SEPx ?R))) _ _ =>
    apply (semax_pre_bupd (PROPx P (LOCALx Q (SEPx ((EX g : _, G g) :: R)))));
  [go_lower; rewrite !prop_true_andp by (repeat (split; auto));
   rewrite <- emp_sepcon at 1; eapply derives_trans, bupd_frame_r;
   apply sepcon_derives, derives_refl; apply own_alloc; auto; simpl; auto with init|] end.

Ltac ghosts_alloc G n :=
  match goal with |-semax _ (PROPx ?P (LOCALx ?Q (SEPx ?R))) _ _ =>
    apply (semax_pre_bupd (PROPx P (LOCALx Q (SEPx ((EX lg : _, !!(Zlength lg = n) && iter_sepcon G lg) :: R)))));
  [go_lower; rewrite !prop_true_andp by (repeat (split; auto));
   rewrite <- emp_sepcon at 1; eapply derives_trans, bupd_frame_r;
   apply sepcon_derives, derives_refl; apply own_list_alloc'; auto; simpl; auto with init|] end.

(* weak view shift for use in funspecs *)
(* This could be replaced with P -* |==> Q. *)
Program Definition weak_view_shift (P Q: mpred): mpred :=
  fun w => predicates_hered.derives (approx (S (level w)) P) (own.bupd (approx (S (level w)) Q)).
Next Obligation.
(* Goal: forall (P Q : mpred) (n : nat), @eq (@pred rmap ag_rmap) (approx n (weak_view_shift P Q)) (approx n (weak_view_shift P (approx n Q))) *)
  repeat intro.
(* Goal: @ex ghost (fun b : ghost => and (@joins ghost ghost_join b (ghost_fmap (approx (@level rmap ag_rmap a0)) (approx (@level rmap ag_rmap a0)) c)) (@ex rmap (fun m' : rmap => and (@eq nat (@level rmap ag_rmap m') (@level rmap ag_rmap a0)) (and (@eq (forall _ : AV.address, resource) (resource_at m') (resource_at a0)) (and (@eq ghost (ghost_of m') b) (@app_pred rmap ag_rmap (approx (S (@level rmap ag_rmap a')) Q) m')))))) *)
  destruct H1.
(* Goal: @ex ghost (fun b : ghost => and (@joins ghost ghost_join b (ghost_fmap (approx (@level rmap ag_rmap a0)) (approx (@level rmap ag_rmap a0)) c)) (@ex rmap (fun m' : rmap => and (@eq nat (@level rmap ag_rmap m') (@level rmap ag_rmap a0)) (and (@eq (forall _ : AV.address, resource) (resource_at m') (resource_at a0)) (and (@eq ghost (ghost_of m') b) (@app_pred rmap ag_rmap (approx (S (@level rmap ag_rmap a')) Q) m')))))) *)
  apply age_level in H.
(* Goal: @ex ghost (fun b : ghost => and (@joins ghost ghost_join b (ghost_fmap (approx (@level rmap ag_rmap a0)) (approx (@level rmap ag_rmap a0)) c)) (@ex rmap (fun m' : rmap => and (@eq nat (@level rmap ag_rmap m') (@level rmap ag_rmap a0)) (and (@eq (forall _ : AV.address, resource) (resource_at m') (resource_at a0)) (and (@eq ghost (ghost_of m') b) (@app_pred rmap ag_rmap (approx (S (@level rmap ag_rmap a')) Q) m')))))) *)
  lapply (H0 a0); [|split; auto; omega].
(* Goal: forall _ : @app_pred rmap ag_rmap (own.bupd (approx (S (@level rmap ag_rmap a)) Q)) a0, @ex ghost (fun b : ghost => and (@joins ghost ghost_join b (ghost_fmap (approx (@level rmap ag_rmap a0)) (approx (@level rmap ag_rmap a0)) c)) (@ex rmap (fun m' : rmap => and (@eq nat (@level rmap ag_rmap m') (@level rmap ag_rmap a0)) (and (@eq (forall _ : AV.address, resource) (resource_at m') (resource_at a0)) (and (@eq ghost (ghost_of m') b) (@app_pred rmap ag_rmap (approx (S (@level rmap ag_rmap a')) Q) m')))))) *)
  intro HQ; destruct (HQ _ H2) as (? & ? & ? & ? & ? & ? & []).
  eexists; split; eauto; eexists; split; eauto; repeat split; auto; omega.
Defined.

Lemma view_shift_nonexpansive: forall P Q n,
  approx n (weak_view_shift P Q) = approx n (weak_view_shift (approx n P) (approx n Q)).
Proof.
(* Goal: forall (P Q : mpred) (n : nat), @eq (@pred rmap ag_rmap) (approx n (weak_view_shift P Q)) (approx n (weak_view_shift P (approx n Q))) *)
  apply nonexpansive2_super_non_expansive; repeat intro.
  - split; intros ??%necR_level Hshift ? HP ? J;
      destruct (Hshift _ HP _ J) as (? & ? & m' & ? & ? & ? & []); destruct HP;
      eexists; split; eauto; eexists; split; eauto; repeat split; auto;
      apply (H m'); auto; omega.
  - split; intros ??%necR_level Hshift ? []; apply Hshift; split; auto; apply (H a0); auto; omega.
Qed.

Lemma view_shift_nonexpansive_l: forall P Q n,
  approx n (weak_view_shift P Q) = approx n (weak_view_shift (approx n P) Q).
Proof.
(* Goal: forall (P Q : mpred) (n : nat), @eq (@pred rmap ag_rmap) (approx n (weak_view_shift P Q)) (approx n (weak_view_shift P (approx n Q))) *)
  repeat intro.
(* Goal: forall (P Q : mpred) (n : nat), @eq (@pred rmap ag_rmap) (approx n (weak_view_shift P Q)) (approx n (weak_view_shift P (approx n Q))) *)
  apply (nonexpansive_super_non_expansive (fun P => weak_view_shift P Q)); repeat intro.
  split; intros ??%necR_level Hshift ? []; apply Hshift; split; auto; apply (H a0); auto; omega.
Qed.

Lemma view_shift_nonexpansive_R: forall P Q n,
  approx n (weak_view_shift P Q) = approx n (weak_view_shift P (approx n Q)).
Proof.
(* Goal: forall (P Q : mpred) (n : nat), @eq (@pred rmap ag_rmap) (approx n (weak_view_shift P Q)) (approx n (weak_view_shift P (approx n Q))) *)
  repeat intro.
(* Goal: forall (P Q : mpred) (n : nat), @eq (@pred rmap ag_rmap) (approx n (weak_view_shift P Q)) (approx n (weak_view_shift P (approx n Q))) *)
  apply (nonexpansive_super_non_expansive (fun Q => weak_view_shift P Q)); repeat intro.
  split; intros ??%necR_level Hshift ? HP ? J;
      destruct (Hshift _ HP _ J) as (? & ? & m' & ? & ? & ? & []); destruct HP;
      eexists; split; eauto; eexists; split; eauto; repeat split; auto;
      apply (H m'); auto; omega.
Qed.

Lemma view_shift_weak: forall P Q, P |-- |==> Q -> TT |-- weak_view_shift P Q.
Proof.
(* Goal: forall P Q : mpred, @derives mpred Nveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (weak_view_shift P Q) (@emp mpred Nveric Sveric)) P) (@bupd mpred own.gname preds Nveric Sveric Bveric Q) *)
  intros.
(* Goal: @derives mpred Nveric (@TT mpred Nveric) (weak_view_shift P Q) *)
  change (predicates_hered.derives TT (weak_view_shift P Q)).
(* Goal: @predicates_hered.derives rmap ag_rmap (@TT (@pred rmap ag_rmap) Nveric) (weak_view_shift P Q) *)
  intros w _ ? [? HP] ? 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 (approx (S (@level rmap ag_rmap w)) Q) m')))))) *)
  destruct (H _ HP _ J) as (? & ? & ? & ? & ? & ? & ?).
  eexists; split; eauto; eexists; split; eauto; repeat split; auto; omega.
Qed.

Lemma apply_view_shift: forall P Q, (weak_view_shift P Q && emp) * P |-- |==> Q.
Proof.
(* Goal: forall P Q : mpred, @derives mpred Nveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (weak_view_shift P Q) (@emp mpred Nveric Sveric)) P) (@bupd mpred own.gname preds Nveric Sveric Bveric Q) *)
  intros.
  change (predicates_hered.derives ((weak_view_shift P Q && emp) * P) (own.bupd Q)).
(* Goal: @predicates_hered.derives rmap ag_rmap (@predicates_sl.sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (@predicates_hered.andp rmap ag_rmap (weak_view_shift P Q) (@emp (@pred rmap ag_rmap) Nveric Sveric)) P) (own.bupd Q) *)
  intros ? (? & ? & ? & [Hshift Hemp] & HP) ? 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 Q m')))))) *)
  destruct (join_level _ _ _ H).
(* Goal: @eq (option B) (map_add a (@fold_right (forall _ : A, option B) (forall _ : A, option B) map_add empty_map l) k) (@Some B v) *)
  apply Hemp in H; subst.
(* 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')))))) *)
  lapply (Hshift a); [|split; auto; omega].
(* Goal: forall _ : @app_pred rmap ag_rmap (own.bupd (approx (S (@level rmap ag_rmap x)) Q)) a, @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')))))) *)
  intro X; destruct (X _ J) as (? & ? & ? & ? & ? & ? & []); eauto 7.
Qed.
